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 ⁡ A B = − A A gcd B ∧ denom ⁡ A B = − B A gcd B

Proof

Step Hyp Ref Expression
1 zssq ⊢ ℤ ⊆ ℚ
2 simp1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → A ∈ ℤ
3 1 2 sseldi ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → A ∈ ℚ
4 simp2 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → B ∈ ℤ
5 1 4 sseldi ⊢ 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 → A B ∈ ℚ
18 3 5 16 17 syl3anc ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → A B ∈ ℚ
19 qnumcl ⊢ A B ∈ ℚ → numer ⁡ A B ∈ ℤ
20 18 19 syl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → numer ⁡ A B ∈ ℤ
21 20 zcnd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → numer ⁡ A B ∈ ℂ
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 ∈ ℕ → A gcd B ∈ ℕ 0
26 25 nn0cnd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → A gcd B ∈ ℂ
27 26 negcld ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → − A gcd B ∈ ℂ
28 15 intnand ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → ¬ A = 0 ∧ B = 0
29 gcdeq0 ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B = 0 ↔ A = 0 ∧ B = 0
30 29 necon3abid ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B ≠ 0 ↔ ¬ A = 0 ∧ B = 0
31 30 3adant3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → A gcd B ≠ 0 ↔ ¬ A = 0 ∧ B = 0
32 28 31 mpbird ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → A gcd B ≠ 0
33 26 32 negne0d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → − A gcd B ≠ 0
34 24 27 33 divcld ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → A − A gcd B ∈ ℂ
35 24 12 16 divneg2d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → − A B = A − B
36 35 fveq2d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → numer ⁡ − A B = numer ⁡ A − B
37 numdenneg ⊢ A B ∈ ℚ → numer ⁡ − A B = − numer ⁡ A B ∧ denom ⁡ − A B = denom ⁡ A B
38 37 simpld ⊢ A B ∈ ℚ → numer ⁡ − A B = − numer ⁡ A B
39 18 38 syl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → numer ⁡ − A B = − numer ⁡ A B
40 gcdneg ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd − B = A gcd B
41 40 3adant3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → A gcd − B = A gcd B
42 41 oveq2d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → A A gcd − B = A A gcd B
43 divnumden ⊢ A ∈ ℤ ∧ − B ∈ ℕ → numer ⁡ A − B = A A gcd − B ∧ denom ⁡ A − B = − B A gcd − B
44 43 simpld ⊢ A ∈ ℤ ∧ − B ∈ ℕ → numer ⁡ A − B = A A gcd − B
45 44 3adant2 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → numer ⁡ A − B = A A gcd − B
46 24 27 33 divnegd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → − A − A gcd B = − A − A gcd B
47 24 26 32 div2negd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → − A − A gcd B = A A gcd B
48 46 47 eqtrd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → − A − A gcd B = A A gcd B
49 42 45 48 3eqtr4d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → numer ⁡ A − B = − A − A gcd B
50 36 39 49 3eqtr3d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → − numer ⁡ A B = − A − A gcd B
51 21 34 50 neg11d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → numer ⁡ A B = A − A gcd B
52 24 26 32 divneg2d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → − A A gcd B = A − A gcd B
53 51 52 eqtr4d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → numer ⁡ A B = − A A gcd B
54 35 fveq2d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → denom ⁡ − A B = denom ⁡ A − B
55 37 simprd ⊢ A B ∈ ℚ → denom ⁡ − A B = denom ⁡ A B
56 18 55 syl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → denom ⁡ − A B = denom ⁡ A B
57 41 oveq2d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → − B A gcd − B = − B A gcd B
58 43 simprd ⊢ A ∈ ℤ ∧ − B ∈ ℕ → denom ⁡ A − B = − B A gcd − B
59 58 3adant2 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → denom ⁡ A − B = − B A gcd − B
60 12 26 32 divneg2d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → − B A gcd B = B − A gcd B
61 12 26 32 divnegd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → − B A gcd B = − B A gcd B
62 60 61 eqtr3d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → B − A gcd B = − B A gcd B
63 57 59 62 3eqtr4d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → denom ⁡ A − B = B − A gcd B
64 54 56 63 3eqtr3d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → denom ⁡ A B = B − A gcd B
65 64 60 eqtr4d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → denom ⁡ A B = − B A gcd B
66 53 65 jca ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ − B ∈ ℕ → numer ⁡ A B = − A A gcd B ∧ denom ⁡ A B = − B A gcd B