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

Theorem caucvgprprlemopu 7551
 Description: Lemma for caucvgprpr 7564. The upper cut of the putative limit is open. (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
caucvgprprlemopu ((𝜑𝑡 ∈ (2nd𝐿)) → ∃𝑠Q (𝑠 <Q 𝑡𝑠 ∈ (2nd𝐿)))
Distinct variable groups:   𝐴,𝑚   𝑚,𝐹   𝐹,𝑙,𝑟,𝑠   𝑢,𝐹,𝑟,𝑠   𝐿,𝑠   𝑝,𝑙,𝑞,𝑡,𝑟,𝑠   𝑢,𝑝,𝑞,𝑡   𝜑,𝑟,𝑠
Allowed substitution hints:   𝜑(𝑢,𝑡,𝑘,𝑚,𝑛,𝑞,𝑝,𝑙)   𝐴(𝑢,𝑡,𝑘,𝑛,𝑠,𝑟,𝑞,𝑝,𝑙)   𝐹(𝑡,𝑘,𝑛,𝑞,𝑝)   𝐿(𝑢,𝑡,𝑘,𝑚,𝑛,𝑟,𝑞,𝑝,𝑙)

Proof of Theorem caucvgprprlemopu
Dummy variable 𝑏 is distinct from all other variables.
StepHypRef Expression
1 caucvgprpr.lim . . . . 5 𝐿 = ⟨{𝑙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 𝑞}⟩}⟩
21caucvgprprlemelu 7538 . . . 4 (𝑡 ∈ (2nd𝐿) ↔ (𝑡Q ∧ ∃𝑏N ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩))
32simprbi 273 . . 3 (𝑡 ∈ (2nd𝐿) → ∃𝑏N ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)
43adantl 275 . 2 ((𝜑𝑡 ∈ (2nd𝐿)) → ∃𝑏N ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)
5 simprr 522 . . . . 5 (((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) → ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)
6 caucvgprpr.f . . . . . . . . 9 (𝜑𝐹:NP)
76ffvelrnda 5564 . . . . . . . 8 ((𝜑𝑏N) → (𝐹𝑏) ∈ P)
8 recnnpr 7400 . . . . . . . . 9 (𝑏N → ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩ ∈ P)
98adantl 275 . . . . . . . 8 ((𝜑𝑏N) → ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩ ∈ P)
10 addclpr 7389 . . . . . . . 8 (((𝐹𝑏) ∈ P ∧ ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩ ∈ P) → ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) ∈ P)
117, 9, 10syl2anc 409 . . . . . . 7 ((𝜑𝑏N) → ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) ∈ P)
1211ad2ant2r 501 . . . . . 6 (((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) → ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) ∈ P)
132simplbi 272 . . . . . . . 8 (𝑡 ∈ (2nd𝐿) → 𝑡Q)
1413ad2antlr 481 . . . . . . 7 (((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) → 𝑡Q)
15 nqprlu 7399 . . . . . . 7 (𝑡Q → ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩ ∈ P)
1614, 15syl 14 . . . . . 6 (((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) → ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩ ∈ P)
17 ltdfpr 7358 . . . . . 6 ((((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) ∈ P ∧ ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩ ∈ P) → (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩ ↔ ∃𝑠Q (𝑠 ∈ (2nd ‘((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)) ∧ 𝑠 ∈ (1st ‘⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩))))
1812, 16, 17syl2anc 409 . . . . 5 (((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) → (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩ ↔ ∃𝑠Q (𝑠 ∈ (2nd ‘((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)) ∧ 𝑠 ∈ (1st ‘⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩))))
195, 18mpbid 146 . . . 4 (((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) → ∃𝑠Q (𝑠 ∈ (2nd ‘((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)) ∧ 𝑠 ∈ (1st ‘⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)))
20 simpr 109 . . . . . . . 8 ((((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) ∧ 𝑠Q) → 𝑠Q)
2112adantr 274 . . . . . . . 8 ((((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) ∧ 𝑠Q) → ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) ∈ P)
22 nqpru 7404 . . . . . . . 8 ((𝑠Q ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) ∈ P) → (𝑠 ∈ (2nd ‘((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)) ↔ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩))
2320, 21, 22syl2anc 409 . . . . . . 7 ((((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) ∧ 𝑠Q) → (𝑠 ∈ (2nd ‘((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)) ↔ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩))
24 vex 2693 . . . . . . . . 9 𝑠 ∈ V
25 breq1 3941 . . . . . . . . 9 (𝑝 = 𝑠 → (𝑝 <Q 𝑡𝑠 <Q 𝑡))
26 ltnqex 7401 . . . . . . . . . 10 {𝑝𝑝 <Q 𝑡} ∈ V
27 gtnqex 7402 . . . . . . . . . 10 {𝑞𝑡 <Q 𝑞} ∈ V
2826, 27op1st 6053 . . . . . . . . 9 (1st ‘⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩) = {𝑝𝑝 <Q 𝑡}
2924, 25, 28elab2 2837 . . . . . . . 8 (𝑠 ∈ (1st ‘⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩) ↔ 𝑠 <Q 𝑡)
3029a1i 9 . . . . . . 7 ((((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) ∧ 𝑠Q) → (𝑠 ∈ (1st ‘⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩) ↔ 𝑠 <Q 𝑡))
3123, 30anbi12d 465 . . . . . 6 ((((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) ∧ 𝑠Q) → ((𝑠 ∈ (2nd ‘((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)) ∧ 𝑠 ∈ (1st ‘⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) ↔ (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩ ∧ 𝑠 <Q 𝑡)))
3231biimpd 143 . . . . 5 ((((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) ∧ 𝑠Q) → ((𝑠 ∈ (2nd ‘((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)) ∧ 𝑠 ∈ (1st ‘⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) → (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩ ∧ 𝑠 <Q 𝑡)))
3332reximdva 2538 . . . 4 (((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) → (∃𝑠Q (𝑠 ∈ (2nd ‘((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)) ∧ 𝑠 ∈ (1st ‘⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) → ∃𝑠Q (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩ ∧ 𝑠 <Q 𝑡)))
3419, 33mpd 13 . . 3 (((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) → ∃𝑠Q (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩ ∧ 𝑠 <Q 𝑡))
35 simprr 522 . . . . . 6 (((((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) ∧ 𝑠Q) ∧ (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩ ∧ 𝑠 <Q 𝑡)) → 𝑠 <Q 𝑡)
36 simplr 520 . . . . . . 7 (((((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) ∧ 𝑠Q) ∧ (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩ ∧ 𝑠 <Q 𝑡)) → 𝑠Q)
37 simplrl 525 . . . . . . . . 9 ((((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) ∧ 𝑠Q) → 𝑏N)
3837adantr 274 . . . . . . . 8 (((((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) ∧ 𝑠Q) ∧ (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩ ∧ 𝑠 <Q 𝑡)) → 𝑏N)
39 simprl 521 . . . . . . . 8 (((((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) ∧ 𝑠Q) ∧ (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩ ∧ 𝑠 <Q 𝑡)) → ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩)
40 fveq2 5430 . . . . . . . . . . 11 (𝑟 = 𝑏 → (𝐹𝑟) = (𝐹𝑏))
41 opeq1 3714 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑏 → ⟨𝑟, 1o⟩ = ⟨𝑏, 1o⟩)
4241eceq1d 6474 . . . . . . . . . . . . . . 15 (𝑟 = 𝑏 → [⟨𝑟, 1o⟩] ~Q = [⟨𝑏, 1o⟩] ~Q )
4342fveq2d 5434 . . . . . . . . . . . . . 14 (𝑟 = 𝑏 → (*Q‘[⟨𝑟, 1o⟩] ~Q ) = (*Q‘[⟨𝑏, 1o⟩] ~Q ))
4443breq2d 3950 . . . . . . . . . . . . 13 (𝑟 = 𝑏 → (𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q ) ↔ 𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )))
4544abbidv 2258 . . . . . . . . . . . 12 (𝑟 = 𝑏 → {𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )} = {𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )})
4643breq1d 3948 . . . . . . . . . . . . 13 (𝑟 = 𝑏 → ((*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞 ↔ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞))
4746abbidv 2258 . . . . . . . . . . . 12 (𝑟 = 𝑏 → {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞} = {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞})
4845, 47opeq12d 3722 . . . . . . . . . . 11 (𝑟 = 𝑏 → ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)
4940, 48oveq12d 5801 . . . . . . . . . 10 (𝑟 = 𝑏 → ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩) = ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩))
5049breq1d 3948 . . . . . . . . 9 (𝑟 = 𝑏 → (((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩ ↔ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩))
5150rspcev 2794 . . . . . . . 8 ((𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩) → ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩)
5238, 39, 51syl2anc 409 . . . . . . 7 (((((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) ∧ 𝑠Q) ∧ (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩ ∧ 𝑠 <Q 𝑡)) → ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩)
531caucvgprprlemelu 7538 . . . . . . 7 (𝑠 ∈ (2nd𝐿) ↔ (𝑠Q ∧ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩))
5436, 52, 53sylanbrc 414 . . . . . 6 (((((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) ∧ 𝑠Q) ∧ (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩ ∧ 𝑠 <Q 𝑡)) → 𝑠 ∈ (2nd𝐿))
5535, 54jca 304 . . . . 5 (((((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) ∧ 𝑠Q) ∧ (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩ ∧ 𝑠 <Q 𝑡)) → (𝑠 <Q 𝑡𝑠 ∈ (2nd𝐿)))
5655ex 114 . . . 4 ((((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) ∧ 𝑠Q) → ((((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩ ∧ 𝑠 <Q 𝑡) → (𝑠 <Q 𝑡𝑠 ∈ (2nd𝐿))))
5756reximdva 2538 . . 3 (((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) → (∃𝑠Q (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑠}, {𝑞𝑠 <Q 𝑞}⟩ ∧ 𝑠 <Q 𝑡) → ∃𝑠Q (𝑠 <Q 𝑡𝑠 ∈ (2nd𝐿))))
5834, 57mpd 13 . 2 (((𝜑𝑡 ∈ (2nd𝐿)) ∧ (𝑏N ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑡}, {𝑞𝑡 <Q 𝑞}⟩)) → ∃𝑠Q (𝑠 <Q 𝑡𝑠 ∈ (2nd𝐿)))
594, 58rexlimddv 2558 1 ((𝜑𝑡 ∈ (2nd𝐿)) → ∃𝑠Q (𝑠 <Q 𝑡𝑠 ∈ (2nd𝐿)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1332   ∈ wcel 1481  {cab 2126  ∀wral 2417  ∃wrex 2418  {crab 2421  ⟨cop 3536   class class class wbr 3938  ⟶wf 5128  ‘cfv 5132  (class class class)co 5783  1st c1st 6045  2nd c2nd 6046  1oc1o 6315  [cec 6436  Ncnpi 7124
 Copyright terms: Public domain W3C validator