Skip to content

Shorten proofs of weiun* theorems #5004

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 1 commit into from
Sep 10, 2025
Merged

Shorten proofs of weiun* theorems #5004

merged 1 commit into from
Sep 10, 2025

Conversation

LegionMammal978
Copy link
Contributor

I haven't totally put the proof steps under a microscope, but at least weiunfr doesn't do an insane amount of rewriting anymore.

@wlammen wlammen merged commit 7ac8411 into metamath:develop Sep 10, 2025
10 checks passed
wlammen pushed a commit to wlammen/set.mm that referenced this pull request Sep 20, 2025
@LegionMammal978 @wlammen
Shorten proofs of weiun* theorems (metamath#5004)
3975a30
wlammen added a commit that referenced this pull request Sep 28, 2025
@wlammen @sctfn
@jkingdon @GinoGiotto @avekens @icecream17 @LegionMammal978 @zwang123 @EricSchmidt-119
reason why df-clab, df-cleq and df-clel should be reordered (#4993)
4fa6f6d 
* reason why df-cleq and df-clel are axioms

* text formatting issues

* typo

* keep checkers silent

* more label issues

* more label issues

* formulas are introduced, not statements

* typo

* some fine tuning

* typo

* add df-wl-clab

* wl-df-clab cannot be a definition with $a

* fine tune df-clab is definition

* fix formatting

* substitution corresponds to rewrite rule of a grammar

* production rule -> rewrite rule

* variables are non-terminal symbols

* fine tuning

* fix display of $

* delete spurious character

* fix issues reported by SN

* minor changes

* typo

* improve text

* improve text

* add theorems about small classes

* fix label

* improve text

* improve text

* improve text

* Surreal dyadic 2 (#4991)

* added addsbday

* shorten addsbday with addsbdaylem

* add addhalfcut

* add pw2cut

* begin working on even/odd theorems

* note move of naddsuc2

* add natural addition closure over _om

* finished zpw2fin

* rewrap

* got madefi and oldfi added

* added cutmax and cutmin

* improve naming consistency

* add missing DV conditions

* get rid of zpw2bday

* proved peano2ons

* added onaddscl, onmulscl, shortened peano2ons

* rewrap

* s/zsmulcld/zmulscld/

---------

Co-authored-by: Fenton <scott.fenton@hpe.com>

* add some basel prerequisites and notes in iset.mm (#4992)

* add fnfvof to mmil.html

* Add ofc1g and ofc2g to iset.mm

This is ofc1 and ofc2 from set.mm with an additional hypotheses
similar to the one in ofvalg .  The proofs are similar to the set.mm proofs.

* add caofass to mmil.html

* Add caofdig to iset.mm

This is caofdi from set.mm with set existence conditions added.  The
proof is similar to the set.mm proof.

* add caofdir to mmil.html

* add caonncan to mmil.html

* Add ofnegsub to iset.mm

Stated as in set.mm.  The proof is the set.mm proof but with changes in
various places for differences in oF theorems.

* Add irrmulap to iset.mm

This is irrmul but with irrational in place of not rational.  The proof
follows without much difficulty from existing theorems including apdivmuld .

* Add sinltxirr to iset.mm

This is sinltx from set.mm but just for irrational numbers.  The proof
is by considering the A < 1 and 1 < A cases in turn.

* add df-ply to mmil.html

* add df-idp to mmil.html

* add df-coe to mmil.html

* Add df-dgr to mmil.html

* Add vieta1 to mmil.html

* Add fta1 to mmil.html

* Add notes about basel to mmil.html

This is basellem1 , basellem2 , basellem3 , basellem4 ,
basellem5 , basellem6b , basellem7 , basellem8 , basellem9 , and
basel

* Prove ax-8 from df-ss (#4995)

* ax-8 from df-ss

* discouraged

* add mvth to mmil.html (#4996)

* Intuitionize gsumreidx (#4997)

* Add seqfveq2g to iset.mm

This is seqfveq2 from set.mm with set existence conditions added.
The proof is the set.mm proof with only small changes for set existence.

* Add seqfveqg to iset.mm

This is seqfveq from set.mm with set existence conditions added.  The
proof is the set.mm proof with small changes for set existence.

* Add seqsplitg to iset.mm

This is seqsplit from set.mm with set existence conditions added.  The
proof is the set.mm proof with small changes for set existence.

* Add seqshft2g to iset.mm

This is seqshft2 from set.mm with set existence conditions added.  The
proof is the set.mm proof with a few small changes for set existence.

* add change bound variable theorems to iset.mm

This is cbvaldvaw , cbvexdvaw , cbval2vw , and cbvex2vw .
Stated as in set.mm including the same distinct variables, but proofs
and axiom usage may be different.

* Add seqm1g to iset.mm

This is seqm1 from set.mm with set existence conditions added.  The
proof is from seq3m1 .

* Add seqf1og to iset.mm

This is similar to seq3f1o in iset.mm and seqf1o in set.mm but the
conditions are slightly different.  The proof, including lemmas,
is the set.mm proof with changes in various places for set existence,
decidability of various propositions, and differences in seq theorems.

Includes lemmas seqf1oglem2a , seqf1oglem1 , and seqf1oglem2 which
are based on seqf1olem2a , seqf1olem1 , and seqf1olem2 from set.mm.

* Add gsumfzreidx to iset.mm

The statement of the theorem is gsumreidx in set.mm with the addition of
conditions that M and N are integers.  The proof is a new one from
gsumfzval and seqf1og .

* Misc cbv* and equality theorems (#4998)

* add equality theorems

* tweaks

* typo

* Add lgseisenlem3 to iset.mm (#4999)

* Add gsumfzsubmcl to iset.mm

This is gsumsubmcl from set.mm with some changes to the hypotheses.
The proof is a new one from gsumfzval , seqclg , and various monoid
theorems.

* Add seqcaopr3g to iset.mm

This is seqcaopr3 from set.mm with set existence conditions added.  The
proof is the set.mm proof except that it uses seq1g and seqp1g in place
of seq1 and seqp1 .

* Add seqcaopr2g to iset.mm

This is seqcaopr2 from set.mm with additional set existence conditions.
The proof is the set.mm proof changed to supply set existence conditions
to various seq theorems.

* Add seqcaoprg to iset.mm

This is seqcaopr from set.mm with set existence conditions added.  The
proof is the set.mm proof with the only change being to use seqcaopr2g
in place of seqcaopr2 .

* Add gsumfzmptfidmadd to iset.mm

This is gsummptfidmadd from set.mm but where the group sum needs to be
indexed by consecutive integers.  The proof is a new one based on
gsumfzval , seqcaoprg , and various monoid theorems.

* Add gsumfzmptfidmadd2 to iset.mm

This is gsummptfidmadd2 from set.mm where the sum is indexed by
consecutive integers.  The proof is via offval2 and gsumfzmptfidmadd

* Add lgseisenlem3 to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with changes for set
existence, for differences in gsum theorems, to use znidom in place
of znfld , to use apartness in place of not equal, to use rationals
rather than reals in modulus theorems, and to use znunit plus coprm
in place of drngunit .

* Graphs being locally isomorphic but not isomorphic (2) (#4990)

* Local isomorphisms map triangles onto triangles

*  theorems moved from mathboxes to main: ~elrab2w,  ~elab2gw, ~elabgw, ~3rspcedvdw, ~fimarab
* new theorems in main: ~rexlimdvvva, ~f1ocoima
* new auxiliary theoems in AV's mathbox: ~3f1oss1, ~3f1oss2
* new theorems for closed neighborhoods in AV's mathbox: ~predgclnbgrel, ~clnbgredg, ~clnbgrssedg
* typo detected by GL fixed in section header "Triangles in graphs"
* new theorems for triangles in AV's mathbox: ~grtrimap
* new theorems for local isomorphisms between grahs in AV's mathbox: ~uspgrlim  (and lemmas), ~usgrlimprop, ~grlimgrtri

* Proof of ~grimgrtri shortened

* The example graphs ` H ` and ` G ` are not locally isomorphic

* Rewrap, lemmas renumbered

* delete outdated OLD theorems (#5002)

* sbbiiev + save ax-11 in sbco4 + misc trig (#5000)

* add and use sbbiiev

* misc unit circle identities + utils
+ shorten nfa1w

in particular lttrii seems to replace most uses of lttri

* fixes, prove tanhalfpim

* move cbvabv sbco4 up, save ax-11 in sbco4, rewrap

* Add Poly to iset.mm (#5003)

* Add Poly and Xp to iset.mm

This is the syntax, df-ply , and df-idp .  Copied without change from
set.mm.

* Revise mmil.html entries for df-coe and df-dgr

This is to clarify how we approach the coefficients and degree of a
polynomial.

* add plyco0 to mmil.html

* Add plyval to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with a number of
changes for set existence.

* copy plybss from set.mm to iset.mm

* Add elply to iset.mm

This is copied from set.mm and although I ended up sending the proof
through mmj2 I didn't need to change anything.

* copy ifexg from set.mm to iset.mm

* Add ifex to iset.mm

Stated as in set.mm.  The proof is from ifexg .

* add elply2 to mmil.html

* copy plyun0 from set.mm to iset.mm

* Add plyf to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with one small
change for differences in finiteness.

* Add plyss to iset.mm

Stated as in set.mm.  I loaded and saved the proof in mmj2 but didn't
need to otherwise edit it.

* Add plyssc to iset.mm

Stated as in set.mm.  The proof is based on the set.mm proof but needs
to have some logic rearranged.

* copy elplyr from set.mm to iset.mm

* Add elplyd to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with a small change
to show one proposition is decidable.

* Add ply1term to iset.mm

Stated as in set.mm.  The proof, including for the lemma ply1termlem ,
is the set.mm proof with small changes for decidability and
finite set theorems.

* copy plypow from set.mm to iset.mm

* copy plyconst from set.mm to iset.mm

* Add df-0p and ne0p to mmil.html

* add ply0 to mmil.html

* Copy opabresid and mptresid from set.mm to iset.mm

This flips the two sides of the equality.

Update the five proofs which use mptresid .

This changed in set.mm in 2023 so this change is to get closer
alignment between set.mm and iset.mm.

* copy plyid from set.mm to iset.mm

* add plyeq0 to mmil.html

* add plypf1 to mmil.html

* copy mptima and mptimass from set.mm to iset.mm

* add rnmptc to mmil.html

* Add elply2 to iset.mm

Stated as in set.mm.  The proof is the set.mm proof except:

* a small change for set existence
* a rewrite of the part of the proof which had used plyco0 , to use
  theorems including mptima , fconstmpt , and rnxpm instead.
* proving decidability when working with if

* Add plyaddlem1 to iset.mm

Stated as in set.mm.  The proof is the set.mm proof except for changes
for differences in sum and maximum theorems.

* Add plymullem1 to iset.mm

Stated as in set.mm.  The proof is the set.mm theorem with changes for
differences in sum and finite set theorems.

* Add plyaddlem to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with one small
change to show that a proposition is decidable.

* Add plymullem to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with small changes
for differences in sum and integer range theorems.

* copy plyadd from set.mm to iset.mm

* copy plymul from set.mm to iset.mm

* copy plysub from set.mm to iset.mm

* copy plyaddcl from set.mm to iset.mm

* copy plymulcl from set.mm to iset.mm

* copy plysubcl from set.mm to iset.mm

* Wording fix to plyf comment

"The" -> "A"

* Shorten proofs of weiun* theorems (#5004)

* Add two more existence examples to mmil.html (#5006)

* Add two more existence examples

1. The existence of coefficients, given a polynomial.

2. The existence of a rate of convergence, given a
sequence known to converge.

* Update mmil.raw.html

Co-authored-by: Steven Nguyen <icecream17.github@gmail.com>

* Remove sentence about isset / truncated existence

It seems like isset would also apply in a situation of explicit
existence.

---------

Co-authored-by: Steven Nguyen <icecream17.github@gmail.com>

* Add lgseisenlem4 to iset.mm (#5010)

* add gsumzsubmcl to mmil.html

* add gsumsubgcl to mmil.html

* add gsumzaddlem , gsumzadd , gsumadd to mmil.html

* add gsummptfsadd to mmil.html

* add gsum split theorems to mmil.html

This is gsumzsplit , gsumsplit , gsumsplit2 , gsummptfidmsplit ,
gsummptfidmsplitres , gsummptfzsplit , and gsummptfzsplitl

* Add gsumfzconst to iset.mm

This is gsumconst from set.mm where the sum is indexed by consecutive
integers.  The proof is a new one by induction.

* add gsumconstf to mmil.html

* add gsummptshft to mmil.html

* Add gsumfzmhm to iset.mm

This is gsummhm from set.mm but where the sum is indexed by consecutive
integers.  The proof is from gsumfzval , seqhomog , and some monoid
theorems.

* Add gsumfzmhm2 to iset.mm

This is gsummhm2 from set.mm where the sum is indexed by
consecutive integers.  The proof is similar to the set.mm proof.

* Add gsumfzconstf to iset.mm

This is gsumconstf from set.mm but indexed by consecutive integers.  It
is also gsumfzconst from iset.mm but with a freeness hypothesis in place
of distinct variables.  The proof is similar to the set.mm proof of
gsumconstf .

* Add gsumfzsnfd to iset.mm

This is gsumsnfd from set.mm except that M has to be an integer.
Naming this similarly to the other gsumfz* theorems seems more
appealing than trying to use a different convention.

The proof is similar to the set.mm proof.

* Add gsumsnd , gsumsnf , gsumsn to mmil.html

* add gsumpr to mmil.html

* Add mpocnfldadd to iset.mm

Stated as in set.mm.  This is provided for compatibility with set.mm but
at least so far makes no effort to reduce axiom usage.  The proof is
based on the set.mm proof of cnfldadd .

* Add gsumfzfsum to iset.mm

This is gsumfsum from set.mm but where the sums are indexed by
consecutive integers.

As with the set.mm proof the proof separates the empty case (lemma
gsumfzfsumlem0 ) from the inhabited case (lemma gsumfzfsumlemm ,
here proved by induction which is perhaps simpler than trying to adapt
theorems like fsum3 ).

* Add submmulg to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with one small
change in extensible structure theorems.

* Add mpocnfldmul to iset.mm

Stated as in set.mm.  At least for now, this uses the same complex
number axioms as cnfldmul .  The proof is from ax-mulf and cnfldmul .

* Add cnfldui to iset.mm

This is similar to drngui from set.mm but for CCfld in particular, not
division rings in general.  The proof is a new one from crngunit ,
dvdsrd , and recapb .

* Add expghmap to iset.mm

This is expghm from set.mm with not equal changed to apart.  The proof
is basically the set.mm proof but needs changes of not equal to apart
and other intuitionizations on most steps.

* Add lgseisenlem4 to iset.mm

Stated as in set.mm.  The proof is basically the set.mm proof but
requires intuitionizing in many places for a variety of reasons.
Remove one sentence from the comment in set.mm (which seemed to be an
incorrect copy-paste from lgseisenlem2 ).

* remove hypotheses in mhp* (#5008)

* remove hypotheses in mhp*

* remove dvs with unused variables

* Add equality deductions for relation predicates to main (#5007)

Co-authored-by: Wolf Lammen <30736367+wlammen@users.noreply.github.com>

* [add] assa2ass2; [shorten] assa2ass (#5009)

* Fix typo in mmil.html (gets->get) (#5013)

* Add mathbox for Eric Schmidt (#5011)

* Add mathbox for Eric Schmidt with some initial theorems

* Add bibliographic references, use M for 'model' in traxext

* Minor formatting change

* Fix markup mistakes

* Add $j statements for avoiding ax-ref

* Fix typo

* Remove duplicate lines

* add unique choice to iset.mm (#5012)

* copy opelopabgf from set.mm to iset.mm

* Add uchoice to iset.mm

We have things sort of like this, but I didn't see anything which states
it quite in a form which might merit the name "unique choice".

* add lgseisen and lgsquadlem1 to iset.mm (#5014)

* Add lgseisen to iset.mm

Stated as in set.mm.  The proof is basically the set.mm proof but needs
intuitionizing in a variety of ways in a number of places.

* copy relopabiv from set.mm to iset.mm

The only change is to the comment to reflect differences in the axioms.

* copy relopabv from set.mm to iset.mm

The only change is to the comment, to reflect differences in the axioms.

* Add opabidw to iset.mm

Stated as in set.mm (including the same distinct variables).  The proof,
however, just uses opabid because the set.mm proof is not easily
adapted.

* copy opelopabgf from set.mm to iset.mm

* Add opabfi to iset.mm

This is a variation of ssfidc but designed to be more specific when used
with an ordered pair abstraction.

* Add lgsquadlem1 to iset.mm

Stated as in set.mm.  The proof is basically the set.mm proof but
various places need changes for decidability, modulus theorems, and
other differences.

* fix opabidw comment

* improve texts

* fix grammar issues

* more fixes

* typos and minor improvements

* minor clarification

* rewrap

* minor wording fixes

* eliminability of a general class variable

* typo

* add a disclaimer

* add preface

* fix a phrase

* typo

---------

Co-authored-by: Scott Fenton <sctfen@gmail.com>
Co-authored-by: Fenton <scott.fenton@hpe.com>
Co-authored-by: Jim Kingdon <kingdon@panix.com>
Co-authored-by: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Co-authored-by: avekens <avekens@yahoo.de>
Co-authored-by: Steven Nguyen <icecream17.github@gmail.com>
Co-authored-by: Matthew House <mattlloydhouse@gmail.com>
Co-authored-by: zwang123 <zhiwang.pku@gmail.com>
Co-authored-by: Eric Schmidt <erics41293@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@avekens avekens avekens approved these changes

+1 more reviewer

@icecream17 icecream17 icecream17 approved these changes

Reviewers whose approvals may not affect merge requirements
Assignees
No one assigned
Labels
mathbox only
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@LegionMammal978 @avekens @icecream17 @wlammen