Theorem recexgt0sr 6950

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 6915	. . . 4 |- <R C_ ( R. X. R. )
2	1	brel 4410	. . 3 |- ( 0R <R A -> ( 0R e. R. /\ A e. R. ) )
3	2	simprd 112	. 2 |- ( 0R <R A -> A e. R. )
4		df-nr 6904	. . 3 |- R. = ( ( P. X. P. ) /. ~R )
5		breq2 3789	. . . 4 |- ( [ <. y , z >. ] ~R = A -> ( 0R <R [ <. y , z >. ] ~R <-> 0R <R A ) )
6		oveq1 5539	. . . . . . 7 |- ( [ <. y , z >. ] ~R = A -> ( [ <. y , z >. ] ~R .R x ) = ( A .R x ) )
7	6	eqeq1d 2089	. . . . . 6 |- ( [ <. y , z >. ] ~R = A -> ( ( [ <. y , z >. ] ~R .R x ) = 1R <-> ( A .R x ) = 1R ) )
8	7	anbi2d 451	. . . . 5 |- ( [ <. y , z >. ] ~R = A -> ( ( 0R <R x /\ ( [ <. y , z >. ] ~R .R x ) = 1R ) <-> ( 0R <R x /\ ( A .R x ) = 1R ) ) )
9	8	rexbidv 2369	. . . 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 232	. . 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 6925	. . . . 5 |- ( 0R <R [ <. y , z >. ] ~R <-> z <P y )
12		ltexpri 6803	. . . . 5 |- ( z <P y -> E. w e. P. ( z +P. w ) = y )
13	11, 12	sylbi 119	. . . 4 |- ( 0R <R [ <. y , z >. ] ~R -> E. w e. P. ( z +P. w ) = y )
14		recexpr 6828	. . . . . . 7 |- ( w e. P. -> E. v e. P. ( w .P. v ) = 1P )
15	14	adantl 271	. . . . . 6 |- ( ( ( y e. P. /\ z e. P. ) /\ w e. P. ) -> E. v e. P. ( w .P. v ) = 1P )
16		1pr 6744	. . . . . . . . . . . . . 14 |- 1P e. P.
17		addclpr 6727	. . . . . . . . . . . . . 14 |- ( ( v e. P. /\ 1P e. P. ) -> ( v +P. 1P ) e. P. )
18	16, 17	mpan2 415	. . . . . . . . . . . . 13 |- ( v e. P. -> ( v +P. 1P ) e. P. )
19		enrex 6914	. . . . . . . . . . . . . 14 |- ~R e. _V
20	19, 4	ecopqsi 6184	. . . . . . . . . . . . 13 |- ( ( ( v +P. 1P ) e. P. /\ 1P e. P. ) -> [ <. ( v +P. 1P ) , 1P >. ] ~R e. R. )
21	18, 16, 20	sylancl 404	. . . . . . . . . . . 12 |- ( v e. P. -> [ <. ( v +P. 1P ) , 1P >. ] ~R e. R. )
22	21	adantl 271	. . . . . . . . . . 11 |- ( ( w e. P. /\ v e. P. ) -> [ <. ( v +P. 1P ) , 1P >. ] ~R e. R. )
23	22	ad2antlr 472	. . . . . . . . . 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 498	. . . . . . . . . . . 12 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> v e. P. )
25	24	adantr 270	. . . . . . . . . . 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 6787	. . . . . . . . . . . . . 14 |- ( ( 1P e. P. /\ v e. P. ) -> 1P <P ( 1P +P. v ) )
27	16, 26	mpan 414	. . . . . . . . . . . . 13 |- ( v e. P. -> 1P <P ( 1P +P. v ) )
28		addcomprg 6768	. . . . . . . . . . . . . 14 |- ( ( 1P e. P. /\ v e. P. ) -> ( 1P +P. v ) = ( v +P. 1P ) )
29	16, 28	mpan 414	. . . . . . . . . . . . 13 |- ( v e. P. -> ( 1P +P. v ) = ( v +P. 1P ) )
30	27, 29	breqtrd 3809	. . . . . . . . . . . 12 |- ( v e. P. -> 1P <P ( v +P. 1P ) )
31		gt0srpr 6925	. . . . . . . . . . . 12 |- ( 0R <R [ <. ( v +P. 1P ) , 1P >. ] ~R <-> 1P <P ( v +P. 1P ) )
32	30, 31	sylibr 132	. . . . . . . . . . 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 306	. . . . . . . . . . . . . . . 16 |- ( v e. P. -> ( ( v +P. 1P ) e. P. /\ 1P e. P. ) )
35	34	anim2i 334	. . . . . . . . . . . . . . 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 270	. . . . . . . . . . . . . 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 6923	. . . . . . . . . . . . . 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 465	. . . . . . . . . . . 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 5539	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( z +P. w ) = y -> ( ( z +P. w ) .P. v ) = ( y .P. v ) )
41	40	eqcomd 2086	. . . . . . . . . . . . . . . . . . . 20 |- ( ( z +P. w ) = y -> ( y .P. v ) = ( ( z +P. w ) .P. v ) )
42	41	ad2antll 474	. . . . . . . . . . . . . . . . . . 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 6770	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( f e. P. /\ h e. P. ) -> ( f .P. h ) = ( h .P. f ) )
44	43	3adant2 957	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( f .P. h ) = ( h .P. f ) )
45		mulcomprg 6770	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( g e. P. /\ h e. P. ) -> ( g .P. h ) = ( h .P. g ) )
46	45	3adant1 956	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( g .P. h ) = ( h .P. g ) )
47	44, 46	oveq12d 5550	. . . . . . . . . . . . . . . . . . . . . . . 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 6778	. . . . . . . . . . . . . . . . . . . . . . . . 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 1145	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( h .P. ( f +P. g ) ) = ( ( h .P. f ) +P. ( h .P. g ) ) )
50		simp3 940	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> h e. P. )
51		addclpr 6727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( f e. P. /\ g e. P. ) -> ( f +P. g ) e. P. )
52	51	3adant3 958	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( f +P. g ) e. P. )
53		mulcomprg 6770	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( h e. P. /\ ( f +P. g ) e. P. ) -> ( h .P. ( f +P. g ) ) = ( ( f +P. g ) .P. h ) )
54	50, 52, 53	syl2anc 403	. . . . . . . . . . . . . . . . . . . . . . . 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 2120	. . . . . . . . . . . . . . . . . . . . . . 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 271	. . . . . . . . . . . . . . . . . . . . . 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 496	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> z e. P. )
58		simprl 497	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> w e. P. )
59	56, 57, 58, 24	caovdird 5699	. . . . . . . . . . . . . . . . . . . . 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 5540	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( w .P. v ) = 1P -> ( ( z .P. v ) +P. ( w .P. v ) ) = ( ( z .P. v ) +P. 1P ) )
61	59, 60	sylan9eq 2133	. . . . . . . . . . . . . . . . . . . 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 462	. . . . . . . . . . . . . . . . . . 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 2113	. . . . . . . . . . . . . . . . . 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 5547	. . . . . . . . . . . . . . . . 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 6762	. . . . . . . . . . . . . . . . . . . 20 |- ( ( z e. P. /\ v e. P. ) -> ( z .P. v ) e. P. )
66	57, 24, 65	syl2anc 403	. . . . . . . . . . . . . . . . . . 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 495	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> y e. P. )
69		mulclpr 6762	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( y e. P. /\ 1P e. P. ) -> ( y .P. 1P ) e. P. )
70	68, 16, 69	sylancl 404	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( y .P. 1P ) e. P. )
71		mulclpr 6762	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( z e. P. /\ 1P e. P. ) -> ( z .P. 1P ) e. P. )
72	57, 16, 71	sylancl 404	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( z .P. 1P ) e. P. )
73		addclpr 6727	. . . . . . . . . . . . . . . . . . . 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 403	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( ( y .P. 1P ) +P. ( z .P. 1P ) ) e. P. )
75		addcomprg 6768	. . . . . . . . . . . . . . . . . . . 20 |- ( ( f e. P. /\ g e. P. ) -> ( f +P. g ) = ( g +P. f ) )
76	75	adantl 271	. . . . . . . . . . . . . . . . . . 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 6769	. . . . . . . . . . . . . . . . . . . 20 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( ( f +P. g ) +P. h ) = ( f +P. ( g +P. h ) ) )
78	77	adantl 271	. . . . . . . . . . . . . . . . . . 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 5701	. . . . . . . . . . . . . . . . . 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 270	. . . . . . . . . . . . . . . . 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 2113	. . . . . . . . . . . . . . . 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 5547	. . . . . . . . . . . . . . 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 6727	. . . . . . . . . . . . . . . . . 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 403	. . . . . . . . . . . . . . . . 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 270	. . . . . . . . . . . . . . . 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 6769	. . . . . . . . . . . . . . . 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 1169	. . . . . . . . . . . . . . 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 2113	. . . . . . . . . . . . . 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 6778	. . . . . . . . . . . . . . . . . . 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 1169	. . . . . . . . . . . . . . . . . 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 5547	. . . . . . . . . . . . . . . . 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 6762	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. P. /\ v e. P. ) -> ( y .P. v ) e. P. )
94	68, 24, 93	syl2anc 403	. . . . . . . . . . . . . . . . . 18 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( y .P. v ) e. P. )
95		addassprg 6769	. . . . . . . . . . . . . . . . . 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 1169	. . . . . . . . . . . . . . . . 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 2113	. . . . . . . . . . . . . . . 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 5547	. . . . . . . . . . . . . . 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 270	. . . . . . . . . . . . . 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 6778	. . . . . . . . . . . . . . . . . . 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 1169	. . . . . . . . . . . . . . . . . 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 5548	. . . . . . . . . . . . . . . . 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 5702	. . . . . . . . . . . . . . . . 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 2113	. . . . . . . . . . . . . . . 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 5547	. . . . . . . . . . . . . . 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 270	. . . . . . . . . . . . . 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 2123	. . . . . . . . . . . . 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 404	. . . . . . . . . . . . . . . . 17 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( v +P. 1P ) e. P. )
109		mulclpr 6762	. . . . . . . . . . . . . . . . 17 |- ( ( y e. P. /\ ( v +P. 1P ) e. P. ) -> ( y .P. ( v +P. 1P ) ) e. P. )
110	68, 108, 109	syl2anc 403	. . . . . . . . . . . . . . . 16 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( y .P. ( v +P. 1P ) ) e. P. )
111		addclpr 6727	. . . . . . . . . . . . . . . 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 403	. . . . . . . . . . . . . . 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 2155	. . . . . . . . . . . . . . 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 6727	. . . . . . . . . . . . . . . . 17 |- ( ( 1P e. P. /\ 1P e. P. ) -> ( 1P +P. 1P ) e. P. )
115	16, 16, 114	mp2an 416	. . . . . . . . . . . . . . . 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 6913	. . . . . . . . . . . . . . 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 1170	. . . . . . . . . . . . . 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 270	. . . . . . . . . . . . 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 165	. . . . . . . . . . . 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 2113	. . . . . . . . . . 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 6909	. . . . . . . . . . 11 |- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
123	121, 122	syl6eqr 2131	. . . . . . . . . 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 3789	. . . . . . . . . . . 12 |- ( x = [ <. ( v +P. 1P ) , 1P >. ] ~R -> ( 0R <R x <-> 0R <R [ <. ( v +P. 1P ) , 1P >. ] ~R ) )
125		oveq2 5540	. . . . . . . . . . . . 13 |- ( x = [ <. ( v +P. 1P ) , 1P >. ] ~R -> ( [ <. y , z >. ] ~R .R x ) = ( [ <. y , z >. ] ~R .R [ <. ( v +P. 1P ) , 1P >. ] ~R ) )
126	125	eqeq1d 2089	. . . . . . . . . . . 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 456	. . . . . . . . . . 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 2701	. . . . . . . . . 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 1167	. . . . . . . . 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 357	. . . . . . . 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 392	. . . . . . 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 2477	. . . . . 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 2477	. . . 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 6216	. 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 102   <-> wb 103   /\ w3a 919   = wceq 1284   e. wcel 1433   E.wrex 2349   <.cop 3401   class class class wbr 3785  (class class class)co 5532   [cec 6127   P.cnp 6481   1Pc1p 6482   +P. cpp 6483   .P. cmp 6484   <P cltp 6485   ~R cer 6486   R.cnr 6487   0Rc0r 6488   1Rc1r 6489   .R cmr 6492   <R cltr 6493

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 576  ax-in2 577  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-13 1444  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-coll 3893  ax-sep 3896  ax-nul 3904  ax-pow 3948  ax-pr 3964  ax-un 4188  ax-setind 4280  ax-iinf 4329

This theorem depends on definitions:  df-bi 115  df-dc 776  df-3or 920  df-3an 921  df-tru 1287  df-fal 1290  df-nf 1390  df-sb 1686  df-eu 1944  df-mo 1945  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ne 2246  df-ral 2353  df-rex 2354  df-reu 2355  df-rab 2357  df-v 2603  df-sbc 2816  df-csb 2909  df-dif 2975  df-un 2977  df-in 2979  df-ss 2986  df-nul 3252  df-pw 3384  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-int 3637  df-iun 3680  df-br 3786  df-opab 3840  df-mpt 3841  df-tr 3876  df-eprel 4044  df-id 4048  df-po 4051  df-iso 4052  df-iord 4121  df-on 4123  df-suc 4126  df-iom 4332  df-xp 4369  df-rel 4370  df-cnv 4371  df-co 4372  df-dm 4373  df-rn 4374  df-res 4375  df-ima 4376  df-iota 4887  df-fun 4924  df-fn 4925  df-f 4926  df-f1 4927  df-fo 4928  df-f1o 4929  df-fv 4930  df-ov 5535  df-oprab 5536  df-mpt2 5537  df-1st 5787  df-2nd 5788  df-recs 5943  df-irdg 5980  df-1o 6024  df-2o 6025  df-oadd 6028  df-omul 6029  df-er 6129  df-ec 6131  df-qs 6135  df-ni 6494  df-pli 6495  df-mi 6496  df-lti 6497  df-plpq 6534  df-mpq 6535  df-enq 6537  df-nqqs 6538  df-plqqs 6539  df-mqqs 6540  df-1nqqs 6541  df-rq 6542  df-ltnqqs 6543  df-enq0 6614  df-nq0 6615  df-0nq0 6616  df-plq0 6617  df-mq0 6618  df-inp 6656  df-i1p 6657  df-iplp 6658  df-imp 6659  df-iltp 6660  df-enr 6903  df-nr 6904  df-mr 6906  df-ltr 6907  df-0r 6908  df-1r 6909

This theorem is referenced by:  recexsrlem  6951  axprecex  7046