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⁡AB≤B

Proof

Step Hyp Ref Expression
1 divnumden ⊢A∈ℤ∧B∈ℕ→numer⁡AB=AAgcdB∧denom⁡AB=BAgcdB
2 1 simprd ⊢A∈ℤ∧B∈ℕ→denom⁡AB=BAgcdB
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→AgcdB∈ℕ
11 3 5 9 10 syl21anc ⊢A∈ℤ∧B∈ℕ→AgcdB∈ℕ
12 11 nnge1d ⊢A∈ℤ∧B∈ℕ→1≤AgcdB
13 1red ⊢A∈ℤ∧B∈ℕ→1∈ℝ
14 0lt1 ⊢0<1
15 14 a1i ⊢A∈ℤ∧B∈ℕ→0<1
16 11 nnred ⊢A∈ℤ∧B∈ℕ→AgcdB∈ℝ
17 11 nngt0d ⊢A∈ℤ∧B∈ℕ→0<AgcdB
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∧AgcdB∈ℝ∧0<AgcdB∧B∈ℝ∧0<B→1≤AgcdB↔BAgcdB≤B1
23 13 15 16 17 19 21 22 syl222anc ⊢A∈ℤ∧B∈ℕ→1≤AgcdB↔BAgcdB≤B1
24 12 23 mpbid ⊢A∈ℤ∧B∈ℕ→BAgcdB≤B1
25 nncn ⊢B∈ℕ→B∈ℂ
26 25 adantl ⊢A∈ℤ∧B∈ℕ→B∈ℂ
27 26 div1d ⊢A∈ℤ∧B∈ℕ→B1=B
28 24 27 breqtrd ⊢A∈ℤ∧B∈ℕ→BAgcdB≤B
29 2 28 eqbrtrd ⊢A∈ℤ∧B∈ℕ→denom⁡AB≤B