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

Theorem caucvgsrlemgt1 7571
Description: Lemma for caucvgsr 7578. 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 2117 . . . 4 (𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R )) = (𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))
51, 2, 3, 4caucvgsrlemf 7568 . . 3 (𝜑 → (𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R )):NP)
61, 2, 3, 4caucvgsrlemcau 7569 . . 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 7570 . . 3 (𝜑 → ∀𝑚N 1P<P ((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑚))
85, 6, 7caucvgprpr 7488 . 2 (𝜑 → ∃𝑎P𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))
9 prsrcl 7560 . . . 4 (𝑎P → [⟨(𝑎 +P 1P), 1P⟩] ~RR)
109ad2antrl 481 . . 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 5750 . . . . . . . . . . . 12 (𝑏 = (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) → (𝑎 +P 𝑏) = (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)))
1211breq2d 3911 . . . . . . . . . . 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 5750 . . . . . . . . . . . 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 3911 . . . . . . . . . . 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 464 . . . . . . . . . 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 2438 . . . . . . . 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 510 . . . . . . . . 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 7559 . . . . . . . . . 10 ((𝑥R ∧ 0R <R 𝑥) → ∃!𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)
21 riotacl 5712 . . . . . . . . . 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 467 . . . . . . . 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 2768 . . . . . . 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 1493 . . . . . . . . . . 11 𝑗𝜑
26 nfv 1493 . . . . . . . . . . . 12 𝑗 𝑎P
27 nfcv 2258 . . . . . . . . . . . . 13 𝑗P
28 nfre1 2453 . . . . . . . . . . . . 13 𝑗𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
2927, 28nfralya 2450 . . . . . . . . . . . 12 𝑗𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
3026, 29nfan 1529 . . . . . . . . . . 11 𝑗(𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))
3125, 30nfan 1529 . . . . . . . . . 10 𝑗(𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))))
32 nfv 1493 . . . . . . . . . 10 𝑗 𝑥R
3331, 32nfan 1529 . . . . . . . . 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 1493 . . . . . . . . 9 𝑗0R <R 𝑥
3533, 34nfan 1529 . . . . . . . 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 1493 . . . . . . . . . . . 12 𝑘𝜑
37 nfv 1493 . . . . . . . . . . . . 13 𝑘 𝑎P
38 nfcv 2258 . . . . . . . . . . . . . 14 𝑘P
39 nfcv 2258 . . . . . . . . . . . . . . 15 𝑘N
40 nfra1 2443 . . . . . . . . . . . . . . 15 𝑘𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
4139, 40nfrexya 2451 . . . . . . . . . . . . . 14 𝑘𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
4238, 41nfralya 2450 . . . . . . . . . . . . 13 𝑘𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
4337, 42nfan 1529 . . . . . . . . . . . 12 𝑘(𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))
4436, 43nfan 1529 . . . . . . . . . . 11 𝑘(𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))))
45 nfv 1493 . . . . . . . . . . 11 𝑘 𝑥R
4644, 45nfan 1529 . . . . . . . . . 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 1493 . . . . . . . . . 10 𝑘0R <R 𝑥
4846, 47nfan 1529 . . . . . . . . 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 485 . . . . . . . . . . . . . 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 5524 . . . . . . . . . . . . 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 509 . . . . . . . . . . . . . . . 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 7313 . . . . . . . . . . . . . . 15 ((𝑎P ∧ (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) ∈ P) → (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ∈ P)
5553, 23, 54syl2anc 408 . . . . . . . . . . . . . 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 7563 . . . . . . . . . . . . 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 408 . . . . . . . . . . . 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 7567 . . . . . . . . . . . . . . . 16 ((𝜑𝑘N) → [⟨(((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 1P), 1P⟩] ~R = (𝐹𝑘))
6059adantlr 468 . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . 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 7562 . . . . . . . . . . . . . . . 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 408 . . . . . . . . . . . . . . 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 7564 . . . . . . . . . . . . . . . . 17 ((𝑥R ∧ 0R <R 𝑥) → [⟨((𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) +P 1P), 1P⟩] ~R = 𝑥)
6665oveq2d 5758 . . . . . . . . . . . . . . . 16 ((𝑥R ∧ 0R <R 𝑥) → ([⟨(𝑎 +P 1P), 1P⟩] ~R +R [⟨((𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) +P 1P), 1P⟩] ~R ) = ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥))
6766adantll 467 . . . . . . . . . . . . . . 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 2150 . . . . . . . . . . . . . 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 3912 . . . . . . . . . . . 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 7313 . . . . . . . . . . . . . 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 408 . . . . . . . . . . . . 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 7563 . . . . . . . . . . . . 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 408 . . . . . . . . . . . 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 7562 . . . . . . . . . . . . . 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 408 . . . . . . . . . . . . 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 3911 . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . 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 5760 . . . . . . . . . . . . 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 3911 . . . . . . . . . . . 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 464 . . . . . . . . . 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 2408 . . . . . . . 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 2413 . . . . . . 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 3903 . . . . . . . . 9 (𝑘 = 𝑖 → (𝑗 <N 𝑘𝑗 <N 𝑖))
92 fveq2 5389 . . . . . . . . . . 11 (𝑘 = 𝑖 → (𝐹𝑘) = (𝐹𝑖))
9392breq1d 3909 . . . . . . . . . 10 (𝑘 = 𝑖 → ((𝐹𝑘) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ↔ (𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥)))
9492oveq1d 5757 . . . . . . . . . . 11 (𝑘 = 𝑖 → ((𝐹𝑘) +R 𝑥) = ((𝐹𝑖) +R 𝑥))
9594breq2d 3911 . . . . . . . . . 10 (𝑘 = 𝑖 → ([⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑘) +R 𝑥) ↔ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥)))
9693, 95anbi12d 464 . . . . . . . . 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 2631 . . . . . . 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 2419 . . . . . 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 2482 . . 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 5749 . . . . . . . . . 10 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → (𝑦 +R 𝑥) = ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥))
104103breq2d 3911 . . . . . . . . 9 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → ((𝐹𝑖) <R (𝑦 +R 𝑥) ↔ (𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥)))
105 breq1 3902 . . . . . . . . 9 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → (𝑦 <R ((𝐹𝑖) +R 𝑥) ↔ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥)))
106104, 105anbi12d 464 . . . . . . . 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 2438 . . . . . 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 2414 . . . 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 2763 . . 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 408 . 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 2531 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 1316  wcel 1465  {cab 2103  wral 2393  wrex 2394  ∃!wreu 2395  cop 3500   class class class wbr 3899  cmpt 3959  wf 5089  cfv 5093  crio 5697  (class class class)co 5742  1oc1o 6274  [cec 6395  Ncnpi 7048   <N clti 7051   ~Q ceq 7055  *Qcrq 7060   <Q cltq 7061  Pcnp 7067  1Pc1p 7068   +P cpp 7069  <P cltp 7071   ~R cer 7072  Rcnr 7073  0Rc0r 7074  1Rc1r 7075   +R cplr 7077   <R cltr 7079
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 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-13 1476  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-coll 4013  ax-sep 4016  ax-nul 4024  ax-pow 4068  ax-pr 4101  ax-un 4325  ax-setind 4422  ax-iinf 4472
This theorem depends on definitions:  df-bi 116  df-dc 805  df-3or 948  df-3an 949  df-tru 1319  df-fal 1322  df-nf 1422  df-sb 1721  df-eu 1980  df-mo 1981  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ne 2286  df-ral 2398  df-rex 2399  df-reu 2400  df-rmo 2401  df-rab 2402  df-v 2662  df-sbc 2883  df-csb 2976  df-dif 3043  df-un 3045  df-in 3047  df-ss 3054  df-nul 3334  df-pw 3482  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-int 3742  df-iun 3785  df-br 3900  df-opab 3960  df-mpt 3961  df-tr 3997  df-eprel 4181  df-id 4185  df-po 4188  df-iso 4189  df-iord 4258  df-on 4260  df-suc 4263  df-iom 4475  df-xp 4515  df-rel 4516  df-cnv 4517  df-co 4518  df-dm 4519  df-rn 4520  df-res 4521  df-ima 4522  df-iota 5058  df-fun 5095  df-fn 5096  df-f 5097  df-f1 5098  df-fo 5099  df-f1o 5100  df-fv 5101  df-riota 5698  df-ov 5745  df-oprab 5746  df-mpo 5747  df-1st 6006  df-2nd 6007  df-recs 6170  df-irdg 6235  df-1o 6281  df-2o 6282  df-oadd 6285  df-omul 6286  df-er 6397  df-ec 6399  df-qs 6403  df-ni 7080  df-pli 7081  df-mi 7082  df-lti 7083  df-plpq 7120  df-mpq 7121  df-enq 7123  df-nqqs 7124  df-plqqs 7125  df-mqqs 7126  df-1nqqs 7127  df-rq 7128  df-ltnqqs 7129  df-enq0 7200  df-nq0 7201  df-0nq0 7202  df-plq0 7203  df-mq0 7204  df-inp 7242  df-i1p 7243  df-iplp 7244  df-iltp 7246  df-enr 7502  df-nr 7503  df-plr 7504  df-ltr 7506  df-0r 7507  df-1r 7508
This theorem is referenced by:  caucvgsrlemoffres  7576
  Copyright terms: Public domain W3C validator