Theorem cauappcvgprlemdisj 7459

Description: Lemma for cauappcvgpr 7470. The putative limit is disjoint. (Contributed by Jim Kingdon, 18-Jul-2020.)

Hypotheses

Ref	Expression
cauappcvgpr.f	|- ( ph -> F : Q. --> Q. )
cauappcvgpr.app	|- ( ph -> A. p e. Q. A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) )
cauappcvgpr.bnd	|- ( ph -> A. p e. Q. A <Q ( F ` p ) )
cauappcvgpr.lim	|- L = <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >.

Assertion

Ref	Expression
cauappcvgprlemdisj	|- ( ph -> A. s e. Q. -. ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) )

Distinct variable groups:   A, p   L, p, q   ph, p, q   L, s   A, s, p   F, l, u, p, q, s   ph, s

Allowed substitution hints:   ph( u, l)   A( u, q, l)   L( u, l)

Proof of Theorem cauappcvgprlemdisj

Dummy variables f g h are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cauappcvgpr.app	. . . . . . 7 |- ( ph -> A. p e. Q. A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) )
2		simpl 108	. . . . . . . . 9 |- ( ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) -> ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) )
3	2	ralimi 2495	. . . . . . . 8 |- ( A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) -> A. q e. Q. ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) )
4	3	ralimi 2495	. . . . . . 7 |- ( A. p e. Q. A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) -> A. p e. Q. A. q e. Q. ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) )
5	1, 4	syl 14	. . . . . 6 |- ( ph -> A. p e. Q. A. q e. Q. ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) )
6	5	adantr 274	. . . . 5 |- ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) -> A. p e. Q. A. q e. Q. ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) )
7		oveq1 5781	. . . . . . . . . . . . 13 |- ( l = s -> ( l +Q q ) = ( s +Q q ) )
8	7	breq1d 3939	. . . . . . . . . . . 12 |- ( l = s -> ( ( l +Q q ) <Q ( F ` q ) <-> ( s +Q q ) <Q ( F ` q ) ) )
9	8	rexbidv 2438	. . . . . . . . . . 11 |- ( l = s -> ( E. q e. Q. ( l +Q q ) <Q ( F ` q ) <-> E. q e. Q. ( s +Q q ) <Q ( F ` q ) ) )
10		cauappcvgpr.lim	. . . . . . . . . . . . 13 |- L = <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >.
11	10	fveq2i 5424	. . . . . . . . . . . 12 |- ( 1st ` L ) = ( 1st ` <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >. )
12		nqex 7171	. . . . . . . . . . . . . 14 |- Q. e. _V
13	12	rabex 4072	. . . . . . . . . . . . 13 |- { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } e. _V
14	12	rabex 4072	. . . . . . . . . . . . 13 |- { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } e. _V
15	13, 14	op1st 6044	. . . . . . . . . . . 12 |- ( 1st ` <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >. ) = { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) }
16	11, 15	eqtri 2160	. . . . . . . . . . 11 |- ( 1st ` L ) = { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) }
17	9, 16	elrab2 2843	. . . . . . . . . 10 |- ( s e. ( 1st ` L ) <-> ( s e. Q. /\ E. q e. Q. ( s +Q q ) <Q ( F ` q ) ) )
18	17	simprbi 273	. . . . . . . . 9 |- ( s e. ( 1st ` L ) -> E. q e. Q. ( s +Q q ) <Q ( F ` q ) )
19		oveq2 5782	. . . . . . . . . . 11 |- ( q = p -> ( s +Q q ) = ( s +Q p ) )
20		fveq2 5421	. . . . . . . . . . 11 |- ( q = p -> ( F ` q ) = ( F ` p ) )
21	19, 20	breq12d 3942	. . . . . . . . . 10 |- ( q = p -> ( ( s +Q q ) <Q ( F ` q ) <-> ( s +Q p ) <Q ( F ` p ) ) )
22	21	cbvrexv 2655	. . . . . . . . 9 |- ( E. q e. Q. ( s +Q q ) <Q ( F ` q ) <-> E. p e. Q. ( s +Q p ) <Q ( F ` p ) )
23	18, 22	sylib 121	. . . . . . . 8 |- ( s e. ( 1st ` L ) -> E. p e. Q. ( s +Q p ) <Q ( F ` p ) )
24		breq2 3933	. . . . . . . . . . 11 |- ( u = s -> ( ( ( F ` q ) +Q q ) <Q u <-> ( ( F ` q ) +Q q ) <Q s ) )
25	24	rexbidv 2438	. . . . . . . . . 10 |- ( u = s -> ( E. q e. Q. ( ( F ` q ) +Q q ) <Q u <-> E. q e. Q. ( ( F ` q ) +Q q ) <Q s ) )
26	10	fveq2i 5424	. . . . . . . . . . 11 |- ( 2nd ` L ) = ( 2nd ` <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >. )
27	13, 14	op2nd 6045	. . . . . . . . . . 11 |- ( 2nd ` <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >. ) = { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u }
28	26, 27	eqtri 2160	. . . . . . . . . 10 |- ( 2nd ` L ) = { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u }
29	25, 28	elrab2 2843	. . . . . . . . 9 |- ( s e. ( 2nd ` L ) <-> ( s e. Q. /\ E. q e. Q. ( ( F ` q ) +Q q ) <Q s ) )
30	29	simprbi 273	. . . . . . . 8 |- ( s e. ( 2nd ` L ) -> E. q e. Q. ( ( F ` q ) +Q q ) <Q s )
31	23, 30	anim12i 336	. . . . . . 7 |- ( ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) -> ( E. p e. Q. ( s +Q p ) <Q ( F ` p ) /\ E. q e. Q. ( ( F ` q ) +Q q ) <Q s ) )
32		reeanv 2600	. . . . . . 7 |- ( E. p e. Q. E. q e. Q. ( ( s +Q p ) <Q ( F ` p ) /\ ( ( F ` q ) +Q q ) <Q s ) <-> ( E. p e. Q. ( s +Q p ) <Q ( F ` p ) /\ E. q e. Q. ( ( F ` q ) +Q q ) <Q s ) )
33	31, 32	sylibr 133	. . . . . 6 |- ( ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) -> E. p e. Q. E. q e. Q. ( ( s +Q p ) <Q ( F ` p ) /\ ( ( F ` q ) +Q q ) <Q s ) )
34	33	adantl 275	. . . . 5 |- ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) -> E. p e. Q. E. q e. Q. ( ( s +Q p ) <Q ( F ` p ) /\ ( ( F ` q ) +Q q ) <Q s ) )
35	6, 34	r19.29d2r 2576	. . . 4 |- ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) -> E. p e. Q. E. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( ( s +Q p ) <Q ( F ` p ) /\ ( ( F ` q ) +Q q ) <Q s ) ) )
36		simprl 520	. . . . . . . . . . . 12 |- ( ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( ( s +Q p ) <Q ( F ` p ) /\ ( ( F ` q ) +Q q ) <Q s ) ) -> ( s +Q p ) <Q ( F ` p ) )
37		simpl 108	. . . . . . . . . . . 12 |- ( ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( ( s +Q p ) <Q ( F ` p ) /\ ( ( F ` q ) +Q q ) <Q s ) ) -> ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) )
38	36, 37	jca 304	. . . . . . . . . . 11 |- ( ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( ( s +Q p ) <Q ( F ` p ) /\ ( ( F ` q ) +Q q ) <Q s ) ) -> ( ( s +Q p ) <Q ( F ` p ) /\ ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) ) )
39	17	simplbi 272	. . . . . . . . . . . . . . 15 |- ( s e. ( 1st ` L ) -> s e. Q. )
40	39	adantr 274	. . . . . . . . . . . . . 14 |- ( ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) -> s e. Q. )
41	40	ad3antlr 484	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> s e. Q. )
42		simplr 519	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> p e. Q. )
43		addclnq 7183	. . . . . . . . . . . . 13 |- ( ( s e. Q. /\ p e. Q. ) -> ( s +Q p ) e. Q. )
44	41, 42, 43	syl2anc 408	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( s +Q p ) e. Q. )
45		cauappcvgpr.f	. . . . . . . . . . . . . 14 |- ( ph -> F : Q. --> Q. )
46	45	ad3antrrr 483	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> F : Q. --> Q. )
47	46, 42	ffvelrnd 5556	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( F ` p ) e. Q. )
48		simpr 109	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> q e. Q. )
49	46, 48	ffvelrnd 5556	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( F ` q ) e. Q. )
50		addclnq 7183	. . . . . . . . . . . . . 14 |- ( ( p e. Q. /\ q e. Q. ) -> ( p +Q q ) e. Q. )
51	42, 48, 50	syl2anc 408	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( p +Q q ) e. Q. )
52		addclnq 7183	. . . . . . . . . . . . 13 |- ( ( ( F ` q ) e. Q. /\ ( p +Q q ) e. Q. ) -> ( ( F ` q ) +Q ( p +Q q ) ) e. Q. )
53	49, 51, 52	syl2anc 408	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( ( F ` q ) +Q ( p +Q q ) ) e. Q. )
54		ltsonq 7206	. . . . . . . . . . . . 13 |- <Q Or Q.
55		sotr 4240	. . . . . . . . . . . . 13 |- ( ( <Q Or Q. /\ ( ( s +Q p ) e. Q. /\ ( F ` p ) e. Q. /\ ( ( F ` q ) +Q ( p +Q q ) ) e. Q. ) ) -> ( ( ( s +Q p ) <Q ( F ` p ) /\ ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) ) -> ( s +Q p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) ) )
56	54, 55	mpan 420	. . . . . . . . . . . 12 |- ( ( ( s +Q p ) e. Q. /\ ( F ` p ) e. Q. /\ ( ( F ` q ) +Q ( p +Q q ) ) e. Q. ) -> ( ( ( s +Q p ) <Q ( F ` p ) /\ ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) ) -> ( s +Q p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) ) )
57	44, 47, 53, 56	syl3anc 1216	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( ( ( s +Q p ) <Q ( F ` p ) /\ ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) ) -> ( s +Q p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) ) )
58	38, 57	syl5 32	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( ( s +Q p ) <Q ( F ` p ) /\ ( ( F ` q ) +Q q ) <Q s ) ) -> ( s +Q p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) ) )
59		simprr 521	. . . . . . . . . . 11 |- ( ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( ( s +Q p ) <Q ( F ` p ) /\ ( ( F ` q ) +Q q ) <Q s ) ) -> ( ( F ` q ) +Q q ) <Q s )
60	59	a1i 9	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( ( s +Q p ) <Q ( F ` p ) /\ ( ( F ` q ) +Q q ) <Q s ) ) -> ( ( F ` q ) +Q q ) <Q s ) )
61	58, 60	jcad 305	. . . . . . . . 9 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( ( s +Q p ) <Q ( F ` p ) /\ ( ( F ` q ) +Q q ) <Q s ) ) -> ( ( s +Q p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( ( F ` q ) +Q q ) <Q s ) ) )
62		addcomnqg 7189	. . . . . . . . . . . 12 |- ( ( s e. Q. /\ p e. Q. ) -> ( s +Q p ) = ( p +Q s ) )
63	41, 42, 62	syl2anc 408	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( s +Q p ) = ( p +Q s ) )
64		addcomnqg 7189	. . . . . . . . . . . . 13 |- ( ( f e. Q. /\ g e. Q. ) -> ( f +Q g ) = ( g +Q f ) )
65	64	adantl 275	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) /\ ( f e. Q. /\ g e. Q. ) ) -> ( f +Q g ) = ( g +Q f ) )
66		addassnqg 7190	. . . . . . . . . . . . 13 |- ( ( f e. Q. /\ g e. Q. /\ h e. Q. ) -> ( ( f +Q g ) +Q h ) = ( f +Q ( g +Q h ) ) )
67	66	adantl 275	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) /\ ( f e. Q. /\ g e. Q. /\ h e. Q. ) ) -> ( ( f +Q g ) +Q h ) = ( f +Q ( g +Q h ) ) )
68	49, 42, 48, 65, 67	caov12d 5952	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( ( F ` q ) +Q ( p +Q q ) ) = ( p +Q ( ( F ` q ) +Q q ) ) )
69	63, 68	breq12d 3942	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( ( s +Q p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) <-> ( p +Q s ) <Q ( p +Q ( ( F ` q ) +Q q ) ) ) )
70	69	anbi1d 460	. . . . . . . . 9 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( ( ( s +Q p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( ( F ` q ) +Q q ) <Q s ) <-> ( ( p +Q s ) <Q ( p +Q ( ( F ` q ) +Q q ) ) /\ ( ( F ` q ) +Q q ) <Q s ) ) )
71	61, 70	sylibd 148	. . . . . . . 8 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( ( s +Q p ) <Q ( F ` p ) /\ ( ( F ` q ) +Q q ) <Q s ) ) -> ( ( p +Q s ) <Q ( p +Q ( ( F ` q ) +Q q ) ) /\ ( ( F ` q ) +Q q ) <Q s ) ) )
72		addclnq 7183	. . . . . . . . . . 11 |- ( ( ( F ` q ) e. Q. /\ q e. Q. ) -> ( ( F ` q ) +Q q ) e. Q. )
73	49, 48, 72	syl2anc 408	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( ( F ` q ) +Q q ) e. Q. )
74		ltanqg 7208	. . . . . . . . . 10 |- ( ( s e. Q. /\ ( ( F ` q ) +Q q ) e. Q. /\ p e. Q. ) -> ( s <Q ( ( F ` q ) +Q q ) <-> ( p +Q s ) <Q ( p +Q ( ( F ` q ) +Q q ) ) ) )
75	41, 73, 42, 74	syl3anc 1216	. . . . . . . . 9 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( s <Q ( ( F ` q ) +Q q ) <-> ( p +Q s ) <Q ( p +Q ( ( F ` q ) +Q q ) ) ) )
76	75	anbi1d 460	. . . . . . . 8 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( ( s <Q ( ( F ` q ) +Q q ) /\ ( ( F ` q ) +Q q ) <Q s ) <-> ( ( p +Q s ) <Q ( p +Q ( ( F ` q ) +Q q ) ) /\ ( ( F ` q ) +Q q ) <Q s ) ) )
77	71, 76	sylibrd 168	. . . . . . 7 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( ( s +Q p ) <Q ( F ` p ) /\ ( ( F ` q ) +Q q ) <Q s ) ) -> ( s <Q ( ( F ` q ) +Q q ) /\ ( ( F ` q ) +Q q ) <Q s ) ) )
78		so2nr 4243	. . . . . . . . . 10 |- ( ( <Q Or Q. /\ ( s e. Q. /\ ( ( F ` q ) +Q q ) e. Q. ) ) -> -. ( s <Q ( ( F ` q ) +Q q ) /\ ( ( F ` q ) +Q q ) <Q s ) )
79	54, 78	mpan 420	. . . . . . . . 9 |- ( ( s e. Q. /\ ( ( F ` q ) +Q q ) e. Q. ) -> -. ( s <Q ( ( F ` q ) +Q q ) /\ ( ( F ` q ) +Q q ) <Q s ) )
80	41, 73, 79	syl2anc 408	. . . . . . . 8 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> -. ( s <Q ( ( F ` q ) +Q q ) /\ ( ( F ` q ) +Q q ) <Q s ) )
81	80	pm2.21d 608	. . . . . . 7 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( ( s <Q ( ( F ` q ) +Q q ) /\ ( ( F ` q ) +Q q ) <Q s ) -> F. ) )
82	77, 81	syld 45	. . . . . 6 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( ( s +Q p ) <Q ( F ` p ) /\ ( ( F ` q ) +Q q ) <Q s ) ) -> F. ) )
83	82	rexlimdva 2549	. . . . 5 |- ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) -> ( E. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( ( s +Q p ) <Q ( F ` p ) /\ ( ( F ` q ) +Q q ) <Q s ) ) -> F. ) )
84	83	rexlimdva 2549	. . . 4 |- ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) -> ( E. p e. Q. E. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( ( s +Q p ) <Q ( F ` p ) /\ ( ( F ` q ) +Q q ) <Q s ) ) -> F. ) )
85	35, 84	mpd 13	. . 3 |- ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) -> F. )
86	85	inegd 1350	. 2 |- ( ph -> -. ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) )
87	86	ralrimivw 2506	1 |- ( ph -> A. s e. Q. -. ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104   /\ w3a 962   = wceq 1331   F. wfal 1336   e. wcel 1480   A.wral 2416   E.wrex 2417   {crab 2420   <.cop 3530   class class class wbr 3929   Or wor 4217   -->wf 5119   ` cfv 5123  (class class class)co 5774   1stc1st 6036   2ndc2nd 6037   Q.cnq 7088   +Q cplq 7090   <Q cltq 7093

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-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-enq 7155  df-nqqs 7156  df-plqqs 7157  df-ltnqqs 7161

This theorem is referenced by:  cauappcvgprlemcl  7461