Metamath Proof Explorer

Theorem divnumden2

Description: Calculate the reduced form of a quotient using gcd . This version extends divnumden for the negative integers. (Contributed by Thierry Arnoux, 25-Oct-2017)

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

Proof

Step Hyp Ref Expression
1 zssq 
 |-  ZZ C_ QQ
2 simp1 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> A e. ZZ )
3 1 2 sselid 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> A e. QQ )
4 simp2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> B e. ZZ )
5 1 4 sselid 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> B e. QQ )
6 nnne0 
 |-  ( -u B e. NN -> -u B =/= 0 )
7 6 3ad2ant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> -u B =/= 0 )
8 neg0 
 |-  -u 0 = 0
9 8 neeq2i 
 |-  ( -u B =/= -u 0 <-> -u B =/= 0 )
10 7 9 sylibr 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> -u B =/= -u 0 )
11 10 neneqd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> -. -u B = -u 0 )
12 4 zcnd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> B e. CC )
13 0cnd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> 0 e. CC )
14 12 13 neg11ad 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( -u B = -u 0 <-> B = 0 ) )
15 11 14 mtbid 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> -. B = 0 )
16 15 neqned 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> B =/= 0 )
17 qdivcl 
 |-  ( ( A e. QQ /\ B e. QQ /\ B =/= 0 ) -> ( A / B ) e. QQ )
18 3 5 16 17 syl3anc 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( A / B ) e. QQ )
19 qnumcl 
 |-  ( ( A / B ) e. QQ -> ( numer ` ( A / B ) ) e. ZZ )
20 18 19 syl 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( numer ` ( A / B ) ) e. ZZ )
21 20 zcnd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( numer ` ( A / B ) ) e. CC )
22 simpl 
 |-  ( ( A e. ZZ /\ -u B e. NN ) -> A e. ZZ )
23 22 zcnd 
 |-  ( ( A e. ZZ /\ -u B e. NN ) -> A e. CC )
24 23 3adant2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> A e. CC )
25 2 4 gcdcld 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( A gcd B ) e. NN0 )
26 25 nn0cnd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( A gcd B ) e. CC )
27 26 negcld 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> -u ( A gcd B ) e. CC )
28 15 intnand 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> -. ( A = 0 /\ B = 0 ) )
29 gcdeq0 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) = 0 <-> ( A = 0 /\ B = 0 ) ) )
30 29 necon3abid 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) =/= 0 <-> -. ( A = 0 /\ B = 0 ) ) )
31 30 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( ( A gcd B ) =/= 0 <-> -. ( A = 0 /\ B = 0 ) ) )
32 28 31 mpbird 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( A gcd B ) =/= 0 )
33 26 32 negne0d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> -u ( A gcd B ) =/= 0 )
34 24 27 33 divcld 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( A / -u ( A gcd B ) ) e. CC )
35 24 12 16 divneg2d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> -u ( A / B ) = ( A / -u B ) )
36 35 fveq2d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( numer ` -u ( A / B ) ) = ( numer ` ( A / -u B ) ) )
37 numdenneg 
 |-  ( ( A / B ) e. QQ -> ( ( numer ` -u ( A / B ) ) = -u ( numer ` ( A / B ) ) /\ ( denom ` -u ( A / B ) ) = ( denom ` ( A / B ) ) ) )
38 37 simpld 
 |-  ( ( A / B ) e. QQ -> ( numer ` -u ( A / B ) ) = -u ( numer ` ( A / B ) ) )
39 18 38 syl 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( numer ` -u ( A / B ) ) = -u ( numer ` ( A / B ) ) )
40 gcdneg 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd -u B ) = ( A gcd B ) )
41 40 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( A gcd -u B ) = ( A gcd B ) )
42 41 oveq2d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( A / ( A gcd -u B ) ) = ( A / ( A gcd B ) ) )
43 divnumden 
 |-  ( ( A e. ZZ /\ -u B e. NN ) -> ( ( numer ` ( A / -u B ) ) = ( A / ( A gcd -u B ) ) /\ ( denom ` ( A / -u B ) ) = ( -u B / ( A gcd -u B ) ) ) )
44 43 simpld 
 |-  ( ( A e. ZZ /\ -u B e. NN ) -> ( numer ` ( A / -u B ) ) = ( A / ( A gcd -u B ) ) )
45 44 3adant2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( numer ` ( A / -u B ) ) = ( A / ( A gcd -u B ) ) )
46 24 27 33 divnegd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> -u ( A / -u ( A gcd B ) ) = ( -u A / -u ( A gcd B ) ) )
47 24 26 32 div2negd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( -u A / -u ( A gcd B ) ) = ( A / ( A gcd B ) ) )
48 46 47 eqtrd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> -u ( A / -u ( A gcd B ) ) = ( A / ( A gcd B ) ) )
49 42 45 48 3eqtr4d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( numer ` ( A / -u B ) ) = -u ( A / -u ( A gcd B ) ) )
50 36 39 49 3eqtr3d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> -u ( numer ` ( A / B ) ) = -u ( A / -u ( A gcd B ) ) )
51 21 34 50 neg11d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( numer ` ( A / B ) ) = ( A / -u ( A gcd B ) ) )
52 24 26 32 divneg2d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> -u ( A / ( A gcd B ) ) = ( A / -u ( A gcd B ) ) )
53 51 52 eqtr4d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( numer ` ( A / B ) ) = -u ( A / ( A gcd B ) ) )
54 35 fveq2d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( denom ` -u ( A / B ) ) = ( denom ` ( A / -u B ) ) )
55 37 simprd 
 |-  ( ( A / B ) e. QQ -> ( denom ` -u ( A / B ) ) = ( denom ` ( A / B ) ) )
56 18 55 syl 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( denom ` -u ( A / B ) ) = ( denom ` ( A / B ) ) )
57 41 oveq2d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( -u B / ( A gcd -u B ) ) = ( -u B / ( A gcd B ) ) )
58 43 simprd 
 |-  ( ( A e. ZZ /\ -u B e. NN ) -> ( denom ` ( A / -u B ) ) = ( -u B / ( A gcd -u B ) ) )
59 58 3adant2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( denom ` ( A / -u B ) ) = ( -u B / ( A gcd -u B ) ) )
60 12 26 32 divneg2d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> -u ( B / ( A gcd B ) ) = ( B / -u ( A gcd B ) ) )
61 12 26 32 divnegd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> -u ( B / ( A gcd B ) ) = ( -u B / ( A gcd B ) ) )
62 60 61 eqtr3d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( B / -u ( A gcd B ) ) = ( -u B / ( A gcd B ) ) )
63 57 59 62 3eqtr4d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( denom ` ( A / -u B ) ) = ( B / -u ( A gcd B ) ) )
64 54 56 63 3eqtr3d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( denom ` ( A / B ) ) = ( B / -u ( A gcd B ) ) )
65 64 60 eqtr4d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( denom ` ( A / B ) ) = -u ( B / ( A gcd B ) ) )
66 53 65 jca 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ -u B e. NN ) -> ( ( numer ` ( A / B ) ) = -u ( A / ( A gcd B ) ) /\ ( denom ` ( A / B ) ) = -u ( B / ( A gcd B ) ) ) )