let n be non zero Nat; for a being non integer Rational holds not a |^ n is integer
let a be non integer Rational; not a |^ n is integer
consider l being Integer, k being Nat such that
A1:
( k > 0 & a = l / k )
by RAT_1:8;
( k = 1 implies l / k is integer )
;
then reconsider k = k as non trivial Nat by A1, NAT_2:def 1;
reconsider l1 = l / (k gcd l) as Integer ;
( k gcd l divides k & |.k.| <> k gcd l )
by A1, INT_2:def 2;
then
( k >= k gcd l & k <> k gcd l )
by NAT_D:7;
then
k > k gcd l
by XXREAL_0:1;
then reconsider k1 = k / (k gcd l) as non trivial Nat by XREAL_1:187, NEWTON03:def 1;
k1 |^ n,l1 |^ n are_coprime
by Th1, WSIERP_1:11;
then A2:
not k1 |^ n divides l1 |^ n
by NAT_2:def 1;
a |^ n =
(l1 / k1) |^ n
by A1, XCMPLX_1:55
.=
(l1 |^ n) / (k1 |^ n)
by PREPOWER:8
;
hence
not a |^ n is integer
by A2, WSIERP_1:17; verum