Proof of Theorem un0addcl
Step | Hyp | Ref
| Expression |
1 | | un0addcl.2 |
. . . . 5
⊢ 𝑇 = (𝑆 ∪ {0}) |
2 | 1 | eleq2i 2830 |
. . . 4
⊢ (𝑁 ∈ 𝑇 ↔ 𝑁 ∈ (𝑆 ∪ {0})) |
3 | | elun 4084 |
. . . 4
⊢ (𝑁 ∈ (𝑆 ∪ {0}) ↔ (𝑁 ∈ 𝑆 ∨ 𝑁 ∈ {0})) |
4 | 2, 3 | bitri 274 |
. . 3
⊢ (𝑁 ∈ 𝑇 ↔ (𝑁 ∈ 𝑆 ∨ 𝑁 ∈ {0})) |
5 | 1 | eleq2i 2830 |
. . . . . 6
⊢ (𝑀 ∈ 𝑇 ↔ 𝑀 ∈ (𝑆 ∪ {0})) |
6 | | elun 4084 |
. . . . . 6
⊢ (𝑀 ∈ (𝑆 ∪ {0}) ↔ (𝑀 ∈ 𝑆 ∨ 𝑀 ∈ {0})) |
7 | 5, 6 | bitri 274 |
. . . . 5
⊢ (𝑀 ∈ 𝑇 ↔ (𝑀 ∈ 𝑆 ∨ 𝑀 ∈ {0})) |
8 | | ssun1 4107 |
. . . . . . . . 9
⊢ 𝑆 ⊆ (𝑆 ∪ {0}) |
9 | 8, 1 | sseqtrri 3959 |
. . . . . . . 8
⊢ 𝑆 ⊆ 𝑇 |
10 | | un0addcl.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → (𝑀 + 𝑁) ∈ 𝑆) |
11 | 9, 10 | sselid 3920 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → (𝑀 + 𝑁) ∈ 𝑇) |
12 | 11 | expr 457 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ 𝑆) → (𝑁 ∈ 𝑆 → (𝑀 + 𝑁) ∈ 𝑇)) |
13 | | un0addcl.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
14 | 13 | sselda 3922 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑆) → 𝑁 ∈ ℂ) |
15 | 14 | addid2d 11174 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑆) → (0 + 𝑁) = 𝑁) |
16 | 9 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ⊆ 𝑇) |
17 | 16 | sselda 3922 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑆) → 𝑁 ∈ 𝑇) |
18 | 15, 17 | eqeltrd 2839 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑆) → (0 + 𝑁) ∈ 𝑇) |
19 | | elsni 4580 |
. . . . . . . . . 10
⊢ (𝑀 ∈ {0} → 𝑀 = 0) |
20 | 19 | oveq1d 7292 |
. . . . . . . . 9
⊢ (𝑀 ∈ {0} → (𝑀 + 𝑁) = (0 + 𝑁)) |
21 | 20 | eleq1d 2823 |
. . . . . . . 8
⊢ (𝑀 ∈ {0} → ((𝑀 + 𝑁) ∈ 𝑇 ↔ (0 + 𝑁) ∈ 𝑇)) |
22 | 18, 21 | syl5ibrcom 246 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑆) → (𝑀 ∈ {0} → (𝑀 + 𝑁) ∈ 𝑇)) |
23 | 22 | impancom 452 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ {0}) → (𝑁 ∈ 𝑆 → (𝑀 + 𝑁) ∈ 𝑇)) |
24 | 12, 23 | jaodan 955 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀 ∈ 𝑆 ∨ 𝑀 ∈ {0})) → (𝑁 ∈ 𝑆 → (𝑀 + 𝑁) ∈ 𝑇)) |
25 | 7, 24 | sylan2b 594 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → (𝑁 ∈ 𝑆 → (𝑀 + 𝑁) ∈ 𝑇)) |
26 | | 0cnd 10966 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℂ) |
27 | 26 | snssd 4744 |
. . . . . . . . . 10
⊢ (𝜑 → {0} ⊆
ℂ) |
28 | 13, 27 | unssd 4121 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 ∪ {0}) ⊆
ℂ) |
29 | 1, 28 | eqsstrid 3970 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ⊆ ℂ) |
30 | 29 | sselda 3922 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → 𝑀 ∈ ℂ) |
31 | 30 | addid1d 11173 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → (𝑀 + 0) = 𝑀) |
32 | | simpr 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → 𝑀 ∈ 𝑇) |
33 | 31, 32 | eqeltrd 2839 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → (𝑀 + 0) ∈ 𝑇) |
34 | | elsni 4580 |
. . . . . . 7
⊢ (𝑁 ∈ {0} → 𝑁 = 0) |
35 | 34 | oveq2d 7293 |
. . . . . 6
⊢ (𝑁 ∈ {0} → (𝑀 + 𝑁) = (𝑀 + 0)) |
36 | 35 | eleq1d 2823 |
. . . . 5
⊢ (𝑁 ∈ {0} → ((𝑀 + 𝑁) ∈ 𝑇 ↔ (𝑀 + 0) ∈ 𝑇)) |
37 | 33, 36 | syl5ibrcom 246 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → (𝑁 ∈ {0} → (𝑀 + 𝑁) ∈ 𝑇)) |
38 | 25, 37 | jaod 856 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → ((𝑁 ∈ 𝑆 ∨ 𝑁 ∈ {0}) → (𝑀 + 𝑁) ∈ 𝑇)) |
39 | 4, 38 | syl5bi 241 |
. 2
⊢ ((𝜑 ∧ 𝑀 ∈ 𝑇) → (𝑁 ∈ 𝑇 → (𝑀 + 𝑁) ∈ 𝑇)) |
40 | 39 | impr 455 |
1
⊢ ((𝜑 ∧ (𝑀 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) → (𝑀 + 𝑁) ∈ 𝑇) |