Theorem recexsrlem 4006

Description: The reciprocal of a positive signed real exists. Part of Proposition 9-4.3 of [Gleason] p. 126.

Hypothesis

Ref	Expression
recexsrlem.1	|- A e. V

Assertion

Ref	Expression
recexsrlem	|- (0R <R A -> E.x(x e. R. /\ (A .R x) = 1R))

Distinct variable group(s):   x,A

Proof of Theorem recexsrlem

Step	Hyp	Ref	Expression
1		recexsrlem.1	. . . . 5 |- A e. V
2		ltrelsr 3974	. . . . 5 |- <R (_ (R. X. R.)
3	1, 2	brel 2459	. . . 4 |- (0R <R A -> (0R e. R. /\ A e. R.))
4	3	pm3.27d 262	. . 3 |- (0R <R A -> A e. R.)
5		df-nr 3961	. . . 4 |- R. = ((P. X. P.)/. ~R )
6		breq2 2066	. . . . 5 |- ([<.y, z>.] ~R = A -> (0R <R [<.y, z>.] ~R <-> 0R <R A))
7		opreq1 3006	. . . . . . 7 |- ([<.y, z>.] ~R = A -> ([<.y, z>.] ~R .R x) = (A .R x))
8	7	cleq1d 1109	. . . . . 6 |- ([<.y, z>.] ~R = A -> (([<.y, z>.] ~R .R x) = 1R <-> (A .R x) = 1R))
9	8	biexdv 936	. . . . 5 |- ([<.y, z>.] ~R = A -> (E.x([<.y, z>.] ~R .R x) = 1R <-> E.x(A .R x) = 1R))
10	6, 9	imbi12d 474	. . . 4 |- ([<.y, z>.] ~R = A -> ((0R <R [<.y, z>.] ~R -> E.x([<.y, z>.] ~R .R x) = 1R) <-> (0R <R A -> E.x(A .R x) = 1R)))
11		1pr 3911	. . . . . . . . . . . . . . . . . . 19 |- 1P e. P.
12		addclpr 3914	. . . . . . . . . . . . . . . . . . 19 |- ((v e. P. /\ 1P e. P.) -> (v +P. 1P) e. P.)
13	11, 12	mpan2 519	. . . . . . . . . . . . . . . . . 18 |- (v e. P. -> (v +P. 1P) e. P.)
14	13, 11	jctir 241	. . . . . . . . . . . . . . . . 17 |- (v e. P. -> ((v +P. 1P) e. P. /\ 1P e. P.))
15	14	anim2i 270	. . . . . . . . . . . . . . . 16 |- (((y e. P. /\ z e. P.) /\ v e. P.) -> ((y e. P. /\ z e. P.) /\ ((v +P. 1P) e. P. /\ 1P e. P.)))
16	15	adantr 306	. . . . . . . . . . . . . . 15 |- ((((y e. P. /\ z e. P.) /\ v e. P.) /\ ((w .P v) = 1P /\ (z +P. w) = y)) -> ((y e. P. /\ z e. P.) /\ ((v +P. 1P) e. P. /\ 1P e. P.)))
17		mulsrpr 3979	. . . . . . . . . . . . . . 15 |- (((y e. P. /\ z e. P.) /\ ((v +P. 1P) e. P. /\ 1P e. P.)) -> ([<.y, z>.] ~R .R [<.(v +P. 1P), 1P>.] ~R ) = [<.((y .P (v +P. 1P)) +P. (z .P 1P)), ((y .P 1P) +P. (z .P (v +P. 1P)))>.] ~R )
18	16, 17	syl 12	. . . . . . . . . . . . . 14 |- ((((y e. P. /\ z e. P.) /\ v e. P.) /\ ((w .P v) = 1P /\ (z +P. w) = y)) -> ([<.y, z>.] ~R .R [<.(v +P. 1P), 1P>.] ~R ) = [<.((y .P (v +P. 1P)) +P. (z .P 1P)), ((y .P 1P) +P. (z .P (v +P. 1P)))>.] ~R )
19		addclpr 3914	. . . . . . . . . . . . . . . . . . . . 21 |- (((y .P (v +P. 1P)) e. P. /\ (z .P 1P) e. P.) -> ((y .P (v +P. 1P)) +P. (z .P 1P)) e. P.)
20		mulclpr 3916	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y e. P. /\ (v +P. 1P) e. P.) -> (y .P (v +P. 1P)) e. P.)
21	20, 13	sylan2 346	. . . . . . . . . . . . . . . . . . . . 21 |- ((y e. P. /\ v e. P.) -> (y .P (v +P. 1P)) e. P.)
22		mulclpr 3916	. . . . . . . . . . . . . . . . . . . . . 22 |- ((z e. P. /\ 1P e. P.) -> (z .P 1P) e. P.)
23	11, 22	mpan2 519	. . . . . . . . . . . . . . . . . . . . 21 |- (z e. P. -> (z .P 1P) e. P.)
24	19, 21, 23	syl2an 349	. . . . . . . . . . . . . . . . . . . 20 |- (((y e. P. /\ v e. P.) /\ z e. P.) -> ((y .P (v +P. 1P)) +P. (z .P 1P)) e. P.)
25	24	an1rs 373	. . . . . . . . . . . . . . . . . . 19 |- (((y e. P. /\ z e. P.) /\ v e. P.) -> ((y .P (v +P. 1P)) +P. (z .P 1P)) e. P.)
26		addclpr 3914	. . . . . . . . . . . . . . . . . . . . 21 |- (((y .P 1P) e. P. /\ (z .P (v +P. 1P)) e. P.) -> ((y .P 1P) +P. (z .P (v +P. 1P))) e. P.)
27		mulclpr 3916	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y e. P. /\ 1P e. P.) -> (y .P 1P) e. P.)
28	11, 27	mpan2 519	. . . . . . . . . . . . . . . . . . . . 21 |- (y e. P. -> (y .P 1P) e. P.)
29		mulclpr 3916	. . . . . . . . . . . . . . . . . . . . . 22 |- ((z e. P. /\ (v +P. 1P) e. P.) -> (z .P (v +P. 1P)) e. P.)
30	29, 13	sylan2 346	. . . . . . . . . . . . . . . . . . . . 21 |- ((z e. P. /\ v e. P.) -> (z .P (v +P. 1P)) e. P.)
31	26, 28, 30	syl2an 349	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. P. /\ (z e. P. /\ v e. P.)) -> ((y .P 1P) +P. (z .P (v +P. 1P))) e. P.)
32	31	anassrs 338	. . . . . . . . . . . . . . . . . . 19 |- (((y e. P. /\ z e. P.) /\ v e. P.) -> ((y .P 1P) +P. (z .P (v +P. 1P))) e. P.)
33	25, 32	jca 236	. . . . . . . . . . . . . . . . . 18 |- (((y e. P. /\ z e. P.) /\ v e. P.) -> (((y .P (v +P. 1P)) +P. (z .P 1P)) e. P. /\ ((y .P 1P) +P. (z .P (v +P. 1P))) e. P.))
34		addclpr 3914	. . . . . . . . . . . . . . . . . . . 20 |- ((1P e. P. /\ 1P e. P.) -> (1P +P. 1P) e. P.)
35	11, 11, 34	mp2an 520	. . . . . . . . . . . . . . . . . . 19 |- (1P +P. 1P) e. P.
36	35, 11	pm3.2i 234	. . . . . . . . . . . . . . . . . 18 |- ((1P +P. 1P) e. P. /\ 1P e. P.)
37	33, 36	jctir 241	. . . . . . . . . . . . . . . . 17 |- (((y e. P. /\ z e. P.) /\ v e. P.) -> ((((y .P (v +P. 1P)) +P. (z .P 1P)) e. P. /\ ((y .P 1P) +P. (z .P (v +P. 1P))) e. P.) /\ ((1P +P. 1P) e. P. /\ 1P e. P.)))
38		enreceq 3971	. . . . . . . . . . . . . . . . 17 |- (((((y .P (v +P. 1P)) +P. (z .P 1P)) e. P. /\ ((y .P 1P) +P. (z .P (v +P. 1P))) e. P.) /\ ((1P +P. 1P) e. P. /\ 1P e. P.)) -> ([<.((y .P (v +P. 1P)) +P. (z .P 1P)), ((y .P 1P) +P. (z .P (v +P. 1P)))>.] ~R = [<.(1P +P. 1P), 1P>.] ~R <-> (((y .P (v +P. 1P)) +P. (z .P 1P)) +P. 1P) = (((y .P 1P) +P. (z .P (v +P. 1P))) +P. (1P +P. 1P))))
39	37, 38	syl 12	. . . . . . . . . . . . . . . 16 |- (((y e. P. /\ z e. P.) /\ v e. P.) -> ([<.((y .P (v +P. 1P)) +P. (z .P 1P)), ((y .P 1P) +P. (z .P (v +P. 1P)))>.] ~R = [<.(1P +P. 1P), 1P>.] ~R <-> (((y .P (v +P. 1P)) +P. (z .P 1P)) +P. 1P) = (((y .P 1P) +P. (z .P (v +P. 1P))) +P. (1P +P. 1P))))
40		opreq1 3006	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((z +P. w) = y -> ((z +P. w) .P v) = (y .P v))
41	40	cleqcomd 1106	. . . . . . . . . . . . . . . . . . . . . 22 |- ((z +P. w) = y -> (y .P v) = ((z +P. w) .P v))
42		opreq2 3007	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((w .P v) = 1P -> ((z .P v) +P. (w .P v)) = ((z .P v) +P. 1P))
43		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . 24 |- z e. V
44		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . 24 |- w e. V
45		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . 24 |- v e. V
46		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- u e. V
47		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- f e. V
48	46, 47	mulcompr 3919	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (u .P f) = (f .P u)
49		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- x e. V
50	47, 49	distrpr 3926	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (u .P (f +P. x)) = ((u .P f) +P. (u .P x))
51	43, 44, 45, 48, 50	caoprdistrr 3081	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((z +P. w) .P v) = ((z .P v) +P. (w .P v))
52	42, 51	syl5eq 1136	. . . . . . . . . . . . . . . . . . . . . 22 |- ((w .P v) = 1P -> ((z +P. w) .P v) = ((z .P v) +P. 1P))
53	41, 52	sylan9eqr 1145	. . . . . . . . . . . . . . . . . . . . 21 |- (((w .P v) = 1P /\ (z +P. w) = y) -> (y .P v) = ((z .P v) +P. 1P))
54	53	opreq1d 3012	. . . . . . . . . . . . . . . . . . . 20 |- (((w .P v) = 1P /\ (z +P. w) = y) -> ((y .P v) +P. ((y .P 1P) +P. (z .P 1P))) = (((z .P v) +P. 1P) +P. ((y .P 1P) +P. (z .P 1P))))
55		oprex 3018	. . . . . . . . . . . . . . . . . . . . 21 |- (z .P v) e. V
56	11	elisseti 1355	. . . . . . . . . . . . . . . . . . . . 21 |- 1P e. V
57		oprex 3018	. . . . . . . . . . . . . . . . . . . . 21 |- ((y .P 1P) +P. (z .P 1P)) e. V
58	46, 47	addcompr 3917	. . . . . . . . . . . . . . . . . . . . 21 |- (u +P. f) = (f +P. u)
59	47, 49	addasspr 3918	. . . . . . . . . . . . . . . . . . . . 21 |- ((u +P. f) +P. x) = (u +P. (f +P. x))
60	55, 56, 57, 58, 59	caopr32 3074	. . . . . . . . . . . . . . . . . . . 20 |- (((z .P v) +P. 1P) +P. ((y .P 1P) +P. (z .P 1P))) = (((z .P v) +P. ((y .P 1P) +P. (z .P 1P))) +P. 1P)
61	54, 60	syl6eq 1140	. . . . . . . . . . . . . . . . . . 19 |- (((w .P v) = 1P /\ (z +P. w) = y) -> ((y .P v) +P. ((y .P 1P) +P. (z .P 1P))) = (((z .P v) +P. ((y .P 1P) +P. (z .P 1P))) +P. 1P))
62	61	opreq1d 3012	. . . . . . . . . . . . . . . . . 18 |- (((w .P v) = 1P /\ (z +P. w) = y) -> (((y .P v) +P. ((y .P 1P) +P. (z