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

Theorem caucvgprprlemexbt 6804
 Description: Lemma for caucvgprpr 6810. 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 6803 . . . . . . 7 (𝜑𝐿P)
7 caucvgprprlemexbt.q . . . . . . . 8 (𝜑𝑄Q)
8 nqprlu 6645 . . . . . . . 8 (𝑄Q → ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩ ∈ P)
97, 8syl 14 . . . . . . 7 (𝜑 → ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩ ∈ P)
10 addclpr 6635 . . . . . . 7 ((𝐿P ∧ ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩ ∈ P) → (𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P)
116, 9, 10syl2anc 391 . . . . . 6 (𝜑 → (𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P)
12 caucvgprprlemexbt.t . . . . . 6 (𝜑𝑇P)
13 ltdfpr 6604 . . . . . 6 (((𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P𝑇P) → ((𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P 𝑇 ↔ ∃𝑥Q (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
1411, 12, 13syl2anc 391 . . . . 5 (𝜑 → ((𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P 𝑇 ↔ ∃𝑥Q (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
151, 14mpbid 135 . . . 4 (𝜑 → ∃𝑥Q (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))
166adantr 261 . . . . . . . 8 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → 𝐿P)
177adantr 261 . . . . . . . 8 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → 𝑄Q)
18 simprrl 491 . . . . . . . 8 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → 𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)))
1916, 17, 18prplnqu 6718 . . . . . . 7 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → ∃𝑦 ∈ (2nd𝐿)(𝑦 +Q 𝑄) = 𝑥)
20 simprl 483 . . . . . . . . . 10 (((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) → 𝑦 ∈ (2nd𝐿))
21 breq2 3768 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑦 → (𝑝 <Q 𝑢𝑝 <Q 𝑦))
2221abbidv 2155 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑦 → {𝑝𝑝 <Q 𝑢} = {𝑝𝑝 <Q 𝑦})
23 breq1 3767 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑦 → (𝑢 <Q 𝑞𝑦 <Q 𝑞))
2423abbidv 2155 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑦 → {𝑞𝑢 <Q 𝑞} = {𝑞𝑦 <Q 𝑞})
2522, 24opeq12d 3557 . . . . . . . . . . . . . . 15 (𝑢 = 𝑦 → ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩)
2625breq2d 3776 . . . . . . . . . . . . . 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 2327 . . . . . . . . . . . . 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 5181 . . . . . . . . . . . . . 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 6461 . . . . . . . . . . . . . . . 16 Q ∈ V
3029rabex 3901 . . . . . . . . . . . . . . 15 {𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)} ∈ V
3129rabex 3901 . . . . . . . . . . . . . . 15 {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩} ∈ V
3230, 31op2nd 5774 . . . . . . . . . . . . . 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 2060 . . . . . . . . . . . . 13 (2nd𝐿) = {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}
3427, 33elrab2 2700 . . . . . . . . . . . 12 (𝑦 ∈ (2nd𝐿) ↔ (𝑦Q ∧ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩))
3534biimpi 113 . . . . . . . . . . 11 (𝑦 ∈ (2nd𝐿) → (𝑦Q ∧ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩))
3635simprd 107 . . . . . . . . . 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 5178 . . . . . . . . . . . 12 (𝑟 = 𝑏 → (𝐹𝑟) = (𝐹𝑏))
39 opeq1 3549 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑏 → ⟨𝑟, 1𝑜⟩ = ⟨𝑏, 1𝑜⟩)
4039eceq1d 6142 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑏 → [⟨𝑟, 1𝑜⟩] ~Q = [⟨𝑏, 1𝑜⟩] ~Q )
4140fveq2d 5182 . . . . . . . . . . . . . . 15 (𝑟 = 𝑏 → (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) = (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))
4241breq2d 3776 . . . . . . . . . . . . . 14 (𝑟 = 𝑏 → (𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) ↔ 𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )))
4342abbidv 2155 . . . . . . . . . . . . 13 (𝑟 = 𝑏 → {𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )} = {𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )})
4441breq1d 3774 . . . . . . . . . . . . . 14 (𝑟 = 𝑏 → ((*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞 ↔ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞))
4544abbidv 2155 . . . . . . . . . . . . 13 (𝑟 = 𝑏 → {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞} = {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞})
4643, 45opeq12d 3557 . . . . . . . . . . . 12 (𝑟 = 𝑏 → ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)
4738, 46oveq12d 5530 . . . . . . . . . . 11 (𝑟 = 𝑏 → ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) = ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
4847breq1d 3774 . . . . . . . . . 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 2534 . . . . . . . . 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 127 . . . . . . . 8 (((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) → ∃𝑏N ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩)
51 simpr 103 . . . . . . . . . . . . . . 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 6717 . . . . . . . . . . . . . . . . 17 ((𝑓P𝑔PP) → (𝑓<P 𝑔 ↔ ( +P 𝑓)<P ( +P 𝑔)))
5352adantl 262 . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . 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 482 . . . . . . . . . . . . . . . . . 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 5303 . . . . . . . . . . . . . . . . 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 6646 . . . . . . . . . . . . . . . . . 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 6635 . . . . . . . . . . . . . . . . 17 (((𝐹𝑏) ∈ P ∧ ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ ∈ P) → ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∈ P)
6056, 58, 59syl2anc 391 . . . . . . . . . . . . . . . 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 457 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → 𝑦 ∈ (2nd𝐿))
6235simpld 105 . . . . . . . . . . . . . . . . . 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 6645 . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . 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 6676 . . . . . . . . . . . . . . . . 17 ((𝑓P𝑔P) → (𝑓 +P 𝑔) = (𝑔 +P 𝑓))
6867adantl 262 . . . . . . . . . . . . . . . 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 5670 . . . . . . . . . . . . . . 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 135 . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . 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 6659 . . . . . . . . . . . . . . 15 ((𝑦Q𝑄Q) → ⟨{𝑝𝑝 <Q (𝑦 +Q 𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q 𝑞}⟩ = (⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩))
7363, 71, 72syl2anc 391 . . . . . . . . . . . . . 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 3790 . . . . . . . . . . . . 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 488 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) → (𝑦 +Q 𝑄) = 𝑥)
7675adantr 261 . . . . . . . . . . . . . 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 3768 . . . . . . . . . . . . . . . . 17 ((𝑦 +Q 𝑄) = 𝑥 → (𝑝 <Q (𝑦 +Q 𝑄) ↔ 𝑝 <Q 𝑥))
7877abbidv 2155 . . . . . . . . . . . . . . . 16 ((𝑦 +Q 𝑄) = 𝑥 → {𝑝𝑝 <Q (𝑦 +Q 𝑄)} = {𝑝𝑝 <Q 𝑥})
79 breq1 3767 . . . . . . . . . . . . . . . . 17 ((𝑦 +Q 𝑄) = 𝑥 → ((𝑦 +Q 𝑄) <Q 𝑞𝑥 <Q 𝑞))
8079abbidv 2155 . . . . . . . . . . . . . . . 16 ((𝑦 +Q 𝑄) = 𝑥 → {𝑞 ∣ (𝑦 +Q 𝑄) <Q 𝑞} = {𝑞𝑥 <Q 𝑞})
8178, 80opeq12d 3557 . . . . . . . . . . . . . . 15 ((𝑦 +Q 𝑄) = 𝑥 → ⟨{𝑝𝑝 <Q (𝑦 +Q 𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q 𝑥}, {𝑞𝑥 <Q 𝑞}⟩)
8281breq2d 3776 . . . . . . . . . . . . . 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 135 . . . . . . . . . . . 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 487 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) → 𝑥Q)
8685ad2antrr 457 . . . . . . . . . . . . 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 6635 . . . . . . . . . . . . . 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 391 . . . . . . . . . . . . 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 6650 . . . . . . . . . . . . 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 391 . . . . . . . . . . . 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 156 . . . . . . . . . . 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 492 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → 𝑥 ∈ (1st𝑇))
9392ad3antrrr 461 . . . . . . . . . . 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 290 . . . . . . . . . 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 108 . . . . . . . . 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 2421 . . . . . . . 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 2437 . . . . . 6 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → ∃𝑏N (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))
9998expr 357 . . . . 5 ((𝜑𝑥Q) → ((𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)) → ∃𝑏N (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
10099reximdva 2421 . . . 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 2474 . . 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 127 . 2 (𝜑 → ∃𝑏N𝑥Q (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))
1042ffvelrnda 5302 . . . . . 6 ((𝜑𝑏N) → (𝐹𝑏) ∈ P)
10557adantl 262 . . . . . 6 ((𝜑𝑏N) → ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ ∈ P)
106104, 105, 59syl2anc 391 . . . . 5 ((𝜑𝑏N) → ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∈ P)
1079adantr 261 . . . . 5 ((𝜑𝑏N) → ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩ ∈ P)
108106, 107, 87syl2anc 391 . . . 4 ((𝜑𝑏N) → (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P)
10912adantr 261 . . . 4 ((𝜑𝑏N) → 𝑇P)
110 ltdfpr 6604 . . . 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 391 . . 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 2323 . 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 156 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 97   ↔ wb 98   ∧ w3a 885   = wceq 1243   ∈ wcel 1393  {cab 2026  ∀wral 2306  ∃wrex 2307  {crab 2310  ⟨cop 3378   class class class wbr 3764  ⟶wf 4898  ‘cfv 4902  (class class class)co 5512  1st c1st 5765  2nd c2nd 5766  1𝑜c1o 5994  [cec 6104  Ncnpi 6370
 Copyright terms: Public domain W3C validator