let m, n, k be Nat; :: thesis: ( (scf (m / n)) . k = (divSeq m,n) . k & (rfs (m / n)) . 1 = n / ((modSeq m,n) . 0 ) & (rfs (m / n)) . (k + 2) = ((modSeq m,n) . k) / ((modSeq m,n) . (k + 1)) )
set fd = divSeq m,n;
set fm = modSeq m,n;
set r = m / n;
A1: (scf (m / n)) . 0 = [\((rfs (m / n)) . 0 )/] by Def5
.= m div n by Def4 ;

per cases ( n = 0 or 0 < n ) ;

suppose A2: n = 0 ; :: thesis: ( (scf (m / n)) . k = (divSeq m,n) . k & (rfs (m / n)) . 1 = n / ((modSeq m,n) . 0 ) & (rfs (m / n)) . (k + 2) = ((modSeq m,n) . k) / ((modSeq m,n) . (k + 1)) )

then A3: m / n = 0 ;
A4: divSeq m,n = NAT --> 0 by A2, Th21;
A5: modSeq m,n = NAT --> 0 by A2, Th22;
A6: k in NAT by ORDINAL1:def 13;
( k = 0 or ex x being Nat st k = x + 1 ) by NAT_1:6;
hence (scf (m / n)) . k = 0 by A3, Th30
.= (divSeq m,n) . k by A4, A6, FUNCOP_1:13 ;
:: thesis: ( (rfs (m / n)) . 1 = n / ((modSeq m,n) . 0 ) & (rfs (m / n)) . (k + 2) = ((modSeq m,n) . k) / ((modSeq m,n) . (k + 1)) )
thus (rfs (m / n)) . 1 = (rfs (m / n)) . (0 + 1)
.= n / ((modSeq m,n) . 0 ) by A2, Th29 ; :: thesis: (rfs (m / n)) . (k + 2) = ((modSeq m,n) . k) / ((modSeq m,n) . (k + 1))
thus (rfs (m / n)) . (k + 2) = (rfs (m / n)) . ((k + 1) + 1)
.= 0 / ((modSeq m,n) . (k + 1)) by A3, Th29
.= ((modSeq m,n) . k) / ((modSeq m,n) . (k + 1)) by A5, A6, FUNCOP_1:13 ; :: thesis: verum

end;

suppose A7: 0 < n ; :: thesis: ( (scf (m / n)) . k = (divSeq m,n) . k & (rfs (m / n)) . 1 = n / ((modSeq m,n) . 0 ) & (rfs (m / n)) . (k + 2) = ((modSeq m,n) . k) / ((modSeq m,n) . (k + 1)) )

then m = (n * (m div n)) + (m mod n) by NAT_D:2;
then A8: m / n = (m div n) + ((m mod n) / n) by A7, XCMPLX_1:114;
A9: (rfs (m / n)) . (0 + 1) = 1 / (frac ((rfs (m / n)) . 0 )) by Def4
.= 1 / (((rfs (m / n)) . 0 ) - ((scf (m / n)) . 0 )) by Def5
.= 1 / ((m / n) - (m div n)) by A1, Def4
.= n / (m mod n) by A8, XCMPLX_1:57
.= n / ((modSeq m,n) . 0 ) by Def2 ;
defpred S₂[ Nat] means ( ( for i being Nat st i <= $1 holds
(scf (m / n)) . i = (divSeq m,n) . i ) & ( for i being Nat st i + 1 <= $1 holds
(rfs (m / n)) . (i + 2) = ((modSeq m,n) . i) / ((modSeq m,n) . (i + 1)) ) );
A10: S₂[ 0 ]

proof

hereby :: thesis: for i being Nat st i + 1 <= 0 holds
(rfs (m / n)) . (i + 2) = ((modSeq m,n) . i) / ((modSeq m,n) . (i + 1))

let i be Nat; :: thesis: ( i <= 0 implies (scf (m / n)) . i = (divSeq m,n) . i )
assume i <= 0 ; :: thesis: (scf (m / n)) . i = (divSeq m,n) . i
then i = 0 ;
hence (scf (m / n)) . i = (divSeq m,n) . i by A1, Def3; :: thesis: verum

end;

let i be Nat; :: thesis: ( i + 1 <= 0 implies (rfs (m / n)) . (i + 2) = ((modSeq m,n) . i) / ((modSeq m,n) . (i + 1)) )
assume i + 1 <= 0 ; :: thesis: (rfs (m / n)) . (i + 2) = ((modSeq m,n) . i) / ((modSeq m,n) . (i + 1))
hence (rfs (m / n)) . (i + 2) = ((modSeq m,n) . i) / ((modSeq m,n) . (i + 1)) ; :: thesis: verum

