Theorem sn-0tie0 39903

Description: Lemma for sn-mul02 39904. Commuted version of sn-it0e0 39879. (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.

Step	Hyp	Ref	Expression
1		0cn 10656	. . 3 ⊢ 0 ∈ ℂ
2		ax-icn 10619	. . 3 ⊢ i ∈ ℂ
3	1, 2	mulcli 10671	. 2 ⊢ (0 · i) ∈ ℂ
4		cnre 10661	. 2 ⊢ ((0 · i) ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (0 · i) = (𝑎 + (i · 𝑏)))
5		simplr 769	. . . . . . 7 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (𝑎 + (i · 𝑏)))
6		neqne 2957	. . . . . . . . . . . 12 ⊢ (¬ (0 · i) = 0 → (0 · i) ≠ 0)
7	6	adantl 486	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) ≠ 0)
8		simplll 775	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 ∈ ℝ)
9		rernegcl 39836	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ ℝ → (0 −ℝ 𝑎) ∈ ℝ)
10	8, 9	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 −ℝ 𝑎) ∈ ℝ)
11		1red 10665	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 1 ∈ ℝ)
12	10, 11	readdcld 10693	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + 1) ∈ ℝ)
13		ax-rrecex 10632	. . . . . . . . . . . . . . 15 ⊢ ((((0 −ℝ 𝑎) + 1) ∈ ℝ ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) → ∃𝑥 ∈ ℝ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)
14	12, 13	sylan 584	. . . . . . . . . . . . . 14 ⊢ (((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) → ∃𝑥 ∈ ℝ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)
15	2	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → i ∈ ℂ)
16	10	recnd 10692	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 −ℝ 𝑎) ∈ ℂ)
17		1cnd 10659	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 1 ∈ ℂ)
18	15, 16, 17	adddid 10688	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · ((0 −ℝ 𝑎) + 1)) = ((i · (0 −ℝ 𝑎)) + (i · 1)))
19		it1ei 39900	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (i · 1) = i
20	19	oveq2i 7154	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((i · (0 −ℝ 𝑎)) + (i · 1)) = ((i · (0 −ℝ 𝑎)) + i)
21	18, 20	eqtrdi 2810	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · ((0 −ℝ 𝑎) + 1)) = ((i · (0 −ℝ 𝑎)) + i))
22	21	oveq2d 7159	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · ((0 −ℝ 𝑎) + 1))) = (0 · ((i · (0 −ℝ 𝑎)) + i)))
23		0cnd 10657	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 0 ∈ ℂ)
24	15, 16	mulcld 10684	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (0 −ℝ 𝑎)) ∈ ℂ)
25	23, 24, 15	adddid 10688	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · ((i · (0 −ℝ 𝑎)) + i)) = ((0 · (i · (0 −ℝ 𝑎))) + (0 · i)))
26	22, 25	eqtrd 2794	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · ((0 −ℝ 𝑎) + 1))) = ((0 · (i · (0 −ℝ 𝑎))) + (0 · i)))
27	5	oveq2d 7159	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + (0 · i)) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏))))
28		renegid2 39878	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ ℝ → ((0 −ℝ 𝑎) + 𝑎) = 0)
29	28	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + 𝑎) = 0)
30	29	oveq1d 7158	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 −ℝ 𝑎) + 𝑎) + (i · 𝑏)) = (0 + (i · 𝑏)))
31	8	recnd 10692	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 ∈ ℂ)
32		simpllr 776	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 ∈ ℝ)
33	32	recnd 10692	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 ∈ ℂ)
34	15, 33	mulcld 10684	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 𝑏) ∈ ℂ)
35	16, 31, 34	addassd 10686	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 −ℝ 𝑎) + 𝑎) + (i · 𝑏)) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏))))
36		sn-addid2 39869	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((i · 𝑏) ∈ ℂ → (0 + (i · 𝑏)) = (i · 𝑏))
37	34, 36	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 + (i · 𝑏)) = (i · 𝑏))
38	30, 35, 37	3eqtr3d 2802	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏))) = (i · 𝑏))
39	27, 38	eqtrd 2794	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + (0 · i)) = (i · 𝑏))
40	39	oveq2d 7159	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · ((0 −ℝ 𝑎) + (0 · i))) = ((0 · i) · (i · 𝑏)))
41	3	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) ∈ ℂ)
42	41, 16, 41	adddid 10688	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · ((0 −ℝ 𝑎) + (0 · i))) = (((0 · i) · (0 −ℝ 𝑎)) + ((0 · i) · (0 · i))))
43	23, 15, 16	mulassd 10687	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (0 −ℝ 𝑎)) = (0 · (i · (0 −ℝ 𝑎))))
44	41, 23, 15	mulassd 10687	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 · i) · 0) · i) = ((0 · i) · (0 · i)))
45		sn-mul01 39889	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((0 · i) ∈ ℂ → ((0 · i) · 0) = 0)
46	41, 45	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · 0) = 0)
47	46	oveq1d 7158	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 · i) · 0) · i) = (0 · i))
48	44, 47	eqtr3d 2796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (0 · i)) = (0 · i))
49	43, 48	oveq12d 7161	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 · i) · (0 −ℝ 𝑎)) + ((0 · i) · (0 · i))) = ((0 · (i · (0 −ℝ 𝑎))) + (0 · i)))
50	42, 49	eqtrd 2794	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · ((0 −ℝ 𝑎) + (0 · i))) = ((0 · (i · (0 −ℝ 𝑎))) + (0 · i)))
51	23, 15, 34	mulassd 10687	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (i · 𝑏)) = (0 · (i · (i · 𝑏))))
52	15, 15, 33	mulassd 10687	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · i) · 𝑏) = (i · (i · 𝑏)))
53		reixi 39886	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (i · i) = (0 −ℝ 1)
54		1re 10664	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 1 ∈ ℝ
55		rernegcl 39836	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1 ∈ ℝ → (0 −ℝ 1) ∈ ℝ)
56	54, 55	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 −ℝ 1) ∈ ℝ
57	53, 56	eqeltri 2847	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (i · i) ∈ ℝ
58	57	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · i) ∈ ℝ)
59	58, 32	remulcld 10694	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · i) · 𝑏) ∈ ℝ)
60	52, 59	eqeltrrd 2852	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (i · 𝑏)) ∈ ℝ)
61		remul02 39870	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((i · (i · 𝑏)) ∈ ℝ → (0 · (i · (i · 𝑏))) = 0)
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (i · 𝑏))) = 0)
63	51, 62	eqtrd 2794	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (i · 𝑏)) = 0)
64	40, 50, 63	3eqtr3d 2802	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · (i · (0 −ℝ 𝑎))) + (0 · i)) = 0)
65	26, 64	eqtrd 2794	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · ((0 −ℝ 𝑎) + 1))) = 0)
66	65	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 · (i · ((0 −ℝ 𝑎) + 1))) = 0)
67	66	oveq1d 7158	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → ((0 · (i · ((0 −ℝ 𝑎) + 1))) · 𝑥) = (0 · 𝑥))
68		0cnd 10657	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → 0 ∈ ℂ)
69	2	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → i ∈ ℂ)
70	10	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 −ℝ 𝑎) ∈ ℝ)
71	70	recnd 10692	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 −ℝ 𝑎) ∈ ℂ)
72		1cnd 10659	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → 1 ∈ ℂ)
73	71, 72	addcld 10683	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → ((0 −ℝ 𝑎) + 1) ∈ ℂ)
74	69, 73	mulcld 10684	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (i · ((0 −ℝ 𝑎) + 1)) ∈ ℂ)
75		simprl 771	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → 𝑥 ∈ ℝ)
76	75	recnd 10692	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → 𝑥 ∈ ℂ)
77	68, 74, 76	mulassd 10687	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → ((0 · (i · ((0 −ℝ 𝑎) + 1))) · 𝑥) = (0 · ((i · ((0 −ℝ 𝑎) + 1)) · 𝑥)))
78	69, 73, 76	mulassd 10687	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → ((i · ((0 −ℝ 𝑎) + 1)) · 𝑥) = (i · (((0 −ℝ 𝑎) + 1) · 𝑥)))
79		simprr 773	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)
80	79	oveq2d 7159	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (i · (((0 −ℝ 𝑎) + 1) · 𝑥)) = (i · 1))
81	80, 19	eqtrdi 2810	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (i · (((0 −ℝ 𝑎) + 1) · 𝑥)) = i)
82	78, 81	eqtrd 2794	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → ((i · ((0 −ℝ 𝑎) + 1)) · 𝑥) = i)
83	82	oveq2d 7159	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 · ((i · ((0 −ℝ 𝑎) + 1)) · 𝑥)) = (0 · i))
84	77, 83	eqtrd 2794	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → ((0 · (i · ((0 −ℝ 𝑎) + 1))) · 𝑥) = (0 · i))
85		remul02 39870	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → (0 · 𝑥) = 0)
86	75, 85	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 · 𝑥) = 0)
87	67, 84, 86	3eqtr3d 2802	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 · i) = 0)
88	14, 87	rexlimddv 3213	. . . . . . . . . . . . 13 ⊢ (((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) → (0 · i) = 0)
89	88	ex 417	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 −ℝ 𝑎) + 1) ≠ 0 → (0 · i) = 0))
90	89	necon1d 2971	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) ≠ 0 → ((0 −ℝ 𝑎) + 1) = 0))
91	7, 90	mpd 15	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + 1) = 0)
92	91	oveq2d 7159	. . . . . . . . 9 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + ((0 −ℝ 𝑎) + 1)) = (𝑎 + 0))
93	31, 16, 17	addassd 10686	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 −ℝ 𝑎)) + 1) = (𝑎 + ((0 −ℝ 𝑎) + 1)))
94		renegid 39838	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℝ → (𝑎 + (0 −ℝ 𝑎)) = 0)
95	8, 94	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (0 −ℝ 𝑎)) = 0)
96	95	oveq1d 7158	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 −ℝ 𝑎)) + 1) = (0 + 1))
97		readdid2 39868	. . . . . . . . . . . 12 ⊢ (1 ∈ ℝ → (0 + 1) = 1)
98	54, 97	ax-mp 5	. . . . . . . . . . 11 ⊢ (0 + 1) = 1
99	96, 98	eqtrdi 2810	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 −ℝ 𝑎)) + 1) = 1)
100	93, 99	eqtr3d 2796	. . . . . . . . 9 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + ((0 −ℝ 𝑎) + 1)) = 1)
101		readdid1 39874	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℝ → (𝑎 + 0) = 𝑎)
102	8, 101	syl 17	. . . . . . . . 9 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + 0) = 𝑎)
103	92, 100, 102	3eqtr3rd 2803	. . . . . . . 8 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 = 1)
104		rernegcl 39836	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ ℝ → (0 −ℝ 𝑏) ∈ ℝ)
105	32, 104	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 −ℝ 𝑏) ∈ ℝ)
106	11, 105	readdcld 10693	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + (0 −ℝ 𝑏)) ∈ ℝ)
107		ax-rrecex 10632	. . . . . . . . . . . . . . . 16 ⊢ (((1 + (0 −ℝ 𝑏)) ∈ ℝ ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) → ∃𝑦 ∈ ℝ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)
108	106, 107	sylan 584	. . . . . . . . . . . . . . 15 ⊢ (((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) → ∃𝑦 ∈ ℝ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)
109	105	recnd 10692	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 −ℝ 𝑏) ∈ ℂ)
110	15, 109	mulcld 10684	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (0 −ℝ 𝑏)) ∈ ℂ)
111	23, 15, 110	adddid 10688	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i + (i · (0 −ℝ 𝑏)))) = ((0 · i) + (0 · (i · (0 −ℝ 𝑏)))))
112		0re 10666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ∈ ℝ
113		remul02 39870	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0 ∈ ℝ → (0 · 0) = 0)
114	112, 113	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0 · 0) = 0
115	114	oveq1i 7153	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((0 · 0) · i) = (0 · i)
116	1, 1, 2	mulassi 10675	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((0 · 0) · i) = (0 · (0 · i))
117	115, 116	eqtr3i 2784	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0 · i) = (0 · (0 · i))
118	117	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (0 · (0 · i)))
119	118	oveq1d 7158	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (0 · (i · (0 −ℝ 𝑏)))) = ((0 · (0 · i)) + (0 · (i · (0 −ℝ 𝑏)))))
120	111, 119	eqtrd 2794	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i + (i · (0 −ℝ 𝑏)))) = ((0 · (0 · i)) + (0 · (i · (0 −ℝ 𝑏)))))
121	15, 17, 109	adddid 10688	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (1 + (0 −ℝ 𝑏))) = ((i · 1) + (i · (0 −ℝ 𝑏))))
122	19	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 1) = i)
123	122	oveq1d 7158	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · 1) + (i · (0 −ℝ 𝑏))) = (i + (i · (0 −ℝ 𝑏))))
124	121, 123	eqtrd 2794	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (1 + (0 −ℝ 𝑏))) = (i + (i · (0 −ℝ 𝑏))))
125	124	oveq2d 7159	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 −ℝ 𝑏)))) = (0 · (i + (i · (0 −ℝ 𝑏)))))
126	23, 41, 110	adddid 10688	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · ((0 · i) + (i · (0 −ℝ 𝑏)))) = ((0 · (0 · i)) + (0 · (i · (0 −ℝ 𝑏)))))
127	120, 125, 126	3eqtr4d 2804	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 −ℝ 𝑏)))) = (0 · ((0 · i) + (i · (0 −ℝ 𝑏)))))
128	103	oveq1d 7158	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (i · 𝑏)) = (1 + (i · 𝑏)))
129	5, 128	eqtrd 2794	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (1 + (i · 𝑏)))
130	129	oveq1d 7158	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (i · (0 −ℝ 𝑏))) = ((1 + (i · 𝑏)) + (i · (0 −ℝ 𝑏))))
131	17, 34, 110	addassd 10686	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (i · 𝑏)) + (i · (0 −ℝ 𝑏))) = (1 + ((i · 𝑏) + (i · (0 −ℝ 𝑏)))))
132		renegid 39838	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑏 ∈ ℝ → (𝑏 + (0 −ℝ 𝑏)) = 0)
133	32, 132	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑏 + (0 −ℝ 𝑏)) = 0)
134	133	oveq2d 7159	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (𝑏 + (0 −ℝ 𝑏))) = (i · 0))
135	15, 33, 109	adddid 10688	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (𝑏 + (0 −ℝ 𝑏))) = ((i · 𝑏) + (i · (0 −ℝ 𝑏))))
136		sn-mul01 39889	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (i ∈ ℂ → (i · 0) = 0)
137	2, 136	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 0) = 0)
138	134, 135, 137	3eqtr3d 2802	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · 𝑏) + (i · (0 −ℝ 𝑏))) = 0)
139	138	oveq2d 7159	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((i · 𝑏) + (i · (0 −ℝ 𝑏)))) = (1 + 0))
140		readdid1 39874	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1 ∈ ℝ → (1 + 0) = 1)
141	54, 140	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1 + 0) = 1
142	139, 141	eqtrdi 2810	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((i · 𝑏) + (i · (0 −ℝ 𝑏)))) = 1)
143	131, 142	eqtrd 2794	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (i · 𝑏)) + (i · (0 −ℝ 𝑏))) = 1)
144	130, 143	eqtrd 2794	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (i · (0 −ℝ 𝑏))) = 1)
145	144	oveq2d 7159	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · ((0 · i) + (i · (0 −ℝ 𝑏)))) = (0 · 1))
146	127, 145	eqtrd 2794	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 −ℝ 𝑏)))) = (0 · 1))
147		ax-1rid 10630	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℝ → (0 · 1) = 0)
148	112, 147	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 · 1) = 0
149	146, 148	eqtrdi 2810	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 −ℝ 𝑏)))) = 0)
150	149	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (0 · (i · (1 + (0 −ℝ 𝑏)))) = 0)
151	150	oveq1d 7158	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → ((0 · (i · (1 + (0 −ℝ 𝑏)))) · 𝑦) = (0 · 𝑦))
152		0cnd 10657	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → 0 ∈ ℂ)
153	2	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → i ∈ ℂ)
154		1cnd 10659	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → 1 ∈ ℂ)
155	109	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (0 −ℝ 𝑏) ∈ ℂ)
156	154, 155	addcld 10683	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (1 + (0 −ℝ 𝑏)) ∈ ℂ)
157	153, 156	mulcld 10684	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (i · (1 + (0 −ℝ 𝑏))) ∈ ℂ)
158		simprl 771	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → 𝑦 ∈ ℝ)
159	158	recnd 10692	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → 𝑦 ∈ ℂ)
160	152, 157, 159	mulassd 10687	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → ((0 · (i · (1 + (0 −ℝ 𝑏)))) · 𝑦) = (0 · ((i · (1 + (0 −ℝ 𝑏))) · 𝑦)))
161	153, 156, 159	mulassd 10687	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → ((i · (1 + (0 −ℝ 𝑏))) · 𝑦) = (i · ((1 + (0 −ℝ 𝑏)) · 𝑦)))
162		simprr 773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)
163	162	oveq2d 7159	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (i · ((1 + (0 −ℝ 𝑏)) · 𝑦)) = (i · 1))
164	163, 19	eqtrdi 2810	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (i · ((1 + (0 −ℝ 𝑏)) · 𝑦)) = i)
165	161, 164	eqtrd 2794	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → ((i · (1 + (0 −ℝ 𝑏))) · 𝑦) = i)
166	165	oveq2d 7159	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (0 · ((i · (1 + (0 −ℝ 𝑏))) · 𝑦)) = (0 · i))
167	160, 166	eqtrd 2794	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → ((0 · (i · (1 + (0 −ℝ 𝑏)))) · 𝑦) = (0 · i))
168		remul02 39870	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℝ → (0 · 𝑦) = 0)
169	158, 168	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (0 · 𝑦) = 0)
170	151, 167, 169	3eqtr3d 2802	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (0 · i) = 0)
171	108, 170	rexlimddv 3213	. . . . . . . . . . . . . 14 ⊢ (((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) → (0 · i) = 0)
172	171	ex 417	. . . . . . . . . . . . 13 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) ≠ 0 → (0 · i) = 0))
173	172	necon1d 2971	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) ≠ 0 → (1 + (0 −ℝ 𝑏)) = 0))
174	7, 173	mpd 15	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + (0 −ℝ 𝑏)) = 0)
175	174	oveq1d 7158	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) + 𝑏) = (0 + 𝑏))
176	17, 109, 33	addassd 10686	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) + 𝑏) = (1 + ((0 −ℝ 𝑏) + 𝑏)))
177		renegid2 39878	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ℝ → ((0 −ℝ 𝑏) + 𝑏) = 0)
178	32, 177	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑏) + 𝑏) = 0)
179	178	oveq2d 7159	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((0 −ℝ 𝑏) + 𝑏)) = (1 + 0))
180	179, 141	eqtrdi 2810	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((0 −ℝ 𝑏) + 𝑏)) = 1)
181	176, 180	eqtrd 2794	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) + 𝑏) = 1)
182		readdid2 39868	. . . . . . . . . . 11 ⊢ (𝑏 ∈ ℝ → (0 + 𝑏) = 𝑏)
183	32, 182	syl 17	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 + 𝑏) = 𝑏)
184	175, 181, 183	3eqtr3rd 2803	. . . . . . . . 9 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 = 1)
185	184	oveq2d 7159	. . . . . . . 8 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 𝑏) = (i · 1))
186	103, 185	oveq12d 7161	. . . . . . 7 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (i · 𝑏)) = (1 + (i · 1)))
187	5, 186	eqtrd 2794	. . . . . 6 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (1 + (i · 1)))
188	19	oveq2i 7154	. . . . . . . . 9 ⊢ (1 + (i · 1)) = (1 + i)
189	188	eqeq2i 2772	. . . . . . . 8 ⊢ ((0 · i) = (1 + (i · 1)) ↔ (0 · i) = (1 + i))
190		oveq2 7151	. . . . . . . . . 10 ⊢ ((0 · i) = (1 + i) → (((i · i) · i) · (0 · i)) = (((i · i) · i) · (1 + i)))
191	2, 2	mulcli 10671	. . . . . . . . . . . . 13 ⊢ (i · i) ∈ ℂ
192	191, 2	mulcli 10671	. . . . . . . . . . . 12 ⊢ ((i · i) · i) ∈ ℂ
193	192, 1, 2	mulassi 10675	. . . . . . . . . . 11 ⊢ ((((i · i) · i) · 0) · i) = (((i · i) · i) · (0 · i))
194		sn-mul01 39889	. . . . . . . . . . . . 13 ⊢ (((i · i) · i) ∈ ℂ → (((i · i) · i) · 0) = 0)
195	192, 194	ax-mp 5	. . . . . . . . . . . 12 ⊢ (((i · i) · i) · 0) = 0
196	195	oveq1i 7153	. . . . . . . . . . 11 ⊢ ((((i · i) · i) · 0) · i) = (0 · i)
197	193, 196	eqtr3i 2784	. . . . . . . . . 10 ⊢ (((i · i) · i) · (0 · i)) = (0 · i)
198		ax-1cn 10618	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
199	192, 198, 2	adddii 10676	. . . . . . . . . . 11 ⊢ (((i · i) · i) · (1 + i)) = ((((i · i) · i) · 1) + (((i · i) · i) · i))
200	191, 2, 198	mulassi 10675	. . . . . . . . . . . . 13 ⊢ (((i · i) · i) · 1) = ((i · i) · (i · 1))
201	19	oveq2i 7154	. . . . . . . . . . . . 13 ⊢ ((i · i) · (i · 1)) = ((i · i) · i)
202	200, 201	eqtri 2782	. . . . . . . . . . . 12 ⊢ (((i · i) · i) · 1) = ((i · i) · i)
203	191, 2, 2	mulassi 10675	. . . . . . . . . . . . 13 ⊢ (((i · i) · i) · i) = ((i · i) · (i · i))
204		rei4 39887	. . . . . . . . . . . . 13 ⊢ ((i · i) · (i · i)) = 1
205	203, 204	eqtri 2782	. . . . . . . . . . . 12 ⊢ (((i · i) · i) · i) = 1
206	202, 205	oveq12i 7155	. . . . . . . . . . 11 ⊢ ((((i · i) · i) · 1) + (((i · i) · i) · i)) = (((i · i) · i) + 1)
207	199, 206	eqtri 2782	. . . . . . . . . 10 ⊢ (((i · i) · i) · (1 + i)) = (((i · i) · i) + 1)
208	190, 197, 207	3eqtr3g 2817	. . . . . . . . 9 ⊢ ((0 · i) = (1 + i) → (0 · i) = (((i · i) · i) + 1))
209	54, 54	readdcli 10679	. . . . . . . . . . 11 ⊢ (1 + 1) ∈ ℝ
210		df-2 11722	. . . . . . . . . . . 12 ⊢ 2 = (1 + 1)
211		sn-0ne2 39871	. . . . . . . . . . . . 13 ⊢ 0 ≠ 2
212	211	necomi 3003	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
213	210, 212	eqnetrri 3020	. . . . . . . . . . 11 ⊢ (1 + 1) ≠ 0
214		ax-rrecex 10632	. . . . . . . . . . 11 ⊢ (((1 + 1) ∈ ℝ ∧ (1 + 1) ≠ 0) → ∃𝑧 ∈ ℝ ((1 + 1) · 𝑧) = 1)
215	209, 213, 214	mp2an 692	. . . . . . . . . 10 ⊢ ∃𝑧 ∈ ℝ ((1 + 1) · 𝑧) = 1
216	192, 198	addcli 10670	. . . . . . . . . . . . . . . . . 18 ⊢ (((i · i) · i) + 1) ∈ ℂ
217	198, 2, 216	addassi 10674	. . . . . . . . . . . . . . . . 17 ⊢ ((1 + i) + (((i · i) · i) + 1)) = (1 + (i + (((i · i) · i) + 1)))
218	2, 192, 198	addassi 10674	. . . . . . . . . . . . . . . . . 18 ⊢ ((i + ((i · i) · i)) + 1) = (i + (((i · i) · i) + 1))
219	218	oveq2i 7154	. . . . . . . . . . . . . . . . 17 ⊢ (1 + ((i + ((i · i) · i)) + 1)) = (1 + (i + (((i · i) · i) + 1)))
220	2, 2, 2	mulassi 10675	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((i · i) · i) = (i · (i · i))
221	220	oveq2i 7154	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (i + ((i · i) · i)) = (i + (i · (i · i)))
222		ipiiie0 39901	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (i + (i · (i · i))) = 0
223	221, 222	eqtri 2782	. . . . . . . . . . . . . . . . . . . 20 ⊢ (i + ((i · i) · i)) = 0
224	223	oveq1i 7153	. . . . . . . . . . . . . . . . . . 19 ⊢ ((i + ((i · i) · i)) + 1) = (0 + 1)
225	224, 98	eqtri 2782	. . . . . . . . . . . . . . . . . 18 ⊢ ((i + ((i · i) · i)) + 1) = 1
226	225	oveq2i 7154	. . . . . . . . . . . . . . . . 17 ⊢ (1 + ((i + ((i · i) · i)) + 1)) = (1 + 1)
227	217, 219, 226	3eqtr2i 2788	. . . . . . . . . . . . . . . 16 ⊢ ((1 + i) + (((i · i) · i) + 1)) = (1 + 1)
228	227	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((1 + i) + (((i · i) · i) + 1)) = (1 + 1))
229	3, 198, 198	adddii 10676	. . . . . . . . . . . . . . . 16 ⊢ ((0 · i) · (1 + 1)) = (((0 · i) · 1) + ((0 · i) · 1))
230	1, 2, 198	mulassi 10675	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 · i) · 1) = (0 · (i · 1))
231	19	oveq2i 7154	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 · (i · 1)) = (0 · i)
232	230, 231	eqtri 2782	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 · i) · 1) = (0 · i)
233		simpl 487	. . . . . . . . . . . . . . . . . 18 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (0 · i) = (1 + i))
234	232, 233	syl5eq 2806	. . . . . . . . . . . . . . . . 17 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · 1) = (1 + i))
235		simpr 489	. . . . . . . . . . . . . . . . . 18 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (0 · i) = (((i · i) · i) + 1))
236	232, 235	syl5eq 2806	. . . . . . . . . . . . . . . . 17 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · 1) = (((i · i) · i) + 1))
237	234, 236	oveq12d 7161	. . . . . . . . . . . . . . . 16 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (((0 · i) · 1) + ((0 · i) · 1)) = ((1 + i) + (((i · i) · i) + 1)))
238	229, 237	syl5eq 2806	. . . . . . . . . . . . . . 15 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · (1 + 1)) = ((1 + i) + (((i · i) · i) + 1)))
239		remulid2 39897	. . . . . . . . . . . . . . . 16 ⊢ ((1 + 1) ∈ ℝ → (1 · (1 + 1)) = (1 + 1))
240	209, 239	mp1i 13	. . . . . . . . . . . . . . 15 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (1 · (1 + 1)) = (1 + 1))
241	228, 238, 240	3eqtr4d 2804	. . . . . . . . . . . . . 14 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · (1 + 1)) = (1 · (1 + 1)))
242	241	oveq1d 7158	. . . . . . . . . . . . 13 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (((0 · i) · (1 + 1)) · 𝑧) = ((1 · (1 + 1)) · 𝑧))
243	242	adantr 485	. . . . . . . . . . . 12 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (((0 · i) · (1 + 1)) · 𝑧) = ((1 · (1 + 1)) · 𝑧))
244	3	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (0 · i) ∈ ℂ)
245		1cnd 10659	. . . . . . . . . . . . . . 15 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 1 ∈ ℂ)
246	245, 245	addcld 10683	. . . . . . . . . . . . . 14 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (1 + 1) ∈ ℂ)
247		simprl 771	. . . . . . . . . . . . . . 15 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 𝑧 ∈ ℝ)
248	247	recnd 10692	. . . . . . . . . . . . . 14 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 𝑧 ∈ ℂ)
249	244, 246, 248	mulassd 10687	. . . . . . . . . . . . 13 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (((0 · i) · (1 + 1)) · 𝑧) = ((0 · i) · ((1 + 1) · 𝑧)))
250		simprr 773	. . . . . . . . . . . . . . 15 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((1 + 1) · 𝑧) = 1)
251	250	oveq2d 7159	. . . . . . . . . . . . . 14 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((0 · i) · ((1 + 1) · 𝑧)) = ((0 · i) · 1))
252	251, 232	eqtrdi 2810	. . . . . . . . . . . . 13 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((0 · i) · ((1 + 1) · 𝑧)) = (0 · i))
253	249, 252	eqtrd 2794	. . . . . . . . . . . 12 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (((0 · i) · (1 + 1)) · 𝑧) = (0 · i))
254	245, 246, 248	mulassd 10687	. . . . . . . . . . . . 13 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((1 · (1 + 1)) · 𝑧) = (1 · ((1 + 1) · 𝑧)))
255	250	oveq2d 7159	. . . . . . . . . . . . . 14 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (1 · ((1 + 1) · 𝑧)) = (1 · 1))
256		1t1e1ALT 39779	. . . . . . . . . . . . . 14 ⊢ (1 · 1) = 1
257	255, 256	eqtrdi 2810	. . . . . . . . . . . . 13 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (1 · ((1 + 1) · 𝑧)) = 1)
258	254, 257	eqtrd 2794	. . . . . . . . . . . 12 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((1 · (1 + 1)) · 𝑧) = 1)
259	243, 253, 258	3eqtr3d 2802	. . . . . . . . . . 11 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (0 · i) = 1)
260	259	rexlimdvaa 3207	. . . . . . . . . 10 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (∃𝑧 ∈ ℝ ((1 + 1) · 𝑧) = 1 → (0 · i) = 1))
261	215, 260	mpi 20	. . . . . . . . 9 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (0 · i) = 1)
262	208, 261	mpdan 687	. . . . . . . 8 ⊢ ((0 · i) = (1 + i) → (0 · i) = 1)
263	189, 262	sylbi 220	. . . . . . 7 ⊢ ((0 · i) = (1 + (i · 1)) → (0 · i) = 1)
264		oveq2 7151	. . . . . . . 8 ⊢ ((0 · i) = 1 → (0 · (0 · i)) = (0 · 1))
265	116, 115	eqtr3i 2784	. . . . . . . 8 ⊢ (0 · (0 · i)) = (0 · i)
266	264, 265, 148	3eqtr3g 2817	. . . . . . 7 ⊢ ((0 · i) = 1 → (0 · i) = 0)
267	263, 266	syl 17	. . . . . 6 ⊢ ((0 · i) = (1 + (i · 1)) → (0 · i) = 0)
268	187, 267	syl 17	. . . . 5 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = 0)
269	268	pm2.18da 800	. . . 4 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) → (0 · i) = 0)
270	269	ex 417	. . 3 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((0 · i) = (𝑎 + (i · 𝑏)) → (0 · i) = 0))
271	270	rexlimivv 3214	. 2 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (0 · i) = (𝑎 + (i · 𝑏)) → (0 · i) = 0)
272	3, 4, 271	mp2b 10	1 ⊢ (0 · i) = 0

