P. 169 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16801-16872   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	repiecelem 16801*	Lemma for repiecele0 16802, repiecege0 16803, and repiecef 16804. 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 16802*	Piecewise definition on the reals agrees with the nonpositive part of the definition. See repiecef 16804 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 16803*	Piecewise definition on the reals agrees with the nonnegative part of the definition. See repiecef 16804 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 16804*	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 16802 and repiecege0 16803. 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. 16803 (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 16805	Two ways of stating real number trichotomy. (Contributed by Jim Kingdon, 23-Aug-2023.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( A < B \/ A = B \/ B < A ) <-> DECID A # B ) )
Theorem	isomninnlem 16806*	Lemma for isomninn 16807. 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 16807*	Omniscience stated in terms of natural numbers. Similar to isomnimap 7427 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 16808*	Lemma for cvgcmp2n 16809. 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 16809*	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 16810	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 16811	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 7432), (1) the Limited Principle of Omniscience (LPO) is om e. Omni (see df-omni 7425), (2) the Weak Limited Principle of Omniscience (WLPO) is om e. WOmni (see df-womni 7454), (3) Markov's Principle (MP) is om e. Markov (see df-markov 7442), (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 16819), (2) Analytic WLPO is decidability of real number equality, A. x e. RR A. y e. RRDECID x = y (see redcwlpo 16832), (3) Analytic MP is A. x e. RR A. y e. RR ( x =/= y -> x # y ) (see neapmkv 16845), (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 11903).
Theorem	trilpolemclim 16812*	Lemma for trilpo 16819. 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 16813*	Lemma for trilpo 16819. 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 16814*	Lemma for trilpo 16819. 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 16815*	Lemma for trilpo 16819. 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 16816*	Lemma for trilpo 16819. 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 16817*	Lemma for trilpo 16819. 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 7430 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 16818*	Lemma for trilpo 16819. 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 16819*	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 16817 (which means the sequence contains a zero), trilpolemeq1 16816 (which means the sequence is all ones), and trilpolemgt1 16815 (which is not possible). Equivalent ways to state real number trichotomy (sometimes called "analytic LPO") include decidability of real number apartness (see triap 16805) or that the real numbers are a discrete field (see trirec0 16820). 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 10599 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 16820*	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 16819). (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 16821*	Version of trirec0 16820 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 16822	Lemma for apdiff 16824. 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 16823	Lemma for apdiff 16824. (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 16824*	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 16825*	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 16824 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 16826*	Lemma for iswomnimap 7456. 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 16827*	Weak omniscience stated in terms of natural numbers. Similar to iswomnimap 7456 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 16828*	Weak omniscience stated in terms of equality with 0. Like iswomninn 16827 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 16829*	Lemma for ismkvnn 16830. 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 16830*	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 16831*	Lemma for redcwlpo 16832. A biconditionalized version of trilpolemeq1 16816. (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 16832*	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 16831). 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 10603 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 16833*	Real trichotomy implies decidability of real number equality. Or in other words, analytic LPO implies analytic WLPO (see trilpo 16819 and redcwlpo 16832). Thus, this is an analytic analogue to lpowlpo 7458. (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 16834*	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 16835*	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 16836*	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 16837*	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 16832 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 16838*	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 16819 for more discussion of decidability of real number apartness. This is a weaker form of dceqnconst 16837 and in fact this theorem can be proved using dceqnconst 16837 as shown at dcapnconstALT 16839. (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 16839*	Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. A proof of dcapnconst 16838 by means of dceqnconst 16837. (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 16840*	Lemma for nconstwlpo 16843. 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 16841*	Lemma for nconstwlpo 16843. 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 16842*	Lemma for nconstwlpo 16843. (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 16843*	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 16844*	Lemma for neapmkv 16845. 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 16845*	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 16846*	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 16847*	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 16845). (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 16848	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 16849	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 16850	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.4.10  Finite group sum over unordered finite set
Syntax	cgfsu 16851	Extend class notation to include finite group sum over unordered finite set.
class gfsumgf
Definition	df-gfsum 16852*	Define the finite group sum (iterated sum) over an unordered finite set. As currently defined, df-igsum 13464 is indexed by consecutive integers, but in the case of a commutative monoid, the order of the sum doesn't matter and we can define a sum indexed by any finite set without needing to specify an order. (Contributed by Jim Kingdon, 23-Mar-2026.)
|- gfsumgf = ( w e. CMnd , f e. _V |-> ( iota x ( dom f e. Fin /\ E. g ( g : ( 1 ... (♯ ` dom f ) ) -1-1-onto-> dom f /\ x = ( w gsumg ( f o. g ) ) ) ) ) )
Theorem	gfsumval 16853	Value of the finite group sum over an unordered finite set. (Contributed by Jim Kingdon, 24-Mar-2026.)
|- B = ( Base ` W )   &    |- ( ph -> W e. CMnd )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> G : ( 1 ... (♯ ` A ) ) -1-1-onto-> A )   =>    |- ( ph -> ( W gfsumgf F ) = ( W gsumg ( F o. G ) ) )
Theorem	gsumgfsum1 16854	On an integer range starting at one, gsumg and gfsumgf agree. (Contributed by Jim Kingdon, 25-Mar-2026.)
|- B = ( Base ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> F : ( 1 ... N ) --> B )   =>    |- ( ph -> ( G gsumg F ) = ( G gfsumgf F ) )
Theorem	gfsum0 16855	An empty finite group sum is the identity. (Contributed by Jim Kingdon, 26-Mar-2026.)
|- ( G e. CMnd -> ( G gfsumgf (/) ) = ( 0g ` G ) )
Theorem	gsumgfsumlem 16856*	Shifting the indexes of a group sum indexed by consecutive integers. (Contributed by Jim Kingdon, 26-Mar-2026.)
|- B = ( Base ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> F : ( M ... N ) --> B )   &    |- S = ( j e. ( 1 ... ( N + ( 1 - M ) ) ) |-> ( j - ( 1 - M ) ) )   =>    |- ( ph -> ( G gsumg F ) = ( G gsumg ( F o. S ) ) )
Theorem	gsumgfsum 16857	On an integer range, gsumg and gfsumgf agree. (Contributed by Jim Kingdon, 25-Mar-2026.)
|- B = ( Base ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> F : ( M ... N ) --> B )   =>    |- ( ph -> ( G gsumg F ) = ( G gfsumgf F ) )
Theorem	gfsumsn 16858*	Group sum of a singleton. (Contributed by Jim Kingdon, 2-Apr-2026.)
|- B = ( Base ` G )   &    |- ( k = M -> A = C )   =>    |- ( ( G e. CMnd /\ M e. V /\ C e. B ) -> ( G gfsumgf ( k e. { M } |-> A ) ) = C )
Theorem	gfsump1 16859	Splitting off one element from a finite group sum. This would typically used in a proof by induction. (Contributed by Jim Kingdon, 3-Apr-2026.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> F : ( Y u. { Z } ) --> B )   &    |- ( ph -> Y e. Fin )   &    |- ( ph -> Z e. V )   &    |- ( ph -> -. Z e. Y )   =>    |- ( ph -> ( G gfsumgf F ) = ( ( G gfsumgf ( F |` Y ) ) .+ ( F ` Z ) ) )
Theorem	gfsumz 16860*	Value of a finite group sum over the zero element. (Contributed by Jim Kingdon, 24-May-2026.)
|- .0. = ( 0g ` G )   =>    |- ( ( G e. CMnd /\ A e. Fin ) -> ( G gfsumgf ( k e. A |-> .0. ) ) = .0. )
Theorem	gfsumcl 16861	Closure of a finite group sum. (Contributed by Jim Kingdon, 8-Apr-2026.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> F : A --> B )   =>    |- ( ph -> ( G gfsumgf F ) e. B )
14.5  Mathbox for Mykola Mostovenko
Theorem	ax1hfs 16862	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 16863	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 ) )
14.6.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 A. x ph -> ps do not imply that ph 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 A.! x ( ph -> ps ), and when restricted (applied to a class) we allow A.! x e. A ph. The first symbol after the setvar variable must always be e. if it is the form applied to a class, and since e. cannot begin a wff, it is unambiguous. The -> looks like it would be a problem because ph or ps might include implications, but any implication arrow -> within any wff must be surrounded by parentheses, so only the implication arrow of A.! 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 16864	Extend wff definition to include "all some" applied to a top-level implication, which means ps is true whenever ph is true, and there is at least least one x where ph is true. (Contributed by David A. Wheeler, 20-Oct-2018.)
wff A.! x ( ph -> ps )
Syntax	walsc 16865	Extend wff definition to include "all some" applied to a class, which means ph is true for all x in A, and there is at least one x in A. (Contributed by David A. Wheeler, 20-Oct-2018.)
wff A.! x e. A ph
Definition	df-alsi 16866	Define "all some" applied to a top-level implication, which means ps is true whenever ph is true and there is at least one x where ph is true. (Contributed by David A. Wheeler, 20-Oct-2018.)
|- ( A.! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
Definition	df-alsc 16867	Define "all some" applied to a class, which means ph is true for all x in A and there is at least one x in A. (Contributed by David A. Wheeler, 20-Oct-2018.)
|- ( A.! x e. A ph <-> ( A. x e. A ph /\ E. x x e. A ) )
Theorem	alsconv 16868	There is an equivalence between the two "all some" forms. (Contributed by David A. Wheeler, 22-Oct-2018.)
|- ( A.! x ( x e. A -> ph ) <-> A.! x e. A ph )
Theorem	alsi1d 16869	Deduction rule: Given "all some" applied to a top-level inference, you can extract the "for all" part. (Contributed by David A. Wheeler, 20-Oct-2018.)
|- ( ph -> A.! x ( ps -> ch ) )   =>    |- ( ph -> A. x ( ps -> ch ) )
Theorem	alsi2d 16870	Deduction rule: Given "all some" applied to a top-level inference, you can extract the "exists" part. (Contributed by David A. Wheeler, 20-Oct-2018.)
|- ( ph -> A.! x ( ps -> ch ) )   =>    |- ( ph -> E. x ps )
Theorem	alsc1d 16871	Deduction rule: Given "all some" applied to a class, you can extract the "for all" part. (Contributed by David A. Wheeler, 20-Oct-2018.)
|- ( ph -> A.! x e. A ps )   =>    |- ( ph -> A. x e. A ps )
Theorem	alsc2d 16872	Deduction rule: Given "all some" applied to a class, you can extract the "there exists" part. (Contributed by David A. Wheeler, 20-Oct-2018.)
|- ( ph -> A.! x e. A ps )   =>    |- ( ph -> E. x x e. A )

< Previous  Wrap >