Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nonsq Structured version   Unicode version

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

Proof of Theorem nonsq
StepHypRef Expression
1 nn0z 10296 . . . 4
3 simprl 733 . . . . 5
4 nn0re 10222 . . . . . . . 8
54ad2antrr 707 . . . . . . 7
65recnd 9106 . . . . . 6
76sqsqrd 12233 . . . . 5
83, 7breqtrrd 4230 . . . 4
9 nn0re 10222 . . . . . 6
109ad2antlr 708 . . . . 5
11 nn0ge0 10239 . . . . . . 7
1211ad2antrr 707 . . . . . 6
135, 12resqrcld 12212 . . . . 5
14 nn0ge0 10239 . . . . . 6
1514ad2antlr 708 . . . . 5
165, 12sqrge0d 12215 . . . . 5
1710, 13, 15, 16lt2sqd 11549 . . . 4
188, 17mpbird 224 . . 3
19 simprr 734 . . . . 5
207, 19eqbrtrd 4224 . . . 4
21 peano2re 9231 . . . . . 6
2210, 21syl 16 . . . . 5
23 peano2nn0 10252 . . . . . . 7
24 nn0ge0 10239 . . . . . . 7
2523, 24syl 16 . . . . . 6
2625ad2antlr 708 . . . . 5
2713, 22, 16, 26lt2sqd 11549 . . . 4
2820, 27mpbird 224 . . 3
29 btwnnz 10338 . . 3
302, 18, 28, 29syl3anc 1184 . 2
31 nn0z 10296 . . . 4