Step | Hyp | Ref
| Expression |
1 | | 0re 9919 |
. 2
⊢ 0 ∈
ℝ |
2 | | ax-rnegex 9886 |
. 2
⊢ (0 ∈
ℝ → ∃𝑐
∈ ℝ (0 + 𝑐) =
0) |
3 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑐 = 0 → (0 + 𝑐) = (0 + 0)) |
4 | 3 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑐 = 0 → ((0 + 𝑐) = 0 ↔ (0 + 0) =
0)) |
5 | 4 | biimpd 218 |
. . . . 5
⊢ (𝑐 = 0 → ((0 + 𝑐) = 0 → (0 + 0) =
0)) |
6 | 5 | adantld 482 |
. . . 4
⊢ (𝑐 = 0 → ((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) → (0 + 0) = 0)) |
7 | | ax-rrecex 9887 |
. . . . . . 7
⊢ ((𝑐 ∈ ℝ ∧ 𝑐 ≠ 0) → ∃𝑦 ∈ ℝ (𝑐 · 𝑦) = 1) |
8 | 7 | adantlr 747 |
. . . . . 6
⊢ (((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) → ∃𝑦 ∈ ℝ (𝑐 · 𝑦) = 1) |
9 | | simplll 794 |
. . . . . . . . . . 11
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → 𝑐 ∈ ℝ) |
10 | 9 | recnd 9947 |
. . . . . . . . . 10
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → 𝑐 ∈ ℂ) |
11 | | simprl 790 |
. . . . . . . . . . 11
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → 𝑦 ∈ ℝ) |
12 | 11 | recnd 9947 |
. . . . . . . . . 10
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → 𝑦 ∈ ℂ) |
13 | | 0cn 9911 |
. . . . . . . . . . 11
⊢ 0 ∈
ℂ |
14 | | mulass 9903 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 0 ∈
ℂ) → ((𝑐
· 𝑦) · 0) =
(𝑐 · (𝑦 · 0))) |
15 | 13, 14 | mp3an3 1405 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑐 · 𝑦) · 0) = (𝑐 · (𝑦 · 0))) |
16 | 10, 12, 15 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · 𝑦) · 0) = (𝑐 · (𝑦 · 0))) |
17 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ ((𝑐 · 𝑦) = 1 → ((𝑐 · 𝑦) · 0) = (1 ·
0)) |
18 | 13 | mulid2i 9922 |
. . . . . . . . . . 11
⊢ (1
· 0) = 0 |
19 | 17, 18 | syl6eq 2660 |
. . . . . . . . . 10
⊢ ((𝑐 · 𝑦) = 1 → ((𝑐 · 𝑦) · 0) = 0) |
20 | 19 | ad2antll 761 |
. . . . . . . . 9
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · 𝑦) · 0) = 0) |
21 | 16, 20 | eqtr3d 2646 |
. . . . . . . 8
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑐 · (𝑦 · 0)) = 0) |
22 | 21 | oveq1d 6564 |
. . . . . . 7
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · (𝑦 · 0)) + 0) = (0 +
0)) |
23 | | simpllr 795 |
. . . . . . . . . . . 12
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 + 𝑐) = 0) |
24 | 23 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((0 + 𝑐) · (𝑦 · 0)) = (0 · (𝑦 · 0))) |
25 | | remulcl 9900 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ ∧ 0 ∈
ℝ) → (𝑦 ·
0) ∈ ℝ) |
26 | 1, 25 | mpan2 703 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ → (𝑦 · 0) ∈
ℝ) |
27 | 26 | ad2antrl 760 |
. . . . . . . . . . . . 13
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑦 · 0) ∈ ℝ) |
28 | 27 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑦 · 0) ∈ ℂ) |
29 | | adddir 9910 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℂ ∧ 𝑐
∈ ℂ ∧ (𝑦
· 0) ∈ ℂ) → ((0 + 𝑐) · (𝑦 · 0)) = ((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0)))) |
30 | 13, 29 | mp3an1 1403 |
. . . . . . . . . . . 12
⊢ ((𝑐 ∈ ℂ ∧ (𝑦 · 0) ∈ ℂ)
→ ((0 + 𝑐) ·
(𝑦 · 0)) = ((0
· (𝑦 · 0)) +
(𝑐 · (𝑦 · 0)))) |
31 | 10, 28, 30 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((0 + 𝑐) · (𝑦 · 0)) = ((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0)))) |
32 | 24, 31 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 · (𝑦 · 0)) = ((0 ·
(𝑦 · 0)) + (𝑐 · (𝑦 · 0)))) |
33 | 32 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((0 · (𝑦 · 0)) + 0) = (((0
· (𝑦 · 0)) +
(𝑐 · (𝑦 · 0))) +
0)) |
34 | | remulcl 9900 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ (𝑦
· 0) ∈ ℝ) → (0 · (𝑦 · 0)) ∈
ℝ) |
35 | 1, 26, 34 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ → (0
· (𝑦 · 0))
∈ ℝ) |
36 | 35 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 · (𝑦 · 0)) ∈
ℝ) |
37 | 36 | recnd 9947 |
. . . . . . . . . 10
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 · (𝑦 · 0)) ∈
ℂ) |
38 | | remulcl 9900 |
. . . . . . . . . . . 12
⊢ ((𝑐 ∈ ℝ ∧ (𝑦 · 0) ∈ ℝ)
→ (𝑐 · (𝑦 · 0)) ∈
ℝ) |
39 | 9, 27, 38 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑐 · (𝑦 · 0)) ∈
ℝ) |
40 | 39 | recnd 9947 |
. . . . . . . . . 10
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑐 · (𝑦 · 0)) ∈
ℂ) |
41 | | addass 9902 |
. . . . . . . . . . 11
⊢ (((0
· (𝑦 · 0))
∈ ℂ ∧ (𝑐
· (𝑦 · 0))
∈ ℂ ∧ 0 ∈ ℂ) → (((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))) + 0) = ((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0))) |
42 | 13, 41 | mp3an3 1405 |
. . . . . . . . . 10
⊢ (((0
· (𝑦 · 0))
∈ ℂ ∧ (𝑐
· (𝑦 · 0))
∈ ℂ) → (((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))) + 0) = ((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0))) |
43 | 37, 40, 42 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))) + 0) = ((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0))) |
44 | 33, 43 | eqtr2d 2645 |
. . . . . . . 8
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)) = ((0 · (𝑦 · 0)) +
0)) |
45 | 26, 38 | sylan2 490 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑐 · (𝑦 · 0)) ∈
ℝ) |
46 | | readdcl 9898 |
. . . . . . . . . . 11
⊢ (((𝑐 · (𝑦 · 0)) ∈ ℝ ∧ 0 ∈
ℝ) → ((𝑐
· (𝑦 · 0)) +
0) ∈ ℝ) |
47 | 45, 1, 46 | sylancl 693 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑐 · (𝑦 · 0)) + 0) ∈
ℝ) |
48 | 9, 11, 47 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · (𝑦 · 0)) + 0) ∈
ℝ) |
49 | | readdcan 10089 |
. . . . . . . . . 10
⊢ ((((𝑐 · (𝑦 · 0)) + 0) ∈ ℝ ∧ 0
∈ ℝ ∧ (0 · (𝑦 · 0)) ∈ ℝ) → (((0
· (𝑦 · 0)) +
((𝑐 · (𝑦 · 0)) + 0)) = ((0
· (𝑦 · 0)) +
0) ↔ ((𝑐 ·
(𝑦 · 0)) + 0) =
0)) |
50 | 1, 49 | mp3an2 1404 |
. . . . . . . . 9
⊢ ((((𝑐 · (𝑦 · 0)) + 0) ∈ ℝ ∧ (0
· (𝑦 · 0))
∈ ℝ) → (((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)) = ((0 · (𝑦 · 0)) + 0) ↔
((𝑐 · (𝑦 · 0)) + 0) =
0)) |
51 | 48, 36, 50 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)) = ((0 · (𝑦 · 0)) + 0) ↔
((𝑐 · (𝑦 · 0)) + 0) =
0)) |
52 | 44, 51 | mpbid 221 |
. . . . . . 7
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · (𝑦 · 0)) + 0) = 0) |
53 | 22, 52 | eqtr3d 2646 |
. . . . . 6
⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 + 0) = 0) |
54 | 8, 53 | rexlimddv 3017 |
. . . . 5
⊢ (((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) → (0 + 0) = 0) |
55 | 54 | expcom 450 |
. . . 4
⊢ (𝑐 ≠ 0 → ((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) → (0 + 0) =
0)) |
56 | 6, 55 | pm2.61ine 2865 |
. . 3
⊢ ((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) → (0 + 0) =
0) |
57 | 56 | rexlimiva 3010 |
. 2
⊢
(∃𝑐 ∈
ℝ (0 + 𝑐) = 0 →
(0 + 0) = 0) |
58 | 1, 2, 57 | mp2b 10 |
1
⊢ (0 + 0) =
0 |