end;

A11: for a being Nat st S₂[a] holds
S₂[a + 1]

proof

let a be Nat; :: thesis: ( S₂[a] implies S₂[a + 1] )
assume A12: S₂[a] ; :: thesis: S₂[a + 1]

per cases ( a = 0 or a > 0 ) ;

suppose A13: a = 0 ; :: thesis: S₂[a + 1]

A14: (scf (m / n)) . (0 + 1) = (scf (1 / (frac (m / n)))) . 0 by Th37
.= [\((rfs (1 / (frac (m / n)))) . 0 )/] by Def5
.= [\(1 / (frac (m / n)))/] by Def4
.= [\(1 / ((m mod n) / n))/] by Th6
.= n div (m mod n) by XCMPLX_1:57
.= n div ((modSeq m,n) . 0 ) by Def2
.= (divSeq m,n) . 1 by Th12 ;

hereby :: thesis: for i being Nat st i + 1 <= a + 1 holds
(rfs (m / n)) . (i + 2) = ((modSeq m,n) . i) / ((modSeq m,n) . (i + 1))

let i be Nat; :: thesis: ( i <= a + 1 implies (scf (m / n)) . i = (divSeq m,n) . i )
assume i <= a + 1 ; :: thesis: (scf (m / n)) . i = (divSeq m,n) . i
then ( i = 0 or i = 1 ) by A13, NAT_1:26;
hence (scf (m / n)) . i = (divSeq m,n) . i by A10, A14; :: thesis: verum

end;

let i be Nat; :: thesis: ( i + 1 <= a + 1 implies (rfs (m / n)) . (i + 2) = ((modSeq m,n) . i) / ((modSeq m,n) . (i + 1)) )
assume i + 1 <= a + 1 ; :: thesis: (rfs (m / n)) . (i + 2) = ((modSeq m,n) . i) / ((modSeq m,n) . (i + 1))
then A15: ( i + 1 = 0 or i + 1 = 0 + 1 ) by A13, NAT_1:26;
set x = m mod n;

per cases ( m mod n = 0 or 0 < m mod n ) ;

suppose A16: m mod n = 0 ; :: thesis: (rfs (m / n)) . (i + 2) = ((modSeq m,n) . i) / ((modSeq m,n) . (i + 1))

thus (rfs (m / n)) . (i + 2) = (rfs (m / n)) . (1 + 1) by A15
.= 1 / (frac ((rfs (m / n)) . 1)) by Def4
.= 1 / ((n / ((modSeq m,n) . 0 )) - ((divSeq m,n) . 1)) by A9, A14, Def5
.= 1 / ((n / (m mod n)) - ((divSeq m,n) . 1)) by Def2
.= 1 / ((n / (m mod n)) - (n div (m mod n))) by Def3
.= 1 / (0 - (n div (m mod n))) by A16
.= 1 / (0 - 0 ) by A16
.= ((modSeq m,n) . i) / 0
.= ((modSeq m,n) . i) / (n mod (m mod n)) by A16
.= ((modSeq m,n) . i) / ((modSeq m,n) . (i + 1)) by A15, Def2 ; :: thesis: verum

end;

suppose A17: 0 < m mod n ; :: thesis: (rfs (m / n)) . (i + 2) = ((modSeq m,n) . i) / ((modSeq m,n) . (i + 1))

then A18: n + 0 = ((m mod n) * (n div (m mod n))) + (n mod (m mod n)) by NAT_D:2;

per cases ( n mod (m mod n) = 0 or n mod (m mod n) <> 0 ) ;

suppose A19: n mod (m mod n) = 0 ; :: thesis: (rfs (m / n)) . (i + 2) = ((modSeq m,n) . i) / ((modSeq m,n) . (i + 1))

then A20: n div (m mod n) = n / (m mod n) by Th4;
thus (rfs (m / n)) . (i + 2) = (rfs (m / n)) . (1 + 1) by A15
.= 1 / (frac ((rfs (m / n)) . 1)) by Def4
.= 1 / ((n / ((modSeq m,n) . 0 )) - ((divSeq m,n) . 1)) by A9, A14, Def5
.= 1 / ((n / (m mod n)) - ((divSeq m,n) . 1)) by Def2
.= 1 / ((n / (m mod n)) - (n div (m mod n))) by Def3
.= 1 / 0 by A20
.= ((modSeq m,n) . i) / (n mod (m mod n)) by A19
.= ((modSeq m,n) . i) / ((modSeq m,n) . (i + 1)) by A15, Def2 ; :: thesis: verum

end;

