Theorem sn-0tie0 40070

Description: Lemma for sn-mul02 40071. Commuted version of sn-it0e0 40046. (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 10790	. . 3 ⊢ 0 ∈ ℂ
2		ax-icn 10753	. . 3 ⊢ i ∈ ℂ
3	1, 2	mulcli 10805	. 2 ⊢ (0 · i) ∈ ℂ
4		cnre 10795	. 2 ⊢ ((0 · i) ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (0 · i) = (𝑎 + (i · 𝑏)))
5		simplr 769	. . . . . . 7 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (𝑎 + (i · 𝑏)))
6		neqne 2940	. . . . . . . . . . . 12 ⊢ (¬ (0 · i) = 0 → (0 · i) ≠ 0)
7	6	adantl 485	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) ≠ 0)
8		simplll 775	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 ∈ ℝ)
9		rernegcl 40003	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ ℝ → (0 −ℝ 𝑎) ∈ ℝ)
10	8, 9	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 −ℝ 𝑎) ∈ ℝ)
11		1red 10799	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 1 ∈ ℝ)
12	10, 11	readdcld 10827	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + 1) ∈ ℝ)
13		ax-rrecex 10766	. . . . . . . . . . . . . . 15 ⊢ ((((0 −ℝ 𝑎) + 1) ∈ ℝ ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) → ∃𝑥 ∈ ℝ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)
14	12, 13	sylan 583	. . . . . . . . . . . . . 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 10826	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 −ℝ 𝑎) ∈ ℂ)
17		1cnd 10793	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 1 ∈ ℂ)
18	15, 16, 17	adddid 10822	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · ((0 −ℝ 𝑎) + 1)) = ((i · (0 −ℝ 𝑎)) + (i · 1)))
19		it1ei 40067	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (i · 1) = i
20	19	oveq2i 7202	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((i · (0 −ℝ 𝑎)) + (i · 1)) = ((i · (0 −ℝ 𝑎)) + i)
21	18, 20	eqtrdi 2787	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · ((0 −ℝ 𝑎) + 1)) = ((i · (0 −ℝ 𝑎)) + i))
22	21	oveq2d 7207	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · ((0 −ℝ 𝑎) + 1))) = (0 · ((i · (0 −ℝ 𝑎)) + i)))
23		0cnd 10791	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 0 ∈ ℂ)
24	15, 16	mulcld 10818	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (0 −ℝ 𝑎)) ∈ ℂ)
25	23, 24, 15	adddid 10822	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · ((i · (0 −ℝ 𝑎)) + i)) = ((0 · (i · (0 −ℝ 𝑎))) + (0 · i)))
26	22, 25	eqtrd 2771	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · ((0 −ℝ 𝑎) + 1))) = ((0 · (i · (0 −ℝ 𝑎))) + (0 · i)))
27	5	oveq2d 7207	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + (0 · i)) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏))))
28		renegid2 40045	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ ℝ → ((0 −ℝ 𝑎) + 𝑎) = 0)
29	28	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + 𝑎) = 0)
30	29	oveq1d 7206	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 −ℝ 𝑎) + 𝑎) + (i · 𝑏)) = (0 + (i · 𝑏)))
31	8	recnd 10826	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 ∈ ℂ)
32		simpllr 776	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 ∈ ℝ)
33	32	recnd 10826	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 ∈ ℂ)
34	15, 33	mulcld 10818	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 𝑏) ∈ ℂ)
35	16, 31, 34	addassd 10820	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 −ℝ 𝑎) + 𝑎) + (i · 𝑏)) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏))))
36		sn-addid2 40036	. . . . . . . . . . . . . . . . . . . . . . 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 2779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏))) = (i · 𝑏))
39	27, 38	eqtrd 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + (0 · i)) = (i · 𝑏))
40	39	oveq2d 7207	. . . . . . . . . . . . . . . . . . 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 10822	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · ((0 −ℝ 𝑎) + (0 · i))) = (((0 · i) · (0 −ℝ 𝑎)) + ((0 · i) · (0 · i))))
43	23, 15, 16	mulassd 10821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (0 −ℝ 𝑎)) = (0 · (i · (0 −ℝ 𝑎))))
44	41, 23, 15	mulassd 10821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 · i) · 0) · i) = ((0 · i) · (0 · i)))
45		sn-mul01 40056	. . . . . . . . . . . . . . . . . . . . . . . 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 7206	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 · i) · 0) · i) = (0 · i))
48	44, 47	eqtr3d 2773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (0 · i)) = (0 · i))
49	43, 48	oveq12d 7209	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 · i) · (0 −ℝ 𝑎)) + ((0 · i) · (0 · i))) = ((0 · (i · (0 −ℝ 𝑎))) + (0 · i)))
50	42, 49	eqtrd 2771	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · ((0 −ℝ 𝑎) + (0 · i))) = ((0 · (i · (0 −ℝ 𝑎))) + (0 · i)))
51	23, 15, 34	mulassd 10821	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (i · 𝑏)) = (0 · (i · (i · 𝑏))))
52	15, 15, 33	mulassd 10821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · i) · 𝑏) = (i · (i · 𝑏)))
53		reixi 40053	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (i · i) = (0 −ℝ 1)
54		1re 10798	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 1 ∈ ℝ
55		rernegcl 40003	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1 ∈ ℝ → (0 −ℝ 1) ∈ ℝ)
56	54, 55	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 −ℝ 1) ∈ ℝ
57	53, 56	eqeltri 2827	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (i · i) ∈ ℝ
58	57	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · i) ∈ ℝ)
59	58, 32	remulcld 10828	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · i) · 𝑏) ∈ ℝ)
60	52, 59	eqeltrrd 2832	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (i · 𝑏)) ∈ ℝ)
61		remul02 40037	. . . . . . . . . . . . . . . . . . . . 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 2771	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (i · 𝑏)) = 0)
64	40, 50, 63	3eqtr3d 2779	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · (i · (0 −ℝ 𝑎))) + (0 · i)) = 0)
65	26, 64	eqtrd 2771	. . . . . . . . . . . . . . . . 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 7206	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → ((0 · (i · ((0 −ℝ 𝑎) + 1))) · 𝑥) = (0 · 𝑥))
68		0cnd 10791	. . . . . . . . . . . . . . . . 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 10826	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 −ℝ 𝑎) ∈ ℂ)
72		1cnd 10793	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → 1 ∈ ℂ)
73	71, 72	addcld 10817	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → ((0 −ℝ 𝑎) + 1) ∈ ℂ)
74	69, 73	mulcld 10818	. . . . . . . . . . . . . . . . 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 10826	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → 𝑥 ∈ ℂ)
77	68, 74, 76	mulassd 10821	. . . . . . . . . . . . . . . 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 10821	. . . . . . . . . . . . . . . . . 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 7207	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (i · (((0 −ℝ 𝑎) + 1) · 𝑥)) = (i · 1))
81	80, 19	eqtrdi 2787	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (i · (((0 −ℝ 𝑎) + 1) · 𝑥)) = i)
82	78, 81	eqtrd 2771	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → ((i · ((0 −ℝ 𝑎) + 1)) · 𝑥) = i)
83	82	oveq2d 7207	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 · ((i · ((0 −ℝ 𝑎) + 1)) · 𝑥)) = (0 · i))
84	77, 83	eqtrd 2771	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → ((0 · (i · ((0 −ℝ 𝑎) + 1))) · 𝑥) = (0 · i))
85		remul02 40037	. . . . . . . . . . . . . . . 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 2779	. . . . . . . . . . . . . 14 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 · i) = 0)
88	14, 87	rexlimddv 3200	. . . . . . . . . . . . 13 ⊢ (((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) → (0 · i) = 0)
89	88	ex 416	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 −ℝ 𝑎) + 1) ≠ 0 → (0 · i) = 0))
90	89	necon1d 2954	. . . . . . . . . . 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 7207	. . . . . . . . 9 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + ((0 −ℝ 𝑎) + 1)) = (𝑎 + 0))
93	31, 16, 17	addassd 10820	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 −ℝ 𝑎)) + 1) = (𝑎 + ((0 −ℝ 𝑎) + 1)))
94		renegid 40005	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℝ → (𝑎 + (0 −ℝ 𝑎)) = 0)
95	8, 94	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (0 −ℝ 𝑎)) = 0)
96	95	oveq1d 7206	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 −ℝ 𝑎)) + 1) = (0 + 1))
97		readdid2 40035	. . . . . . . . . . . 12 ⊢ (1 ∈ ℝ → (0 + 1) = 1)
98	54, 97	ax-mp 5	. . . . . . . . . . 11 ⊢ (0 + 1) = 1
99	96, 98	eqtrdi 2787	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 −ℝ 𝑎)) + 1) = 1)
100	93, 99	eqtr3d 2773	. . . . . . . . 9 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + ((0 −ℝ 𝑎) + 1)) = 1)
101		readdid1 40041	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℝ → (𝑎 + 0) = 𝑎)
102	8, 101	syl 17	. . . . . . . . 9 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + 0) = 𝑎)
103	92, 100, 102	3eqtr3rd 2780	. . . . . . . 8 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 = 1)
104		rernegcl 40003	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ ℝ → (0 −ℝ 𝑏) ∈ ℝ)
105	32, 104	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 −ℝ 𝑏) ∈ ℝ)
106	11, 105	readdcld 10827	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + (0 −ℝ 𝑏)) ∈ ℝ)
107		ax-rrecex 10766	. . . . . . . . . . . . . . . 16 ⊢ (((1 + (0 −ℝ 𝑏)) ∈ ℝ ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) → ∃𝑦 ∈ ℝ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)
108	106, 107	sylan 583	. . . . . . . . . . . . . . 15 ⊢ (((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) → ∃𝑦 ∈ ℝ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)
109	105	recnd 10826	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 −ℝ 𝑏) ∈ ℂ)
110	15, 109	mulcld 10818	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (0 −ℝ 𝑏)) ∈ ℂ)
111	23, 15, 110	adddid 10822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i + (i · (0 −ℝ 𝑏)))) = ((0 · i) + (0 · (i · (0 −ℝ 𝑏)))))
112		0re 10800	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ∈ ℝ
113		remul02 40037	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0 ∈ ℝ → (0 · 0) = 0)
114	112, 113	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0 · 0) = 0
115	114	oveq1i 7201	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((0 · 0) · i) = (0 · i)
116	1, 1, 2	mulassi 10809	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((0 · 0) · i) = (0 · (0 · i))
117	115, 116	eqtr3i 2761	. . . . . . . . . . . . . . . . . . . . . . . 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 7206	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (0 · (i · (0 −ℝ 𝑏)))) = ((0 · (0 · i)) + (0 · (i · (0 −ℝ 𝑏)))))
120	111, 119	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i + (i · (0 −ℝ 𝑏)))) = ((0 · (0 · i)) + (0 · (i · (0 −ℝ 𝑏)))))
121	15, 17, 109	adddid 10822	. . . . . . . . . . . . . . . . . . . . . . 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 7206	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · 1) + (i · (0 −ℝ 𝑏))) = (i + (i · (0 −ℝ 𝑏))))
124	121, 123	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (1 + (0 −ℝ 𝑏))) = (i + (i · (0 −ℝ 𝑏))))
125	124	oveq2d 7207	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 −ℝ 𝑏)))) = (0 · (i + (i · (0 −ℝ 𝑏)))))
126	23, 41, 110	adddid 10822	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · ((0 · i) + (i · (0 −ℝ 𝑏)))) = ((0 · (0 · i)) + (0 · (i · (0 −ℝ 𝑏)))))
127	120, 125, 126	3eqtr4d 2781	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 −ℝ 𝑏)))) = (0 · ((0 · i) + (i · (0 −ℝ 𝑏)))))
128	103	oveq1d 7206	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (i · 𝑏)) = (1 + (i · 𝑏)))
129	5, 128	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (1 + (i · 𝑏)))
130	129	oveq1d 7206	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (i · (0 −ℝ 𝑏))) = ((1 + (i · 𝑏)) + (i · (0 −ℝ 𝑏))))
131	17, 34, 110	addassd 10820	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (i · 𝑏)) + (i · (0 −ℝ 𝑏))) = (1 + ((i · 𝑏) + (i · (0 −ℝ 𝑏)))))
132		renegid 40005	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑏 ∈ ℝ → (𝑏 + (0 −ℝ 𝑏)) = 0)
133	32, 132	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑏 + (0 −ℝ 𝑏)) = 0)
134	133	oveq2d 7207	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (𝑏 + (0 −ℝ 𝑏))) = (i · 0))
135	15, 33, 109	adddid 10822	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (𝑏 + (0 −ℝ 𝑏))) = ((i · 𝑏) + (i · (0 −ℝ 𝑏))))
136		sn-mul01 40056	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2779	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · 𝑏) + (i · (0 −ℝ 𝑏))) = 0)
139	138	oveq2d 7207	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((i · 𝑏) + (i · (0 −ℝ 𝑏)))) = (1 + 0))
140		readdid1 40041	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1 ∈ ℝ → (1 + 0) = 1)
141	54, 140	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1 + 0) = 1
142	139, 141	eqtrdi 2787	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((i · 𝑏) + (i · (0 −ℝ 𝑏)))) = 1)
143	131, 142	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (i · 𝑏)) + (i · (0 −ℝ 𝑏))) = 1)
144	130, 143	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (i · (0 −ℝ 𝑏))) = 1)
145	144	oveq2d 7207	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · ((0 · i) + (i · (0 −ℝ 𝑏)))) = (0 · 1))
146	127, 145	eqtrd 2771	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 −ℝ 𝑏)))) = (0 · 1))
147		ax-1rid 10764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℝ → (0 · 1) = 0)
148	112, 147	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 · 1) = 0
149	146, 148	eqtrdi 2787	. . . . . . . . . . . . . . . . . 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 7206	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → ((0 · (i · (1 + (0 −ℝ 𝑏)))) · 𝑦) = (0 · 𝑦))
152		0cnd 10791	. . . . . . . . . . . . . . . . . 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 10793	. . . . . . . . . . . . . . . . . . . 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 10817	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (1 + (0 −ℝ 𝑏)) ∈ ℂ)
157	153, 156	mulcld 10818	. . . . . . . . . . . . . . . . . 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 10826	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → 𝑦 ∈ ℂ)
160	152, 157, 159	mulassd 10821	. . . . . . . . . . . . . . . . 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 10821	. . . . . . . . . . . . . . . . . . 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 7207	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (i · ((1 + (0 −ℝ 𝑏)) · 𝑦)) = (i · 1))
164	163, 19	eqtrdi 2787	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (i · ((1 + (0 −ℝ 𝑏)) · 𝑦)) = i)
165	161, 164	eqtrd 2771	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → ((i · (1 + (0 −ℝ 𝑏))) · 𝑦) = i)
166	165	oveq2d 7207	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (0 · ((i · (1 + (0 −ℝ 𝑏))) · 𝑦)) = (0 · i))
167	160, 166	eqtrd 2771	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → ((0 · (i · (1 + (0 −ℝ 𝑏)))) · 𝑦) = (0 · i))
168		remul02 40037	. . . . . . . . . . . . . . . . 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 2779	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (0 · i) = 0)
171	108, 170	rexlimddv 3200	. . . . . . . . . . . . . 14 ⊢ (((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) → (0 · i) = 0)
172	171	ex 416	. . . . . . . . . . . . 13 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) ≠ 0 → (0 · i) = 0))
173	172	necon1d 2954	. . . . . . . . . . . 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 7206	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) + 𝑏) = (0 + 𝑏))
176	17, 109, 33	addassd 10820	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) + 𝑏) = (1 + ((0 −ℝ 𝑏) + 𝑏)))
177		renegid2 40045	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ℝ → ((0 −ℝ 𝑏) + 𝑏) = 0)
178	32, 177	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑏) + 𝑏) = 0)
179	178	oveq2d 7207	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((0 −ℝ 𝑏) + 𝑏)) = (1 + 0))
180	179, 141	eqtrdi 2787	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((0 −ℝ 𝑏) + 𝑏)) = 1)
181	176, 180	eqtrd 2771	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) + 𝑏) = 1)
182		readdid2 40035	. . . . . . . . . . 11 ⊢ (𝑏 ∈ ℝ → (0 + 𝑏) = 𝑏)
183	32, 182	syl 17	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 + 𝑏) = 𝑏)
184	175, 181, 183	3eqtr3rd 2780	. . . . . . . . 9 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 = 1)
185	184	oveq2d 7207	. . . . . . . 8 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 𝑏) = (i · 1))
186	103, 185	oveq12d 7209	. . . . . . 7 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (i · 𝑏)) = (1 + (i · 1)))
187	5, 186	eqtrd 2771	. . . . . 6 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (1 + (i · 1)))
188	19	oveq2i 7202	. . . . . . . . 9 ⊢ (1 + (i · 1)) = (1 + i)
189	188	eqeq2i 2749	. . . . . . . 8 ⊢ ((0 · i) = (1 + (i · 1)) ↔ (0 · i) = (1 + i))
190		oveq2 7199	. . . . . . . . . 10 ⊢ ((0 · i) = (1 + i) → (((i · i) · i) · (0 · i)) = (((i · i) · i) · (1 + i)))
191	2, 2	mulcli 10805	. . . . . . . . . . . . 13 ⊢ (i · i) ∈ ℂ
192	191, 2	mulcli 10805	. . . . . . . . . . . 12 ⊢ ((i · i) · i) ∈ ℂ
193	192, 1, 2	mulassi 10809	. . . . . . . . . . 11 ⊢ ((((i · i) · i) · 0) · i) = (((i · i) · i) · (0 · i))
194		sn-mul01 40056	. . . . . . . . . . . . 13 ⊢ (((i · i) · i) ∈ ℂ → (((i · i) · i) · 0) = 0)
195	192, 194	ax-mp 5	. . . . . . . . . . . 12 ⊢ (((i · i) · i) · 0) = 0
196	195	oveq1i 7201	. . . . . . . . . . 11 ⊢ ((((i · i) · i) · 0) · i) = (0 · i)
197	193, 196	eqtr3i 2761	. . . . . . . . . 10 ⊢ (((i · i) · i) · (0 · i)) = (0 · i)
198		ax-1cn 10752	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
199	192, 198, 2	adddii 10810	. . . . . . . . . . 11 ⊢ (((i · i) · i) · (1 + i)) = ((((i · i) · i) · 1) + (((i · i) · i) · i))
200	191, 2, 198	mulassi 10809	. . . . . . . . . . . . 13 ⊢ (((i · i) · i) · 1) = ((i · i) · (i · 1))
201	19	oveq2i 7202	. . . . . . . . . . . . 13 ⊢ ((i · i) · (i · 1)) = ((i · i) · i)
202	200, 201	eqtri 2759	. . . . . . . . . . . 12 ⊢ (((i · i) · i) · 1) = ((i · i) · i)
203	191, 2, 2	mulassi 10809	. . . . . . . . . . . . 13 ⊢ (((i · i) · i) · i) = ((i · i) · (i · i))
204		rei4 40054	. . . . . . . . . . . . 13 ⊢ ((i · i) · (i · i)) = 1
205	203, 204	eqtri 2759	. . . . . . . . . . . 12 ⊢ (((i · i) · i) · i) = 1
206	202, 205	oveq12i 7203	. . . . . . . . . . 11 ⊢ ((((i · i) · i) · 1) + (((i · i) · i) · i)) = (((i · i) · i) + 1)
207	199, 206	eqtri 2759	. . . . . . . . . 10 ⊢ (((i · i) · i) · (1 + i)) = (((i · i) · i) + 1)
208	190, 197, 207	3eqtr3g 2794	. . . . . . . . 9 ⊢ ((0 · i) = (1 + i) → (0 · i) = (((i · i) · i) + 1))
209	54, 54	readdcli 10813	. . . . . . . . . . 11 ⊢ (1 + 1) ∈ ℝ
210		df-2 11858	. . . . . . . . . . . 12 ⊢ 2 = (1 + 1)
211		sn-0ne2 40038	. . . . . . . . . . . . 13 ⊢ 0 ≠ 2
212	211	necomi 2986	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
213	210, 212	eqnetrri 3003	. . . . . . . . . . 11 ⊢ (1 + 1) ≠ 0
214		ax-rrecex 10766	. . . . . . . . . . 11 ⊢ (((1 + 1) ∈ ℝ ∧ (1 + 1) ≠ 0) → ∃𝑧 ∈ ℝ ((1 + 1) · 𝑧) = 1)
215	209, 213, 214	mp2an 692	. . . . . . . . . 10 ⊢ ∃𝑧 ∈ ℝ ((1 + 1) · 𝑧) = 1
216	192, 198	addcli 10804	. . . . . . . . . . . . . . . . . 18 ⊢ (((i · i) · i) + 1) ∈ ℂ
217	198, 2, 216	addassi 10808	. . . . . . . . . . . . . . . . 17 ⊢ ((1 + i) + (((i · i) · i) + 1)) = (1 + (i + (((i · i) · i) + 1)))
218	2, 192, 198	addassi 10808	. . . . . . . . . . . . . . . . . 18 ⊢ ((i + ((i · i) · i)) + 1) = (i + (((i · i) · i) + 1))
219	218	oveq2i 7202	. . . . . . . . . . . . . . . . 17 ⊢ (1 + ((i + ((i · i) · i)) + 1)) = (1 + (i + (((i · i) · i) + 1)))
220	2, 2, 2	mulassi 10809	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((i · i) · i) = (i · (i · i))
221	220	oveq2i 7202	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (i + ((i · i) · i)) = (i + (i · (i · i)))
222		ipiiie0 40068	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (i + (i · (i · i))) = 0
223	221, 222	eqtri 2759	. . . . . . . . . . . . . . . . . . . 20 ⊢ (i + ((i · i) · i)) = 0
224	223	oveq1i 7201	. . . . . . . . . . . . . . . . . . 19 ⊢ ((i + ((i · i) · i)) + 1) = (0 + 1)
225	224, 98	eqtri 2759	. . . . . . . . . . . . . . . . . 18 ⊢ ((i + ((i · i) · i)) + 1) = 1
226	225	oveq2i 7202	. . . . . . . . . . . . . . . . 17 ⊢ (1 + ((i + ((i · i) · i)) + 1)) = (1 + 1)
227	217, 219, 226	3eqtr2i 2765	. . . . . . . . . . . . . . . 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 10810	. . . . . . . . . . . . . . . 16 ⊢ ((0 · i) · (1 + 1)) = (((0 · i) · 1) + ((0 · i) · 1))
230	1, 2, 198	mulassi 10809	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 · i) · 1) = (0 · (i · 1))
231	19	oveq2i 7202	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 · (i · 1)) = (0 · i)
232	230, 231	eqtri 2759	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 · i) · 1) = (0 · i)
233		simpl 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (0 · i) = (1 + i))
234	232, 233	syl5eq 2783	. . . . . . . . . . . . . . . . 17 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · 1) = (1 + i))
235		simpr 488	. . . . . . . . . . . . . . . . . 18 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (0 · i) = (((i · i) · i) + 1))
236	232, 235	syl5eq 2783	. . . . . . . . . . . . . . . . 17 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · 1) = (((i · i) · i) + 1))
237	234, 236	oveq12d 7209	. . . . . . . . . . . . . . . 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 2783	. . . . . . . . . . . . . . 15 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · (1 + 1)) = ((1 + i) + (((i · i) · i) + 1)))
239		remulid2 40064	. . . . . . . . . . . . . . . 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 2781	. . . . . . . . . . . . . 14 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · (1 + 1)) = (1 · (1 + 1)))
242	241	oveq1d 7206	. . . . . . . . . . . . 13 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → (((0 · i) · (1 + 1)) · 𝑧) = ((1 · (1 + 1)) · 𝑧))
243	242	adantr 484	. . . . . . . . . . . 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 10793	. . . . . . . . . . . . . . 15 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 1 ∈ ℂ)
246	245, 245	addcld 10817	. . . . . . . . . . . . . 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 10826	. . . . . . . . . . . . . 14 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 𝑧 ∈ ℂ)
249	244, 246, 248	mulassd 10821	. . . . . . . . . . . . 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 7207	. . . . . . . . . . . . . 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 2787	. . . . . . . . . . . . 13 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((0 · i) · ((1 + 1) · 𝑧)) = (0 · i))
253	249, 252	eqtrd 2771	. . . . . . . . . . . 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 10821	. . . . . . . . . . . . 13 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((1 · (1 + 1)) · 𝑧) = (1 · ((1 + 1) · 𝑧)))
255	250	oveq2d 7207	. . . . . . . . . . . . . 14 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (1 · ((1 + 1) · 𝑧)) = (1 · 1))
256		1t1e1ALT 39940	. . . . . . . . . . . . . 14 ⊢ (1 · 1) = 1
257	255, 256	eqtrdi 2787	. . . . . . . . . . . . 13 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (1 · ((1 + 1) · 𝑧)) = 1)
258	254, 257	eqtrd 2771	. . . . . . . . . . . 12 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((1 · (1 + 1)) · 𝑧) = 1)
259	243, 253, 258	3eqtr3d 2779	. . . . . . . . . . 11 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (0 · i) = 1)
260	259	rexlimdvaa 3194	. . . . . . . . . 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 7199	. . . . . . . 8 ⊢ ((0 · i) = 1 → (0 · (0 · i)) = (0 · 1))
265	116, 115	eqtr3i 2761	. . . . . . . 8 ⊢ (0 · (0 · i)) = (0 · i)
266	264, 265, 148	3eqtr3g 2794	. . . . . . 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 416	. . 3 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((0 · i) = (𝑎 + (i · 𝑏)) → (0 · i) = 0))
271	270	rexlimivv 3201	. 2 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (0 · i) = (𝑎 + (i · 𝑏)) → (0 · i) = 0)
272	3, 4, 271	mp2b 10	1 ⊢ (0 · i) = 0

