let a, b be non zero Nat; :: thesis: ( b <= 2 * a implies 2 -root ((a |^ 2) + b) is irrational )
A1: ((a + 1) + 0) |^ 2 = (((((a |^ 2) + (1 |^ 2)) + (0 |^ 2)) + ((2 * a) * 1)) + ((2 * a) * 0)) + ((2 * 1) * 0) by SERIES_4:1;
assume b <= 2 * a ; :: thesis: 2 -root ((a |^ 2) + b) is irrational
then b < (2 * a) + 1 by NAT_1:13;
then ((2 * a) + 1) + (a |^ 2) > b + (a |^ 2) by XREAL_1:6;
then ( (a + 1) |^ 2 > (a |^ 2) + b & (a |^ 2) + b > (a |^ 2) + 0 ) by A1, XREAL_1:6;
hence 2 -root ((a |^ 2) + b) is irrational by Th4; :: thesis: verum