Theorem recexgt0sr 8104

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 8069	. . . 4 |- <R C_ ( R. X. R. )
2	1	brel 4807	. . 3 |- ( 0R <R A -> ( 0R e. R. /\ A e. R. ) )
3	2	simprd 114	. 2 |- ( 0R <R A -> A e. R. )
4		df-nr 8058	. . 3 |- R. = ( ( P. X. P. ) /. ~R )
5		breq2 4118	. . . 4 |- ( [ <. y , z >. ] ~R = A -> ( 0R <R [ <. y , z >. ] ~R <-> 0R <R A ) )
6		oveq1 6065	. . . . . . 7 |- ( [ <. y , z >. ] ~R = A -> ( [ <. y , z >. ] ~R .R x ) = ( A .R x ) )
7	6	eqeq1d 2243	. . . . . 6 |- ( [ <. y , z >. ] ~R = A -> ( ( [ <. y , z >. ] ~R .R x ) = 1R <-> ( A .R x ) = 1R ) )
8	7	anbi2d 464	. . . . 5 |- ( [ <. y , z >. ] ~R = A -> ( ( 0R <R x /\ ( [ <. y , z >. ] ~R .R x ) = 1R ) <-> ( 0R <R x /\ ( A .R x ) = 1R ) ) )
9	8	rexbidv 2545	. . . 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 234	. . 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 8079	. . . . 5 |- ( 0R <R [ <. y , z >. ] ~R <-> z <P y )
12		ltexpri 7944	. . . . 5 |- ( z <P y -> E. w e. P. ( z +P. w ) = y )
13	11, 12	sylbi 121	. . . 4 |- ( 0R <R [ <. y , z >. ] ~R -> E. w e. P. ( z +P. w ) = y )
14		recexpr 7969	. . . . . . 7 |- ( w e. P. -> E. v e. P. ( w .P. v ) = 1P )
15	14	adantl 277	. . . . . 6 |- ( ( ( y e. P. /\ z e. P. ) /\ w e. P. ) -> E. v e. P. ( w .P. v ) = 1P )
16		1pr 7885	. . . . . . . . . . . . . 14 |- 1P e. P.
17		addclpr 7868	. . . . . . . . . . . . . 14 |- ( ( v e. P. /\ 1P e. P. ) -> ( v +P. 1P ) e. P. )
18	16, 17	mpan2 425	. . . . . . . . . . . . 13 |- ( v e. P. -> ( v +P. 1P ) e. P. )
19		enrex 8068	. . . . . . . . . . . . . 14 |- ~R e. _V
20	19, 4	ecopqsi 6837	. . . . . . . . . . . . 13 |- ( ( ( v +P. 1P ) e. P. /\ 1P e. P. ) -> [ <. ( v +P. 1P ) , 1P >. ] ~R e. R. )
21	18, 16, 20	sylancl 413	. . . . . . . . . . . 12 |- ( v e. P. -> [ <. ( v +P. 1P ) , 1P >. ] ~R e. R. )
22	21	adantl 277	. . . . . . . . . . 11 |- ( ( w e. P. /\ v e. P. ) -> [ <. ( v +P. 1P ) , 1P >. ] ~R e. R. )
23	22	ad2antlr 489	. . . . . . . . . 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 533	. . . . . . . . . . . 12 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> v e. P. )
25	24	adantr 276	. . . . . . . . . . 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 7928	. . . . . . . . . . . . . 14 |- ( ( 1P e. P. /\ v e. P. ) -> 1P <P ( 1P +P. v ) )
27	16, 26	mpan 424	. . . . . . . . . . . . 13 |- ( v e. P. -> 1P <P ( 1P +P. v ) )
28		addcomprg 7909	. . . . . . . . . . . . . 14 |- ( ( 1P e. P. /\ v e. P. ) -> ( 1P +P. v ) = ( v +P. 1P ) )
29	16, 28	mpan 424	. . . . . . . . . . . . 13 |- ( v e. P. -> ( 1P +P. v ) = ( v +P. 1P ) )
30	27, 29	breqtrd 4140	. . . . . . . . . . . 12 |- ( v e. P. -> 1P <P ( v +P. 1P ) )
31		gt0srpr 8079	. . . . . . . . . . . 12 |- ( 0R <R [ <. ( v +P. 1P ) , 1P >. ] ~R <-> 1P <P ( v +P. 1P ) )
32	30, 31	sylibr 134	. . . . . . . . . . 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 313	. . . . . . . . . . . . . . . 16 |- ( v e. P. -> ( ( v +P. 1P ) e. P. /\ 1P e. P. ) )
35	34	anim2i 342	. . . . . . . . . . . . . . 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 276	. . . . . . . . . . . . . 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 8077	. . . . . . . . . . . . . 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 482	. . . . . . . . . . . 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 6065	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( z +P. w ) = y -> ( ( z +P. w ) .P. v ) = ( y .P. v ) )
41	40	eqcomd 2240	. . . . . . . . . . . . . . . . . . . 20 |- ( ( z +P. w ) = y -> ( y .P. v ) = ( ( z +P. w ) .P. v ) )
42	41	ad2antll 491	. . . . . . . . . . . . . . . . . . 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 7911	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( f e. P. /\ h e. P. ) -> ( f .P. h ) = ( h .P. f ) )
44	43	3adant2 1043	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( f .P. h ) = ( h .P. f ) )
45		mulcomprg 7911	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( g e. P. /\ h e. P. ) -> ( g .P. h ) = ( h .P. g ) )
46	45	3adant1 1042	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( g .P. h ) = ( h .P. g ) )
47	44, 46	oveq12d 6076	. . . . . . . . . . . . . . . . . . . . . . . 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 7919	. . . . . . . . . . . . . . . . . . . . . . . . 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 1237	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( h .P. ( f +P. g ) ) = ( ( h .P. f ) +P. ( h .P. g ) ) )
50		simp3 1026	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> h e. P. )
51		addclpr 7868	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( f e. P. /\ g e. P. ) -> ( f +P. g ) e. P. )
52	51	3adant3 1044	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( f +P. g ) e. P. )
53		mulcomprg 7911	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( h e. P. /\ ( f +P. g ) e. P. ) -> ( h .P. ( f +P. g ) ) = ( ( f +P. g ) .P. h ) )
54	50, 52, 53	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . 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 2274	. . . . . . . . . . . . . . . . . . . . . . 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 277	. . . . . . . . . . . . . . . . . . . . . 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 529	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> z e. P. )
58		simprl 531	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> w e. P. )
59	56, 57, 58, 24	caovdird 6241	. . . . . . . . . . . . . . . . . . . . 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 6066	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( w .P. v ) = 1P -> ( ( z .P. v ) +P. ( w .P. v ) ) = ( ( z .P. v ) +P. 1P ) )
61	59, 60	sylan9eq 2287	. . . . . . . . . . . . . . . . . . . 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 479	. . . . . . . . . . . . . . . . . . 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 2267	. . . . . . . . . . . . . . . . . 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 6073	. . . . . . . . . . . . . . . . 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 7903	. . . . . . . . . . . . . . . . . . . 20 |- ( ( z e. P. /\ v e. P. ) -> ( z .P. v ) e. P. )
66	57, 24, 65	syl2anc 411	. . . . . . . . . . . . . . . . . . 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 527	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> y e. P. )
69		mulclpr 7903	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( y e. P. /\ 1P e. P. ) -> ( y .P. 1P ) e. P. )
70	68, 16, 69	sylancl 413	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( y .P. 1P ) e. P. )
71		mulclpr 7903	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( z e. P. /\ 1P e. P. ) -> ( z .P. 1P ) e. P. )
72	57, 16, 71	sylancl 413	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( z .P. 1P ) e. P. )
73		addclpr 7868	. . . . . . . . . . . . . . . . . . . 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 411	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( ( y .P. 1P ) +P. ( z .P. 1P ) ) e. P. )
75		addcomprg 7909	. . . . . . . . . . . . . . . . . . . 20 |- ( ( f e. P. /\ g e. P. ) -> ( f +P. g ) = ( g +P. f ) )
76	75	adantl 277	. . . . . . . . . . . . . . . . . . 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 7910	. . . . . . . . . . . . . . . . . . . 20 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( ( f +P. g ) +P. h ) = ( f +P. ( g +P. h ) ) )
78	77	adantl 277	. . . . . . . . . . . . . . . . . . 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 6243	. . . . . . . . . . . . . . . . . 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 276	. . . . . . . . . . . . . . . . 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 2267	. . . . . . . . . . . . . . . 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 6073	. . . . . . . . . . . . . . 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 7868	. . . . . . . . . . . . . . . . . 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 411	. . . . . . . . . . . . . . . . 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 276	. . . . . . . . . . . . . . . 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 7910	. . . . . . . . . . . . . . . 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 1274	. . . . . . . . . . . . . . 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 2267	. . . . . . . . . . . . . 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 7919	. . . . . . . . . . . . . . . . . . 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 1274	. . . . . . . . . . . . . . . . . 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 6073	. . . . . . . . . . . . . . . . 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 7903	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. P. /\ v e. P. ) -> ( y .P. v ) e. P. )
94	68, 24, 93	syl2anc 411	. . . . . . . . . . . . . . . . . 18 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( y .P. v ) e. P. )
95		addassprg 7910	. . . . . . . . . . . . . . . . . 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 1274	. . . . . . . . . . . . . . . . 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 2267	. . . . . . . . . . . . . . . 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 6073	. . . . . . . . . . . . . . 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 276	. . . . . . . . . . . . . 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 7919	. . . . . . . . . . . . . . . . . . 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 1274	. . . . . . . . . . . . . . . . . 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 6074	. . . . . . . . . . . . . . . . 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 6244	. . . . . . . . . . . . . . . . 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 2267	. . . . . . . . . . . . . . . 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 6073	. . . . . . . . . . . . . . 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 276	. . . . . . . . . . . . . 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 2277	. . . . . . . . . . . . 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 413	. . . . . . . . . . . . . . . . 17 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( v +P. 1P ) e. P. )
109		mulclpr 7903	. . . . . . . . . . . . . . . . 17 |- ( ( y e. P. /\ ( v +P. 1P ) e. P. ) -> ( y .P. ( v +P. 1P ) ) e. P. )
110	68, 108, 109	syl2anc 411	. . . . . . . . . . . . . . . 16 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( y .P. ( v +P. 1P ) ) e. P. )
111		addclpr 7868	. . . . . . . . . . . . . . . 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 411	. . . . . . . . . . . . . . 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 2311	. . . . . . . . . . . . . . 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 7868	. . . . . . . . . . . . . . . . 17 |- ( ( 1P e. P. /\ 1P e. P. ) -> ( 1P +P. 1P ) e. P. )
115	16, 16, 114	mp2an 426	. . . . . . . . . . . . . . . 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 8067	. . . . . . . . . . . . . . 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 1275	. . . . . . . . . . . . . 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 276	. . . . . . . . . . . . 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 167	. . . . . . . . . . . 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 2267	. . . . . . . . . . 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 8063	. . . . . . . . . . 11 |- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
123	121, 122	eqtr4di 2285	. . . . . . . . . 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 4118	. . . . . . . . . . . 12 |- ( x = [ <. ( v +P. 1P ) , 1P >. ] ~R -> ( 0R <R x <-> 0R <R [ <. ( v +P. 1P ) , 1P >. ] ~R ) )
125		oveq2 6066	. . . . . . . . . . . . 13 |- ( x = [ <. ( v +P. 1P ) , 1P >. ] ~R -> ( [ <. y , z >. ] ~R .R x ) = ( [ <. y , z >. ] ~R .R [ <. ( v +P. 1P ) , 1P >. ] ~R ) )
126	125	eqeq1d 2243	. . . . . . . . . . . 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 473	. . . . . . . . . . 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 2923	. . . . . . . . . 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 1272	. . . . . . . . 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 365	. . . . . . . 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 400	. . . . . . 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 2662	. . . . . 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 2662	. . . 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 32	. . 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 6869	. 2 |- ( A e. R. -> ( 0R <R A -> E. x e. R. ( 0R <R x /\ ( A .R x ) = 1R ) ) )
137	3, 136	mpcom 36	1 |- ( 0R <R A -> E. x e. R. ( 0R <R x /\ ( A .R x ) = 1R ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 1005   = wceq 1398   e. wcel 2205   E.wrex 2523   <.cop 3697   class class class wbr 4114  (class class class)co 6058   [cec 6778   P.cnp 7622   1Pc1p 7623   +P. cpp 7624   .P. cmp 7625   <P cltp 7626   ~R cer 7627   R.cnr 7628   0Rc0r 7629   1Rc1r 7630   .R cmr 7633   <R cltr 7634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2207  ax-14 2208  ax-ext 2216  ax-coll 4230  ax-sep 4233  ax-nul 4241  ax-pow 4292  ax-pr 4327  ax-un 4559  ax-setind 4664  ax-iinf 4715

This theorem depends on definitions:  df-bi 117  df-dc 843  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ne 2415  df-ral 2527  df-rex 2528  df-reu 2529  df-rab 2531  df-v 2817  df-sbc 3046  df-csb 3142  df-dif 3216  df-un 3218  df-in 3220  df-ss 3227  df-nul 3513  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-int 3955  df-iun 3998  df-br 4115  df-opab 4177  df-mpt 4178  df-tr 4214  df-eprel 4415  df-id 4419  df-po 4422  df-iso 4423  df-iord 4492  df-on 4494  df-suc 4497  df-iom 4718  df-xp 4760  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-rn 4765  df-res 4766  df-ima 4767  df-iota 5317  df-fun 5359  df-fn 5360  df-f 5361  df-f1 5362  df-fo 5363  df-f1o 5364  df-fv 5365  df-ov 6061  df-oprab 6062  df-mpo 6063  df-1st 6347  df-2nd 6348  df-recs 6549  df-irdg 6614  df-1o 6660  df-2o 6661  df-oadd 6664  df-omul 6665  df-er 6780  df-ec 6782  df-qs 6786  df-ni 7635  df-pli 7636  df-mi 7637  df-lti 7638  df-plpq 7675  df-mpq 7676  df-enq 7678  df-nqqs 7679  df-plqqs 7680  df-mqqs 7681  df-1nqqs 7682  df-rq 7683  df-ltnqqs 7684  df-enq0 7755  df-nq0 7756  df-0nq0 7757  df-plq0 7758  df-mq0 7759  df-inp 7797  df-i1p 7798  df-iplp 7799  df-imp 7800  df-iltp 7801  df-enr 8057  df-nr 8058  df-mr 8060  df-ltr 8061  df-0r 8062  df-1r 8063

This theorem is referenced by:  recexsrlem  8105  axprecex  8211