Proof of Theorem sadadd2lem2
Step | Hyp | Ref
| Expression |
1 | | 0cn 9911 |
. . . . . . . . 9
⊢ 0 ∈
ℂ |
2 | | ifcl 4080 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 0 ∈
ℂ) → if(𝜓, 𝐴, 0) ∈
ℂ) |
3 | 1, 2 | mpan2 703 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → if(𝜓, 𝐴, 0) ∈ ℂ) |
4 | 3 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if(𝜓, 𝐴, 0) ∈ ℂ) |
5 | | simpll 786 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → 𝐴 ∈ ℂ) |
6 | 4, 5, 5 | add12d 10141 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if(𝜓, 𝐴, 0) + (𝐴 + 𝐴)) = (𝐴 + (if(𝜓, 𝐴, 0) + 𝐴))) |
7 | 5, 4, 5 | addassd 9941 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → ((𝐴 + if(𝜓, 𝐴, 0)) + 𝐴) = (𝐴 + (if(𝜓, 𝐴, 0) + 𝐴))) |
8 | 6, 7 | eqtr4d 2647 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if(𝜓, 𝐴, 0) + (𝐴 + 𝐴)) = ((𝐴 + if(𝜓, 𝐴, 0)) + 𝐴)) |
9 | | pm5.501 355 |
. . . . . . . . 9
⊢ (𝜑 → (𝜓 ↔ (𝜑 ↔ 𝜓))) |
10 | 9 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (𝜓 ↔ (𝜑 ↔ 𝜓))) |
11 | 10 | bicomd 212 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → ((𝜑 ↔ 𝜓) ↔ 𝜓)) |
12 | 11 | ifbid 4058 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if((𝜑 ↔ 𝜓), 𝐴, 0) = if(𝜓, 𝐴, 0)) |
13 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → 𝜑) |
14 | 13 | orcd 406 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (𝜑 ∨ 𝜓)) |
15 | | iftrue 4042 |
. . . . . . . 8
⊢ ((𝜑 ∨ 𝜓) → if((𝜑 ∨ 𝜓), (2 · 𝐴), 0) = (2 · 𝐴)) |
16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if((𝜑 ∨ 𝜓), (2 · 𝐴), 0) = (2 · 𝐴)) |
17 | 5 | 2timesd 11152 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (2 · 𝐴) = (𝐴 + 𝐴)) |
18 | 16, 17 | eqtrd 2644 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if((𝜑 ∨ 𝜓), (2 · 𝐴), 0) = (𝐴 + 𝐴)) |
19 | 12, 18 | oveq12d 6567 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + (𝐴 + 𝐴))) |
20 | | iftrue 4042 |
. . . . . . . 8
⊢ (𝜑 → if(𝜑, 𝐴, 0) = 𝐴) |
21 | 20 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if(𝜑, 𝐴, 0) = 𝐴) |
22 | 21 | oveq1d 6564 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (𝐴 + if(𝜓, 𝐴, 0))) |
23 | 22 | oveq1d 6564 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴) = ((𝐴 + if(𝜓, 𝐴, 0)) + 𝐴)) |
24 | 8, 19, 23 | 3eqtr4d 2654 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴)) |
25 | | iffalse 4045 |
. . . . . . . . 9
⊢ (¬
𝜑 → if(𝜑, 𝐴, 0) = 0) |
26 | 25 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜑, 𝐴, 0) = 0) |
27 | 26 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (0 + if(𝜓, 𝐴, 0))) |
28 | 3 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜓, 𝐴, 0) ∈ ℂ) |
29 | 28 | addid2d 10116 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (0 + if(𝜓, 𝐴, 0)) = if(𝜓, 𝐴, 0)) |
30 | 27, 29 | eqtrd 2644 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = if(𝜓, 𝐴, 0)) |
31 | 30 | oveq1d 6564 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴) = (if(𝜓, 𝐴, 0) + 𝐴)) |
32 | | 2cnd 10970 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → 2 ∈
ℂ) |
33 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → 𝐴 ∈
ℂ) |
34 | 32, 33 | mulcld 9939 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (2
· 𝐴) ∈
ℂ) |
35 | 34 | addid2d 10116 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (0 + (2
· 𝐴)) = (2 ·
𝐴)) |
36 | | 2times 11022 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (2
· 𝐴) = (𝐴 + 𝐴)) |
37 | 35, 36 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (0 + (2
· 𝐴)) = (𝐴 + 𝐴)) |
38 | 37 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (0 + (2 · 𝐴)) = (𝐴 + 𝐴)) |
39 | | iftrue 4042 |
. . . . . . . . . 10
⊢ (𝜓 → if(𝜓, 0, 𝐴) = 0) |
40 | 39 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → if(𝜓, 0, 𝐴) = 0) |
41 | | iftrue 4042 |
. . . . . . . . . 10
⊢ (𝜓 → if(𝜓, (2 · 𝐴), 0) = (2 · 𝐴)) |
42 | 41 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → if(𝜓, (2 · 𝐴), 0) = (2 · 𝐴)) |
43 | 40, 42 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (0 + (2 · 𝐴))) |
44 | | iftrue 4042 |
. . . . . . . . . 10
⊢ (𝜓 → if(𝜓, 𝐴, 0) = 𝐴) |
45 | 44 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → if(𝜓, 𝐴, 0) = 𝐴) |
46 | 45 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 𝐴, 0) + 𝐴) = (𝐴 + 𝐴)) |
47 | 38, 43, 46 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴)) |
48 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → 𝐴 ∈ ℂ) |
49 | | 0cnd 9912 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → 0 ∈
ℂ) |
50 | 48, 49 | addcomd 10117 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → (𝐴 + 0) = (0 + 𝐴)) |
51 | | iffalse 4045 |
. . . . . . . . . 10
⊢ (¬
𝜓 → if(𝜓, 0, 𝐴) = 𝐴) |
52 | 51 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → if(𝜓, 0, 𝐴) = 𝐴) |
53 | | iffalse 4045 |
. . . . . . . . . 10
⊢ (¬
𝜓 → if(𝜓, (2 · 𝐴), 0) = 0) |
54 | 53 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → if(𝜓, (2 · 𝐴), 0) = 0) |
55 | 52, 54 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + 0)) |
56 | | iffalse 4045 |
. . . . . . . . . 10
⊢ (¬
𝜓 → if(𝜓, 𝐴, 0) = 0) |
57 | 56 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → if(𝜓, 𝐴, 0) = 0) |
58 | 57 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → (if(𝜓, 𝐴, 0) + 𝐴) = (0 + 𝐴)) |
59 | 50, 55, 58 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴)) |
60 | 47, 59 | pm2.61dan 828 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴)) |
61 | 60 | ad2antrr 758 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴)) |
62 | | ifnot 4083 |
. . . . . . 7
⊢ if(¬
𝜓, 𝐴, 0) = if(𝜓, 0, 𝐴) |
63 | | nbn2 359 |
. . . . . . . . 9
⊢ (¬
𝜑 → (¬ 𝜓 ↔ (𝜑 ↔ 𝜓))) |
64 | 63 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (¬ 𝜓 ↔ (𝜑 ↔ 𝜓))) |
65 | 64 | ifbid 4058 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(¬ 𝜓, 𝐴, 0) = if((𝜑 ↔ 𝜓), 𝐴, 0)) |
66 | 62, 65 | syl5eqr 2658 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜓, 0, 𝐴) = if((𝜑 ↔ 𝜓), 𝐴, 0)) |
67 | | biorf 419 |
. . . . . . . 8
⊢ (¬
𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓))) |
68 | 67 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (𝜓 ↔ (𝜑 ∨ 𝜓))) |
69 | 68 | ifbid 4058 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜓, (2 · 𝐴), 0) = if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)) |
70 | 66, 69 | oveq12d 6567 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0))) |
71 | 31, 61, 70 | 3eqtr2rd 2651 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴)) |
72 | 24, 71 | pm2.61dan 828 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴)) |
73 | | hadrot 1531 |
. . . . . . 7
⊢
(hadd(𝜒, 𝜑, 𝜓) ↔ hadd(𝜑, 𝜓, 𝜒)) |
74 | | had1 1533 |
. . . . . . 7
⊢ (𝜒 → (hadd(𝜒, 𝜑, 𝜓) ↔ (𝜑 ↔ 𝜓))) |
75 | 73, 74 | syl5bbr 273 |
. . . . . 6
⊢ (𝜒 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ↔ 𝜓))) |
76 | 75 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ↔ 𝜓))) |
77 | 76 | ifbid 4058 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) = if((𝜑 ↔ 𝜓), 𝐴, 0)) |
78 | | cad1 1546 |
. . . . . 6
⊢ (𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∨ 𝜓))) |
79 | 78 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∨ 𝜓))) |
80 | 79 | ifbid 4058 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0) = if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)) |
81 | 77, 80 | oveq12d 6567 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0))) |
82 | | iftrue 4042 |
. . . . 5
⊢ (𝜒 → if(𝜒, 𝐴, 0) = 𝐴) |
83 | 82 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → if(𝜒, 𝐴, 0) = 𝐴) |
84 | 83 | oveq2d 6565 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴)) |
85 | 72, 81, 84 | 3eqtr4d 2654 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0))) |
86 | 20 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → if(𝜑, 𝐴, 0) = 𝐴) |
87 | 86 | oveq1d 6564 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (𝐴 + if(𝜓, 𝐴, 0))) |
88 | 45 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (𝐴 + if(𝜓, 𝐴, 0)) = (𝐴 + 𝐴)) |
89 | 38, 43, 88 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0))) |
90 | 54, 57 | eqtr4d 2647 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → if(𝜓, (2 · 𝐴), 0) = if(𝜓, 𝐴, 0)) |
91 | 52, 90 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0))) |
92 | 89, 91 | pm2.61dan 828 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0))) |
93 | 92 | ad2antrr 758 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0))) |
94 | 9 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → (𝜓 ↔ (𝜑 ↔ 𝜓))) |
95 | 94 | notbid 307 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → (¬ 𝜓 ↔ ¬ (𝜑 ↔ 𝜓))) |
96 | | df-xor 1457 |
. . . . . . . . 9
⊢ ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓)) |
97 | 95, 96 | syl6bbr 277 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → (¬ 𝜓 ↔ (𝜑 ⊻ 𝜓))) |
98 | 97 | ifbid 4058 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → if(¬ 𝜓, 𝐴, 0) = if((𝜑 ⊻ 𝜓), 𝐴, 0)) |
99 | 62, 98 | syl5eqr 2658 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → if(𝜓, 0, 𝐴) = if((𝜑 ⊻ 𝜓), 𝐴, 0)) |
100 | | ibar 524 |
. . . . . . . 8
⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) |
101 | 100 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → (𝜓 ↔ (𝜑 ∧ 𝜓))) |
102 | 101 | ifbid 4058 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → if(𝜓, (2 · 𝐴), 0) = if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)) |
103 | 99, 102 | oveq12d 6567 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0))) |
104 | 87, 93, 103 | 3eqtr2rd 2651 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0))) |
105 | | simplll 794 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) ∧ 𝜓) → 𝐴 ∈ ℂ) |
106 | | 0cnd 9912 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) ∧ ¬ 𝜓) → 0 ∈ ℂ) |
107 | 105, 106 | ifclda 4070 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → if(𝜓, 𝐴, 0) ∈ ℂ) |
108 | | 0cnd 9912 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → 0 ∈
ℂ) |
109 | 107, 108 | addcomd 10117 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → (if(𝜓, 𝐴, 0) + 0) = (0 + if(𝜓, 𝐴, 0))) |
110 | 63 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → (¬ 𝜓 ↔ (𝜑 ↔ 𝜓))) |
111 | 110 | con1bid 344 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → (¬ (𝜑 ↔ 𝜓) ↔ 𝜓)) |
112 | 96, 111 | syl5bb 271 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → ((𝜑 ⊻ 𝜓) ↔ 𝜓)) |
113 | 112 | ifbid 4058 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → if((𝜑 ⊻ 𝜓), 𝐴, 0) = if(𝜓, 𝐴, 0)) |
114 | | simpr 476 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → ¬ 𝜑) |
115 | 114 | intnanrd 954 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → ¬ (𝜑 ∧ 𝜓)) |
116 | | iffalse 4045 |
. . . . . . 7
⊢ (¬
(𝜑 ∧ 𝜓) → if((𝜑 ∧ 𝜓), (2 · 𝐴), 0) = 0) |
117 | 115, 116 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → if((𝜑 ∧ 𝜓), (2 · 𝐴), 0) = 0) |
118 | 113, 117 | oveq12d 6567 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 0)) |
119 | 25 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → if(𝜑, 𝐴, 0) = 0) |
120 | 119 | oveq1d 6564 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (0 + if(𝜓, 𝐴, 0))) |
121 | 109, 118,
120 | 3eqtr4d 2654 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0))) |
122 | 104, 121 | pm2.61dan 828 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜒) → (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0))) |
123 | | had0 1534 |
. . . . . . 7
⊢ (¬
𝜒 → (hadd(𝜒, 𝜑, 𝜓) ↔ (𝜑 ⊻ 𝜓))) |
124 | 73, 123 | syl5bbr 273 |
. . . . . 6
⊢ (¬
𝜒 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ⊻ 𝜓))) |
125 | 124 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜒) → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ⊻ 𝜓))) |
126 | 125 | ifbid 4058 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜒) → if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) = if((𝜑 ⊻ 𝜓), 𝐴, 0)) |
127 | | cad0 1547 |
. . . . . 6
⊢ (¬
𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∧ 𝜓))) |
128 | 127 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜒) → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∧ 𝜓))) |
129 | 128 | ifbid 4058 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜒) → if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0) = if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)) |
130 | 126, 129 | oveq12d 6567 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0))) |
131 | | iffalse 4045 |
. . . . 5
⊢ (¬
𝜒 → if(𝜒, 𝐴, 0) = 0) |
132 | 131 | oveq2d 6565 |
. . . 4
⊢ (¬
𝜒 → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 0)) |
133 | | ifcl 4080 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 ∈
ℂ) → if(𝜑, 𝐴, 0) ∈
ℂ) |
134 | 1, 133 | mpan2 703 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → if(𝜑, 𝐴, 0) ∈ ℂ) |
135 | 134, 3 | addcld 9938 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) ∈ ℂ) |
136 | 135 | addid1d 10115 |
. . . 4
⊢ (𝐴 ∈ ℂ →
((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 0) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0))) |
137 | 132, 136 | sylan9eqr 2666 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜒) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0))) |
138 | 122, 130,
137 | 3eqtr4d 2654 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0))) |
139 | 85, 138 | pm2.61dan 828 |
1
⊢ (𝐴 ∈ ℂ →
(if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0))) |