let n be Nat; :: thesis: for r being Real st r is irrational holds
r = ((((c_n r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_n r) . n)) / ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n))
let r be Real; :: thesis: ( r is irrational implies r = ((((c_n r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_n r) . n)) / ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n)) )
assume A1: r is irrational ; :: thesis: r = ((((c_n r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_n r) . n)) / ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n))
defpred S1[ Nat] means r = ((((c_n r) . ($1 + 1)) * ((rfs r) . ($1 + 2))) + ((c_n r) . $1)) / ((((c_d r) . ($1 + 1)) * ((rfs r) . ($1 + 2))) + ((c_d r) . $1));
A2: S1[ 0 ]
proof
A3: (rfs r) . 1 = ((scf r) . 1) + (1 / ((rfs r) . (1 + 1))) by Th1;
A4: (((c_n r) . 1) * ((rfs r) . 2)) + ((c_n r) . 0) = (((((scf r) . 1) * ((scf r) . 0)) + 1) * ((rfs r) . 2)) + ((c_n r) . 0) by REAL_3:def 5
.= (((((scf r) . 1) * ((scf r) . 0)) + 1) * ((rfs r) . 2)) + ((scf r) . 0) by REAL_3:def 5
.= (((scf r) . 0) * ((((scf r) . 1) * ((rfs r) . 2)) + 1)) + ((rfs r) . 2) ;
A5: (((c_d r) . 1) * ((rfs r) . 2)) + ((c_d r) . 0) = (((scf r) . 1) * ((rfs r) . 2)) + ((c_d r) . 0) by REAL_3:def 6
.= (((scf r) . 1) * ((rfs r) . 2)) + 1 by REAL_3:def 6 ;
A6: ( (rfs r) . 2 <> 0 & (((scf r) . 1) * ((rfs r) . 2)) + 1 <> 0 ) by A1, Th3;
((((c_n r) . 1) * ((rfs r) . 2)) + ((c_n r) . 0)) / ((((c_d r) . 1) * ((rfs r) . 2)) + ((c_d r) . 0)) = ((((scf r) . 0) * ((((scf r) . 1) * ((rfs r) . 2)) + 1)) + ((rfs r) . 2)) / ((((c_d r) . 1) * ((rfs r) . 2)) + ((c_d r) . 0)) by A4
.= (((scf r) . 0) * (((((scf r) . 1) * ((rfs r) . 2)) + 1) / ((((scf r) . 1) * ((rfs r) . 2)) + 1))) + (((rfs r) . 2) / ((((scf r) . 1) * ((rfs r) . 2)) + 1)) by A5
.= (((scf r) . 0) * 1) + (((rfs r) . 2) / ((((scf r) . 1) * ((rfs r) . 2)) + 1)) by A6, XCMPLX_1:60
.= ((scf r) . 0) + ((((rfs r) . 2) / ((rfs r) . 2)) / (((((scf r) . 1) * ((rfs r) . 2)) + 1) / ((rfs r) . 2))) by A6, XCMPLX_1:55
.= ((scf r) . 0) + (1 / (((((scf r) . 1) * ((rfs r) . 2)) + 1) / ((rfs r) . 2))) by A6, XCMPLX_1:60
.= ((scf r) . 0) + (1 / ((((scf r) . 1) * (((rfs r) . 2) / ((rfs r) . 2))) + (1 / ((rfs r) . 2))))
.= ((scf r) . 0) + (1 / ((((scf r) . 1) * 1) + (1 / ((rfs r) . 2)))) by A1, Th3, XCMPLX_1:60
.= r by Th1, A3 ;
hence S1[ 0 ] ; :: thesis: verum
end;
A7: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A8: S1[n] ; :: thesis: S1[n + 1]
A9: (rfs r) . (n + 2) = ((scf r) . (n + 2)) + (1 / ((rfs r) . ((n + 2) + 1))) by Th1
.= ((scf r) . (n + 2)) + (1 / ((rfs r) . (n + 3))) ;
A10: 1 = ((rfs r) . (n + 3)) / ((rfs r) . (n + 3)) by A1, Th3, XCMPLX_1:60;
A11: (((c_n r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_n r) . n) = (((c_n r) . (n + 1)) * (((scf r) . (n + 2)) + (1 / ((rfs r) . (n + 3))))) + ((c_n r) . n) by A9
.= ((((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n)) + (((c_n r) . (n + 1)) * (1 / ((rfs r) . (n + 3))))
.= ((c_n r) . (n + 2)) + (((c_n r) . (n + 1)) * (1 / ((rfs r) . (n + 3)))) by REAL_3:def 5 ;
A12: (((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n) = (((c_d r) . (n + 1)) * (((scf r) . (n + 2)) + (1 / ((rfs r) . (n + 3))))) + ((c_d r) . n) by A9
.= ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)) + (((c_d r) . (n + 1)) * (1 / ((rfs r) . (n + 3))))
.= ((c_d r) . (n + 2)) + (((c_d r) . (n + 1)) * (1 / ((rfs r) . (n + 3)))) by REAL_3:def 6 ;
r = ((((c_n r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_n r) . n)) / ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n)) by A8
.= (((c_n r) . (n + 2)) + (((c_n r) . (n + 1)) * (1 / ((rfs r) . (n + 3))))) / (((c_d r) . (n + 2)) + (((c_d r) . (n + 1)) * (1 / ((rfs r) . (n + 3))))) by A11, A12
.= ((((c_n r) . (n + 2)) + (((c_n r) . (n + 1)) * (1 / ((rfs r) . (n + 3))))) / (((c_d r) . (n + 2)) + (((c_d r) . (n + 1)) * (1 / ((rfs r) . (n + 3)))))) * (((rfs r) . (n + 3)) / ((rfs r) . (n + 3))) by A10
.= ((((c_n r) . (n + 2)) + (((c_n r) . (n + 1)) * (1 / ((rfs r) . (n + 3))))) * ((rfs r) . (n + 3))) / ((((c_d r) . (n + 2)) + (((c_d r) . (n + 1)) * (1 / ((rfs r) . (n + 3))))) * ((rfs r) . (n + 3))) by XCMPLX_1:76
.= ((((c_n r) . (n + 2)) * ((rfs r) . (n + 3))) + (((c_n r) . (n + 1)) * ((1 / ((rfs r) . (n + 3))) * ((rfs r) . (n + 3))))) / ((((c_d r) . (n + 2)) * ((rfs r) . (n + 3))) + (((c_d r) . (n + 1)) * ((1 / ((rfs r) . (n + 3))) * ((rfs r) . (n + 3)))))
.= ((((c_n r) . (n + 2)) * ((rfs r) . (n + 3))) + (((c_n r) . (n + 1)) * 1)) / ((((c_d r) . (n + 2)) * ((rfs r) . (n + 3))) + (((c_d r) . (n + 1)) * ((1 / ((rfs r) . (n + 3))) * ((rfs r) . (n + 3))))) by XCMPLX_1:106, A1, Th3
.= ((((c_n r) . (n + 2)) * ((rfs r) . (n + 3))) + (((c_n r) . (n + 1)) * 1)) / ((((c_d r) . (n + 2)) * ((rfs r) . (n + 3))) + (((c_d r) . (n + 1)) * 1)) by XCMPLX_1:106, A1, Th3
.= ((((c_n r) . ((n + 1) + 1)) * ((rfs r) . ((n + 1) + 2))) + ((c_n r) . (n + 1))) / ((((c_d r) . ((n + 1) + 1)) * ((rfs r) . ((n + 1) + 2))) + ((c_d r) . (n + 1))) ;
hence S1[n + 1] ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A2, A7);
 hence r = ((((c_n r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_n r) . n)) / ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n)) ; :: thesis: verum