let b be non zero Nat; :: thesis: for n being non trivial Nat st 2 -root b is natural holds
2 -root (b + 2) is irrational
let n be non trivial Nat; :: thesis: ( 2 -root b is natural implies 2 -root (b + 2) is irrational )
reconsider a = b + 1 as non trivial Nat ;
(2 -root b) * (2 -root (b + 2)) = 2 -root ((a - 1) * (a + 1)) by POWER:11
.= 2 -root ((a |^ 2) - (1 |^ 2)) by NEWTON01:1
.= 2 -root ((a |^ 2) - 1) ;
hence ( 2 -root b is natural implies 2 -root (b + 2) is irrational ) ; :: thesis: verum