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

Theorem caucvgsrlemgt1 7022
Description: Lemma for caucvgsr 7029. 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 2082 . . . 4 (𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R )) = (𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))
51, 2, 3, 4caucvgsrlemf 7019 . . 3 (𝜑 → (𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R )):NP)
61, 2, 3, 4caucvgsrlemcau 7020 . . 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 7021 . . 3 (𝜑 → ∀𝑚N 1P<P ((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑚))
85, 6, 7caucvgprpr 6953 . 2 (𝜑 → ∃𝑎P𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))
9 prsrcl 7011 . . . 4 (𝑎P → [⟨(𝑎 +P 1P), 1P⟩] ~RR)
109ad2antrl 474 . . 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 7010 . . . . . . . . . 10 ((𝑥R ∧ 0R <R 𝑥) → ∃!𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)
12 riotacl 5507 . . . . . . . . . 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 460 . . . . . . . 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 503 . . . . . . . . 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 270 . . . . . . . 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 5545 . . . . . . . . . . . . 13 (𝑏 = (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) → (𝑎 +P 𝑏) = (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)))
1817breq2d 3799 . . . . . . . . . . . 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 5545 . . . . . . . . . . . . 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 3799 . . . . . . . . . . . 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 457 . . . . . . . . . . 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 228 . . . . . . . . . 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 2393 . . . . . . . . 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 2700 . . . . . . . 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 403 . . . . . . 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 1462 . . . . . . . . . . 11 𝑗𝜑
27 nfv 1462 . . . . . . . . . . . 12 𝑗 𝑎P
28 nfcv 2220 . . . . . . . . . . . . 13 𝑗P
29 nfre1 2408 . . . . . . . . . . . . 13 𝑗𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
3028, 29nfralya 2405 . . . . . . . . . . . 12 𝑗𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
3127, 30nfan 1498 . . . . . . . . . . 11 𝑗(𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))
3226, 31nfan 1498 . . . . . . . . . 10 𝑗(𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))))
33 nfv 1462 . . . . . . . . . 10 𝑗 𝑥R
3432, 33nfan 1498 . . . . . . . . 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 1462 . . . . . . . . 9 𝑗0R <R 𝑥
3634, 35nfan 1498 . . . . . . . 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 1462 . . . . . . . . . . . 12 𝑘𝜑
38 nfv 1462 . . . . . . . . . . . . 13 𝑘 𝑎P
39 nfcv 2220 . . . . . . . . . . . . . 14 𝑘P
40 nfcv 2220 . . . . . . . . . . . . . . 15 𝑘N
41 nfra1 2398 . . . . . . . . . . . . . . 15 𝑘𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
4240, 41nfrexya 2406 . . . . . . . . . . . . . 14 𝑘𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
4339, 42nfralya 2405 . . . . . . . . . . . . 13 𝑘𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
4438, 43nfan 1498 . . . . . . . . . . . 12 𝑘(𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))
4537, 44nfan 1498 . . . . . . . . . . 11 𝑘(𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))))
46 nfv 1462 . . . . . . . . . . 11 𝑘 𝑥R
4745, 46nfan 1498 . . . . . . . . . 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 1462 . . . . . . . . . 10 𝑘0R <R 𝑥
4947, 48nfan 1498 . . . . . . . . 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 478 . . . . . . . . . . . . . 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 108 . . . . . . . . . . . . . 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 5329 . . . . . . . . . . . . 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 502 . . . . . . . . . . . . . . . 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 270 . . . . . . . . . . . . . . 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 6778 . . . . . . . . . . . . . . 15 ((𝑎P ∧ (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) ∈ P) → (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ∈ P)
5654, 14, 55syl2anc 403 . . . . . . . . . . . . . 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 270 . . . . . . . . . . . . 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 7014 . . . . . . . . . . . . 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 403 . . . . . . . . . . . 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 7018 . . . . . . . . . . . . . . . 16 ((𝜑𝑘N) → [⟨(((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 1P), 1P⟩] ~R = (𝐹𝑘))
6160adantlr 461 . . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . 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 7013 . . . . . . . . . . . . . . . 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 403 . . . . . . . . . . . . . . 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 7015 . . . . . . . . . . . . . . . . 17 ((𝑥R ∧ 0R <R 𝑥) → [⟨((𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) +P 1P), 1P⟩] ~R = 𝑥)
6766oveq2d 5553 . . . . . . . . . . . . . . . 16 ((𝑥R ∧ 0R <R 𝑥) → ([⟨(𝑎 +P 1P), 1P⟩] ~R +R [⟨((𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) +P 1P), 1P⟩] ~R ) = ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥))
6867adantll 460 . . . . . . . . . . . . . . 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 2114 . . . . . . . . . . . . . 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 270 . . . . . . . . . . . . 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 3800 . . . . . . . . . . . 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 186 . . . . . . . . . . 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 270 . . . . . . . . . . . . 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 270 . . . . . . . . . . . . . 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 6778 . . . . . . . . . . . . . 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 403 . . . . . . . . . . . . 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 7014 . . . . . . . . . . . . 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 403 . . . . . . . . . . . 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 7013 . . . . . . . . . . . . . 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 403 . . . . . . . . . . . . 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 3799 . . . . . . . . . . . 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 460 . . . . . . . . . . . . . . 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 270 . . . . . . . . . . . . . 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 5555 . . . . . . . . . . . . 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 3799 . . . . . . . . . . . 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 212 . . . . . . . . . . 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 457 . . . . . . . . . 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 228 . . . . . . . . 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 2363 . . . . . . . 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 2368 . . . . . . 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 145 . . . . . 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 3791 . . . . . . . . 9 (𝑘 = 𝑖 → (𝑗 <N 𝑘𝑗 <N 𝑖))
93 fveq2 5203 . . . . . . . . . . 11 (𝑘 = 𝑖 → (𝐹𝑘) = (𝐹𝑖))
9493breq1d 3797 . . . . . . . . . 10 (𝑘 = 𝑖 → ((𝐹𝑘) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ↔ (𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥)))
9593oveq1d 5552 . . . . . . . . . . 11 (𝑘 = 𝑖 → ((𝐹𝑘) +R 𝑥) = ((𝐹𝑖) +R 𝑥))
9695breq2d 3799 . . . . . . . . . 10 (𝑘 = 𝑖 → ([⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑘) +R 𝑥) ↔ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥)))
9794, 96anbi12d 457 . . . . . . . . 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 232 . . . . . . . 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 2578 . . . . . . 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 2374 . . . . . 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 120 . . . . 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 113 . . . 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 2435 . . 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 5544 . . . . . . . . . 10 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → (𝑦 +R 𝑥) = ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥))
105104breq2d 3799 . . . . . . . . 9 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → ((𝐹𝑖) <R (𝑦 +R 𝑥) ↔ (𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥)))
106 breq1 3790 . . . . . . . . 9 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → (𝑦 <R ((𝐹𝑖) +R 𝑥) ↔ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥)))
107105, 106anbi12d 457 . . . . . . . 8 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → (((𝐹𝑖) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹𝑖) +R 𝑥)) ↔ ((𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥))))
108107imbi2d 228 . . . . . . 7 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → ((𝑗 <N 𝑖 → ((𝐹𝑖) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹𝑖) +R 𝑥))) ↔ (𝑗 <N 𝑖 → ((𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥)))))
109108rexralbidv 2393 . . . . . 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 228 . . . . 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 2369 . . . 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 2702 . . 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 403 . 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 2482 1 (𝜑 → ∃𝑦R𝑥R (0R <R 𝑥 → ∃𝑗N𝑖N (𝑗 <N 𝑖 → ((𝐹𝑖) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹𝑖) +R 𝑥)))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103   = wceq 1285  wcel 1434  {cab 2068  wral 2349  wrex 2350  ∃!wreu 2351  cop 3403   class class class wbr 3787  cmpt 3841  wf 4922  cfv 4926  crio 5492  (class class class)co 5537  1𝑜c1o 6052  [cec 6163  Ncnpi 6513   <N clti 6516   ~Q ceq 6520  *Qcrq 6525   <Q cltq 6526  Pcnp 6532  1Pc1p 6533   +P cpp 6534  <P cltp 6536   ~R cer 6537  Rcnr 6538  0Rc0r 6539  1Rc1r 6540   +R cplr 6542   <R cltr 6544
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-coll 3895  ax-sep 3898  ax-nul 3906  ax-pow 3950  ax-pr 3966  ax-un 4190  ax-setind 4282  ax-iinf 4331
This theorem depends on definitions:  df-bi 115  df-dc 777  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1687  df-eu 1945  df-mo 1946  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-ne 2247  df-ral 2354  df-rex 2355  df-reu 2356  df-rmo 2357  df-rab 2358  df-v 2604  df-sbc 2817  df-csb 2910  df-dif 2976  df-un 2978  df-in 2980  df-ss 2987  df-nul 3253  df-pw 3386  df-sn 3406  df-pr 3407  df-op 3409  df-uni 3604  df-int 3639  df-iun 3682  df-br 3788  df-opab 3842  df-mpt 3843  df-tr 3878  df-eprel 4046  df-id 4050  df-po 4053  df-iso 4054  df-iord 4123  df-on 4125  df-suc 4128  df-iom 4334  df-xp 4371  df-rel 4372  df-cnv 4373  df-co 4374  df-dm 4375  df-rn 4376  df-res 4377  df-ima 4378  df-iota 4891  df-fun 4928  df-fn 4929  df-f 4930  df-f1 4931  df-fo 4932  df-f1o 4933  df-fv 4934  df-riota 5493  df-ov 5540  df-oprab 5541  df-mpt2 5542  df-1st 5792  df-2nd 5793  df-recs 5948  df-irdg 6013  df-1o 6059  df-2o 6060  df-oadd 6063  df-omul 6064  df-er 6165  df-ec 6167  df-qs 6171  df-ni 6545  df-pli 6546  df-mi 6547  df-lti 6548  df-plpq 6585  df-mpq 6586  df-enq 6588  df-nqqs 6589  df-plqqs 6590  df-mqqs 6591  df-1nqqs 6592  df-rq 6593  df-ltnqqs 6594  df-enq0 6665  df-nq0 6666  df-0nq0 6667  df-plq0 6668  df-mq0 6669  df-inp 6707  df-i1p 6708  df-iplp 6709  df-iltp 6711  df-enr 6954  df-nr 6955  df-plr 6956  df-ltr 6958  df-0r 6959  df-1r 6960
This theorem is referenced by:  caucvgsrlemoffres  7027
  Copyright terms: Public domain W3C validator