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

Theorem caucvgprprlemexbt 7212
Description: Lemma for caucvgprpr 7218. 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 7211 . . . . . . 7 (𝜑𝐿P)
7 caucvgprprlemexbt.q . . . . . . . 8 (𝜑𝑄Q)
8 nqprlu 7053 . . . . . . . 8 (𝑄Q → ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩ ∈ P)
97, 8syl 14 . . . . . . 7 (𝜑 → ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩ ∈ P)
10 addclpr 7043 . . . . . . 7 ((𝐿P ∧ ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩ ∈ P) → (𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P)
116, 9, 10syl2anc 403 . . . . . 6 (𝜑 → (𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P)
12 caucvgprprlemexbt.t . . . . . 6 (𝜑𝑇P)
13 ltdfpr 7012 . . . . . 6 (((𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P𝑇P) → ((𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P 𝑇 ↔ ∃𝑥Q (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
1411, 12, 13syl2anc 403 . . . . 5 (𝜑 → ((𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P 𝑇 ↔ ∃𝑥Q (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
151, 14mpbid 145 . . . 4 (𝜑 → ∃𝑥Q (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))
166adantr 270 . . . . . . . 8 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → 𝐿P)
177adantr 270 . . . . . . . 8 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → 𝑄Q)
18 simprrl 506 . . . . . . . 8 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → 𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)))
1916, 17, 18prplnqu 7126 . . . . . . 7 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → ∃𝑦 ∈ (2nd𝐿)(𝑦 +Q 𝑄) = 𝑥)
20 simprl 498 . . . . . . . . . 10 (((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) → 𝑦 ∈ (2nd𝐿))
21 breq2 3826 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑦 → (𝑝 <Q 𝑢𝑝 <Q 𝑦))
2221abbidv 2202 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑦 → {𝑝𝑝 <Q 𝑢} = {𝑝𝑝 <Q 𝑦})
23 breq1 3825 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑦 → (𝑢 <Q 𝑞𝑦 <Q 𝑞))
2423abbidv 2202 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑦 → {𝑞𝑢 <Q 𝑞} = {𝑞𝑦 <Q 𝑞})
2522, 24opeq12d 3615 . . . . . . . . . . . . . . 15 (𝑢 = 𝑦 → ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩)
2625breq2d 3834 . . . . . . . . . . . . . 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 2377 . . . . . . . . . . . . 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 5273 . . . . . . . . . . . . . 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 6869 . . . . . . . . . . . . . . . 16 Q ∈ V
3029rabex 3960 . . . . . . . . . . . . . . 15 {𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)} ∈ V
3129rabex 3960 . . . . . . . . . . . . . . 15 {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩} ∈ V
3230, 31op2nd 5877 . . . . . . . . . . . . . 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 2105 . . . . . . . . . . . . 13 (2nd𝐿) = {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}
3427, 33elrab2 2765 . . . . . . . . . . . 12 (𝑦 ∈ (2nd𝐿) ↔ (𝑦Q ∧ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩))
3534biimpi 118 . . . . . . . . . . 11 (𝑦 ∈ (2nd𝐿) → (𝑦Q ∧ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩))
3635simprd 112 . . . . . . . . . 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 5270 . . . . . . . . . . . 12 (𝑟 = 𝑏 → (𝐹𝑟) = (𝐹𝑏))
39 opeq1 3607 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑏 → ⟨𝑟, 1𝑜⟩ = ⟨𝑏, 1𝑜⟩)
4039eceq1d 6282 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑏 → [⟨𝑟, 1𝑜⟩] ~Q = [⟨𝑏, 1𝑜⟩] ~Q )
4140fveq2d 5274 . . . . . . . . . . . . . . 15 (𝑟 = 𝑏 → (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) = (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ))
4241breq2d 3834 . . . . . . . . . . . . . 14 (𝑟 = 𝑏 → (𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) ↔ 𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )))
4342abbidv 2202 . . . . . . . . . . . . 13 (𝑟 = 𝑏 → {𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )} = {𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )})
4441breq1d 3832 . . . . . . . . . . . . . 14 (𝑟 = 𝑏 → ((*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞 ↔ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞))
4544abbidv 2202 . . . . . . . . . . . . 13 (𝑟 = 𝑏 → {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞} = {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞})
4643, 45opeq12d 3615 . . . . . . . . . . . 12 (𝑟 = 𝑏 → ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)
4738, 46oveq12d 5633 . . . . . . . . . . 11 (𝑟 = 𝑏 → ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) = ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
4847breq1d 3832 . . . . . . . . . 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 2587 . . . . . . . . 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 120 . . . . . . . 8 (((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) → ∃𝑏N ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩)
51 simpr 108 . . . . . . . . . . . . . . 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 7125 . . . . . . . . . . . . . . . . 17 ((𝑓P𝑔PP) → (𝑓<P 𝑔 ↔ ( +P 𝑓)<P ( +P 𝑔)))
5352adantl 271 . . . . . . . . . . . . . . . 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 478 . . . . . . . . . . . . . . . . . 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 497 . . . . . . . . . . . . . . . . . 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 5400 . . . . . . . . . . . . . . . . 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 7054 . . . . . . . . . . . . . . . . . 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 7043 . . . . . . . . . . . . . . . . 17 (((𝐹𝑏) ∈ P ∧ ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ ∈ P) → ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∈ P)
6056, 58, 59syl2anc 403 . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → 𝑦 ∈ (2nd𝐿))
6235simpld 110 . . . . . . . . . . . . . . . . . 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 7053 . . . . . . . . . . . . . . . . 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 478 . . . . . . . . . . . . . . . 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 7084 . . . . . . . . . . . . . . . . 17 ((𝑓P𝑔P) → (𝑓 +P 𝑔) = (𝑔 +P 𝑓))
6867adantl 271 . . . . . . . . . . . . . . . 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 5773 . . . . . . . . . . . . . . 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 145 . . . . . . . . . . . . . 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 478 . . . . . . . . . . . . . . 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 7067 . . . . . . . . . . . . . . 15 ((𝑦Q𝑄Q) → ⟨{𝑝𝑝 <Q (𝑦 +Q 𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q 𝑞}⟩ = (⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩))
7363, 71, 72syl2anc 403 . . . . . . . . . . . . . 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 3848 . . . . . . . . . . . . 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 503 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) → (𝑦 +Q 𝑄) = 𝑥)
7675adantr 270 . . . . . . . . . . . . . 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 3826 . . . . . . . . . . . . . . . . 17 ((𝑦 +Q 𝑄) = 𝑥 → (𝑝 <Q (𝑦 +Q 𝑄) ↔ 𝑝 <Q 𝑥))
7877abbidv 2202 . . . . . . . . . . . . . . . 16 ((𝑦 +Q 𝑄) = 𝑥 → {𝑝𝑝 <Q (𝑦 +Q 𝑄)} = {𝑝𝑝 <Q 𝑥})
79 breq1 3825 . . . . . . . . . . . . . . . . 17 ((𝑦 +Q 𝑄) = 𝑥 → ((𝑦 +Q 𝑄) <Q 𝑞𝑥 <Q 𝑞))
8079abbidv 2202 . . . . . . . . . . . . . . . 16 ((𝑦 +Q 𝑄) = 𝑥 → {𝑞 ∣ (𝑦 +Q 𝑄) <Q 𝑞} = {𝑞𝑥 <Q 𝑞})
8178, 80opeq12d 3615 . . . . . . . . . . . . . . 15 ((𝑦 +Q 𝑄) = 𝑥 → ⟨{𝑝𝑝 <Q (𝑦 +Q 𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q 𝑥}, {𝑞𝑥 <Q 𝑞}⟩)
8281breq2d 3834 . . . . . . . . . . . . . 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 145 . . . . . . . . . . . 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 502 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) → 𝑥Q)
8685ad2antrr 472 . . . . . . . . . . . . 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 7043 . . . . . . . . . . . . . 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 403 . . . . . . . . . . . . 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 7058 . . . . . . . . . . . . 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 403 . . . . . . . . . . . 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 165 . . . . . . . . . . 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 507 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → 𝑥 ∈ (1st𝑇))
9392ad3antrrr 476 . . . . . . . . . . 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 300 . . . . . . . . . 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 113 . . . . . . . . 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 2471 . . . . . . . 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 2489 . . . . . 6 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → ∃𝑏N (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))
9998expr 367 . . . . 5 ((𝜑𝑥Q) → ((𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)) → ∃𝑏N (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
10099reximdva 2471 . . . 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 2527 . . 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 120 . 2 (𝜑 → ∃𝑏N𝑥Q (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))
1042ffvelrnda 5399 . . . . . 6 ((𝜑𝑏N) → (𝐹𝑏) ∈ P)
10557adantl 271 . . . . . 6 ((𝜑𝑏N) → ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩ ∈ P)
106104, 105, 59syl2anc 403 . . . . 5 ((𝜑𝑏N) → ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∈ P)
1079adantr 270 . . . . 5 ((𝜑𝑏N) → ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩ ∈ P)
108106, 107, 87syl2anc 403 . . . 4 ((𝜑𝑏N) → (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P)
10912adantr 270 . . . 4 ((𝜑𝑏N) → 𝑇P)
110 ltdfpr 7012 . . . 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 403 . . 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 2373 . 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 165 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 102  wb 103  w3a 922   = wceq 1287  wcel 1436  {cab 2071  wral 2355  wrex 2356  {crab 2359  cop 3434   class class class wbr 3822  wf 4979  cfv 4983  (class class class)co 5615  1st c1st 5868  2nd c2nd 5869  1𝑜c1o 6130  [cec 6244  Ncnpi 6778   <N clti 6781   ~Q ceq 6785  Qcnq 6786   +Q cplq 6788  *Qcrq 6790   <Q cltq 6791  Pcnp 6797   +P cpp 6799  <P cltp 6801
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-coll 3931  ax-sep 3934  ax-nul 3942  ax-pow 3986  ax-pr 4012  ax-un 4236  ax-setind 4328  ax-iinf 4378
This theorem depends on definitions:  df-bi 115  df-dc 779  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-ral 2360  df-rex 2361  df-reu 2362  df-rab 2364  df-v 2617  df-sbc 2830  df-csb 2923  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-nul 3276  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-int 3674  df-iun 3717  df-br 3823  df-opab 3877  df-mpt 3878  df-tr 3914  df-eprel 4092  df-id 4096  df-po 4099  df-iso 4100  df-iord 4169  df-on 4171  df-suc 4174  df-iom 4381  df-xp 4419  df-rel 4420  df-cnv 4421  df-co 4422  df-dm 4423  df-rn 4424  df-res 4425  df-ima 4426  df-iota 4948  df-fun 4985  df-fn 4986  df-f 4987  df-f1 4988  df-fo 4989  df-f1o 4990  df-fv 4991  df-ov 5618  df-oprab 5619  df-mpt2 5620  df-1st 5870  df-2nd 5871  df-recs 6026  df-irdg 6091  df-1o 6137  df-2o 6138  df-oadd 6141  df-omul 6142  df-er 6246  df-ec 6248  df-qs 6252  df-ni 6810  df-pli 6811  df-mi 6812  df-lti 6813  df-plpq 6850  df-mpq 6851  df-enq 6853  df-nqqs 6854  df-plqqs 6855  df-mqqs 6856  df-1nqqs 6857  df-rq 6858  df-ltnqqs 6859  df-enq0 6930  df-nq0 6931  df-0nq0 6932  df-plq0 6933  df-mq0 6934  df-inp 6972  df-iplp 6974  df-iltp 6976
This theorem is referenced by:  caucvgprprlemexb  7213
  Copyright terms: Public domain W3C validator