let a, x be Nat; ( a >= 1 & ((a + 1) |^ 2) + (((a + 1) + x) |^ 2) <= (((a + 1) + x) + 1) |^ 2 implies (a |^ 2) + ((a + x) |^ 2) < ((a + x) + 1) |^ 2 )
A2: ((a + x) + 1) |^ 2 =
(((((a |^ 2) + (x |^ 2)) + (1 |^ 2)) + ((2 * a) * x)) + ((2 * a) * 1)) + ((2 * x) * 1)
by SERIES_4:1
.=
(((((a |^ 2) + (x |^ 2)) + ((2 * a) * x)) + (2 * x)) + (2 * a)) + 1
;
A3: ((a + x) + 2) |^ 2 =
(((((a |^ 2) + (x |^ 2)) + (2 |^ 2)) + ((2 * a) * x)) + ((2 * a) * 2)) + ((2 * x) * 2)
by SERIES_4:1
.=
(((((((2 * a) * 2) + (2 * x)) + (2 * x)) + (2 |^ 2)) + (a |^ 2)) + ((2 * a) * x)) + (x |^ 2)
;
A4:
(a + x) |^ 2 = ((a |^ 2) + ((2 * a) * x)) + (x |^ 2)
by Lm10;
assume A5:
( a >= 1 & ((a + 1) |^ 2) + (((a + 1) + x) |^ 2) <= (((a + 1) + x) + 1) |^ 2 )
; (a |^ 2) + ((a + x) |^ 2) < ((a + x) + 1) |^ 2
then A5a:
(((a + 1) |^ 2) + (((a + x) + 1) |^ 2)) - (((a + x) + 2) |^ 2) <= (((a + x) + 2) |^ 2) - (((a + x) + 2) |^ 2)
by XREAL_1:9;
- ((((a + 1) |^ 2) + (((a + x) + 1) |^ 2)) - (((a + x) + 2) |^ 2)) =
(((a + x) + 2) |^ 2) - (((a + 1) |^ 2) + (((a + x) + 1) |^ 2))
.=
(((((((a |^ 2) + (x |^ 2)) + (2 |^ 2)) + ((2 * a) * x)) + ((2 * 2) * a)) + (2 * x)) + (2 * x)) - ((((a |^ 2) + (2 * a)) + 1) + ((((((a |^ 2) + (x |^ 2)) + (1 |^ 2)) + ((2 * a) * x)) + ((2 * a) * 1)) + ((2 * x) * 1)))
by Lm10, A2, A3
.=
((((2 |^ 2) + (2 * x)) - 1) - (a |^ 2)) - (1 * 1)
.=
((((2 * 2) + (2 * x)) - 1) - (a |^ 2)) - 1
by WSIERP_1:1
;
then A6:
((a |^ 2) + ((a + x) |^ 2)) + 0 <= ((a |^ 2) + ((a + x) |^ 2)) + (((4 + (2 * x)) - (a |^ 2)) - 2)
by A5a, XREAL_1:6;
A7:
( a + 1 > 0 + 1 & a + 1 >= 1 + 1 )
by A5, XREAL_1:6;
then
a + (a + 1) > a + (1 + 0)
by XREAL_1:6;
then
(2 * a) + 1 > 1 + 1
by A7, XXREAL_0:2;
then
((((a |^ 2) + (x |^ 2)) + ((2 * a) * x)) + (2 * x)) + ((2 * a) + 1) > ((((a |^ 2) + (x |^ 2)) + ((2 * a) * x)) + (2 * x)) + 2
by XREAL_1:6;
hence
(a |^ 2) + ((a + x) |^ 2) < ((a + x) + 1) |^ 2
by A2, A4, A6, XXREAL_0:2; verum