A1
:
(
r
"
)
"
<=
0
by
XXREAL_0:def 6
;
assume
A2
:
r
"
>
0
;
:: according to
XXREAL_0:def 6
:: thesis:
contradiction
per
cases
(
(
r
"
)
"
=
0
or
(
r
"
)
"
<
0
)
by
A1
,
Lm4
;
suppose
(
r
"
)
"
=
0
;
:: thesis:
contradiction
hence
contradiction
by
A2
;
:: thesis:
verum
end;
suppose
A3
:
(
r
"
)
"
<
0
;
:: thesis:
contradiction
(
r
"
)
*
(
(
r
"
)
"
)
=
1
by
A2
,
XCMPLX_0:def 7
;
hence
contradiction
by
A2
,
A3
,
Lm8
,
Lm18
;
:: thesis:
verum
end;
end;