let k be Element of NAT ; :: thesis: for th being Real holds
( (th * <i> ) |^ (2 * k) = ((- 1) |^ k) * (th |^ (2 * k)) & (th * <i> ) |^ ((2 * k) + 1) = (((- 1) |^ k) * (th |^ ((2 * k) + 1))) * <i> )
let th be Real; :: thesis: ( (th * <i> ) |^ (2 * k) = ((- 1) |^ k) * (th |^ (2 * k)) & (th * <i> ) |^ ((2 * k) + 1) = (((- 1) |^ k) * (th |^ ((2 * k) + 1))) * <i> )
A1: (((- 1) |^ 0 ) * (th |^ (2 * 0 ))) * <i> = (((- 1) |^ 0 ) * ((th GeoSeq ) . 0 )) * <i> by PREPOWER:def 1
.= (((- 1) |^ 0 ) * 1) * <i> by PREPOWER:4
.= (((- 1) GeoSeq ) . 0 ) * <i> by PREPOWER:def 1
.= 1 * <i> by PREPOWER:4 ;
A2: (th * <i> ) |^ ((2 * 0 ) + 1) = (((th * <i> ) GeoSeq ) . 0 ) * (th * <i> ) by COMSEQ_3:def 1
.= 1 * (th * <i> ) by COMSEQ_3:def 1
.= th * <i> ;
defpred S₁[ Element of NAT ] means ( (th * <i> ) |^ (2 * $1) = ((- 1) |^ $1) * (th |^ (2 * $1)) & (th * <i> ) |^ ((2 * $1) + 1) = (((- 1) |^ $1) * (th |^ ((2 * $1) + 1))) * <i> );
A3: (((- 1) |^ 0 ) * (th |^ ((2 * 0 ) + 1))) * <i> = (((- 1) |^ 0 ) * ((th GeoSeq ) . ((2 * 0 ) + 1))) * <i> by PREPOWER:def 1
.= (((- 1) |^ 0 ) * (((th GeoSeq ) . 0 ) * th)) * <i> by PREPOWER:4
.= (((- 1) |^ 0 ) * (1 * th)) * <i> by PREPOWER:4
.= ((((- 1) GeoSeq ) . 0 ) * th) * <i> by PREPOWER:def 1
.= (1 * th) * <i> by PREPOWER:4
.= th * <i> ;
A4: S₁[ 0 ] by A1, A2, A3, COMSEQ_3:def 1;
A5: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A6: (th * <i> ) |^ (2 * k) = ((- 1) |^ k) * (th |^ (2 * k)) and
A7: (th * <i> ) |^ ((2 * k) + 1) = (((- 1) |^ k) * (th |^ ((2 * k) + 1))) * <i> ; :: thesis: S₁[k + 1]
A8: (th * <i> ) |^ (2 * (k + 1)) = ((th * <i> ) |^ 2) |^ (k + 1) by Th35
.= (((th * <i> ) |^ 2) |^ k) * ((th * <i> ) |^ 2) by COMSEQ_3:def 1
.= (((- 1) |^ k) * (th |^ (2 * k))) * (((th * <i> ) GeoSeq ) . (1 + 1)) by A6, Th35
.= (((- 1) |^ k) * (th |^ (2 * k))) * ((((th * <i> ) GeoSeq ) . (0 + 1)) * (th * <i> )) by COMSEQ_3:def 1
.= (((- 1) |^ k) * (th |^ (2 * k))) * (((((th * <i> ) GeoSeq ) . 0 ) * (th * <i> )) * (th * <i> )) by COMSEQ_3:def 1
.= (((- 1) |^ k) * (th |^ (2 * k))) * ((1r * (th * <i> )) * (th * <i> )) by COMSEQ_3:def 1
.= (((((- 1) |^ k) * (- 1)) * (th |^ (2 * k))) * th) * th
.= ((((((- 1) GeoSeq ) . k) * (- 1)) * (th |^ (2 * k))) * th) * th by PREPOWER:def 1
.= (((((- 1) GeoSeq ) . (k + 1)) * (th |^ (2 * k))) * th) * th by PREPOWER:4
.= ((((- 1) |^ (k + 1)) * (th |^ (2 * k))) * th) * th by PREPOWER:def 1
.= ((((- 1) |^ (k + 1)) * ((th GeoSeq ) . (2 * k))) * th) * th by PREPOWER:def 1
.= (((- 1) |^ (k + 1)) * (((th GeoSeq ) . (2 * k)) * th)) * th
.= (((- 1) |^ (k + 1)) * ((th GeoSeq ) . ((2 * k) + 1))) * th by PREPOWER:4
.= ((- 1) |^ (k + 1)) * (((th GeoSeq ) . ((2 * k) + 1)) * th)
.= ((- 1) |^ (k + 1)) * ((th GeoSeq ) . (((2 * k) + 1) + 1)) by PREPOWER:4
.= ((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1))) by PREPOWER:def 1 ;
A9: (th * <i> ) |^ ((2 * (k + 1)) + 1) = (((th * <i> ) GeoSeq ) . (((2 * k) + 1) + 1)) * (th * <i> ) by COMSEQ_3:def 1
.= ((((th * <i> ) GeoSeq ) . ((2 * k) + 1)) * (th * <i> )) * (th * <i> ) by COMSEQ_3:def 1
.= ((((((- 1) |^ k) * (- 1)) * (th |^ ((2 * k) + 1))) * th) * th) * <i> by A7
.= (((((((- 1) GeoSeq ) . k) * (- 1)) * (th |^ ((2 * k) + 1))) * th) * th) * <i> by PREPOWER:def 1
.= ((((((- 1) GeoSeq ) . (k + 1)) * (th |^ ((2 * k) + 1))) * th) * th) * <i> by PREPOWER:4
.= (((((- 1) |^ (k + 1)) * (th |^ ((2 * k) + 1))) * th) * th) * <i> by PREPOWER:def 1
.= (((((- 1) |^ (k + 1)) * ((th GeoSeq ) . ((2 * k) + 1))) * th) * th) * <i> by PREPOWER:def 1
.= ((((- 1) |^ (k + 1)) * (((th GeoSeq ) . ((2 * k) + 1)) * th)) * th) * <i>
.= ((((- 1) |^ (k + 1)) * ((th GeoSeq ) . (((2 * k) + 1) + 1))) * th) * <i> by PREPOWER:4
.= (((- 1) |^ (k + 1)) * (((th GeoSeq ) . (((2 * k) + 1) + 1)) * th)) * <i>
.= (((- 1) |^ (k + 1)) * ((th GeoSeq ) . ((2 * (k + 1)) + 1))) * <i> by PREPOWER:4
.= (((- 1) |^ (k + 1)) * (th |^ ((2 * (k + 1)) + 1))) * <i> by PREPOWER:def 1 ;
thus S₁[k + 1] by A8, A9; :: thesis: verum

end;

A10: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A5);
thus ( (th * <i> ) |^ (2 * k) = ((- 1) |^ k) * (th |^ (2 * k)) & (th * <i> ) |^ ((2 * k) + 1) = (((- 1) |^ k) * (th |^ ((2 * k) + 1))) * <i> ) by A10; :: thesis: verum