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 ↔ 𝐴 ∈ ℤ ) )