Home Intuitionistic Logic ExplorerTheorem List (p. 67 of 95) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 6601-6700   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremrecexprlemrnd 6601* B is rounded. Lemma for recexpr 6610. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (𝑞 Q (𝑞 (1stB) ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1stB))) 𝑟 Q (𝑟 (2ndB) ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2ndB)))))

Theoremrecexprlemdisj 6602* B is disjoint. Lemma for recexpr 6610. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P𝑞 Q ¬ (𝑞 (1stB) 𝑞 (2ndB)))

Theoremrecexprlemloc 6603* B is located. Lemma for recexpr 6610. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1stB) 𝑟 (2ndB))))

Theoremrecexprlempr 6604* B is a positive real. Lemma for recexpr 6610. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A PB P)

Theoremrecexprlem1ssl 6605* The lower cut of one is a subset of the lower cut of A ·P B. Lemma for recexpr 6610. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (1st ‘1P) ⊆ (1st ‘(A ·P B)))

Theoremrecexprlem1ssu 6606* The upper cut of one is a subset of the upper cut of A ·P B. Lemma for recexpr 6610. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (2nd ‘1P) ⊆ (2nd ‘(A ·P B)))

Theoremrecexprlemss1l 6607* The lower cut of A ·P B is a subset of the lower cut of one. Lemma for recexpr 6610. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (1st ‘(A ·P B)) ⊆ (1st ‘1P))

Theoremrecexprlemss1u 6608* The upper cut of A ·P B is a subset of the upper cut of one. Lemma for recexpr 6610. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (2nd ‘(A ·P B)) ⊆ (2nd ‘1P))

Theoremrecexprlemex 6609* B is the reciprocal of A. Lemma for recexpr 6610. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (A ·P B) = 1P)

Theoremrecexpr 6610* The reciprocal of a positive real exists. Part of Proposition 9-3.7(v) of [Gleason] p. 124. (Contributed by NM, 15-May-1996.) (Revised by Mario Carneiro, 12-Jun-2013.)
(A Px P (A ·P x) = 1P)

Theoremaptiprleml 6611 Lemma for aptipr 6613. (Contributed by Jim Kingdon, 28-Jan-2020.)
((A P B P ¬ B<P A) → (1stA) ⊆ (1stB))

Theoremaptiprlemu 6612 Lemma for aptipr 6613. (Contributed by Jim Kingdon, 28-Jan-2020.)
((A P B P ¬ B<P A) → (2ndB) ⊆ (2ndA))

Theoremaptipr 6613 Apartness of positive reals is tight. (Contributed by Jim Kingdon, 28-Jan-2020.)
((A P B P ¬ (A<P B B<P A)) → A = B)

Theoremltmprr 6614 Ordering property of multiplication. (Contributed by Jim Kingdon, 18-Feb-2020.)
((A P B P 𝐶 P) → ((𝐶 ·P A)<P (𝐶 ·P B) → A<P B))

Theoremarchpr 6615* For any positive real, there is an integer that is greater than it. This is also known as the "archimedean property". The integer x is embedded into the reals as described at nnprlu 6534. (Contributed by Jim Kingdon, 22-Apr-2020.)
(A Px N A<P ⟨{𝑙𝑙 <Q [⟨x, 1𝑜⟩] ~Q }, {u ∣ [⟨x, 1𝑜⟩] ~Q <Q u}⟩)

Theoremcauappcvgprlemcan 6616* Lemma for cauappcvgprlemladdrl 6629. Cancelling a term from both sides. (Contributed by Jim Kingdon, 15-Aug-2020.)
(φ𝐿 P)    &   (φ𝑆 Q)    &   (φ𝑅 Q)    &   (φ𝑄 Q)       (φ → ((𝑅 +Q 𝑄) (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q (𝑆 +Q 𝑄)}, {u ∣ (𝑆 +Q 𝑄) <Q u}⟩)) ↔ 𝑅 (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩))))

Theoremcauappcvgprlemm 6617* Lemma for cauappcvgpr 6634. The putative limit is inhabited. (Contributed by Jim Kingdon, 18-Jul-2020.)
(φ𝐹:QQ)    &   (φ𝑝 Q 𝑞 Q ((𝐹𝑝) <Q ((𝐹𝑞) +Q (𝑝 +Q 𝑞)) (𝐹𝑞) <Q ((𝐹𝑝) +Q (𝑝 +Q 𝑞))))    &   (φ𝑝 Q A <Q (𝐹𝑝))    &   𝐿 = ⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)}, {u Q𝑞 Q ((𝐹𝑞) +Q 𝑞) <Q u}⟩       (φ → (𝑠 Q 𝑠 (1st𝐿) 𝑟 Q 𝑟 (2nd𝐿)))

