Proof of Theorem div2neg
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | negcl 11508 | . . . . 5
⊢ (𝐵 ∈ ℂ → -𝐵 ∈
ℂ) | 
| 2 | 1 | 3ad2ant2 1135 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → -𝐵 ∈
ℂ) | 
| 3 |  | simp1 1137 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → 𝐴 ∈
ℂ) | 
| 4 |  | simp2 1138 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → 𝐵 ∈
ℂ) | 
| 5 |  | simp3 1139 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → 𝐵 ≠ 0) | 
| 6 |  | div12 11944 | . . . 4
⊢ ((-𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (-𝐵 · (𝐴 / 𝐵)) = (𝐴 · (-𝐵 / 𝐵))) | 
| 7 | 2, 3, 4, 5, 6 | syl112anc 1376 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (-𝐵 · (𝐴 / 𝐵)) = (𝐴 · (-𝐵 / 𝐵))) | 
| 8 |  | divneg 11959 | . . . . . . 7
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → -(𝐵 / 𝐵) = (-𝐵 / 𝐵)) | 
| 9 | 4, 8 | syld3an1 1412 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → -(𝐵 / 𝐵) = (-𝐵 / 𝐵)) | 
| 10 |  | divid 11953 | . . . . . . . 8
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐵 / 𝐵) = 1) | 
| 11 | 10 | 3adant1 1131 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐵 / 𝐵) = 1) | 
| 12 | 11 | negeqd 11502 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → -(𝐵 / 𝐵) = -1) | 
| 13 | 9, 12 | eqtr3d 2779 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (-𝐵 / 𝐵) = -1) | 
| 14 | 13 | oveq2d 7447 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 · (-𝐵 / 𝐵)) = (𝐴 · -1)) | 
| 15 |  | ax-1cn 11213 | . . . . . . . 8
⊢ 1 ∈
ℂ | 
| 16 | 15 | negcli 11577 | . . . . . . 7
⊢ -1 ∈
ℂ | 
| 17 |  | mulcom 11241 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ -1 ∈
ℂ) → (𝐴 ·
-1) = (-1 · 𝐴)) | 
| 18 | 16, 17 | mpan2 691 | . . . . . 6
⊢ (𝐴 ∈ ℂ → (𝐴 · -1) = (-1 ·
𝐴)) | 
| 19 |  | mulm1 11704 | . . . . . 6
⊢ (𝐴 ∈ ℂ → (-1
· 𝐴) = -𝐴) | 
| 20 | 18, 19 | eqtrd 2777 | . . . . 5
⊢ (𝐴 ∈ ℂ → (𝐴 · -1) = -𝐴) | 
| 21 | 20 | 3ad2ant1 1134 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 · -1) = -𝐴) | 
| 22 | 14, 21 | eqtrd 2777 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 · (-𝐵 / 𝐵)) = -𝐴) | 
| 23 | 7, 22 | eqtrd 2777 | . 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (-𝐵 · (𝐴 / 𝐵)) = -𝐴) | 
| 24 |  | negcl 11508 | . . . 4
⊢ (𝐴 ∈ ℂ → -𝐴 ∈
ℂ) | 
| 25 | 24 | 3ad2ant1 1134 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → -𝐴 ∈
ℂ) | 
| 26 |  | divcl 11928 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℂ) | 
| 27 |  | negeq0 11563 | . . . . . 6
⊢ (𝐵 ∈ ℂ → (𝐵 = 0 ↔ -𝐵 = 0)) | 
| 28 | 27 | necon3bid 2985 | . . . . 5
⊢ (𝐵 ∈ ℂ → (𝐵 ≠ 0 ↔ -𝐵 ≠ 0)) | 
| 29 | 28 | biimpa 476 | . . . 4
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → -𝐵 ≠ 0) | 
| 30 | 29 | 3adant1 1131 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → -𝐵 ≠ 0) | 
| 31 |  | divmul 11925 | . . 3
⊢ ((-𝐴 ∈ ℂ ∧ (𝐴 / 𝐵) ∈ ℂ ∧ (-𝐵 ∈ ℂ ∧ -𝐵 ≠ 0)) → ((-𝐴 / -𝐵) = (𝐴 / 𝐵) ↔ (-𝐵 · (𝐴 / 𝐵)) = -𝐴)) | 
| 32 | 25, 26, 2, 30, 31 | syl112anc 1376 | . 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((-𝐴 / -𝐵) = (𝐴 / 𝐵) ↔ (-𝐵 · (𝐴 / 𝐵)) = -𝐴)) | 
| 33 | 23, 32 | mpbird 257 | 1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (-𝐴 / -𝐵) = (𝐴 / 𝐵)) |