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

Theorem cauappcvgpr 7561
 Description: A Cauchy approximation has a limit. A Cauchy approximation, here 𝐹, is similar to a Cauchy sequence but is indexed by the desired tolerance (that is, how close together terms needs to be) rather than by natural numbers. This is basically Theorem 11.2.12 of [HoTT], p. (varies) with a few differences such as that we are proving the existence of a limit without anything about how fast it converges (that is, mere existence instead of existence, in HoTT terms), and that the codomain of 𝐹 is Q rather than P. 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 caucvgpr 7581 and caucvgprpr 7611 but is somewhat simpler, so reading this one first may help understanding the other two. (Contributed by Jim Kingdon, 19-Jun-2020.)
Hypotheses
Ref Expression
cauappcvgpr.f (𝜑𝐹:QQ)
cauappcvgpr.app (𝜑 → ∀𝑝Q𝑞Q ((𝐹𝑝) <Q ((𝐹𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹𝑞) <Q ((𝐹𝑝) +Q (𝑝 +Q 𝑞))))
cauappcvgpr.bnd (𝜑 → ∀𝑝Q 𝐴 <Q (𝐹𝑝))
Assertion
Ref Expression
cauappcvgpr (𝜑 → ∃𝑦P𝑞Q𝑟Q (⟨{𝑙𝑙 <Q (𝐹𝑞)}, {𝑢 ∣ (𝐹𝑞) <Q 𝑢}⟩<P (𝑦 +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q 𝑢}⟩) ∧ 𝑦<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {𝑢 ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q 𝑢}⟩))
Distinct variable groups:   𝐴,𝑝   𝐹,𝑞,𝑦,𝑟,𝑢   𝐹,𝑝,𝑙,𝑞   𝑦,𝑙,𝑟   𝑢,𝑞,𝑦,𝑟   𝑢,𝑝,𝑟,𝑞,𝑙   𝜑,𝑞,𝑝
Allowed substitution hints:   𝜑(𝑦,𝑢,𝑟,𝑙)   𝐴(𝑦,𝑢,𝑟,𝑞,𝑙)