Theoremcauappcvgprlemopl 6618* Lemma for cauappcvgpr 6634. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.)
(φ𝐹:QQ)    &   (φ𝑝 Q 𝑞 Q ((𝐹𝑝) <Q ((𝐹𝑞) +Q (𝑝 +Q 𝑞)) (𝐹𝑞) <Q ((𝐹𝑝) +Q (𝑝 +Q 𝑞))))    &   (φ𝑝 Q A <Q (𝐹𝑝))    &   𝐿 = ⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)}, {u Q𝑞 Q ((𝐹𝑞) +Q 𝑞) <Q u}⟩       ((φ 𝑠 (1st𝐿)) → 𝑟 Q (𝑠 <Q 𝑟 𝑟 (1st𝐿)))

Theoremcauappcvgprlemlol 6619* Lemma for cauappcvgpr 6634. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 4-Aug-2020.)
(φ𝐹:QQ)    &   (φ𝑝 Q 𝑞 Q ((𝐹𝑝) <Q ((𝐹𝑞) +Q (𝑝 +Q 𝑞)) (𝐹𝑞) <Q ((𝐹𝑝) +Q (𝑝 +Q 𝑞))))    &   (φ𝑝 Q A <Q (𝐹𝑝))    &   𝐿 = ⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)}, {u Q𝑞 Q ((𝐹𝑞) +Q 𝑞) <Q u}⟩       ((φ 𝑠 <Q 𝑟 𝑟 (1st𝐿)) → 𝑠 (1st𝐿))

Theoremcauappcvgprlemopu 6620* Lemma for cauappcvgpr 6634. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.)
(φ𝐹:QQ)    &   (φ𝑝 Q 𝑞 Q ((𝐹𝑝) <Q ((𝐹𝑞) +Q (𝑝 +Q 𝑞)) (𝐹𝑞) <Q ((𝐹𝑝) +Q (𝑝 +Q 𝑞))))    &   (φ𝑝 Q A <Q (𝐹𝑝))    &   𝐿 = ⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)}, {u Q𝑞 Q ((𝐹𝑞) +Q 𝑞) <Q u}⟩       ((φ 𝑟 (2nd𝐿)) → 𝑠 Q (𝑠 <Q 𝑟 𝑠 (2nd𝐿)))

Theoremcauappcvgprlemupu 6621* Lemma for cauappcvgpr 6634. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 4-Aug-2020.)
(φ𝐹:QQ)    &   (φ𝑝 Q 𝑞 Q ((𝐹𝑝) <Q ((𝐹𝑞) +Q (𝑝 +Q 𝑞)) (𝐹𝑞) <Q ((𝐹𝑝) +Q (𝑝 +Q 𝑞))))    &   (φ𝑝 Q A <Q (𝐹𝑝))    &   𝐿 = ⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)}, {u Q𝑞 Q ((𝐹𝑞) +Q 𝑞) <Q u}⟩       ((φ 𝑠 <Q 𝑟 𝑠 (2nd𝐿)) → 𝑟 (2nd𝐿))

Theoremcauappcvgprlemrnd 6622* Lemma for cauappcvgpr 6634. The putative limit is rounded. (Contributed by Jim Kingdon, 18-Jul-2020.)
(φ𝐹:QQ)    &   (φ𝑝 Q 𝑞 Q ((𝐹𝑝) <Q ((𝐹𝑞) +Q (𝑝 +Q 𝑞)) (𝐹𝑞) <Q ((𝐹𝑝) +Q (𝑝 +Q 𝑞))))    &   (φ𝑝 Q A <Q (𝐹𝑝))    &   𝐿 = ⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)}, {u Q𝑞 Q ((𝐹𝑞) +Q 𝑞) <Q u}⟩       (φ → (𝑠 Q (𝑠 (1st𝐿) ↔ 𝑟 Q (𝑠 <Q 𝑟 𝑟 (1st𝐿))) 𝑟 Q (𝑟 (2nd𝐿) ↔ 𝑠 Q (𝑠 <Q 𝑟 𝑠 (2nd𝐿)))))

Theoremcauappcvgprlemdisj 6623* Lemma for cauappcvgpr 6634. The putative limit is disjoint. (Contributed by Jim Kingdon, 18-Jul-2020.)
(φ𝐹:QQ)    &   (φ𝑝 Q 𝑞 Q ((𝐹𝑝) <Q ((𝐹𝑞) +Q (𝑝 +Q 𝑞)) (𝐹𝑞) <Q ((𝐹𝑝) +Q (𝑝 +Q 𝑞))))    &   (φ𝑝 Q A <Q (𝐹𝑝))    &   𝐿 = ⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)}, {u Q𝑞 Q ((𝐹𝑞) +Q 𝑞) <Q u}⟩       (φ𝑠 Q ¬ (𝑠 (1st𝐿) 𝑠 (2nd𝐿)))

Theoremcauappcvgprlemloc 6624* Lemma for cauappcvgpr 6634. The putative limit is located. (Contributed by Jim Kingdon, 18-Jul-2020.)
(φ𝐹:QQ)    &   (φ𝑝 Q 𝑞 Q ((𝐹𝑝) <Q ((𝐹𝑞) +Q (𝑝 +Q 𝑞)) (𝐹𝑞) <Q ((𝐹𝑝) +Q (𝑝 +Q 𝑞))))    &   (φ𝑝 Q A <Q (𝐹𝑝))    &   𝐿 = ⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)}, {u Q𝑞 Q ((𝐹𝑞) +Q 𝑞) <Q u}⟩       (φ𝑠 Q 𝑟 Q (𝑠 <Q 𝑟 → (𝑠 (1st𝐿) 𝑟 (2nd𝐿))))

