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

Theorem caucvgsrlemgt1 6877
Description: Lemma for caucvgsr 6884. A Cauchy sequence whose terms are greater than one converges. (Contributed by Jim Kingdon, 22-Jun-2021.)
Hypotheses
Ref Expression
caucvgsr.f (𝜑𝐹:NR)
caucvgsr.cau (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛) <R ((𝐹𝑘) +R [⟨(⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹𝑘) <R ((𝐹𝑛) +R [⟨(⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))
caucvgsrlemgt1.gt1 (𝜑 → ∀𝑚N 1R <R (𝐹𝑚))
Assertion
Ref Expression
caucvgsrlemgt1 (𝜑 → ∃𝑦R𝑥R (0R <R 𝑥 → ∃𝑗N𝑖N (𝑗 <N 𝑖 → ((𝐹𝑖) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹𝑖) +R 𝑥)))))
Distinct variable groups:   𝑗,𝐹,𝑘,𝑙,𝑢   𝑖,𝐹,𝑥,𝑗,𝑘   𝑚,𝐹,𝑛,𝑘   𝑛,𝑙,𝑢   𝑦,𝐹,𝑖,𝑗,𝑥   𝜑,𝑗,𝑘,𝑥   𝜑,𝑛   𝑘,𝑚,𝑛
Allowed substitution hints:   𝜑(𝑦,𝑢,𝑖,𝑚,𝑙)

Proof of Theorem caucvgsrlemgt1
Dummy variables 𝑎 𝑏 𝑤 𝑧 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 caucvgsr.f . . . 4 (𝜑𝐹:NR)
2 caucvgsr.cau . . . 4 (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛) <R ((𝐹𝑘) +R [⟨(⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹𝑘) <R ((𝐹𝑛) +R [⟨(⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))
3 caucvgsrlemgt1.gt1 . . . 4 (𝜑 → ∀𝑚N 1R <R (𝐹𝑚))
4 eqid 2040 . . . 4 (𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R )) = (𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))
51, 2, 3, 4caucvgsrlemf 6874 . . 3 (𝜑 → (𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R )):NP)
61, 2, 3, 4caucvgsrlemcau 6875 . . 3 (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑛)<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ ((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
71, 2, 3, 4caucvgsrlembound 6876 . . 3 (𝜑 → ∀𝑚N 1P<P ((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑚))
85, 6, 7caucvgprpr 6808 . 2 (𝜑 → ∃𝑎P𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))
9 prsrcl 6866 . . . 4 (𝑎P → [⟨(𝑎 +P 1P), 1P⟩] ~RR)
109ad2antrl 459 . . 3 ((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) → [⟨(𝑎 +P 1P), 1P⟩] ~RR)
11 srpospr 6865 . . . . . . . . . 10 ((𝑥R ∧ 0R <R 𝑥) → ∃!𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)
12 riotacl 5482 . . . . . . . . . 10 (∃!𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥 → (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) ∈ P)
1311, 12syl 14 . . . . . . . . 9 ((𝑥R ∧ 0R <R 𝑥) → (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) ∈ P)
1413adantll 445 . . . . . . . 8 ((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) → (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) ∈ P)
15 simplrr 488 . . . . . . . . 9 (((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) → ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))
1615adantr 261 . . . . . . . 8 ((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) → ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))
17 oveq2 5520 . . . . . . . . . . . . 13 (𝑏 = (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) → (𝑎 +P 𝑏) = (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)))
1817breq2d 3776 . . . . . . . . . . . 12 (𝑏 = (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ↔ ((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥))))
19 oveq2 5520 . . . . . . . . . . . . 13 (𝑏 = (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏) = (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)))
2019breq2d 3776 . . . . . . . . . . . 12 (𝑏 = (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) → (𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏) ↔ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥))))
2118, 20anbi12d 442 . . . . . . . . . . 11 (𝑏 = (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) → ((((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)) ↔ (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)))))
2221imbi2d 219 . . . . . . . . . 10 (𝑏 = (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) → ((𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))) ↔ (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥))))))
2322rexralbidv 2350 . . . . . . . . 9 (𝑏 = (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) → (∃𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))) ↔ ∃𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥))))))
2423rspcva 2654 . . . . . . . 8 (((𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) ∈ P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))) → ∃𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)))))
2514, 16, 24syl2anc 391 . . . . . . 7 ((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) → ∃𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)))))
26 nfv 1421 . . . . . . . . . . 11 𝑗𝜑
27 nfv 1421 . . . . . . . . . . . 12 𝑗 𝑎P
28 nfcv 2178 . . . . . . . . . . . . 13 𝑗P
29 nfre1 2365 . . . . . . . . . . . . 13 𝑗𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
3028, 29nfralya 2362 . . . . . . . . . . . 12 𝑗𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
3127, 30nfan 1457 . . . . . . . . . . 11 𝑗(𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))
3226, 31nfan 1457 . . . . . . . . . 10 𝑗(𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))))
33 nfv 1421 . . . . . . . . . 10 𝑗 𝑥R
3432, 33nfan 1457 . . . . . . . . 9 𝑗((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R)
35 nfv 1421 . . . . . . . . 9 𝑗0R <R 𝑥
3634, 35nfan 1457 . . . . . . . 8 𝑗(((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥)
37 nfv 1421 . . . . . . . . . . . 12 𝑘𝜑
38 nfv 1421 . . . . . . . . . . . . 13 𝑘 𝑎P
39 nfcv 2178 . . . . . . . . . . . . . 14 𝑘P
40 nfcv 2178 . . . . . . . . . . . . . . 15 𝑘N
41 nfra1 2355 . . . . . . . . . . . . . . 15 𝑘𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
4240, 41nfrexya 2363 . . . . . . . . . . . . . 14 𝑘𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
4339, 42nfralya 2362 . . . . . . . . . . . . 13 𝑘𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
4438, 43nfan 1457 . . . . . . . . . . . 12 𝑘(𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))
4537, 44nfan 1457 . . . . . . . . . . 11 𝑘(𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))))
46 nfv 1421 . . . . . . . . . . 11 𝑘 𝑥R
4745, 46nfan 1457 . . . . . . . . . 10 𝑘((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R)
48 nfv 1421 . . . . . . . . . 10 𝑘0R <R 𝑥
4947, 48nfan 1457 . . . . . . . . 9 𝑘(((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥)
505ad4antr 463 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) ∧ 𝑘N) → (𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R )):NP)
51 simpr 103 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) ∧ 𝑘N) → 𝑘N)
5250, 51ffvelrnd 5303 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) ∧ 𝑘N) → ((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) ∈ P)
53 simplrl 487 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) → 𝑎P)
5453adantr 261 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) → 𝑎P)
55 addclpr 6633 . . . . . . . . . . . . . . 15 ((𝑎P ∧ (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) ∈ P) → (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ∈ P)
5654, 14, 55syl2anc 391 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) → (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ∈ P)
5756adantr 261 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) ∧ 𝑘N) → (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ∈ P)
58 prsrlt 6869 . . . . . . . . . . . . 13 ((((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) ∈ P ∧ (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ∈ P) → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ↔ [⟨(((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 1P), 1P⟩] ~R <R [⟨((𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) +P 1P), 1P⟩] ~R ))
5952, 57, 58syl2anc 391 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) ∧ 𝑘N) → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ↔ [⟨(((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 1P), 1P⟩] ~R <R [⟨((𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) +P 1P), 1P⟩] ~R ))
601, 2, 3, 4caucvgsrlemfv 6873 . . . . . . . . . . . . . . . 16 ((𝜑𝑘N) → [⟨(((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 1P), 1P⟩] ~R = (𝐹𝑘))
6160adantlr 446 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑘N) → [⟨(((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 1P), 1P⟩] ~R = (𝐹𝑘))
6261adantlr 446 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 𝑘N) → [⟨(((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 1P), 1P⟩] ~R = (𝐹𝑘))
6362adantlr 446 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) ∧ 𝑘N) → [⟨(((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 1P), 1P⟩] ~R = (𝐹𝑘))
64 prsradd 6868 . . . . . . . . . . . . . . . 16 ((𝑎P ∧ (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) ∈ P) → [⟨((𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) +P 1P), 1P⟩] ~R = ([⟨(𝑎 +P 1P), 1P⟩] ~R +R [⟨((𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) +P 1P), 1P⟩] ~R ))
6554, 14, 64syl2anc 391 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) → [⟨((𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) +P 1P), 1P⟩] ~R = ([⟨(𝑎 +P 1P), 1P⟩] ~R +R [⟨((𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) +P 1P), 1P⟩] ~R ))
66 prsrriota 6870 . . . . . . . . . . . . . . . . 17 ((𝑥R ∧ 0R <R 𝑥) → [⟨((𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) +P 1P), 1P⟩] ~R = 𝑥)
6766oveq2d 5528 . . . . . . . . . . . . . . . 16 ((𝑥R ∧ 0R <R 𝑥) → ([⟨(𝑎 +P 1P), 1P⟩] ~R +R [⟨((𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) +P 1P), 1P⟩] ~R ) = ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥))
6867adantll 445 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) → ([⟨(𝑎 +P 1P), 1P⟩] ~R +R [⟨((𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) +P 1P), 1P⟩] ~R ) = ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥))
6965, 68eqtrd 2072 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) → [⟨((𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) +P 1P), 1P⟩] ~R = ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥))
7069adantr 261 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) ∧ 𝑘N) → [⟨((𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) +P 1P), 1P⟩] ~R = ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥))
7163, 70breq12d 3777 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) ∧ 𝑘N) → ([⟨(((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 1P), 1P⟩] ~R <R [⟨((𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) +P 1P), 1P⟩] ~R ↔ (𝐹𝑘) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥)))
7259, 71bitrd 177 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) ∧ 𝑘N) → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ↔ (𝐹𝑘) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥)))
7354adantr 261 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) ∧ 𝑘N) → 𝑎P)
7414adantr 261 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) ∧ 𝑘N) → (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) ∈ P)
75 addclpr 6633 . . . . . . . . . . . . . 14 ((((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) ∈ P ∧ (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) ∈ P) → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ∈ P)
7652, 74, 75syl2anc 391 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) ∧ 𝑘N) → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ∈ P)
77 prsrlt 6869 . . . . . . . . . . . . 13 ((𝑎P ∧ (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ∈ P) → (𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ↔ [⟨(𝑎 +P 1P), 1P⟩] ~R <R [⟨((((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) +P 1P), 1P⟩] ~R ))
7873, 76, 77syl2anc 391 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) ∧ 𝑘N) → (𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ↔ [⟨(𝑎 +P 1P), 1P⟩] ~R <R [⟨((((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) +P 1P), 1P⟩] ~R ))
79 prsradd 6868 . . . . . . . . . . . . . 14 ((((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) ∈ P ∧ (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) ∈ P) → [⟨((((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) +P 1P), 1P⟩] ~R = ([⟨(((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 1P), 1P⟩] ~R +R [⟨((𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) +P 1P), 1P⟩] ~R ))
8052, 74, 79syl2anc 391 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) ∧ 𝑘N) → [⟨((((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) +P 1P), 1P⟩] ~R = ([⟨(((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 1P), 1P⟩] ~R +R [⟨((𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) +P 1P), 1P⟩] ~R ))
8180breq2d 3776 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) ∧ 𝑘N) → ([⟨(𝑎 +P 1P), 1P⟩] ~R <R [⟨((((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) +P 1P), 1P⟩] ~R ↔ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ([⟨(((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 1P), 1P⟩] ~R +R [⟨((𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) +P 1P), 1P⟩] ~R )))
8266adantll 445 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) → [⟨((𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) +P 1P), 1P⟩] ~R = 𝑥)
8382adantr 261 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) ∧ 𝑘N) → [⟨((𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) +P 1P), 1P⟩] ~R = 𝑥)
8463, 83oveq12d 5530 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) ∧ 𝑘N) → ([⟨(((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 1P), 1P⟩] ~R +R [⟨((𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) +P 1P), 1P⟩] ~R ) = ((𝐹𝑘) +R 𝑥))
8584breq2d 3776 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) ∧ 𝑘N) → ([⟨(𝑎 +P 1P), 1P⟩] ~R <R ([⟨(((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 1P), 1P⟩] ~R +R [⟨((𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) +P 1P), 1P⟩] ~R ) ↔ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑘) +R 𝑥)))
8678, 81, 853bitrd 203 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) ∧ 𝑘N) → (𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ↔ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑘) +R 𝑥)))
8772, 86anbi12d 442 . . . . . . . . . 10 (((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) ∧ 𝑘N) → ((((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥))) ↔ ((𝐹𝑘) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑘) +R 𝑥))))
8887imbi2d 219 . . . . . . . . 9 (((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) ∧ 𝑘N) → ((𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)))) ↔ (𝑗 <N 𝑘 → ((𝐹𝑘) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑘) +R 𝑥)))))
8949, 88ralbida 2320 . . . . . . . 8 ((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) → (∀𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)))) ↔ ∀𝑘N (𝑗 <N 𝑘 → ((𝐹𝑘) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑘) +R 𝑥)))))
9036, 89rexbid 2325 . . . . . . 7 ((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) → (∃𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)))) ↔ ∃𝑗N𝑘N (𝑗 <N 𝑘 → ((𝐹𝑘) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑘) +R 𝑥)))))
9125, 90mpbid 135 . . . . . 6 ((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) → ∃𝑗N𝑘N (𝑗 <N 𝑘 → ((𝐹𝑘) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑘) +R 𝑥))))
92 breq2 3768 . . . . . . . . 9 (𝑘 = 𝑖 → (𝑗 <N 𝑘𝑗 <N 𝑖))
93 fveq2 5178 . . . . . . . . . . 11 (𝑘 = 𝑖 → (𝐹𝑘) = (𝐹𝑖))
9493breq1d 3774 . . . . . . . . . 10 (𝑘 = 𝑖 → ((𝐹𝑘) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ↔ (𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥)))
9593oveq1d 5527 . . . . . . . . . . 11 (𝑘 = 𝑖 → ((𝐹𝑘) +R 𝑥) = ((𝐹𝑖) +R 𝑥))
9695breq2d 3776 . . . . . . . . . 10 (𝑘 = 𝑖 → ([⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑘) +R 𝑥) ↔ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥)))
9794, 96anbi12d 442 . . . . . . . . 9 (𝑘 = 𝑖 → (((𝐹𝑘) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑘) +R 𝑥)) ↔ ((𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥))))
9892, 97imbi12d 223 . . . . . . . 8 (𝑘 = 𝑖 → ((𝑗 <N 𝑘 → ((𝐹𝑘) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑘) +R 𝑥))) ↔ (𝑗 <N 𝑖 → ((𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥)))))
9998cbvralv 2533 . . . . . . 7 (∀𝑘N (𝑗 <N 𝑘 → ((𝐹𝑘) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑘) +R 𝑥))) ↔ ∀𝑖N (𝑗 <N 𝑖 → ((𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥))))
10099rexbii 2331 . . . . . 6 (∃𝑗N𝑘N (𝑗 <N 𝑘 → ((𝐹𝑘) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑘) +R 𝑥))) ↔ ∃𝑗N𝑖N (𝑗 <N 𝑖 → ((𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥))))
10191, 100sylib 127 . . . . 5 ((((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) ∧ 0R <R 𝑥) → ∃𝑗N𝑖N (𝑗 <N 𝑖 → ((𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥))))
102101ex 108 . . . 4 (((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) → (0R <R 𝑥 → ∃𝑗N𝑖N (𝑗 <N 𝑖 → ((𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥)))))
103102ralrimiva 2392 . . 3 ((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) → ∀𝑥R (0R <R 𝑥 → ∃𝑗N𝑖N (𝑗 <N 𝑖 → ((𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥)))))
104 oveq1 5519 . . . . . . . . . 10 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → (𝑦 +R 𝑥) = ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥))
105104breq2d 3776 . . . . . . . . 9 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → ((𝐹𝑖) <R (𝑦 +R 𝑥) ↔ (𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥)))
106 breq1 3767 . . . . . . . . 9 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → (𝑦 <R ((𝐹𝑖) +R 𝑥) ↔ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥)))
107105, 106anbi12d 442 . . . . . . . 8 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → (((𝐹𝑖) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹𝑖) +R 𝑥)) ↔ ((𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥))))
108107imbi2d 219 . . . . . . 7 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → ((𝑗 <N 𝑖 → ((𝐹𝑖) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹𝑖) +R 𝑥))) ↔ (𝑗 <N 𝑖 → ((𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥)))))
109108rexralbidv 2350 . . . . . 6 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → (∃𝑗N𝑖N (𝑗 <N 𝑖 → ((𝐹𝑖) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹𝑖) +R 𝑥))) ↔ ∃𝑗N𝑖N (𝑗 <N 𝑖 → ((𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥)))))
110109imbi2d 219 . . . . 5 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → ((0R <R 𝑥 → ∃𝑗N𝑖N (𝑗 <N 𝑖 → ((𝐹𝑖) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹𝑖) +R 𝑥)))) ↔ (0R <R 𝑥 → ∃𝑗N𝑖N (𝑗 <N 𝑖 → ((𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥))))))
111110ralbidv 2326 . . . 4 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → (∀𝑥R (0R <R 𝑥 → ∃𝑗N𝑖N (𝑗 <N 𝑖 → ((𝐹𝑖) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹𝑖) +R 𝑥)))) ↔ ∀𝑥R (0R <R 𝑥 → ∃𝑗N𝑖N (𝑗 <N 𝑖 → ((𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥))))))
112111rspcev 2656 . . 3 (([⟨(𝑎 +P 1P), 1P⟩] ~RR ∧ ∀𝑥R (0R <R 𝑥 → ∃𝑗N𝑖N (𝑗 <N 𝑖 → ((𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥))))) → ∃𝑦R𝑥R (0R <R 𝑥 → ∃𝑗N𝑖N (𝑗 <N 𝑖 → ((𝐹𝑖) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹𝑖) +R 𝑥)))))
11310, 103, 112syl2anc 391 . 2 ((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) → ∃𝑦R𝑥R (0R <R 𝑥 → ∃𝑗N𝑖N (𝑗 <N 𝑖 → ((𝐹𝑖) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹𝑖) +R 𝑥)))))
1148, 113rexlimddv 2437 1 (𝜑 → ∃𝑦R𝑥R (0R <R 𝑥 → ∃𝑗N𝑖N (𝑗 <N 𝑖 → ((𝐹𝑖) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹𝑖) +R 𝑥)))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wb 98   = wceq 1243  wcel 1393  {cab 2026  wral 2306  wrex 2307  ∃!wreu 2308  cop 3378   class class class wbr 3764  cmpt 3818  wf 4898  cfv 4902  crio 5467  (class class class)co 5512  1𝑜c1o 5994  [cec 6104  Ncnpi 6368   <N clti 6371   ~Q ceq 6375  *Qcrq 6380   <Q cltq 6381  Pcnp 6387  1Pc1p 6388   +P cpp 6389  <P cltp 6391   ~R cer 6392  Rcnr 6393  0Rc0r 6394  1Rc1r 6395   +R cplr 6397   <R cltr 6399
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-13 1404  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-coll 3872  ax-sep 3875  ax-nul 3883  ax-pow 3927  ax-pr 3944  ax-un 4170  ax-setind 4262  ax-iinf 4311
This theorem depends on definitions:  df-bi 110  df-dc 743  df-3or 886  df-3an 887  df-tru 1246  df-fal 1249  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ne 2206  df-ral 2311  df-rex 2312  df-reu 2313  df-rmo 2314  df-rab 2315  df-v 2559  df-sbc 2765  df-csb 2853  df-dif 2920  df-un 2922  df-in 2924  df-ss 2931  df-nul 3225  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-int 3616  df-iun 3659  df-br 3765  df-opab 3819  df-mpt 3820  df-tr 3855  df-eprel 4026  df-id 4030  df-po 4033  df-iso 4034  df-iord 4103  df-on 4105  df-suc 4108  df-iom 4314  df-xp 4351  df-rel 4352  df-cnv 4353  df-co 4354  df-dm 4355  df-rn 4356  df-res 4357  df-ima 4358  df-iota 4867  df-fun 4904  df-fn 4905  df-f 4906  df-f1 4907  df-fo 4908  df-f1o 4909  df-fv 4910  df-riota 5468  df-ov 5515  df-oprab 5516  df-mpt2 5517  df-1st 5767  df-2nd 5768  df-recs 5920  df-irdg 5957  df-1o 6001  df-2o 6002  df-oadd 6005  df-omul 6006  df-er 6106  df-ec 6108  df-qs 6112  df-ni 6400  df-pli 6401  df-mi 6402  df-lti 6403  df-plpq 6440  df-mpq 6441  df-enq 6443  df-nqqs 6444  df-plqqs 6445  df-mqqs 6446  df-1nqqs 6447  df-rq 6448  df-ltnqqs 6449  df-enq0 6520  df-nq0 6521  df-0nq0 6522  df-plq0 6523  df-mq0 6524  df-inp 6562  df-i1p 6563  df-iplp 6564  df-iltp 6566  df-enr 6809  df-nr 6810  df-plr 6811  df-ltr 6813  df-0r 6814  df-1r 6815
This theorem is referenced by:  caucvgsrlemoffres  6882
  Copyright terms: Public domain W3C validator