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 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ - 𝐵 ∈ ℕ ) → ( ( numer ‘ ( 𝐴 / 𝐵 ) ) = - ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∧ ( denom ‘ ( 𝐴 / 𝐵 ) ) = - ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) )

Proof

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