Theoremcauappcvgprlemcl 6625* Lemma for cauappcvgpr 6634. The putative limit is a positive real. (Contributed by Jim Kingdon, 20-Jun-2020.)
(φ𝐹:QQ)    &   (φ𝑝 Q 𝑞 Q ((𝐹𝑝) <Q ((𝐹𝑞) +Q (𝑝 +Q 𝑞)) (𝐹𝑞) <Q ((𝐹𝑝) +Q (𝑝 +Q 𝑞))))    &   (φ𝑝 Q A <Q (𝐹𝑝))    &   𝐿 = ⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)}, {u Q𝑞 Q ((𝐹𝑞) +Q 𝑞) <Q u}⟩       (φ𝐿 P)

Theoremcauappcvgprlemladdfu 6626* Lemma for cauappcvgprlemladd 6630. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.)
(φ𝐹:QQ)    &   (φ𝑝 Q 𝑞 Q ((𝐹𝑝) <Q ((𝐹𝑞) +Q (𝑝 +Q 𝑞)) (𝐹𝑞) <Q ((𝐹𝑝) +Q (𝑝 +Q 𝑞))))    &   (φ𝑝 Q A <Q (𝐹𝑝))    &   𝐿 = ⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)}, {u Q𝑞 Q ((𝐹𝑞) +Q 𝑞) <Q u}⟩    &   (φ𝑆 Q)       (φ → (2nd ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩)) ⊆ (2nd ‘⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q ((𝐹𝑞) +Q 𝑆)}, {u Q𝑞 Q (((𝐹𝑞) +Q 𝑞) +Q 𝑆) <Q u}⟩))

Theoremcauappcvgprlemladdfl 6627* Lemma for cauappcvgprlemladd 6630. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.)
(φ𝐹:QQ)    &   (φ𝑝 Q 𝑞 Q ((𝐹𝑝) <Q ((𝐹𝑞) +Q (𝑝 +Q 𝑞)) (𝐹𝑞) <Q ((𝐹𝑝) +Q (𝑝 +Q 𝑞))))    &   (φ𝑝 Q A <Q (𝐹𝑝))    &   𝐿 = ⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)}, {u Q𝑞 Q ((𝐹𝑞) +Q 𝑞) <Q u}⟩    &   (φ𝑆 Q)       (φ → (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩)) ⊆ (1st ‘⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q ((𝐹𝑞) +Q 𝑆)}, {u Q𝑞 Q (((𝐹𝑞) +Q 𝑞) +Q 𝑆) <Q u}⟩))

Theoremcauappcvgprlemladdru 6628* Lemma for cauappcvgprlemladd 6630. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.)
(φ𝐹:QQ)    &   (φ𝑝 Q 𝑞 Q ((𝐹𝑝) <Q ((𝐹𝑞) +Q (𝑝 +Q 𝑞)) (𝐹𝑞) <Q ((𝐹𝑝) +Q (𝑝 +Q 𝑞))))    &   (φ𝑝 Q A <Q (𝐹𝑝))    &   𝐿 = ⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)}, {u Q𝑞 Q ((𝐹𝑞) +Q 𝑞) <Q u}⟩    &   (φ𝑆 Q)       (φ → (2nd ‘⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q ((𝐹𝑞) +Q 𝑆)}, {u Q𝑞 Q (((𝐹𝑞) +Q 𝑞) +Q 𝑆) <Q u}⟩) ⊆ (2nd ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩)))

Theoremcauappcvgprlemladdrl 6629* Lemma for cauappcvgprlemladd 6630. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.)
(φ𝐹:QQ)    &   (φ𝑝 Q 𝑞 Q ((𝐹𝑝) <Q ((𝐹𝑞) +Q (𝑝 +Q 𝑞)) (𝐹𝑞) <Q ((𝐹𝑝) +Q (𝑝 +Q 𝑞))))    &   (φ𝑝 Q A <Q (𝐹𝑝))    &   𝐿 = ⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)}, {u Q𝑞 Q ((𝐹𝑞) +Q 𝑞) <Q u}⟩    &   (φ𝑆 Q)       (φ → (1st ‘⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q ((𝐹𝑞) +Q 𝑆)}, {u Q𝑞 Q (((𝐹𝑞) +Q 𝑞) +Q 𝑆) <Q u}⟩) ⊆ (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩)))

