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 40894
Description: Lemma for sn-mul02 40895. Commuted version of sn-it0e0 40870. (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 11147 . . 3 0 ∈ ℂ
2 ax-icn 11110 . . 3 i ∈ ℂ
31, 2mulcli 11162 . 2 (0 · i) ∈ ℂ
4 cnre 11152 . 2 ((0 · i) ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (0 · i) = (𝑎 + (i · 𝑏)))
5 simplr 767 . . . . . . 7 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (𝑎 + (i · 𝑏)))
6 neqne 2951 . . . . . . . . . . . 12 (¬ (0 · i) = 0 → (0 · i) ≠ 0)
76adantl 482 . . . . . . . . . . 11 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) ≠ 0)
8 simplll 773 . . . . . . . . . . . . . . . . 17 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 ∈ ℝ)
9 rernegcl 40826 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ ℝ → (0 − 𝑎) ∈ ℝ)
108, 9syl 17 . . . . . . . . . . . . . . . 16 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 − 𝑎) ∈ ℝ)
11 1red 11156 . . . . . . . . . . . . . . . 16 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 1 ∈ ℝ)
1210, 11readdcld 11184 . . . . . . . . . . . . . . 15 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 − 𝑎) + 1) ∈ ℝ)
13 ax-rrecex 11123 . . . . . . . . . . . . . . 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 11183 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 − 𝑎) ∈ ℂ)
17 1cnd 11150 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 1 ∈ ℂ)
1815, 16, 17adddid 11179 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · ((0 − 𝑎) + 1)) = ((i · (0 − 𝑎)) + (i · 1)))
19 it1ei 40891 . . . . . . . . . . . . . . . . . . . . . 22 (i · 1) = i
2019oveq2i 7368 . . . . . . . . . . . . . . . . . . . . 21 ((i · (0 − 𝑎)) + (i · 1)) = ((i · (0 − 𝑎)) + i)
2118, 20eqtrdi 2792 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · ((0 − 𝑎) + 1)) = ((i · (0 − 𝑎)) + i))
2221oveq2d 7373 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · ((0 − 𝑎) + 1))) = (0 · ((i · (0 − 𝑎)) + i)))
23 0cnd 11148 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 0 ∈ ℂ)
2415, 16mulcld 11175 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (0 − 𝑎)) ∈ ℂ)
2523, 24, 15adddid 11179 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · ((i · (0 − 𝑎)) + i)) = ((0 · (i · (0 − 𝑎))) + (0 · i)))
2622, 25eqtrd 2776 . . . . . . . . . . . . . . . . . 18 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · ((0 − 𝑎) + 1))) = ((0 · (i · (0 − 𝑎))) + (0 · i)))
275oveq2d 7373 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 − 𝑎) + (0 · i)) = ((0 − 𝑎) + (𝑎 + (i · 𝑏))))
28 renegid2 40868 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 ∈ ℝ → ((0 − 𝑎) + 𝑎) = 0)
2928ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 − 𝑎) + 𝑎) = 0)
3029oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 − 𝑎) + 𝑎) + (i · 𝑏)) = (0 + (i · 𝑏)))
318recnd 11183 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 ∈ ℂ)
32 simpllr 774 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 ∈ ℝ)
3332recnd 11183 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 ∈ ℂ)
3415, 33mulcld 11175 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 𝑏) ∈ ℂ)
3516, 31, 34addassd 11177 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 − 𝑎) + 𝑎) + (i · 𝑏)) = ((0 − 𝑎) + (𝑎 + (i · 𝑏))))
36 sn-addid2 40859 . . . . . . . . . . . . . . . . . . . . . . 23 ((i · 𝑏) ∈ ℂ → (0 + (i · 𝑏)) = (i · 𝑏))
3734, 36syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 + (i · 𝑏)) = (i · 𝑏))
3830, 35, 373eqtr3d 2784 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 − 𝑎) + (𝑎 + (i · 𝑏))) = (i · 𝑏))
3927, 38eqtrd 2776 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 − 𝑎) + (0 · i)) = (i · 𝑏))
4039oveq2d 7373 . . . . . . . . . . . . . . . . . . 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 11179 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · ((0 − 𝑎) + (0 · i))) = (((0 · i) · (0 − 𝑎)) + ((0 · i) · (0 · i))))
4323, 15, 16mulassd 11178 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (0 − 𝑎)) = (0 · (i · (0 − 𝑎))))
4441, 23, 15mulassd 11178 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 · i) · 0) · i) = ((0 · i) · (0 · i)))
45 sn-mul01 40880 . . . . . . . . . . . . . . . . . . . . . . . 24 ((0 · i) ∈ ℂ → ((0 · i) · 0) = 0)
4641, 45syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · 0) = 0)
4746oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 · i) · 0) · i) = (0 · i))
4844, 47eqtr3d 2778 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (0 · i)) = (0 · i))
4943, 48oveq12d 7375 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 · i) · (0 − 𝑎)) + ((0 · i) · (0 · i))) = ((0 · (i · (0 − 𝑎))) + (0 · i)))
5042, 49eqtrd 2776 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · ((0 − 𝑎) + (0 · i))) = ((0 · (i · (0 − 𝑎))) + (0 · i)))
5123, 15, 34mulassd 11178 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (i · 𝑏)) = (0 · (i · (i · 𝑏))))
5215, 15, 33mulassd 11178 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · i) · 𝑏) = (i · (i · 𝑏)))
53 reixi 40877 . . . . . . . . . . . . . . . . . . . . . . . . 25 (i · i) = (0 − 1)
54 1re 11155 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ ℝ
55 rernegcl 40826 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 ∈ ℝ → (0 − 1) ∈ ℝ)
5654, 55ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 − 1) ∈ ℝ
5753, 56eqeltri 2834 . . . . . . . . . . . . . . . . . . . . . . . 24 (i · i) ∈ ℝ
5857a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · i) ∈ ℝ)
5958, 32remulcld 11185 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · i) · 𝑏) ∈ ℝ)
6052, 59eqeltrrd 2839 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (i · 𝑏)) ∈ ℝ)
61 remul02 40860 . . . . . . . . . . . . . . . . . . . . 21 ((i · (i · 𝑏)) ∈ ℝ → (0 · (i · (i · 𝑏))) = 0)
6260, 61syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (i · 𝑏))) = 0)
6351, 62eqtrd 2776 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (i · 𝑏)) = 0)
6440, 50, 633eqtr3d 2784 . . . . . . . . . . . . . . . . . 18 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · (i · (0 − 𝑎))) + (0 · i)) = 0)
6526, 64eqtrd 2776 . . . . . . . . . . . . . . . . 17 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · ((0 − 𝑎) + 1))) = 0)
6665ad2antrr 724 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (0 · (i · ((0 − 𝑎) + 1))) = 0)
6766oveq1d 7372 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → ((0 · (i · ((0 − 𝑎) + 1))) · 𝑥) = (0 · 𝑥))
68 0cnd 11148 . . . . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (0 − 𝑎) ∈ ℝ)
7170recnd 11183 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (0 − 𝑎) ∈ ℂ)
72 1cnd 11150 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → 1 ∈ ℂ)
7371, 72addcld 11174 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → ((0 − 𝑎) + 1) ∈ ℂ)
7469, 73mulcld 11175 . . . . . . . . . . . . . . . . 17 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (i · ((0 − 𝑎) + 1)) ∈ ℂ)
75 simprl 769 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → 𝑥 ∈ ℝ)
7675recnd 11183 . . . . . . . . . . . . . . . . 17 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → 𝑥 ∈ ℂ)
7768, 74, 76mulassd 11178 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → ((0 · (i · ((0 − 𝑎) + 1))) · 𝑥) = (0 · ((i · ((0 − 𝑎) + 1)) · 𝑥)))
7869, 73, 76mulassd 11178 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → ((i · ((0 − 𝑎) + 1)) · 𝑥) = (i · (((0 − 𝑎) + 1) · 𝑥)))
79 simprr 771 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (((0 − 𝑎) + 1) · 𝑥) = 1)
8079oveq2d 7373 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (i · (((0 − 𝑎) + 1) · 𝑥)) = (i · 1))
8180, 19eqtrdi 2792 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (i · (((0 − 𝑎) + 1) · 𝑥)) = i)
8278, 81eqtrd 2776 . . . . . . . . . . . . . . . . 17 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → ((i · ((0 − 𝑎) + 1)) · 𝑥) = i)
8382oveq2d 7373 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (0 · ((i · ((0 − 𝑎) + 1)) · 𝑥)) = (0 · i))
8477, 83eqtrd 2776 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → ((0 · (i · ((0 − 𝑎) + 1))) · 𝑥) = (0 · i))
85 remul02 40860 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → (0 · 𝑥) = 0)
8675, 85syl 17 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (0 · 𝑥) = 0)
8767, 84, 863eqtr3d 2784 . . . . . . . . . . . . . 14 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 − 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 − 𝑎) + 1) · 𝑥) = 1)) → (0 · i) = 0)
8814, 87rexlimddv 3158 . . . . . . . . . . . . 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 2965 . . . . . . . . . . 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 7373 . . . . . . . . 9 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + ((0 − 𝑎) + 1)) = (𝑎 + 0))
9331, 16, 17addassd 11177 . . . . . . . . . 10 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 − 𝑎)) + 1) = (𝑎 + ((0 − 𝑎) + 1)))
94 renegid 40828 . . . . . . . . . . . . 13 (𝑎 ∈ ℝ → (𝑎 + (0 − 𝑎)) = 0)
958, 94syl 17 . . . . . . . . . . . 12 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (0 − 𝑎)) = 0)
9695oveq1d 7372 . . . . . . . . . . 11 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 − 𝑎)) + 1) = (0 + 1))
97 readdid2 40858 . . . . . . . . . . . 12 (1 ∈ ℝ → (0 + 1) = 1)
9854, 97ax-mp 5 . . . . . . . . . . 11 (0 + 1) = 1
9996, 98eqtrdi 2792 . . . . . . . . . 10 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 − 𝑎)) + 1) = 1)
10093, 99eqtr3d 2778 . . . . . . . . 9 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + ((0 − 𝑎) + 1)) = 1)
101 readdid1 40864 . . . . . . . . . 10 (𝑎 ∈ ℝ → (𝑎 + 0) = 𝑎)
1028, 101syl 17 . . . . . . . . 9 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + 0) = 𝑎)
10392, 100, 1023eqtr3rd 2785 . . . . . . . 8 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 = 1)
104 rernegcl 40826 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ ℝ → (0 − 𝑏) ∈ ℝ)
10532, 104syl 17 . . . . . . . . . . . . . . . . 17 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 − 𝑏) ∈ ℝ)
10611, 105readdcld 11184 . . . . . . . . . . . . . . . 16 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + (0 − 𝑏)) ∈ ℝ)
107 ax-rrecex 11123 . . . . . . . . . . . . . . . 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 11183 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 − 𝑏) ∈ ℂ)
11015, 109mulcld 11175 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (0 − 𝑏)) ∈ ℂ)
11123, 15, 110adddid 11179 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i + (i · (0 − 𝑏)))) = ((0 · i) + (0 · (i · (0 − 𝑏)))))
112 0re 11157 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ∈ ℝ
113 remul02 40860 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (0 ∈ ℝ → (0 · 0) = 0)
114112, 113ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 · 0) = 0
115114oveq1i 7367 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0 · 0) · i) = (0 · i)
1161, 1, 2mulassi 11166 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0 · 0) · i) = (0 · (0 · i))
117115, 116eqtr3i 2766 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 · i) = (0 · (0 · i))
118117a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (0 · (0 · i)))
119118oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (0 · (i · (0 − 𝑏)))) = ((0 · (0 · i)) + (0 · (i · (0 − 𝑏)))))
120111, 119eqtrd 2776 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i + (i · (0 − 𝑏)))) = ((0 · (0 · i)) + (0 · (i · (0 − 𝑏)))))
12115, 17, 109adddid 11179 . . . . . . . . . . . . . . . . . . . . . . 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 7372 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · 1) + (i · (0 − 𝑏))) = (i + (i · (0 − 𝑏))))
124121, 123eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (1 + (0 − 𝑏))) = (i + (i · (0 − 𝑏))))
125124oveq2d 7373 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 − 𝑏)))) = (0 · (i + (i · (0 − 𝑏)))))
12623, 41, 110adddid 11179 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · ((0 · i) + (i · (0 − 𝑏)))) = ((0 · (0 · i)) + (0 · (i · (0 − 𝑏)))))
127120, 125, 1263eqtr4d 2786 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 − 𝑏)))) = (0 · ((0 · i) + (i · (0 − 𝑏)))))
128103oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (i · 𝑏)) = (1 + (i · 𝑏)))
1295, 128eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (1 + (i · 𝑏)))
130129oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (i · (0 − 𝑏))) = ((1 + (i · 𝑏)) + (i · (0 − 𝑏))))
13117, 34, 110addassd 11177 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (i · 𝑏)) + (i · (0 − 𝑏))) = (1 + ((i · 𝑏) + (i · (0 − 𝑏)))))
132 renegid 40828 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑏 ∈ ℝ → (𝑏 + (0 − 𝑏)) = 0)
13332, 132syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑏 + (0 − 𝑏)) = 0)
134133oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (𝑏 + (0 − 𝑏))) = (i · 0))
13515, 33, 109adddid 11179 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (𝑏 + (0 − 𝑏))) = ((i · 𝑏) + (i · (0 − 𝑏))))
136 sn-mul01 40880 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (i ∈ ℂ → (i · 0) = 0)
1372, 136mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 0) = 0)
138134, 135, 1373eqtr3d 2784 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · 𝑏) + (i · (0 − 𝑏))) = 0)
139138oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((i · 𝑏) + (i · (0 − 𝑏)))) = (1 + 0))
140 readdid1 40864 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℝ → (1 + 0) = 1)
14154, 140ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 + 0) = 1
142139, 141eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((i · 𝑏) + (i · (0 − 𝑏)))) = 1)
143131, 142eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (i · 𝑏)) + (i · (0 − 𝑏))) = 1)
144130, 143eqtrd 2776 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (i · (0 − 𝑏))) = 1)
145144oveq2d 7373 . . . . . . . . . . . . . . . . . . . 20 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · ((0 · i) + (i · (0 − 𝑏)))) = (0 · 1))
146127, 145eqtrd 2776 . . . . . . . . . . . . . . . . . . 19 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 − 𝑏)))) = (0 · 1))
147 ax-1rid 11121 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℝ → (0 · 1) = 0)
148112, 147ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (0 · 1) = 0
149146, 148eqtrdi 2792 . . . . . . . . . . . . . . . . . 18 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 − 𝑏)))) = 0)
150149ad2antrr 724 . . . . . . . . . . . . . . . . 17 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (0 · (i · (1 + (0 − 𝑏)))) = 0)
151150oveq1d 7372 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → ((0 · (i · (1 + (0 − 𝑏)))) · 𝑦) = (0 · 𝑦))
152 0cnd 11148 . . . . . . . . . . . . . . . . . 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 11150 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → 1 ∈ ℂ)
155109ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (0 − 𝑏) ∈ ℂ)
156154, 155addcld 11174 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (1 + (0 − 𝑏)) ∈ ℂ)
157153, 156mulcld 11175 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (i · (1 + (0 − 𝑏))) ∈ ℂ)
158 simprl 769 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → 𝑦 ∈ ℝ)
159158recnd 11183 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → 𝑦 ∈ ℂ)
160152, 157, 159mulassd 11178 . . . . . . . . . . . . . . . . 17 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → ((0 · (i · (1 + (0 − 𝑏)))) · 𝑦) = (0 · ((i · (1 + (0 − 𝑏))) · 𝑦)))
161153, 156, 159mulassd 11178 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → ((i · (1 + (0 − 𝑏))) · 𝑦) = (i · ((1 + (0 − 𝑏)) · 𝑦)))
162 simprr 771 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → ((1 + (0 − 𝑏)) · 𝑦) = 1)
163162oveq2d 7373 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (i · ((1 + (0 − 𝑏)) · 𝑦)) = (i · 1))
164163, 19eqtrdi 2792 . . . . . . . . . . . . . . . . . . 19 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (i · ((1 + (0 − 𝑏)) · 𝑦)) = i)
165161, 164eqtrd 2776 . . . . . . . . . . . . . . . . . 18 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → ((i · (1 + (0 − 𝑏))) · 𝑦) = i)
166165oveq2d 7373 . . . . . . . . . . . . . . . . 17 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (0 · ((i · (1 + (0 − 𝑏))) · 𝑦)) = (0 · i))
167160, 166eqtrd 2776 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → ((0 · (i · (1 + (0 − 𝑏)))) · 𝑦) = (0 · i))
168 remul02 40860 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ → (0 · 𝑦) = 0)
169158, 168syl 17 . . . . . . . . . . . . . . . 16 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (0 · 𝑦) = 0)
170151, 167, 1693eqtr3d 2784 . . . . . . . . . . . . . . 15 ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 − 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 − 𝑏)) · 𝑦) = 1)) → (0 · i) = 0)
171108, 170rexlimddv 3158 . . . . . . . . . . . . . 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 2965 . . . . . . . . . . . 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 7372 . . . . . . . . . 10 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 − 𝑏)) + 𝑏) = (0 + 𝑏))
17617, 109, 33addassd 11177 . . . . . . . . . . 11 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 − 𝑏)) + 𝑏) = (1 + ((0 − 𝑏) + 𝑏)))
177 renegid2 40868 . . . . . . . . . . . . . 14 (𝑏 ∈ ℝ → ((0 − 𝑏) + 𝑏) = 0)
17832, 177syl 17 . . . . . . . . . . . . 13 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 − 𝑏) + 𝑏) = 0)
179178oveq2d 7373 . . . . . . . . . . . 12 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((0 − 𝑏) + 𝑏)) = (1 + 0))
180179, 141eqtrdi 2792 . . . . . . . . . . 11 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((0 − 𝑏) + 𝑏)) = 1)
181176, 180eqtrd 2776 . . . . . . . . . 10 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 − 𝑏)) + 𝑏) = 1)
182 readdid2 40858 . . . . . . . . . . 11 (𝑏 ∈ ℝ → (0 + 𝑏) = 𝑏)
18332, 182syl 17 . . . . . . . . . 10 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 + 𝑏) = 𝑏)
184175, 181, 1833eqtr3rd 2785 . . . . . . . . 9 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 = 1)
185184oveq2d 7373 . . . . . . . 8 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 𝑏) = (i · 1))
186103, 185oveq12d 7375 . . . . . . 7 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (i · 𝑏)) = (1 + (i · 1)))
1875, 186eqtrd 2776 . . . . . 6 ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (1 + (i · 1)))
18819oveq2i 7368 . . . . . . . . 9 (1 + (i · 1)) = (1 + i)
189188eqeq2i 2749 . . . . . . . 8 ((0 · i) = (1 + (i · 1)) ↔ (0 · i) = (1 + i))
190 oveq2 7365 . . . . . . . . . 10 ((0 · i) = (1 + i) → (((i · i) · i) · (0 · i)) = (((i · i) · i) · (1 + i)))
1912, 2mulcli 11162 . . . . . . . . . . . . 13 (i · i) ∈ ℂ
192191, 2mulcli 11162 . . . . . . . . . . . 12 ((i · i) · i) ∈ ℂ
193192, 1, 2mulassi 11166 . . . . . . . . . . 11 ((((i · i) · i) · 0) · i) = (((i · i) · i) · (0 · i))
194 sn-mul01 40880 . . . . . . . . . . . . 13 (((i · i) · i) ∈ ℂ → (((i · i) · i) · 0) = 0)
195192, 194ax-mp 5 . . . . . . . . . . . 12 (((i · i) · i) · 0) = 0
196195oveq1i 7367 . . . . . . . . . . 11 ((((i · i) · i) · 0) · i) = (0 · i)
197193, 196eqtr3i 2766 . . . . . . . . . 10 (((i · i) · i) · (0 · i)) = (0 · i)
198 ax-1cn 11109 . . . . . . . . . . . 12 1 ∈ ℂ
199192, 198, 2adddii 11167 . . . . . . . . . . 11 (((i · i) · i) · (1 + i)) = ((((i · i) · i) · 1) + (((i · i) · i) · i))
200191, 2, 198mulassi 11166 . . . . . . . . . . . . 13 (((i · i) · i) · 1) = ((i · i) · (i · 1))
20119oveq2i 7368 . . . . . . . . . . . . 13 ((i · i) · (i · 1)) = ((i · i) · i)
202200, 201eqtri 2764 . . . . . . . . . . . 12 (((i · i) · i) · 1) = ((i · i) · i)
203191, 2, 2mulassi 11166 . . . . . . . . . . . . 13 (((i · i) · i) · i) = ((i · i) · (i · i))
204 rei4 40878 . . . . . . . . . . . . 13 ((i · i) · (i · i)) = 1
205203, 204eqtri 2764 . . . . . . . . . . . 12 (((i · i) · i) · i) = 1
206202, 205oveq12i 7369 . . . . . . . . . . 11 ((((i · i) · i) · 1) + (((i · i) · i) · i)) = (((i · i) · i) + 1)
207199, 206eqtri 2764 . . . . . . . . . 10 (((i · i) · i) · (1 + i)) = (((i · i) · i) + 1)
208190, 197, 2073eqtr3g 2799 . . . . . . . . 9 ((0 · i) = (1 + i) → (0 · i) = (((i · i) · i) + 1))
20954, 54readdcli 11170 . . . . . . . . . . 11 (1 + 1) ∈ ℝ
210 df-2 12216 . . . . . . . . . . . 12 2 = (1 + 1)
211 sn-0ne2 40861 . . . . . . . . . . . . 13 0 ≠ 2
212211necomi 2998 . . . . . . . . . . . 12 2 ≠ 0
213210, 212eqnetrri 3015 . . . . . . . . . . 11 (1 + 1) ≠ 0
214 ax-rrecex 11123 . . . . . . . . . . 11 (((1 + 1) ∈ ℝ ∧ (1 + 1) ≠ 0) → ∃𝑧 ∈ ℝ ((1 + 1) · 𝑧) = 1)
215209, 213, 214mp2an 690 . . . . . . . . . 10 𝑧 ∈ ℝ ((1 + 1) · 𝑧) = 1
216192, 198addcli 11161 . . . . . . . . . . . . . . . . . 18 (((i · i) · i) + 1) ∈ ℂ
217198, 2, 216addassi 11165 . . . . . . . . . . . . . . . . 17 ((1 + i) + (((i · i) · i) + 1)) = (1 + (i + (((i · i) · i) + 1)))
2182, 192, 198addassi 11165 . . . . . . . . . . . . . . . . . 18 ((i + ((i · i) · i)) + 1) = (i + (((i · i) · i) + 1))
219218oveq2i 7368 . . . . . . . . . . . . . . . . 17 (1 + ((i + ((i · i) · i)) + 1)) = (1 + (i + (((i · i) · i) + 1)))
2202, 2, 2mulassi 11166 . . . . . . . . . . . . . . . . . . . . . 22 ((i · i) · i) = (i · (i · i))
221220oveq2i 7368 . . . . . . . . . . . . . . . . . . . . 21 (i + ((i · i) · i)) = (i + (i · (i · i)))
222 ipiiie0 40892 . . . . . . . . . . . . . . . . . . . . 21 (i + (i · (i · i))) = 0
223221, 222eqtri 2764 . . . . . . . . . . . . . . . . . . . 20 (i + ((i · i) · i)) = 0
224223oveq1i 7367 . . . . . . . . . . . . . . . . . . 19 ((i + ((i · i) · i)) + 1) = (0 + 1)
225224, 98eqtri 2764 . . . . . . . . . . . . . . . . . 18 ((i + ((i · i) · i)) + 1) = 1
226225oveq2i 7368 . . . . . . . . . . . . . . . . 17 (1 + ((i + ((i · i) · i)) + 1)) = (1 + 1)
227217, 219, 2263eqtr2i 2770 . . . . . . . . . . . . . . . 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 11167 . . . . . . . . . . . . . . . 16 ((0 · i) · (1 + 1)) = (((0 · i) · 1) + ((0 · i) · 1))
2301, 2, 198mulassi 11166 . . . . . . . . . . . . . . . . . . 19 ((0 · i) · 1) = (0 · (i · 1))
23119oveq2i 7368 . . . . . . . . . . . . . . . . . . 19 (0 · (i · 1)) = (0 · i)
232230, 231eqtri 2764 . . . . . . . . . . . . . . . . . 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 2788 . . . . . . . . . . . . . . . . 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 2788 . . . . . . . . . . . . . . . . 17 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · 1) = (((i · i) · i) + 1))
237234, 236oveq12d 7375 . . . . . . . . . . . . . . . 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 2788 . . . . . . . . . . . . . . 15 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · (1 + 1)) = ((1 + i) + (((i · i) · i) + 1)))
239 remulid2 40888 . . . . . . . . . . . . . . . 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 2786 . . . . . . . . . . . . . 14 (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · (1 + 1)) = (1 · (1 + 1)))
242241oveq1d 7372 . . . . . . . . . . . . 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 11150 . . . . . . . . . . . . . . 15 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 1 ∈ ℂ)
246245, 245addcld 11174 . . . . . . . . . . . . . 14 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (1 + 1) ∈ ℂ)
247 simprl 769 . . . . . . . . . . . . . . 15 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 𝑧 ∈ ℝ)
248247recnd 11183 . . . . . . . . . . . . . 14 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 𝑧 ∈ ℂ)
249244, 246, 248mulassd 11178 . . . . . . . . . . . . 13 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (((0 · i) · (1 + 1)) · 𝑧) = ((0 · i) · ((1 + 1) · 𝑧)))
250 simprr 771 . . . . . . . . . . . . . . 15 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((1 + 1) · 𝑧) = 1)
251250oveq2d 7373 . . . . . . . . . . . . . 14 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((0 · i) · ((1 + 1) · 𝑧)) = ((0 · i) · 1))
252251, 232eqtrdi 2792 . . . . . . . . . . . . 13 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((0 · i) · ((1 + 1) · 𝑧)) = (0 · i))
253249, 252eqtrd 2776 . . . . . . . . . . . 12 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (((0 · i) · (1 + 1)) · 𝑧) = (0 · i))
254245, 246, 248mulassd 11178 . . . . . . . . . . . . 13 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((1 · (1 + 1)) · 𝑧) = (1 · ((1 + 1) · 𝑧)))
255250oveq2d 7373 . . . . . . . . . . . . . 14 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (1 · ((1 + 1) · 𝑧)) = (1 · 1))
256 1t1e1ALT 40764 . . . . . . . . . . . . . 14 (1 · 1) = 1
257255, 256eqtrdi 2792 . . . . . . . . . . . . 13 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (1 · ((1 + 1) · 𝑧)) = 1)
258254, 257eqtrd 2776 . . . . . . . . . . . 12 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((1 · (1 + 1)) · 𝑧) = 1)
259243, 253, 2583eqtr3d 2784 . . . . . . . . . . 11 ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (0 · i) = 1)
260259rexlimdvaa 3153 . . . . . . . . . 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 685 . . . . . . . 8 ((0 · i) = (1 + i) → (0 · i) = 1)
263189, 262sylbi 216 . . . . . . 7 ((0 · i) = (1 + (i · 1)) → (0 · i) = 1)
264 oveq2 7365 . . . . . . . 8 ((0 · i) = 1 → (0 · (0 · i)) = (0 · 1))
265116, 115eqtr3i 2766 . . . . . . . 8 (0 · (0 · i)) = (0 · i)
266264, 265, 1483eqtr3g 2799 . . . . . . 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 798 . . . 4 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) → (0 · i) = 0)
270269ex 413 . . 3 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((0 · i) = (𝑎 + (i · 𝑏)) → (0 · i) = 0))
271270rexlimivv 3196 . 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 1541  wcel 2106  wne 2943  wrex 3073  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052  ici 11053   + caddc 11054   · cmul 11056  2c2 12208   cresub 40820
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-po 5545  df-so 5546  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11191  df-mnf 11192  df-ltxr 11194  df-2 12216  df-3 12217  df-resub 40821
This theorem is referenced by:  sn-mul02  40895  retire  40922
  Copyright terms: Public domain W3C validator