let k, n, m 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 Def4
.= m div n by Def3 ;
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: modSeq (m,n) = NAT --> 0 by Th22;
A4: divSeq (m,n) = NAT --> 0 by A2, Th21;
A5: k in NAT by ORDINAL1:def 12;
( k = 0 or ex x being Nat st k = x + 1 ) by NAT_1:6;
hence (scf (m / n)) . k = 0 by A2, Th30
.= (divSeq (m,n)) . k by A4, A5, FUNCOP_1:7 ;
:: 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 A2, Th29
.= ((modSeq (m,n)) . k) / ((modSeq (m,n)) . (k + 1)) by A3, A5, FUNCOP_1:7 ; :: thesis: verum
end;
suppose A6: 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 A7: m / n = (m div n) + ((m mod n) / n) by A6, XCMPLX_1:113;
defpred S2[ 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)) ) );
A8: (rfs (m / n)) . (0 + 1) = 1 / (frac ((rfs (m / n)) . 0)) by Def3
.= 1 / (((rfs (m / n)) . 0) - ((scf (m / n)) . 0)) by Def4
.= 1 / ((m / n) - (m div n)) by A1, Def3
.= n / (m mod n) by A7, XCMPLX_1:57
.= n / ((modSeq (m,n)) . 0) by Def1 ;
A9: S2[ 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, Def2; :: 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;
A10: for a being Nat st S2[a] holds
S2[a + 1]
proof
let a be Nat; :: thesis: ( S2[a] implies S2[a + 1] )
assume A11: S2[a] ; :: thesis: S2[a + 1]
per cases ( a = 0 or a > 0 ) ;
suppose A12: a = 0 ; :: thesis: S2[a + 1]
set x = m mod n;
A13: (scf (m / n)) . (0 + 1) = (scf (1 / (frac (m / n)))) . 0 by Th37
.= [\((rfs (1 / (frac (m / n)))) . 0)/] by Def4
.= [\(1 / (frac (m / n)))/] by Def3
.= [\(1 / ((m mod n) / n))/] by Th6
.= n div (m mod n) by XCMPLX_1:57
.= n div ((modSeq (m,n)) . 0) by Def1
.= (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 A12, NAT_1:25;
hence (scf (m / n)) . i = (divSeq (m,n)) . i by A9, A13; :: 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 A14: ( i + 1 = 0 or i + 1 = 0 + 1 ) by A12, NAT_1:25;
per cases ( m mod n = 0 or 0 < m mod n ) ;
suppose A15: 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 A14
.= 1 / (frac ((rfs (m / n)) . 1)) by Def3
.= 1 / ((n / ((modSeq (m,n)) . 0)) - ((divSeq (m,n)) . 1)) by A8, A13, Def4
.= 1 / ((n / (m mod n)) - ((divSeq (m,n)) . 1)) by Def1
.= 1 / ((n / (m mod n)) - (n div (m mod n))) by Def2
.= 1 / (0 - (n div (m mod n))) by A15
.= 1 / (0 - 0) by A15
.= ((modSeq (m,n)) . i) / 0
.= ((modSeq (m,n)) . i) / (n mod (m mod n)) by A15
.= ((modSeq (m,n)) . i) / ((modSeq (m,n)) . (i + 1)) by A14, Def1 ; :: thesis: verum
end;
suppose A16: 0 < m mod n ; :: thesis: (rfs (m / n)) . (i + 2) = ((modSeq (m,n)) . i) / ((modSeq (m,n)) . (i + 1))
then A17: 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 A18: n mod (m mod n) = 0 ; :: thesis: (rfs (m / n)) . (i + 2) = ((modSeq (m,n)) . i) / ((modSeq (m,n)) . (i + 1))
then A19: n div (m mod n) = n / (m mod n) by Th4;
thus (rfs (m / n)) . (i + 2) = (rfs (m / n)) . (1 + 1) by A14
.= 1 / (frac ((rfs (m / n)) . 1)) by Def3
.= 1 / ((n / ((modSeq (m,n)) . 0)) - ((divSeq (m,n)) . 1)) by A8, A13, Def4
.= 1 / ((n / (m mod n)) - ((divSeq (m,n)) . 1)) by Def1
.= 1 / ((n / (m mod n)) - (n div (m mod n))) by Def2
.= 1 / 0 by A19
.= ((modSeq (m,n)) . i) / (n mod (m mod n)) by A18
.= ((modSeq (m,n)) . i) / ((modSeq (m,n)) . (i + 1)) by A14, Def1 ; :: thesis: verum
end;
suppose A20: n mod (m mod n) <> 0 ; :: thesis: (rfs (m / n)) . (i + 2) = ((modSeq (m,n)) . i) / ((modSeq (m,n)) . (i + 1))
then A21: (n / (m mod n)) - (n div (m mod n)) <> 0 by Th5;
thus (rfs (m / n)) . (i + 2) = (rfs (m / n)) . (1 + 1) by A14
.= 1 / (frac ((rfs (m / n)) . 1)) by Def3
.= 1 / ((n / ((modSeq (m,n)) . 0)) - ((divSeq (m,n)) . 1)) by A8, A13, Def4
.= 1 / ((n / (m mod n)) - ((divSeq (m,n)) . 1)) by Def1
.= 1 / ((n / (m mod n)) - (n div (m mod n))) by Def2
.= (m mod n) / (n mod (m mod n)) by A16, A17, A20, A21, Lm1
.= ((modSeq (m,n)) . i) / (n mod (m mod n)) by A14, Def1
.= ((modSeq (m,n)) . i) / ((modSeq (m,n)) . (i + 1)) by A14, Def1 ; :: thesis: verum
end;
end;
end;
end;
end;
suppose a > 0 ; :: thesis: S2[a + 1]
then A22: 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)) . b1 = (divSeq (m,n)) . b1 )
assume b <= a + 1 ; :: thesis: (scf (m / n)) . b1 = (divSeq (m,n)) . b1
then A24: ( b < a + 1 or b = a + 1 ) by XXREAL_0:1;
per cases ( b <= a or b - 1 = a ) by A24, NAT_1:13;
suppose b <= a ; :: thesis: (scf (m / n)) . b1 = (divSeq (m,n)) . b1
hence (scf (m / n)) . b = (divSeq (m,n)) . b by A11; :: thesis: verum
end;
suppose A25: b - 1 = a ; :: thesis: (scf (m / n)) . b1 = (divSeq (m,n)) . b1
reconsider a2 = a - 1 as Element of NAT by A22, INT_1:5;
A26: b = (a - 1) + 2 by A25;
thus (scf (m / n)) . b = [\((rfs (m / n)) . b)/] by Def4
.= ((modSeq (m,n)) . a2) div ((modSeq (m,n)) . (a2 + 1)) by A11, A26
.= (divSeq (m,n)) . b by A26, Def2 ; :: 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 A27: 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 A27, 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 A11; :: thesis: verum
end;
suppose A28: 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 A22, INT_1:5;
A29: b + 1 = b1 + (1 + 1) ;
A30: b1 + 2 = (b1 + 1) + 1 ;
A31: b + 2 = (b + 1) + 1 ;
per cases ( 0 = (modSeq (m,n)) . (b1 + 1) or 0 < (modSeq (m,n)) . (b1 + 1) ) ;
suppose A32: 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 A31, Th26
.= 1 / (((rfs (m / n)) . (b + 1)) - ((divSeq (m,n)) . (b + 1))) by A23, A28
.= 1 / ((((modSeq (m,n)) . b1) / ((modSeq (m,n)) . (b1 + 1))) - ((divSeq (m,n)) . ((b1 + 1) + 1))) by A11, A28, A29
.= 1 / ((((modSeq (m,n)) . b1) / 0) - (((modSeq (m,n)) . b1) div 0)) by A30, A32, Def2
.= ((modSeq (m,n)) . b) / ((modSeq (m,n)) . (b + 1)) by A32 ; :: thesis: verum
end;
suppose A33: 0 < (modSeq (m,n)) . (b1 + 1) ; :: thesis: (rfs (m / n)) . (b + 2) = ((modSeq (m,n)) . b) / ((modSeq (m,n)) . (b + 1))
then A34: ((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 A35: ((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 A36: (((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 A31, Th26
.= 1 / (((rfs (m / n)) . (b + 1)) - ((divSeq (m,n)) . (b + 1))) by A23, A28
.= 1 / ((((modSeq (m,n)) . b1) / ((modSeq (m,n)) . (b1 + 1))) - ((divSeq (m,n)) . ((b1 + 1) + 1))) by A11, A28, A29
.= 1 / 0 by A30, A36, Def2
.= ((modSeq (m,n)) . (b1 + 1)) / (((modSeq (m,n)) . b1) mod ((modSeq (m,n)) . (b1 + 1))) by A35
.= ((modSeq (m,n)) . b) / ((modSeq (m,n)) . (b + 1)) by A30, Def1 ; :: thesis: verum
end;
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 A38: (((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 A31, Th26
.= 1 / (((rfs (m / n)) . (b + 1)) - ((divSeq (m,n)) . (b + 1))) by A23, A28
.= 1 / ((((modSeq (m,n)) . b1) / ((modSeq (m,n)) . (b1 + 1))) - ((divSeq (m,n)) . ((b1 + 1) + 1))) by A11, A28, A29
.= 1 / ((((modSeq (m,n)) . b1) / ((modSeq (m,n)) . (b1 + 1))) - (((modSeq (m,n)) . b1) div ((modSeq (m,n)) . (b1 + 1)))) by A30, Def2
.= ((modSeq (m,n)) . (b1 + 1)) / (((modSeq (m,n)) . b1) mod ((modSeq (m,n)) . (b1 + 1))) by A33, A34, A37, A38, Lm1
.= ((modSeq (m,n)) . b) / ((modSeq (m,n)) . (b + 1)) by A30, Def1 ; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
end;
for a being Nat holds S2[a] from NAT_1:sch 2(A9, A10);
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 A8; :: thesis: verum
end;
end;