Theoremcauappcvgprlemladd 6630* Lemma for cauappcvgpr 6634. This takes 𝐿 and offsets it by the positive fraction 𝑆. (Contributed by Jim Kingdon, 23-Jun-2020.)
(φ𝐹:QQ)    &   (φ𝑝 Q 𝑞 Q ((𝐹𝑝) <Q ((𝐹𝑞) +Q (𝑝 +Q 𝑞)) (𝐹𝑞) <Q ((𝐹𝑝) +Q (𝑝 +Q 𝑞))))    &   (φ𝑝 Q A <Q (𝐹𝑝))    &   𝐿 = ⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)}, {u Q𝑞 Q ((𝐹𝑞) +Q 𝑞) <Q u}⟩    &   (φ𝑆 Q)       (φ → (𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩) = ⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q ((𝐹𝑞) +Q 𝑆)}, {u Q𝑞 Q (((𝐹𝑞) +Q 𝑞) +Q 𝑆) <Q u}⟩)

Theoremcauappcvgprlem1 6631* Lemma for cauappcvgpr 6634. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.)
(φ𝐹:QQ)    &   (φ𝑝 Q 𝑞 Q ((𝐹𝑝) <Q ((𝐹𝑞) +Q (𝑝 +Q 𝑞)) (𝐹𝑞) <Q ((𝐹𝑝) +Q (𝑝 +Q 𝑞))))    &   (φ𝑝 Q A <Q (𝐹𝑝))    &   𝐿 = ⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)}, {u Q𝑞 Q ((𝐹𝑞) +Q 𝑞) <Q u}⟩    &   (φ𝑄 Q)    &   (φ𝑅 Q)       (φ → ⟨{𝑙𝑙 <Q (𝐹𝑄)}, {u ∣ (𝐹𝑄) <Q u}⟩<P (𝐿 +P ⟨{𝑙𝑙 <Q (𝑄 +Q 𝑅)}, {u ∣ (𝑄 +Q 𝑅) <Q u}⟩))

Theoremcauappcvgprlem2 6632* Lemma for cauappcvgpr 6634. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.)
(φ𝐹:QQ)    &   (φ𝑝 Q 𝑞 Q ((𝐹𝑝) <Q ((𝐹𝑞) +Q (𝑝 +Q 𝑞)) (𝐹𝑞) <Q ((𝐹𝑝) +Q (𝑝 +Q 𝑞))))    &   (φ𝑝 Q A <Q (𝐹𝑝))    &   𝐿 = ⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)}, {u Q𝑞 Q ((𝐹𝑞) +Q 𝑞) <Q u}⟩    &   (φ𝑄 Q)    &   (φ𝑅 Q)       (φ𝐿<P ⟨{𝑙𝑙 <Q ((𝐹𝑄) +Q (𝑄 +Q 𝑅))}, {u ∣ ((𝐹𝑄) +Q (𝑄 +Q 𝑅)) <Q u}⟩)

Theoremcauappcvgprlemlim 6633* Lemma for cauappcvgpr 6634. The putative limit is a limit. (Contributed by Jim Kingdon, 20-Jun-2020.)
(φ𝐹:QQ)    &   (φ𝑝 Q 𝑞 Q ((𝐹𝑝) <Q ((𝐹𝑞) +Q (𝑝 +Q 𝑞)) (𝐹𝑞) <Q ((𝐹𝑝) +Q (𝑝 +Q 𝑞))))    &   (φ𝑝 Q A <Q (𝐹𝑝))    &   𝐿 = ⟨{𝑙 Q𝑞 Q (𝑙 +Q 𝑞) <Q (𝐹𝑞)}, {u Q𝑞 Q ((𝐹𝑞) +Q 𝑞) <Q u}⟩       (φ𝑞 Q 𝑟 Q (⟨{𝑙𝑙 <Q (𝐹𝑞)}, {u ∣ (𝐹𝑞) <Q u}⟩<P (𝐿 +P ⟨{𝑙𝑙 <Q (𝑞 +Q 𝑟)}, {u ∣ (𝑞 +Q 𝑟) <Q u}⟩) 𝐿<P ⟨{𝑙𝑙 <Q ((𝐹𝑞) +Q (𝑞 +Q 𝑟))}, {u ∣ ((𝐹𝑞) +Q (𝑞 +Q 𝑟)) <Q u}⟩))

Theoremcauappcvgpr 6634* 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.)
(φ𝐹:QQ)    &   (φ𝑝 Q 𝑞 Q ((𝐹𝑝) <Q ((𝐹𝑞) +Q (𝑝 +Q 𝑞)) (𝐹𝑞) <Q ((𝐹𝑝) +Q (𝑝 +Q 𝑞))))    &   (φ𝑝 Q A <Q (𝐹𝑝))       (φ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}⟩))

Theoremarchrecnq 6635* Archimedean principle for fractions (reciprocal version). (Contributed by Jim Kingdon, 27-Sep-2020.)
(A Q𝑗 N (*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) <Q A)

Theoremcaucvgprlemk 6636 Lemma for caucvgpr 6653. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 9-Oct-2020.)
(φ𝐽 <N 𝐾)    &   (φ → (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑄)       (φ → (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) <Q 𝑄)

Theoremcaucvgprlemnkj 6637* Lemma for caucvgpr 6653. Part of disjointness. (Contributed by Jim Kingdon, 23-Oct-2020.)
(φ𝐹:NQ)    &   (φ𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))    &   (φ𝐾 N)    &   (φ𝐽 N)    &   (φ𝑆 Q)       (φ → ¬ ((𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q (𝐹𝐾) ((𝐹𝐽) +Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )) <Q 𝑆))

