:: REAL_3 semantic presentation begin Lm1: now__::_thesis:_for_n_being_Nat_st_n_>_1_holds_ n_-_1_is_Nat let n be Nat; ::_thesis: ( n > 1 implies n - 1 is Nat ) assume n > 1 ; ::_thesis: n - 1 is Nat then n - 1 > 1 - 1 by XREAL_1:14; then n - 1 in NAT by INT_1:3; hence n - 1 is Nat ; ::_thesis: verum end; Lm2: for a, b, c, d being real number st (a / b) - c <> 0 & d <> 0 & b <> 0 & a = (b * c) + d holds 1 / ((a / b) - c) = b / d proof let a, b, c, d be real number ; ::_thesis: ( (a / b) - c <> 0 & d <> 0 & b <> 0 & a = (b * c) + d implies 1 / ((a / b) - c) = b / d ) assume that A1: ( (a / b) - c <> 0 & d <> 0 ) and A2: b <> 0 ; ::_thesis: ( not a = (b * c) + d or 1 / ((a / b) - c) = b / d ) assume a = (b * c) + d ; ::_thesis: 1 / ((a / b) - c) = b / d then d = b * ((a - (b * c)) / b) by A2, XCMPLX_1:87 .= b * ((a / b) - ((b * c) / b)) ; then 1 * d = b * ((a / b) - c) by A2, XCMPLX_1:89; hence 1 / ((a / b) - c) = b / d by A1, XCMPLX_1:94; ::_thesis: verum end; registration let n be Nat; clustern div 0 -> zero ; coherence n div 0 is zero by NAT_D:def_1; clustern mod 0 -> zero ; coherence n mod 0 is zero by NAT_D:def_2; cluster0 div n -> zero ; coherence 0 div n is zero by NAT_2:2; cluster0 mod n -> zero ; coherence 0 mod n is zero by NAT_D:26; end; registration let c be complex number ; clusterc - c -> zero ; coherence c - c is zero by XCMPLX_1:14; clusterc / 0 -> zero ; coherence c / 0 is zero ; end; registration cluster[\0/] -> zero ; coherence [\0/] is zero by INT_1:25; end; theorem Th1: :: REAL_3:1 for r being real number st 0 < r & r < 1 holds 1 < 1 / r proof let r be real number ; ::_thesis: ( 0 < r & r < 1 implies 1 < 1 / r ) assume that A1: 0 < r and A2: r < 1 ; ::_thesis: 1 < 1 / r 1 * (r ") > r * (r ") by A1, A2, XREAL_1:68; hence 1 < 1 / r by A1, XCMPLX_0:def_7; ::_thesis: verum end; theorem Th2: :: REAL_3:2 for i being Integer for r being real number st i <= r & r < i + 1 holds [\r/] = i proof let i be Integer; ::_thesis: for r being real number st i <= r & r < i + 1 holds [\r/] = i let r be real number ; ::_thesis: ( i <= r & r < i + 1 implies [\r/] = i ) assume A1: i <= r ; ::_thesis: ( not r < i + 1 or [\r/] = i ) assume r < i + 1 ; ::_thesis: [\r/] = i then r - 1 < (i + 1) - 1 by XREAL_1:14; hence [\r/] = i by A1, INT_1:def_6; ::_thesis: verum end; theorem :: REAL_3:3 for m, n being Nat holds [\(m / n)/] = m div n ; theorem Th4: :: REAL_3:4 for m, n being Nat st m mod n = 0 holds m / n = m div n proof let m, n be Nat; ::_thesis: ( m mod n = 0 implies m / n = m div n ) reconsider i = m as Integer ; assume A1: m mod n = 0 ; ::_thesis: m / n = m div n percases ( n = 0 or n <> 0 ) ; supposeA2: n = 0 ; ::_thesis: m / n = m div n hence m / n = 0 .= m div n by A2 ; ::_thesis: verum end; supposeA3: n <> 0 ; ::_thesis: m / n = m div n then i - ((i div n) * n) = 0 by A1, INT_1:def_10; hence m / n = m div n by A3, XCMPLX_1:89; ::_thesis: verum end; end; end; theorem Th5: :: REAL_3:5 for m, n being Nat st m / n = m div n holds m mod n = 0 proof let m, n be Nat; ::_thesis: ( m / n = m div n implies m mod n = 0 ) assume A1: m / n = m div n ; ::_thesis: m mod n = 0 percases ( n = 0 or n > 0 ) ; suppose n = 0 ; ::_thesis: m mod n = 0 hence m mod n = 0 ; ::_thesis: verum end; supposeA2: n > 0 ; ::_thesis: m mod n = 0 then m + 0 = (n * (m / n)) + (m mod n) by A1, NAT_D:2; then (m mod n) - 0 = m - (n * (m / n)) ; hence m mod n = m - m by A2, XCMPLX_1:87 .= 0 ; ::_thesis: verum end; end; end; theorem Th6: :: REAL_3:6 for m, n being Nat holds frac (m / n) = (m mod n) / n proof let m, n be Nat; ::_thesis: frac (m / n) = (m mod n) / n percases ( n = 0 or n > 0 ) ; supposeA1: n = 0 ; ::_thesis: frac (m / n) = (m mod n) / n hence frac (m / n) = frac 0 .= (m mod n) / n by A1 ; ::_thesis: verum end; supposeA2: n > 0 ; ::_thesis: frac (m / n) = (m mod n) / n then m = (n * (m div n)) + (m mod n) by NAT_D:2; then (m / n) + 0 = (m div n) + ((m mod n) / n) by A2, XCMPLX_1:113; hence frac (m / n) = (m mod n) / n ; ::_thesis: verum end; end; end; theorem Th7: :: REAL_3:7 for p being rational number st p >= 0 holds ex m, n being Nat st ( n <> 0 & p = m / n ) proof let p be rational number ; ::_thesis: ( p >= 0 implies ex m, n being Nat st ( n <> 0 & p = m / n ) ) consider m being Integer, k being Element of NAT such that A1: ( k <> 0 & p = m / k ) by RAT_1:8; assume p >= 0 ; ::_thesis: ex m, n being Nat st ( n <> 0 & p = m / n ) then ( ( k > 0 & m >= 0 ) or ( k < 0 & m <= 0 ) ) by A1, XREAL_1:141; then reconsider m = m as Element of NAT by INT_1:3; take m ; ::_thesis: ex n being Nat st ( n <> 0 & p = m / n ) take k ; ::_thesis: ( k <> 0 & p = m / k ) thus ( k <> 0 & p = m / k ) by A1; ::_thesis: verum end; registration cluster non zero Relation-like NAT -defined REAL -valued INT -valued Function-like V26( NAT ) V30( NAT , REAL ) V35() V36() V37() for Element of K6(K7(NAT,REAL)); existence ex b1 being Real_Sequence st b1 is INT -valued proof set s = NAT --> 1; ( dom (NAT --> 1) = NAT & ( for n being Element of NAT holds (NAT --> 1) . n is real ) ) by FUNCOP_1:13; then reconsider s = NAT --> 1 as Real_Sequence by SEQ_1:2; take s ; ::_thesis: s is INT -valued thus s is INT -valued ; ::_thesis: verum end; end; definition mode Integer_Sequence is INT -valued Real_Sequence; end; theorem Th8: :: REAL_3:8 for f being Function holds ( f is Integer_Sequence iff ( dom f = NAT & ( for x being set st x in NAT holds f . x is integer ) ) ) proof let f be Function; ::_thesis: ( f is Integer_Sequence iff ( dom f = NAT & ( for x being set st x in NAT holds f . x is integer ) ) ) thus ( f is Integer_Sequence implies ( dom f = NAT & ( for x being set st x in NAT holds f . x is integer ) ) ) by SEQ_1:1; ::_thesis: ( dom f = NAT & ( for x being set st x in NAT holds f . x is integer ) implies f is Integer_Sequence ) assume that A1: dom f = NAT and A2: for x being set st x in NAT holds f . x is integer ; ::_thesis: f is Integer_Sequence now__::_thesis:_for_y_being_set_st_y_in_rng_f_holds_ y_in_INT let y be set ; ::_thesis: ( y in rng f implies y in INT ) assume y in rng f ; ::_thesis: y in INT then consider x being set such that A3: x in dom f and A4: y = f . x by FUNCT_1:def_3; f . x is integer by A1, A2, A3; hence y in INT by A4, INT_1:def_2; ::_thesis: verum end; then A5: rng f c= INT by TARSKI:def_3; for x being set st x in NAT holds f . x is real proof let x be set ; ::_thesis: ( x in NAT implies f . x is real ) assume x in NAT ; ::_thesis: f . x is real then f . x is integer by A2; hence f . x is real ; ::_thesis: verum end; hence f is Integer_Sequence by A1, A5, SEQ_1:1, RELAT_1:def_19; ::_thesis: verum end; theorem Th9: :: REAL_3:9 for f being Function holds ( f is Function of NAT,INT iff f is Integer_Sequence ) proof let f be Function; ::_thesis: ( f is Function of NAT,INT iff f is Integer_Sequence ) hereby ::_thesis: ( f is Integer_Sequence implies f is Function of NAT,INT ) assume f is Function of NAT,INT ; ::_thesis: f is Integer_Sequence then reconsider g = f as Function of NAT,INT ; ( dom g = NAT & ( for x being set st x in NAT holds g . x is integer ) ) by FUNCT_2:def_1; hence f is Integer_Sequence by Th8; ::_thesis: verum end; assume f is Integer_Sequence ; ::_thesis: f is Function of NAT,INT then ( dom f = NAT & rng f c= INT ) by FUNCT_2:def_1, RELAT_1:def_19; hence f is Function of NAT,INT by FUNCT_2:2; ::_thesis: verum end; theorem :: REAL_3:10 for f being Function holds ( f is sequence of NAT iff ( dom f = NAT & ( for x being set st x in NAT holds f . x is natural ) ) ) proof let f be Function; ::_thesis: ( f is sequence of NAT iff ( dom f = NAT & ( for x being set st x in NAT holds f . x is natural ) ) ) thus ( f is sequence of NAT implies ( dom f = NAT & ( for x being set st x in NAT holds f . x is natural ) ) ) by FUNCT_2:def_1; ::_thesis: ( dom f = NAT & ( for x being set st x in NAT holds f . x is natural ) implies f is sequence of NAT ) assume that A1: dom f = NAT and A2: for x being set st x in NAT holds f . x is natural ; ::_thesis: f is sequence of NAT rng f c= NAT proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in NAT ) assume x in rng f ; ::_thesis: x in NAT then ex y being set st ( y in NAT & x = f . y ) by A1, FUNCT_1:def_3; then x is natural by A2; hence x in NAT by ORDINAL1:def_12; ::_thesis: verum end; hence f is sequence of NAT by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; theorem :: REAL_3:11 for f being Function holds ( f is Function of NAT,NAT iff f is sequence of NAT ) ; begin definition deffunc H1( Nat, Element of NAT , Element of NAT ) -> Element of NAT = $2 mod $3; let m, n be Nat; set a = m mod n; set b = n mod (m mod n); func modSeq (m,n) -> sequence of NAT means :Def1: :: REAL_3:def 1 ( it . 0 = m mod n & it . 1 = n mod (m mod n) & ( for k being Nat holds it . (k + 2) = (it . k) mod (it . (k + 1)) ) ); existence ex b1 being sequence of NAT st ( b1 . 0 = m mod n & b1 . 1 = n mod (m mod n) & ( for k being Nat holds b1 . (k + 2) = (b1 . k) mod (b1 . (k + 1)) ) ) proof consider f being Function of NAT,NAT such that A1: ( f . 0 = m mod n & f . 1 = n mod (m mod n) ) and A2: for n being Element of NAT holds f . (n + 2) = H1(n,f . n,f . (n + 1)) from RECDEF_2:sch_5(); reconsider f = f as sequence of NAT ; take f ; ::_thesis: ( f . 0 = m mod n & f . 1 = n mod (m mod n) & ( for k being Nat holds f . (k + 2) = (f . k) mod (f . (k + 1)) ) ) thus ( f . 0 = m mod n & f . 1 = n mod (m mod n) ) by A1; ::_thesis: for k being Nat holds f . (k + 2) = (f . k) mod (f . (k + 1)) let k be Nat; ::_thesis: f . (k + 2) = (f . k) mod (f . (k + 1)) k in NAT by ORDINAL1:def_12; hence f . (k + 2) = (f . k) mod (f . (k + 1)) by A2; ::_thesis: verum end; uniqueness for b1, b2 being sequence of NAT st b1 . 0 = m mod n & b1 . 1 = n mod (m mod n) & ( for k being Nat holds b1 . (k + 2) = (b1 . k) mod (b1 . (k + 1)) ) & b2 . 0 = m mod n & b2 . 1 = n mod (m mod n) & ( for k being Nat holds b2 . (k + 2) = (b2 . k) mod (b2 . (k + 1)) ) holds b1 = b2 proof let f, g be sequence of NAT; ::_thesis: ( f . 0 = m mod n & f . 1 = n mod (m mod n) & ( for k being Nat holds f . (k + 2) = (f . k) mod (f . (k + 1)) ) & g . 0 = m mod n & g . 1 = n mod (m mod n) & ( for k being Nat holds g . (k + 2) = (g . k) mod (g . (k + 1)) ) implies f = g ) assume that A3: ( f . 0 = m mod n & f . 1 = n mod (m mod n) ) and A4: for n being Nat holds f . (n + 2) = (f . n) mod (f . (n + 1)) and A5: ( g . 0 = m mod n & g . 1 = n mod (m mod n) ) and A6: for n being Nat holds g . (n + 2) = (g . n) mod (g . (n + 1)) ; ::_thesis: f = g reconsider f = f, g = g as Function of NAT,NAT ; A7: ( g . 0 = m mod n & g . 1 = n mod (m mod n) ) by A5; A8: for n being Element of NAT holds g . (n + 2) = H1(n,g . n,g . (n + 1)) by A6; A9: for n being Element of NAT holds f . (n + 2) = H1(n,f . n,f . (n + 1)) by A4; A10: ( f . 0 = m mod n & f . 1 = n mod (m mod n) ) by A3; f = g from RECDEF_2:sch_7(A10, A9, A7, A8); hence f = g ; ::_thesis: verum end; end; :: deftheorem Def1 defines modSeq REAL_3:def_1_:_ for m, n being Nat for b3 being sequence of NAT holds ( b3 = modSeq (m,n) iff ( b3 . 0 = m mod n & b3 . 1 = n mod (m mod n) & ( for k being Nat holds b3 . (k + 2) = (b3 . k) mod (b3 . (k + 1)) ) ) ); definition let m, n be Nat; set a = m div n; set b = n div (m mod n); deffunc H1( Nat, Element of NAT , Element of NAT ) -> Element of NAT = ((modSeq (m,n)) . $1) div ((modSeq (m,n)) . ($1 + 1)); func divSeq (m,n) -> sequence of NAT means :Def2: :: REAL_3:def 2 ( it . 0 = m div n & it . 1 = n div (m mod n) & ( for k being Nat holds it . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ) ); existence ex b1 being sequence of NAT st ( b1 . 0 = m div n & b1 . 1 = n div (m mod n) & ( for k being Nat holds b1 . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ) ) proof consider f being Function of NAT,NAT such that A1: ( f . 0 = m div n & f . 1 = n div (m mod n) ) and A2: for n being Element of NAT holds f . (n + 2) = H1(n,f . n,f . (n + 1)) from RECDEF_2:sch_5(); reconsider f = f as sequence of NAT ; take f ; ::_thesis: ( f . 0 = m div n & f . 1 = n div (m mod n) & ( for k being Nat holds f . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ) ) thus ( f . 0 = m div n & f . 1 = n div (m mod n) ) by A1; ::_thesis: for k being Nat holds f . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) let k be Nat; ::_thesis: f . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) k in NAT by ORDINAL1:def_12; hence f . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) by A2; ::_thesis: verum end; uniqueness for b1, b2 being sequence of NAT st b1 . 0 = m div n & b1 . 1 = n div (m mod n) & ( for k being Nat holds b1 . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ) & b2 . 0 = m div n & b2 . 1 = n div (m mod n) & ( for k being Nat holds b2 . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ) holds b1 = b2 proof let f, g be sequence of NAT; ::_thesis: ( f . 0 = m div n & f . 1 = n div (m mod n) & ( for k being Nat holds f . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ) & g . 0 = m div n & g . 1 = n div (m mod n) & ( for k being Nat holds g . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ) implies f = g ) assume that A3: ( f . 0 = m div n & f . 1 = n div (m mod n) ) and A4: for k being Nat holds f . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) and A5: ( g . 0 = m div n & g . 1 = n div (m mod n) ) and A6: for k being Nat holds g . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ; ::_thesis: f = g reconsider f = f, g = g as Function of NAT,NAT ; A7: ( g . 0 = m div n & g . 1 = n div (m mod n) ) by A5; A8: for n being Element of NAT holds g . (n + 2) = H1(n,g . n,g . (n + 1)) by A6; A9: for n being Element of NAT holds f . (n + 2) = H1(n,f . n,f . (n + 1)) by A4; A10: ( f . 0 = m div n & f . 1 = n div (m mod n) ) by A3; f = g from RECDEF_2:sch_7(A10, A9, A7, A8); hence f = g ; ::_thesis: verum end; end; :: deftheorem Def2 defines divSeq REAL_3:def_2_:_ for m, n being Nat for b3 being sequence of NAT holds ( b3 = divSeq (m,n) iff ( b3 . 0 = m div n & b3 . 1 = n div (m mod n) & ( for k being Nat holds b3 . (k + 2) = ((modSeq (m,n)) . k) div ((modSeq (m,n)) . (k + 1)) ) ) ); theorem Th12: :: REAL_3:12 for m, n being Nat holds (divSeq (m,n)) . 1 = n div ((modSeq (m,n)) . 0) proof let m, n be Nat; ::_thesis: (divSeq (m,n)) . 1 = n div ((modSeq (m,n)) . 0) thus (divSeq (m,n)) . 1 = n div (m mod n) by Def2 .= n div ((modSeq (m,n)) . 0) by Def1 ; ::_thesis: verum end; theorem Th13: :: REAL_3:13 for m, n being Nat holds (modSeq (m,n)) . 1 = n mod ((modSeq (m,n)) . 0) proof let m, n be Nat; ::_thesis: (modSeq (m,n)) . 1 = n mod ((modSeq (m,n)) . 0) thus (modSeq (m,n)) . 1 = n mod (m mod n) by Def1 .= n mod ((modSeq (m,n)) . 0) by Def1 ; ::_thesis: verum end; theorem Th14: :: REAL_3:14 for a, b, m, n being Nat st a <= b & (modSeq (m,n)) . a = 0 holds (modSeq (m,n)) . b = 0 proof let a, b, m, n be Nat; ::_thesis: ( a <= b & (modSeq (m,n)) . a = 0 implies (modSeq (m,n)) . b = 0 ) set fm = modSeq (m,n); assume that A1: a <= b and A2: (modSeq (m,n)) . a = 0 ; ::_thesis: (modSeq (m,n)) . b = 0 A3: ( a < b or a = b ) by A1, XXREAL_0:1; defpred S1[ Nat] means ( a < $1 implies (modSeq (m,n)) . $1 = 0 ); A4: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A5: S1[k] ; ::_thesis: S1[k + 1] assume A6: a < k + 1 ; ::_thesis: (modSeq (m,n)) . (k + 1) = 0 then A7: a <= k by NAT_1:13; percases ( k = 0 or k = 1 or k > 1 ) by NAT_1:25; supposeA8: k = 0 ; ::_thesis: (modSeq (m,n)) . (k + 1) = 0 then A9: a = 0 by A6, NAT_1:13; thus (modSeq (m,n)) . (k + 1) = n mod ((modSeq (m,n)) . 0) by A8, Th13 .= 0 by A2, A9 ; ::_thesis: verum end; supposeA10: k = 1 ; ::_thesis: (modSeq (m,n)) . (k + 1) = 0 then A11: ( a = 0 or a = 1 ) by A7, NAT_1:25; 2 = 2 + 0 ; hence (modSeq (m,n)) . (k + 1) = ((modSeq (m,n)) . 0) mod ((modSeq (m,n)) . (0 + 1)) by A10, Def1 .= 0 by A2, A11 ; ::_thesis: verum end; suppose k > 1 ; ::_thesis: (modSeq (m,n)) . (k + 1) = 0 then reconsider k1 = k - 1 as Nat by Lm1; percases ( a = k or a < k ) by A7, XXREAL_0:1; supposeA12: a = k ; ::_thesis: (modSeq (m,n)) . (k + 1) = 0 thus (modSeq (m,n)) . (k + 1) = (modSeq (m,n)) . (k1 + 2) .= ((modSeq (m,n)) . k1) mod ((modSeq (m,n)) . (k1 + 1)) by Def1 .= 0 by A2, A12 ; ::_thesis: verum end; supposeA13: a < k ; ::_thesis: (modSeq (m,n)) . (k + 1) = 0 thus (modSeq (m,n)) . (k + 1) = (modSeq (m,n)) . (k1 + 2) .= ((modSeq (m,n)) . k1) mod ((modSeq (m,n)) . (k1 + 1)) by Def1 .= 0 by A5, A13 ; ::_thesis: verum end; end; end; end; end; A14: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A14, A4); hence (modSeq (m,n)) . b = 0 by A2, A3; ::_thesis: verum end; Lm3: for m, n, a being Nat holds ( (modSeq (m,n)) . a > (modSeq (m,n)) . (a + 1) or (modSeq (m,n)) . a = 0 ) proof let m, n, a be Nat; ::_thesis: ( (modSeq (m,n)) . a > (modSeq (m,n)) . (a + 1) or (modSeq (m,n)) . a = 0 ) set fm = modSeq (m,n); percases ( a = 0 or a = 1 or a > 1 ) by NAT_1:25; supposeA1: a = 0 ; ::_thesis: ( (modSeq (m,n)) . a > (modSeq (m,n)) . (a + 1) or (modSeq (m,n)) . a = 0 ) ( (modSeq (m,n)) . (0 + 1) = n mod (m mod n) & (modSeq (m,n)) . 0 = m mod n ) by Def1; hence ( (modSeq (m,n)) . a > (modSeq (m,n)) . (a + 1) or (modSeq (m,n)) . a = 0 ) by A1, NAT_D:1; ::_thesis: verum end; supposeA2: a = 1 ; ::_thesis: ( (modSeq (m,n)) . a > (modSeq (m,n)) . (a + 1) or (modSeq (m,n)) . a = 0 ) (modSeq (m,n)) . (0 + 2) = ((modSeq (m,n)) . 0) mod ((modSeq (m,n)) . (0 + 1)) by Def1; hence ( (modSeq (m,n)) . a > (modSeq (m,n)) . (a + 1) or (modSeq (m,n)) . a = 0 ) by A2, NAT_D:1; ::_thesis: verum end; suppose a > 1 ; ::_thesis: ( (modSeq (m,n)) . a > (modSeq (m,n)) . (a + 1) or (modSeq (m,n)) . a = 0 ) then reconsider a1 = a - 1 as Nat by Lm1; (modSeq (m,n)) . (a + 1) = (modSeq (m,n)) . (a1 + (1 + 1)) .= ((modSeq (m,n)) . a1) mod ((modSeq (m,n)) . (a1 + 1)) by Def1 ; hence ( (modSeq (m,n)) . a > (modSeq (m,n)) . (a + 1) or (modSeq (m,n)) . a = 0 ) by NAT_D:1; ::_thesis: verum end; end; end; theorem Th15: :: REAL_3:15 for a, b, m, n being Nat holds ( not a < b or (modSeq (m,n)) . a > (modSeq (m,n)) . b or (modSeq (m,n)) . a = 0 ) proof let a, b, m, n be Nat; ::_thesis: ( not a < b or (modSeq (m,n)) . a > (modSeq (m,n)) . b or (modSeq (m,n)) . a = 0 ) set fm = modSeq (m,n); assume A1: a < b ; ::_thesis: ( (modSeq (m,n)) . a > (modSeq (m,n)) . b or (modSeq (m,n)) . a = 0 ) percases ( (modSeq (m,n)) . a = 0 or (modSeq (m,n)) . a > 0 ) ; suppose (modSeq (m,n)) . a = 0 ; ::_thesis: ( (modSeq (m,n)) . a > (modSeq (m,n)) . b or (modSeq (m,n)) . a = 0 ) hence ( (modSeq (m,n)) . a > (modSeq (m,n)) . b or (modSeq (m,n)) . a = 0 ) ; ::_thesis: verum end; supposeA2: (modSeq (m,n)) . a > 0 ; ::_thesis: ( (modSeq (m,n)) . a > (modSeq (m,n)) . b or (modSeq (m,n)) . a = 0 ) defpred S1[ Nat] means ( a < $1 implies (modSeq (m,n)) . a > (modSeq (m,n)) . $1 ); A3: for x being Nat st S1[x] holds S1[x + 1] proof let x be Nat; ::_thesis: ( S1[x] implies S1[x + 1] ) assume A4: S1[x] ; ::_thesis: S1[x + 1] assume a < x + 1 ; ::_thesis: (modSeq (m,n)) . a > (modSeq (m,n)) . (x + 1) then A5: a <= x by NAT_1:13; percases ( a = x or a < x ) by A5, XXREAL_0:1; suppose a = x ; ::_thesis: (modSeq (m,n)) . a > (modSeq (m,n)) . (x + 1) hence (modSeq (m,n)) . a > (modSeq (m,n)) . (x + 1) by A2, Lm3; ::_thesis: verum end; supposeA6: a < x ; ::_thesis: (modSeq (m,n)) . a > (modSeq (m,n)) . (x + 1) thus (modSeq (m,n)) . a > (modSeq (m,n)) . (x + 1) ::_thesis: verum proof percases ( (modSeq (m,n)) . x > (modSeq (m,n)) . (x + 1) or (modSeq (m,n)) . x = 0 ) by Lm3; suppose (modSeq (m,n)) . x > (modSeq (m,n)) . (x + 1) ; ::_thesis: (modSeq (m,n)) . a > (modSeq (m,n)) . (x + 1) hence (modSeq (m,n)) . a > (modSeq (m,n)) . (x + 1) by A4, A6, XXREAL_0:2; ::_thesis: verum end; suppose (modSeq (m,n)) . x = 0 ; ::_thesis: (modSeq (m,n)) . a > (modSeq (m,n)) . (x + 1) hence (modSeq (m,n)) . a > (modSeq (m,n)) . (x + 1) by A2, Th14, NAT_1:11; ::_thesis: verum end; end; end; end; end; end; A7: S1[ 0 ] ; for x being Nat holds S1[x] from NAT_1:sch_2(A7, A3); hence ( (modSeq (m,n)) . a > (modSeq (m,n)) . b or (modSeq (m,n)) . a = 0 ) by A1; ::_thesis: verum end; end; end; theorem Th16: :: REAL_3:16 for m, n, a being Nat st (divSeq (m,n)) . (a + 1) = 0 holds (modSeq (m,n)) . a = 0 proof let m, n, a be Nat; ::_thesis: ( (divSeq (m,n)) . (a + 1) = 0 implies (modSeq (m,n)) . a = 0 ) set fd = divSeq (m,n); set fm = modSeq (m,n); defpred S1[ Nat] means ( (divSeq (m,n)) . ($1 + 1) = 0 implies (modSeq (m,n)) . $1 = 0 ); A1: for b being Nat st S1[b] holds S1[b + 1] proof let b be Nat; ::_thesis: ( S1[b] implies S1[b + 1] ) assume S1[b] ; ::_thesis: S1[b + 1] set x = (modSeq (m,n)) . (b + 1); assume (divSeq (m,n)) . ((b + 1) + 1) = 0 ; ::_thesis: (modSeq (m,n)) . (b + 1) = 0 then (divSeq (m,n)) . (b + (1 + 1)) = 0 ; then A2: ((modSeq (m,n)) . b) div ((modSeq (m,n)) . (b + 1)) = 0 by Def2; assume A3: (modSeq (m,n)) . (b + 1) <> 0 ; ::_thesis: contradiction then (modSeq (m,n)) . b = (((modSeq (m,n)) . (b + 1)) * (((modSeq (m,n)) . b) div ((modSeq (m,n)) . (b + 1)))) + (((modSeq (m,n)) . b) mod ((modSeq (m,n)) . (b + 1))) by NAT_D:2; then A4: (modSeq (m,n)) . b < (modSeq (m,n)) . (b + 1) by A2, A3, NAT_D:1; A5: b + 0 < b + 1 by XREAL_1:6; then (modSeq (m,n)) . b <> 0 by A3, Th14; hence contradiction by A4, A5, Th15; ::_thesis: verum end; A6: S1[ 0 ] proof set x = m mod n; assume (divSeq (m,n)) . (0 + 1) = 0 ; ::_thesis: (modSeq (m,n)) . 0 = 0 then A7: n div ((modSeq (m,n)) . 0) = 0 by Th12; assume A8: (modSeq (m,n)) . 0 <> 0 ; ::_thesis: contradiction then m mod n <> 0 by Def1; then A9: n <> 0 ; A10: (modSeq (m,n)) . 0 = m mod n by Def1; then n = ((m mod n) * (n div (m mod n))) + (n mod (m mod n)) by A8, NAT_D:2; then n < m mod n by A7, A10, A8, NAT_D:1; hence contradiction by A9, NAT_D:1; ::_thesis: verum end; for b being Nat holds S1[b] from NAT_1:sch_2(A6, A1); hence ( (divSeq (m,n)) . (a + 1) = 0 implies (modSeq (m,n)) . a = 0 ) ; ::_thesis: verum end; Lm4: for m, n, a being Nat st (modSeq (m,n)) . a = 0 holds (divSeq (m,n)) . (a + 1) = 0 proof let m, n, a be Nat; ::_thesis: ( (modSeq (m,n)) . a = 0 implies (divSeq (m,n)) . (a + 1) = 0 ) set fd = divSeq (m,n); set fm = modSeq (m,n); defpred S1[ Nat] means ( (modSeq (m,n)) . $1 = 0 implies (divSeq (m,n)) . ($1 + 1) = 0 ); A1: for b being Nat st S1[b] holds S1[b + 1] proof let b be Nat; ::_thesis: ( S1[b] implies S1[b + 1] ) assume that S1[b] and A2: (modSeq (m,n)) . (b + 1) = 0 ; ::_thesis: (divSeq (m,n)) . ((b + 1) + 1) = 0 thus (divSeq (m,n)) . ((b + 1) + 1) = (divSeq (m,n)) . (b + (1 + 1)) .= ((modSeq (m,n)) . b) div ((modSeq (m,n)) . (b + 1)) by Def2 .= 0 by A2 ; ::_thesis: verum end; A3: S1[ 0 ] proof assume A4: (modSeq (m,n)) . 0 = 0 ; ::_thesis: (divSeq (m,n)) . (0 + 1) = 0 thus (divSeq (m,n)) . (0 + 1) = n div ((modSeq (m,n)) . 0) by Th12 .= 0 by A4 ; ::_thesis: verum end; for b being Nat holds S1[b] from NAT_1:sch_2(A3, A1); hence ( (modSeq (m,n)) . a = 0 implies (divSeq (m,n)) . (a + 1) = 0 ) ; ::_thesis: verum end; theorem Th17: :: REAL_3:17 for a, b, m, n being Nat st a <> 0 & a <= b & (divSeq (m,n)) . a = 0 holds (divSeq (m,n)) . b = 0 proof let a, b, m, n be Nat; ::_thesis: ( a <> 0 & a <= b & (divSeq (m,n)) . a = 0 implies (divSeq (m,n)) . b = 0 ) set fd = divSeq (m,n); set fm = modSeq (m,n); assume that A1: a <> 0 and A2: a <= b and A3: (divSeq (m,n)) . a = 0 ; ::_thesis: (divSeq (m,n)) . b = 0 A4: ( a < b or a = b ) by A2, XXREAL_0:1; defpred S1[ Nat] means ( a < $1 implies ( (divSeq (m,n)) . $1 = 0 & (modSeq (m,n)) . $1 = 0 ) ); A5: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A6: S1[k] ; ::_thesis: S1[k + 1] assume A7: a < k + 1 ; ::_thesis: ( (divSeq (m,n)) . (k + 1) = 0 & (modSeq (m,n)) . (k + 1) = 0 ) then A8: a <= k by NAT_1:13; percases ( k = 0 or k = 1 or k > 1 ) by NAT_1:25; suppose k = 0 ; ::_thesis: ( (divSeq (m,n)) . (k + 1) = 0 & (modSeq (m,n)) . (k + 1) = 0 ) hence ( (divSeq (m,n)) . (k + 1) = 0 & (modSeq (m,n)) . (k + 1) = 0 ) by A1, A7, NAT_1:13; ::_thesis: verum end; supposeA9: k = 1 ; ::_thesis: ( (divSeq (m,n)) . (k + 1) = 0 & (modSeq (m,n)) . (k + 1) = 0 ) then (divSeq (m,n)) . (0 + 1) = 0 by A1, A3, A8, NAT_1:25; then A10: (modSeq (m,n)) . 0 = 0 by Th16; A11: 2 = 2 + 0 ; hence (divSeq (m,n)) . (k + 1) = ((modSeq (m,n)) . 0) div ((modSeq (m,n)) . (0 + 1)) by A9, Def2 .= 0 by A10 ; ::_thesis: (modSeq (m,n)) . (k + 1) = 0 thus (modSeq (m,n)) . (k + 1) = ((modSeq (m,n)) . 0) mod ((modSeq (m,n)) . (0 + 1)) by A9, A11, Def1 .= 0 by A10 ; ::_thesis: verum end; suppose k > 1 ; ::_thesis: ( (divSeq (m,n)) . (k + 1) = 0 & (modSeq (m,n)) . (k + 1) = 0 ) then reconsider k1 = k - 1 as Nat by Lm1; A12: k = k1 + 1 ; percases ( a = k or a < k ) by A8, XXREAL_0:1; suppose a = k ; ::_thesis: ( (divSeq (m,n)) . (k + 1) = 0 & (modSeq (m,n)) . (k + 1) = 0 ) then A13: (modSeq (m,n)) . k1 = 0 by A3, A12, Th16; thus (divSeq (m,n)) . (k + 1) = (divSeq (m,n)) . (k1 + 2) .= ((modSeq (m,n)) . k1) div ((modSeq (m,n)) . (k1 + 1)) by Def2 .= 0 by A13 ; ::_thesis: (modSeq (m,n)) . (k + 1) = 0 thus (modSeq (m,n)) . (k + 1) = (modSeq (m,n)) . (k1 + 2) .= ((modSeq (m,n)) . k1) mod ((modSeq (m,n)) . (k1 + 1)) by Def1 .= 0 by A13 ; ::_thesis: verum end; supposeA14: a < k ; ::_thesis: ( (divSeq (m,n)) . (k + 1) = 0 & (modSeq (m,n)) . (k + 1) = 0 ) thus (divSeq (m,n)) . (k + 1) = (divSeq (m,n)) . (k1 + 2) .= ((modSeq (m,n)) . k1) div ((modSeq (m,n)) . (k1 + 1)) by Def2 .= 0 by A6, A14 ; ::_thesis: (modSeq (m,n)) . (k + 1) = 0 thus (modSeq (m,n)) . (k + 1) = (modSeq (m,n)) . (k1 + 2) .= ((modSeq (m,n)) . k1) mod ((modSeq (m,n)) . (k1 + 1)) by Def1 .= 0 by A6, A14 ; ::_thesis: verum end; end; end; end; end; A15: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A15, A5); hence (divSeq (m,n)) . b = 0 by A3, A4; ::_thesis: verum end; theorem Th18: :: REAL_3:18 for a, b, m, n being Nat st a < b & (modSeq (m,n)) . a = 0 holds (divSeq (m,n)) . b = 0 proof let a, b, m, n be Nat; ::_thesis: ( a < b & (modSeq (m,n)) . a = 0 implies (divSeq (m,n)) . b = 0 ) set fd = divSeq (m,n); set fm = modSeq (m,n); assume a < b ; ::_thesis: ( not (modSeq (m,n)) . a = 0 or (divSeq (m,n)) . b = 0 ) then A1: a + 1 <= b by NAT_1:13; assume (modSeq (m,n)) . a = 0 ; ::_thesis: (divSeq (m,n)) . b = 0 then (divSeq (m,n)) . (a + 1) = 0 by Lm4; hence (divSeq (m,n)) . b = 0 by A1, Th17; ::_thesis: verum end; theorem Th19: :: REAL_3:19 for n, m being Nat st n <> 0 holds m = (((divSeq (m,n)) . 0) * n) + ((modSeq (m,n)) . 0) proof let n, m be Nat; ::_thesis: ( n <> 0 implies m = (((divSeq (m,n)) . 0) * n) + ((modSeq (m,n)) . 0) ) set fd = divSeq (m,n); set fm = modSeq (m,n); assume A1: n <> 0 ; ::_thesis: m = (((divSeq (m,n)) . 0) * n) + ((modSeq (m,n)) . 0) ( (divSeq (m,n)) . 0 = m div n & (modSeq (m,n)) . 0 = m mod n ) by Def1, Def2; hence m = (((divSeq (m,n)) . 0) * n) + ((modSeq (m,n)) . 0) by A1, NAT_D:2; ::_thesis: verum end; theorem :: REAL_3:20 for n, m being Nat st n <> 0 holds m / n = ((divSeq (m,n)) . 0) + (1 / (n / ((modSeq (m,n)) . 0))) proof let n, m be Nat; ::_thesis: ( n <> 0 implies m / n = ((divSeq (m,n)) . 0) + (1 / (n / ((modSeq (m,n)) . 0))) ) set fd = divSeq (m,n); set fm = modSeq (m,n); assume A1: n <> 0 ; ::_thesis: m / n = ((divSeq (m,n)) . 0) + (1 / (n / ((modSeq (m,n)) . 0))) hence m / n = ((((divSeq (m,n)) . 0) * n) + ((modSeq (m,n)) . 0)) / n by Th19 .= (((modSeq (m,n)) . 0) / n) + ((divSeq (m,n)) . 0) by A1, XCMPLX_1:113 .= ((divSeq (m,n)) . 0) + (1 / (n / ((modSeq (m,n)) . 0))) by XCMPLX_1:57 ; ::_thesis: verum end; set g = NAT --> 0; Lm5: dom (NAT --> 0) = NAT by FUNCOP_1:13; theorem Th21: :: REAL_3:21 for m being Nat holds divSeq (m,0) = NAT --> 0 proof let m be Nat; ::_thesis: divSeq (m,0) = NAT --> 0 set g = NAT --> 0; set fd = divSeq (m,0); A1: for x being set st x in dom (divSeq (m,0)) holds (divSeq (m,0)) . x = (NAT --> 0) . x proof defpred S1[ Nat] means (divSeq (m,0)) . $1 = 0 ; let x be set ; ::_thesis: ( x in dom (divSeq (m,0)) implies (divSeq (m,0)) . x = (NAT --> 0) . x ) assume x in dom (divSeq (m,0)) ; ::_thesis: (divSeq (m,0)) . x = (NAT --> 0) . x then reconsider x = x as Element of NAT ; A2: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A3: S1[n] ; ::_thesis: S1[n + 1] percases ( n = 0 or 0 <> n ) ; supposeA4: n = 0 ; ::_thesis: S1[n + 1] (divSeq (m,0)) . 1 = 0 div (m mod 0) by Def2 .= 0 ; hence S1[n + 1] by A4; ::_thesis: verum end; suppose 0 <> n ; ::_thesis: S1[n + 1] hence S1[n + 1] by A3, Th17, NAT_1:11; ::_thesis: verum end; end; end; (divSeq (m,0)) . 0 = m div 0 by Def2 .= 0 ; then A5: S1[ 0 ] ; for n being Nat holds S1[n] from NAT_1:sch_2(A5, A2); then (divSeq (m,0)) . x = 0 ; hence (divSeq (m,0)) . x = (NAT --> 0) . x by FUNCOP_1:7; ::_thesis: verum end; dom (divSeq (m,0)) = NAT by FUNCT_2:def_1; hence divSeq (m,0) = NAT --> 0 by A1, Lm5, FUNCT_1:2; ::_thesis: verum end; theorem Th22: :: REAL_3:22 for m being Nat holds modSeq (m,0) = NAT --> 0 proof let m be Nat; ::_thesis: modSeq (m,0) = NAT --> 0 set fm = modSeq (m,0); A1: for x being set st x in dom (modSeq (m,0)) holds (modSeq (m,0)) . x = (NAT --> 0) . x proof defpred S1[ Nat] means (modSeq (m,0)) . $1 = 0 ; let x be set ; ::_thesis: ( x in dom (modSeq (m,0)) implies (modSeq (m,0)) . x = (NAT --> 0) . x ) assume x in dom (modSeq (m,0)) ; ::_thesis: (modSeq (m,0)) . x = (NAT --> 0) . x then reconsider x = x as Element of NAT ; (modSeq (m,0)) . 0 = m mod 0 by Def1 .= 0 ; then A2: S1[ 0 ] ; A3: for n being Nat st S1[n] holds S1[n + 1] by Th14, NAT_1:11; for n being Nat holds S1[n] from NAT_1:sch_2(A2, A3); then (modSeq (m,0)) . x = 0 ; hence (modSeq (m,0)) . x = (NAT --> 0) . x by FUNCOP_1:7; ::_thesis: verum end; dom (modSeq (m,0)) = NAT by FUNCT_2:def_1; hence modSeq (m,0) = NAT --> 0 by A1, Lm5, FUNCT_1:2; ::_thesis: verum end; theorem :: REAL_3:23 for n being Nat holds divSeq (0,n) = NAT --> 0 proof let n be Nat; ::_thesis: divSeq (0,n) = NAT --> 0 set fd = divSeq (0,n); A1: for x being set st x in dom (divSeq (0,n)) holds (divSeq (0,n)) . x = (NAT --> 0) . x proof defpred S1[ Nat] means (divSeq (0,n)) . $1 = 0 ; let x be set ; ::_thesis: ( x in dom (divSeq (0,n)) implies (divSeq (0,n)) . x = (NAT --> 0) . x ) assume x in dom (divSeq (0,n)) ; ::_thesis: (divSeq (0,n)) . x = (NAT --> 0) . x then reconsider x = x as Element of NAT ; A2: for x being Nat st S1[x] holds S1[x + 1] proof let x be Nat; ::_thesis: ( S1[x] implies S1[x + 1] ) assume A3: S1[x] ; ::_thesis: S1[x + 1] percases ( x = 0 or 0 <> x ) ; supposeA4: x = 0 ; ::_thesis: S1[x + 1] (divSeq (0,n)) . 1 = n div (0 mod n) by Def2 .= n div 0 ; hence S1[x + 1] by A4; ::_thesis: verum end; suppose 0 <> x ; ::_thesis: S1[x + 1] hence S1[x + 1] by A3, Th17, NAT_1:11; ::_thesis: verum end; end; end; (divSeq (0,n)) . 0 = 0 div n by Def2 .= 0 ; then A5: S1[ 0 ] ; for n being Nat holds S1[n] from NAT_1:sch_2(A5, A2); then (divSeq (0,n)) . x = 0 ; hence (divSeq (0,n)) . x = (NAT --> 0) . x by FUNCOP_1:7; ::_thesis: verum end; dom (divSeq (0,n)) = NAT by FUNCT_2:def_1; hence divSeq (0,n) = NAT --> 0 by A1, Lm5, FUNCT_1:2; ::_thesis: verum end; theorem :: REAL_3:24 for n being Nat holds modSeq (0,n) = NAT --> 0 proof let n be Nat; ::_thesis: modSeq (0,n) = NAT --> 0 set fm = modSeq (0,n); A1: for x being set st x in dom (modSeq (0,n)) holds (modSeq (0,n)) . x = (NAT --> 0) . x proof defpred S1[ Nat] means (modSeq (0,n)) . $1 = 0 ; let x be set ; ::_thesis: ( x in dom (modSeq (0,n)) implies (modSeq (0,n)) . x = (NAT --> 0) . x ) assume x in dom (modSeq (0,n)) ; ::_thesis: (modSeq (0,n)) . x = (NAT --> 0) . x then reconsider x = x as Element of NAT ; (modSeq (0,n)) . 0 = 0 mod n by Def1 .= 0 ; then A2: S1[ 0 ] ; A3: for x being Nat st S1[x] holds S1[x + 1] by Th14, NAT_1:11; for n being Nat holds S1[n] from NAT_1:sch_2(A2, A3); then (modSeq (0,n)) . x = 0 ; hence (modSeq (0,n)) . x = (NAT --> 0) . x by FUNCOP_1:7; ::_thesis: verum end; dom (modSeq (0,n)) = NAT by FUNCT_2:def_1; hence modSeq (0,n) = NAT --> 0 by A1, Lm5, FUNCT_1:2; ::_thesis: verum end; Lm6: for m, n being Nat ex k being Nat st (modSeq (m,n)) . k = 0 proof let m, n be Nat; ::_thesis: ex k being Nat st (modSeq (m,n)) . k = 0 set f = modSeq (m,n); defpred S1[ Nat] means ex k being Nat st (modSeq (m,n)) . k = $1; A1: for a being Nat st a <> 0 & S1[a] holds ex w being Nat st ( w < a & S1[w] ) proof let a be Nat; ::_thesis: ( a <> 0 & S1[a] implies ex w being Nat st ( w < a & S1[w] ) ) assume A2: a <> 0 ; ::_thesis: ( not S1[a] or ex w being Nat st ( w < a & S1[w] ) ) given k being Nat such that A3: (modSeq (m,n)) . k = a ; ::_thesis: ex w being Nat st ( w < a & S1[w] ) take w = (modSeq (m,n)) . (k + 1); ::_thesis: ( w < a & S1[w] ) k + 0 < k + 1 by XREAL_1:6; hence w < a by A2, A3, Th15; ::_thesis: S1[w] thus S1[w] ; ::_thesis: verum end; A4: ex a being Nat st S1[a] proof take (modSeq (m,n)) . 0 ; ::_thesis: S1[(modSeq (m,n)) . 0] take 0 ; ::_thesis: (modSeq (m,n)) . 0 = (modSeq (m,n)) . 0 thus (modSeq (m,n)) . 0 = (modSeq (m,n)) . 0 ; ::_thesis: verum end; thus S1[ 0 ] from NAT_1:sch_7(A4, A1); ::_thesis: verum end; theorem Th25: :: REAL_3:25 for m, n being Nat ex k being Nat st ( (divSeq (m,n)) . k = 0 & (modSeq (m,n)) . k = 0 ) proof let m, n be Nat; ::_thesis: ex k being Nat st ( (divSeq (m,n)) . k = 0 & (modSeq (m,n)) . k = 0 ) set f = modSeq (m,n); consider k being Nat such that A1: (modSeq (m,n)) . k = 0 by Lm6; take k + 1 ; ::_thesis: ( (divSeq (m,n)) . (k + 1) = 0 & (modSeq (m,n)) . (k + 1) = 0 ) A2: k + 0 < k + 1 by XREAL_1:6; hence (divSeq (m,n)) . (k + 1) = 0 by A1, Th18; ::_thesis: (modSeq (m,n)) . (k + 1) = 0 thus (modSeq (m,n)) . (k + 1) = 0 by A1, A2, Th14; ::_thesis: verum end; begin defpred S1[ set , Element of REAL , set ] means $3 = 1 / (frac $2); definition let r be real number ; func remainders_for_scf r -> Real_Sequence means :Def3: :: REAL_3:def 3 ( it . 0 = r & ( for n being Nat holds it . (n + 1) = 1 / (frac (it . n)) ) ); existence ex b1 being Real_Sequence st ( b1 . 0 = r & ( for n being Nat holds b1 . (n + 1) = 1 / (frac (b1 . n)) ) ) proof reconsider r1 = r as Element of REAL by XREAL_0:def_1; A1: for n being Element of NAT for x being Element of REAL ex y being Element of REAL st S1[n,x,y] ; consider f being Function of NAT,REAL such that A2: f . 0 = r1 and A3: for n being Element of NAT holds S1[n,f . n,f . (n + 1)] from RECDEF_1:sch_2(A1); take f ; ::_thesis: ( f . 0 = r & ( for n being Nat holds f . (n + 1) = 1 / (frac (f . n)) ) ) thus f . 0 = r by A2; ::_thesis: for n being Nat holds f . (n + 1) = 1 / (frac (f . n)) let n be Nat; ::_thesis: f . (n + 1) = 1 / (frac (f . n)) n in NAT by ORDINAL1:def_12; hence f . (n + 1) = 1 / (frac (f . n)) by A3; ::_thesis: verum end; uniqueness for b1, b2 being Real_Sequence st b1 . 0 = r & ( for n being Nat holds b1 . (n + 1) = 1 / (frac (b1 . n)) ) & b2 . 0 = r & ( for n being Nat holds b2 . (n + 1) = 1 / (frac (b2 . n)) ) holds b1 = b2 proof A4: for n being Nat for x, y1, y2 being Element of REAL st S1[n,x,y1] & S1[n,x,y2] holds y1 = y2 ; reconsider r1 = r as Element of REAL by XREAL_0:def_1; let g1, g2 be Real_Sequence; ::_thesis: ( g1 . 0 = r & ( for n being Nat holds g1 . (n + 1) = 1 / (frac (g1 . n)) ) & g2 . 0 = r & ( for n being Nat holds g2 . (n + 1) = 1 / (frac (g2 . n)) ) implies g1 = g2 ) assume that A5: g1 . 0 = r and A6: for n being Nat holds g1 . (n + 1) = 1 / (frac (g1 . n)) and A7: g2 . 0 = r and A8: for n being Nat holds g2 . (n + 1) = 1 / (frac (g2 . n)) ; ::_thesis: g1 = g2 A9: for n being Nat holds S1[n,g1 . n,g1 . (n + 1)] by A6; A10: for n being Nat holds S1[n,g2 . n,g2 . (n + 1)] by A8; A11: g2 . 0 = r1 by A7; A12: g1 . 0 = r1 by A5; thus g1 = g2 from NAT_1:sch_14(A12, A9, A11, A10, A4); ::_thesis: verum end; end; :: deftheorem Def3 defines remainders_for_scf REAL_3:def_3_:_ for r being real number for b2 being Real_Sequence holds ( b2 = remainders_for_scf r iff ( b2 . 0 = r & ( for n being Nat holds b2 . (n + 1) = 1 / (frac (b2 . n)) ) ) ); notation let r be real number ; synonym rfs r for remainders_for_scf r; end; definition let r be real number ; func SimpleContinuedFraction r -> Integer_Sequence means :Def4: :: REAL_3:def 4 for n being Nat holds it . n = [\((rfs r) . n)/]; existence ex b1 being Integer_Sequence st for n being Nat holds b1 . n = [\((rfs r) . n)/] proof defpred S2[ set , set ] means $2 = [\((rfs r) . $1)/]; A1: for x being Element of NAT ex y being Element of INT st S2[x,y] proof let x be Element of NAT ; ::_thesis: ex y being Element of INT st S2[x,y] reconsider y = [\((rfs r) . x)/] as Element of INT by INT_1:def_2; take y ; ::_thesis: S2[x,y] thus S2[x,y] ; ::_thesis: verum end; consider f being Function of NAT,INT such that A2: for x being Element of NAT holds S2[x,f . x] from FUNCT_2:sch_3(A1); reconsider f = f as Integer_Sequence by Th9; take f ; ::_thesis: for n being Nat holds f . n = [\((rfs r) . n)/] let n be Nat; ::_thesis: f . n = [\((rfs r) . n)/] n in NAT by ORDINAL1:def_12; hence f . n = [\((rfs r) . n)/] by A2; ::_thesis: verum end; uniqueness for b1, b2 being Integer_Sequence st ( for n being Nat holds b1 . n = [\((rfs r) . n)/] ) & ( for n being Nat holds b2 . n = [\((rfs r) . n)/] ) holds b1 = b2 proof let f1, f2 be Integer_Sequence; ::_thesis: ( ( for n being Nat holds f1 . n = [\((rfs r) . n)/] ) & ( for n being Nat holds f2 . n = [\((rfs r) . n)/] ) implies f1 = f2 ) assume that A3: for n being Nat holds f1 . n = [\((rfs r) . n)/] and A4: for n being Nat holds f2 . n = [\((rfs r) . n)/] ; ::_thesis: f1 = f2 let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: f1 . n = f2 . n thus f1 . n = [\((rfs r) . n)/] by A3 .= f2 . n by A4 ; ::_thesis: verum end; end; :: deftheorem Def4 defines SimpleContinuedFraction REAL_3:def_4_:_ for r being real number for b2 being Integer_Sequence holds ( b2 = SimpleContinuedFraction r iff for n being Nat holds b2 . n = [\((rfs r) . n)/] ); notation let r be real number ; synonym scf r for SimpleContinuedFraction r; end; theorem Th26: :: REAL_3:26 for n being Nat for r being real number holds (rfs r) . (n + 1) = 1 / (((rfs r) . n) - ((scf r) . n)) proof let n be Nat; ::_thesis: for r being real number holds (rfs r) . (n + 1) = 1 / (((rfs r) . n) - ((scf r) . n)) let r be real number ; ::_thesis: (rfs r) . (n + 1) = 1 / (((rfs r) . n) - ((scf r) . n)) thus (rfs r) . (n + 1) = 1 / (frac ((rfs r) . n)) by Def3 .= 1 / (((rfs r) . n) - ((scf r) . n)) by Def4 ; ::_thesis: verum end; theorem Th27: :: REAL_3:27 for n, m being Nat for r being real number st (rfs r) . n = 0 & n <= m holds (rfs r) . m = 0 proof let n, m be Nat; ::_thesis: for r being real number st (rfs r) . n = 0 & n <= m holds (rfs r) . m = 0 let r be real number ; ::_thesis: ( (rfs r) . n = 0 & n <= m implies (rfs r) . m = 0 ) assume that A1: (rfs r) . n = 0 and A2: n <= m ; ::_thesis: (rfs r) . m = 0 percases ( n = m or n < m ) by A2, XXREAL_0:1; suppose n = m ; ::_thesis: (rfs r) . m = 0 hence (rfs r) . m = 0 by A1; ::_thesis: verum end; supposeA3: n < m ; ::_thesis: (rfs r) . m = 0 defpred S2[ Nat] means ( n < $1 implies (rfs r) . $1 = 0 ); A4: for a being Nat st S2[a] holds S2[a + 1] proof let a be Nat; ::_thesis: ( S2[a] implies S2[a + 1] ) assume A5: S2[a] ; ::_thesis: S2[a + 1] assume n < a + 1 ; ::_thesis: (rfs r) . (a + 1) = 0 then A6: n <= a by NAT_1:13; percases ( n = a or n < a ) by A6, XXREAL_0:1; supposeA7: n = a ; ::_thesis: (rfs r) . (a + 1) = 0 thus (rfs r) . (a + 1) = 1 / (frac ((rfs r) . a)) by Def3 .= 1 / (((rfs r) . a) - ((rfs r) . a)) by A1, A7 .= 0 ; ::_thesis: verum end; supposeA8: n < a ; ::_thesis: (rfs r) . (a + 1) = 0 thus (rfs r) . (a + 1) = 1 / (frac ((rfs r) . a)) by Def3 .= 1 / (((rfs r) . a) - ((rfs r) . a)) by A5, A8 .= 0 ; ::_thesis: verum end; end; end; A9: S2[ 0 ] ; for a being Nat holds S2[a] from NAT_1:sch_2(A9, A4); hence (rfs r) . m = 0 by A3; ::_thesis: verum end; end; end; theorem :: REAL_3:28 for n, m being Nat for r being real number st (rfs r) . n = 0 & n <= m holds (scf r) . m = 0 proof let n, m be Nat; ::_thesis: for r being real number st (rfs r) . n = 0 & n <= m holds (scf r) . m = 0 let r be real number ; ::_thesis: ( (rfs r) . n = 0 & n <= m implies (scf r) . m = 0 ) assume A1: ( (rfs r) . n = 0 & n <= m ) ; ::_thesis: (scf r) . m = 0 thus (scf r) . m = [\((rfs r) . m)/] by Def4 .= [\0/] by A1, Th27 .= 0 ; ::_thesis: verum end; theorem Th29: :: REAL_3:29 for n being Nat for i being Integer holds (rfs i) . (n + 1) = 0 proof let n be Nat; ::_thesis: for i being Integer holds (rfs i) . (n + 1) = 0 let i be Integer; ::_thesis: (rfs i) . (n + 1) = 0 defpred S2[ Nat] means (rfs i) . ($1 + 1) = 0 ; A1: (rfs i) . 0 = i by Def3; A2: for n being Nat st S2[n] holds S2[n + 1] proof let n be Nat; ::_thesis: ( S2[n] implies S2[n + 1] ) assume A3: S2[n] ; ::_thesis: S2[n + 1] thus (rfs i) . ((n + 1) + 1) = 1 / (frac ((rfs i) . (n + 1))) by Def3 .= 1 / (0 - 0) by A3 .= 0 ; ::_thesis: verum end; (rfs i) . (0 + 1) = 1 / (frac ((rfs i) . 0)) by Def3 .= 1 / (i - i) by A1, INT_1:25 .= 0 ; then A4: S2[ 0 ] ; for n being Nat holds S2[n] from NAT_1:sch_2(A4, A2); hence (rfs i) . (n + 1) = 0 ; ::_thesis: verum end; theorem Th30: :: REAL_3:30 for n being Nat for i being Integer holds ( (scf i) . 0 = i & (scf i) . (n + 1) = 0 ) proof let n be Nat; ::_thesis: for i being Integer holds ( (scf i) . 0 = i & (scf i) . (n + 1) = 0 ) let i be Integer; ::_thesis: ( (scf i) . 0 = i & (scf i) . (n + 1) = 0 ) defpred S2[ Nat] means ( (rfs i) . ($1 + 1) = 0 & (scf i) . ($1 + 1) = 0 ); thus (scf i) . 0 = [\((rfs i) . 0)/] by Def4 .= [\i/] by Def3 .= i by INT_1:25 ; ::_thesis: (scf i) . (n + 1) = 0 A1: for n being Nat st S2[n] holds S2[n + 1] proof let n be Nat; ::_thesis: ( S2[n] implies S2[n + 1] ) assume A2: S2[n] ; ::_thesis: S2[n + 1] thus (rfs i) . ((n + 1) + 1) = 1 / (frac ((rfs i) . (n + 1))) by Def3 .= 1 / (0 - 0) by A2 .= 0 ; ::_thesis: (scf i) . ((n + 1) + 1) = 0 thus (scf i) . ((n + 1) + 1) = [\((rfs i) . ((n + 1) + 1))/] by Def4 .= [\0/] by Th29 .= 0 ; ::_thesis: verum end; (scf i) . (0 + 1) = [\((rfs i) . (0 + 1))/] by Def4 .= [\0/] by Th29 .= 0 ; then A3: S2[ 0 ] by Th29; for n being Nat holds S2[n] from NAT_1:sch_2(A3, A1); hence (scf i) . (n + 1) = 0 ; ::_thesis: verum end; Lm7: for n being Nat for i being Integer st i > 1 holds ( (rfs (1 / i)) . 1 = i & (rfs (1 / i)) . (n + 2) = 0 & (scf (1 / i)) . 0 = 0 & (scf (1 / i)) . 1 = i & (scf (1 / i)) . (n + 2) = 0 ) proof let n be Nat; ::_thesis: for i being Integer st i > 1 holds ( (rfs (1 / i)) . 1 = i & (rfs (1 / i)) . (n + 2) = 0 & (scf (1 / i)) . 0 = 0 & (scf (1 / i)) . 1 = i & (scf (1 / i)) . (n + 2) = 0 ) let i be Integer; ::_thesis: ( i > 1 implies ( (rfs (1 / i)) . 1 = i & (rfs (1 / i)) . (n + 2) = 0 & (scf (1 / i)) . 0 = 0 & (scf (1 / i)) . 1 = i & (scf (1 / i)) . (n + 2) = 0 ) ) set r = 1 / i; defpred S2[ Nat] means ( (rfs (1 / i)) . ($1 + 2) = 0 & (scf (1 / i)) . ($1 + 2) = 0 ); assume A1: i > 1 ; ::_thesis: ( (rfs (1 / i)) . 1 = i & (rfs (1 / i)) . (n + 2) = 0 & (scf (1 / i)) . 0 = 0 & (scf (1 / i)) . 1 = i & (scf (1 / i)) . (n + 2) = 0 ) then A2: 1 / i < 0 + 1 by XREAL_1:189; A3: [\((rfs (1 / i)) . 0)/] = [\(1 / i)/] by Def3 .= 0 by A1, A2, Th2 ; thus A4: (rfs (1 / i)) . 1 = (rfs (1 / i)) . (0 + 1) .= 1 / (frac ((rfs (1 / i)) . 0)) by Def3 .= 1 / ((1 / i) - 0) by A3, Def3 .= i ; ::_thesis: ( (rfs (1 / i)) . (n + 2) = 0 & (scf (1 / i)) . 0 = 0 & (scf (1 / i)) . 1 = i & (scf (1 / i)) . (n + 2) = 0 ) then A5: (scf (1 / i)) . 1 = [\i/] by Def4; A6: for n being Nat st S2[n] holds S2[n + 1] proof let n be Nat; ::_thesis: ( S2[n] implies S2[n + 1] ) assume A7: S2[n] ; ::_thesis: S2[n + 1] thus (rfs (1 / i)) . ((n + 1) + 2) = (rfs (1 / i)) . ((n + 2) + 1) .= 1 / (frac ((rfs (1 / i)) . (n + 2))) by Def3 .= 1 / (0 - 0) by A7 .= 0 ; ::_thesis: (scf (1 / i)) . ((n + 1) + 2) = 0 hence (scf (1 / i)) . ((n + 1) + 2) = [\0/] by Def4 .= 0 ; ::_thesis: verum end; A8: (rfs (1 / i)) . (0 + 2) = (rfs (1 / i)) . (1 + 1) .= 1 / (frac ((rfs (1 / i)) . 1)) by Def3 .= 1 / (i - i) by A4, INT_1:25 .= 0 ; then (scf (1 / i)) . (0 + 2) = [\0/] by Def4 .= 0 ; then A9: S2[ 0 ] by A8; A10: for n being Nat holds S2[n] from NAT_1:sch_2(A9, A6); (scf (1 / i)) . 0 = [\((rfs (1 / i)) . 0)/] by Def4 .= [\(1 / i)/] by Def3 .= 0 by A1, A2, Th2 ; hence ( (rfs (1 / i)) . (n + 2) = 0 & (scf (1 / i)) . 0 = 0 & (scf (1 / i)) . 1 = i & (scf (1 / i)) . (n + 2) = 0 ) by A5, A10, INT_1:25; ::_thesis: verum end; theorem :: REAL_3:31 for n being Nat for i being Integer st i > 1 holds ( (rfs (1 / i)) . 1 = i & (rfs (1 / i)) . (n + 2) = 0 ) by Lm7; theorem :: REAL_3:32 for n being Nat for i being Integer st i > 1 holds ( (scf (1 / i)) . 0 = 0 & (scf (1 / i)) . 1 = i & (scf (1 / i)) . (n + 2) = 0 ) by Lm7; theorem Th33: :: REAL_3:33 for n being Nat for r being real number st ( for n being Nat holds (scf r) . n = 0 ) holds (rfs r) . n = 0 proof let n be Nat; ::_thesis: for r being real number st ( for n being Nat holds (scf r) . n = 0 ) holds (rfs r) . n = 0 let r be real number ; ::_thesis: ( ( for n being Nat holds (scf r) . n = 0 ) implies (rfs r) . n = 0 ) assume that A1: for n being Nat holds (scf r) . n = 0 and A2: (rfs r) . n <> 0 ; ::_thesis: contradiction A3: (scf r) . n = 0 by A1; set x = (rfs r) . n; A4: (scf r) . n = [\((rfs r) . n)/] by Def4; percases ( (rfs r) . n < 0 or (rfs r) . n >= 1 or ( 0 < (rfs r) . n & (rfs r) . n < 1 ) ) by A2; suppose (rfs r) . n < 0 ; ::_thesis: contradiction hence contradiction by A3, A4, INT_1:def_6; ::_thesis: verum end; suppose (rfs r) . n >= 1 ; ::_thesis: contradiction hence contradiction by A3, A4, INT_1:54; ::_thesis: verum end; suppose ( 0 < (rfs r) . n & (rfs r) . n < 1 ) ; ::_thesis: contradiction then A5: 1 / ((rfs r) . n) > 1 by Th1; A6: ( (scf r) . (n + 1) = 0 & (scf r) . (n + 1) = [\((rfs r) . (n + 1))/] ) by A1, Def4; (rfs r) . (n + 1) = 1 / (frac ((rfs r) . n)) by Def3 .= 1 / (((rfs r) . n) - ((scf r) . n)) by Def4 .= 1 / (((rfs r) . n) - 0) by A1 .= 1 / ((rfs r) . n) ; hence contradiction by A5, A6, INT_1:54; ::_thesis: verum end; end; end; theorem Th34: :: REAL_3:34 for r being real number st ( for n being Nat holds (scf r) . n = 0 ) holds r = 0 proof let r be real number ; ::_thesis: ( ( for n being Nat holds (scf r) . n = 0 ) implies r = 0 ) assume for n being Nat holds (scf r) . n = 0 ; ::_thesis: r = 0 then (rfs r) . 0 = 0 by Th33; hence r = 0 by Def3; ::_thesis: verum end; Lm8: for n being Nat for r being real number holds ( (rfs (1 / (r - ((scf r) . 0)))) . n = (rfs r) . (n + 1) & (scf (1 / (r - ((scf r) . 0)))) . n = (scf r) . (n + 1) ) proof let n be Nat; ::_thesis: for r being real number holds ( (rfs (1 / (r - ((scf r) . 0)))) . n = (rfs r) . (n + 1) & (scf (1 / (r - ((scf r) . 0)))) . n = (scf r) . (n + 1) ) let r be real number ; ::_thesis: ( (rfs (1 / (r - ((scf r) . 0)))) . n = (rfs r) . (n + 1) & (scf (1 / (r - ((scf r) . 0)))) . n = (scf r) . (n + 1) ) set x = r - ((scf r) . 0); defpred S2[ Nat] means ( (rfs (1 / (r - ((scf r) . 0)))) . $1 = (rfs r) . ($1 + 1) & (scf (1 / (r - ((scf r) . 0)))) . $1 = (scf r) . ($1 + 1) ); A1: for n being Nat st S2[n] holds S2[n + 1] proof let n be Nat; ::_thesis: ( S2[n] implies S2[n + 1] ) assume S2[n] ; ::_thesis: S2[n + 1] hence (rfs (1 / (r - ((scf r) . 0)))) . (n + 1) = 1 / (frac ((rfs r) . (n + 1))) by Def3 .= (rfs r) . ((n + 1) + 1) by Def3 ; ::_thesis: (scf (1 / (r - ((scf r) . 0)))) . (n + 1) = (scf r) . ((n + 1) + 1) hence (scf (1 / (r - ((scf r) . 0)))) . (n + 1) = [\((rfs r) . ((n + 1) + 1))/] by Def4 .= (scf r) . ((n + 1) + 1) by Def4 ; ::_thesis: verum end; A2: (rfs (1 / (r - ((scf r) . 0)))) . 0 = 1 / (r - ((scf r) . 0)) by Def3 .= 1 / (((rfs r) . 0) - ((scf r) . 0)) by Def3 .= 1 / (frac ((rfs r) . 0)) by Def4 .= (rfs r) . (0 + 1) by Def3 ; then (scf (1 / (r - ((scf r) . 0)))) . 0 = [\((rfs r) . 1)/] by Def4 .= (scf r) . (0 + 1) by Def4 ; then A3: S2[ 0 ] by A2; for n being Nat holds S2[n] from NAT_1:sch_2(A3, A1); hence ( (rfs (1 / (r - ((scf r) . 0)))) . n = (rfs r) . (n + 1) & (scf (1 / (r - ((scf r) . 0)))) . n = (scf r) . (n + 1) ) ; ::_thesis: verum end; theorem Th35: :: REAL_3:35 for r being real number holds frac r = r - ((scf r) . 0) proof let r be real number ; ::_thesis: frac r = r - ((scf r) . 0) thus frac r = r - [\((rfs r) . 0)/] by Def3 .= r - ((scf r) . 0) by Def4 ; ::_thesis: verum end; theorem :: REAL_3:36 for n being Nat for r being real number holds (rfs r) . (n + 1) = (rfs (1 / (frac r))) . n proof let n be Nat; ::_thesis: for r being real number holds (rfs r) . (n + 1) = (rfs (1 / (frac r))) . n let r be real number ; ::_thesis: (rfs r) . (n + 1) = (rfs (1 / (frac r))) . n frac r = r - ((scf r) . 0) by Th35; hence (rfs r) . (n + 1) = (rfs (1 / (frac r))) . n by Lm8; ::_thesis: verum end; theorem Th37: :: REAL_3:37 for n being Nat for r being real number holds (scf r) . (n + 1) = (scf (1 / (frac r))) . n proof let n be Nat; ::_thesis: for r being real number holds (scf r) . (n + 1) = (scf (1 / (frac r))) . n let r be real number ; ::_thesis: (scf r) . (n + 1) = (scf (1 / (frac r))) . n frac r = r - ((scf r) . 0) by Th35; hence (scf r) . (n + 1) = (scf (1 / (frac r))) . n by Lm8; ::_thesis: verum end; theorem Th38: :: REAL_3:38 for n being Nat for r being real number st n >= 1 holds (scf r) . n >= 0 proof let n be Nat; ::_thesis: for r being real number st n >= 1 holds (scf r) . n >= 0 let r be real number ; ::_thesis: ( n >= 1 implies (scf r) . n >= 0 ) defpred S2[ Nat] means (scf r) . $1 >= 0 ; [\r/] <= r by INT_1:def_6; then frac r >= 0 by XREAL_1:48; then A1: (1 / (frac r)) - 1 >= 0 - 1 by XREAL_1:9; A2: for n being Nat st n >= 1 & S2[n] holds S2[n + 1] proof let n be Nat; ::_thesis: ( n >= 1 & S2[n] implies S2[n + 1] ) assume n >= 1 ; ::_thesis: ( not S2[n] or S2[n + 1] ) [\((rfs r) . n)/] <= (rfs r) . n by INT_1:def_6; then frac ((rfs r) . n) >= 0 by XREAL_1:48; then A3: (1 / (frac ((rfs r) . n))) - 1 >= 0 - 1 by XREAL_1:9; (scf r) . (n + 1) = [\((rfs r) . (n + 1))/] by Def4 .= [\(1 / (frac ((rfs r) . n)))/] by Def3 ; then (scf r) . (n + 1) > (1 / (((rfs r) . n) - [\((rfs r) . n)/])) - 1 by INT_1:def_6; then ((scf r) . (n + 1)) - (- 1) > ((1 / (frac ((rfs r) . n))) - 1) - ((1 / (frac ((rfs r) . n))) - 1) by A3, XREAL_1:14; hence ( not S2[n] or S2[n + 1] ) by INT_1:7; ::_thesis: verum end; (scf r) . 1 = [\((rfs r) . (0 + 1))/] by Def4 .= [\(1 / (frac ((rfs r) . 0)))/] by Def3 .= [\(1 / (frac r))/] by Def3 ; then (scf r) . 1 > (1 / (frac r)) - 1 by INT_1:def_6; then ((scf r) . 1) - (- 1) > ((1 / (frac r)) - 1) - ((1 / (frac r)) - 1) by A1, XREAL_1:14; then A4: S2[1] by INT_1:7; for n being Nat st n >= 1 holds S2[n] from NAT_1:sch_8(A4, A2); hence ( n >= 1 implies (scf r) . n >= 0 ) ; ::_thesis: verum end; theorem :: REAL_3:39 for n being Nat for r being real number st n >= 1 holds (scf r) . n in NAT by Th38, INT_1:3; theorem Th40: :: REAL_3:40 for n being Nat for r being real number st n >= 1 & (scf r) . n <> 0 holds (scf r) . n >= 1 proof let n be Nat; ::_thesis: for r being real number st n >= 1 & (scf r) . n <> 0 holds (scf r) . n >= 1 let r be real number ; ::_thesis: ( n >= 1 & (scf r) . n <> 0 implies (scf r) . n >= 1 ) assume ( n >= 1 & (scf r) . n <> 0 ) ; ::_thesis: (scf r) . n >= 1 then (scf r) . n > 0 by Th38; then (scf r) . n >= 0 + 1 by INT_1:7; hence (scf r) . n >= 1 ; ::_thesis: verum end; theorem Th41: :: REAL_3:41 for m, n, k being Nat holds ( (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)) ) proof 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 Def4 .= m div n by Def3 ; percases ( n = 0 or 0 < n ) ; supposeA2: 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; supposeA6: 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] percases ( a = 0 or a > 0 ) ; supposeA12: 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; percases ( m mod n = 0 or 0 < m mod n ) ; supposeA15: 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; supposeA16: 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; percases ( n mod (m mod n) = 0 or n mod (m mod n) <> 0 ) ; supposeA18: 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; supposeA20: 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, Lm2 .= ((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; percases ( 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; supposeA25: 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)) percases ( 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; supposeA28: 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 ; percases ( 0 = (modSeq (m,n)) . (b1 + 1) or 0 < (modSeq (m,n)) . (b1 + 1) ) ; supposeA32: 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; supposeA33: 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; percases ( ((modSeq (m,n)) . b1) mod ((modSeq (m,n)) . (b1 + 1)) = 0 or ((modSeq (m,n)) . b1) mod ((modSeq (m,n)) . (b1 + 1)) <> 0 ) ; supposeA35: ((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; supposeA37: ((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, Lm2 .= ((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; end; theorem Th42: :: REAL_3:42 for r being real number holds ( r is rational iff ex n being Nat st for m being Nat st m >= n holds (scf r) . m = 0 ) proof let r be real number ; ::_thesis: ( r is rational iff ex n being Nat st for m being Nat st m >= n holds (scf r) . m = 0 ) defpred S2[ Nat] means for s being real number st ( for m being Nat st m >= $1 holds (scf s) . m = 0 ) holds s is rational ; A1: for m being Nat st S2[m] holds S2[m + 1] proof let m be Nat; ::_thesis: ( S2[m] implies S2[m + 1] ) assume A2: S2[m] ; ::_thesis: S2[m + 1] let s be real number ; ::_thesis: ( ( for m being Nat st m >= m + 1 holds (scf s) . m = 0 ) implies s is rational ) assume A3: for n being Nat st n >= m + 1 holds (scf s) . n = 0 ; ::_thesis: s is rational set B = 1 / (s - ((scf s) . 0)); for n being Nat st n >= m holds (scf (1 / (s - ((scf s) . 0)))) . n = 0 proof let n be Nat; ::_thesis: ( n >= m implies (scf (1 / (s - ((scf s) . 0)))) . n = 0 ) assume n >= m ; ::_thesis: (scf (1 / (s - ((scf s) . 0)))) . n = 0 then A4: n + 1 >= m + 1 by XREAL_1:6; thus (scf (1 / (s - ((scf s) . 0)))) . n = (scf s) . (n + 1) by Lm8 .= 0 by A3, A4 ; ::_thesis: verum end; then reconsider B = 1 / (s - ((scf s) . 0)) as rational number by A2; ((scf s) . 0) + (1 / B) is rational ; hence s is rational ; ::_thesis: verum end; thus ( r is rational implies ex n being Nat st for m being Nat st m >= n holds (scf r) . m = 0 ) ::_thesis: ( ex n being Nat st for m being Nat st m >= n holds (scf r) . m = 0 implies r is rational ) proof assume r is rational ; ::_thesis: ex n being Nat st for m being Nat st m >= n holds (scf r) . m = 0 then reconsider r = r as rational number ; consider m, n being Nat such that A5: n <> 0 and A6: frac r = m / n by Th7, INT_1:43; frac r < 1 by INT_1:43; then A7: m < n by A5, A6, XREAL_1:181; set fm = modSeq (n,m); set fd = divSeq (n,m); percases ( m = 0 or m <> 0 ) ; supposeA8: m = 0 ; ::_thesis: ex n being Nat st for m being Nat st m >= n holds (scf r) . m = 0 take 1 ; ::_thesis: for m being Nat st m >= 1 holds (scf r) . m = 0 let a be Nat; ::_thesis: ( a >= 1 implies (scf r) . a = 0 ) assume a >= 1 ; ::_thesis: (scf r) . a = 0 then ex x being Nat st a = x + 1 by NAT_1:6; hence (scf r) . a = 0 by A6, A8, Th30; ::_thesis: verum end; supposeA9: m <> 0 ; ::_thesis: ex n being Nat st for m being Nat st m >= n holds (scf r) . m = 0 consider k being Nat such that A10: (divSeq (n,m)) . k = 0 and (modSeq (n,m)) . k = 0 by Th25; A11: now__::_thesis:_not_k_=_0 assume A12: k = 0 ; ::_thesis: contradiction ( m <= 0 or n div m <> 0 ) by A7, NAT_2:12; hence contradiction by A9, A10, A12, Def2; ::_thesis: verum end; take k + 1 ; ::_thesis: for m being Nat st m >= k + 1 holds (scf r) . m = 0 let a be Nat; ::_thesis: ( a >= k + 1 implies (scf r) . a = 0 ) assume A13: a >= k + 1 ; ::_thesis: (scf r) . a = 0 1 <= k + 1 by NAT_1:11; then reconsider a1 = a - 1 as Element of NAT by A13, INT_1:5, XXREAL_0:2; A14: a = a1 + 1 ; k + 0 < k + 1 by XREAL_1:6; then k < a by A13, XXREAL_0:2; then A15: k <= a1 by A14, NAT_1:13; (scf r) . a = (scf (1 / (frac r))) . a1 by A14, Th37 .= (scf (n / m)) . a1 by A6, XCMPLX_1:57 .= (divSeq (n,m)) . a1 by Th41 .= 0 by A10, A11, A15, Th17 ; hence (scf r) . a = 0 ; ::_thesis: verum end; end; end; given n being Nat such that A16: for m being Nat st m >= n holds (scf r) . m = 0 ; ::_thesis: r is rational A17: S2[ 0 ] proof let s be real number ; ::_thesis: ( ( for m being Nat st m >= 0 holds (scf s) . m = 0 ) implies s is rational ) assume for m being Nat st m >= 0 holds (scf s) . m = 0 ; ::_thesis: s is rational then for m being Nat holds (scf s) . m = 0 ; hence s is rational by Th34; ::_thesis: verum end; for n being Nat holds S2[n] from NAT_1:sch_2(A17, A1); hence r is rational by A16; ::_thesis: verum end; theorem :: REAL_3:43 for r being real number st ( for n being Nat holds (scf r) . n <> 0 ) holds r is irrational proof let r be real number ; ::_thesis: ( ( for n being Nat holds (scf r) . n <> 0 ) implies r is irrational ) assume A1: for n being Nat holds (scf r) . n <> 0 ; ::_thesis: r is irrational for n being Nat ex m being Nat st ( m >= n & not (scf r) . m = 0 ) proof let n be Nat; ::_thesis: ex m being Nat st ( m >= n & not (scf r) . m = 0 ) take n ; ::_thesis: ( n >= n & not (scf r) . n = 0 ) thus ( n >= n & not (scf r) . n = 0 ) by A1; ::_thesis: verum end; hence r is irrational by Th42; ::_thesis: verum end; begin definition let r be real number ; func convergent_numerators r -> Real_Sequence means :Def5: :: REAL_3:def 5 ( it . 0 = (scf r) . 0 & it . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ( for n being Nat holds it . (n + 2) = (((scf r) . (n + 2)) * (it . (n + 1))) + (it . n) ) ); existence ex b1 being Real_Sequence st ( b1 . 0 = (scf r) . 0 & b1 . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ( for n being Nat holds b1 . (n + 2) = (((scf r) . (n + 2)) * (b1 . (n + 1))) + (b1 . n) ) ) proof set s = scf r; deffunc H1( Nat, Real, Real) -> Element of REAL = (((scf r) . ($1 + 2)) * $3) + $2; consider f being Real_Sequence such that A1: ( f . 0 = (scf r) . 0 & f . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 ) and A2: for n being Element of NAT holds f . (n + 2) = H1(n,f . n,f . (n + 1)) from RECDEF_2:sch_5(); take f ; ::_thesis: ( f . 0 = (scf r) . 0 & f . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ( for n being Nat holds f . (n + 2) = (((scf r) . (n + 2)) * (f . (n + 1))) + (f . n) ) ) thus ( f . 0 = (scf r) . 0 & f . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 ) by A1; ::_thesis: for n being Nat holds f . (n + 2) = (((scf r) . (n + 2)) * (f . (n + 1))) + (f . n) let n be Nat; ::_thesis: f . (n + 2) = (((scf r) . (n + 2)) * (f . (n + 1))) + (f . n) n in NAT by ORDINAL1:def_12; hence f . (n + 2) = (((scf r) . (n + 2)) * (f . (n + 1))) + (f . n) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Real_Sequence st b1 . 0 = (scf r) . 0 & b1 . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ( for n being Nat holds b1 . (n + 2) = (((scf r) . (n + 2)) * (b1 . (n + 1))) + (b1 . n) ) & b2 . 0 = (scf r) . 0 & b2 . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ( for n being Nat holds b2 . (n + 2) = (((scf r) . (n + 2)) * (b2 . (n + 1))) + (b2 . n) ) holds b1 = b2 proof set s = scf r; deffunc H1( Nat, Real, Real) -> Element of REAL = (((scf r) . ($1 + 2)) * $3) + $2; let f, g be Real_Sequence; ::_thesis: ( f . 0 = (scf r) . 0 & f . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ( for n being Nat holds f . (n + 2) = (((scf r) . (n + 2)) * (f . (n + 1))) + (f . n) ) & g . 0 = (scf r) . 0 & g . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ( for n being Nat holds g . (n + 2) = (((scf r) . (n + 2)) * (g . (n + 1))) + (g . n) ) implies f = g ) assume that A3: ( f . 0 = (scf r) . 0 & f . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 ) and A4: for k being Nat holds f . (k + 2) = (((scf r) . (k + 2)) * (f . (k + 1))) + (f . k) and A5: ( g . 0 = (scf r) . 0 & g . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 ) and A6: for k being Nat holds g . (k + 2) = (((scf r) . (k + 2)) * (g . (k + 1))) + (g . k) ; ::_thesis: f = g A7: ( g . 0 = (scf r) . 0 & g . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 ) by A5; A8: for k being Element of NAT holds g . (k + 2) = H1(k,g . k,g . (k + 1)) by A6; A9: for k being Element of NAT holds f . (k + 2) = H1(k,f . k,f . (k + 1)) by A4; A10: ( f . 0 = (scf r) . 0 & f . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 ) by A3; f = g from RECDEF_2:sch_7(A10, A9, A7, A8); hence f = g ; ::_thesis: verum end; end; :: deftheorem Def5 defines convergent_numerators REAL_3:def_5_:_ for r being real number for b2 being Real_Sequence holds ( b2 = convergent_numerators r iff ( b2 . 0 = (scf r) . 0 & b2 . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ( for n being Nat holds b2 . (n + 2) = (((scf r) . (n + 2)) * (b2 . (n + 1))) + (b2 . n) ) ) ); definition let r be real number ; set s = scf r; func convergent_denominators r -> Real_Sequence means :Def6: :: REAL_3:def 6 ( it . 0 = 1 & it . 1 = (scf r) . 1 & ( for n being Nat holds it . (n + 2) = (((scf r) . (n + 2)) * (it . (n + 1))) + (it . n) ) ); existence ex b1 being Real_Sequence st ( b1 . 0 = 1 & b1 . 1 = (scf r) . 1 & ( for n being Nat holds b1 . (n + 2) = (((scf r) . (n + 2)) * (b1 . (n + 1))) + (b1 . n) ) ) proof deffunc H1( Nat, Real, Real) -> Element of REAL = (((scf r) . ($1 + 2)) * $3) + $2; consider f being Real_Sequence such that A1: ( f . 0 = 1 & f . 1 = (scf r) . 1 ) and A2: for n being Element of NAT holds f . (n + 2) = H1(n,f . n,f . (n + 1)) from RECDEF_2:sch_5(); take f ; ::_thesis: ( f . 0 = 1 & f . 1 = (scf r) . 1 & ( for n being Nat holds f . (n + 2) = (((scf r) . (n + 2)) * (f . (n + 1))) + (f . n) ) ) thus ( f . 0 = 1 & f . 1 = (scf r) . 1 ) by A1; ::_thesis: for n being Nat holds f . (n + 2) = (((scf r) . (n + 2)) * (f . (n + 1))) + (f . n) let n be Nat; ::_thesis: f . (n + 2) = (((scf r) . (n + 2)) * (f . (n + 1))) + (f . n) n in NAT by ORDINAL1:def_12; hence f . (n + 2) = (((scf r) . (n + 2)) * (f . (n + 1))) + (f . n) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Real_Sequence st b1 . 0 = 1 & b1 . 1 = (scf r) . 1 & ( for n being Nat holds b1 . (n + 2) = (((scf r) . (n + 2)) * (b1 . (n + 1))) + (b1 . n) ) & b2 . 0 = 1 & b2 . 1 = (scf r) . 1 & ( for n being Nat holds b2 . (n + 2) = (((scf r) . (n + 2)) * (b2 . (n + 1))) + (b2 . n) ) holds b1 = b2 proof deffunc H1( Nat, Real, Real) -> Element of REAL = (((scf r) . ($1 + 2)) * $3) + $2; let f, g be Real_Sequence; ::_thesis: ( f . 0 = 1 & f . 1 = (scf r) . 1 & ( for n being Nat holds f . (n + 2) = (((scf r) . (n + 2)) * (f . (n + 1))) + (f . n) ) & g . 0 = 1 & g . 1 = (scf r) . 1 & ( for n being Nat holds g . (n + 2) = (((scf r) . (n + 2)) * (g . (n + 1))) + (g . n) ) implies f = g ) assume that A3: ( f . 0 = 1 & f . 1 = (scf r) . 1 ) and A4: for k being Nat holds f . (k + 2) = (((scf r) . (k + 2)) * (f . (k + 1))) + (f . k) and A5: ( g . 0 = 1 & g . 1 = (scf r) . 1 ) and A6: for k being Nat holds g . (k + 2) = (((scf r) . (k + 2)) * (g . (k + 1))) + (g . k) ; ::_thesis: f = g A7: ( g . 0 = 1 & g . 1 = (scf r) . 1 ) by A5; A8: for k being Element of NAT holds g . (k + 2) = H1(k,g . k,g . (k + 1)) by A6; A9: for k being Element of NAT holds f . (k + 2) = H1(k,f . k,f . (k + 1)) by A4; A10: ( f . 0 = 1 & f . 1 = (scf r) . 1 ) by A3; f = g from RECDEF_2:sch_7(A10, A9, A7, A8); hence f = g ; ::_thesis: verum end; end; :: deftheorem Def6 defines convergent_denominators REAL_3:def_6_:_ for r being real number for b2 being Real_Sequence holds ( b2 = convergent_denominators r iff ( b2 . 0 = 1 & b2 . 1 = (scf r) . 1 & ( for n being Nat holds b2 . (n + 2) = (((scf r) . (n + 2)) * (b2 . (n + 1))) + (b2 . n) ) ) ); notation let r be real number ; synonym c_n r for convergent_numerators r; synonym c_d r for convergent_denominators r; end; theorem Th44: :: REAL_3:44 for r being real number st (scf r) . 0 > 0 holds for n being Nat holds (c_n r) . n in NAT proof let r be real number ; ::_thesis: ( (scf r) . 0 > 0 implies for n being Nat holds (c_n r) . n in NAT ) set s1 = c_n r; set s = scf r; defpred S2[ Nat] means (c_n r) . $1 in NAT ; A1: for n being Nat st S2[n] & S2[n + 1] holds S2[n + 2] proof let n be Nat; ::_thesis: ( S2[n] & S2[n + 1] implies S2[n + 2] ) assume that A2: (c_n r) . n in NAT and A3: (c_n r) . (n + 1) in NAT ; ::_thesis: S2[n + 2] reconsider n2 = (c_n r) . (n + 1) as Element of NAT by A3; reconsider n1 = (c_n r) . n as Element of NAT by A2; n + 2 >= 0 + 1 by XREAL_1:7; then reconsider n3 = (scf r) . (n + 2) as Element of NAT by Th38, INT_1:3; (n3 * n2) + n1 in NAT ; hence S2[n + 2] by Def5; ::_thesis: verum end; assume A4: (scf r) . 0 > 0 ; ::_thesis: for n being Nat holds (c_n r) . n in NAT A5: S2[1] proof reconsider n2 = (scf r) . 0 as Element of NAT by A4, INT_1:3; reconsider n1 = (scf r) . 1 as Element of NAT by Th38, INT_1:3; (n1 * n2) + 1 in NAT ; hence S2[1] by Def5; ::_thesis: verum end; let n be Nat; ::_thesis: (c_n r) . n in NAT (scf r) . 0 in NAT by A4, INT_1:3; then A6: S2[ 0 ] by Def5; for n being Nat holds S2[n] from FIB_NUM:sch_1(A6, A5, A1); hence (c_n r) . n in NAT ; ::_thesis: verum end; theorem Th45: :: REAL_3:45 for r being real number st (scf r) . 0 > 0 holds for n being Nat holds (c_n r) . n > 0 proof let r be real number ; ::_thesis: ( (scf r) . 0 > 0 implies for n being Nat holds (c_n r) . n > 0 ) assume A1: (scf r) . 0 > 0 ; ::_thesis: for n being Nat holds (c_n r) . n > 0 set s1 = c_n r; set s = scf r; defpred S2[ Nat] means (c_n r) . $1 > 0 ; ( (c_n r) . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & (scf r) . 1 >= 0 ) by Def5, Th38; then A2: S2[1] by A1; let n be Nat; ::_thesis: (c_n r) . n > 0 A3: for n being Nat st S2[n] & S2[n + 1] holds S2[n + 2] proof let n be Nat; ::_thesis: ( S2[n] & S2[n + 1] implies S2[n + 2] ) assume A4: ( (c_n r) . n > 0 & (c_n r) . (n + 1) > 0 ) ; ::_thesis: S2[n + 2] n + 2 > 1 + 0 by XREAL_1:8; then A5: (scf r) . (n + 2) >= 0 by Th38; (c_n r) . (n + 2) = (((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n) by Def5; hence S2[n + 2] by A5, A4; ::_thesis: verum end; A6: S2[ 0 ] by A1, Def5; for n being Nat holds S2[n] from FIB_NUM:sch_1(A6, A2, A3); hence (c_n r) . n > 0 ; ::_thesis: verum end; theorem :: REAL_3:46 for r being real number st (scf r) . 0 > 0 holds for n being Nat holds (c_n r) . (n + 2) > ((scf r) . (n + 2)) * ((c_n r) . (n + 1)) proof let r be real number ; ::_thesis: ( (scf r) . 0 > 0 implies for n being Nat holds (c_n r) . (n + 2) > ((scf r) . (n + 2)) * ((c_n r) . (n + 1)) ) assume A1: (scf r) . 0 > 0 ; ::_thesis: for n being Nat holds (c_n r) . (n + 2) > ((scf r) . (n + 2)) * ((c_n r) . (n + 1)) let n be Nat; ::_thesis: (c_n r) . (n + 2) > ((scf r) . (n + 2)) * ((c_n r) . (n + 1)) set s = scf r; set s1 = c_n r; set m = ((scf r) . (n + 2)) * ((c_n r) . (n + 1)); ((c_n r) . (n + 2)) - (((scf r) . (n + 2)) * ((c_n r) . (n + 1))) = ((((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n)) - (((scf r) . (n + 2)) * ((c_n r) . (n + 1))) by Def5; then ((c_n r) . (n + 2)) - (((scf r) . (n + 2)) * ((c_n r) . (n + 1))) > 0 by A1, Th45; then (((c_n r) . (n + 2)) - (((scf r) . (n + 2)) * ((c_n r) . (n + 1)))) + (((scf r) . (n + 2)) * ((c_n r) . (n + 1))) > 0 + (((scf r) . (n + 2)) * ((c_n r) . (n + 1))) by XREAL_1:6; hence (c_n r) . (n + 2) > ((scf r) . (n + 2)) * ((c_n r) . (n + 1)) ; ::_thesis: verum end; theorem :: REAL_3:47 for r being real number for n1, n2 being Nat st (scf r) . 0 > 0 holds for n being Nat st n1 = (c_n r) . (n + 1) & n2 = (c_n r) . n holds n1 gcd n2 = 1 proof let r be real number ; ::_thesis: for n1, n2 being Nat st (scf r) . 0 > 0 holds for n being Nat st n1 = (c_n r) . (n + 1) & n2 = (c_n r) . n holds n1 gcd n2 = 1 let n1, n2 be Nat; ::_thesis: ( (scf r) . 0 > 0 implies for n being Nat st n1 = (c_n r) . (n + 1) & n2 = (c_n r) . n holds n1 gcd n2 = 1 ) set s1 = c_n r; set s = scf r; defpred S2[ Nat] means for n1, n2 being Nat st n1 = (c_n r) . ($1 + 1) & n2 = (c_n r) . $1 holds n1 gcd n2 = 1; assume A1: (scf r) . 0 > 0 ; ::_thesis: for n being Nat st n1 = (c_n r) . (n + 1) & n2 = (c_n r) . n holds n1 gcd n2 = 1 A2: for k being Nat st S2[k] holds S2[k + 1] proof let k be Nat; ::_thesis: ( S2[k] implies S2[k + 1] ) reconsider n3 = (c_n r) . (k + 2) as Element of NAT by A1, Th44; reconsider n2 = (c_n r) . k as Element of NAT by A1, Th44; k + 2 >= 0 + 1 by XREAL_1:7; then reconsider n4 = (scf r) . (k + 2) as Element of NAT by Th38, INT_1:3; reconsider n1 = (c_n r) . (k + 1) as Element of NAT by A1, Th44; assume for n1, n2 being Nat st n1 = (c_n r) . (k + 1) & n2 = (c_n r) . k holds n1 gcd n2 = 1 ; ::_thesis: S2[k + 1] then A3: n1 gcd n2 = 1 ; n3 = (n4 * n1) + n2 by Def5; hence S2[k + 1] by A3, EULER_1:8; ::_thesis: verum end; A4: S2[ 0 ] proof reconsider u = (scf r) . 1 as Element of NAT by Th38, INT_1:3; let n1, n2 be Nat; ::_thesis: ( n1 = (c_n r) . (0 + 1) & n2 = (c_n r) . 0 implies n1 gcd n2 = 1 ) assume that A5: n1 = (c_n r) . (0 + 1) and A6: n2 = (c_n r) . 0 ; ::_thesis: n1 gcd n2 = 1 n1 = (u * ((scf r) . 0)) + 1 by A5, Def5; then A7: n1 = (u * n2) + 1 by A6, Def5; 1 gcd n2 = 1 by NEWTON:51; hence n1 gcd n2 = 1 by A7, EULER_1:8; ::_thesis: verum end; for n being Nat holds S2[n] from NAT_1:sch_2(A4, A2); hence for n being Nat st n1 = (c_n r) . (n + 1) & n2 = (c_n r) . n holds n1 gcd n2 = 1 ; ::_thesis: verum end; theorem :: REAL_3:48 for r being real number st (scf r) . 0 > 0 & ( for n being Nat holds (scf r) . n <> 0 ) holds for n being Nat holds (c_n r) . n >= tau |^ n proof let r be real number ; ::_thesis: ( (scf r) . 0 > 0 & ( for n being Nat holds (scf r) . n <> 0 ) implies for n being Nat holds (c_n r) . n >= tau |^ n ) assume that A1: (scf r) . 0 > 0 and A2: for n being Nat holds (scf r) . n <> 0 ; ::_thesis: for n being Nat holds (c_n r) . n >= tau |^ n set s = scf r; A3: (scf r) . 0 >= 0 + 1 by A1, INT_1:7; set s1 = c_n r; defpred S2[ Nat] means (c_n r) . $1 >= tau |^ $1; A4: for n being Nat st S2[n] & S2[n + 1] holds S2[n + 2] proof let n be Nat; ::_thesis: ( S2[n] & S2[n + 1] implies S2[n + 2] ) assume that A5: (c_n r) . n >= tau |^ n and A6: (c_n r) . (n + 1) >= tau |^ (n + 1) ; ::_thesis: S2[n + 2] A7: (tau |^ (n + 1)) + (tau |^ n) = ((((1 + (sqrt 5)) / 2) |^ n) * ((1 + (sqrt 5)) / 2)) + (((1 + (sqrt 5)) / 2) |^ n) by FIB_NUM:def_1, NEWTON:6 .= (((1 + (sqrt 5)) / 2) |^ n) * ((6 + (2 * (sqrt 5))) / 4) ; sqrt 5 >= 0 by SQUARE_1:def_2; then (1 + (sqrt 5)) / 2 > 0 by XREAL_1:139; then A8: tau |^ (n + 1) > 0 by FIB_NUM:def_1, PREPOWER:6; A9: tau |^ (n + 2) = (((1 + (sqrt 5)) / 2) |^ n) * (((1 + (sqrt 5)) / 2) |^ 2) by FIB_NUM:def_1, NEWTON:8 .= (((1 + (sqrt 5)) / 2) |^ n) * (((1 + (sqrt 5)) / 2) ^2) by WSIERP_1:1 .= (((1 + (sqrt 5)) / 2) |^ n) * ((((1 ^2) + ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2)) / 4) .= (((1 + (sqrt 5)) / 2) |^ n) * (((1 + (2 * (sqrt 5))) + 5) / 4) by SQUARE_1:def_2 .= (((1 + (sqrt 5)) / 2) |^ n) * ((6 + (2 * (sqrt 5))) / 4) ; A10: (c_n r) . ((n + 1) + 1) = (((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n) by Def5; n + 2 >= 0 + 1 by XREAL_1:7; then (scf r) . (n + 2) >= 1 by A2, Th40; then ((scf r) . (n + 2)) * ((c_n r) . (n + 1)) >= 1 * (tau |^ (n + 1)) by A6, A8, XREAL_1:66; hence S2[n + 2] by A5, A10, A7, A9, XREAL_1:7; ::_thesis: verum end; (c_n r) . 0 = (scf r) . 0 by Def5; then A11: S2[ 0 ] by A3, NEWTON:4; (scf r) . 1 >= 1 by A2, Th40; then ((scf r) . 1) * ((scf r) . 0) >= 1 by A3, XREAL_1:159; then A12: (((scf r) . 1) * ((scf r) . 0)) + 1 >= 1 + 1 by XREAL_1:6; let n be Nat; ::_thesis: (c_n r) . n >= tau |^ n sqrt 5 < sqrt (3 ^2) by SQUARE_1:27; then sqrt 5 < 3 by SQUARE_1:22; then 1 + (sqrt 5) < 1 + 3 by XREAL_1:8; then A13: (1 + (sqrt 5)) / 2 < 4 / 2 by XREAL_1:74; ( (c_n r) . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ((1 + (sqrt 5)) / 2) |^ 1 = (1 + (sqrt 5)) / 2 ) by Def5, NEWTON:5; then A14: S2[1] by A12, A13, FIB_NUM:def_1, XXREAL_0:2; for n being Nat holds S2[n] from FIB_NUM:sch_1(A11, A14, A4); hence (c_n r) . n >= tau |^ n ; ::_thesis: verum end; theorem :: REAL_3:49 for b being Nat for r being real number st (scf r) . 0 > 0 & ( for n being Nat holds (scf r) . n <= b ) holds for n being Nat holds (c_n r) . n <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1) proof let b be Nat; ::_thesis: for r being real number st (scf r) . 0 > 0 & ( for n being Nat holds (scf r) . n <= b ) holds for n being Nat holds (c_n r) . n <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1) let r be real number ; ::_thesis: ( (scf r) . 0 > 0 & ( for n being Nat holds (scf r) . n <= b ) implies for n being Nat holds (c_n r) . n <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1) ) assume that A1: (scf r) . 0 > 0 and A2: for n being Nat holds (scf r) . n <= b ; ::_thesis: for n being Nat holds (c_n r) . n <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1) set s1 = c_n r; set s = scf r; A3: (scf r) . 0 <= b by A2; defpred S2[ Nat] means (c_n r) . $1 <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ ($1 + 1); A4: for n being Nat st S2[n] & S2[n + 1] holds S2[n + 2] proof let n be Nat; ::_thesis: ( S2[n] & S2[n + 1] implies S2[n + 2] ) assume that A5: (c_n r) . n <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1) and A6: (c_n r) . (n + 1) <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ ((n + 1) + 1) ; ::_thesis: S2[n + 2] n + 2 >= 0 + 1 by XREAL_1:7; then A7: (scf r) . (n + 2) >= 0 by Th38; ( (scf r) . (n + 2) <= b & (c_n r) . (n + 1) > 0 ) by A1, A2, Th45; then A8: ((scf r) . (n + 2)) * ((c_n r) . (n + 1)) <= b * (((b + (sqrt ((b ^2) + 4))) / 2) |^ ((n + 1) + 1)) by A6, A7, XREAL_1:66; A9: (b * (((b + (sqrt ((b ^2) + 4))) / 2) |^ ((n + 1) + 1))) + (((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)) = (b * ((((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)) * ((b + (sqrt ((b ^2) + 4))) / 2))) + (((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)) by NEWTON:6 .= (((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)) * ((((b ^2) + (b * (sqrt ((b ^2) + 4)))) + 2) / 2) ; A10: ((b + (sqrt ((b ^2) + 4))) / 2) |^ ((n + 2) + 1) = ((b + (sqrt ((b ^2) + 4))) / 2) |^ ((n + 1) + 2) .= (((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)) * (((b + (sqrt ((b ^2) + 4))) / 2) |^ 2) by NEWTON:8 .= (((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)) * (((b + (sqrt ((b ^2) + 4))) / 2) ^2) by WSIERP_1:1 .= (((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)) * ((((b ^2) + ((2 * b) * (sqrt ((b ^2) + 4)))) + ((sqrt ((b ^2) + 4)) ^2)) / (2 * 2)) .= (((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)) * ((((b ^2) + ((2 * b) * (sqrt ((b ^2) + 4)))) + ((b ^2) + 4)) / (2 * 2)) by SQUARE_1:def_2 .= (((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)) * ((((b ^2) + (b * (sqrt ((b ^2) + 4)))) + 2) / 2) ; (c_n r) . ((n + 1) + 1) = (((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n) by Def5; hence S2[n + 2] by A5, A8, A9, A10, XREAL_1:7; ::_thesis: verum end; let n be Nat; ::_thesis: (c_n r) . n <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1) (b ^2) + 4 > b ^2 by XREAL_1:39; then sqrt ((b ^2) + 4) > sqrt (b ^2) by SQUARE_1:27; then A11: sqrt ((b ^2) + 4) > b by SQUARE_1:22; then b + (sqrt ((b ^2) + 4)) > b + b by XREAL_1:8; then (b + (sqrt ((b ^2) + 4))) / 2 > (2 * b) / 2 by XREAL_1:74; then A12: ((b + (sqrt ((b ^2) + 4))) / 2) |^ (0 + 1) > b by NEWTON:5; A13: (scf r) . 1 >= 0 by Th38; A14: (c_n r) . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 by Def5; (scf r) . 1 <= b by A2; then ((scf r) . 1) * ((scf r) . 0) <= b ^2 by A1, A3, A13, XREAL_1:66; then A15: (c_n r) . 1 <= (b ^2) + 1 by A14, XREAL_1:6; b * (sqrt ((b ^2) + 4)) >= b * b by A11, XREAL_1:64; then (b ^2) + (b * (sqrt ((b ^2) + 4))) >= (b ^2) + (b * b) by XREAL_1:6; then ((b ^2) + (b * (sqrt ((b ^2) + 4)))) + 2 >= ((b ^2) + (b ^2)) + 2 by XREAL_1:6; then A16: (((b ^2) + (b * (sqrt ((b ^2) + 4)))) + 2) / 2 >= (2 * ((b ^2) + 1)) / 2 by XREAL_1:72; ((b + (sqrt ((b ^2) + 4))) / 2) |^ (1 + 1) = ((b + (sqrt ((b ^2) + 4))) / 2) ^2 by WSIERP_1:1 .= (((b ^2) + ((2 * b) * (sqrt ((b ^2) + 4)))) + ((sqrt ((b ^2) + 4)) ^2)) / (2 * 2) .= (((b ^2) + ((2 * b) * (sqrt ((b ^2) + 4)))) + ((b ^2) + 4)) / (2 * 2) by SQUARE_1:def_2 .= (((b ^2) + (b * (sqrt ((b ^2) + 4)))) + 2) / 2 ; then A17: S2[1] by A15, A16, XXREAL_0:2; (c_n r) . 0 = (scf r) . 0 by Def5; then A18: S2[ 0 ] by A3, A12, XXREAL_0:2; for n being Nat holds S2[n] from FIB_NUM:sch_1(A18, A17, A4); hence (c_n r) . n <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1) ; ::_thesis: verum end; theorem Th50: :: REAL_3:50 for n being Nat for r being real number holds (c_d r) . n in NAT proof let n be Nat; ::_thesis: for r being real number holds (c_d r) . n in NAT let r be real number ; ::_thesis: (c_d r) . n in NAT set s = scf r; set s2 = c_d r; defpred S2[ Nat] means (c_d r) . $1 in NAT ; (c_d r) . 0 = 1 by Def6; then A1: S2[ 0 ] ; A2: for n being Nat st S2[n] & S2[n + 1] holds S2[n + 2] proof let n be Nat; ::_thesis: ( S2[n] & S2[n + 1] implies S2[n + 2] ) assume that A3: (c_d r) . n in NAT and A4: (c_d r) . (n + 1) in NAT ; ::_thesis: S2[n + 2] reconsider n2 = (c_d r) . (n + 1) as Element of NAT by A4; reconsider n1 = (c_d r) . n as Element of NAT by A3; n + 2 >= 0 + 1 by XREAL_1:7; then reconsider n3 = (scf r) . (n + 2) as Element of NAT by Th38, INT_1:3; (n3 * n2) + n1 in NAT ; hence S2[n + 2] by Def6; ::_thesis: verum end; (c_d r) . 1 = (scf r) . 1 by Def6; then A5: S2[1] by Th38, INT_1:3; for n being Nat holds S2[n] from FIB_NUM:sch_1(A1, A5, A2); hence (c_d r) . n in NAT ; ::_thesis: verum end; theorem Th51: :: REAL_3:51 for n being Nat for r being real number holds (c_d r) . n >= 0 proof let n be Nat; ::_thesis: for r being real number holds (c_d r) . n >= 0 let r be real number ; ::_thesis: (c_d r) . n >= 0 set s = scf r; set s1 = c_d r; defpred S2[ Nat] means (c_d r) . $1 >= 0 ; A1: for n being Nat st S2[n] & S2[n + 1] holds S2[n + 2] proof let n be Nat; ::_thesis: ( S2[n] & S2[n + 1] implies S2[n + 2] ) assume A2: (c_d r) . n >= 0 ; ::_thesis: ( not S2[n + 1] or S2[n + 2] ) A3: (c_d r) . (n + 2) = (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n) by Def6; n + 2 > 1 + 0 by XREAL_1:8; then A4: (scf r) . (n + 2) >= 0 by Th38; assume (c_d r) . (n + 1) >= 0 ; ::_thesis: S2[n + 2] hence S2[n + 2] by A4, A3, A2; ::_thesis: verum end; (scf r) . 1 >= 0 by Th38; then A5: S2[1] by Def6; A6: S2[ 0 ] by Def6; for n being Nat holds S2[n] from FIB_NUM:sch_1(A6, A5, A1); hence (c_d r) . n >= 0 ; ::_thesis: verum end; theorem Th52: :: REAL_3:52 for r being real number st (scf r) . 1 > 0 holds for n being Nat holds (c_d r) . n > 0 proof let r be real number ; ::_thesis: ( (scf r) . 1 > 0 implies for n being Nat holds (c_d r) . n > 0 ) set s = scf r; set s1 = c_d r; defpred S2[ Nat] means (c_d r) . $1 > 0 ; assume (scf r) . 1 > 0 ; ::_thesis: for n being Nat holds (c_d r) . n > 0 then A1: S2[1] by Def6; let n be Nat; ::_thesis: (c_d r) . n > 0 A2: for n being Nat st S2[n] & S2[n + 1] holds S2[n + 2] proof let n be Nat; ::_thesis: ( S2[n] & S2[n + 1] implies S2[n + 2] ) assume A3: (c_d r) . n > 0 ; ::_thesis: ( not S2[n + 1] or S2[n + 2] ) A4: (c_d r) . (n + 2) = (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n) by Def6; n + 2 > 1 + 0 by XREAL_1:8; then A5: (scf r) . (n + 2) >= 0 by Th38; assume (c_d r) . (n + 1) > 0 ; ::_thesis: S2[n + 2] hence S2[n + 2] by A5, A4, A3; ::_thesis: verum end; A6: S2[ 0 ] by Def6; for n being Nat holds S2[n] from FIB_NUM:sch_1(A6, A1, A2); hence (c_d r) . n > 0 ; ::_thesis: verum end; theorem :: REAL_3:53 for n being Nat for r being real number holds (c_d r) . (n + 2) >= ((scf r) . (n + 2)) * ((c_d r) . (n + 1)) proof let n be Nat; ::_thesis: for r being real number holds (c_d r) . (n + 2) >= ((scf r) . (n + 2)) * ((c_d r) . (n + 1)) let r be real number ; ::_thesis: (c_d r) . (n + 2) >= ((scf r) . (n + 2)) * ((c_d r) . (n + 1)) set s = scf r; set s1 = c_d r; set m = ((scf r) . (n + 2)) * ((c_d r) . (n + 1)); ((c_d r) . (n + 2)) - (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) = ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)) - (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) by Def6; then ((c_d r) . (n + 2)) - (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) >= 0 by Th51; then (((c_d r) . (n + 2)) - (((scf r) . (n + 2)) * ((c_d r) . (n + 1)))) + (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) >= 0 + (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) by XREAL_1:6; hence (c_d r) . (n + 2) >= ((scf r) . (n + 2)) * ((c_d r) . (n + 1)) ; ::_thesis: verum end; theorem :: REAL_3:54 for r being real number st (scf r) . 1 > 0 holds for n being Nat holds (c_d r) . (n + 2) > ((scf r) . (n + 2)) * ((c_d r) . (n + 1)) proof let r be real number ; ::_thesis: ( (scf r) . 1 > 0 implies for n being Nat holds (c_d r) . (n + 2) > ((scf r) . (n + 2)) * ((c_d r) . (n + 1)) ) assume A1: (scf r) . 1 > 0 ; ::_thesis: for n being Nat holds (c_d r) . (n + 2) > ((scf r) . (n + 2)) * ((c_d r) . (n + 1)) let n be Nat; ::_thesis: (c_d r) . (n + 2) > ((scf r) . (n + 2)) * ((c_d r) . (n + 1)) set s1 = c_d r; set s = scf r; set m = ((scf r) . (n + 2)) * ((c_d r) . (n + 1)); ((c_d r) . (n + 2)) - (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) = ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)) - (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) by Def6; then ((c_d r) . (n + 2)) - (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) > 0 by A1, Th52; then (((c_d r) . (n + 2)) - (((scf r) . (n + 2)) * ((c_d r) . (n + 1)))) + (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) > 0 + (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) by XREAL_1:6; hence (c_d r) . (n + 2) > ((scf r) . (n + 2)) * ((c_d r) . (n + 1)) ; ::_thesis: verum end; theorem :: REAL_3:55 for r being real number st ( for n being Nat holds (scf r) . n > 0 ) holds for n being Nat st n >= 1 holds 1 / (((c_d r) . n) * ((c_d r) . (n + 1))) < 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2)) proof let r be real number ; ::_thesis: ( ( for n being Nat holds (scf r) . n > 0 ) implies for n being Nat st n >= 1 holds 1 / (((c_d r) . n) * ((c_d r) . (n + 1))) < 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2)) ) set s = scf r; set s2 = c_d r; defpred S2[ Nat] means 1 / (((c_d r) . $1) * ((c_d r) . ($1 + 1))) < 1 / (((scf r) . ($1 + 1)) * (((c_d r) . $1) ^2)); assume A1: for n being Nat holds (scf r) . n > 0 ; ::_thesis: for n being Nat st n >= 1 holds 1 / (((c_d r) . n) * ((c_d r) . (n + 1))) < 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2)) then A2: (scf r) . 2 > 0 ; A3: (scf r) . 1 > 0 by A1; A4: for n being Nat st n >= 1 & S2[n] holds S2[n + 1] proof let n be Nat; ::_thesis: ( n >= 1 & S2[n] implies S2[n + 1] ) assume that n >= 1 and 1 / (((c_d r) . n) * ((c_d r) . (n + 1))) < 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2)) ; ::_thesis: S2[n + 1] A5: (c_d r) . (n + 1) > 0 by A3, Th52; then A6: ((c_d r) . (n + 1)) ^2 > 0 by SQUARE_1:12; (scf r) . (n + 2) > 0 by A1; then A7: ((scf r) . (n + 2)) * (((c_d r) . (n + 1)) ^2) > 0 by A6, XREAL_1:129; (c_d r) . n > 0 by A3, Th52; then A8: ((c_d r) . (n + 1)) * ((c_d r) . n) > 0 by A5, XREAL_1:129; ((c_d r) . (n + 1)) * ((c_d r) . ((n + 1) + 1)) = ((c_d r) . (n + 1)) * ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)) by Def6 .= (((scf r) . (n + 2)) * (((c_d r) . (n + 1)) ^2)) + (((c_d r) . (n + 1)) * ((c_d r) . n)) ; hence S2[n + 1] by A8, A7, XREAL_1:29, XREAL_1:76; ::_thesis: verum end; A9: (scf r) . 1 > 0 by A1; then ((scf r) . 1) ^2 > 0 by SQUARE_1:12; then ((scf r) . 2) * (((scf r) . 1) ^2) > 0 by A2, XREAL_1:129; then A10: 1 / ((((scf r) . 2) * (((scf r) . 1) ^2)) + ((scf r) . 1)) < 1 / (((scf r) . 2) * (((scf r) . 1) ^2)) by A9, XREAL_1:29, XREAL_1:76; let n be Nat; ::_thesis: ( n >= 1 implies 1 / (((c_d r) . n) * ((c_d r) . (n + 1))) < 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2)) ) 1 / (((c_d r) . 1) * ((c_d r) . (1 + 1))) = 1 / (((c_d r) . 1) * ((((scf r) . (0 + 2)) * ((c_d r) . (0 + 1))) + ((c_d r) . 0))) by Def6 .= 1 / (((c_d r) . 1) * ((((scf r) . 2) * ((scf r) . 1)) + ((c_d r) . 0))) by Def6 .= 1 / (((scf r) . 1) * ((((scf r) . 2) * ((scf r) . 1)) + ((c_d r) . 0))) by Def6 .= 1 / (((scf r) . 1) * ((((scf r) . 2) * ((scf r) . 1)) + 1)) by Def6 .= 1 / ((((scf r) . 2) * (((scf r) . 1) ^2)) + ((scf r) . 1)) ; then A11: S2[1] by A10, Def6; for n being Nat st n >= 1 holds S2[n] from NAT_1:sch_8(A11, A4); hence ( n >= 1 implies 1 / (((c_d r) . n) * ((c_d r) . (n + 1))) < 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2)) ) ; ::_thesis: verum end; theorem :: REAL_3:56 for b being Nat for r being real number st ( for n being Nat holds (scf r) . n <= b ) holds for n being Nat holds (c_d r) . (n + 1) <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1) proof let b be Nat; ::_thesis: for r being real number st ( for n being Nat holds (scf r) . n <= b ) holds for n being Nat holds (c_d r) . (n + 1) <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1) let r be real number ; ::_thesis: ( ( for n being Nat holds (scf r) . n <= b ) implies for n being Nat holds (c_d r) . (n + 1) <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1) ) set s = scf r; set s2 = c_d r; defpred S2[ Nat] means (c_d r) . ($1 + 1) <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ ($1 + 1); assume A1: for n being Nat holds (scf r) . n <= b ; ::_thesis: for n being Nat holds (c_d r) . (n + 1) <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1) then A2: (scf r) . 1 <= b ; A3: (scf r) . 2 <= b by A1; ( (scf r) . 2 >= 0 & (scf r) . 1 >= 0 ) by Th38; then A4: ((scf r) . 2) * ((scf r) . 1) <= b ^2 by A2, A3, XREAL_1:66; (c_d r) . (1 + 1) = (((scf r) . (0 + 2)) * ((c_d r) . (0 + 1))) + ((c_d r) . 0) by Def6 .= (((scf r) . 2) * ((c_d r) . 1)) + 1 by Def6 .= (((scf r) . 2) * ((scf r) . 1)) + 1 by Def6 ; then A5: (c_d r) . (1 + 1) <= (b ^2) + 1 by A4, XREAL_1:6; let n be Nat; ::_thesis: (c_d r) . (n + 1) <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1) (b ^2) + 4 > b ^2 by XREAL_1:39; then sqrt ((b ^2) + 4) > sqrt (b ^2) by SQUARE_1:27; then A6: sqrt ((b ^2) + 4) > b by SQUARE_1:22; then b + (sqrt ((b ^2) + 4)) > b + b by XREAL_1:8; then (b + (sqrt ((b ^2) + 4))) / 2 > (2 * b) / 2 by XREAL_1:74; then A7: ((b + (sqrt ((b ^2) + 4))) / 2) |^ (0 + 1) > b by NEWTON:5; A8: for n being Nat st S2[n] & S2[n + 1] holds S2[n + 2] proof let n be Nat; ::_thesis: ( S2[n] & S2[n + 1] implies S2[n + 2] ) assume that A9: (c_d r) . (n + 1) <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1) and A10: (c_d r) . ((n + 1) + 1) <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ ((n + 1) + 1) ; ::_thesis: S2[n + 2] A11: (b * (((b + (sqrt ((b ^2) + 4))) / 2) |^ ((n + 1) + 1))) + (((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)) = (b * ((((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)) * ((b + (sqrt ((b ^2) + 4))) / 2))) + (((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)) by NEWTON:6 .= (((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)) * ((((b ^2) + (b * (sqrt ((b ^2) + 4)))) + 2) / 2) ; n + 3 >= 0 + 1 by XREAL_1:7; then A12: (scf r) . (n + 3) >= 0 by Th38; A13: ((b + (sqrt ((b ^2) + 4))) / 2) |^ ((n + 2) + 1) = ((b + (sqrt ((b ^2) + 4))) / 2) |^ ((n + 1) + 2) .= (((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)) * (((b + (sqrt ((b ^2) + 4))) / 2) |^ 2) by NEWTON:8 .= (((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)) * (((b + (sqrt ((b ^2) + 4))) / 2) ^2) by WSIERP_1:1 .= (((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)) * ((((b ^2) + ((2 * b) * (sqrt ((b ^2) + 4)))) + ((sqrt ((b ^2) + 4)) ^2)) / (2 * 2)) .= (((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)) * ((((b ^2) + ((2 * b) * (sqrt ((b ^2) + 4)))) + ((b ^2) + 4)) / (2 * 2)) by SQUARE_1:def_2 .= (((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)) * ((((b ^2) + (b * (sqrt ((b ^2) + 4)))) + 2) / 2) ; A14: (c_d r) . ((n + 2) + 1) = (((scf r) . ((n + 1) + 2)) * ((c_d r) . ((n + 1) + 1))) + ((c_d r) . (n + 1)) by Def6 .= (((scf r) . (n + 3)) * ((c_d r) . ((n + 1) + 1))) + ((c_d r) . (n + 1)) ; ( (scf r) . (n + 3) <= b & (c_d r) . ((n + 1) + 1) >= 0 ) by A1, Th51; then ((scf r) . (n + 3)) * ((c_d r) . ((n + 1) + 1)) <= b * (((b + (sqrt ((b ^2) + 4))) / 2) |^ ((n + 1) + 1)) by A10, A12, XREAL_1:66; hence S2[n + 2] by A9, A14, A11, A13, XREAL_1:7; ::_thesis: verum end; b * (sqrt ((b ^2) + 4)) >= b * b by A6, XREAL_1:64; then (b ^2) + (b * (sqrt ((b ^2) + 4))) >= (b ^2) + (b * b) by XREAL_1:6; then ((b ^2) + (b * (sqrt ((b ^2) + 4)))) + 2 >= ((b ^2) + (b ^2)) + 2 by XREAL_1:6; then A15: (((b ^2) + (b * (sqrt ((b ^2) + 4)))) + 2) / 2 >= (2 * ((b ^2) + 1)) / 2 by XREAL_1:72; ((b + (sqrt ((b ^2) + 4))) / 2) |^ (1 + 1) = ((b + (sqrt ((b ^2) + 4))) / 2) ^2 by WSIERP_1:1 .= (((b ^2) + ((2 * b) * (sqrt ((b ^2) + 4)))) + ((sqrt ((b ^2) + 4)) ^2)) / (2 * 2) .= (((b ^2) + ((2 * b) * (sqrt ((b ^2) + 4)))) + ((b ^2) + 4)) / (2 * 2) by SQUARE_1:def_2 .= (((b ^2) + (b * (sqrt ((b ^2) + 4)))) + 2) / 2 ; then A16: S2[1] by A5, A15, XXREAL_0:2; (c_d r) . (0 + 1) = (scf r) . 1 by Def6; then A17: S2[ 0 ] by A2, A7, XXREAL_0:2; for n being Nat holds S2[n] from FIB_NUM:sch_1(A17, A16, A8); hence (c_d r) . (n + 1) <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1) ; ::_thesis: verum end; theorem :: REAL_3:57 for n being Nat for r being real number for n1, n2 being Nat st n1 = (c_d r) . (n + 1) & n2 = (c_d r) . n holds n1 gcd n2 = 1 proof let n be Nat; ::_thesis: for r being real number for n1, n2 being Nat st n1 = (c_d r) . (n + 1) & n2 = (c_d r) . n holds n1 gcd n2 = 1 let r be real number ; ::_thesis: for n1, n2 being Nat st n1 = (c_d r) . (n + 1) & n2 = (c_d r) . n holds n1 gcd n2 = 1 let n1, n2 be Nat; ::_thesis: ( n1 = (c_d r) . (n + 1) & n2 = (c_d r) . n implies n1 gcd n2 = 1 ) set s = scf r; set s2 = c_d r; defpred S2[ Nat] means for n1, n2 being Nat st n1 = (c_d r) . ($1 + 1) & n2 = (c_d r) . $1 holds n1 gcd n2 = 1; A1: for k being Nat st S2[k] holds S2[k + 1] proof let k be Nat; ::_thesis: ( S2[k] implies S2[k + 1] ) k + 2 >= 0 + 1 by XREAL_1:7; then reconsider n4 = (scf r) . (k + 2) as Element of NAT by Th38, INT_1:3; reconsider n3 = (c_d r) . (k + 2) as Element of NAT by Th50; reconsider n2 = (c_d r) . k as Element of NAT by Th50; reconsider n1 = (c_d r) . (k + 1) as Element of NAT by Th50; assume for n1, n2 being Nat st n1 = (c_d r) . (k + 1) & n2 = (c_d r) . k holds n1 gcd n2 = 1 ; ::_thesis: S2[k + 1] then A2: n1 gcd n2 = 1 ; n3 = (n4 * n1) + n2 by Def6; hence S2[k + 1] by A2, EULER_1:8; ::_thesis: verum end; A3: S2[ 0 ] proof let n1, n2 be Nat; ::_thesis: ( n1 = (c_d r) . (0 + 1) & n2 = (c_d r) . 0 implies n1 gcd n2 = 1 ) assume that n1 = (c_d r) . (0 + 1) and A4: n2 = (c_d r) . 0 ; ::_thesis: n1 gcd n2 = 1 n1 gcd 1 = 1 by NEWTON:51; hence n1 gcd n2 = 1 by A4, Def6; ::_thesis: verum end; for n being Nat holds S2[n] from NAT_1:sch_2(A3, A1); hence ( n1 = (c_d r) . (n + 1) & n2 = (c_d r) . n implies n1 gcd n2 = 1 ) ; ::_thesis: verum end; theorem Th58: :: REAL_3:58 for r being real number st ( for n being Nat holds (scf r) . n > 0 ) holds for n being Nat holds ((c_d r) . (n + 1)) / ((c_d r) . n) >= 1 / ((scf r) . (n + 2)) proof let r be real number ; ::_thesis: ( ( for n being Nat holds (scf r) . n > 0 ) implies for n being Nat holds ((c_d r) . (n + 1)) / ((c_d r) . n) >= 1 / ((scf r) . (n + 2)) ) set s = scf r; set s1 = c_d r; defpred S2[ Nat] means ((c_d r) . ($1 + 1)) / ((c_d r) . $1) >= 1 / ((scf r) . ($1 + 2)); assume A1: for n being Nat holds (scf r) . n > 0 ; ::_thesis: for n being Nat holds ((c_d r) . (n + 1)) / ((c_d r) . n) >= 1 / ((scf r) . (n + 2)) then A2: (scf r) . 1 <> 0 ; A3: for n being Nat st S2[n] holds S2[n + 1] proof let n be Nat; ::_thesis: ( S2[n] implies S2[n + 1] ) assume ((c_d r) . (n + 1)) / ((c_d r) . n) >= 1 / ((scf r) . (n + 2)) ; ::_thesis: S2[n + 1] set r = (c_d r) . (n + 1); A4: (scf r) . 1 > 0 by A1; then A5: (c_d r) . (n + 1) > 0 by Th52; ( n + 3 >= 0 + 1 & (scf r) . (n + 3) <> 0 ) by A1, XREAL_1:7; then (scf r) . (n + 3) >= 1 by Th40; then A6: 1 / ((scf r) . (n + 3)) <= 1 / 1 by XREAL_1:118; ( n + 2 >= 0 + 1 & (scf r) . (n + 2) <> 0 ) by A1, XREAL_1:7; then A7: (scf r) . (n + 2) >= 1 by Th40; A8: (c_d r) . n > 0 by A4, Th52; ((c_d r) . (n + 2)) / ((c_d r) . (n + 1)) = ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)) / ((c_d r) . (n + 1)) by Def6 .= ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) / ((c_d r) . (n + 1))) + (((c_d r) . n) / ((c_d r) . (n + 1))) .= (((scf r) . (n + 2)) * (((c_d r) . (n + 1)) / ((c_d r) . (n + 1)))) + (((c_d r) . n) / ((c_d r) . (n + 1))) .= ((scf r) . (n + 2)) + (((c_d r) . n) / ((c_d r) . (n + 1))) by A5, XCMPLX_1:88 ; then ((c_d r) . (n + 2)) / ((c_d r) . (n + 1)) >= 1 + 0 by A5, A8, A7, XREAL_1:7; hence S2[n + 1] by A6, XXREAL_0:2; ::_thesis: verum end; (scf r) . 2 <> 0 by A1; then (scf r) . (0 + 2) >= 1 by Th40; then A9: 1 / ((scf r) . (0 + 2)) <= 1 / 1 by XREAL_1:118; ( (c_d r) . 0 = 1 & (c_d r) . 1 = (scf r) . 1 ) by Def6; then ((c_d r) . (0 + 1)) / ((c_d r) . 0) >= 1 by A2, Th40; then A10: S2[ 0 ] by A9, XXREAL_0:2; for n being Nat holds S2[n] from NAT_1:sch_2(A10, A3); hence for n being Nat holds ((c_d r) . (n + 1)) / ((c_d r) . n) >= 1 / ((scf r) . (n + 2)) ; ::_thesis: verum end; theorem :: REAL_3:59 for r being real number st ( for n being Nat holds (scf r) . n > 0 ) holds for n being Nat holds (c_d r) . (n + 2) <= (2 * ((scf r) . (n + 2))) * ((c_d r) . (n + 1)) proof let r be real number ; ::_thesis: ( ( for n being Nat holds (scf r) . n > 0 ) implies for n being Nat holds (c_d r) . (n + 2) <= (2 * ((scf r) . (n + 2))) * ((c_d r) . (n + 1)) ) assume A1: for n being Nat holds (scf r) . n > 0 ; ::_thesis: for n being Nat holds (c_d r) . (n + 2) <= (2 * ((scf r) . (n + 2))) * ((c_d r) . (n + 1)) let n be Nat; ::_thesis: (c_d r) . (n + 2) <= (2 * ((scf r) . (n + 2))) * ((c_d r) . (n + 1)) set s = scf r; set s1 = c_d r; A2: (scf r) . (n + 2) > 0 by A1; (scf r) . 1 > 0 by A1; then A3: (c_d r) . n > 0 by Th52; A4: ((c_d r) . (n + 1)) / ((c_d r) . n) >= 1 / ((scf r) . (n + 2)) by A1, Th58; (((c_d r) . (n + 1)) / ((c_d r) . n)) * ((c_d r) . n) = (((c_d r) . n) / ((c_d r) . n)) * ((c_d r) . (n + 1)) .= (c_d r) . (n + 1) by A3, XCMPLX_1:88 ; then A5: (c_d r) . (n + 1) >= ((c_d r) . n) / ((scf r) . (n + 2)) by A4, A3, XREAL_1:64; (((c_d r) . n) / ((scf r) . (n + 2))) * ((scf r) . (n + 2)) = (((scf r) . (n + 2)) / ((scf r) . (n + 2))) * ((c_d r) . n) .= (c_d r) . n by A2, XCMPLX_1:88 ; then ((c_d r) . (n + 1)) * ((scf r) . (n + 2)) >= (c_d r) . n by A5, A2, XREAL_1:64; then (((c_d r) . (n + 1)) * ((scf r) . (n + 2))) + (((c_d r) . (n + 1)) * ((scf r) . (n + 2))) >= ((c_d r) . n) + (((c_d r) . (n + 1)) * ((scf r) . (n + 2))) by XREAL_1:6; hence (c_d r) . (n + 2) <= (2 * ((scf r) . (n + 2))) * ((c_d r) . (n + 1)) by Def6; ::_thesis: verum end; theorem :: REAL_3:60 for r being real number st ( for n being Nat holds (scf r) . n <> 0 ) holds for n being Nat holds 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2)) <= 1 / (((c_d r) . n) ^2) proof let r be real number ; ::_thesis: ( ( for n being Nat holds (scf r) . n <> 0 ) implies for n being Nat holds 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2)) <= 1 / (((c_d r) . n) ^2) ) assume A1: for n being Nat holds (scf r) . n <> 0 ; ::_thesis: for n being Nat holds 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2)) <= 1 / (((c_d r) . n) ^2) let n be Nat; ::_thesis: 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2)) <= 1 / (((c_d r) . n) ^2) set s = scf r; set s2 = c_d r; (scf r) . 1 <> 0 by A1; then (scf r) . 1 > 0 by Th38; then A2: (c_d r) . n > 0 by Th52; ( n + 1 >= 1 + 0 & (scf r) . (n + 1) <> 0 ) by A1, XREAL_1:7; then ((scf r) . (n + 1)) * (((c_d r) . n) ^2) >= 1 * (((c_d r) . n) ^2) by A2, Th40, XREAL_1:64; hence 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2)) <= 1 / (((c_d r) . n) ^2) by A2, SQUARE_1:12, XREAL_1:118; ::_thesis: verum end; theorem :: REAL_3:61 for r being real number st ( for n being Nat holds (scf r) . n <> 0 ) holds for n being Nat holds (c_d r) . (n + 1) >= tau |^ n proof let r be real number ; ::_thesis: ( ( for n being Nat holds (scf r) . n <> 0 ) implies for n being Nat holds (c_d r) . (n + 1) >= tau |^ n ) set s2 = c_d r; set s = scf r; defpred S2[ Nat] means (c_d r) . ($1 + 1) >= tau |^ $1; sqrt 5 < sqrt (3 ^2) by SQUARE_1:27; then sqrt 5 < 3 by SQUARE_1:22; then 1 + (sqrt 5) < 1 + 3 by XREAL_1:8; then A1: ( ((1 + (sqrt 5)) / 2) |^ 1 = (1 + (sqrt 5)) / 2 & (1 + (sqrt 5)) / 2 < 4 / 2 ) by NEWTON:5, XREAL_1:74; assume A2: for n being Nat holds (scf r) . n <> 0 ; ::_thesis: for n being Nat holds (c_d r) . (n + 1) >= tau |^ n then A3: (scf r) . 1 >= 1 by Th40; then (c_d r) . (0 + 1) >= 1 by Def6; then A4: S2[ 0 ] by NEWTON:4; let n be Nat; ::_thesis: (c_d r) . (n + 1) >= tau |^ n A5: for n being Nat st S2[n] & S2[n + 1] holds S2[n + 2] proof let n be Nat; ::_thesis: ( S2[n] & S2[n + 1] implies S2[n + 2] ) assume that A6: (c_d r) . (n + 1) >= tau |^ n and A7: (c_d r) . ((n + 1) + 1) >= tau |^ (n + 1) ; ::_thesis: S2[n + 2] A8: (tau |^ (n + 1)) + (tau |^ n) = ((((1 + (sqrt 5)) / 2) |^ n) * ((1 + (sqrt 5)) / 2)) + (((1 + (sqrt 5)) / 2) |^ n) by FIB_NUM:def_1, NEWTON:6 .= (((1 + (sqrt 5)) / 2) |^ n) * ((6 + (2 * (sqrt 5))) / 4) ; sqrt 5 >= 0 by SQUARE_1:def_2; then (1 + (sqrt 5)) / 2 > 0 by XREAL_1:139; then A9: tau |^ (n + 1) > 0 by FIB_NUM:def_1, PREPOWER:6; A10: tau |^ (n + 2) = (((1 + (sqrt 5)) / 2) |^ n) * (((1 + (sqrt 5)) / 2) |^ 2) by FIB_NUM:def_1, NEWTON:8 .= (((1 + (sqrt 5)) / 2) |^ n) * (((1 + (sqrt 5)) / 2) ^2) by WSIERP_1:1 .= (((1 + (sqrt 5)) / 2) |^ n) * ((((1 ^2) + ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2)) / 4) .= (((1 + (sqrt 5)) / 2) |^ n) * (((1 + (2 * (sqrt 5))) + 5) / 4) by SQUARE_1:def_2 .= (((1 + (sqrt 5)) / 2) |^ n) * ((6 + (2 * (sqrt 5))) / 4) ; A11: (c_d r) . ((n + 2) + 1) = (((scf r) . ((n + 1) + 2)) * ((c_d r) . ((n + 1) + 1))) + ((c_d r) . (n + 1)) by Def6 .= (((scf r) . (n + 3)) * ((c_d r) . ((n + 1) + 1))) + ((c_d r) . (n + 1)) ; n + 3 >= 0 + 1 by XREAL_1:7; then (scf r) . (n + 3) >= 1 by A2, Th40; then ((scf r) . (n + 3)) * ((c_d r) . ((n + 1) + 1)) >= 1 * (tau |^ (n + 1)) by A7, A9, XREAL_1:66; hence S2[n + 2] by A6, A11, A8, A10, XREAL_1:7; ::_thesis: verum end; (scf r) . 2 >= 1 by A2, Th40; then ((scf r) . 2) * ((scf r) . 1) >= 1 by A3, XREAL_1:159; then A12: (((scf r) . 2) * ((scf r) . 1)) + 1 >= 1 + 1 by XREAL_1:6; (c_d r) . (1 + 1) = (((scf r) . (0 + 2)) * ((c_d r) . (0 + 1))) + ((c_d r) . 0) by Def6 .= (((scf r) . 2) * ((c_d r) . 1)) + 1 by Def6 .= (((scf r) . 2) * ((scf r) . 1)) + 1 by Def6 ; then A13: S2[1] by A12, A1, FIB_NUM:def_1, XXREAL_0:2; for n being Nat holds S2[n] from FIB_NUM:sch_1(A4, A13, A5); hence (c_d r) . (n + 1) >= tau |^ n ; ::_thesis: verum end; theorem :: REAL_3:62 for a being Nat for r being real number st a > 0 & ( for n being Nat holds (scf r) . n >= a ) holds for n being Nat holds (c_d r) . (n + 1) >= ((a + (sqrt ((a ^2) + 4))) / 2) |^ n proof let a be Nat; ::_thesis: for r being real number st a > 0 & ( for n being Nat holds (scf r) . n >= a ) holds for n being Nat holds (c_d r) . (n + 1) >= ((a + (sqrt ((a ^2) + 4))) / 2) |^ n let r be real number ; ::_thesis: ( a > 0 & ( for n being Nat holds (scf r) . n >= a ) implies for n being Nat holds (c_d r) . (n + 1) >= ((a + (sqrt ((a ^2) + 4))) / 2) |^ n ) assume that A1: a > 0 and A2: for n being Nat holds (scf r) . n >= a ; ::_thesis: for n being Nat holds (c_d r) . (n + 1) >= ((a + (sqrt ((a ^2) + 4))) / 2) |^ n set s = scf r; set s2 = c_d r; defpred S2[ Nat] means (c_d r) . ($1 + 1) >= ((a + (sqrt ((a ^2) + 4))) / 2) |^ $1; A3: (scf r) . 1 > 0 by A1, A2; then (scf r) . 1 >= 1 by Th40; then (c_d r) . (0 + 1) >= 1 by Def6; then A4: S2[ 0 ] by NEWTON:4; (scf r) . 2 > 0 by A1, A2; then ((scf r) . 2) * ((scf r) . 1) >= 1 * ((scf r) . 1) by A3, Th40, XREAL_1:64; then A5: (((scf r) . 2) * ((scf r) . 1)) + 1 >= ((scf r) . 1) + 1 by XREAL_1:6; (scf r) . 1 >= a by A2; then ((scf r) . 1) + 1 >= a + 1 by XREAL_1:6; then A6: (((scf r) . 2) * ((scf r) . 1)) + 1 >= a + 1 by A5, XXREAL_0:2; 4 * a > 0 by A1, XREAL_1:129; then (a ^2) + 4 < ((a ^2) + 4) + (4 * a) by XREAL_1:39; then sqrt ((a ^2) + 4) < sqrt ((a + 2) ^2) by SQUARE_1:27; then sqrt ((a ^2) + 4) < a + 2 by SQUARE_1:22; then a + (sqrt ((a ^2) + 4)) < a + (a + 2) by XREAL_1:8; then A7: ( ((a + (sqrt ((a ^2) + 4))) / 2) |^ 1 = (a + (sqrt ((a ^2) + 4))) / 2 & (a + (sqrt ((a ^2) + 4))) / 2 < ((2 * a) + (2 * 1)) / 2 ) by NEWTON:5, XREAL_1:74; let n be Nat; ::_thesis: (c_d r) . (n + 1) >= ((a + (sqrt ((a ^2) + 4))) / 2) |^ n A8: for n being Nat st S2[n] & S2[n + 1] holds S2[n + 2] proof let n be Nat; ::_thesis: ( S2[n] & S2[n + 1] implies S2[n + 2] ) assume that A9: (c_d r) . (n + 1) >= ((a + (sqrt ((a ^2) + 4))) / 2) |^ n and A10: (c_d r) . ((n + 1) + 1) >= ((a + (sqrt ((a ^2) + 4))) / 2) |^ (n + 1) ; ::_thesis: S2[n + 2] A11: (a * (((a + (sqrt ((a ^2) + 4))) / 2) |^ (n + 1))) + (((a + (sqrt ((a ^2) + 4))) / 2) |^ n) = (a * ((((a + (sqrt ((a ^2) + 4))) / 2) |^ n) * ((a + (sqrt ((a ^2) + 4))) / 2))) + (((a + (sqrt ((a ^2) + 4))) / 2) |^ n) by NEWTON:6 .= (((a + (sqrt ((a ^2) + 4))) / 2) |^ n) * ((((a ^2) + (a * (sqrt ((a ^2) + 4)))) + 2) / 2) ; sqrt ((a ^2) + 4) > 0 by SQUARE_1:25; then (a + (sqrt ((a ^2) + 4))) / 2 > 0 by XREAL_1:139; then A12: ((a + (sqrt ((a ^2) + 4))) / 2) |^ (n + 1) > 0 by PREPOWER:6; A13: ((a + (sqrt ((a ^2) + 4))) / 2) |^ (n + 2) = (((a + (sqrt ((a ^2) + 4))) / 2) |^ n) * (((a + (sqrt ((a ^2) + 4))) / 2) |^ 2) by NEWTON:8 .= (((a + (sqrt ((a ^2) + 4))) / 2) |^ n) * (((a + (sqrt ((a ^2) + 4))) / 2) ^2) by WSIERP_1:1 .= (((a + (sqrt ((a ^2) + 4))) / 2) |^ n) * ((((a ^2) + ((2 * a) * (sqrt ((a ^2) + 4)))) + ((sqrt ((a ^2) + 4)) ^2)) / (2 * 2)) .= (((a + (sqrt ((a ^2) + 4))) / 2) |^ n) * ((((a ^2) + ((2 * a) * (sqrt ((a ^2) + 4)))) + ((a ^2) + 4)) / (2 * 2)) by SQUARE_1:def_2 .= (((a + (sqrt ((a ^2) + 4))) / 2) |^ n) * ((((a ^2) + (a * (sqrt ((a ^2) + 4)))) + 2) / 2) ; A14: (c_d r) . ((n + 2) + 1) = (((scf r) . ((n + 1) + 2)) * ((c_d r) . ((n + 1) + 1))) + ((c_d r) . (n + 1)) by Def6 .= (((scf r) . (n + 3)) * ((c_d r) . ((n + 1) + 1))) + ((c_d r) . (n + 1)) ; (scf r) . (n + 3) >= a by A2; then ((scf r) . (n + 3)) * ((c_d r) . ((n + 1) + 1)) >= a * (((a + (sqrt ((a ^2) + 4))) / 2) |^ (n + 1)) by A10, A12, XREAL_1:66; hence S2[n + 2] by A9, A14, A11, A13, XREAL_1:7; ::_thesis: verum end; (c_d r) . (1 + 1) = (((scf r) . (0 + 2)) * ((c_d r) . (0 + 1))) + ((c_d r) . 0) by Def6 .= (((scf r) . 2) * ((c_d r) . 1)) + 1 by Def6 .= (((scf r) . 2) * ((scf r) . 1)) + 1 by Def6 ; then A15: S2[1] by A6, A7, XXREAL_0:2; for n being Nat holds S2[n] from FIB_NUM:sch_1(A4, A15, A8); hence (c_d r) . (n + 1) >= ((a + (sqrt ((a ^2) + 4))) / 2) |^ n ; ::_thesis: verum end; theorem :: REAL_3:63 for n being Nat for r being real number holds ((c_n r) . (n + 2)) / ((c_d r) . (n + 2)) = ((((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n)) / ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)) proof let n be Nat; ::_thesis: for r being real number holds ((c_n r) . (n + 2)) / ((c_d r) . (n + 2)) = ((((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n)) / ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)) let r be real number ; ::_thesis: ((c_n r) . (n + 2)) / ((c_d r) . (n + 2)) = ((((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n)) / ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)) (c_n r) . (n + 2) = (((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n) by Def5; hence ((c_n r) . (n + 2)) / ((c_d r) . (n + 2)) = ((((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n)) / ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)) by Def6; ::_thesis: verum end; theorem Th64: :: REAL_3:64 for n being Nat for r being real number holds (((c_n r) . (n + 1)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 1))) = (- 1) |^ n proof let n be Nat; ::_thesis: for r being real number holds (((c_n r) . (n + 1)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 1))) = (- 1) |^ n let r be real number ; ::_thesis: (((c_n r) . (n + 1)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 1))) = (- 1) |^ n set s = scf r; set s1 = c_n r; set s2 = c_d r; defpred S2[ Nat] means (((c_n r) . ($1 + 1)) * ((c_d r) . $1)) - (((c_n r) . $1) * ((c_d r) . ($1 + 1))) = (- 1) |^ $1; A1: ( (c_d r) . 0 = 1 & (c_d r) . 1 = (scf r) . 1 ) by Def6; A2: for n being Nat st S2[n] holds S2[n + 1] proof let l be Nat; ::_thesis: ( S2[l] implies S2[l + 1] ) assume A3: (((c_n r) . (l + 1)) * ((c_d r) . l)) - (((c_n r) . l) * ((c_d r) . (l + 1))) = (- 1) |^ l ; ::_thesis: S2[l + 1] (((c_n r) . (l + 2)) * ((c_d r) . (l + 1))) - (((c_n r) . (l + 1)) * ((c_d r) . (l + 2))) = (((((scf r) . (l + 2)) * ((c_n r) . (l + 1))) + ((c_n r) . l)) * ((c_d r) . (l + 1))) - (((c_n r) . (l + 1)) * ((c_d r) . (l + 2))) by Def5 .= (((((scf r) . (l + 2)) * ((c_n r) . (l + 1))) * ((c_d r) . (l + 1))) + (((c_n r) . l) * ((c_d r) . (l + 1)))) - (((c_n r) . (l + 1)) * ((((scf r) . (l + 2)) * ((c_d r) . (l + 1))) + ((c_d r) . l))) by Def6 .= (- 1) * ((((c_n r) . (l + 1)) * ((c_d r) . l)) - (((c_n r) . l) * ((c_d r) . (l + 1)))) .= (- 1) |^ (l + 1) by A3, NEWTON:6 ; hence S2[l + 1] ; ::_thesis: verum end; ( (c_n r) . 0 = (scf r) . 0 & (c_n r) . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 ) by Def5; then A4: S2[ 0 ] by A1, NEWTON:4; for n being Nat holds S2[n] from NAT_1:sch_2(A4, A2); hence (((c_n r) . (n + 1)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 1))) = (- 1) |^ n ; ::_thesis: verum end; theorem Th65: :: REAL_3:65 for n being Nat for r being real number st ( for n being Nat holds (c_d r) . n <> 0 ) holds (((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n)) = ((- 1) |^ n) / (((c_d r) . (n + 1)) * ((c_d r) . n)) proof let n be Nat; ::_thesis: for r being real number st ( for n being Nat holds (c_d r) . n <> 0 ) holds (((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n)) = ((- 1) |^ n) / (((c_d r) . (n + 1)) * ((c_d r) . n)) let r be real number ; ::_thesis: ( ( for n being Nat holds (c_d r) . n <> 0 ) implies (((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n)) = ((- 1) |^ n) / (((c_d r) . (n + 1)) * ((c_d r) . n)) ) set s1 = c_n r; set s2 = c_d r; assume for n being Nat holds (c_d r) . n <> 0 ; ::_thesis: (((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n)) = ((- 1) |^ n) / (((c_d r) . (n + 1)) * ((c_d r) . n)) then ( (c_d r) . n <> 0 & (c_d r) . (n + 1) <> 0 ) ; then (((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n)) = ((((c_n r) . (n + 1)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 1)))) / (((c_d r) . (n + 1)) * ((c_d r) . n)) by XCMPLX_1:130 .= ((- 1) |^ n) / (((c_d r) . (n + 1)) * ((c_d r) . n)) by Th64 ; hence (((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n)) = ((- 1) |^ n) / (((c_d r) . (n + 1)) * ((c_d r) . n)) ; ::_thesis: verum end; theorem Th66: :: REAL_3:66 for n being Nat for r being real number holds (((c_n r) . (n + 2)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 2))) = ((- 1) |^ n) * ((scf r) . (n + 2)) proof let n be Nat; ::_thesis: for r being real number holds (((c_n r) . (n + 2)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 2))) = ((- 1) |^ n) * ((scf r) . (n + 2)) let r be real number ; ::_thesis: (((c_n r) . (n + 2)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 2))) = ((- 1) |^ n) * ((scf r) . (n + 2)) set s1 = c_n r; set s2 = c_d r; set s = scf r; (((c_n r) . (n + 2)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 2))) = (((((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 2))) by Def5 .= (((((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n)) * ((c_d r) . n)) - (((c_n r) . n) * ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n))) by Def6 .= ((scf r) . (n + 2)) * ((((c_n r) . (n + 1)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 1)))) .= ((- 1) |^ n) * ((scf r) . (n + 2)) by Th64 ; hence (((c_n r) . (n + 2)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 2))) = ((- 1) |^ n) * ((scf r) . (n + 2)) ; ::_thesis: verum end; theorem :: REAL_3:67 for n being Nat for r being real number st ( for n being Nat holds (c_d r) . n <> 0 ) holds (((c_n r) . (n + 2)) / ((c_d r) . (n + 2))) - (((c_n r) . n) / ((c_d r) . n)) = (((- 1) |^ n) * ((scf r) . (n + 2))) / (((c_d r) . (n + 2)) * ((c_d r) . n)) proof let n be Nat; ::_thesis: for r being real number st ( for n being Nat holds (c_d r) . n <> 0 ) holds (((c_n r) . (n + 2)) / ((c_d r) . (n + 2))) - (((c_n r) . n) / ((c_d r) . n)) = (((- 1) |^ n) * ((scf r) . (n + 2))) / (((c_d r) . (n + 2)) * ((c_d r) . n)) let r be real number ; ::_thesis: ( ( for n being Nat holds (c_d r) . n <> 0 ) implies (((c_n r) . (n + 2)) / ((c_d r) . (n + 2))) - (((c_n r) . n) / ((c_d r) . n)) = (((- 1) |^ n) * ((scf r) . (n + 2))) / (((c_d r) . (n + 2)) * ((c_d r) . n)) ) set s1 = c_n r; set s2 = c_d r; set s = scf r; assume for n being Nat holds (c_d r) . n <> 0 ; ::_thesis: (((c_n r) . (n + 2)) / ((c_d r) . (n + 2))) - (((c_n r) . n) / ((c_d r) . n)) = (((- 1) |^ n) * ((scf r) . (n + 2))) / (((c_d r) . (n + 2)) * ((c_d r) . n)) then ( (c_d r) . n <> 0 & (c_d r) . (n + 2) <> 0 ) ; then (((c_n r) . (n + 2)) / ((c_d r) . (n + 2))) - (((c_n r) . n) / ((c_d r) . n)) = ((((c_n r) . (n + 2)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 2)))) / (((c_d r) . (n + 2)) * ((c_d r) . n)) by XCMPLX_1:130 .= (((- 1) |^ n) * ((scf r) . (n + 2))) / (((c_d r) . (n + 2)) * ((c_d r) . n)) by Th66 ; hence (((c_n r) . (n + 2)) / ((c_d r) . (n + 2))) - (((c_n r) . n) / ((c_d r) . n)) = (((- 1) |^ n) * ((scf r) . (n + 2))) / (((c_d r) . (n + 2)) * ((c_d r) . n)) ; ::_thesis: verum end; theorem :: REAL_3:68 for r being real number st ( for n being Nat holds (scf r) . n <> 0 ) holds for n being Nat st n >= 1 holds ((c_n r) . n) / ((c_d r) . n) = (((c_n r) . (n + 1)) - ((c_n r) . (n - 1))) / (((c_d r) . (n + 1)) - ((c_d r) . (n - 1))) proof let r be real number ; ::_thesis: ( ( for n being Nat holds (scf r) . n <> 0 ) implies for n being Nat st n >= 1 holds ((c_n r) . n) / ((c_d r) . n) = (((c_n r) . (n + 1)) - ((c_n r) . (n - 1))) / (((c_d r) . (n + 1)) - ((c_d r) . (n - 1))) ) set s1 = c_n r; set s2 = c_d r; set s = scf r; defpred S2[ Nat] means ((c_n r) . $1) / ((c_d r) . $1) = (((c_n r) . ($1 + 1)) - ((c_n r) . ($1 - 1))) / (((c_d r) . ($1 + 1)) - ((c_d r) . ($1 - 1))); assume A1: for n being Nat holds (scf r) . n <> 0 ; ::_thesis: for n being Nat st n >= 1 holds ((c_n r) . n) / ((c_d r) . n) = (((c_n r) . (n + 1)) - ((c_n r) . (n - 1))) / (((c_d r) . (n + 1)) - ((c_d r) . (n - 1))) A2: for n being Nat st n >= 1 & S2[n] holds S2[n + 1] proof let n be Nat; ::_thesis: ( n >= 1 & S2[n] implies S2[n + 1] ) assume that n >= 1 and ((c_n r) . n) / ((c_d r) . n) = (((c_n r) . (n + 1)) - ((c_n r) . (n - 1))) / (((c_d r) . (n + 1)) - ((c_d r) . (n - 1))) ; ::_thesis: S2[n + 1] ( ((((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n)) - ((c_n r) . n) = ((c_n r) . (n + 2)) - ((c_n r) . n) & ((c_d r) . (n + 2)) - ((c_d r) . n) = ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)) - ((c_d r) . n) ) by Def5, Def6; hence S2[n + 1] by A1, XCMPLX_1:91; ::_thesis: verum end; let n be Nat; ::_thesis: ( n >= 1 implies ((c_n r) . n) / ((c_d r) . n) = (((c_n r) . (n + 1)) - ((c_n r) . (n - 1))) / (((c_d r) . (n + 1)) - ((c_d r) . (n - 1))) ) (((c_n r) . (1 + 1)) - ((c_n r) . (1 - 1))) / (((c_d r) . (1 + 1)) - ((c_d r) . (1 - 1))) = (((((scf r) . (2 + 0)) * ((c_n r) . (0 + 1))) + ((c_n r) . 0)) - ((c_n r) . 0)) / (((c_d r) . (2 + 0)) - ((c_d r) . 0)) by Def5 .= (((((scf r) . 2) * ((c_n r) . 1)) + ((c_n r) . 0)) - ((c_n r) . 0)) / (((((scf r) . 2) * ((c_d r) . 1)) + ((c_d r) . 0)) - ((c_d r) . 0)) by Def6 .= ((c_n r) . 1) / ((c_d r) . 1) by A1, XCMPLX_1:91 ; then A3: S2[1] ; for n being Nat st n >= 1 holds S2[n] from NAT_1:sch_8(A3, A2); hence ( n >= 1 implies ((c_n r) . n) / ((c_d r) . n) = (((c_n r) . (n + 1)) - ((c_n r) . (n - 1))) / (((c_d r) . (n + 1)) - ((c_d r) . (n - 1))) ) ; ::_thesis: verum end; theorem :: REAL_3:69 for r being real number st ( for n being Nat holds (c_d r) . n <> 0 ) holds for n being Nat holds abs ((((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n))) = 1 / (abs (((c_d r) . (n + 1)) * ((c_d r) . n))) proof let r be real number ; ::_thesis: ( ( for n being Nat holds (c_d r) . n <> 0 ) implies for n being Nat holds abs ((((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n))) = 1 / (abs (((c_d r) . (n + 1)) * ((c_d r) . n))) ) set s1 = c_n r; set s2 = c_d r; assume A1: for n being Nat holds (c_d r) . n <> 0 ; ::_thesis: for n being Nat holds abs ((((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n))) = 1 / (abs (((c_d r) . (n + 1)) * ((c_d r) . n))) let n be Nat; ::_thesis: abs ((((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n))) = 1 / (abs (((c_d r) . (n + 1)) * ((c_d r) . n))) reconsider n = n as Element of NAT by ORDINAL1:def_12; abs ((((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n))) = abs (((- 1) |^ n) / (((c_d r) . (n + 1)) * ((c_d r) . n))) by A1, Th65 .= (abs ((- 1) |^ n)) / (abs (((c_d r) . (n + 1)) * ((c_d r) . n))) by COMPLEX1:67 .= (abs ((- 1) to_power n)) / (abs (((c_d r) . (n + 1)) * ((c_d r) . n))) by POWER:41 .= ((abs (- 1)) to_power n) / (abs (((c_d r) . (n + 1)) * ((c_d r) . n))) by SERIES_1:2 .= ((- (- 1)) to_power n) / (abs (((c_d r) . (n + 1)) * ((c_d r) . n))) by ABSVALUE:def_1 .= 1 / (abs (((c_d r) . (n + 1)) * ((c_d r) . n))) by POWER:26 ; hence abs ((((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n))) = 1 / (abs (((c_d r) . (n + 1)) * ((c_d r) . n))) ; ::_thesis: verum end; theorem :: REAL_3:70 for r being real number st (scf r) . 1 > 0 holds for n being Nat holds ((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) > ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) proof let r be real number ; ::_thesis: ( (scf r) . 1 > 0 implies for n being Nat holds ((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) > ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) ) set s1 = c_n r; set s2 = c_d r; set s = scf r; defpred S2[ Nat] means ((c_n r) . ((2 * $1) + 1)) / ((c_d r) . ((2 * $1) + 1)) > ((c_n r) . (2 * $1)) / ((c_d r) . (2 * $1)); A1: ((c_n r) . (2 * 0)) / ((c_d r) . (2 * 0)) = ((scf r) . 0) / ((c_d r) . 0) by Def5 .= ((scf r) . 0) / 1 by Def6 .= (scf r) . 0 ; assume A2: (scf r) . 1 > 0 ; ::_thesis: for n being Nat holds ((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) > ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) A3: for n being Nat st S2[n] holds S2[n + 1] proof let n be Nat; ::_thesis: ( S2[n] implies S2[n + 1] ) assume ((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) > ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) ; ::_thesis: S2[n + 1] reconsider n = n as Element of NAT by ORDINAL1:def_12; (((c_n r) . ((2 * (n + 1)) + 1)) * ((c_d r) . (2 * (n + 1)))) - (((c_n r) . (2 * (n + 1))) * ((c_d r) . ((2 * (n + 1)) + 1))) = (- 1) |^ (2 * (n + 1)) by Th64 .= 1 |^ (2 * (n + 1)) by WSIERP_1:2 .= 1 by NEWTON:10 ; then A4: ((c_n r) . ((2 * (n + 1)) + 1)) * ((c_d r) . (2 * (n + 1))) > ((c_n r) . (2 * (n + 1))) * ((c_d r) . ((2 * (n + 1)) + 1)) by XREAL_1:47; ( (c_d r) . ((2 * (n + 1)) + 1) > 0 & (c_d r) . (2 * (n + 1)) > 0 ) by A2, Th52; hence S2[n + 1] by A4, XREAL_1:106; ::_thesis: verum end; ((c_n r) . ((2 * 0) + 1)) / ((c_d r) . ((2 * 0) + 1)) = ((((scf r) . 1) * ((scf r) . 0)) + 1) / ((c_d r) . 1) by Def5 .= ((((scf r) . 1) * ((scf r) . 0)) + 1) / ((scf r) . 1) by Def6 .= ((scf r) . 0) + (1 / ((scf r) . 1)) by A2, XCMPLX_1:113 ; then A5: S2[ 0 ] by A2, A1, XREAL_1:29; for n being Nat holds S2[n] from NAT_1:sch_2(A5, A3); hence for n being Nat holds ((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) > ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) ; ::_thesis: verum end; definition let r be real number ; func convergents_of_continued_fractions r -> Real_Sequence equals :: REAL_3:def 7 (c_n r) /" (c_d r); coherence (c_n r) /" (c_d r) is Real_Sequence ; end; :: deftheorem defines convergents_of_continued_fractions REAL_3:def_7_:_ for r being real number holds convergents_of_continued_fractions r = (c_n r) /" (c_d r); notation let r be real number ; synonym cocf r for convergents_of_continued_fractions r; end; theorem :: REAL_3:71 for r being real number holds (cocf r) . 0 = (scf r) . 0 proof let r be real number ; ::_thesis: (cocf r) . 0 = (scf r) . 0 thus (cocf r) . 0 = ((c_n r) . 0) * (((c_d r) ") . 0) by SEQ_1:8 .= ((c_n r) . 0) * (((c_d r) . 0) ") by VALUED_1:10 .= ((c_n r) . 0) * (1 / ((c_d r) . 0)) .= ((c_n r) . 0) / ((c_d r) . 0) .= ((scf r) . 0) / ((c_d r) . 0) by Def5 .= ((scf r) . 0) / 1 by Def6 .= (scf r) . 0 ; ::_thesis: verum end; theorem Th72: :: REAL_3:72 for r being real number st (scf r) . 1 <> 0 holds (cocf r) . 1 = ((scf r) . 0) + (1 / ((scf r) . 1)) proof let r be real number ; ::_thesis: ( (scf r) . 1 <> 0 implies (cocf r) . 1 = ((scf r) . 0) + (1 / ((scf r) . 1)) ) set s = scf r; assume A1: (scf r) . 1 <> 0 ; ::_thesis: (cocf r) . 1 = ((scf r) . 0) + (1 / ((scf r) . 1)) thus (cocf r) . 1 = ((c_n r) . 1) * (((c_d r) ") . 1) by SEQ_1:8 .= ((c_n r) . 1) * (((c_d r) . 1) ") by VALUED_1:10 .= ((c_n r) . 1) * (1 / ((c_d r) . 1)) .= ((c_n r) . 1) / ((c_d r) . 1) .= ((((scf r) . 1) * ((scf r) . 0)) + 1) / ((c_d r) . 1) by Def5 .= ((((scf r) . 1) * ((scf r) . 0)) + 1) / ((scf r) . 1) by Def6 .= ((scf r) . 0) + (1 / ((scf r) . 1)) by A1, XCMPLX_1:113 ; ::_thesis: verum end; theorem Th73: :: REAL_3:73 for r being real number st ( for n being Nat holds (scf r) . n > 0 ) holds (cocf r) . 2 = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / ((scf r) . 2)))) proof let r be real number ; ::_thesis: ( ( for n being Nat holds (scf r) . n > 0 ) implies (cocf r) . 2 = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / ((scf r) . 2)))) ) set s = scf r; A1: (cocf r) . 2 = ((c_n r) . 2) * (((c_d r) ") . 2) by SEQ_1:8 .= ((c_n r) . 2) * (((c_d r) . 2) ") by VALUED_1:10 .= ((c_n r) . 2) * (1 / ((c_d r) . 2)) .= ((c_n r) . 2) / ((c_d r) . 2) ; assume A2: for n being Nat holds (scf r) . n > 0 ; ::_thesis: (cocf r) . 2 = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / ((scf r) . 2)))) then A3: (scf r) . 1 > 0 ; A4: (c_d r) . 2 = (((scf r) . (0 + 2)) * ((c_d r) . (0 + 1))) + ((c_d r) . 0) by Def6 .= (((scf r) . 2) * ((scf r) . 1)) + ((c_d r) . 0) by Def6 .= (((scf r) . 2) * ((scf r) . 1)) + 1 by Def6 ; A5: (c_n r) . 2 = (((scf r) . (0 + 2)) * ((c_n r) . (0 + 1))) + ((c_n r) . 0) by Def5 .= (((scf r) . 2) * ((((scf r) . 1) * ((scf r) . 0)) + 1)) + ((c_n r) . 0) by Def5 .= (((((scf r) . 2) * ((scf r) . 1)) * ((scf r) . 0)) + ((scf r) . 2)) + ((scf r) . 0) by Def5 ; A6: (scf r) . 2 > 0 by A2; then ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / ((scf r) . 2)))) = ((scf r) . 0) + (1 / (((((scf r) . 1) * ((scf r) . 2)) + 1) / ((scf r) . 2))) by XCMPLX_1:113 .= ((scf r) . 0) + (((scf r) . 2) / ((((scf r) . 1) * ((scf r) . 2)) + 1)) by XCMPLX_1:57 .= ((((scf r) . 0) * ((((scf r) . 1) * ((scf r) . 2)) + 1)) + ((scf r) . 2)) / ((((scf r) . 1) * ((scf r) . 2)) + 1) by A3, A6, XCMPLX_1:113 .= (cocf r) . 2 by A1, A5, A4 ; hence (cocf r) . 2 = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / ((scf r) . 2)))) ; ::_thesis: verum end; theorem Th74: :: REAL_3:74 for r being real number st ( for n being Nat holds (scf r) . n > 0 ) holds (cocf r) . 3 = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / (((scf r) . 2) + (1 / ((scf r) . 3)))))) proof let r be real number ; ::_thesis: ( ( for n being Nat holds (scf r) . n > 0 ) implies (cocf r) . 3 = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / (((scf r) . 2) + (1 / ((scf r) . 3)))))) ) set s = scf r; A1: (cocf r) . 3 = ((c_n r) . 3) * (((c_d r) ") . 3) by SEQ_1:8 .= ((c_n r) . 3) * (((c_d r) . 3) ") by VALUED_1:10 .= ((c_n r) . 3) * (1 / ((c_d r) . 3)) .= ((c_n r) . 3) / ((c_d r) . 3) ; assume A2: for n being Nat holds (scf r) . n > 0 ; ::_thesis: (cocf r) . 3 = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / (((scf r) . 2) + (1 / ((scf r) . 3)))))) then A3: (scf r) . 1 > 0 ; A4: (c_d r) . 2 = (((scf r) . (0 + 2)) * ((c_d r) . (0 + 1))) + ((c_d r) . 0) by Def6 .= (((scf r) . 2) * ((scf r) . 1)) + ((c_d r) . 0) by Def6 .= (((scf r) . 2) * ((scf r) . 1)) + 1 by Def6 ; A5: (c_d r) . 3 = (((scf r) . (1 + 2)) * ((c_d r) . (1 + 1))) + ((c_d r) . 1) by Def6 .= (((scf r) . 3) * ((((scf r) . 2) * ((scf r) . 1)) + 1)) + ((scf r) . 1) by A4, Def6 .= (((scf r) . 1) * ((((scf r) . 2) * ((scf r) . 3)) + 1)) + ((scf r) . 3) ; A6: (c_n r) . 2 = (((scf r) . (0 + 2)) * ((c_n r) . (0 + 1))) + ((c_n r) . 0) by Def5 .= (((scf r) . 2) * ((((scf r) . 1) * ((scf r) . 0)) + 1)) + ((c_n r) . 0) by Def5 .= (((((scf r) . 2) * ((scf r) . 1)) * ((scf r) . 0)) + ((scf r) . 2)) + ((scf r) . 0) by Def5 ; A7: (c_n r) . 3 = (((scf r) . (1 + 2)) * ((c_n r) . (1 + 1))) + ((c_n r) . 1) by Def5 .= (((scf r) . 3) * ((((((scf r) . 2) * ((scf r) . 1)) * ((scf r) . 0)) + ((scf r) . 2)) + ((scf r) . 0))) + ((((scf r) . 1) * ((scf r) . 0)) + 1) by A6, Def5 .= ((((((((scf r) . 3) * ((scf r) . 2)) * ((scf r) . 1)) * ((scf r) . 0)) + (((scf r) . 3) * ((scf r) . 2))) + (((scf r) . 3) * ((scf r) . 0))) + (((scf r) . 1) * ((scf r) . 0))) + 1 ; A8: (scf r) . 2 > 0 by A2; A9: (scf r) . 3 > 0 by A2; then ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / (((scf r) . 2) + (1 / ((scf r) . 3)))))) = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / (((((scf r) . 2) * ((scf r) . 3)) + 1) / ((scf r) . 3))))) by XCMPLX_1:113 .= ((scf r) . 0) + (1 / (((scf r) . 1) + (((scf r) . 3) / ((((scf r) . 2) * ((scf r) . 3)) + 1)))) by XCMPLX_1:57 .= ((scf r) . 0) + (1 / (((((scf r) . 1) * ((((scf r) . 2) * ((scf r) . 3)) + 1)) + ((scf r) . 3)) / ((((scf r) . 2) * ((scf r) . 3)) + 1))) by A8, A9, XCMPLX_1:113 .= ((scf r) . 0) + (((((scf r) . 2) * ((scf r) . 3)) + 1) / ((((scf r) . 1) * ((((scf r) . 2) * ((scf r) . 3)) + 1)) + ((scf r) . 3))) by XCMPLX_1:57 .= ((((scf r) . 0) * ((((scf r) . 1) * ((((scf r) . 2) * ((scf r) . 3)) + 1)) + ((scf r) . 3))) + ((((scf r) . 2) * ((scf r) . 3)) + 1)) / ((((scf r) . 1) * ((((scf r) . 2) * ((scf r) . 3)) + 1)) + ((scf r) . 3)) by A3, A8, A9, XCMPLX_1:113 ; hence (cocf r) . 3 = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / (((scf r) . 2) + (1 / ((scf r) . 3)))))) by A1, A7, A5; ::_thesis: verum end; theorem :: REAL_3:75 for r being real number st ( for n being Nat holds (scf r) . n > 0 ) holds for n being Nat st n >= 1 holds ((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1)) proof let r be real number ; ::_thesis: ( ( for n being Nat holds (scf r) . n > 0 ) implies for n being Nat st n >= 1 holds ((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1)) ) set s = scf r; set s1 = c_n r; set s2 = c_d r; defpred S2[ Nat] means ((c_n r) . ((2 * $1) + 1)) / ((c_d r) . ((2 * $1) + 1)) < ((c_n r) . ((2 * $1) - 1)) / ((c_d r) . ((2 * $1) - 1)); assume A1: for n being Nat holds (scf r) . n > 0 ; ::_thesis: for n being Nat st n >= 1 holds ((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1)) then A2: (scf r) . 3 > 0 ; (cocf r) . 3 = ((c_n r) . 3) * (((c_d r) ") . 3) by SEQ_1:8 .= ((c_n r) . 3) * (((c_d r) . 3) ") by VALUED_1:10 .= ((c_n r) . 3) * (1 / ((c_d r) . 3)) .= ((c_n r) . 3) / ((c_d r) . 3) ; then A3: ((c_n r) . ((2 * 1) + 1)) / ((c_d r) . ((2 * 1) + 1)) = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / (((scf r) . 2) + (1 / ((scf r) . 3)))))) by A1, Th74 .= ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / (((((scf r) . 2) * ((scf r) . 3)) + 1) / ((scf r) . 3))))) by A2, XCMPLX_1:113 .= ((scf r) . 0) + (1 / (((scf r) . 1) + (((scf r) . 3) / ((((scf r) . 2) * ((scf r) . 3)) + 1)))) by XCMPLX_1:57 ; let n be Nat; ::_thesis: ( n >= 1 implies ((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1)) ) A4: (scf r) . 1 > 0 by A1; A5: (scf r) . 1 > 0 by A1; A6: for n being Nat st n >= 1 & S2[n] holds S2[n + 1] proof let n be Nat; ::_thesis: ( n >= 1 & S2[n] implies S2[n + 1] ) assume that n >= 1 and ((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1)) ; ::_thesis: S2[n + 1] (((c_n r) . ((2 * (n + 1)) + 1)) * ((c_d r) . ((2 * (n + 1)) - 1))) - (((c_n r) . ((2 * (n + 1)) - 1)) * ((c_d r) . ((2 * (n + 1)) + 1))) = (((((scf r) . (((2 * n) + 1) + 2)) * ((c_n r) . (((2 * n) + 1) + 1))) + ((c_n r) . ((2 * n) + 1))) * ((c_d r) . ((2 * n) + 1))) - (((c_n r) . ((2 * n) + 1)) * ((c_d r) . ((2 * n) + 3))) by Def5 .= (((((scf r) . (((2 * n) + 1) + 2)) * ((c_n r) . (((2 * n) + 1) + 1))) + ((c_n r) . ((2 * n) + 1))) * ((c_d r) . ((2 * n) + 1))) - (((c_n r) . ((2 * n) + 1)) * ((((scf r) . (((2 * n) + 1) + 2)) * ((c_d r) . (((2 * n) + 1) + 1))) + ((c_d r) . ((2 * n) + 1)))) by Def6 .= ((scf r) . (((2 * n) + 1) + 2)) * ((((c_n r) . (((2 * n) + 1) + 1)) * ((c_d r) . ((2 * n) + 1))) - (((c_n r) . ((2 * n) + 1)) * ((c_d r) . (((2 * n) + 1) + 1)))) .= ((scf r) . (((2 * n) + 1) + 2)) * ((- 1) |^ ((2 * n) + 1)) by Th64 .= ((scf r) . (((2 * n) + 1) + 2)) * (- (1 |^ ((2 * n) + 1))) by WSIERP_1:2 .= ((scf r) . (((2 * n) + 1) + 2)) * (- 1) by NEWTON:10 ; then (((c_n r) . ((2 * (n + 1)) + 1)) * ((c_d r) . ((2 * (n + 1)) - 1))) - (((c_n r) . ((2 * (n + 1)) - 1)) * ((c_d r) . ((2 * (n + 1)) + 1))) < 0 by A1, XREAL_1:132; then A7: ((c_n r) . ((2 * (n + 1)) + 1)) * ((c_d r) . ((2 * (n + 1)) - 1)) < ((c_n r) . ((2 * (n + 1)) - 1)) * ((c_d r) . ((2 * (n + 1)) + 1)) by XREAL_1:48; ( (c_d r) . ((2 * n) + 1) > 0 & (c_d r) . ((2 * n) + 3) > 0 ) by A5, Th52; hence S2[n + 1] by A7, XREAL_1:106; ::_thesis: verum end; (scf r) . 2 > 0 by A1; then ((scf r) . 3) / ((((scf r) . 2) * ((scf r) . 3)) + 1) > 0 by A2, XREAL_1:139; then A8: 1 / (((scf r) . 1) + (((scf r) . 3) / ((((scf r) . 2) * ((scf r) . 3)) + 1))) < 1 / ((scf r) . 1) by A4, XREAL_1:29, XREAL_1:76; ((c_n r) . ((2 * 1) - 1)) / ((c_d r) . ((2 * 1) - 1)) = ((((scf r) . 1) * ((scf r) . 0)) + 1) / ((c_d r) . 1) by Def5 .= ((((scf r) . 1) * ((scf r) . 0)) + 1) / ((scf r) . 1) by Def6 .= ((scf r) . 0) + (1 / ((scf r) . 1)) by A4, XCMPLX_1:113 ; then A9: S2[1] by A8, A3, XREAL_1:8; for n being Nat st n >= 1 holds S2[n] from NAT_1:sch_8(A9, A6); hence ( n >= 1 implies ((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1)) ) ; ::_thesis: verum end; theorem :: REAL_3:76 for r being real number st ( for n being Nat holds (scf r) . n > 0 ) holds for n being Nat st n >= 1 holds ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) > ((c_n r) . ((2 * n) - 2)) / ((c_d r) . ((2 * n) - 2)) proof let r be real number ; ::_thesis: ( ( for n being Nat holds (scf r) . n > 0 ) implies for n being Nat st n >= 1 holds ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) > ((c_n r) . ((2 * n) - 2)) / ((c_d r) . ((2 * n) - 2)) ) set s = scf r; set s1 = c_n r; set s2 = c_d r; defpred S2[ Nat] means ((c_n r) . (2 * $1)) / ((c_d r) . (2 * $1)) > ((c_n r) . ((2 * $1) - 2)) / ((c_d r) . ((2 * $1) - 2)); assume A1: for n being Nat holds (scf r) . n > 0 ; ::_thesis: for n being Nat st n >= 1 holds ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) > ((c_n r) . ((2 * n) - 2)) / ((c_d r) . ((2 * n) - 2)) then A2: (scf r) . 1 > 0 ; A3: (scf r) . 1 > 0 by A1; A4: for n being Nat st n >= 1 & S2[n] holds S2[n + 1] proof let n be Nat; ::_thesis: ( n >= 1 & S2[n] implies S2[n + 1] ) assume that n >= 1 and ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) > ((c_n r) . ((2 * n) - 2)) / ((c_d r) . ((2 * n) - 2)) ; ::_thesis: S2[n + 1] (((c_n r) . (2 * (n + 1))) * ((c_d r) . ((2 * (n + 1)) - 2))) - (((c_n r) . ((2 * (n + 1)) - 2)) * ((c_d r) . (2 * (n + 1)))) = (((((scf r) . ((2 * n) + 2)) * ((c_n r) . ((2 * n) + 1))) + ((c_n r) . (2 * n))) * ((c_d r) . (2 * n))) - (((c_n r) . (2 * n)) * ((c_d r) . ((2 * n) + 2))) by Def5 .= (((((scf r) . ((2 * n) + 2)) * ((c_n r) . ((2 * n) + 1))) + ((c_n r) . (2 * n))) * ((c_d r) . (2 * n))) - (((c_n r) . (2 * n)) * ((((scf r) . ((2 * n) + 2)) * ((c_d r) . ((2 * n) + 1))) + ((c_d r) . (2 * n)))) by Def6 .= ((scf r) . ((2 * n) + 2)) * ((((c_n r) . ((2 * n) + 1)) * ((c_d r) . (2 * n))) - (((c_n r) . (2 * n)) * ((c_d r) . ((2 * n) + 1)))) .= ((scf r) . ((2 * n) + 2)) * ((- 1) |^ (2 * n)) by Th64 .= ((scf r) . ((2 * n) + 2)) * (1 |^ (2 * n)) by WSIERP_1:2 .= ((scf r) . ((2 * n) + 2)) * 1 by NEWTON:10 .= (scf r) . ((2 * n) + 2) ; then A5: ((c_n r) . (2 * (n + 1))) * ((c_d r) . ((2 * (n + 1)) - 2)) > ((c_n r) . ((2 * (n + 1)) - 2)) * ((c_d r) . (2 * (n + 1))) by A1, XREAL_1:47; ( (c_d r) . (2 * n) > 0 & (c_d r) . ((2 * n) + 2) > 0 ) by A3, Th52; hence S2[n + 1] by A5, XREAL_1:106; ::_thesis: verum end; let n be Nat; ::_thesis: ( n >= 1 implies ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) > ((c_n r) . ((2 * n) - 2)) / ((c_d r) . ((2 * n) - 2)) ) A6: ((c_n r) . ((2 * 1) - 2)) / ((c_d r) . ((2 * 1) - 2)) = ((scf r) . 0) / ((c_d r) . 0) by Def5 .= ((scf r) . 0) / 1 by Def6 .= (scf r) . 0 ; A7: (scf r) . 2 > 0 by A1; (cocf r) . 2 = ((c_n r) . 2) * (((c_d r) ") . 2) by SEQ_1:8 .= ((c_n r) . 2) * (((c_d r) . 2) ") by VALUED_1:10 .= ((c_n r) . 2) * (1 / ((c_d r) . 2)) .= ((c_n r) . 2) / ((c_d r) . 2) ; then ((c_n r) . (2 * 1)) / ((c_d r) . (2 * 1)) = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / ((scf r) . 2)))) by A1, Th73 .= ((scf r) . 0) + (1 / (((((scf r) . 1) * ((scf r) . 2)) + 1) / ((scf r) . 2))) by A7, XCMPLX_1:113 .= ((scf r) . 0) + (((scf r) . 2) / ((((scf r) . 1) * ((scf r) . 2)) + 1)) by XCMPLX_1:57 ; then A8: S2[1] by A2, A7, A6, XREAL_1:29, XREAL_1:139; for n being Nat st n >= 1 holds S2[n] from NAT_1:sch_8(A8, A4); hence ( n >= 1 implies ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) > ((c_n r) . ((2 * n) - 2)) / ((c_d r) . ((2 * n) - 2)) ) ; ::_thesis: verum end; theorem :: REAL_3:77 for r being real number st ( for n being Nat holds (scf r) . n > 0 ) holds for n being Nat st n >= 1 holds ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1)) proof let r be real number ; ::_thesis: ( ( for n being Nat holds (scf r) . n > 0 ) implies for n being Nat st n >= 1 holds ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1)) ) set s = scf r; set s1 = c_n r; set s2 = c_d r; defpred S2[ Nat] means ((c_n r) . (2 * $1)) / ((c_d r) . (2 * $1)) < ((c_n r) . ((2 * $1) - 1)) / ((c_d r) . ((2 * $1) - 1)); assume A1: for n being Nat holds (scf r) . n > 0 ; ::_thesis: for n being Nat st n >= 1 holds ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1)) then ( (scf r) . 1 > 0 & (scf r) . 2 > 0 ) ; then A2: 1 / (((scf r) . 1) + (1 / ((scf r) . 2))) < 1 / ((scf r) . 1) by XREAL_1:29, XREAL_1:76; let n be Nat; ::_thesis: ( n >= 1 implies ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1)) ) A3: (scf r) . 1 > 0 by A1; A4: for n being Nat st n >= 1 & S2[n] holds S2[n + 1] proof let n be Nat; ::_thesis: ( n >= 1 & S2[n] implies S2[n + 1] ) assume that n >= 1 and ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1)) ; ::_thesis: S2[n + 1] (((c_n r) . (2 * (n + 1))) * ((c_d r) . ((2 * (n + 1)) - 1))) - (((c_n r) . ((2 * (n + 1)) - 1)) * ((c_d r) . (2 * (n + 1)))) = (((c_n r) . (((2 * n) + 1) + 1)) * ((c_d r) . ((2 * n) + 1))) - (((c_n r) . ((2 * n) + 1)) * ((c_d r) . (((2 * n) + 1) + 1))) .= (- 1) |^ ((2 * n) + 1) by Th64 .= - (1 |^ ((2 * n) + 1)) by WSIERP_1:2 .= - 1 by NEWTON:10 ; then A5: ((c_n r) . (2 * (n + 1))) * ((c_d r) . ((2 * (n + 1)) - 1)) < ((c_n r) . ((2 * (n + 1)) - 1)) * ((c_d r) . (2 * (n + 1))) by XREAL_1:48; ( (c_d r) . ((2 * n) + 1) > 0 & (c_d r) . ((2 * n) + 2) > 0 ) by A3, Th52; hence S2[n + 1] by A5, XREAL_1:106; ::_thesis: verum end; (cocf r) . 1 = ((c_n r) . 1) * (((c_d r) ") . 1) by SEQ_1:8 .= ((c_n r) . 1) * (((c_d r) . 1) ") by VALUED_1:10 .= ((c_n r) . 1) * (1 / ((c_d r) . 1)) .= ((c_n r) . ((2 * 1) - 1)) / ((c_d r) . ((2 * 1) - 1)) ; then A6: ((c_n r) . ((2 * 1) - 1)) / ((c_d r) . ((2 * 1) - 1)) = ((scf r) . 0) + (1 / ((scf r) . 1)) by A3, Th72; (cocf r) . 2 = ((c_n r) . 2) * (((c_d r) ") . 2) by SEQ_1:8 .= ((c_n r) . 2) * (((c_d r) . 2) ") by VALUED_1:10 .= ((c_n r) . 2) * (1 / ((c_d r) . 2)) .= ((c_n r) . (2 * 1)) / ((c_d r) . (2 * 1)) ; then ((c_n r) . (2 * 1)) / ((c_d r) . (2 * 1)) = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / ((scf r) . 2)))) by A1, Th73; then A7: S2[1] by A6, A2, XREAL_1:8; for n being Nat st n >= 1 holds S2[n] from NAT_1:sch_8(A7, A4); hence ( n >= 1 implies ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1)) ) ; ::_thesis: verum end; definition let r be real number ; set s = scf r; func backContinued_fraction r -> Real_Sequence means :Def8: :: REAL_3:def 8 ( it . 0 = (scf r) . 0 & ( for n being Nat holds it . (n + 1) = (1 / (it . n)) + ((scf r) . (n + 1)) ) ); existence ex b1 being Real_Sequence st ( b1 . 0 = (scf r) . 0 & ( for n being Nat holds b1 . (n + 1) = (1 / (b1 . n)) + ((scf r) . (n + 1)) ) ) proof deffunc H1( Nat, Real) -> Element of REAL = (1 / $2) + ((scf r) . ($1 + 1)); consider f being Real_Sequence such that A1: f . 0 = (scf r) . 0 and A2: for n being Nat holds f . (n + 1) = H1(n,f . n) from NAT_1:sch_12(); take f ; ::_thesis: ( f . 0 = (scf r) . 0 & ( for n being Nat holds f . (n + 1) = (1 / (f . n)) + ((scf r) . (n + 1)) ) ) thus f . 0 = (scf r) . 0 by A1; ::_thesis: for n being Nat holds f . (n + 1) = (1 / (f . n)) + ((scf r) . (n + 1)) let n be Nat; ::_thesis: f . (n + 1) = (1 / (f . n)) + ((scf r) . (n + 1)) thus f . (n + 1) = (1 / (f . n)) + ((scf r) . (n + 1)) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Real_Sequence st b1 . 0 = (scf r) . 0 & ( for n being Nat holds b1 . (n + 1) = (1 / (b1 . n)) + ((scf r) . (n + 1)) ) & b2 . 0 = (scf r) . 0 & ( for n being Nat holds b2 . (n + 1) = (1 / (b2 . n)) + ((scf r) . (n + 1)) ) holds b1 = b2 proof let s1, s2 be Real_Sequence; ::_thesis: ( s1 . 0 = (scf r) . 0 & ( for n being Nat holds s1 . (n + 1) = (1 / (s1 . n)) + ((scf r) . (n + 1)) ) & s2 . 0 = (scf r) . 0 & ( for n being Nat holds s2 . (n + 1) = (1 / (s2 . n)) + ((scf r) . (n + 1)) ) implies s1 = s2 ) assume that A3: s1 . 0 = (scf r) . 0 and A4: for n being Nat holds s1 . (n + 1) = (1 / (s1 . n)) + ((scf r) . (n + 1)) and A5: s2 . 0 = (scf r) . 0 and A6: for n being Nat holds s2 . (n + 1) = (1 / (s2 . n)) + ((scf r) . (n + 1)) ; ::_thesis: s1 = s2 defpred S2[ Nat] means s1 . $1 = s2 . $1; A7: for k being Nat st S2[k] holds S2[k + 1] proof let k be Nat; ::_thesis: ( S2[k] implies S2[k + 1] ) assume s1 . k = s2 . k ; ::_thesis: S2[k + 1] hence s1 . (k + 1) = (1 / (s2 . k)) + ((scf r) . (k + 1)) by A4 .= s2 . (k + 1) by A6 ; ::_thesis: verum end; let x be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: s1 . x = s2 . x A8: S2[ 0 ] by A3, A5; for n being Nat holds S2[n] from NAT_1:sch_2(A8, A7); hence s1 . x = s2 . x ; ::_thesis: verum end; end; :: deftheorem Def8 defines backContinued_fraction REAL_3:def_8_:_ for r being real number for b2 being Real_Sequence holds ( b2 = backContinued_fraction r iff ( b2 . 0 = (scf r) . 0 & ( for n being Nat holds b2 . (n + 1) = (1 / (b2 . n)) + ((scf r) . (n + 1)) ) ) ); notation let r be real number ; synonym bcf r for backContinued_fraction r; end; theorem :: REAL_3:78 for r being real number st (scf r) . 0 > 0 holds for n being Nat holds (bcf r) . (n + 1) = ((c_n r) . (n + 1)) / ((c_n r) . n) proof let r be real number ; ::_thesis: ( (scf r) . 0 > 0 implies for n being Nat holds (bcf r) . (n + 1) = ((c_n r) . (n + 1)) / ((c_n r) . n) ) set s1 = c_n r; set s = scf r; defpred S2[ Nat] means (bcf r) . ($1 + 1) = ((c_n r) . ($1 + 1)) / ((c_n r) . $1); set s3 = bcf r; assume A1: (scf r) . 0 > 0 ; ::_thesis: for n being Nat holds (bcf r) . (n + 1) = ((c_n r) . (n + 1)) / ((c_n r) . n) A2: for n being Nat st S2[n] holds S2[n + 1] proof let n be Nat; ::_thesis: ( S2[n] implies S2[n + 1] ) assume A3: (bcf r) . (n + 1) = ((c_n r) . (n + 1)) / ((c_n r) . n) ; ::_thesis: S2[n + 1] A4: (c_n r) . (n + 1) > 0 by A1, Th45; (bcf r) . ((n + 1) + 1) = (1 / ((bcf r) . (n + 1))) + ((scf r) . ((n + 1) + 1)) by Def8 .= (((c_n r) . n) / ((c_n r) . (n + 1))) + ((scf r) . ((n + 1) + 1)) by A3, XCMPLX_1:57 .= (((c_n r) . n) + (((scf r) . (n + 2)) * ((c_n r) . (n + 1)))) / ((c_n r) . (n + 1)) by A4, XCMPLX_1:113 .= ((c_n r) . (n + 2)) / ((c_n r) . (n + 1)) by Def5 ; hence S2[n + 1] ; ::_thesis: verum end; (bcf r) . (0 + 1) = (1 / ((bcf r) . 0)) + ((scf r) . (0 + 1)) by Def8 .= (1 / ((scf r) . 0)) + ((scf r) . 1) by Def8 .= (1 + (((scf r) . 0) * ((scf r) . 1))) / ((scf r) . 0) by A1, XCMPLX_1:113 .= ((c_n r) . 1) / ((scf r) . 0) by Def5 .= ((c_n r) . (0 + 1)) / ((c_n r) . 0) by Def5 ; then A5: S2[ 0 ] ; for n being Nat holds S2[n] from NAT_1:sch_2(A5, A2); hence for n being Nat holds (bcf r) . (n + 1) = ((c_n r) . (n + 1)) / ((c_n r) . n) ; ::_thesis: verum end;