caucvgprprlemloc - Intuitionistic Logic Explorer

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

Theorem caucvgprprlemloc 7815

Description: Lemma for caucvgprpr 7824. 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 7521	. . . . 5 ⊢ (𝑠 <_Q 𝑡 → ∃𝑦 ∈ Q (𝑠 +_Q 𝑦) = 𝑡)
2	1	adantl 277	. . . 4 ⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) → ∃𝑦 ∈ Q (𝑠 +_Q 𝑦) = 𝑡)
3		subhalfnqq 7526	. . . . . 6 ⊢ (𝑦 ∈ Q → ∃𝑥 ∈ Q (𝑥 +_Q 𝑥) <_Q 𝑦)
4	3	ad2antrl 490	. . . . 5 ⊢ ((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) → ∃𝑥 ∈ Q (𝑥 +_Q 𝑥) <_Q 𝑦)
5		archrecnq 7775	. . . . . . 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 7796	. . . . . . . 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 7534	. . . . . . . . . . . . . 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 7504	. . . . . . . . . . . . 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 7487	. . . . . . . . . . . 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 7659	. . . . . . . . . . 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 7659	. . . . . . . . . . 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 7649	. . . . . . . . . 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 7659	. . . . . . . . . 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 5715	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (𝐹‘𝑐) ∈ P)
39		ltrelnq 7477	. . . . . . . . . . . . . 14 ⊢ <_Q ⊆ (Q × Q)
40	39	brel 4726	. . . . . . . . . . . . 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 7649	. . . . . . . . . 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 7708	. . . . . . . . . 10 ⊢ <_P Or P
47		sowlin 4366	. . . . . . . . . 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 1249	. . . . . . . 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 7731	. . . . . . . . . . . . . 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 7690	. . . . . . . . . . . . . 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 6115	. . . . . . . . . . . 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 3818	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑐 → ⟨𝑎, 1_o⟩ = ⟨𝑐, 1_o⟩)
66	65	eceq1d 6655	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑐 → [⟨𝑎, 1_o⟩] ~_Q = [⟨𝑐, 1_o⟩] ~_Q )
67	66	fveq2d 5579	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑐 → (_Q‘[⟨𝑎, 1_o⟩] ~_Q ) = (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))
68	67	oveq2d 5959	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑐 → (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) = (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )))
69	68	breq2d 4055	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑐 → (𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ↔ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))))
70	69	abbidv 2322	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → {𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))} = {𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))})
71	68	breq1d 4053	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑐 → ((𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) <_Q 𝑞 ↔ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞))
72	71	abbidv 2322	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) <_Q 𝑞} = {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞})
73	70, 72	opeq12d 3826	. . . . . . . . . . . . 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 5575	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝐹‘𝑎) = (𝐹‘𝑐))
75	73, 74	breq12d 4056	. . . . . . . . . . . 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 2876	. . . . . . . . . . 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 7797	. . . . . . . . . 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 5575	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑐 → (𝐹‘𝑏) = (𝐹‘𝑐))
84		opeq1 3818	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 𝑐 → ⟨𝑏, 1_o⟩ = ⟨𝑐, 1_o⟩)
85	84	eceq1d 6655	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑐 → [⟨𝑏, 1_o⟩] ~_Q = [⟨𝑐, 1_o⟩] ~_Q )
86	85	fveq2d 5579	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑐 → (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) = (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))
87	86	breq2d 4055	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑐 → (𝑝 <_Q (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) ↔ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )))
88	87	abbidv 2322	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → {𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_o⟩] ~_Q )} = {𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )})
89	86	breq1d 4053	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑐 → ((_Q‘[⟨𝑏, 1_o⟩] ~_Q ) <_Q 𝑞 ↔ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞))
90	89	abbidv 2322	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → {𝑞 ∣ (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) <_Q 𝑞} = {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞})
91	88, 90	opeq12d 3826	. . . . . . . . . . . . . 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 5961	. . . . . . . . . . . . 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 4053	. . . . . . . . . . . 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 2876	. . . . . . . . . . 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 7798	. . . . . . . . . 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 787	. . . . . . 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 2627	. . . . 5 ⊢ (((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿)))
102	4, 101	rexlimddv 2627	. . . 4 ⊢ ((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿)))
103	2, 102	rexlimddv 2627	. . 3 ⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿)))
104	103	ex 115	. 2 ⊢ ((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) → (𝑠 <_Q 𝑡 → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿))))
105	104	ralrimivva 2587	1 ⊢ (𝜑 → ∀𝑠 ∈ Q ∀𝑡 ∈ Q (𝑠 <_Q 𝑡 → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿))))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 709 ∧ w3a 980 = wceq 1372 ∈ wcel 2175 {cab 2190 ∀wral 2483 ∃wrex 2484 {crab 2487 ⟨cop 3635 class class class wbr 4043 Or wor 4341 ⟶wf 5266 ‘cfv 5270 (class class class)co 5943 1^st c1st 6223 2^nd c2nd 6224 1_oc1o 6494 [cec 6617 Ncnpi 7384 <_N clti 7387 ~_Q ceq 7391 Qcnq 7392 +_Q cplq 7394 *_Qcrq 7396 <_Q cltq 7397 Pcnp 7403 +_P cpp 7405 <_P cltp 7407

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 615 ax-in2 616 ax-io 710 ax-5 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-13 2177 ax-14 2178 ax-ext 2186 ax-coll 4158 ax-sep 4161 ax-nul 4169 ax-pow 4217 ax-pr 4252 ax-un 4479 ax-setind 4584 ax-iinf 4635

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1375 df-fal 1378 df-nf 1483 df-sb 1785 df-eu 2056 df-mo 2057 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-ne 2376 df-ral 2488 df-rex 2489 df-reu 2490 df-rab 2492 df-v 2773 df-sbc 2998 df-csb 3093 df-dif 3167 df-un 3169 df-in 3171 df-ss 3178 df-nul 3460 df-pw 3617 df-sn 3638 df-pr 3639 df-op 3641 df-uni 3850 df-int 3885 df-iun 3928 df-br 4044 df-opab 4105 df-mpt 4106 df-tr 4142 df-eprel 4335 df-id 4339 df-po 4342 df-iso 4343 df-iord 4412 df-on 4414 df-suc 4417 df-iom 4638 df-xp 4680 df-rel 4681 df-cnv 4682 df-co 4683 df-dm 4684 df-rn 4685 df-res 4686 df-ima 4687 df-iota 5231 df-fun 5272 df-fn 5273 df-f 5274 df-f1 5275 df-fo 5276 df-f1o 5277 df-fv 5278 df-ov 5946 df-oprab 5947 df-mpo 5948 df-1st 6225 df-2nd 6226 df-recs 6390 df-irdg 6455 df-1o 6501 df-2o 6502 df-oadd 6505 df-omul 6506 df-er 6619 df-ec 6621 df-qs 6625 df-ni 7416 df-pli 7417 df-mi 7418 df-lti 7419 df-plpq 7456 df-mpq 7457 df-enq 7459 df-nqqs 7460 df-plqqs 7461 df-mqqs 7462 df-1nqqs 7463 df-rq 7464 df-ltnqqs 7465 df-enq0 7536 df-nq0 7537 df-0nq0 7538 df-plq0 7539 df-mq0 7540 df-inp 7578 df-iplp 7580 df-iltp 7582

This theorem is referenced by: caucvgprprlemcl 7816

W3C validator