Theoremcaucvgprlemnbj 6638* Lemma for caucvgpr 6653. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 18-Oct-2020.)
(φ𝐹:NQ)    &   (φ𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))    &   (φB N)    &   (φ𝐽 N)       (φ → ¬ (((𝐹B) +Q (*Q‘[⟨B, 1𝑜⟩] ~Q )) +Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )) <Q (𝐹𝐽))

Theoremcaucvgprlemm 6639* Lemma for caucvgpr 6653. The putative limit is inhabited. (Contributed by Jim Kingdon, 27-Sep-2020.)
(φ𝐹:NQ)    &   (φ𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))    &   (φ𝑗 N A <Q (𝐹𝑗))    &   𝐿 = ⟨{𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)}, {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u}⟩       (φ → (𝑠 Q 𝑠 (1st𝐿) 𝑟 Q 𝑟 (2nd𝐿)))

Theoremcaucvgprlemopl 6640* Lemma for caucvgpr 6653. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.)
(φ𝐹:NQ)    &   (φ𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))    &   (φ𝑗 N A <Q (𝐹𝑗))    &   𝐿 = ⟨{𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)}, {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u}⟩       ((φ 𝑠 (1st𝐿)) → 𝑟 Q (𝑠 <Q 𝑟 𝑟 (1st𝐿)))

Theoremcaucvgprlemlol 6641* Lemma for caucvgpr 6653. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 20-Oct-2020.)
(φ𝐹:NQ)    &   (φ𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))    &   (φ𝑗 N A <Q (𝐹𝑗))    &   𝐿 = ⟨{𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)}, {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u}⟩       ((φ 𝑠 <Q 𝑟 𝑟 (1st𝐿)) → 𝑠 (1st𝐿))

Theoremcaucvgprlemopu 6642* Lemma for caucvgpr 6653. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.)
(φ𝐹:NQ)    &   (φ𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))    &   (φ𝑗 N A <Q (𝐹𝑗))    &   𝐿 = ⟨{𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)}, {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u}⟩       ((φ 𝑟 (2nd𝐿)) → 𝑠 Q (𝑠 <Q 𝑟 𝑠 (2nd𝐿)))

Theoremcaucvgprlemupu 6643* Lemma for caucvgpr 6653. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 20-Oct-2020.)
(φ𝐹:NQ)    &   (φ𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))    &   (φ𝑗 N A <Q (𝐹𝑗))    &   𝐿 = ⟨{𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)}, {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u}⟩       ((φ 𝑠 <Q 𝑟 𝑠 (2nd𝐿)) → 𝑟 (2nd𝐿))

Theoremcaucvgprlemrnd 6644* Lemma for caucvgpr 6653. The putative limit is rounded. (Contributed by Jim Kingdon, 27-Sep-2020.)
(φ𝐹:NQ)    &   (φ𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))    &   (φ𝑗 N A <Q (𝐹𝑗))    &   𝐿 = ⟨{𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)}, {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u}⟩       (φ → (𝑠 Q (𝑠 (1st𝐿) ↔ 𝑟 Q (𝑠 <Q 𝑟 𝑟 (1st𝐿))) 𝑟 Q (𝑟 (2nd𝐿) ↔ 𝑠 Q (𝑠 <Q 𝑟 𝑠 (2nd𝐿)))))

Theoremcaucvgprlemdisj 6645* Lemma for caucvgpr 6653. The putative limit is disjoint. (Contributed by Jim Kingdon, 27-Sep-2020.)
(φ𝐹:NQ)    &   (φ𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))    &   (φ𝑗 N A <Q (𝐹𝑗))    &   𝐿 = ⟨{𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)}, {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u}⟩       (φ𝑠 Q ¬ (𝑠 (1st𝐿) 𝑠 (2nd𝐿)))

Theoremcaucvgprlemloc 6646* Lemma for caucvgpr 6653. The putative limit is located. (Contributed by Jim Kingdon, 27-Sep-2020.)
(φ𝐹:NQ)    &   (φ𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))    &   (φ𝑗 N A <Q (𝐹𝑗))    &   𝐿 = ⟨{𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)}, {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u}⟩       (φ𝑠 Q 𝑟 Q (𝑠 <Q 𝑟 → (𝑠 (1st𝐿) 𝑟 (2nd𝐿))))

Theoremcaucvgprlemcl 6647* Lemma for caucvgpr 6653. The putative limit is a positive real. (Contributed by Jim Kingdon, 26-Sep-2020.)
(φ𝐹:NQ)    &   (φ𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))    &   (φ𝑗 N A <Q (𝐹𝑗))    &   𝐿 = ⟨{𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)}, {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u}⟩       (φ𝐿 P)

