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

Theorem caucvgpr 7302
 Description: A Cauchy sequence of positive fractions with a modulus of convergence converges to a positive real. This is basically Corollary 11.2.13 of [HoTT], p. (varies) (one key difference being that this is for positive reals rather than signed reals). Also, the HoTT book theorem has a modulus of convergence (that is, a rate of convergence) specified by (11.2.9) in HoTT whereas this theorem fixes the rate of convergence to say that all terms after the nth term must be within 1 / 𝑛 of the nth term (it should later be able to prove versions of this theorem with a different fixed rate or a modulus of convergence supplied as a hypothesis). We also specify that every term needs to be larger than a fraction 𝐴, to avoid the case where we have positive terms which "converge" to zero (which is not a positive real). This proof (including its lemmas) is similar to the proofs of cauappcvgpr 7282 and caucvgprpr 7332. Reading cauappcvgpr 7282 first (the simplest of the three) might help understanding the other two. (Contributed by Jim Kingdon, 18-Jun-2020.)
Hypotheses
Ref Expression
caucvgpr.f (𝜑𝐹:NQ)
caucvgpr.cau (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )))))
caucvgpr.bnd (𝜑 → ∀𝑗N 𝐴 <Q (𝐹𝑗))
Assertion
Ref Expression
caucvgpr (𝜑 → ∃𝑦P𝑥Q𝑗N𝑘N (𝑗 <N 𝑘 → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (𝑦 +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ∧ 𝑦<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩)))
Distinct variable groups:   𝐴,𝑗   𝑗,𝐹,𝑘,𝑛,𝑙,𝑢,𝑥,𝑦   𝜑,𝑗,𝑘,𝑥
Allowed substitution hints:   𝜑(𝑦,𝑢,𝑛,𝑙)   𝐴(𝑥,𝑦,𝑢,𝑘,𝑛,𝑙)

Proof of Theorem caucvgpr
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 caucvgpr.f . . 3 (𝜑𝐹:NQ)
2 caucvgpr.cau . . 3 (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )))))
3 caucvgpr.bnd . . 3 (𝜑 → ∀𝑗N 𝐴 <Q (𝐹𝑗))
4 opeq1 3628 . . . . . . . . . . 11 (𝑧 = 𝑗 → ⟨𝑧, 1o⟩ = ⟨𝑗, 1o⟩)
54eceq1d 6342 . . . . . . . . . 10 (𝑧 = 𝑗 → [⟨𝑧, 1o⟩] ~Q = [⟨𝑗, 1o⟩] ~Q )
65fveq2d 5322 . . . . . . . . 9 (𝑧 = 𝑗 → (*Q‘[⟨𝑧, 1o⟩] ~Q ) = (*Q‘[⟨𝑗, 1o⟩] ~Q ))
76oveq2d 5682 . . . . . . . 8 (𝑧 = 𝑗 → (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) = (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )))
8 fveq2 5318 . . . . . . . 8 (𝑧 = 𝑗 → (𝐹𝑧) = (𝐹𝑗))
97, 8breq12d 3864 . . . . . . 7 (𝑧 = 𝑗 → ((𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧) ↔ (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q (𝐹𝑗)))
109cbvrexv 2592 . . . . . 6 (∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧) ↔ ∃𝑗N (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q (𝐹𝑗))
1110a1i 9 . . . . 5 (𝑙Q → (∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧) ↔ ∃𝑗N (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q (𝐹𝑗)))
1211rabbiia 2605 . . . 4 {𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)} = {𝑙Q ∣ ∃𝑗N (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q (𝐹𝑗)}
138, 6oveq12d 5684 . . . . . . . 8 (𝑧 = 𝑗 → ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) = ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )))
1413breq1d 3861 . . . . . . 7 (𝑧 = 𝑗 → (((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢 ↔ ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q 𝑢))
1514cbvrexv 2592 . . . . . 6 (∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢 ↔ ∃𝑗N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q 𝑢)
1615a1i 9 . . . . 5 (𝑢Q → (∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢 ↔ ∃𝑗N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q 𝑢))
1716rabbiia 2605 . . . 4 {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢} = {𝑢Q ∣ ∃𝑗N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q 𝑢}
1812, 17opeq12i 3633 . . 3 ⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩ = ⟨{𝑙Q ∣ ∃𝑗N (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q (𝐹𝑗)}, {𝑢Q ∣ ∃𝑗N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q 𝑢}⟩
191, 2, 3, 18caucvgprlemcl 7296 . 2 (𝜑 → ⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩ ∈ P)
201, 2, 3, 18caucvgprlemlim 7301 . 2 (𝜑 → ∀𝑥Q𝑗N𝑘N (𝑗 <N 𝑘 → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩ +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ∧ ⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩)))
21 oveq1 5673 . . . . . . . 8 (𝑦 = ⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩ → (𝑦 +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) = (⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩ +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩))
2221breq2d 3863 . . . . . . 7 (𝑦 = ⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩ → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (𝑦 +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ↔ ⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩ +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩)))
23 breq1 3854 . . . . . . 7 (𝑦 = ⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩ → (𝑦<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩ ↔ ⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩))
2422, 23anbi12d 458 . . . . . 6 (𝑦 = ⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩ → ((⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (𝑦 +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ∧ 𝑦<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩) ↔ (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩ +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ∧ ⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩)))
2524imbi2d 229 . . . . 5 (𝑦 = ⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩ → ((𝑗 <N 𝑘 → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (𝑦 +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ∧ 𝑦<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩)) ↔ (𝑗 <N 𝑘 → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩ +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ∧ ⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩))))
2625rexralbidv 2405 . . . 4 (𝑦 = ⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩ → (∃𝑗N𝑘N (𝑗 <N 𝑘 → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (𝑦 +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ∧ 𝑦<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩)) ↔ ∃𝑗N𝑘N (𝑗 <N 𝑘 → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩ +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ∧ ⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩))))
2726ralbidv 2381 . . 3 (𝑦 = ⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩ → (∀𝑥Q𝑗N𝑘N (𝑗 <N 𝑘 → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (𝑦 +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ∧ 𝑦<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩)) ↔ ∀𝑥Q𝑗N𝑘N (𝑗 <N 𝑘 → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩ +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ∧ ⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩))))
2827rspcev 2723 . 2 ((⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩ ∈ P ∧ ∀𝑥Q𝑗N𝑘N (𝑗 <N 𝑘 → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩ +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ∧ ⟨{𝑙Q ∣ ∃𝑧N (𝑙 +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧N ((𝐹𝑧) +Q (*Q‘[⟨𝑧, 1o⟩] ~Q )) <Q 𝑢}⟩<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩))) → ∃𝑦P𝑥Q𝑗N𝑘N (𝑗 <N 𝑘 → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (𝑦 +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ∧ 𝑦<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩)))
2919, 20, 28syl2anc 404 1 (𝜑 → ∃𝑦P𝑥Q𝑗N𝑘N (𝑗 <N 𝑘 → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {𝑢 ∣ (𝐹𝑘) <Q 𝑢}⟩<P (𝑦 +P ⟨{𝑙𝑙 <Q 𝑥}, {𝑢𝑥 <Q 𝑢}⟩) ∧ 𝑦<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹𝑘) +Q 𝑥) <Q 𝑢}⟩)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1290   ∈ wcel 1439  {cab 2075  ∀wral 2360  ∃wrex 2361  {crab 2364  ⟨cop 3453   class class class wbr 3851  ⟶wf 5024  ‘cfv 5028  (class class class)co 5666  1oc1o 6188  [cec 6304  Ncnpi 6892
 Copyright terms: Public domain W3C validator