 Intuitionistic Logic Explorer Most Recent Proofs Mirrors  >  Home  >  ILE Home  >  Th. List  >  Recent MPE Most Recent             Other  >  MM 100

Most recent proofs    These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the iset.mm database for the Intuitionistic Logic Explorer. The iset.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from the commit given on the MPE Most Recent Proofs page. The database from that commit is also available here: iset.mm.

See the MPE Most Recent Proofs page for news and some useful links.

 Color key: Intuitionistic Logic Explorer User Mathboxes

Last updated on 27-Sep-2020 at 11:05 PM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem

26-Aug-2020sqrt0rlem 9192 Lemma for sqrt0 9193. (Contributed by Jim Kingdon, 26-Aug-2020.)
((A ((A↑2) = 0 0 ≤ A)) ↔ A = 0)

23-Aug-2020sqrtrval 9189 Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.)
(A ℝ → (√‘A) = (x ℝ ((x↑2) = A 0 ≤ x)))

23-Aug-2020df-rsqrt 9187 Define a function whose value is the square root of a nonnegative real number.

Defining the square root for complex numbers has one difficult part: choosing between the two roots. The usual way to define a principal square root for all complex numbers relies on excluded middle or something similar. But in the case of a nonnegative real number, we don't have the complications presented for general complex numbers, and we can choose the nonnegative root.

(Contributed by Jim Kingdon, 23-Aug-2020.)

√ = (x ℝ ↦ (y ℝ ((y↑2) = x 0 ≤ y)))

19-Aug-2020addnqpr 6541 Addition of fractions embedded into positive reals. One can either add the fractions as fractions, or embed them into positive reals and add them as positive reals, and get the same result. (Contributed by Jim Kingdon, 19-Aug-2020.)
((A Q B Q) → ⟨{𝑙𝑙 <Q (A +Q B)}, {u ∣ (A +Q B) <Q u}⟩ = (⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P ⟨{𝑙𝑙 <Q B}, {uB <Q u}⟩))

19-Aug-2020addnqprlemfu 6540 Lemma for addnqpr 6541. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
((A Q B Q) → (2nd ‘⟨{𝑙𝑙 <Q (A +Q B)}, {u ∣ (A +Q B) <Q u}⟩) ⊆ (2nd ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P ⟨{𝑙𝑙 <Q B}, {uB <Q u}⟩)))

19-Aug-2020addnqprlemfl 6539 Lemma for addnqpr 6541. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
((A Q B Q) → (1st ‘⟨{𝑙𝑙 <Q (A +Q B)}, {u ∣ (A +Q B) <Q u}⟩) ⊆ (1st ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P ⟨{𝑙𝑙 <Q B}, {uB <Q u}⟩)))

19-Aug-2020addnqprlemru 6538 Lemma for addnqpr 6541. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
((A Q B Q) → (2nd ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P ⟨{𝑙𝑙 <Q B}, {uB <Q u}⟩)) ⊆ (2nd ‘⟨{𝑙𝑙 <Q (A +Q B)}, {u ∣ (A +Q B) <Q u}⟩))

19-Aug-2020addnqprlemrl 6537 Lemma for addnqpr 6541. The reverse subset relationship for the lower cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
((A Q B Q) → (1st ‘(⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ +P ⟨{𝑙𝑙 <Q B}, {uB <Q u}⟩)) ⊆ (1st ‘⟨{𝑙𝑙 <Q (A +Q B)}, {u ∣ (A +Q B) <Q u}⟩))

15-Aug-2020cauappcvgprlemcan 6615 Lemma for cauappcvgprlemladdrl 6628. 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}⟩))))

4-Aug-2020cauappcvgprlemupu 6620 Lemma for cauappcvgpr 6633. 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𝐿))

4-Aug-2020cauappcvgprlemopu 6619 Lemma for cauappcvgpr 6633. 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𝐿)))

4-Aug-2020cauappcvgprlemlol 6618 Lemma for cauappcvgpr 6633. 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𝐿))

4-Aug-2020cauappcvgprlemopl 6617 Lemma for cauappcvgpr 6633. 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𝐿)))

18-Jul-2020cauappcvgprlemloc 6623 Lemma for cauappcvgpr 6633. 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𝐿))))

