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

Metamath Proof Explorer

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 ‘ ( 𝐴 / 𝐵 ) ) ≤ 𝐵 )