Theorem recexgt0sr 7605

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 7570	. . . 4 |- <R C_ ( R. X. R. )
2	1	brel 4599	. . 3 |- ( 0R <R A -> ( 0R e. R. /\ A e. R. ) )
3	2	simprd 113	. 2 |- ( 0R <R A -> A e. R. )
4		df-nr 7559	. . 3 |- R. = ( ( P. X. P. ) /. ~R )
5		breq2 3941	. . . 4 |- ( [ <. y , z >. ] ~R = A -> ( 0R <R [ <. y , z >. ] ~R <-> 0R <R A ) )
6		oveq1 5789	. . . . . . 7 |- ( [ <. y , z >. ] ~R = A -> ( [ <. y , z >. ] ~R .R x ) = ( A .R x ) )
7	6	eqeq1d 2149	. . . . . 6 |- ( [ <. y , z >. ] ~R = A -> ( ( [ <. y , z >. ] ~R .R x ) = 1R <-> ( A .R x ) = 1R ) )
8	7	anbi2d 460	. . . . 5 |- ( [ <. y , z >. ] ~R = A -> ( ( 0R <R x /\ ( [ <. y , z >. ] ~R .R x ) = 1R ) <-> ( 0R <R x /\ ( A .R x ) = 1R ) ) )
9	8	rexbidv 2439	. . . 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 233	. . 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 7580	. . . . 5 |- ( 0R <R [ <. y , z >. ] ~R <-> z <P y )
12		ltexpri 7445	. . . . 5 |- ( z <P y -> E. w e. P. ( z +P. w ) = y )
13	11, 12	sylbi 120	. . . 4 |- ( 0R <R [ <. y , z >. ] ~R -> E. w e. P. ( z +P. w ) = y )
14		recexpr 7470	. . . . . . 7 |- ( w e. P. -> E. v e. P. ( w .P. v ) = 1P )
15	14	adantl 275	. . . . . 6 |- ( ( ( y e. P. /\ z e. P. ) /\ w e. P. ) -> E. v e. P. ( w .P. v ) = 1P )
16		1pr 7386	. . . . . . . . . . . . . 14 |- 1P e. P.
17		addclpr 7369	. . . . . . . . . . . . . 14 |- ( ( v e. P. /\ 1P e. P. ) -> ( v +P. 1P ) e. P. )
18	16, 17	mpan2 422	. . . . . . . . . . . . 13 |- ( v e. P. -> ( v +P. 1P ) e. P. )
19		enrex 7569	. . . . . . . . . . . . . 14 |- ~R e. _V
20	19, 4	ecopqsi 6492	. . . . . . . . . . . . 13 |- ( ( ( v +P. 1P ) e. P. /\ 1P e. P. ) -> [ <. ( v +P. 1P ) , 1P >. ] ~R e. R. )
21	18, 16, 20	sylancl 410	. . . . . . . . . . . 12 |- ( v e. P. -> [ <. ( v +P. 1P ) , 1P >. ] ~R e. R. )
22	21	adantl 275	. . . . . . . . . . 11 |- ( ( w e. P. /\ v e. P. ) -> [ <. ( v +P. 1P ) , 1P >. ] ~R e. R. )
23	22	ad2antlr 481	. . . . . . . . . 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 522	. . . . . . . . . . . 12 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> v e. P. )
25	24	adantr 274	. . . . . . . . . . 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 7429	. . . . . . . . . . . . . 14 |- ( ( 1P e. P. /\ v e. P. ) -> 1P <P ( 1P +P. v ) )
27	16, 26	mpan 421	. . . . . . . . . . . . 13 |- ( v e. P. -> 1P <P ( 1P +P. v ) )
28		addcomprg 7410	. . . . . . . . . . . . . 14 |- ( ( 1P e. P. /\ v e. P. ) -> ( 1P +P. v ) = ( v +P. 1P ) )
29	16, 28	mpan 421	. . . . . . . . . . . . 13 |- ( v e. P. -> ( 1P +P. v ) = ( v +P. 1P ) )
30	27, 29	breqtrd 3962	. . . . . . . . . . . 12 |- ( v e. P. -> 1P <P ( v +P. 1P ) )
31		gt0srpr 7580	. . . . . . . . . . . 12 |- ( 0R <R [ <. ( v +P. 1P ) , 1P >. ] ~R <-> 1P <P ( v +P. 1P ) )
32	30, 31	sylibr 133	. . . . . . . . . . 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 311	. . . . . . . . . . . . . . . 16 |- ( v e. P. -> ( ( v +P. 1P ) e. P. /\ 1P e. P. ) )
35	34	anim2i 340	. . . . . . . . . . . . . . 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 274	. . . . . . . . . . . . . 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 7578	. . . . . . . . . . . . . 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 474	. . . . . . . . . . . 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 5789	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( z +P. w ) = y -> ( ( z +P. w ) .P. v ) = ( y .P. v ) )
41	40	eqcomd 2146	. . . . . . . . . . . . . . . . . . . 20 |- ( ( z +P. w ) = y -> ( y .P. v ) = ( ( z +P. w ) .P. v ) )
42	41	ad2antll 483	. . . . . . . . . . . . . . . . . . 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 7412	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( f e. P. /\ h e. P. ) -> ( f .P. h ) = ( h .P. f ) )
44	43	3adant2 1001	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( f .P. h ) = ( h .P. f ) )
45		mulcomprg 7412	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( g e. P. /\ h e. P. ) -> ( g .P. h ) = ( h .P. g ) )
46	45	3adant1 1000	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( g .P. h ) = ( h .P. g ) )
47	44, 46	oveq12d 5800	. . . . . . . . . . . . . . . . . . . . . . . 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 7420	. . . . . . . . . . . . . . . . . . . . . . . . 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 1189	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( h .P. ( f +P. g ) ) = ( ( h .P. f ) +P. ( h .P. g ) ) )
50		simp3 984	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> h e. P. )
51		addclpr 7369	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( f e. P. /\ g e. P. ) -> ( f +P. g ) e. P. )
52	51	3adant3 1002	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( f +P. g ) e. P. )
53		mulcomprg 7412	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( h e. P. /\ ( f +P. g ) e. P. ) -> ( h .P. ( f +P. g ) ) = ( ( f +P. g ) .P. h ) )
54	50, 52, 53	syl2anc 409	. . . . . . . . . . . . . . . . . . . . . . . 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 2180	. . . . . . . . . . . . . . . . . . . . . . 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 275	. . . . . . . . . . . . . . . . . . . . . 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 520	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> z e. P. )
58		simprl 521	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> w e. P. )
59	56, 57, 58, 24	caovdird 5957	. . . . . . . . . . . . . . . . . . . . 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 5790	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( w .P. v ) = 1P -> ( ( z .P. v ) +P. ( w .P. v ) ) = ( ( z .P. v ) +P. 1P ) )
61	59, 60	sylan9eq 2193	. . . . . . . . . . . . . . . . . . . 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 471	. . . . . . . . . . . . . . . . . . 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 2173	. . . . . . . . . . . . . . . . . 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 5797	. . . . . . . . . . . . . . . . 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 7404	. . . . . . . . . . . . . . . . . . . 20 |- ( ( z e. P. /\ v e. P. ) -> ( z .P. v ) e. P. )
66	57, 24, 65	syl2anc 409	. . . . . . . . . . . . . . . . . . 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 519	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> y e. P. )
69		mulclpr 7404	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( y e. P. /\ 1P e. P. ) -> ( y .P. 1P ) e. P. )
70	68, 16, 69	sylancl 410	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( y .P. 1P ) e. P. )
71		mulclpr 7404	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( z e. P. /\ 1P e. P. ) -> ( z .P. 1P ) e. P. )
72	57, 16, 71	sylancl 410	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( z .P. 1P ) e. P. )
73		addclpr 7369	. . . . . . . . . . . . . . . . . . . 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 409	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( ( y .P. 1P ) +P. ( z .P. 1P ) ) e. P. )
75		addcomprg 7410	. . . . . . . . . . . . . . . . . . . 20 |- ( ( f e. P. /\ g e. P. ) -> ( f +P. g ) = ( g +P. f ) )
76	75	adantl 275	. . . . . . . . . . . . . . . . . . 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 7411	. . . . . . . . . . . . . . . . . . . 20 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( ( f +P. g ) +P. h ) = ( f +P. ( g +P. h ) ) )
78	77	adantl 275	. . . . . . . . . . . . . . . . . . 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 5959	. . . . . . . . . . . . . . . . . 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 274	. . . . . . . . . . . . . . . . 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 2173	. . . . . . . . . . . . . . . 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 5797	. . . . . . . . . . . . . . 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 7369	. . . . . . . . . . . . . . . . . 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 409	. . . . . . . . . . . . . . . . 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 274	. . . . . . . . . . . . . . . 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 7411	. . . . . . . . . . . . . . . 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 1217	. . . . . . . . . . . . . . 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 2173	. . . . . . . . . . . . . 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 7420	. . . . . . . . . . . . . . . . . . 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 1217	. . . . . . . . . . . . . . . . . 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 5797	. . . . . . . . . . . . . . . . 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 7404	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. P. /\ v e. P. ) -> ( y .P. v ) e. P. )
94	68, 24, 93	syl2anc 409	. . . . . . . . . . . . . . . . . 18 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( y .P. v ) e. P. )
95		addassprg 7411	. . . . . . . . . . . . . . . . . 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 1217	. . . . . . . . . . . . . . . . 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 2173	. . . . . . . . . . . . . . . 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 5797	. . . . . . . . . . . . . . 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 274	. . . . . . . . . . . . . 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 7420	. . . . . . . . . . . . . . . . . . 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 1217	. . . . . . . . . . . . . . . . . 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 5798	. . . . . . . . . . . . . . . . 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 5960	. . . . . . . . . . . . . . . . 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 2173	. . . . . . . . . . . . . . . 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 5797	. . . . . . . . . . . . . . 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 274	. . . . . . . . . . . . . 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 2183	. . . . . . . . . . . . 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 410	. . . . . . . . . . . . . . . . 17 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( v +P. 1P ) e. P. )
109		mulclpr 7404	. . . . . . . . . . . . . . . . 17 |- ( ( y e. P. /\ ( v +P. 1P ) e. P. ) -> ( y .P. ( v +P. 1P ) ) e. P. )
110	68, 108, 109	syl2anc 409	. . . . . . . . . . . . . . . 16 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( y .P. ( v +P. 1P ) ) e. P. )
111		addclpr 7369	. . . . . . . . . . . . . . . 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 409	. . . . . . . . . . . . . . 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 2217	. . . . . . . . . . . . . . 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 7369	. . . . . . . . . . . . . . . . 17 |- ( ( 1P e. P. /\ 1P e. P. ) -> ( 1P +P. 1P ) e. P. )
115	16, 16, 114	mp2an 423	. . . . . . . . . . . . . . . 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 7568	. . . . . . . . . . . . . . 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 1218	. . . . . . . . . . . . . 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 274	. . . . . . . . . . . . 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 166	. . . . . . . . . . . 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 2173	. . . . . . . . . . 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 7564	. . . . . . . . . . 11 |- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
123	121, 122	eqtr4di 2191	. . . . . . . . . 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 3941	. . . . . . . . . . . 12 |- ( x = [ <. ( v +P. 1P ) , 1P >. ] ~R -> ( 0R <R x <-> 0R <R [ <. ( v +P. 1P ) , 1P >. ] ~R ) )
125		oveq2 5790	. . . . . . . . . . . . 13 |- ( x = [ <. ( v +P. 1P ) , 1P >. ] ~R -> ( [ <. y , z >. ] ~R .R x ) = ( [ <. y , z >. ] ~R .R [ <. ( v +P. 1P ) , 1P >. ] ~R ) )
126	125	eqeq1d 2149	. . . . . . . . . . . 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 465	. . . . . . . . . . 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 2793	. . . . . . . . . 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 1215	. . . . . . . . 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 363	. . . . . . . 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 398	. . . . . . 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 2552	. . . . . 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 2552	. . . 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 6524	. 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 103   <-> wb 104   /\ w3a 963   = wceq 1332   e. wcel 1481   E.wrex 2418   <.cop 3535   class class class wbr 3937  (class class class)co 5782   [cec 6435   P.cnp 7123   1Pc1p 7124   +P. cpp 7125   .P. cmp 7126   <P cltp 7127   ~R cer 7128   R.cnr 7129   0Rc0r 7130   1Rc1r 7131   .R cmr 7134   <R cltr 7135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4051  ax-sep 4054  ax-nul 4062  ax-pow 4106  ax-pr 4139  ax-un 4363  ax-setind 4460  ax-iinf 4510

This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2691  df-sbc 2914  df-csb 3008  df-dif 3078  df-un 3080  df-in 3082  df-ss 3089  df-nul 3369  df-pw 3517  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-int 3780  df-iun 3823  df-br 3938  df-opab 3998  df-mpt 3999  df-tr 4035  df-eprel 4219  df-id 4223  df-po 4226  df-iso 4227  df-iord 4296  df-on 4298  df-suc 4301  df-iom 4513  df-xp 4553  df-rel 4554  df-cnv 4555  df-co 4556  df-dm 4557  df-rn 4558  df-res 4559  df-ima 4560  df-iota 5096  df-fun 5133  df-fn 5134  df-f 5135  df-f1 5136  df-fo 5137  df-f1o 5138  df-fv 5139  df-ov 5785  df-oprab 5786  df-mpo 5787  df-1st 6046  df-2nd 6047  df-recs 6210  df-irdg 6275  df-1o 6321  df-2o 6322  df-oadd 6325  df-omul 6326  df-er 6437  df-ec 6439  df-qs 6443  df-ni 7136  df-pli 7137  df-mi 7138  df-lti 7139  df-plpq 7176  df-mpq 7177  df-enq 7179  df-nqqs 7180  df-plqqs 7181  df-mqqs 7182  df-1nqqs 7183  df-rq 7184  df-ltnqqs 7185  df-enq0 7256  df-nq0 7257  df-0nq0 7258  df-plq0 7259  df-mq0 7260  df-inp 7298  df-i1p 7299  df-iplp 7300  df-imp 7301  df-iltp 7302  df-enr 7558  df-nr 7559  df-mr 7561  df-ltr 7562  df-0r 7563  df-1r 7564

This theorem is referenced by:  recexsrlem  7606  axprecex  7712