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 39563
Description: Lemma for sn-mul02 39564. Commuted version of sn-it0e0 39539. (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 10626 . . 3 0 ∈ ℂ
2 ax-icn 10589 . . 3 i ∈ ℂ
31, 2mulcli 10641 . 2 (0 · i) ∈ ℂ
4 cnre 10631 . 2 ((0 · i) ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (0 · i) = (𝑎 + (i · 𝑏)))
5 simplr 768 . . . . . . 7 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (𝑎 + (i · 𝑏)))
6 neqne 2998 . . . . . . . . . . . 12 (¬ (0 · i) = 0 → (0 · i) ≠ 0)
76adantl 485 . . . . . . . . . . 11 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) ≠ 0)
8 simplll 774 . . . . . . . . . . . . . . . . 17 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 ∈ ℝ)
9 rernegcl 39496 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ ℝ → (0 − 𝑎) ∈ ℝ)
108, 9syl 17 . . . . . . . . . . . . . . . 16 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 − 𝑎) ∈ ℝ)
11 1red 10635 . . . . . . . . . . . . . . . 16 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 1 ∈ ℝ)
1210, 11readdcld 10663 . . . . . . . . . . . . . . 15 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 − 𝑎) + 1) ∈ ℝ)
13 ax-rrecex 10602 . . . . . . . . . . . . . . 15 ((((0 − 𝑎) + 1) ∈ ℝ ∧ ((0 − 𝑎) + 1) ≠ 0) → ∃𝑥 ∈ ℝ (((0 − 𝑎) + 1) · 𝑥) = 1)
1412, 13sylan 583 . . . . . . . . . . . . . 14 (((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) → ∃𝑥 ∈ ℝ (((0 − 𝑎) + 1) · 𝑥) = 1)
152a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → i ∈ ℂ)
1610recnd 10662 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 − 𝑎) ∈ ℂ)
17 1cnd 10629 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 1 ∈ ℂ)
1815, 16, 17adddid 10658 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · ((0 − 𝑎) + 1)) = ((i · (0 − 𝑎)) + (i · 1)))
19 it1ei 39560 . . . . . . . . . . . . . . . . . . . . . 22 (i · 1) = i
2019oveq2i 7150 . . . . . . . . . . . . . . . . . . . . 21 ((i · (0 − 𝑎)) + (i · 1)) = ((i · (0 − 𝑎)) + i)
2118, 20eqtrdi 2852 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · ((0 − 𝑎) + 1)) = ((i · (0 − 𝑎)) + i))
2221oveq2d 7155 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · ((0 − 𝑎) + 1))) = (0 · ((i · (0 − 𝑎)) + i)))
23 0cnd 10627 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 0 ∈ ℂ)
2415, 16mulcld 10654 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (0 − 𝑎)) ∈ ℂ)
2523, 24, 15adddid 10658 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · ((i · (0 − 𝑎)) + i)) = ((0 · (i · (0 − 𝑎))) + (0 · i)))
2622, 25eqtrd 2836 . . . . . . . . . . . . . . . . . 18 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · ((0 − 𝑎) + 1))) = ((0 · (i · (0 − 𝑎))) + (0 · i)))
275oveq2d 7155 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 − 𝑎) + (0 · i)) = ((0 − 𝑎) + (𝑎 + (i · 𝑏))))
28 renegid2 39538 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 ∈ ℝ → ((0 − 𝑎) + 𝑎) = 0)
2928ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 − 𝑎) + 𝑎) = 0)
3029oveq1d 7154 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 − 𝑎) + 𝑎) + (i · 𝑏)) = (0 + (i · 𝑏)))
318recnd 10662 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 ∈ ℂ)
32 simpllr 775 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 ∈ ℝ)
3332recnd 10662 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 ∈ ℂ)
3415, 33mulcld 10654 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 𝑏) ∈ ℂ)
3516, 31, 34addassd 10656 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 − 𝑎) + 𝑎) + (i · 𝑏)) = ((0 − 𝑎) + (𝑎 + (i · 𝑏))))
36 sn-addid2 39529 . . . . . . . . . . . . . . . . . . . . . . 23 ((i · 𝑏) ∈ ℂ → (0 + (i · 𝑏)) = (i · 𝑏))
3734, 36syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 + (i · 𝑏)) = (i · 𝑏))
3830, 35, 373eqtr3d 2844 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 − 𝑎) + (𝑎 + (i · 𝑏))) = (i · 𝑏))
3927, 38eqtrd 2836 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 − 𝑎) + (0 · i)) = (i · 𝑏))
4039oveq2d 7155 . . . . . . . . . . . . . . . . . . 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 10658 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · ((0 − 𝑎) + (0 · i))) = (((0 · i) · (0 − 𝑎)) + ((0 · i) · (0 · i))))
4323, 15, 16mulassd 10657 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (0 − 𝑎)) = (0 · (i · (0 − 𝑎))))
4441, 23, 15mulassd 10657 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 · i) · 0) · i) = ((0 · i) · (0 · i)))
45 sn-mul01 39549 . . . . . . . . . . . . . . . . . . . . . . . 24 ((0 · i) ∈ ℂ → ((0 · i) · 0) = 0)
4641, 45syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · 0) = 0)
4746oveq1d 7154 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 · i) · 0) · i) = (0 · i))
4844, 47eqtr3d 2838 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (0 · i)) = (0 · i))
4943, 48oveq12d 7157 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 · i) · (0 − 𝑎)) + ((0 · i) · (0 · i))) = ((0 · (i · (0 − 𝑎))) + (0 · i)))
5042, 49eqtrd 2836 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · ((0 − 𝑎) + (0 · i))) = ((0 · (i · (0 − 𝑎))) + (0 · i)))
5123, 15, 34mulassd 10657 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (i · 𝑏)) = (0 · (i · (i · 𝑏))))
5215, 15, 33mulassd 10657 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · i) · 𝑏) = (i · (i · 𝑏)))
53 reixi 39546 . . . . . . . . . . . . . . . . . . . . . . . . 25 (i · i) = (0 − 1)
54 1re 10634 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ ℝ
55 rernegcl 39496 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 ∈ ℝ → (0 − 1) ∈ ℝ)
5654, 55ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 − 1) ∈ ℝ
5753, 56eqeltri 2889 . . . . . . . . . . . . . . . . . . . . . . . 24 (i · i) ∈ ℝ
5857a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · i) ∈ ℝ)
5958, 32remulcld 10664 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · i) · 𝑏) ∈ ℝ)
6052, 59eqeltrrd 2894 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (i · 𝑏)) ∈ ℝ)
61 remul02 39530 . . . . . . . . . . . . . . . . . . . . 21 ((i · (i · 𝑏)) ∈ ℝ → (0 · (i · (i · 𝑏))) = 0)
6260, 61syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (i · 𝑏))) = 0)
6351, 62eqtrd 2836 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (i · 𝑏)) = 0)
6440, 50, 633eqtr3d 2844 . . . . . . . . . . . . . . . . . 18 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · (i · (0 − 𝑎))) + (0 · i)) = 0)
6526, 64eqtrd 2836 . . . . . . . . . . . . . . . . 17 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · ((0 − 𝑎) + 1))) = 0)
6665ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (0 · (i · ((0 − 𝑎) + 1))) = 0)
6766oveq1d 7154 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → ((0 · (i · ((0 − 𝑎) + 1))) · 𝑥) = (0 · 𝑥))
68 0cnd 10627 . . . . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (0 − 𝑎) ∈ ℝ)
7170recnd 10662 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (0 − 𝑎) ∈ ℂ)
72 1cnd 10629 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → 1 ∈ ℂ)
7371, 72addcld 10653 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → ((0 − 𝑎) + 1) ∈ ℂ)
7469, 73mulcld 10654 . . . . . . . . . . . . . . . . 17 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (i · ((0 − 𝑎) + 1)) ∈ ℂ)
75 simprl 770 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → 𝑥 ∈ ℝ)
7675recnd 10662 . . . . . . . . . . . . . . . . 17 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → 𝑥 ∈ ℂ)
7768, 74, 76mulassd 10657 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → ((0 · (i · ((0 − 𝑎) + 1))) · 𝑥) = (0 · ((i · ((0 − 𝑎) + 1)) · 𝑥)))
7869, 73, 76mulassd 10657 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → ((i · ((0 − 𝑎) + 1)) · 𝑥) = (i · (((0 − 𝑎) + 1) · 𝑥)))
79 simprr 772 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (((0 − 𝑎) + 1) · 𝑥) = 1)
8079oveq2d 7155 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (i · (((0 − 𝑎) + 1) · 𝑥)) = (i · 1))
8180, 19eqtrdi 2852 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (i · (((0 − 𝑎) + 1) · 𝑥)) = i)
8278, 81eqtrd 2836 . . . . . . . . . . . . . . . . 17 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → ((i · ((0 − 𝑎) + 1)) · 𝑥) = i)
8382oveq2d 7155 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (0 · ((i · ((0 − 𝑎) + 1)) · 𝑥)) = (0 · i))
8477, 83eqtrd 2836 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → ((0 · (i · ((0 − 𝑎) + 1))) · 𝑥) = (0 · i))
85 remul02 39530 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → (0 · 𝑥) = 0)
8675, 85syl 17 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (0 · 𝑥) = 0)
8767, 84, 863eqtr3d 2844 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (0 · i) = 0)
8814, 87rexlimddv 3253 . . . . . . . . . . . . 13 (((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) → (0 · i) = 0)
8988ex 416 . . . . . . . . . . . 12 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 − 𝑎) + 1) ≠ 0 → (0 · i) = 0))
9089necon1d 3012 . . . . . . . . . . 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 7155 . . . . . . . . 9 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + ((0 − 𝑎) + 1)) = (𝑎 + 0))
9331, 16, 17addassd 10656 . . . . . . . . . 10 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 − 𝑎)) + 1) = (𝑎 + ((0 − 𝑎) + 1)))
94 renegid 39498 . . . . . . . . . . . . 13 (𝑎 ∈ ℝ → (𝑎 + (0 − 𝑎)) = 0)
958, 94syl 17 . . . . . . . . . . . 12 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (0 − 𝑎)) = 0)
9695oveq1d 7154 . . . . . . . . . . 11 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 − 𝑎)) + 1) = (0 + 1))
97 readdid2 39528 . . . . . . . . . . . 12 (1 ∈ ℝ → (0 + 1) = 1)
9854, 97ax-mp 5 . . . . . . . . . . 11 (0 + 1) = 1
9996, 98eqtrdi 2852 . . . . . . . . . 10 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 − 𝑎)) + 1) = 1)
10093, 99eqtr3d 2838 . . . . . . . . 9 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + ((0 − 𝑎) + 1)) = 1)
101 readdid1 39534 . . . . . . . . . 10 (𝑎 ∈ ℝ → (𝑎 + 0) = 𝑎)
1028, 101syl 17 . . . . . . . . 9 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + 0) = 𝑎)
10392, 100, 1023eqtr3rd 2845 . . . . . . . 8 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 = 1)
104 rernegcl 39496 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ ℝ → (0 − 𝑏) ∈ ℝ)
10532, 104syl 17 . . . . . . . . . . . . . . . . 17 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 − 𝑏) ∈ ℝ)
10611, 105readdcld 10663 . . . . . . . . . . . . . . . 16 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + (0 − 𝑏)) ∈ ℝ)
107 ax-rrecex 10602 . . . . . . . . . . . . . . . 16 (((1 + (0 − 𝑏)) ∈ ℝ ∧ (1 + (0 − 𝑏)) ≠ 0) → ∃𝑦 ∈ ℝ ((1 + (0 − 𝑏)) · 𝑦) = 1)
108106, 107sylan 583 . . . . . . . . . . . . . . 15 (((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) → ∃𝑦 ∈ ℝ ((1 + (0 − 𝑏)) · 𝑦) = 1)
109105recnd 10662 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 − 𝑏) ∈ ℂ)
11015, 109mulcld 10654 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (0 − 𝑏)) ∈ ℂ)
11123, 15, 110adddid 10658 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i + (i · (0 − 𝑏)))) = ((0 · i) + (0 · (i · (0 − 𝑏)))))
112 0re 10636 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ∈ ℝ
113 remul02 39530 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (0 ∈ ℝ → (0 · 0) = 0)
114112, 113ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 · 0) = 0
115114oveq1i 7149 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0 · 0) · i) = (0 · i)
1161, 1, 2mulassi 10645 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0 · 0) · i) = (0 · (0 · i))
117115, 116eqtr3i 2826 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 · i) = (0 · (0 · i))
118117a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (0 · (0 · i)))
119118oveq1d 7154 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (0 · (i · (0 − 𝑏)))) = ((0 · (0 · i)) + (0 · (i · (0 − 𝑏)))))
120111, 119eqtrd 2836 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i + (i · (0 − 𝑏)))) = ((0 · (0 · i)) + (0 · (i · (0 − 𝑏)))))
12115, 17, 109adddid 10658 . . . . . . . . . . . . . . . . . . . . . . 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 7154 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · 1) + (i · (0 − 𝑏))) = (i + (i · (0 − 𝑏))))
124121, 123eqtrd 2836 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (1 + (0 − 𝑏))) = (i + (i · (0 − 𝑏))))
125124oveq2d 7155 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 − 𝑏)))) = (0 · (i + (i · (0 − 𝑏)))))
12623, 41, 110adddid 10658 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · ((0 · i) + (i · (0 − 𝑏)))) = ((0 · (0 · i)) + (0 · (i · (0 − 𝑏)))))
127120, 125, 1263eqtr4d 2846 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 − 𝑏)))) = (0 · ((0 · i) + (i · (0 − 𝑏)))))
128103oveq1d 7154 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (i · 𝑏)) = (1 + (i · 𝑏)))
1295, 128eqtrd 2836 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (1 + (i · 𝑏)))
130129oveq1d 7154 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (i · (0 − 𝑏))) = ((1 + (i · 𝑏)) + (i · (0 − 𝑏))))
13117, 34, 110addassd 10656 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (i · 𝑏)) + (i · (0 − 𝑏))) = (1 + ((i · 𝑏) + (i · (0 − 𝑏)))))
132 renegid 39498 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑏 ∈ ℝ → (𝑏 + (0 − 𝑏)) = 0)
13332, 132syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑏 + (0 − 𝑏)) = 0)
134133oveq2d 7155 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (𝑏 + (0 − 𝑏))) = (i · 0))
13515, 33, 109adddid 10658 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (𝑏 + (0 − 𝑏))) = ((i · 𝑏) + (i · (0 − 𝑏))))
136 sn-mul01 39549 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (i ∈ ℂ → (i · 0) = 0)
1372, 136mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 0) = 0)
138134, 135, 1373eqtr3d 2844 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · 𝑏) + (i · (0 − 𝑏))) = 0)
139138oveq2d 7155 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((i · 𝑏) + (i · (0 − 𝑏)))) = (1 + 0))
140 readdid1 39534 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℝ → (1 + 0) = 1)
14154, 140ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 + 0) = 1
142139, 141eqtrdi 2852 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((i · 𝑏) + (i · (0 − 𝑏)))) = 1)
143131, 142eqtrd 2836 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (i · 𝑏)) + (i · (0 − 𝑏))) = 1)
144130, 143eqtrd 2836 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (i · (0 − 𝑏))) = 1)
145144oveq2d 7155 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · ((0 · i) + (i · (0 − 𝑏)))) = (0 · 1))
146127, 145eqtrd 2836 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 − 𝑏)))) = (0 · 1))
147 ax-1rid 10600 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℝ → (0 · 1) = 0)
148112, 147ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (0 · 1) = 0
149146, 148eqtrdi 2852 . . . . . . . . . . . . . . . . . 18 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 − 𝑏)))) = 0)
150149ad2antrr 725 . . . . . . . . . . . . . . . . 17 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (0 · (i · (1 + (0 − 𝑏)))) = 0)
151150oveq1d 7154 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → ((0 · (i · (1 + (0 − 𝑏)))) · 𝑦) = (0 · 𝑦))
152 0cnd 10627 . . . . . . . . . . . . . . . . . 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 10629 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → 1 ∈ ℂ)
155109ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (0 − 𝑏) ∈ ℂ)
156154, 155addcld 10653 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (1 + (0 − 𝑏)) ∈ ℂ)
157153, 156mulcld 10654 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (i · (1 + (0 − 𝑏))) ∈ ℂ)
158 simprl 770 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → 𝑦 ∈ ℝ)
159158recnd 10662 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → 𝑦 ∈ ℂ)
160152, 157, 159mulassd 10657 . . . . . . . . . . . . . . . . 17 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → ((0 · (i · (1 + (0 − 𝑏)))) · 𝑦) = (0 · ((i · (1 + (0 − 𝑏))) · 𝑦)))
161153, 156, 159mulassd 10657 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → ((i · (1 + (0 − 𝑏))) · 𝑦) = (i · ((1 + (0 − 𝑏)) · 𝑦)))
162 simprr 772 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → ((1 + (0 − 𝑏)) · 𝑦) = 1)
163162oveq2d 7155 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (i · ((1 + (0 − 𝑏)) · 𝑦)) = (i · 1))
164163, 19eqtrdi 2852 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (i · ((1 + (0 − 𝑏)) · 𝑦)) = i)
165161, 164eqtrd 2836 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → ((i · (1 + (0 − 𝑏))) · 𝑦) = i)
166165oveq2d 7155 . . . . . . . . . . . . . . . . 17 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (0 · ((i · (1 + (0 − 𝑏))) · 𝑦)) = (0 · i))
167160, 166eqtrd 2836 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → ((0 · (i · (1 + (0 − 𝑏)))) · 𝑦) = (0 · i))
168 remul02 39530 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ → (0 · 𝑦) = 0)
169158, 168syl 17 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (0 · 𝑦) = 0)
170151, 167, 1693eqtr3d 2844 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (0 · i) = 0)
171108, 170rexlimddv 3253 . . . . . . . . . . . . . 14 (((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) → (0 · i) = 0)
172171ex 416 . . . . . . . . . . . . 13 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 − 𝑏)) ≠ 0 → (0 · i) = 0))
173172necon1d 3012 . . . . . . . . . . . 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 7154 . . . . . . . . . 10 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 − 𝑏)) + 𝑏) = (0 + 𝑏))
17617, 109, 33addassd 10656 . . . . . . . . . . 11 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 − 𝑏)) + 𝑏) = (1 + ((0 − 𝑏) + 𝑏)))
177 renegid2 39538 . . . . . . . . . . . . . 14 (𝑏 ∈ ℝ → ((0 − 𝑏) + 𝑏) = 0)
17832, 177syl 17 . . . . . . . . . . . . 13 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 − 𝑏) + 𝑏) = 0)
179178oveq2d 7155 . . . . . . . . . . . 12 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((0 − 𝑏) + 𝑏)) = (1 + 0))
180179, 141eqtrdi 2852 . . . . . . . . . . 11 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((0 − 𝑏) + 𝑏)) = 1)
181176, 180eqtrd 2836 . . . . . . . . . 10 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 − 𝑏)) + 𝑏) = 1)
182 readdid2 39528 . . . . . . . . . . 11 (𝑏 ∈ ℝ → (0 + 𝑏) = 𝑏)
18332, 182syl 17 . . . . . . . . . 10 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 + 𝑏) = 𝑏)
184175, 181, 1833eqtr3rd 2845 . . . . . . . . 9 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 = 1)
185184oveq2d 7155 . . . . . . . 8 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 𝑏) = (i · 1))
186103, 185oveq12d 7157 . . . . . . 7 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (i · 𝑏)) = (1 + (i · 1)))
1875, 186eqtrd 2836 . . . . . 6 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (1 + (i · 1)))
18819oveq2i 7150 . . . . . . . . 9 (1 + (i · 1)) = (1 + i)
189188eqeq2i 2814 . . . . . . . 8 ((0 · i) = (1 + (i · 1)) ↔ (0 · i) = (1 + i))
190 oveq2 7147 . . . . . . . . . 10 ((0 · i) = (1 + i) → (((i · i) · i) · (0 · i)) = (((i · i) · i) · (1 + i)))
1912, 2mulcli 10641 . . . . . . . . . . . . 13 (i · i) ∈ ℂ
192191, 2mulcli 10641 . . . . . . . . . . . 12 ((i · i) · i) ∈ ℂ
193192, 1, 2mulassi 10645 . . . . . . . . . . 11 ((((i · i) · i) · 0) · i) = (((i · i) · i) · (0 · i))
194 sn-mul01 39549 . . . . . . . . . . . . 13 (((i · i) · i) ∈ ℂ → (((i · i) · i) · 0) = 0)
195192, 194ax-mp 5 . . . . . . . . . . . 12 (((i · i) · i) · 0) = 0
196195oveq1i 7149 . . . . . . . . . . 11 ((((i · i) · i) · 0) · i) = (0 · i)
197193, 196eqtr3i 2826 . . . . . . . . . 10 (((i · i) · i) · (0 · i)) = (0 · i)
198 ax-1cn 10588 . . . . . . . . . . . 12 1 ∈ ℂ
199192, 198, 2adddii 10646 . . . . . . . . . . 11 (((i · i) · i) · (1 + i)) = ((((i · i) · i) · 1) + (((i · i) · i) · i))
200191, 2, 198mulassi 10645 . . . . . . . . . . . . 13 (((i · i) · i) · 1) = ((i · i) · (i · 1))
20119oveq2i 7150 . . . . . . . . . . . . 13 ((i · i) · (i · 1)) = ((i · i) · i)
202200, 201eqtri 2824 . . . . . . . . . . . 12 (((i · i) · i) · 1) = ((i · i) · i)
203191, 2, 2mulassi 10645 . . . . . . . . . . . . 13 (((i · i) · i) · i) = ((i · i) · (i · i))
204 rei4 39547 . . . . . . . . . . . . 13 ((i · i) · (i · i)) = 1
205203, 204eqtri 2824 . . . . . . . . . . . 12 (((i · i) · i) · i) = 1
206202, 205oveq12i 7151 . . . . . . . . . . 11 ((((i · i) · i) · 1) + (((i · i) · i) · i)) = (((i · i) · i) + 1)
207199, 206eqtri 2824 . . . . . . . . . 10 (((i · i) · i) · (1 + i)) = (((i · i) · i) + 1)
208190, 197, 2073eqtr3g 2859 . . . . . . . . 9 ((0 · i) = (1 + i) → (0 · i) = (((i · i) · i) + 1))
20954, 54readdcli 10649 . . . . . . . . . . 11 (1 + 1) ∈ ℝ
210 df-2 11692 . . . . . . . . . . . 12 2 = (1 + 1)
211 sn-0ne2 39531 . . . . . . . . . . . . 13 0 ≠ 2
212211necomi 3044 . . . . . . . . . . . 12 2 ≠ 0
213210, 212eqnetrri 3061 . . . . . . . . . . 11 (1 + 1) ≠ 0
214 ax-rrecex 10602 . . . . . . . . . . 11 (((1 + 1) ∈ ℝ ∧ (1 + 1) ≠ 0) → ∃𝑧 ∈ ℝ ((1 + 1) · 𝑧) = 1)
215209, 213, 214mp2an 691 . . . . . . . . . 10 𝑧 ∈ ℝ ((1 + 1) · 𝑧) = 1
216192, 198addcli 10640 . . . . . . . . . . . . . . . . . 18 (((i · i) · i) + 1) ∈ ℂ
217198, 2, 216addassi 10644 . . . . . . . . . . . . . . . . 17 ((1 + i) + (((i · i) · i) + 1)) = (1 + (i + (((i · i) · i) + 1)))
2182, 192, 198addassi 10644 . . . . . . . . . . . . . . . . . 18 ((i + ((i · i) · i)) + 1) = (i + (((i · i) · i) + 1))
219218oveq2i 7150 . . . . . . . . . . . . . . . . 17 (1 + ((i + ((i · i) · i)) + 1)) = (1 + (i + (((i · i) · i) + 1)))
2202, 2, 2mulassi 10645 . . . . . . . . . . . . . . . . . . . . . 22 ((i · i) · i) = (i · (i · i))
221220oveq2i 7150 . . . . . . . . . . . . . . . . . . . . 21 (i + ((i · i) · i)) = (i + (i · (i · i)))
222 ipiiie0 39561 . . . . . . . . . . . . . . . . . . . . 21 (i + (i · (i · i))) = 0
223221, 222eqtri 2824 . . . . . . . . . . . . . . . . . . . 20 (i + ((i · i) · i)) = 0
224223oveq1i 7149 . . . . . . . . . . . . . . . . . . 19 ((i + ((i · i) · i)) + 1) = (0 + 1)
225224, 98eqtri 2824 . . . . . . . . . . . . . . . . . 18 ((i + ((i · i) · i)) + 1) = 1
226225oveq2i 7150 . . . . . . . . . . . . . . . . 17 (1 + ((i + ((i · i) · i)) + 1)) = (1 + 1)
227217, 219, 2263eqtr2i 2830 . . . . . . . . . . . . . . . 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 10646 . . . . . . . . . . . . . . . 16 ((0 · i) · (1 + 1)) = (((0 · i) · 1) + ((0 · i) · 1))
2301, 2, 198mulassi 10645 . . . . . . . . . . . . . . . . . . 19 ((0 · i) · 1) = (0 · (i · 1))
23119oveq2i 7150 . . . . . . . . . . . . . . . . . . 19 (0 · (i · 1)) = (0 · i)
232230, 231eqtri 2824 . . . . . . . . . . . . . . . . . 18 ((0 · i) · 1) = (0 · i)
233 simpl 486 . . . . . . . . . . . . . . . . . 18 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (0 · i) = (1 + i))
234232, 233syl5eq 2848 . . . . . . . . . . . . . . . . 17 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · 1) = (1 + i))
235 simpr 488 . . . . . . . . . . . . . . . . . 18 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (0 · i) = (((i · i) · i) + 1))
236232, 235syl5eq 2848 . . . . . . . . . . . . . . . . 17 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · 1) = (((i · i) · i) + 1))
237234, 236oveq12d 7157 . . . . . . . . . . . . . . . 16 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (((0 · i) · 1) + ((0 · i) · 1)) = ((1 + i) + (((i · i) · i) + 1)))
238229, 237syl5eq 2848 . . . . . . . . . . . . . . 15 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · (1 + 1)) = ((1 + i) + (((i · i) · i) + 1)))
239 remulid2 39557 . . . . . . . . . . . . . . . 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 2846 . . . . . . . . . . . . . 14 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · (1 + 1)) = (1 · (1 + 1)))
242241oveq1d 7154 . . . . . . . . . . . . 13 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (((0 · i) · (1 + 1)) · 𝑧) = ((1 · (1 + 1)) · 𝑧))
243242adantr 484 . . . . . . . . . . . 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 10629 . . . . . . . . . . . . . . 15 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 1 ∈ ℂ)
246245, 245addcld 10653 . . . . . . . . . . . . . 14 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (1 + 1) ∈ ℂ)
247 simprl 770 . . . . . . . . . . . . . . 15 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 𝑧 ∈ ℝ)
248247recnd 10662 . . . . . . . . . . . . . 14 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 𝑧 ∈ ℂ)
249244, 246, 248mulassd 10657 . . . . . . . . . . . . 13 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (((0 · i) · (1 + 1)) · 𝑧) = ((0 · i) · ((1 + 1) · 𝑧)))
250 simprr 772 . . . . . . . . . . . . . . 15 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((1 + 1) · 𝑧) = 1)
251250oveq2d 7155 . . . . . . . . . . . . . 14 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((0 · i) · ((1 + 1) · 𝑧)) = ((0 · i) · 1))
252251, 232eqtrdi 2852 . . . . . . . . . . . . 13 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((0 · i) · ((1 + 1) · 𝑧)) = (0 · i))
253249, 252eqtrd 2836 . . . . . . . . . . . 12 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (((0 · i) · (1 + 1)) · 𝑧) = (0 · i))
254245, 246, 248mulassd 10657 . . . . . . . . . . . . 13 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((1 · (1 + 1)) · 𝑧) = (1 · ((1 + 1) · 𝑧)))
255250oveq2d 7155 . . . . . . . . . . . . . 14 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (1 · ((1 + 1) · 𝑧)) = (1 · 1))
256 1t1e1ALT 39450 . . . . . . . . . . . . . 14 (1 · 1) = 1
257255, 256eqtrdi 2852 . . . . . . . . . . . . 13 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (1 · ((1 + 1) · 𝑧)) = 1)
258254, 257eqtrd 2836 . . . . . . . . . . . 12 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((1 · (1 + 1)) · 𝑧) = 1)
259243, 253, 2583eqtr3d 2844 . . . . . . . . . . 11 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (0 · i) = 1)
260259rexlimdvaa 3247 . . . . . . . . . 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 686 . . . . . . . 8 ((0 · i) = (1 + i) → (0 · i) = 1)
263189, 262sylbi 220 . . . . . . 7 ((0 · i) = (1 + (i · 1)) → (0 · i) = 1)
264 oveq2 7147 . . . . . . . 8 ((0 · i) = 1 → (0 · (0 · i)) = (0 · 1))
265116, 115eqtr3i 2826 . . . . . . . 8 (0 · (0 · i)) = (0 · i)
266264, 265, 1483eqtr3g 2859 . . . . . . 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 799 . . . 4 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) → (0 · i) = 0)
270269ex 416 . . 3 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((0 · i) = (𝑎 + (i · 𝑏)) → (0 · i) = 0))
271270rexlimivv 3254 . 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 399   = wceq 1538  wcel 2112  wne 2990  wrex 3110  (class class class)co 7139  cc 10528  cr 10529  0cc0 10530  1c1 10531  ici 10532   + caddc 10533   · cmul 10535  2c2 11684   cresub 39490
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-po 5442  df-so 5443  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10670  df-mnf 10671  df-ltxr 10673  df-2 11692  df-3 11693  df-resub 39491
This theorem is referenced by:  sn-mul02  39564  retire  39579
  Copyright terms: Public domain W3C validator