suppose A21: n mod (m mod n) <> 0 ; :: thesis: (rfs (m / n)) . (i + 2) = ((modSeq m,n) . i) / ((modSeq m,n) . (i + 1))

then A22: (n / (m mod n)) - (n div (m mod n)) <> 0 by Th5;
thus (rfs (m / n)) . (i + 2) = (rfs (m / n)) . (1 + 1) by A15
.= 1 / (frac ((rfs (m / n)) . 1)) by Def4
.= 1 / ((n / ((modSeq m,n) . 0 )) - ((divSeq m,n) . 1)) by A9, A14, Def5
.= 1 / ((n / (m mod n)) - ((divSeq m,n) . 1)) by Def2
.= 1 / ((n / (m mod n)) - (n div (m mod n))) by Def3
.= (m mod n) / (n mod (m mod n)) by A17, A18, A21, A22, Lm2
.= ((modSeq m,n) . i) / (n mod (m mod n)) by A15, Def2
.= ((modSeq m,n) . i) / ((modSeq m,n) . (i + 1)) by A15, Def2 ; :: thesis: verum

end;

end;

end;

end;

end;

suppose a > 0 ; :: thesis: S₂[a + 1]

then A23: 0 + 1 <= a by NAT_1:13;

hereby :: thesis: for i being Nat st i + 1 <= a + 1 holds
(rfs (m / n)) . (i + 2) = ((modSeq m,n) . i) / ((modSeq m,n) . (i + 1))

let b be Nat; :: thesis: ( b <= a + 1 implies (scf (m / n)) . b₁ = (divSeq m,n) . b₁ )
assume A25: b <= a + 1 ; :: thesis: (scf (m / n)) . b₁ = (divSeq m,n) . b₁
A26: ( b < a + 1 or b = a + 1 ) by A25, XXREAL_0:1;

per cases ( b <= a or b - 1 = a ) by A26, NAT_1:13;

suppose b <= a ; :: thesis: (scf (m / n)) . b₁ = (divSeq m,n) . b₁

hence (scf (m / n)) . b = (divSeq m,n) . b by A12; :: thesis: verum

end;

suppose A27: b - 1 = a ; :: thesis: (scf (m / n)) . b₁ = (divSeq m,n) . b₁

reconsider a2 = a - 1 as Element of NAT by A23, INT_1:18;
A28: b = (a - 1) + 2 by A27;
thus (scf (m / n)) . b = [\((rfs (m / n)) . b)/] by Def5
.= ((modSeq m,n) . a2) div ((modSeq m,n) . (a2 + 1)) by A12, A28
.= (divSeq m,n) . b by A28, Def3 ; :: thesis: verum

end;

end;

end;

let b be Nat; :: thesis: ( b + 1 <= a + 1 implies (rfs (m / n)) . (b + 2) = ((modSeq m,n) . b) / ((modSeq m,n) . (b + 1)) )
assume A29: b + 1 <= a + 1 ; :: thesis: (rfs (m / n)) . (b + 2) = ((modSeq m,n) . b) / ((modSeq m,n) . (b + 1))

per cases ( b + 1 < a + 1 or b + 1 = a + 1 ) by A29, XXREAL_0:1;

suppose b + 1 < a + 1 ; :: thesis: (rfs (m / n)) . (b + 2) = ((modSeq m,n) . b) / ((modSeq m,n) . (b + 1))

then b + 1 <= a by NAT_1:13;
hence (rfs (m / n)) . (b + 2) = ((modSeq m,n) . b) / ((modSeq m,n) . (b + 1)) by A12; :: thesis: verum

end;

suppose A30: b + 1 = a + 1 ; :: thesis: (rfs (m / n)) . (b + 2) = ((modSeq m,n) . b) / ((modSeq m,n) . (b + 1))

then reconsider b1 = b - 1 as Element of NAT by A23, INT_1:18;
A31: b + 1 = b1 + (1 + 1) ;
A32: b1 + 2 = (b1 + 1) + 1 ;
A33: b + 2 = (b + 1) + 1 ;

per cases ( 0 = (modSeq m,n) . (b1 + 1) or 0 < (modSeq m,n) . (b1 + 1) ) ;

suppose A34: 0 = (modSeq m,n) . (b1 + 1) ; :: thesis: (rfs (m / n)) . (b + 2) = ((modSeq m,n) . b) / ((modSeq m,n) . (b + 1))