Theoremcaucvgprlemladdfu 6648* Lemma for caucvgpr 6653. Adding 𝑆 after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 9-Oct-2020.)
(φ𝐹:NQ)    &   (φ𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))    &   (φ𝑗 N A <Q (𝐹𝑗))    &   𝐿 = ⟨{𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)}, {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u}⟩    &   (φ𝑆 Q)       (φ → (2nd ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩)) ⊆ {u Q𝑗 N (((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) +Q 𝑆) <Q u})

Theoremcaucvgprlemladdrl 6649* Lemma for caucvgpr 6653. Adding 𝑆 after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 8-Oct-2020.)
(φ𝐹:NQ)    &   (φ𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))    &   (φ𝑗 N A <Q (𝐹𝑗))    &   𝐿 = ⟨{𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)}, {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u}⟩    &   (φ𝑆 Q)       (φ → {𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q ((𝐹𝑗) +Q 𝑆)} ⊆ (1st ‘(𝐿 +P ⟨{𝑙𝑙 <Q 𝑆}, {u𝑆 <Q u}⟩)))

Theoremcaucvgprlem1 6650* Lemma for caucvgpr 6653. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.)
(φ𝐹:NQ)    &   (φ𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))    &   (φ𝑗 N A <Q (𝐹𝑗))    &   𝐿 = ⟨{𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)}, {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u}⟩    &   (φ𝑄 Q)    &   (φ𝐽 <N 𝐾)    &   (φ → (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑄)       (φ → ⟨{𝑙𝑙 <Q (𝐹𝐾)}, {u ∣ (𝐹𝐾) <Q u}⟩<P (𝐿 +P ⟨{𝑙𝑙 <Q 𝑄}, {u𝑄 <Q u}⟩))

Theoremcaucvgprlem2 6651* Lemma for caucvgpr 6653. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.)
(φ𝐹:NQ)    &   (φ𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))    &   (φ𝑗 N A <Q (𝐹𝑗))    &   𝐿 = ⟨{𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)}, {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u}⟩    &   (φ𝑄 Q)    &   (φ𝐽 <N 𝐾)    &   (φ → (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑄)       (φ𝐿<P ⟨{𝑙𝑙 <Q ((𝐹𝐾) +Q 𝑄)}, {u ∣ ((𝐹𝐾) +Q 𝑄) <Q u}⟩)

Theoremcaucvgprlemlim 6652* Lemma for caucvgpr 6653. The putative limit is a limit. (Contributed by Jim Kingdon, 1-Oct-2020.)
(φ𝐹:NQ)    &   (φ𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))    &   (φ𝑗 N A <Q (𝐹𝑗))    &   𝐿 = ⟨{𝑙 Q𝑗 N (𝑙 +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q (𝐹𝑗)}, {u Q𝑗 N ((𝐹𝑗) +Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )) <Q u}⟩       (φx Q 𝑗 N 𝑘 N (𝑗 <N 𝑘 → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {u ∣ (𝐹𝑘) <Q u}⟩<P (𝐿 +P ⟨{𝑙𝑙 <Q x}, {ux <Q u}⟩) 𝐿<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q x)}, {u ∣ ((𝐹𝑘) +Q x) <Q u}⟩)))

Theoremcaucvgpr 6653* 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 A, to avoid the case where we have positive fractions which converge to zero (which is not a positive real). (Contributed by Jim Kingdon, 18-Jun-2020.)
(φ𝐹:NQ)    &   (φ𝑛 N 𝑘 N (𝑛 <N 𝑘 → ((𝐹𝑛) <Q ((𝐹𝑘) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )) (𝐹𝑘) <Q ((𝐹𝑛) +Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )))))    &   (φ𝑗 N A <Q (𝐹𝑗))       (φy P x Q 𝑗 N 𝑘 N (𝑗 <N 𝑘 → (⟨{𝑙𝑙 <Q (𝐹𝑘)}, {u ∣ (𝐹𝑘) <Q u}⟩<P (y +P ⟨{𝑙𝑙 <Q x}, {ux <Q u}⟩) y<P ⟨{𝑙𝑙 <Q ((𝐹𝑘) +Q x)}, {u ∣ ((𝐹𝑘) +Q x) <Q u}⟩)))

Definitiondf-enr 6654* Define equivalence relation for signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.1 of [Gleason] p. 126. (Contributed by NM, 25-Jul-1995.)
~R = {⟨x, y⟩ ∣ ((x (P × P) y (P × P)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z +P u) = (w +P v)))}

Definitiondf-nr 6655 Define class of signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 25-Jul-1995.)
R = ((P × P) / ~R )

Definitiondf-plr 6656* Define addition on signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 25-Aug-1995.)
+R = {⟨⟨x, y⟩, z⟩ ∣ ((x R y R) wvuf((x = [⟨w, v⟩] ~R y = [⟨u, f⟩] ~R ) z = [⟨(w +P u), (v +P f)⟩] ~R ))}

Definitiondf-mr 6657* Define multiplication on signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 25-Aug-1995.)
·R = {⟨⟨x, y⟩, z⟩ ∣ ((x R y R) wvuf((x = [⟨w, v⟩] ~R y = [⟨u, f⟩] ~R ) z = [⟨((w ·P u) +P (v ·P f)), ((w ·P f) +P (v ·P u))⟩] ~R ))}

