Theorem divdenle

Description: Reducing a quotient never increases the denominator. (Contributed by Stefan O'Rear, 13-Sep-2014)

	Ref	Expression
Assertion	divdenle	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( denom ‘ ( 𝐴 / 𝐵 ) ) ≤ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		divnumden	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( ( numer ‘ ( 𝐴 / 𝐵 ) ) = ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∧ ( denom ‘ ( 𝐴 / 𝐵 ) ) = ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) )
2	1	simprd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( denom ‘ ( 𝐴 / 𝐵 ) ) = ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) )
3		simpl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 𝐴 ∈ ℤ )
4		nnz	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
5	4	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℤ )
6		nnne0	⊢ ( 𝐵 ∈ ℕ → 𝐵 ≠ 0 )
7	6	neneqd	⊢ ( 𝐵 ∈ ℕ → ¬ 𝐵 = 0 )
8	7	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ¬ 𝐵 = 0 )
9	8	intnand	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
10		gcdn0cl	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
11	3 5 9 10	syl21anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
12	11	nnge1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 1 ≤ ( 𝐴 gcd 𝐵 ) )
13		1red	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 1 ∈ ℝ )
14		0lt1	⊢ 0 < 1
15	14	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 0 < 1 )
16	11	nnred	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℝ )
17	11	nngt0d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 0 < ( 𝐴 gcd 𝐵 ) )
18		nnre	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
19	18	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℝ )
20		nngt0	⊢ ( 𝐵 ∈ ℕ → 0 < 𝐵 )
21	20	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 0 < 𝐵 )
22		lediv2	⊢ ( ( ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( ( 𝐴 gcd 𝐵 ) ∈ ℝ ∧ 0 < ( 𝐴 gcd 𝐵 ) ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 1 ≤ ( 𝐴 gcd 𝐵 ) ↔ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ≤ ( 𝐵 / 1 ) ) )
23	13 15 16 17 19 21 22	syl222anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 1 ≤ ( 𝐴 gcd 𝐵 ) ↔ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ≤ ( 𝐵 / 1 ) ) )
24	12 23	mpbid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ≤ ( 𝐵 / 1 ) )
25		nncn	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℂ )
26	25	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℂ )
27	26	div1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐵 / 1 ) = 𝐵 )
28	24 27	breqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ≤ 𝐵 )
29	2 28	eqbrtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( denom ‘ ( 𝐴 / 𝐵 ) ) ≤ 𝐵 )