thus (rfs (m / n)) . (b + 2) = 1 / (((rfs (m / n)) . (b + 1)) - ((scf (m / n)) . (b + 1))) by A33, Th26
.= 1 / (((rfs (m / n)) . (b + 1)) - ((divSeq m,n) . (b + 1))) by A24, A30
.= 1 / ((((modSeq m,n) . b1) / ((modSeq m,n) . (b1 + 1))) - ((divSeq m,n) . ((b1 + 1) + 1))) by A12, A30, A31
.= 1 / ((((modSeq m,n) . b1) / 0 ) - (((modSeq m,n) . b1) div 0 )) by A32, A34, Def3
.= ((modSeq m,n) . b) / ((modSeq m,n) . (b + 1)) by A34 ; :: thesis: verum

end;

suppose A35: 0 < (modSeq m,n) . (b1 + 1) ; :: thesis: (rfs (m / n)) . (b + 2) = ((modSeq m,n) . b) / ((modSeq m,n) . (b + 1))

then A36: ((modSeq m,n) . b1) + 0 = (((modSeq m,n) . (b1 + 1)) * (((modSeq m,n) . b1) div ((modSeq m,n) . (b1 + 1)))) + (((modSeq m,n) . b1) mod ((modSeq m,n) . (b1 + 1))) by NAT_D:2;

per cases ( ((modSeq m,n) . b1) mod ((modSeq m,n) . (b1 + 1)) = 0 or ((modSeq m,n) . b1) mod ((modSeq m,n) . (b1 + 1)) <> 0 ) ;

suppose A37: ((modSeq m,n) . b1) mod ((modSeq m,n) . (b1 + 1)) = 0 ; :: thesis: (rfs (m / n)) . (b + 2) = ((modSeq m,n) . b) / ((modSeq m,n) . (b + 1))

then ((modSeq m,n) . b1) / ((modSeq m,n) . (b1 + 1)) = ((modSeq m,n) . b1) div ((modSeq m,n) . (b1 + 1)) by Th4;
then A38: (((modSeq m,n) . b1) / ((modSeq m,n) . (b1 + 1))) - (((modSeq m,n) . b1) div ((modSeq m,n) . (b1 + 1))) = 0 ;
thus (rfs (m / n)) . (b + 2) = 1 / (((rfs (m / n)) . (b + 1)) - ((scf (m / n)) . (b + 1))) by A33, Th26
.= 1 / (((rfs (m / n)) . (b + 1)) - ((divSeq m,n) . (b + 1))) by A24, A30
.= 1 / ((((modSeq m,n) . b1) / ((modSeq m,n) . (b1 + 1))) - ((divSeq m,n) . ((b1 + 1) + 1))) by A12, A30, A31
.= 1 / 0 by A32, A38, Def3
.= ((modSeq m,n) . (b1 + 1)) / (((modSeq m,n) . b1) mod ((modSeq m,n) . (b1 + 1))) by A37
.= ((modSeq m,n) . b) / ((modSeq m,n) . (b + 1)) by A32, Def2 ; :: thesis: verum

end;

suppose A39: ((modSeq m,n) . b1) mod ((modSeq m,n) . (b1 + 1)) <> 0 ; :: thesis: (rfs (m / n)) . (b + 2) = ((modSeq m,n) . b) / ((modSeq m,n) . (b + 1))

then A40: (((modSeq m,n) . b1) / ((modSeq m,n) . (b1 + 1))) - (((modSeq m,n) . b1) div ((modSeq m,n) . (b1 + 1))) <> 0 by Th5;
thus (rfs (m / n)) . (b + 2) = 1 / (((rfs (m / n)) . (b + 1)) - ((scf (m / n)) . (b + 1))) by A33, Th26
.= 1 / (((rfs (m / n)) . (b + 1)) - ((divSeq m,n) . (b + 1))) by A24, A30
.= 1 / ((((modSeq m,n) . b1) / ((modSeq m,n) . (b1 + 1))) - ((divSeq m,n) . ((b1 + 1) + 1))) by A12, A30, A31
.= 1 / ((((modSeq m,n) . b1) / ((modSeq m,n) . (b1 + 1))) - (((modSeq m,n) . b1) div ((modSeq m,n) . (b1 + 1)))) by A32, Def3
.= ((modSeq m,n) . (b1 + 1)) / (((modSeq m,n) . b1) mod ((modSeq m,n) . (b1 + 1))) by A35, A36, A39, A40, Lm2
.= ((modSeq m,n) . b) / ((modSeq m,n) . (b + 1)) by A32, Def2 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

for a being Nat holds S₂[a] from NAT_1:sch 2(A10, A11);
hence ( (scf (m / n)) . k = (divSeq m,n) . k & (rfs (m / n)) . 1 = n / ((modSeq m,n) . 0 ) & (rfs (m / n)) . (k + 2) = ((modSeq m,n) . k) / ((modSeq m,n) . (k + 1)) ) by A9; :: thesis: verum

end;

end;