:: FIB_NUM semantic presentation begin theorem Th1: :: FIB_NUM:1 for m, n being Element of NAT holds m gcd n = m gcd (n + m) proof let m, n be Element of NAT ; ::_thesis: m gcd n = m gcd (n + m) set a = m gcd n; set b = m gcd (n + m); A1: m gcd n divides m by NAT_D:def_5; A2: m gcd (n + m) divides m by NAT_D:def_5; m gcd (n + m) divides n + m by NAT_D:def_5; then m gcd (n + m) divides n by A2, NAT_D:10; then A3: m gcd (n + m) divides m gcd n by A2, NAT_D:def_5; m gcd n divides n by NAT_D:def_5; then m gcd n divides n + m by A1, NAT_D:8; then m gcd n divides m gcd (n + m) by A1, NAT_D:def_5; hence m gcd n = m gcd (n + m) by A3, NAT_D:5; ::_thesis: verum end; theorem Th2: :: FIB_NUM:2 for k, m, n being Element of NAT st k gcd m = 1 holds k gcd (m * n) = k gcd n proof defpred S1[ Nat] means for m, n being Element of NAT st \$1 gcd m = 1 holds \$1 gcd (m * n) = \$1 gcd n; A1: for k being Nat st ( for a being Nat st a < k holds S1[a] ) holds S1[k] proof let k be Nat; ::_thesis: ( ( for a being Nat st a < k holds S1[a] ) implies S1[k] ) assume A2: for a being Nat st a < k holds S1[a] ; ::_thesis: S1[k] percases ( k = 0 or k = 1 or k > 1 ) by NAT_1:25; supposeA3: k = 0 ; ::_thesis: S1[k] let m, n be Element of NAT ; ::_thesis: ( k gcd m = 1 implies k gcd (m * n) = k gcd n ) assume k gcd m = 1 ; ::_thesis: k gcd (m * n) = k gcd n then 1 = m by A3, NEWTON:52; hence k gcd (m * n) = k gcd n ; ::_thesis: verum end; supposeA4: k = 1 ; ::_thesis: S1[k] let m, n be Element of NAT ; ::_thesis: ( k gcd m = 1 implies k gcd (m * n) = k gcd n ) assume k gcd m = 1 ; ::_thesis: k gcd (m * n) = k gcd n k gcd (m * n) = 1 by A4, NEWTON:51; hence k gcd (m * n) = k gcd n by A4, NEWTON:51; ::_thesis: verum end; supposeA5: k > 1 ; ::_thesis: S1[k] let m, n be Element of NAT ; ::_thesis: ( k gcd m = 1 implies k gcd (m * n) = k gcd n ) set b = k gcd (m * n); assume A6: k gcd m = 1 ; ::_thesis: k gcd (m * n) = k gcd n thus k gcd (m * n) = k gcd n ::_thesis: verum proof percases ( k gcd (m * n) = 0 or k gcd (m * n) = 1 or k gcd (m * n) > 1 ) by NAT_1:25; suppose k gcd (m * n) = 0 ; ::_thesis: k gcd (m * n) = k gcd n then 0 divides k by NAT_D:def_5; then k = 0 by INT_2:3; hence k gcd (m * n) = k gcd n by A5; ::_thesis: verum end; supposeA7: k gcd (m * n) = 1 ; ::_thesis: k gcd (m * n) = k gcd n set c = k gcd n; A8: k gcd n divides k by NAT_D:def_5; A9: n divides m * n by NAT_D:def_3; k gcd n divides n by NAT_D:def_5; then k gcd n divides m * n by A9, NAT_D:4; then k gcd n divides 1 by A7, A8, NAT_D:def_5; hence k gcd (m * n) = k gcd n by A7, WSIERP_1:15; ::_thesis: verum end; suppose k gcd (m * n) > 1 ; ::_thesis: k gcd (m * n) = k gcd n then k gcd (m * n) >= 1 + 1 by NAT_1:13; then consider p being Element of NAT such that A10: p is prime and A11: p divides k gcd (m * n) by INT_2:31; k gcd (m * n) divides k by NAT_D:def_5; then A12: p divides k by A11, NAT_D:4; then consider s being Nat such that A13: k = p * s by NAT_D:def_3; A14: not p divides m proof assume p divides m ; ::_thesis: contradiction then p divides 1 by A6, A12, NAT_D:def_5; then p = 1 by WSIERP_1:15; hence contradiction by A10, INT_2:def_4; ::_thesis: verum end; k gcd (m * n) divides m * n by NAT_D:def_5; then p divides m * n by A11, NAT_D:4; then p divides n by A10, A14, NEWTON:80; then consider r being Nat such that A15: n = p * r by NAT_D:def_3; reconsider s = s as Element of NAT by ORDINAL1:def_12; A16: s + 1 > s by XREAL_1:29; p > 1 by A10, INT_2:def_4; then p >= 1 + 1 by NAT_1:13; then A17: s * p >= s * (1 + 1) by NAT_1:4; s <> 0 by A5, A13; then s + s > s by NAT_1:3, XREAL_1:29; then s + s >= s + 1 by NAT_1:13; then k >= s + 1 by A13, A17, XXREAL_0:2; then A18: s < k by A16, XXREAL_0:2; A19: s gcd m = 1 proof set c = s gcd m; A20: s gcd m divides s by NAT_D:def_5; A21: s gcd m divides m by NAT_D:def_5; s divides k by A13, NAT_D:def_3; then s gcd m divides k by A20, NAT_D:4; then s gcd m divides 1 by A6, A21, NAT_D:def_5; hence s gcd m = 1 by WSIERP_1:15; ::_thesis: verum end; reconsider r = r as Element of NAT by ORDINAL1:def_12; A22: k gcd n = p * (s gcd r) by A13, A15, PYTHTRIP:8; k gcd (m * n) = (p * s) gcd (p * (m * r)) by A13, A15 .= p * (s gcd (m * r)) by PYTHTRIP:8 ; hence k gcd (m * n) = k gcd n by A2, A18, A19, A22; ::_thesis: verum end; end; end; end; end; end; for k being Nat holds S1[k] from NAT_1:sch_4(A1); hence for k, m, n being Element of NAT st k gcd m = 1 holds k gcd (m * n) = k gcd n ; ::_thesis: verum end; theorem Th3: :: FIB_NUM:3 for s being real number st s > 0 holds ex n being Element of NAT st ( n > 0 & 0 < 1 / n & 1 / n <= s ) proof let s be real number ; ::_thesis: ( s > 0 implies ex n being Element of NAT st ( n > 0 & 0 < 1 / n & 1 / n <= s ) ) consider n being Element of NAT such that A1: n > 1 / s by SEQ_4:3; A2: 1 / (1 / s) = 1 / (s ") .= s ; assume s > 0 ; ::_thesis: ex n being Element of NAT st ( n > 0 & 0 < 1 / n & 1 / n <= s ) then A3: 1 / s > 0 by XREAL_1:139; take n ; ::_thesis: ( n > 0 & 0 < 1 / n & 1 / n <= s ) n > 0 by A3, A1, XXREAL_0:2; hence ( n > 0 & 0 < 1 / n & 1 / n <= s ) by A3, A1, A2, XREAL_1:85, XREAL_1:139; ::_thesis: verum end; scheme :: FIB_NUM:sch 1 FibInd{ P1[ set ] } : for k being Nat holds P1[k] provided A1: P1[ 0 ] and A2: P1[1] and A3: for k being Nat st P1[k] & P1[k + 1] holds P1[k + 2] proof let k be Nat; ::_thesis: P1[k] defpred S1[ Nat] means ( P1[\$1] & P1[\$1 + 1] ); A4: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) A5: k + 2 = (k + 1) + 1 ; assume S1[k] ; ::_thesis: S1[k + 1] hence S1[k + 1] by A3, A5; ::_thesis: verum end; A6: S1[ 0 ] by A1, A2; for k being Nat holds S1[k] from NAT_1:sch_2(A6, A4); hence P1[k] ; ::_thesis: verum end; scheme :: FIB_NUM:sch 2 BinInd{ P1[ Nat, Nat] } : for m, n being Element of NAT holds P1[m,n] provided A1: for m, n being Element of NAT st P1[m,n] holds P1[n,m] and A2: for k being Element of NAT st ( for m, n being Element of NAT st m < k & n < k holds P1[m,n] ) holds for m being Element of NAT st m <= k holds P1[k,m] proof defpred S1[ Nat] means for m, n being Element of NAT st m <= \$1 & n <= \$1 holds P1[m,n]; A3: for k being Nat st ( for r being Nat st r < k holds S1[r] ) holds S1[k] proof let k be Nat; ::_thesis: ( ( for r being Nat st r < k holds S1[r] ) implies S1[k] ) assume A4: for r being Nat st r < k holds S1[r] ; ::_thesis: S1[k] let m, n be Element of NAT ; ::_thesis: ( m <= k & n <= k implies P1[m,n] ) assume that A5: m <= k and A6: n <= k ; ::_thesis: P1[m,n] set s = max (m,n); A7: max (m,n) <= k by A5, A6, XXREAL_0:28; percases ( max (m,n) < k or max (m,n) = k ) by A7, XXREAL_0:1; suppose max (m,n) < k ; ::_thesis: P1[m,n] then ( m <= max (m,n) & n <= max (m,n) implies P1[m,n] ) by A4; hence P1[m,n] by XXREAL_0:25; ::_thesis: verum end; supposeA8: max (m,n) = k ; ::_thesis: P1[m,n] A9: for m, n being Element of NAT st m < k & n < k holds P1[m,n] proof let m, n be Element of NAT ; ::_thesis: ( m < k & n < k implies P1[m,n] ) assume that A10: m < k and A11: n < k ; ::_thesis: P1[m,n] set s = max (m,n); A12: m <= max (m,n) by XXREAL_0:25; A13: n <= max (m,n) by XXREAL_0:25; max (m,n) < k by A10, A11, XXREAL_0:16; hence P1[m,n] by A4, A12, A13; ::_thesis: verum end; thus P1[m,n] ::_thesis: verum proof percases ( k = m or k = n ) by A8, XXREAL_0:16; suppose k = m ; ::_thesis: P1[m,n] hence P1[m,n] by A2, A6, A9; ::_thesis: verum end; suppose k = n ; ::_thesis: P1[m,n] then P1[n,m] by A2, A5, A9; hence P1[m,n] by A1; ::_thesis: verum end; end; end; end; end; end; A14: for k being Nat holds S1[k] from NAT_1:sch_4(A3); let m, n be Element of NAT ; ::_thesis: P1[m,n] set k = max (m,n); ( m <= max (m,n) & n <= max (m,n) implies P1[m,n] ) by A14; hence P1[m,n] by XXREAL_0:30; ::_thesis: verum end; (0 + 1) + 1 = 2 ; then Lm1: Fib 2 = 1 by PRE_FF:1; Lm2: (1 + 1) + 1 = 3 ; Lm3: for k being Nat holds Fib (k + 1) >= k proof defpred S1[ Nat] means Fib (\$1 + 1) >= \$1; (0 + 1) + 1 = 2 ; then A1: S1[1] by PRE_FF:1; A2: for k being Nat st S1[k] & S1[k + 1] holds S1[k + 2] proof let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] ) assume that A3: S1[k] and A4: S1[k + 1] ; ::_thesis: S1[k + 2] percases ( k = 0 or k <> 0 ) ; suppose k = 0 ; ::_thesis: S1[k + 2] hence S1[k + 2] by Lm1, Lm2, PRE_FF:1; ::_thesis: verum end; suppose k <> 0 ; ::_thesis: S1[k + 2] then 1 <= k by NAT_1:14; then A5: 1 + (k + 1) <= k + (k + 1) by XREAL_1:6; A6: Fib ((k + 2) + 1) = (Fib ((k + 1) + 1)) + (Fib (k + 1)) by PRE_FF:1; A7: k + (k + 1) <= (Fib (k + 1)) + (k + 1) by A3, XREAL_1:6; (Fib (k + 1)) + (k + 1) <= (Fib ((k + 1) + 1)) + (Fib (k + 1)) by A4, XREAL_1:6; then k + (k + 1) <= Fib ((k + 2) + 1) by A6, A7, XXREAL_0:2; hence S1[k + 2] by A5, XXREAL_0:2; ::_thesis: verum end; end; end; A8: S1[ 0 ] by PRE_FF:1; thus for k being Nat holds S1[k] from FIB_NUM:sch_1(A8, A1, A2); ::_thesis: verum end; Lm4: for m being Element of NAT holds Fib (m + 1) >= Fib m proof defpred S1[ Element of NAT ] means Fib (\$1 + 1) >= Fib \$1; A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) A2: Fib k >= 0 by NAT_1:2; Fib ((k + 1) + 1) = (Fib (k + 1)) + (Fib k) by PRE_FF:1; then Fib ((k + 1) + 1) >= (Fib (k + 1)) + 0 by A2, XREAL_1:6; hence ( S1[k] implies S1[k + 1] ) ; ::_thesis: verum end; A3: S1[ 0 ] by PRE_FF:1; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A1); ::_thesis: verum end; Lm5: for m, n being Element of NAT st m >= n holds Fib m >= Fib n proof A1: for k, n being Element of NAT holds Fib (n + k) >= Fib n proof defpred S1[ Element of NAT ] means for n being Element of NAT holds Fib (n + \$1) >= Fib n; A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] let n be Element of NAT ; ::_thesis: Fib (n + (k + 1)) >= Fib n n + (k + 1) = (n + k) + 1 ; then A4: Fib (n + (k + 1)) >= Fib (n + k) by Lm4; Fib (n + k) >= Fib n by A3; hence Fib (n + (k + 1)) >= Fib n by A4, XXREAL_0:2; ::_thesis: verum end; let k, n be Element of NAT ; ::_thesis: Fib (n + k) >= Fib n A5: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A5, A2); hence Fib (n + k) >= Fib n ; ::_thesis: verum end; let m, n be Element of NAT ; ::_thesis: ( m >= n implies Fib m >= Fib n ) assume m >= n ; ::_thesis: Fib m >= Fib n then consider k being Nat such that A6: m = n + k by NAT_1:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; m = n + k by A6; hence Fib m >= Fib n by A1; ::_thesis: verum end; Lm6: for m being Element of NAT holds Fib (m + 1) <> 0 proof let m be Element of NAT ; ::_thesis: Fib (m + 1) <> 0 percases ( m = 0 or m <> 0 ) ; suppose m = 0 ; ::_thesis: Fib (m + 1) <> 0 hence Fib (m + 1) <> 0 by PRE_FF:1; ::_thesis: verum end; suppose m <> 0 ; ::_thesis: Fib (m + 1) <> 0 hence Fib (m + 1) <> 0 by Lm3, NAT_1:3; ::_thesis: verum end; end; end; theorem Th4: :: FIB_NUM:4 for m, n being Nat holds Fib (m + (n + 1)) = ((Fib n) * (Fib m)) + ((Fib (n + 1)) * (Fib (m + 1))) proof defpred S1[ Nat] means for n being Nat holds Fib (\$1 + (n + 1)) = ((Fib n) * (Fib \$1)) + ((Fib (n + 1)) * (Fib (\$1 + 1))); A1: S1[ 0 ] by PRE_FF:1; A2: now__::_thesis:_for_k_being_Nat_st_S1[k]_&_S1[k_+_1]_holds_ S1[k_+_2] let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] ) assume that A3: S1[k] and A4: S1[k + 1] ; ::_thesis: S1[k + 2] thus S1[k + 2] ::_thesis: verum proof let n be Nat; ::_thesis: Fib ((k + 2) + (n + 1)) = ((Fib n) * (Fib (k + 2))) + ((Fib (n + 1)) * (Fib ((k + 2) + 1))) A5: Fib (((k + 1) + 1) + (n + 1)) = Fib (((k + (n + 1)) + 1) + 1) .= (Fib (k + (n + 1))) + (Fib ((k + 1) + (n + 1))) by PRE_FF:1 ; set a = (Fib n) * (Fib k); set b = (Fib (n + 1)) * (Fib (k + 1)); set c = (Fib n) * (Fib (k + 1)); set d = (Fib (n + 1)) * (Fib ((k + 1) + 1)); A6: (((Fib n) * (Fib k)) + ((Fib (n + 1)) * (Fib (k + 1)))) + (((Fib n) * (Fib (k + 1))) + ((Fib (n + 1)) * (Fib ((k + 1) + 1)))) = (((Fib n) * (Fib k)) + ((Fib n) * (Fib (k + 1)))) + (((Fib (n + 1)) * (Fib (k + 1))) + ((Fib (n + 1)) * (Fib ((k + 1) + 1)))) ; A7: ((Fib (n + 1)) * (Fib (k + 1))) + ((Fib (n + 1)) * (Fib ((k + 1) + 1))) = (Fib (n + 1)) * ((Fib (k + 1)) + (Fib ((k + 1) + 1))) .= (Fib (n + 1)) * (Fib (((k + 1) + 1) + 1)) by PRE_FF:1 ; A8: ((Fib n) * (Fib k)) + ((Fib n) * (Fib (k + 1))) = (Fib n) * ((Fib k) + (Fib (k + 1))) .= (Fib n) * (Fib ((k + 1) + 1)) by PRE_FF:1 ; Fib (k + (n + 1)) = ((Fib n) * (Fib k)) + ((Fib (n + 1)) * (Fib (k + 1))) by A3; hence Fib ((k + 2) + (n + 1)) = ((Fib n) * (Fib (k + 2))) + ((Fib (n + 1)) * (Fib ((k + 2) + 1))) by A4, A5, A6, A8, A7; ::_thesis: verum end; end; A9: S1[1] by Lm1, PRE_FF:1; thus for k being Nat holds S1[k] from FIB_NUM:sch_1(A1, A9, A2); ::_thesis: verum end; Lm7: for n being Element of NAT holds (Fib n) gcd (Fib (n + 1)) = 1 proof defpred S1[ Element of NAT ] means (Fib \$1) gcd (Fib (\$1 + 1)) = 1; A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] (Fib (k + 1)) gcd (Fib ((k + 1) + 1)) = (Fib (k + 1)) gcd ((Fib (k + 1)) + (Fib k)) by PRE_FF:1 .= 1 by A2, Th1 ; hence S1[k + 1] ; ::_thesis: verum end; A3: S1[ 0 ] by NEWTON:52, PRE_FF:1; thus for m being Element of NAT holds S1[m] from NAT_1:sch_1(A3, A1); ::_thesis: verum end; theorem :: FIB_NUM:5 for m, n being Element of NAT holds (Fib m) gcd (Fib n) = Fib (m gcd n) proof defpred S1[ Element of NAT , Element of NAT ] means (Fib \$1) gcd (Fib \$2) = Fib (\$1 gcd \$2); A1: for k being Element of NAT st ( for m, n being Element of NAT st m < k & n < k holds S1[m,n] ) holds for m being Element of NAT st m <= k holds S1[k,m] proof let k be Element of NAT ; ::_thesis: ( ( for m, n being Element of NAT st m < k & n < k holds S1[m,n] ) implies for m being Element of NAT st m <= k holds S1[k,m] ) assume A2: for m, n being Element of NAT st m < k & n < k holds S1[m,n] ; ::_thesis: for m being Element of NAT st m <= k holds S1[k,m] let m be Element of NAT ; ::_thesis: ( m <= k implies S1[k,m] ) assume A3: m <= k ; ::_thesis: S1[k,m] percases ( m = k or m < k ) by A3, XXREAL_0:1; supposeA4: m = k ; ::_thesis: S1[k,m] hence (Fib k) gcd (Fib m) = Fib k by NAT_D:32 .= Fib (k gcd m) by A4, NAT_D:32 ; ::_thesis: verum end; supposeA5: m < k ; ::_thesis: S1[k,m] A6: not m < 0 by NAT_1:2; thus S1[k,m] ::_thesis: verum proof percases ( m = 0 or m > 0 ) by A6, XXREAL_0:1; supposeA7: m = 0 ; ::_thesis: S1[k,m] then (Fib k) gcd (Fib m) = Fib k by NEWTON:52, PRE_FF:1; hence S1[k,m] by A7, NEWTON:52; ::_thesis: verum end; supposeA8: m > 0 ; ::_thesis: S1[k,m] thus S1[k,m] ::_thesis: verum proof consider r being Nat such that A9: k = m + r by A3, NAT_1:10; reconsider r = r as Element of NAT by ORDINAL1:def_12; A10: r <= k by A9, NAT_1:11; r <> 0 by A5, A9; then consider rr being Nat such that A11: r = rr + 1 by NAT_1:6; reconsider rr = rr as Element of NAT by ORDINAL1:def_12; Fib k = ((Fib (rr + 1)) * (Fib (m + 1))) + ((Fib rr) * (Fib m)) by A9, A11, Th4; then A12: (Fib k) gcd (Fib m) = (Fib m) gcd ((Fib (m + 1)) * (Fib r)) by A11, EULER_1:8; (Fib m) gcd (Fib (m + 1)) = 1 by Lm7; then A13: (Fib k) gcd (Fib m) = (Fib m) gcd (Fib r) by A12, Th2; r <> k by A8, A9; then A14: r < k by A10, XXREAL_0:1; k gcd m = m gcd r by A9, Th1; hence S1[k,m] by A2, A5, A13, A14; ::_thesis: verum end; end; end; end; end; end; end; A15: for m, n being Element of NAT st S1[m,n] holds S1[n,m] ; thus for m, n being Element of NAT holds S1[m,n] from FIB_NUM:sch_2(A15, A1); ::_thesis: verum end; begin theorem Th6: :: FIB_NUM:6 for x, a, b, c being real number st a <> 0 & delta (a,b,c) >= 0 holds ( ((a * (x ^2)) + (b * x)) + c = 0 iff ( x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) ) proof let x, a, b, c be real number ; ::_thesis: ( a <> 0 & delta (a,b,c) >= 0 implies ( ((a * (x ^2)) + (b * x)) + c = 0 iff ( x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) ) ) set lh = ((a * (x ^2)) + (b * x)) + c; set r1 = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a); set r2 = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a); assume that A1: a <> 0 and A2: delta (a,b,c) >= 0 ; ::_thesis: ( ((a * (x ^2)) + (b * x)) + c = 0 iff ( x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) ) ((a * (x ^2)) + (b * x)) + c = (a * (x - (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)))) * (x - (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) by A1, A2, QUIN_1:16; hence ( ((a * (x ^2)) + (b * x)) + c = 0 iff ( x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) ) by A1, A2, QUIN_1:15; ::_thesis: verum end; definition func tau -> real number equals :: FIB_NUM:def 1 (1 + (sqrt 5)) / 2; correctness coherence (1 + (sqrt 5)) / 2 is real number ; ; end; :: deftheorem defines tau FIB_NUM:def_1_:_ tau = (1 + (sqrt 5)) / 2; definition func tau_bar -> real number equals :: FIB_NUM:def 2 (1 - (sqrt 5)) / 2; correctness coherence (1 - (sqrt 5)) / 2 is real number ; ; end; :: deftheorem defines tau_bar FIB_NUM:def_2_:_ tau_bar = (1 - (sqrt 5)) / 2; Lm8: ( tau ^2 = tau + 1 & tau_bar ^2 = tau_bar + 1 ) proof A1: delta (1,(- 1),(- 1)) = ((- 1) ^2) - ((4 * 1) * (- 1)) by QUIN_1:def_1 .= 5 ; then A2: ((- (- 1)) - (sqrt (delta (1,(- 1),(- 1))))) / (2 * 1) = tau_bar ; A3: for x being real number st ( x = tau or x = tau_bar ) holds x ^2 = x + 1 proof let x be real number ; ::_thesis: ( ( x = tau or x = tau_bar ) implies x ^2 = x + 1 ) assume ( x = tau or x = tau_bar ) ; ::_thesis: x ^2 = x + 1 then ((1 * (x ^2)) + ((- 1) * x)) + (- 1) = 0 by A1, A2, Th6; hence x ^2 = x + 1 ; ::_thesis: verum end; hence tau ^2 = tau + 1 ; ::_thesis: tau_bar ^2 = tau_bar + 1 thus tau_bar ^2 = tau_bar + 1 by A3; ::_thesis: verum end; Lm9: 2 < sqrt 5 by SQUARE_1:20, SQUARE_1:27; Lm10: sqrt 5 <> 0 by SQUARE_1:20, SQUARE_1:27; Lm11: sqrt 5 < 3 proof 3 ^2 = 9 ; then sqrt 9 = 3 by SQUARE_1:22; hence sqrt 5 < 3 by SQUARE_1:27; ::_thesis: verum end; 1 < tau proof 2 < sqrt 5 by SQUARE_1:20, SQUARE_1:27; then 1 < sqrt 5 by XXREAL_0:2; then 1 + 1 < 1 + (sqrt 5) by XREAL_1:8; then 2 / 2 < (1 + (sqrt 5)) / 2 by XREAL_1:74; hence 1 < tau ; ::_thesis: verum end; then Lm12: 0 < tau by XXREAL_0:2; Lm13: tau_bar < 0 proof 2 < sqrt 5 by SQUARE_1:20, SQUARE_1:27; then not 0 + (sqrt 5) <= 1 by XXREAL_0:2; then 0 * 2 > (1 - (sqrt 5)) / 1 by XREAL_1:19; then (1 - (sqrt 5)) / 2 < 0 * 1 by XREAL_1:113; hence tau_bar < 0 ; ::_thesis: verum end; Lm14: abs tau_bar < 1 proof (sqrt 5) - 1 < 3 - 1 by Lm11, XREAL_1:9; then A1: ((sqrt 5) - 1) / 2 < 2 / 2 by XREAL_1:74; abs tau_bar = - ((1 - (sqrt 5)) / 2) by Lm13, ABSVALUE:def_1 .= ((sqrt 5) - 1) / 2 ; hence abs tau_bar < 1 by A1; ::_thesis: verum end; theorem Th7: :: FIB_NUM:7 for n being Nat holds Fib n = ((tau to_power n) - (tau_bar to_power n)) / (sqrt 5) proof defpred S1[ Nat] means Fib \$1 = ((tau to_power \$1) - (tau_bar to_power \$1)) / (sqrt 5); A1: tau_bar to_power 1 = tau_bar by POWER:25; tau_bar to_power 0 = 1 by POWER:24; then ((tau to_power 0) - (tau_bar to_power 0)) / (sqrt 5) = (1 - 1) / (sqrt 5) by POWER:24 .= 0 ; then A2: S1[ 0 ] by PRE_FF:1; A3: for k being Nat st S1[k] & S1[k + 1] holds S1[k + 2] proof let k be Nat; ::_thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] ) assume that A4: S1[k] and A5: S1[k + 1] ; ::_thesis: S1[k + 2] set a = tau to_power k; set a1 = tau_bar to_power k; set b = tau to_power (k + 1); set b1 = tau_bar to_power (k + 1); set c = tau to_power (k + 2); set c1 = tau_bar to_power (k + 2); A6: tau_bar to_power (k + 2) = tau_bar |^ (k + 2) by POWER:41 .= (tau_bar |^ k) * (tau_bar |^ (1 + 1)) by NEWTON:8 .= (tau_bar |^ k) * (tau_bar * (tau_bar |^ 1)) by NEWTON:6 .= (tau_bar |^ k) * (tau_bar + 1) by Lm8, NEWTON:5 .= ((tau_bar |^ k) * tau_bar) + ((tau_bar |^ k) * 1) .= (tau_bar |^ (k + 1)) + ((tau_bar |^ k) * 1) by NEWTON:6 .= (tau_bar to_power (k + 1)) + (tau_bar |^ k) by POWER:41 .= (tau_bar to_power k) + (tau_bar to_power (k + 1)) by POWER:41 ; A7: tau to_power (k + 2) = (tau to_power 2) * (tau to_power k) by Lm12, POWER:27 .= (tau to_power k) * (tau + 1) by Lm8, POWER:46 .= ((tau to_power k) * tau) + ((tau to_power k) * 1) .= ((tau to_power k) * (tau to_power 1)) + (tau to_power k) by POWER:25 .= (tau to_power k) + (tau to_power (k + 1)) by Lm12, POWER:27 ; Fib (k + 2) = Fib ((k + 1) + 1) .= (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5)) + (((tau to_power (k + 1)) - (tau_bar to_power (k + 1))) / (sqrt 5)) by A4, A5, PRE_FF:1 .= ((tau to_power (k + 2)) - (tau_bar to_power (k + 2))) / (sqrt 5) by A7, A6 ; hence S1[k + 2] ; ::_thesis: verum end; tau - tau_bar = sqrt 5 ; then ((tau to_power 1) - (tau_bar to_power 1)) / (sqrt 5) = (sqrt 5) / (sqrt 5) by A1, POWER:25 .= Fib 1 by Lm10, PRE_FF:1, XCMPLX_1:60 ; then A8: S1[1] ; thus for n being Nat holds S1[n] from FIB_NUM:sch_1(A2, A8, A3); ::_thesis: verum end; Lm15: for n being Element of NAT for x being real number st abs x <= 1 holds abs (x |^ n) <= 1 proof let n be Element of NAT ; ::_thesis: for x being real number st abs x <= 1 holds abs (x |^ n) <= 1 let x be real number ; ::_thesis: ( abs x <= 1 implies abs (x |^ n) <= 1 ) defpred S1[ Element of NAT ] means abs (x |^ \$1) <= 1; assume A1: abs x <= 1 ; ::_thesis: abs (x |^ n) <= 1 A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) A3: abs (x |^ (k + 1)) = abs ((x |^ k) * x) by NEWTON:6 .= (abs (x |^ k)) * (abs x) by COMPLEX1:65 ; assume S1[k] ; ::_thesis: S1[k + 1] hence S1[k + 1] by A1, A3, COMPLEX1:46, XREAL_1:160; ::_thesis: verum end; abs (x |^ 0) = abs 1 by NEWTON:4 .= 1 by ABSVALUE:def_1 ; then A4: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A2); hence abs (x |^ n) <= 1 ; ::_thesis: verum end; Lm16: for n being Element of NAT holds abs ((tau_bar to_power n) / (sqrt 5)) < 1 proof let n be Element of NAT ; ::_thesis: abs ((tau_bar to_power n) / (sqrt 5)) < 1 set y = tau_bar to_power n; set z = sqrt 5; A1: abs (tau_bar to_power n) = abs (tau_bar |^ n) by POWER:41; A2: abs ((tau_bar to_power n) / (sqrt 5)) = abs ((tau_bar to_power n) * ((sqrt 5) ")) .= (abs (tau_bar to_power n)) * (abs ((sqrt 5) ")) by COMPLEX1:65 ; A3: 1 / (sqrt 5) < 1 / 2 by Lm9, XREAL_1:88; sqrt 5 > 0 by Lm9, XXREAL_0:2; then A4: (sqrt 5) " > 0 by XREAL_1:122; then abs ((sqrt 5) ") = (sqrt 5) " by ABSVALUE:def_1; then A5: abs ((sqrt 5) ") < 1 by A3, XXREAL_0:2; abs ((sqrt 5) ") >= 0 by A4, ABSVALUE:def_1; hence abs ((tau_bar to_power n) / (sqrt 5)) < 1 by A1, A2, A5, Lm14, Lm15, XREAL_1:162; ::_thesis: verum end; theorem :: FIB_NUM:8 for n being Element of NAT holds abs ((Fib n) - ((tau to_power n) / (sqrt 5))) < 1 proof let n be Element of NAT ; ::_thesis: abs ((Fib n) - ((tau to_power n) / (sqrt 5))) < 1 set k = Fib n; set x = tau to_power n; set y = tau_bar to_power n; set z = sqrt 5; Fib n = ((tau to_power n) - (tau_bar to_power n)) / (sqrt 5) by Th7 .= ((tau to_power n) / (sqrt 5)) - ((tau_bar to_power n) / (sqrt 5)) ; then abs (- ((Fib n) - ((tau to_power n) / (sqrt 5)))) < 1 by Lm16; hence abs ((Fib n) - ((tau to_power n) / (sqrt 5))) < 1 by COMPLEX1:52; ::_thesis: verum end; theorem Th9: :: FIB_NUM:9 for f, g, h being Real_Sequence st g is non-zero holds (f /" g) (#) (g /" h) = f /" h proof let f, g, h be Real_Sequence; ::_thesis: ( g is non-zero implies (f /" g) (#) (g /" h) = f /" h ) set f3 = f /" g; set g3 = g /" h; set h3 = f /" h; assume A1: g is non-zero ; ::_thesis: (f /" g) (#) (g /" h) = f /" h for n being Element of NAT holds ((f /" g) (#) (g /" h)) . n = (f /" h) . n proof let n be Element of NAT ; ::_thesis: ((f /" g) (#) (g /" h)) . n = (f /" h) . n set a = f . n; set b = (g . n) " ; set c = g . n; set d = (h . n) " ; A2: (g /" h) . n = (g . n) * ((h ") . n) by SEQ_1:8 .= (g . n) * ((h . n) ") by VALUED_1:10 ; A3: (f /" h) . n = (f . n) * ((h ") . n) by SEQ_1:8 .= (f . n) * ((h . n) ") by VALUED_1:10 ; A4: g . n <> 0 by A1, SEQ_1:5; A5: ((g . n) ") * (g . n) = (1 / (g . n)) * (g . n) .= 1 by A4, XCMPLX_1:106 ; (f /" g) . n = (f . n) * ((g ") . n) by SEQ_1:8 .= (f . n) * ((g . n) ") by VALUED_1:10 ; then ((f /" g) (#) (g /" h)) . n = ((f . n) * ((g . n) ")) * ((g . n) * ((h . n) ")) by A2, SEQ_1:8 .= ((((g . n) ") * (g . n)) * (f . n)) * ((h . n) ") .= (f /" h) . n by A3, A5 ; hence ((f /" g) (#) (g /" h)) . n = (f /" h) . n ; ::_thesis: verum end; hence (f /" g) (#) (g /" h) = f /" h by FUNCT_2:63; ::_thesis: verum end; theorem Th10: :: FIB_NUM:10 for f, g being Real_Sequence for n being Element of NAT holds ( (f /" g) . n = (f . n) / (g . n) & (f /" g) . n = (f . n) * ((g . n) ") ) proof let f, g be Real_Sequence; ::_thesis: for n being Element of NAT holds ( (f /" g) . n = (f . n) / (g . n) & (f /" g) . n = (f . n) * ((g . n) ") ) let n be Element of NAT ; ::_thesis: ( (f /" g) . n = (f . n) / (g . n) & (f /" g) . n = (f . n) * ((g . n) ") ) A1: (f /" g) . n = (f . n) * ((g ") . n) by SEQ_1:8 .= (f . n) * ((g . n) ") by VALUED_1:10 ; hence (f /" g) . n = (f . n) / (g . n) ; ::_thesis: (f /" g) . n = (f . n) * ((g . n) ") thus (f /" g) . n = (f . n) * ((g . n) ") by A1; ::_thesis: verum end; theorem :: FIB_NUM:11 for F being Real_Sequence st ( for n being Element of NAT holds F . n = (Fib (n + 1)) / (Fib n) ) holds ( F is convergent & lim F = tau ) proof deffunc H1( Element of NAT ) -> Element of COMPLEX = (tau to_power \$1) / (sqrt 5); let F be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds F . n = (Fib (n + 1)) / (Fib n) ) implies ( F is convergent & lim F = tau ) ) consider f being Real_Sequence such that A1: for n being Element of NAT holds f . n = Fib n from SEQ_1:sch_1(); set f2 = f ^\ 2; set f1 = f ^\ 1; A2: (f ^\ 1) ^\ 1 = f ^\ (1 + 1) by NAT_1:48 .= f ^\ 2 ; A3: for n being Element of NAT holds (f ^\ 2) . n <> 0 proof let n be Element of NAT ; ::_thesis: (f ^\ 2) . n <> 0 (f ^\ 2) . n = f . (n + 2) by NAT_1:def_3 .= Fib ((n + 1) + 1) by A1 ; hence (f ^\ 2) . n <> 0 by Lm3, NAT_1:5; ::_thesis: verum end; A4: for n being Nat holds ((f ^\ 2) /" (f ^\ 2)) . n = 1 proof let n be Nat; ::_thesis: ((f ^\ 2) /" (f ^\ 2)) . n = 1 A5: n in NAT by ORDINAL1:def_12; then ((f ^\ 2) /" (f ^\ 2)) . n = ((f ^\ 2) . n) * (((f ^\ 2) . n) ") by Th10 .= ((f ^\ 2) . n) * (1 / ((f ^\ 2) . n)) .= 1 by A3, A5, XCMPLX_1:106 ; hence ((f ^\ 2) /" (f ^\ 2)) . n = 1 ; ::_thesis: verum end; then A6: (f ^\ 2) /" (f ^\ 2) is constant by VALUED_0:def_18; A7: (f /" f) ^\ 2 = (f ^\ 2) /" (f ^\ 2) by SEQM_3:20; then A8: f /" f is convergent by A6, SEQ_4:21; ((f ^\ 2) /" (f ^\ 2)) . 0 = 1 by A4; then lim ((f ^\ 2) /" (f ^\ 2)) = 1 by A6, SEQ_4:25; then A9: lim (f /" f) = 1 by A6, A7, SEQ_4:22; ex g being Real_Sequence st for n being Element of NAT holds g . n = H1(n) from SEQ_1:sch_1(); then consider g being Real_Sequence such that A10: for n being Element of NAT holds g . n = H1(n) ; set g1 = g ^\ 1; A11: for n being Element of NAT holds g . n <> 0 proof let n be Element of NAT ; ::_thesis: g . n <> 0 A12: (sqrt 5) " <> 0 by SQUARE_1:20, SQUARE_1:27, XCMPLX_1:202; A13: tau |^ n <> 0 by Lm12, PREPOWER:5; g . n = (tau to_power n) / (sqrt 5) by A10 .= (tau to_power n) * ((sqrt 5) ") .= (tau |^ n) * ((sqrt 5) ") by POWER:41 ; hence g . n <> 0 by A13, A12, XCMPLX_1:6; ::_thesis: verum end; then A14: g is non-zero by SEQ_1:5; then A15: (f ^\ 2) /" (f ^\ 1) = ((f ^\ 2) /" (g ^\ 1)) (#) ((g ^\ 1) /" (f ^\ 1)) by Th9; set g2 = (g ^\ 1) ^\ 1; for n being Element of NAT holds (f ^\ 1) . n <> 0 proof let n be Element of NAT ; ::_thesis: (f ^\ 1) . n <> 0 (f ^\ 1) . n = f . (n + 1) by NAT_1:def_3 .= Fib (n + 1) by A1 ; hence (f ^\ 1) . n <> 0 by Lm6; ::_thesis: verum end; then A16: f ^\ 1 is non-zero by SEQ_1:5; for n being Element of NAT holds (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n <> 0 proof let n be Element of NAT ; ::_thesis: (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n <> 0 A17: ((g ^\ 1) ^\ 1) . n <> 0 by A14, SEQ_1:5; A18: (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n = (((g ^\ 1) ^\ 1) . n) * (((f ^\ 2) . n) ") by Th10; ((f ^\ 2) . n) " <> 0 by A16, A2, SEQ_1:5, XCMPLX_1:202; hence (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n <> 0 by A17, A18, XCMPLX_1:6; ::_thesis: verum end; then A19: ((g ^\ 1) ^\ 1) /" (f ^\ 2) is non-zero by SEQ_1:5; (g ^\ 1) ^\ 1 = g ^\ (1 + 1) by NAT_1:48; then A20: ((g ^\ 1) ^\ 1) /" (f ^\ 2) = (g /" f) ^\ 2 by SEQM_3:20; A21: for n being Element of NAT holds (f ^\ 1) . n = Fib (n + 1) proof let n be Element of NAT ; ::_thesis: (f ^\ 1) . n = Fib (n + 1) (f ^\ 1) . n = f . (n + 1) by NAT_1:def_3 .= Fib (n + 1) by A1 ; hence (f ^\ 1) . n = Fib (n + 1) ; ::_thesis: verum end; assume A22: for n being Element of NAT holds F . n = (Fib (n + 1)) / (Fib n) ; ::_thesis: ( F is convergent & lim F = tau ) for n being Element of NAT holds F . n = ((f ^\ 1) /" f) . n proof let n be Element of NAT ; ::_thesis: F . n = ((f ^\ 1) /" f) . n ((f ^\ 1) /" f) . n = ((f ^\ 1) . n) / (f . n) by Th10 .= (Fib (n + 1)) / (f . n) by A21 .= (Fib (n + 1)) / (Fib n) by A1 ; hence F . n = ((f ^\ 1) /" f) . n by A22; ::_thesis: verum end; then F = (f ^\ 1) /" f by FUNCT_2:63; then A23: (f ^\ 2) /" (f ^\ 1) = F ^\ 1 by A2, SEQM_3:20; A24: ((g ^\ 1) ^\ 1) /" (g ^\ 1) = ((g ^\ 1) /" g) ^\ 1 by SEQM_3:20; A25: for n being Nat holds ((g ^\ 1) /" g) . n = tau proof let n be Nat; ::_thesis: ((g ^\ 1) /" g) . n = tau A26: n in NAT by ORDINAL1:def_12; then A27: g . n = (tau to_power n) / (sqrt 5) by A10 .= (tau to_power n) * ((sqrt 5) ") .= (tau |^ n) * ((sqrt 5) ") by POWER:41 ; A28: g . n <> 0 by A11, A26; (g ^\ 1) . n = g . (n + 1) by NAT_1:def_3 .= (tau to_power (n + 1)) / (sqrt 5) by A10 .= (tau to_power (n + 1)) * ((sqrt 5) ") .= (tau |^ (n + 1)) * ((sqrt 5) ") by POWER:41 .= (tau * (tau |^ n)) * ((sqrt 5) ") by NEWTON:6 .= tau * (g . n) by A27 ; then ((g ^\ 1) /" g) . n = (tau * (g . n)) * ((g . n) ") by A26, Th10 .= tau * ((g . n) * ((g . n) ")) .= tau * 1 by A28, XCMPLX_0:def_7 .= tau ; hence ((g ^\ 1) /" g) . n = tau ; ::_thesis: verum end; tau in REAL by XREAL_0:def_1; then A29: (g ^\ 1) /" g is constant by A25, VALUED_0:def_18; A30: for x being real number st 0 < x holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((f ") . m) - 0) < x proof let x be real number ; ::_thesis: ( 0 < x implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((f ") . m) - 0) < x ) assume 0 < x ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((f ") . m) - 0) < x then consider k being Element of NAT such that A31: k > 0 and 0 < 1 / k and A32: 1 / k <= x by Th3; for m being Element of NAT st k + 2 <= m holds abs (((f ") . m) - 0) < x proof let m be Element of NAT ; ::_thesis: ( k + 2 <= m implies abs (((f ") . m) - 0) < x ) k + 2 = (k + 1) + 1 ; then A33: Fib (k + 2) >= k + 1 by Lm3; assume k + 2 <= m ; ::_thesis: abs (((f ") . m) - 0) < x then Fib (k + 2) <= Fib m by Lm5; then k + 1 <= Fib m by A33, XXREAL_0:2; then A34: k + 1 <= f . m by A1; then 0 < f . m by NAT_1:5, XXREAL_0:2; then A35: 0 <= (f . m) " by XREAL_1:122; k + 0 < k + 1 by XREAL_1:6; then A36: 1 / (k + 1) < 1 / k by A31, XREAL_1:88; A37: abs (((f ") . m) - 0) = abs ((f . m) ") by VALUED_1:10 .= (f . m) " by A35, ABSVALUE:def_1 .= 1 / (f . m) ; 1 / (f . m) <= 1 / (k + 1) by A34, NAT_1:5, XREAL_1:85; then 1 / (f . m) < 1 / k by A36, XXREAL_0:2; hence abs (((f ") . m) - 0) < x by A32, A37, XXREAL_0:2; ::_thesis: verum end; hence ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((f ") . m) - 0) < x ; ::_thesis: verum end; then A38: f " is convergent by SEQ_2:def_6; then A39: lim (f ") = 0 by A30, SEQ_2:def_7; deffunc H2( Element of NAT ) -> Element of COMPLEX = (tau_bar to_power \$1) / (sqrt 5); ex h being Real_Sequence st for n being Element of NAT holds h . n = H2(n) from SEQ_1:sch_1(); then consider h being Real_Sequence such that A40: for n being Element of NAT holds h . n = H2(n) ; A41: for n being Element of NAT holds f . n = (g . n) - (h . n) proof let n be Element of NAT ; ::_thesis: f . n = (g . n) - (h . n) f . n = Fib n by A1 .= ((tau to_power n) - (tau_bar to_power n)) / (sqrt 5) by Th7 .= ((tau to_power n) / (sqrt 5)) - ((tau_bar to_power n) / (sqrt 5)) .= (g . n) - ((tau_bar to_power n) / (sqrt 5)) by A10 .= (g . n) - (h . n) by A40 ; hence f . n = (g . n) - (h . n) ; ::_thesis: verum end; for n being Element of NAT holds g . n = (f . n) + (h . n) proof let n be Element of NAT ; ::_thesis: g . n = (f . n) + (h . n) f . n = (g . n) - (h . n) by A41; hence g . n = (f . n) + (h . n) ; ::_thesis: verum end; then g = f + h by SEQ_1:7; then A42: g /" f = (f /" f) + (h /" f) by SEQ_1:49; for n being Element of NAT holds abs (h . n) < 1 proof let n be Element of NAT ; ::_thesis: abs (h . n) < 1 h . n = (tau_bar to_power n) / (sqrt 5) by A40; hence abs (h . n) < 1 by Lm16; ::_thesis: verum end; then A43: h is bounded by SEQ_2:3; f " is convergent by A30, SEQ_2:def_6; then A44: h /" f is convergent by A43, A39, SEQ_2:25; then A45: g /" f is convergent by A8, A42, SEQ_2:5; ((g ^\ 1) /" g) . 0 = tau by A25; then lim ((g ^\ 1) /" g) = tau by A29, SEQ_4:25; then A46: lim (((g ^\ 1) ^\ 1) /" (g ^\ 1)) = tau by A29, A24, SEQ_4:20; A47: (g ^\ 1) /" (f ^\ 1) = (g /" f) ^\ 1 by SEQM_3:20; lim (h /" f) = 0 by A43, A38, A39, SEQ_2:26; then A48: lim (g /" f) = 1 + 0 by A44, A8, A9, A42, SEQ_2:6 .= 1 ; then A49: lim (((g ^\ 1) ^\ 1) /" (f ^\ 2)) = 1 by A45, A20, SEQ_4:20; then (((g ^\ 1) ^\ 1) /" (f ^\ 2)) " is convergent by A45, A20, A19, SEQ_2:21; then A50: (f ^\ 2) /" ((g ^\ 1) ^\ 1) is convergent by SEQ_1:40; A51: (f ^\ 2) /" (g ^\ 1) = ((f ^\ 2) /" ((g ^\ 1) ^\ 1)) (#) (((g ^\ 1) ^\ 1) /" (g ^\ 1)) by A14, Th9; then A52: (f ^\ 2) /" (g ^\ 1) is convergent by A29, A50, A24, SEQ_2:14; then A53: (f ^\ 2) /" (f ^\ 1) is convergent by A45, A47, A15, SEQ_2:14; hence F is convergent by A23, SEQ_4:21; ::_thesis: lim F = tau lim ((((g ^\ 1) ^\ 1) /" (f ^\ 2)) ") = 1 " by A45, A20, A49, A19, SEQ_2:22 .= 1 ; then lim ((f ^\ 2) /" ((g ^\ 1) ^\ 1)) = 1 by SEQ_1:40; then A54: lim ((f ^\ 2) /" (g ^\ 1)) = 1 * tau by A29, A51, A50, A24, A46, SEQ_2:15 .= tau ; lim ((g ^\ 1) /" (f ^\ 1)) = 1 by A45, A48, A47, SEQ_4:20; then lim ((f ^\ 2) /" (f ^\ 1)) = tau * 1 by A45, A54, A52, A47, A15, SEQ_2:15; hence lim F = tau by A53, A23, SEQ_4:22; ::_thesis: verum end;