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

Theorem caucvgsrlemgt1 7757
Description: Lemma for caucvgsr 7764. 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‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹𝑘) <R ((𝐹𝑛) +R [⟨(⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~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‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹𝑘) <R ((𝐹𝑛) +R [⟨(⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))
3 caucvgsrlemgt1.gt1 . . . 4 (𝜑 → ∀𝑚N 1R <R (𝐹𝑚))
4 eqid 2170 . . . 4 (𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R )) = (𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))
51, 2, 3, 4caucvgsrlemf 7754 . . 3 (𝜑 → (𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R )):NP)
61, 2, 3, 4caucvgsrlemcau 7755 . . 3 (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑛)<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ ((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩))))
71, 2, 3, 4caucvgsrlembound 7756 . . 3 (𝜑 → ∀𝑚N 1P<P ((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑚))
85, 6, 7caucvgprpr 7674 . 2 (𝜑 → ∃𝑎P𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))
9 prsrcl 7746 . . . 4 (𝑎P → [⟨(𝑎 +P 1P), 1P⟩] ~RR)
109ad2antrl 487 . . 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 oveq2 5861 . . . . . . . . . . . 12 (𝑏 = (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) → (𝑎 +P 𝑏) = (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)))
1211breq2d 4001 . . . . . . . . . . 11 (𝑏 = (𝑐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 = 𝑥))))
13 oveq2 5861 . . . . . . . . . . . 12 (𝑏 = (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏) = (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)))
1413breq2d 4001 . . . . . . . . . . 11 (𝑏 = (𝑐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 = 𝑥))))
1512, 14anbi12d 470 . . . . . . . . . 10 (𝑏 = (𝑐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 = 𝑥)))))
1615imbi2d 229 . . . . . . . . 9 (𝑏 = (𝑐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 = 𝑥))))))
1716rexralbidv 2496 . . . . . . . 8 (𝑏 = (𝑐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 = 𝑥))))))
18 simplrr 531 . . . . . . . . 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 𝑏))))
1918adantr 274 . . . . . . . 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 𝑏))))
20 srpospr 7745 . . . . . . . . . 10 ((𝑥R ∧ 0R <R 𝑥) → ∃!𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)
21 riotacl 5823 . . . . . . . . . 10 (∃!𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥 → (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) ∈ P)
2220, 21syl 14 . . . . . . . . 9 ((𝑥R ∧ 0R <R 𝑥) → (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) ∈ P)
2322adantll 473 . . . . . . . 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)
2417, 19, 23rspcdva 2839 . . . . . . 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 = 𝑥)))))
25 nfv 1521 . . . . . . . . . . 11 𝑗𝜑
26 nfv 1521 . . . . . . . . . . . 12 𝑗 𝑎P
27 nfcv 2312 . . . . . . . . . . . . 13 𝑗P
28 nfre1 2513 . . . . . . . . . . . . 13 𝑗𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
2927, 28nfralya 2510 . . . . . . . . . . . 12 𝑗𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
3026, 29nfan 1558 . . . . . . . . . . 11 𝑗(𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))
3125, 30nfan 1558 . . . . . . . . . 10 𝑗(𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))))
32 nfv 1521 . . . . . . . . . 10 𝑗 𝑥R
3331, 32nfan 1558 . . . . . . . . 9 𝑗((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R)
34 nfv 1521 . . . . . . . . 9 𝑗0R <R 𝑥
3533, 34nfan 1558 . . . . . . . 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 𝑥)
36 nfv 1521 . . . . . . . . . . . 12 𝑘𝜑
37 nfv 1521 . . . . . . . . . . . . 13 𝑘 𝑎P
38 nfcv 2312 . . . . . . . . . . . . . 14 𝑘P
39 nfcv 2312 . . . . . . . . . . . . . . 15 𝑘N
40 nfra1 2501 . . . . . . . . . . . . . . 15 𝑘𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
4139, 40nfrexya 2511 . . . . . . . . . . . . . 14 𝑘𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
4238, 41nfralya 2510 . . . . . . . . . . . . 13 𝑘𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
4337, 42nfan 1558 . . . . . . . . . . . 12 𝑘(𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))
4436, 43nfan 1558 . . . . . . . . . . 11 𝑘(𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))))
45 nfv 1521 . . . . . . . . . . 11 𝑘 𝑥R
4644, 45nfan 1558 . . . . . . . . . 10 𝑘((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R)
47 nfv 1521 . . . . . . . . . 10 𝑘0R <R 𝑥
4846, 47nfan 1558 . . . . . . . . 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 𝑥)
495ad4antr 491 . . . . . . . . . . . . . 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)
50 simpr 109 . . . . . . . . . . . . . 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)
5149, 50ffvelrnd 5632 . . . . . . . . . . . . 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)
52 simplrl 530 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))) ∧ 𝑥R) → 𝑎P)
5352adantr 274 . . . . . . . . . . . . . . 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)
54 addclpr 7499 . . . . . . . . . . . . . . 15 ((𝑎P ∧ (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) ∈ P) → (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ∈ P)
5553, 23, 54syl2anc 409 . . . . . . . . . . . . . 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)
5655adantr 274 . . . . . . . . . . . . 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)
57 prsrlt 7749 . . . . . . . . . . . . 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 ))
5851, 56, 57syl2anc 409 . . . . . . . . . . . 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 ))
591, 2, 3, 4caucvgsrlemfv 7753 . . . . . . . . . . . . . . . 16 ((𝜑𝑘N) → [⟨(((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 1P), 1P⟩] ~R = (𝐹𝑘))
6059adantlr 474 . . . . . . . . . . . . . . 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 = (𝐹𝑘))
6160adantlr 474 . . . . . . . . . . . . . 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 = (𝐹𝑘))
6261adantlr 474 . . . . . . . . . . . . 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 = (𝐹𝑘))
63 prsradd 7748 . . . . . . . . . . . . . . . 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 ))
6453, 23, 63syl2anc 409 . . . . . . . . . . . . . . 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 ))
65 prsrriota 7750 . . . . . . . . . . . . . . . . 17 ((𝑥R ∧ 0R <R 𝑥) → [⟨((𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) +P 1P), 1P⟩] ~R = 𝑥)
6665oveq2d 5869 . . . . . . . . . . . . . . . 16 ((𝑥R ∧ 0R <R 𝑥) → ([⟨(𝑎 +P 1P), 1P⟩] ~R +R [⟨((𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) +P 1P), 1P⟩] ~R ) = ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥))
6766adantll 473 . . . . . . . . . . . . . . 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 𝑥))
6864, 67eqtrd 2203 . . . . . . . . . . . . . 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 𝑥))
6968adantr 274 . . . . . . . . . . . . 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 𝑥))
7062, 69breq12d 4002 . . . . . . . . . . . 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 𝑥)))
7158, 70bitrd 187 . . . . . . . . . . 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 𝑥)))
7253adantr 274 . . . . . . . . . . . . 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)
7323adantr 274 . . . . . . . . . . . . . 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)
74 addclpr 7499 . . . . . . . . . . . . . 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)
7551, 73, 74syl2anc 409 . . . . . . . . . . . . 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)
76 prsrlt 7749 . . . . . . . . . . . . 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 ))
7772, 75, 76syl2anc 409 . . . . . . . . . . . 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 ))
78 prsradd 7748 . . . . . . . . . . . . . 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 ))
7951, 73, 78syl2anc 409 . . . . . . . . . . . . 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 ))
8079breq2d 4001 . . . . . . . . . . . 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 )))
8165adantll 473 . . . . . . . . . . . . . . 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 = 𝑥)
8281adantr 274 . . . . . . . . . . . . . 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 = 𝑥)
8362, 82oveq12d 5871 . . . . . . . . . . . . 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 𝑥))
8483breq2d 4001 . . . . . . . . . . . 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 𝑥)))
8577, 80, 843bitrd 213 . . . . . . . . . . 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 𝑥)))
8671, 85anbi12d 470 . . . . . . . . . 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 𝑥))))
8786imbi2d 229 . . . . . . . . 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 𝑥)))))
8848, 87ralbida 2464 . . . . . . . 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 𝑥)))))
8935, 88rexbid 2469 . . . . . . 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 𝑥)))))
9024, 89mpbid 146 . . . . . 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 𝑥))))
91 breq2 3993 . . . . . . . . 9 (𝑘 = 𝑖 → (𝑗 <N 𝑘𝑗 <N 𝑖))
92 fveq2 5496 . . . . . . . . . . 11 (𝑘 = 𝑖 → (𝐹𝑘) = (𝐹𝑖))
9392breq1d 3999 . . . . . . . . . 10 (𝑘 = 𝑖 → ((𝐹𝑘) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ↔ (𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥)))
9492oveq1d 5868 . . . . . . . . . . 11 (𝑘 = 𝑖 → ((𝐹𝑘) +R 𝑥) = ((𝐹𝑖) +R 𝑥))
9594breq2d 4001 . . . . . . . . . 10 (𝑘 = 𝑖 → ([⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑘) +R 𝑥) ↔ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥)))
9693, 95anbi12d 470 . . . . . . . . 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 𝑥))))
9791, 96imbi12d 233 . . . . . . . 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 𝑥)))))
9897cbvralv 2696 . . . . . . 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 𝑥))))
9998rexbii 2477 . . . . . 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 𝑥))))
10090, 99sylib 121 . . . . 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 𝑥))))
101100ex 114 . . . 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 𝑥)))))
102101ralrimiva 2543 . . 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 𝑥)))))
103 oveq1 5860 . . . . . . . . . 10 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → (𝑦 +R 𝑥) = ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥))
104103breq2d 4001 . . . . . . . . 9 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → ((𝐹𝑖) <R (𝑦 +R 𝑥) ↔ (𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥)))
105 breq1 3992 . . . . . . . . 9 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → (𝑦 <R ((𝐹𝑖) +R 𝑥) ↔ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥)))
106104, 105anbi12d 470 . . . . . . . 8 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → (((𝐹𝑖) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹𝑖) +R 𝑥)) ↔ ((𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥))))
107106imbi2d 229 . . . . . . 7 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → ((𝑗 <N 𝑖 → ((𝐹𝑖) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹𝑖) +R 𝑥))) ↔ (𝑗 <N 𝑖 → ((𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥)))))
108107rexralbidv 2496 . . . . . 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 𝑥)))))
109108imbi2d 229 . . . . 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 𝑥))))))
110109ralbidv 2470 . . . 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 𝑥))))))
111110rspcev 2834 . . 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 𝑥)))))
11210, 102, 111syl2anc 409 . 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 𝑥)))))
1138, 112rexlimddv 2592 1 (𝜑 → ∃𝑦R𝑥R (0R <R 𝑥 → ∃𝑗N𝑖N (𝑗 <N 𝑖 → ((𝐹𝑖) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹𝑖) +R 𝑥)))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1348  wcel 2141  {cab 2156  wral 2448  wrex 2449  ∃!wreu 2450  cop 3586   class class class wbr 3989  cmpt 4050  wf 5194  cfv 5198  crio 5808  (class class class)co 5853  1oc1o 6388  [cec 6511  Ncnpi 7234   <N clti 7237   ~Q ceq 7241  *Qcrq 7246   <Q cltq 7247  Pcnp 7253  1Pc1p 7254   +P cpp 7255  <P cltp 7257   ~R cer 7258  Rcnr 7259  0Rc0r 7260  1Rc1r 7261   +R cplr 7263   <R cltr 7265
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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4104  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-iinf 4572
This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-reu 2455  df-rmo 2456  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-int 3832  df-iun 3875  df-br 3990  df-opab 4051  df-mpt 4052  df-tr 4088  df-eprel 4274  df-id 4278  df-po 4281  df-iso 4282  df-iord 4351  df-on 4353  df-suc 4356  df-iom 4575  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-riota 5809  df-ov 5856  df-oprab 5857  df-mpo 5858  df-1st 6119  df-2nd 6120  df-recs 6284  df-irdg 6349  df-1o 6395  df-2o 6396  df-oadd 6399  df-omul 6400  df-er 6513  df-ec 6515  df-qs 6519  df-ni 7266  df-pli 7267  df-mi 7268  df-lti 7269  df-plpq 7306  df-mpq 7307  df-enq 7309  df-nqqs 7310  df-plqqs 7311  df-mqqs 7312  df-1nqqs 7313  df-rq 7314  df-ltnqqs 7315  df-enq0 7386  df-nq0 7387  df-0nq0 7388  df-plq0 7389  df-mq0 7390  df-inp 7428  df-i1p 7429  df-iplp 7430  df-iltp 7432  df-enr 7688  df-nr 7689  df-plr 7690  df-ltr 7692  df-0r 7693  df-1r 7694
This theorem is referenced by:  caucvgsrlemoffres  7762
  Copyright terms: Public domain W3C validator