let k be 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:3
.= (((- 1) GeoSeq) . 0) * <i> by PREPOWER:def 1
.= 1 * <i> by PREPOWER:3 ;
defpred S₁[ Nat] means ( (th * <i>) |^ (2 * $1) = ((- 1) |^ $1) * (th |^ (2 * $1)) & (th * <i>) |^ ((2 * $1) + 1) = (((- 1) |^ $1) * (th |^ ((2 * $1) + 1))) * <i> );
(((- 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:3
.= (((- 1) |^ 0) * (1 * th)) * <i> by PREPOWER:3
.= ((((- 1) GeoSeq) . 0) * th) * <i> by PREPOWER:def 1
.= (1 * th) * <i> by PREPOWER:3
.= th * <i> ;
then A2: S₁[ 0 ] by A1, COMSEQ_3:def 1;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A4: (th * <i>) |^ (2 * k) = ((- 1) |^ k) * (th |^ (2 * k)) and
A5: (th * <i>) |^ ((2 * k) + 1) = (((- 1) |^ k) * (th |^ ((2 * k) + 1))) * <i> ; :: thesis: S₁[k + 1]
A6: (th * <i>) |^ (2 * (k + 1)) = ((th * <i>) |^ 2) |^ (k + 1) by Th32
.= (((th * <i>) |^ 2) |^ k) * ((th * <i>) |^ 2) by COMSEQ_3:def 1
.= (((- 1) |^ k) * (th |^ (2 * k))) * (((th * <i>) GeoSeq) . (1 + 1)) by A4, Th32
.= (((- 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:3
.= ((((- 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:3
.= ((- 1) |^ (k + 1)) * (((th GeoSeq) . ((2 * k) + 1)) * th)
.= ((- 1) |^ (k + 1)) * ((th GeoSeq) . (((2 * k) + 1) + 1)) by PREPOWER:3
.= ((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1))) by PREPOWER:def 1 ;
(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 A5
.= (((((((- 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:3
.= (((((- 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:3
.= (((- 1) |^ (k + 1)) * (((th GeoSeq) . (((2 * k) + 1) + 1)) * th)) * <i>
.= (((- 1) |^ (k + 1)) * ((th GeoSeq) . ((2 * (k + 1)) + 1))) * <i> by PREPOWER:3
.= (((- 1) |^ (k + 1)) * (th |^ ((2 * (k + 1)) + 1))) * <i> by PREPOWER:def 1 ;
hence S₁[k + 1] by A6; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
hence ( (th * <i>) |^ (2 * k) = ((- 1) |^ k) * (th |^ (2 * k)) & (th * <i>) |^ ((2 * k) + 1) = (((- 1) |^ k) * (th |^ ((2 * k) + 1))) * <i> ) ; :: thesis: verum