P. 157 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15601-15700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-inf2vn2 15601*	A sufficient condition for ω to be a set; unbounded version of bj-inf2vn 15600. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → 𝐴 = ω))
Axiom	ax-inf2 15602*	Another axiom of infinity in a constructive setting (see ax-infvn 15567). (Contributed by BJ, 14-Nov-2019.) (New usage is discouraged.)
⊢ ∃𝑎∀𝑥(𝑥 ∈ 𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝑎 𝑥 = suc 𝑦))
Theorem	bj-omex2 15603	Using bounded set induction and the strong axiom of infinity, ω is a set, that is, we recover ax-infvn 15567 (see bj-2inf 15564 for the equivalence of the latter with bj-omex 15568). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ω ∈ V
Theorem	bj-nn0sucALT 15604*	Alternate proof of bj-nn0suc 15590, also constructive but from ax-inf2 15602, hence requiring ax-bdsetind 15594. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ ω ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥))
13.2.11.2  Full induction In this section, using the axiom of set induction, we prove full induction on the set of natural numbers.
Theorem	bj-findis 15605*	Principle of induction, using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See bj-bdfindis 15573 for a bounded version not requiring ax-setind 4573. See finds 4636 for a proof in IZF. From this version, it is easy to prove of finds 4636, finds2 4637, finds1 4638. (Contributed by BJ, 22-Dec-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑥𝜃    &   ⊢ (𝑥 = ∅ → (𝜓 → 𝜑))    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜒))    &   ⊢ (𝑥 = suc 𝑦 → (𝜃 → 𝜑))    ⇒   ⊢ ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒 → 𝜃)) → ∀𝑥 ∈ ω 𝜑)
Theorem	bj-findisg 15606*	Version of bj-findis 15605 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-findis 15605 for explanations. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑥𝜃    &   ⊢ (𝑥 = ∅ → (𝜓 → 𝜑))    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜒))    &   ⊢ (𝑥 = suc 𝑦 → (𝜃 → 𝜑))    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜏    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜏))    ⇒   ⊢ ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒 → 𝜃)) → (𝐴 ∈ ω → 𝜏))
Theorem	bj-findes 15607	Principle of induction, using explicit substitutions. Constructive proof (from CZF). See the comment of bj-findis 15605 for explanations. From this version, it is easy to prove findes 4639. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
⊢ (([∅ / 𝑥]𝜑 ∧ ∀𝑥 ∈ ω (𝜑 → [suc 𝑥 / 𝑥]𝜑)) → ∀𝑥 ∈ ω 𝜑)
13.2.12  CZF: Strong collection In this section, we state the axiom scheme of strong collection, which is part of CZF set theory.
Axiom	ax-strcoll 15608*	Axiom scheme of strong collection. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. The antecedent means that 𝜑 represents a multivalued function on 𝑎, or equivalently a collection of nonempty classes indexed by 𝑎, and the axiom asserts the existence of a set 𝑏 which "collects" at least one element in the image of each 𝑥 ∈ 𝑎 and which is made only of such elements. That second conjunct is what makes it "strong", compared to the axiom scheme of collection ax-coll 4148. (Contributed by BJ, 5-Oct-2019.)
⊢ ∀𝑎(∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑))
Theorem	strcoll2 15609*	Version of ax-strcoll 15608 with one disjoint variable condition removed and without initial universal quantifier. (Contributed by BJ, 5-Oct-2019.)
⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑))
Theorem	strcollnft 15610*	Closed form of strcollnf 15611. (Contributed by BJ, 21-Oct-2019.)
⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑)))
Theorem	strcollnf 15611*	Version of ax-strcoll 15608 with one disjoint variable condition removed, the other disjoint variable condition replaced with a nonfreeness hypothesis, and without initial universal quantifier. Version of strcoll2 15609 with the disjoint variable condition on 𝑏, 𝜑 replaced with a nonfreeness hypothesis. This proof aims to demonstrate a standard technique, but strcoll2 15609 will generally suffice: since the theorem asserts the existence of a set 𝑏, supposing that that setvar does not occur in the already defined 𝜑 is not a big constraint. (Contributed by BJ, 21-Oct-2019.)
⊢ Ⅎ𝑏𝜑    ⇒   ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑))
Theorem	strcollnfALT 15612*	Alternate proof of strcollnf 15611, not using strcollnft 15610. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑏𝜑    ⇒   ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑))
13.2.13  CZF: Subset collection In this section, we state the axiom scheme of subset collection, which is part of CZF set theory.
Axiom	ax-sscoll 15613*	Axiom scheme of subset collection. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. The antecedent means that 𝜑 represents a multivalued function from 𝑎 to 𝑏, or equivalently a collection of nonempty subsets of 𝑏 indexed by 𝑎, and the consequent asserts the existence of a subset of 𝑐 which "collects" at least one element in the image of each 𝑥 ∈ 𝑎 and which is made only of such elements. The axiom asserts the existence, for any sets 𝑎, 𝑏, of a set 𝑐 such that that implication holds for any value of the parameter 𝑧 of 𝜑. (Contributed by BJ, 5-Oct-2019.)
⊢ ∀𝑎∀𝑏∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑑 𝜑 ∧ ∀𝑦 ∈ 𝑑 ∃𝑥 ∈ 𝑎 𝜑))
Theorem	sscoll2 15614*	Version of ax-sscoll 15613 with two disjoint variable conditions removed and without initial universal quantifiers. (Contributed by BJ, 5-Oct-2019.)
⊢ ∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑑 𝜑 ∧ ∀𝑦 ∈ 𝑑 ∃𝑥 ∈ 𝑎 𝜑))
13.2.14  Real numbers
Axiom	ax-ddkcomp 15615	Axiom of Dedekind completeness for Dedekind real numbers: every inhabited upper-bounded located set of reals has a real upper bound. Ideally, this axiom should be "proved" as "axddkcomp" for the real numbers constructed from IZF, and then Axiom ax-ddkcomp 15615 should be used in place of construction specific results. In particular, axcaucvg 7967 should be proved from it. (Contributed by BJ, 24-Oct-2021.)
⊢ (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ∧ ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → 𝑥 ≤ 𝐵)))
13.3  Mathbox for Jim Kingdon
13.3.1  Propositional and predicate logic
Theorem	nnnotnotr 15616	Double negation of double negation elimination. Suggested by an online post by Martin Escardo. Although this statement resembles nnexmid 851, it can be proved with reference only to implication and negation (that is, without use of disjunction). (Contributed by Jim Kingdon, 21-Oct-2024.)
⊢ ¬ ¬ (¬ ¬ 𝜑 → 𝜑)
13.3.2  Natural numbers
Theorem	1dom1el 15617	If a set is dominated by one, then any two of its elements are equal. (Contributed by Jim Kingdon, 23-Apr-2025.)
⊢ ((𝐴 ≼ 1o ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → 𝐵 = 𝐶)
Theorem	ss1oel2o 15618	Any subset of ordinal one being an element of ordinal two is equivalent to excluded middle. A variation of exmid01 4231 which more directly illustrates the contrast with el2oss1o 6501. (Contributed by Jim Kingdon, 8-Aug-2022.)
⊢ (EXMID ↔ ∀𝑥(𝑥 ⊆ 1o → 𝑥 ∈ 2o))
Theorem	nnti 15619	Ordering on a natural number generates a tight apartness. (Contributed by Jim Kingdon, 7-Aug-2022.)
⊢ (𝜑 → 𝐴 ∈ ω)    ⇒   ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢 E 𝑣 ∧ ¬ 𝑣 E 𝑢)))
Theorem	012of 15620	Mapping zero and one between ℕ0 and ω style integers. (Contributed by Jim Kingdon, 28-Jun-2024.)
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    ⇒   ⊢ (◡𝐺 ↾ {0, 1}):{0, 1}⟶2o
Theorem	2o01f 15621	Mapping zero and one between ω and ℕ0 style integers. (Contributed by Jim Kingdon, 28-Jun-2024.)
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    ⇒   ⊢ (𝐺 ↾ 2o):2o⟶{0, 1}
13.3.3  The power set of a singleton
Theorem	pwtrufal 15622	A subset of the singleton {∅} cannot be anything other than ∅ or {∅}. Removing the double negation would change the meaning, as seen at exmid01 4231. If we view a subset of a singleton as a truth value (as seen in theorems like exmidexmid 4229), then this theorem states there are no truth values other than true and false, as described in section 1.1 of [Bauer], p. 481. (Contributed by Mario Carneiro and Jim Kingdon, 11-Sep-2023.)
⊢ (𝐴 ⊆ {∅} → ¬ ¬ (𝐴 = ∅ ∨ 𝐴 = {∅}))
Theorem	pwle2 15623*	An exercise related to 𝑁 copies of a singleton and the power set of a singleton (where the latter can also be thought of as representing truth values). Posed as an exercise by Martin Escardo online. (Contributed by Jim Kingdon, 3-Sep-2023.)
⊢ 𝑇 = ∪ 𝑥 ∈ 𝑁 ({𝑥} × 1o)    ⇒   ⊢ ((𝑁 ∈ ω ∧ 𝐺:𝑇–1-1→𝒫 1o) → 𝑁 ⊆ 2o)
Theorem	pwf1oexmid 15624*	An exercise related to 𝑁 copies of a singleton and the power set of a singleton (where the latter can also be thought of as representing truth values). Posed as an exercise by Martin Escardo online. (Contributed by Jim Kingdon, 3-Sep-2023.)
⊢ 𝑇 = ∪ 𝑥 ∈ 𝑁 ({𝑥} × 1o)    ⇒   ⊢ ((𝑁 ∈ ω ∧ 𝐺:𝑇–1-1→𝒫 1o) → (ran 𝐺 = 𝒫 1o ↔ (𝑁 = 2o ∧ EXMID)))
Theorem	subctctexmid 15625*	If every subcountable set is countable and Markov's principle holds, excluded middle follows. Proposition 2.6 of [BauerSwan], p. 14:4. The proof is taken from that paper. (Contributed by Jim Kingdon, 29-Nov-2023.)
⊢ (𝜑 → ∀𝑥(∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→𝑥) → ∃𝑔 𝑔:ω–onto→(𝑥 ⊔ 1o)))    &   ⊢ (𝜑 → ω ∈ Markov)    ⇒   ⊢ (𝜑 → EXMID)
Theorem	sssneq 15626*	Any two elements of a subset of a singleton are equal. (Contributed by Jim Kingdon, 28-May-2024.)
⊢ (𝐴 ⊆ {𝐵} → ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 𝑦 = 𝑧)
Theorem	pw1nct 15627*	A condition which ensures that the powerset of a singleton is not countable. The antecedent here can be referred to as the uniformity principle. Based on Mastodon posts by Andrej Bauer and Rahul Chhabra. (Contributed by Jim Kingdon, 29-May-2024.)
⊢ (∀𝑟(𝑟 ⊆ (𝒫 1o × ω) → (∀𝑝 ∈ 𝒫 1o∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1o𝑞𝑟𝑚)) → ¬ ∃𝑓 𝑓:ω–onto→(𝒫 1o ⊔ 1o))
13.3.4  Omniscience of NN+oo
Theorem	0nninf 15628	The zero element of ℕ∞ (the constant sequence equal to ∅). (Contributed by Jim Kingdon, 14-Jul-2022.)
⊢ (ω × {∅}) ∈ ℕ∞
Theorem	nnsf 15629*	Domain and range of 𝑆. Part of Definition 3.3 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 30-Jul-2022.)
⊢ 𝑆 = (𝑝 ∈ ℕ∞ ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖))))    ⇒   ⊢ 𝑆:ℕ∞⟶ℕ∞
Theorem	peano4nninf 15630*	The successor function on ℕ∞ is one to one. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 31-Jul-2022.)
⊢ 𝑆 = (𝑝 ∈ ℕ∞ ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖))))    ⇒   ⊢ 𝑆:ℕ∞–1-1→ℕ∞
Theorem	peano3nninf 15631*	The successor function on ℕ∞ is never zero. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 1-Aug-2022.)
⊢ 𝑆 = (𝑝 ∈ ℕ∞ ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖))))    ⇒   ⊢ (𝐴 ∈ ℕ∞ → (𝑆‘𝐴) ≠ (𝑥 ∈ ω ↦ ∅))
Theorem	nninfalllem1 15632*	Lemma for nninfall 15633. (Contributed by Jim Kingdon, 1-Aug-2022.)
⊢ (𝜑 → 𝑄 ∈ (2o ↑𝑚 ℕ∞))    &   ⊢ (𝜑 → (𝑄‘(𝑥 ∈ ω ↦ 1o)) = 1o)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω (𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = 1o)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ∞)    &   ⊢ (𝜑 → (𝑄‘𝑃) = ∅)    ⇒   ⊢ (𝜑 → ∀𝑛 ∈ ω (𝑃‘𝑛) = 1o)
Theorem	nninfall 15633*	Given a decidable predicate on ℕ∞, showing it holds for natural numbers and the point at infinity suffices to show it holds everywhere. The sense in which 𝑄 is a decidable predicate is that it assigns a value of either ∅ or 1o (which can be thought of as false and true) to every element of ℕ∞. Lemma 3.5 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 1-Aug-2022.)
⊢ (𝜑 → 𝑄 ∈ (2o ↑𝑚 ℕ∞))    &   ⊢ (𝜑 → (𝑄‘(𝑥 ∈ ω ↦ 1o)) = 1o)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω (𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = 1o)    ⇒   ⊢ (𝜑 → ∀𝑝 ∈ ℕ∞ (𝑄‘𝑝) = 1o)
Theorem	nninfsellemdc 15634*	Lemma for nninfself 15637. Showing that the selection function is well defined. (Contributed by Jim Kingdon, 8-Aug-2022.)
⊢ ((𝑄 ∈ (2o ↑𝑚 ℕ∞) ∧ 𝑁 ∈ ω) → DECID ∀𝑘 ∈ suc 𝑁(𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o)
Theorem	nninfsellemcl 15635*	Lemma for nninfself 15637. (Contributed by Jim Kingdon, 8-Aug-2022.)
⊢ ((𝑄 ∈ (2o ↑𝑚 ℕ∞) ∧ 𝑁 ∈ ω) → if(∀𝑘 ∈ suc 𝑁(𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o, 1o, ∅) ∈ 2o)
Theorem	nninfsellemsuc 15636*	Lemma for nninfself 15637. (Contributed by Jim Kingdon, 6-Aug-2022.)
⊢ ((𝑄 ∈ (2o ↑𝑚 ℕ∞) ∧ 𝐽 ∈ ω) → if(∀𝑘 ∈ suc suc 𝐽(𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o, 1o, ∅) ⊆ if(∀𝑘 ∈ suc 𝐽(𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o, 1o, ∅))
Theorem	nninfself 15637*	Domain and range of the selection function for ℕ∞. (Contributed by Jim Kingdon, 6-Aug-2022.)
⊢ 𝐸 = (𝑞 ∈ (2o ↑𝑚 ℕ∞) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o, 1o, ∅)))    ⇒   ⊢ 𝐸:(2o ↑𝑚 ℕ∞)⟶ℕ∞
Theorem	nninfsellemeq 15638*	Lemma for nninfsel 15641. (Contributed by Jim Kingdon, 9-Aug-2022.)
⊢ 𝐸 = (𝑞 ∈ (2o ↑𝑚 ℕ∞) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o, 1o, ∅)))    &   ⊢ (𝜑 → 𝑄 ∈ (2o ↑𝑚 ℕ∞))    &   ⊢ (𝜑 → (𝑄‘(𝐸‘𝑄)) = 1o)    &   ⊢ (𝜑 → 𝑁 ∈ ω)    &   ⊢ (𝜑 → ∀𝑘 ∈ 𝑁 (𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o)    &   ⊢ (𝜑 → (𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))) = ∅)    ⇒   ⊢ (𝜑 → (𝐸‘𝑄) = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)))
Theorem	nninfsellemqall 15639*	Lemma for nninfsel 15641. (Contributed by Jim Kingdon, 9-Aug-2022.)
⊢ 𝐸 = (𝑞 ∈ (2o ↑𝑚 ℕ∞) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o, 1o, ∅)))    &   ⊢ (𝜑 → 𝑄 ∈ (2o ↑𝑚 ℕ∞))    &   ⊢ (𝜑 → (𝑄‘(𝐸‘𝑄)) = 1o)    &   ⊢ (𝜑 → 𝑁 ∈ ω)    ⇒   ⊢ (𝜑 → (𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))) = 1o)
Theorem	nninfsellemeqinf 15640*	Lemma for nninfsel 15641. (Contributed by Jim Kingdon, 9-Aug-2022.)
⊢ 𝐸 = (𝑞 ∈ (2o ↑𝑚 ℕ∞) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o, 1o, ∅)))    &   ⊢ (𝜑 → 𝑄 ∈ (2o ↑𝑚 ℕ∞))    &   ⊢ (𝜑 → (𝑄‘(𝐸‘𝑄)) = 1o)    ⇒   ⊢ (𝜑 → (𝐸‘𝑄) = (𝑖 ∈ ω ↦ 1o))
Theorem	nninfsel 15641*	𝐸 is a selection function for ℕ∞. Theorem 3.6 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 9-Aug-2022.)
⊢ 𝐸 = (𝑞 ∈ (2o ↑𝑚 ℕ∞) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o, 1o, ∅)))    &   ⊢ (𝜑 → 𝑄 ∈ (2o ↑𝑚 ℕ∞))    &   ⊢ (𝜑 → (𝑄‘(𝐸‘𝑄)) = 1o)    ⇒   ⊢ (𝜑 → ∀𝑝 ∈ ℕ∞ (𝑄‘𝑝) = 1o)
Theorem	nninfomnilem 15642*	Lemma for nninfomni 15643. (Contributed by Jim Kingdon, 10-Aug-2022.)
⊢ 𝐸 = (𝑞 ∈ (2o ↑𝑚 ℕ∞) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o, 1o, ∅)))    ⇒   ⊢ ℕ∞ ∈ Omni
Theorem	nninfomni 15643	ℕ∞ is omniscient. Corollary 3.7 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 10-Aug-2022.)
⊢ ℕ∞ ∈ Omni
Theorem	nninffeq 15644*	Equality of two functions on ℕ∞ which agree at every integer and at the point at infinity. From an online post by Martin Escardo. Remark: the last two hypotheses can be grouped into one, ⊢ (𝜑 → ∀𝑛 ∈ suc ω...). (Contributed by Jim Kingdon, 4-Aug-2023.)
⊢ (𝜑 → 𝐹:ℕ∞⟶ℕ0)    &   ⊢ (𝜑 → 𝐺:ℕ∞⟶ℕ0)    &   ⊢ (𝜑 → (𝐹‘(𝑥 ∈ ω ↦ 1o)) = (𝐺‘(𝑥 ∈ ω ↦ 1o)))    &   ⊢ (𝜑 → ∀𝑛 ∈ ω (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	nnnninfen 15645	Equinumerosity of the natural numbers and ℕ∞ is equivalent to the Limited Principle of Omniscience (LPO). Remark in Section 1.1 of [Pradic2025], p. 2. (Contributed by Jim Kingdon, 8-Jul-2025.)
⊢ (ω ≈ ℕ∞ ↔ ω ∈ Omni)
13.3.5  Schroeder-Bernstein Theorem
Theorem	exmidsbthrlem 15646*	Lemma for exmidsbthr 15647. (Contributed by Jim Kingdon, 11-Aug-2022.)
⊢ 𝑆 = (𝑝 ∈ ℕ∞ ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖))))    ⇒   ⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → EXMID)
Theorem	exmidsbthr 15647*	The Schroeder-Bernstein Theorem implies excluded middle. Theorem 1 of [PradicBrown2022], p. 1. (Contributed by Jim Kingdon, 11-Aug-2022.)
⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → EXMID)
Theorem	exmidsbth 15648*	The Schroeder-Bernstein Theorem is equivalent to excluded middle. This is Metamath 100 proof #25. The forward direction (isbth 7033) is the proof of the Schroeder-Bernstein Theorem from the Metamath Proof Explorer database (in which excluded middle holds), but adapted to use EXMID as an antecedent rather than being unconditionally true, as in the non-intuitionistic proof at https://us.metamath.org/mpeuni/sbth.html 7033. The reverse direction (exmidsbthr 15647) is the one which establishes that Schroeder-Bernstein implies excluded middle. This resolves the question of whether we will be able to prove Schroeder-Bernstein from our axioms in the negative. (Contributed by Jim Kingdon, 13-Aug-2022.)
⊢ (EXMID ↔ ∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦))
Theorem	sbthomlem 15649	Lemma for sbthom 15650. (Contributed by Mario Carneiro and Jim Kingdon, 13-Jul-2023.)
⊢ (𝜑 → ω ∈ Omni)    &   ⊢ (𝜑 → 𝑌 ⊆ {∅})    &   ⊢ (𝜑 → 𝐹:ω–1-1-onto→(𝑌 ⊔ ω))    ⇒   ⊢ (𝜑 → (𝑌 = ∅ ∨ 𝑌 = {∅}))
Theorem	sbthom 15650	Schroeder-Bernstein is not possible even for ω. We know by exmidsbth 15648 that full Schroeder-Bernstein will not be provable but what about the case where one of the sets is ω? That case plus the Limited Principle of Omniscience (LPO) implies excluded middle, so we will not be able to prove it. (Contributed by Mario Carneiro and Jim Kingdon, 10-Jul-2023.)
⊢ ((∀𝑥((𝑥 ≼ ω ∧ ω ≼ 𝑥) → 𝑥 ≈ ω) ∧ ω ∈ Omni) → EXMID)
13.3.6  Real and complex numbers
Theorem	qdencn 15651*	The set of complex numbers whose real and imaginary parts are rational is dense in the complex plane. This is a two dimensional analogue to qdenre 11355 (and also would hold for ℝ × ℝ with the usual metric; this is not about complex numbers in particular). (Contributed by Jim Kingdon, 18-Oct-2021.)
⊢ 𝑄 = {𝑧 ∈ ℂ ∣ ((ℜ‘𝑧) ∈ ℚ ∧ (ℑ‘𝑧) ∈ ℚ)}    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+) → ∃𝑥 ∈ 𝑄 (abs‘(𝑥 − 𝐴)) < 𝐵)
Theorem	refeq 15652*	Equality of two real functions which agree at negative numbers, positive numbers, and zero. This holds even without real trichotomy. From an online post by Martin Escardo. (Contributed by Jim Kingdon, 9-Jul-2023.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝐺:ℝ⟶ℝ)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑥 < 0 → (𝐹‘𝑥) = (𝐺‘𝑥)))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ (0 < 𝑥 → (𝐹‘𝑥) = (𝐺‘𝑥)))    &   ⊢ (𝜑 → (𝐹‘0) = (𝐺‘0))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	triap 15653	Two ways of stating real number trichotomy. (Contributed by Jim Kingdon, 23-Aug-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴) ↔ DECID 𝐴 # 𝐵))
Theorem	isomninnlem 15654*	Lemma for isomninn 15655. The result, with a hypothesis to provide a convenient notation. (Contributed by Jim Kingdon, 30-Aug-2023.)
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)))
Theorem	isomninn 15655*	Omniscience stated in terms of natural numbers. Similar to isomnimap 7203 but it will sometimes be more convenient to use 0 and 1 rather than ∅ and 1o. (Contributed by Jim Kingdon, 30-Aug-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)))
Theorem	cvgcmp2nlemabs 15656*	Lemma for cvgcmp2n 15657. The partial sums get closer to each other as we go further out. The proof proceeds by rewriting (seq1( + , 𝐺)‘𝑁) as the sum of (seq1( + , 𝐺)‘𝑀) and a term which gets smaller as 𝑀 gets large. (Contributed by Jim Kingdon, 25-Aug-2023.)
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐺‘𝑘))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ≤ (1 / (2↑𝑘)))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (𝜑 → (abs‘((seq1( + , 𝐺)‘𝑁) − (seq1( + , 𝐺)‘𝑀))) < (2 / 𝑀))
Theorem	cvgcmp2n 15657*	A comparison test for convergence of a real infinite series. (Contributed by Jim Kingdon, 25-Aug-2023.)
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐺‘𝑘))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ≤ (1 / (2↑𝑘)))    ⇒   ⊢ (𝜑 → seq1( + , 𝐺) ∈ dom ⇝ )
Theorem	iooref1o 15658	A one-to-one mapping from the real numbers onto the open unit interval. (Contributed by Jim Kingdon, 27-Jun-2024.)
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (1 / (1 + (exp‘𝑥))))    ⇒   ⊢ 𝐹:ℝ–1-1-onto→(0(,)1)
Theorem	iooreen 15659	An open interval is equinumerous to the real numbers. (Contributed by Jim Kingdon, 27-Jun-2024.)
⊢ (0(,)1) ≈ ℝ
13.3.7  Analytic omniscience principles Omniscience principles refer to several propositions, most of them weaker than full excluded middle, which do not follow from the axioms of IZF set theory. They are: (0) the Principle of Omniscience (PO), which is another name for excluded middle (see exmidomni 7208), (1) the Limited Principle of Omniscience (LPO) is ω ∈ Omni (see df-omni 7201), (2) the Weak Limited Principle of Omniscience (WLPO) is ω ∈ WOmni (see df-womni 7230), (3) Markov's Principle (MP) is ω ∈ Markov (see df-markov 7218), (4) the Lesser Limited Principle of Omniscience (LLPO) is not yet defined in iset.mm. They also have analytic counterparts each of which follows from the corresponding omniscience principle: (1) Analytic LPO is real number trichotomy, ∀𝑥 ∈ ℝ∀𝑦 ∈ ℝ(𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) (see trilpo 15667), (2) Analytic WLPO is decidability of real number equality, ∀𝑥 ∈ ℝ∀𝑦 ∈ ℝDECID 𝑥 = 𝑦 (see redcwlpo 15679), (3) Analytic MP is ∀𝑥 ∈ ℝ∀𝑦 ∈ ℝ(𝑥 ≠ 𝑦 → 𝑥 # 𝑦) (see neapmkv 15692), (4) Analytic LLPO is real number dichotomy, ∀𝑥 ∈ ℝ∀𝑦 ∈ ℝ(𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥) (most relevant current theorem is maxclpr 11375).
Theorem	trilpolemclim 15660*	Lemma for trilpo 15667. Convergence of the series. (Contributed by Jim Kingdon, 24-Aug-2023.)
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))    ⇒   ⊢ (𝜑 → seq1( + , 𝐺) ∈ dom ⇝ )
Theorem	trilpolemcl 15661*	Lemma for trilpo 15667. The sum exists. (Contributed by Jim Kingdon, 23-Aug-2023.)
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖))    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	trilpolemisumle 15662*	Lemma for trilpo 15667. An upper bound for the sum of the digits beyond a certain point. (Contributed by Jim Kingdon, 28-Aug-2023.)
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖))    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    ⇒   ⊢ (𝜑 → Σ𝑖 ∈ 𝑍 ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ Σ𝑖 ∈ 𝑍 (1 / (2↑𝑖)))
Theorem	trilpolemgt1 15663*	Lemma for trilpo 15667. The 1 < 𝐴 case. (Contributed by Jim Kingdon, 23-Aug-2023.)
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖))    ⇒   ⊢ (𝜑 → ¬ 1 < 𝐴)
Theorem	trilpolemeq1 15664*	Lemma for trilpo 15667. The 𝐴 = 1 case. This is proved by noting that if any (𝐹‘𝑥) is zero, then the infinite sum 𝐴 is less than one based on the term which is zero. We are using the fact that the 𝐹 sequence is decidable (in the sense that each element is either zero or one). (Contributed by Jim Kingdon, 23-Aug-2023.)
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖))    &   ⊢ (𝜑 → 𝐴 = 1)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ ℕ (𝐹‘𝑥) = 1)
Theorem	trilpolemlt1 15665*	Lemma for trilpo 15667. The 𝐴 < 1 case. We can use the distance between 𝐴 and one (that is, 1 − 𝐴) to find a position in the sequence 𝑛 where terms after that point will not add up to as much as 1 − 𝐴. By finomni 7206 we know the terms up to 𝑛 either contain a zero or are all one. But if they are all one that contradicts the way we constructed 𝑛, so we know that the sequence contains a zero. (Contributed by Jim Kingdon, 23-Aug-2023.)
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖))    &   ⊢ (𝜑 → 𝐴 < 1)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0)
Theorem	trilpolemres 15666*	Lemma for trilpo 15667. The result. (Contributed by Jim Kingdon, 23-Aug-2023.)
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖))    &   ⊢ (𝜑 → (𝐴 < 1 ∨ 𝐴 = 1 ∨ 1 < 𝐴))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0 ∨ ∀𝑥 ∈ ℕ (𝐹‘𝑥) = 1))
Theorem	trilpo 15667*	Real number trichotomy implies the Limited Principle of Omniscience (LPO). We expect that we'd need some form of countable choice to prove the converse. Here's the outline of the proof. Given an infinite sequence F of zeroes and ones, we need to show the sequence contains a zero or it is all ones. Construct a real number A whose representation in base two consists of a zero, a decimal point, and then the numbers of the sequence. Compare it with one using trichotomy. The three cases from trichotomy are trilpolemlt1 15665 (which means the sequence contains a zero), trilpolemeq1 15664 (which means the sequence is all ones), and trilpolemgt1 15663 (which is not possible). Equivalent ways to state real number trichotomy (sometimes called "analytic LPO") include decidability of real number apartness (see triap 15653) or that the real numbers are a discrete field (see trirec0 15668). LPO is known to not be provable in IZF (and most constructive foundations), so this theorem establishes that we will be unable to prove an analogue to qtri3or 10319 for real numbers. (Contributed by Jim Kingdon, 23-Aug-2023.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) → ω ∈ Omni)
Theorem	trirec0 15668*	Every real number having a reciprocal or equaling zero is equivalent to real number trichotomy. This is the key part of the definition of what is known as a discrete field, so "the real numbers are a discrete field" can be taken as an equivalent way to state real trichotomy (see further discussion at trilpo 15667). (Contributed by Jim Kingdon, 10-Jun-2024.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) ↔ ∀𝑥 ∈ ℝ (∃𝑧 ∈ ℝ (𝑥 · 𝑧) = 1 ∨ 𝑥 = 0))
Theorem	trirec0xor 15669*	Version of trirec0 15668 with exclusive-or. The definition of a discrete field is sometimes stated in terms of exclusive-or but as proved here, this is equivalent to inclusive-or because the two disjuncts cannot be simultaneously true. (Contributed by Jim Kingdon, 10-Jun-2024.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) ↔ ∀𝑥 ∈ ℝ (∃𝑧 ∈ ℝ (𝑥 · 𝑧) = 1 ⊻ 𝑥 = 0))
Theorem	apdifflemf 15670	Lemma for apdiff 15672. Being apart from the point halfway between 𝑄 and 𝑅 suffices for 𝐴 to be a different distance from 𝑄 and from 𝑅. (Contributed by Jim Kingdon, 18-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑄 ∈ ℚ)    &   ⊢ (𝜑 → 𝑅 ∈ ℚ)    &   ⊢ (𝜑 → 𝑄 < 𝑅)    &   ⊢ (𝜑 → ((𝑄 + 𝑅) / 2) # 𝐴)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) # (abs‘(𝐴 − 𝑅)))
Theorem	apdifflemr 15671	Lemma for apdiff 15672. (Contributed by Jim Kingdon, 19-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑆 ∈ ℚ)    &   ⊢ (𝜑 → (abs‘(𝐴 − -1)) # (abs‘(𝐴 − 1)))    &   ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (abs‘(𝐴 − 0)) # (abs‘(𝐴 − (2 · 𝑆))))    ⇒   ⊢ (𝜑 → 𝐴 # 𝑆)
Theorem	apdiff 15672*	The irrationals (reals apart from any rational) are exactly those reals that are a different distance from every rational. (Contributed by Jim Kingdon, 17-May-2024.)
⊢ (𝐴 ∈ ℝ → (∀𝑞 ∈ ℚ 𝐴 # 𝑞 ↔ ∀𝑞 ∈ ℚ ∀𝑟 ∈ ℚ (𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))))
Theorem	iswomninnlem 15673*	Lemma for iswomnimap 7232. The result, with a hypothesis for convenience. (Contributed by Jim Kingdon, 20-Jun-2024.)
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))
Theorem	iswomninn 15674*	Weak omniscience stated in terms of natural numbers. Similar to iswomnimap 7232 but it will sometimes be more convenient to use 0 and 1 rather than ∅ and 1o. (Contributed by Jim Kingdon, 20-Jun-2024.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))
Theorem	iswomni0 15675*	Weak omniscience stated in terms of equality with 0. Like iswomninn 15674 but with zero in place of one. (Contributed by Jim Kingdon, 24-Jul-2024.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
Theorem	ismkvnnlem 15676*	Lemma for ismkvnn 15677. The result, with a hypothesis to give a name to an expression for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.)
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)))
Theorem	ismkvnn 15677*	The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 25-Jun-2024.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)))
Theorem	redcwlpolemeq1 15678*	Lemma for redcwlpo 15679. A biconditionalized version of trilpolemeq1 15664. (Contributed by Jim Kingdon, 21-Jun-2024.)
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖))    ⇒   ⊢ (𝜑 → (𝐴 = 1 ↔ ∀𝑥 ∈ ℕ (𝐹‘𝑥) = 1))
Theorem	redcwlpo 15679*	Decidability of real number equality implies the Weak Limited Principle of Omniscience (WLPO). We expect that we'd need some form of countable choice to prove the converse. Here's the outline of the proof. Given an infinite sequence F of zeroes and ones, we need to show the sequence is all ones or it is not. Construct a real number A whose representation in base two consists of a zero, a decimal point, and then the numbers of the sequence. This real number will equal one if and only if the sequence is all ones (redcwlpolemeq1 15678). Therefore decidability of real number equality would imply decidability of whether the sequence is all ones. Because of this theorem, decidability of real number equality is sometimes called "analytic WLPO". WLPO is known to not be provable in IZF (and most constructive foundations), so this theorem establishes that we will be unable to prove an analogue to qdceq 10323 for real numbers. (Contributed by Jim Kingdon, 20-Jun-2024.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ DECID 𝑥 = 𝑦 → ω ∈ WOmni)
Theorem	tridceq 15680*	Real trichotomy implies decidability of real number equality. Or in other words, analytic LPO implies analytic WLPO (see trilpo 15667 and redcwlpo 15679). Thus, this is an analytic analogue to lpowlpo 7234. (Contributed by Jim Kingdon, 24-Jul-2024.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) → ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ DECID 𝑥 = 𝑦)
Theorem	redc0 15681*	Two ways to express decidability of real number equality. (Contributed by Jim Kingdon, 23-Jul-2024.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ DECID 𝑥 = 𝑦 ↔ ∀𝑧 ∈ ℝ DECID 𝑧 = 0)
Theorem	reap0 15682*	Real number trichotomy is equivalent to decidability of apartness from zero. (Contributed by Jim Kingdon, 27-Jul-2024.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) ↔ ∀𝑧 ∈ ℝ DECID 𝑧 # 0)
Theorem	cndcap 15683*	Real number trichotomy is equivalent to decidability of complex number apartness. (Contributed by Jim Kingdon, 10-Apr-2025.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) ↔ ∀𝑧 ∈ ℂ ∀𝑤 ∈ ℂ DECID 𝑧 # 𝑤)
Theorem	dceqnconst 15684*	Decidability of real number equality implies the existence of a certain non-constant function from real numbers to integers. Variation of Exercise 11.6(i) of [HoTT], p. (varies). See redcwlpo 15679 for more discussion of decidability of real number equality. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.) (Revised by Jim Kingdon, 23-Jul-2024.)
⊢ (∀𝑥 ∈ ℝ DECID 𝑥 = 0 → ∃𝑓(𝑓:ℝ⟶ℤ ∧ (𝑓‘0) = 0 ∧ ∀𝑥 ∈ ℝ+ (𝑓‘𝑥) ≠ 0))
Theorem	dcapnconst 15685*	Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. Variation of Exercise 11.6(i) of [HoTT], p. (varies). See trilpo 15667 for more discussion of decidability of real number apartness. This is a weaker form of dceqnconst 15684 and in fact this theorem can be proved using dceqnconst 15684 as shown at dcapnconstALT 15686. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.)
⊢ (∀𝑥 ∈ ℝ DECID 𝑥 # 0 → ∃𝑓(𝑓:ℝ⟶ℤ ∧ (𝑓‘0) = 0 ∧ ∀𝑥 ∈ ℝ+ (𝑓‘𝑥) ≠ 0))
Theorem	dcapnconstALT 15686*	Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. A proof of dcapnconst 15685 by means of dceqnconst 15684. (Contributed by Jim Kingdon, 27-Jul-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (∀𝑥 ∈ ℝ DECID 𝑥 # 0 → ∃𝑓(𝑓:ℝ⟶ℤ ∧ (𝑓‘0) = 0 ∧ ∀𝑥 ∈ ℝ+ (𝑓‘𝑥) ≠ 0))
Theorem	nconstwlpolem0 15687*	Lemma for nconstwlpo 15690. If all the terms of the series are zero, so is their sum. (Contributed by Jim Kingdon, 26-Jul-2024.)
⊢ (𝜑 → 𝐺:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐺‘𝑖))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ (𝐺‘𝑥) = 0)    ⇒   ⊢ (𝜑 → 𝐴 = 0)
Theorem	nconstwlpolemgt0 15688*	Lemma for nconstwlpo 15690. If one of the terms of series is positive, so is the sum. (Contributed by Jim Kingdon, 26-Jul-2024.)
⊢ (𝜑 → 𝐺:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐺‘𝑖))    &   ⊢ (𝜑 → ∃𝑥 ∈ ℕ (𝐺‘𝑥) = 1)    ⇒   ⊢ (𝜑 → 0 < 𝐴)
Theorem	nconstwlpolem 15689*	Lemma for nconstwlpo 15690. (Contributed by Jim Kingdon, 23-Jul-2024.)
⊢ (𝜑 → 𝐹:ℝ⟶ℤ)    &   ⊢ (𝜑 → (𝐹‘0) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝐹‘𝑥) ≠ 0)    &   ⊢ (𝜑 → 𝐺:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐺‘𝑖))    ⇒   ⊢ (𝜑 → (∀𝑦 ∈ ℕ (𝐺‘𝑦) = 0 ∨ ¬ ∀𝑦 ∈ ℕ (𝐺‘𝑦) = 0))
Theorem	nconstwlpo 15690*	Existence of a certain non-constant function from reals to integers implies ω ∈ WOmni (the Weak Limited Principle of Omniscience or WLPO). Based on Exercise 11.6(ii) of [HoTT], p. (varies). (Contributed by BJ and Jim Kingdon, 22-Jul-2024.)
⊢ (𝜑 → 𝐹:ℝ⟶ℤ)    &   ⊢ (𝜑 → (𝐹‘0) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝐹‘𝑥) ≠ 0)    ⇒   ⊢ (𝜑 → ω ∈ WOmni)
Theorem	neapmkvlem 15691*	Lemma for neapmkv 15692. The result, with a few hypotheses broken out for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.)
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖))    &   ⊢ ((𝜑 ∧ 𝐴 ≠ 1) → 𝐴 # 1)    ⇒   ⊢ (𝜑 → (¬ ∀𝑥 ∈ ℕ (𝐹‘𝑥) = 1 → ∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0))
Theorem	neapmkv 15692*	If negated equality for real numbers implies apartness, Markov's Principle follows. Exercise 11.10 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 24-Jun-2024.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 ≠ 𝑦 → 𝑥 # 𝑦) → ω ∈ Markov)
Theorem	neap0mkv 15693*	The analytic Markov principle can be expressed either with two arbitrary real numbers, or one arbitrary number and zero. (Contributed by Jim Kingdon, 23-Feb-2025.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 ≠ 𝑦 → 𝑥 # 𝑦) ↔ ∀𝑥 ∈ ℝ (𝑥 ≠ 0 → 𝑥 # 0))
Theorem	ltlenmkv 15694*	If < can be expressed as holding exactly when ≤ holds and the values are not equal, then the analytic Markov's Principle applies. (To get the regular Markov's Principle, combine with neapmkv 15692). (Contributed by Jim Kingdon, 23-Feb-2025.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ↔ (𝑥 ≤ 𝑦 ∧ 𝑦 ≠ 𝑥)) → ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 ≠ 𝑦 → 𝑥 # 𝑦))
13.3.8  Supremum and infimum
Theorem	supfz 15695	The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → sup((𝑀...𝑁), ℤ, < ) = 𝑁)
Theorem	inffz 15696	The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → inf((𝑀...𝑁), ℤ, < ) = 𝑀)
13.3.9  Circle constant
Theorem	taupi 15697	Relationship between τ and π. This can be seen as connecting the ratio of a circle's circumference to its radius and the ratio of a circle's circumference to its diameter. (Contributed by Jim Kingdon, 19-Feb-2019.) (Revised by AV, 1-Oct-2020.)
⊢ τ = (2 · π)
13.4  Mathbox for Mykola Mostovenko
Theorem	ax1hfs 15698	Heyting's formal system Axiom #1 from [Heyting] p. 127. (Contributed by MM, 11-Aug-2018.)
⊢ (𝜑 → (𝜑 ∧ 𝜑))
13.5  Mathbox for David A. Wheeler
13.5.1  Testable propositions
Theorem	dftest 15699	A proposition is testable iff its negative or double-negative is true. See Chapter 2 [Moschovakis] p. 2. We do not formally define testability with a new token, but instead use DECID ¬ before the formula in question. For example, DECID ¬ 𝑥 = 𝑦 corresponds to "𝑥 = 𝑦 is testable". (Contributed by David A. Wheeler, 13-Aug-2018.) For statements about testable propositions, search for the keyword "testable" in the comments of statements, for instance using the Metamath command "MM> SEARCH * "testable" / COMMENTS". (New usage is discouraged.)
⊢ (DECID ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑))
13.5.2  Allsome quantifier These are definitions and proofs involving an experimental "allsome" quantifier (aka "all some"). In informal language, statements like "All Martians are green" imply that there is at least one Martian. But it's easy to mistranslate informal language into formal notations because similar statements like ∀𝑥𝜑 → 𝜓 do not imply that 𝜑 is ever true, leading to vacuous truths. Some systems include a mechanism to counter this, e.g., PVS allows types to be appended with "+" to declare that they are nonempty. This section presents a different solution to the same problem. The "allsome" quantifier expressly includes the notion of both "all" and "there exists at least one" (aka some), and is defined to make it easier to more directly express both notions. The hope is that if a quantifier more directly expresses this concept, it will be used instead and reduce the risk of creating formal expressions that look okay but in fact are mistranslations. The term "allsome" was chosen because it's short, easy to say, and clearly hints at the two concepts it combines. I do not expect this to be used much in metamath, because in metamath there's a general policy of avoiding the use of new definitions unless there are very strong reasons to do so. Instead, my goal is to rigorously define this quantifier and demonstrate a few basic properties of it. The syntax allows two forms that look like they would be problematic, but they are fine. When applied to a top-level implication we allow ∀!𝑥(𝜑 → 𝜓), and when restricted (applied to a class) we allow ∀!𝑥 ∈ 𝐴𝜑. The first symbol after the setvar variable must always be ∈ if it is the form applied to a class, and since ∈ cannot begin a wff, it is unambiguous. The → looks like it would be a problem because 𝜑 or 𝜓 might include implications, but any implication arrow → within any wff must be surrounded by parentheses, so only the implication arrow of ∀! can follow the wff. The implication syntax would work fine without the parentheses, but I added the parentheses because it makes things clearer inside larger complex expressions, and it's also more consistent with the rest of the syntax. For more, see "The Allsome Quantifier" by David A. Wheeler at https://dwheeler.com/essays/allsome.html I hope that others will eventually agree that allsome is awesome.
Syntax	walsi 15700	Extend wff definition to include "all some" applied to a top-level implication, which means 𝜓 is true whenever 𝜑 is true, and there is at least least one 𝑥 where 𝜑 is true. (Contributed by David A. Wheeler, 20-Oct-2018.)
wff ∀!𝑥(𝜑 → 𝜓)