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∈ℤ∧B∈ℤ∧−B∈ℕ→numer⁡AB=−AAgcdB∧denom⁡AB=−BAgcdB

Proof

Step Hyp Ref Expression
1 zssq ⊢ℤ⊆ℚ
2 simp1 ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→A∈ℤ
3 1 2 sselid ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→A∈ℚ
4 simp2 ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→B∈ℤ
5 1 4 sselid ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→B∈ℚ
6 nnne0 ⊢−B∈ℕ→−B≠0
7 6 3ad2ant3 ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→−B≠0
8 neg0 ⊢−0=0
9 8 neeq2i ⊢−B≠−0↔−B≠0
10 7 9 sylibr ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→−B≠−0
11 10 neneqd ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→¬−B=−0
12 4 zcnd ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→B∈ℂ
13 0cnd ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→0∈ℂ
14 12 13 neg11ad ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→−B=−0↔B=0
15 11 14 mtbid ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→¬B=0
16 15 neqned ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→B≠0
17 qdivcl ⊢A∈ℚ∧B∈ℚ∧B≠0→AB∈ℚ
18 3 5 16 17 syl3anc ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→AB∈ℚ
19 qnumcl ⊢AB∈ℚ→numer⁡AB∈ℤ
20 18 19 syl ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→numer⁡AB∈ℤ
21 20 zcnd ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→numer⁡AB∈ℂ
22 simpl ⊢A∈ℤ∧−B∈ℕ→A∈ℤ
23 22 zcnd ⊢A∈ℤ∧−B∈ℕ→A∈ℂ
24 23 3adant2 ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→A∈ℂ
25 2 4 gcdcld ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→AgcdB∈ℕ0
26 25 nn0cnd ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→AgcdB∈ℂ
27 26 negcld ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→−AgcdB∈ℂ
28 15 intnand ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→¬A=0∧B=0
29 gcdeq0 ⊢A∈ℤ∧B∈ℤ→AgcdB=0↔A=0∧B=0
30 29 necon3abid ⊢A∈ℤ∧B∈ℤ→AgcdB≠0↔¬A=0∧B=0
31 30 3adant3 ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→AgcdB≠0↔¬A=0∧B=0
32 28 31 mpbird ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→AgcdB≠0
33 26 32 negne0d ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→−AgcdB≠0
34 24 27 33 divcld ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→A−AgcdB∈ℂ
35 24 12 16 divneg2d ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→−AB=A−B
36 35 fveq2d ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→numer⁡−AB=numer⁡A−B
37 numdenneg ⊢AB∈ℚ→numer⁡−AB=−numer⁡AB∧denom⁡−AB=denom⁡AB
38 37 simpld ⊢AB∈ℚ→numer⁡−AB=−numer⁡AB
39 18 38 syl ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→numer⁡−AB=−numer⁡AB
40 gcdneg ⊢A∈ℤ∧B∈ℤ→Agcd−B=AgcdB
41 40 3adant3 ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→Agcd−B=AgcdB
42 41 oveq2d ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→AAgcd−B=AAgcdB
43 divnumden ⊢A∈ℤ∧−B∈ℕ→numer⁡A−B=AAgcd−B∧denom⁡A−B=−BAgcd−B
44 43 simpld ⊢A∈ℤ∧−B∈ℕ→numer⁡A−B=AAgcd−B
45 44 3adant2 ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→numer⁡A−B=AAgcd−B
46 24 27 33 divnegd ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→−A−AgcdB=−A−AgcdB
47 24 26 32 div2negd ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→−A−AgcdB=AAgcdB
48 46 47 eqtrd ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→−A−AgcdB=AAgcdB
49 42 45 48 3eqtr4d ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→numer⁡A−B=−A−AgcdB
50 36 39 49 3eqtr3d ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→−numer⁡AB=−A−AgcdB
51 21 34 50 neg11d ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→numer⁡AB=A−AgcdB
52 24 26 32 divneg2d ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→−AAgcdB=A−AgcdB
53 51 52 eqtr4d ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→numer⁡AB=−AAgcdB
54 35 fveq2d ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→denom⁡−AB=denom⁡A−B
55 37 simprd ⊢AB∈ℚ→denom⁡−AB=denom⁡AB
56 18 55 syl ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→denom⁡−AB=denom⁡AB
57 41 oveq2d ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→−BAgcd−B=−BAgcdB
58 43 simprd ⊢A∈ℤ∧−B∈ℕ→denom⁡A−B=−BAgcd−B
59 58 3adant2 ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→denom⁡A−B=−BAgcd−B
60 12 26 32 divneg2d ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→−BAgcdB=B−AgcdB
61 12 26 32 divnegd ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→−BAgcdB=−BAgcdB
62 60 61 eqtr3d ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→B−AgcdB=−BAgcdB
63 57 59 62 3eqtr4d ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→denom⁡A−B=B−AgcdB
64 54 56 63 3eqtr3d ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→denom⁡AB=B−AgcdB
65 64 60 eqtr4d ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→denom⁡AB=−BAgcdB
66 53 65 jca ⊢A∈ℤ∧B∈ℤ∧−B∈ℕ→numer⁡AB=−AAgcdB∧denom⁡AB=−BAgcdB