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 
|- ( ( A e. ZZ /\ B e. NN ) -> ( denom ` ( A / B ) ) <_ B )

Proof

Step Hyp Ref Expression
1 divnumden 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( numer ` ( A / B ) ) = ( A / ( A gcd B ) ) /\ ( denom ` ( A / B ) ) = ( B / ( A gcd B ) ) ) )
2 1 simprd 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( denom ` ( A / B ) ) = ( B / ( A gcd B ) ) )
3 simpl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> A e. ZZ )
4 nnz 
 |-  ( B e. NN -> B e. ZZ )
5 4 adantl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> B e. ZZ )
6 nnne0 
 |-  ( B e. NN -> B =/= 0 )
7 6 neneqd 
 |-  ( B e. NN -> -. B = 0 )
8 7 adantl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> -. B = 0 )
9 8 intnand 
 |-  ( ( A e. ZZ /\ B e. NN ) -> -. ( A = 0 /\ B = 0 ) )
10 gcdn0cl 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ -. ( A = 0 /\ B = 0 ) ) -> ( A gcd B ) e. NN )
11 3 5 9 10 syl21anc 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A gcd B ) e. NN )
12 11 nnge1d 
 |-  ( ( A e. ZZ /\ B e. NN ) -> 1 <_ ( A gcd B ) )
13 1red 
 |-  ( ( A e. ZZ /\ B e. NN ) -> 1 e. RR )
14 0lt1 
 |-  0 < 1
15 14 a1i 
 |-  ( ( A e. ZZ /\ B e. NN ) -> 0 < 1 )
16 11 nnred 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A gcd B ) e. RR )
17 11 nngt0d 
 |-  ( ( A e. ZZ /\ B e. NN ) -> 0 < ( A gcd B ) )
18 nnre 
 |-  ( B e. NN -> B e. RR )
19 18 adantl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> B e. RR )
20 nngt0 
 |-  ( B e. NN -> 0 < B )
21 20 adantl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> 0 < B )
22 lediv2 
 |-  ( ( ( 1 e. RR /\ 0 < 1 ) /\ ( ( A gcd B ) e. RR /\ 0 < ( A gcd B ) ) /\ ( B e. RR /\ 0 < B ) ) -> ( 1 <_ ( A gcd B ) <-> ( B / ( A gcd B ) ) <_ ( B / 1 ) ) )
23 13 15 16 17 19 21 22 syl222anc 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( 1 <_ ( A gcd B ) <-> ( B / ( A gcd B ) ) <_ ( B / 1 ) ) )
24 12 23 mpbid 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( B / ( A gcd B ) ) <_ ( B / 1 ) )
25 nncn 
 |-  ( B e. NN -> B e. CC )
26 25 adantl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> B e. CC )
27 26 div1d 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( B / 1 ) = B )
28 24 27 breqtrd 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( B / ( A gcd B ) ) <_ B )
29 2 28 eqbrtrd 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( denom ` ( A / B ) ) <_ B )