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

Theorem caucvgprprlemlol 7470
 Description: Lemma for caucvgprpr 7484. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 21-Dec-2020.)
Hypotheses
Ref Expression
caucvgprpr.f (𝜑𝐹:NP)
caucvgprpr.cau (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩))))
caucvgprpr.bnd (𝜑 → ∀𝑚N 𝐴<P (𝐹𝑚))
caucvgprpr.lim 𝐿 = ⟨{𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}, {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}⟩
Assertion
Ref Expression
caucvgprprlemlol ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → 𝑠 ∈ (1st𝐿))
Distinct variable groups:   𝐴,𝑚   𝑚,𝐹   𝐹,𝑙   𝑢,𝐹,𝑟   𝑝,𝑙,𝑠   𝑞,𝑙,𝑠,𝑟   𝑡,𝑙,𝑝   𝑢,𝑞,𝑠,𝑟   𝑢,𝑝,𝑡,𝑟   𝜑,𝑟   𝑟,𝑞,𝑡
Allowed substitution hints:   𝜑(𝑢,𝑡,𝑘,𝑚,𝑛,𝑠,𝑞,𝑝,𝑙)   𝐴(𝑢,𝑡,𝑘,𝑛,𝑠,𝑟,𝑞,𝑝,𝑙)   𝐹(𝑡,𝑘,𝑛,𝑠,𝑞,𝑝)   𝐿(𝑢,𝑡,𝑘,𝑚,𝑛,𝑠,𝑟,𝑞,𝑝,𝑙)

