let
a
,
b
be
Real
;
:: thesis:
(
a
>=
0
implies
sqrt
(
a
+
(
b
^2
)
)
>=
b
)
assume
A1
:
a
>=
0
;
:: thesis:
sqrt
(
a
+
(
b
^2
)
)
>=
b
per
cases
(
b
<
0
or
b
>=
0
)
;
suppose
b
<
0
;
:: thesis:
sqrt
(
a
+
(
b
^2
)
)
>=
b
hence
sqrt
(
a
+
(
b
^2
)
)
>=
b
by
A1
,
Def2
;
:: thesis:
verum
end;
suppose
A2
:
b
>=
0
;
:: thesis:
sqrt
(
a
+
(
b
^2
)
)
>=
b
A3
:
b
^2
>=
0
by
XREAL_1:63
;
a
+
(
b
^2
)
>=
0
+
(
b
^2
)
by
A1
,
XREAL_1:6
;
then
sqrt
(
a
+
(
b
^2
)
)
>=
sqrt
(
b
^2
)
by
A3
,
Th26
;
hence
sqrt
(
a
+
(
b
^2
)
)
>=
b
by
A2
,
Def2
;
:: thesis:
verum
end;
end;