ILE Home 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   <N clti 7090   ~Q ceq 7094  Qcnq 7095   +Q cplq 7097  *Qcrq 7099   <Q cltq 7100  Pcnp 7106   +P cpp 7108  <P cltp 7110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502
This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-eprel 4211  df-id 4215  df-po 4218  df-iso 4219  df-iord 4288  df-on 4290  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-irdg 6267  df-1o 6313  df-2o 6314  df-oadd 6317  df-omul 6318  df-er 6429  df-ec 6431  df-qs 6435  df-ni 7119  df-pli 7120  df-mi 7121  df-lti 7122  df-plpq 7159  df-mpq 7160  df-enq 7162  df-nqqs 7163  df-plqqs 7164  df-mqqs 7165  df-1nqqs 7166  df-rq 7167  df-ltnqqs 7168  df-enq0 7239  df-nq0 7240  df-0nq0 7241  df-plq0 7242  df-mq0 7243  df-inp 7281  df-iplp 7283  df-iltp 7285
This theorem is referenced by:  caucvgprprlemexb  7522
  Copyright terms: Public domain W3C validator