Definitiondf-ltr 6658* Define ordering relation on signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.4 of [Gleason] p. 127. (Contributed by NM, 14-Feb-1996.)
<R = {⟨x, y⟩ ∣ ((x R y R) zwvu((x = [⟨z, w⟩] ~R y = [⟨v, u⟩] ~R ) (z +P u)<P (w +P v)))}

Definitiondf-0r 6659 Define signed real constant 0. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 9-Aug-1995.)
0R = [⟨1P, 1P⟩] ~R

Definitiondf-1r 6660 Define signed real constant 1. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 9-Aug-1995.)
1R = [⟨(1P +P 1P), 1P⟩] ~R

Definitiondf-m1r 6661 Define signed real constant -1. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 9-Aug-1995.)
-1R = [⟨1P, (1P +P 1P)⟩] ~R

Theoremenrbreq 6662 Equivalence relation for signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.)
(((A P B P) (𝐶 P 𝐷 P)) → (⟨A, B⟩ ~R𝐶, 𝐷⟩ ↔ (A +P 𝐷) = (B +P 𝐶)))

Theoremenrer 6663 The equivalence relation for signed reals is an equivalence relation. Proposition 9-4.1 of [Gleason] p. 126. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 6-Jul-2015.)
~R Er (P × P)

Theoremenreceq 6664 Equivalence class equality of positive fractions in terms of positive integers. (Contributed by NM, 29-Nov-1995.)
(((A P B P) (𝐶 P 𝐷 P)) → ([⟨A, B⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ↔ (A +P 𝐷) = (B +P 𝐶)))

Theoremenrex 6665 The equivalence relation for signed reals exists. (Contributed by NM, 25-Jul-1995.)
~R V

Theoremltrelsr 6666 Signed real 'less than' is a relation on signed reals. (Contributed by NM, 14-Feb-1996.)
<R ⊆ (R × R)

((((A P B P) (𝐶 P 𝐷 P)) ((𝐹 P 𝐺 P) (𝑅 P 𝑆 P))) → (((A +P 𝐷) = (B +P 𝐶) (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ⟨(A +P 𝐹), (B +P 𝐺)⟩ ~R ⟨(𝐶 +P 𝑅), (𝐷 +P 𝑆)⟩))

Theoremmulcmpblnrlemg 6668 Lemma used in lemma showing compatibility of multiplication. (Contributed by Jim Kingdon, 1-Jan-2020.)
((((A P B P) (𝐶 P 𝐷 P)) ((𝐹 P 𝐺 P) (𝑅 P 𝑆 P))) → (((A +P 𝐷) = (B +P 𝐶) (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ((𝐷 ·P 𝐹) +P (((A ·P 𝐹) +P (B ·P 𝐺)) +P ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅)))) = ((𝐷 ·P 𝐹) +P (((A ·P 𝐺) +P (B ·P 𝐹)) +P ((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆))))))

Theoremmulcmpblnr 6669 Lemma showing compatibility of multiplication. (Contributed by NM, 5-Sep-1995.)
((((A P B P) (𝐶 P 𝐷 P)) ((𝐹 P 𝐺 P) (𝑅 P 𝑆 P))) → (((A +P 𝐷) = (B +P 𝐶) (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ⟨((A ·P 𝐹) +P (B ·P 𝐺)), ((A ·P 𝐺) +P (B ·P 𝐹))⟩ ~R ⟨((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)), ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅))⟩))

Theoremprsrlem1 6670* Decomposing signed reals into positive reals. Lemma for addsrpr 6673 and mulsrpr 6674. (Contributed by Jim Kingdon, 30-Dec-2019.)
(((A ((P × P) / ~R ) B ((P × P) / ~R )) ((A = [⟨w, v⟩] ~R B = [⟨u, 𝑡⟩] ~R ) (A = [⟨𝑠, f⟩] ~R B = [⟨g, ⟩] ~R ))) → ((((w P v P) (𝑠 P f P)) ((u P 𝑡 P) (g P P))) ((w +P f) = (v +P 𝑠) (u +P ) = (𝑡 +P g))))

Theoremaddsrmo 6671* There is at most one result from adding signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
((A ((P × P) / ~R ) B ((P × P) / ~R )) → ∃*zwvu𝑡((A = [⟨w, v⟩] ~R B = [⟨u, 𝑡⟩] ~R ) z = [⟨(w +P u), (v +P 𝑡)⟩] ~R ))

Theoremmulsrmo 6672* There is at most one result from multiplying signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
((A ((P × P) / ~R ) B ((P × P) / ~R )) → ∃*zwvu𝑡((A = [⟨w, v⟩] ~R B = [⟨u, 𝑡⟩] ~R ) z = [⟨((w ·P u) +P (v ·P 𝑡)), ((w ·P 𝑡) +P (v ·P u))⟩] ~R ))

Theoremaddsrpr 6673 Addition of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
(((A P B P) (𝐶 P 𝐷 P)) → ([⟨A, B⟩] ~R +R [⟨𝐶, 𝐷⟩] ~R ) = [⟨(A +P 𝐶), (B +P 𝐷)⟩] ~R )

Theoremmulsrpr 6674 Multiplication of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
(((A P B P) (𝐶 P 𝐷 P)) → ([⟨A, B⟩] ~R ·R [⟨𝐶, 𝐷⟩] ~R ) = [⟨((A ·P 𝐶) +P (B ·P 𝐷)), ((A ·P 𝐷) +P (B ·P 𝐶))⟩] ~R )

Theoremltsrprg 6675 Ordering of signed reals in terms of positive reals. (Contributed by Jim Kingdon, 2-Jan-2019.)
(((A P B P) (𝐶 P 𝐷 P)) → ([⟨A, B⟩] ~R <R [⟨𝐶, 𝐷⟩] ~R ↔ (A +P 𝐷)<P (B +P 𝐶)))

Theoremgt0srpr 6676 Greater than zero in terms of positive reals. (Contributed by NM, 13-May-1996.)
(0R <R [⟨A, B⟩] ~RB<P A)

Theorem0nsr 6677 The empty set is not a signed real. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.)
¬ ∅ R

Theorem0r 6678 The constant 0R is a signed real. (Contributed by NM, 9-Aug-1995.)
0R R

Theorem1sr 6679 The constant 1R is a signed real. (Contributed by NM, 9-Aug-1995.)
1R R

Theoremm1r 6680 The constant -1R is a signed real. (Contributed by NM, 9-Aug-1995.)
-1R R

Theoremaddclsr 6681 Closure of addition on signed reals. (Contributed by NM, 25-Jul-1995.)
((A R B R) → (A +R B) R)

Theoremmulclsr 6682 Closure of multiplication on signed reals. (Contributed by NM, 10-Aug-1995.)
((A R B R) → (A ·R B) R)

Theoremaddcomsrg 6683 Addition of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.)
((A R B R) → (A +R B) = (B +R A))

Theoremaddasssrg 6684 Addition of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.)
((A R B R 𝐶 R) → ((A +R B) +R 𝐶) = (A +R (B +R 𝐶)))

