let n be Nat; :: thesis: 17 <> ((10 |^ (n + 1)) - 7) / 3
10 |^ (0 + 1) = 10 ;
then A1: 10 |^ (1 + 1) = 10 * 10 by NEWTON:6;

per cases ( n = 0 or n >= 1 ) by NAT_1:14;

suppose n = 0 ; :: thesis: 17 <> ((10 |^ (n + 1)) - 7) / 3

hence 17 <> ((10 |^ (n + 1)) - 7) / 3 ; :: thesis: verum

end;

suppose n >= 1 ; :: thesis: 17 <> ((10 |^ (n + 1)) - 7) / 3

then n + 1 >= 1 + 1 by XREAL_1:6;
then (10 |^ (n + 1)) - 7 >= (10 |^ 2) - 7 by NAT_6:1, XREAL_1:9;
then ((10 |^ (n + 1)) - 7) / 3 >= ((10 |^ 2) - 7) / 3 by XREAL_1:72;
hence 17 <> ((10 |^ (n + 1)) - 7) / 3 by A1; :: thesis: verum

end;

end;