reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
per cases ( d = 0 or d <> 0 ) ;
suppose A3: d = 0 ; :: thesis: ex b1 being Nat st
( d |^ b1 divides n & not d |^ (b1 + 1) divides n )
take 0 ; :: thesis: ( d |^ 0 divides n & not d |^ (0 + 1) divides n )
0 |^ 0 = 1 by NEWTON:4;
hence d |^ 0 divides n by A3, NAT_D:6; :: thesis: not d |^ (0 + 1) divides n
not 0 divides n1 by A2;
hence not d |^ (0 + 1) divides n by A3; :: thesis: verum
end;
suppose A4: d <> 0 ; :: thesis: ex b1 being Nat st
( d |^ b1 divides n & not d |^ (b1 + 1) divides n )
defpred S1[ Nat] means d |^ $1 divides n;
A5: for k being Nat st S1[k] holds
k <= n1
proof
let k be Nat; :: thesis: ( S1[k] implies k <= n1 )
assume S1[k] ; :: thesis: k <= n1
then A6: d |^ k <= n by A2, NAT_D:7;
k <= d |^ k by A1, A4, Th2, NAT_1:25;
hence k <= n1 by A6, XXREAL_0:2; :: thesis: verum
end;
A7: ex k being Nat st S1[k]
proof
take 0 ; :: thesis: S1[ 0 ]
d |^ 0 = 1 by NEWTON:4;
hence S1[ 0 ] by NAT_D:6; :: thesis: verum
end;
consider k being Nat such that
A8: ( S1[k] & ( for n being Nat st S1[n] holds
n <= k ) ) from NAT_1:sch 6(A5, A7);
take k ; :: thesis: ( d |^ k divides n & not d |^ (k + 1) divides n )
k + 0 < k + 1 by XREAL_1:6;
hence ( d |^ k divides n & not d |^ (k + 1) divides n ) by A8; :: thesis: verum
end;
end;