Syntax hints:  ¬ wn 3   ∧ wa 399   = wceq 1543   ∈ wcel 2112   ≠ wne 2932  ∃wrex 3052  (class class class)co 7191  ℂcc 10692  ℝcr 10693  0cc0 10694  1c1 10695  ici 10696   + caddc 10697   · cmul 10699  2c2 11850   −_ℝ cresub 39997

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501  ax-resscn 10751  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-addrcl 10755  ax-mulcl 10756  ax-mulrcl 10757  ax-addass 10759  ax-mulass 10760  ax-distr 10761  ax-i2m1 10762  ax-1ne0 10763  ax-1rid 10764  ax-rnegex 10765  ax-rrecex 10766  ax-cnre 10767  ax-pre-lttri 10768  ax-pre-lttrn 10769  ax-pre-ltadd 10770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-nel 3037  df-ral 3056  df-rex 3057  df-reu 3058  df-rmo 3059  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-po 5453  df-so 5454  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-riota 7148  df-ov 7194  df-oprab 7195  df-mpo 7196  df-er 8369  df-en 8605  df-dom 8606  df-sdom 8607  df-pnf 10834  df-mnf 10835  df-ltxr 10837  df-2 11858  df-3 11859  df-resub 39998

This theorem is referenced by:  sn-mul02  40071  retire  40086