Theorem recexsrlem 5184

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:   x,A

Proof of Theorem recexsrlem

Step	Hyp	Ref	Expression
1		recexsrlem.1	. . . . 5 |- A e. V
2		ltrelsr 5152	. . . . 5 |- <R (_ (R. X. R.)
3	1, 2	brel 3213	. . . 4 |- (0R <R A -> (0R e. R. /\ A e. R.))
4	3	pm3.27d 325	. . 3 |- (0R <R A -> A e. R.)
5		df-nr 5139	. . . 4 |- R. = ((P. X. P.)/. ~R )
6		breq2 2613	. . . . 5 |- ([<.y, z>.] ~R = A -> (0R <R [<.y, z>.] ~R <-> 0R <R A))
7		opreq1 3953	. . . . . . 7 |- ([<.y, z>.] ~R = A -> ([<.y, z>.] ~R .R x) = (A .R x))
8	7	eqeq1d 1475	. . . . . 6 |- ([<.y, z>.] ~R = A -> (([<.y, z>.] ~R .R x) = 1R <-> (A .R x) = 1R))
9	8	exbidv 1274	. . . . 5 |- ([<.y, z>.] ~R = A -> (E.x([<.y, z>.] ~R .R x) = 1R <-> E.x(A .R x) = 1R))
10	6, 9	imbi12d 624	. . . 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 5089	. . . . . . . . . . . . . . . . . . 19 |- 1P e. P.
12		addclpr 5092	. . . . . . . . . . . . . . . . . . 19 |- ((v e. P. /\ 1P e. P.) -> (v +P. 1P) e. P.)
13	11, 12	mpan2 694	. . . . . . . . . . . . . . . . . 18 |- (v e. P. -> (v +P. 1P) e. P.)
14	13, 11	jctir 293	. . . . . . . . . . . . . . . . 17 |- (v e. P. -> ((v +P. 1P) e. P. /\ 1P e. P.))
15	14	anim2i 335	. . . . . . . . . . . . . . . 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 389	. . . . . . . . . . . . . . 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 5157	. . . . . . . . . . . . . . 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 10	. . . . . . . . . . . . . 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 5092	. . . . . . . . . . . . . . . . . . . . 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 5094	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y e. P. /\ (v +P. 1P) e. P.) -> (y .P. (v +P. 1P)) e. P.)
21	20, 13	sylan2 451	. . . . . . . . . . . . . . . . . . . . 21 |- ((y e. P. /\ v e. P.) -> (y .P. (v +P. 1P)) e. P.)
22		mulclpr 5094	. . . . . . . . . . . . . . . . . . . . . 22 |- ((z e. P. /\ 1P e. P.) -> (z .P. 1P) e. P.)
23	11, 22	mpan2 694	. . . . . . . . . . . . . . . . . . . . 21 |- (z e. P. -> (z .P. 1P) e. P.)
24	19, 21, 23	syl2an 454	. . . . . . . . . . . . . . . . . . . 20 |- (((y e. P. /\ v e. P.) /\ z e. P.) -> ((y .P. (v +P. 1P)) +P. (z .P. 1P)) e. P.)
25	24	an1rs 488	. . . . . . . . . . . . . . . . . . 19 |- (((y e. P. /\ z e. P.) /\ v e. P.) -> ((y .P. (v +P. 1P)) +P. (z .P. 1P)) e. P.)
26		addclpr 5092	. . . . . . . . . . . . . . . . . . . . 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 5094	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y e. P. /\ 1P e. P.) -> (y .P. 1P) e. P.)
28	11, 27	mpan2 694	. . . . . . . . . . . . . . . . . . . . 21 |- (y e. P. -> (y .P. 1P) e. P.)
29		mulclpr 5094	. . . . . . . . . . . . . . . . . . . . . 22 |- ((z e. P. /\ (v +P. 1P) e. P.) -> (z .P. (v +P. 1P)) e. P.)
30	29, 13	sylan2 451	. . . . . . . . . . . . . . . . . . . . 21 |- ((z e. P. /\ v e. P.) -> (z .P. (v +P. 1P)) e. P.)
31	26, 28, 30	syl2an 454	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. P. /\ (z e. P. /\ v e. P.)) -> ((y .P. 1P) +P. (z .P. (v +P. 1P))) e. P.)
32	31	anassrs 441	. . . . . . . . . . . . . . . . . . 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 288	. . . . . . . . . . . . . . . . . 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 5092	. . . . . . . . . . . . . . . . . . . 20 |- ((1P e. P. /\ 1P e. P.) -> (1P +P. 1P) e. P.)
35	11, 11, 34	mp2an 695	. . . . . . . . . . . . . . . . . . 19 |- (1P +P. 1P) e. P.
36	35, 11	pm3.2i 285	. . . . . . . . . . . . . . . . . 18 |- ((1P +P. 1P) e. P. /\ 1P e. P.)
37	33, 36	jctir 293	. . . . . . . . . . . . . . . . 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 5149	. . . . . . . . . . . . . . . . 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 10	. . . . . . . . . . . . . . . 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 3953	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((z +P. w) = y -> ((z +P. w) .P. v) = (y .P. v))
41	40	eqcomd 1472	. . . . . . . . . . . . . . . . . . . . . 22 |- ((z +P. w) = y -> (y .P. v) = ((z +P. w) .P. v))
42		opreq2 3954	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((w .P. v) = 1P -> ((z .P. v) +P. (w .P. v)) = ((z .P. v) +P. 1P))
43		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . 24 |- z e. V
44		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . 24 |- w e. V
45		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . 24 |- v e. V
46		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- u e. V
47		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- f e. V
48	46, 47	mulcompr 5097	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (u .P. f) = (f .P. u)
49		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- x e. V
50	47, 49	distrpr 5104	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (u .P. (f +P. x)) = ((u .P. f) +P. (u .P. x))
51	43, 44, 45, 48, 50	caoprdistrr 4053	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((z +P. w) .P. v) = ((z .P. v) +P. (w .P. v))
52	42, 51	syl5eq 1511	. . . . . . . . . . . . . . . . . . . . . 22 |- ((w .P. v) = 1P -> ((z +P. w) .P. v) = ((z .P. v) +P. 1P))
53	41, 52	sylan9eqr 1521	. . . . . . . . . . . . . . . . . . . . 21 |- (((w .P. v) = 1P /\ (z +P. w) = y) -> (y .P. v) = ((z .P. v) +P. 1P))
54	53	opreq1d 3960	. . . . . . . . . . . . . . . . . . . 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 3968	. . . . . . . . . . . . . . . . . . . . 21 |- (z .P. v) e. V
56	11	elisseti 1809	. . . . . . . . . . . . . . . . . . . . 21 |- 1P e. V
57		oprex 3968	. . . . . . . . . . . . . . . . . . . . 21 |- ((y .P. 1P) +P. (z .P. 1P)) e. V
58	46, 47	addcompr 5095	. . . . . . . . . . . . . . . . . . . . 21 |- (u +P. f) = (f +P. u)
59	47, 49	addasspr 5096	. . . . . . . . . . . . . . . . . . . . 21 |- ((u +P. f) +P. x) = (u +P. (f +P. x))
60	55, 56, 57, 58, 59	caopr32 4046	. . . . . . . . . . . . . . . . . . . 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 1515	. . . . . . . . . . . . . . . . . . 19 |- (((w .P. v) = 1P /\ (z +P. w) = y) -> ((y .P. v) +P. ((y .P. 1P) +P. (z