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 ⊢ A ∈ ℤ ∧ B ∈ ℕ → denom ⁡ A B ≤ B

Proof

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