Proof of Theorem cauappcvgpr
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 cauappcvgpr.f . . 3 (𝜑𝐹:QQ)
2 cauappcvgpr.app . . 3 (𝜑 → ∀𝑝Q𝑞Q ((𝐹𝑝) <Q ((𝐹𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹𝑞) <Q ((𝐹𝑝) +Q (𝑝 +Q 𝑞))))
3 cauappcvgpr.bnd . . 3 (𝜑 → ∀𝑝Q 𝐴 <Q (𝐹𝑝))
4 oveq2 5822 . . . . . . . 8 (𝑧 = 𝑞 → (𝑙 +Q 𝑧) = (𝑙 +Q 𝑞))
5 fveq2 5461 . . . . . . . 8 (𝑧 = 𝑞 → (𝐹𝑧) = (𝐹𝑞))
64, 5breq12d 3974 . . . . . . 7 (𝑧 = 𝑞 → ((𝑙 +Q 𝑧) <Q (𝐹𝑧) ↔ (𝑙 +Q 𝑞) <Q (𝐹𝑞)))
76cbvrexv 2678 . . . . . 6 (∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧) ↔ ∃𝑞Q (𝑙 +Q 𝑞) <Q (𝐹𝑞))
87a1i 9 . . . . 5 (𝑙Q → (∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧) ↔ ∃𝑞Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)))
98rabbiia 2694 . . . 4 {𝑙Q ∣ ∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧)} = {𝑙Q ∣ ∃𝑞Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)}
10 id 19 . . . . . . . . 9 (𝑧 = 𝑞𝑧 = 𝑞)
115, 10oveq12d 5832 . . . . . . . 8 (𝑧 = 𝑞 → ((𝐹𝑧) +Q 𝑧) = ((𝐹𝑞) +Q 𝑞))
1211breq1d 3971 . . . . . . 7 (𝑧 = 𝑞 → (((𝐹𝑧) +Q 𝑧) <Q 𝑢 ↔ ((𝐹𝑞) +Q 𝑞) <Q 𝑢))
1312cbvrexv 2678 . . . . . 6 (∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢 ↔ ∃𝑞Q ((𝐹𝑞) +Q 𝑞) <Q 𝑢)
1413a1i 9 . . . . 5 (𝑢Q → (∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢 ↔ ∃𝑞Q ((𝐹𝑞) +Q 𝑞) <Q 𝑢))
1514rabbiia 2694 . . . 4 {𝑢Q ∣ ∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢} = {𝑢Q ∣ ∃𝑞Q ((𝐹𝑞) +Q 𝑞) <Q 𝑢}
169, 15opeq12i 3742 . . 3 ⟨{𝑙Q ∣ ∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢}⟩ = ⟨{𝑙Q ∣ ∃𝑞Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)}, {𝑢Q ∣ ∃𝑞Q ((𝐹𝑞) +Q 𝑞) <Q 𝑢}⟩
171, 2, 3, 16cauappcvgprlemcl 7552 . 2 (𝜑 → ⟨{𝑙Q ∣ ∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢}⟩ ∈ P)
181, 2, 3, 16cauappcvgprlemlim 7560 . 2 (𝜑 → ∀𝑞Q𝑟Q (⟨{𝑙𝑙 <Q (𝐹𝑞)}, {𝑢 ∣ (𝐹𝑞) <Q 𝑢}⟩<P (⟨{𝑙Q ∣ ∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢}⟩ +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q 𝑢}⟩) ∧ ⟨{𝑙Q ∣ ∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢}⟩<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {𝑢 ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q 𝑢}⟩))
19 oveq1 5821 . . . . . 6 (𝑦 = ⟨{𝑙Q ∣ ∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢}⟩ → (𝑦 +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q 𝑢}⟩) = (⟨{𝑙Q ∣ ∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢}⟩ +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q 𝑢}⟩))
2019breq2d 3973 . . . . 5 (𝑦 = ⟨{𝑙Q ∣ ∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢}⟩ → (⟨{𝑙𝑙 <Q (𝐹𝑞)}, {𝑢 ∣ (𝐹𝑞) <Q 𝑢}⟩<P (𝑦 +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q 𝑢}⟩) ↔ ⟨{𝑙𝑙 <Q (𝐹𝑞)}, {𝑢 ∣ (𝐹𝑞) <Q 𝑢}⟩<P (⟨{𝑙Q ∣ ∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢}⟩ +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q 𝑢}⟩)))
21 breq1 3964 . . . . 5 (𝑦 = ⟨{𝑙Q ∣ ∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢}⟩ → (𝑦<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {𝑢 ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q 𝑢}⟩ ↔ ⟨{𝑙Q ∣ ∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢}⟩<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {𝑢 ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q 𝑢}⟩))
2220, 21anbi12d 465 . . . 4 (𝑦 = ⟨{𝑙Q ∣ ∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢}⟩ → ((⟨{𝑙𝑙 <Q (𝐹𝑞)}, {𝑢 ∣ (𝐹𝑞) <Q 𝑢}⟩<P (𝑦 +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q 𝑢}⟩) ∧ 𝑦<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {𝑢 ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q 𝑢}⟩) ↔ (⟨{𝑙𝑙 <Q (𝐹𝑞)}, {𝑢 ∣ (𝐹𝑞) <Q 𝑢}⟩<P (⟨{𝑙Q ∣ ∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢}⟩ +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q 𝑢}⟩) ∧ ⟨{𝑙Q ∣ ∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢}⟩<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {𝑢 ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q 𝑢}⟩)))
23222ralbidv 2478 . . 3 (𝑦 = ⟨{𝑙Q ∣ ∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢}⟩ → (∀𝑞Q𝑟Q (⟨{𝑙𝑙 <Q (𝐹𝑞)}, {𝑢 ∣ (𝐹𝑞) <Q 𝑢}⟩<P (𝑦 +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q 𝑢}⟩) ∧ 𝑦<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {𝑢 ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q 𝑢}⟩) ↔ ∀𝑞Q𝑟Q (⟨{𝑙𝑙 <Q (𝐹𝑞)}, {𝑢 ∣ (𝐹𝑞) <Q 𝑢}⟩<P (⟨{𝑙Q ∣ ∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢}⟩ +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q 𝑢}⟩) ∧ ⟨{𝑙Q ∣ ∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢}⟩<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {𝑢 ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q 𝑢}⟩)))
2423rspcev 2813 . 2 ((⟨{𝑙Q ∣ ∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢}⟩ ∈ P ∧ ∀𝑞Q𝑟Q (⟨{𝑙𝑙 <Q (𝐹𝑞)}, {𝑢 ∣ (𝐹𝑞) <Q 𝑢}⟩<P (⟨{𝑙Q ∣ ∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢}⟩ +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q 𝑢}⟩) ∧ ⟨{𝑙Q ∣ ∃𝑧Q (𝑙 +Q 𝑧) <Q (𝐹𝑧)}, {𝑢Q ∣ ∃𝑧Q ((𝐹𝑧) +Q 𝑧) <Q 𝑢}⟩<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {𝑢 ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q 𝑢}⟩)) → ∃𝑦P𝑞Q𝑟Q (⟨{𝑙𝑙 <Q (𝐹𝑞)}, {𝑢 ∣ (𝐹𝑞) <Q 𝑢}⟩<P (𝑦 +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q 𝑢}⟩) ∧ 𝑦<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {𝑢 ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q 𝑢}⟩))
2517, 18, 24syl2anc 409 1 (𝜑 → ∃𝑦P𝑞Q𝑟Q (⟨{𝑙𝑙 <Q (𝐹𝑞)}, {𝑢 ∣ (𝐹𝑞) <Q 𝑢}⟩<P (𝑦 +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q 𝑢}⟩) ∧ 𝑦<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {𝑢 ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q 𝑢}⟩))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1332   ∈ wcel 2125  {cab 2140  ∀wral 2432  ∃wrex 2433  {crab 2436  ⟨cop 3559   class class class wbr 3961  ⟶wf 5159  ‘cfv 5163  (class class class)co 5814  Qcnq 7179   +Q cplq 7181
 Copyright terms: Public domain W3C validator