18-Jul-2020cauappcvgprlemdisj 6622 Lemma for cauappcvgpr 6633. 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𝐿)))

18-Jul-2020cauappcvgprlemrnd 6621 Lemma for cauappcvgpr 6633. 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𝐿)))))

18-Jul-2020cauappcvgprlemm 6616 Lemma for cauappcvgpr 6633. 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𝐿)))

11-Jul-2020cauappcvgprlemladdrl 6628 Lemma for cauappcvgprlemladd 6629. 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}⟩)))

11-Jul-2020cauappcvgprlemladdru 6627 Lemma for cauappcvgprlemladd 6629. 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}⟩)))

11-Jul-2020cauappcvgprlemladdfl 6626 Lemma for cauappcvgprlemladd 6629. 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}⟩))

11-Jul-2020cauappcvgprlemladdfu 6625 Lemma for cauappcvgprlemladd 6629. 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}⟩))

8-Jul-2020nqprl 6532 Comparing a fraction to a real can be done by whether it is an element of the lower cut, or by <P. (Contributed by Jim Kingdon, 8-Jul-2020.)
((A Q B P) → (A (1stB) ↔ ⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩<P B))

24-Jun-2020nqprlu 6529 The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 24-Jun-2020.)
(A Q → ⟨{𝑙𝑙 <Q A}, {uA <Q u}⟩ P)

23-Jun-2020cauappcvgprlem2 6631 Lemma for cauappcvgpr 6633. 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}⟩)

23-Jun-2020cauappcvgprlem1 6630 Lemma for cauappcvgpr 6633. 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}⟩))

23-Jun-2020cauappcvgprlemladd 6629 Lemma for cauappcvgpr 6633. 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}⟩)

20-Jun-2020cauappcvgprlemlim 6632 Lemma for cauappcvgpr 6633. 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}⟩))

20-Jun-2020cauappcvgprlemcl 6624 Lemma for cauappcvgpr 6633. 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)

19-Jun-2020cauappcvgpr 6633 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}⟩))