Theoremmulcomsrg 6685 Multiplication of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.)
((A R B R) → (A ·R B) = (B ·R A))

Theoremmulasssrg 6686 Multiplication of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.)
((A R B R 𝐶 R) → ((A ·R B) ·R 𝐶) = (A ·R (B ·R 𝐶)))

Theoremdistrsrg 6687 Multiplication of signed reals is distributive. (Contributed by Jim Kingdon, 4-Jan-2020.)
((A R B R 𝐶 R) → (A ·R (B +R 𝐶)) = ((A ·R B) +R (A ·R 𝐶)))

Theoremm1p1sr 6688 Minus one plus one is zero for signed reals. (Contributed by NM, 5-May-1996.)
(-1R +R 1R) = 0R

Theoremm1m1sr 6689 Minus one times minus one is plus one for signed reals. (Contributed by NM, 14-May-1996.)
(-1R ·R -1R) = 1R

Theoremlttrsr 6690* Signed real 'less than' is a transitive relation. (Contributed by Jim Kingdon, 4-Jan-2019.)
((f R g R R) → ((f <R g g <R ) → f <R ))

Theoremltposr 6691 Signed real 'less than' is a partial order. (Contributed by Jim Kingdon, 4-Jan-2019.)
<R Po R

Theoremltsosr 6692 Signed real 'less than' is a strict ordering. (Contributed by NM, 19-Feb-1996.)
<R Or R

Theorem0lt1sr 6693 0 is less than 1 for signed reals. (Contributed by NM, 26-Mar-1996.)
0R <R 1R

Theorem1ne0sr 6694 1 and 0 are distinct for signed reals. (Contributed by NM, 26-Mar-1996.)
¬ 1R = 0R

Theorem0idsr 6695 The signed real number 0 is an identity element for addition of signed reals. (Contributed by NM, 10-Apr-1996.)
(A R → (A +R 0R) = A)

Theorem1idsr 6696 1 is an identity element for multiplication. (Contributed by Jim Kingdon, 5-Jan-2020.)
(A R → (A ·R 1R) = A)

Theorem00sr 6697 A signed real times 0 is 0. (Contributed by NM, 10-Apr-1996.)
(A R → (A ·R 0R) = 0R)

Theoremltasrg 6698 Ordering property of addition. (Contributed by NM, 10-May-1996.)
((A R B R 𝐶 R) → (A <R B ↔ (𝐶 +R A) <R (𝐶 +R B)))

Theorempn0sr 6699 A signed real plus its negative is zero. (Contributed by NM, 14-May-1996.)
(A R → (A +R (A ·R -1R)) = 0R)

Theoremnegexsr 6700* Existence of negative signed real. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 2-May-1996.)
(A Rx R (A +R x) = 0R)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9457
 Copyright terms: Public domain < Previous  Next >