Theorem cauappcvgprlemladdru 6628

Description: Lemma for cauappcvgprlemladd 6630. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.)

Hypotheses

Ref	Expression
cauappcvgpr.f	⊢ (φ → 𝐹:Q⟶Q)
cauappcvgpr.app	⊢ (φ → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞))))
cauappcvgpr.bnd	⊢ (φ → ∀𝑝 ∈ Q A <Q (𝐹‘𝑝))
cauappcvgpr.lim	⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {u ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q u}⟩
cauappcvgprlemladd.s	⊢ (φ → 𝑆 ∈ Q)

Assertion

Ref	Expression
cauappcvgprlemladdru	⊢ (φ → (2nd ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {u ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q u}⟩) ⊆ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩)))

Distinct variable groups:   A,𝑝   𝐿,𝑝,𝑞   φ,𝑝,𝑞   𝐹,𝑙,u,𝑝,𝑞   𝑆,𝑙,𝑞,u

Allowed substitution hints:   φ(u,𝑙)   A(u,𝑞,𝑙)   𝑆(𝑝)   𝐿(u,𝑙)

Proof of Theorem cauappcvgprlemladdru

Dummy variables f g ℎ 𝑟 v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq2 3759	. . . . 5 ⊢ (u = 𝑟 → ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q u ↔ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑟))
2	1	rexbidv 2321	. . . 4 ⊢ (u = 𝑟 → (∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q u ↔ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑟))
3		nqex 6347	. . . . . 6 ⊢ Q ∈ V
4	3	rabex 3892	. . . . 5 ⊢ {𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)} ∈ V
5	3	rabex 3892	. . . . 5 ⊢ {u ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q u} ∈ V
6	4, 5	op2nd 5716	. . . 4 ⊢ (2nd ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {u ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q u}⟩) = {u ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q u}
7	2, 6	elrab2 2694	. . 3 ⊢ (𝑟 ∈ (2nd ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {u ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q u}⟩) ↔ (𝑟 ∈ Q ∧ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑟))
8		cauappcvgpr.f	. . . . . . . . . . . . 13 ⊢ (φ → 𝐹:Q⟶Q)
9		cauappcvgpr.app	. . . . . . . . . . . . 13 ⊢ (φ → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞))))
10		cauappcvgpr.bnd	. . . . . . . . . . . . 13 ⊢ (φ → ∀𝑝 ∈ Q A <Q (𝐹‘𝑝))
11		cauappcvgpr.lim	. . . . . . . . . . . . 13 ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {u ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q u}⟩
12		cauappcvgprlemladd.s	. . . . . . . . . . . . 13 ⊢ (φ → 𝑆 ∈ Q)
13	8, 9, 10, 11, 12	cauappcvgprlemladdfl 6627	. . . . . . . . . . . 12 ⊢ (φ → (1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩)) ⊆ (1st ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {u ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q u}⟩))
14		oveq2 5463	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = v → (𝑙 +Q 𝑞) = (𝑙 +Q v))
15		fveq2 5121	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = v → (𝐹‘𝑞) = (𝐹‘v))
16	15	oveq1d 5470	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = v → ((𝐹‘𝑞) +Q 𝑆) = ((𝐹‘v) +Q 𝑆))
17	14, 16	breq12d 3768	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 = v → ((𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆) ↔ (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆)))
18	17	cbvrexv 2528	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆) ↔ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆))
19	18	a1i 9	. . . . . . . . . . . . . . 15 ⊢ (𝑙 ∈ Q → (∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆) ↔ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆)))
20	19	rabbiia 2541	. . . . . . . . . . . . . 14 ⊢ {𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)} = {𝑙 ∈ Q ∣ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆)}
21		id 19	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑞 = v → 𝑞 = v)
22	15, 21	oveq12d 5473	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = v → ((𝐹‘𝑞) +Q 𝑞) = ((𝐹‘v) +Q v))
23	22	oveq1d 5470	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = v → (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) = (((𝐹‘v) +Q v) +Q 𝑆))
24	23	breq1d 3765	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 = v → ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q u ↔ (((𝐹‘v) +Q v) +Q 𝑆) <Q u))
25	24	cbvrexv 2528	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q u ↔ ∃v ∈ Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u)
26	25	a1i 9	. . . . . . . . . . . . . . 15 ⊢ (u ∈ Q → (∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q u ↔ ∃v ∈ Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u))
27	26	rabbiia 2541	. . . . . . . . . . . . . 14 ⊢ {u ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q u} = {u ∈ Q ∣ ∃v ∈ Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u}
28	20, 27	opeq12i 3545	. . . . . . . . . . . . 13 ⊢ ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {u ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q u}⟩ = ⟨{𝑙 ∈ Q ∣ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆)}, {u ∈ Q ∣ ∃v ∈ Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u}⟩
29	28	fveq2i 5124	. . . . . . . . . . . 12 ⊢ (1st ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {u ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q u}⟩) = (1st ‘⟨{𝑙 ∈ Q ∣ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆)}, {u ∈ Q ∣ ∃v ∈ Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u}⟩)
30	13, 29	syl6sseq 2985	. . . . . . . . . . 11 ⊢ (φ → (1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩)) ⊆ (1st ‘⟨{𝑙 ∈ Q ∣ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆)}, {u ∈ Q ∣ ∃v ∈ Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u}⟩))
31	30	adantr 261	. . . . . . . . . 10 ⊢ ((φ ∧ 𝑞 ∈ Q) → (1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩)) ⊆ (1st ‘⟨{𝑙 ∈ Q ∣ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆)}, {u ∈ Q ∣ ∃v ∈ Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u}⟩))
32	8	ad2antrr 457	. . . . . . . . . . . . . . . . . 18 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → 𝐹:Q⟶Q)
33		simplr 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → 𝑞 ∈ Q)
34	32, 33	ffvelrnd 5246	. . . . . . . . . . . . . . . . 17 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (𝐹‘𝑞) ∈ Q)
35		simpr 103	. . . . . . . . . . . . . . . . 17 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → v ∈ Q)
36		addassnqg 6366	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑞) ∈ Q ∧ 𝑞 ∈ Q ∧ v ∈ Q) → (((𝐹‘𝑞) +Q 𝑞) +Q v) = ((𝐹‘𝑞) +Q (𝑞 +Q v)))
37	34, 33, 35, 36	syl3anc 1134	. . . . . . . . . . . . . . . 16 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (((𝐹‘𝑞) +Q 𝑞) +Q v) = ((𝐹‘𝑞) +Q (𝑞 +Q v)))
38		addclnq 6359	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑞) ∈ Q ∧ 𝑞 ∈ Q) → ((𝐹‘𝑞) +Q 𝑞) ∈ Q)
39	34, 33, 38	syl2anc 391	. . . . . . . . . . . . . . . . 17 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ((𝐹‘𝑞) +Q 𝑞) ∈ Q)
40		addclnq 6359	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑞) +Q 𝑞) ∈ Q ∧ v ∈ Q) → (((𝐹‘𝑞) +Q 𝑞) +Q v) ∈ Q)
41	39, 40	sylancom 397	. . . . . . . . . . . . . . . 16 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (((𝐹‘𝑞) +Q 𝑞) +Q v) ∈ Q)
42	37, 41	eqeltrrd 2112	. . . . . . . . . . . . . . 15 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ((𝐹‘𝑞) +Q (𝑞 +Q v)) ∈ Q)
43	32, 35	ffvelrnd 5246	. . . . . . . . . . . . . . 15 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (𝐹‘v) ∈ Q)
44		ltsonq 6382	. . . . . . . . . . . . . . . 16 ⊢ <Q Or Q
45		so2nr 4049	. . . . . . . . . . . . . . . 16 ⊢ (( <Q Or Q ∧ (((𝐹‘𝑞) +Q (𝑞 +Q v)) ∈ Q ∧ (𝐹‘v) ∈ Q)) → ¬ (((𝐹‘𝑞) +Q (𝑞 +Q v)) <Q (𝐹‘v) ∧ (𝐹‘v) <Q ((𝐹‘𝑞) +Q (𝑞 +Q v))))
46	44, 45	mpan 400	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑞) +Q (𝑞 +Q v)) ∈ Q ∧ (𝐹‘v) ∈ Q) → ¬ (((𝐹‘𝑞) +Q (𝑞 +Q v)) <Q (𝐹‘v) ∧ (𝐹‘v) <Q ((𝐹‘𝑞) +Q (𝑞 +Q v))))
47	42, 43, 46	syl2anc 391	. . . . . . . . . . . . . 14 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ¬ (((𝐹‘𝑞) +Q (𝑞 +Q v)) <Q (𝐹‘v) ∧ (𝐹‘v) <Q ((𝐹‘𝑞) +Q (𝑞 +Q v))))
48	12	ad2antrr 457	. . . . . . . . . . . . . . . . . . 19 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → 𝑆 ∈ Q)
49		addcomnqg 6365	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((f ∈ Q ∧ g ∈ Q) → (f +Q g) = (g +Q f))
50	49	adantl 262	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) ∧ (f ∈ Q ∧ g ∈ Q)) → (f +Q g) = (g +Q f))
51		addassnqg 6366	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((f ∈ Q ∧ g ∈ Q ∧ ℎ ∈ Q) → ((f +Q g) +Q ℎ) = (f +Q (g +Q ℎ)))
52	51	adantl 262	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) ∧ (f ∈ Q ∧ g ∈ Q ∧ ℎ ∈ Q)) → ((f +Q g) +Q ℎ) = (f +Q (g +Q ℎ)))
53	39, 48, 35, 50, 52	caov32d 5623	. . . . . . . . . . . . . . . . . 18 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q v) = ((((𝐹‘𝑞) +Q 𝑞) +Q v) +Q 𝑆))
54	53	breq1d 3765	. . . . . . . . . . . . . . . . 17 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q v) <Q ((𝐹‘v) +Q 𝑆) ↔ ((((𝐹‘𝑞) +Q 𝑞) +Q v) +Q 𝑆) <Q ((𝐹‘v) +Q 𝑆)))
55		ltanqg 6384	. . . . . . . . . . . . . . . . . . 19 ⊢ ((f ∈ Q ∧ g ∈ Q ∧ ℎ ∈ Q) → (f <Q g ↔ (ℎ +Q f) <Q (ℎ +Q g)))
56	55	adantl 262	. . . . . . . . . . . . . . . . . 18 ⊢ ((((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) ∧ (f ∈ Q ∧ g ∈ Q ∧ ℎ ∈ Q)) → (f <Q g ↔ (ℎ +Q f) <Q (ℎ +Q g)))
57	56, 41, 43, 48, 50	caovord2d 5612	. . . . . . . . . . . . . . . . 17 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ((((𝐹‘𝑞) +Q 𝑞) +Q v) <Q (𝐹‘v) ↔ ((((𝐹‘𝑞) +Q 𝑞) +Q v) +Q 𝑆) <Q ((𝐹‘v) +Q 𝑆)))
58	37	breq1d 3765	. . . . . . . . . . . . . . . . 17 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ((((𝐹‘𝑞) +Q 𝑞) +Q v) <Q (𝐹‘v) ↔ ((𝐹‘𝑞) +Q (𝑞 +Q v)) <Q (𝐹‘v)))
59	54, 57, 58	3bitr2d 205	. . . . . . . . . . . . . . . 16 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q v) <Q ((𝐹‘v) +Q 𝑆) ↔ ((𝐹‘𝑞) +Q (𝑞 +Q v)) <Q (𝐹‘v)))
60	59	biimpd 132	. . . . . . . . . . . . . . 15 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q v) <Q ((𝐹‘v) +Q 𝑆) → ((𝐹‘𝑞) +Q (𝑞 +Q v)) <Q (𝐹‘v)))
61	9	ad2antrr 457	. . . . . . . . . . . . . . . . . . 19 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞))))
62		fveq2 5121	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = v → (𝐹‘𝑝) = (𝐹‘v))
63		oveq1 5462	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = v → (𝑝 +Q 𝑞) = (v +Q 𝑞))
64	63	oveq2d 5471	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = v → ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) = ((𝐹‘𝑞) +Q (v +Q 𝑞)))
65	62, 64	breq12d 3768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = v → ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ↔ (𝐹‘v) <Q ((𝐹‘𝑞) +Q (v +Q 𝑞))))
66	62, 63	oveq12d 5473	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = v → ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)) = ((𝐹‘v) +Q (v +Q 𝑞)))
67	66	breq2d 3767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = v → ((𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)) ↔ (𝐹‘𝑞) <Q ((𝐹‘v) +Q (v +Q 𝑞))))
68	65, 67	anbi12d 442	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = v → (((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞))) ↔ ((𝐹‘v) <Q ((𝐹‘𝑞) +Q (v +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘v) +Q (v +Q 𝑞)))))
69	68	ralbidv 2320	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = v → (∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞))) ↔ ∀𝑞 ∈ Q ((𝐹‘v) <Q ((𝐹‘𝑞) +Q (v +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘v) +Q (v +Q 𝑞)))))
70	69	rspcv 2646	. . . . . . . . . . . . . . . . . . . 20 ⊢ (v ∈ Q → (∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞))) → ∀𝑞 ∈ Q ((𝐹‘v) <Q ((𝐹‘𝑞) +Q (v +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘v) +Q (v +Q 𝑞)))))
71	70	adantl 262	. . . . . . . . . . . . . . . . . . 19 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞))) → ∀𝑞 ∈ Q ((𝐹‘v) <Q ((𝐹‘𝑞) +Q (v +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘v) +Q (v +Q 𝑞)))))
72	61, 71	mpd 13	. . . . . . . . . . . . . . . . . 18 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ∀𝑞 ∈ Q ((𝐹‘v) <Q ((𝐹‘𝑞) +Q (v +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘v) +Q (v +Q 𝑞))))
73		rsp 2363	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑞 ∈ Q ((𝐹‘v) <Q ((𝐹‘𝑞) +Q (v +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘v) +Q (v +Q 𝑞))) → (𝑞 ∈ Q → ((𝐹‘v) <Q ((𝐹‘𝑞) +Q (v +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘v) +Q (v +Q 𝑞)))))
74	72, 33, 73	sylc 56	. . . . . . . . . . . . . . . . 17 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ((𝐹‘v) <Q ((𝐹‘𝑞) +Q (v +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘v) +Q (v +Q 𝑞))))
75	74	simpld 105	. . . . . . . . . . . . . . . 16 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (𝐹‘v) <Q ((𝐹‘𝑞) +Q (v +Q 𝑞)))
76		addcomnqg 6365	. . . . . . . . . . . . . . . . . 18 ⊢ ((v ∈ Q ∧ 𝑞 ∈ Q) → (v +Q 𝑞) = (𝑞 +Q v))
77	35, 33, 76	syl2anc 391	. . . . . . . . . . . . . . . . 17 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (v +Q 𝑞) = (𝑞 +Q v))
78	77	oveq2d 5471	. . . . . . . . . . . . . . . 16 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ((𝐹‘𝑞) +Q (v +Q 𝑞)) = ((𝐹‘𝑞) +Q (𝑞 +Q v)))
79	75, 78	breqtrd 3779	. . . . . . . . . . . . . . 15 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (𝐹‘v) <Q ((𝐹‘𝑞) +Q (𝑞 +Q v)))
80	60, 79	jctird 300	. . . . . . . . . . . . . 14 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → (((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q v) <Q ((𝐹‘v) +Q 𝑆) → (((𝐹‘𝑞) +Q (𝑞 +Q v)) <Q (𝐹‘v) ∧ (𝐹‘v) <Q ((𝐹‘𝑞) +Q (𝑞 +Q v)))))
81	47, 80	mtod 588	. . . . . . . . . . . . 13 ⊢ (((φ ∧ 𝑞 ∈ Q) ∧ v ∈ Q) → ¬ ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q v) <Q ((𝐹‘v) +Q 𝑆))
82	81	nrexdv 2406	. . . . . . . . . . . 12 ⊢ ((φ ∧ 𝑞 ∈ Q) → ¬ ∃v ∈ Q ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q v) <Q ((𝐹‘v) +Q 𝑆))
83	8	ffvelrnda 5245	. . . . . . . . . . . . . . 15 ⊢ ((φ ∧ 𝑞 ∈ Q) → (𝐹‘𝑞) ∈ Q)
84	83, 38	sylancom 397	. . . . . . . . . . . . . 14 ⊢ ((φ ∧ 𝑞 ∈ Q) → ((𝐹‘𝑞) +Q 𝑞) ∈ Q)
85	12	adantr 261	. . . . . . . . . . . . . 14 ⊢ ((φ ∧ 𝑞 ∈ Q) → 𝑆 ∈ Q)
86		addclnq 6359	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑞) +Q 𝑞) ∈ Q ∧ 𝑆 ∈ Q) → (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ Q)
87	84, 85, 86	syl2anc 391	. . . . . . . . . . . . 13 ⊢ ((φ ∧ 𝑞 ∈ Q) → (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ Q)
88		oveq1 5462	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) → (𝑙 +Q v) = ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q v))
89	88	breq1d 3765	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) → ((𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆) ↔ ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q v) <Q ((𝐹‘v) +Q 𝑆)))
90	89	rexbidv 2321	. . . . . . . . . . . . . 14 ⊢ (𝑙 = (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) → (∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆) ↔ ∃v ∈ Q ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q v) <Q ((𝐹‘v) +Q 𝑆)))
91	90	elrab3 2693	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ Q → ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ {𝑙 ∈ Q ∣ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆)} ↔ ∃v ∈ Q ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q v) <Q ((𝐹‘v) +Q 𝑆)))
92	87, 91	syl 14	. . . . . . . . . . . 12 ⊢ ((φ ∧ 𝑞 ∈ Q) → ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ {𝑙 ∈ Q ∣ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆)} ↔ ∃v ∈ Q ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) +Q v) <Q ((𝐹‘v) +Q 𝑆)))
93	82, 92	mtbird 597	. . . . . . . . . . 11 ⊢ ((φ ∧ 𝑞 ∈ Q) → ¬ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ {𝑙 ∈ Q ∣ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆)})
94	3	rabex 3892	. . . . . . . . . . . . 13 ⊢ {𝑙 ∈ Q ∣ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆)} ∈ V
95	3	rabex 3892	. . . . . . . . . . . . 13 ⊢ {u ∈ Q ∣ ∃v ∈ Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u} ∈ V
96	94, 95	op1st 5715	. . . . . . . . . . . 12 ⊢ (1st ‘⟨{𝑙 ∈ Q ∣ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆)}, {u ∈ Q ∣ ∃v ∈ Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u}⟩) = {𝑙 ∈ Q ∣ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆)}
97	96	eleq2i 2101	. . . . . . . . . . 11 ⊢ ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ (1st ‘⟨{𝑙 ∈ Q ∣ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆)}, {u ∈ Q ∣ ∃v ∈ Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u}⟩) ↔ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ {𝑙 ∈ Q ∣ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆)})
98	93, 97	sylnibr 601	. . . . . . . . . 10 ⊢ ((φ ∧ 𝑞 ∈ Q) → ¬ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ (1st ‘⟨{𝑙 ∈ Q ∣ ∃v ∈ Q (𝑙 +Q v) <Q ((𝐹‘v) +Q 𝑆)}, {u ∈ Q ∣ ∃v ∈ Q (((𝐹‘v) +Q v) +Q 𝑆) <Q u}⟩))
99	31, 98	ssneldd 2942	. . . . . . . . 9 ⊢ ((φ ∧ 𝑞 ∈ Q) → ¬ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ (1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩)))
100	99	adantlr 446	. . . . . . . 8 ⊢ (((φ ∧ 𝑟 ∈ Q) ∧ 𝑞 ∈ Q) → ¬ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ (1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩)))
101	100	adantr 261	. . . . . . 7 ⊢ ((((φ ∧ 𝑟 ∈ Q) ∧ 𝑞 ∈ Q) ∧ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑟) → ¬ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ (1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩)))
102	8, 9, 10, 11	cauappcvgprlemcl 6625	. . . . . . . . . . . . 13 ⊢ (φ → 𝐿 ∈ P)
103		nqprlu 6530	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ Q → ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩ ∈ P)
104	12, 103	syl 14	. . . . . . . . . . . . 13 ⊢ (φ → ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩ ∈ P)
105		addclpr 6520	. . . . . . . . . . . . 13 ⊢ ((𝐿 ∈ P ∧ ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩ ∈ P) → (𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩) ∈ P)
106	102, 104, 105	syl2anc 391	. . . . . . . . . . . 12 ⊢ (φ → (𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩) ∈ P)
107		prop 6458	. . . . . . . . . . . 12 ⊢ ((𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩) ∈ P → ⟨(1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩)), (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩))⟩ ∈ P)
108	106, 107	syl 14	. . . . . . . . . . 11 ⊢ (φ → ⟨(1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩)), (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩))⟩ ∈ P)
109		prloc 6474	. . . . . . . . . . 11 ⊢ ((⟨(1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩)), (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩))⟩ ∈ P ∧ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑟) → ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ (1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩)) ∨ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩))))
110	108, 109	sylan 267	. . . . . . . . . 10 ⊢ ((φ ∧ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑟) → ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ (1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩)) ∨ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩))))
111	110	adantlr 446	. . . . . . . . 9 ⊢ (((φ ∧ 𝑟 ∈ Q) ∧ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑟) → ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ (1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩)) ∨ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩))))
112	111	adantlr 446	. . . . . . . 8 ⊢ ((((φ ∧ 𝑟 ∈ Q) ∧ 𝑞 ∈ Q) ∧ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑟) → ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ (1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩)) ∨ 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩))))
113	112	orcomd 647	. . . . . . 7 ⊢ ((((φ ∧ 𝑟 ∈ Q) ∧ 𝑞 ∈ Q) ∧ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑟) → (𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩)) ∨ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) ∈ (1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩))))
114	101, 113	ecased 1238	. . . . . 6 ⊢ ((((φ ∧ 𝑟 ∈ Q) ∧ 𝑞 ∈ Q) ∧ (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑟) → 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩)))
115	114	ex 108	. . . . 5 ⊢ (((φ ∧ 𝑟 ∈ Q) ∧ 𝑞 ∈ Q) → ((((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑟 → 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩))))
116	115	rexlimdva 2427	. . . 4 ⊢ ((φ ∧ 𝑟 ∈ Q) → (∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑟 → 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩))))
117	116	expimpd 345	. . 3 ⊢ (φ → ((𝑟 ∈ Q ∧ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑟) → 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩))))
118	7, 117	syl5bi 141	. 2 ⊢ (φ → (𝑟 ∈ (2nd ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {u ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q u}⟩) → 𝑟 ∈ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩))))
119	118	ssrdv 2945	1 ⊢ (φ → (2nd ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {u ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q u}⟩) ⊆ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {u ∣ 𝑆 <Q u}⟩)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 628   ∧ w3a 884   = wceq 1242   ∈ wcel 1390  {cab 2023  ∀wral 2300  ∃wrex 2301  {crab 2304   ⊆ wss 2911  ⟨cop 3370   class class class wbr 3755   Or wor 4023  ⟶wf 4841  ‘cfv 4845  (class class class)co 5455  1^st c1st 5707  2^nd c2nd 5708  Qcnq 6264   +_Q cplq 6266   <_Q cltq 6269  Pcnp 6275   +_P cpp 6277

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-bnd 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

This theorem is referenced by:  cauappcvgprlemladd  6630