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

Theorem caucvgprprlemexbt 7521
 Description: Lemma for caucvgprpr 7527. 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‘[⟨𝑛, 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 𝑞}⟩}⟩
caucvgprprlemexbt.q (𝜑𝑄Q)
caucvgprprlemexbt.t (𝜑𝑇P)
caucvgprprlemexbt.lt (𝜑 → (𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P 𝑇)
Assertion
Ref Expression
caucvgprprlemexbt (𝜑 → ∃𝑏N (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~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‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩))))
4 caucvgprpr.bnd . . . . . . . 8 (𝜑 → ∀𝑚N 𝐴<P (𝐹𝑚))
5 caucvgprpr.lim . . . . . . . 8 𝐿 = ⟨{𝑙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 𝑞}⟩}⟩
62, 3, 4, 5caucvgprprlemclphr 7520 . . . . . . 7 (𝜑𝐿P)
7 caucvgprprlemexbt.q . . . . . . . 8 (𝜑𝑄Q)
8 nqprlu 7362 . . . . . . . 8 (𝑄Q → ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩ ∈ P)
97, 8syl 14 . . . . . . 7 (𝜑 → ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩ ∈ P)
10 addclpr 7352 . . . . . . 7 ((𝐿P ∧ ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩ ∈ P) → (𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P)
116, 9, 10syl2anc 408 . . . . . 6 (𝜑 → (𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P)
12 caucvgprprlemexbt.t . . . . . 6 (𝜑𝑇P)
13 ltdfpr 7321 . . . . . 6 (((𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P𝑇P) → ((𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P 𝑇 ↔ ∃𝑥Q (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
1411, 12, 13syl2anc 408 . . . . 5 (𝜑 → ((𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P 𝑇 ↔ ∃𝑥Q (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
151, 14mpbid 146 . . . 4 (𝜑 → ∃𝑥Q (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))
166adantr 274 . . . . . . . 8 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → 𝐿P)
177adantr 274 . . . . . . . 8 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → 𝑄Q)
18 simprrl 528 . . . . . . . 8 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → 𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)))
1916, 17, 18prplnqu 7435 . . . . . . 7 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → ∃𝑦 ∈ (2nd𝐿)(𝑦 +Q 𝑄) = 𝑥)
20 simprl 520 . . . . . . . . . 10 (((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) → 𝑦 ∈ (2nd𝐿))
21 breq2 3933 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑦 → (𝑝 <Q 𝑢𝑝 <Q 𝑦))
2221abbidv 2257 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑦 → {𝑝𝑝 <Q 𝑢} = {𝑝𝑝 <Q 𝑦})
23 breq1 3932 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑦 → (𝑢 <Q 𝑞𝑦 <Q 𝑞))
2423abbidv 2257 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑦 → {𝑞𝑢 <Q 𝑞} = {𝑞𝑦 <Q 𝑞})
2522, 24opeq12d 3713 . . . . . . . . . . . . . . 15 (𝑢 = 𝑦 → ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩)
2625breq2d 3941 . . . . . . . . . . . . . 14 (𝑢 = 𝑦 → (((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩ ↔ ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩))
2726rexbidv 2438 . . . . . . . . . . . . 13 (𝑢 = 𝑦 → (∃𝑟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 𝑞}⟩))
285fveq2i 5424 . . . . . . . . . . . . . 14 (2nd𝐿) = (2nd ‘⟨{𝑙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 𝑞}⟩}⟩)
29 nqex 7178 . . . . . . . . . . . . . . . 16 Q ∈ V
3029rabex 4072 . . . . . . . . . . . . . . 15 {𝑙Q ∣ ∃𝑟N ⟨{𝑝𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝑟)} ∈ V
3129rabex 4072 . . . . . . . . . . . . . . 15 {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩} ∈ V
3230, 31op2nd 6045 . . . . . . . . . . . . . 14 (2nd ‘⟨{𝑙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 𝑞}⟩}⟩) = {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}
3328, 32eqtri 2160 . . . . . . . . . . . . 13 (2nd𝐿) = {𝑢Q ∣ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑢}, {𝑞𝑢 <Q 𝑞}⟩}
3427, 33elrab2 2843 . . . . . . . . . . . 12 (𝑦 ∈ (2nd𝐿) ↔ (𝑦Q ∧ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩))
3534biimpi 119 . . . . . . . . . . 11 (𝑦 ∈ (2nd𝐿) → (𝑦Q ∧ ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩))
3635simprd 113 . . . . . . . . . 10 (𝑦 ∈ (2nd𝐿) → ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩)
3720, 36syl 14 . . . . . . . . 9 (((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) → ∃𝑟N ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩)
38 fveq2 5421 . . . . . . . . . . . 12 (𝑟 = 𝑏 → (𝐹𝑟) = (𝐹𝑏))
39 opeq1 3705 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑏 → ⟨𝑟, 1o⟩ = ⟨𝑏, 1o⟩)
4039eceq1d 6465 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑏 → [⟨𝑟, 1o⟩] ~Q = [⟨𝑏, 1o⟩] ~Q )
4140fveq2d 5425 . . . . . . . . . . . . . . 15 (𝑟 = 𝑏 → (*Q‘[⟨𝑟, 1o⟩] ~Q ) = (*Q‘[⟨𝑏, 1o⟩] ~Q ))
4241breq2d 3941 . . . . . . . . . . . . . 14 (𝑟 = 𝑏 → (𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q ) ↔ 𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )))
4342abbidv 2257 . . . . . . . . . . . . 13 (𝑟 = 𝑏 → {𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )} = {𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )})
4441breq1d 3939 . . . . . . . . . . . . . 14 (𝑟 = 𝑏 → ((*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞 ↔ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞))
4544abbidv 2257 . . . . . . . . . . . . 13 (𝑟 = 𝑏 → {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞} = {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞})
4643, 45opeq12d 3713 . . . . . . . . . . . 12 (𝑟 = 𝑏 → ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)
4738, 46oveq12d 5792 . . . . . . . . . . 11 (𝑟 = 𝑏 → ((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩) = ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩))
4847breq1d 3939 . . . . . . . . . 10 (𝑟 = 𝑏 → (((𝐹𝑟) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ ↔ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩))
4948cbvrexv 2655 . . . . . . . . 9 (∃𝑟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 𝑞}⟩)
5037, 49sylib 121 . . . . . . . 8 (((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) → ∃𝑏N ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩)
51 simpr 109 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏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 𝑞}⟩)
52 ltaprg 7434 . . . . . . . . . . . . . . . . 17 ((𝑓P𝑔PP) → (𝑓<P 𝑔 ↔ ( +P 𝑓)<P ( +P 𝑔)))
5352adantl 275 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) ∧ (𝑓P𝑔PP)) → (𝑓<P 𝑔 ↔ ( +P 𝑓)<P ( +P 𝑔)))
542ad4antr 485 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → 𝐹:NP)
55 simplr 519 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → 𝑏N)
5654, 55ffvelrnd 5556 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → (𝐹𝑏) ∈ P)
57 recnnpr 7363 . . . . . . . . . . . . . . . . . 18 (𝑏N → ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩ ∈ P)
5855, 57syl 14 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩ ∈ P)
59 addclpr 7352 . . . . . . . . . . . . . . . . 17 (((𝐹𝑏) ∈ P ∧ ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩ ∈ P) → ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) ∈ P)
6056, 58, 59syl2anc 408 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) ∈ P)
6120ad2antrr 479 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → 𝑦 ∈ (2nd𝐿))
6235simpld 111 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (2nd𝐿) → 𝑦Q)
6361, 62syl 14 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → 𝑦Q)
64 nqprlu 7362 . . . . . . . . . . . . . . . . 17 (𝑦Q → ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ ∈ P)
6563, 64syl 14 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ ∈ P)
669ad4antr 485 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩ ∈ P)
67 addcomprg 7393 . . . . . . . . . . . . . . . . 17 ((𝑓P𝑔P) → (𝑓 +P 𝑔) = (𝑔 +P 𝑓))
6867adantl 275 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) ∧ (𝑓P𝑔P)) → (𝑓 +P 𝑔) = (𝑔 +P 𝑓))
6953, 60, 65, 66, 68caovord2d 5940 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏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 𝑞}⟩ ↔ (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P (⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)))
7051, 69mpbid 146 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏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 𝑞}⟩)<P (⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩))
717ad4antr 485 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → 𝑄Q)
72 addnqpr 7376 . . . . . . . . . . . . . . 15 ((𝑦Q𝑄Q) → ⟨{𝑝𝑝 <Q (𝑦 +Q 𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q 𝑞}⟩ = (⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩))
7363, 71, 72syl2anc 408 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → ⟨{𝑝𝑝 <Q (𝑦 +Q 𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q 𝑞}⟩ = (⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩))
7470, 73breqtrrd 3956 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏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 𝑞}⟩)<P ⟨{𝑝𝑝 <Q (𝑦 +Q 𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q 𝑞}⟩)
75 simplrr 525 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) → (𝑦 +Q 𝑄) = 𝑥)
7675adantr 274 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → (𝑦 +Q 𝑄) = 𝑥)
77 breq2 3933 . . . . . . . . . . . . . . . . 17 ((𝑦 +Q 𝑄) = 𝑥 → (𝑝 <Q (𝑦 +Q 𝑄) ↔ 𝑝 <Q 𝑥))
7877abbidv 2257 . . . . . . . . . . . . . . . 16 ((𝑦 +Q 𝑄) = 𝑥 → {𝑝𝑝 <Q (𝑦 +Q 𝑄)} = {𝑝𝑝 <Q 𝑥})
79 breq1 3932 . . . . . . . . . . . . . . . . 17 ((𝑦 +Q 𝑄) = 𝑥 → ((𝑦 +Q 𝑄) <Q 𝑞𝑥 <Q 𝑞))
8079abbidv 2257 . . . . . . . . . . . . . . . 16 ((𝑦 +Q 𝑄) = 𝑥 → {𝑞 ∣ (𝑦 +Q 𝑄) <Q 𝑞} = {𝑞𝑥 <Q 𝑞})
8178, 80opeq12d 3713 . . . . . . . . . . . . . . 15 ((𝑦 +Q 𝑄) = 𝑥 → ⟨{𝑝𝑝 <Q (𝑦 +Q 𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q 𝑞}⟩ = ⟨{𝑝𝑝 <Q 𝑥}, {𝑞𝑥 <Q 𝑞}⟩)
8281breq2d 3941 . . . . . . . . . . . . . 14 ((𝑦 +Q 𝑄) = 𝑥 → ((((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q (𝑦 +Q 𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q 𝑞}⟩ ↔ (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑥}, {𝑞𝑥 <Q 𝑞}⟩))
8376, 82syl 14 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏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 𝑞}⟩)<P ⟨{𝑝𝑝 <Q (𝑦 +Q 𝑄)}, {𝑞 ∣ (𝑦 +Q 𝑄) <Q 𝑞}⟩ ↔ (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑥}, {𝑞𝑥 <Q 𝑞}⟩))
8474, 83mpbid 146 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏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 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑥}, {𝑞𝑥 <Q 𝑞}⟩)
85 simplrl 524 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) → 𝑥Q)
8685ad2antrr 479 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → 𝑥Q)
87 addclpr 7352 . . . . . . . . . . . . . 14 ((((𝐹𝑏) +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 𝑞}⟩) ∈ P)
8860, 66, 87syl2anc 408 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏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 𝑞}⟩) ∈ P)
89 nqpru 7367 . . . . . . . . . . . . 13 ((𝑥Q ∧ (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P) → (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ↔ (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑥}, {𝑞𝑥 <Q 𝑞}⟩))
9086, 88, 89syl2anc 408 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ↔ (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑥}, {𝑞𝑥 <Q 𝑞}⟩))
9184, 90mpbird 166 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → 𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)))
92 simprrr 529 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → 𝑥 ∈ (1st𝑇))
9392ad3antrrr 483 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → 𝑥 ∈ (1st𝑇))
9491, 93jca 304 . . . . . . . . . 10 (((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) ∧ ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩) → (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))
9594ex 114 . . . . . . . . 9 ((((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) ∧ 𝑏N) → (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ → (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
9695reximdva 2534 . . . . . . . 8 (((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) → (∃𝑏N ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑦}, {𝑞𝑦 <Q 𝑞}⟩ → ∃𝑏N (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
9750, 96mpd 13 . . . . . . 7 (((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) ∧ (𝑦 ∈ (2nd𝐿) ∧ (𝑦 +Q 𝑄) = 𝑥)) → ∃𝑏N (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))
9819, 97rexlimddv 2554 . . . . . 6 ((𝜑 ∧ (𝑥Q ∧ (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))) → ∃𝑏N (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))
9998expr 372 . . . . 5 ((𝜑𝑥Q) → ((𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)) → ∃𝑏N (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
10099reximdva 2534 . . . 4 (𝜑 → (∃𝑥Q (𝑥 ∈ (2nd ‘(𝐿 +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)) → ∃𝑥Q𝑏N (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
10115, 100mpd 13 . . 3 (𝜑 → ∃𝑥Q𝑏N (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))
102 rexcom 2595 . . 3 (∃𝑥Q𝑏N (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)) ↔ ∃𝑏N𝑥Q (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))
103101, 102sylib 121 . 2 (𝜑 → ∃𝑏N𝑥Q (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇)))
1042ffvelrnda 5555 . . . . . 6 ((𝜑𝑏N) → (𝐹𝑏) ∈ P)
10557adantl 275 . . . . . 6 ((𝜑𝑏N) → ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩ ∈ P)
106104, 105, 59syl2anc 408 . . . . 5 ((𝜑𝑏N) → ((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) ∈ P)
1079adantr 274 . . . . 5 ((𝜑𝑏N) → ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩ ∈ P)
108106, 107, 87syl2anc 408 . . . 4 ((𝜑𝑏N) → (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P)
10912adantr 274 . . . 4 ((𝜑𝑏N) → 𝑇P)
110 ltdfpr 7321 . . . 4 (((((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩) ∈ P𝑇P) → ((((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P 𝑇 ↔ ∃𝑥Q (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
111108, 109, 110syl2anc 408 . . 3 ((𝜑𝑏N) → ((((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P 𝑇 ↔ ∃𝑥Q (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
112111rexbidva 2434 . 2 (𝜑 → (∃𝑏N (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P 𝑇 ↔ ∃𝑏N𝑥Q (𝑥 ∈ (2nd ‘(((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)) ∧ 𝑥 ∈ (1st𝑇))))
113103, 112mpbird 166 1 (𝜑 → ∃𝑏N (((𝐹𝑏) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝𝑝 <Q 𝑄}, {𝑞𝑄 <Q 𝑞}⟩)<P 𝑇)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 962   = wceq 1331   ∈ wcel 1480  {cab 2125  ∀wral 2416  ∃wrex 2417  {crab 2420  ⟨cop 3530   class class class wbr 3929  ⟶wf 5119  ‘cfv 5123  (class class class)co 5774  1st c1st 6036  2nd c2nd 6037  1oc1o 6306  [cec 6427  Ncnpi 7087
 Copyright terms: Public domain W3C validator