15-Jun-2020imdivapd 9182 Imaginary part of a division. Related to remul2 9081. (Contributed by Jim Kingdon, 15-Jun-2020.)
(φA ℝ)    &   (φB ℂ)    &   (φA # 0)       (φ → (ℑ‘(B / A)) = ((ℑ‘B) / A))

15-Jun-2020redivapd 9181 Real part of a division. Related to remul2 9081. (Contributed by Jim Kingdon, 15-Jun-2020.)
(φA ℝ)    &   (φB ℂ)    &   (φA # 0)       (φ → (ℜ‘(B / A)) = ((ℜ‘B) / A))

15-Jun-2020cjdivapd 9175 Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)       (φ → (∗‘(A / B)) = ((∗‘A) / (∗‘B)))

15-Jun-2020riotaexg 5415 Restricted iota is a set. (Contributed by Jim Kingdon, 15-Jun-2020.)
(A 𝑉 → (x A ψ) V)

14-Jun-2020cjdivapi 9143 Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
A     &   B        (B # 0 → (∗‘(A / B)) = ((∗‘A) / (∗‘B)))

14-Jun-2020cjdivap 9117 Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
((A B B # 0) → (∗‘(A / B)) = ((∗‘A) / (∗‘B)))

14-Jun-2020cjap0 9115 A number is apart from zero iff its complex conjugate is apart from zero. (Contributed by Jim Kingdon, 14-Jun-2020.)
(A ℂ → (A # 0 ↔ (∗‘A) # 0))

14-Jun-2020cjap 9114 Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.)
((A B ℂ) → ((∗‘A) # (∗‘B) ↔ A # B))

14-Jun-2020imdivap 9089 Imaginary part of a division. Related to immul2 9088. (Contributed by Jim Kingdon, 14-Jun-2020.)
((A B B # 0) → (ℑ‘(A / B)) = ((ℑ‘A) / B))

14-Jun-2020redivap 9082 Real part of a division. Related to remul2 9081. (Contributed by Jim Kingdon, 14-Jun-2020.)
((A B B # 0) → (ℜ‘(A / B)) = ((ℜ‘A) / B))

14-Jun-2020mulreap 9072 A product with a real multiplier apart from zero is real iff the multiplicand is real. (Contributed by Jim Kingdon, 14-Jun-2020.)
((A B B # 0) → (A ℝ ↔ (B · A) ℝ))

13-Jun-2020sqgt0apd 9041 The square of a real apart from zero is positive. (Contributed by Jim Kingdon, 13-Jun-2020.)
(φA ℝ)    &   (φA # 0)       (φ → 0 < (A↑2))

13-Jun-2020reexpclzapd 9038 Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.)
(φA ℝ)    &   (φA # 0)    &   (φ𝑁 ℤ)       (φ → (A𝑁) ℝ)

13-Jun-2020expdivapd 9028 Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 13-Jun-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)    &   (φ𝑁 0)       (φ → ((A / B)↑𝑁) = ((A𝑁) / (B𝑁)))

13-Jun-2020sqdivapd 9027 Distribution of square over division. (Contributed by Jim Kingdon, 13-Jun-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φB # 0)       (φ → ((A / B)↑2) = ((A↑2) / (B↑2)))

12-Jun-2020expsubapd 9025 Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)    &   (φ𝑁 ℤ)    &   (φ𝑀 ℤ)       (φ → (A↑(𝑀𝑁)) = ((A𝑀) / (A𝑁)))

12-Jun-2020expm1apd 9024 Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)    &   (φ𝑁 ℤ)       (φ → (A↑(𝑁 − 1)) = ((A𝑁) / A))

12-Jun-2020expp1zapd 9023 Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)    &   (φ𝑁 ℤ)       (φ → (A↑(𝑁 + 1)) = ((A𝑁) · A))

12-Jun-2020exprecapd 9022 Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)    &   (φ𝑁 ℤ)       (φ → ((1 / A)↑𝑁) = (1 / (A𝑁)))

12-Jun-2020expnegapd 9021 Value of a complex number raised to a negative power. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)    &   (φ𝑁 ℤ)       (φ → (A↑-𝑁) = (1 / (A𝑁)))

12-Jun-2020expap0d 9020 Nonnegative integer exponentiation is nonzero if its mantissa is nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)    &   (φ𝑁 ℤ)       (φ → (A𝑁) # 0)

12-Jun-2020expclzapd 9019 Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)    &   (φ𝑁 ℤ)       (φ → (A𝑁) ℂ)

12-Jun-2020sqrecapd 9018 Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)       (φ → ((1 / A)↑2) = (1 / (A↑2)))

12-Jun-2020sqgt0api 8972 The square of a nonzero real is positive. (Contributed by Jim Kingdon, 12-Jun-2020.)
A        (A # 0 → 0 < (A↑2))

12-Jun-2020sqdivapi 8970 Distribution of square over division. (Contributed by Jim Kingdon, 12-Jun-2020.)
A     &   B     &   B # 0       ((A / B)↑2) = ((A↑2) / (B↑2))

11-Jun-2020sqgt0ap 8955 The square of a nonzero real is positive. (Contributed by Jim Kingdon, 11-Jun-2020.)
((A A # 0) → 0 < (A↑2))

11-Jun-2020sqdivap 8952 Distribution of square over division. (Contributed by Jim Kingdon, 11-Jun-2020.)
((A B B # 0) → ((A / B)↑2) = ((A↑2) / (B↑2)))

11-Jun-2020expdivap 8939 Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 11-Jun-2020.)
((A (B B # 0) 𝑁 0) → ((A / B)↑𝑁) = ((A𝑁) / (B𝑁)))

11-Jun-2020expm1ap 8938 Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 11-Jun-2020.)
((A A # 0 𝑁 ℤ) → (A↑(𝑁 − 1)) = ((A𝑁) / A))

11-Jun-2020expp1zap 8937 Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 11-Jun-2020.)
((A A # 0 𝑁 ℤ) → (A↑(𝑁 + 1)) = ((A𝑁) · A))

11-Jun-2020expsubap 8936 Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.)
(((A A # 0) (𝑀 𝑁 ℤ)) → (A↑(𝑀𝑁)) = ((A𝑀) / (A𝑁)))

11-Jun-2020expmulzap 8935 Product of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.)
(((A A # 0) (𝑀 𝑁 ℤ)) → (A↑(𝑀 · 𝑁)) = ((A𝑀)↑𝑁))

10-Jun-2020expaddzap 8933 Sum of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 10-Jun-2020.)
(((A A # 0) (𝑀 𝑁 ℤ)) → (A↑(𝑀 + 𝑁)) = ((A𝑀) · (A𝑁)))

(((A A # 0) (𝑀 -𝑀 ℕ) 𝑁 0) → (A↑(𝑀 + 𝑁)) = ((A𝑀) · (A𝑁)))

10-Jun-2020exprecap 8930 Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 10-Jun-2020.)
((A A # 0 𝑁 ℤ) → ((1 / A)↑𝑁) = (1 / (A𝑁)))

10-Jun-2020mulexpzap 8929 Integer exponentiation of a product. (Contributed by Jim Kingdon, 10-Jun-2020.)
(((A A # 0) (B B # 0) 𝑁 ℤ) → ((A · B)↑𝑁) = ((A𝑁) · (B𝑁)))

10-Jun-2020expap0i 8921 Integer exponentiation is apart from zero if its mantissa is apart from zero. (Contributed by Jim Kingdon, 10-Jun-2020.)
((A A # 0 𝑁 ℤ) → (A𝑁) # 0)

10-Jun-2020expap0 8919 Positive integer exponentiation is apart from zero iff its mantissa is apart from zero. That it is easier to prove this first, and then prove expeq0 8920 in terms of it, rather than the other way around, is perhaps an illustration of the maxim "In constructive analysis, the apartness is more basic [ than ] equality." ([Geuvers], p. 1). (Contributed by Jim Kingdon, 10-Jun-2020.)
((A 𝑁 ℕ) → ((A𝑁) # 0 ↔ A # 0))

10-Jun-2020mvllmulapd 7570 Move LHS left multiplication to RHS. (Contributed by Jim Kingdon, 10-Jun-2020.)
(φA ℂ)    &   (φB ℂ)    &   (φA # 0)    &   (φ → (A · B) = 𝐶)       (φB = (𝐶 / A))

9-Jun-2020expclzap 8914 Closure law for integer exponentiation. (Contributed by Jim Kingdon, 9-Jun-2020.)
((A A # 0 𝑁 ℤ) → (A𝑁) ℂ)

9-Jun-2020expclzaplem 8913 Closure law for integer exponentiation. Lemma for expclzap 8914 and expap0i 8921. (Contributed by Jim Kingdon, 9-Jun-2020.)
((A A # 0 𝑁 ℤ) → (A𝑁) {z ℂ ∣ z # 0})

9-Jun-2020reexpclzap 8909 Closure of exponentiation of reals. (Contributed by Jim Kingdon, 9-Jun-2020.)
((A A # 0 𝑁 ℤ) → (A𝑁) ℝ)

9-Jun-2020neg1ap0 7784 -1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.)
-1 # 0

8-Jun-2020expcl2lemap 8901 Lemma for proving integer exponentiation closure laws. (Contributed by Jim Kingdon, 8-Jun-2020.)
𝐹 ⊆ ℂ    &   ((x 𝐹 y 𝐹) → (x · y) 𝐹)    &   1 𝐹    &   ((x 𝐹 x # 0) → (1 / x) 𝐹)       ((A 𝐹 A # 0 B ℤ) → (AB) 𝐹)

8-Jun-2020expn1ap0 8899 A number to the negative one power is the reciprocal. (Contributed by Jim Kingdon, 8-Jun-2020.)
((A A # 0) → (A↑-1) = (1 / A))

8-Jun-2020expineg2 8898 Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.)
(((A A # 0) (𝑁 -𝑁 0)) → (A𝑁) = (1 / (A↑-𝑁)))

8-Jun-2020expnegap0 8897 Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.)
((A A # 0 𝑁 0) → (A↑-𝑁) = (1 / (A𝑁)))

8-Jun-2020expinnval 8892 Value of exponentiation to positive integer powers. (Contributed by Jim Kingdon, 8-Jun-2020.)
((A 𝑁 ℕ) → (A𝑁) = (seq1( · , (ℕ × {A}), ℂ)‘𝑁))

7-Jun-2020expival 8891 Value of exponentiation to integer powers. (Contributed by Jim Kingdon, 7-Jun-2020.)
((A 𝑁 (A # 0 0 ≤ 𝑁)) → (A𝑁) = if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {A}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {A}), ℂ)‘-𝑁)))))

7-Jun-2020expivallem 8890 Lemma for expival 8891. If we take a complex number apart from zero and raise it to a positive integer power, the result is apart from zero. (Contributed by Jim Kingodon, 7-Jun-2020.)
((A A # 0 𝑁 ℕ) → (seq1( · , (ℕ × {A}), ℂ)‘𝑁) # 0)

7-Jun-2020df-iexp 8889 Define exponentiation to nonnegative integer powers. This definition is not meant to be used directly; instead, exp0 8893 and expp1 8896 provide the standard recursive definition. The up-arrow notation is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976) and is convenient for us since we don't have superscripts. 10-Jun-2005: The definition was extended to include zero exponents, so that 0↑0 = 1 per the convention of Definition 10-4.1 of [Gleason] p. 134. 4-Jun-2014: The definition was extended to include negative integer exponents. The case x = 0, y < 0 gives the value (1 / 0), so we will avoid this case in our theorems. (Contributed by Jim Kingodon, 7-Jun-2020.)
↑ = (x ℂ, y ℤ ↦ if(y = 0, 1, if(0 < y, (seq1( · , (ℕ × {x}), ℂ)‘y), (1 / (seq1( · , (ℕ × {x}), ℂ)‘-y)))))

4-Jun-2020iseqfveq 8887 Equality of sequences. (Contributed by Jim Kingdon, 4-Jun-2020.)
(φ𝑁 (ℤ𝑀))    &   ((φ 𝑘 (𝑀...𝑁)) → (𝐹𝑘) = (𝐺𝑘))    &   (φ𝑆 𝑉)    &   ((φ x (ℤ𝑀)) → (𝐹x) 𝑆)    &   ((φ x (ℤ𝑀)) → (𝐺x) 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x + y) 𝑆)       (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq𝑀( + , 𝐺, 𝑆)‘𝑁))

3-Jun-2020iseqfeq2 8886 Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.)
(φ𝐾 (ℤ𝑀))    &   (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (𝐺𝐾))    &   (φ𝑆 𝑉)    &   ((φ x (ℤ𝑀)) → (𝐹x) 𝑆)    &   ((φ x (ℤ𝐾)) → (𝐺x) 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x + y) 𝑆)    &   ((φ 𝑘 (ℤ‘(𝐾 + 1))) → (𝐹𝑘) = (𝐺𝑘))       (φ → (seq𝑀( + , 𝐹, 𝑆) ↾ (ℤ𝐾)) = seq𝐾( + , 𝐺, 𝑆))

3-Jun-2020iseqfveq2 8885 Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.)
(φ𝐾 (ℤ𝑀))    &   (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (𝐺𝐾))    &   (φ𝑆 𝑉)    &   ((φ x (ℤ𝑀)) → (𝐹x) 𝑆)    &   ((φ x (ℤ𝐾)) → (𝐺x) 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x + y) 𝑆)    &   (φ𝑁 (ℤ𝐾))    &   ((φ 𝑘 ((𝐾 + 1)...𝑁)) → (𝐹𝑘) = (𝐺𝑘))       (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq𝐾( + , 𝐺, 𝑆)‘𝑁))

1-Jun-2020iseqcl 8883 Closure properties of the recursive sequence builder. (Contributed by Jim Kingdon, 1-Jun-2020.)
(φ𝑁 (ℤ𝑀))    &   (φ𝑆 𝑉)    &   ((φ x (ℤ𝑀)) → (𝐹x) 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x + y) 𝑆)       (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) 𝑆)

1-Jun-2020fzdcel 8654 Decidability of membership in a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.)
((𝐾 𝑀 𝑁 ℤ) → DECID 𝐾 (𝑀...𝑁))

1-Jun-2020fztri3or 8653 Trichotomy in terms of a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.)
((𝐾 𝑀 𝑁 ℤ) → (𝐾 < 𝑀 𝐾 (𝑀...𝑁) 𝑁 < 𝐾))

1-Jun-2020zdclt 8074 Integer < is decidable. (Contributed by Jim Kingdon, 1-Jun-2020.)
((A B ℤ) → DECID A < B)

31-May-2020iseqp1 8884 Value of the sequence builder function at a successor. (Contributed by Jim Kingdon, 31-May-2020.)
(φ𝑁 (ℤ𝑀))    &   (φ𝑆 𝑉)    &   ((φ x (ℤ𝑀)) → (𝐹x) 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x + y) 𝑆)       (φ → (seq𝑀( + , 𝐹, 𝑆)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑁) + (𝐹‘(𝑁 + 1))))

31-May-2020iseq1 8882 Value of the sequence builder function at its initial value. (Contributed by Jim Kingdon, 31-May-2020.)
(φ𝑀 ℤ)    &   (φ𝑆 𝑉)    &   ((φ x (ℤ𝑀)) → (𝐹x) 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x + y) 𝑆)       (φ → (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = (𝐹𝑀))

31-May-2020iseqovex 8879 Closure of a function used in proving sequence builder theorems. This can be thought of as a lemma for the small number of sequence builder theorems which need it. (Contributed by Jim Kingdon, 31-May-2020.)
((φ x (ℤ𝑀)) → (𝐹x) 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x + y) 𝑆)       ((φ (x (ℤ𝑀) y 𝑆)) → (x(z (ℤ𝑀), w 𝑆 ↦ (w + (𝐹‘(z + 1))))y) 𝑆)

31-May-2020frecuzrdgcl 8860 Closure law for the recursive definition generator on upper integers. See comment in frec2uz0d 8846 for the description of 𝐺 as the mapping from 𝜔 to (ℤ𝐶). (Contributed by Jim Kingdon, 31-May-2020.)
(φ𝐶 ℤ)    &   𝐺 = frec((x ℤ ↦ (x + 1)), 𝐶)    &   (φ𝑆 𝑉)    &   (φA 𝑆)    &   ((φ (x (ℤ𝐶) y 𝑆)) → (x𝐹y) 𝑆)    &   𝑅 = frec((x (ℤ𝐶), y 𝑆 ↦ ⟨(x + 1), (x𝐹y)⟩), ⟨𝐶, A⟩)    &   (φ𝑇 = ran 𝑅)       ((φ B (ℤ𝐶)) → (𝑇B) 𝑆)

30-May-2020iseqfn 8881 The sequence builder function is a function. (Contributed by Jim Kingdon, 30-May-2020.)
(φ𝑀 ℤ)    &   (φ𝑆 𝑉)    &   ((φ x (ℤ𝑀)) → (𝐹x) 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x + y) 𝑆)       (φ → seq𝑀( + , 𝐹, 𝑆) Fn (ℤ𝑀))

30-May-2020iseqval 8880 Value of the sequence builder function. (Contributed by Jim Kingdon, 30-May-2020.)
𝑅 = frec((x (ℤ𝑀), y 𝑆 ↦ ⟨(x + 1), (x(z (ℤ𝑀), w 𝑆 ↦ (w + (𝐹‘(z + 1))))y)⟩), ⟨𝑀, (𝐹𝑀)⟩)    &   ((φ x (ℤ𝑀)) → (𝐹x) 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x + y) 𝑆)       (φ → seq𝑀( + , 𝐹, 𝑆) = ran 𝑅)

30-May-2020nfiseq 8878 Hypothesis builder for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
x𝑀    &   x +    &   x𝐹    &   x𝑆       xseq𝑀( + , 𝐹, 𝑆)

30-May-2020iseqeq4 8877 Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
(𝑆 = 𝑇 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀( + , 𝐹, 𝑇))

30-May-2020iseqeq3 8876 Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
(𝐹 = 𝐺 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀( + , 𝐺, 𝑆))

30-May-2020iseqeq2 8875 Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
( + = 𝑄 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀(𝑄, 𝐹, 𝑆))

30-May-2020iseqeq1 8874 Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
(𝑀 = 𝑁 → seq𝑀( + , 𝐹, 𝑆) = seq𝑁( + , 𝐹, 𝑆))

30-May-2020nffrec 5921 Bound-variable hypothesis builder for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.)
x𝐹    &   xA       xfrec(𝐹, A)

30-May-2020freceq2 5920 Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.)
(A = B → frec(𝐹, A) = frec(𝐹, B))

 Copyright terms: Public domain W3C HTML validation [external]