caucvgprprlemloc - Intuitionistic Logic Explorer

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

Theorem caucvgprprlemloc 7719

Description: Lemma for caucvgprpr 7728. 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 7425	. . . . 5 ⊢ (𝑠 <_Q 𝑡 → ∃𝑦 ∈ Q (𝑠 +_Q 𝑦) = 𝑡)
2	1	adantl 277	. . . 4 ⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) → ∃𝑦 ∈ Q (𝑠 +_Q 𝑦) = 𝑡)
3		subhalfnqq 7430	. . . . . 6 ⊢ (𝑦 ∈ Q → ∃𝑥 ∈ Q (𝑥 +_Q 𝑥) <_Q 𝑦)
4	3	ad2antrl 490	. . . . 5 ⊢ ((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) → ∃𝑥 ∈ Q (𝑥 +_Q 𝑥) <_Q 𝑦)
5		archrecnq 7679	. . . . . . 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 7700	. . . . . . . 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 7438	. . . . . . . . . . . . . 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 7408	. . . . . . . . . . . . 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 7391	. . . . . . . . . . . 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 7563	. . . . . . . . . . 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 7563	. . . . . . . . . . 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 7553	. . . . . . . . . 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 7563	. . . . . . . . . 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 5667	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (𝐹‘𝑐) ∈ P)
39		ltrelnq 7381	. . . . . . . . . . . . . 14 ⊢ <_Q ⊆ (Q × Q)
40	39	brel 4692	. . . . . . . . . . . . 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 7553	. . . . . . . . . 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 7612	. . . . . . . . . 10 ⊢ <_P Or P
47		sowlin 4334	. . . . . . . . . 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 1248	. . . . . . . 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 7635	. . . . . . . . . . . . . 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 7594	. . . . . . . . . . . . . 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 6060	. . . . . . . . . . . 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 3792	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑐 → ⟨𝑎, 1_o⟩ = ⟨𝑐, 1_o⟩)
66	65	eceq1d 6588	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑐 → [⟨𝑎, 1_o⟩] ~_Q = [⟨𝑐, 1_o⟩] ~_Q )
67	66	fveq2d 5533	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑐 → (_Q‘[⟨𝑎, 1_o⟩] ~_Q ) = (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))
68	67	oveq2d 5906	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑐 → (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) = (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )))
69	68	breq2d 4029	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑐 → (𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ↔ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))))
70	69	abbidv 2306	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → {𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))} = {𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))})
71	68	breq1d 4027	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑐 → ((𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) <_Q 𝑞 ↔ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞))
72	71	abbidv 2306	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) <_Q 𝑞} = {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞})
73	70, 72	opeq12d 3800	. . . . . . . . . . . . 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 5529	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝐹‘𝑎) = (𝐹‘𝑐))
75	73, 74	breq12d 4030	. . . . . . . . . . . 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 2855	. . . . . . . . . . 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 7701	. . . . . . . . . 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 5529	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑐 → (𝐹‘𝑏) = (𝐹‘𝑐))
84		opeq1 3792	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 𝑐 → ⟨𝑏, 1_o⟩ = ⟨𝑐, 1_o⟩)
85	84	eceq1d 6588	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑐 → [⟨𝑏, 1_o⟩] ~_Q = [⟨𝑐, 1_o⟩] ~_Q )
86	85	fveq2d 5533	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑐 → (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) = (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))
87	86	breq2d 4029	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑐 → (𝑝 <_Q (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) ↔ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )))
88	87	abbidv 2306	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → {𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_o⟩] ~_Q )} = {𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )})
89	86	breq1d 4027	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑐 → ((_Q‘[⟨𝑏, 1_o⟩] ~_Q ) <_Q 𝑞 ↔ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞))
90	89	abbidv 2306	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → {𝑞 ∣ (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) <_Q 𝑞} = {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞})
91	88, 90	opeq12d 3800	. . . . . . . . . . . . . 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 5908	. . . . . . . . . . . . 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 4027	. . . . . . . . . . . 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 2855	. . . . . . . . . . 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 7702	. . . . . . . . . 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 2611	. . . . 5 ⊢ (((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿)))
102	4, 101	rexlimddv 2611	. . . 4 ⊢ ((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿)))
103	2, 102	rexlimddv 2611	. . 3 ⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿)))
104	103	ex 115	. 2 ⊢ ((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) → (𝑠 <_Q 𝑡 → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿))))
105	104	ralrimivva 2571	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 979 = wceq 1363 ∈ wcel 2159 {cab 2174 ∀wral 2467 ∃wrex 2468 {crab 2471 ⟨cop 3609 class class class wbr 4017 Or wor 4309 ⟶wf 5226 ‘cfv 5230 (class class class)co 5890 1^st c1st 6156 2^nd c2nd 6157 1_oc1o 6427 [cec 6550 Ncnpi 7288 <_N clti 7291 ~_Q ceq 7295 Qcnq 7296 +_Q cplq 7298 *_Qcrq 7300 <_Q cltq 7301 Pcnp 7307 +_P cpp 7309 <_P cltp 7311

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 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-13 2161 ax-14 2162 ax-ext 2170 ax-coll 4132 ax-sep 4135 ax-nul 4143 ax-pow 4188 ax-pr 4223 ax-un 4447 ax-setind 4550 ax-iinf 4601

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 980 df-3an 981 df-tru 1366 df-fal 1369 df-nf 1471 df-sb 1773 df-eu 2040 df-mo 2041 df-clab 2175 df-cleq 2181 df-clel 2184 df-nfc 2320 df-ne 2360 df-ral 2472 df-rex 2473 df-reu 2474 df-rab 2476 df-v 2753 df-sbc 2977 df-csb 3072 df-dif 3145 df-un 3147 df-in 3149 df-ss 3156 df-nul 3437 df-pw 3591 df-sn 3612 df-pr 3613 df-op 3615 df-uni 3824 df-int 3859 df-iun 3902 df-br 4018 df-opab 4079 df-mpt 4080 df-tr 4116 df-eprel 4303 df-id 4307 df-po 4310 df-iso 4311 df-iord 4380 df-on 4382 df-suc 4385 df-iom 4604 df-xp 4646 df-rel 4647 df-cnv 4648 df-co 4649 df-dm 4650 df-rn 4651 df-res 4652 df-ima 4653 df-iota 5192 df-fun 5232 df-fn 5233 df-f 5234 df-f1 5235 df-fo 5236 df-f1o 5237 df-fv 5238 df-ov 5893 df-oprab 5894 df-mpo 5895 df-1st 6158 df-2nd 6159 df-recs 6323 df-irdg 6388 df-1o 6434 df-2o 6435 df-oadd 6438 df-omul 6439 df-er 6552 df-ec 6554 df-qs 6558 df-ni 7320 df-pli 7321 df-mi 7322 df-lti 7323 df-plpq 7360 df-mpq 7361 df-enq 7363 df-nqqs 7364 df-plqqs 7365 df-mqqs 7366 df-1nqqs 7367 df-rq 7368 df-ltnqqs 7369 df-enq0 7440 df-nq0 7441 df-0nq0 7442 df-plq0 7443 df-mq0 7444 df-inp 7482 df-iplp 7484 df-iltp 7486

This theorem is referenced by: caucvgprprlemcl 7720

W3C validator