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

Theorem caucvgsrlemgt1 7287
Description: Lemma for caucvgsr 7294. 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 2085 . . . 4 (𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R )) = (𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))
51, 2, 3, 4caucvgsrlemf 7284 . . 3 (𝜑 → (𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R )):NP)
61, 2, 3, 4caucvgsrlemcau 7285 . . 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 7286 . . 3 (𝜑 → ∀𝑚N 1P<P ((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑚))
85, 6, 7caucvgprpr 7218 . 2 (𝜑 → ∃𝑎P𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))
9 prsrcl 7276 . . . 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 oveq2 5623 . . . . . . . . . . . 12 (𝑏 = (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) → (𝑎 +P 𝑏) = (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)))
1211breq2d 3834 . . . . . . . . . . 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 5623 . . . . . . . . . . . 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 3834 . . . . . . . . . . 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 457 . . . . . . . . . 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 228 . . . . . . . . 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 2400 . . . . . . . 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 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 𝑏))))
1918adantr 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 𝑏))))
20 srpospr 7275 . . . . . . . . . 10 ((𝑥R ∧ 0R <R 𝑥) → ∃!𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)
21 riotacl 5585 . . . . . . . . . 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 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)
2417, 19, 23rspcdva 2720 . . . . . . 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 1464 . . . . . . . . . . 11 𝑗𝜑
26 nfv 1464 . . . . . . . . . . . 12 𝑗 𝑎P
27 nfcv 2225 . . . . . . . . . . . . 13 𝑗P
28 nfre1 2415 . . . . . . . . . . . . 13 𝑗𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
2927, 28nfralya 2412 . . . . . . . . . . . 12 𝑗𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
3026, 29nfan 1500 . . . . . . . . . . 11 𝑗(𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))
3125, 30nfan 1500 . . . . . . . . . 10 𝑗(𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))))
32 nfv 1464 . . . . . . . . . 10 𝑗 𝑥R
3331, 32nfan 1500 . . . . . . . . 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 1464 . . . . . . . . 9 𝑗0R <R 𝑥
3533, 34nfan 1500 . . . . . . . 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 1464 . . . . . . . . . . . 12 𝑘𝜑
37 nfv 1464 . . . . . . . . . . . . 13 𝑘 𝑎P
38 nfcv 2225 . . . . . . . . . . . . . 14 𝑘P
39 nfcv 2225 . . . . . . . . . . . . . . 15 𝑘N
40 nfra1 2405 . . . . . . . . . . . . . . 15 𝑘𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
4139, 40nfrexya 2413 . . . . . . . . . . . . . 14 𝑘𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
4238, 41nfralya 2412 . . . . . . . . . . . . 13 𝑘𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))
4337, 42nfan 1500 . . . . . . . . . . . 12 𝑘(𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏))))
4436, 43nfan 1500 . . . . . . . . . . 11 𝑘(𝜑 ∧ (𝑎P ∧ ∀𝑏P𝑗N𝑘N (𝑗 <N 𝑘 → (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘)<P (𝑎 +P 𝑏) ∧ 𝑎<P (((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 𝑏)))))
45 nfv 1464 . . . . . . . . . . 11 𝑘 𝑥R
4644, 45nfan 1500 . . . . . . . . . 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 1464 . . . . . . . . . 10 𝑘0R <R 𝑥
4846, 47nfan 1500 . . . . . . . . 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 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)
50 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)
5149, 50ffvelrnd 5400 . . . . . . . . . . . . 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 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)
5352adantr 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)
54 addclpr 7043 . . . . . . . . . . . . . . 15 ((𝑎P ∧ (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) ∈ P) → (𝑎 +P (𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥)) ∈ P)
5553, 23, 54syl2anc 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)
5655adantr 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)
57 prsrlt 7279 . . . . . . . . . . . . 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 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 ))
591, 2, 3, 4caucvgsrlemfv 7283 . . . . . . . . . . . . . . . 16 ((𝜑𝑘N) → [⟨(((𝑧N ↦ (𝑤P (𝐹𝑧) = [⟨(𝑤 +P 1P), 1P⟩] ~R ))‘𝑘) +P 1P), 1P⟩] ~R = (𝐹𝑘))
6059adantlr 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 = (𝐹𝑘))
6160adantlr 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 = (𝐹𝑘))
6261adantlr 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 = (𝐹𝑘))
63 prsradd 7278 . . . . . . . . . . . . . . . 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 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 ))
65 prsrriota 7280 . . . . . . . . . . . . . . . . 17 ((𝑥R ∧ 0R <R 𝑥) → [⟨((𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) +P 1P), 1P⟩] ~R = 𝑥)
6665oveq2d 5631 . . . . . . . . . . . . . . . 16 ((𝑥R ∧ 0R <R 𝑥) → ([⟨(𝑎 +P 1P), 1P⟩] ~R +R [⟨((𝑐P [⟨(𝑐 +P 1P), 1P⟩] ~R = 𝑥) +P 1P), 1P⟩] ~R ) = ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥))
6766adantll 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 𝑥))
6864, 67eqtrd 2117 . . . . . . . . . . . . . 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 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 𝑥))
7062, 69breq12d 3835 . . . . . . . . . . . 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 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 𝑥)))
7253adantr 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)
7323adantr 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)
74 addclpr 7043 . . . . . . . . . . . . . 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 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)
76 prsrlt 7279 . . . . . . . . . . . . 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 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 ))
78 prsradd 7278 . . . . . . . . . . . . . 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 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 ))
8079breq2d 3834 . . . . . . . . . . . 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 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 = 𝑥)
8281adantr 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 = 𝑥)
8362, 82oveq12d 5633 . . . . . . . . . . . . 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 3834 . . . . . . . . . . . 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 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 𝑥)))
8671, 85anbi12d 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 𝑥))))
8786imbi2d 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 𝑥)))))
8848, 87ralbida 2370 . . . . . . . 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 2375 . . . . . . 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 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 𝑥))))
91 breq2 3826 . . . . . . . . 9 (𝑘 = 𝑖 → (𝑗 <N 𝑘𝑗 <N 𝑖))
92 fveq2 5270 . . . . . . . . . . 11 (𝑘 = 𝑖 → (𝐹𝑘) = (𝐹𝑖))
9392breq1d 3832 . . . . . . . . . 10 (𝑘 = 𝑖 → ((𝐹𝑘) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ↔ (𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥)))
9492oveq1d 5630 . . . . . . . . . . 11 (𝑘 = 𝑖 → ((𝐹𝑘) +R 𝑥) = ((𝐹𝑖) +R 𝑥))
9594breq2d 3834 . . . . . . . . . 10 (𝑘 = 𝑖 → ([⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑘) +R 𝑥) ↔ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥)))
9693, 95anbi12d 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 𝑥))))
9791, 96imbi12d 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 𝑥)))))
9897cbvralv 2586 . . . . . . 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 2381 . . . . . 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 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 𝑥))))
101100ex 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 𝑥)))))
102101ralrimiva 2442 . . 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 5622 . . . . . . . . . 10 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → (𝑦 +R 𝑥) = ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥))
104103breq2d 3834 . . . . . . . . 9 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → ((𝐹𝑖) <R (𝑦 +R 𝑥) ↔ (𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥)))
105 breq1 3825 . . . . . . . . 9 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → (𝑦 <R ((𝐹𝑖) +R 𝑥) ↔ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥)))
106104, 105anbi12d 457 . . . . . . . 8 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → (((𝐹𝑖) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹𝑖) +R 𝑥)) ↔ ((𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥))))
107106imbi2d 228 . . . . . . 7 (𝑦 = [⟨(𝑎 +P 1P), 1P⟩] ~R → ((𝑗 <N 𝑖 → ((𝐹𝑖) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹𝑖) +R 𝑥))) ↔ (𝑗 <N 𝑖 → ((𝐹𝑖) <R ([⟨(𝑎 +P 1P), 1P⟩] ~R +R 𝑥) ∧ [⟨(𝑎 +P 1P), 1P⟩] ~R <R ((𝐹𝑖) +R 𝑥)))))
108107rexralbidv 2400 . . . . . 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 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 𝑥))))))
110109ralbidv 2376 . . . 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 2715 . . 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 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 𝑥)))))
1138, 112rexlimddv 2489 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 1287  wcel 1436  {cab 2071  wral 2355  wrex 2356  ∃!wreu 2357  cop 3434   class class class wbr 3822  cmpt 3876  wf 4979  cfv 4983  crio 5570  (class class class)co 5615  1𝑜c1o 6130  [cec 6244  Ncnpi 6778   <N clti 6781   ~Q ceq 6785  *Qcrq 6790   <Q cltq 6791  Pcnp 6797  1Pc1p 6798   +P cpp 6799  <P cltp 6801   ~R cer 6802  Rcnr 6803  0Rc0r 6804  1Rc1r 6805   +R cplr 6807   <R cltr 6809
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-coll 3931  ax-sep 3934  ax-nul 3942  ax-pow 3986  ax-pr 4012  ax-un 4236  ax-setind 4328  ax-iinf 4378
This theorem depends on definitions:  df-bi 115  df-dc 779  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-ral 2360  df-rex 2361  df-reu 2362  df-rmo 2363  df-rab 2364  df-v 2617  df-sbc 2830  df-csb 2923  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-nul 3276  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-int 3674  df-iun 3717  df-br 3823  df-opab 3877  df-mpt 3878  df-tr 3914  df-eprel 4092  df-id 4096  df-po 4099  df-iso 4100  df-iord 4169  df-on 4171  df-suc 4174  df-iom 4381  df-xp 4419  df-rel 4420  df-cnv 4421  df-co 4422  df-dm 4423  df-rn 4424  df-res 4425  df-ima 4426  df-iota 4948  df-fun 4985  df-fn 4986  df-f 4987  df-f1 4988  df-fo 4989  df-f1o 4990  df-fv 4991  df-riota 5571  df-ov 5618  df-oprab 5619  df-mpt2 5620  df-1st 5870  df-2nd 5871  df-recs 6026  df-irdg 6091  df-1o 6137  df-2o 6138  df-oadd 6141  df-omul 6142  df-er 6246  df-ec 6248  df-qs 6252  df-ni 6810  df-pli 6811  df-mi 6812  df-lti 6813  df-plpq 6850  df-mpq 6851  df-enq 6853  df-nqqs 6854  df-plqqs 6855  df-mqqs 6856  df-1nqqs 6857  df-rq 6858  df-ltnqqs 6859  df-enq0 6930  df-nq0 6931  df-0nq0 6932  df-plq0 6933  df-mq0 6934  df-inp 6972  df-i1p 6973  df-iplp 6974  df-iltp 6976  df-enr 7219  df-nr 7220  df-plr 7221  df-ltr 7223  df-0r 7224  df-1r 7225
This theorem is referenced by:  caucvgsrlemoffres  7292
  Copyright terms: Public domain W3C validator