let n be Nat; :: thesis: for a, b being non trivial Nat st a <= b holds

( Px (a,n) <= Px (b,n) & Py (a,n) <= Py (b,n) )

let a, b be non trivial Nat; :: thesis: ( a <= b implies ( Px (a,n) <= Px (b,n) & Py (a,n) <= Py (b,n) ) )

assume A1: a <= b ; :: thesis: ( Px (a,n) <= Px (b,n) & Py (a,n) <= Py (b,n) )

defpred S_{1}[ Nat] means ( Px (a,$1) <= Px (b,$1) & Py (a,$1) <= Py (b,$1) );

( Px (a,0) = 1 & Py (a,0) = 0 & Px (b,0) = 1 & Py (b,0) = 0 ) by HILB10_1:3;

then A2: S_{1}[ 0 ]
;

A3: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A2, A3);

hence ( Px (a,n) <= Px (b,n) & Py (a,n) <= Py (b,n) ) ; :: thesis: verum

( Px (a,n) <= Px (b,n) & Py (a,n) <= Py (b,n) )

let a, b be non trivial Nat; :: thesis: ( a <= b implies ( Px (a,n) <= Px (b,n) & Py (a,n) <= Py (b,n) ) )

assume A1: a <= b ; :: thesis: ( Px (a,n) <= Px (b,n) & Py (a,n) <= Py (b,n) )

defpred S

( Px (a,0) = 1 & Py (a,0) = 0 & Px (b,0) = 1 & Py (b,0) = 0 ) by HILB10_1:3;

then A2: S

A3: for k being Nat st S

S

proof

for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A4: S_{1}[k]
; :: thesis: S_{1}[k + 1]

set k1 = k + 1;

A5: ( a * a = a ^2 & b * b = b ^2 ) by SQUARE_1:def 1;

then ( a ^2 >= 1 + 0 & b ^2 >= 1 + 0 ) by NAT_1:13;

then A6: ( (a ^2) -' 1 = (a ^2) - 1 & (b ^2) -' 1 = (b ^2) - 1 ) by XREAL_1:233;

a ^2 <= b ^2 by A5, A1, XREAL_1:66;

then A7: (a ^2) -' 1 <= (b ^2) -' 1 by A6, XREAL_1:9;

( (Px (a,k)) * a <= (Px (b,k)) * b & (Py (a,k)) * ((a ^2) -' 1) <= (Py (b,k)) * ((b ^2) -' 1) ) by A1, A7, A4, XREAL_1:66;

then ( Px (a,(k + 1)) = ((Px (a,k)) * a) + ((Py (a,k)) * ((a ^2) -' 1)) & ((Px (a,k)) * a) + ((Py (a,k)) * ((a ^2) -' 1)) <= ((Px (b,k)) * b) + ((Py (b,k)) * ((b ^2) -' 1)) ) by XREAL_1:7, HILB10_1:6;

hence Px (a,(k + 1)) <= Px (b,(k + 1)) by HILB10_1:6; :: thesis: Py (a,(k + 1)) <= Py (b,(k + 1))

(Py (a,k)) * a <= (Py (b,k)) * b by A1, A4, XREAL_1:66;

then ( Py (a,(k + 1)) = (Px (a,k)) + ((Py (a,k)) * a) & (Px (a,k)) + ((Py (a,k)) * a) <= (Px (b,k)) + ((Py (b,k)) * b) ) by A4, XREAL_1:7, HILB10_1:6;

hence Py (a,(k + 1)) <= Py (b,(k + 1)) by HILB10_1:6; :: thesis: verum

end;assume A4: S

set k1 = k + 1;

A5: ( a * a = a ^2 & b * b = b ^2 ) by SQUARE_1:def 1;

then ( a ^2 >= 1 + 0 & b ^2 >= 1 + 0 ) by NAT_1:13;

then A6: ( (a ^2) -' 1 = (a ^2) - 1 & (b ^2) -' 1 = (b ^2) - 1 ) by XREAL_1:233;

a ^2 <= b ^2 by A5, A1, XREAL_1:66;

then A7: (a ^2) -' 1 <= (b ^2) -' 1 by A6, XREAL_1:9;

( (Px (a,k)) * a <= (Px (b,k)) * b & (Py (a,k)) * ((a ^2) -' 1) <= (Py (b,k)) * ((b ^2) -' 1) ) by A1, A7, A4, XREAL_1:66;

then ( Px (a,(k + 1)) = ((Px (a,k)) * a) + ((Py (a,k)) * ((a ^2) -' 1)) & ((Px (a,k)) * a) + ((Py (a,k)) * ((a ^2) -' 1)) <= ((Px (b,k)) * b) + ((Py (b,k)) * ((b ^2) -' 1)) ) by XREAL_1:7, HILB10_1:6;

hence Px (a,(k + 1)) <= Px (b,(k + 1)) by HILB10_1:6; :: thesis: Py (a,(k + 1)) <= Py (b,(k + 1))

(Py (a,k)) * a <= (Py (b,k)) * b by A1, A4, XREAL_1:66;

then ( Py (a,(k + 1)) = (Px (a,k)) + ((Py (a,k)) * a) & (Px (a,k)) + ((Py (a,k)) * a) <= (Px (b,k)) + ((Py (b,k)) * b) ) by A4, XREAL_1:7, HILB10_1:6;

hence Py (a,(k + 1)) <= Py (b,(k + 1)) by HILB10_1:6; :: thesis: verum

hence ( Px (a,n) <= Px (b,n) & Py (a,n) <= Py (b,n) ) ; :: thesis: verum