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

Theorem caucvgprprlemexbt 6862
Description: Lemma for caucvgprpr 6868. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 16-Jun-2021.)
Hypotheses
Ref Expression
caucvgprpr.f (𝜑𝐹:NP)
caucvgprpr.cau (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
caucvgprpr.bnd (𝜑 → ∀𝑚N 𝐴<P (𝐹𝑚))
caucvgprpr.lim 𝐿 = ⟨{𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}, {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}⟩
caucvgprprlemexbt.q (𝜑𝑄Q)
caucvgprprlemexbt.t (𝜑𝑇P)
caucvgprprlemexbt.lt (𝜑 → (𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P 𝑇)
Assertion
Ref Expression
caucvgprprlemexbt (𝜑 → ∃𝑏N (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P 𝑇)
Distinct variable groups:   𝐴,𝑚   𝑚,𝐹   𝐴,𝑟,𝑚   𝐹,𝑏   𝑘,𝐹,𝑙,𝑛,𝑢   𝐹,𝑟   𝐿,𝑏   𝑘,𝐿   𝑄,𝑏,𝑝,𝑞   𝑇,𝑏   𝜑,𝑏   𝑟,𝑏,𝑝,𝑞   𝑘,𝑝,𝑞,𝑟,𝑙,𝑢
Allowed substitution hints:   𝜑(𝑢,𝑘,𝑚,𝑛,𝑟,𝑞,𝑝,𝑙)   𝐴(𝑢,𝑘,𝑛,𝑞,𝑝,𝑏,𝑙)   𝑄(𝑢,𝑘,𝑚,𝑛,𝑟,𝑙)   𝑇(𝑢,𝑘,𝑚,𝑛,𝑟,𝑞,𝑝,𝑙)   𝐹(𝑞,𝑝)   𝐿(𝑢,𝑚,𝑛,𝑟,𝑞,𝑝,𝑙)

Proof of Theorem caucvgprprlemexbt
Dummy variables 𝑓 𝑔 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 caucvgprprlemexbt.lt . . . . 5 (𝜑 → (𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P 𝑇)
2 caucvgprpr.f . . . . . . . 8 (𝜑𝐹:NP)
3 caucvgprpr.cau . . . . . . . 8 (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
4 caucvgprpr.bnd . . . . . . . 8 (𝜑 → ∀𝑚N 𝐴<P (𝐹𝑚))
5 caucvgprpr.lim . . . . . . . 8 𝐿 = ⟨{𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}, {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}⟩
62, 3, 4, 5caucvgprprlemclphr 6861 . . . . . . 7 (𝜑𝐿P)
7 caucvgprprlemexbt.q . . . . . . . 8 (𝜑𝑄Q)
8 nqprlu 6703 . . . . . . . 8 (𝑄Q → ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩ ∈ P)
97, 8syl 14 . . . . . . 7 (𝜑 → ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩ ∈ P)
10 addclpr 6693 . . . . . . 7 ((𝐿P ∧ ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩ ∈ P) → (𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P)
116, 9, 10syl2anc 397 . . . . . 6 (𝜑 → (𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P)
12 caucvgprprlemexbt.t . . . . . 6 (𝜑𝑇P)
13 ltdfpr 6662 . . . . . 6 (((𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P𝑇P) → ((𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P 𝑇 ↔ ∃𝑥Q (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
1411, 12, 13syl2anc 397 . . . . 5 (𝜑 → ((𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P 𝑇 ↔ ∃𝑥Q (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
151, 14mpbid 139 . . . 4 (𝜑 → ∃𝑥Q (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))
166adantr 265 . . . . . . . 8 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → 𝐿P)
177adantr 265 . . . . . . . 8 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → 𝑄Q)
18 simprrl 499 . . . . . . . 8 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → 𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)))
1916, 17, 18prplnqu 6776 . . . . . . 7 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → ∃𝑦 ∈ (2nd𝐿)(𝑦 +Q 𝑄) = 𝑥)
20 simprl 491 . . . . . . . . . 10 (((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) → 𝑦 ∈ (2nd𝐿))
21 breq2 3796 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑦 → (𝑝 <Q 𝑢𝑝 <Q 𝑦))
2221abbidv 2171 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑦 → {𝑝𝑝 <Q 𝑢} = {𝑝𝑝 <Q 𝑦})
23 breq1 3795 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑦 → (𝑢 <Q 𝑞𝑦 <Q 𝑞))
2423abbidv 2171 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑦 → {𝑞𝑢 <Q 𝑞} = {𝑞𝑦 <Q 𝑞})
2522, 24opeq12d 3585 . . . . . . . . . . . . . . 15 (𝑢 = 𝑦 → ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩)
2625breq2d 3804 . . . . . . . . . . . . . 14 (𝑢 = 𝑦 → (((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩ ↔ ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩))
2726rexbidv 2344 . . . . . . . . . . . . 13 (𝑢 = 𝑦 → (∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩ ↔ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩))
285fveq2i 5209 . . . . . . . . . . . . . 14 (2nd𝐿) = (2nd ‘⟨{𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}, {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}⟩)
29 nqex 6519 . . . . . . . . . . . . . . . 16 Q ∈ V
3029rabex 3929 . . . . . . . . . . . . . . 15 {𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)} ∈ V
3129rabex 3929 . . . . . . . . . . . . . . 15 {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩} ∈ V
3230, 31op2nd 5802 . . . . . . . . . . . . . 14 (2nd ‘⟨{𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)}, {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}⟩) = {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}
3328, 32eqtri 2076 . . . . . . . . . . . . 13 (2nd𝐿) = {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}
3427, 33elrab2 2723 . . . . . . . . . . . 12 (𝑦 ∈ (2nd𝐿) ↔ (𝑦Q ∧ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩))
3534biimpi 117 . . . . . . . . . . 11 (𝑦 ∈ (2nd𝐿) → (𝑦Q ∧ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩))
3635simprd 111 . . . . . . . . . 10 (𝑦 ∈ (2nd𝐿) → ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩)
3720, 36syl 14 . . . . . . . . 9 (((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) → ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩)
38 fveq2 5206 . . . . . . . . . . . 12 (𝑟 = 𝑏 → (𝐹𝑟) = (𝐹𝑏))
39 opeq1 3577 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑏 → ⟨𝑟, 1𝑜⟩ = ⟨𝑏, 1𝑜⟩)
4039eceq1d 6173 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑏 → [⟨𝑟, 1𝑜⟩] ~Q = [⟨𝑏, 1𝑜⟩] ~Q )
4140fveq2d 5210 . . . . . . . . . . . . . . 15 (𝑟 = 𝑏 → (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) = (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))
4241breq2d 3804 . . . . . . . . . . . . . 14 (𝑟 = 𝑏 → (𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) ↔ 𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )))
4342abbidv 2171 . . . . . . . . . . . . 13 (𝑟 = 𝑏 → {𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )} = {𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )})
4441breq1d 3802 . . . . . . . . . . . . . 14 (𝑟 = 𝑏 → ((*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞 ↔ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞))
4544abbidv 2171 . . . . . . . . . . . . 13 (𝑟 = 𝑏 → {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞} = {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞})
4643, 45opeq12d 3585 . . . . . . . . . . . 12 (𝑟 = 𝑏 → ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)
4738, 46oveq12d 5558 . . . . . . . . . . 11 (𝑟 = 𝑏 → ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) = ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
4847breq1d 3802 . . . . . . . . . 10 (𝑟 = 𝑏 → (((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ ↔ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩))
4948cbvrexv 2551 . . . . . . . . 9 (∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ ↔ ∃𝑏N ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩)
5037, 49sylib 131 . . . . . . . 8 (((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) → ∃𝑏N ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩)
51 simpr 107 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩)
52 ltaprg 6775 . . . . . . . . . . . . . . . . 17 ((𝑓P𝑔PP) → (𝑓<P 𝑔 ↔ ( +P 𝑓)<P ( +P 𝑔)))
5352adantl 266 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) ∧ (𝑓P𝑔PP)) → (𝑓<P 𝑔 ↔ ( +P 𝑓)<P ( +P 𝑔)))
542ad4antr 471 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → 𝐹:NP)
55 simplr 490 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → 𝑏N)
5654, 55ffvelrnd 5331 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → (𝐹𝑏) ∈ P)
57 recnnpr 6704 . . . . . . . . . . . . . . . . . 18 (𝑏N → ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ ∈ P)
5855, 57syl 14 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ ∈ P)
59 addclpr 6693 . . . . . . . . . . . . . . . . 17 (((𝐹𝑏) ∈ P ∧ ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ ∈ P) → ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∈ P)
6056, 58, 59syl2anc 397 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∈ P)
6120ad2antrr 465 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → 𝑦 ∈ (2nd𝐿))
6235simpld 109 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (2nd𝐿) → 𝑦Q)
6361, 62syl 14 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → 𝑦Q)
64 nqprlu 6703 . . . . . . . . . . . . . . . . 17 (𝑦Q → ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ ∈ P)
6563, 64syl 14 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ ∈ P)
669ad4antr 471 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩ ∈ P)
67 addcomprg 6734 . . . . . . . . . . . . . . . . 17 ((𝑓P𝑔P) → (𝑓 +P 𝑔) = (𝑔 +P 𝑓))
6867adantl 266 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) ∧ (𝑓P𝑔P)) → (𝑓 +P 𝑔) = (𝑔 +P 𝑓))
6953, 60, 65, 66, 68caovord2d 5698 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ ↔ (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P (⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)))
7051, 69mpbid 139 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P (⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩))
717ad4antr 471 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → 𝑄Q)
72 addnqpr 6717 . . . . . . . . . . . . . . 15 ((𝑦Q𝑄Q) → ⟨{𝑝𝑝 <Q (𝑦 +Q 𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q 𝑞}⟩ = (⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩))
7363, 71, 72syl2anc 397 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → ⟨{𝑝𝑝 <Q (𝑦 +Q 𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q 𝑞}⟩ = (⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩))
7470, 73breqtrrd 3818 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q (𝑦 +Q 𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q 𝑞}⟩)
75 simplrr 496 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) → (𝑦 +Q 𝑄) = 𝑥)
7675adantr 265 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → (𝑦 +Q 𝑄) = 𝑥)
77 breq2 3796 . . . . . . . . . . . . . . . . 17 ((𝑦 +Q 𝑄) = 𝑥 → (𝑝 <Q (𝑦 +Q 𝑄) ↔ 𝑝 <Q 𝑥))
7877abbidv 2171 . . . . . . . . . . . . . . . 16 ((𝑦 +Q 𝑄) = 𝑥 → {𝑝𝑝 <Q (𝑦 +Q 𝑄)} = {𝑝𝑝 <Q 𝑥})
79 breq1 3795 . . . . . . . . . . . . . . . . 17 ((𝑦 +Q 𝑄) = 𝑥 → ((𝑦 +Q 𝑄) <Q 𝑞𝑥 <Q 𝑞))
8079abbidv 2171 . . . . . . . . . . . . . . . 16 ((𝑦 +Q 𝑄) = 𝑥 → {𝑞 ∣ (𝑦 +Q 𝑄) <Q 𝑞} = {𝑞𝑥 <Q 𝑞})
8178, 80opeq12d 3585 . . . . . . . . . . . . . . 15 ((𝑦 +Q 𝑄) = 𝑥 → ⟨{𝑝𝑝 <Q (𝑦 +Q 𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q 𝑥}, {𝑞𝑥 <Q 𝑞}⟩)
8281breq2d 3804 . . . . . . . . . . . . . 14 ((𝑦 +Q 𝑄) = 𝑥 → ((((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q (𝑦 +Q 𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q 𝑞}⟩ ↔ (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑥}, {𝑞𝑥 <Q 𝑞}⟩))
8376, 82syl 14 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → ((((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q (𝑦 +Q 𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q 𝑞}⟩ ↔ (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑥}, {𝑞𝑥 <Q 𝑞}⟩))
8474, 83mpbid 139 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑥}, {𝑞𝑥 <Q 𝑞}⟩)
85 simplrl 495 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) → 𝑥Q)
8685ad2antrr 465 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → 𝑥Q)
87 addclpr 6693 . . . . . . . . . . . . . 14 ((((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∈ P ∧ ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩ ∈ P) → (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P)
8860, 66, 87syl2anc 397 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P)
89 nqpru 6708 . . . . . . . . . . . . 13 ((𝑥Q ∧ (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P) → (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ↔ (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑥}, {𝑞𝑥 <Q 𝑞}⟩))
9086, 88, 89syl2anc 397 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ↔ (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑥}, {𝑞𝑥 <Q 𝑞}⟩))
9184, 90mpbird 160 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → 𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)))
92 simprrr 500 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → 𝑥 ∈ (1st𝑇))
9392ad3antrrr 469 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → 𝑥 ∈ (1st𝑇))
9491, 93jca 294 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))
9594ex 112 . . . . . . . . 9 ((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) → (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ → (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
9695reximdva 2438 . . . . . . . 8 (((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) → (∃𝑏N ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ → ∃𝑏N (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
9750, 96mpd 13 . . . . . . 7 (((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) → ∃𝑏N (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))
9819, 97rexlimddv 2454 . . . . . 6 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → ∃𝑏N (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))
9998expr 361 . . . . 5 ((𝜑𝑥Q) → ((𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)) → ∃𝑏N (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
10099reximdva 2438 . . . 4 (𝜑 → (∃𝑥Q (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)) → ∃𝑥Q𝑏N (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
10115, 100mpd 13 . . 3 (𝜑 → ∃𝑥Q𝑏N (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))
102 rexcom 2491 . . 3 (∃𝑥Q𝑏N (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)) ↔ ∃𝑏N𝑥Q (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))
103101, 102sylib 131 . 2 (𝜑 → ∃𝑏N𝑥Q (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))
1042ffvelrnda 5330 . . . . . 6 ((𝜑𝑏N) → (𝐹𝑏) ∈ P)
10557adantl 266 . . . . . 6 ((𝜑𝑏N) → ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ ∈ P)
106104, 105, 59syl2anc 397 . . . . 5 ((𝜑𝑏N) → ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∈ P)
1079adantr 265 . . . . 5 ((𝜑𝑏N) → ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩ ∈ P)
108106, 107, 87syl2anc 397 . . . 4 ((𝜑𝑏N) → (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P)
10912adantr 265 . . . 4 ((𝜑𝑏N) → 𝑇P)
110 ltdfpr 6662 . . . 4 (((((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P𝑇P) → ((((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P 𝑇 ↔ ∃𝑥Q (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
111108, 109, 110syl2anc 397 . . 3 ((𝜑𝑏N) → ((((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P 𝑇 ↔ ∃𝑥Q (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
112111rexbidva 2340 . 2 (𝜑 → (∃𝑏N (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P 𝑇 ↔ ∃𝑏N𝑥Q (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
113103, 112mpbird 160 1 (𝜑 → ∃𝑏N (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P 𝑇)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wb 102  w3a 896   = wceq 1259  wcel 1409  {cab 2042  wral 2323  wrex 2324  {crab 2327  cop 3406   class class class wbr 3792  wf 4926  cfv 4930  (class class class)co 5540  1st c1st 5793  2nd c2nd 5794  1𝑜c1o 6025  [cec 6135  Ncnpi 6428   <N clti 6431   ~Q ceq 6435  Qcnq 6436   +Q cplq 6438  *Qcrq 6440   <Q cltq 6441  Pcnp 6447   +P cpp 6449  <P cltp 6451
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-13 1420  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-coll 3900  ax-sep 3903  ax-nul 3911  ax-pow 3955  ax-pr 3972  ax-un 4198  ax-setind 4290  ax-iinf 4339
This theorem depends on definitions:  df-bi 114  df-dc 754  df-3or 897  df-3an 898  df-tru 1262  df-fal 1265  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ne 2221  df-ral 2328  df-rex 2329  df-reu 2330  df-rab 2332  df-v 2576  df-sbc 2788  df-csb 2881  df-dif 2948  df-un 2950  df-in 2952  df-ss 2959  df-nul 3253  df-pw 3389  df-sn 3409  df-pr 3410  df-op 3412  df-uni 3609  df-int 3644  df-iun 3687  df-br 3793  df-opab 3847  df-mpt 3848  df-tr 3883  df-eprel 4054  df-id 4058  df-po 4061  df-iso 4062  df-iord 4131  df-on 4133  df-suc 4136  df-iom 4342  df-xp 4379  df-rel 4380  df-cnv 4381  df-co 4382  df-dm 4383  df-rn 4384  df-res 4385  df-ima 4386  df-iota 4895  df-fun 4932  df-fn 4933  df-f 4934  df-f1 4935  df-fo 4936  df-f1o 4937  df-fv 4938  df-ov 5543  df-oprab 5544  df-mpt2 5545  df-1st 5795  df-2nd 5796  df-recs 5951  df-irdg 5988  df-1o 6032  df-2o 6033  df-oadd 6036  df-omul 6037  df-er 6137  df-ec 6139  df-qs 6143  df-ni 6460  df-pli 6461  df-mi 6462  df-lti 6463  df-plpq 6500  df-mpq 6501  df-enq 6503  df-nqqs 6504  df-plqqs 6505  df-mqqs 6506  df-1nqqs 6507  df-rq 6508  df-ltnqqs 6509  df-enq0 6580  df-nq0 6581  df-0nq0 6582  df-plq0 6583  df-mq0 6584  df-inp 6622  df-iplp 6624  df-iltp 6626
This theorem is referenced by:  caucvgprprlemexb  6863
  Copyright terms: Public domain W3C validator