Proof of Theorem divnumden2
| Step | Hyp | Ref
| Expression |
| 1 | | zssq 12998 |
. . . . . . . 8
⊢ ℤ
⊆ ℚ |
| 2 | | simp1 1137 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → 𝐴 ∈
ℤ) |
| 3 | 1, 2 | sselid 3981 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → 𝐴 ∈
ℚ) |
| 4 | | simp2 1138 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → 𝐵 ∈
ℤ) |
| 5 | 1, 4 | sselid 3981 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → 𝐵 ∈
ℚ) |
| 6 | | nnne0 12300 |
. . . . . . . . . . . 12
⊢ (-𝐵 ∈ ℕ → -𝐵 ≠ 0) |
| 7 | 6 | 3ad2ant3 1136 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → -𝐵 ≠ 0) |
| 8 | | neg0 11555 |
. . . . . . . . . . . 12
⊢ -0 =
0 |
| 9 | 8 | neeq2i 3006 |
. . . . . . . . . . 11
⊢ (-𝐵 ≠ -0 ↔ -𝐵 ≠ 0) |
| 10 | 7, 9 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → -𝐵 ≠ -0) |
| 11 | 10 | neneqd 2945 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → ¬
-𝐵 = -0) |
| 12 | 4 | zcnd 12723 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → 𝐵 ∈
ℂ) |
| 13 | | 0cnd 11254 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → 0 ∈
ℂ) |
| 14 | 12, 13 | neg11ad 11616 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → (-𝐵 = -0 ↔ 𝐵 = 0)) |
| 15 | 11, 14 | mtbid 324 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → ¬
𝐵 = 0) |
| 16 | 15 | neqned 2947 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → 𝐵 ≠ 0) |
| 17 | | qdivcl 13012 |
. . . . . . 7
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℚ) |
| 18 | 3, 5, 16, 17 | syl3anc 1373 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ) |
| 19 | | qnumcl 16777 |
. . . . . 6
⊢ ((𝐴 / 𝐵) ∈ ℚ → (numer‘(𝐴 / 𝐵)) ∈ ℤ) |
| 20 | 18, 19 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) →
(numer‘(𝐴 / 𝐵)) ∈
ℤ) |
| 21 | 20 | zcnd 12723 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) →
(numer‘(𝐴 / 𝐵)) ∈
ℂ) |
| 22 | | simpl 482 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ -𝐵 ∈ ℕ) → 𝐴 ∈
ℤ) |
| 23 | 22 | zcnd 12723 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ -𝐵 ∈ ℕ) → 𝐴 ∈
ℂ) |
| 24 | 23 | 3adant2 1132 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → 𝐴 ∈
ℂ) |
| 25 | 2, 4 | gcdcld 16545 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∈
ℕ0) |
| 26 | 25 | nn0cnd 12589 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℂ) |
| 27 | 26 | negcld 11607 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → -(𝐴 gcd 𝐵) ∈ ℂ) |
| 28 | 15 | intnand 488 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → ¬
(𝐴 = 0 ∧ 𝐵 = 0)) |
| 29 | | gcdeq0 16554 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0))) |
| 30 | 29 | necon3abid 2977 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ≠ 0 ↔ ¬ (𝐴 = 0 ∧ 𝐵 = 0))) |
| 31 | 30 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) ≠ 0 ↔ ¬ (𝐴 = 0 ∧ 𝐵 = 0))) |
| 32 | 28, 31 | mpbird 257 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ≠ 0) |
| 33 | 26, 32 | negne0d 11618 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → -(𝐴 gcd 𝐵) ≠ 0) |
| 34 | 24, 27, 33 | divcld 12043 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → (𝐴 / -(𝐴 gcd 𝐵)) ∈ ℂ) |
| 35 | 24, 12, 16 | divneg2d 12057 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → -(𝐴 / 𝐵) = (𝐴 / -𝐵)) |
| 36 | 35 | fveq2d 6910 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) →
(numer‘-(𝐴 / 𝐵)) = (numer‘(𝐴 / -𝐵))) |
| 37 | | numdenneg 32816 |
. . . . . . 7
⊢ ((𝐴 / 𝐵) ∈ ℚ →
((numer‘-(𝐴 / 𝐵)) = -(numer‘(𝐴 / 𝐵)) ∧ (denom‘-(𝐴 / 𝐵)) = (denom‘(𝐴 / 𝐵)))) |
| 38 | 37 | simpld 494 |
. . . . . 6
⊢ ((𝐴 / 𝐵) ∈ ℚ → (numer‘-(𝐴 / 𝐵)) = -(numer‘(𝐴 / 𝐵))) |
| 39 | 18, 38 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) →
(numer‘-(𝐴 / 𝐵)) = -(numer‘(𝐴 / 𝐵))) |
| 40 | | gcdneg 16559 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd -𝐵) = (𝐴 gcd 𝐵)) |
| 41 | 40 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → (𝐴 gcd -𝐵) = (𝐴 gcd 𝐵)) |
| 42 | 41 | oveq2d 7447 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → (𝐴 / (𝐴 gcd -𝐵)) = (𝐴 / (𝐴 gcd 𝐵))) |
| 43 | | divnumden 16785 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ -𝐵 ∈ ℕ) →
((numer‘(𝐴 / -𝐵)) = (𝐴 / (𝐴 gcd -𝐵)) ∧ (denom‘(𝐴 / -𝐵)) = (-𝐵 / (𝐴 gcd -𝐵)))) |
| 44 | 43 | simpld 494 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ -𝐵 ∈ ℕ) →
(numer‘(𝐴 / -𝐵)) = (𝐴 / (𝐴 gcd -𝐵))) |
| 45 | 44 | 3adant2 1132 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) →
(numer‘(𝐴 / -𝐵)) = (𝐴 / (𝐴 gcd -𝐵))) |
| 46 | 24, 27, 33 | divnegd 12056 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → -(𝐴 / -(𝐴 gcd 𝐵)) = (-𝐴 / -(𝐴 gcd 𝐵))) |
| 47 | 24, 26, 32 | div2negd 12058 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → (-𝐴 / -(𝐴 gcd 𝐵)) = (𝐴 / (𝐴 gcd 𝐵))) |
| 48 | 46, 47 | eqtrd 2777 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → -(𝐴 / -(𝐴 gcd 𝐵)) = (𝐴 / (𝐴 gcd 𝐵))) |
| 49 | 42, 45, 48 | 3eqtr4d 2787 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) →
(numer‘(𝐴 / -𝐵)) = -(𝐴 / -(𝐴 gcd 𝐵))) |
| 50 | 36, 39, 49 | 3eqtr3d 2785 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) →
-(numer‘(𝐴 / 𝐵)) = -(𝐴 / -(𝐴 gcd 𝐵))) |
| 51 | 21, 34, 50 | neg11d 11632 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) →
(numer‘(𝐴 / 𝐵)) = (𝐴 / -(𝐴 gcd 𝐵))) |
| 52 | 24, 26, 32 | divneg2d 12057 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → -(𝐴 / (𝐴 gcd 𝐵)) = (𝐴 / -(𝐴 gcd 𝐵))) |
| 53 | 51, 52 | eqtr4d 2780 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) →
(numer‘(𝐴 / 𝐵)) = -(𝐴 / (𝐴 gcd 𝐵))) |
| 54 | 35 | fveq2d 6910 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) →
(denom‘-(𝐴 / 𝐵)) = (denom‘(𝐴 / -𝐵))) |
| 55 | 37 | simprd 495 |
. . . . 5
⊢ ((𝐴 / 𝐵) ∈ ℚ → (denom‘-(𝐴 / 𝐵)) = (denom‘(𝐴 / 𝐵))) |
| 56 | 18, 55 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) →
(denom‘-(𝐴 / 𝐵)) = (denom‘(𝐴 / 𝐵))) |
| 57 | 41 | oveq2d 7447 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → (-𝐵 / (𝐴 gcd -𝐵)) = (-𝐵 / (𝐴 gcd 𝐵))) |
| 58 | 43 | simprd 495 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ -𝐵 ∈ ℕ) →
(denom‘(𝐴 / -𝐵)) = (-𝐵 / (𝐴 gcd -𝐵))) |
| 59 | 58 | 3adant2 1132 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) →
(denom‘(𝐴 / -𝐵)) = (-𝐵 / (𝐴 gcd -𝐵))) |
| 60 | 12, 26, 32 | divneg2d 12057 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → -(𝐵 / (𝐴 gcd 𝐵)) = (𝐵 / -(𝐴 gcd 𝐵))) |
| 61 | 12, 26, 32 | divnegd 12056 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → -(𝐵 / (𝐴 gcd 𝐵)) = (-𝐵 / (𝐴 gcd 𝐵))) |
| 62 | 60, 61 | eqtr3d 2779 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → (𝐵 / -(𝐴 gcd 𝐵)) = (-𝐵 / (𝐴 gcd 𝐵))) |
| 63 | 57, 59, 62 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) →
(denom‘(𝐴 / -𝐵)) = (𝐵 / -(𝐴 gcd 𝐵))) |
| 64 | 54, 56, 63 | 3eqtr3d 2785 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) →
(denom‘(𝐴 / 𝐵)) = (𝐵 / -(𝐴 gcd 𝐵))) |
| 65 | 64, 60 | eqtr4d 2780 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) →
(denom‘(𝐴 / 𝐵)) = -(𝐵 / (𝐴 gcd 𝐵))) |
| 66 | 53, 65 | jca 511 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) →
((numer‘(𝐴 / 𝐵)) = -(𝐴 / (𝐴 gcd 𝐵)) ∧ (denom‘(𝐴 / 𝐵)) = -(𝐵 / (𝐴 gcd 𝐵)))) |