This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℤ ∧ ( √ ‘ 𝐴 ) ∈ ℚ ) → ( √ ‘ 𝐴 ) ∈ ℤ )

Proof

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