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.

Step	Hyp	Ref	Expression
1		0cn 11147	. . 3 ⊢ 0 ∈ ℂ
2		ax-icn 11110	. . 3 ⊢ i ∈ ℂ
3	1, 2	mulcli 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)
7	6	adantl 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 −ℝ 𝑎) ∈ ℝ)
10	8, 9	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 −ℝ 𝑎) ∈ ℝ)
11		1red 11156	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 1 ∈ ℝ)
12	10, 11	readdcld 11184	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + 1) ∈ ℝ)
13		ax-rrecex 11123	. . . . . . . . . . . . . . 15 ⊢ ((((0 −ℝ 𝑎) + 1) ∈ ℝ ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) → ∃𝑥 ∈ ℝ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)
14	12, 13	sylan 580	. . . . . . . . . . . . . 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 11183	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 −ℝ 𝑎) ∈ ℂ)
17		1cnd 11150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 1 ∈ ℂ)
18	15, 16, 17	adddid 11179	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · ((0 −ℝ 𝑎) + 1)) = ((i · (0 −ℝ 𝑎)) + (i · 1)))
19		it1ei 40891	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (i · 1) = i
20	19	oveq2i 7368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((i · (0 −ℝ 𝑎)) + (i · 1)) = ((i · (0 −ℝ 𝑎)) + i)
21	18, 20	eqtrdi 2792	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · ((0 −ℝ 𝑎) + 1)) = ((i · (0 −ℝ 𝑎)) + i))
22	21	oveq2d 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 ∈ ℂ)
24	15, 16	mulcld 11175	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (0 −ℝ 𝑎)) ∈ ℂ)
25	23, 24, 15	adddid 11179	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · ((i · (0 −ℝ 𝑎)) + i)) = ((0 · (i · (0 −ℝ 𝑎))) + (0 · i)))
26	22, 25	eqtrd 2776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · ((0 −ℝ 𝑎) + 1))) = ((0 · (i · (0 −ℝ 𝑎))) + (0 · i)))
27	5	oveq2d 7373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + (0 · i)) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏))))
28		renegid2 40868	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ ℝ → ((0 −ℝ 𝑎) + 𝑎) = 0)
29	28	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + 𝑎) = 0)
30	29	oveq1d 7372	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 −ℝ 𝑎) + 𝑎) + (i · 𝑏)) = (0 + (i · 𝑏)))
31	8	recnd 11183	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 ∈ ℂ)
32		simpllr 774	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 ∈ ℝ)
33	32	recnd 11183	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 ∈ ℂ)
34	15, 33	mulcld 11175	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 𝑏) ∈ ℂ)
35	16, 31, 34	addassd 11177	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 −ℝ 𝑎) + 𝑎) + (i · 𝑏)) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏))))
36		sn-addid2 40859	. . . . . . . . . . . . . . . . . . . . . . 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 2784	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏))) = (i · 𝑏))
39	27, 38	eqtrd 2776	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + (0 · i)) = (i · 𝑏))
40	39	oveq2d 7373	. . . . . . . . . . . . . . . . . . 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 11179	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · ((0 −ℝ 𝑎) + (0 · i))) = (((0 · i) · (0 −ℝ 𝑎)) + ((0 · i) · (0 · i))))
43	23, 15, 16	mulassd 11178	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (0 −ℝ 𝑎)) = (0 · (i · (0 −ℝ 𝑎))))
44	41, 23, 15	mulassd 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)
46	41, 45	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · 0) = 0)
47	46	oveq1d 7372	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 · i) · 0) · i) = (0 · i))
48	44, 47	eqtr3d 2778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (0 · i)) = (0 · i))
49	43, 48	oveq12d 7375	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 · i) · (0 −ℝ 𝑎)) + ((0 · i) · (0 · i))) = ((0 · (i · (0 −ℝ 𝑎))) + (0 · i)))
50	42, 49	eqtrd 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · ((0 −ℝ 𝑎) + (0 · i))) = ((0 · (i · (0 −ℝ 𝑎))) + (0 · i)))
51	23, 15, 34	mulassd 11178	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (i · 𝑏)) = (0 · (i · (i · 𝑏))))
52	15, 15, 33	mulassd 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) ∈ ℝ)
56	54, 55	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 −ℝ 1) ∈ ℝ
57	53, 56	eqeltri 2834	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (i · i) ∈ ℝ
58	57	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · i) ∈ ℝ)
59	58, 32	remulcld 11185	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · i) · 𝑏) ∈ ℝ)
60	52, 59	eqeltrrd 2839	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (i · 𝑏)) ∈ ℝ)
61		remul02 40860	. . . . . . . . . . . . . . . . . . . . 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 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (i · 𝑏)) = 0)
64	40, 50, 63	3eqtr3d 2784	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · (i · (0 −ℝ 𝑎))) + (0 · i)) = 0)
65	26, 64	eqtrd 2776	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · ((0 −ℝ 𝑎) + 1))) = 0)
66	65	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 · (i · ((0 −ℝ 𝑎) + 1))) = 0)
67	66	oveq1d 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 ∈ ℂ)
69	2	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → i ∈ ℂ)
70	10	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 −ℝ 𝑎) ∈ ℝ)
71	70	recnd 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 ∈ ℂ)
73	71, 72	addcld 11174	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → ((0 −ℝ 𝑎) + 1) ∈ ℂ)
74	69, 73	mulcld 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)) → 𝑥 ∈ ℝ)
76	75	recnd 11183	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → 𝑥 ∈ ℂ)
77	68, 74, 76	mulassd 11178	. . . . . . . . . . . . . . . 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 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)
80	79	oveq2d 7373	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (i · (((0 −ℝ 𝑎) + 1) · 𝑥)) = (i · 1))
81	80, 19	eqtrdi 2792	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (i · (((0 −ℝ 𝑎) + 1) · 𝑥)) = i)
82	78, 81	eqtrd 2776	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → ((i · ((0 −ℝ 𝑎) + 1)) · 𝑥) = i)
83	82	oveq2d 7373	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 · ((i · ((0 −ℝ 𝑎) + 1)) · 𝑥)) = (0 · i))
84	77, 83	eqtrd 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)
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 2784	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 · i) = 0)
88	14, 87	rexlimddv 3158	. . . . . . . . . . . . 13 ⊢ (((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) → (0 · i) = 0)
89	88	ex 413	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 −ℝ 𝑎) + 1) ≠ 0 → (0 · i) = 0))
90	89	necon1d 2965	. . . . . . . . . . 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 7373	. . . . . . . . 9 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + ((0 −ℝ 𝑎) + 1)) = (𝑎 + 0))
93	31, 16, 17	addassd 11177	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 −ℝ 𝑎)) + 1) = (𝑎 + ((0 −ℝ 𝑎) + 1)))
94		renegid 40828	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℝ → (𝑎 + (0 −ℝ 𝑎)) = 0)
95	8, 94	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (0 −ℝ 𝑎)) = 0)
96	95	oveq1d 7372	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 −ℝ 𝑎)) + 1) = (0 + 1))
97		readdid2 40858	. . . . . . . . . . . 12 ⊢ (1 ∈ ℝ → (0 + 1) = 1)
98	54, 97	ax-mp 5	. . . . . . . . . . 11 ⊢ (0 + 1) = 1
99	96, 98	eqtrdi 2792	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 −ℝ 𝑎)) + 1) = 1)
100	93, 99	eqtr3d 2778	. . . . . . . . 9 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + ((0 −ℝ 𝑎) + 1)) = 1)
101		readdid1 40864	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℝ → (𝑎 + 0) = 𝑎)
102	8, 101	syl 17	. . . . . . . . 9 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + 0) = 𝑎)
103	92, 100, 102	3eqtr3rd 2785	. . . . . . . 8 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 = 1)
104		rernegcl 40826	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ ℝ → (0 −ℝ 𝑏) ∈ ℝ)
105	32, 104	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 −ℝ 𝑏) ∈ ℝ)
106	11, 105	readdcld 11184	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + (0 −ℝ 𝑏)) ∈ ℝ)
107		ax-rrecex 11123	. . . . . . . . . . . . . . . 16 ⊢ (((1 + (0 −ℝ 𝑏)) ∈ ℝ ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) → ∃𝑦 ∈ ℝ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)
108	106, 107	sylan 580	. . . . . . . . . . . . . . 15 ⊢ (((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) → ∃𝑦 ∈ ℝ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)
109	105	recnd 11183	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 −ℝ 𝑏) ∈ ℂ)
110	15, 109	mulcld 11175	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (0 −ℝ 𝑏)) ∈ ℂ)
111	23, 15, 110	adddid 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)
114	112, 113	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0 · 0) = 0
115	114	oveq1i 7367	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((0 · 0) · i) = (0 · i)
116	1, 1, 2	mulassi 11166	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((0 · 0) · i) = (0 · (0 · i))
117	115, 116	eqtr3i 2766	. . . . . . . . . . . . . . . . . . . . . . . 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 7372	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (0 · (i · (0 −ℝ 𝑏)))) = ((0 · (0 · i)) + (0 · (i · (0 −ℝ 𝑏)))))
120	111, 119	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i + (i · (0 −ℝ 𝑏)))) = ((0 · (0 · i)) + (0 · (i · (0 −ℝ 𝑏)))))
121	15, 17, 109	adddid 11179	. . . . . . . . . . . . . . . . . . . . . . 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 7372	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · 1) + (i · (0 −ℝ 𝑏))) = (i + (i · (0 −ℝ 𝑏))))
124	121, 123	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (1 + (0 −ℝ 𝑏))) = (i + (i · (0 −ℝ 𝑏))))
125	124	oveq2d 7373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 −ℝ 𝑏)))) = (0 · (i + (i · (0 −ℝ 𝑏)))))
126	23, 41, 110	adddid 11179	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · ((0 · i) + (i · (0 −ℝ 𝑏)))) = ((0 · (0 · i)) + (0 · (i · (0 −ℝ 𝑏)))))
127	120, 125, 126	3eqtr4d 2786	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 −ℝ 𝑏)))) = (0 · ((0 · i) + (i · (0 −ℝ 𝑏)))))
128	103	oveq1d 7372	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (i · 𝑏)) = (1 + (i · 𝑏)))
129	5, 128	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (1 + (i · 𝑏)))
130	129	oveq1d 7372	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (i · (0 −ℝ 𝑏))) = ((1 + (i · 𝑏)) + (i · (0 −ℝ 𝑏))))
131	17, 34, 110	addassd 11177	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (i · 𝑏)) + (i · (0 −ℝ 𝑏))) = (1 + ((i · 𝑏) + (i · (0 −ℝ 𝑏)))))
132		renegid 40828	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑏 ∈ ℝ → (𝑏 + (0 −ℝ 𝑏)) = 0)
133	32, 132	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑏 + (0 −ℝ 𝑏)) = 0)
134	133	oveq2d 7373	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (𝑏 + (0 −ℝ 𝑏))) = (i · 0))
135	15, 33, 109	adddid 11179	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (𝑏 + (0 −ℝ 𝑏))) = ((i · 𝑏) + (i · (0 −ℝ 𝑏))))
136		sn-mul01 40880	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2784	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · 𝑏) + (i · (0 −ℝ 𝑏))) = 0)
139	138	oveq2d 7373	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((i · 𝑏) + (i · (0 −ℝ 𝑏)))) = (1 + 0))
140		readdid1 40864	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1 ∈ ℝ → (1 + 0) = 1)
141	54, 140	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1 + 0) = 1
142	139, 141	eqtrdi 2792	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((i · 𝑏) + (i · (0 −ℝ 𝑏)))) = 1)
143	131, 142	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (i · 𝑏)) + (i · (0 −ℝ 𝑏))) = 1)
144	130, 143	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (i · (0 −ℝ 𝑏))) = 1)
145	144	oveq2d 7373	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · ((0 · i) + (i · (0 −ℝ 𝑏)))) = (0 · 1))
146	127, 145	eqtrd 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 −ℝ 𝑏)))) = (0 · 1))
147		ax-1rid 11121	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℝ → (0 · 1) = 0)
148	112, 147	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 · 1) = 0
149	146, 148	eqtrdi 2792	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 −ℝ 𝑏)))) = 0)
150	149	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (0 · (i · (1 + (0 −ℝ 𝑏)))) = 0)
151	150	oveq1d 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 ∈ ℂ)
153	2	a1i 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 ∈ ℂ)
155	109	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (0 −ℝ 𝑏) ∈ ℂ)
156	154, 155	addcld 11174	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (1 + (0 −ℝ 𝑏)) ∈ ℂ)
157	153, 156	mulcld 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)) → 𝑦 ∈ ℝ)
159	158	recnd 11183	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → 𝑦 ∈ ℂ)
160	152, 157, 159	mulassd 11178	. . . . . . . . . . . . . . . . 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 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)
163	162	oveq2d 7373	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (i · ((1 + (0 −ℝ 𝑏)) · 𝑦)) = (i · 1))
164	163, 19	eqtrdi 2792	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (i · ((1 + (0 −ℝ 𝑏)) · 𝑦)) = i)
165	161, 164	eqtrd 2776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → ((i · (1 + (0 −ℝ 𝑏))) · 𝑦) = i)
166	165	oveq2d 7373	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (0 · ((i · (1 + (0 −ℝ 𝑏))) · 𝑦)) = (0 · i))
167	160, 166	eqtrd 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)
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 2784	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (0 · i) = 0)
171	108, 170	rexlimddv 3158	. . . . . . . . . . . . . 14 ⊢ (((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) → (0 · i) = 0)
172	171	ex 413	. . . . . . . . . . . . 13 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) ≠ 0 → (0 · i) = 0))
173	172	necon1d 2965	. . . . . . . . . . . 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 7372	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) + 𝑏) = (0 + 𝑏))
176	17, 109, 33	addassd 11177	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) + 𝑏) = (1 + ((0 −ℝ 𝑏) + 𝑏)))
177		renegid2 40868	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ℝ → ((0 −ℝ 𝑏) + 𝑏) = 0)
178	32, 177	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑏) + 𝑏) = 0)
179	178	oveq2d 7373	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((0 −ℝ 𝑏) + 𝑏)) = (1 + 0))
180	179, 141	eqtrdi 2792	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((0 −ℝ 𝑏) + 𝑏)) = 1)
181	176, 180	eqtrd 2776	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) + 𝑏) = 1)
182		readdid2 40858	. . . . . . . . . . 11 ⊢ (𝑏 ∈ ℝ → (0 + 𝑏) = 𝑏)
183	32, 182	syl 17	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 + 𝑏) = 𝑏)
184	175, 181, 183	3eqtr3rd 2785	. . . . . . . . 9 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 = 1)
185	184	oveq2d 7373	. . . . . . . 8 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 𝑏) = (i · 1))
186	103, 185	oveq12d 7375	. . . . . . 7 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (i · 𝑏)) = (1 + (i · 1)))
187	5, 186	eqtrd 2776	. . . . . 6 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (1 + (i · 1)))
188	19	oveq2i 7368	. . . . . . . . 9 ⊢ (1 + (i · 1)) = (1 + i)
189	188	eqeq2i 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)))
191	2, 2	mulcli 11162	. . . . . . . . . . . . 13 ⊢ (i · i) ∈ ℂ
192	191, 2	mulcli 11162	. . . . . . . . . . . 12 ⊢ ((i · i) · i) ∈ ℂ
193	192, 1, 2	mulassi 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)
195	192, 194	ax-mp 5	. . . . . . . . . . . 12 ⊢ (((i · i) · i) · 0) = 0
196	195	oveq1i 7367	. . . . . . . . . . 11 ⊢ ((((i · i) · i) · 0) · i) = (0 · i)
197	193, 196	eqtr3i 2766	. . . . . . . . . 10 ⊢ (((i · i) · i) · (0 · i)) = (0 · i)
198		ax-1cn 11109	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
199	192, 198, 2	adddii 11167	. . . . . . . . . . 11 ⊢ (((i · i) · i) · (1 + i)) = ((((i · i) · i) · 1) + (((i · i) · i) · i))
200	191, 2, 198	mulassi 11166	. . . . . . . . . . . . 13 ⊢ (((i · i) · i) · 1) = ((i · i) · (i · 1))
201	19	oveq2i 7368	. . . . . . . . . . . . 13 ⊢ ((i · i) · (i · 1)) = ((i · i) · i)
202	200, 201	eqtri 2764	. . . . . . . . . . . 12 ⊢ (((i · i) · i) · 1) = ((i · i) · i)
203	191, 2, 2	mulassi 11166	. . . . . . . . . . . . 13 ⊢ (((i · i) · i) · i) = ((i · i) · (i · i))
204		rei4 40878	. . . . . . . . . . . . 13 ⊢ ((i · i) · (i · i)) = 1
205	203, 204	eqtri 2764	. . . . . . . . . . . 12 ⊢ (((i · i) · i) · i) = 1
206	202, 205	oveq12i 7369	. . . . . . . . . . 11 ⊢ ((((i · i) · i) · 1) + (((i · i) · i) · i)) = (((i · i) · i) + 1)
207	199, 206	eqtri 2764	. . . . . . . . . 10 ⊢ (((i · i) · i) · (1 + i)) = (((i · i) · i) + 1)
208	190, 197, 207	3eqtr3g 2799	. . . . . . . . 9 ⊢ ((0 · i) = (1 + i) → (0 · i) = (((i · i) · i) + 1))
209	54, 54	readdcli 11170	. . . . . . . . . . 11 ⊢ (1 + 1) ∈ ℝ
210		df-2 12216	. . . . . . . . . . . 12 ⊢ 2 = (1 + 1)
211		sn-0ne2 40861	. . . . . . . . . . . . 13 ⊢ 0 ≠ 2
212	211	necomi 2998	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
213	210, 212	eqnetrri 3015	. . . . . . . . . . 11 ⊢ (1 + 1) ≠ 0
214		ax-rrecex 11123	. . . . . . . . . . 11 ⊢ (((1 + 1) ∈ ℝ ∧ (1 + 1) ≠ 0) → ∃𝑧 ∈ ℝ ((1 + 1) · 𝑧) = 1)
215	209, 213, 214	mp2an 690	. . . . . . . . . 10 ⊢ ∃𝑧 ∈ ℝ ((1 + 1) · 𝑧) = 1
216	192, 198	addcli 11161	. . . . . . . . . . . . . . . . . 18 ⊢ (((i · i) · i) + 1) ∈ ℂ
217	198, 2, 216	addassi 11165	. . . . . . . . . . . . . . . . 17 ⊢ ((1 + i) + (((i · i) · i) + 1)) = (1 + (i + (((i · i) · i) + 1)))
218	2, 192, 198	addassi 11165	. . . . . . . . . . . . . . . . . 18 ⊢ ((i + ((i · i) · i)) + 1) = (i + (((i · i) · i) + 1))
219	218	oveq2i 7368	. . . . . . . . . . . . . . . . 17 ⊢ (1 + ((i + ((i · i) · i)) + 1)) = (1 + (i + (((i · i) · i) + 1)))
220	2, 2, 2	mulassi 11166	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((i · i) · i) = (i · (i · i))
221	220	oveq2i 7368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (i + ((i · i) · i)) = (i + (i · (i · i)))
222		ipiiie0 40892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (i + (i · (i · i))) = 0
223	221, 222	eqtri 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (i + ((i · i) · i)) = 0
224	223	oveq1i 7367	. . . . . . . . . . . . . . . . . . 19 ⊢ ((i + ((i · i) · i)) + 1) = (0 + 1)
225	224, 98	eqtri 2764	. . . . . . . . . . . . . . . . . 18 ⊢ ((i + ((i · i) · i)) + 1) = 1
226	225	oveq2i 7368	. . . . . . . . . . . . . . . . 17 ⊢ (1 + ((i + ((i · i) · i)) + 1)) = (1 + 1)
227	217, 219, 226	3eqtr2i 2770	. . . . . . . . . . . . . . . 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 11167	. . . . . . . . . . . . . . . 16 ⊢ ((0 · i) · (1 + 1)) = (((0 · i) · 1) + ((0 · i) · 1))
230	1, 2, 198	mulassi 11166	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 · i) · 1) = (0 · (i · 1))
231	19	oveq2i 7368	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 · (i · 1)) = (0 · i)
232	230, 231	eqtri 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))
234	232, 233	eqtrid 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))
236	232, 235	eqtrid 2788	. . . . . . . . . . . . . . . . 17 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · 1) = (((i · i) · i) + 1))
237	234, 236	oveq12d 7375	. . . . . . . . . . . . . . . 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	eqtrid 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))
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 2786	. . . . . . . . . . . . . 14 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · (1 + 1)) = (1 · (1 + 1)))
242	241	oveq1d 7372	. . . . . . . . . . . . 13 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (((0 · i) · (1 + 1)) · 𝑧) = ((1 · (1 + 1)) · 𝑧))
243	242	adantr 481	. . . . . . . . . . . 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 11150	. . . . . . . . . . . . . . 15 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 1 ∈ ℂ)
246	245, 245	addcld 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)) → 𝑧 ∈ ℝ)
248	247	recnd 11183	. . . . . . . . . . . . . 14 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 𝑧 ∈ ℂ)
249	244, 246, 248	mulassd 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)
251	250	oveq2d 7373	. . . . . . . . . . . . . 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 2792	. . . . . . . . . . . . 13 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((0 · i) · ((1 + 1) · 𝑧)) = (0 · i))
253	249, 252	eqtrd 2776	. . . . . . . . . . . 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 11178	. . . . . . . . . . . . 13 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((1 · (1 + 1)) · 𝑧) = (1 · ((1 + 1) · 𝑧)))
255	250	oveq2d 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
257	255, 256	eqtrdi 2792	. . . . . . . . . . . . 13 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (1 · ((1 + 1) · 𝑧)) = 1)
258	254, 257	eqtrd 2776	. . . . . . . . . . . 12 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((1 · (1 + 1)) · 𝑧) = 1)
259	243, 253, 258	3eqtr3d 2784	. . . . . . . . . . 11 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (0 · i) = 1)
260	259	rexlimdvaa 3153	. . . . . . . . . 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 685	. . . . . . . 8 ⊢ ((0 · i) = (1 + i) → (0 · i) = 1)
263	189, 262	sylbi 216	. . . . . . 7 ⊢ ((0 · i) = (1 + (i · 1)) → (0 · i) = 1)
264		oveq2 7365	. . . . . . . 8 ⊢ ((0 · i) = 1 → (0 · (0 · i)) = (0 · 1))
265	116, 115	eqtr3i 2766	. . . . . . . 8 ⊢ (0 · (0 · i)) = (0 · i)
266	264, 265, 148	3eqtr3g 2799	. . . . . . 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 798	. . . 4 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) → (0 · i) = 0)
270	269	ex 413	. . 3 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((0 · i) = (𝑎 + (i · 𝑏)) → (0 · i) = 0))
271	270	rexlimivv 3196	. 2 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (0 · i) = (𝑎 + (i · 𝑏)) → (0 · i) = 0)
272	3, 4, 271	mp2b 10	1 ⊢ (0 · i) = 0

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