Theorem recexgt0sr 6701

Description: The reciprocal of a positive signed real exists and is positive. (Contributed by Jim Kingdon, 6-Feb-2020.)

Assertion

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

Distinct variable group:   x,A

Proof of Theorem recexgt0sr

Dummy variables y z w v f g h are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ltrelsr 6666	. . . 4 |- <R C_ ( R. X. R.)
2	1	brel 4335	. . 3 |- ( 0R <R A -> ( 0R e. R. /\ A e. R.))
3	2	simprd 107	. 2 |- ( 0R <R A -> A e. R.)
4		df-nr 6655	. . 3 |- R. = (( P. X. P.) /. ~R )
5		breq2 3759	. . . 4 |- ([ <.y , z >.] ~R = A -> ( 0R <R [ <.y , z >.] ~R <-> 0R <R A))
6		oveq1 5462	. . . . . . 7 |- ([ <.y , z >.] ~R = A -> ([ <.y , z >.] ~R .R x) = (A .R x))
7	6	eqeq1d 2045	. . . . . 6 |- ([ <.y , z >.] ~R = A -> (([ <.y , z >.] ~R .R x) = 1R <-> (A .R x) = 1R))
8	7	anbi2d 437	. . . . 5 |- ([ <.y , z >.] ~R = A -> (( 0R <R x /\ ([ <.y , z >.] ~R .R x) = 1R) <-> ( 0R <R x /\ (A .R x) = 1R)))
9	8	rexbidv 2321	. . . 4 |- ([ <.y , z >.] ~R = A -> (E.x e. R. ( 0R <R x /\ ([ <.y , z >.] ~R .R x) = 1R) <-> E.x e. R. ( 0R <R x /\ (A .R x) = 1R)))
10	5, 9	imbi12d 223	. . 3 |- ([ <.y , z >.] ~R = A -> (( 0R <R [ <.y , z >.] ~R -> E.x e. R. ( 0R <R x /\ ([ <.y , z >.] ~R .R x) = 1R)) <-> ( 0R <R A -> E.x e. R. ( 0R <R x /\ (A .R x) = 1R))))
11		gt0srpr 6676	. . . . 5 |- ( 0R <R [ <.y , z >.] ~R <-> z <P y)
12		ltexpri 6587	. . . . 5 |- (z <P y -> E.w e. P. (z +P. w) = y)
13	11, 12	sylbi 114	. . . 4 |- ( 0R <R [ <.y , z >.] ~R -> E.w e. P. (z +P. w) = y)
14		recexpr 6610	. . . . . . 7 |- (w e. P. -> E.v e. P. (w .P. v) = 1P)
15	14	adantl 262	. . . . . 6 |- (((y e. P. /\ z e. P.) /\ w e. P.) -> E.v e. P. (w .P. v) = 1P)
16		1pr 6535	. . . . . . . . . . . . . 14 |- 1P e. P.
17		addclpr 6520	. . . . . . . . . . . . . 14 |- ((v e. P. /\ 1P e. P.) -> (v +P. 1P) e. P.)
18	16, 17	mpan2 401	. . . . . . . . . . . . 13 |- (v e. P. -> (v +P. 1P) e. P.)
19		enrex 6665	. . . . . . . . . . . . . 14 |- ~R e. _V
20	19, 4	ecopqsi 6097	. . . . . . . . . . . . 13 |- (((v +P. 1P) e. P. /\ 1P e. P.) -> [ <.(v +P. 1P) , 1P >.] ~R e. R.)
21	18, 16, 20	sylancl 392	. . . . . . . . . . . 12 |- (v e. P. -> [ <.(v +P. 1P) , 1P >.] ~R e. R.)
22	21	adantl 262	. . . . . . . . . . 11 |- ((w e. P. /\ v e. P.) -> [ <.(v +P. 1P) , 1P >.] ~R e. R.)
23	22	ad2antlr 458	. . . . . . . . . 10 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((w .P. v) = 1P /\ (z +P. w) = y)) -> [ <.(v +P. 1P) , 1P >.] ~R e. R.)
24		simprr 484	. . . . . . . . . . . 12 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> v e. P.)
25	24	adantr 261	. . . . . . . . . . 11 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((w .P. v) = 1P /\ (z +P. w) = y)) -> v e. P.)
26		ltaddpr 6571	. . . . . . . . . . . . . 14 |- (( 1P e. P. /\ v e. P.) -> 1P <P ( 1P +P. v))
27	16, 26	mpan 400	. . . . . . . . . . . . 13 |- (v e. P. -> 1P <P ( 1P +P. v))
28		addcomprg 6554	. . . . . . . . . . . . . 14 |- (( 1P e. P. /\ v e. P.) -> ( 1P +P. v) = (v +P. 1P))
29	16, 28	mpan 400	. . . . . . . . . . . . 13 |- (v e. P. -> ( 1P +P. v) = (v +P. 1P))
30	27, 29	breqtrd 3779	. . . . . . . . . . . 12 |- (v e. P. -> 1P <P (v +P. 1P))
31		gt0srpr 6676	. . . . . . . . . . . 12 |- ( 0R <R [ <.(v +P. 1P) , 1P >.] ~R <-> 1P <P (v +P. 1P))
32	30, 31	sylibr 137	. . . . . . . . . . 11 |- (v e. P. -> 0R <R [ <.(v +P. 1P) , 1P >.] ~R )
33	25, 32	syl 14	. . . . . . . . . 10 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((w .P. v) = 1P /\ (z +P. w) = y)) -> 0R <R [ <.(v +P. 1P) , 1P >.] ~R )
34	18, 16	jctir 296	. . . . . . . . . . . . . . . 16 |- (v e. P. -> ((v +P. 1P) e. P. /\ 1P e. P.))
35	34	anim2i 324	. . . . . . . . . . . . . . 15 |- (((y e. P. /\ z e. P.) /\ v e. P.) -> ((y e. P. /\ z e. P.) /\ ((v +P. 1P) e. P. /\ 1P e. P.)))
36	35	adantr 261	. . . . . . . . . . . . . 14 |- ((((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.)))
37		mulsrpr 6674	. . . . . . . . . . . . . 14 |- (((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 )
38	36, 37	syl 14	. . . . . . . . . . . . 13 |- ((((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 )
39	38	adantlrl 451	. . . . . . . . . . . 12 |- ((((y e. P. /\ z e. P.) /\ (w 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 )
40		oveq1 5462	. . . . . . . . . . . . . . . . . . . . 21 |- ((z +P. w) = y -> ((z +P. w) .P. v) = (y .P. v))
41	40	eqcomd 2042	. . . . . . . . . . . . . . . . . . . 20 |- ((z +P. w) = y -> (y .P. v) = ((z +P. w) .P. v))
42	41	ad2antll 460	. . . . . . . . . . . . . . . . . . 19 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((w .P. v) = 1P /\ (z +P. w) = y)) -> (y .P. v) = ((z +P. w) .P. v))
43		mulcomprg 6556	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((f e. P. /\ h e. P.) -> (f .P. h) = ( h .P. f))
44	43	3adant2 922	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((f e. P. /\ g e. P. /\ h e. P.) -> (f .P. h) = ( h .P. f))
45		mulcomprg 6556	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((g e. P. /\ h e. P.) -> (g .P. h) = ( h .P. g))
46	45	3adant1 921	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((f e. P. /\ g e. P. /\ h e. P.) -> (g .P. h) = ( h .P. g))
47	44, 46	oveq12d 5473	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((f e. P. /\ g e. P. /\ h e. P.) -> ((f .P. h) +P. (g .P. h)) = (( h .P. f) +P. ( h .P. g)))
48		distrprg 6564	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (( h e. P. /\ f e. P. /\ g e. P.) -> ( h .P. (f +P. g)) = (( h .P. f) +P. ( h .P. g)))
49	48	3coml 1110	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((f e. P. /\ g e. P. /\ h e. P.) -> ( h .P. (f +P. g)) = (( h .P. f) +P. ( h .P. g)))
50		simp3 905	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((f e. P. /\ g e. P. /\ h e. P.) -> h e. P.)
51		addclpr 6520	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((f e. P. /\ g e. P.) -> (f +P. g) e. P.)
52	51	3adant3 923	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((f e. P. /\ g e. P. /\ h e. P.) -> (f +P. g) e. P.)
53		mulcomprg 6556	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (( h e. P. /\ (f +P. g) e. P.) -> ( h .P. (f +P. g)) = ((f +P. g) .P. h))
54	50, 52, 53	syl2anc 391	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((f e. P. /\ g e. P. /\ h e. P.) -> ( h .P. (f +P. g)) = ((f +P. g) .P. h))
55	47, 49, 54	3eqtr2rd 2076	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f e. P. /\ g e. P. /\ h e. P.) -> ((f +P. g) .P. h) = ((f .P. h) +P. (g .P. h)))
56	55	adantl 262	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ (f e. P. /\ g e. P. /\ h e. P.)) -> ((f +P. g) .P. h) = ((f .P. h) +P. (g .P. h)))
57		simplr 482	. . . . . . . . . . . . . . . . . . . . . 22 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> z e. P.)
58		simprl 483	. . . . . . . . . . . . . . . . . . . . . 22 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> w e. P.)
59	56, 57, 58, 24	caovdird 5621	. . . . . . . . . . . . . . . . . . . . 21 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> ((z +P. w) .P. v) = ((z .P. v) +P. (w .P. v)))
60		oveq2 5463	. . . . . . . . . . . . . . . . . . . . 21 |- ((w .P. v) = 1P -> ((z .P. v) +P. (w .P. v)) = ((z .P. v) +P. 1P))
61	59, 60	sylan9eq 2089	. . . . . . . . . . . . . . . . . . . 20 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ (w .P. v) = 1P) -> ((z +P. w) .P. v) = ((z .P. v) +P. 1P))
62	61	adantrr 448	. . . . . . . . . . . . . . . . . . 19 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((w .P. v) = 1P /\ (z +P. w) = y)) -> ((z +P. w) .P. v) = ((z .P. v) +P. 1P))
63	42, 62	eqtrd 2069	. . . . . . . . . . . . . . . . . 18 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((w .P. v) = 1P /\ (z +P. w) = y)) -> (y .P. v) = ((z .P. v) +P. 1P))
64	63	oveq1d 5470	. . . . . . . . . . . . . . . . 17 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((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))))
65		mulclpr 6553	. . . . . . . . . . . . . . . . . . . 20 |- ((z e. P. /\ v e. P.) -> (z .P. v) e. P.)
66	57, 24, 65	syl2anc 391	. . . . . . . . . . . . . . . . . . 19 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> (z .P. v) e. P.)
67	16	a1i 9	. . . . . . . . . . . . . . . . . . 19 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> 1P e. P.)
68		simpll 481	. . . . . . . . . . . . . . . . . . . . 21 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> y e. P.)
69		mulclpr 6553	. . . . . . . . . . . . . . . . . . . . 21 |- ((y e. P. /\ 1P e. P.) -> (y .P. 1P) e. P.)
70	68, 16, 69	sylancl 392	. . . . . . . . . . . . . . . . . . . 20 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> (y .P. 1P) e. P.)
71		mulclpr 6553	. . . . . . . . . . . . . . . . . . . . 21 |- ((z e. P. /\ 1P e. P.) -> (z .P. 1P) e. P.)
72	57, 16, 71	sylancl 392	. . . . . . . . . . . . . . . . . . . 20 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> (z .P. 1P) e. P.)
73		addclpr 6520	. . . . . . . . . . . . . . . . . . . 20 |- (((y .P. 1P) e. P. /\ (z .P. 1P) e. P.) -> ((y .P. 1P) +P. (z .P. 1P)) e. P.)
74	70, 72, 73	syl2anc 391	. . . . . . . . . . . . . . . . . . 19 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> ((y .P. 1P) +P. (z .P. 1P)) e. P.)
75		addcomprg 6554	. . . . . . . . . . . . . . . . . . . 20 |- ((f e. P. /\ g e. P.) -> (f +P. g) = (g +P. f))
76	75	adantl 262	. . . . . . . . . . . . . . . . . . 19 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ (f e. P. /\ g e. P.)) -> (f +P. g) = (g +P. f))
77		addassprg 6555	. . . . . . . . . . . . . . . . . . . 20 |- ((f e. P. /\ g e. P. /\ h e. P.) -> ((f +P. g) +P. h) = (f +P. (g +P. h)))
78	77	adantl 262	. . . . . . . . . . . . . . . . . . 19 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ (f e. P. /\ g e. P. /\ h e. P.)) -> ((f +P. g) +P. h) = (f +P. (g +P. h)))
79	66, 67, 74, 76, 78	caov32d 5623	. . . . . . . . . . . . . . . . . 18 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> (((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))
80	79	adantr 261	. . . . . . . . . . . . . . . . 17 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((w .P. v) = 1P /\ (z +P. w) = y)) -> (((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))
81	64, 80	eqtrd 2069	. . . . . . . . . . . . . . . 16 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((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))
82	81	oveq1d 5470	. . . . . . . . . . . . . . 15 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((w .P. v) = 1P /\ (z +P. w) = y)) -> (((y .P. v) +P. ((y .P. 1P) +P. (z .P. 1P))) +P. 1P) = ((((z .P. v) +P. ((y .P. 1P) +P. (z .P. 1P))) +P. 1P) +P. 1P))
83		addclpr 6520	. . . . . . . . . . . . . . . . . 18 |- (((z .P. v) e. P. /\ ((y .P. 1P) +P. (z .P. 1P)) e. P.) -> ((z .P. v) +P. ((y .P. 1P) +P. (z .P. 1P))) e. P.)
84	66, 74, 83	syl2anc 391	. . . . . . . . . . . . . . . . 17 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> ((z .P. v) +P. ((y .P. 1P) +P. (z .P. 1P))) e. P.)
85	84	adantr 261	. . . . . . . . . . . . . . . 16 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((w .P. v) = 1P /\ (z +P. w) = y)) -> ((z .P. v) +P. ((y .P. 1P) +P. (z .P. 1P))) e. P.)
86	16	a1i 9	. . . . . . . . . . . . . . . 16 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((w .P. v) = 1P /\ (z +P. w) = y)) -> 1P e. P.)
87		addassprg 6555	. . . . . . . . . . . . . . . 16 |- ((((z .P. v) +P. ((y .P. 1P) +P. (z .P. 1P))) e. P. /\ 1P e. P. /\ 1P e. P.) -> ((((z .P. v) +P. ((y .P. 1P) +P. (z .P. 1P))) +P. 1P) +P. 1P) = (((z .P. v) +P. ((y .P. 1P) +P. (z .P. 1P))) +P. ( 1P +P. 1P)))
88	85, 86, 86, 87	syl3anc 1134	. . . . . . . . . . . . . . 15 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((w .P. v) = 1P /\ (z +P. w) = y)) -> ((((z .P. v) +P. ((y .P. 1P) +P. (z .P. 1P))) +P. 1P) +P. 1P) = (((z .P. v) +P. ((y .P. 1P) +P. (z .P. 1P))) +P. ( 1P +P. 1P)))
89	82, 88	eqtrd 2069	. . . . . . . . . . . . . 14 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((w .P. v) = 1P /\ (z +P. w) = y)) -> (((y .P. v) +P. ((y .P. 1P) +P. (z .P. 1P))) +P. 1P) = (((z .P. v) +P. ((y .P. 1P) +P. (z .P. 1P))) +P. ( 1P +P. 1P)))
90		distrprg 6564	. . . . . . . . . . . . . . . . . . 19 |- ((y e. P. /\ v e. P. /\ 1P e. P.) -> (y .P. (v +P. 1P)) = ((y .P. v) +P. (y .P. 1P)))
91	68, 24, 67, 90	syl3anc 1134	. . . . . . . . . . . . . . . . . 18 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> (y .P. (v +P. 1P)) = ((y .P. v) +P. (y .P. 1P)))
92	91	oveq1d 5470	. . . . . . . . . . . . . . . . 17 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> ((y .P. (v +P. 1P)) +P. (z .P. 1P)) = (((y .P. v) +P. (y .P. 1P)) +P. (z .P. 1P)))
93		mulclpr 6553	. . . . . . . . . . . . . . . . . . 19 |- ((y e. P. /\ v e. P.) -> (y .P. v) e. P.)
94	68, 24, 93	syl2anc 391	. . . . . . . . . . . . . . . . . 18 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> (y .P. v) e. P.)
95		addassprg 6555	. . . . . . . . . . . . . . . . . 18 |- (((y .P. v) e. P. /\ (y .P. 1P) e. P. /\ (z .P. 1P) e. P.) -> (((y .P. v) +P. (y .P. 1P)) +P. (z .P. 1P)) = ((y .P. v) +P. ((y .P. 1P) +P. (z .P. 1P))))
96	94, 70, 72, 95	syl3anc 1134	. . . . . . . . . . . . . . . . 17 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> (((y .P. v) +P. (y .P. 1P)) +P. (z .P. 1P)) = ((y .P. v) +P. ((y .P. 1P) +P. (z .P. 1P))))
97	92, 96	eqtrd 2069	. . . . . . . . . . . . . . . 16 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> ((y .P. (v +P. 1P)) +P. (z .P. 1P)) = ((y .P. v) +P. ((y .P. 1P) +P. (z .P. 1P))))
98	97	oveq1d 5470	. . . . . . . . . . . . . . 15 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> (((y .P. (v +P. 1P)) +P. (z .P. 1P)) +P. 1P) = (((y .P. v) +P. ((y .P. 1P) +P. (z .P. 1P))) +P. 1P))
99	98	adantr 261	. . . . . . . . . . . . . 14 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((w .P. v) = 1P /\ (z +P. w) = y)) -> (((y .P. (v +P. 1P)) +P. (z .P. 1P)) +P. 1P) = (((y .P. v) +P. ((y .P. 1P) +P. (z .P. 1P))) +P. 1P))
100		distrprg 6564	. . . . . . . . . . . . . . . . . . 19 |- ((z e. P. /\ v e. P. /\ 1P e. P.) -> (z .P. (v +P. 1P)) = ((z .P. v) +P. (z .P. 1P)))
101	57, 24, 67, 100	syl3anc 1134	. . . . . . . . . . . . . . . . . 18 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> (z .P. (v +P. 1P)) = ((z .P. v) +P. (z .P. 1P)))
102	101	oveq2d 5471	. . . . . . . . . . . . . . . . 17 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> ((y .P. 1P) +P. (z .P. (v +P. 1P))) = ((y .P. 1P) +P. ((z .P. v) +P. (z .P. 1P))))
103	70, 66, 72, 76, 78	caov12d 5624	. . . . . . . . . . . . . . . . 17 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> ((y .P. 1P) +P. ((z .P. v) +P. (z .P. 1P))) = ((z .P. v) +P. ((y .P. 1P) +P. (z .P. 1P))))
104	102, 103	eqtrd 2069	. . . . . . . . . . . . . . . 16 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> ((y .P. 1P) +P. (z .P. (v +P. 1P))) = ((z .P. v) +P. ((y .P. 1P) +P. (z .P. 1P))))
105	104	oveq1d 5470	. . . . . . . . . . . . . . 15 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> (((y .P. 1P) +P. (z .P. (v +P. 1P))) +P. ( 1P +P. 1P)) = (((z .P. v) +P. ((y .P. 1P) +P. (z .P. 1P))) +P. ( 1P +P. 1P)))
106	105	adantr 261	. . . . . . . . . . . . . 14 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((w .P. v) = 1P /\ (z +P. w) = y)) -> (((y .P. 1P) +P. (z .P. (v +P. 1P))) +P. ( 1P +P. 1P)) = (((z .P. v) +P. ((y .P. 1P) +P. (z .P. 1P))) +P. ( 1P +P. 1P)))
107	89, 99, 106	3eqtr4d 2079	. . . . . . . . . . . . 13 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((w .P. v) = 1P /\ (z +P. w) = y)) -> (((y .P. (v +P. 1P)) +P. (z .P. 1P)) +P. 1P) = (((y .P. 1P) +P. (z .P. (v +P. 1P))) +P. ( 1P +P. 1P)))
108	24, 16, 17	sylancl 392	. . . . . . . . . . . . . . . . 17 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> (v +P. 1P) e. P.)
109		mulclpr 6553	. . . . . . . . . . . . . . . . 17 |- ((y e. P. /\ (v +P. 1P) e. P.) -> (y .P. (v +P. 1P)) e. P.)
110	68, 108, 109	syl2anc 391	. . . . . . . . . . . . . . . 16 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> (y .P. (v +P. 1P)) e. P.)
111		addclpr 6520	. . . . . . . . . . . . . . . 16 |- (((y .P. (v +P. 1P)) e. P. /\ (z .P. 1P) e. P.) -> ((y .P. (v +P. 1P)) +P. (z .P. 1P)) e. P.)
112	110, 72, 111	syl2anc 391	. . . . . . . . . . . . . . 15 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> ((y .P. (v +P. 1P)) +P. (z .P. 1P)) e. P.)
113	104, 84	eqeltrd 2111	. . . . . . . . . . . . . . 15 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> ((y .P. 1P) +P. (z .P. (v +P. 1P))) e. P.)
114		addclpr 6520	. . . . . . . . . . . . . . . . 17 |- (( 1P e. P. /\ 1P e. P.) -> ( 1P +P. 1P) e. P.)
115	16, 16, 114	mp2an 402	. . . . . . . . . . . . . . . 16 |- ( 1P +P. 1P) e. P.
116	115	a1i 9	. . . . . . . . . . . . . . 15 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> ( 1P +P. 1P) e. P.)
117		enreceq 6664	. . . . . . . . . . . . . . 15 |- (((((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))))
118	112, 113, 116, 67, 117	syl22anc 1135	. . . . . . . . . . . . . 14 |- (((y e. P. /\ z e. P.) /\ (w 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))))
119	118	adantr 261	. . . . . . . . . . . . 13 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((w .P. v) = 1P /\ (z +P. w) = y)) -> ([ <.((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))))
120	107, 119	mpbird 156	. . . . . . . . . . . 12 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((w .P. v) = 1P /\ (z +P. w) = y)) -> [ <.((y .P. (v +P. 1P)) +P. (z .P. 1P)) , ((y .P. 1P) +P. (z .P. (v +P. 1P))) >.] ~R = [ <.( 1P +P. 1P) , 1P >.] ~R )
121	39, 120	eqtrd 2069	. . . . . . . . . . 11 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((w .P. v) = 1P /\ (z +P. w) = y)) -> ([ <.y , z >.] ~R .R [ <.(v +P. 1P) , 1P >.] ~R ) = [ <.( 1P +P. 1P) , 1P >.] ~R )
122		df-1r 6660	. . . . . . . . . . 11 |- 1R = [ <.( 1P +P. 1P) , 1P >.] ~R
123	121, 122	syl6eqr 2087	. . . . . . . . . 10 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((w .P. v) = 1P /\ (z +P. w) = y)) -> ([ <.y , z >.] ~R .R [ <.(v +P. 1P) , 1P >.] ~R ) = 1R)
124		breq2 3759	. . . . . . . . . . . 12 |- (x = [ <.(v +P. 1P) , 1P >.] ~R -> ( 0R <R x <-> 0R <R [ <.(v +P. 1P) , 1P >.] ~R ))
125		oveq2 5463	. . . . . . . . . . . . 13 |- (x = [ <.(v +P. 1P) , 1P >.] ~R -> ([ <.y , z >.] ~R .R x) = ([ <.y , z >.] ~R .R [ <.(v +P. 1P) , 1P >.] ~R ))
126	125	eqeq1d 2045	. . . . . . . . . . . 12 |- (x = [ <.(v +P. 1P) , 1P >.] ~R -> (([ <.y , z >.] ~R .R x) = 1R <-> ([ <.y , z >.] ~R .R [ <.(v +P. 1P) , 1P >.] ~R ) = 1R))
127	124, 126	anbi12d 442	. . . . . . . . . . 11 |- (x = [ <.(v +P. 1P) , 1P >.] ~R -> (( 0R <R x /\ ([ <.y , z >.] ~R .R x) = 1R) <-> ( 0R <R [ <.(v +P. 1P) , 1P >.] ~R /\ ([ <.y , z >.] ~R .R [ <.(v +P. 1P) , 1P >.] ~R ) = 1R)))
128	127	rspcev 2650	. . . . . . . . . 10 |- (([ <.(v +P. 1P) , 1P >.] ~R e. R. /\ ( 0R <R [ <.(v +P. 1P) , 1P >.] ~R /\ ([ <.y , z >.] ~R .R [ <.(v +P. 1P) , 1P >.] ~R ) = 1R)) -> E.x e. R. ( 0R <R x /\ ([ <.y , z >.] ~R .R x) = 1R))
129	23, 33, 123, 128	syl12anc 1132	. . . . . . . . 9 |- ((((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) /\ ((w .P. v) = 1P /\ (z +P. w) = y)) -> E.x e. R. ( 0R <R x /\ ([ <.y , z >.] ~R .R x) = 1R))
130	129	exp32 347	. . . . . . . 8 |- (((y e. P. /\ z e. P.) /\ (w e. P. /\ v e. P.)) -> ((w .P. v) = 1P -> ((z +P. w) = y -> E.x e. R. ( 0R <R x /\ ([ <.y , z >.] ~R .R x) = 1R))))
131	130	anassrs 380	. . . . . . 7 |- ((((y e. P. /\ z e. P.) /\ w e. P.) /\ v e. P.) -> ((w .P. v) = 1P -> ((z +P. w) = y -> E.x e. R. ( 0R <R x /\ ([ <.y , z >.] ~R .R x) = 1R))))
132	131	rexlimdva 2427	. . . . . 6 |- (((y e. P. /\ z e. P.) /\ w e. P.) -> (E.v e. P. (w .P. v) = 1P -> ((z +P. w) = y -> E.x e. R. ( 0R <R x /\ ([ <.y , z >.] ~R .R x) = 1R))))
133	15, 132	mpd 13	. . . . 5 |- (((y e. P. /\ z e. P.) /\ w e. P.) -> ((z +P. w) = y -> E.x e. R. ( 0R <R x /\ ([ <.y , z >.] ~R .R x) = 1R)))
134	133	rexlimdva 2427	. . . 4 |- ((y e. P. /\ z e. P.) -> (E.w e. P. (z +P. w) = y -> E.x e. R. ( 0R <R x /\ ([ <.y , z >.] ~R .R x) = 1R)))
135	13, 134	syl5 28	. . 3 |- ((y e. P. /\ z e. P.) -> ( 0R <R [ <.y , z >.] ~R -> E.x e. R. ( 0R <R x /\ ([ <.y , z >.] ~R .R x) = 1R)))
136	4, 10, 135	ecoptocl 6129	. 2 |- (A e. R. -> ( 0R <R A -> E.x e. R. ( 0R <R x /\ (A .R x) = 1R)))
137	3, 136	mpcom 32	1 |- ( 0R <R A -> E.x e. R. ( 0R <R x /\ (A .R x) = 1R))

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98   /\ w3a 884   = wceq 1242   e. wcel 1390  E.wrex 2301   <.cop 3370   class class class wbr 3755  (class class class)co 5455  [cec 6040   P.cnp 6275   1Pc1p 6276   +P. cpp 6277   .P. cmp 6278   <P cltp 6279   ~R cer 6280   R.cnr 6281   0Rc0r 6282   1Rc1r 6283   .R cmr 6286   <R cltr 6287

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3863  ax-sep 3866  ax-nul 3874  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-setind 4220  ax-iinf 4254

This theorem depends on definitions:  df-bi 110  df-dc 742  df-3or 885  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-int 3607  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-tr 3846  df-eprel 4017  df-id 4021  df-po 4024  df-iso 4025  df-iord 4069  df-on 4071  df-suc 4074  df-iom 4257  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-ov 5458  df-oprab 5459  df-mpt2 5460  df-1st 5709  df-2nd 5710  df-recs 5861  df-irdg 5897  df-1o 5940  df-2o 5941  df-oadd 5944  df-omul 5945  df-er 6042  df-ec 6044  df-qs 6048  df-ni 6288  df-pli 6289  df-mi 6290  df-lti 6291  df-plpq 6328  df-mpq 6329  df-enq 6331  df-nqqs 6332  df-plqqs 6333  df-mqqs 6334  df-1nqqs 6335  df-rq 6336  df-ltnqqs 6337  df-enq0 6407  df-nq0 6408  df-0nq0 6409  df-plq0 6410  df-mq0 6411  df-inp 6449  df-i1p 6450  df-iplp 6451  df-imp 6452  df-iltp 6453  df-enr 6654  df-nr 6655  df-mr 6657  df-ltr 6658  df-0r 6659  df-1r 6660

This theorem is referenced by:  recexsrlem  6702  axprecex  6764