Theorem axrecex 4079

Description: Existence of reciprocal of nonzero complex number. One of the 28 axioms for real and complex numbers, derived from ZF set theory.

Assertion

Ref	Expression
axrecex	⊢ ((A ∈ ℂ ∧ A ≠ 0) → ∃x ∈ ℂ (A · x) = 1)

Distinct variable group(s):   x,A

Proof of Theorem axrecex

Step	Hyp	Ref	Expression
1		df-c 4034	. . 3 ⊢ ℂ = (R × R)
2		neeq1 1194	. . . 4 ⊢ (⟨y, z⟩ = A → (⟨y, z⟩ ≠ 0 ↔ A ≠ 0))
3		opreq1 3006	. . . . . 6 ⊢ (⟨y, z⟩ = A → (⟨y, z⟩ · x) = (A · x))
4	3	cleq1d 1109	. . . . 5 ⊢ (⟨y, z⟩ = A → ((⟨y, z⟩ · x) = 1 ↔ (A · x) = 1))
5	4	birexdv 1220	. . . 4 ⊢ (⟨y, z⟩ = A → (∃x ∈ ℂ (⟨y, z⟩ · x) = 1 ↔ ∃x ∈ ℂ (A · x) = 1))
6	2, 5	imbi12d 474	. . 3 ⊢ (⟨y, z⟩ = A → ((⟨y, z⟩ ≠ 0 → ∃x ∈ ℂ (⟨y, z⟩ · x) = 1) ↔ (A ≠ 0 → ∃x ∈ ℂ (A · x) = 1)))
7		visset 1350	. . . . . . . 8 ⊢ y ∈ V
8		visset 1350	. . . . . . . 8 ⊢ z ∈ V
9	7, 8	ssgt0sr 4011	. . . . . . 7 ⊢ ((y ∈ R ∧ z ∈ R) → (¬ (y = 0R ∧ z = 0R) → 0R <R ((y ·R y) +R (z ·R z))))
10		oprex 3018	. . . . . . . 8 ⊢ ((y ·R y) +R (z ·R z)) ∈ V
11	10	recexsrlem 4006	. . . . . . 7 ⊢ (0R <R ((y ·R y) +R (z ·R z)) → ∃w(w ∈ R ∧ (((y ·R y) +R (z ·R z)) ·R w) = 1R))
12	9, 11	syl6 23	. . . . . 6 ⊢ ((y ∈ R ∧ z ∈ R) → (¬ (y = 0R ∧ z = 0R) → ∃w(w ∈ R ∧ (((y ·R y) +R (z ·R z)) ·R w) = 1R)))
13		df-ne 1192	. . . . . . 7 ⊢ (⟨y, z⟩ ≠ 0 ↔ ¬ ⟨y, z⟩ = 0)
14		df-0 4035	. . . . . . . . . 10 ⊢ 0 = ⟨0R, 0R⟩
15	14	cleq2i 1111	. . . . . . . . 9 ⊢ (⟨y, z⟩ = 0 ↔ ⟨y, z⟩ = ⟨0R, 0R⟩)
16		0r 3983	. . . . . . . . . . 11 ⊢ 0R ∈ R
17	16	elisseti 1355	. . . . . . . . . 10 ⊢ 0R ∈ V
18	7, 8, 17	opth 1898	. . . . . . . . 9 ⊢ (⟨y, z⟩ = ⟨0R, 0R⟩ ↔ (y = 0R ∧ z = 0R))
19	15, 18	bitr 151	. . . . . . . 8 ⊢ (⟨y, z⟩ = 0 ↔ (y = 0R ∧ z = 0R))
20	19	negbii 162	. . . . . . 7 ⊢ (¬ ⟨y, z⟩ = 0 ↔ ¬ (y = 0R ∧ z = 0R))
21	13, 20	bitr 151	. . . . . 6 ⊢ (⟨y, z⟩ ≠ 0 ↔ ¬ (y = 0R ∧ z = 0R))
22	12, 21	syl5ib 181	. . . . 5 ⊢ ((y ∈ R ∧ z ∈ R) → (⟨y, z⟩ ≠ 0 → ∃w(w ∈ R ∧ (((y ·R y) +R (z ·R z)) ·R w) = 1R)))
23		opex 1893	. . . . . . . . 9 ⊢ ⟨(y ·R w), (-1R ·R (z ·R w))⟩ ∈ V
24		eleq1 1149	. . . . . . . . . 10 ⊢ (x = ⟨(y ·R w), (-1R ·R (z ·R w))⟩ → (x ∈ ℂ ↔ ⟨(y ·R w), (-1R ·R (z ·R w))⟩ ∈ ℂ))
25		opreq2 3007	. . . . . . . . . . 11 ⊢ (x = ⟨(y ·R w), (-1R ·R (z ·R w))⟩ → (⟨y, z⟩ · x) = (⟨y, z⟩ · ⟨(y ·R w), (-1R ·R (z ·R w))⟩))
26	25	cleq1d 1109	. . . . . . . . . 10 ⊢ (x = ⟨(y ·R w), (-1R ·R (z ·R w))⟩ → ((⟨y, z⟩ · x) = 1 ↔ (⟨y, z⟩ · ⟨(y ·R w), (-1R ·R (z ·R w))⟩) = 1))
27	24, 26	anbi12d 476	. . . . . . . . 9 ⊢ (x = ⟨(y ·R w), (-1R ·R (z ·R w))⟩ → ((x ∈ ℂ ∧ (⟨y, z⟩ · x) = 1) ↔ (⟨(y ·R w), (-1R ·R (z ·R w))⟩ ∈ ℂ ∧ (⟨y, z⟩ · ⟨(y ·R w), (-1R ·R (z ·R w))⟩) = 1)))
28	23, 27	cla4ev 1401	. . . . . . . 8 ⊢ ((⟨(y ·R w), (-1R ·R (z ·R w))⟩ ∈ ℂ ∧ (⟨y, z⟩ · ⟨(y ·R w), (-1R ·R (z ·R w))⟩) = 1) → ∃x(x ∈ ℂ ∧ (⟨y, z⟩ · x) = 1))
29		mulclsr 3987	. . . . . . . . . . 11 ⊢ ((y ∈ R ∧ w ∈ R) → (y ·R w) ∈ R)
30		mulclsr 3987	. . . . . . . . . . . . 13 ⊢ ((z ∈ R ∧ w ∈ R) → (z ·R w) ∈ R)
31		m1r 3985	. . . . . . . . . . . . 13 ⊢ -1R ∈ R
32	30, 31	jctil 240	. . . . . . . . . . . 12 ⊢ ((z ∈ R ∧ w ∈ R) → (-1R ∈ R ∧ (z ·R w) ∈ R))
33		mulclsr 3987	. . . . . . . . . . . 12 ⊢ ((-1R ∈ R ∧ (z ·R w) ∈ R) → (-1R ·R (z ·R w)) ∈ R)
34	32, 33	syl 12	. . . . . . . . . . 11 ⊢ ((z ∈ R ∧ w ∈ R) → (-1R ·R (z ·R w)) ∈ R)
35	29, 34	anim12i 268	. . . . . . . . . 10 ⊢ (((y ∈ R ∧ w ∈ R) ∧ (z ∈ R ∧ w ∈ R)) → ((y ·R w) ∈ R ∧ (-1R ·R (z ·R w)) ∈ R))
36		anandir 393	. . . . . . . . . 10 ⊢ (((y ∈ R ∧ z ∈ R) ∧ w ∈ R) ↔ ((y ∈ R ∧ w ∈ R) ∧ (z ∈ R ∧ w ∈ R)))
37		oprex 3018	. . . . . . . . . . 11 ⊢ (-1R ·R (z ·R w)) ∈ V
38	37	opelcn 4042	. . . . . . . . . 10 ⊢ (⟨(y ·R w), (-1R ·R (z ·R w))⟩ ∈ ℂ ↔ ((y ·R w) ∈ R ∧ (-1R ·R (z ·R w)) ∈ R))
39	35, 36, 38	3imtr4 192	. . . . . . . . 9 ⊢ (((y ∈ R ∧ z ∈ R) ∧ w ∈ R) → ⟨(y ·R w), (-1R ·R (z ·R w))⟩ ∈ ℂ)
40	39	adantrr 312	. . . . . . . 8 ⊢ (((y ∈ R ∧ z ∈ R) ∧ (w ∈ R ∧ (((y ·R y) +R (z ·R z)) ·R w) = 1R)) → ⟨(y ·R w), (-1R ·R (z ·R w))⟩ ∈ ℂ)
41		pm3.26 256	. . . . . . . . . . . . 13 ⊢ (((y ∈ R ∧ z ∈ R) ∧ w ∈ R) → (y ∈ R ∧ z ∈ R))
42	35	anandirs 395	. . . . . . . . . . . . 13 ⊢ (((y ∈ R ∧ z ∈ R) ∧ w ∈ R) → ((y ·R w) ∈ R ∧ (-1R ·R (z ·R w)) ∈ R))
43	41, 42	jca 236	. . . . . . . . . . . 12 ⊢ (((y ∈ R ∧ z ∈ R) ∧ w ∈ R) → ((y ∈ R ∧ z ∈ R) ∧ ((y ·R w) ∈ R ∧ (-1R ·R (z ·R w)) ∈ R)))
44	43	adantrr 312	. . . . . . . . . . 11 ⊢ (((y ∈ R ∧ z ∈ R) ∧ (w ∈ R ∧ (((y ·R y) +R (z ·R z)) ·R w) = 1R)) → ((y ∈ R ∧ z ∈ R) ∧ ((y ·R w) ∈ R ∧ (-1R ·R (z ·R w)) ∈ R)))
45		mulcnsr 4048	. . . . . . . . . . 11 ⊢ (((y ∈ R ∧ z ∈ R) ∧ ((y ·R w) ∈ R ∧ (-1R ·R (z ·R w)) ∈ R)) → (⟨y, z⟩ · ⟨(y ·R w), (-1R ·R (z ·R w))⟩) = ⟨((y ·R (y ·R w)) +R (-1R ·R (z ·R (-1R ·R (z ·R w))))), ((z ·R (y ·R w)) +R (y ·R (-1R ·R (z ·R w))))⟩)
46	44, 45	syl 12	. . . . . . . . . 10 ⊢ (((y ∈ R ∧ z ∈ R) ∧ (w ∈ R ∧ (((y ·R y) +R (z ·R z)) ·R w) = 1R)) → (⟨y, z⟩ · ⟨(y ·R w), (-1R ·R (z ·R w))⟩) = ⟨((y ·R (y ·R w)) +R (-1R ·R (z ·R (-1R ·R (z ·R w))))), ((z ·R (y ·R w)) +R (y ·R (-1R ·R (z ·R w))))⟩)
47		opeq12 1878	. . . . . . . . . . 11 ⊢ ((((y ·R (y ·R w)) +R (-1R ·R (z ·R (-1R ·R (z ·R w))))) = 1R ∧ ((z ·R (y ·R w)) +R (y ·R (-1R ·R (z ·R w)))) = 0R) → ⟨((y ·R (y ·R w)) +R (-1R ·R (z ·R (-1R ·R (z ·R w))))), ((z ·R (y ·R w)) +R (y ·R (-1R ·R (z ·R w))))⟩ = ⟨1R, 0R⟩)
48		cleq2 1110	. . . . . . . . . . . . . . . 16 ⊢ ((((y ·R y) +R (z ·R z)) ·R w) = 1R → (((y ·R (y ·R w)) +R (-1R ·R (z ·R (-1R ·R (z ·R w))))) = (((y ·R y) +R (z ·R z)) ·R w) ↔ ((y ·R (y ·R w)) +R (-1R ·R (z ·R (-1R ·R (z ·R w))))) = 1R))
49		visset 1350	. . . . . . . . . . . . . . . . . . . . 21 ⊢ w ∈ V
50	7, 49	mulasssr 3993	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ·R y) ·R w) = (y ·R (y ·R w))
51	50	cleqcomi 1105	. . . . . . . . . . . . . . . . . . 19 ⊢ (y ·R (y ·R w)) = ((y ·R y) ·R w)
52	51	a1i 7	. . . . . . . . . . . . . . . . . 18 ⊢ ((z ∈ R ∧ w ∈ R) → (y ·R (y ·R w)) = ((y ·R y) ·R w))
53		pm3.26 256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((z ∈ R ∧ w ∈ R) → z ∈ R)
54	53, 30	jca 236	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((z ∈ R ∧ w ∈ R) → (z ∈ R ∧ (z ·R w) ∈ R))
55		mulclsr 3987	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((z ∈ R ∧ (z ·R w) ∈ R) → (z ·R (z ·R w)) ∈ R)
56		1idsr 4001	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((z ·R (z ·R w)) ∈ R → ((z ·R (z ·R w)) ·R 1R) = (z ·R (z ·R w)))
57	54, 55, 56	3syl 21	. . . . . . . . . . . . . . . . . . 19 ⊢ ((z ∈ R ∧ w ∈ R) → ((z ·R (z ·R w)) ·R 1R) = (z ·R (z ·R w)))
58		m1m1sr 3996	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (-1R ·R -1R) = 1R
59	58	opreq1i 3009	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((-1R ·R -1R) ·R (z ·R (z ·R w))) = (1R ·R (z ·R (z ·R w)))
60	31	elisseti 1355	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ -1R ∈ V
61		oprex 3018	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (z ·R w) ∈ V
62		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ v ∈ V
63		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ u ∈ V
64	62, 63	mulcomsr 3992	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (v ·R u) = (u ·R v)
65		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ x ∈ V
66	63, 65	mulasssr 3993	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((v ·R u) ·R x) = (v ·R (u ·R x))
67	8, 60, 61, 64, 66	caopr12 3075	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (z ·R (-1R ·R (z ·R w))) = (-1R ·R (z ·R (z ·R w)))
68	67	opreq2i 3010	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (-1R ·R (z ·R (-1R ·R (z ·R w)))) = (-1R ·R (-1R ·R (z ·R (z ·R w))))
69		oprex 3018	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (z ·R (z ·R w)) ∈ V
70	60, 69	mulasssr 3993	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((-1R ·R -1R) ·R (z ·R (z ·R w))) = (-1R ·R (-1R ·R (z ·R (z ·R w))))
71	68, 70	eqtr4 1122	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-1R ·R (z ·R (-1R ·R (z ·R w)))) = ((-1R ·R -1R) ·R (z ·R (z ·R w)))
72		1r 3984	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1R ∈ R
73	72	elisseti 1355	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1R ∈ V
74	69, 73	mulcomsr 3992	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((z ·R (z ·R w)) ·R 1R) = (1R ·R (z ·R (z ·R w)))
75	59, 71, 74	3eqtr4 1126	. . . . . . . . . . . . . . . . . . 19 ⊢ (-1R ·R (z ·R (-1R ·R (z ·R w)))) = ((z ·R (z ·R w)) ·R 1R)
76	8, 49	mulasssr 3993	. . . . . . . . . . . . . . . . . . 19 ⊢ ((z ·R z) ·R w) = (z ·R (z ·R w))
77	57, 75, 76	3eqtr4g 1147	. . . . . . . . . . . . . . . . . 18 ⊢ ((z ∈ R ∧ w ∈ R) → (-1R ·R (z ·R (-1R ·R (z ·R w)))) = ((z ·R z) ·R w))
78	52, 77	opreq12d 3014	. . . . . . . . . . . . . . . . 17 ⊢ ((z ∈ R ∧ w ∈ R) → ((y ·R (y ·R w)) +R (-1R ·R (z ·R (-1R ·R (z ·R w))))) = (((y ·R y) ·R w) +R ((z ·R z) ·R w)))
79		oprex 3018	. . . . . . . . . . . . . . . . . 18 ⊢ (y ·R y) ∈ V
80		oprex 3018	. . . . . . . . . . . . . . . . . 18 ⊢ (z ·R z) ∈ V
81	63, 65	distrsr 3994	. . . . . . . . . . . . . . . . . 18 ⊢ (v ·R (u +R x)) = ((v ·R u) +R (v ·R x))
82	79, 80, 49, 64, 81	caoprdistrr 3081	. . . . . . . . . . . . . . . . 17 ⊢ (((y ·R y) +R (z ·R z)) ·R w) = (((y ·R y) ·R w) +R ((z ·R z) ·R w))
83	78, 82	syl6eqr 1142	. . . . . . . . . . . . . . . 16 ⊢ ((z ∈ R ∧ w ∈ R) → ((y ·R (y ·R w)) +R (-1R ·R (z ·R (-1R ·R (z ·R w))))) = (((y ·R y) +R (z ·R z)) ·R w))
84	48, 83	syl5bi 183	. . . . . . . . . . . . . . 15 ⊢ ((((y ·R y) +R (z ·R z)) ·R w) = 1R → ((z ∈ R ∧ w ∈ R) → ((y ·R (y ·R w)) +R (-1R ·R (z ·R (-1R ·R (z ·R w))))) = 1R))
85	84	exp3a 292	. . . . . . . . . . . . . 14 ⊢ ((((y ·R y) +R (z ·R z)) ·R w) = 1R → (z ∈ R → (w ∈ R → ((y ·R (y ·R w)) +R (-1R ·R (z ·R (-1R ·R (z ·R w))))) = 1R)))
86	85	com3l 34	. . . . . . . . . . . . 13 ⊢ (z ∈ R → (w ∈ R → ((((y ·R y) +R (z ·R z)) ·R w) = 1R → ((y ·R (y ·R w)) +R (-1R ·R (z ·R (-1R ·R (z ·R w))))) = 1R)))
87	86	imp32 281	. . . . . . . . . . . 12 ⊢ ((z ∈ R ∧ (w ∈ R ∧ (((y ·R y) +R (z ·R z)) ·R w) = 1R)) → ((y ·R (y ·R w)) +R (-1R ·R (z ·R (-1R ·R (z ·R w))))) = 1R)
88	87	adantll 309	. . . . . . . . . . 11 ⊢ (((y ∈ R ∧ z ∈ R) ∧ (w ∈ R ∧ (((y ·R y) +R (z ·R z)) ·R w) = 1R)) → ((y ·R (y ·R w)) +R (-1R ·R (z ·R (-1R ·R (z ·R w))))) = 1R)
89		mulclsr 3987	. . . . . . . . . . . . . . 15 ⊢ ((y ∈ R ∧ (z ·R w) ∈ R) → (y ·R (z ·R w)) ∈ R)
90	89, 30	sylan2 346	. . . . . . . . . . . . . 14 ⊢ ((y ∈ R ∧ (z ∈ R ∧ w ∈ R)) → (y ·R (z ·R w)) ∈ R)
91	90	anassrs 338	. . . . . . . . . . . . 13 ⊢ (((y ∈ R ∧ z ∈ R) ∧ w ∈ R) → (y ·R (z ·R w)) ∈ R)
92	91	adantrr 312	. . . . . . . . . . . 12 ⊢ (((y ∈ R ∧ z ∈ R) ∧ (w ∈ R ∧ (((y ·R y) +R (z ·R z)) ·R w) = 1R)) → (y ·R (z ·R w)) ∈ R)
93		pn0sr 4004	. . . . . . . . . . . . 13 ⊢ ((y ·R (z ·R w)) ∈ R → ((y ·R (z ·R w)) +R ((y ·R (z ·R w)) ·R -1R)) = 0R)
94	8, 7, 49, 64, 66	caopr12 3075	. . . . . . . . . . . . . 14 ⊢ (z ·R (y ·R w)) = (y ·R (z ·R w))
95	7, 60, 61, 64, 66	caopr12 3075	. . . . . . . . . . . . . . 15 ⊢ (y ·R (-1R ·R (z ·R w))) = (-1R ·R (y ·R (z ·R w)))
96		oprex 3018	. . . . . . . . . . . . . . . 16 ⊢ (y ·R (z ·R w)) ∈ V
97	60, 96	mulcomsr 3992	. . . . . . . . . . . . . . 15 ⊢ (-1R ·R (y ·R (z ·R w))) = ((y ·R (z ·R w)) ·R -1R)
98	95, 97	eqtr 1119	. . . . . . . . . . . . . 14 ⊢ (y ·R (-1R ·R (z ·R w))) = ((y ·R (z ·R w)) ·R -1R)
99	94, 98	opreq12i 3011	. . . . . . . . . . . . 13 ⊢ ((z ·R (y ·R w)) +R (y ·R (-1R ·R (z ·R w)))) = ((y ·R (z ·R w)) +R ((y ·R (z ·R w)) ·R -1R))
100	93, 99	syl5eq 1136	. . . . . . . . . . . 12 ⊢ ((y ·R (z ·R w)) ∈ R → ((z ·R (y ·R w)) +R (y ·R (-1R ·R (z ·R w)))) = 0R)
101	92, 100	syl 12	. . . . . . . . . . 11 ⊢ (((y ∈ R ∧ z ∈ R) ∧ (w ∈ R ∧ (((y ·R y) +R (z ·R z)) ·R w) = 1R)) → ((z ·R (y ·R w)) +R (y ·R (-1R ·R (z ·R w)))) = 0R)
102	47, 88, 101	sylanc 361	. . . . . . . . . 10 ⊢ (((y ∈ R ∧ z ∈ R) ∧ (w ∈ R ∧ (((y ·R y) +R (z ·R z)) ·R w) = 1R)) → ⟨((y ·R (y ·R w)) +R (-1R ·R (z ·R (-1R ·R (z ·R w))))), ((z ·R (y ·R w)) +R (y ·R (-1R ·R (z ·R w))))⟩ = ⟨1R, 0R⟩)
103	46, 102	eqtrd 1128	. . . . . . . . 9 ⊢ (((y ∈ R ∧ z ∈ R) ∧ (w ∈ R ∧ (((y ·R y) +R (z ·R z)) ·R w) = 1R)) → (⟨y, z⟩ · ⟨(y ·R w), (-1R ·R (z ·R w))⟩) = ⟨1R, 0R⟩)
104		df-1 4036	. . . . . . . . 9 ⊢ 1 = ⟨1R, 0R⟩
105	103, 104	syl6eqr 1142	. . . . . . . 8 ⊢ (((y ∈ R ∧ z ∈ R) ∧ (w ∈ R ∧ (((y ·R y) +R (z ·R z)) ·R w) = 1R)) → (⟨y, z⟩ · ⟨(y ·R w), (-1R ·R (z ·R w))⟩) = 1)
106	28, 40, 105	sylanc 361	. . . . . . 7 ⊢ (((y ∈ R ∧ z ∈ R) ∧ (w ∈ R ∧ (((y ·R y) +R (z ·R z)) ·R w) = 1R)) → ∃x(x ∈ ℂ ∧ (⟨y, z⟩ · x) = 1))
107	106	exp 291	. . . . . 6 ⊢ ((y ∈ R ∧ z ∈ R) → ((w ∈ R ∧ (((y ·R y) +R (z ·R z)) ·R w) = 1R) → ∃x(x ∈ ℂ ∧ (⟨y, z⟩ · x) = 1)))
108	107	19.23adv 954	. . . . 5 ⊢ ((y ∈ R ∧ z ∈ R) → (∃w(w ∈ R ∧ (((y ·R y) +R (z ·R z)) ·R w) = 1R) → ∃x(x ∈ ℂ ∧ (⟨y, z⟩ · x) = 1)))
109	22, 108	syld 27	. . . 4 ⊢ ((y ∈ R ∧ z ∈ R) → (⟨y, z⟩ ≠ 0 → ∃x(x ∈ ℂ ∧ (⟨y, z⟩ · x) = 1)))
110		df-rex 1206	. . . 4 ⊢ (∃x ∈ ℂ (⟨y, z⟩ · x) = 1 ↔ ∃x(x ∈ ℂ ∧ (⟨y, z⟩ · x) = 1))
111	109, 110	syl6ibr 186	. . 3 ⊢ ((y ∈ R ∧ z ∈ R) → (⟨y, z⟩ ≠ 0 → ∃x ∈ ℂ (⟨y, z⟩ · x) = 1))
112	1, 6, 111	optocl 2469	. 2 ⊢ (A ∈ ℂ → (A ≠ 0 → ∃x ∈ ℂ (A · x) = 1))
113	112	imp 277	1 ⊢ ((A ∈ ℂ ∧ A ≠ 0) → ∃x ∈ ℂ (A · x) = 1)

