Metamath Proof Explorer

Theorem qden1elz

Description: A rational is an integer iff it has denominator 1. (Contributed by Stefan O'Rear, 15-Sep-2014)

Ref Expression
Assertion qden1elz ⊢ A ∈ ℚ → denom ⁡ A = 1 ↔ A ∈ ℤ

Proof

Step Hyp Ref Expression
1 qeqnumdivden ⊢ A ∈ ℚ → A = numer ⁡ A denom ⁡ A
2 1 adantr ⊢ A ∈ ℚ ∧ denom ⁡ A = 1 → A = numer ⁡ A denom ⁡ A
3 oveq2 ⊢ denom ⁡ A = 1 → numer ⁡ A denom ⁡ A = numer ⁡ A 1
4 3 adantl ⊢ A ∈ ℚ ∧ denom ⁡ A = 1 → numer ⁡ A denom ⁡ A = numer ⁡ A 1
5 qnumcl ⊢ A ∈ ℚ → numer ⁡ A ∈ ℤ
6 5 adantr ⊢ A ∈ ℚ ∧ denom ⁡ A = 1 → numer ⁡ A ∈ ℤ
7 6 zcnd ⊢ A ∈ ℚ ∧ denom ⁡ A = 1 → numer ⁡ A ∈ ℂ
8 7 div1d ⊢ A ∈ ℚ ∧ denom ⁡ A = 1 → numer ⁡ A 1 = numer ⁡ A
9 2 4 8 3eqtrd ⊢ A ∈ ℚ ∧ denom ⁡ A = 1 → A = numer ⁡ A
10 9 6 eqeltrd ⊢ A ∈ ℚ ∧ denom ⁡ A = 1 → A ∈ ℤ
11 simpr ⊢ A ∈ ℚ ∧ A ∈ ℤ → A ∈ ℤ
12 11 zcnd ⊢ A ∈ ℚ ∧ A ∈ ℤ → A ∈ ℂ
13 12 div1d ⊢ A ∈ ℚ ∧ A ∈ ℤ → A 1 = A
14 13 fveq2d ⊢ A ∈ ℚ ∧ A ∈ ℤ → denom ⁡ A 1 = denom ⁡ A
15 1nn ⊢ 1 ∈ ℕ
16 divdenle ⊢ A ∈ ℤ ∧ 1 ∈ ℕ → denom ⁡ A 1 ≤ 1
17 11 15 16 sylancl ⊢ A ∈ ℚ ∧ A ∈ ℤ → denom ⁡ A 1 ≤ 1
18 14 17 eqbrtrrd ⊢ A ∈ ℚ ∧ A ∈ ℤ → denom ⁡ A ≤ 1
19 qdencl ⊢ A ∈ ℚ → denom ⁡ A ∈ ℕ
20 19 adantr ⊢ A ∈ ℚ ∧ A ∈ ℤ → denom ⁡ A ∈ ℕ
21 nnle1eq1 ⊢ denom ⁡ A ∈ ℕ → denom ⁡ A ≤ 1 ↔ denom ⁡ A = 1
22 20 21 syl ⊢ A ∈ ℚ ∧ A ∈ ℤ → denom ⁡ A ≤ 1 ↔ denom ⁡ A = 1
23 18 22 mpbid ⊢ A ∈ ℚ ∧ A ∈ ℤ → denom ⁡ A = 1
24 10 23 impbida ⊢ A ∈ ℚ → denom ⁡ A = 1 ↔ A ∈ ℤ