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 ⊢ 1 2 = 1
10 9 a1i ⊢ A ∈ ℤ ∧ A ∈ ℚ → 1 2 = 1
11 zcn ⊢ A ∈ ℤ → A ∈ ℂ
12 11 sqsqrtd ⊢ A ∈ ℤ → A 2 = A
13 12 adantr ⊢ A ∈ ℤ ∧ A ∈ ℚ → A 2 = A
14 13 fveq2d ⊢ A ∈ ℤ ∧ A ∈ ℚ → denom ⁡ A 2 = 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 ⁡ A 2 = 1
22 densq ⊢ A ∈ ℚ → denom ⁡ A 2 = denom ⁡ A 2
23 22 adantl ⊢ A ∈ ℤ ∧ A ∈ ℚ → denom ⁡ A 2 = denom ⁡ A 2
24 10 21 23 3eqtr2rd ⊢ A ∈ ℤ ∧ A ∈ ℚ → denom ⁡ A 2 = 1 2
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 ∈ ℤ