Theorem cauappcvgprlemdisj 7189

Description: Lemma for cauappcvgpr 7200. 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 107	. . . . . . . . 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 2438	. . . . . . . 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 2438	. . . . . . 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 270	. . . . 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 5641	. . . . . . . . . . . . 13 |- ( l = s -> ( l +Q q ) = ( s +Q q ) )
8	7	breq1d 3847	. . . . . . . . . . . 12 |- ( l = s -> ( ( l +Q q ) <Q ( F ` q ) <-> ( s +Q q ) <Q ( F ` q ) ) )
9	8	rexbidv 2381	. . . . . . . . . . 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 5292	. . . . . . . . . . . 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 6901	. . . . . . . . . . . . . 14 |- Q. e. _V
13	12	rabex 3975	. . . . . . . . . . . . 13 |- { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } e. _V
14	12	rabex 3975	. . . . . . . . . . . . 13 |- { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } e. _V
15	13, 14	op1st 5899	. . . . . . . . . . . 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 2108	. . . . . . . . . . 11 |- ( 1st ` L ) = { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) }
17	9, 16	elrab2 2772	. . . . . . . . . 10 |- ( s e. ( 1st ` L ) <-> ( s e. Q. /\ E. q e. Q. ( s +Q q ) <Q ( F ` q ) ) )
18	17	simprbi 269	. . . . . . . . 9 |- ( s e. ( 1st ` L ) -> E. q e. Q. ( s +Q q ) <Q ( F ` q ) )
19		oveq2 5642	. . . . . . . . . . 11 |- ( q = p -> ( s +Q q ) = ( s +Q p ) )
20		fveq2 5289	. . . . . . . . . . 11 |- ( q = p -> ( F ` q ) = ( F ` p ) )
21	19, 20	breq12d 3850	. . . . . . . . . 10 |- ( q = p -> ( ( s +Q q ) <Q ( F ` q ) <-> ( s +Q p ) <Q ( F ` p ) ) )
22	21	cbvrexv 2591	. . . . . . . . 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 120	. . . . . . . 8 |- ( s e. ( 1st ` L ) -> E. p e. Q. ( s +Q p ) <Q ( F ` p ) )
24		breq2 3841	. . . . . . . . . . 11 |- ( u = s -> ( ( ( F ` q ) +Q q ) <Q u <-> ( ( F ` q ) +Q q ) <Q s ) )
25	24	rexbidv 2381	. . . . . . . . . 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 5292	. . . . . . . . . . 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 5900	. . . . . . . . . . 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 2108	. . . . . . . . . 10 |- ( 2nd ` L ) = { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u }
29	25, 28	elrab2 2772	. . . . . . . . 9 |- ( s e. ( 2nd ` L ) <-> ( s e. Q. /\ E. q e. Q. ( ( F ` q ) +Q q ) <Q s ) )
30	29	simprbi 269	. . . . . . . 8 |- ( s e. ( 2nd ` L ) -> E. q e. Q. ( ( F ` q ) +Q q ) <Q s )
31	23, 30	anim12i 331	. . . . . . 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 2536	. . . . . . 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 132	. . . . . 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 271	. . . . 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 2512	. . . 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 498	. . . . . . . . . . . 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 107	. . . . . . . . . . . 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 300	. . . . . . . . . . 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 268	. . . . . . . . . . . . . . 15 |- ( s e. ( 1st ` L ) -> s e. Q. )
40	39	adantr 270	. . . . . . . . . . . . . 14 |- ( ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) -> s e. Q. )
41	40	ad3antlr 477	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> s e. Q. )
42		simplr 497	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> p e. Q. )
43		addclnq 6913	. . . . . . . . . . . . 13 |- ( ( s e. Q. /\ p e. Q. ) -> ( s +Q p ) e. Q. )
44	41, 42, 43	syl2anc 403	. . . . . . . . . . . 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 476	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> F : Q. --> Q. )
47	46, 42	ffvelrnd 5419	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( F ` p ) e. Q. )
48		simpr 108	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> q e. Q. )
49	46, 48	ffvelrnd 5419	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( F ` q ) e. Q. )
50		addclnq 6913	. . . . . . . . . . . . . 14 |- ( ( p e. Q. /\ q e. Q. ) -> ( p +Q q ) e. Q. )
51	42, 48, 50	syl2anc 403	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( p +Q q ) e. Q. )
52		addclnq 6913	. . . . . . . . . . . . 13 |- ( ( ( F ` q ) e. Q. /\ ( p +Q q ) e. Q. ) -> ( ( F ` q ) +Q ( p +Q q ) ) e. Q. )
53	49, 51, 52	syl2anc 403	. . . . . . . . . . . 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 6936	. . . . . . . . . . . . 13 |- <Q Or Q.
55		sotr 4136	. . . . . . . . . . . . 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 415	. . . . . . . . . . . 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 1174	. . . . . . . . . . 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 499	. . . . . . . . . . 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 301	. . . . . . . . 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 6919	. . . . . . . . . . . 12 |- ( ( s e. Q. /\ p e. Q. ) -> ( s +Q p ) = ( p +Q s ) )
63	41, 42, 62	syl2anc 403	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( s +Q p ) = ( p +Q s ) )
64		addcomnqg 6919	. . . . . . . . . . . . 13 |- ( ( f e. Q. /\ g e. Q. ) -> ( f +Q g ) = ( g +Q f ) )
65	64	adantl 271	. . . . . . . . . . . 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 6920	. . . . . . . . . . . . 13 |- ( ( f e. Q. /\ g e. Q. /\ h e. Q. ) -> ( ( f +Q g ) +Q h ) = ( f +Q ( g +Q h ) ) )
67	66	adantl 271	. . . . . . . . . . . 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 5808	. . . . . . . . . . 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 3850	. . . . . . . . . 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 453	. . . . . . . . 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 147	. . . . . . . 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 6913	. . . . . . . . . . 11 |- ( ( ( F ` q ) e. Q. /\ q e. Q. ) -> ( ( F ` q ) +Q q ) e. Q. )
73	49, 48, 72	syl2anc 403	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) ) /\ p e. Q. ) /\ q e. Q. ) -> ( ( F ` q ) +Q q ) e. Q. )
74		ltanqg 6938	. . . . . . . . . 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 1174	. . . . . . . . 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 453	. . . . . . . 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 167	. . . . . . 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 4139	. . . . . . . . . 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 415	. . . . . . . . 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 403	. . . . . . . 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 584	. . . . . . 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 44	. . . . . 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 2489	. . . . 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 2489	. . . 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 1308	. 2 |- ( ph -> -. ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) )
87	86	ralrimivw 2447	1 |- ( ph -> A. s e. Q. -. ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 102   <-> wb 103   /\ w3a 924   = wceq 1289   F. wfal 1294   e. wcel 1438   A.wral 2359   E.wrex 2360   {crab 2363   <.cop 3444   class class class wbr 3837   Or wor 4113   -->wf 4998   ` cfv 5002  (class class class)co 5634   1stc1st 5891   2ndc2nd 5892   Q.cnq 6818   +Q cplq 6820   <Q cltq 6823

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-coll 3946  ax-sep 3949  ax-nul 3957  ax-pow 4001  ax-pr 4027  ax-un 4251  ax-setind 4343  ax-iinf 4393

This theorem depends on definitions:  df-bi 115  df-dc 781  df-3or 925  df-3an 926  df-tru 1292  df-fal 1295  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ne 2256  df-ral 2364  df-rex 2365  df-reu 2366  df-rab 2368  df-v 2621  df-sbc 2839  df-csb 2932  df-dif 2999  df-un 3001  df-in 3003  df-ss 3010  df-nul 3285  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-int 3684  df-iun 3727  df-br 3838  df-opab 3892  df-mpt 3893  df-tr 3929  df-eprel 4107  df-id 4111  df-po 4114  df-iso 4115  df-iord 4184  df-on 4186  df-suc 4189  df-iom 4396  df-xp 4434  df-rel 4435  df-cnv 4436  df-co 4437  df-dm 4438  df-rn 4439  df-res 4440  df-ima 4441  df-iota 4967  df-fun 5004  df-fn 5005  df-f 5006  df-f1 5007  df-fo 5008  df-f1o 5009  df-fv 5010  df-ov 5637  df-oprab 5638  df-mpt2 5639  df-1st 5893  df-2nd 5894  df-recs 6052  df-irdg 6117  df-oadd 6167  df-omul 6168  df-er 6272  df-ec 6274  df-qs 6278  df-ni 6842  df-pli 6843  df-mi 6844  df-lti 6845  df-plpq 6882  df-enq 6885  df-nqqs 6886  df-plqqs 6887  df-ltnqqs 6891

This theorem is referenced by:  cauappcvgprlemcl  7191