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 e. CC /\ A =/= 0) -> E.x e. CC (A x. x) = 1)

Distinct variable group(s):   x,A

Proof of Theorem axrecex

Step	Hyp	Ref	Expression
1		df-c 4034	. . 3 |- CC = (R. X. R.)
2		neeq1 1194	. . . 4 |- (<.y, z>. = A -> (<.y, z>. =/= 0 <-> A =/= 0))
3		opreq1 3006	. . . . . 6 |- (<.y, z>. = A -> (<.y, z>. x. x) = (A x. x))
4	3	cleq1d 1109	. . . . 5 |- (<.y, z>. = A -> ((<.y, z>. x. x) = 1 <-> (A x. x) = 1))
5	4	birexdv 1220	. . . 4 |- (<.y, z>. = A -> (E.x e. CC (<.y, z>. x. x) = 1 <-> E.x e. CC (A x. x) = 1))
6	2, 5	imbi12d 474	. . 3 |- (<.y, z>. = A -> ((<.y, z>. =/= 0 -> E.x e. CC (<.y, z>. x. x) = 1) <-> (A =/= 0 -> E.x e. CC (A x. x) = 1)))
7		visset 1350	. . . . . . . 8 |- y e. V
8		visset 1350	. . . . . . . 8 |- z e. V
9	7, 8	ssgt0sr 4011	. . . . . . 7 |- ((y e. R. /\ z e. 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)) e. V
11	10	recexsrlem 4006	. . . . . . 7 |- (0R <R ((y .R y) +R (z .R z)) -> E.w(w e. R. /\ (((y .R y) +R (z .R z)) .R w) = 1R))
12	9, 11	syl6 23	. . . . . 6 |- ((y e. R. /\ z e. R.) -> (-. (y = 0R /\ z = 0R) -> E.w(w e. 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 e. R.
17	16	elisseti 1355	. . . . . . . . . 10 |- 0R e. 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 e. R. /\ z e. R.) -> (<.y, z>. =/= 0 -> E.w(w e. R. /\ (((y .R y) +R (z .R z)) .R w) = 1R)))
23		opex 1893	. . . . . . . . 9 |- <.(y .R w), (-1R .R (z .R w))>. e. V
24		eleq1 1149	. . . . . . . . . 10 |- (x = <.(y .R w), (-1R .R (z .R w))>. -> (x e. CC <-> <.(y .R w), (-1R .R (z .R w))>. e. CC))
25		opreq2 3007	. . . . . . . . . . 11 |- (x = <.(y .R w), (-1R .R (z .R w))>. -> (<.y, z>. x. x) = (<.y, z>. x. <.(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. x) = 1 <-> (<.y, z>. x. <.(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 e. CC /\ (<.y, z>. x. x) = 1) <-> (<.(y .R w), (-1R .R (z .R w))>. e. CC /\ (<.y, z>. x. <.(y .R w), (-1R .R (z .R w))>.) = 1)))
28	23, 27	cla4ev 1401	. . . . . . . 8 |- ((<.(y .R w), (-1R .R (z .R w))>. e. CC /\ (<.y, z>. x. <.(y .R w), (-1R .R (z .R w))>.) = 1) -> E.x(x e. CC /\ (<.y, z>. x. x) = 1))
29		mulclsr 3987	. . . . . . . . . . 11 |- ((y e. R. /\ w e. R.) -> (y .R w) e. R.)
30		mulclsr 3987	. . . . . . . . . . . . 13 |- ((z e. R. /\ w e. R.) -> (z .R w) e. R.)
31		m1r 3985	. . . . . . . . . . . . 13 |- -1R e. R.
32	30, 31	jctil 240	. . . . . . . . . . . 12 |- ((z e. R. /\ w e. R.) -> (-1R e. R. /\ (z .R w) e. R.))
33		mulclsr 3987	. . . . . . . . . . . 12 |- ((-1R e. R. /\ (z .R w) e. R.) -> (-1R .R (z .R w)) e. R.)
34	32, 33	syl 12	. . . . . . . . . . 11 |- ((z e. R. /\ w e. R.) -> (-1R .R (z .R w)) e. R.)
35	29, 34	anim12i 268	. . . . . . . . . 10 |- (((y e. R. /\ w e. R.) /\ (z e. R. /\ w e. R.)) -> ((y .R w) e. R. /\ (-1R .R (z .R w)) e. R.))
36		anandir 393	. . . . . . . . . 10 |- (((y e. R. /\ z e. R.) /\ w e. R.) <-> ((y e. R. /\ w e. R.) /\ (z e. R. /\ w e. R.)))
37		oprex 3018	. . . . . . . . . . 11 |- (-1R .R (z .R w)) e. V
38	37	opelcn 4042	. . . . . . . . . 10 |- (<.(y .R w), (-1R .R (z .R w))>. e. CC <-> ((y .R w) e. R. /\ (-1R .R (z .R w)) e. R.))
39	35, 36, 38	3imtr4 192	. . . . . . . . 9 |- (((y e. R. /\ z e. R.) /\ w e. R.) -> <.(y .R w), (-1R .R (z .R w))>. e. CC)
40	39	adantrr 312	. . . . . . . 8 |- (((y e. R. /\ z e. R.) /\ (w e. R. /\ (((y .R y) +R (z .R z)) .R w) = 1R)) -> <.(y .R w), (-1R .R (z .R w))>. e. CC)
41		pm3.26 256	. . . . . . . . . . . . 13 |- (((y e. R. /\ z e. R.) /\ w e. R.) -> (y e. R. /\ z e. R.))
42	35	anandirs 395	. . . . . . . . . . . . 13 |- (((y e. R. /\ z e. R.) /\ w e. R.) -> ((y .R w) e. R. /\ (-1R .R (z .R w)) e. R.))
43	41, 42	jca 236	. . . . . . . . . . . 12 |- (((y e. R. /\ z e. R.) /\ w e. R.) -> ((y e. R. /\ z e. R.) /\ ((y .R w) e. R. /\ (-1R .R (z .R w)) e. R.)))
44	43	adantrr 312	. . . . . . . . . . 11 |- (((y e. R. /\ z e. R.) /\ (w e. R. /\ (((y .R y) +R (z .R z)) .R w) = 1R)) -> ((y e. R. /\ z e. R.) /\ ((y .R w) e. R. /\ (-1R .R (z .R w)) e. R.)))
45		mulcnsr 4048	. . . . . . . . . . 11 |- (((y e. R. /\ z e. R.) /\ ((y .R w) e. R. /\ (-1R .R (z .R w)) e. R.)) -> (<.y, z>. x. <.(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 e. R. /\ z e. R.) /\ (w e. R. /\ (((y .R y) +R (z .R z)) .R w) = 1R)) -> (<.y, z>. x. <.(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 e. 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 e. R. /\ w e. R.) -> (y .R (y .R w)) = ((y .R y) .R w))
53		pm3.26 256	. . . . . . . . . . . . . . . . . . . . 21 |- ((z e. R. /\ w e. R.) -> z e. R.)
54	53, 30	jca 236	. . . . . . . . . . . . . . . . . . . 20 |- ((z e. R. /\ w e. R.) -> (z e. R. /\ (z .R w) e. R.))
55		mulclsr 3987	. . . . . . . . . . . . . . . . . . . 20 |- ((z e. R. /\ (z