let a be square-free Nat; :: thesis: for b being non zero Nat
for n being non trivial Nat st b < a |^ n & a divides b holds
n -root b is irrational
let b be non zero Nat; :: thesis: for n being non trivial Nat st b < a |^ n & a divides b holds
n -root b is irrational
let n be non trivial Nat; :: thesis: ( b < a |^ n & a divides b implies n -root b is irrational )
assume A1: ( b < a |^ n & a divides b ) ; :: thesis: n -root b is irrational
A1a: b >= 1 by NAT_1:14;
then a |^ n > 1 |^ n by A1, XXREAL_0:2;
then A2: |.a.| > 1 by NEWTON02:40;
reconsider a = a as non trivial Nat by NAT_2:def 1, A1, A1a;
reconsider m = a |-count b as Nat ;
a |^ 1 divides b by A1;
then reconsider m = m as non zero Nat by NEWTON03:59;
m < n by A1, NEWTON03:62;
then consider k being Nat such that
A3: n = m + k by NAT_1:10;
reconsider k = k as non zero Nat by A1, NEWTON03:62, A3;
a |^ (a |-count b) divides b by A2, NEWTON03:def 7;
then consider c being Nat such that
A4: b = (a |^ (a |-count b)) * c by NAT_D:def 3;
reconsider c = c as non zero Nat by A4;
(m + k) -root ((a |^ m) * c) is irrational by Th20, A4, NEWTON03:76;
hence n -root b is irrational by A3, A4; :: thesis: verum