caucvgprlemopl - Intuitionistic Logic Explorer

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

Theorem caucvgprlemopl 6767

Description: Lemma for caucvgpr 6780. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.)

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

**Assertion**
Ref	Expression
caucvgprlemopl	⊢ ((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) → ∃𝑟 ∈ Q (𝑠 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐿)))

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

Proof of Theorem caucvgprlemopl Dummy variable 𝑡 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 5519	. . . . . . 7 ⊢ (𝑙 = 𝑠 → (𝑙 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) = (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )))
2	1	breq1d 3774	. . . . . 6 ⊢ (𝑙 = 𝑠 → ((𝑙 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗) ↔ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗)))
3	2	rexbidv 2327	. . . . 5 ⊢ (𝑙 = 𝑠 → (∃𝑗 ∈ N (𝑙 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗) ↔ ∃𝑗 ∈ N (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗)))
4		caucvgpr.lim	. . . . . . 7 ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑢}⟩
5	4	fveq2i 5181	. . . . . 6 ⊢ (1^st ‘𝐿) = (1^st ‘⟨{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑢}⟩)
6		nqex 6461	. . . . . . . 8 ⊢ Q ∈ V
7	6	rabex 3901	. . . . . . 7 ⊢ {𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +_Q (*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗)} ∈ V
8	6	rabex 3901	. . . . . . 7 ⊢ {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +_Q (*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑢} ∈ V
9	7, 8	op1st 5773	. . . . . 6 ⊢ (1^st ‘⟨{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑢}⟩) = {𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +_Q (*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗)}
10	5, 9	eqtri 2060	. . . . 5 ⊢ (1^st ‘𝐿) = {𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +_Q (*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗)}
11	3, 10	elrab2 2700	. . . 4 ⊢ (𝑠 ∈ (1^st ‘𝐿) ↔ (𝑠 ∈ Q ∧ ∃𝑗 ∈ N (𝑠 +_Q (*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗)))
12	11	simprbi 260	. . 3 ⊢ (𝑠 ∈ (1^st ‘𝐿) → ∃𝑗 ∈ N (𝑠 +_Q (*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))
13	12	adantl 262	. 2 ⊢ ((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) → ∃𝑗 ∈ N (𝑠 +_Q (*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))
14		simprr 484	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) → (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))
15		ltbtwnnqq 6513	. . . 4 ⊢ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗) ↔ ∃𝑡 ∈ Q ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))
16	14, 15	sylib 127	. . 3 ⊢ (((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) → ∃𝑡 ∈ Q ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))
17		simplrl 487	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) → 𝑗 ∈ N)
18		nnnq 6520	. . . . . . . . 9 ⊢ (𝑗 ∈ N → [⟨𝑗, 1_𝑜⟩] ~_Q ∈ Q)
19		recclnq 6490	. . . . . . . . 9 ⊢ ([⟨𝑗, 1_𝑜⟩] ~_Q ∈ Q → (*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) ∈ Q)
20	17, 18, 19	3syl 17	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) → (*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) ∈ Q)
21	11	simplbi 259	. . . . . . . . 9 ⊢ (𝑠 ∈ (1^st ‘𝐿) → 𝑠 ∈ Q)
22	21	ad3antlr 462	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) → 𝑠 ∈ Q)
23		ltaddnq 6505	. . . . . . . 8 ⊢ (((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) ∈ Q ∧ 𝑠 ∈ Q) → (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) <_Q ((*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑠))
24	20, 22, 23	syl2anc 391	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) → (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) <_Q ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑠))
25		addcomnqg 6479	. . . . . . . 8 ⊢ (((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) ∈ Q ∧ 𝑠 ∈ Q) → ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑠) = (𝑠 +_Q (*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )))
26	20, 22, 25	syl2anc 391	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) → ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑠) = (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )))
27	24, 26	breqtrd 3788	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) → (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) <_Q (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )))
28		simprrl 491	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) → (𝑠 +_Q (*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡)
29		ltsonq 6496	. . . . . . 7 ⊢ <_Q Or Q
30		ltrelnq 6463	. . . . . . 7 ⊢ <_Q ⊆ (Q × Q)
31	29, 30	sotri 4720	. . . . . 6 ⊢ (((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) <_Q (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡) → (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) <_Q 𝑡)
32	27, 28, 31	syl2anc 391	. . . . 5 ⊢ ((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) → (*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) <_Q 𝑡)
33		simprl 483	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) → 𝑡 ∈ Q)
34		ltexnqq 6506	. . . . . 6 ⊢ (((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) ∈ Q ∧ 𝑡 ∈ Q) → ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) <_Q 𝑡 ↔ ∃𝑟 ∈ Q ((*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡))
35	20, 33, 34	syl2anc 391	. . . . 5 ⊢ ((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) → ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) <_Q 𝑡 ↔ ∃𝑟 ∈ Q ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡))
36	32, 35	mpbid 135	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) → ∃𝑟 ∈ Q ((*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡)
37	22	ad2antrr 457	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) ∧ 𝑟 ∈ Q) ∧ ((*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡) → 𝑠 ∈ Q)
38	20	ad2antrr 457	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) ∧ 𝑟 ∈ Q) ∧ ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡) → (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) ∈ Q)
39		addcomnqg 6479	. . . . . . . . . . 11 ⊢ ((𝑠 ∈ Q ∧ (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) ∈ Q) → (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) = ((*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑠))
40	37, 38, 39	syl2anc 391	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) ∧ 𝑟 ∈ Q) ∧ ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡) → (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) = ((*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑠))
41	28	ad2antrr 457	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) ∧ 𝑟 ∈ Q) ∧ ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡) → (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡)
42	40, 41	eqbrtrrd 3786	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) ∧ 𝑟 ∈ Q) ∧ ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡) → ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑠) <_Q 𝑡)
43		simpr 103	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) ∧ 𝑟 ∈ Q) ∧ ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡) → ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡)
44	42, 43	breqtrrd 3790	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) ∧ 𝑟 ∈ Q) ∧ ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡) → ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑠) <_Q ((*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟))
45		simplr 482	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) ∧ 𝑟 ∈ Q) ∧ ((*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡) → 𝑟 ∈ Q)
46		ltanqg 6498	. . . . . . . . 9 ⊢ ((𝑠 ∈ Q ∧ 𝑟 ∈ Q ∧ (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) ∈ Q) → (𝑠 <_Q 𝑟 ↔ ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑠) <_Q ((*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟)))
47	37, 45, 38, 46	syl3anc 1135	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) ∧ 𝑟 ∈ Q) ∧ ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡) → (𝑠 <_Q 𝑟 ↔ ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑠) <_Q ((*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟)))
48	44, 47	mpbird 156	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) ∧ 𝑟 ∈ Q) ∧ ((*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡) → 𝑠 <_Q 𝑟)
49	17	ad2antrr 457	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) ∧ 𝑟 ∈ Q) ∧ ((*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡) → 𝑗 ∈ N)
50		simprrr 492	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) → 𝑡 <_Q (𝐹‘𝑗))
51	50	ad2antrr 457	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) ∧ 𝑟 ∈ Q) ∧ ((*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡) → 𝑡 <_Q (𝐹‘𝑗))
52		addcomnqg 6479	. . . . . . . . . . . . 13 ⊢ (((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) ∈ Q ∧ 𝑟 ∈ Q) → ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = (𝑟 +_Q (*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )))
53	38, 45, 52	syl2anc 391	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) ∧ 𝑟 ∈ Q) ∧ ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡) → ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = (𝑟 +_Q (*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )))
54	53, 43	eqtr3d 2074	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) ∧ 𝑟 ∈ Q) ∧ ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡) → (𝑟 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) = 𝑡)
55	54	breq1d 3774	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) ∧ 𝑟 ∈ Q) ∧ ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡) → ((𝑟 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗) ↔ 𝑡 <_Q (𝐹‘𝑗)))
56	51, 55	mpbird 156	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) ∧ 𝑟 ∈ Q) ∧ ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡) → (𝑟 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))
57		rspe 2370	. . . . . . . . 9 ⊢ ((𝑗 ∈ N ∧ (𝑟 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗)) → ∃𝑗 ∈ N (𝑟 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))
58	49, 56, 57	syl2anc 391	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) ∧ 𝑟 ∈ Q) ∧ ((_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡) → ∃𝑗 ∈ N (𝑟 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))
59		oveq1 5519	. . . . . . . . . . 11 ⊢ (𝑙 = 𝑟 → (𝑙 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) = (𝑟 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )))
60	59	breq1d 3774	. . . . . . . . . 10 ⊢ (𝑙 = 𝑟 → ((𝑙 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗) ↔ (𝑟 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗)))
61	60	rexbidv 2327	. . . . . . . . 9 ⊢ (𝑙 = 𝑟 → (∃𝑗 ∈ N (𝑙 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗) ↔ ∃𝑗 ∈ N (𝑟 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗)))
62	61, 10	elrab2 2700	. . . . . . . 8 ⊢ (𝑟 ∈ (1^st ‘𝐿) ↔ (𝑟 ∈ Q ∧ ∃𝑗 ∈ N (𝑟 +_Q (*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗)))
63	45, 58, 62	sylanbrc 394	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) ∧ 𝑟 ∈ Q) ∧ ((*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡) → 𝑟 ∈ (1^st ‘𝐿))
64	48, 63	jca 290	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) ∧ 𝑟 ∈ Q) ∧ ((*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡) → (𝑠 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐿)))
65	64	ex 108	. . . . 5 ⊢ (((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) ∧ 𝑟 ∈ Q) → (((*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡 → (𝑠 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐿))))
66	65	reximdva 2421	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) → (∃𝑟 ∈ Q ((*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q ) +_Q 𝑟) = 𝑡 → ∃𝑟 ∈ Q (𝑠 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐿))))
67	36, 66	mpd 13	. . 3 ⊢ ((((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) ∧ (𝑡 ∈ Q ∧ ((𝑠 +_Q (_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q 𝑡 ∧ 𝑡 <_Q (𝐹‘𝑗)))) → ∃𝑟 ∈ Q (𝑠 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐿)))
68	16, 67	rexlimddv 2437	. 2 ⊢ (((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) ∧ (𝑗 ∈ N ∧ (𝑠 +_Q (*_Q‘[⟨𝑗, 1_𝑜⟩] ~_Q )) <_Q (𝐹‘𝑗))) → ∃𝑟 ∈ Q (𝑠 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐿)))
69	13, 68	rexlimddv 2437	1 ⊢ ((𝜑 ∧ 𝑠 ∈ (1^st ‘𝐿)) → ∃𝑟 ∈ Q (𝑠 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐿)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 = wceq 1243 ∈ wcel 1393 ∀wral 2306 ∃wrex 2307 {crab 2310 ⟨cop 3378 class class class wbr 3764 ⟶wf 4898 ‘cfv 4902 (class class class)co 5512 1^st c1st 5765 1_𝑜c1o 5994 [cec 6104 Ncnpi 6370 <_N clti 6373 ~_Q ceq 6377 Qcnq 6378 +_Q cplq 6380 *_Qcrq 6382 <_Q cltq 6383

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-13 1404 ax-14 1405 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 ax-coll 3872 ax-sep 3875 ax-nul 3883 ax-pow 3927 ax-pr 3944 ax-un 4170 ax-setind 4262 ax-iinf 4311

This theorem depends on definitions: df-bi 110 df-dc 743 df-3or 886 df-3an 887 df-tru 1246 df-fal 1249 df-nf 1350 df-sb 1646 df-eu 1903 df-mo 1904 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-ne 2206 df-ral 2311 df-rex 2312 df-reu 2313 df-rab 2315 df-v 2559 df-sbc 2765 df-csb 2853 df-dif 2920 df-un 2922 df-in 2924 df-ss 2931 df-nul 3225 df-pw 3361 df-sn 3381 df-pr 3382 df-op 3384 df-uni 3581 df-int 3616 df-iun 3659 df-br 3765 df-opab 3819 df-mpt 3820 df-tr 3855 df-eprel 4026 df-id 4030 df-po 4033 df-iso 4034 df-iord 4103 df-on 4105 df-suc 4108 df-iom 4314 df-xp 4351 df-rel 4352 df-cnv 4353 df-co 4354 df-dm 4355 df-rn 4356 df-res 4357 df-ima 4358 df-iota 4867 df-fun 4904 df-fn 4905 df-f 4906 df-f1 4907 df-fo 4908 df-f1o 4909 df-fv 4910 df-ov 5515 df-oprab 5516 df-mpt2 5517 df-1st 5767 df-2nd 5768 df-recs 5920 df-irdg 5957 df-1o 6001 df-oadd 6005 df-omul 6006 df-er 6106 df-ec 6108 df-qs 6112 df-ni 6402 df-pli 6403 df-mi 6404 df-lti 6405 df-plpq 6442 df-mpq 6443 df-enq 6445 df-nqqs 6446 df-plqqs 6447 df-mqqs 6448 df-1nqqs 6449 df-rq 6450 df-ltnqqs 6451

This theorem is referenced by: caucvgprlemrnd 6771

W3C validator