Syntax hints:  ¬ wn 1   → wi 2   ∧ wa 196  ∃wex 678   = wceq 1091   ∈ wcel 1092   ≠ wne 1190  ∃wrex 1202  ⟨cop 1810   class class class wbr 2054  (class class class)co 3001  Rcnr 3787  0_Rc0r 3788  1_Rc1r 3789  -1_Rcm1r 3790   +_R cplr 3791   ·_R cmr 3792   <_R cltr 3793  ℂcc 4026  0cc0 4028  1c1 4029   · cmulc 4032

This theorem is referenced by:  recex 4117

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077  ax-reg 1078  ax-inf 1079

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-ral 1205  df-rex 1206  df-reu 1207  df-rab 1208  df-v 1349  df-sbc 1441  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-pss 1494  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-int 1966  df-iun 1996  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fv 2438  df-rdg 2970  df-opr 3003  df-oprab 3004  df-1o 3104  df-oadd 3106  df-omul 3107  df-er 3200  df-ec 3202  df-qs 3205  df-ni 3794  df-pli 3795  df-mi 3796  df-lti 3797  df-plpq 3829  df-mpq 3830  df-enq 3831  df-nq 3832  df-plq 3833  df-mq 3834  df-rq 3835  df-ltq 3836  df-1q 3837  df-np 3880  df-1p 3881  df-plp 3882  df-mp 3883  df-ltp 3884  df-plpr 3958  df-mpr 3959  df-enr 3960  df-nr 3961  df-plr 3962  df-mr 3963  df-ltr 3964  df-0r 3965  df-1r 3966  df-m1r 3967  df-c 4034  df-0 4035  df-1 4036  df-mul 4040

metamath.org