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 15-Dec-2025 at 7:07 AM ET.

Recent Additions to the Intuitionistic Logic Explorer

Date	Label	Description
Theorem
30-Nov-2025	nninfnfiinf 15778	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 ) )
27-Nov-2025	psrelbasfi 14310	Simpler form of psrelbas 14309 when the index set is finite. (Contributed by Jim Kingdon, 27-Nov-2025.)
|- S = ( I mPwSer R )   &    |- K = ( Base ` R )   &    |- ( ph -> I e. Fin )   &    |- B = ( Base ` S )   &    |- ( ph -> X e. B )   =>    |- ( ph -> X : ( NN0 ^m I ) --> K )
26-Nov-2025	mplsubgfileminv 14334	Lemma for mplsubgfi 14335. The additive inverse of a polynomial is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.)
|- S = ( I mPwSer R )   &    |- P = ( I mPoly R )   &    |- U = ( Base ` P )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Grp )   &    |- ( ph -> X e. U )   &    |- N = ( invg ` S )   =>    |- ( ph -> ( N ` X ) e. U )
26-Nov-2025	mplsubgfilemcl 14333	Lemma for mplsubgfi 14335. The sum of two polynomials is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.)
|- S = ( I mPwSer R )   &    |- P = ( I mPoly R )   &    |- U = ( Base ` P )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Grp )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- .+ = ( +g ` S )   =>    |- ( ph -> ( X .+ Y ) e. U )
25-Nov-2025	nninfinfwlpo 7255	The point at infinity in ℕ∞ being isolated is equivalent to the Weak Limited Principle of Omniscience (WLPO). By isolated, we mean that the equality of that point with every other element of ℕ∞ is decidable. From an online post by Martin Escardo. By contrast, elements of ℕ∞ corresponding to natural numbers are isolated (nninfisol 7208). (Contributed by Jim Kingdon, 25-Nov-2025.)
|- ( A. x e. ℕ∞ DECID x = ( i e. om |-> 1o ) <-> om e. WOmni )
23-Nov-2025	psrbagfi 14307	A finite index set gives a simpler expression for finite bags. (Contributed by Jim Kingdon, 23-Nov-2025.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( I e. Fin -> D = ( NN0 ^m I ) )
22-Nov-2025	df-acnm 7260	Define a local and length-limited version of the axiom of choice. The definition of the predicate X e. AC A is that for all families of inhabited subsets of X indexed on A (i.e. functions A --> { z e. ~P X | E. j j e. z }), there is a function which selects an element from each set in the family. (Contributed by Mario Carneiro, 31-Aug-2015.) Change nonempty to inhabited. (Revised by Jim Kingdon, 22-Nov-2025.)
|- AC A = { x | ( A e. _V /\ A. f e. ( { z e. ~P x | E. j j e. z } ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) }
21-Nov-2025	mplsubgfilemm 14332	Lemma for mplsubgfi 14335. There exists a polynomial. (Contributed by Jim Kingdon, 21-Nov-2025.)
|- S = ( I mPwSer R )   &    |- P = ( I mPoly R )   &    |- U = ( Base ` P )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Grp )   =>    |- ( ph -> E. j j e. U )
14-Nov-2025	2omapen 15751	Equinumerosity of ( 2o ^m A ) and the set of decidable subsets of A. (Contributed by Jim Kingdon, 14-Nov-2025.)
|- ( A e. V -> ( 2o ^m A ) ~~ { x e. ~P A | A. y e. A DECID y e. x } )
12-Nov-2025	2omap 15750	Mapping between ( 2o ^m A ) and decidable subsets of A. (Contributed by Jim Kingdon, 12-Nov-2025.)
|- F = ( s e. ( 2o ^m A ) |-> { z e. A | ( s ` z ) = 1o } )   =>    |- ( A e. V -> F : ( 2o ^m A ) -1-1-onto-> { x e. ~P A | A. y e. A DECID y e. x } )
11-Nov-2025	domomsubct 15756	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 ) )
10-Nov-2025	prdsbaslemss 12978	Lemma for prdsbas 12980 and similar theorems. (Contributed by Jim Kingdon, 10-Nov-2025.)
|- P = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> R e. W )   &    |- A = ( E ` P )   &    |- E = Slot ( E ` ndx )   &    |- ( E ` ndx ) e. NN   &    |- ( ph -> T e. X )   &    |- ( ph -> { <. ( E ` ndx ) , T >. } C_ P )   =>    |- ( ph -> A = T )
5-Nov-2025	fnmpl 14327	mPoly has universal domain. (Contributed by Jim Kingdon, 5-Nov-2025.)
|- mPoly Fn ( _V X. _V )
4-Nov-2025	mplelbascoe 14326	Property of being a polynomial. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.)
|- P = ( I mPoly R )   &    |- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .0. = ( 0g ` R )   &    |- U = ( Base ` P )   =>    |- ( ( I e. V /\ R e. W ) -> ( X e. U <-> ( X e. B /\ E. a e. ( NN0 ^m I ) A. b e. ( NN0 ^m I ) ( A. k e. I ( a ` k ) < ( b ` k ) -> ( X ` b ) = .0. ) ) ) )
4-Nov-2025	mplbascoe 14325	Base set of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.)
|- P = ( I mPoly R )   &    |- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .0. = ( 0g ` R )   &    |- U = ( Base ` P )   =>    |- ( ( I e. V /\ R e. W ) -> U = { f e. B | E. a e. ( NN0 ^m I ) A. b e. ( NN0 ^m I ) ( A. k e. I ( a ` k ) < ( b ` k ) -> ( f ` b ) = .0. ) } )
4-Nov-2025	mplvalcoe 14324	Value of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.)
|- P = ( I mPoly R )   &    |- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .0. = ( 0g ` R )   &    |- U = { f e. B | E. a e. ( NN0 ^m I ) A. b e. ( NN0 ^m I ) ( A. k e. I ( a ` k ) < ( b ` k ) -> ( f ` b ) = .0. ) }   =>    |- ( ( I e. V /\ R e. W ) -> P = ( S ↾s U ) )
1-Nov-2025	ficardon 7269	The cardinal number of a finite set is an ordinal. (Contributed by Jim Kingdon, 1-Nov-2025.)
|- ( A e. Fin -> ( card ` A ) e. On )
31-Oct-2025	bitsdc 12131	Whether a bit is set is decidable. (Contributed by Jim Kingdon, 31-Oct-2025.)
|- ( ( N e. ZZ /\ M e. NN0 ) -> DECID M e. (bits ` N ) )
28-Oct-2025	nn0maxcl 11409	The maximum of two nonnegative integers is a nonnegative integer. (Contributed by Jim Kingdon, 28-Oct-2025.)
|- ( ( A e. NN0 /\ B e. NN0 ) -> sup ( { A , B } , RR , < ) e. NN0 )
28-Oct-2025	qdcle 10355	Rational <_ is decidable. (Contributed by Jim Kingdon, 28-Oct-2025.)
|- ( ( A e. QQ /\ B e. QQ ) -> DECID A <_ B )
17-Oct-2025	plycoeid3 15101	Reconstruct a polynomial as an explicit sum of the coefficient function up to an index no smaller than the degree of the polynomial. (Contributed by Jim Kingdon, 17-Oct-2025.)
|- ( ph -> D e. NN0 )   &    |- ( ph -> A : NN0 --> CC )   &    |- ( ph -> ( A " ( ZZ>= ` ( D + 1 ) ) ) = { 0 } )   &    |- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... D ) ( ( A ` k ) x. ( z ^ k ) ) ) )   &    |- ( ph -> M e. ( ZZ>= ` D ) )   &    |- ( ph -> X e. CC )   =>    |- ( ph -> ( F ` X ) = sum_ j e. ( 0 ... M ) ( ( A ` j ) x. ( X ^ j ) ) )
13-Oct-2025	tpfidceq 7000	A triple is finite if it consists of elements of a class with decidable equality. (Contributed by Jim Kingdon, 13-Oct-2025.)
|- ( ph -> A e. D )   &    |- ( ph -> B e. D )   &    |- ( ph -> C e. D )   &    |- ( ph -> A. x e. D A. y e. D DECID x = y )   =>    |- ( ph -> { A , B , C } e. Fin )
13-Oct-2025	prfidceq 6998	A pair is finite if it consists of elements of a class with decidable equality. (Contributed by Jim Kingdon, 13-Oct-2025.)
|- ( ph -> A e. C )   &    |- ( ph -> B e. C )   &    |- ( ph -> A. x e. C A. y e. C DECID x = y )   =>    |- ( ph -> { A , B } e. Fin )
13-Oct-2025	dcun 3561	The union of two decidable classes is decidable. (Contributed by Jim Kingdon, 5-Oct-2022.) (Revised by Jim Kingdon, 13-Oct-2025.)
|- ( ph -> DECID C e. A )   &    |- ( ph -> DECID C e. B )   =>    |- ( ph -> DECID C e. ( A u. B ) )
9-Oct-2025	dvdsfi 12434	A natural number has finitely many divisors. (Contributed by Jim Kingdon, 9-Oct-2025.)
|- ( N e. NN -> { x e. NN | x || N } e. Fin )
7-Oct-2025	df-mplcoe 14298	Define the subalgebra of the power series algebra generated by the variables; this is the polynomial algebra (the set of power series with finite degree). The index set (which has an element for each variable) is i, the coefficients are in ring r, and for each variable there is a "degree" such that the coefficient is zero for a term where the powers are all greater than those degrees. (Degree is in quotes because there is no guarantee that coefficients below that degree are nonzero, as we do not assume decidable equality for r). (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 7-Oct-2025.)
|- mPoly = ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / w ]_ ( w ↾s { f e. ( Base ` w ) | E. a e. ( NN0 ^m i ) A. b e. ( NN0 ^m i ) ( A. k e. i ( a ` k ) < ( b ` k ) -> ( f ` b ) = ( 0g ` r ) ) } ) )
6-Oct-2025	dvconstss 15042	Derivative of a constant function defined on an open set. (Contributed by Jim Kingdon, 6-Oct-2025.)
|- ( ph -> S e. { RR , CC } )   &    |- J = ( K ↾t S )   &    |- K = ( MetOpen ` ( abs o. - ) )   &    |- ( ph -> X e. J )   &    |- ( ph -> A e. CC )   =>    |- ( ph -> ( S _D ( X X. { A } ) ) = ( X X. { 0 } ) )
6-Oct-2025	dcfrompeirce 1460	The decidability of a proposition ch follows from a suitable instance of Peirce's law. Therefore, if we were to introduce Peirce's law as a general principle (without the decidability condition in peircedc 915), then we could prove that every proposition is decidable, giving us the classical system of propositional calculus (since Perice's law is itself classically valid). (Contributed by Adrian Ducourtial, 6-Oct-2025.)
|- ( ph <-> ( ch \/ -. ch ) )   &    |- ( ps <-> F. )   &    |- ( ( ( ph -> ps ) -> ph ) -> ph )   =>    |- DECID ch
6-Oct-2025	dcfromcon 1459	The decidability of a proposition ch follows from a suitable instance of the principle of contraposition. Therefore, if we were to introduce contraposition as a general principle (without the decidability condition in condc 854), then we could prove that every proposition is decidable, giving us the classical system of propositional calculus (since the principle of contraposition is itself classically valid). (Contributed by Adrian Ducourtial, 6-Oct-2025.)
|- ( ph <-> ( ch \/ -. ch ) )   &    |- ( ps <-> T. )   &    |- ( ( -. ph -> -. ps ) -> ( ps -> ph ) )   =>    |- DECID ch
6-Oct-2025	dcfromnotnotr 1458	The decidability of a proposition ps follows from a suitable instance of double negation elimination (DNE). Therefore, if we were to introduce DNE as a general principle (without the decidability condition in notnotrdc 844), then we could prove that every proposition is decidable, giving us the classical system of propositional calculus (since DNE itself is classically valid). (Contributed by Adrian Ducourtial, 6-Oct-2025.)
|- ( ph <-> ( ps \/ -. ps ) )   &    |- ( -. -. ph -> ph )   =>    |- DECID ps
3-Oct-2025	dvidre 15041	Real derivative of the identity function. (Contributed by Jim Kingdon, 3-Oct-2025.)
|- ( RR _D ( _I |` RR ) ) = ( RR X. { 1 } )
3-Oct-2025	dvconstre 15040	Real derivative of a constant function. (Contributed by Jim Kingdon, 3-Oct-2025.)
|- ( A e. CC -> ( RR _D ( RR X. { A } ) ) = ( RR X. { 0 } ) )
3-Oct-2025	dvidsslem 15037	Lemma for dvconstss 15042. Analogue of dvidlemap 15035 where F is defined on an open subset of the real or complex numbers. (Contributed by Jim Kingdon, 3-Oct-2025.)
|- ( ph -> S e. { RR , CC } )   &    |- J = ( K ↾t S )   &    |- K = ( MetOpen ` ( abs o. - ) )   &    |- ( ph -> F : X --> CC )   &    |- ( ph -> X e. J )   &    |- ( ( ph /\ ( x e. X /\ z e. X /\ z # x ) ) -> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) = B )   &    |- B e. CC   =>    |- ( ph -> ( S _D F ) = ( X X. { B } ) )
3-Oct-2025	dvidrelem 15036	Lemma for dvidre 15041 and dvconstre 15040. Analogue of dvidlemap 15035 for real numbers rather than complex numbers. (Contributed by Jim Kingdon, 3-Oct-2025.)
|- ( ph -> F : RR --> CC )   &    |- ( ( ph /\ ( x e. RR /\ z e. RR /\ z # x ) ) -> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) = B )   &    |- B e. CC   =>    |- ( ph -> ( RR _D F ) = ( RR X. { B } ) )
28-Sep-2025	metuex 14189	Applying metUnif yields a set. (Contributed by Jim Kingdon, 28-Sep-2025.)
|- ( A e. V -> (metUnif ` A ) e. _V )
28-Sep-2025	cndsex 14187	The standard distance function on the complex numbers is a set. (Contributed by Jim Kingdon, 28-Sep-2025.)
|- ( abs o. - ) e. _V
25-Sep-2025	cntopex 14188	The standard topology on the complex numbers is a set. (Contributed by Jim Kingdon, 25-Sep-2025.)
|- ( MetOpen ` ( abs o. - ) ) e. _V
24-Sep-2025	mopnset 14186	Getting a set by applying MetOpen. (Contributed by Jim Kingdon, 24-Sep-2025.)
|- ( D e. V -> ( MetOpen ` D ) e. _V )
24-Sep-2025	blfn 14185	The ball function has universal domain. (Contributed by Jim Kingdon, 24-Sep-2025.)
|- ball Fn _V
22-Sep-2025	plycjlemc 15104	Lemma for plycj 15105. (Contributed by Mario Carneiro, 24-Jul-2014.) (Revised by Jim Kingdon, 22-Sep-2025.)
|- ( ph -> N e. NN0 )   &    |- G = ( ( * o. F ) o. * )   &    |- ( ph -> A : NN0 --> ( S u. { 0 } ) )   &    |- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )   &    |- ( ph -> F e. (Poly ` S ) )   =>    |- ( ph -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( * o. A ) ` k ) x. ( z ^ k ) ) ) )
20-Sep-2025	plycolemc 15102	Lemma for plyco 15103. The result expressed as a sum, with a degree and coefficients for F specified as hypotheses. (Contributed by Jim Kingdon, 20-Sep-2025.)
|- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> G e. (Poly ` S ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> A : NN0 --> ( S u. { 0 } ) )   &    |- ( ph -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )   &    |- ( ph -> F = ( x e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( x ^ k ) ) ) )   =>    |- ( ph -> ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( ( G ` z ) ^ k ) ) ) e. (Poly ` S ) )
16-Sep-2025	lgsquadlemofi 15425	Lemma for lgsquad 15429. There are finitely many members of S with odd first part. (Contributed by Jim Kingdon, 16-Sep-2025.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- M = ( ( P - 1 ) / 2 )   &    |- N = ( ( Q - 1 ) / 2 )   &    |- S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }   =>    |- ( ph -> { z e. S | -. 2 || ( 1st ` z ) } e. Fin )
16-Sep-2025	lgsquadlemsfi 15424	Lemma for lgsquad 15429. S is finite. (Contributed by Jim Kingdon, 16-Sep-2025.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- M = ( ( P - 1 ) / 2 )   &    |- N = ( ( Q - 1 ) / 2 )   &    |- S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }   =>    |- ( ph -> S e. Fin )
16-Sep-2025	opabfi 7008	Finiteness of an ordered pair abstraction which is a decidable subset of finite sets. (Contributed by Jim Kingdon, 16-Sep-2025.)
|- S = { <. x , y >. | ( ( x e. A /\ y e. B ) /\ ps ) }   &    |- ( ph -> A e. Fin )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> A. x e. A A. y e. B DECID ps )   =>    |- ( ph -> S e. Fin )
13-Sep-2025	uchoice 6204	Principle of unique choice. This is also called non-choice. The name choice results in its similarity to something like acfun 7292 (with the key difference being the change of E. to E!) but unique choice in fact follows from the axiom of collection and our other axioms. This is somewhat similar to Corollary 3.9.2 of [HoTT], p. (varies) but is better described by the paragraph at the end of Section 3.9 which starts "A similar issue arises in set-theoretic mathematics". (Contributed by Jim Kingdon, 13-Sep-2025.)
|- ( ( A e. V /\ A. x e. A E! y ph ) -> E. f ( f Fn A /\ A. x e. A [. ( f ` x ) / y ]. ph ) )
11-Sep-2025	expghmap 14241	Exponentiation is a group homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015.) (Revised by AV, 10-Jun-2019.) (Revised by Jim Kingdon, 11-Sep-2025.)
|- M = (mulGrp ` ℂfld )   &    |- U = ( M ↾s { z e. CC | z # 0 } )   =>    |- ( ( A e. CC /\ A # 0 ) -> ( x e. ZZ |-> ( A ^ x ) ) e. (ℤring GrpHom U ) )
11-Sep-2025	cnfldui 14223	The invertible complex numbers are exactly those apart from zero. This is recapb 8717 but expressed in terms of ℂfld. (Contributed by Jim Kingdon, 11-Sep-2025.)
|- { z e. CC | z # 0 } = (Unit ` ℂfld )
9-Sep-2025	gsumfzfsumlemm 14221	Lemma for gsumfzfsum 14222. The case where the sum is inhabited. (Contributed by Jim Kingdon, 9-Sep-2025.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> B e. CC )   =>    |- ( ph -> (ℂfld gsumg ( k e. ( M ... N ) |-> B ) ) = sum_ k e. ( M ... N ) B )
9-Sep-2025	gsumfzfsumlem0 14220	Lemma for gsumfzfsum 14222. The case where the sum is empty. (Contributed by Jim Kingdon, 9-Sep-2025.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> N < M )   =>    |- ( ph -> (ℂfld gsumg ( k e. ( M ... N ) |-> B ) ) = sum_ k e. ( M ... N ) B )
9-Sep-2025	gsumfzmhm2 13552	Apply a group homomorphism to a group sum, mapping version with implicit substitution. (Contributed by Mario Carneiro, 5-May-2015.) (Revised by AV, 6-Jun-2019.) (Revised by Jim Kingdon, 9-Sep-2025.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> H e. Mnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> ( x e. B |-> C ) e. ( G MndHom H ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> X e. B )   &    |- ( x = X -> C = D )   &    |- ( x = ( G gsumg ( k e. ( M ... N ) |-> X ) ) -> C = E )   =>    |- ( ph -> ( H gsumg ( k e. ( M ... N ) |-> D ) ) = E )
8-Sep-2025	gsumfzmhm 13551	Apply a monoid homomorphism to a group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 6-Jun-2019.) (Revised by Jim Kingdon, 8-Sep-2025.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> H e. Mnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> K e. ( G MndHom H ) )   &    |- ( ph -> F : ( M ... N ) --> B )   =>    |- ( ph -> ( H gsumg ( K o. F ) ) = ( K ` ( G gsumg F ) ) )
8-Sep-2025	5ndvds6 12119	5 does not divide 6. (Contributed by AV, 8-Sep-2025.)
|- -. 5 || 6
8-Sep-2025	5ndvds3 12118	5 does not divide 3. (Contributed by AV, 8-Sep-2025.)
|- -. 5 || 3
6-Sep-2025	gsumfzconst 13549	Sum of a constant series. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Jim Kingdon, 6-Sep-2025.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. Mnd /\ N e. ( ZZ>= ` M ) /\ X e. B ) -> ( G gsumg ( k e. ( M ... N ) |-> X ) ) = ( ( ( N - M ) + 1 ) .x. X ) )
31-Aug-2025	gsumfzmptfidmadd 13547	The sum of two group sums expressed as mappings with finite domain. (Contributed by AV, 23-Jul-2019.) (Revised by Jim Kingdon, 31-Aug-2025.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ x e. ( M ... N ) ) -> C e. B )   &    |- ( ( ph /\ x e. ( M ... N ) ) -> D e. B )   &    |- F = ( x e. ( M ... N ) |-> C )   &    |- H = ( x e. ( M ... N ) |-> D )   =>    |- ( ph -> ( G gsumg ( x e. ( M ... N ) |-> ( C .+ D ) ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) )
30-Aug-2025	gsumfzsubmcl 13546	Closure of a group sum in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015.) (Revised by AV, 3-Jun-2019.) (Revised by Jim Kingdon, 30-Aug-2025.)
|- ( ph -> G e. Mnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> S e. (SubMnd ` G ) )   &    |- ( ph -> F : ( M ... N ) --> S )   =>    |- ( ph -> ( G gsumg F ) e. S )
30-Aug-2025	seqm1g 10585	Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 30-Aug-2025.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )   &    |- ( ph -> .+ e. V )   &    |- ( ph -> F e. W )   =>    |- ( ph -> ( seq M ( .+ , F ) ` N ) = ( ( seq M ( .+ , F ) ` ( N - 1 ) ) .+ ( F ` N ) ) )
29-Aug-2025	seqf1og 10632	Rearrange a sum via an arbitrary bijection on ( M ... N ). (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Jim Kingdon, 29-Aug-2025.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> C C_ S )   &    |- ( ph -> .+ e. V )   &    |- ( ph -> F : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- ( ( ph /\ x e. ( M ... N ) ) -> ( G ` x ) e. C )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( G ` ( F ` k ) ) )   &    |- ( ph -> G e. W )   &    |- ( ph -> H e. X )   =>    |- ( ph -> ( seq M ( .+ , H ) ` N ) = ( seq M ( .+ , G ) ` N ) )
25-Aug-2025	irrmulap 9741	The product of an irrational with a nonzero rational is irrational. By irrational we mean apart from any rational number. For a similar theorem with not rational in place of irrational, see irrmul 9740. (Contributed by Jim Kingdon, 25-Aug-2025.)
|- ( ph -> A e. RR )   &    |- ( ph -> A. q e. QQ A # q )   &    |- ( ph -> B e. QQ )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> Q e. QQ )   =>    |- ( ph -> ( A x. B ) # Q )
19-Aug-2025	seqp1g 10577	Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 19-Aug-2025.)
|- ( ( N e. ( ZZ>= ` M ) /\ F e. V /\ .+ e. W ) -> ( seq M ( .+ , F ) ` ( N + 1 ) ) = ( ( seq M ( .+ , F ) ` N ) .+ ( F ` ( N + 1 ) ) ) )
19-Aug-2025	seq1g 10574	Value of the sequence builder function at its initial value. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 19-Aug-2025.)
|- ( ( M e. ZZ /\ F e. V /\ .+ e. W ) -> ( seq M ( .+ , F ) ` M ) = ( F ` M ) )
18-Aug-2025	iswrdiz 10961	A zero-based sequence is a word. In iswrdinn0 10959 we can specify a length as an nonnegative integer. However, it will occasionally be helpful to allow a negative length, as well as zero, to specify an empty sequence. (Contributed by Jim Kingdon, 18-Aug-2025.)
|- ( ( W : ( 0..^ L ) --> S /\ L e. ZZ ) -> W e. Word S )
16-Aug-2025	gsumfzcl 13203	Closure of a finite group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 3-Jun-2019.) (Revised by Jim Kingdon, 16-Aug-2025.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> F : ( M ... N ) --> B )   =>    |- ( ph -> ( G gsumg F ) e. B )
16-Aug-2025	iswrdinn0 10959	A zero-based sequence is a word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 16-Aug-2025.)
|- ( ( W : ( 0..^ L ) --> S /\ L e. NN0 ) -> W e. Word S )
15-Aug-2025	gsumfzz 13199	Value of a group sum over the zero element. (Contributed by Mario Carneiro, 7-Dec-2014.) (Revised by Jim Kingdon, 15-Aug-2025.)
|- .0. = ( 0g ` G )   =>    |- ( ( G e. Mnd /\ M e. ZZ /\ N e. ZZ ) -> ( G gsumg ( k e. ( M ... N ) |-> .0. ) ) = .0. )
14-Aug-2025	gsumfzval 13095	An expression for gsumg when summing over a finite set of sequential integers. (Contributed by Jim Kingdon, 14-Aug-2025.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> F : ( M ... N ) --> B )   =>    |- ( ph -> ( G gsumg F ) = if ( N < M , .0. , ( seq M ( .+ , F ) ` N ) ) )
13-Aug-2025	znidom 14291	The ℤ/nℤ structure is an integral domain when n is prime. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by Jim Kingdon, 13-Aug-2025.)
|- Y = (ℤ/nℤ ` N )   =>    |- ( N e. Prime -> Y e. IDomn )
12-Aug-2025	rrgmex 13895	A structure whose set of left-regular elements is inhabited is a set. (Contributed by Jim Kingdon, 12-Aug-2025.)
|- E = (RLReg ` R )   =>    |- ( A e. E -> R e. _V )
10-Aug-2025	gausslemma2dlem1cl 15408	Lemma for gausslemma2dlem1 15410. Closure of the body of the definition of R. (Contributed by Jim Kingdon, 10-Aug-2025.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   &    |- ( ph -> A e. ( 1 ... H ) )   =>    |- ( ph -> if ( ( A x. 2 ) < ( P / 2 ) , ( A x. 2 ) , ( P - ( A x. 2 ) ) ) e. ZZ )
9-Aug-2025	gausslemma2dlem1f1o 15409	Lemma for gausslemma2dlem1 15410. (Contributed by Jim Kingdon, 9-Aug-2025.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- H = ( ( P - 1 ) / 2 )   &    |- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )   =>    |- ( ph -> R : ( 1 ... H ) -1-1-onto-> ( 1 ... H ) )
7-Aug-2025	qdclt 10354	Rational < is decidable. (Contributed by Jim Kingdon, 7-Aug-2025.)
|- ( ( A e. QQ /\ B e. QQ ) -> DECID A < B )
22-Jul-2025	ivthdich 14997	The intermediate value theorem implies real number dichotomy. Because real number dichotomy (also known as analytic LLPO) is a constructive taboo, this means we will be unable to prove the intermediate value theorem as stated here (although versions with additional conditions, such as ivthinc 14987 for strictly monotonic functions, can be proved). The proof is via a function which we call the hover function and which is also described in Section 5.1 of [Bauer], p. 493. Consider any real number z. We want to show that z <_ 0 \/ 0 <_ z. Because of hovercncf 14990, hovera 14991, and hoverb 14992, we are able to apply the intermediate value theorem to get a value c such that the hover function at c equals z. By axltwlin 8113, c < 1 or 0 < c, and that leads to z <_ 0 by hoverlt1 14993 or 0 <_ z by hovergt0 14994. (Contributed by Jim Kingdon and Mario Carneiro, 22-Jul-2025.)
|- ( A. f ( f e. ( RR -cn-> RR ) -> A. a e. RR A. b e. RR ( ( a < b /\ ( f ` a ) < 0 /\ 0 < ( f ` b ) ) -> E. x e. RR ( a < x /\ x < b /\ ( f ` x ) = 0 ) ) ) -> A. r e. RR A. s e. RR ( r <_ s \/ s <_ r ) )
22-Jul-2025	dich0 14996	Real number dichotomy stated in terms of two real numbers or a real number and zero. (Contributed by Jim Kingdon, 22-Jul-2025.)
|- ( A. z e. RR ( z <_ 0 \/ 0 <_ z ) <-> A. x e. RR A. y e. RR ( x <_ y \/ y <_ x ) )
22-Jul-2025	ivthdichlem 14995	Lemma for ivthdich 14997. The result, with a few notational conveniences. (Contributed by Jim Kingdon, 22-Jul-2025.)
|- F = ( x e. RR |-> sup ( {inf ( { x , 0 } , RR , < ) , ( x - 1 ) } , RR , < ) )   &    |- ( ph -> Z e. RR )   &    |- ( ph -> A. f ( f e. ( RR -cn-> RR ) -> A. a e. RR A. b e. RR ( ( a < b /\ ( f ` a ) < 0 /\ 0 < ( f ` b ) ) -> E. x e. RR ( a < x /\ x < b /\ ( f ` x ) = 0 ) ) ) )   =>    |- ( ph -> ( Z <_ 0 \/ 0 <_ Z ) )
22-Jul-2025	hovergt0 14994	The hover function evaluated at a point greater than zero. (Contributed by Jim Kingdon, 22-Jul-2025.)
|- F = ( x e. RR |-> sup ( {inf ( { x , 0 } , RR , < ) , ( x - 1 ) } , RR , < ) )   =>    |- ( ( C e. RR /\ 0 < C ) -> 0 <_ ( F ` C ) )
22-Jul-2025	hoverlt1 14993	The hover function evaluated at a point less than one. (Contributed by Jim Kingdon, 22-Jul-2025.)
|- F = ( x e. RR |-> sup ( {inf ( { x , 0 } , RR , < ) , ( x - 1 ) } , RR , < ) )   =>    |- ( ( C e. RR /\ C < 1 ) -> ( F ` C ) <_ 0 )
21-Jul-2025	hoverb 14992	A point at which the hover function is greater than a given value. (Contributed by Jim Kingdon, 21-Jul-2025.)
|- F = ( x e. RR |-> sup ( {inf ( { x , 0 } , RR , < ) , ( x - 1 ) } , RR , < ) )   =>    |- ( Z e. RR -> Z < ( F ` ( Z + 2 ) ) )
21-Jul-2025	hovera 14991	A point at which the hover function is less than a given value. (Contributed by Jim Kingdon, 21-Jul-2025.)
|- F = ( x e. RR |-> sup ( {inf ( { x , 0 } , RR , < ) , ( x - 1 ) } , RR , < ) )   =>    |- ( Z e. RR -> ( F ` ( Z - 1 ) ) < Z )
21-Jul-2025	rexeqtrrdv 2704	Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.)
|- ( ph -> E. x e. A ps )   &    |- ( ph -> B = A )   =>    |- ( ph -> E. x e. B ps )
21-Jul-2025	raleqtrrdv 2703	Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.)
|- ( ph -> A. x e. A ps )   &    |- ( ph -> B = A )   =>    |- ( ph -> A. x e. B ps )
21-Jul-2025	rexeqtrdv 2702	Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.)
|- ( ph -> E. x e. A ps )   &    |- ( ph -> A = B )   =>    |- ( ph -> E. x e. B ps )
21-Jul-2025	raleqtrdv 2701	Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.)
|- ( ph -> A. x e. A ps )   &    |- ( ph -> A = B )   =>    |- ( ph -> A. x e. B ps )
20-Jul-2025	hovercncf 14990	The hover function is continuous. By hover function, we mean a a function which starts out as a line of slope one, is constant at zero from zero to one, and then resumes as a slope of one. (Contributed by Jim Kingdon, 20-Jul-2025.)
|- F = ( x e. RR |-> sup ( {inf ( { x , 0 } , RR , < ) , ( x - 1 ) } , RR , < ) )   =>    |- F e. ( RR -cn-> RR )
19-Jul-2025	mincncf 14960	The minimum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 19-Jul-2025.)
|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> RR ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( X -cn-> RR ) )   =>    |- ( ph -> ( x e. X |-> inf ( { A , B } , RR , < ) ) e. ( X -cn-> RR ) )
18-Jul-2025	maxcncf 14959	The maximum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 18-Jul-2025.)
|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> RR ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( X -cn-> RR ) )   =>    |- ( ph -> ( x e. X |-> sup ( { A , B } , RR , < ) ) e. ( X -cn-> RR ) )
14-Jul-2025	xnn0nnen 10548	The set of extended nonnegative integers is equinumerous to the set of natural numbers. (Contributed by Jim Kingdon, 14-Jul-2025.)
|- NN0* ~~ NN
12-Jul-2025	nninfninc 7198	All values beyond a zero in an ℕ∞ sequence are zero. This is another way of stating that elements of ℕ∞ are nonincreasing. (Contributed by Jim Kingdon, 12-Jul-2025.)
|- ( ph -> A e. ℕ∞ )   &    |- ( ph -> X e. om )   &    |- ( ph -> Y e. om )   &    |- ( ph -> X C_ Y )   &    |- ( ph -> ( A ` X ) = (/) )   =>    |- ( ph -> ( A ` Y ) = (/) )
10-Jul-2025	nninfctlemfo 12234	Lemma for nninfct 12235. (Contributed by Jim Kingdon, 10-Jul-2025.)
|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- F = ( n e. om |-> ( i e. om |-> if ( i e. n , 1o , (/) ) ) )   &    |- I = ( ( F o. `' G ) u. { <. +oo , ( om X. { 1o } ) >. } )   =>    |- ( om e. Omni -> I :NN0* -onto->ℕ∞ )
8-Jul-2025	nnnninfen 15776	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 )
8-Jul-2025	nninfct 12235	The limited principle of omniscience (LPO) implies that ℕ∞ is countable. (Contributed by Jim Kingdon, 8-Jul-2025.)
|- ( om e. Omni -> E. f f : om -onto-> (ℕ∞ ⊔ 1o ) )
8-Jul-2025	nninfinf 10554	ℕ∞ is infinte. (Contributed by Jim Kingdon, 8-Jul-2025.)
|- om ~<_ ℕ∞
7-Jul-2025	ivthreinc 14989	Restating the intermediate value theorem. Given a hypothesis stating the intermediate value theorem (in a strong form which is not provable given our axioms alone), provide a conclusion similar to the theorem as stated in the Metamath Proof Explorer (which is also similar to how we state the theorem for a strictly monotonic function at ivthinc 14987). Being able to have a hypothesis stating the intermediate value theorem will be helpful when it comes time to show that it implies a constructive taboo. This version of the theorem requires that the function F is continuous on the entire real line, not just ( A [,] B ) which may be an unnecessary condition but which is sufficient for the way we want to use it. (Contributed by Jim Kingdon, 7-Jul-2025.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> F e. ( RR -cn-> RR ) )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ph -> A. f ( f e. ( RR -cn-> RR ) -> A. a e. RR A. b e. RR ( ( a < b /\ ( f ` a ) < 0 /\ 0 < ( f ` b ) ) -> E. x e. RR ( a < x /\ x < b /\ ( f ` x ) = 0 ) ) ) )   =>    |- ( ph -> E. c e. ( A (,) B ) ( F ` c ) = U )
28-Jun-2025	fngsum 13092	Iterated sum has a universal domain. (Contributed by Jim Kingdon, 28-Jun-2025.)
|- gsumg Fn ( _V X. _V )
28-Jun-2025	iotaexel 5885	Set existence of an iota expression in which all values are contained within a set. (Contributed by Jim Kingdon, 28-Jun-2025.)
|- ( ( A e. V /\ A. x ( ph -> x e. A ) ) -> ( iota x ph ) e. _V )
27-Jun-2025	df-igsum 12963	Define a finite group sum (also called "iterated sum") of a structure. Given G gsumg F where F : A --> ( Base ` G ), the set of indices is A and the values are given by F at each index. A group sum over a multiplicative group may be viewed as a product. The definition is meaningful in different contexts, depending on the size of the index set A and each demanding different properties of G. 1. If A = (/) and G has an identity element, then the sum equals this identity. 2. If A = ( M ... N ) and G is any magma, then the sum is the sum of the elements, evaluated left-to-right, i.e., ( ( F ` 1 ) + ( F ` 2 ) ) + ( F ` 3 ), etc. 3. This definition does not handle other cases. (Contributed by FL, 5-Sep-2010.) (Revised by Mario Carneiro, 7-Dec-2014.) (Revised by Jim Kingdon, 27-Jun-2025.)
|- gsumg = ( w e. _V , f e. _V |-> ( iota x ( ( dom f = (/) /\ x = ( 0g ` w ) ) \/ E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) ) ) )
20-Jun-2025	opprnzrbg 13819	The opposite of a nonzero ring is nonzero, bidirectional form of opprnzr 13820. (Contributed by SN, 20-Jun-2025.)
|- O = (oppr ` R )   =>    |- ( R e. V -> ( R e. NzRing <-> O e. NzRing ) )
16-Jun-2025	fnpsr 14301	The multivariate power series constructor has a universal domain. (Contributed by Jim Kingdon, 16-Jun-2025.)
|- mPwSer Fn ( _V X. _V )
14-Jun-2025	basm 12766	A structure whose base is inhabited is inhabited. (Contributed by Jim Kingdon, 14-Jun-2025.)
|- B = ( Base ` G )   =>    |- ( A e. B -> E. j j e. G )
14-Jun-2025	elfvm 5594	If a function value has a member, the function is inhabited. (Contributed by Jim Kingdon, 14-Jun-2025.)
|- ( A e. ( F ` B ) -> E. j j e. F )
6-Jun-2025	pcxqcl 12508	The general prime count function is an integer or infinite. (Contributed by Jim Kingdon, 6-Jun-2025.)
|- ( ( P e. Prime /\ N e. QQ ) -> ( ( P pCnt N ) e. ZZ \/ ( P pCnt N ) = +oo ) )