Step | Hyp | Ref
| Expression |
1 | | 0re 10252 |
. 2
⊢ 0 ∈
ℝ |
2 | | ax-rnegex 10219 |
. 2
⊢ (0 ∈
ℝ → ∃𝑐
∈ ℝ (0 + 𝑐) =
0) |
3 | | oveq2 6822 |
. . . . . . 7
⊢ (𝑐 = 0 → (0 + 𝑐) = (0 + 0)) |
4 | 3 | eqeq1d 2762 |
. . . . . 6
⊢ (𝑐 = 0 → ((0 + 𝑐) = 0 ↔ (0 + 0) =
0)) |
5 | 4 | biimpd 219 |
. . . . 5
⊢ (𝑐 = 0 → ((0 + 𝑐) = 0 → (0 + 0) =
0)) |
6 | 5 | adantld 484 |
. . . 4
⊢ (𝑐 = 0 → ((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) → (0 + 0) = 0)) |
7 | | ax-rrecex 10220 |
. . . . . . 7
⊢ ((𝑐 ∈ ℝ ∧ 𝑐 ≠ 0) → ∃𝑦 ∈ ℝ (𝑐 · 𝑦) = 1) |
8 | 7 | adantlr 753 |
. . . . . 6
⊢ (((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) → ∃𝑦 ∈ ℝ (𝑐 · 𝑦) = 1) |
9 | | simplll 815 |
. . . . . . . . . . 11
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → 𝑐 ∈ ℝ) |
10 | 9 | recnd 10280 |
. . . . . . . . . 10
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → 𝑐 ∈ ℂ) |
11 | | simprl 811 |
. . . . . . . . . . 11
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → 𝑦 ∈ ℝ) |
12 | 11 | recnd 10280 |
. . . . . . . . . 10
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → 𝑦 ∈ ℂ) |
13 | | 0cn 10244 |
. . . . . . . . . . 11
⊢ 0 ∈
ℂ |
14 | | mulass 10236 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 0 ∈
ℂ) → ((𝑐
· 𝑦) · 0) =
(𝑐 · (𝑦 · 0))) |
15 | 13, 14 | mp3an3 1562 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑐 · 𝑦) · 0) = (𝑐 · (𝑦 · 0))) |
16 | 10, 12, 15 | syl2anc 696 |
. . . . . . . . 9
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · 𝑦) · 0) = (𝑐 · (𝑦 · 0))) |
17 | | oveq1 6821 |
. . . . . . . . . . 11
⊢ ((𝑐 · 𝑦) = 1 → ((𝑐 · 𝑦) · 0) = (1 ·
0)) |
18 | 13 | mulid2i 10255 |
. . . . . . . . . . 11
⊢ (1
· 0) = 0 |
19 | 17, 18 | syl6eq 2810 |
. . . . . . . . . 10
⊢ ((𝑐 · 𝑦) = 1 → ((𝑐 · 𝑦) · 0) = 0) |
20 | 19 | ad2antll 767 |
. . . . . . . . 9
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · 𝑦) · 0) = 0) |
21 | 16, 20 | eqtr3d 2796 |
. . . . . . . 8
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑐 · (𝑦 · 0)) = 0) |
22 | 21 | oveq1d 6829 |
. . . . . . 7
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · (𝑦 · 0)) + 0) = (0 +
0)) |
23 | | simpllr 817 |
. . . . . . . . . . . 12
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 + 𝑐) = 0) |
24 | 23 | oveq1d 6829 |
. . . . . . . . . . 11
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((0 + 𝑐) · (𝑦 · 0)) = (0 · (𝑦 · 0))) |
25 | | remulcl 10233 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ ∧ 0 ∈
ℝ) → (𝑦 ·
0) ∈ ℝ) |
26 | 1, 25 | mpan2 709 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ → (𝑦 · 0) ∈
ℝ) |
27 | 26 | ad2antrl 766 |
. . . . . . . . . . . . 13
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑦 · 0) ∈ ℝ) |
28 | 27 | recnd 10280 |
. . . . . . . . . . . 12
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑦 · 0) ∈ ℂ) |
29 | | adddir 10243 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℂ ∧ 𝑐
∈ ℂ ∧ (𝑦
· 0) ∈ ℂ) → ((0 + 𝑐) · (𝑦 · 0)) = ((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0)))) |
30 | 13, 29 | mp3an1 1560 |
. . . . . . . . . . . 12
⊢ ((𝑐 ∈ ℂ ∧ (𝑦 · 0) ∈ ℂ)
→ ((0 + 𝑐) ·
(𝑦 · 0)) = ((0
· (𝑦 · 0)) +
(𝑐 · (𝑦 · 0)))) |
31 | 10, 28, 30 | syl2anc 696 |
. . . . . . . . . . 11
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((0 + 𝑐) · (𝑦 · 0)) = ((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0)))) |
32 | 24, 31 | eqtr3d 2796 |
. . . . . . . . . 10
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 · (𝑦 · 0)) = ((0 ·
(𝑦 · 0)) + (𝑐 · (𝑦 · 0)))) |
33 | 32 | oveq1d 6829 |
. . . . . . . . 9
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((0 · (𝑦 · 0)) + 0) = (((0
· (𝑦 · 0)) +
(𝑐 · (𝑦 · 0))) +
0)) |
34 | | remulcl 10233 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ (𝑦
· 0) ∈ ℝ) → (0 · (𝑦 · 0)) ∈
ℝ) |
35 | 1, 26, 34 | sylancr 698 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ → (0
· (𝑦 · 0))
∈ ℝ) |
36 | 35 | ad2antrl 766 |
. . . . . . . . . . 11
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 · (𝑦 · 0)) ∈
ℝ) |
37 | 36 | recnd 10280 |
. . . . . . . . . 10
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 · (𝑦 · 0)) ∈
ℂ) |
38 | | remulcl 10233 |
. . . . . . . . . . . 12
⊢ ((𝑐 ∈ ℝ ∧ (𝑦 · 0) ∈ ℝ)
→ (𝑐 · (𝑦 · 0)) ∈
ℝ) |
39 | 9, 27, 38 | syl2anc 696 |
. . . . . . . . . . 11
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑐 · (𝑦 · 0)) ∈
ℝ) |
40 | 39 | recnd 10280 |
. . . . . . . . . 10
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑐 · (𝑦 · 0)) ∈
ℂ) |
41 | | addass 10235 |
. . . . . . . . . . 11
⊢ (((0
· (𝑦 · 0))
∈ ℂ ∧ (𝑐
· (𝑦 · 0))
∈ ℂ ∧ 0 ∈ ℂ) → (((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))) + 0) = ((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0))) |
42 | 13, 41 | mp3an3 1562 |
. . . . . . . . . 10
⊢ (((0
· (𝑦 · 0))
∈ ℂ ∧ (𝑐
· (𝑦 · 0))
∈ ℂ) → (((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))) + 0) = ((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0))) |
43 | 37, 40, 42 | syl2anc 696 |
. . . . . . . . 9
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))) + 0) = ((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0))) |
44 | 33, 43 | eqtr2d 2795 |
. . . . . . . 8
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)) = ((0 · (𝑦 · 0)) +
0)) |
45 | 26, 38 | sylan2 492 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑐 · (𝑦 · 0)) ∈
ℝ) |
46 | | readdcl 10231 |
. . . . . . . . . . 11
⊢ (((𝑐 · (𝑦 · 0)) ∈ ℝ ∧ 0 ∈
ℝ) → ((𝑐
· (𝑦 · 0)) +
0) ∈ ℝ) |
47 | 45, 1, 46 | sylancl 697 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑐 · (𝑦 · 0)) + 0) ∈
ℝ) |
48 | 9, 11, 47 | syl2anc 696 |
. . . . . . . . 9
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · (𝑦 · 0)) + 0) ∈
ℝ) |
49 | | readdcan 10422 |
. . . . . . . . . 10
⊢ ((((𝑐 · (𝑦 · 0)) + 0) ∈ ℝ ∧ 0
∈ ℝ ∧ (0 · (𝑦 · 0)) ∈ ℝ) → (((0
· (𝑦 · 0)) +
((𝑐 · (𝑦 · 0)) + 0)) = ((0
· (𝑦 · 0)) +
0) ↔ ((𝑐 ·
(𝑦 · 0)) + 0) =
0)) |
50 | 1, 49 | mp3an2 1561 |
. . . . . . . . 9
⊢ ((((𝑐 · (𝑦 · 0)) + 0) ∈ ℝ ∧ (0
· (𝑦 · 0))
∈ ℝ) → (((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)) = ((0 · (𝑦 · 0)) + 0) ↔
((𝑐 · (𝑦 · 0)) + 0) =
0)) |
51 | 48, 36, 50 | syl2anc 696 |
. . . . . . . 8
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)) = ((0 · (𝑦 · 0)) + 0) ↔
((𝑐 · (𝑦 · 0)) + 0) =
0)) |
52 | 44, 51 | mpbid 222 |
. . . . . . 7
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · (𝑦 · 0)) + 0) = 0) |
53 | 22, 52 | eqtr3d 2796 |
. . . . . 6
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 + 0) = 0) |
54 | 8, 53 | rexlimddv 3173 |
. . . . 5
⊢ (((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) → (0 + 0) = 0) |
55 | 54 | expcom 450 |
. . . 4
⊢ (𝑐 ≠ 0 → ((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) → (0 + 0) =
0)) |
56 | 6, 55 | pm2.61ine 3015 |
. . 3
⊢ ((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) → (0 + 0) =
0) |
57 | 56 | rexlimiva 3166 |
. 2
⊢
(∃𝑐 ∈
ℝ (0 + 𝑐) = 0 →
(0 + 0) = 0) |
58 | 1, 2, 57 | mp2b 10 |
1
⊢ (0 + 0) =
0 |