Syntax hints:  ¬ wn 3   ∧ wa 400   = wceq 1539   ∈ wcel 2112   ≠ wne 2949  ∃wrex 3069  (class class class)co 7143  ℂcc 10558  ℝcr 10559  0cc0 10560  1c1 10561  ici 10562   + caddc 10563   · cmul 10565  2c2 11714   −_ℝ cresub 39830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5162  ax-nul 5169  ax-pow 5227  ax-pr 5291  ax-un 7452  ax-resscn 10617  ax-1cn 10618  ax-icn 10619  ax-addcl 10620  ax-addrcl 10621  ax-mulcl 10622  ax-mulrcl 10623  ax-addass 10625  ax-mulass 10626  ax-distr 10627  ax-i2m1 10628  ax-1ne0 10629  ax-1rid 10630  ax-rnegex 10631  ax-rrecex 10632  ax-cnre 10633  ax-pre-lttri 10634  ax-pre-lttrn 10635  ax-pre-ltadd 10636

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ne 2950  df-nel 3054  df-ral 3073  df-rex 3074  df-reu 3075  df-rmo 3076  df-rab 3077  df-v 3409  df-sbc 3694  df-csb 3802  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-nul 4222  df-if 4414  df-pw 4489  df-sn 4516  df-pr 4518  df-op 4522  df-uni 4792  df-br 5026  df-opab 5088  df-mpt 5106  df-id 5423  df-po 5436  df-so 5437  df-xp 5523  df-rel 5524  df-cnv 5525  df-co 5526  df-dm 5527  df-rn 5528  df-res 5529  df-ima 5530  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 7101  df-ov 7146  df-oprab 7147  df-mpo 7148  df-er 8292  df-en 8521  df-dom 8522  df-sdom 8523  df-pnf 10700  df-mnf 10701  df-ltxr 10703  df-2 11722  df-3 11723  df-resub 39831

This theorem is referenced by:  sn-mul02  39904  retire  39919