Users' Mathboxes Mathbox for Steven Nguyen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sn-0tie0 Structured version   Visualization version   GIF version

Theorem sn-0tie0 40418
Description: Lemma for sn-mul02 40419. Commuted version of sn-it0e0 40394. (Contributed by SN, 30-Jun-2024.)
Assertion
Ref Expression
sn-0tie0 (0 · i) = 0

Proof of Theorem sn-0tie0
Dummy variables 𝑎 𝑏 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0cn 10968 . . 3 0 ∈ ℂ
2 ax-icn 10931 . . 3 i ∈ ℂ
31, 2mulcli 10983 . 2 (0 · i) ∈ ℂ
4 cnre 10973 . 2 ((0 · i) ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (0 · i) = (𝑎 + (i · 𝑏)))
5 simplr 766 . . . . . . 7 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (𝑎 + (i · 𝑏)))
6 neqne 2953 . . . . . . . . . . . 12 (¬ (0 · i) = 0 → (0 · i) ≠ 0)
76adantl 482 . . . . . . . . . . 11 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) ≠ 0)
8 simplll 772 . . . . . . . . . . . . . . . . 17 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 ∈ ℝ)
9 rernegcl 40351 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ ℝ → (0 − 𝑎) ∈ ℝ)
108, 9syl 17 . . . . . . . . . . . . . . . 16 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 − 𝑎) ∈ ℝ)
11 1red 10977 . . . . . . . . . . . . . . . 16 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 1 ∈ ℝ)
1210, 11readdcld 11005 . . . . . . . . . . . . . . 15 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 − 𝑎) + 1) ∈ ℝ)
13 ax-rrecex 10944 . . . . . . . . . . . . . . 15 ((((0 − 𝑎) + 1) ∈ ℝ ∧ ((0 − 𝑎) + 1) ≠ 0) → ∃𝑥 ∈ ℝ (((0 − 𝑎) + 1) · 𝑥) = 1)
1412, 13sylan 580 . . . . . . . . . . . . . 14 (((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) → ∃𝑥 ∈ ℝ (((0 − 𝑎) + 1) · 𝑥) = 1)
152a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → i ∈ ℂ)
1610recnd 11004 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 − 𝑎) ∈ ℂ)
17 1cnd 10971 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 1 ∈ ℂ)
1815, 16, 17adddid 11000 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · ((0 − 𝑎) + 1)) = ((i · (0 − 𝑎)) + (i · 1)))
19 it1ei 40415 . . . . . . . . . . . . . . . . . . . . . 22 (i · 1) = i
2019oveq2i 7282 . . . . . . . . . . . . . . . . . . . . 21 ((i · (0 − 𝑎)) + (i · 1)) = ((i · (0 − 𝑎)) + i)
2118, 20eqtrdi 2796 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · ((0 − 𝑎) + 1)) = ((i · (0 − 𝑎)) + i))
2221oveq2d 7287 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · ((0 − 𝑎) + 1))) = (0 · ((i · (0 − 𝑎)) + i)))
23 0cnd 10969 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 0 ∈ ℂ)
2415, 16mulcld 10996 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (0 − 𝑎)) ∈ ℂ)
2523, 24, 15adddid 11000 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · ((i · (0 − 𝑎)) + i)) = ((0 · (i · (0 − 𝑎))) + (0 · i)))
2622, 25eqtrd 2780 . . . . . . . . . . . . . . . . . 18 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · ((0 − 𝑎) + 1))) = ((0 · (i · (0 − 𝑎))) + (0 · i)))
275oveq2d 7287 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 − 𝑎) + (0 · i)) = ((0 − 𝑎) + (𝑎 + (i · 𝑏))))
28 renegid2 40393 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 ∈ ℝ → ((0 − 𝑎) + 𝑎) = 0)
2928ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 − 𝑎) + 𝑎) = 0)
3029oveq1d 7286 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 − 𝑎) + 𝑎) + (i · 𝑏)) = (0 + (i · 𝑏)))
318recnd 11004 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 ∈ ℂ)
32 simpllr 773 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 ∈ ℝ)
3332recnd 11004 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 ∈ ℂ)
3415, 33mulcld 10996 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 𝑏) ∈ ℂ)
3516, 31, 34addassd 10998 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 − 𝑎) + 𝑎) + (i · 𝑏)) = ((0 − 𝑎) + (𝑎 + (i · 𝑏))))
36 sn-addid2 40384 . . . . . . . . . . . . . . . . . . . . . . 23 ((i · 𝑏) ∈ ℂ → (0 + (i · 𝑏)) = (i · 𝑏))
3734, 36syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 + (i · 𝑏)) = (i · 𝑏))
3830, 35, 373eqtr3d 2788 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 − 𝑎) + (𝑎 + (i · 𝑏))) = (i · 𝑏))
3927, 38eqtrd 2780 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 − 𝑎) + (0 · i)) = (i · 𝑏))
4039oveq2d 7287 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · ((0 − 𝑎) + (0 · i))) = ((0 · i) · (i · 𝑏)))
413a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) ∈ ℂ)
4241, 16, 41adddid 11000 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · ((0 − 𝑎) + (0 · i))) = (((0 · i) · (0 − 𝑎)) + ((0 · i) · (0 · i))))
4323, 15, 16mulassd 10999 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (0 − 𝑎)) = (0 · (i · (0 − 𝑎))))
4441, 23, 15mulassd 10999 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 · i) · 0) · i) = ((0 · i) · (0 · i)))
45 sn-mul01 40404 . . . . . . . . . . . . . . . . . . . . . . . 24 ((0 · i) ∈ ℂ → ((0 · i) · 0) = 0)
4641, 45syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · 0) = 0)
4746oveq1d 7286 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 · i) · 0) · i) = (0 · i))
4844, 47eqtr3d 2782 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (0 · i)) = (0 · i))
4943, 48oveq12d 7289 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 · i) · (0 − 𝑎)) + ((0 · i) · (0 · i))) = ((0 · (i · (0 − 𝑎))) + (0 · i)))
5042, 49eqtrd 2780 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · ((0 − 𝑎) + (0 · i))) = ((0 · (i · (0 − 𝑎))) + (0 · i)))
5123, 15, 34mulassd 10999 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (i · 𝑏)) = (0 · (i · (i · 𝑏))))
5215, 15, 33mulassd 10999 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · i) · 𝑏) = (i · (i · 𝑏)))
53 reixi 40401 . . . . . . . . . . . . . . . . . . . . . . . . 25 (i · i) = (0 − 1)
54 1re 10976 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ ℝ
55 rernegcl 40351 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 ∈ ℝ → (0 − 1) ∈ ℝ)
5654, 55ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 − 1) ∈ ℝ
5753, 56eqeltri 2837 . . . . . . . . . . . . . . . . . . . . . . . 24 (i · i) ∈ ℝ
5857a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · i) ∈ ℝ)
5958, 32remulcld 11006 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · i) · 𝑏) ∈ ℝ)
6052, 59eqeltrrd 2842 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (i · 𝑏)) ∈ ℝ)
61 remul02 40385 . . . . . . . . . . . . . . . . . . . . 21 ((i · (i · 𝑏)) ∈ ℝ → (0 · (i · (i · 𝑏))) = 0)
6260, 61syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (i · 𝑏))) = 0)
6351, 62eqtrd 2780 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (i · 𝑏)) = 0)
6440, 50, 633eqtr3d 2788 . . . . . . . . . . . . . . . . . 18 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · (i · (0 − 𝑎))) + (0 · i)) = 0)
6526, 64eqtrd 2780 . . . . . . . . . . . . . . . . 17 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · ((0 − 𝑎) + 1))) = 0)
6665ad2antrr 723 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (0 · (i · ((0 − 𝑎) + 1))) = 0)
6766oveq1d 7286 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → ((0 · (i · ((0 − 𝑎) + 1))) · 𝑥) = (0 · 𝑥))
68 0cnd 10969 . . . . . . . . . . . . . . . . 17 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → 0 ∈ ℂ)
692a1i 11 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → i ∈ ℂ)
7010ad2antrr 723 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (0 − 𝑎) ∈ ℝ)
7170recnd 11004 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (0 − 𝑎) ∈ ℂ)
72 1cnd 10971 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → 1 ∈ ℂ)
7371, 72addcld 10995 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → ((0 − 𝑎) + 1) ∈ ℂ)
7469, 73mulcld 10996 . . . . . . . . . . . . . . . . 17 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (i · ((0 − 𝑎) + 1)) ∈ ℂ)
75 simprl 768 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → 𝑥 ∈ ℝ)
7675recnd 11004 . . . . . . . . . . . . . . . . 17 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → 𝑥 ∈ ℂ)
7768, 74, 76mulassd 10999 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → ((0 · (i · ((0 − 𝑎) + 1))) · 𝑥) = (0 · ((i · ((0 − 𝑎) + 1)) · 𝑥)))
7869, 73, 76mulassd 10999 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → ((i · ((0 − 𝑎) + 1)) · 𝑥) = (i · (((0 − 𝑎) + 1) · 𝑥)))
79 simprr 770 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (((0 − 𝑎) + 1) · 𝑥) = 1)
8079oveq2d 7287 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (i · (((0 − 𝑎) + 1) · 𝑥)) = (i · 1))
8180, 19eqtrdi 2796 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (i · (((0 − 𝑎) + 1) · 𝑥)) = i)
8278, 81eqtrd 2780 . . . . . . . . . . . . . . . . 17 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → ((i · ((0 − 𝑎) + 1)) · 𝑥) = i)
8382oveq2d 7287 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (0 · ((i · ((0 − 𝑎) + 1)) · 𝑥)) = (0 · i))
8477, 83eqtrd 2780 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → ((0 · (i · ((0 − 𝑎) + 1))) · 𝑥) = (0 · i))
85 remul02 40385 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → (0 · 𝑥) = 0)
8675, 85syl 17 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (0 · 𝑥) = 0)
8767, 84, 863eqtr3d 2788 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (0 · i) = 0)
8814, 87rexlimddv 3222 . . . . . . . . . . . . 13 (((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) → (0 · i) = 0)
8988ex 413 . . . . . . . . . . . 12 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 − 𝑎) + 1) ≠ 0 → (0 · i) = 0))
9089necon1d 2967 . . . . . . . . . . 11 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) ≠ 0 → ((0 − 𝑎) + 1) = 0))
917, 90mpd 15 . . . . . . . . . 10 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 − 𝑎) + 1) = 0)
9291oveq2d 7287 . . . . . . . . 9 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + ((0 − 𝑎) + 1)) = (𝑎 + 0))
9331, 16, 17addassd 10998 . . . . . . . . . 10 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 − 𝑎)) + 1) = (𝑎 + ((0 − 𝑎) + 1)))
94 renegid 40353 . . . . . . . . . . . . 13 (𝑎 ∈ ℝ → (𝑎 + (0 − 𝑎)) = 0)
958, 94syl 17 . . . . . . . . . . . 12 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (0 − 𝑎)) = 0)
9695oveq1d 7286 . . . . . . . . . . 11 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 − 𝑎)) + 1) = (0 + 1))
97 readdid2 40383 . . . . . . . . . . . 12 (1 ∈ ℝ → (0 + 1) = 1)
9854, 97ax-mp 5 . . . . . . . . . . 11 (0 + 1) = 1
9996, 98eqtrdi 2796 . . . . . . . . . 10 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 − 𝑎)) + 1) = 1)
10093, 99eqtr3d 2782 . . . . . . . . 9 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + ((0 − 𝑎) + 1)) = 1)
101 readdid1 40389 . . . . . . . . . 10 (𝑎 ∈ ℝ → (𝑎 + 0) = 𝑎)
1028, 101syl 17 . . . . . . . . 9 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + 0) = 𝑎)
10392, 100, 1023eqtr3rd 2789 . . . . . . . 8 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 = 1)
104 rernegcl 40351 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ ℝ → (0 − 𝑏) ∈ ℝ)
10532, 104syl 17 . . . . . . . . . . . . . . . . 17 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 − 𝑏) ∈ ℝ)
10611, 105readdcld 11005 . . . . . . . . . . . . . . . 16 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + (0 − 𝑏)) ∈ ℝ)
107 ax-rrecex 10944 . . . . . . . . . . . . . . . 16 (((1 + (0 − 𝑏)) ∈ ℝ ∧ (1 + (0 − 𝑏)) ≠ 0) → ∃𝑦 ∈ ℝ ((1 + (0 − 𝑏)) · 𝑦) = 1)
108106, 107sylan 580 . . . . . . . . . . . . . . 15 (((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) → ∃𝑦 ∈ ℝ ((1 + (0 − 𝑏)) · 𝑦) = 1)
109105recnd 11004 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 − 𝑏) ∈ ℂ)
11015, 109mulcld 10996 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (0 − 𝑏)) ∈ ℂ)
11123, 15, 110adddid 11000 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i + (i · (0 − 𝑏)))) = ((0 · i) + (0 · (i · (0 − 𝑏)))))
112 0re 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ∈ ℝ
113 remul02 40385 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (0 ∈ ℝ → (0 · 0) = 0)
114112, 113ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 · 0) = 0
115114oveq1i 7281 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0 · 0) · i) = (0 · i)
1161, 1, 2mulassi 10987 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0 · 0) · i) = (0 · (0 · i))
117115, 116eqtr3i 2770 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 · i) = (0 · (0 · i))
118117a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (0 · (0 · i)))
119118oveq1d 7286 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (0 · (i · (0 − 𝑏)))) = ((0 · (0 · i)) + (0 · (i · (0 − 𝑏)))))
120111, 119eqtrd 2780 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i + (i · (0 − 𝑏)))) = ((0 · (0 · i)) + (0 · (i · (0 − 𝑏)))))
12115, 17, 109adddid 11000 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (1 + (0 − 𝑏))) = ((i · 1) + (i · (0 − 𝑏))))
12219a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 1) = i)
123122oveq1d 7286 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · 1) + (i · (0 − 𝑏))) = (i + (i · (0 − 𝑏))))
124121, 123eqtrd 2780 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (1 + (0 − 𝑏))) = (i + (i · (0 − 𝑏))))
125124oveq2d 7287 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 − 𝑏)))) = (0 · (i + (i · (0 − 𝑏)))))
12623, 41, 110adddid 11000 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · ((0 · i) + (i · (0 − 𝑏)))) = ((0 · (0 · i)) + (0 · (i · (0 − 𝑏)))))
127120, 125, 1263eqtr4d 2790 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 − 𝑏)))) = (0 · ((0 · i) + (i · (0 − 𝑏)))))
128103oveq1d 7286 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (i · 𝑏)) = (1 + (i · 𝑏)))
1295, 128eqtrd 2780 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (1 + (i · 𝑏)))
130129oveq1d 7286 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (i · (0 − 𝑏))) = ((1 + (i · 𝑏)) + (i · (0 − 𝑏))))
13117, 34, 110addassd 10998 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (i · 𝑏)) + (i · (0 − 𝑏))) = (1 + ((i · 𝑏) + (i · (0 − 𝑏)))))
132 renegid 40353 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑏 ∈ ℝ → (𝑏 + (0 − 𝑏)) = 0)
13332, 132syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑏 + (0 − 𝑏)) = 0)
134133oveq2d 7287 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (𝑏 + (0 − 𝑏))) = (i · 0))
13515, 33, 109adddid 11000 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (𝑏 + (0 − 𝑏))) = ((i · 𝑏) + (i · (0 − 𝑏))))
136 sn-mul01 40404 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (i ∈ ℂ → (i · 0) = 0)
1372, 136mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 0) = 0)
138134, 135, 1373eqtr3d 2788 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · 𝑏) + (i · (0 − 𝑏))) = 0)
139138oveq2d 7287 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((i · 𝑏) + (i · (0 − 𝑏)))) = (1 + 0))
140 readdid1 40389 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℝ → (1 + 0) = 1)
14154, 140ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 + 0) = 1
142139, 141eqtrdi 2796 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((i · 𝑏) + (i · (0 − 𝑏)))) = 1)
143131, 142eqtrd 2780 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (i · 𝑏)) + (i · (0 − 𝑏))) = 1)
144130, 143eqtrd 2780 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (i · (0 − 𝑏))) = 1)
145144oveq2d 7287 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · ((0 · i) + (i · (0 − 𝑏)))) = (0 · 1))
146127, 145eqtrd 2780 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 − 𝑏)))) = (0 · 1))
147 ax-1rid 10942 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℝ → (0 · 1) = 0)
148112, 147ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (0 · 1) = 0
149146, 148eqtrdi 2796 . . . . . . . . . . . . . . . . . 18 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 − 𝑏)))) = 0)
150149ad2antrr 723 . . . . . . . . . . . . . . . . 17 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (0 · (i · (1 + (0 − 𝑏)))) = 0)
151150oveq1d 7286 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → ((0 · (i · (1 + (0 − 𝑏)))) · 𝑦) = (0 · 𝑦))
152 0cnd 10969 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → 0 ∈ ℂ)
1532a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → i ∈ ℂ)
154 1cnd 10971 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → 1 ∈ ℂ)
155109ad2antrr 723 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (0 − 𝑏) ∈ ℂ)
156154, 155addcld 10995 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (1 + (0 − 𝑏)) ∈ ℂ)
157153, 156mulcld 10996 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (i · (1 + (0 − 𝑏))) ∈ ℂ)
158 simprl 768 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → 𝑦 ∈ ℝ)
159158recnd 11004 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → 𝑦 ∈ ℂ)
160152, 157, 159mulassd 10999 . . . . . . . . . . . . . . . . 17 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → ((0 · (i · (1 + (0 − 𝑏)))) · 𝑦) = (0 · ((i · (1 + (0 − 𝑏))) · 𝑦)))
161153, 156, 159mulassd 10999 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → ((i · (1 + (0 − 𝑏))) · 𝑦) = (i · ((1 + (0 − 𝑏)) · 𝑦)))
162 simprr 770 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → ((1 + (0 − 𝑏)) · 𝑦) = 1)
163162oveq2d 7287 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (i · ((1 + (0 − 𝑏)) · 𝑦)) = (i · 1))
164163, 19eqtrdi 2796 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (i · ((1 + (0 − 𝑏)) · 𝑦)) = i)
165161, 164eqtrd 2780 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → ((i · (1 + (0 − 𝑏))) · 𝑦) = i)
166165oveq2d 7287 . . . . . . . . . . . . . . . . 17 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (0 · ((i · (1 + (0 − 𝑏))) · 𝑦)) = (0 · i))
167160, 166eqtrd 2780 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → ((0 · (i · (1 + (0 − 𝑏)))) · 𝑦) = (0 · i))
168 remul02 40385 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ → (0 · 𝑦) = 0)
169158, 168syl 17 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (0 · 𝑦) = 0)
170151, 167, 1693eqtr3d 2788 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (0 · i) = 0)
171108, 170rexlimddv 3222 . . . . . . . . . . . . . 14 (((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) → (0 · i) = 0)
172171ex 413 . . . . . . . . . . . . 13 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 − 𝑏)) ≠ 0 → (0 · i) = 0))
173172necon1d 2967 . . . . . . . . . . . 12 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) ≠ 0 → (1 + (0 − 𝑏)) = 0))
1747, 173mpd 15 . . . . . . . . . . 11 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + (0 − 𝑏)) = 0)
175174oveq1d 7286 . . . . . . . . . 10 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 − 𝑏)) + 𝑏) = (0 + 𝑏))
17617, 109, 33addassd 10998 . . . . . . . . . . 11 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 − 𝑏)) + 𝑏) = (1 + ((0 − 𝑏) + 𝑏)))
177 renegid2 40393 . . . . . . . . . . . . . 14 (𝑏 ∈ ℝ → ((0 − 𝑏) + 𝑏) = 0)
17832, 177syl 17 . . . . . . . . . . . . 13 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 − 𝑏) + 𝑏) = 0)
179178oveq2d 7287 . . . . . . . . . . . 12 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((0 − 𝑏) + 𝑏)) = (1 + 0))
180179, 141eqtrdi 2796 . . . . . . . . . . 11 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((0 − 𝑏) + 𝑏)) = 1)
181176, 180eqtrd 2780 . . . . . . . . . 10 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 − 𝑏)) + 𝑏) = 1)
182 readdid2 40383 . . . . . . . . . . 11 (𝑏 ∈ ℝ → (0 + 𝑏) = 𝑏)
18332, 182syl 17 . . . . . . . . . 10 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 + 𝑏) = 𝑏)
184175, 181, 1833eqtr3rd 2789 . . . . . . . . 9 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 = 1)
185184oveq2d 7287 . . . . . . . 8 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 𝑏) = (i · 1))
186103, 185oveq12d 7289 . . . . . . 7 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (i · 𝑏)) = (1 + (i · 1)))
1875, 186eqtrd 2780 . . . . . 6 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (1 + (i · 1)))
18819oveq2i 7282 . . . . . . . . 9 (1 + (i · 1)) = (1 + i)
189188eqeq2i 2753 . . . . . . . 8 ((0 · i) = (1 + (i · 1)) ↔ (0 · i) = (1 + i))
190 oveq2 7279 . . . . . . . . . 10 ((0 · i) = (1 + i) → (((i · i) · i) · (0 · i)) = (((i · i) · i) · (1 + i)))
1912, 2mulcli 10983 . . . . . . . . . . . . 13 (i · i) ∈ ℂ
192191, 2mulcli 10983 . . . . . . . . . . . 12 ((i · i) · i) ∈ ℂ
193192, 1, 2mulassi 10987 . . . . . . . . . . 11 ((((i · i) · i) · 0) · i) = (((i · i) · i) · (0 · i))
194 sn-mul01 40404 . . . . . . . . . . . . 13 (((i · i) · i) ∈ ℂ → (((i · i) · i) · 0) = 0)
195192, 194ax-mp 5 . . . . . . . . . . . 12 (((i · i) · i) · 0) = 0
196195oveq1i 7281 . . . . . . . . . . 11 ((((i · i) · i) · 0) · i) = (0 · i)
197193, 196eqtr3i 2770 . . . . . . . . . 10 (((i · i) · i) · (0 · i)) = (0 · i)
198 ax-1cn 10930 . . . . . . . . . . . 12 1 ∈ ℂ
199192, 198, 2adddii 10988 . . . . . . . . . . 11 (((i · i) · i) · (1 + i)) = ((((i · i) · i) · 1) + (((i · i) · i) · i))
200191, 2, 198mulassi 10987 . . . . . . . . . . . . 13 (((i · i) · i) · 1) = ((i · i) · (i · 1))
20119oveq2i 7282 . . . . . . . . . . . . 13 ((i · i) · (i · 1)) = ((i · i) · i)
202200, 201eqtri 2768 . . . . . . . . . . . 12 (((i · i) · i) · 1) = ((i · i) · i)
203191, 2, 2mulassi 10987 . . . . . . . . . . . . 13 (((i · i) · i) · i) = ((i · i) · (i · i))
204 rei4 40402 . . . . . . . . . . . . 13 ((i · i) · (i · i)) = 1
205203, 204eqtri 2768 . . . . . . . . . . . 12 (((i · i) · i) · i) = 1
206202, 205oveq12i 7283 . . . . . . . . . . 11 ((((i · i) · i) · 1) + (((i · i) · i) · i)) = (((i · i) · i) + 1)
207199, 206eqtri 2768 . . . . . . . . . 10 (((i · i) · i) · (1 + i)) = (((i · i) · i) + 1)
208190, 197, 2073eqtr3g 2803 . . . . . . . . 9 ((0 · i) = (1 + i) → (0 · i) = (((i · i) · i) + 1))
20954, 54readdcli 10991 . . . . . . . . . . 11 (1 + 1) ∈ ℝ
210 df-2 12036 . . . . . . . . . . . 12 2 = (1 + 1)
211 sn-0ne2 40386 . . . . . . . . . . . . 13 0 ≠ 2
212211necomi 3000 . . . . . . . . . . . 12 2 ≠ 0
213210, 212eqnetrri 3017 . . . . . . . . . . 11 (1 + 1) ≠ 0
214 ax-rrecex 10944 . . . . . . . . . . 11 (((1 + 1) ∈ ℝ ∧ (1 + 1) ≠ 0) → ∃𝑧 ∈ ℝ ((1 + 1) · 𝑧) = 1)
215209, 213, 214mp2an 689 . . . . . . . . . 10 𝑧 ∈ ℝ ((1 + 1) · 𝑧) = 1
216192, 198addcli 10982 . . . . . . . . . . . . . . . . . 18 (((i · i) · i) + 1) ∈ ℂ
217198, 2, 216addassi 10986 . . . . . . . . . . . . . . . . 17 ((1 + i) + (((i · i) · i) + 1)) = (1 + (i + (((i · i) · i) + 1)))
2182, 192, 198addassi 10986 . . . . . . . . . . . . . . . . . 18 ((i + ((i · i) · i)) + 1) = (i + (((i · i) · i) + 1))
219218oveq2i 7282 . . . . . . . . . . . . . . . . 17 (1 + ((i + ((i · i) · i)) + 1)) = (1 + (i + (((i · i) · i) + 1)))
2202, 2, 2mulassi 10987 . . . . . . . . . . . . . . . . . . . . . 22 ((i · i) · i) = (i · (i · i))
221220oveq2i 7282 . . . . . . . . . . . . . . . . . . . . 21 (i + ((i · i) · i)) = (i + (i · (i · i)))
222 ipiiie0 40416 . . . . . . . . . . . . . . . . . . . . 21 (i + (i · (i · i))) = 0
223221, 222eqtri 2768 . . . . . . . . . . . . . . . . . . . 20 (i + ((i · i) · i)) = 0
224223oveq1i 7281 . . . . . . . . . . . . . . . . . . 19 ((i + ((i · i) · i)) + 1) = (0 + 1)
225224, 98eqtri 2768 . . . . . . . . . . . . . . . . . 18 ((i + ((i · i) · i)) + 1) = 1
226225oveq2i 7282 . . . . . . . . . . . . . . . . 17 (1 + ((i + ((i · i) · i)) + 1)) = (1 + 1)
227217, 219, 2263eqtr2i 2774 . . . . . . . . . . . . . . . 16 ((1 + i) + (((i · i) · i) + 1)) = (1 + 1)
228227a1i 11 . . . . . . . . . . . . . . 15 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((1 + i) + (((i · i) · i) + 1)) = (1 + 1))
2293, 198, 198adddii 10988 . . . . . . . . . . . . . . . 16 ((0 · i) · (1 + 1)) = (((0 · i) · 1) + ((0 · i) · 1))
2301, 2, 198mulassi 10987 . . . . . . . . . . . . . . . . . . 19 ((0 · i) · 1) = (0 · (i · 1))
23119oveq2i 7282 . . . . . . . . . . . . . . . . . . 19 (0 · (i · 1)) = (0 · i)
232230, 231eqtri 2768 . . . . . . . . . . . . . . . . . 18 ((0 · i) · 1) = (0 · i)
233 simpl 483 . . . . . . . . . . . . . . . . . 18 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (0 · i) = (1 + i))
234232, 233eqtrid 2792 . . . . . . . . . . . . . . . . 17 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · 1) = (1 + i))
235 simpr 485 . . . . . . . . . . . . . . . . . 18 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (0 · i) = (((i · i) · i) + 1))
236232, 235eqtrid 2792 . . . . . . . . . . . . . . . . 17 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · 1) = (((i · i) · i) + 1))
237234, 236oveq12d 7289 . . . . . . . . . . . . . . . 16 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (((0 · i) · 1) + ((0 · i) · 1)) = ((1 + i) + (((i · i) · i) + 1)))
238229, 237eqtrid 2792 . . . . . . . . . . . . . . 15 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · (1 + 1)) = ((1 + i) + (((i · i) · i) + 1)))
239 remulid2 40412 . . . . . . . . . . . . . . . 16 ((1 + 1) ∈ ℝ → (1 · (1 + 1)) = (1 + 1))
240209, 239mp1i 13 . . . . . . . . . . . . . . 15 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (1 · (1 + 1)) = (1 + 1))
241228, 238, 2403eqtr4d 2790 . . . . . . . . . . . . . 14 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · (1 + 1)) = (1 · (1 + 1)))
242241oveq1d 7286 . . . . . . . . . . . . 13 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (((0 · i) · (1 + 1)) · 𝑧) = ((1 · (1 + 1)) · 𝑧))
243242adantr 481 . . . . . . . . . . . 12 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (((0 · i) · (1 + 1)) · 𝑧) = ((1 · (1 + 1)) · 𝑧))
2443a1i 11 . . . . . . . . . . . . . 14 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (0 · i) ∈ ℂ)
245 1cnd 10971 . . . . . . . . . . . . . . 15 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 1 ∈ ℂ)
246245, 245addcld 10995 . . . . . . . . . . . . . 14 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (1 + 1) ∈ ℂ)
247 simprl 768 . . . . . . . . . . . . . . 15 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 𝑧 ∈ ℝ)
248247recnd 11004 . . . . . . . . . . . . . 14 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 𝑧 ∈ ℂ)
249244, 246, 248mulassd 10999 . . . . . . . . . . . . 13 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (((0 · i) · (1 + 1)) · 𝑧) = ((0 · i) · ((1 + 1) · 𝑧)))
250 simprr 770 . . . . . . . . . . . . . . 15 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((1 + 1) · 𝑧) = 1)
251250oveq2d 7287 . . . . . . . . . . . . . 14 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((0 · i) · ((1 + 1) · 𝑧)) = ((0 · i) · 1))
252251, 232eqtrdi 2796 . . . . . . . . . . . . 13 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((0 · i) · ((1 + 1) · 𝑧)) = (0 · i))
253249, 252eqtrd 2780 . . . . . . . . . . . 12 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (((0 · i) · (1 + 1)) · 𝑧) = (0 · i))
254245, 246, 248mulassd 10999 . . . . . . . . . . . . 13 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((1 · (1 + 1)) · 𝑧) = (1 · ((1 + 1) · 𝑧)))
255250oveq2d 7287 . . . . . . . . . . . . . 14 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (1 · ((1 + 1) · 𝑧)) = (1 · 1))
256 1t1e1ALT 40289 . . . . . . . . . . . . . 14 (1 · 1) = 1
257255, 256eqtrdi 2796 . . . . . . . . . . . . 13 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (1 · ((1 + 1) · 𝑧)) = 1)
258254, 257eqtrd 2780 . . . . . . . . . . . 12 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((1 · (1 + 1)) · 𝑧) = 1)
259243, 253, 2583eqtr3d 2788 . . . . . . . . . . 11 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (0 · i) = 1)
260259rexlimdvaa 3216 . . . . . . . . . 10 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (∃𝑧 ∈ ℝ ((1 + 1) · 𝑧) = 1 → (0 · i) = 1))
261215, 260mpi 20 . . . . . . . . 9 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (0 · i) = 1)
262208, 261mpdan 684 . . . . . . . 8 ((0 · i) = (1 + i) → (0 · i) = 1)
263189, 262sylbi 216 . . . . . . 7 ((0 · i) = (1 + (i · 1)) → (0 · i) = 1)
264 oveq2 7279 . . . . . . . 8 ((0 · i) = 1 → (0 · (0 · i)) = (0 · 1))
265116, 115eqtr3i 2770 . . . . . . . 8 (0 · (0 · i)) = (0 · i)
266264, 265, 1483eqtr3g 2803 . . . . . . 7 ((0 · i) = 1 → (0 · i) = 0)
267263, 266syl 17 . . . . . 6 ((0 · i) = (1 + (i · 1)) → (0 · i) = 0)
268187, 267syl 17 . . . . 5 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = 0)
269268pm2.18da 797 . . . 4 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) → (0 · i) = 0)
270269ex 413 . . 3 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((0 · i) = (𝑎 + (i · 𝑏)) → (0 · i) = 0))
271270rexlimivv 3223 . 2 (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (0 · i) = (𝑎 + (i · 𝑏)) → (0 · i) = 0)
2723, 4, 271mp2b 10 1 (0 · i) = 0
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 396   = wceq 1542  wcel 2110  wne 2945  wrex 3067  (class class class)co 7271  cc 10870  cr 10871  0cc0 10872  1c1 10873  ici 10874   + caddc 10875   · cmul 10877  2c2 12028   cresub 40345
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7582  ax-resscn 10929  ax-1cn 10930  ax-icn 10931  ax-addcl 10932  ax-addrcl 10933  ax-mulcl 10934  ax-mulrcl 10935  ax-addass 10937  ax-mulass 10938  ax-distr 10939  ax-i2m1 10940  ax-1ne0 10941  ax-1rid 10942  ax-rnegex 10943  ax-rrecex 10944  ax-cnre 10945  ax-pre-lttri 10946  ax-pre-lttrn 10947  ax-pre-ltadd 10948
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rmo 3074  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-po 5504  df-so 5505  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-riota 7228  df-ov 7274  df-oprab 7275  df-mpo 7276  df-er 8481  df-en 8717  df-dom 8718  df-sdom 8719  df-pnf 11012  df-mnf 11013  df-ltxr 11015  df-2 12036  df-3 12037  df-resub 40346
This theorem is referenced by:  sn-mul02  40419  retire  40434
  Copyright terms: Public domain W3C validator