Theorem cauappcvgprlemdisj 7826

Description: Lemma for cauappcvgpr 7837. 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 109	. . . . . . . . 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 2593	. . . . . . . 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 2593	. . . . . . 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 276	. . . . 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 6001	. . . . . . . . . . . . 13 |- ( l = s -> ( l +Q q ) = ( s +Q q ) )
8	7	breq1d 4092	. . . . . . . . . . . 12 |- ( l = s -> ( ( l +Q q ) <Q ( F ` q ) <-> ( s +Q q ) <Q ( F ` q ) ) )
9	8	rexbidv 2531	. . . . . . . . . . 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 5626	. . . . . . . . . . . 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 7538	. . . . . . . . . . . . . 14 |- Q. e. _V
13	12	rabex 4227	. . . . . . . . . . . . 13 |- { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } e. _V
14	12	rabex 4227	. . . . . . . . . . . . 13 |- { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } e. _V
15	13, 14	op1st 6282	. . . . . . . . . . . 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 2250	. . . . . . . . . . 11 |- ( 1st ` L ) = { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) }
17	9, 16	elrab2 2962	. . . . . . . . . 10 |- ( s e. ( 1st ` L ) <-> ( s e. Q. /\ E. q e. Q. ( s +Q q ) <Q ( F ` q ) ) )
18	17	simprbi 275	. . . . . . . . 9 |- ( s e. ( 1st ` L ) -> E. q e. Q. ( s +Q q ) <Q ( F ` q ) )
19		oveq2 6002	. . . . . . . . . . 11 |- ( q = p -> ( s +Q q ) = ( s +Q p ) )
20		fveq2 5623	. . . . . . . . . . 11 |- ( q = p -> ( F ` q ) = ( F ` p ) )
21	19, 20	breq12d 4095	. . . . . . . . . 10 |- ( q = p -> ( ( s +Q q ) <Q ( F ` q ) <-> ( s +Q p ) <Q ( F ` p ) ) )
22	21	cbvrexv 2766	. . . . . . . . 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 122	. . . . . . . 8 |- ( s e. ( 1st ` L ) -> E. p e. Q. ( s +Q p ) <Q ( F ` p ) )
24		breq2 4086	. . . . . . . . . . 11 |- ( u = s -> ( ( ( F ` q ) +Q q ) <Q u <-> ( ( F ` q ) +Q q ) <Q s ) )
25	24	rexbidv 2531	. . . . . . . . . 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 5626	. . . . . . . . . . 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 6283	. . . . . . . . . . 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 2250	. . . . . . . . . 10 |- ( 2nd ` L ) = { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u }
29	25, 28	elrab2 2962	. . . . . . . . 9 |- ( s e. ( 2nd ` L ) <-> ( s e. Q. /\ E. q e. Q. ( ( F ` q ) +Q q ) <Q s ) )
30	29	simprbi 275	. . . . . . . 8 |- ( s e. ( 2nd ` L ) -> E. q e. Q. ( ( F ` q ) +Q q ) <Q s )
31	23, 30	anim12i 338	. . . . . . 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 2701	. . . . . . 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 134	. . . . . 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 277	. . . . 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 2675	. . . 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 529	. . . . . . . . . . . 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 109	. . . . . . . . . . . 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 306	. . . . . . . . . . 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 274	. . . . . . . . . . . . . . 15 |- ( s e. ( 1st ` L ) -> s e. Q. )
40	39	adantr 276	. . . . . . . . . . . . . 14 |- ( ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) -> s e. Q. )
41	40	ad3antlr 493	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> s e. Q. )
42		simplr 528	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> p e. Q. )
43		addclnq 7550	. . . . . . . . . . . . 13 |- ( ( s e. Q. /\ p e. Q. ) -> ( s +Q p ) e. Q. )
44	41, 42, 43	syl2anc 411	. . . . . . . . . . . 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 492	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> F : Q. --> Q. )
47	46, 42	ffvelcdmd 5764	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( F ` p ) e. Q. )
48		simpr 110	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> q e. Q. )
49	46, 48	ffvelcdmd 5764	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( F ` q ) e. Q. )
50		addclnq 7550	. . . . . . . . . . . . . 14 |- ( ( p e. Q. /\ q e. Q. ) -> ( p +Q q ) e. Q. )
51	42, 48, 50	syl2anc 411	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( p +Q q ) e. Q. )
52		addclnq 7550	. . . . . . . . . . . . 13 |- ( ( ( F ` q ) e. Q. /\ ( p +Q q ) e. Q. ) -> ( ( F ` q ) +Q ( p +Q q ) ) e. Q. )
53	49, 51, 52	syl2anc 411	. . . . . . . . . . . 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 7573	. . . . . . . . . . . . 13 |- <Q Or Q.
55		sotr 4406	. . . . . . . . . . . . 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 424	. . . . . . . . . . . 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 1271	. . . . . . . . . . 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 531	. . . . . . . . . . 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 307	. . . . . . . . 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 7556	. . . . . . . . . . . 12 |- ( ( s e. Q. /\ p e. Q. ) -> ( s +Q p ) = ( p +Q s ) )
63	41, 42, 62	syl2anc 411	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( s +Q p ) = ( p +Q s ) )
64		addcomnqg 7556	. . . . . . . . . . . . 13 |- ( ( f e. Q. /\ g e. Q. ) -> ( f +Q g ) = ( g +Q f ) )
65	64	adantl 277	. . . . . . . . . . . 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 7557	. . . . . . . . . . . . 13 |- ( ( f e. Q. /\ g e. Q. /\ h e. Q. ) -> ( ( f +Q g ) +Q h ) = ( f +Q ( g +Q h ) ) )
67	66	adantl 277	. . . . . . . . . . . 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 6178	. . . . . . . . . . 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 4095	. . . . . . . . . 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 465	. . . . . . . . 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 149	. . . . . . . 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 7550	. . . . . . . . . . 11 |- ( ( ( F ` q ) e. Q. /\ q e. Q. ) -> ( ( F ` q ) +Q q ) e. Q. )
73	49, 48, 72	syl2anc 411	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( ( F ` q ) +Q q ) e. Q. )
74		ltanqg 7575	. . . . . . . . . 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 1271	. . . . . . . . 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 465	. . . . . . . 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 169	. . . . . . 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 4409	. . . . . . . . . 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 424	. . . . . . . . 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 411	. . . . . . . 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 622	. . . . . . 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 2648	. . . . 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 2648	. . . 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 1414	. 2 |- ( ph -> -. ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) )
87	86	ralrimivw 2604	1 |- ( ph -> A. s e. Q. -. ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 1002   = wceq 1395   F. wfal 1400   e. wcel 2200   A.wral 2508   E.wrex 2509   {crab 2512   <.cop 3669   class class class wbr 4082   Or wor 4383   -->wf 5310   ` cfv 5314  (class class class)co 5994   1stc1st 6274   2ndc2nd 6275   Q.cnq 7455   +Q cplq 7457   <Q cltq 7460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-coll 4198  ax-sep 4201  ax-nul 4209  ax-pow 4257  ax-pr 4292  ax-un 4521  ax-setind 4626  ax-iinf 4677

This theorem depends on definitions:  df-bi 117  df-dc 840  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2801  df-sbc 3029  df-csb 3125  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-nul 3492  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-int 3923  df-iun 3966  df-br 4083  df-opab 4145  df-mpt 4146  df-tr 4182  df-eprel 4377  df-id 4381  df-po 4384  df-iso 4385  df-iord 4454  df-on 4456  df-suc 4459  df-iom 4680  df-xp 4722  df-rel 4723  df-cnv 4724  df-co 4725  df-dm 4726  df-rn 4727  df-res 4728  df-ima 4729  df-iota 5274  df-fun 5316  df-fn 5317  df-f 5318  df-f1 5319  df-fo 5320  df-f1o 5321  df-fv 5322  df-ov 5997  df-oprab 5998  df-mpo 5999  df-1st 6276  df-2nd 6277  df-recs 6441  df-irdg 6506  df-oadd 6556  df-omul 6557  df-er 6670  df-ec 6672  df-qs 6676  df-ni 7479  df-pli 7480  df-mi 7481  df-lti 7482  df-plpq 7519  df-enq 7522  df-nqqs 7523  df-plqqs 7524  df-ltnqqs 7528

This theorem is referenced by:  cauappcvgprlemcl  7828