Proof of Theorem caucvgprprlemlol
Dummy variables 𝑏 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltrelnq 7137 . . . . 5 <Q ⊆ (Q × Q)
21brel 4559 . . . 4 (𝑠 <Q 𝑡 → (𝑠Q𝑡Q))
32simpld 111 . . 3 (𝑠 <Q 𝑡𝑠Q)
433ad2ant2 986 . 2 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → 𝑠Q)
5 caucvgprpr.lim . . . . . . 7 𝐿 = ⟨{𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}, {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}⟩
65caucvgprprlemell 7457 . . . . . 6 (𝑡 ∈ (1st𝐿) ↔ (𝑡Q ∧ ∃𝑏N ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)))
76simprbi 271 . . . . 5 (𝑡 ∈ (1st𝐿) → ∃𝑏N ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏))
873ad2ant3 987 . . . 4 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → ∃𝑏N ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏))
9 simpll2 1004 . . . . . . . . 9 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → 𝑠 <Q 𝑡)
10 ltanqg 7172 . . . . . . . . . . 11 ((𝑥Q𝑦Q𝑧Q) → (𝑥 <Q 𝑦 ↔ (𝑧 +Q 𝑥) <Q (𝑧 +Q 𝑦)))
1110adantl 273 . . . . . . . . . 10 (((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) ∧ (𝑥Q𝑦Q𝑧Q)) → (𝑥 <Q 𝑦 ↔ (𝑧 +Q 𝑥) <Q (𝑧 +Q 𝑦)))
124ad2antrr 477 . . . . . . . . . 10 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → 𝑠Q)
132simprd 113 . . . . . . . . . . . 12 (𝑠 <Q 𝑡𝑡Q)
14133ad2ant2 986 . . . . . . . . . . 11 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → 𝑡Q)
1514ad2antrr 477 . . . . . . . . . 10 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → 𝑡Q)
16 simplr 502 . . . . . . . . . . 11 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → 𝑏N)
17 nnnq 7194 . . . . . . . . . . 11 (𝑏N → [⟨𝑏, 1o⟩] ~QQ)
18 recclnq 7164 . . . . . . . . . . 11 ([⟨𝑏, 1o⟩] ~QQ → (*Q‘[⟨𝑏, 1o⟩] ~Q ) ∈ Q)
1916, 17, 183syl 17 . . . . . . . . . 10 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → (*Q‘[⟨𝑏, 1o⟩] ~Q ) ∈ Q)
20 addcomnqg 7153 . . . . . . . . . . 11 ((𝑥Q𝑦Q) → (𝑥 +Q 𝑦) = (𝑦 +Q 𝑥))
2120adantl 273 . . . . . . . . . 10 (((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) ∧ (𝑥Q𝑦Q)) → (𝑥 +Q 𝑦) = (𝑦 +Q 𝑥))
2211, 12, 15, 19, 21caovord2d 5906 . . . . . . . . 9 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → (𝑠 <Q 𝑡 ↔ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))))
239, 22mpbid 146 . . . . . . . 8 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )))
24 ltnqpri 7366 . . . . . . . 8 ((𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) → ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩)
2523, 24syl 14 . . . . . . 7 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩)
26 ltsopr 7368 . . . . . . . 8 <P Or P
27 ltrelpr 7277 . . . . . . . 8 <P ⊆ (P × P)
2826, 27sotri 4902 . . . . . . 7 ((⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩ ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏))
2925, 28sylancom 414 . . . . . 6 ((((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) ∧ ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)) → ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏))
3029ex 114 . . . . 5 (((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) ∧ 𝑏N) → (⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏) → ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)))
3130reximdva 2509 . . . 4 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → (∃𝑏N ⟨{𝑝𝑝 <Q (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑡 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏) → ∃𝑏N ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏)))
328, 31mpd 13 . . 3 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → ∃𝑏N ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏))
33 opeq1 3673 . . . . . . . . . . 11 (𝑏 = 𝑟 → ⟨𝑏, 1o⟩ = ⟨𝑟, 1o⟩)
3433eceq1d 6431 . . . . . . . . . 10 (𝑏 = 𝑟 → [⟨𝑏, 1o⟩] ~Q = [⟨𝑟, 1o⟩] ~Q )
3534fveq2d 5391 . . . . . . . . 9 (𝑏 = 𝑟 → (*Q‘[⟨𝑏, 1o⟩] ~Q ) = (*Q‘[⟨𝑟, 1o⟩] ~Q ))
3635oveq2d 5756 . . . . . . . 8 (𝑏 = 𝑟 → (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) = (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )))
3736breq2d 3909 . . . . . . 7 (𝑏 = 𝑟 → (𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) ↔ 𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))))
3837abbidv 2233 . . . . . 6 (𝑏 = 𝑟 → {𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))} = {𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))})
3936breq1d 3907 . . . . . . 7 (𝑏 = 𝑟 → ((𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞 ↔ (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞))
4039abbidv 2233 . . . . . 6 (𝑏 = 𝑟 → {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞} = {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞})
4138, 40opeq12d 3681 . . . . 5 (𝑏 = 𝑟 → ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩)
42 fveq2 5387 . . . . 5 (𝑏 = 𝑟 → (𝐹𝑏) = (𝐹𝑟))
4341, 42breq12d 3910 . . . 4 (𝑏 = 𝑟 → (⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏) ↔ ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)))
4443cbvrexv 2630 . . 3 (∃𝑏N ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑏) ↔ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟))
4532, 44sylib 121 . 2 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → ∃𝑟N ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟))
465caucvgprprlemell 7457 . 2 (𝑠 ∈ (1st𝐿) ↔ (𝑠Q ∧ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑠 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)))
474, 45, 46sylanbrc 411 1 ((𝜑𝑠 <Q 𝑡𝑡 ∈ (1st𝐿)) → 𝑠 ∈ (1st𝐿))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 945   = wceq 1314   ∈ wcel 1463  {cab 2101  ∀wral 2391  ∃wrex 2392  {crab 2395  ⟨cop 3498   class class class wbr 3897  ⟶wf 5087  ‘cfv 5091  (class class class)co 5740  1st c1st 6002  1oc1o 6272  [cec 6393  Ncnpi 7044
 Copyright terms: Public domain W3C validator