thus ( n is square-containing implies ex r being Real st r = 0 ) ; :: thesis: ( not n is square-containing implies ex b1 being Real ex n9 being non zero Nat st
( n9 = n & b1 = (- 1) |^ (card (support (ppf n9))) ) )
( n is square-free implies ex n9 being non zero Nat st
( n9 = n & ex r being Real st r = (- 1) |^ (card (support (ppf n9))) ) )
proof
assume A1: n is square-free ; :: thesis: ex n9 being non zero Nat st
( n9 = n & ex r being Real st r = (- 1) |^ (card (support (ppf n9))) )
n is non zero Nat
proof
set p = the Prime;
assume n is not non zero Nat ; :: thesis: contradiction
then the Prime |^ 2 divides n by NAT_D:6;
hence contradiction by A1; :: thesis: verum
end;
then reconsider n9 = n as non zero Nat ;
ex r being Real st r = (- 1) |^ (card (support (ppf n9))) ;
hence ex n9 being non zero Nat st
( n9 = n & ex r being Real st r = (- 1) |^ (card (support (ppf n9))) ) ; :: thesis: verum
end;
hence ( not n is square-containing implies ex b1 being Real ex n9 being non zero Nat st
( n9 = n & b1 = (- 1) |^ (card (support (ppf n9))) ) ) ; :: thesis: verum