Theorem sn-0tie0 40342

Description: Lemma for sn-mul02 40343. Commuted version of sn-it0e0 40318. (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 10898	. . 3 ⊢ 0 ∈ ℂ
2		ax-icn 10861	. . 3 ⊢ i ∈ ℂ
3	1, 2	mulcli 10913	. 2 ⊢ (0 · i) ∈ ℂ
4		cnre 10903	. 2 ⊢ ((0 · i) ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (0 · i) = (𝑎 + (i · 𝑏)))
5		simplr 765	. . . . . . 7 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (𝑎 + (i · 𝑏)))
6		neqne 2950	. . . . . . . . . . . 12 ⊢ (¬ (0 · i) = 0 → (0 · i) ≠ 0)
7	6	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) ≠ 0)
8		simplll 771	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 ∈ ℝ)
9		rernegcl 40275	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ ℝ → (0 −ℝ 𝑎) ∈ ℝ)
10	8, 9	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 −ℝ 𝑎) ∈ ℝ)
11		1red 10907	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 1 ∈ ℝ)
12	10, 11	readdcld 10935	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + 1) ∈ ℝ)
13		ax-rrecex 10874	. . . . . . . . . . . . . . 15 ⊢ ((((0 −ℝ 𝑎) + 1) ∈ ℝ ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) → ∃𝑥 ∈ ℝ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)
14	12, 13	sylan 579	. . . . . . . . . . . . . 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 10934	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 −ℝ 𝑎) ∈ ℂ)
17		1cnd 10901	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 1 ∈ ℂ)
18	15, 16, 17	adddid 10930	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · ((0 −ℝ 𝑎) + 1)) = ((i · (0 −ℝ 𝑎)) + (i · 1)))
19		it1ei 40339	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (i · 1) = i
20	19	oveq2i 7266	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((i · (0 −ℝ 𝑎)) + (i · 1)) = ((i · (0 −ℝ 𝑎)) + i)
21	18, 20	eqtrdi 2795	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · ((0 −ℝ 𝑎) + 1)) = ((i · (0 −ℝ 𝑎)) + i))
22	21	oveq2d 7271	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · ((0 −ℝ 𝑎) + 1))) = (0 · ((i · (0 −ℝ 𝑎)) + i)))
23		0cnd 10899	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 0 ∈ ℂ)
24	15, 16	mulcld 10926	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (0 −ℝ 𝑎)) ∈ ℂ)
25	23, 24, 15	adddid 10930	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · ((i · (0 −ℝ 𝑎)) + i)) = ((0 · (i · (0 −ℝ 𝑎))) + (0 · i)))
26	22, 25	eqtrd 2778	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · ((0 −ℝ 𝑎) + 1))) = ((0 · (i · (0 −ℝ 𝑎))) + (0 · i)))
27	5	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + (0 · i)) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏))))
28		renegid2 40317	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ ℝ → ((0 −ℝ 𝑎) + 𝑎) = 0)
29	28	ad3antrrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + 𝑎) = 0)
30	29	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 −ℝ 𝑎) + 𝑎) + (i · 𝑏)) = (0 + (i · 𝑏)))
31	8	recnd 10934	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 ∈ ℂ)
32		simpllr 772	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 ∈ ℝ)
33	32	recnd 10934	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 ∈ ℂ)
34	15, 33	mulcld 10926	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 𝑏) ∈ ℂ)
35	16, 31, 34	addassd 10928	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 −ℝ 𝑎) + 𝑎) + (i · 𝑏)) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏))))
36		sn-addid2 40308	. . . . . . . . . . . . . . . . . . . . . . 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 2786	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏))) = (i · 𝑏))
39	27, 38	eqtrd 2778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + (0 · i)) = (i · 𝑏))
40	39	oveq2d 7271	. . . . . . . . . . . . . . . . . . 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 10930	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · ((0 −ℝ 𝑎) + (0 · i))) = (((0 · i) · (0 −ℝ 𝑎)) + ((0 · i) · (0 · i))))
43	23, 15, 16	mulassd 10929	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (0 −ℝ 𝑎)) = (0 · (i · (0 −ℝ 𝑎))))
44	41, 23, 15	mulassd 10929	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 · i) · 0) · i) = ((0 · i) · (0 · i)))
45		sn-mul01 40328	. . . . . . . . . . . . . . . . . . . . . . . 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 7270	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 · i) · 0) · i) = (0 · i))
48	44, 47	eqtr3d 2780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (0 · i)) = (0 · i))
49	43, 48	oveq12d 7273	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 · i) · (0 −ℝ 𝑎)) + ((0 · i) · (0 · i))) = ((0 · (i · (0 −ℝ 𝑎))) + (0 · i)))
50	42, 49	eqtrd 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · ((0 −ℝ 𝑎) + (0 · i))) = ((0 · (i · (0 −ℝ 𝑎))) + (0 · i)))
51	23, 15, 34	mulassd 10929	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (i · 𝑏)) = (0 · (i · (i · 𝑏))))
52	15, 15, 33	mulassd 10929	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · i) · 𝑏) = (i · (i · 𝑏)))
53		reixi 40325	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (i · i) = (0 −ℝ 1)
54		1re 10906	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 1 ∈ ℝ
55		rernegcl 40275	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1 ∈ ℝ → (0 −ℝ 1) ∈ ℝ)
56	54, 55	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 −ℝ 1) ∈ ℝ
57	53, 56	eqeltri 2835	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (i · i) ∈ ℝ
58	57	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · i) ∈ ℝ)
59	58, 32	remulcld 10936	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · i) · 𝑏) ∈ ℝ)
60	52, 59	eqeltrrd 2840	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (i · 𝑏)) ∈ ℝ)
61		remul02 40309	. . . . . . . . . . . . . . . . . . . . 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 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (i · 𝑏)) = 0)
64	40, 50, 63	3eqtr3d 2786	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · (i · (0 −ℝ 𝑎))) + (0 · i)) = 0)
65	26, 64	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · ((0 −ℝ 𝑎) + 1))) = 0)
66	65	ad2antrr 722	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 · (i · ((0 −ℝ 𝑎) + 1))) = 0)
67	66	oveq1d 7270	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → ((0 · (i · ((0 −ℝ 𝑎) + 1))) · 𝑥) = (0 · 𝑥))
68		0cnd 10899	. . . . . . . . . . . . . . . . 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 722	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 −ℝ 𝑎) ∈ ℝ)
71	70	recnd 10934	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 −ℝ 𝑎) ∈ ℂ)
72		1cnd 10901	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → 1 ∈ ℂ)
73	71, 72	addcld 10925	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → ((0 −ℝ 𝑎) + 1) ∈ ℂ)
74	69, 73	mulcld 10926	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (i · ((0 −ℝ 𝑎) + 1)) ∈ ℂ)
75		simprl 767	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → 𝑥 ∈ ℝ)
76	75	recnd 10934	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → 𝑥 ∈ ℂ)
77	68, 74, 76	mulassd 10929	. . . . . . . . . . . . . . . 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 10929	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → ((i · ((0 −ℝ 𝑎) + 1)) · 𝑥) = (i · (((0 −ℝ 𝑎) + 1) · 𝑥)))
79		simprr 769	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)
80	79	oveq2d 7271	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (i · (((0 −ℝ 𝑎) + 1) · 𝑥)) = (i · 1))
81	80, 19	eqtrdi 2795	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (i · (((0 −ℝ 𝑎) + 1) · 𝑥)) = i)
82	78, 81	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → ((i · ((0 −ℝ 𝑎) + 1)) · 𝑥) = i)
83	82	oveq2d 7271	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 · ((i · ((0 −ℝ 𝑎) + 1)) · 𝑥)) = (0 · i))
84	77, 83	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → ((0 · (i · ((0 −ℝ 𝑎) + 1))) · 𝑥) = (0 · i))
85		remul02 40309	. . . . . . . . . . . . . . . 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 2786	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 · i) = 0)
88	14, 87	rexlimddv 3219	. . . . . . . . . . . . 13 ⊢ (((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) → (0 · i) = 0)
89	88	ex 412	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 −ℝ 𝑎) + 1) ≠ 0 → (0 · i) = 0))
90	89	necon1d 2964	. . . . . . . . . . 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 7271	. . . . . . . . 9 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + ((0 −ℝ 𝑎) + 1)) = (𝑎 + 0))
93	31, 16, 17	addassd 10928	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 −ℝ 𝑎)) + 1) = (𝑎 + ((0 −ℝ 𝑎) + 1)))
94		renegid 40277	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℝ → (𝑎 + (0 −ℝ 𝑎)) = 0)
95	8, 94	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (0 −ℝ 𝑎)) = 0)
96	95	oveq1d 7270	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 −ℝ 𝑎)) + 1) = (0 + 1))
97		readdid2 40307	. . . . . . . . . . . 12 ⊢ (1 ∈ ℝ → (0 + 1) = 1)
98	54, 97	ax-mp 5	. . . . . . . . . . 11 ⊢ (0 + 1) = 1
99	96, 98	eqtrdi 2795	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 −ℝ 𝑎)) + 1) = 1)
100	93, 99	eqtr3d 2780	. . . . . . . . 9 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + ((0 −ℝ 𝑎) + 1)) = 1)
101		readdid1 40313	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℝ → (𝑎 + 0) = 𝑎)
102	8, 101	syl 17	. . . . . . . . 9 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + 0) = 𝑎)
103	92, 100, 102	3eqtr3rd 2787	. . . . . . . 8 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 = 1)
104		rernegcl 40275	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ ℝ → (0 −ℝ 𝑏) ∈ ℝ)
105	32, 104	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 −ℝ 𝑏) ∈ ℝ)
106	11, 105	readdcld 10935	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + (0 −ℝ 𝑏)) ∈ ℝ)
107		ax-rrecex 10874	. . . . . . . . . . . . . . . 16 ⊢ (((1 + (0 −ℝ 𝑏)) ∈ ℝ ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) → ∃𝑦 ∈ ℝ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)
108	106, 107	sylan 579	. . . . . . . . . . . . . . 15 ⊢ (((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) → ∃𝑦 ∈ ℝ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)
109	105	recnd 10934	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 −ℝ 𝑏) ∈ ℂ)
110	15, 109	mulcld 10926	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (0 −ℝ 𝑏)) ∈ ℂ)
111	23, 15, 110	adddid 10930	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i + (i · (0 −ℝ 𝑏)))) = ((0 · i) + (0 · (i · (0 −ℝ 𝑏)))))
112		0re 10908	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ∈ ℝ
113		remul02 40309	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0 ∈ ℝ → (0 · 0) = 0)
114	112, 113	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0 · 0) = 0
115	114	oveq1i 7265	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((0 · 0) · i) = (0 · i)
116	1, 1, 2	mulassi 10917	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((0 · 0) · i) = (0 · (0 · i))
117	115, 116	eqtr3i 2768	. . . . . . . . . . . . . . . . . . . . . . . 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 7270	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (0 · (i · (0 −ℝ 𝑏)))) = ((0 · (0 · i)) + (0 · (i · (0 −ℝ 𝑏)))))
120	111, 119	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i + (i · (0 −ℝ 𝑏)))) = ((0 · (0 · i)) + (0 · (i · (0 −ℝ 𝑏)))))
121	15, 17, 109	adddid 10930	. . . . . . . . . . . . . . . . . . . . . . 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 7270	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · 1) + (i · (0 −ℝ 𝑏))) = (i + (i · (0 −ℝ 𝑏))))
124	121, 123	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (1 + (0 −ℝ 𝑏))) = (i + (i · (0 −ℝ 𝑏))))
125	124	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 −ℝ 𝑏)))) = (0 · (i + (i · (0 −ℝ 𝑏)))))
126	23, 41, 110	adddid 10930	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · ((0 · i) + (i · (0 −ℝ 𝑏)))) = ((0 · (0 · i)) + (0 · (i · (0 −ℝ 𝑏)))))
127	120, 125, 126	3eqtr4d 2788	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 −ℝ 𝑏)))) = (0 · ((0 · i) + (i · (0 −ℝ 𝑏)))))
128	103	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (i · 𝑏)) = (1 + (i · 𝑏)))
129	5, 128	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (1 + (i · 𝑏)))
130	129	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (i · (0 −ℝ 𝑏))) = ((1 + (i · 𝑏)) + (i · (0 −ℝ 𝑏))))
131	17, 34, 110	addassd 10928	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (i · 𝑏)) + (i · (0 −ℝ 𝑏))) = (1 + ((i · 𝑏) + (i · (0 −ℝ 𝑏)))))
132		renegid 40277	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑏 ∈ ℝ → (𝑏 + (0 −ℝ 𝑏)) = 0)
133	32, 132	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑏 + (0 −ℝ 𝑏)) = 0)
134	133	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (𝑏 + (0 −ℝ 𝑏))) = (i · 0))
135	15, 33, 109	adddid 10930	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (𝑏 + (0 −ℝ 𝑏))) = ((i · 𝑏) + (i · (0 −ℝ 𝑏))))
136		sn-mul01 40328	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2786	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · 𝑏) + (i · (0 −ℝ 𝑏))) = 0)
139	138	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((i · 𝑏) + (i · (0 −ℝ 𝑏)))) = (1 + 0))
140		readdid1 40313	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1 ∈ ℝ → (1 + 0) = 1)
141	54, 140	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1 + 0) = 1
142	139, 141	eqtrdi 2795	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((i · 𝑏) + (i · (0 −ℝ 𝑏)))) = 1)
143	131, 142	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (i · 𝑏)) + (i · (0 −ℝ 𝑏))) = 1)
144	130, 143	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (i · (0 −ℝ 𝑏))) = 1)
145	144	oveq2d 7271	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · ((0 · i) + (i · (0 −ℝ 𝑏)))) = (0 · 1))
146	127, 145	eqtrd 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 −ℝ 𝑏)))) = (0 · 1))
147		ax-1rid 10872	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℝ → (0 · 1) = 0)
148	112, 147	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 · 1) = 0
149	146, 148	eqtrdi 2795	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 −ℝ 𝑏)))) = 0)
150	149	ad2antrr 722	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (0 · (i · (1 + (0 −ℝ 𝑏)))) = 0)
151	150	oveq1d 7270	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → ((0 · (i · (1 + (0 −ℝ 𝑏)))) · 𝑦) = (0 · 𝑦))
152		0cnd 10899	. . . . . . . . . . . . . . . . . 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 10901	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → 1 ∈ ℂ)
155	109	ad2antrr 722	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (0 −ℝ 𝑏) ∈ ℂ)
156	154, 155	addcld 10925	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (1 + (0 −ℝ 𝑏)) ∈ ℂ)
157	153, 156	mulcld 10926	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (i · (1 + (0 −ℝ 𝑏))) ∈ ℂ)
158		simprl 767	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → 𝑦 ∈ ℝ)
159	158	recnd 10934	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → 𝑦 ∈ ℂ)
160	152, 157, 159	mulassd 10929	. . . . . . . . . . . . . . . . 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 10929	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → ((i · (1 + (0 −ℝ 𝑏))) · 𝑦) = (i · ((1 + (0 −ℝ 𝑏)) · 𝑦)))
162		simprr 769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)
163	162	oveq2d 7271	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (i · ((1 + (0 −ℝ 𝑏)) · 𝑦)) = (i · 1))
164	163, 19	eqtrdi 2795	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (i · ((1 + (0 −ℝ 𝑏)) · 𝑦)) = i)
165	161, 164	eqtrd 2778	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → ((i · (1 + (0 −ℝ 𝑏))) · 𝑦) = i)
166	165	oveq2d 7271	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (0 · ((i · (1 + (0 −ℝ 𝑏))) · 𝑦)) = (0 · i))
167	160, 166	eqtrd 2778	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → ((0 · (i · (1 + (0 −ℝ 𝑏)))) · 𝑦) = (0 · i))
168		remul02 40309	. . . . . . . . . . . . . . . . 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 2786	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (0 · i) = 0)
171	108, 170	rexlimddv 3219	. . . . . . . . . . . . . 14 ⊢ (((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) → (0 · i) = 0)
172	171	ex 412	. . . . . . . . . . . . 13 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) ≠ 0 → (0 · i) = 0))
173	172	necon1d 2964	. . . . . . . . . . . 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 7270	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) + 𝑏) = (0 + 𝑏))
176	17, 109, 33	addassd 10928	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) + 𝑏) = (1 + ((0 −ℝ 𝑏) + 𝑏)))
177		renegid2 40317	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ℝ → ((0 −ℝ 𝑏) + 𝑏) = 0)
178	32, 177	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑏) + 𝑏) = 0)
179	178	oveq2d 7271	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((0 −ℝ 𝑏) + 𝑏)) = (1 + 0))
180	179, 141	eqtrdi 2795	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((0 −ℝ 𝑏) + 𝑏)) = 1)
181	176, 180	eqtrd 2778	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) + 𝑏) = 1)
182		readdid2 40307	. . . . . . . . . . 11 ⊢ (𝑏 ∈ ℝ → (0 + 𝑏) = 𝑏)
183	32, 182	syl 17	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 + 𝑏) = 𝑏)
184	175, 181, 183	3eqtr3rd 2787	. . . . . . . . 9 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 = 1)
185	184	oveq2d 7271	. . . . . . . 8 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 𝑏) = (i · 1))
186	103, 185	oveq12d 7273	. . . . . . 7 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (i · 𝑏)) = (1 + (i · 1)))
187	5, 186	eqtrd 2778	. . . . . 6 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (1 + (i · 1)))
188	19	oveq2i 7266	. . . . . . . . 9 ⊢ (1 + (i · 1)) = (1 + i)
189	188	eqeq2i 2751	. . . . . . . 8 ⊢ ((0 · i) = (1 + (i · 1)) ↔ (0 · i) = (1 + i))
190		oveq2 7263	. . . . . . . . . 10 ⊢ ((0 · i) = (1 + i) → (((i · i) · i) · (0 · i)) = (((i · i) · i) · (1 + i)))
191	2, 2	mulcli 10913	. . . . . . . . . . . . 13 ⊢ (i · i) ∈ ℂ
192	191, 2	mulcli 10913	. . . . . . . . . . . 12 ⊢ ((i · i) · i) ∈ ℂ
193	192, 1, 2	mulassi 10917	. . . . . . . . . . 11 ⊢ ((((i · i) · i) · 0) · i) = (((i · i) · i) · (0 · i))
194		sn-mul01 40328	. . . . . . . . . . . . 13 ⊢ (((i · i) · i) ∈ ℂ → (((i · i) · i) · 0) = 0)
195	192, 194	ax-mp 5	. . . . . . . . . . . 12 ⊢ (((i · i) · i) · 0) = 0
196	195	oveq1i 7265	. . . . . . . . . . 11 ⊢ ((((i · i) · i) · 0) · i) = (0 · i)
197	193, 196	eqtr3i 2768	. . . . . . . . . 10 ⊢ (((i · i) · i) · (0 · i)) = (0 · i)
198		ax-1cn 10860	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
199	192, 198, 2	adddii 10918	. . . . . . . . . . 11 ⊢ (((i · i) · i) · (1 + i)) = ((((i · i) · i) · 1) + (((i · i) · i) · i))
200	191, 2, 198	mulassi 10917	. . . . . . . . . . . . 13 ⊢ (((i · i) · i) · 1) = ((i · i) · (i · 1))
201	19	oveq2i 7266	. . . . . . . . . . . . 13 ⊢ ((i · i) · (i · 1)) = ((i · i) · i)
202	200, 201	eqtri 2766	. . . . . . . . . . . 12 ⊢ (((i · i) · i) · 1) = ((i · i) · i)
203	191, 2, 2	mulassi 10917	. . . . . . . . . . . . 13 ⊢ (((i · i) · i) · i) = ((i · i) · (i · i))
204		rei4 40326	. . . . . . . . . . . . 13 ⊢ ((i · i) · (i · i)) = 1
205	203, 204	eqtri 2766	. . . . . . . . . . . 12 ⊢ (((i · i) · i) · i) = 1
206	202, 205	oveq12i 7267	. . . . . . . . . . 11 ⊢ ((((i · i) · i) · 1) + (((i · i) · i) · i)) = (((i · i) · i) + 1)
207	199, 206	eqtri 2766	. . . . . . . . . 10 ⊢ (((i · i) · i) · (1 + i)) = (((i · i) · i) + 1)
208	190, 197, 207	3eqtr3g 2802	. . . . . . . . 9 ⊢ ((0 · i) = (1 + i) → (0 · i) = (((i · i) · i) + 1))
209	54, 54	readdcli 10921	. . . . . . . . . . 11 ⊢ (1 + 1) ∈ ℝ
210		df-2 11966	. . . . . . . . . . . 12 ⊢ 2 = (1 + 1)
211		sn-0ne2 40310	. . . . . . . . . . . . 13 ⊢ 0 ≠ 2
212	211	necomi 2997	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
213	210, 212	eqnetrri 3014	. . . . . . . . . . 11 ⊢ (1 + 1) ≠ 0
214		ax-rrecex 10874	. . . . . . . . . . 11 ⊢ (((1 + 1) ∈ ℝ ∧ (1 + 1) ≠ 0) → ∃𝑧 ∈ ℝ ((1 + 1) · 𝑧) = 1)
215	209, 213, 214	mp2an 688	. . . . . . . . . 10 ⊢ ∃𝑧 ∈ ℝ ((1 + 1) · 𝑧) = 1
216	192, 198	addcli 10912	. . . . . . . . . . . . . . . . . 18 ⊢ (((i · i) · i) + 1) ∈ ℂ
217	198, 2, 216	addassi 10916	. . . . . . . . . . . . . . . . 17 ⊢ ((1 + i) + (((i · i) · i) + 1)) = (1 + (i + (((i · i) · i) + 1)))
218	2, 192, 198	addassi 10916	. . . . . . . . . . . . . . . . . 18 ⊢ ((i + ((i · i) · i)) + 1) = (i + (((i · i) · i) + 1))
219	218	oveq2i 7266	. . . . . . . . . . . . . . . . 17 ⊢ (1 + ((i + ((i · i) · i)) + 1)) = (1 + (i + (((i · i) · i) + 1)))
220	2, 2, 2	mulassi 10917	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((i · i) · i) = (i · (i · i))
221	220	oveq2i 7266	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (i + ((i · i) · i)) = (i + (i · (i · i)))
222		ipiiie0 40340	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (i + (i · (i · i))) = 0
223	221, 222	eqtri 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (i + ((i · i) · i)) = 0
224	223	oveq1i 7265	. . . . . . . . . . . . . . . . . . 19 ⊢ ((i + ((i · i) · i)) + 1) = (0 + 1)
225	224, 98	eqtri 2766	. . . . . . . . . . . . . . . . . 18 ⊢ ((i + ((i · i) · i)) + 1) = 1
226	225	oveq2i 7266	. . . . . . . . . . . . . . . . 17 ⊢ (1 + ((i + ((i · i) · i)) + 1)) = (1 + 1)
227	217, 219, 226	3eqtr2i 2772	. . . . . . . . . . . . . . . 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 10918	. . . . . . . . . . . . . . . 16 ⊢ ((0 · i) · (1 + 1)) = (((0 · i) · 1) + ((0 · i) · 1))
230	1, 2, 198	mulassi 10917	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 · i) · 1) = (0 · (i · 1))
231	19	oveq2i 7266	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 · (i · 1)) = (0 · i)
232	230, 231	eqtri 2766	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 · i) · 1) = (0 · i)
233		simpl 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (0 · i) = (1 + i))
234	232, 233	syl5eq 2791	. . . . . . . . . . . . . . . . 17 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · 1) = (1 + i))
235		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (0 · i) = (((i · i) · i) + 1))
236	232, 235	syl5eq 2791	. . . . . . . . . . . . . . . . 17 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · 1) = (((i · i) · i) + 1))
237	234, 236	oveq12d 7273	. . . . . . . . . . . . . . . 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 2791	. . . . . . . . . . . . . . 15 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · (1 + 1)) = ((1 + i) + (((i · i) · i) + 1)))
239		remulid2 40336	. . . . . . . . . . . . . . . 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 2788	. . . . . . . . . . . . . 14 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · (1 + 1)) = (1 · (1 + 1)))
242	241	oveq1d 7270	. . . . . . . . . . . . 13 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (((0 · i) · (1 + 1)) · 𝑧) = ((1 · (1 + 1)) · 𝑧))
243	242	adantr 480	. . . . . . . . . . . 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 10901	. . . . . . . . . . . . . . 15 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 1 ∈ ℂ)
246	245, 245	addcld 10925	. . . . . . . . . . . . . 14 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (1 + 1) ∈ ℂ)
247		simprl 767	. . . . . . . . . . . . . . 15 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 𝑧 ∈ ℝ)
248	247	recnd 10934	. . . . . . . . . . . . . 14 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 𝑧 ∈ ℂ)
249	244, 246, 248	mulassd 10929	. . . . . . . . . . . . 13 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (((0 · i) · (1 + 1)) · 𝑧) = ((0 · i) · ((1 + 1) · 𝑧)))
250		simprr 769	. . . . . . . . . . . . . . 15 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((1 + 1) · 𝑧) = 1)
251	250	oveq2d 7271	. . . . . . . . . . . . . 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 2795	. . . . . . . . . . . . 13 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((0 · i) · ((1 + 1) · 𝑧)) = (0 · i))
253	249, 252	eqtrd 2778	. . . . . . . . . . . 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 10929	. . . . . . . . . . . . 13 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((1 · (1 + 1)) · 𝑧) = (1 · ((1 + 1) · 𝑧)))
255	250	oveq2d 7271	. . . . . . . . . . . . . 14 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (1 · ((1 + 1) · 𝑧)) = (1 · 1))
256		1t1e1ALT 40213	. . . . . . . . . . . . . 14 ⊢ (1 · 1) = 1
257	255, 256	eqtrdi 2795	. . . . . . . . . . . . 13 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (1 · ((1 + 1) · 𝑧)) = 1)
258	254, 257	eqtrd 2778	. . . . . . . . . . . 12 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((1 · (1 + 1)) · 𝑧) = 1)
259	243, 253, 258	3eqtr3d 2786	. . . . . . . . . . 11 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (0 · i) = 1)
260	259	rexlimdvaa 3213	. . . . . . . . . 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 683	. . . . . . . 8 ⊢ ((0 · i) = (1 + i) → (0 · i) = 1)
263	189, 262	sylbi 216	. . . . . . 7 ⊢ ((0 · i) = (1 + (i · 1)) → (0 · i) = 1)
264		oveq2 7263	. . . . . . . 8 ⊢ ((0 · i) = 1 → (0 · (0 · i)) = (0 · 1))
265	116, 115	eqtr3i 2768	. . . . . . . 8 ⊢ (0 · (0 · i)) = (0 · i)
266	264, 265, 148	3eqtr3g 2802	. . . . . . 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 796	. . . 4 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) → (0 · i) = 0)
270	269	ex 412	. . 3 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((0 · i) = (𝑎 + (i · 𝑏)) → (0 · i) = 0))
271	270	rexlimivv 3220	. 2 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (0 · i) = (𝑎 + (i · 𝑏)) → (0 · i) = 0)
272	3, 4, 271	mp2b 10	1 ⊢ (0 · i) = 0

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  ∃wrex 3064  (class class class)co 7255  ℂcc 10800  ℝcr 10801  0cc0 10802  1c1 10803  ici 10804   + caddc 10805   · cmul 10807  2c2 11958   −_ℝ cresub 40269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-ltxr 10945  df-2 11966  df-3 11967  df-resub 40270

This theorem is referenced by:  sn-mul02  40343  retire  40358