let m, D be natural positive Number ; :: thesis: for a, b being Nat st a < b holds
( ((exampleSierpinski150 (m,D)) . a) `1 < ((exampleSierpinski150 (m,D)) . b) `1 & ((exampleSierpinski150 (m,D)) . a) `2 < ((exampleSierpinski150 (m,D)) . b) `2 )
let a, b be Nat; :: thesis: ( a < b implies ( ((exampleSierpinski150 (m,D)) . a) `1 < ((exampleSierpinski150 (m,D)) . b) `1 & ((exampleSierpinski150 (m,D)) . a) `2 < ((exampleSierpinski150 (m,D)) . b) `2 ) )
assume A1: a < b ; :: thesis: ( ((exampleSierpinski150 (m,D)) . a) `1 < ((exampleSierpinski150 (m,D)) . b) `1 & ((exampleSierpinski150 (m,D)) . a) `2 < ((exampleSierpinski150 (m,D)) . b) `2 )
set f = exampleSierpinski150 (m,D);
defpred S₁[ Nat] means ( $1 > a implies ( ((exampleSierpinski150 (m,D)) . $1) `1 > ((exampleSierpinski150 (m,D)) . a) `1 & ((exampleSierpinski150 (m,D)) . $1) `2 > ((exampleSierpinski150 (m,D)) . a) `2 ) );
A2: S₁[ 0 ] ;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A4: S₁[k] and
A5: k + 1 > a ; :: thesis: ( ((exampleSierpinski150 (m,D)) . (k + 1)) `1 > ((exampleSierpinski150 (m,D)) . a) `1 & ((exampleSierpinski150 (m,D)) . (k + 1)) `2 > ((exampleSierpinski150 (m,D)) . a) `2 )
A6: (exampleSierpinski150 (m,D)) . (k + 1) = [(((((exampleSierpinski150 (m,D)) . k) `1) ^2) + (D * ((((exampleSierpinski150 (m,D)) . k) `2) ^2))),((2 * (((exampleSierpinski150 (m,D)) . k) `1)) * (((exampleSierpinski150 (m,D)) . k) `2))] by Def19;
A7: ((exampleSierpinski150 (m,D)) . k) `1 >= 0 + 1 by NAT_1:13;
then 2 * (((exampleSierpinski150 (m,D)) . k) `1) >= 2 * 1 by XREAL_1:64;
then A8: 2 * (((exampleSierpinski150 (m,D)) . k) `1) > 1 by XXREAL_0:2;
A9: (((exampleSierpinski150 (m,D)) . k) `1) ^2 >= 1 * (((exampleSierpinski150 (m,D)) . k) `1) by A7, XREAL_1:64;
k >= a by A5, NAT_1:13;

per cases then ( k > a or k = a ) by XXREAL_0:1;

suppose A10: k > a ; :: thesis: ( ((exampleSierpinski150 (m,D)) . (k + 1)) `1 > ((exampleSierpinski150 (m,D)) . a) `1 & ((exampleSierpinski150 (m,D)) . (k + 1)) `2 > ((exampleSierpinski150 (m,D)) . a) `2 )

((((exampleSierpinski150 (m,D)) . k) `1) ^2) + (D * ((((exampleSierpinski150 (m,D)) . k) `2) ^2)) >= (((exampleSierpinski150 (m,D)) . k) `1) + 0 by A9, XREAL_1:7;
hence ((exampleSierpinski150 (m,D)) . (k + 1)) `1 > ((exampleSierpinski150 (m,D)) . a) `1 by A4, A6, A10, XXREAL_0:2; :: thesis: ((exampleSierpinski150 (m,D)) . (k + 1)) `2 > ((exampleSierpinski150 (m,D)) . a) `2
(2 * (((exampleSierpinski150 (m,D)) . k) `1)) * (((exampleSierpinski150 (m,D)) . k) `2) >= (((exampleSierpinski150 (m,D)) . k) `2) * 1 by A8, XREAL_1:68;
hence ((exampleSierpinski150 (m,D)) . (k + 1)) `2 > ((exampleSierpinski150 (m,D)) . a) `2 by A4, A6, A10, XXREAL_0:2; :: thesis: verum

end;

suppose A11: k = a ; :: thesis: ( ((exampleSierpinski150 (m,D)) . (k + 1)) `1 > ((exampleSierpinski150 (m,D)) . a) `1 & ((exampleSierpinski150 (m,D)) . (k + 1)) `2 > ((exampleSierpinski150 (m,D)) . a) `2 )

((((exampleSierpinski150 (m,D)) . k) `1) ^2) + (D * ((((exampleSierpinski150 (m,D)) . k) `2) ^2)) > (((exampleSierpinski150 (m,D)) . k) `1) + 0 by A9, XREAL_1:8;
hence ((exampleSierpinski150 (m,D)) . (k + 1)) `1 > ((exampleSierpinski150 (m,D)) . a) `1 by A6, A11; :: thesis: ((exampleSierpinski150 (m,D)) . (k + 1)) `2 > ((exampleSierpinski150 (m,D)) . a) `2
(2 * (((exampleSierpinski150 (m,D)) . k) `1)) * (((exampleSierpinski150 (m,D)) . k) `2) > 1 * (((exampleSierpinski150 (m,D)) . k) `2) by A8, XREAL_1:68;
hence ((exampleSierpinski150 (m,D)) . (k + 1)) `2 > ((exampleSierpinski150 (m,D)) . a) `2 by A6, A11; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
hence ( ((exampleSierpinski150 (m,D)) . a) `1 < ((exampleSierpinski150 (m,D)) . b) `1 & ((exampleSierpinski150 (m,D)) . a) `2 < ((exampleSierpinski150 (m,D)) . b) `2 ) by A1; :: thesis: verum