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

Metamath Proof Explorer

Theorem divnumden

Description: Calculate the reduced form of a quotient using gcd . (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion divnumden 
|- ( ( A e. ZZ /\ B e. NN ) -> ( ( numer ` ( A / B ) ) = ( A / ( A gcd B ) ) /\ ( denom ` ( A / B ) ) = ( B / ( A gcd B ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> A e. ZZ )
2 nnz 
 |-  ( B e. NN -> B e. ZZ )
3 2 adantl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> B e. ZZ )
4 nnne0 
 |-  ( B e. NN -> B =/= 0 )
5 4 neneqd 
 |-  ( B e. NN -> -. B = 0 )
6 5 adantl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> -. B = 0 )
7 6 intnand 
 |-  ( ( A e. ZZ /\ B e. NN ) -> -. ( A = 0 /\ B = 0 ) )
8 gcdn0cl 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ -. ( A = 0 /\ B = 0 ) ) -> ( A gcd B ) e. NN )
9 1 3 7 8 syl21anc 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A gcd B ) e. NN )
10 gcddvds 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
11 2 10 sylan2 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
12 gcddiv 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( A gcd B ) e. NN ) /\ ( ( A gcd B ) || A /\ ( A gcd B ) || B ) ) -> ( ( A gcd B ) / ( A gcd B ) ) = ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) )
13 1 3 9 11 12 syl31anc 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( A gcd B ) / ( A gcd B ) ) = ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) )
14 9 nncnd 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A gcd B ) e. CC )
15 9 nnne0d 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A gcd B ) =/= 0 )
16 14 15 dividd 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( A gcd B ) / ( A gcd B ) ) = 1 )
17 13 16 eqtr3d 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 )
18 zcn 
 |-  ( A e. ZZ -> A e. CC )
19 18 adantr 
 |-  ( ( A e. ZZ /\ B e. NN ) -> A e. CC )
20 nncn 
 |-  ( B e. NN -> B e. CC )
21 20 adantl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> B e. CC )
22 4 adantl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> B =/= 0 )
23 divcan7 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( ( A gcd B ) e. CC /\ ( A gcd B ) =/= 0 ) ) -> ( ( A / ( A gcd B ) ) / ( B / ( A gcd B ) ) ) = ( A / B ) )
24 23 eqcomd 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( ( A gcd B ) e. CC /\ ( A gcd B ) =/= 0 ) ) -> ( A / B ) = ( ( A / ( A gcd B ) ) / ( B / ( A gcd B ) ) ) )
25 19 21 22 14 15 24 syl122anc 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A / B ) = ( ( A / ( A gcd B ) ) / ( B / ( A gcd B ) ) ) )
26 znq 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A / B ) e. QQ )
27 11 simpld 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A gcd B ) || A )
28 gcdcl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) e. NN0 )
29 28 nn0zd 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) e. ZZ )
30 2 29 sylan2 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A gcd B ) e. ZZ )
31 dvdsval2 
 |-  ( ( ( A gcd B ) e. ZZ /\ ( A gcd B ) =/= 0 /\ A e. ZZ ) -> ( ( A gcd B ) || A <-> ( A / ( A gcd B ) ) e. ZZ ) )
32 30 15 1 31 syl3anc 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( A gcd B ) || A <-> ( A / ( A gcd B ) ) e. ZZ ) )
33 27 32 mpbid 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A / ( A gcd B ) ) e. ZZ )
34 11 simprd 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A gcd B ) || B )
35 simpr 
 |-  ( ( A e. ZZ /\ B e. NN ) -> B e. NN )
36 nndivdvds 
 |-  ( ( B e. NN /\ ( A gcd B ) e. NN ) -> ( ( A gcd B ) || B <-> ( B / ( A gcd B ) ) e. NN ) )
37 35 9 36 syl2anc 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( A gcd B ) || B <-> ( B / ( A gcd B ) ) e. NN ) )
38 34 37 mpbid 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( B / ( A gcd B ) ) e. NN )
39 qnumdenbi 
 |-  ( ( ( A / B ) e. QQ /\ ( A / ( A gcd B ) ) e. ZZ /\ ( B / ( A gcd B ) ) e. NN ) -> ( ( ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 /\ ( A / B ) = ( ( A / ( A gcd B ) ) / ( B / ( A gcd B ) ) ) ) <-> ( ( numer ` ( A / B ) ) = ( A / ( A gcd B ) ) /\ ( denom ` ( A / B ) ) = ( B / ( A gcd B ) ) ) ) )
40 26 33 38 39 syl3anc 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 /\ ( A / B ) = ( ( A / ( A gcd B ) ) / ( B / ( A gcd B ) ) ) ) <-> ( ( numer ` ( A / B ) ) = ( A / ( A gcd B ) ) /\ ( denom ` ( A / B ) ) = ( B / ( A gcd B ) ) ) ) )
41 17 25 40 mpbi2and 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( numer ` ( A / B ) ) = ( A / ( A gcd B ) ) /\ ( denom ` ( A / B ) ) = ( B / ( A gcd B ) ) ) )