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

Theorem nn0sqrtelqelz 11873
 Description: If a nonnegative integer has a rational square root, that root must be an integer. (Contributed by Jim Kingdon, 24-May-2022.)
Assertion
Ref Expression
nn0sqrtelqelz

Proof of Theorem nn0sqrtelqelz
StepHypRef Expression
1 qdencl 11856 . . . . 5 denom
21adantl 275 . . . 4 denom
32nnred 8726 . . 3 denom
4 1red 7774 . . 3
52nnnn0d 9023 . . . 4 denom
65nn0ge0d 9026 . . 3 denom
7 0le1 8236 . . . 4
87a1i 9 . . 3
9 sq1 10379 . . . . 5
109a1i 9 . . . 4
11 simpl 108 . . . . . . . 8
1211nn0red 9024 . . . . . . 7
1311nn0ge0d 9026 . . . . . . 7
14 resqrtth 10796 . . . . . . 7
1512, 13, 14syl2anc 408 . . . . . 6
1615fveq2d 5418 . . . . 5 denom denom
17 nn0z 9067 . . . . . . 7
1811, 17syl 14 . . . . . 6
19 zq 9411 . . . . . . . . 9
2017, 19syl 14 . . . . . . . 8
2111, 20syl 14 . . . . . . 7
22 qden1elz 11872 . . . . . . 7 denom
2321, 22syl 14 . . . . . 6 denom
2418, 23mpbird 166 . . . . 5 denom
2516, 24eqtrd 2170 . . . 4 denom
26 densq 11871 . . . . 5 denom denom
2726adantl 275 . . . 4 denom denom
2810, 25, 273eqtr2rd 2177 . . 3 denom
293, 4, 6, 8, 28sq11d 10450 . 2 denom
30 qden1elz 11872 . . 3 denom