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

Theorem zsqrelqelz 13958
 Description: If an integer has a rational square root, that root is must be an integer. (Contributed by Stefan O'Rear, 15-Sep-2014.)
Assertion
Ref Expression
zsqrelqelz

Proof of Theorem zsqrelqelz
StepHypRef Expression
1 qdencl 13941 . . . . 5 denom
21adantl 466 . . . 4 denom
32nnred 10452 . . 3 denom
4 1red 9516 . . 3
52nnnn0d 10751 . . . 4 denom
65nn0ge0d 10754 . . 3 denom
7 0le1 9978 . . . 4
87a1i 11 . . 3
9 sq1 12081 . . . . 5
109a1i 11 . . . 4
11 zcn 10766 . . . . . . . 8
1211sqsqrd 13047 . . . . . . 7
1312adantr 465 . . . . . 6
1413fveq2d 5806 . . . . 5 denom denom
15 simpl 457 . . . . . 6
16 zq 11074 . . . . . . . 8
1716adantr 465 . . . . . . 7
18 qden1elz 13957 . . . . . . 7 denom
1917, 18syl 16 . . . . . 6 denom
2015, 19mpbird 232 . . . . 5 denom
2114, 20eqtrd 2495 . . . 4 denom
22 densq 13956 . . . . 5 denom denom
2322adantl 466 . . . 4 denom denom
2410, 21, 233eqtr2rd 2502 . . 3 denom
253, 4, 6, 8, 24sq11d 12165 . 2 denom
26 qden1elz 13957 . . 3 denom