sn-0tie0

Description: Lemma for sn-mul02 . Commuted version of sn-it0e0 . (Contributed by SN, 30-Jun-2024)

		Ref	Expression
	Assertion	sn-0tie0	$⊢ 0 \cdot i = 0$

Proof

Step	Hyp	Ref	Expression
1		0cn	$⊢ 0 \in ℂ$
2		ax-icn	$⊢ i \in ℂ$
3	1 2	mulcli	$⊢ 0 \cdot i \in ℂ$
4		cnre	$⊢ 0 \cdot i \in ℂ \to \exists a \in ℝ \exists b \in ℝ 0 \cdot i = a + i b$
5		simplr	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i = a + i b$
6		neqne	$⊢ \neg 0 \cdot i = 0 \to 0 \cdot i \neq 0$
7	6	adantl	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i \neq 0$
8		simplll	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to a \in ℝ$
9		rernegcl	$⊢ a \in ℝ \to 0 -_{ℝ} a \in ℝ$
10	8 9	syl	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 -_{ℝ} a \in ℝ$
11		1red	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 1 \in ℝ$
12	10 11	readdcld	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to (0 -_{ℝ} a) + 1 \in ℝ$
13		ax-rrecex	$⊢ ((0 -_{ℝ} a) + 1 \in ℝ \land (0 -_{ℝ} a) + 1 \neq 0) \to \exists x \in ℝ ((0 -_{ℝ} a) + 1) x = 1$
14	12 13	sylan	$⊢ ((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \to \exists x \in ℝ ((0 -_{ℝ} a) + 1) x = 1$
15	2	a1i	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to i \in ℂ$
16	10	recnd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 -_{ℝ} a \in ℂ$
17		1cnd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 1 \in ℂ$
18	15 16 17	adddid	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to i ((0 -_{ℝ} a) + 1) = i (0 -_{ℝ} a) + i \cdot 1$
19		sn-it1ei	$⊢ i \cdot 1 = i$
20	19	oveq2i	$⊢ i (0 -_{ℝ} a) + i \cdot 1 = i (0 -_{ℝ} a) + i$
21	18 20	eqtrdi	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to i ((0 -_{ℝ} a) + 1) = i (0 -_{ℝ} a) + i$
22	21	oveq2d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i ((0 -_{ℝ} a) + 1) = 0 \cdot (i (0 -_{ℝ} a) + i)$
23		0cnd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \in ℂ$
24	15 16	mulcld	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to i (0 -_{ℝ} a) \in ℂ$
25	23 24 15	adddid	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot (i (0 -_{ℝ} a) + i) = 0 \cdot i (0 -_{ℝ} a) + 0 \cdot i$
26	22 25	eqtrd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i ((0 -_{ℝ} a) + 1) = 0 \cdot i (0 -_{ℝ} a) + 0 \cdot i$
27	5	oveq2d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to (0 -_{ℝ} a) + 0 \cdot i = (0 -_{ℝ} a) + a + i b$
28		renegid2	$⊢ a \in ℝ \to (0 -_{ℝ} a) + a = 0$
29	28	ad3antrrr	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to (0 -_{ℝ} a) + a = 0$
30	29	oveq1d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to (0 -_{ℝ} a) + a + i b = 0 + i b$
31	8	recnd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to a \in ℂ$
32		simpllr	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to b \in ℝ$
33	32	recnd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to b \in ℂ$
34	15 33	mulcld	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to i b \in ℂ$
35	16 31 34	addassd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to (0 -_{ℝ} a) + a + i b = (0 -_{ℝ} a) + a + i b$
36		sn-addlid	$⊢ i b \in ℂ \to 0 + i b = i b$
37	34 36	syl	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 + i b = i b$
38	30 35 37	3eqtr3d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to (0 -_{ℝ} a) + a + i b = i b$
39	27 38	eqtrd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to (0 -_{ℝ} a) + 0 \cdot i = i b$
40	39	oveq2d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i ((0 -_{ℝ} a) + 0 \cdot i) = 0 \cdot i i b$
41	3	a1i	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i \in ℂ$
42	41 16 41	adddid	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i ((0 -_{ℝ} a) + 0 \cdot i) = 0 \cdot i (0 -_{ℝ} a) + 0 \cdot i 0 \cdot i$
43	23 15 16	mulassd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i (0 -_{ℝ} a) = 0 \cdot i (0 -_{ℝ} a)$
44	41 23 15	mulassd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i \cdot 0 i = 0 \cdot i 0 \cdot i$
45		sn-mul01	$⊢ 0 \cdot i \in ℂ \to 0 \cdot i \cdot 0 = 0$
46	41 45	syl	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i \cdot 0 = 0$
47	46	oveq1d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i \cdot 0 i = 0 \cdot i$
48	44 47	eqtr3d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i 0 \cdot i = 0 \cdot i$
49	43 48	oveq12d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i (0 -_{ℝ} a) + 0 \cdot i 0 \cdot i = 0 \cdot i (0 -_{ℝ} a) + 0 \cdot i$
50	42 49	eqtrd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i ((0 -_{ℝ} a) + 0 \cdot i) = 0 \cdot i (0 -_{ℝ} a) + 0 \cdot i$
51	23 15 34	mulassd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i i b = 0 \cdot i i b$
52	15 15 33	mulassd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to i i b = i i b$
53		reixi	$⊢ i i = 0 -_{ℝ} 1$
54		1re	$⊢ 1 \in ℝ$
55		rernegcl	$⊢ 1 \in ℝ \to 0 -_{ℝ} 1 \in ℝ$
56	54 55	ax-mp	$⊢ 0 -_{ℝ} 1 \in ℝ$
57	53 56	eqeltri	$⊢ i i \in ℝ$
58	57	a1i	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to i i \in ℝ$
59	58 32	remulcld	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to i i b \in ℝ$
60	52 59	eqeltrrd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to i i b \in ℝ$
61		remul02	$⊢ i i b \in ℝ \to 0 \cdot i i b = 0$
62	60 61	syl	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i i b = 0$
63	51 62	eqtrd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i i b = 0$
64	40 50 63	3eqtr3d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i (0 -_{ℝ} a) + 0 \cdot i = 0$
65	26 64	eqtrd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i ((0 -_{ℝ} a) + 1) = 0$
66	65	ad2antrr	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \land (x \in ℝ \land ((0 -_{ℝ} a) + 1) x = 1)) \to 0 \cdot i ((0 -_{ℝ} a) + 1) = 0$
67	66	oveq1d	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \land (x \in ℝ \land ((0 -_{ℝ} a) + 1) x = 1)) \to 0 \cdot i ((0 -_{ℝ} a) + 1) x = 0 \cdot x$
68		0cnd	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \land (x \in ℝ \land ((0 -_{ℝ} a) + 1) x = 1)) \to 0 \in ℂ$
69	2	a1i	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \land (x \in ℝ \land ((0 -_{ℝ} a) + 1) x = 1)) \to i \in ℂ$
70	10	ad2antrr	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \land (x \in ℝ \land ((0 -_{ℝ} a) + 1) x = 1)) \to 0 -_{ℝ} a \in ℝ$
71	70	recnd	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \land (x \in ℝ \land ((0 -_{ℝ} a) + 1) x = 1)) \to 0 -_{ℝ} a \in ℂ$
72		1cnd	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \land (x \in ℝ \land ((0 -_{ℝ} a) + 1) x = 1)) \to 1 \in ℂ$
73	71 72	addcld	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \land (x \in ℝ \land ((0 -_{ℝ} a) + 1) x = 1)) \to (0 -_{ℝ} a) + 1 \in ℂ$
74	69 73	mulcld	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \land (x \in ℝ \land ((0 -_{ℝ} a) + 1) x = 1)) \to i ((0 -_{ℝ} a) + 1) \in ℂ$
75		simprl	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \land (x \in ℝ \land ((0 -_{ℝ} a) + 1) x = 1)) \to x \in ℝ$
76	75	recnd	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \land (x \in ℝ \land ((0 -_{ℝ} a) + 1) x = 1)) \to x \in ℂ$
77	68 74 76	mulassd	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \land (x \in ℝ \land ((0 -_{ℝ} a) + 1) x = 1)) \to 0 \cdot i ((0 -_{ℝ} a) + 1) x = 0 \cdot i ((0 -_{ℝ} a) + 1) x$
78	69 73 76	mulassd	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \land (x \in ℝ \land ((0 -_{ℝ} a) + 1) x = 1)) \to i ((0 -_{ℝ} a) + 1) x = i ((0 -_{ℝ} a) + 1) x$
79		simprr	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \land (x \in ℝ \land ((0 -_{ℝ} a) + 1) x = 1)) \to ((0 -_{ℝ} a) + 1) x = 1$
80	79	oveq2d	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \land (x \in ℝ \land ((0 -_{ℝ} a) + 1) x = 1)) \to i ((0 -_{ℝ} a) + 1) x = i \cdot 1$
81	80 19	eqtrdi	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \land (x \in ℝ \land ((0 -_{ℝ} a) + 1) x = 1)) \to i ((0 -_{ℝ} a) + 1) x = i$
82	78 81	eqtrd	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \land (x \in ℝ \land ((0 -_{ℝ} a) + 1) x = 1)) \to i ((0 -_{ℝ} a) + 1) x = i$
83	82	oveq2d	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \land (x \in ℝ \land ((0 -_{ℝ} a) + 1) x = 1)) \to 0 \cdot i ((0 -_{ℝ} a) + 1) x = 0 \cdot i$
84	77 83	eqtrd	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \land (x \in ℝ \land ((0 -_{ℝ} a) + 1) x = 1)) \to 0 \cdot i ((0 -_{ℝ} a) + 1) x = 0 \cdot i$
85		remul02	$⊢ x \in ℝ \to 0 \cdot x = 0$
86	75 85	syl	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \land (x \in ℝ \land ((0 -_{ℝ} a) + 1) x = 1)) \to 0 \cdot x = 0$
87	67 84 86	3eqtr3d	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \land (x \in ℝ \land ((0 -_{ℝ} a) + 1) x = 1)) \to 0 \cdot i = 0$
88	14 87	rexlimddv	$⊢ ((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land (0 -_{ℝ} a) + 1 \neq 0) \to 0 \cdot i = 0$
89	88	ex	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to ((0 -_{ℝ} a) + 1 \neq 0 \to 0 \cdot i = 0)$
90	89	necon1d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to (0 \cdot i \neq 0 \to (0 -_{ℝ} a) + 1 = 0)$
91	7 90	mpd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to (0 -_{ℝ} a) + 1 = 0$
92	91	oveq2d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to a + (0 -_{ℝ} a) + 1 = a + 0$
93	31 16 17	addassd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to a + (0 -_{ℝ} a) + 1 = a + (0 -_{ℝ} a) + 1$
94		renegid	$⊢ a \in ℝ \to a + (0 -_{ℝ} a) = 0$
95	8 94	syl	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to a + (0 -_{ℝ} a) = 0$
96	95	oveq1d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to a + (0 -_{ℝ} a) + 1 = 0 + 1$
97		readdlid	$⊢ 1 \in ℝ \to 0 + 1 = 1$
98	54 97	ax-mp	$⊢ 0 + 1 = 1$
99	96 98	eqtrdi	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to a + (0 -_{ℝ} a) + 1 = 1$
100	93 99	eqtr3d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to a + (0 -_{ℝ} a) + 1 = 1$
101		readdrid	$⊢ a \in ℝ \to a + 0 = a$
102	8 101	syl	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to a + 0 = a$
103	92 100 102	3eqtr3rd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to a = 1$
104		rernegcl	$⊢ b \in ℝ \to 0 -_{ℝ} b \in ℝ$
105	32 104	syl	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 -_{ℝ} b \in ℝ$
106	11 105	readdcld	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 1 + (0 -_{ℝ} b) \in ℝ$
107		ax-rrecex	$⊢ (1 + (0 -_{ℝ} b) \in ℝ \land 1 + (0 -_{ℝ} b) \neq 0) \to \exists y \in ℝ (1 + (0 -_{ℝ} b)) y = 1$
108	106 107	sylan	$⊢ ((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \to \exists y \in ℝ (1 + (0 -_{ℝ} b)) y = 1$
109	105	recnd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 -_{ℝ} b \in ℂ$
110	15 109	mulcld	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to i (0 -_{ℝ} b) \in ℂ$
111	23 15 110	adddid	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot (i + i (0 -_{ℝ} b)) = 0 \cdot i + 0 \cdot i (0 -_{ℝ} b)$
112		0re	$⊢ 0 \in ℝ$
113		remul02	$⊢ 0 \in ℝ \to 0 \cdot 0 = 0$
114	112 113	ax-mp	$⊢ 0 \cdot 0 = 0$
115	114	oveq1i	$⊢ 0 \cdot 0 i = 0 \cdot i$
116	1 1 2	mulassi	$⊢ 0 \cdot 0 i = 0 \cdot 0 \cdot i$
117	115 116	eqtr3i	$⊢ 0 \cdot i = 0 \cdot 0 \cdot i$
118	117	a1i	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i = 0 \cdot 0 \cdot i$
119	118	oveq1d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i + 0 \cdot i (0 -_{ℝ} b) = 0 \cdot 0 \cdot i + 0 \cdot i (0 -_{ℝ} b)$
120	111 119	eqtrd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot (i + i (0 -_{ℝ} b)) = 0 \cdot 0 \cdot i + 0 \cdot i (0 -_{ℝ} b)$
121	15 17 109	adddid	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to i (1 + (0 -_{ℝ} b)) = i \cdot 1 + i (0 -_{ℝ} b)$
122	19	a1i	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to i \cdot 1 = i$
123	122	oveq1d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to i \cdot 1 + i (0 -_{ℝ} b) = i + i (0 -_{ℝ} b)$
124	121 123	eqtrd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to i (1 + (0 -_{ℝ} b)) = i + i (0 -_{ℝ} b)$
125	124	oveq2d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i (1 + (0 -_{ℝ} b)) = 0 \cdot (i + i (0 -_{ℝ} b))$
126	23 41 110	adddid	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot (0 \cdot i + i (0 -_{ℝ} b)) = 0 \cdot 0 \cdot i + 0 \cdot i (0 -_{ℝ} b)$
127	120 125 126	3eqtr4d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i (1 + (0 -_{ℝ} b)) = 0 \cdot (0 \cdot i + i (0 -_{ℝ} b))$
128	103	oveq1d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to a + i b = 1 + i b$
129	5 128	eqtrd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i = 1 + i b$
130	129	oveq1d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i + i (0 -_{ℝ} b) = 1 + i b + i (0 -_{ℝ} b)$
131	17 34 110	addassd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 1 + i b + i (0 -_{ℝ} b) = 1 + i b + i (0 -_{ℝ} b)$
132		renegid	$⊢ b \in ℝ \to b + (0 -_{ℝ} b) = 0$
133	32 132	syl	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to b + (0 -_{ℝ} b) = 0$
134	133	oveq2d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to i (b + (0 -_{ℝ} b)) = i \cdot 0$
135	15 33 109	adddid	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to i (b + (0 -_{ℝ} b)) = i b + i (0 -_{ℝ} b)$
136		sn-mul01	$⊢ i \in ℂ \to i \cdot 0 = 0$
137	2 136	mp1i	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to i \cdot 0 = 0$
138	134 135 137	3eqtr3d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to i b + i (0 -_{ℝ} b) = 0$
139	138	oveq2d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 1 + i b + i (0 -_{ℝ} b) = 1 + 0$
140		readdrid	$⊢ 1 \in ℝ \to 1 + 0 = 1$
141	54 140	ax-mp	$⊢ 1 + 0 = 1$
142	139 141	eqtrdi	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 1 + i b + i (0 -_{ℝ} b) = 1$
143	131 142	eqtrd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 1 + i b + i (0 -_{ℝ} b) = 1$
144	130 143	eqtrd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i + i (0 -_{ℝ} b) = 1$
145	144	oveq2d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot (0 \cdot i + i (0 -_{ℝ} b)) = 0 \cdot 1$
146	127 145	eqtrd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i (1 + (0 -_{ℝ} b)) = 0 \cdot 1$
147		ax-1rid	$⊢ 0 \in ℝ \to 0 \cdot 1 = 0$
148	112 147	ax-mp	$⊢ 0 \cdot 1 = 0$
149	146 148	eqtrdi	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i (1 + (0 -_{ℝ} b)) = 0$
150	149	ad2antrr	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \land (y \in ℝ \land (1 + (0 -_{ℝ} b)) y = 1)) \to 0 \cdot i (1 + (0 -_{ℝ} b)) = 0$
151	150	oveq1d	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \land (y \in ℝ \land (1 + (0 -_{ℝ} b)) y = 1)) \to 0 \cdot i (1 + (0 -_{ℝ} b)) y = 0 \cdot y$
152		0cnd	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \land (y \in ℝ \land (1 + (0 -_{ℝ} b)) y = 1)) \to 0 \in ℂ$
153	2	a1i	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \land (y \in ℝ \land (1 + (0 -_{ℝ} b)) y = 1)) \to i \in ℂ$
154		1cnd	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \land (y \in ℝ \land (1 + (0 -_{ℝ} b)) y = 1)) \to 1 \in ℂ$
155	109	ad2antrr	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \land (y \in ℝ \land (1 + (0 -_{ℝ} b)) y = 1)) \to 0 -_{ℝ} b \in ℂ$
156	154 155	addcld	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \land (y \in ℝ \land (1 + (0 -_{ℝ} b)) y = 1)) \to 1 + (0 -_{ℝ} b) \in ℂ$
157	153 156	mulcld	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \land (y \in ℝ \land (1 + (0 -_{ℝ} b)) y = 1)) \to i (1 + (0 -_{ℝ} b)) \in ℂ$
158		simprl	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \land (y \in ℝ \land (1 + (0 -_{ℝ} b)) y = 1)) \to y \in ℝ$
159	158	recnd	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \land (y \in ℝ \land (1 + (0 -_{ℝ} b)) y = 1)) \to y \in ℂ$
160	152 157 159	mulassd	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \land (y \in ℝ \land (1 + (0 -_{ℝ} b)) y = 1)) \to 0 \cdot i (1 + (0 -_{ℝ} b)) y = 0 \cdot i (1 + (0 -_{ℝ} b)) y$
161	153 156 159	mulassd	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \land (y \in ℝ \land (1 + (0 -_{ℝ} b)) y = 1)) \to i (1 + (0 -_{ℝ} b)) y = i (1 + (0 -_{ℝ} b)) y$
162		simprr	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \land (y \in ℝ \land (1 + (0 -_{ℝ} b)) y = 1)) \to (1 + (0 -_{ℝ} b)) y = 1$
163	162	oveq2d	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \land (y \in ℝ \land (1 + (0 -_{ℝ} b)) y = 1)) \to i (1 + (0 -_{ℝ} b)) y = i \cdot 1$
164	163 19	eqtrdi	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \land (y \in ℝ \land (1 + (0 -_{ℝ} b)) y = 1)) \to i (1 + (0 -_{ℝ} b)) y = i$
165	161 164	eqtrd	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \land (y \in ℝ \land (1 + (0 -_{ℝ} b)) y = 1)) \to i (1 + (0 -_{ℝ} b)) y = i$
166	165	oveq2d	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \land (y \in ℝ \land (1 + (0 -_{ℝ} b)) y = 1)) \to 0 \cdot i (1 + (0 -_{ℝ} b)) y = 0 \cdot i$
167	160 166	eqtrd	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \land (y \in ℝ \land (1 + (0 -_{ℝ} b)) y = 1)) \to 0 \cdot i (1 + (0 -_{ℝ} b)) y = 0 \cdot i$
168		remul02	$⊢ y \in ℝ \to 0 \cdot y = 0$
169	158 168	syl	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \land (y \in ℝ \land (1 + (0 -_{ℝ} b)) y = 1)) \to 0 \cdot y = 0$
170	151 167 169	3eqtr3d	$⊢ (((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \land (y \in ℝ \land (1 + (0 -_{ℝ} b)) y = 1)) \to 0 \cdot i = 0$
171	108 170	rexlimddv	$⊢ ((((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \land 1 + (0 -_{ℝ} b) \neq 0) \to 0 \cdot i = 0$
172	171	ex	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to (1 + (0 -_{ℝ} b) \neq 0 \to 0 \cdot i = 0)$
173	172	necon1d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to (0 \cdot i \neq 0 \to 1 + (0 -_{ℝ} b) = 0)$
174	7 173	mpd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 1 + (0 -_{ℝ} b) = 0$
175	174	oveq1d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 1 + (0 -_{ℝ} b) + b = 0 + b$
176	17 109 33	addassd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 1 + (0 -_{ℝ} b) + b = 1 + (0 -_{ℝ} b) + b$
177		renegid2	$⊢ b \in ℝ \to (0 -_{ℝ} b) + b = 0$
178	32 177	syl	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to (0 -_{ℝ} b) + b = 0$
179	178	oveq2d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 1 + (0 -_{ℝ} b) + b = 1 + 0$
180	179 141	eqtrdi	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 1 + (0 -_{ℝ} b) + b = 1$
181	176 180	eqtrd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 1 + (0 -_{ℝ} b) + b = 1$
182		readdlid	$⊢ b \in ℝ \to 0 + b = b$
183	32 182	syl	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 + b = b$
184	175 181 183	3eqtr3rd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to b = 1$
185	184	oveq2d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to i b = i \cdot 1$
186	103 185	oveq12d	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to a + i b = 1 + i \cdot 1$
187	5 186	eqtrd	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i = 1 + i \cdot 1$
188	19	oveq2i	$⊢ 1 + i \cdot 1 = 1 + i$
189	188	eqeq2i	$⊢ 0 \cdot i = 1 + i \cdot 1 \leftrightarrow 0 \cdot i = 1 + i$
190		oveq2	$⊢ 0 \cdot i = 1 + i \to i i i 0 \cdot i = i i i (1 + i)$
191	2 2	mulcli	$⊢ i i \in ℂ$
192	191 2	mulcli	$⊢ i i i \in ℂ$
193	192 1 2	mulassi	$⊢ i i i \cdot 0 i = i i i 0 \cdot i$
194		sn-mul01	$⊢ i i i \in ℂ \to i i i \cdot 0 = 0$
195	192 194	ax-mp	$⊢ i i i \cdot 0 = 0$
196	195	oveq1i	$⊢ i i i \cdot 0 i = 0 \cdot i$
197	193 196	eqtr3i	$⊢ i i i 0 \cdot i = 0 \cdot i$
198		ax-1cn	$⊢ 1 \in ℂ$
199	192 198 2	adddii	$⊢ i i i (1 + i) = i i i \cdot 1 + i i i i$
200	191 2 198	mulassi	$⊢ i i i \cdot 1 = i i i \cdot 1$
201	19	oveq2i	$⊢ i i i \cdot 1 = i i i$
202	200 201	eqtri	$⊢ i i i \cdot 1 = i i i$
203	191 2 2	mulassi	$⊢ i i i i = i i i i$
204		rei4	$⊢ i i i i = 1$
205	203 204	eqtri	$⊢ i i i i = 1$
206	202 205	oveq12i	$⊢ i i i \cdot 1 + i i i i = i i i + 1$
207	199 206	eqtri	$⊢ i i i (1 + i) = i i i + 1$
208	190 197 207	3eqtr3g	$⊢ 0 \cdot i = 1 + i \to 0 \cdot i = i i i + 1$
209	54 54	readdcli	$⊢ 1 + 1 \in ℝ$
210		df-2	$⊢ 2 = 1 + 1$
211		sn-0ne2	$⊢ 0 \neq 2$
212	211	necomi	$⊢ 2 \neq 0$
213	210 212	eqnetrri	$⊢ 1 + 1 \neq 0$
214		ax-rrecex	$⊢ (1 + 1 \in ℝ \land 1 + 1 \neq 0) \to \exists z \in ℝ (1 + 1) z = 1$
215	209 213 214	mp2an	$⊢ \exists z \in ℝ (1 + 1) z = 1$
216	192 198	addcli	$⊢ i i i + 1 \in ℂ$
217	198 2 216	addassi	$⊢ 1 + i + i i i + 1 = 1 + i + (i i i + 1)$
218	2 192 198	addassi	$⊢ i + i i i + 1 = i + i i i + 1$
219	218	oveq2i	$⊢ 1 + (i + i i i) + 1 = 1 + i + (i i i + 1)$
220	2 2 2	mulassi	$⊢ i i i = i i i$
221	220	oveq2i	$⊢ i + i i i = i + i i i$
222		ipiiie0	$⊢ i + i i i = 0$
223	221 222	eqtri	$⊢ i + i i i = 0$
224	223	oveq1i	$⊢ i + i i i + 1 = 0 + 1$
225	224 98	eqtri	$⊢ i + i i i + 1 = 1$
226	225	oveq2i	$⊢ 1 + (i + i i i) + 1 = 1 + 1$
227	217 219 226	3eqtr2i	$⊢ 1 + i + i i i + 1 = 1 + 1$
228	227	a1i	$⊢ (0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \to 1 + i + i i i + 1 = 1 + 1$
229	3 198 198	adddii	$⊢ 0 \cdot i (1 + 1) = 0 \cdot i \cdot 1 + 0 \cdot i \cdot 1$
230	1 2 198	mulassi	$⊢ 0 \cdot i \cdot 1 = 0 \cdot i \cdot 1$
231	19	oveq2i	$⊢ 0 \cdot i \cdot 1 = 0 \cdot i$
232	230 231	eqtri	$⊢ 0 \cdot i \cdot 1 = 0 \cdot i$
233		simpl	$⊢ (0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \to 0 \cdot i = 1 + i$
234	232 233	eqtrid	$⊢ (0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \to 0 \cdot i \cdot 1 = 1 + i$
235		simpr	$⊢ (0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \to 0 \cdot i = i i i + 1$
236	232 235	eqtrid	$⊢ (0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \to 0 \cdot i \cdot 1 = i i i + 1$
237	234 236	oveq12d	$⊢ (0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \to 0 \cdot i \cdot 1 + 0 \cdot i \cdot 1 = 1 + i + i i i + 1$
238	229 237	eqtrid	$⊢ (0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \to 0 \cdot i (1 + 1) = 1 + i + i i i + 1$
239		remullid	$⊢ 1 + 1 \in ℝ \to 1 (1 + 1) = 1 + 1$
240	209 239	mp1i	$⊢ (0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \to 1 (1 + 1) = 1 + 1$
241	228 238 240	3eqtr4d	$⊢ (0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \to 0 \cdot i (1 + 1) = 1 (1 + 1)$
242	241	oveq1d	$⊢ (0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \to 0 \cdot i (1 + 1) z = 1 (1 + 1) z$
243	242	adantr	$⊢ ((0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \land (z \in ℝ \land (1 + 1) z = 1)) \to 0 \cdot i (1 + 1) z = 1 (1 + 1) z$
244	3	a1i	$⊢ ((0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \land (z \in ℝ \land (1 + 1) z = 1)) \to 0 \cdot i \in ℂ$
245		1cnd	$⊢ ((0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \land (z \in ℝ \land (1 + 1) z = 1)) \to 1 \in ℂ$
246	245 245	addcld	$⊢ ((0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \land (z \in ℝ \land (1 + 1) z = 1)) \to 1 + 1 \in ℂ$
247		simprl	$⊢ ((0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \land (z \in ℝ \land (1 + 1) z = 1)) \to z \in ℝ$
248	247	recnd	$⊢ ((0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \land (z \in ℝ \land (1 + 1) z = 1)) \to z \in ℂ$
249	244 246 248	mulassd	$⊢ ((0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \land (z \in ℝ \land (1 + 1) z = 1)) \to 0 \cdot i (1 + 1) z = 0 \cdot i (1 + 1) z$
250		simprr	$⊢ ((0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \land (z \in ℝ \land (1 + 1) z = 1)) \to (1 + 1) z = 1$
251	250	oveq2d	$⊢ ((0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \land (z \in ℝ \land (1 + 1) z = 1)) \to 0 \cdot i (1 + 1) z = 0 \cdot i \cdot 1$
252	251 232	eqtrdi	$⊢ ((0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \land (z \in ℝ \land (1 + 1) z = 1)) \to 0 \cdot i (1 + 1) z = 0 \cdot i$
253	249 252	eqtrd	$⊢ ((0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \land (z \in ℝ \land (1 + 1) z = 1)) \to 0 \cdot i (1 + 1) z = 0 \cdot i$
254	245 246 248	mulassd	$⊢ ((0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \land (z \in ℝ \land (1 + 1) z = 1)) \to 1 (1 + 1) z = 1 (1 + 1) z$
255	250	oveq2d	$⊢ ((0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \land (z \in ℝ \land (1 + 1) z = 1)) \to 1 (1 + 1) z = 1 \cdot 1$
256		1t1e1ALT	$⊢ 1 \cdot 1 = 1$
257	255 256	eqtrdi	$⊢ ((0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \land (z \in ℝ \land (1 + 1) z = 1)) \to 1 (1 + 1) z = 1$
258	254 257	eqtrd	$⊢ ((0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \land (z \in ℝ \land (1 + 1) z = 1)) \to 1 (1 + 1) z = 1$
259	243 253 258	3eqtr3d	$⊢ ((0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \land (z \in ℝ \land (1 + 1) z = 1)) \to 0 \cdot i = 1$
260	259	rexlimdvaa	$⊢ (0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \to (\exists z \in ℝ (1 + 1) z = 1 \to 0 \cdot i = 1)$
261	215 260	mpi	$⊢ (0 \cdot i = 1 + i \land 0 \cdot i = i i i + 1) \to 0 \cdot i = 1$
262	208 261	mpdan	$⊢ 0 \cdot i = 1 + i \to 0 \cdot i = 1$
263	189 262	sylbi	$⊢ 0 \cdot i = 1 + i \cdot 1 \to 0 \cdot i = 1$
264		oveq2	$⊢ 0 \cdot i = 1 \to 0 \cdot 0 \cdot i = 0 \cdot 1$
265	116 115	eqtr3i	$⊢ 0 \cdot 0 \cdot i = 0 \cdot i$
266	264 265 148	3eqtr3g	$⊢ 0 \cdot i = 1 \to 0 \cdot i = 0$
267	263 266	syl	$⊢ 0 \cdot i = 1 + i \cdot 1 \to 0 \cdot i = 0$
268	187 267	syl	$⊢ (((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \land \neg 0 \cdot i = 0) \to 0 \cdot i = 0$
269	268	pm2.18da	$⊢ ((a \in ℝ \land b \in ℝ) \land 0 \cdot i = a + i b) \to 0 \cdot i = 0$
270	269	ex	$⊢ (a \in ℝ \land b \in ℝ) \to (0 \cdot i = a + i b \to 0 \cdot i = 0)$
271	270	rexlimivv	$⊢ \exists a \in ℝ \exists b \in ℝ 0 \cdot i = a + i b \to 0 \cdot i = 0$
272	3 4 271	mp2b	$⊢ 0 \cdot i = 0$

Metamath Proof Explorer

Theorem sn-0tie0

Proof