| Step | Hyp | Ref
| Expression |
| 1 | | 1re 11261 |
. 2
⊢ 1 ∈
ℝ |
| 2 | | ax-rnegex 11226 |
. 2
⊢ (1 ∈
ℝ → ∃𝑐
∈ ℝ (1 + 𝑐) =
0) |
| 3 | | ax-1ne0 11224 |
. . . . . 6
⊢ 1 ≠
0 |
| 4 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑐 = 0 → (1 + 𝑐) = (1 + 0)) |
| 5 | 4 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑐 = 0 → ((1 + 𝑐) = 0 ↔ (1 + 0) =
0)) |
| 6 | 5 | biimpcd 249 |
. . . . . . . 8
⊢ ((1 +
𝑐) = 0 → (𝑐 = 0 → (1 + 0) =
0)) |
| 7 | | oveq2 7439 |
. . . . . . . . 9
⊢ ((1 + 0)
= 0 → (((i · i) · (i · i)) · (1 + 0)) = (((i
· i) · (i · i)) · 0)) |
| 8 | | ax-icn 11214 |
. . . . . . . . . . . . . . 15
⊢ i ∈
ℂ |
| 9 | 8, 8 | mulcli 11268 |
. . . . . . . . . . . . . 14
⊢ (i
· i) ∈ ℂ |
| 10 | 9, 9 | mulcli 11268 |
. . . . . . . . . . . . 13
⊢ ((i
· i) · (i · i)) ∈ ℂ |
| 11 | | ax-1cn 11213 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
| 12 | | 0cn 11253 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℂ |
| 13 | 10, 11, 12 | adddii 11273 |
. . . . . . . . . . . 12
⊢ (((i
· i) · (i · i)) · (1 + 0)) = ((((i · i)
· (i · i)) · 1) + (((i · i) · (i ·
i)) · 0)) |
| 14 | 10 | mulridi 11265 |
. . . . . . . . . . . . 13
⊢ (((i
· i) · (i · i)) · 1) = ((i · i) · (i
· i)) |
| 15 | | mul01 11440 |
. . . . . . . . . . . . . . 15
⊢ (((i
· i) · (i · i)) ∈ ℂ → (((i · i)
· (i · i)) · 0) = 0) |
| 16 | 10, 15 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (((i
· i) · (i · i)) · 0) = 0 |
| 17 | | ax-i2m1 11223 |
. . . . . . . . . . . . . 14
⊢ ((i
· i) + 1) = 0 |
| 18 | 16, 17 | eqtr4i 2768 |
. . . . . . . . . . . . 13
⊢ (((i
· i) · (i · i)) · 0) = ((i · i) +
1) |
| 19 | 14, 18 | oveq12i 7443 |
. . . . . . . . . . . 12
⊢ ((((i
· i) · (i · i)) · 1) + (((i · i) · (i
· i)) · 0)) = (((i · i) · (i · i)) + ((i
· i) + 1)) |
| 20 | 13, 19 | eqtri 2765 |
. . . . . . . . . . 11
⊢ (((i
· i) · (i · i)) · (1 + 0)) = (((i · i)
· (i · i)) + ((i · i) + 1)) |
| 21 | 20, 16 | eqeq12i 2755 |
. . . . . . . . . 10
⊢ ((((i
· i) · (i · i)) · (1 + 0)) = (((i · i)
· (i · i)) · 0) ↔ (((i · i) · (i
· i)) + ((i · i) + 1)) = 0) |
| 22 | 10, 9, 11 | addassi 11271 |
. . . . . . . . . . . 12
⊢ ((((i
· i) · (i · i)) + (i · i)) + 1) = (((i · i)
· (i · i)) + ((i · i) + 1)) |
| 23 | 9 | mulridi 11265 |
. . . . . . . . . . . . . . 15
⊢ ((i
· i) · 1) = (i · i) |
| 24 | 23 | oveq2i 7442 |
. . . . . . . . . . . . . 14
⊢ (((i
· i) · (i · i)) + ((i · i) · 1)) = (((i
· i) · (i · i)) + (i · i)) |
| 25 | 9, 9, 11 | adddii 11273 |
. . . . . . . . . . . . . . 15
⊢ ((i
· i) · ((i · i) + 1)) = (((i · i) · (i
· i)) + ((i · i) · 1)) |
| 26 | 17 | oveq2i 7442 |
. . . . . . . . . . . . . . . 16
⊢ ((i
· i) · ((i · i) + 1)) = ((i · i) ·
0) |
| 27 | | mul01 11440 |
. . . . . . . . . . . . . . . . 17
⊢ ((i
· i) ∈ ℂ → ((i · i) · 0) =
0) |
| 28 | 9, 27 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ((i
· i) · 0) = 0 |
| 29 | 26, 28 | eqtri 2765 |
. . . . . . . . . . . . . . 15
⊢ ((i
· i) · ((i · i) + 1)) = 0 |
| 30 | 25, 29 | eqtr3i 2767 |
. . . . . . . . . . . . . 14
⊢ (((i
· i) · (i · i)) + ((i · i) · 1)) =
0 |
| 31 | 24, 30 | eqtr3i 2767 |
. . . . . . . . . . . . 13
⊢ (((i
· i) · (i · i)) + (i · i)) = 0 |
| 32 | 31 | oveq1i 7441 |
. . . . . . . . . . . 12
⊢ ((((i
· i) · (i · i)) + (i · i)) + 1) = (0 +
1) |
| 33 | 22, 32 | eqtr3i 2767 |
. . . . . . . . . . 11
⊢ (((i
· i) · (i · i)) + ((i · i) + 1)) = (0 +
1) |
| 34 | | 00id 11436 |
. . . . . . . . . . . 12
⊢ (0 + 0) =
0 |
| 35 | 34 | eqcomi 2746 |
. . . . . . . . . . 11
⊢ 0 = (0 +
0) |
| 36 | 33, 35 | eqeq12i 2755 |
. . . . . . . . . 10
⊢ ((((i
· i) · (i · i)) + ((i · i) + 1)) = 0 ↔ (0 + 1)
= (0 + 0)) |
| 37 | | 0re 11263 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
| 38 | | readdcan 11435 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ 0 ∈ ℝ ∧ 0 ∈ ℝ) → ((0 + 1) =
(0 + 0) ↔ 1 = 0)) |
| 39 | 1, 37, 37, 38 | mp3an 1463 |
. . . . . . . . . 10
⊢ ((0 + 1)
= (0 + 0) ↔ 1 = 0) |
| 40 | 21, 36, 39 | 3bitri 297 |
. . . . . . . . 9
⊢ ((((i
· i) · (i · i)) · (1 + 0)) = (((i · i)
· (i · i)) · 0) ↔ 1 = 0) |
| 41 | 7, 40 | sylib 218 |
. . . . . . . 8
⊢ ((1 + 0)
= 0 → 1 = 0) |
| 42 | 6, 41 | syl6 35 |
. . . . . . 7
⊢ ((1 +
𝑐) = 0 → (𝑐 = 0 → 1 =
0)) |
| 43 | 42 | necon3d 2961 |
. . . . . 6
⊢ ((1 +
𝑐) = 0 → (1 ≠ 0
→ 𝑐 ≠
0)) |
| 44 | 3, 43 | mpi 20 |
. . . . 5
⊢ ((1 +
𝑐) = 0 → 𝑐 ≠ 0) |
| 45 | | ax-rrecex 11227 |
. . . . 5
⊢ ((𝑐 ∈ ℝ ∧ 𝑐 ≠ 0) → ∃𝑥 ∈ ℝ (𝑐 · 𝑥) = 1) |
| 46 | 44, 45 | sylan2 593 |
. . . 4
⊢ ((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) → ∃𝑥 ∈ ℝ (𝑐 · 𝑥) = 1) |
| 47 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝐴 ∈ ℂ) |
| 48 | | simplrl 777 |
. . . . . . . . . . 11
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝑥 ∈ ℝ) |
| 49 | 48 | recnd 11289 |
. . . . . . . . . 10
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝑥 ∈ ℂ) |
| 50 | 47, 49 | mulcld 11281 |
. . . . . . . . 9
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝐴 · 𝑥) ∈ ℂ) |
| 51 | | simplll 775 |
. . . . . . . . . 10
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝑐 ∈ ℝ) |
| 52 | 51 | recnd 11289 |
. . . . . . . . 9
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝑐 ∈ ℂ) |
| 53 | 12 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 0 ∈
ℂ) |
| 54 | 50, 52, 53 | adddid 11285 |
. . . . . . . 8
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · (𝑐 + 0)) = (((𝐴 · 𝑥) · 𝑐) + ((𝐴 · 𝑥) · 0))) |
| 55 | 11 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 1 ∈
ℂ) |
| 56 | 55, 52, 53 | addassd 11283 |
. . . . . . . . . . . 12
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((1 + 𝑐) + 0) = (1 + (𝑐 + 0))) |
| 57 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (1 + 𝑐) = 0) |
| 58 | 57 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((1 + 𝑐) + 0) = (0 +
0)) |
| 59 | 56, 58 | eqtr3d 2779 |
. . . . . . . . . . 11
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (1 + (𝑐 + 0)) = (0 +
0)) |
| 60 | 34, 59, 57 | 3eqtr4a 2803 |
. . . . . . . . . 10
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (1 + (𝑐 + 0)) = (1 + 𝑐)) |
| 61 | 37 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 0 ∈
ℝ) |
| 62 | 51, 61 | readdcld 11290 |
. . . . . . . . . . 11
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝑐 + 0) ∈ ℝ) |
| 63 | 1 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 1 ∈
ℝ) |
| 64 | | readdcan 11435 |
. . . . . . . . . . 11
⊢ (((𝑐 + 0) ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 1 ∈
ℝ) → ((1 + (𝑐 +
0)) = (1 + 𝑐) ↔ (𝑐 + 0) = 𝑐)) |
| 65 | 62, 51, 63, 64 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((1 + (𝑐 + 0)) = (1 + 𝑐) ↔ (𝑐 + 0) = 𝑐)) |
| 66 | 60, 65 | mpbid 232 |
. . . . . . . . 9
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝑐 + 0) = 𝑐) |
| 67 | 66 | oveq2d 7447 |
. . . . . . . 8
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · (𝑐 + 0)) = ((𝐴 · 𝑥) · 𝑐)) |
| 68 | 54, 67 | eqtr3d 2779 |
. . . . . . 7
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (((𝐴 · 𝑥) · 𝑐) + ((𝐴 · 𝑥) · 0)) = ((𝐴 · 𝑥) · 𝑐)) |
| 69 | | mul31 11428 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑐 ∈ ℂ) → ((𝐴 · 𝑥) · 𝑐) = ((𝑐 · 𝑥) · 𝐴)) |
| 70 | 47, 49, 52, 69 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · 𝑐) = ((𝑐 · 𝑥) · 𝐴)) |
| 71 | | simplrr 778 |
. . . . . . . . . 10
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝑐 · 𝑥) = 1) |
| 72 | 71 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝑐 · 𝑥) · 𝐴) = (1 · 𝐴)) |
| 73 | 47 | mullidd 11279 |
. . . . . . . . 9
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = 𝐴) |
| 74 | 70, 72, 73 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · 𝑐) = 𝐴) |
| 75 | | mul01 11440 |
. . . . . . . . 9
⊢ ((𝐴 · 𝑥) ∈ ℂ → ((𝐴 · 𝑥) · 0) = 0) |
| 76 | 50, 75 | syl 17 |
. . . . . . . 8
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · 0) = 0) |
| 77 | 74, 76 | oveq12d 7449 |
. . . . . . 7
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (((𝐴 · 𝑥) · 𝑐) + ((𝐴 · 𝑥) · 0)) = (𝐴 + 0)) |
| 78 | 68, 77, 74 | 3eqtr3d 2785 |
. . . . . 6
⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝐴 + 0) = 𝐴) |
| 79 | 78 | exp42 435 |
. . . . 5
⊢ ((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) → (𝑥 ∈ ℝ → ((𝑐 · 𝑥) = 1 → (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)))) |
| 80 | 79 | rexlimdv 3153 |
. . . 4
⊢ ((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) → (∃𝑥 ∈ ℝ (𝑐 · 𝑥) = 1 → (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴))) |
| 81 | 46, 80 | mpd 15 |
. . 3
⊢ ((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) → (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)) |
| 82 | 81 | rexlimiva 3147 |
. 2
⊢
(∃𝑐 ∈
ℝ (1 + 𝑐) = 0 →
(𝐴 ∈ ℂ →
(𝐴 + 0) = 𝐴)) |
| 83 | 1, 2, 82 | mp2b 10 |
1
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) |