Theorem sn-0tie0 42474

Description: Lemma for sn-mul02 42475. Commuted version of sn-it0e0 42450. (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 11254	. . 3 ⊢ 0 ∈ ℂ
2		ax-icn 11215	. . 3 ⊢ i ∈ ℂ
3	1, 2	mulcli 11269	. 2 ⊢ (0 · i) ∈ ℂ
4		cnre 11259	. 2 ⊢ ((0 · i) ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (0 · i) = (𝑎 + (i · 𝑏)))
5		simplr 768	. . . . . . 7 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) = (𝑎 + (i · 𝑏)))
6		neqne 2947	. . . . . . . . . . . 12 ⊢ (¬ (0 · i) = 0 → (0 · i) ≠ 0)
7	6	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · i) ≠ 0)
8		simplll 774	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 ∈ ℝ)
9		rernegcl 42406	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ ℝ → (0 −ℝ 𝑎) ∈ ℝ)
10	8, 9	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 −ℝ 𝑎) ∈ ℝ)
11		1red 11263	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 1 ∈ ℝ)
12	10, 11	readdcld 11291	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + 1) ∈ ℝ)
13		ax-rrecex 11228	. . . . . . . . . . . . . . 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 11290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 −ℝ 𝑎) ∈ ℂ)
17		1cnd 11257	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 1 ∈ ℂ)
18	15, 16, 17	adddid 11286	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · ((0 −ℝ 𝑎) + 1)) = ((i · (0 −ℝ 𝑎)) + (i · 1)))
19		sn-it1ei 42471	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (i · 1) = i
20	19	oveq2i 7443	. . . . . . . . . . . . . . . . . . . . 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 7448	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · ((0 −ℝ 𝑎) + 1))) = (0 · ((i · (0 −ℝ 𝑎)) + i)))
23		0cnd 11255	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 0 ∈ ℂ)
24	15, 16	mulcld 11282	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (0 −ℝ 𝑎)) ∈ ℂ)
25	23, 24, 15	adddid 11286	. . . . . . . . . . . . . . . . . . 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 7448	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + (0 · i)) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏))))
28		renegid2 42448	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ ℝ → ((0 −ℝ 𝑎) + 𝑎) = 0)
29	28	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑎) + 𝑎) = 0)
30	29	oveq1d 7447	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 −ℝ 𝑎) + 𝑎) + (i · 𝑏)) = (0 + (i · 𝑏)))
31	8	recnd 11290	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑎 ∈ ℂ)
32		simpllr 775	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 ∈ ℝ)
33	32	recnd 11290	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → 𝑏 ∈ ℂ)
34	15, 33	mulcld 11282	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 𝑏) ∈ ℂ)
35	16, 31, 34	addassd 11284	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 −ℝ 𝑎) + 𝑎) + (i · 𝑏)) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏))))
36		sn-addlid 42439	. . . . . . . . . . . . . . . . . . . . . . 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 7448	. . . . . . . . . . . . . . . . . . 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 11286	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · ((0 −ℝ 𝑎) + (0 · i))) = (((0 · i) · (0 −ℝ 𝑎)) + ((0 · i) · (0 · i))))
43	23, 15, 16	mulassd 11285	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (0 −ℝ 𝑎)) = (0 · (i · (0 −ℝ 𝑎))))
44	41, 23, 15	mulassd 11285	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (((0 · i) · 0) · i) = ((0 · i) · (0 · i)))
45		sn-mul01 42460	. . . . . . . . . . . . . . . . . . . . . . . 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 7447	. . . . . . . . . . . . . . . . . . . . . 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 7450	. . . . . . . . . . . . . . . . . . . 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 11285	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) · (i · 𝑏)) = (0 · (i · (i · 𝑏))))
52	15, 15, 33	mulassd 11285	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · i) · 𝑏) = (i · (i · 𝑏)))
53		reixi 42457	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (i · i) = (0 −ℝ 1)
54		1re 11262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 1 ∈ ℝ
55		rernegcl 42406	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1 ∈ ℝ → (0 −ℝ 1) ∈ ℝ)
56	54, 55	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 −ℝ 1) ∈ ℝ
57	53, 56	eqeltri 2836	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (i · i) ∈ ℝ
58	57	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · i) ∈ ℝ)
59	58, 32	remulcld 11292	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((i · i) · 𝑏) ∈ ℝ)
60	52, 59	eqeltrrd 2841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (i · 𝑏)) ∈ ℝ)
61		remul02 42440	. . . . . . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 · (i · ((0 −ℝ 𝑎) + 1))) = 0)
67	66	oveq1d 7447	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → ((0 · (i · ((0 −ℝ 𝑎) + 1))) · 𝑥) = (0 · 𝑥))
68		0cnd 11255	. . . . . . . . . . . . . . . . 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 11290	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 −ℝ 𝑎) ∈ ℂ)
72		1cnd 11257	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → 1 ∈ ℂ)
73	71, 72	addcld 11281	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → ((0 −ℝ 𝑎) + 1) ∈ ℂ)
74	69, 73	mulcld 11282	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (i · ((0 −ℝ 𝑎) + 1)) ∈ ℂ)
75		simprl 770	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → 𝑥 ∈ ℝ)
76	75	recnd 11290	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → 𝑥 ∈ ℂ)
77	68, 74, 76	mulassd 11285	. . . . . . . . . . . . . . . 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 11285	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → ((i · ((0 −ℝ 𝑎) + 1)) · 𝑥) = (i · (((0 −ℝ 𝑎) + 1) · 𝑥)))
79		simprr 772	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0 −ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)) → (((0 −ℝ 𝑎) + 1) · 𝑥) = 1)
80	79	oveq2d 7448	. . . . . . . . . . . . . . . . . . 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 7448	. . . . . . . . . . . . . . . 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 42440	. . . . . . . . . . . . . . . 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 3160	. . . . . . . . . . . . 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 2961	. . . . . . . . . . 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 7448	. . . . . . . . 9 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + ((0 −ℝ 𝑎) + 1)) = (𝑎 + 0))
93	31, 16, 17	addassd 11284	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 −ℝ 𝑎)) + 1) = (𝑎 + ((0 −ℝ 𝑎) + 1)))
94		renegid 42408	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℝ → (𝑎 + (0 −ℝ 𝑎)) = 0)
95	8, 94	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑎 + (0 −ℝ 𝑎)) = 0)
96	95	oveq1d 7447	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((𝑎 + (0 −ℝ 𝑎)) + 1) = (0 + 1))
97		readdlid 42438	. . . . . . . . . . . 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		readdrid 42444	. . . . . . . . . 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 42406	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ ℝ → (0 −ℝ 𝑏) ∈ ℝ)
105	32, 104	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 −ℝ 𝑏) ∈ ℝ)
106	11, 105	readdcld 11291	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + (0 −ℝ 𝑏)) ∈ ℝ)
107		ax-rrecex 11228	. . . . . . . . . . . . . . . 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 11290	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 −ℝ 𝑏) ∈ ℂ)
110	15, 109	mulcld 11282	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (0 −ℝ 𝑏)) ∈ ℂ)
111	23, 15, 110	adddid 11286	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i + (i · (0 −ℝ 𝑏)))) = ((0 · i) + (0 · (i · (0 −ℝ 𝑏)))))
112		0re 11264	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ∈ ℝ
113		remul02 42440	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (0 ∈ ℝ → (0 · 0) = 0)
114	112, 113	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0 · 0) = 0
115	114	oveq1i 7442	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((0 · 0) · i) = (0 · i)
116	1, 1, 2	mulassi 11273	. . . . . . . . . . . . . . . . . . . . . . . . 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 7447	. . . . . . . . . . . . . . . . . . . . . 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 11286	. . . . . . . . . . . . . . . . . . . . . . 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 7447	. . . . . . . . . . . . . . . . . . . . . . 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 7448	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (0 · (i · (1 + (0 −ℝ 𝑏)))) = (0 · (i + (i · (0 −ℝ 𝑏)))))
126	23, 41, 110	adddid 11286	. . . . . . . . . . . . . . . . . . . . 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 7447	. . . . . . . . . . . . . . . . . . . . . . . 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 7447	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 · i) + (i · (0 −ℝ 𝑏))) = ((1 + (i · 𝑏)) + (i · (0 −ℝ 𝑏))))
131	17, 34, 110	addassd 11284	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (i · 𝑏)) + (i · (0 −ℝ 𝑏))) = (1 + ((i · 𝑏) + (i · (0 −ℝ 𝑏)))))
132		renegid 42408	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑏 ∈ ℝ → (𝑏 + (0 −ℝ 𝑏)) = 0)
133	32, 132	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (𝑏 + (0 −ℝ 𝑏)) = 0)
134	133	oveq2d 7448	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (𝑏 + (0 −ℝ 𝑏))) = (i · 0))
135	15, 33, 109	adddid 11286	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · (𝑏 + (0 −ℝ 𝑏))) = ((i · 𝑏) + (i · (0 −ℝ 𝑏))))
136		sn-mul01 42460	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 7448	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (1 + ((i · 𝑏) + (i · (0 −ℝ 𝑏)))) = (1 + 0))
140		readdrid 42444	. . . . . . . . . . . . . . . . . . . . . . . . 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 7448	. . . . . . . . . . . . . . . . . . . 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 11226	. . . . . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (0 · (i · (1 + (0 −ℝ 𝑏)))) = 0)
151	150	oveq1d 7447	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → ((0 · (i · (1 + (0 −ℝ 𝑏)))) · 𝑦) = (0 · 𝑦))
152		0cnd 11255	. . . . . . . . . . . . . . . . . 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 11257	. . . . . . . . . . . . . . . . . . . 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 11281	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (1 + (0 −ℝ 𝑏)) ∈ ℂ)
157	153, 156	mulcld 11282	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → (i · (1 + (0 −ℝ 𝑏))) ∈ ℂ)
158		simprl 770	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → 𝑦 ∈ ℝ)
159	158	recnd 11290	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → 𝑦 ∈ ℂ)
160	152, 157, 159	mulassd 11285	. . . . . . . . . . . . . . . . 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 11285	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → ((i · (1 + (0 −ℝ 𝑏))) · 𝑦) = (i · ((1 + (0 −ℝ 𝑏)) · 𝑦)))
162		simprr 772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1 + (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)) → ((1 + (0 −ℝ 𝑏)) · 𝑦) = 1)
163	162	oveq2d 7448	. . . . . . . . . . . . . . . . . . . 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 7448	. . . . . . . . . . . . . . . . 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 42440	. . . . . . . . . . . . . . . . 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 3160	. . . . . . . . . . . . . 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 2961	. . . . . . . . . . . 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 7447	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) + 𝑏) = (0 + 𝑏))
176	17, 109, 33	addassd 11284	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) + 𝑏) = (1 + ((0 −ℝ 𝑏) + 𝑏)))
177		renegid2 42448	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ℝ → ((0 −ℝ 𝑏) + 𝑏) = 0)
178	32, 177	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → ((0 −ℝ 𝑏) + 𝑏) = 0)
179	178	oveq2d 7448	. . . . . . . . . . . 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		readdlid 42438	. . . . . . . . . . 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 7448	. . . . . . . 8 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) → (i · 𝑏) = (i · 1))
186	103, 185	oveq12d 7450	. . . . . . 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 7443	. . . . . . . . 9 ⊢ (1 + (i · 1)) = (1 + i)
189	188	eqeq2i 2749	. . . . . . . 8 ⊢ ((0 · i) = (1 + (i · 1)) ↔ (0 · i) = (1 + i))
190		oveq2 7440	. . . . . . . . . 10 ⊢ ((0 · i) = (1 + i) → (((i · i) · i) · (0 · i)) = (((i · i) · i) · (1 + i)))
191	2, 2	mulcli 11269	. . . . . . . . . . . . 13 ⊢ (i · i) ∈ ℂ
192	191, 2	mulcli 11269	. . . . . . . . . . . 12 ⊢ ((i · i) · i) ∈ ℂ
193	192, 1, 2	mulassi 11273	. . . . . . . . . . 11 ⊢ ((((i · i) · i) · 0) · i) = (((i · i) · i) · (0 · i))
194		sn-mul01 42460	. . . . . . . . . . . . 13 ⊢ (((i · i) · i) ∈ ℂ → (((i · i) · i) · 0) = 0)
195	192, 194	ax-mp 5	. . . . . . . . . . . 12 ⊢ (((i · i) · i) · 0) = 0
196	195	oveq1i 7442	. . . . . . . . . . 11 ⊢ ((((i · i) · i) · 0) · i) = (0 · i)
197	193, 196	eqtr3i 2766	. . . . . . . . . 10 ⊢ (((i · i) · i) · (0 · i)) = (0 · i)
198		ax-1cn 11214	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
199	192, 198, 2	adddii 11274	. . . . . . . . . . 11 ⊢ (((i · i) · i) · (1 + i)) = ((((i · i) · i) · 1) + (((i · i) · i) · i))
200	191, 2, 198	mulassi 11273	. . . . . . . . . . . . 13 ⊢ (((i · i) · i) · 1) = ((i · i) · (i · 1))
201	19	oveq2i 7443	. . . . . . . . . . . . 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 11273	. . . . . . . . . . . . 13 ⊢ (((i · i) · i) · i) = ((i · i) · (i · i))
204		rei4 42458	. . . . . . . . . . . . 13 ⊢ ((i · i) · (i · i)) = 1
205	203, 204	eqtri 2764	. . . . . . . . . . . 12 ⊢ (((i · i) · i) · i) = 1
206	202, 205	oveq12i 7444	. . . . . . . . . . 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 11277	. . . . . . . . . . 11 ⊢ (1 + 1) ∈ ℝ
210		df-2 12330	. . . . . . . . . . . 12 ⊢ 2 = (1 + 1)
211		sn-0ne2 42441	. . . . . . . . . . . . 13 ⊢ 0 ≠ 2
212	211	necomi 2994	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
213	210, 212	eqnetrri 3011	. . . . . . . . . . 11 ⊢ (1 + 1) ≠ 0
214		ax-rrecex 11228	. . . . . . . . . . 11 ⊢ (((1 + 1) ∈ ℝ ∧ (1 + 1) ≠ 0) → ∃𝑧 ∈ ℝ ((1 + 1) · 𝑧) = 1)
215	209, 213, 214	mp2an 692	. . . . . . . . . 10 ⊢ ∃𝑧 ∈ ℝ ((1 + 1) · 𝑧) = 1
216	192, 198	addcli 11268	. . . . . . . . . . . . . . . . . 18 ⊢ (((i · i) · i) + 1) ∈ ℂ
217	198, 2, 216	addassi 11272	. . . . . . . . . . . . . . . . 17 ⊢ ((1 + i) + (((i · i) · i) + 1)) = (1 + (i + (((i · i) · i) + 1)))
218	2, 192, 198	addassi 11272	. . . . . . . . . . . . . . . . . 18 ⊢ ((i + ((i · i) · i)) + 1) = (i + (((i · i) · i) + 1))
219	218	oveq2i 7443	. . . . . . . . . . . . . . . . 17 ⊢ (1 + ((i + ((i · i) · i)) + 1)) = (1 + (i + (((i · i) · i) + 1)))
220	2, 2, 2	mulassi 11273	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((i · i) · i) = (i · (i · i))
221	220	oveq2i 7443	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (i + ((i · i) · i)) = (i + (i · (i · i)))
222		ipiiie0 42472	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (i + (i · (i · i))) = 0
223	221, 222	eqtri 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (i + ((i · i) · i)) = 0
224	223	oveq1i 7442	. . . . . . . . . . . . . . . . . . 19 ⊢ ((i + ((i · i) · i)) + 1) = (0 + 1)
225	224, 98	eqtri 2764	. . . . . . . . . . . . . . . . . 18 ⊢ ((i + ((i · i) · i)) + 1) = 1
226	225	oveq2i 7443	. . . . . . . . . . . . . . . . 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 11274	. . . . . . . . . . . . . . . 16 ⊢ ((0 · i) · (1 + 1)) = (((0 · i) · 1) + ((0 · i) · 1))
230	1, 2, 198	mulassi 11273	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 · i) · 1) = (0 · (i · 1))
231	19	oveq2i 7443	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 · (i · 1)) = (0 · i)
232	230, 231	eqtri 2764	. . . . . . . . . . . . . . . . . 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	eqtrid 2788	. . . . . . . . . . . . . . . . 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	eqtrid 2788	. . . . . . . . . . . . . . . . 17 ⊢ (((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) → ((0 · i) · 1) = (((i · i) · i) + 1))
237	234, 236	oveq12d 7450	. . . . . . . . . . . . . . . 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		remullid 42468	. . . . . . . . . . . . . . . 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 7447	. . . . . . . . . . . . 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 11257	. . . . . . . . . . . . . . 15 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 1 ∈ ℂ)
246	245, 245	addcld 11281	. . . . . . . . . . . . . 14 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (1 + 1) ∈ ℂ)
247		simprl 770	. . . . . . . . . . . . . . 15 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 𝑧 ∈ ℝ)
248	247	recnd 11290	. . . . . . . . . . . . . 14 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → 𝑧 ∈ ℂ)
249	244, 246, 248	mulassd 11285	. . . . . . . . . . . . 13 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (((0 · i) · (1 + 1)) · 𝑧) = ((0 · i) · ((1 + 1) · 𝑧)))
250		simprr 772	. . . . . . . . . . . . . . 15 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((1 + 1) · 𝑧) = 1)
251	250	oveq2d 7448	. . . . . . . . . . . . . 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 11285	. . . . . . . . . . . . 13 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → ((1 · (1 + 1)) · 𝑧) = (1 · ((1 + 1) · 𝑧)))
255	250	oveq2d 7448	. . . . . . . . . . . . . 14 ⊢ ((((0 · i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1)) ∧ (𝑧 ∈ ℝ ∧ ((1 + 1) · 𝑧) = 1)) → (1 · ((1 + 1) · 𝑧)) = (1 · 1))
256		1t1e1ALT 42296	. . . . . . . . . . . . . 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 3155	. . . . . . . . . 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 217	. . . . . . 7 ⊢ ((0 · i) = (1 + (i · 1)) → (0 · i) = 1)
264		oveq2 7440	. . . . . . . 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 799	. . . 4 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) → (0 · i) = 0)
270	269	ex 412	. . 3 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((0 · i) = (𝑎 + (i · 𝑏)) → (0 · i) = 0))
271	270	rexlimivv 3200	. 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 2107   ≠ wne 2939  ∃wrex 3069  (class class class)co 7432  ℂcc 11154  ℝcr 11155  0cc0 11156  1c1 11157  ici 11158   + caddc 11159   · cmul 11161  2c2 12322   −_ℝ cresub 42400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-po 5591  df-so 5592  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-er 8746  df-en 8987  df-dom 8988  df-sdom 8989  df-pnf 11298  df-mnf 11299  df-ltxr 11301  df-2 12330  df-3 12331  df-resub 42401

This theorem is referenced by:  sn-mul02  42475  sn-retire  42504