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⁡Adenom⁡A
2 1 adantr ⊢A∈ℚ∧denom⁡A=1→A=numer⁡Adenom⁡A
3 oveq2 ⊢denom⁡A=1→numer⁡Adenom⁡A=numer⁡A1
4 3 adantl ⊢A∈ℚ∧denom⁡A=1→numer⁡Adenom⁡A=numer⁡A1
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⁡A1=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∈ℤ→A1=A
14 13 fveq2d ⊢A∈ℚ∧A∈ℤ→denom⁡A1=denom⁡A
15 1nn ⊢1∈ℕ
16 divdenle ⊢A∈ℤ∧1∈ℕ→denom⁡A1≤1
17 11 15 16 sylancl ⊢A∈ℚ∧A∈ℤ→denom⁡A1≤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∈ℤ