let n be non zero Nat; :: thesis: 'I' . (2 * n) = ((Product (odd-seq n)) / (Product (even-seq n))) * (PI / 2)
defpred S₁[ non zero Nat] means 'I' . (2 * $1) = ((Product (odd-seq $1)) / (Product (even-seq $1))) * (PI / 2);
A1: for n being non zero Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non zero Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
set Podd1 = Product (odd-seq n);
set Peven1 = Product (even-seq n);
n + 1 >= 0 + 1 by XREAL_1:6;
then A3: 2 * (n + 1) >= 2 * 1 by XREAL_1:64;
then A4: (2 * (n + 1)) -' 1 = (2 * (n + 1)) - 1 by XXREAL_0:2, XREAL_1:233
.= (2 * n) + 1 ;
A5: (2 * (n + 1)) -' 2 = (2 * (n + 1)) - 2 by A3, XREAL_1:233
.= 2 * n ;
A6: Product (even-seq (n + 1)) = (2 * (n + 1)) * (Product (even-seq n)) by Th9;
'I' . (2 * (n + 1)) = (((2 * n) + 1) / (2 * (n + 1))) * ('I' . (2 * n)) by Th36, A3, A4, A5
.= ((((2 * n) + 1) / (2 * (n + 1))) * ((Product (odd-seq n)) / (Product (even-seq n)))) * (PI / 2) by A2
.= ((((2 * n) + 1) * (Product (odd-seq n))) / ((2 * (n + 1)) * (Product (even-seq n)))) * (PI / 2) by XCMPLX_1:76
.= ((Product (odd-seq (n + 1))) / (Product (even-seq (n + 1)))) * (PI / 2) by A6, Th10 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A7: S₁[1]

proof

set n = 1;
A8: 2 -' 2 = 2 - 2 by XREAL_1:233
.= 0 ;
2 -' 1 = 2 - 1 by XREAL_1:233
.= 1 ;
then 'I' . (2 * 1) = (1 / 2) * ('I' . 0) by A8, Th36
.= (1 / 2) * (PI / 2) by Th32, Def6 ;
hence S₁[1] by Th5, Th8; :: thesis: verum

end;

for n being non zero Nat holds S₁[n] from NAT_1:sch 10(A7, A1);
hence 'I' . (2 * n) = ((Product (odd-seq n)) / (Product (even-seq n))) * (PI / 2) ; :: thesis: verum