P. 171 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 17001-17100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	3dom 17001*	A set that dominates ordinal 3 has at least 3 different members. (Contributed by Jim Kingdon, 12-Feb-2026.)
|- ( 3o ~<_ A -> E. x e. A E. y e. A E. z e. A ( x =/= y /\ x =/= z /\ y =/= z ) )
Theorem	pw1ndom3lem 17002	Lemma for pw1ndom3 17003. (Contributed by Jim Kingdon, 14-Feb-2026.)
|- ( ph -> X e. ~P 1o )   &    |- ( ph -> Y e. ~P 1o )   &    |- ( ph -> Z e. ~P 1o )   &    |- ( ph -> X =/= Y )   &    |- ( ph -> X =/= Z )   &    |- ( ph -> Y =/= Z )   =>    |- ( ph -> X = (/) )
Theorem	pw1ndom3 17003	The powerset of 1o does not dominate 3o. This is another way of saying that ~P 1o does not have three elements (like pwntru 4334). (Contributed by Steven Nguyen and Jim Kingdon, 14-Feb-2026.)
|- -. 3o ~<_ ~P 1o
Theorem	pw1ninf 17004	The powerset of 1o is not infinite. Since we cannot prove it is finite (see pw1fin 7211), this provides a concrete example of a set which we cannot show to be finite or infinite, as seen another way at inffiexmid 7207. (Contributed by Jim Kingdon, 14-Feb-2026.)
|- -. om ~<_ ~P 1o
Theorem	nnti 17005	Ordering on a natural number generates a tight apartness. (Contributed by Jim Kingdon, 7-Aug-2022.)
|- ( ph -> A e. om )   =>    |- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u _E v /\ -. v _E u ) ) )
Theorem	012of 17006	Mapping zero and one between NN0 and om style integers. (Contributed by Jim Kingdon, 28-Jun-2024.)
|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   =>    |- ( `' G |` { 0 , 1 } ) : { 0 , 1 } --> 2o
Theorem	2o01f 17007	Mapping zero and one between om and NN0 style integers. (Contributed by Jim Kingdon, 28-Jun-2024.)
|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   =>    |- ( G |` 2o ) : 2o --> { 0 , 1 }
Theorem	pw1map 17008*	Mapping between ( ~P 1o ^m A ) and subsets of A. (Contributed by Jim Kingdon, 9-Jan-2026.)
|- F = ( s e. ( ~P 1o ^m A ) |-> { z e. A | ( s ` z ) = 1o } )   =>    |- ( A e. V -> F : ( ~P 1o ^m A ) -1-1-onto-> ~P A )
Theorem	pw1mapen 17009	Equinumerosity of ( ~P 1o ^m A ) and the set of subsets of A. (Contributed by Jim Kingdon, 10-Jan-2026.)
|- ( A e. V -> ( ~P 1o ^m A ) ~~ ~P A )
14.4.3  The power set of a singleton
Theorem	pwtrufal 17010	A subset of the singleton { (/) } cannot be anything other than (/) or { (/) }. Removing the double negation would change the meaning, as seen at exmid01 4333. If we view a subset of a singleton as a truth value (as seen in theorems like exmidexmid 4331), 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.)
|- ( A C_ { (/) } -> -. -. ( A = (/) \/ A = { (/) } ) )
Theorem	pwle2 17011*	An exercise related to N 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.)
|- T = U_ x e. N ( { x } X. 1o )   =>    |- ( ( N e. om /\ G : T -1-1-> ~P 1o ) -> N C_ 2o )
Theorem	pwf1oexmid 17012*	An exercise related to N 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.)
|- T = U_ x e. N ( { x } X. 1o )   =>    |- ( ( N e. om /\ G : T -1-1-> ~P 1o ) -> ( ran G = ~P 1o <-> ( N = 2o /\ EXMID ) ) )
Theorem	subctctexmid 17013*	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.)
|- ( ph -> A. x ( E. s ( s C_ om /\ E. f f : s -onto-> x ) -> E. g g : om -onto-> ( x ⊔ 1o ) ) )   &    |- ( ph -> om e. Markov )   =>    |- ( ph -> EXMID )
Theorem	domomsubct 17014*	A set dominated by om is subcountable. (Contributed by Jim Kingdon, 11-Nov-2025.)
|- ( A ~<_ om -> E. s ( s C_ om /\ E. f f : s -onto-> A ) )
Theorem	sssneq 17015*	Any two elements of a subset of a singleton are equal. (Contributed by Jim Kingdon, 28-May-2024.)
|- ( A C_ { B } -> A. y e. A A. z e. A y = z )
Theorem	pw1nct 17016*	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.)
|- ( A. r ( r C_ ( ~P 1o X. om ) -> ( A. p e. ~P 1o E. n e. om p r n -> E. m e. om A. q e. ~P 1o q r m ) ) -> -. E. f f : om -onto-> ( ~P 1o ⊔ 1o ) )
Theorem	pw1dceq 17017*	The powerset of 1o having decidable equality is equivalent to excluded middle. (Contributed by Jim Kingdon, 12-Feb-2026.)
|- (EXMID <-> A. x e. ~P 1o A. y e. ~P 1oDECID x = y )
Theorem	exmidnotnotr 17018	Excluded middle is equivalent to double negation elimination. Read an element of ~P 1o as being a truth value and x = 1o being that x is true. For a similar theorem, but expressed in terms of formulas rather than subsets of 1o, see dcfromnotnotr 1497. (Contributed by Jim Kingdon, 22-Apr-2026.)
|- (EXMID <-> A. x e. ~P 1o ( -. -. x = 1o -> x = 1o ) )
Theorem	exmidcon 17019*	Excluded middle is equivalent to the form of contraposition which removes negation. Read an element of ~P 1o as being a truth value and x = 1o being that x is true. For a similar theorem, but expressed in terms of formulas rather than subsets of 1o, see dcfromcon 1498. (Contributed by Jim Kingdon, 22-Apr-2026.)
|- (EXMID <-> A. x e. ~P 1o A. y e. ~P 1o ( ( -. y = 1o -> -. x = 1o ) -> ( x = 1o -> y = 1o ) ) )
Theorem	exmidpeirce 17020*	Excluded middle is equivalent to Peirce's law. Read an element of ~P 1o as being a truth value and x = 1o being that x is true. For a similar theorem, but expressed in terms of formulas rather than subsets of 1o, see dcfrompeirce 1499. (Contributed by Jim Kingdon, 23-Apr-2026.)
|- (EXMID <-> A. x e. ~P 1o A. y e. ~P 1o ( ( ( x = 1o -> y = 1o ) -> x = 1o ) -> x = 1o ) )
Theorem	stnot 17021*	A proposition is double negation stable if and only if it is equivalent to a negated proposition. Here by "proposition" we mean a subset of a singleton (which is a choice which allows us to quantify over them). Posed as an exercise online by Yannick Forster. (Contributed by Jim Kingdon, 24-Jul-2026.)
|- ( A e. ~P 1o -> ( ( -. -. A = 1o -> A = 1o ) <-> E. y e. ~P 1o ( A = 1o <-> -. y = 1o ) ) )
14.4.4  Omniscience of NN+oo
Theorem	0nninf 17022	The zero element of ℕ∞ (the constant sequence equal to (/)). (Contributed by Jim Kingdon, 14-Jul-2022.)
|- ( om X. { (/) } ) e. ℕ∞
Theorem	nnsf 17023*	Domain and range of S. Part of Definition 3.3 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 30-Jul-2022.)
|- S = ( p e. ℕ∞ |-> ( i e. om |-> if ( i = (/) , 1o , ( p ` U. i ) ) ) )   =>    |- S :ℕ∞ -->ℕ∞
Theorem	peano4nninf 17024*	The successor function on ℕ∞ is one to one. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 31-Jul-2022.)
|- S = ( p e. ℕ∞ |-> ( i e. om |-> if ( i = (/) , 1o , ( p ` U. i ) ) ) )   =>    |- S :ℕ∞ -1-1->ℕ∞
Theorem	peano3nninf 17025*	The successor function on ℕ∞ is never zero. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 1-Aug-2022.)
|- S = ( p e. ℕ∞ |-> ( i e. om |-> if ( i = (/) , 1o , ( p ` U. i ) ) ) )   =>    |- ( A e. ℕ∞ -> ( S ` A ) =/= ( x e. om |-> (/) ) )
Theorem	nninfalllem1 17026*	Lemma for nninfall 17027. (Contributed by Jim Kingdon, 1-Aug-2022.)
|- ( ph -> Q e. ( 2o ^m ℕ∞ ) )   &    |- ( ph -> ( Q ` ( x e. om |-> 1o ) ) = 1o )   &    |- ( ph -> A. n e. om ( Q ` ( i e. om |-> if ( i e. n , 1o , (/) ) ) ) = 1o )   &    |- ( ph -> P e. ℕ∞ )   &    |- ( ph -> ( Q ` P ) = (/) )   =>    |- ( ph -> A. n e. om ( P ` n ) = 1o )
Theorem	nninfall 17027*	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 Q 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.)
|- ( ph -> Q e. ( 2o ^m ℕ∞ ) )   &    |- ( ph -> ( Q ` ( x e. om |-> 1o ) ) = 1o )   &    |- ( ph -> A. n e. om ( Q ` ( i e. om |-> if ( i e. n , 1o , (/) ) ) ) = 1o )   =>    |- ( ph -> A. p e. ℕ∞ ( Q ` p ) = 1o )
Theorem	nninfsellemdc 17028*	Lemma for nninfself 17031. Showing that the selection function is well defined. (Contributed by Jim Kingdon, 8-Aug-2022.)
|- ( ( Q e. ( 2o ^m ℕ∞ ) /\ N e. om ) -> DECID A. k e. suc N ( Q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o )
Theorem	nninfsellemcl 17029*	Lemma for nninfself 17031. (Contributed by Jim Kingdon, 8-Aug-2022.)
|- ( ( Q e. ( 2o ^m ℕ∞ ) /\ N e. om ) -> if ( A. k e. suc N ( Q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o , 1o , (/) ) e. 2o )
Theorem	nninfsellemsuc 17030*	Lemma for nninfself 17031. (Contributed by Jim Kingdon, 6-Aug-2022.)
|- ( ( Q e. ( 2o ^m ℕ∞ ) /\ J e. om ) -> if ( A. k e. suc suc J ( Q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o , 1o , (/) ) C_ if ( A. k e. suc J ( Q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o , 1o , (/) ) )
Theorem	nninfself 17031*	Domain and range of the selection function for ℕ∞. (Contributed by Jim Kingdon, 6-Aug-2022.)
|- E = ( q e. ( 2o ^m ℕ∞ ) |-> ( n e. om |-> if ( A. k e. suc n ( q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o , 1o , (/) ) ) )   =>    |- E : ( 2o ^m ℕ∞ ) -->ℕ∞
Theorem	nninfsellemeq 17032*	Lemma for nninfsel 17035. (Contributed by Jim Kingdon, 9-Aug-2022.)
|- E = ( q e. ( 2o ^m ℕ∞ ) |-> ( n e. om |-> if ( A. k e. suc n ( q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o , 1o , (/) ) ) )   &    |- ( ph -> Q e. ( 2o ^m ℕ∞ ) )   &    |- ( ph -> ( Q ` ( E ` Q ) ) = 1o )   &    |- ( ph -> N e. om )   &    |- ( ph -> A. k e. N ( Q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o )   &    |- ( ph -> ( Q ` ( i e. om |-> if ( i e. N , 1o , (/) ) ) ) = (/) )   =>    |- ( ph -> ( E ` Q ) = ( i e. om |-> if ( i e. N , 1o , (/) ) ) )
Theorem	nninfsellemqall 17033*	Lemma for nninfsel 17035. (Contributed by Jim Kingdon, 9-Aug-2022.)
|- E = ( q e. ( 2o ^m ℕ∞ ) |-> ( n e. om |-> if ( A. k e. suc n ( q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o , 1o , (/) ) ) )   &    |- ( ph -> Q e. ( 2o ^m ℕ∞ ) )   &    |- ( ph -> ( Q ` ( E ` Q ) ) = 1o )   &    |- ( ph -> N e. om )   =>    |- ( ph -> ( Q ` ( i e. om |-> if ( i e. N , 1o , (/) ) ) ) = 1o )
Theorem	nninfsellemeqinf 17034*	Lemma for nninfsel 17035. (Contributed by Jim Kingdon, 9-Aug-2022.)
|- E = ( q e. ( 2o ^m ℕ∞ ) |-> ( n e. om |-> if ( A. k e. suc n ( q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o , 1o , (/) ) ) )   &    |- ( ph -> Q e. ( 2o ^m ℕ∞ ) )   &    |- ( ph -> ( Q ` ( E ` Q ) ) = 1o )   =>    |- ( ph -> ( E ` Q ) = ( i e. om |-> 1o ) )
Theorem	nninfsel 17035*	E is a selection function for ℕ∞. Theorem 3.6 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 9-Aug-2022.)
|- E = ( q e. ( 2o ^m ℕ∞ ) |-> ( n e. om |-> if ( A. k e. suc n ( q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o , 1o , (/) ) ) )   &    |- ( ph -> Q e. ( 2o ^m ℕ∞ ) )   &    |- ( ph -> ( Q ` ( E ` Q ) ) = 1o )   =>    |- ( ph -> A. p e. ℕ∞ ( Q ` p ) = 1o )
Theorem	nninfomnilem 17036*	Lemma for nninfomni 17037. (Contributed by Jim Kingdon, 10-Aug-2022.)
|- E = ( q e. ( 2o ^m ℕ∞ ) |-> ( n e. om |-> if ( A. k e. suc n ( q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o , 1o , (/) ) ) )   =>    |- ℕ∞ e. Omni
Theorem	nninfomni 17037	ℕ∞ is omniscient. Corollary 3.7 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 10-Aug-2022.)
|- ℕ∞ e. Omni
Theorem	nninffeq 17038*	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, |- ( ph -> A. n e. suc om ... ). (Contributed by Jim Kingdon, 4-Aug-2023.)
|- ( ph -> F :ℕ∞ --> NN0 )   &    |- ( ph -> G :ℕ∞ --> NN0 )   &    |- ( ph -> ( F ` ( x e. om |-> 1o ) ) = ( G ` ( x e. om |-> 1o ) ) )   &    |- ( ph -> A. n e. om ( F ` ( i e. om |-> if ( i e. n , 1o , (/) ) ) ) = ( G ` ( i e. om |-> if ( i e. n , 1o , (/) ) ) ) )   =>    |- ( ph -> F = G )
Theorem	nnnninfen 17039	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.)
|- ( om ~~ ℕ∞ <-> om e. Omni )
Theorem	nnnninfex 17040*	If an element of ℕ∞ has a value of zero somewhere, then it is the mapping of a natural number. (Contributed by Jim Kingdon, 4-Aug-2022.)
|- ( ph -> P e. ℕ∞ )   &    |- ( ph -> N e. om )   &    |- ( ph -> ( P ` N ) = (/) )   =>    |- ( ph -> E. n e. om P = ( i e. om |-> if ( i e. n , 1o , (/) ) ) )
Theorem	nninfnfiinf 17041*	An element of ℕ∞ which is not finite is infinite. (Contributed by Jim Kingdon, 30-Nov-2025.)
|- ( ( A e. ℕ∞ /\ -. E. n e. om A = ( i e. om |-> if ( i e. n , 1o , (/) ) ) ) -> A = ( i e. om |-> 1o ) )
14.4.5  Schroeder-Bernstein Theorem
Theorem	exmidsbthrlem 17042*	Lemma for exmidsbthr 17043. (Contributed by Jim Kingdon, 11-Aug-2022.)
|- S = ( p e. ℕ∞ |-> ( i e. om |-> if ( i = (/) , 1o , ( p ` U. i ) ) ) )   =>    |- ( A. x A. y ( ( x ~<_ y /\ y ~<_ x ) -> x ~~ y ) -> EXMID )
Theorem	exmidsbthr 17043*	The Schroeder-Bernstein Theorem implies excluded middle. Theorem 1 of [PradicBrown2022], p. 1. (Contributed by Jim Kingdon, 11-Aug-2022.)
|- ( A. x A. y ( ( x ~<_ y /\ y ~<_ x ) -> x ~~ y ) -> EXMID )
Theorem	exmidsbth 17044*	The Schroeder-Bernstein Theorem is equivalent to excluded middle. This is Metamath 100 proof #25. The forward direction (isbth 7278) 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 7278. The reverse direction (exmidsbthr 17043) 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 <-> A. x A. y ( ( x ~<_ y /\ y ~<_ x ) -> x ~~ y ) )
Theorem	sbthomlem 17045	Lemma for sbthom 17046. (Contributed by Mario Carneiro and Jim Kingdon, 13-Jul-2023.)
|- ( ph -> om e. Omni )   &    |- ( ph -> Y C_ { (/) } )   &    |- ( ph -> F : om -1-1-onto-> ( Y ⊔ om ) )   =>    |- ( ph -> ( Y = (/) \/ Y = { (/) } ) )
Theorem	sbthom 17046	Schroeder-Bernstein is not possible even for om. We know by exmidsbth 17044 that full Schroeder-Bernstein will not be provable but what about the case where one of the sets is om? 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.)
|- ( ( A. x ( ( x ~<_ om /\ om ~<_ x ) -> x ~~ om ) /\ om e. Omni ) -> EXMID )
14.4.6  Real and complex numbers
Theorem	qdencn 17047*	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 11951 (and also would hold for RR X. RR with the usual metric; this is not about complex numbers in particular). (Contributed by Jim Kingdon, 18-Oct-2021.)
|- Q = { z e. CC | ( ( Re ` z ) e. QQ /\ ( Im ` z ) e. QQ ) }   =>    |- ( ( A e. CC /\ B e. RR+ ) -> E. x e. Q ( abs ` ( x - A ) ) < B )
Theorem	refeq 17048*	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.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> G : RR --> RR )   &    |- ( ph -> A. x e. RR ( x < 0 -> ( F ` x ) = ( G ` x ) ) )   &    |- ( ph -> A. x e. RR ( 0 < x -> ( F ` x ) = ( G ` x ) ) )   &    |- ( ph -> ( F ` 0 ) = ( G ` 0 ) )   =>    |- ( ph -> F = G )
Theorem	repiecelem 17049*	Lemma for repiecele0 17050, repiecege0 17051, and repiecef 17052. The function H is defined everywhere. (Contributed by Jim Kingdon, 27-Apr-2026.)
|- ( ph -> F : ( -oo (,] 0 ) --> RR )   &    |- ( ph -> G : ( 0 [,) +oo ) --> RR )   &    |- ( ph -> ( F ` 0 ) = ( G ` 0 ) )   &    |- H = ( x e. RR |-> ( ( ( F ` inf ( { x , 0 } , RR , < ) ) + ( G ` sup ( { x , 0 } , RR , < ) ) ) - ( F ` 0 ) ) )   =>    |- ( ( ph /\ A e. RR ) -> ( ( ( F ` inf ( { A , 0 } , RR , < ) ) + ( G ` sup ( { A , 0 } , RR , < ) ) ) - ( F ` 0 ) ) e. RR )
Theorem	repiecele0 17050*	Piecewise definition on the reals agrees with the nonpositive part of the definition. See repiecef 17052 for more on this construction. (Contributed by Jim Kingdon, 27-Apr-2026.)
|- ( ph -> F : ( -oo (,] 0 ) --> RR )   &    |- ( ph -> G : ( 0 [,) +oo ) --> RR )   &    |- ( ph -> ( F ` 0 ) = ( G ` 0 ) )   &    |- H = ( x e. RR |-> ( ( ( F ` inf ( { x , 0 } , RR , < ) ) + ( G ` sup ( { x , 0 } , RR , < ) ) ) - ( F ` 0 ) ) )   =>    |- ( ( ph /\ A e. RR /\ A <_ 0 ) -> ( H ` A ) = ( F ` A ) )
Theorem	repiecege0 17051*	Piecewise definition on the reals agrees with the nonnegative part of the definition. See repiecef 17052 for more on this construction. (Contributed by Jim Kingdon, 27-Apr-2026.)
|- ( ph -> F : ( -oo (,] 0 ) --> RR )   &    |- ( ph -> G : ( 0 [,) +oo ) --> RR )   &    |- ( ph -> ( F ` 0 ) = ( G ` 0 ) )   &    |- H = ( x e. RR |-> ( ( ( F ` inf ( { x , 0 } , RR , < ) ) + ( G ` sup ( { x , 0 } , RR , < ) ) ) - ( F ` 0 ) ) )   =>    |- ( ( ph /\ A e. RR /\ 0 <_ A ) -> ( H ` A ) = ( G ` A ) )
Theorem	repiecef 17052*	Piecewise definition on the reals yields a function. The function agrees with F and G on their respective parts of the real line; see repiecele0 17050 and repiecege0 17051. From an online post by James E Hanson. The construction was published in Martín Hötzel Escardó, "Effective and sequential definition by cases on the reals via infinite signed-digit numerals", Electronic Notes in Theoretical Computer Science 10 (1998), page 2, https://martinescardo.github.io/papers/lexnew.pdf. 17051 (Contributed by Jim Kingdon, 27-Apr-2026.)
|- ( ph -> F : ( -oo (,] 0 ) --> RR )   &    |- ( ph -> G : ( 0 [,) +oo ) --> RR )   &    |- ( ph -> ( F ` 0 ) = ( G ` 0 ) )   &    |- H = ( x e. RR |-> ( ( ( F ` inf ( { x , 0 } , RR , < ) ) + ( G ` sup ( { x , 0 } , RR , < ) ) ) - ( F ` 0 ) ) )   =>    |- ( ph -> H : RR --> RR )
Theorem	triap 17053	Two ways of stating real number trichotomy. See also cndcap 17084 which is similar but for complex number apartness. (Contributed by Jim Kingdon, 23-Aug-2023.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( A < B \/ A = B \/ B < A ) <-> DECID A # B ) )
Theorem	isomninnlem 17054*	Lemma for isomninn 17055. The result, with a hypothesis to provide a convenient notation. (Contributed by Jim Kingdon, 30-Aug-2023.)
|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   =>    |- ( A e. V -> ( A e. Omni <-> A. f e. ( { 0 , 1 } ^m A ) ( E. x e. A ( f ` x ) = 0 \/ A. x e. A ( f ` x ) = 1 ) ) )
Theorem	isomninn 17055*	Omniscience stated in terms of natural numbers. Similar to isomnimap 7471 but it will sometimes be more convenient to use 0 and 1 rather than (/) and 1o. (Contributed by Jim Kingdon, 30-Aug-2023.)
|- ( A e. V -> ( A e. Omni <-> A. f e. ( { 0 , 1 } ^m A ) ( E. x e. A ( f ` x ) = 0 \/ A. x e. A ( f ` x ) = 1 ) ) )
Theorem	cvgcmp2nlemabs 17056*	Lemma for cvgcmp2n 17057. The partial sums get closer to each other as we go further out. The proof proceeds by rewriting ( seq 1 ( + , G ) ` N ) as the sum of ( seq 1 ( + , G ) ` M ) and a term which gets smaller as M gets large. (Contributed by Jim Kingdon, 25-Aug-2023.)
|- ( ( ph /\ k e. NN ) -> ( G ` k ) e. RR )   &    |- ( ( ph /\ k e. NN ) -> 0 <_ ( G ` k ) )   &    |- ( ( ph /\ k e. NN ) -> ( G ` k ) <_ ( 1 / ( 2 ^ k ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   =>    |- ( ph -> ( abs ` ( ( seq 1 ( + , G ) ` N ) - ( seq 1 ( + , G ) ` M ) ) ) < ( 2 / M ) )
Theorem	cvgcmp2n 17057*	A comparison test for convergence of a real infinite series. (Contributed by Jim Kingdon, 25-Aug-2023.)
|- ( ( ph /\ k e. NN ) -> ( G ` k ) e. RR )   &    |- ( ( ph /\ k e. NN ) -> 0 <_ ( G ` k ) )   &    |- ( ( ph /\ k e. NN ) -> ( G ` k ) <_ ( 1 / ( 2 ^ k ) ) )   =>    |- ( ph -> seq 1 ( + , G ) e. dom ~~> )
Theorem	iooref1o 17058	A one-to-one mapping from the real numbers onto the open unit interval. (Contributed by Jim Kingdon, 27-Jun-2024.)
|- F = ( x e. RR |-> ( 1 / ( 1 + ( exp ` x ) ) ) )   =>    |- F : RR -1-1-onto-> ( 0 (,) 1 )
Theorem	iooreen 17059	An open interval is equinumerous to the real numbers. (Contributed by Jim Kingdon, 27-Jun-2024.)
|- ( 0 (,) 1 ) ~~ RR
14.4.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 7476), (1) the Limited Principle of Omniscience (LPO) is om e. Omni (see df-omni 7469), (2) the Weak Limited Principle of Omniscience (WLPO) is om e. WOmni (see df-womni 7498), (3) Markov's Principle (MP) is om e. Markov (see df-markov 7486), (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, A. x e. RR A. y e. RR ( x < y \/ x = y \/ y < x ) (see trilpo 17067), (2) Analytic WLPO is decidability of real number equality, A. x e. RR A. y e. RRDECID x = y (see redcwlpo 17080), (3) Analytic MP is A. x e. RR A. y e. RR ( x =/= y -> x # y ) (see neapmkv 17093), (4) Analytic LLPO is real number dichotomy, A. x e. RR A. y e. RR ( x <_ y \/ y <_ x ) (most relevant current theorem is maxclpr 11971).
Theorem	trilpolemclim 17060*	Lemma for trilpo 17067. Convergence of the series. (Contributed by Jim Kingdon, 24-Aug-2023.)
|- ( ph -> F : NN --> { 0 , 1 } )   &    |- G = ( n e. NN |-> ( ( 1 / ( 2 ^ n ) ) x. ( F ` n ) ) )   =>    |- ( ph -> seq 1 ( + , G ) e. dom ~~> )
Theorem	trilpolemcl 17061*	Lemma for trilpo 17067. The sum exists. (Contributed by Jim Kingdon, 23-Aug-2023.)
|- ( ph -> F : NN --> { 0 , 1 } )   &    |- A = sum_ i e. NN ( ( 1 / ( 2 ^ i ) ) x. ( F ` i ) )   =>    |- ( ph -> A e. RR )
Theorem	trilpolemisumle 17062*	Lemma for trilpo 17067. An upper bound for the sum of the digits beyond a certain point. (Contributed by Jim Kingdon, 28-Aug-2023.)
|- ( ph -> F : NN --> { 0 , 1 } )   &    |- A = sum_ i e. NN ( ( 1 / ( 2 ^ i ) ) x. ( F ` i ) )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. NN )   =>    |- ( ph -> sum_ i e. Z ( ( 1 / ( 2 ^ i ) ) x. ( F ` i ) ) <_ sum_ i e. Z ( 1 / ( 2 ^ i ) ) )
Theorem	trilpolemgt1 17063*	Lemma for trilpo 17067. The 1 < A case. (Contributed by Jim Kingdon, 23-Aug-2023.)
|- ( ph -> F : NN --> { 0 , 1 } )   &    |- A = sum_ i e. NN ( ( 1 / ( 2 ^ i ) ) x. ( F ` i ) )   =>    |- ( ph -> -. 1 < A )
Theorem	trilpolemeq1 17064*	Lemma for trilpo 17067. The A = 1 case. This is proved by noting that if any ( F ` x ) is zero, then the infinite sum A is less than one based on the term which is zero. We are using the fact that the F sequence is decidable (in the sense that each element is either zero or one). (Contributed by Jim Kingdon, 23-Aug-2023.)
|- ( ph -> F : NN --> { 0 , 1 } )   &    |- A = sum_ i e. NN ( ( 1 / ( 2 ^ i ) ) x. ( F ` i ) )   &    |- ( ph -> A = 1 )   =>    |- ( ph -> A. x e. NN ( F ` x ) = 1 )
Theorem	trilpolemlt1 17065*	Lemma for trilpo 17067. The A < 1 case. We can use the distance between A and one (that is, 1 - A) to find a position in the sequence n where terms after that point will not add up to as much as 1 - A. By finomni 7474 we know the terms up to n either contain a zero or are all one. But if they are all one that contradicts the way we constructed n, so we know that the sequence contains a zero. (Contributed by Jim Kingdon, 23-Aug-2023.)
|- ( ph -> F : NN --> { 0 , 1 } )   &    |- A = sum_ i e. NN ( ( 1 / ( 2 ^ i ) ) x. ( F ` i ) )   &    |- ( ph -> A < 1 )   =>    |- ( ph -> E. x e. NN ( F ` x ) = 0 )
Theorem	trilpolemres 17066*	Lemma for trilpo 17067. The result. (Contributed by Jim Kingdon, 23-Aug-2023.)
|- ( ph -> F : NN --> { 0 , 1 } )   &    |- A = sum_ i e. NN ( ( 1 / ( 2 ^ i ) ) x. ( F ` i ) )   &    |- ( ph -> ( A < 1 \/ A = 1 \/ 1 < A ) )   =>    |- ( ph -> ( E. x e. NN ( F ` x ) = 0 \/ A. x e. NN ( F ` x ) = 1 ) )
Theorem	trilpo 17067*	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 17065 (which means the sequence contains a zero), trilpolemeq1 17064 (which means the sequence is all ones), and trilpolemgt1 17063 (which is not possible). Equivalent ways to state real number trichotomy (sometimes called "analytic LPO") include decidability of real number apartness (see triap 17053) or that the real numbers are a discrete field (see trirec0 17068). 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 10658 for real numbers. (Contributed by Jim Kingdon, 23-Aug-2023.)
|- ( A. x e. RR A. y e. RR ( x < y \/ x = y \/ y < x ) -> om e. Omni )
Theorem	trirec0 17068*	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 17067). (Contributed by Jim Kingdon, 10-Jun-2024.)
|- ( A. x e. RR A. y e. RR ( x < y \/ x = y \/ y < x ) <-> A. x e. RR ( E. z e. RR ( x x. z ) = 1 \/ x = 0 ) )
Theorem	trirec0xor 17069*	Version of trirec0 17068 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.)
|- ( A. x e. RR A. y e. RR ( x < y \/ x = y \/ y < x ) <-> A. x e. RR ( E. z e. RR ( x x. z ) = 1 \/_ x = 0 ) )
Theorem	apdifflemf 17070	Lemma for apdiff 17072. Being apart from the point halfway between Q and R suffices for A to be a different distance from Q and from R. (Contributed by Jim Kingdon, 18-May-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> Q e. QQ )   &    |- ( ph -> R e. QQ )   &    |- ( ph -> Q < R )   &    |- ( ph -> ( ( Q + R ) / 2 ) # A )   =>    |- ( ph -> ( abs ` ( A - Q ) ) # ( abs ` ( A - R ) ) )
Theorem	apdifflemr 17071	Lemma for apdiff 17072. (Contributed by Jim Kingdon, 19-May-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> S e. QQ )   &    |- ( ph -> ( abs ` ( A - -u 1 ) ) # ( abs ` ( A - 1 ) ) )   &    |- ( ( ph /\ S =/= 0 ) -> ( abs ` ( A - 0 ) ) # ( abs ` ( A - ( 2 x. S ) ) ) )   =>    |- ( ph -> A # S )
Theorem	apdiff 17072*	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.)
|- ( A e. RR -> ( A. q e. QQ A # q <-> A. q e. QQ A. r e. QQ ( q =/= r -> ( abs ` ( A - q ) ) # ( abs ` ( A - r ) ) ) ) )
Theorem	qdiff 17073*	The rationals are exactly those reals for which there exist two distinct rationals that are the same distance from the original number. Similar to apdiff 17072 but by stating the result positively we can completely sidestep the issue of not equal versus apart in the statement of the result. From an online post by Ingo Blechschmidt. (Contributed by Jim Kingdon, 24-Apr-2026.)
|- ( A e. RR -> ( A e. QQ <-> E. q e. QQ E. r e. QQ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) )
Theorem	iswomninnlem 17074*	Lemma for iswomnimap 7500. The result, with a hypothesis for convenience. (Contributed by Jim Kingdon, 20-Jun-2024.)
|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   =>    |- ( A e. V -> ( A e. WOmni <-> A. f e. ( { 0 , 1 } ^m A )DECID A. x e. A ( f ` x ) = 1 ) )
Theorem	iswomninn 17075*	Weak omniscience stated in terms of natural numbers. Similar to iswomnimap 7500 but it will sometimes be more convenient to use 0 and 1 rather than (/) and 1o. (Contributed by Jim Kingdon, 20-Jun-2024.)
|- ( A e. V -> ( A e. WOmni <-> A. f e. ( { 0 , 1 } ^m A )DECID A. x e. A ( f ` x ) = 1 ) )
Theorem	iswomni0 17076*	Weak omniscience stated in terms of equality with 0. Like iswomninn 17075 but with zero in place of one. (Contributed by Jim Kingdon, 24-Jul-2024.)
|- ( A e. V -> ( A e. WOmni <-> A. f e. ( { 0 , 1 } ^m A )DECID A. x e. A ( f ` x ) = 0 ) )
Theorem	ismkvnnlem 17077*	Lemma for ismkvnn 17078. The result, with a hypothesis to give a name to an expression for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.)
|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   =>    |- ( A e. V -> ( A e. Markov <-> A. f e. ( { 0 , 1 } ^m A ) ( -. A. x e. A ( f ` x ) = 1 -> E. x e. A ( f ` x ) = 0 ) ) )
Theorem	ismkvnn 17078*	The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 25-Jun-2024.)
|- ( A e. V -> ( A e. Markov <-> A. f e. ( { 0 , 1 } ^m A ) ( -. A. x e. A ( f ` x ) = 1 -> E. x e. A ( f ` x ) = 0 ) ) )
Theorem	redcwlpolemeq1 17079*	Lemma for redcwlpo 17080. A biconditionalized version of trilpolemeq1 17064. (Contributed by Jim Kingdon, 21-Jun-2024.)
|- ( ph -> F : NN --> { 0 , 1 } )   &    |- A = sum_ i e. NN ( ( 1 / ( 2 ^ i ) ) x. ( F ` i ) )   =>    |- ( ph -> ( A = 1 <-> A. x e. NN ( F ` x ) = 1 ) )
Theorem	redcwlpo 17080*	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 17079). 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 10662 for real numbers. (Contributed by Jim Kingdon, 20-Jun-2024.)
|- ( A. x e. RR A. y e. RR DECID x = y -> om e. WOmni )
Theorem	tridceq 17081*	Real trichotomy implies decidability of real number equality. Or in other words, analytic LPO implies analytic WLPO (see trilpo 17067 and redcwlpo 17080). Thus, this is an analytic analogue to lpowlpo 7502. (Contributed by Jim Kingdon, 24-Jul-2024.)
|- ( A. x e. RR A. y e. RR ( x < y \/ x = y \/ y < x ) -> A. x e. RR A. y e. RR DECID x = y )
Theorem	redc0 17082*	Two ways to express decidability of real number equality. (Contributed by Jim Kingdon, 23-Jul-2024.)
|- ( A. x e. RR A. y e. RR DECID x = y <-> A. z e. RR DECID z = 0 )
Theorem	reap0 17083*	Real number trichotomy is equivalent to decidability of apartness from zero. (Contributed by Jim Kingdon, 27-Jul-2024.)
|- ( A. x e. RR A. y e. RR ( x < y \/ x = y \/ y < x ) <-> A. z e. RR DECID z # 0 )
Theorem	cndcap 17084*	Real number trichotomy is equivalent to decidability of complex number apartness. (Contributed by Jim Kingdon, 10-Apr-2025.)
|- ( A. x e. RR A. y e. RR ( x < y \/ x = y \/ y < x ) <-> A. z e. CC A. w e. CC DECID z # w )
Theorem	dceqnconst 17085*	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 17080 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.)
|- ( A. x e. RR DECID x = 0 -> E. f ( f : RR --> ZZ /\ ( f ` 0 ) = 0 /\ A. x e. RR+ ( f ` x ) =/= 0 ) )
Theorem	dcapnconst 17086*	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 17067 for more discussion of decidability of real number apartness. This is a weaker form of dceqnconst 17085 and in fact this theorem can be proved using dceqnconst 17085 as shown at dcapnconstALT 17087. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.)
|- ( A. x e. RR DECID x # 0 -> E. f ( f : RR --> ZZ /\ ( f ` 0 ) = 0 /\ A. x e. RR+ ( f ` x ) =/= 0 ) )
Theorem	dcapnconstALT 17087*	Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. A proof of dcapnconst 17086 by means of dceqnconst 17085. (Contributed by Jim Kingdon, 27-Jul-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A. x e. RR DECID x # 0 -> E. f ( f : RR --> ZZ /\ ( f ` 0 ) = 0 /\ A. x e. RR+ ( f ` x ) =/= 0 ) )
Theorem	nconstwlpolem0 17088*	Lemma for nconstwlpo 17091. If all the terms of the series are zero, so is their sum. (Contributed by Jim Kingdon, 26-Jul-2024.)
|- ( ph -> G : NN --> { 0 , 1 } )   &    |- A = sum_ i e. NN ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) )   &    |- ( ph -> A. x e. NN ( G ` x ) = 0 )   =>    |- ( ph -> A = 0 )
Theorem	nconstwlpolemgt0 17089*	Lemma for nconstwlpo 17091. If one of the terms of series is positive, so is the sum. (Contributed by Jim Kingdon, 26-Jul-2024.)
|- ( ph -> G : NN --> { 0 , 1 } )   &    |- A = sum_ i e. NN ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) )   &    |- ( ph -> E. x e. NN ( G ` x ) = 1 )   =>    |- ( ph -> 0 < A )
Theorem	nconstwlpolem 17090*	Lemma for nconstwlpo 17091. (Contributed by Jim Kingdon, 23-Jul-2024.)
|- ( ph -> F : RR --> ZZ )   &    |- ( ph -> ( F ` 0 ) = 0 )   &    |- ( ( ph /\ x e. RR+ ) -> ( F ` x ) =/= 0 )   &    |- ( ph -> G : NN --> { 0 , 1 } )   &    |- A = sum_ i e. NN ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) )   =>    |- ( ph -> ( A. y e. NN ( G ` y ) = 0 \/ -. A. y e. NN ( G ` y ) = 0 ) )
Theorem	nconstwlpo 17091*	Existence of a certain non-constant function from reals to integers implies om e. 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.)
|- ( ph -> F : RR --> ZZ )   &    |- ( ph -> ( F ` 0 ) = 0 )   &    |- ( ( ph /\ x e. RR+ ) -> ( F ` x ) =/= 0 )   =>    |- ( ph -> om e. WOmni )
Theorem	neapmkvlem 17092*	Lemma for neapmkv 17093. The result, with a few hypotheses broken out for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.)
|- ( ph -> F : NN --> { 0 , 1 } )   &    |- A = sum_ i e. NN ( ( 1 / ( 2 ^ i ) ) x. ( F ` i ) )   &    |- ( ( ph /\ A =/= 1 ) -> A # 1 )   =>    |- ( ph -> ( -. A. x e. NN ( F ` x ) = 1 -> E. x e. NN ( F ` x ) = 0 ) )
Theorem	neapmkv 17093*	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.)
|- ( A. x e. RR A. y e. RR ( x =/= y -> x # y ) -> om e. Markov )
Theorem	neap0mkv 17094*	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.)
|- ( A. x e. RR A. y e. RR ( x =/= y -> x # y ) <-> A. x e. RR ( x =/= 0 -> x # 0 ) )
Theorem	ltlenmkv 17095*	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 17093). (Contributed by Jim Kingdon, 23-Feb-2025.)
|- ( A. x e. RR A. y e. RR ( x < y <-> ( x <_ y /\ y =/= x ) ) -> A. x e. RR A. y e. RR ( x =/= y -> x # y ) )
14.4.8  Supremum and infimum
Theorem	supfz 17096	The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.)
|- ( N e. ( ZZ>= ` M ) -> sup ( ( M ... N ) , ZZ , < ) = N )
Theorem	inffz 17097	The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.)
|- ( N e. ( ZZ>= ` M ) -> inf ( ( M ... N ) , ZZ , < ) = M )
14.4.9  Circle constant
Theorem	taupi 17098	Relationship between tau and pi. 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.)
|- tau = ( 2 x. pi )
14.5  Mathbox for Mykola Mostovenko
Theorem	ax1hfs 17099	Heyting's formal system Axiom #1 from [Heyting] p. 127. (Contributed by MM, 11-Aug-2018.)
|- ( ph -> ( ph /\ ph ) )
14.6  Mathbox for David A. Wheeler
14.6.1  Testable propositions
Theorem	dftest 17100	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 -. x = y corresponds to " x = y 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 -. ph <-> ( -. ph \/ -. -. ph ) )