Most Recent Proofs - Intuitionistic Logic Explorer

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

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

Last updated on 21-Dec-2024 at 6:40 AM ET.

Recent Additions to the Intuitionistic Logic Explorer

Date	Label	Description
Theorem
9-Dec-2024	nninfwlpoim 7154	Decidable equality for ℕ∞ implies the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 9-Dec-2024.)
|- ( A. x e. ℕ∞ A. y e. ℕ∞ DECID x = y -> om e. WOmni )
8-Dec-2024	nninfwlpoimlemdc 7153	Lemma for nninfwlpoim 7154. (Contributed by Jim Kingdon, 8-Dec-2024.)
|- ( ph -> F : om --> 2o )   &    |- G = ( i e. om |-> if ( E. x e. suc i ( F ` x ) = (/) , (/) , 1o ) )   &    |- ( ph -> A. x e. ℕ∞ A. y e. ℕ∞ DECID x = y )   =>    |- ( ph -> DECID A. n e. om ( F ` n ) = 1o )
8-Dec-2024	nninfwlpoimlemginf 7152	Lemma for nninfwlpoim 7154. (Contributed by Jim Kingdon, 8-Dec-2024.)
|- ( ph -> F : om --> 2o )   &    |- G = ( i e. om |-> if ( E. x e. suc i ( F ` x ) = (/) , (/) , 1o ) )   =>    |- ( ph -> ( G = ( i e. om |-> 1o ) <-> A. n e. om ( F ` n ) = 1o ) )
8-Dec-2024	nninfwlpoimlemg 7151	Lemma for nninfwlpoim 7154. (Contributed by Jim Kingdon, 8-Dec-2024.)
|- ( ph -> F : om --> 2o )   &    |- G = ( i e. om |-> if ( E. x e. suc i ( F ` x ) = (/) , (/) , 1o ) )   =>    |- ( ph -> G e. ℕ∞ )
7-Dec-2024	nninfwlpor 7150	The Weak Limited Principle of Omniscience (WLPO) implies that equality for ℕ∞ is decidable. (Contributed by Jim Kingdon, 7-Dec-2024.)
|- ( om e. WOmni -> A. x e. ℕ∞ A. y e. ℕ∞ DECID x = y )
7-Dec-2024	nninfwlporlem 7149	Lemma for nninfwlpor 7150. The result. (Contributed by Jim Kingdon, 7-Dec-2024.)
|- ( ph -> X : om --> 2o )   &    |- ( ph -> Y : om --> 2o )   &    |- D = ( i e. om |-> if ( ( X ` i ) = ( Y ` i ) , 1o , (/) ) )   &    |- ( ph -> om e. WOmni )   =>    |- ( ph -> DECID X = Y )
6-Dec-2024	nninfwlporlemd 7148	Given two countably infinite sequences of zeroes and ones, they are equal if and only if a sequence formed by pointwise comparing them is all ones. (Contributed by Jim Kingdon, 6-Dec-2024.)
|- ( ph -> X : om --> 2o )   &    |- ( ph -> Y : om --> 2o )   &    |- D = ( i e. om |-> if ( ( X ` i ) = ( Y ` i ) , 1o , (/) ) )   =>    |- ( ph -> ( X = Y <-> D = ( i e. om |-> 1o ) ) )
3-Dec-2024	nninfwlpo 7155	Decidability of equality for ℕ∞ is equivalent to the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 3-Dec-2024.)
|- ( A. x e. ℕ∞ A. y e. ℕ∞ DECID x = y <-> om e. WOmni )
3-Dec-2024	nninfdcinf 7147	The Weak Limited Principle of Omniscience (WLPO) implies that it is decidable whether an element of ℕ∞ equals the point at infinity. (Contributed by Jim Kingdon, 3-Dec-2024.)
|- ( ph -> om e. WOmni )   &    |- ( ph -> N e. ℕ∞ )   =>    |- ( ph -> DECID N = ( i e. om |-> 1o ) )
28-Nov-2024	basmexd 12475	A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 28-Nov-2024.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> A e. B )   =>    |- ( ph -> G e. _V )
22-Nov-2024	eliotaeu 5187	An inhabited iota expression has a unique value. (Contributed by Jim Kingdon, 22-Nov-2024.)
|- ( A e. ( iota x ph ) -> E! x ph )
22-Nov-2024	eliota 5186	An element of an iota expression. (Contributed by Jim Kingdon, 22-Nov-2024.)
|- ( A e. ( iota x ph ) <-> E. y ( A e. y /\ A. x ( ph <-> x = y ) ) )
18-Nov-2024	basmex 12474	A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 18-Nov-2024.)
|- B = ( Base ` G )   =>    |- ( A e. B -> G e. _V )
11-Nov-2024	bj-con1st 13786	Contraposition when the antecedent is a negated stable proposition. See con1dc 851. (Contributed by BJ, 11-Nov-2024.)
|- (STAB ph -> ( ( -. ph -> ps ) -> ( -. ps -> ph ) ) )
11-Nov-2024	const 847	Contraposition when the antecedent is a negated stable proposition. See comment of condc 848. (Contributed by BJ, 18-Nov-2023.) (Proof shortened by BJ, 11-Nov-2024.)
|- (STAB ph -> ( ( -. ph -> -. ps ) -> ( ps -> ph ) ) )
4-Nov-2024	lgsfvalg 13700	Value of the function F which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.) (Revised by Jim Kingdon, 4-Nov-2024.)
|- F = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) , 1 ) )   =>    |- ( ( A e. ZZ /\ N e. NN /\ M e. NN ) -> ( F ` M ) = if ( M e. Prime , ( if ( M = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( M - 1 ) / 2 ) ) + 1 ) mod M ) - 1 ) ) ^ ( M pCnt N ) ) , 1 ) )
1-Nov-2024	qsqeqor 10586	The squares of two rational numbers are equal iff one number equals the other or its negative. (Contributed by Jim Kingdon, 1-Nov-2024.)
|- ( ( A e. QQ /\ B e. QQ ) -> ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( A = B \/ A = -u B ) ) )
29-Oct-2024	fiubnn 10765	A finite set of natural numbers has an upper bound which is a a natural number. (Contributed by Jim Kingdon, 29-Oct-2024.)
|- ( ( A C_ NN /\ A e. Fin ) -> E. x e. NN A. y e. A y <_ x )
29-Oct-2024	fiubz 10764	A finite set of integers has an upper bound which is an integer. (Contributed by Jim Kingdon, 29-Oct-2024.)
|- ( ( A C_ ZZ /\ A e. Fin ) -> E. x e. ZZ A. y e. A y <_ x )
29-Oct-2024	fiubm 10763	Lemma for fiubz 10764 and fiubnn 10765. A general form of those theorems. (Contributed by Jim Kingdon, 29-Oct-2024.)
|- ( ph -> A C_ B )   &    |- ( ph -> B C_ QQ )   &    |- ( ph -> C e. B )   &    |- ( ph -> A e. Fin )   =>    |- ( ph -> E. x e. B A. y e. A y <_ x )
27-Oct-2024	bj-nnst 13778	Double negation of stability of a formula. Intuitionistic logic refutes unstability (but does not prove stability) of any formula. This theorem can also be proved in classical refutability calculus (see https://us.metamath.org/mpeuni/bj-peircestab.html) but not in minimal calculus (see https://us.metamath.org/mpeuni/bj-stabpeirce.html). See nnnotnotr 14025 for the version not using the definition of stability. (Contributed by BJ, 9-Oct-2019.) Prove it in ( -> , -. ) -intuitionistic calculus with definitions (uses of ax-ia1 105, ax-ia2 106, ax-ia3 107 are via sylibr 133, necessary for definition unpackaging), and in ( -> , <-> , -. )-intuitionistic calculus, following a discussion with Jim Kingdon. (Revised by BJ, 27-Oct-2024.)
|- -. -. STAB ph
27-Oct-2024	bj-imnimnn 13773	If a formula is implied by both a formula and its negation, then it is not refutable. There is another proof using the inference associated with bj-nnclavius 13772 as its last step. (Contributed by BJ, 27-Oct-2024.)
|- ( ph -> ps )   &    |- ( -. ph -> ps )   =>    |- -. -. ps
25-Oct-2024	nnwosdc 11994	Well-ordering principle: any inhabited decidable set of positive integers has a least element (schema form). (Contributed by NM, 17-Aug-2001.) (Revised by Jim Kingdon, 25-Oct-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( ( E. x e. NN ph /\ A. x e. NN DECID ph ) -> E. x e. NN ( ph /\ A. y e. NN ( ps -> x <_ y ) ) )
23-Oct-2024	nnwodc 11991	Well-ordering principle: any inhabited decidable set of positive integers has a least element. Theorem I.37 (well-ordering principle) of [Apostol] p. 34. (Contributed by NM, 17-Aug-2001.) (Revised by Jim Kingdon, 23-Oct-2024.)
|- ( ( A C_ NN /\ E. w w e. A /\ A. j e. NN DECID j e. A ) -> E. x e. A A. y e. A x <_ y )
22-Oct-2024	uzwodc 11992	Well-ordering principle: any inhabited decidable subset of an upper set of integers has a least element. (Contributed by NM, 8-Oct-2005.) (Revised by Jim Kingdon, 22-Oct-2024.)
|- ( ( S C_ ( ZZ>= ` M ) /\ E. x x e. S /\ A. x e. ( ZZ>= ` M )DECID x e. S ) -> E. j e. S A. k e. S j <_ k )
21-Oct-2024	nnnotnotr 14025	Double negation of double negation elimination. Suggested by an online post by Martin Escardo. Although this statement resembles nnexmid 845, it can be proved with reference only to implication and negation (that is, without use of disjunction). (Contributed by Jim Kingdon, 21-Oct-2024.)
|- -. -. ( -. -. ph -> ph )
20-Oct-2024	isprm5lem 12095	Lemma for isprm5 12096. The interesting direction (showing that one only needs to check prime divisors up to the square root of P). (Contributed by Jim Kingdon, 20-Oct-2024.)
|- ( ph -> P e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A. z e. Prime ( ( z ^ 2 ) <_ P -> -. z || P ) )   &    |- ( ph -> X e. ( 2 ... ( P - 1 ) ) )   =>    |- ( ph -> -. X || P )
17-Oct-2024	elnndc 9571	Membership of an integer in NN is decidable. (Contributed by Jim Kingdon, 17-Oct-2024.)
|- ( N e. ZZ -> DECID N e. NN )
14-Oct-2024	2zinfmin 11206	Two ways to express the minimum of two integers. Because order of integers is decidable, we have more flexibility than for real numbers. (Contributed by Jim Kingdon, 14-Oct-2024.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> inf ( { A , B } , RR , < ) = if ( A <_ B , A , B ) )
14-Oct-2024	mingeb 11205	Equivalence of <_ and being equal to the minimum of two reals. (Contributed by Jim Kingdon, 14-Oct-2024.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> inf ( { A , B } , RR , < ) = A ) )
13-Oct-2024	pcxnn0cl 12264	Extended nonnegative integer closure of the general prime count function. (Contributed by Jim Kingdon, 13-Oct-2024.)
|- ( ( P e. Prime /\ N e. ZZ ) -> ( P pCnt N ) e. NN0* )
13-Oct-2024	xnn0letri 9760	Dichotomy for extended nonnegative integers. (Contributed by Jim Kingdon, 13-Oct-2024.)
|- ( ( A e. NN0* /\ B e. NN0* ) -> ( A <_ B \/ B <_ A ) )
13-Oct-2024	xnn0dcle 9759	Decidability of <_ for extended nonnegative integers. (Contributed by Jim Kingdon, 13-Oct-2024.)
|- ( ( A e. NN0* /\ B e. NN0* ) -> DECID A <_ B )
9-Oct-2024	nn0leexp2 10645	Ordering law for exponentiation. (Contributed by Jim Kingdon, 9-Oct-2024.)
|- ( ( ( A e. RR /\ M e. NN0 /\ N e. NN0 ) /\ 1 < A ) -> ( M <_ N <-> ( A ^ M ) <_ ( A ^ N ) ) )
8-Oct-2024	pclemdc 12242	Lemma for the prime power pre-function's properties. (Contributed by Jim Kingdon, 8-Oct-2024.)
|- A = { n e. NN0 | ( P ^ n ) || N }   =>    |- ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> A. x e. ZZ DECID x e. A )
8-Oct-2024	elnn0dc 9570	Membership of an integer in NN0 is decidable. (Contributed by Jim Kingdon, 8-Oct-2024.)
|- ( N e. ZZ -> DECID N e. NN0 )
7-Oct-2024	pclemub 12241	Lemma for the prime power pre-function's properties. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Jim Kingdon, 7-Oct-2024.)
|- A = { n e. NN0 | ( P ^ n ) || N }   =>    |- ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> E. x e. ZZ A. y e. A y <_ x )
7-Oct-2024	pclem0 12240	Lemma for the prime power pre-function's properties. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Jim Kingdon, 7-Oct-2024.)
|- A = { n e. NN0 | ( P ^ n ) || N }   =>    |- ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> 0 e. A )
7-Oct-2024	nn0ltexp2 10644	Special case of ltexp2 13654 which we use here because we haven't yet defined df-rpcxp 13574 which is used in the current proof of ltexp2 13654. (Contributed by Jim Kingdon, 7-Oct-2024.)
|- ( ( ( A e. RR /\ M e. NN0 /\ N e. NN0 ) /\ 1 < A ) -> ( M < N <-> ( A ^ M ) < ( A ^ N ) ) )
6-Oct-2024	suprzcl2dc 11910	The supremum of a bounded-above decidable set of integers is a member of the set. (This theorem avoids ax-pre-suploc 7895.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 6-Oct-2024.)
|- ( ph -> A C_ ZZ )   &    |- ( ph -> A. x e. ZZ DECID x e. A )   &    |- ( ph -> E. x e. ZZ A. y e. A y <_ x )   &    |- ( ph -> E. x x e. A )   =>    |- ( ph -> sup ( A , RR , < ) e. A )
5-Oct-2024	zsupssdc 11909	An inhabited decidable bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-suploc 7895.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.)
|- ( ph -> A C_ ZZ )   &    |- ( ph -> E. x x e. A )   &    |- ( ph -> A. x e. ZZ DECID x e. A )   &    |- ( ph -> E. x e. ZZ A. y e. A y <_ x )   =>    |- ( ph -> E. x e. A ( A. y e. A -. x < y /\ A. y e. B ( y < x -> E. z e. A y < z ) ) )
5-Oct-2024	suprzubdc 11907	The supremum of a bounded-above decidable set of integers is greater than any member of the set. (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.)
|- ( ph -> A C_ ZZ )   &    |- ( ph -> A. x e. ZZ DECID x e. A )   &    |- ( ph -> E. x e. ZZ A. y e. A y <_ x )   &    |- ( ph -> B e. A )   =>    |- ( ph -> B <_ sup ( A , RR , < ) )
1-Oct-2024	infex2g 7011	Existence of infimum. (Contributed by Jim Kingdon, 1-Oct-2024.)
|- ( A e. C -> inf ( B , A , R ) e. _V )
30-Sep-2024	unbendc 12409	An unbounded decidable set of positive integers is infinite. (Contributed by NM, 5-May-2005.) (Revised by Jim Kingdon, 30-Sep-2024.)
|- ( ( A C_ NN /\ A. x e. NN DECID x e. A /\ A. m e. NN E. n e. A m < n ) -> A ~~ NN )
30-Sep-2024	prmdc 12084	Primality is decidable. (Contributed by Jim Kingdon, 30-Sep-2024.)
|- ( N e. NN -> DECID N e. Prime )
30-Sep-2024	dcfi 6958	Decidability of a family of propositions indexed by a finite set. (Contributed by Jim Kingdon, 30-Sep-2024.)
|- ( ( A e. Fin /\ A. x e. A DECID ph ) -> DECID A. x e. A ph )
29-Sep-2024	ssnnct 12402	A decidable subset of NN is countable. (Contributed by Jim Kingdon, 29-Sep-2024.)
|- ( ( A C_ NN /\ A. x e. NN DECID x e. A ) -> E. f f : om -onto-> ( A ⊔ 1o ) )
29-Sep-2024	ssnnctlemct 12401	Lemma for ssnnct 12402. The result. (Contributed by Jim Kingdon, 29-Sep-2024.)
|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 1 )   =>    |- ( ( A C_ NN /\ A. x e. NN DECID x e. A ) -> E. f f : om -onto-> ( A ⊔ 1o ) )
28-Sep-2024	nninfdcex 11908	A decidable set of natural numbers has an infimum. (Contributed by Jim Kingdon, 28-Sep-2024.)
|- ( ph -> A C_ NN )   &    |- ( ph -> A. x e. NN DECID x e. A )   &    |- ( ph -> E. y y e. A )   =>    |- ( ph -> E. x e. RR ( A. y e. A -. y < x /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) )
27-Sep-2024	infregelbex 9557	Any lower bound of a set of real numbers with an infimum is less than or equal to the infimum. (Contributed by Jim Kingdon, 27-Sep-2024.)
|- ( ph -> E. x e. RR ( A. y e. A -. y < x /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( B <_ inf ( A , RR , < ) <-> A. z e. A B <_ z ) )
26-Sep-2024	nninfdclemp1 12405	Lemma for nninfdc 12408. Each element of the sequence F is greater than the previous element. (Contributed by Jim Kingdon, 26-Sep-2024.)
|- ( ph -> A C_ NN )   &    |- ( ph -> A. x e. NN DECID x e. A )   &    |- ( ph -> A. m e. NN E. n e. A m < n )   &    |- ( ph -> ( J e. A /\ 1 < J ) )   &    |- F = seq 1 ( ( y e. NN , z e. NN |-> inf ( ( A i^i ( ZZ>= ` ( y + 1 ) ) ) , RR , < ) ) , ( i e. NN |-> J ) )   &    |- ( ph -> U e. NN )   =>    |- ( ph -> ( F ` U ) < ( F ` ( U + 1 ) ) )
26-Sep-2024	nnminle 11990	The infimum of a decidable subset of the natural numbers is less than an element of the set. The infimum is also a minimum as shown at nnmindc 11989. (Contributed by Jim Kingdon, 26-Sep-2024.)
|- ( ( A C_ NN /\ A. x e. NN DECID x e. A /\ B e. A ) -> inf ( A , RR , < ) <_ B )
25-Sep-2024	nninfdclemcl 12403	Lemma for nninfdc 12408. (Contributed by Jim Kingdon, 25-Sep-2024.)
|- ( ph -> A C_ NN )   &    |- ( ph -> A. x e. NN DECID x e. A )   &    |- ( ph -> A. m e. NN E. n e. A m < n )   &    |- ( ph -> P e. A )   &    |- ( ph -> Q e. A )   =>    |- ( ph -> ( P ( y e. NN , z e. NN |-> inf ( ( A i^i ( ZZ>= ` ( y + 1 ) ) ) , RR , < ) ) Q ) e. A )
24-Sep-2024	nninfdclemlt 12406	Lemma for nninfdc 12408. The function from nninfdclemf 12404 is strictly monotonic. (Contributed by Jim Kingdon, 24-Sep-2024.)
|- ( ph -> A C_ NN )   &    |- ( ph -> A. x e. NN DECID x e. A )   &    |- ( ph -> A. m e. NN E. n e. A m < n )   &    |- ( ph -> ( J e. A /\ 1 < J ) )   &    |- F = seq 1 ( ( y e. NN , z e. NN |-> inf ( ( A i^i ( ZZ>= ` ( y + 1 ) ) ) , RR , < ) ) , ( i e. NN |-> J ) )   &    |- ( ph -> U e. NN )   &    |- ( ph -> V e. NN )   &    |- ( ph -> U < V )   =>    |- ( ph -> ( F ` U ) < ( F ` V ) )
23-Sep-2024	nninfdc 12408	An unbounded decidable set of positive integers is infinite. (Contributed by Jim Kingdon, 23-Sep-2024.)
|- ( ( A C_ NN /\ A. x e. NN DECID x e. A /\ A. m e. NN E. n e. A m < n ) -> om ~<_ A )
23-Sep-2024	nninfdclemf1 12407	Lemma for nninfdc 12408. The function from nninfdclemf 12404 is one-to-one. (Contributed by Jim Kingdon, 23-Sep-2024.)
|- ( ph -> A C_ NN )   &    |- ( ph -> A. x e. NN DECID x e. A )   &    |- ( ph -> A. m e. NN E. n e. A m < n )   &    |- ( ph -> ( J e. A /\ 1 < J ) )   &    |- F = seq 1 ( ( y e. NN , z e. NN |-> inf ( ( A i^i ( ZZ>= ` ( y + 1 ) ) ) , RR , < ) ) , ( i e. NN |-> J ) )   =>    |- ( ph -> F : NN -1-1-> A )
23-Sep-2024	nninfdclemf 12404	Lemma for nninfdc 12408. A function from the natural numbers into A. (Contributed by Jim Kingdon, 23-Sep-2024.)
|- ( ph -> A C_ NN )   &    |- ( ph -> A. x e. NN DECID x e. A )   &    |- ( ph -> A. m e. NN E. n e. A m < n )   &    |- ( ph -> ( J e. A /\ 1 < J ) )   &    |- F = seq 1 ( ( y e. NN , z e. NN |-> inf ( ( A i^i ( ZZ>= ` ( y + 1 ) ) ) , RR , < ) ) , ( i e. NN |-> J ) )   =>    |- ( ph -> F : NN --> A )
23-Sep-2024	nnmindc 11989	An inhabited decidable subset of the natural numbers has a minimum. (Contributed by Jim Kingdon, 23-Sep-2024.)
|- ( ( A C_ NN /\ A. x e. NN DECID x e. A /\ E. y y e. A ) -> inf ( A , RR , < ) e. A )
19-Sep-2024	ssomct 12400	A decidable subset of om is countable. (Contributed by Jim Kingdon, 19-Sep-2024.)
|- ( ( A C_ om /\ A. x e. om DECID x e. A ) -> E. f f : om -onto-> ( A ⊔ 1o ) )
14-Sep-2024	nnpredlt 4608	The predecessor (see nnpredcl 4607) of a nonzero natural number is less than (see df-iord 4351) that number. (Contributed by Jim Kingdon, 14-Sep-2024.)
|- ( ( A e. om /\ A =/= (/) ) -> U. A e. A )
13-Sep-2024	nninfisollemeq 7108	Lemma for nninfisol 7109. The case where N is a successor and N and X are equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
|- ( ph -> X e. ℕ∞ )   &    |- ( ph -> ( X ` N ) = (/) )   &    |- ( ph -> N e. om )   &    |- ( ph -> N =/= (/) )   &    |- ( ph -> ( X ` U. N ) = 1o )   =>    |- ( ph -> DECID ( i e. om |-> if ( i e. N , 1o , (/) ) ) = X )
13-Sep-2024	nninfisollemne 7107	Lemma for nninfisol 7109. A case where N is a successor and N and X are not equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
|- ( ph -> X e. ℕ∞ )   &    |- ( ph -> ( X ` N ) = (/) )   &    |- ( ph -> N e. om )   &    |- ( ph -> N =/= (/) )   &    |- ( ph -> ( X ` U. N ) = (/) )   =>    |- ( ph -> DECID ( i e. om |-> if ( i e. N , 1o , (/) ) ) = X )
13-Sep-2024	nninfisollem0 7106	Lemma for nninfisol 7109. The case where N is zero. (Contributed by Jim Kingdon, 13-Sep-2024.)
|- ( ph -> X e. ℕ∞ )   &    |- ( ph -> ( X ` N ) = (/) )   &    |- ( ph -> N e. om )   &    |- ( ph -> N = (/) )   =>    |- ( ph -> DECID ( i e. om |-> if ( i e. N , 1o , (/) ) ) = X )
12-Sep-2024	nninfisol 7109	Finite elements of ℕ∞ are isolated. That is, given a natural number and any element of ℕ∞, it is decidable whether the natural number (when converted to an element of ℕ∞) is equal to the given element of ℕ∞. Stated in an online post by Martin Escardo. One way to understand this theorem is that you do not need to look at an unbounded number of elements of the sequence X to decide whether it is equal to N (in fact, you only need to look at two elements and N tells you where to look). (Contributed by BJ and Jim Kingdon, 12-Sep-2024.)
|- ( ( N e. om /\ X e. ℕ∞ ) -> DECID ( i e. om |-> if ( i e. N , 1o , (/) ) ) = X )
7-Sep-2024	eulerthlemfi 12182	Lemma for eulerth 12187. The set S is finite. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)
|- ( ph -> ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) )   &    |- S = { y e. ( 0..^ N ) | ( y gcd N ) = 1 }   =>    |- ( ph -> S e. Fin )
7-Sep-2024	modqexp 10602	Exponentiation property of the modulo operation, see theorem 5.2(c) in [ApostolNT] p. 107. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> C e. NN0 )   &    |- ( ph -> D e. QQ )   &    |- ( ph -> 0 < D )   &    |- ( ph -> ( A mod D ) = ( B mod D ) )   =>    |- ( ph -> ( ( A ^ C ) mod D ) = ( ( B ^ C ) mod D ) )
5-Sep-2024	eulerthlemh 12185	Lemma for eulerth 12187. A permutation of ( 1 ... ( phi ` N ) ). (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 5-Sep-2024.)
|- ( ph -> ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) )   &    |- S = { y e. ( 0..^ N ) | ( y gcd N ) = 1 }   &    |- ( ph -> F : ( 1 ... ( phi ` N ) ) -1-1-onto-> S )   &    |- H = ( `' F o. ( y e. ( 1 ... ( phi ` N ) ) |-> ( ( A x. ( F ` y ) ) mod N ) ) )   =>    |- ( ph -> H : ( 1 ... ( phi ` N ) ) -1-1-onto-> ( 1 ... ( phi ` N ) ) )
2-Sep-2024	eulerthlemth 12186	Lemma for eulerth 12187. The result. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
|- ( ph -> ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) )   &    |- S = { y e. ( 0..^ N ) | ( y gcd N ) = 1 }   &    |- ( ph -> F : ( 1 ... ( phi ` N ) ) -1-1-onto-> S )   =>    |- ( ph -> ( ( A ^ ( phi ` N ) ) mod N ) = ( 1 mod N ) )
2-Sep-2024	eulerthlema 12184	Lemma for eulerth 12187. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
|- ( ph -> ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) )   &    |- S = { y e. ( 0..^ N ) | ( y gcd N ) = 1 }   &    |- ( ph -> F : ( 1 ... ( phi ` N ) ) -1-1-onto-> S )   =>    |- ( ph -> ( ( ( A ^ ( phi ` N ) ) x. prod_ x e. ( 1 ... ( phi ` N ) ) ( F ` x ) ) mod N ) = ( prod_ x e. ( 1 ... ( phi ` N ) ) ( ( A x. ( F ` x ) ) mod N ) mod N ) )
2-Sep-2024	eulerthlemrprm 12183	Lemma for eulerth 12187. N and prod_ x e. ( 1 ... ( phi ` N ) ) ( F ` x ) are relatively prime. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
|- ( ph -> ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) )   &    |- S = { y e. ( 0..^ N ) | ( y gcd N ) = 1 }   &    |- ( ph -> F : ( 1 ... ( phi ` N ) ) -1-1-onto-> S )   =>    |- ( ph -> ( N gcd prod_ x e. ( 1 ... ( phi ` N ) ) ( F ` x ) ) = 1 )
30-Aug-2024	fprodap0f 11599	A finite product of terms apart from zero is apart from zero. A version of fprodap0 11584 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by Jim Kingdon, 30-Aug-2024.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. A ) -> B # 0 )   =>    |- ( ph -> prod_ k e. A B # 0 )
28-Aug-2024	fprodrec 11592	The finite product of reciprocals is the reciprocal of the product. (Contributed by Jim Kingdon, 28-Aug-2024.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. A ) -> B # 0 )   =>    |- ( ph -> prod_ k e. A ( 1 / B ) = ( 1 / prod_ k e. A B ) )
26-Aug-2024	exmidontri2or 7220	Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
|- (EXMID <-> A. x e. On A. y e. On ( x C_ y \/ y C_ x ) )
26-Aug-2024	exmidontri 7216	Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
|- (EXMID <-> A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x ) )
26-Aug-2024	ontri2orexmidim 4556	Ordinal trichotomy implies excluded middle. Closed form of ordtri2or2exmid 4555. (Contributed by Jim Kingdon, 26-Aug-2024.)
|- ( A. x e. On A. y e. On ( x C_ y \/ y C_ x ) -> DECID ph )
26-Aug-2024	ontriexmidim 4506	Ordinal trichotomy implies excluded middle. Closed form of ordtriexmid 4505. (Contributed by Jim Kingdon, 26-Aug-2024.)
|- ( A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x ) -> DECID ph )
25-Aug-2024	onntri2or 7223	Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
|- ( -. -. EXMID <-> A. x e. On A. y e. On -. -. ( x C_ y \/ y C_ x ) )
25-Aug-2024	onntri3or 7222	Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
|- ( -. -. EXMID <-> A. x e. On A. y e. On -. -. ( x e. y \/ x = y \/ y e. x ) )
25-Aug-2024	csbcow 3060	Composition law for chained substitutions into a class. Version of csbco 3059 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 10-Nov-2005.) (Revised by Gino Giotto, 25-Aug-2024.)
|- [_ A / y ]_ [_ y / x ]_ B = [_ A / x ]_ B
25-Aug-2024	cbvreuvw 2702	Version of cbvreuv 2698 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E! x e. A ph <-> E! y e. A ps )
25-Aug-2024	cbvrexvw 2701	Version of cbvrexv 2697 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x e. A ph <-> E. y e. A ps )
25-Aug-2024	cbvralvw 2700	Version of cbvralv 2696 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x e. A ph <-> A. y e. A ps )
25-Aug-2024	cbvabw 2293	Version of cbvab 2294 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- { x | ph } = { y | ps }
25-Aug-2024	nfsbv 1940	If z is not free in ph, it is not free in [ y / x ] ph when z is distinct from x and y. Version of nfsb 1939 requiring more disjoint variables. (Contributed by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on x , y. (Revised by Steven Nguyen, 13-Aug-2023.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
|- F/ z ph   =>    |- F/ z [ y / x ] ph
25-Aug-2024	cbvexvw 1913	Change bound variable. See cbvexv 1911 for a version with fewer disjoint variable conditions. (Contributed by NM, 19-Apr-2017.) Avoid ax-7 1441. (Revised by Gino Giotto, 25-Aug-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ph <-> E. y ps )
25-Aug-2024	cbvalvw 1912	Change bound variable. See cbvalv 1910 for a version with fewer disjoint variable conditions. (Contributed by NM, 9-Apr-2017.) Avoid ax-7 1441. (Revised by Gino Giotto, 25-Aug-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph <-> A. y ps )
25-Aug-2024	nfal 1569	If x is not free in ph, it is not free in A. y ph. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-4 1503. (Revised by Gino Giotto, 25-Aug-2024.)
|- F/ x ph   =>    |- F/ x A. y ph
24-Aug-2024	gcdcomd 11929	The gcd operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> ( M gcd N ) = ( N gcd M ) )
21-Aug-2024	dvds2addd 11791	Deduction form of dvds2add 11787. (Contributed by SN, 21-Aug-2024.)
|- ( ph -> K e. ZZ )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> K || M )   &    |- ( ph -> K || N )   =>    |- ( ph -> K || ( M + N ) )
17-Aug-2024	fprodcl2lem 11568	Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.)
|- ( ph -> S C_ CC )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. S )   &    |- ( ph -> A =/= (/) )   =>    |- ( ph -> prod_ k e. A B e. S )
16-Aug-2024	if0ab 13840	Expression of a conditional class as a class abstraction when the False alternative is the empty class: in that case, the conditional class is the extension, in the True alternative, of the condition. Remark: a consequence which could be formalized is the inclusion |- if ( ph , A , (/) ) C_ A and therefore, using elpwg 3574, |- ( A e. V -> if ( ph , A , (/) ) e. ~P A ), from which fmelpw1o 13841 could be derived, yielding an alternative proof. (Contributed by BJ, 16-Aug-2024.)
|- if ( ph , A , (/) ) = { x e. A | ph }
16-Aug-2024	fprodunsn 11567	Multiply in an additional term in a finite product. See also fprodsplitsn 11596 which is the same but with a F/ k ph hypothesis in place of the distinct variable condition between ph and k. (Contributed by Jim Kingdon, 16-Aug-2024.)
|- F/_ k D   &    |- ( ph -> A e. Fin )   &    |- ( ph -> B e. V )   &    |- ( ph -> -. B e. A )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( k = B -> C = D )   =>    |- ( ph -> prod_ k e. ( A u. { B } ) C = ( prod_ k e. A C x. D ) )
15-Aug-2024	bj-charfundcALT 13844	Alternate proof of bj-charfundc 13843. It was expected to be much shorter since it uses bj-charfun 13842 for the main part of the proof and the rest is basic computations, but these turn out to be lengthy, maybe because of the limited library of available lemmas. (Contributed by BJ, 15-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> F = ( x e. X |-> if ( x e. A , 1o , (/) ) ) )   &    |- ( ph -> A. x e. X DECID x e. A )   =>    |- ( ph -> ( F : X --> 2o /\ ( A. x e. ( X i^i A ) ( F ` x ) = 1o /\ A. x e. ( X \ A ) ( F ` x ) = (/) ) ) )
15-Aug-2024	bj-charfun 13842	Properties of the characteristic function on the class X of the class A. (Contributed by BJ, 15-Aug-2024.)
|- ( ph -> F = ( x e. X |-> if ( x e. A , 1o , (/) ) ) )   =>    |- ( ph -> ( ( F : X --> ~P 1o /\ ( F |` ( ( X i^i A ) u. ( X \ A ) ) ) : ( ( X i^i A ) u. ( X \ A ) ) --> 2o ) /\ ( A. x e. ( X i^i A ) ( F ` x ) = 1o /\ A. x e. ( X \ A ) ( F ` x ) = (/) ) ) )
15-Aug-2024	fmelpw1o 13841	With a formula ph one can associate an element of ~P 1o, which can therefore be thought of as the set of "truth values" (but recall that there are no other genuine truth values than T. and F., by nndc 846, which translate to 1o and (/) respectively by iftrue 3531 and iffalse 3534, giving pwtrufal 14030). As proved in if0ab 13840, the associated element of ~P 1o is the extension, in ~P 1o, of the formula ph. (Contributed by BJ, 15-Aug-2024.)
|- if ( ph , 1o , (/) ) e. ~P 1o
15-Aug-2024	cnstab 8564	Equality of complex numbers is stable. Stability here means -. -. A = B -> A = B as defined at df-stab 826. This theorem for real numbers is Proposition 5.2 of [BauerHanson], p. 27. (Contributed by Jim Kingdon, 1-Aug-2023.) (Proof shortened by BJ, 15-Aug-2024.)
|- ( ( A e. CC /\ B e. CC ) -> STAB A = B )
15-Aug-2024	subap0d 8563	Two numbers apart from each other have difference apart from zero. (Contributed by Jim Kingdon, 12-Aug-2021.) (Proof shortened by BJ, 15-Aug-2024.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # B )   =>    |- ( ph -> ( A - B ) # 0 )
15-Aug-2024	ifexd 4469	Existence of a conditional class (deduction form). (Contributed by BJ, 15-Aug-2024.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> if ( ps , A , B ) e. _V )
15-Aug-2024	ifelpwun 4468	Existence of a conditional class, quantitative version (inference form). (Contributed by BJ, 15-Aug-2024.)
|- A e. _V   &    |- B e. _V   =>    |- if ( ph , A , B ) e. ~P ( A u. B )
15-Aug-2024	ifelpwund 4467	Existence of a conditional class, quantitative version (deduction form). (Contributed by BJ, 15-Aug-2024.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> if ( ps , A , B ) e. ~P ( A u. B ) )