Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  nonsq Unicode version

Theorem nonsq 11885
 Description: Any integer strictly between two adjacent squares has a non-rational square root. (Contributed by Stefan O'Rear, 15-Sep-2014.)
Assertion
Ref Expression
nonsq

Proof of Theorem nonsq
StepHypRef Expression
1 nn0z 9074 . . . 4
3 simprl 520 . . . . 5
4 simpll 518 . . . . . . 7
54nn0red 9031 . . . . . 6
64nn0ge0d 9033 . . . . . 6
7 resqrtth 10803 . . . . . 6
85, 6, 7syl2anc 408 . . . . 5
93, 8breqtrrd 3956 . . . 4
10 simplr 519 . . . . . 6
1110nn0red 9031 . . . . 5
12 nn0re 8986 . . . . . . 7
1312ad2antrr 479 . . . . . 6
1413, 6resqrtcld 10935 . . . . 5
1510nn0ge0d 9033 . . . . 5
1613, 6sqrtge0d 10938 . . . . 5
1711, 14, 15, 16lt2sqd 10455 . . . 4
189, 17mpbird 166 . . 3
19 simprr 521 . . . . 5
208, 19eqbrtrd 3950 . . . 4
21 peano2re 7898 . . . . . 6
2211, 21syl 14 . . . . 5
23 peano2nn0 9017 . . . . . . 7
2423ad2antlr 480 . . . . . 6
2524nn0ge0d 9033 . . . . 5
2614, 22, 16, 25lt2sqd 10455 . . . 4
2720, 26mpbird 166 . . 3
28 btwnnz 9145 . . 3
292, 18, 27, 28syl3anc 1216 . 2
30 nn0sqrtelqelz 11884 . . . 4
3130ex 114 . . 3