Metamath Proof Explorer

Theorem zsqrtelqelz

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

Ref Expression
Assertion zsqrtelqelz ⊢A∈ℤ∧A∈ℚ→A∈ℤ

Proof

Step Hyp Ref Expression
1 qdencl ⊢A∈ℚ→denom⁡A∈ℕ
2 1 adantl ⊢A∈ℤ∧A∈ℚ→denom⁡A∈ℕ
3 2 nnred ⊢A∈ℤ∧A∈ℚ→denom⁡A∈ℝ
4 1red ⊢A∈ℤ∧A∈ℚ→1∈ℝ
5 2 nnnn0d ⊢A∈ℤ∧A∈ℚ→denom⁡A∈ℕ0
6 5 nn0ge0d ⊢A∈ℤ∧A∈ℚ→0≤denom⁡A
7 0le1 ⊢0≤1
8 7 a1i ⊢A∈ℤ∧A∈ℚ→0≤1
9 sq1 ⊢12=1
10 9 a1i ⊢A∈ℤ∧A∈ℚ→12=1
11 zcn ⊢A∈ℤ→A∈ℂ
12 11 sqsqrtd ⊢A∈ℤ→A2=A
13 12 adantr ⊢A∈ℤ∧A∈ℚ→A2=A
14 13 fveq2d ⊢A∈ℤ∧A∈ℚ→denom⁡A2=denom⁡A
15 simpl ⊢A∈ℤ∧A∈ℚ→A∈ℤ
16 zq ⊢A∈ℤ→A∈ℚ
17 16 adantr ⊢A∈ℤ∧A∈ℚ→A∈ℚ
18 qden1elz ⊢A∈ℚ→denom⁡A=1↔A∈ℤ
19 17 18 syl ⊢A∈ℤ∧A∈ℚ→denom⁡A=1↔A∈ℤ
20 15 19 mpbird ⊢A∈ℤ∧A∈ℚ→denom⁡A=1
21 14 20 eqtrd ⊢A∈ℤ∧A∈ℚ→denom⁡A2=1
22 densq ⊢A∈ℚ→denom⁡A2=denom⁡A2
23 22 adantl ⊢A∈ℤ∧A∈ℚ→denom⁡A2=denom⁡A2
24 10 21 23 3eqtr2rd ⊢A∈ℤ∧A∈ℚ→denom⁡A2=12
25 3 4 6 8 24 sq11d ⊢A∈ℤ∧A∈ℚ→denom⁡A=1
26 qden1elz ⊢A∈ℚ→denom⁡A=1↔A∈ℤ
27 26 adantl ⊢A∈ℤ∧A∈ℚ→denom⁡A=1↔A∈ℤ
28 25 27 mpbid ⊢A∈ℤ∧A∈ℚ→A∈ℤ