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

Theorem cauappcvgpr 6634
 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 A, to avoid the case where we have positive fractions which converge to zero (which is not a positive real). (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 A <Q (𝐹𝑝))
Assertion
Ref Expression
cauappcvgpr (φy P 𝑞 Q 𝑟 Q (⟨{𝑙𝑙 <Q (𝐹𝑞)}, {u ∣ (𝐹𝑞) <Q u}⟩<P (y +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {u ∣ (𝑞 +Q 𝑟) <Q u}⟩) y<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {u ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q u}⟩))
Distinct variable groups:   A,𝑝   𝐹,𝑞,y,𝑟,u   𝐹,𝑝,𝑙,𝑞   y,𝑙,𝑟   u,𝑞,y,𝑟   u,𝑝,𝑟,𝑞,𝑙   φ,𝑞,𝑝
Allowed substitution hints:   φ(y,u,𝑟,𝑙)   A(y,u,𝑟,𝑞,𝑙)

Proof of Theorem cauappcvgpr
Dummy variable z 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 A <Q (𝐹𝑝))
4 oveq2 5463 . . . . . . . 8 (z = 𝑞 → (𝑙 +Q z) = (𝑙 +Q 𝑞))
5 fveq2 5121 . . . . . . . 8 (z = 𝑞 → (𝐹z) = (𝐹𝑞))
64, 5breq12d 3768 . . . . . . 7 (z = 𝑞 → ((𝑙 +Q z) <Q (𝐹z) ↔ (𝑙 +Q 𝑞) <Q (𝐹𝑞)))
76cbvrexv 2528 . . . . . 6 (z Q (𝑙 +Q z) <Q (𝐹z) ↔ 𝑞 Q (𝑙 +Q 𝑞) <Q (𝐹𝑞))
87a1i 9 . . . . 5 (𝑙 Q → (z Q (𝑙 +Q z) <Q (𝐹z) ↔ 𝑞 Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)))
98rabbiia 2541 . . . 4 {𝑙 Qz Q (𝑙 +Q z) <Q (𝐹z)} = {𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)}
10 id 19 . . . . . . . . 9 (z = 𝑞z = 𝑞)
115, 10oveq12d 5473 . . . . . . . 8 (z = 𝑞 → ((𝐹z) +Q z) = ((𝐹𝑞) +Q 𝑞))
1211breq1d 3765 . . . . . . 7 (z = 𝑞 → (((𝐹z) +Q z) <Q u ↔ ((𝐹𝑞) +Q 𝑞) <Q u))
1312cbvrexv 2528 . . . . . 6 (z Q ((𝐹z) +Q z) <Q u𝑞 Q ((𝐹𝑞) +Q 𝑞) <Q u)
1413a1i 9 . . . . 5 (u Q → (z Q ((𝐹z) +Q z) <Q u𝑞 Q ((𝐹𝑞) +Q 𝑞) <Q u))
1514rabbiia 2541 . . . 4 {u Qz Q ((𝐹z) +Q z) <Q u} = {u Q𝑞 Q ((𝐹𝑞) +Q 𝑞) <Q u}
169, 15opeq12i 3545 . . 3 ⟨{𝑙 Qz Q (𝑙 +Q z) <Q (𝐹z)}, {u Qz Q ((𝐹z) +Q z) <Q u}⟩ = ⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)}, {u Q𝑞 Q ((𝐹𝑞) +Q 𝑞) <Q u}⟩
171, 2, 3, 16cauappcvgprlemcl 6625 . 2 (φ → ⟨{𝑙 Qz Q (𝑙 +Q z) <Q (𝐹z)}, {u Qz Q ((𝐹z) +Q z) <Q u}⟩ P)
181, 2, 3, 16cauappcvgprlemlim 6633 . 2 (φ𝑞 Q 𝑟 Q (⟨{𝑙𝑙 <Q (𝐹𝑞)}, {u ∣ (𝐹𝑞) <Q u}⟩<P (⟨{𝑙 Qz Q (𝑙 +Q z) <Q (𝐹z)}, {u Qz Q ((𝐹z) +Q z) <Q u}⟩ +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {u ∣ (𝑞 +Q 𝑟) <Q u}⟩) ⟨{𝑙 Qz Q (𝑙 +Q z) <Q (𝐹z)}, {u Qz Q ((𝐹z) +Q z) <Q u}⟩<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {u ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q u}⟩))
19 oveq1 5462 . . . . . 6 (y = ⟨{𝑙 Qz Q (𝑙 +Q z) <Q (𝐹z)}, {u Qz Q ((𝐹z) +Q z) <Q u}⟩ → (y +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {u ∣ (𝑞 +Q 𝑟) <Q u}⟩) = (⟨{𝑙 Qz Q (𝑙 +Q z) <Q (𝐹z)}, {u Qz Q ((𝐹z) +Q z) <Q u}⟩ +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {u ∣ (𝑞 +Q 𝑟) <Q u}⟩))
2019breq2d 3767 . . . . 5 (y = ⟨{𝑙 Qz Q (𝑙 +Q z) <Q (𝐹z)}, {u Qz Q ((𝐹z) +Q z) <Q u}⟩ → (⟨{𝑙𝑙 <Q (𝐹𝑞)}, {u ∣ (𝐹𝑞) <Q u}⟩<P (y +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {u ∣ (𝑞 +Q 𝑟) <Q u}⟩) ↔ ⟨{𝑙𝑙 <Q (𝐹𝑞)}, {u ∣ (𝐹𝑞) <Q u}⟩<P (⟨{𝑙 Qz Q (𝑙 +Q z) <Q (𝐹z)}, {u Qz Q ((𝐹z) +Q z) <Q u}⟩ +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {u ∣ (𝑞 +Q 𝑟) <Q u}⟩)))
21 breq1 3758 . . . . 5 (y = ⟨{𝑙 Qz Q (𝑙 +Q z) <Q (𝐹z)}, {u Qz Q ((𝐹z) +Q z) <Q u}⟩ → (y<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {u ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q u}⟩ ↔ ⟨{𝑙 Qz Q (𝑙 +Q z) <Q (𝐹z)}, {u Qz Q ((𝐹z) +Q z) <Q u}⟩<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {u ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q u}⟩))
2220, 21anbi12d 442 . . . 4 (y = ⟨{𝑙 Qz Q (𝑙 +Q z) <Q (𝐹z)}, {u Qz Q ((𝐹z) +Q z) <Q u}⟩ → ((⟨{𝑙𝑙 <Q (𝐹𝑞)}, {u ∣ (𝐹𝑞) <Q u}⟩<P (y +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {u ∣ (𝑞 +Q 𝑟) <Q u}⟩) y<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {u ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q u}⟩) ↔ (⟨{𝑙𝑙 <Q (𝐹𝑞)}, {u ∣ (𝐹𝑞) <Q u}⟩<P (⟨{𝑙 Qz Q (𝑙 +Q z) <Q (𝐹z)}, {u Qz Q ((𝐹z) +Q z) <Q u}⟩ +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {u ∣ (𝑞 +Q 𝑟) <Q u}⟩) ⟨{𝑙 Qz Q (𝑙 +Q z) <Q (𝐹z)}, {u Qz Q ((𝐹z) +Q z) <Q u}⟩<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {u ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q u}⟩)))
23222ralbidv 2342 . . 3 (y = ⟨{𝑙 Qz Q (𝑙 +Q z) <Q (𝐹z)}, {u Qz Q ((𝐹z) +Q z) <Q u}⟩ → (𝑞 Q 𝑟 Q (⟨{𝑙𝑙 <Q (𝐹𝑞)}, {u ∣ (𝐹𝑞) <Q u}⟩<P (y +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {u ∣ (𝑞 +Q 𝑟) <Q u}⟩) y<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {u ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q u}⟩) ↔ 𝑞 Q 𝑟 Q (⟨{𝑙𝑙 <Q (𝐹𝑞)}, {u ∣ (𝐹𝑞) <Q u}⟩<P (⟨{𝑙 Qz Q (𝑙 +Q z) <Q (𝐹z)}, {u Qz Q ((𝐹z) +Q z) <Q u}⟩ +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {u ∣ (𝑞 +Q 𝑟) <Q u}⟩) ⟨{𝑙 Qz Q (𝑙 +Q z) <Q (𝐹z)}, {u Qz Q ((𝐹z) +Q z) <Q u}⟩<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {u ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q u}⟩)))
2423rspcev 2650 . 2 ((⟨{𝑙 Qz Q (𝑙 +Q z) <Q (𝐹z)}, {u Qz Q ((𝐹z) +Q z) <Q u}⟩ P 𝑞 Q 𝑟 Q (⟨{𝑙𝑙 <Q (𝐹𝑞)}, {u ∣ (𝐹𝑞) <Q u}⟩<P (⟨{𝑙 Qz Q (𝑙 +Q z) <Q (𝐹z)}, {u Qz Q ((𝐹z) +Q z) <Q u}⟩ +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {u ∣ (𝑞 +Q 𝑟) <Q u}⟩) ⟨{𝑙 Qz Q (𝑙 +Q z) <Q (𝐹z)}, {u Qz Q ((𝐹z) +Q z) <Q u}⟩<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {u ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q u}⟩)) → y P 𝑞 Q 𝑟 Q (⟨{𝑙𝑙 <Q (𝐹𝑞)}, {u ∣ (𝐹𝑞) <Q u}⟩<P (y +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {u ∣ (𝑞 +Q 𝑟) <Q u}⟩) y<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {u ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q u}⟩))
2517, 18, 24syl2anc 391 1 (φy P 𝑞 Q 𝑟 Q (⟨{𝑙𝑙 <Q (𝐹𝑞)}, {u ∣ (𝐹𝑞) <Q u}⟩<P (y +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {u ∣ (𝑞 +Q 𝑟) <Q u}⟩) y<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {u ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q u}⟩))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1242   ∈ wcel 1390  {cab 2023  ∀wral 2300  ∃wrex 2301  {crab 2304  ⟨cop 3370   class class class wbr 3755  ⟶wf 4841  ‘cfv 4845  (class class class)co 5455  Qcnq 6264   +Q cplq 6266
 Copyright terms: Public domain W3C validator