Theorem recexgt0sr 6858

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 6823	. . . 4 |- <R C_ ( R. X. R. )
2	1	brel 4392	. . 3 |- ( 0R <R A -> ( 0R e. R. /\ A e. R. ) )
3	2	simprd 107	. 2 |- ( 0R <R A -> A e. R. )
4		df-nr 6812	. . 3 |- R. = ( ( P. X. P. ) /. ~R )
5		breq2 3768	. . . 4 |- ( [ <. y , z >. ] ~R = A -> ( 0R <R [ <. y , z >. ] ~R <-> 0R <R A ) )
6		oveq1 5519	. . . . . . 7 |- ( [ <. y , z >. ] ~R = A -> ( [ <. y , z >. ] ~R .R x ) = ( A .R x ) )
7	6	eqeq1d 2048	. . . . . 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 2327	. . . 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 6833	. . . . 5 |- ( 0R <R [ <. y , z >. ] ~R <-> z <P y )
12		ltexpri 6711	. . . . 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 6736	. . . . . . 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 6652	. . . . . . . . . . . . . 14 |- 1P e. P.
17		addclpr 6635	. . . . . . . . . . . . . 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 6822	. . . . . . . . . . . . . 14 |- ~R e. _V
20	19, 4	ecopqsi 6161	. . . . . . . . . . . . 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 6695	. . . . . . . . . . . . . 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 6676	. . . . . . . . . . . . . 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 3788	. . . . . . . . . . . 12 |- ( v e. P. -> 1P <P ( v +P. 1P ) )
31		gt0srpr 6833	. . . . . . . . . . . 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 6831	. . . . . . . . . . . . . 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 5519	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( z +P. w ) = y -> ( ( z +P. w ) .P. v ) = ( y .P. v ) )
41	40	eqcomd 2045	. . . . . . . . . . . . . . . . . . . 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 6678	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( f e. P. /\ h e. P. ) -> ( f .P. h ) = ( h .P. f ) )
44	43	3adant2 923	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( f .P. h ) = ( h .P. f ) )
45		mulcomprg 6678	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( g e. P. /\ h e. P. ) -> ( g .P. h ) = ( h .P. g ) )
46	45	3adant1 922	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( g .P. h ) = ( h .P. g ) )
47	44, 46	oveq12d 5530	. . . . . . . . . . . . . . . . . . . . . . . 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 6686	. . . . . . . . . . . . . . . . . . . . . . . . 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 1111	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( h .P. ( f +P. g ) ) = ( ( h .P. f ) +P. ( h .P. g ) ) )
50		simp3 906	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> h e. P. )
51		addclpr 6635	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( f e. P. /\ g e. P. ) -> ( f +P. g ) e. P. )
52	51	3adant3 924	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( f +P. g ) e. P. )
53		mulcomprg 6678	. . . . . . . . . . . . . . . . . . . . . . . . 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 2079	. . . . . . . . . . . . . . . . . . . . . . 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 5679	. . . . . . . . . . . . . . . . . . . . 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 5520	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( w .P. v ) = 1P -> ( ( z .P. v ) +P. ( w .P. v ) ) = ( ( z .P. v ) +P. 1P ) )
61	59, 60	sylan9eq 2092	. . . . . . . . . . . . . . . . . . . 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 2072	. . . . . . . . . . . . . . . . . 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 5527	. . . . . . . . . . . . . . . . 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 6670	. . . . . . . . . . . . . . . . . . . 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 6670	. . . . . . . . . . . . . . . . . . . . 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 6670	. . . . . . . . . . . . . . . . . . . . 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 6635	. . . . . . . . . . . . . . . . . . . 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 6676	. . . . . . . . . . . . . . . . . . . 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 6677	. . . . . . . . . . . . . . . . . . . 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 5681	. . . . . . . . . . . . . . . . . 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 2072	. . . . . . . . . . . . . . . 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 5527	. . . . . . . . . . . . . . 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 6635	. . . . . . . . . . . . . . . . . 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 6677	. . . . . . . . . . . . . . . 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 1135	. . . . . . . . . . . . . . 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 2072	. . . . . . . . . . . . . 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 6686	. . . . . . . . . . . . . . . . . . 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 1135	. . . . . . . . . . . . . . . . . 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 5527	. . . . . . . . . . . . . . . . 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 6670	. . . . . . . . . . . . . . . . . . 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 6677	. . . . . . . . . . . . . . . . . 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 1135	. . . . . . . . . . . . . . . . 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 2072	. . . . . . . . . . . . . . . 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 5527	. . . . . . . . . . . . . . 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 6686	. . . . . . . . . . . . . . . . . . 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 1135	. . . . . . . . . . . . . . . . . 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 5528	. . . . . . . . . . . . . . . . 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 5682	. . . . . . . . . . . . . . . . 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 2072	. . . . . . . . . . . . . . . 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 5527	. . . . . . . . . . . . . . 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 2082	. . . . . . . . . . . . 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 6670	. . . . . . . . . . . . . . . . 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 6635	. . . . . . . . . . . . . . . 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 2114	. . . . . . . . . . . . . . 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 6635	. . . . . . . . . . . . . . . . 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 6821	. . . . . . . . . . . . . . 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 1136	. . . . . . . . . . . . . 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 2072	. . . . . . . . . . 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 6817	. . . . . . . . . . 11 |- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
123	121, 122	syl6eqr 2090	. . . . . . . . . 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 3768	. . . . . . . . . . . 12 |- ( x = [ <. ( v +P. 1P ) , 1P >. ] ~R -> ( 0R <R x <-> 0R <R [ <. ( v +P. 1P ) , 1P >. ] ~R ) )
125		oveq2 5520	. . . . . . . . . . . . 13 |- ( x = [ <. ( v +P. 1P ) , 1P >. ] ~R -> ( [ <. y , z >. ] ~R .R x ) = ( [ <. y , z >. ] ~R .R [ <. ( v +P. 1P ) , 1P >. ] ~R ) )
126	125	eqeq1d 2048	. . . . . . . . . . . 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 2656	. . . . . . . . . 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 1133	. . . . . . . . 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 2433	. . . . . 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 2433	. . . 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 6193	. 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 885   = wceq 1243   e. wcel 1393   E.wrex 2307   <.cop 3378   class class class wbr 3764  (class class class)co 5512   [cec 6104   P.cnp 6389   1Pc1p 6390   +P. cpp 6391   .P. cmp 6392   <P cltp 6393   ~R cer 6394   R.cnr 6395   0Rc0r 6396   1Rc1r 6397   .R cmr 6400   <R cltr 6401

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 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-13 1404  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-coll 3872  ax-sep 3875  ax-nul 3883  ax-pow 3927  ax-pr 3944  ax-un 4170  ax-setind 4262  ax-iinf 4311

This theorem depends on definitions:  df-bi 110  df-dc 743  df-3or 886  df-3an 887  df-tru 1246  df-fal 1249  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ne 2206  df-ral 2311  df-rex 2312  df-reu 2313  df-rab 2315  df-v 2559  df-sbc 2765  df-csb 2853  df-dif 2920  df-un 2922  df-in 2924  df-ss 2931  df-nul 3225  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-int 3616  df-iun 3659  df-br 3765  df-opab 3819  df-mpt 3820  df-tr 3855  df-eprel 4026  df-id 4030  df-po 4033  df-iso 4034  df-iord 4103  df-on 4105  df-suc 4108  df-iom 4314  df-xp 4351  df-rel 4352  df-cnv 4353  df-co 4354  df-dm 4355  df-rn 4356  df-res 4357  df-ima 4358  df-iota 4867  df-fun 4904  df-fn 4905  df-f 4906  df-f1 4907  df-fo 4908  df-f1o 4909  df-fv 4910  df-ov 5515  df-oprab 5516  df-mpt2 5517  df-1st 5767  df-2nd 5768  df-recs 5920  df-irdg 5957  df-1o 6001  df-2o 6002  df-oadd 6005  df-omul 6006  df-er 6106  df-ec 6108  df-qs 6112  df-ni 6402  df-pli 6403  df-mi 6404  df-lti 6405  df-plpq 6442  df-mpq 6443  df-enq 6445  df-nqqs 6446  df-plqqs 6447  df-mqqs 6448  df-1nqqs 6449  df-rq 6450  df-ltnqqs 6451  df-enq0 6522  df-nq0 6523  df-0nq0 6524  df-plq0 6525  df-mq0 6526  df-inp 6564  df-i1p 6565  df-iplp 6566  df-imp 6567  df-iltp 6568  df-enr 6811  df-nr 6812  df-mr 6814  df-ltr 6815  df-0r 6816  df-1r 6817

This theorem is referenced by:  recexsrlem  6859  axprecex  6954