Proof of Theorem sigarms
Step | Hyp | Ref
| Expression |
1 | | simp1 1116 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → 𝐴 ∈
ℂ) |
2 | | simp2 1117 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → 𝐵 ∈
ℂ) |
3 | | simp3 1118 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → 𝐶 ∈
ℂ) |
4 | 2, 3 | subcld 10798 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐵 − 𝐶) ∈ ℂ) |
5 | | sigar |
. . . 4
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦
(ℑ‘((∗‘𝑥) · 𝑦))) |
6 | 5 | sigarac 42546 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 − 𝐶) ∈ ℂ) → (𝐴𝐺(𝐵 − 𝐶)) = -((𝐵 − 𝐶)𝐺𝐴)) |
7 | 1, 4, 6 | syl2anc 576 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴𝐺(𝐵 − 𝐶)) = -((𝐵 − 𝐶)𝐺𝐴)) |
8 | 5 | sigarmf 42548 |
. . . . 5
⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐵 − 𝐶)𝐺𝐴) = ((𝐵𝐺𝐴) − (𝐶𝐺𝐴))) |
9 | 8 | negeqd 10680 |
. . . 4
⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → -((𝐵 − 𝐶)𝐺𝐴) = -((𝐵𝐺𝐴) − (𝐶𝐺𝐴))) |
10 | 9 | 3com12 1103 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → -((𝐵 − 𝐶)𝐺𝐴) = -((𝐵𝐺𝐴) − (𝐶𝐺𝐴))) |
11 | | 3simpa 1128 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 ∈ ℂ ∧ 𝐵 ∈
ℂ)) |
12 | 11 | ancomd 454 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐵 ∈ ℂ ∧ 𝐴 ∈
ℂ)) |
13 | 5 | sigarim 42545 |
. . . . . 6
⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵𝐺𝐴) ∈ ℝ) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐵𝐺𝐴) ∈ ℝ) |
15 | 14 | recnd 10468 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐵𝐺𝐴) ∈ ℂ) |
16 | | 3simpb 1129 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 ∈ ℂ ∧ 𝐶 ∈
ℂ)) |
17 | 16 | ancomd 454 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐶 ∈ ℂ ∧ 𝐴 ∈
ℂ)) |
18 | 5 | sigarim 42545 |
. . . . . 6
⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐶𝐺𝐴) ∈ ℝ) |
19 | 17, 18 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐶𝐺𝐴) ∈ ℝ) |
20 | 19 | recnd 10468 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐶𝐺𝐴) ∈ ℂ) |
21 | | negsubdi 10743 |
. . . . 5
⊢ (((𝐵𝐺𝐴) ∈ ℂ ∧ (𝐶𝐺𝐴) ∈ ℂ) → -((𝐵𝐺𝐴) − (𝐶𝐺𝐴)) = (-(𝐵𝐺𝐴) + (𝐶𝐺𝐴))) |
22 | | simpl 475 |
. . . . . . 7
⊢ (((𝐵𝐺𝐴) ∈ ℂ ∧ (𝐶𝐺𝐴) ∈ ℂ) → (𝐵𝐺𝐴) ∈ ℂ) |
23 | 22 | negcld 10785 |
. . . . . 6
⊢ (((𝐵𝐺𝐴) ∈ ℂ ∧ (𝐶𝐺𝐴) ∈ ℂ) → -(𝐵𝐺𝐴) ∈ ℂ) |
24 | | simpr 477 |
. . . . . 6
⊢ (((𝐵𝐺𝐴) ∈ ℂ ∧ (𝐶𝐺𝐴) ∈ ℂ) → (𝐶𝐺𝐴) ∈ ℂ) |
25 | 23, 24 | subnegd 10805 |
. . . . 5
⊢ (((𝐵𝐺𝐴) ∈ ℂ ∧ (𝐶𝐺𝐴) ∈ ℂ) → (-(𝐵𝐺𝐴) − -(𝐶𝐺𝐴)) = (-(𝐵𝐺𝐴) + (𝐶𝐺𝐴))) |
26 | 21, 25 | eqtr4d 2817 |
. . . 4
⊢ (((𝐵𝐺𝐴) ∈ ℂ ∧ (𝐶𝐺𝐴) ∈ ℂ) → -((𝐵𝐺𝐴) − (𝐶𝐺𝐴)) = (-(𝐵𝐺𝐴) − -(𝐶𝐺𝐴))) |
27 | 15, 20, 26 | syl2anc 576 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → -((𝐵𝐺𝐴) − (𝐶𝐺𝐴)) = (-(𝐵𝐺𝐴) − -(𝐶𝐺𝐴))) |
28 | 10, 27 | eqtrd 2814 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → -((𝐵 − 𝐶)𝐺𝐴) = (-(𝐵𝐺𝐴) − -(𝐶𝐺𝐴))) |
29 | 5 | sigarac 42546 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐺𝐵) = -(𝐵𝐺𝐴)) |
30 | 1, 2, 29 | syl2anc 576 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴𝐺𝐵) = -(𝐵𝐺𝐴)) |
31 | 30 | eqcomd 2784 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → -(𝐵𝐺𝐴) = (𝐴𝐺𝐵)) |
32 | 5 | sigarac 42546 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴𝐺𝐶) = -(𝐶𝐺𝐴)) |
33 | 1, 3, 32 | syl2anc 576 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴𝐺𝐶) = -(𝐶𝐺𝐴)) |
34 | 33 | eqcomd 2784 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → -(𝐶𝐺𝐴) = (𝐴𝐺𝐶)) |
35 | 31, 34 | oveq12d 6994 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (-(𝐵𝐺𝐴) − -(𝐶𝐺𝐴)) = ((𝐴𝐺𝐵) − (𝐴𝐺𝐶))) |
36 | 7, 28, 35 | 3eqtrd 2818 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴𝐺(𝐵 − 𝐶)) = ((𝐴𝐺𝐵) − (𝐴𝐺𝐶))) |