Theorem cauappcvgprlem1 6631

Description: Lemma for cauappcvgpr 6634. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-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 } >.
cauappcvgprlem.q	|- (ph -> Q e. Q.)
cauappcvgprlem.r	|- (ph -> R e. Q.)

Assertion

Ref	Expression
cauappcvgprlem1	|- (ph -> <. { l | l <Q ( F ` Q) } , {u | ( F ` Q) <Q u } >. <P ( L +P. <. { l | l <Q ( Q +Q R) } , {u | ( Q +Q R) <Q u } >.))

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

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

Proof of Theorem cauappcvgprlem1

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

Step	Hyp	Ref	Expression
1		cauappcvgprlem.r	. . . . 5 |- (ph -> R e. Q.)
2		halfnqq 6393	. . . . 5 |- ( R e. Q. -> E.x e. Q. (x +Q x) = R)
3	1, 2	syl 14	. . . 4 |- (ph -> E.x e. Q. (x +Q x) = R)
4		simprl 483	. . . . 5 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> x e. Q.)
5		cauappcvgpr.app	. . . . . . . . . . 11 |- (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))))
6	5	adantr 261	. . . . . . . . . 10 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> 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))))
7		cauappcvgprlem.q	. . . . . . . . . . . 12 |- (ph -> Q e. Q.)
8	7	adantr 261	. . . . . . . . . . 11 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> Q e. Q.)
9		fveq2 5121	. . . . . . . . . . . . . 14 |- ( p = Q -> ( F ` p) = ( F ` Q))
10		oveq1 5462	. . . . . . . . . . . . . . 15 |- ( p = Q -> ( p +Q q) = ( Q +Q q))
11	10	oveq2d 5471	. . . . . . . . . . . . . 14 |- ( p = Q -> (( F ` q) +Q ( p +Q q)) = (( F ` q) +Q ( Q +Q q)))
12	9, 11	breq12d 3768	. . . . . . . . . . . . 13 |- ( p = Q -> (( F ` p) <Q (( F ` q) +Q ( p +Q q)) <-> ( F ` Q) <Q (( F ` q) +Q ( Q +Q q))))
13	9, 10	oveq12d 5473	. . . . . . . . . . . . . 14 |- ( p = Q -> (( F ` p) +Q ( p +Q q)) = (( F ` Q) +Q ( Q +Q q)))
14	13	breq2d 3767	. . . . . . . . . . . . 13 |- ( p = Q -> (( F ` q) <Q (( F ` p) +Q ( p +Q q)) <-> ( F ` q) <Q (( F ` Q) +Q ( Q +Q q))))
15	12, 14	anbi12d 442	. . . . . . . . . . . 12 |- ( p = Q -> ((( F ` p) <Q (( F ` q) +Q ( p +Q q)) /\ ( F ` q) <Q (( F ` p) +Q ( p +Q q))) <-> (( F ` Q) <Q (( F ` q) +Q ( Q +Q q)) /\ ( F ` q) <Q (( F ` Q) +Q ( Q +Q q)))))
16		fveq2 5121	. . . . . . . . . . . . . . 15 |- ( q = x -> ( F ` q) = ( F ` x))
17		oveq2 5463	. . . . . . . . . . . . . . 15 |- ( q = x -> ( Q +Q q) = ( Q +Q x))
18	16, 17	oveq12d 5473	. . . . . . . . . . . . . 14 |- ( q = x -> (( F ` q) +Q ( Q +Q q)) = (( F ` x) +Q ( Q +Q x)))
19	18	breq2d 3767	. . . . . . . . . . . . 13 |- ( q = x -> (( F ` Q) <Q (( F ` q) +Q ( Q +Q q)) <-> ( F ` Q) <Q (( F ` x) +Q ( Q +Q x))))
20	17	oveq2d 5471	. . . . . . . . . . . . . 14 |- ( q = x -> (( F ` Q) +Q ( Q +Q q)) = (( F ` Q) +Q ( Q +Q x)))
21	16, 20	breq12d 3768	. . . . . . . . . . . . 13 |- ( q = x -> (( F ` q) <Q (( F ` Q) +Q ( Q +Q q)) <-> ( F ` x) <Q (( F ` Q) +Q ( Q +Q x))))
22	19, 21	anbi12d 442	. . . . . . . . . . . 12 |- ( q = x -> ((( F ` Q) <Q (( F ` q) +Q ( Q +Q q)) /\ ( F ` q) <Q (( F ` Q) +Q ( Q +Q q))) <-> (( F ` Q) <Q (( F ` x) +Q ( Q +Q x)) /\ ( F ` x) <Q (( F ` Q) +Q ( Q +Q x)))))
23	15, 22	rspc2v 2656	. . . . . . . . . . 11 |- (( Q e. Q. /\ x e. Q.) -> (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))) -> (( F ` Q) <Q (( F ` x) +Q ( Q +Q x)) /\ ( F ` x) <Q (( F ` Q) +Q ( Q +Q x)))))
24	8, 4, 23	syl2anc 391	. . . . . . . . . 10 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> (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))) -> (( F ` Q) <Q (( F ` x) +Q ( Q +Q x)) /\ ( F ` x) <Q (( F ` Q) +Q ( Q +Q x)))))
25	6, 24	mpd 13	. . . . . . . . 9 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> (( F ` Q) <Q (( F ` x) +Q ( Q +Q x)) /\ ( F ` x) <Q (( F ` Q) +Q ( Q +Q x))))
26	25	simpld 105	. . . . . . . 8 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> ( F ` Q) <Q (( F ` x) +Q ( Q +Q x)))
27		cauappcvgpr.f	. . . . . . . . . . 11 |- (ph -> F : Q. --> Q.)
28	27	adantr 261	. . . . . . . . . 10 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> F : Q. --> Q.)
29	28, 4	ffvelrnd 5246	. . . . . . . . 9 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> ( F ` x) e. Q.)
30		addassnqg 6366	. . . . . . . . 9 |- ((( F ` x) e. Q. /\ Q e. Q. /\ x e. Q.) -> ((( F ` x) +Q Q) +Q x) = (( F ` x) +Q ( Q +Q x)))
31	29, 8, 4, 30	syl3anc 1134	. . . . . . . 8 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> ((( F ` x) +Q Q) +Q x) = (( F ` x) +Q ( Q +Q x)))
32	26, 31	breqtrrd 3781	. . . . . . 7 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> ( F ` Q) <Q ((( F ` x) +Q Q) +Q x))
33		ltanqg 6384	. . . . . . . . 9 |- ((f e. Q. /\ g e. Q. /\ h e. Q.) -> (f <Q g <-> ( h +Q f) <Q ( h +Q g)))
34	33	adantl 262	. . . . . . . 8 |- (((ph /\ (x e. Q. /\ (x +Q x) = R)) /\ (f e. Q. /\ g e. Q. /\ h e. Q.)) -> (f <Q g <-> ( h +Q f) <Q ( h +Q g)))
35	27, 7	ffvelrnd 5246	. . . . . . . . 9 |- (ph -> ( F ` Q) e. Q.)
36	35	adantr 261	. . . . . . . 8 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> ( F ` Q) e. Q.)
37		addclnq 6359	. . . . . . . . . 10 |- ((( F ` x) e. Q. /\ Q e. Q.) -> (( F ` x) +Q Q) e. Q.)
38	29, 8, 37	syl2anc 391	. . . . . . . . 9 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> (( F ` x) +Q Q) e. Q.)
39		addclnq 6359	. . . . . . . . 9 |- (((( F ` x) +Q Q) e. Q. /\ x e. Q.) -> ((( F ` x) +Q Q) +Q x) e. Q.)
40	38, 4, 39	syl2anc 391	. . . . . . . 8 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> ((( F ` x) +Q Q) +Q x) e. Q.)
41		addcomnqg 6365	. . . . . . . . 9 |- ((f e. Q. /\ g e. Q.) -> (f +Q g) = (g +Q f))
42	41	adantl 262	. . . . . . . 8 |- (((ph /\ (x e. Q. /\ (x +Q x) = R)) /\ (f e. Q. /\ g e. Q.)) -> (f +Q g) = (g +Q f))
43	34, 36, 40, 4, 42	caovord2d 5612	. . . . . . 7 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> (( F ` Q) <Q ((( F ` x) +Q Q) +Q x) <-> (( F ` Q) +Q x) <Q (((( F ` x) +Q Q) +Q x) +Q x)))
44	32, 43	mpbid 135	. . . . . 6 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> (( F ` Q) +Q x) <Q (((( F ` x) +Q Q) +Q x) +Q x))
45		addassnqg 6366	. . . . . . . 8 |- (((( F ` x) +Q Q) e. Q. /\ x e. Q. /\ x e. Q.) -> (((( F ` x) +Q Q) +Q x) +Q x) = ((( F ` x) +Q Q) +Q (x +Q x)))
46	38, 4, 4, 45	syl3anc 1134	. . . . . . 7 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> (((( F ` x) +Q Q) +Q x) +Q x) = ((( F ` x) +Q Q) +Q (x +Q x)))
47		simprr 484	. . . . . . . 8 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> (x +Q x) = R)
48	47	oveq2d 5471	. . . . . . 7 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> ((( F ` x) +Q Q) +Q (x +Q x)) = ((( F ` x) +Q Q) +Q R))
49	1	adantr 261	. . . . . . . 8 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> R e. Q.)
50		addassnqg 6366	. . . . . . . 8 |- ((( F ` x) e. Q. /\ Q e. Q. /\ R e. Q.) -> ((( F ` x) +Q Q) +Q R) = (( F ` x) +Q ( Q +Q R)))
51	29, 8, 49, 50	syl3anc 1134	. . . . . . 7 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> ((( F ` x) +Q Q) +Q R) = (( F ` x) +Q ( Q +Q R)))
52	46, 48, 51	3eqtrd 2073	. . . . . 6 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> (((( F ` x) +Q Q) +Q x) +Q x) = (( F ` x) +Q ( Q +Q R)))
53	44, 52	breqtrd 3779	. . . . 5 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> (( F ` Q) +Q x) <Q (( F ` x) +Q ( Q +Q R)))
54		oveq2 5463	. . . . . . 7 |- ( q = x -> (( F ` Q) +Q q) = (( F ` Q) +Q x))
55	16	oveq1d 5470	. . . . . . 7 |- ( q = x -> (( F ` q) +Q ( Q +Q R)) = (( F ` x) +Q ( Q +Q R)))
56	54, 55	breq12d 3768	. . . . . 6 |- ( q = x -> ((( F ` Q) +Q q) <Q (( F ` q) +Q ( Q +Q R)) <-> (( F ` Q) +Q x) <Q (( F ` x) +Q ( Q +Q R))))
57	56	rspcev 2650	. . . . 5 |- ((x e. Q. /\ (( F ` Q) +Q x) <Q (( F ` x) +Q ( Q +Q R))) -> E. q e. Q. (( F ` Q) +Q q) <Q (( F ` q) +Q ( Q +Q R)))
58	4, 53, 57	syl2anc 391	. . . 4 |- ((ph /\ (x e. Q. /\ (x +Q x) = R)) -> E. q e. Q. (( F ` Q) +Q q) <Q (( F ` q) +Q ( Q +Q R)))
59	3, 58	rexlimddv 2431	. . 3 |- (ph -> E. q e. Q. (( F ` Q) +Q q) <Q (( F ` q) +Q ( Q +Q R)))
60		cauappcvgpr.bnd	. . . . . . . 8 |- (ph -> A. p e. Q. A <Q ( F ` p))
61		cauappcvgpr.lim	. . . . . . . 8 |- 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 } >.
62		addclnq 6359	. . . . . . . . 9 |- (( Q e. Q. /\ R e. Q.) -> ( Q +Q R) e. Q.)
63	7, 1, 62	syl2anc 391	. . . . . . . 8 |- (ph -> ( Q +Q R) e. Q.)
64	27, 5, 60, 61, 63	cauappcvgprlemladd 6630	. . . . . . 7 |- (ph -> ( L +P. <. { l | l <Q ( Q +Q R) } , {u | ( Q +Q R) <Q u } >.) = <. { l e. Q. | E. q e. Q. ( l +Q q) <Q (( F ` q) +Q ( Q +Q R)) } , {u e. Q. | E. q e. Q. ((( F ` q) +Q q) +Q ( Q +Q R)) <Q u } >.)
65	64	fveq2d 5125	. . . . . 6 |- (ph -> ( 1st ` ( L +P. <. { l | l <Q ( Q +Q R) } , {u | ( Q +Q R) <Q u } >.)) = ( 1st ` <. { l e. Q. | E. q e. Q. ( l +Q q) <Q (( F ` q) +Q ( Q +Q R)) } , {u e. Q. | E. q e. Q. ((( F ` q) +Q q) +Q ( Q +Q R)) <Q u } >.))
66		nqex 6347	. . . . . . . 8 |- Q. e. _V
67	66	rabex 3892	. . . . . . 7 |- { l e. Q. | E. q e. Q. ( l +Q q) <Q (( F ` q) +Q ( Q +Q R)) } e. _V
68	66	rabex 3892	. . . . . . 7 |- {u e. Q. | E. q e. Q. ((( F ` q) +Q q) +Q ( Q +Q R)) <Q u } e. _V
69	67, 68	op1st 5715	. . . . . 6 |- ( 1st ` <. { l e. Q. | E. q e. Q. ( l +Q q) <Q (( F ` q) +Q ( Q +Q R)) } , {u e. Q. | E. q e. Q. ((( F ` q) +Q q) +Q ( Q +Q R)) <Q u } >.) = { l e. Q. | E. q e. Q. ( l +Q q) <Q (( F ` q) +Q ( Q +Q R)) }
70	65, 69	syl6eq 2085	. . . . 5 |- (ph -> ( 1st ` ( L +P. <. { l | l <Q ( Q +Q R) } , {u | ( Q +Q R) <Q u } >.)) = { l e. Q. | E. q e. Q. ( l +Q q) <Q (( F ` q) +Q ( Q +Q R)) })
71	70	eleq2d 2104	. . . 4 |- (ph -> (( F ` Q) e. ( 1st ` ( L +P. <. { l | l <Q ( Q +Q R) } , {u | ( Q +Q R) <Q u } >.)) <-> ( F ` Q) e. { l e. Q. | E. q e. Q. ( l +Q q) <Q (( F ` q) +Q ( Q +Q R)) }))
72		oveq1 5462	. . . . . . . 8 |- ( l = ( F ` Q) -> ( l +Q q) = (( F ` Q) +Q q))
73	72	breq1d 3765	. . . . . . 7 |- ( l = ( F ` Q) -> (( l +Q q) <Q (( F ` q) +Q ( Q +Q R)) <-> (( F ` Q) +Q q) <Q (( F ` q) +Q ( Q +Q R))))
74	73	rexbidv 2321	. . . . . 6 |- ( l = ( F ` Q) -> (E. q e. Q. ( l +Q q) <Q (( F ` q) +Q ( Q +Q R)) <-> E. q e. Q. (( F ` Q) +Q q) <Q (( F ` q) +Q ( Q +Q R))))
75	74	elrab3 2693	. . . . 5 |- (( F ` Q) e. Q. -> (( F ` Q) e. { l e. Q. | E. q e. Q. ( l +Q q) <Q (( F ` q) +Q ( Q +Q R)) } <-> E. q e. Q. (( F ` Q) +Q q) <Q (( F ` q) +Q ( Q +Q R))))
76	35, 75	syl 14	. . . 4 |- (ph -> (( F ` Q) e. { l e. Q. | E. q e. Q. ( l +Q q) <Q (( F ` q) +Q ( Q +Q R)) } <-> E. q e. Q. (( F ` Q) +Q q) <Q (( F ` q) +Q ( Q +Q R))))
77	71, 76	bitrd 177	. . 3 |- (ph -> (( F ` Q) e. ( 1st ` ( L +P. <. { l | l <Q ( Q +Q R) } , {u | ( Q +Q R) <Q u } >.)) <-> E. q e. Q. (( F ` Q) +Q q) <Q (( F ` q) +Q ( Q +Q R))))
78	59, 77	mpbird 156	. 2 |- (ph -> ( F ` Q) e. ( 1st ` ( L +P. <. { l | l <Q ( Q +Q R) } , {u | ( Q +Q R) <Q u } >.)))
79	27, 5, 60, 61	cauappcvgprlemcl 6625	. . . 4 |- (ph -> L e. P.)
80		nqprlu 6530	. . . . 5 |- (( Q +Q R) e. Q. -> <. { l | l <Q ( Q +Q R) } , {u | ( Q +Q R) <Q u } >. e. P.)
81	63, 80	syl 14	. . . 4 |- (ph -> <. { l | l <Q ( Q +Q R) } , {u | ( Q +Q R) <Q u } >. e. P.)
82		addclpr 6520	. . . 4 |- (( L e. P. /\ <. { l | l <Q ( Q +Q R) } , {u | ( Q +Q R) <Q u } >. e. P.) -> ( L +P. <. { l | l <Q ( Q +Q R) } , {u | ( Q +Q R) <Q u } >.) e. P.)
83	79, 81, 82	syl2anc 391	. . 3 |- (ph -> ( L +P. <. { l | l <Q ( Q +Q R) } , {u | ( Q +Q R) <Q u } >.) e. P.)
84		nqprl 6533	. . 3 |- ((( F ` Q) e. Q. /\ ( L +P. <. { l | l <Q ( Q +Q R) } , {u | ( Q +Q R) <Q u } >.) e. P.) -> (( F ` Q) e. ( 1st ` ( L +P. <. { l | l <Q ( Q +Q R) } , {u | ( Q +Q R) <Q u } >.)) <-> <. { l | l <Q ( F ` Q) } , {u | ( F ` Q) <Q u } >. <P ( L +P. <. { l | l <Q ( Q +Q R) } , {u | ( Q +Q R) <Q u } >.)))
85	35, 83, 84	syl2anc 391	. 2 |- (ph -> (( F ` Q) e. ( 1st ` ( L +P. <. { l | l <Q ( Q +Q R) } , {u | ( Q +Q R) <Q u } >.)) <-> <. { l | l <Q ( F ` Q) } , {u | ( F ` Q) <Q u } >. <P ( L +P. <. { l | l <Q ( Q +Q R) } , {u | ( Q +Q R) <Q u } >.)))
86	78, 85	mpbid 135	1 |- (ph -> <. { l | l <Q ( F ` Q) } , {u | ( F ` Q) <Q u } >. <P ( L +P. <. { l | l <Q ( Q +Q R) } , {u | ( Q +Q R) <Q u } >.))

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98   /\ w3a 884   = wceq 1242   e. wcel 1390   {cab 2023  A.wral 2300  E.wrex 2301   {crab 2304   <.cop 3370   class class class wbr 3755   -->wf 4841   ` cfv 4845  (class class class)co 5455   1stc1st 5707   Q.cnq 6264   +Q cplq 6266   <Q cltq 6269   P.cnp 6275   +P. cpp 6277   <P cltp 6279

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3863  ax-sep 3866  ax-nul 3874  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-setind 4220  ax-iinf 4254

This theorem depends on definitions:  df-bi 110  df-dc 742  df-3or 885  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-int 3607  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-tr 3846  df-eprel 4017  df-id 4021  df-po 4024  df-iso 4025  df-iord 4069  df-on 4071  df-suc 4074  df-iom 4257  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-ov 5458  df-oprab 5459  df-mpt2 5460  df-1st 5709  df-2nd 5710  df-recs 5861  df-irdg 5897  df-1o 5940  df-2o 5941  df-oadd 5944  df-omul 5945  df-er 6042  df-ec 6044  df-qs 6048  df-ni 6288  df-pli 6289  df-mi 6290  df-lti 6291  df-plpq 6328  df-mpq 6329  df-enq 6331  df-nqqs 6332  df-plqqs 6333  df-mqqs 6334  df-1nqqs 6335  df-rq 6336  df-ltnqqs 6337  df-enq0 6407  df-nq0 6408  df-0nq0 6409  df-plq0 6410  df-mq0 6411  df-inp 6449  df-iplp 6451  df-iltp 6453

This theorem is referenced by:  cauappcvgprlemlim  6633