let r be natural Number ; for n being Nat holds
( ( r <> 0 or n = 0 ) iff r |^ n <> 0 )
let n be Nat; ( ( r <> 0 or n = 0 ) iff r |^ n <> 0 )
defpred S2[ Nat] means ( ( r <> 0 or $1 = 0 ) iff r |^ $1 <> 0 );
A1:
for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
assume A2:
S2[
k]
;
S2[k + 1]
r |^ (k + 1) = (r |^ k) * r
by Th6;
hence
S2[
k + 1]
by A2;
verum
end;
A3:
S2[ 0 ]
by RVSUM_1:94;
for k being Nat holds S2[k]
from NAT_1:sch 2(A3, A1);
hence
( ( r <> 0 or n = 0 ) iff r |^ n <> 0 )
; verum