Theorem recexgt0sr 7581

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 7546	. . . 4 |- <R C_ ( R. X. R. )
2	1	brel 4591	. . 3 |- ( 0R <R A -> ( 0R e. R. /\ A e. R. ) )
3	2	simprd 113	. 2 |- ( 0R <R A -> A e. R. )
4		df-nr 7535	. . 3 |- R. = ( ( P. X. P. ) /. ~R )
5		breq2 3933	. . . 4 |- ( [ <. y , z >. ] ~R = A -> ( 0R <R [ <. y , z >. ] ~R <-> 0R <R A ) )
6		oveq1 5781	. . . . . . 7 |- ( [ <. y , z >. ] ~R = A -> ( [ <. y , z >. ] ~R .R x ) = ( A .R x ) )
7	6	eqeq1d 2148	. . . . . 6 |- ( [ <. y , z >. ] ~R = A -> ( ( [ <. y , z >. ] ~R .R x ) = 1R <-> ( A .R x ) = 1R ) )
8	7	anbi2d 459	. . . . 5 |- ( [ <. y , z >. ] ~R = A -> ( ( 0R <R x /\ ( [ <. y , z >. ] ~R .R x ) = 1R ) <-> ( 0R <R x /\ ( A .R x ) = 1R ) ) )
9	8	rexbidv 2438	. . . 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 7556	. . . . 5 |- ( 0R <R [ <. y , z >. ] ~R <-> z <P y )
12		ltexpri 7421	. . . . 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 7446	. . . . . . 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 7362	. . . . . . . . . . . . . 14 |- 1P e. P.
17		addclpr 7345	. . . . . . . . . . . . . 14 |- ( ( v e. P. /\ 1P e. P. ) -> ( v +P. 1P ) e. P. )
18	16, 17	mpan2 421	. . . . . . . . . . . . 13 |- ( v e. P. -> ( v +P. 1P ) e. P. )
19		enrex 7545	. . . . . . . . . . . . . 14 |- ~R e. _V
20	19, 4	ecopqsi 6484	. . . . . . . . . . . . 13 |- ( ( ( v +P. 1P ) e. P. /\ 1P e. P. ) -> [ <. ( v +P. 1P ) , 1P >. ] ~R e. R. )
21	18, 16, 20	sylancl 409	. . . . . . . . . . . 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 480	. . . . . . . . . 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 521	. . . . . . . . . . . 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 7405	. . . . . . . . . . . . . 14 |- ( ( 1P e. P. /\ v e. P. ) -> 1P <P ( 1P +P. v ) )
27	16, 26	mpan 420	. . . . . . . . . . . . 13 |- ( v e. P. -> 1P <P ( 1P +P. v ) )
28		addcomprg 7386	. . . . . . . . . . . . . 14 |- ( ( 1P e. P. /\ v e. P. ) -> ( 1P +P. v ) = ( v +P. 1P ) )
29	16, 28	mpan 420	. . . . . . . . . . . . 13 |- ( v e. P. -> ( 1P +P. v ) = ( v +P. 1P ) )
30	27, 29	breqtrd 3954	. . . . . . . . . . . 12 |- ( v e. P. -> 1P <P ( v +P. 1P ) )
31		gt0srpr 7556	. . . . . . . . . . . 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 339	. . . . . . . . . . . . . . 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 7554	. . . . . . . . . . . . . 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 473	. . . . . . . . . . . 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 5781	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( z +P. w ) = y -> ( ( z +P. w ) .P. v ) = ( y .P. v ) )
41	40	eqcomd 2145	. . . . . . . . . . . . . . . . . . . 20 |- ( ( z +P. w ) = y -> ( y .P. v ) = ( ( z +P. w ) .P. v ) )
42	41	ad2antll 482	. . . . . . . . . . . . . . . . . . 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 7388	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( f e. P. /\ h e. P. ) -> ( f .P. h ) = ( h .P. f ) )
44	43	3adant2 1000	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( f .P. h ) = ( h .P. f ) )
45		mulcomprg 7388	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( g e. P. /\ h e. P. ) -> ( g .P. h ) = ( h .P. g ) )
46	45	3adant1 999	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( g .P. h ) = ( h .P. g ) )
47	44, 46	oveq12d 5792	. . . . . . . . . . . . . . . . . . . . . . . 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 7396	. . . . . . . . . . . . . . . . . . . . . . . . 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 1188	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( h .P. ( f +P. g ) ) = ( ( h .P. f ) +P. ( h .P. g ) ) )
50		simp3 983	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> h e. P. )
51		addclpr 7345	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( f e. P. /\ g e. P. ) -> ( f +P. g ) e. P. )
52	51	3adant3 1001	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f e. P. /\ g e. P. /\ h e. P. ) -> ( f +P. g ) e. P. )
53		mulcomprg 7388	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( h e. P. /\ ( f +P. g ) e. P. ) -> ( h .P. ( f +P. g ) ) = ( ( f +P. g ) .P. h ) )
54	50, 52, 53	syl2anc 408	. . . . . . . . . . . . . . . . . . . . . . . 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 2179	. . . . . . . . . . . . . . . . . . . . . . 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 519	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> z e. P. )
58		simprl 520	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> w e. P. )
59	56, 57, 58, 24	caovdird 5949	. . . . . . . . . . . . . . . . . . . . 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 5782	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( w .P. v ) = 1P -> ( ( z .P. v ) +P. ( w .P. v ) ) = ( ( z .P. v ) +P. 1P ) )
61	59, 60	sylan9eq 2192	. . . . . . . . . . . . . . . . . . . 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 470	. . . . . . . . . . . . . . . . . . 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 2172	. . . . . . . . . . . . . . . . . 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 5789	. . . . . . . . . . . . . . . . 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 7380	. . . . . . . . . . . . . . . . . . . 20 |- ( ( z e. P. /\ v e. P. ) -> ( z .P. v ) e. P. )
66	57, 24, 65	syl2anc 408	. . . . . . . . . . . . . . . . . . 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 518	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> y e. P. )
69		mulclpr 7380	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( y e. P. /\ 1P e. P. ) -> ( y .P. 1P ) e. P. )
70	68, 16, 69	sylancl 409	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( y .P. 1P ) e. P. )
71		mulclpr 7380	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( z e. P. /\ 1P e. P. ) -> ( z .P. 1P ) e. P. )
72	57, 16, 71	sylancl 409	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( z .P. 1P ) e. P. )
73		addclpr 7345	. . . . . . . . . . . . . . . . . . . 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 408	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( ( y .P. 1P ) +P. ( z .P. 1P ) ) e. P. )
75		addcomprg 7386	. . . . . . . . . . . . . . . . . . . 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 7387	. . . . . . . . . . . . . . . . . . . 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 5951	. . . . . . . . . . . . . . . . . 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 2172	. . . . . . . . . . . . . . . 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 5789	. . . . . . . . . . . . . . 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 7345	. . . . . . . . . . . . . . . . . 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 408	. . . . . . . . . . . . . . . . 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 7387	. . . . . . . . . . . . . . . 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 1216	. . . . . . . . . . . . . . 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 2172	. . . . . . . . . . . . . 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 7396	. . . . . . . . . . . . . . . . . . 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 1216	. . . . . . . . . . . . . . . . . 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 5789	. . . . . . . . . . . . . . . . 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 7380	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. P. /\ v e. P. ) -> ( y .P. v ) e. P. )
94	68, 24, 93	syl2anc 408	. . . . . . . . . . . . . . . . . 18 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( y .P. v ) e. P. )
95		addassprg 7387	. . . . . . . . . . . . . . . . . 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 1216	. . . . . . . . . . . . . . . . 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 2172	. . . . . . . . . . . . . . . 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 5789	. . . . . . . . . . . . . . 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 7396	. . . . . . . . . . . . . . . . . . 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 1216	. . . . . . . . . . . . . . . . . 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 5790	. . . . . . . . . . . . . . . . 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 5952	. . . . . . . . . . . . . . . . 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 2172	. . . . . . . . . . . . . . . 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 5789	. . . . . . . . . . . . . . 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 2182	. . . . . . . . . . . . 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 409	. . . . . . . . . . . . . . . . 17 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( v +P. 1P ) e. P. )
109		mulclpr 7380	. . . . . . . . . . . . . . . . 17 |- ( ( y e. P. /\ ( v +P. 1P ) e. P. ) -> ( y .P. ( v +P. 1P ) ) e. P. )
110	68, 108, 109	syl2anc 408	. . . . . . . . . . . . . . . 16 |- ( ( ( y e. P. /\ z e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( y .P. ( v +P. 1P ) ) e. P. )
111		addclpr 7345	. . . . . . . . . . . . . . . 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 408	. . . . . . . . . . . . . . 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 2216	. . . . . . . . . . . . . . 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 7345	. . . . . . . . . . . . . . . . 17 |- ( ( 1P e. P. /\ 1P e. P. ) -> ( 1P +P. 1P ) e. P. )
115	16, 16, 114	mp2an 422	. . . . . . . . . . . . . . . 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 7544	. . . . . . . . . . . . . . 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 1217	. . . . . . . . . . . . . 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 2172	. . . . . . . . . . 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 7540	. . . . . . . . . . 11 |- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
123	121, 122	syl6eqr 2190	. . . . . . . . . 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 3933	. . . . . . . . . . . 12 |- ( x = [ <. ( v +P. 1P ) , 1P >. ] ~R -> ( 0R <R x <-> 0R <R [ <. ( v +P. 1P ) , 1P >. ] ~R ) )
125		oveq2 5782	. . . . . . . . . . . . 13 |- ( x = [ <. ( v +P. 1P ) , 1P >. ] ~R -> ( [ <. y , z >. ] ~R .R x ) = ( [ <. y , z >. ] ~R .R [ <. ( v +P. 1P ) , 1P >. ] ~R ) )
126	125	eqeq1d 2148	. . . . . . . . . . . 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 464	. . . . . . . . . . 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 2789	. . . . . . . . . 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 1214	. . . . . . . . 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 362	. . . . . . . 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 397	. . . . . . 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 2549	. . . . . 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 2549	. . . 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 6516	. 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 962   = wceq 1331   e. wcel 1480   E.wrex 2417   <.cop 3530   class class class wbr 3929  (class class class)co 5774   [cec 6427   P.cnp 7099   1Pc1p 7100   +P. cpp 7101   .P. cmp 7102   <P cltp 7103   ~R cer 7104   R.cnr 7105   0Rc0r 7106   1Rc1r 7107   .R cmr 7110   <R cltr 7111

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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502

This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-eprel 4211  df-id 4215  df-po 4218  df-iso 4219  df-iord 4288  df-on 4290  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-irdg 6267  df-1o 6313  df-2o 6314  df-oadd 6317  df-omul 6318  df-er 6429  df-ec 6431  df-qs 6435  df-ni 7112  df-pli 7113  df-mi 7114  df-lti 7115  df-plpq 7152  df-mpq 7153  df-enq 7155  df-nqqs 7156  df-plqqs 7157  df-mqqs 7158  df-1nqqs 7159  df-rq 7160  df-ltnqqs 7161  df-enq0 7232  df-nq0 7233  df-0nq0 7234  df-plq0 7235  df-mq0 7236  df-inp 7274  df-i1p 7275  df-iplp 7276  df-imp 7277  df-iltp 7278  df-enr 7534  df-nr 7535  df-mr 7537  df-ltr 7538  df-0r 7539  df-1r 7540

This theorem is referenced by:  recexsrlem  7582  axprecex  7688