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

Theorem caucvgsrlembound 6936
 Description: Lemma for caucvgsr 6944. Defining the boundedness condition in terms of positive reals. (Contributed by Jim Kingdon, 25-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 (𝐹𝑚))
caucvgsrlemf.xfr 𝐺 = (𝑥N ↦ (𝑦P (𝐹𝑥) = [⟨(𝑦 +P 1P), 1P⟩] ~R ))
Assertion
Ref Expression
caucvgsrlembound (𝜑 → ∀𝑚N 1P<P (𝐺𝑚))
Distinct variable groups:   𝑚,𝐹,𝑥,𝑦   𝜑,𝑥   𝑚,𝐺
Allowed substitution hints:   𝜑(𝑦,𝑢,𝑘,𝑚,𝑛,𝑙)   𝐹(𝑢,𝑘,𝑛,𝑙)   𝐺(𝑥,𝑦,𝑢,𝑘,𝑛,𝑙)

Proof of Theorem caucvgsrlembound
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 caucvgsrlemgt1.gt1 . . . . . . 7 (𝜑 → ∀𝑚N 1R <R (𝐹𝑚))
2 fveq2 5206 . . . . . . . . 9 (𝑚 = 𝑤 → (𝐹𝑚) = (𝐹𝑤))
32breq2d 3804 . . . . . . . 8 (𝑚 = 𝑤 → (1R <R (𝐹𝑚) ↔ 1R <R (𝐹𝑤)))
43cbvralv 2550 . . . . . . 7 (∀𝑚N 1R <R (𝐹𝑚) ↔ ∀𝑤N 1R <R (𝐹𝑤))
51, 4sylib 131 . . . . . 6 (𝜑 → ∀𝑤N 1R <R (𝐹𝑤))
65r19.21bi 2424 . . . . 5 ((𝜑𝑤N) → 1R <R (𝐹𝑤))
7 df-1r 6875 . . . . . . 7 1R = [⟨(1P +P 1P), 1P⟩] ~R
87eqcomi 2060 . . . . . 6 [⟨(1P +P 1P), 1P⟩] ~R = 1R
98a1i 9 . . . . 5 ((𝜑𝑤N) → [⟨(1P +P 1P), 1P⟩] ~R = 1R)
10 caucvgsr.f . . . . . 6 (𝜑𝐹:NR)
11 caucvgsr.cau . . . . . 6 (𝜑 → ∀𝑛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 ))))
12 caucvgsrlemf.xfr . . . . . 6 𝐺 = (𝑥N ↦ (𝑦P (𝐹𝑥) = [⟨(𝑦 +P 1P), 1P⟩] ~R ))
1310, 11, 1, 12caucvgsrlemfv 6933 . . . . 5 ((𝜑𝑤N) → [⟨((𝐺𝑤) +P 1P), 1P⟩] ~R = (𝐹𝑤))
146, 9, 133brtr4d 3822 . . . 4 ((𝜑𝑤N) → [⟨(1P +P 1P), 1P⟩] ~R <R [⟨((𝐺𝑤) +P 1P), 1P⟩] ~R )
15 1pr 6710 . . . . 5 1PP
1610, 11, 1, 12caucvgsrlemf 6934 . . . . . 6 (𝜑𝐺:NP)
1716ffvelrnda 5330 . . . . 5 ((𝜑𝑤N) → (𝐺𝑤) ∈ P)
18 prsrlt 6929 . . . . 5 ((1PP ∧ (𝐺𝑤) ∈ P) → (1P<P (𝐺𝑤) ↔ [⟨(1P +P 1P), 1P⟩] ~R <R [⟨((𝐺𝑤) +P 1P), 1P⟩] ~R ))
1915, 17, 18sylancr 399 . . . 4 ((𝜑𝑤N) → (1P<P (𝐺𝑤) ↔ [⟨(1P +P 1P), 1P⟩] ~R <R [⟨((𝐺𝑤) +P 1P), 1P⟩] ~R ))
2014, 19mpbird 160 . . 3 ((𝜑𝑤N) → 1P<P (𝐺𝑤))
2120ralrimiva 2409 . 2 (𝜑 → ∀𝑤N 1P<P (𝐺𝑤))
22 fveq2 5206 . . . 4 (𝑤 = 𝑚 → (𝐺𝑤) = (𝐺𝑚))
2322breq2d 3804 . . 3 (𝑤 = 𝑚 → (1P<P (𝐺𝑤) ↔ 1P<P (𝐺𝑚)))
2423cbvralv 2550 . 2 (∀𝑤N 1P<P (𝐺𝑤) ↔ ∀𝑚N 1P<P (𝐺𝑚))
2521, 24sylib 131 1 (𝜑 → ∀𝑚N 1P<P (𝐺𝑚))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102   = wceq 1259   ∈ wcel 1409  {cab 2042  ∀wral 2323  ⟨cop 3406   class class class wbr 3792   ↦ cmpt 3846  ⟶wf 4926  ‘cfv 4930  ℩crio 5495  (class class class)co 5540  1𝑜c1o 6025  [cec 6135  Ncnpi 6428
 Copyright terms: Public domain W3C validator