caucvgprprlemloc - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > caucvgprprlemloc		GIF version

Theorem caucvgprprlemloc 6893

Description: Lemma for caucvgprpr 6902. The putative limit is located. (Contributed by Jim Kingdon, 21-Dec-2020.)

**Hypotheses**
Ref	Expression
caucvgprpr.f	⊢ (𝜑 → 𝐹:N⟶P)
caucvgprpr.cau	⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <_N 𝑘 → ((𝐹‘𝑛)<_P ((𝐹‘𝑘) +_P ⟨{𝑙 ∣ 𝑙 <_Q (_Q‘[⟨𝑛, 1_𝑜⟩] ~_Q )}, {𝑢 ∣ (_Q‘[⟨𝑛, 1_𝑜⟩] ~_Q ) <_Q 𝑢}⟩) ∧ (𝐹‘𝑘)<_P ((𝐹‘𝑛) +_P ⟨{𝑙 ∣ 𝑙 <_Q (_Q‘[⟨𝑛, 1_𝑜⟩] ~_Q )}, {𝑢 ∣ (_Q‘[⟨𝑛, 1_𝑜⟩] ~_Q ) <_Q 𝑢}⟩))))
caucvgprpr.bnd	⊢ (𝜑 → ∀𝑚 ∈ N 𝐴<_P (𝐹‘𝑚))
caucvgprpr.lim	⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N ⟨{𝑝 ∣ 𝑝 <_Q (𝑙 +_Q (_Q‘[⟨𝑟, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑙 +_Q (_Q‘[⟨𝑟, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑟, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑟, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑢}, {𝑞 ∣ 𝑢 <_Q 𝑞}⟩}⟩

**Assertion**
Ref	Expression
caucvgprprlemloc	⊢ (𝜑 → ∀𝑠 ∈ Q ∀𝑡 ∈ Q (𝑠 <_Q 𝑡 → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿))))

Distinct variable groups: 𝐴,𝑚 𝑚,𝐹 𝐹,𝑙,𝑟 𝑢,𝐹,𝑟 𝑞,𝑝,𝑠,𝑡 𝜑,𝑠,𝑡 𝑝,𝑙,𝑞,𝑠,𝑡,𝑟 𝑢,𝑝,𝑞,𝑠,𝑡 Allowed substitution hints: 𝜑(𝑢,𝑘,𝑚,𝑛,𝑟,𝑞,𝑝,𝑙) 𝐴(𝑢,𝑡,𝑘,𝑛,𝑠,𝑟,𝑞,𝑝,𝑙) 𝐹(𝑡,𝑘,𝑛,𝑠,𝑞,𝑝) 𝐿(𝑢,𝑡,𝑘,𝑚,𝑛,𝑠,𝑟,𝑞,𝑝,𝑙)

Proof of Theorem caucvgprprlemloc Dummy variables 𝑎 𝑏 𝑓 𝑔 ℎ 𝑐 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ltexnqi 6599	. . . . 5 ⊢ (𝑠 <_Q 𝑡 → ∃𝑦 ∈ Q (𝑠 +_Q 𝑦) = 𝑡)
2	1	adantl 271	. . . 4 ⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) → ∃𝑦 ∈ Q (𝑠 +_Q 𝑦) = 𝑡)
3		subhalfnqq 6604	. . . . . 6 ⊢ (𝑦 ∈ Q → ∃𝑥 ∈ Q (𝑥 +_Q 𝑥) <_Q 𝑦)
4	3	ad2antrl 473	. . . . 5 ⊢ ((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) → ∃𝑥 ∈ Q (𝑥 +_Q 𝑥) <_Q 𝑦)
5		archrecnq 6853	. . . . . . 7 ⊢ (𝑥 ∈ Q → ∃𝑐 ∈ N (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)
6	5	ad2antrl 473	. . . . . 6 ⊢ (((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) → ∃𝑐 ∈ N (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)
7		simpllr 500	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) → 𝑠 <_Q 𝑡)
8	7	adantr 270	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → 𝑠 <_Q 𝑡)
9		simplrl 501	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) → 𝑦 ∈ Q)
10	9	adantr 270	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → 𝑦 ∈ Q)
11		simplrr 502	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) → (𝑠 +_Q 𝑦) = 𝑡)
12	11	adantr 270	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → (𝑠 +_Q 𝑦) = 𝑡)
13		simplrl 501	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → 𝑥 ∈ Q)
14		simplrr 502	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → (𝑥 +_Q 𝑥) <_Q 𝑦)
15		simprl 497	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → 𝑐 ∈ N)
16		simprr 498	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)
17	8, 10, 12, 13, 14, 15, 16	caucvgprprlemloccalc 6874	. . . . . . . 8 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩)
18		simplrl 501	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) → 𝑠 ∈ Q)
19	18	ad3antrrr 475	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → 𝑠 ∈ Q)
20		nnnq 6612	. . . . . . . . . . . . . 14 ⊢ (𝑐 ∈ N → [⟨𝑐, 1_𝑜⟩] ~_Q ∈ Q)
21	20	ad2antrl 473	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → [⟨𝑐, 1_𝑜⟩] ~_Q ∈ Q)
22		recclnq 6582	. . . . . . . . . . . . 13 ⊢ ([⟨𝑐, 1_𝑜⟩] ~_Q ∈ Q → (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) ∈ Q)
23	21, 22	syl 14	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) ∈ Q)
24		addclnq 6565	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ Q ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) ∈ Q) → (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) ∈ Q)
25	19, 23, 24	syl2anc 403	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) ∈ Q)
26		nqprlu 6737	. . . . . . . . . . 11 ⊢ ((𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) ∈ Q → ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ ∈ P)
27	25, 26	syl 14	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ ∈ P)
28		nqprlu 6737	. . . . . . . . . . 11 ⊢ ((_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) ∈ Q → ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩ ∈ P)
29	23, 28	syl 14	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩ ∈ P)
30		addclpr 6727	. . . . . . . . . 10 ⊢ ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ ∈ P ∧ ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩ ∈ P) → (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P)
31	27, 29, 30	syl2anc 403	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P)
32		simplrr 502	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) → 𝑡 ∈ Q)
33	32	ad3antrrr 475	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → 𝑡 ∈ Q)
34		nqprlu 6737	. . . . . . . . . 10 ⊢ (𝑡 ∈ Q → ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ ∈ P)
35	33, 34	syl 14	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ ∈ P)
36		caucvgprpr.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:N⟶P)
37	36	ad5antr 479	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → 𝐹:N⟶P)
38	37, 15	ffvelrnd 5324	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → (𝐹‘𝑐) ∈ P)
39		ltrelnq 6555	. . . . . . . . . . . . . 14 ⊢ <_Q ⊆ (Q × Q)
40	39	brel 4410	. . . . . . . . . . . . 13 ⊢ ((_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥 → ((_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) ∈ Q ∧ 𝑥 ∈ Q))
41	40	simpld 110	. . . . . . . . . . . 12 ⊢ ((_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥 → (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) ∈ Q)
42	41	ad2antll 474	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) ∈ Q)
43	42, 28	syl 14	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩ ∈ P)
44		addclpr 6727	. . . . . . . . . 10 ⊢ (((𝐹‘𝑐) ∈ P ∧ ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩ ∈ P) → ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P)
45	38, 43, 44	syl2anc 403	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P)
46		ltsopr 6786	. . . . . . . . . 10 ⊢ <_P Or P
47		sowlin 4075	. . . . . . . . . 10 ⊢ ((<_P Or P ∧ ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P ∧ ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ ∈ P ∧ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P)) → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩) ∨ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩)))
48	46, 47	mpan 414	. . . . . . . . 9 ⊢ (((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P ∧ ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ ∈ P ∧ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P) → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩) ∨ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩)))
49	31, 35, 45, 48	syl3anc 1169	. . . . . . . 8 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩) ∨ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩)))
50	17, 49	mpd 13	. . . . . . 7 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩) ∨ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩))
51	19	adantr 270	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)) → 𝑠 ∈ Q)
52		simplrl 501	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)) → 𝑐 ∈ N)
53		simpr 108	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)) → (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩))
54		ltaprg 6809	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P ∧ ℎ ∈ P) → (𝑓<_P 𝑔 ↔ (ℎ +_P 𝑓)<_P (ℎ +_P 𝑔)))
55	54	adantl 271	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)) ∧ (𝑓 ∈ P ∧ 𝑔 ∈ P ∧ ℎ ∈ P)) → (𝑓<_P 𝑔 ↔ (ℎ +_P 𝑓)<_P (ℎ +_P 𝑔)))
56	42	adantr 270	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)) → (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) ∈ Q)
57	51, 56, 24	syl2anc 403	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)) → (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) ∈ Q)
58	57, 26	syl 14	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)) → ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ ∈ P)
59	38	adantr 270	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)) → (𝐹‘𝑐) ∈ P)
60	56, 28	syl 14	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)) → ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩ ∈ P)
61		addcomprg 6768	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) → (𝑓 +_P 𝑔) = (𝑔 +_P 𝑓))
62	61	adantl 271	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)) ∧ (𝑓 ∈ P ∧ 𝑔 ∈ P)) → (𝑓 +_P 𝑔) = (𝑔 +_P 𝑓))
63	55, 58, 59, 60, 62	caovord2d 5690	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)) → (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑐) ↔ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)))
64	53, 63	mpbird 165	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)) → ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑐))
65		opeq1 3570	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑐 → ⟨𝑎, 1_𝑜⟩ = ⟨𝑐, 1_𝑜⟩)
66	65	eceq1d 6165	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑐 → [⟨𝑎, 1_𝑜⟩] ~_Q = [⟨𝑐, 1_𝑜⟩] ~_Q )
67	66	fveq2d 5202	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑐 → (_Q‘[⟨𝑎, 1_𝑜⟩] ~_Q ) = (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))
68	67	oveq2d 5548	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑐 → (𝑠 +_Q (_Q‘[⟨𝑎, 1_𝑜⟩] ~_Q )) = (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )))
69	68	breq2d 3797	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑐 → (𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_𝑜⟩] ~_Q )) ↔ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))))
70	69	abbidv 2196	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → {𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_𝑜⟩] ~_Q ))} = {𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))})
71	68	breq1d 3795	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑐 → ((𝑠 +_Q (_Q‘[⟨𝑎, 1_𝑜⟩] ~_Q )) <_Q 𝑞 ↔ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞))
72	71	abbidv 2196	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑎, 1_𝑜⟩] ~_Q )) <_Q 𝑞} = {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞})
73	70, 72	opeq12d 3578	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑎, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ = ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩)
74		fveq2 5198	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝐹‘𝑎) = (𝐹‘𝑐))
75	73, 74	breq12d 3798	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑎, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑎) ↔ ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑐)))
76	75	rspcev 2701	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ N ∧ ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑐)) → ∃𝑎 ∈ N ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑎, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑎))
77	52, 64, 76	syl2anc 403	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)) → ∃𝑎 ∈ N ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (*_Q‘[⟨𝑎, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑎))
78		caucvgprpr.lim	. . . . . . . . . . 11 ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N ⟨{𝑝 ∣ 𝑝 <_Q (𝑙 +_Q (_Q‘[⟨𝑟, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑙 +_Q (_Q‘[⟨𝑟, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑟, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑟, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑢}, {𝑞 ∣ 𝑢 <_Q 𝑞}⟩}⟩
79	78	caucvgprprlemell 6875	. . . . . . . . . 10 ⊢ (𝑠 ∈ (1^st ‘𝐿) ↔ (𝑠 ∈ Q ∧ ∃𝑎 ∈ N ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑎, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑎)))
80	51, 77, 79	sylanbrc 408	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)) → 𝑠 ∈ (1^st ‘𝐿))
81	80	ex 113	. . . . . . . 8 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩) → 𝑠 ∈ (1^st ‘𝐿)))
82	33	adantr 270	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) ∧ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩) → 𝑡 ∈ Q)
83		fveq2 5198	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑐 → (𝐹‘𝑏) = (𝐹‘𝑐))
84		opeq1 3570	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 𝑐 → ⟨𝑏, 1_𝑜⟩ = ⟨𝑐, 1_𝑜⟩)
85	84	eceq1d 6165	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑐 → [⟨𝑏, 1_𝑜⟩] ~_Q = [⟨𝑐, 1_𝑜⟩] ~_Q )
86	85	fveq2d 5202	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑐 → (_Q‘[⟨𝑏, 1_𝑜⟩] ~_Q ) = (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))
87	86	breq2d 3797	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑐 → (𝑝 <_Q (_Q‘[⟨𝑏, 1_𝑜⟩] ~_Q ) ↔ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )))
88	87	abbidv 2196	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → {𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_𝑜⟩] ~_Q )} = {𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )})
89	86	breq1d 3795	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑐 → ((_Q‘[⟨𝑏, 1_𝑜⟩] ~_Q ) <_Q 𝑞 ↔ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞))
90	89	abbidv 2196	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → {𝑞 ∣ (_Q‘[⟨𝑏, 1_𝑜⟩] ~_Q ) <_Q 𝑞} = {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞})
91	88, 90	opeq12d 3578	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑐 → ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑏, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩ = ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)
92	83, 91	oveq12d 5550	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑐 → ((𝐹‘𝑏) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑏, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩) = ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩))
93	92	breq1d 3795	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑐 → (((𝐹‘𝑏) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑏, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ ↔ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩))
94	93	rspcev 2701	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ N ∧ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩) → ∃𝑏 ∈ N ((𝐹‘𝑏) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑏, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩)
95	15, 94	sylan 277	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) ∧ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩) → ∃𝑏 ∈ N ((𝐹‘𝑏) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑏, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩)
96	78	caucvgprprlemelu 6876	. . . . . . . . . 10 ⊢ (𝑡 ∈ (2^nd ‘𝐿) ↔ (𝑡 ∈ Q ∧ ∃𝑏 ∈ N ((𝐹‘𝑏) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑏, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩))
97	82, 95, 96	sylanbrc 408	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) ∧ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩) → 𝑡 ∈ (2^nd ‘𝐿))
98	97	ex 113	. . . . . . . 8 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → (((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ → 𝑡 ∈ (2^nd ‘𝐿)))
99	81, 98	orim12d 732	. . . . . . 7 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → (((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩) ∨ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩) → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿))))
100	50, 99	mpd 13	. . . . . 6 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_𝑜⟩] ~_Q ) <_Q 𝑥)) → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿)))
101	6, 100	rexlimddv 2481	. . . . 5 ⊢ (((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿)))
102	4, 101	rexlimddv 2481	. . . 4 ⊢ ((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿)))
103	2, 102	rexlimddv 2481	. . 3 ⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿)))
104	103	ex 113	. 2 ⊢ ((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) → (𝑠 <_Q 𝑡 → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿))))
105	104	ralrimivva 2443	1 ⊢ (𝜑 → ∀𝑠 ∈ Q ∀𝑡 ∈ Q (𝑠 <_Q 𝑡 → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿))))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 102 ↔ wb 103 ∨ wo 661 ∧ w3a 919 = wceq 1284 ∈ wcel 1433 {cab 2067 ∀wral 2348 ∃wrex 2349 {crab 2352 ⟨cop 3401 class class class wbr 3785 Or wor 4050 ⟶wf 4918 ‘cfv 4922 (class class class)co 5532 1^st c1st 5785 2^nd c2nd 5786 1_𝑜c1o 6017 [cec 6127 Ncnpi 6462 <_N clti 6465 ~_Q ceq 6469 Qcnq 6470 +_Q cplq 6472 *_Qcrq 6474 <_Q cltq 6475 Pcnp 6481 +_P cpp 6483 <_P cltp 6485

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 576 ax-in2 577 ax-io 662 ax-5 1376 ax-7 1377 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-8 1435 ax-10 1436 ax-11 1437 ax-i12 1438 ax-bndl 1439 ax-4 1440 ax-13 1444 ax-14 1445 ax-17 1459 ax-i9 1463 ax-ial 1467 ax-i5r 1468 ax-ext 2063 ax-coll 3893 ax-sep 3896 ax-nul 3904 ax-pow 3948 ax-pr 3964 ax-un 4188 ax-setind 4280 ax-iinf 4329

This theorem depends on definitions: df-bi 115 df-dc 776 df-3or 920 df-3an 921 df-tru 1287 df-fal 1290 df-nf 1390 df-sb 1686 df-eu 1944 df-mo 1945 df-clab 2068 df-cleq 2074 df-clel 2077 df-nfc 2208 df-ne 2246 df-ral 2353 df-rex 2354 df-reu 2355 df-rab 2357 df-v 2603 df-sbc 2816 df-csb 2909 df-dif 2975 df-un 2977 df-in 2979 df-ss 2986 df-nul 3252 df-pw 3384 df-sn 3404 df-pr 3405 df-op 3407 df-uni 3602 df-int 3637 df-iun 3680 df-br 3786 df-opab 3840 df-mpt 3841 df-tr 3876 df-eprel 4044 df-id 4048 df-po 4051 df-iso 4052 df-iord 4121 df-on 4123 df-suc 4126 df-iom 4332 df-xp 4369 df-rel 4370 df-cnv 4371 df-co 4372 df-dm 4373 df-rn 4374 df-res 4375 df-ima 4376 df-iota 4887 df-fun 4924 df-fn 4925 df-f 4926 df-f1 4927 df-fo 4928 df-f1o 4929 df-fv 4930 df-ov 5535 df-oprab 5536 df-mpt2 5537 df-1st 5787 df-2nd 5788 df-recs 5943 df-irdg 5980 df-1o 6024 df-2o 6025 df-oadd 6028 df-omul 6029 df-er 6129 df-ec 6131 df-qs 6135 df-ni 6494 df-pli 6495 df-mi 6496 df-lti 6497 df-plpq 6534 df-mpq 6535 df-enq 6537 df-nqqs 6538 df-plqqs 6539 df-mqqs 6540 df-1nqqs 6541 df-rq 6542 df-ltnqqs 6543 df-enq0 6614 df-nq0 6615 df-0nq0 6616 df-plq0 6617 df-mq0 6618 df-inp 6656 df-iplp 6658 df-iltp 6660

This theorem is referenced by: caucvgprprlemcl 6894

W3C validator