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

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 ( 𝐴 ∈ ℚ → ( ( denom ‘ 𝐴 ) = 1 ↔ 𝐴 ∈ ℤ ) )

Proof

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