caucvgprprlemloc - Intuitionistic Logic Explorer

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

Theorem caucvgprprlemloc 7913

Description: Lemma for caucvgprpr 7922. 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_o⟩] ~_Q )}, {𝑢 ∣ (_Q‘[⟨𝑛, 1_o⟩] ~_Q ) <_Q 𝑢}⟩) ∧ (𝐹‘𝑘)<_P ((𝐹‘𝑛) +_P ⟨{𝑙 ∣ 𝑙 <_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )}, {𝑢 ∣ (_Q‘[⟨𝑛, 1_o⟩] ~_Q ) <_Q 𝑢}⟩))))
caucvgprpr.bnd	⊢ (𝜑 → ∀𝑚 ∈ N 𝐴<_P (𝐹‘𝑚))
caucvgprpr.lim	⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N ⟨{𝑝 ∣ 𝑝 <_Q (𝑙 +_Q (_Q‘[⟨𝑟, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑙 +_Q (_Q‘[⟨𝑟, 1_o⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑟, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑟, 1_o⟩] ~_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 7619	. . . . 5 ⊢ (𝑠 <_Q 𝑡 → ∃𝑦 ∈ Q (𝑠 +_Q 𝑦) = 𝑡)
2	1	adantl 277	. . . 4 ⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) → ∃𝑦 ∈ Q (𝑠 +_Q 𝑦) = 𝑡)
3		subhalfnqq 7624	. . . . . 6 ⊢ (𝑦 ∈ Q → ∃𝑥 ∈ Q (𝑥 +_Q 𝑥) <_Q 𝑦)
4	3	ad2antrl 490	. . . . 5 ⊢ ((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) → ∃𝑥 ∈ Q (𝑥 +_Q 𝑥) <_Q 𝑦)
5		archrecnq 7873	. . . . . . 7 ⊢ (𝑥 ∈ Q → ∃𝑐 ∈ N (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)
6	5	ad2antrl 490	. . . . . 6 ⊢ (((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) → ∃𝑐 ∈ N (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)
7		simpllr 534	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) → 𝑠 <_Q 𝑡)
8	7	adantr 276	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → 𝑠 <_Q 𝑡)
9		simplrl 535	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) → 𝑦 ∈ Q)
10	9	adantr 276	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → 𝑦 ∈ Q)
11		simplrr 536	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) → (𝑠 +_Q 𝑦) = 𝑡)
12	11	adantr 276	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (𝑠 +_Q 𝑦) = 𝑡)
13		simplrl 535	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → 𝑥 ∈ Q)
14		simplrr 536	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (𝑥 +_Q 𝑥) <_Q 𝑦)
15		simprl 529	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → 𝑐 ∈ N)
16		simprr 531	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)
17	8, 10, 12, 13, 14, 15, 16	caucvgprprlemloccalc 7894	. . . . . . . 8 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩)
18		simplrl 535	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) → 𝑠 ∈ Q)
19	18	ad3antrrr 492	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → 𝑠 ∈ Q)
20		nnnq 7632	. . . . . . . . . . . . . 14 ⊢ (𝑐 ∈ N → [⟨𝑐, 1_o⟩] ~_Q ∈ Q)
21	20	ad2antrl 490	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → [⟨𝑐, 1_o⟩] ~_Q ∈ Q)
22		recclnq 7602	. . . . . . . . . . . . 13 ⊢ ([⟨𝑐, 1_o⟩] ~_Q ∈ Q → (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) ∈ Q)
23	21, 22	syl 14	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) ∈ Q)
24		addclnq 7585	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ Q ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) ∈ Q) → (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) ∈ Q)
25	19, 23, 24	syl2anc 411	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) ∈ Q)
26		nqprlu 7757	. . . . . . . . . . 11 ⊢ ((𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) ∈ Q → ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (*_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ ∈ P)
27	25, 26	syl 14	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (*_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ ∈ P)
28		nqprlu 7757	. . . . . . . . . . 11 ⊢ ((_Q‘[⟨𝑐, 1_o⟩] ~_Q ) ∈ Q → ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩ ∈ P)
29	23, 28	syl 14	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩ ∈ P)
30		addclpr 7747	. . . . . . . . . 10 ⊢ ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ ∈ P ∧ ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩ ∈ P) → (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P)
31	27, 29, 30	syl2anc 411	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P)
32		simplrr 536	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) → 𝑡 ∈ Q)
33	32	ad3antrrr 492	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → 𝑡 ∈ Q)
34		nqprlu 7757	. . . . . . . . . 10 ⊢ (𝑡 ∈ Q → ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ ∈ P)
35	33, 34	syl 14	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ ∈ P)
36		caucvgprpr.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:N⟶P)
37	36	ad5antr 496	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → 𝐹:N⟶P)
38	37, 15	ffvelcdmd 5779	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (𝐹‘𝑐) ∈ P)
39		ltrelnq 7575	. . . . . . . . . . . . . 14 ⊢ <_Q ⊆ (Q × Q)
40	39	brel 4776	. . . . . . . . . . . . 13 ⊢ ((_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥 → ((_Q‘[⟨𝑐, 1_o⟩] ~_Q ) ∈ Q ∧ 𝑥 ∈ Q))
41	40	simpld 112	. . . . . . . . . . . 12 ⊢ ((_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥 → (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) ∈ Q)
42	41	ad2antll 491	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) ∈ Q)
43	42, 28	syl 14	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩ ∈ P)
44		addclpr 7747	. . . . . . . . . 10 ⊢ (((𝐹‘𝑐) ∈ P ∧ ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩ ∈ P) → ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P)
45	38, 43, 44	syl2anc 411	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P)
46		ltsopr 7806	. . . . . . . . . 10 ⊢ <_P Or P
47		sowlin 4415	. . . . . . . . . 10 ⊢ ((<_P Or P ∧ ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P ∧ ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ ∈ P ∧ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P)) → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∨ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩)))
48	46, 47	mpan 424	. . . . . . . . 9 ⊢ (((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P ∧ ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ ∈ P ∧ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P) → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∨ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩)))
49	31, 35, 45, 48	syl3anc 1271	. . . . . . . 8 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∨ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩)))
50	17, 49	mpd 13	. . . . . . 7 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∨ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩))
51	19	adantr 276	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → 𝑠 ∈ Q)
52		simplrl 535	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → 𝑐 ∈ N)
53		simpr 110	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩))
54		ltaprg 7829	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P ∧ ℎ ∈ P) → (𝑓<_P 𝑔 ↔ (ℎ +_P 𝑓)<_P (ℎ +_P 𝑔)))
55	54	adantl 277	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) ∧ (𝑓 ∈ P ∧ 𝑔 ∈ P ∧ ℎ ∈ P)) → (𝑓<_P 𝑔 ↔ (ℎ +_P 𝑓)<_P (ℎ +_P 𝑔)))
56	42	adantr 276	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) ∈ Q)
57	51, 56, 24	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) ∈ Q)
58	57, 26	syl 14	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (*_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ ∈ P)
59	38	adantr 276	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → (𝐹‘𝑐) ∈ P)
60	56, 28	syl 14	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩ ∈ P)
61		addcomprg 7788	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) → (𝑓 +_P 𝑔) = (𝑔 +_P 𝑓))
62	61	adantl 277	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) ∧ (𝑓 ∈ P ∧ 𝑔 ∈ P)) → (𝑓 +_P 𝑔) = (𝑔 +_P 𝑓))
63	55, 58, 59, 60, 62	caovord2d 6187	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑐) ↔ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)))
64	53, 63	mpbird 167	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (*_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑐))
65		opeq1 3860	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑐 → ⟨𝑎, 1_o⟩ = ⟨𝑐, 1_o⟩)
66	65	eceq1d 6733	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑐 → [⟨𝑎, 1_o⟩] ~_Q = [⟨𝑐, 1_o⟩] ~_Q )
67	66	fveq2d 5639	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑐 → (_Q‘[⟨𝑎, 1_o⟩] ~_Q ) = (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))
68	67	oveq2d 6029	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑐 → (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) = (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )))
69	68	breq2d 4098	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑐 → (𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ↔ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))))
70	69	abbidv 2347	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → {𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))} = {𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))})
71	68	breq1d 4096	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑐 → ((𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) <_Q 𝑞 ↔ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞))
72	71	abbidv 2347	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) <_Q 𝑞} = {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞})
73	70, 72	opeq12d 3868	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ = ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩)
74		fveq2 5635	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝐹‘𝑎) = (𝐹‘𝑐))
75	73, 74	breq12d 4099	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑎) ↔ ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑐)))
76	75	rspcev 2908	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ N ∧ ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑐)) → ∃𝑎 ∈ N ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑎))
77	52, 64, 76	syl2anc 411	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → ∃𝑎 ∈ N ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (*_Q‘[⟨𝑎, 1_o⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑎))
78		caucvgprpr.lim	. . . . . . . . . . 11 ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N ⟨{𝑝 ∣ 𝑝 <_Q (𝑙 +_Q (_Q‘[⟨𝑟, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑙 +_Q (_Q‘[⟨𝑟, 1_o⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑟, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑟, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑢}, {𝑞 ∣ 𝑢 <_Q 𝑞}⟩}⟩
79	78	caucvgprprlemell 7895	. . . . . . . . . 10 ⊢ (𝑠 ∈ (1^st ‘𝐿) ↔ (𝑠 ∈ Q ∧ ∃𝑎 ∈ N ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑎)))
80	51, 77, 79	sylanbrc 417	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → 𝑠 ∈ (1^st ‘𝐿))
81	80	ex 115	. . . . . . . 8 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) → 𝑠 ∈ (1^st ‘𝐿)))
82	33	adantr 276	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩) → 𝑡 ∈ Q)
83		fveq2 5635	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑐 → (𝐹‘𝑏) = (𝐹‘𝑐))
84		opeq1 3860	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 𝑐 → ⟨𝑏, 1_o⟩ = ⟨𝑐, 1_o⟩)
85	84	eceq1d 6733	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑐 → [⟨𝑏, 1_o⟩] ~_Q = [⟨𝑐, 1_o⟩] ~_Q )
86	85	fveq2d 5639	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑐 → (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) = (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))
87	86	breq2d 4098	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑐 → (𝑝 <_Q (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) ↔ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )))
88	87	abbidv 2347	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → {𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_o⟩] ~_Q )} = {𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )})
89	86	breq1d 4096	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑐 → ((_Q‘[⟨𝑏, 1_o⟩] ~_Q ) <_Q 𝑞 ↔ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞))
90	89	abbidv 2347	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → {𝑞 ∣ (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) <_Q 𝑞} = {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞})
91	88, 90	opeq12d 3868	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑐 → ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) <_Q 𝑞}⟩ = ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)
92	83, 91	oveq12d 6031	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑐 → ((𝐹‘𝑏) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) = ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩))
93	92	breq1d 4096	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑐 → (((𝐹‘𝑏) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ ↔ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩))
94	93	rspcev 2908	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ N ∧ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩) → ∃𝑏 ∈ N ((𝐹‘𝑏) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩)
95	15, 94	sylan 283	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩) → ∃𝑏 ∈ N ((𝐹‘𝑏) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑏, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩)
96	78	caucvgprprlemelu 7896	. . . . . . . . . 10 ⊢ (𝑡 ∈ (2^nd ‘𝐿) ↔ (𝑡 ∈ Q ∧ ∃𝑏 ∈ N ((𝐹‘𝑏) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩))
97	82, 95, 96	sylanbrc 417	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩) → 𝑡 ∈ (2^nd ‘𝐿))
98	97	ex 115	. . . . . . . 8 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ → 𝑡 ∈ (2^nd ‘𝐿)))
99	81, 98	orim12d 791	. . . . . . 7 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∨ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_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_o⟩] ~_Q ) <_Q 𝑥)) → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿)))
101	6, 100	rexlimddv 2653	. . . . 5 ⊢ (((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿)))
102	4, 101	rexlimddv 2653	. . . 4 ⊢ ((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿)))
103	2, 102	rexlimddv 2653	. . 3 ⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿)))
104	103	ex 115	. 2 ⊢ ((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) → (𝑠 <_Q 𝑡 → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿))))
105	104	ralrimivva 2612	1 ⊢ (𝜑 → ∀𝑠 ∈ Q ∀𝑡 ∈ Q (𝑠 <_Q 𝑡 → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿))))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 713 ∧ w3a 1002 = wceq 1395 ∈ wcel 2200 {cab 2215 ∀wral 2508 ∃wrex 2509 {crab 2512 ⟨cop 3670 class class class wbr 4086 Or wor 4390 ⟶wf 5320 ‘cfv 5324 (class class class)co 6013 1^st c1st 6296 2^nd c2nd 6297 1_oc1o 6570 [cec 6695 Ncnpi 7482 <_N clti 7485 ~_Q ceq 7489 Qcnq 7490 +_Q cplq 7492 *_Qcrq 7494 <_Q cltq 7495 Pcnp 7501 +_P cpp 7503 <_P cltp 7505

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 4202 ax-sep 4205 ax-nul 4213 ax-pow 4262 ax-pr 4297 ax-un 4528 ax-setind 4633 ax-iinf 4684

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 2802 df-sbc 3030 df-csb 3126 df-dif 3200 df-un 3202 df-in 3204 df-ss 3211 df-nul 3493 df-pw 3652 df-sn 3673 df-pr 3674 df-op 3676 df-uni 3892 df-int 3927 df-iun 3970 df-br 4087 df-opab 4149 df-mpt 4150 df-tr 4186 df-eprel 4384 df-id 4388 df-po 4391 df-iso 4392 df-iord 4461 df-on 4463 df-suc 4466 df-iom 4687 df-xp 4729 df-rel 4730 df-cnv 4731 df-co 4732 df-dm 4733 df-rn 4734 df-res 4735 df-ima 4736 df-iota 5284 df-fun 5326 df-fn 5327 df-f 5328 df-f1 5329 df-fo 5330 df-f1o 5331 df-fv 5332 df-ov 6016 df-oprab 6017 df-mpo 6018 df-1st 6298 df-2nd 6299 df-recs 6466 df-irdg 6531 df-1o 6577 df-2o 6578 df-oadd 6581 df-omul 6582 df-er 6697 df-ec 6699 df-qs 6703 df-ni 7514 df-pli 7515 df-mi 7516 df-lti 7517 df-plpq 7554 df-mpq 7555 df-enq 7557 df-nqqs 7558 df-plqqs 7559 df-mqqs 7560 df-1nqqs 7561 df-rq 7562 df-ltnqqs 7563 df-enq0 7634 df-nq0 7635 df-0nq0 7636 df-plq0 7637 df-mq0 7638 df-inp 7676 df-iplp 7678 df-iltp 7680

This theorem is referenced by: caucvgprprlemcl 7914

W3C validator