[Metamath] Re: question about fsumshft

t; Olivier > > > Le samedi 2 novembre 2019 00:33:58 UTC+1, Norman Megill a écrit : >> >> By using one less dummy variable, I found a shorter proof that might be >> easier to understand, updated at >> >> http://us2.metamath.org/mpeuni/fsumshftd.html >&

[Metamath] Re: question about fsumshft

. Of particular interest is the use of csbied at step 22, which, using the new (weaker) hypothesis fsumshftd.5, gives us [_ ( k - K ) / j ]_ A = B to get rid of the explicit substitution on A and result in B. Norm On Friday, November 1, 2019 at 1:27:50 PM UTC-4, Norman Megill wrote: > > Gettin

[Metamath] When to use a "ph ->" antecedent in a deduction form

(This continues the thread "question about fsumshft" https://groups.google.com/d/msg/metamath/vt6SqLrxEfo/t8WbKnW4DgAJ but is more general, so I am starting a new thread.) A general issue raised by the previous thread is our convention for when we should or shouldn't use "ph ->" as an

[Metamath] Re: question about fsumshft

Getting back to your original question, we can prove fsumshft with your modified (weaker) fsumshft.5 starting from directly from fsumshft with the stronger fsumshft.5. I show a proof here: http://us2.metamath.org/mpeuni/fsumshftd.html To summarize the proof, we use csbeq1 at step 15 to

[Metamath] Re: Future directions

On Thursday, October 31, 2019 at 1:38:28 PM UTC-4, ookami wrote: > > Now that Christmas is approaching, I would love to come up with my personal > wish list, that I slowly gathered over the past years. Okay, I am not > going to > command others here to fulfil my needs. But maybe, one or the

[Metamath] Re: question about fsumshft

On Wednesday, October 30, 2019 at 6:47:24 AM UTC-4, Olivier Binda wrote: > > After considering things through, I understand what > Norman/Alexander/Giovani were saying : > some hypothesis are just there to allow the theorem to do it's > (verification) job. And are not really "needed", when you

[Metamath] Re: question about fsumshft

fsumshft.5 doesn't have a "ph ->" antecedent because its purpose is simply to specify that B is a substitution instance of A. We sometimes call this "implicit substitution" as opposed to "explicit substitution", which would be B = [. ( k - K ) / j ]. A (or just using [. ( k - K ) / j ]. A in

Re: [Metamath] DNS event

On Thursday, October 24, 2019 at 11:21:58 AM UTC-4, Benoit wrote: > > Now that it's back to normal, I have two naive questions: > > 1) Isn't the purpose of mirror sites to serve as replacements when an > event like this occurs ? However, during the event, it seems the mirror > sites were

Re: [Metamath] DNS event

I have tried to reach domainmonger.com via phone, both of their numbers, and left urgent messages about my support ticket asking them to call me on the phone. There is no way to reach a human. They will close in 40 minutes based on the hours posted on their site. David, could you see if

Re: [Metamath] DNS event

Forget that. Yahoo won't let me log in without verifying via n...@alum.mit.edu, which doesn't work now. I'll check this group for any messages for me. Norm On Wednesday, October 23, 2019 at 5:37:59 PM UTC-4, Norman Megill wrote: > > An alternate email that I normally don't check i

Re: [Metamath] DNS event

An alternate email that I normally don't check is nmeg...@yahoo.com. On Wednesday, October 23, 2019 at 5:30:08 PM UTC-4, Norman Megill wrote: > > David has alerted me to this. > > I opened a ticket with the DNS provider. I have no idea what is > happening. I checked the

Re: [Metamath] DNS event

David has alerted me to this. I opened a ticket with the DNS provider. I have no idea what is happening. I checked the DNS setup form on their site and everything looks fine. The service is provided by domainmonger.com, and metamath.org is paid for through 02/04/2020. The last change I made

[Metamath] Re: How to encode first-order logic without equality in Metamath

It seems you are asking several things, let's back up a little. It might help if you explain a little more what your application is, and why equality is not desirable, since you have to go through some hoops to eliminate it and still have a complete FOL. In most systems of practical interest,

[Metamath] Re: [set.mm] The conditional operator for propositions

On Saturday, October 5, 2019 at 6:53:27 AM UTC-4, Benoit wrote: > > Hi all, > > A few months ago, I added the "conditional operator for propositions" to > my mathbox (currently Section 21.29.1.6, beginning at > http://us2.metamath.org/mpeuni/wif.html). I propose to move it to the > main part

Re: [Metamath] Re: New Gource visualization of set.mm

On Saturday, October 5, 2019 at 1:00:27 PM UTC-4, David A. Wheeler wrote: > > On Sat, 5 Oct 2019 09:03:45 -0700 (PDT), Benoit wrote: > ... > > It's a bit strange that at around 0:01, the image blows out of frame: we > > lose some information (even if some might like the "big bang effect" > this

Re: [Metamath] Major Metamath set.mm past events?

On Friday, October 4, 2019 at 6:05:57 PM UTC-4, David A. Wheeler wrote: > > Here's what set.mm currently says about df-pi: > > $( Define pi = 3.14159..., which is the smallest positive number whose > sine >is zero. Definition of pi in [Gleason] p. 311. (We use the > inverse of >

[Metamath] Re: Verifying nnawordi / omssadd history

I commented on this case at https://github.com/metamath/set.mm/pull/1141#issuecomment-537664085 Essentially both dates are Scott Fenton's, and the 2nd date should probably be removed for the reasons discussed there. Also note that in early set.mm's, there were no acknowledgments in mathboxes,

[Metamath] Re: 'minimize_with' command in metamath.exe

I added links to "How can I contribute to Metamath?" ( http://us2.metamath.org/index.html#contribute ) near the top of these pages: http://us2.metamath.org/mpeuni/mmset.html http://us2.metamath.org/mpeuni/mmrecent.html I also added links to the wiki

[Metamath] 'minimize_with' command in metamath.exe

*1. Changes to 'minimize_with'* As noted on the 10-Aug-2019 news item on the Most Recent Proofs page http://us2.metamath.org/mpeuni/mmrecent.html the behavior of the 'minimize' command has been changed. Before the change, 'minimize *' with no

[Metamath] Re: Help with Table of Contents links in Chrome browser

. Chrome isn't my primary browser and I'm not familiar with their community. Norm On Friday, November 2, 2018 at 8:29:19 PM UTC-4, Norman Megill wrote: > > On Tuesday, October 23, 2018 at 1:39:25 PM UTC-4, Norman Megill wrote: >> >> After I added the anchors for linking to TOC headers

[Metamath] Re: Updates of the "us" and "us2" servers

On Friday, August 23, 2019 at 9:30:24 AM UTC-4, Benoit wrote: > > Thanks Norm for the "/old" repository. By the way, the "tensions" about > the pace of updating reminded me of this cartoon: > https://abstrusegoose.com/531 where mathematics and computer programming > occupy the two opposite

[Metamath] Re: Updates of the "us" and "us2" servers

On Wednesday, August 21, 2019 at 9:47:11 PM UTC-4, Norman Megill wrote: >All us2 queries to us2.metamath.org:88/old/. <http://us2.metamath.org:88/old/>.. will be a previous version of us2.metamath.old:88/... should be All us2 queries to us2.metamath.org:88/old/. <http://us2.met

[Metamath] Re: Updates of the "us" and "us2" servers

Right now I initiate mirror updates manually by renaming a cache directory (copy of the most recent us2 site build) to become the rsync directory. Within 24 hours of doing that, the mirrors are updated, depending on the timing of their daily cron jobs. Usually I do this cache renaming within a

[Metamath] Re: ex-natded5.3i used on minimize

On Tuesday, August 20, 2019 at 12:36:53 PM UTC-4, Alexander van der Vekens wrote: > > It's the second time now I got ex-natded5.3i into my proof on minimize! > > Since it seems that this is a very useful theorem, I want to propose to > put it into the first part of set.mm (maybe after ~ jctir),

[Metamath] Re: Updates of the "us" and "us2" servers

While it is possible to delay the update of the mirrors by any number of days, I don't know if it's a good idea. I want us.metamath.org to be the main site that the general public uses, and it needs to be updated relatively quickly when for example we announce a new mm100 theorem. I attempt

Re: [Metamath] Trying to generalize David Wheeler's Algebra helpers.

On Friday, August 9, 2019 at 5:01:46 PM UTC-4, David A. Wheeler wrote: > > On Fri, 9 Aug 2019 13:49:49 -0700 (PDT), Jon P wrote: > > I used mvllmuld as the final step of this proof > >

[Metamath] Re: ex-natded5.3i used on minimize

On Wednesday, August 7, 2019 at 10:07:46 AM UTC-4, Alexander van der Vekens wrote: > > After minimizing a proof (min */ver) of a theorem within my Mathbox I > observed that the theorem ex-natded5.3i was used to shorten my proof. I > wonder if this should happen or actually be allowed, because

[Metamath] Metamath page on Wikipedia

The content of https://en.wikipedia.org/wiki/Metamath is somewhat outdated and doesn't reflect the current focus. Since I am mentioned several times on the page, I have chosen not to edit it myself because it would feel like a conflict of interest. But anyone else is welcome to update it.

[Metamath] Re: Proving quadratic equation formula without delta with complex coefficients and with complex X

I, too, am puzzled by this. My initial though was that maybe it could be done via complex exponentiation, which relates to the sqr function for all complex numbers via ~ cxpsqr. However, ~ divcxp accepts only nonnegative real arguments for the ratio terms (although the exponent can be

[Metamath] Re: Metamath Search Engine

Nice work! Thanks for fixing "MetaMath" -> "Metamath". :) (The former sometimes gets confused w/ Chaitin's book.) I agree w/ David that the XITS web fonts would look nicer, and it would also match the main site.. One problem with infinite scrolling is if there are many matches, it can be

Re: [Metamath] Re: unbundling set.mm

On Wednesday, June 19, 2019 at 10:49:46 PM UTC-4, Mario Carneiro wrote: > > ... > You seem to be suggesting a massive revision and complication of set.mm with a nonstandard notation, I assume in order to make it easier to translate to type theory. Let's look at df-ral: > One unsightly thing

Re: [Metamath] Re: RFC: Mandatory definitions after constants

On Sunday, June 16, 2019 at 1:35:04 AM UTC-4, Mario Carneiro wrote: > > > I would like to renew my suggestion that we change these to ax-bi, >>> ax-clab, ax-cleq, ax-clel. It adds complexity to the tooling to have an >>> inconsistent naming convention, since we are signaling that these are >>>

Re: [Metamath] Re: RFC: Mandatory definitions after constants

rewritten, is this a good time to change the definition of T. to be A. x x = x <-> A. x x = x? You mentioned that there is a special section for df-tru, and it could be eliminated if we make this change. On Fri, Jun 14, 2019 at 1:30 PM Norman Megill wrote: > The four definitions df-bi

[Metamath] Re: RFC: Mandatory definitions after constants

I can go along with this. My first question is, how will it be checked? Can the mmj2 definition check be modified to ensure it? Norm On Friday, June 14, 2019 at 8:55:10 AM UTC-4, Mario Carneiro wrote: > > Hi All, > > This is a fairly irrelevant looking change, but it does affect most of the

Re: [Metamath] Area of a triangle

On Monday, June 10, 2019 at 7:41:30 AM UTC-4, Thierry Arnoux wrote: > > Actually, in this case, you can just skip your steps 78 and 79: > > 80:77:ss2abdv |- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) > -> { x | ( x e. ( A (,] B ) /\ x e. ( B [,) C ) ) } > C_ { x | x e. ( B [,] B ) } ) >

[Metamath] Re: The distinctness of dummy variables

In Sec. 4.1.4 under "Verifying Disjoint Variable Restrictions", it says: "Second, each possible pair of variables, one from each expression, must exist in an active $d statement of the $p statement containing the proof." The word "active" in "active $d statement" means either a "mandatory" or

[Metamath] Metamath book cover

The Metamath book cover proposed by David is here: https://dwheeler.com/misc/24804269_cover.pdf The cover logo aleph is a slightly different shape from our standard logo, since David used another source to get a clean (non-jagged) font. Here is the largest standard logo we have, which is

Re: [Metamath] How to do substitutions in Metamath?

On Sunday, June 2, 2019 at 1:31:34 PM UTC-4, Norman Megill wrote: > > On Sunday, June 2, 2019 at 12:52:21 PM UTC-4, Tony wrote: >> >> On Sunday, June 2, 2019 at 6:02:30 PM UTC+2, Norman Megill wrote: >> >> We have been calling [. A / x ]. ph "explicit" (beca

Re: [Metamath] How to do substitutions in Metamath?

On Sunday, June 2, 2019 at 12:52:21 PM UTC-4, Tony wrote: > > On Sunday, June 2, 2019 at 6:02:30 PM UTC+2, Norman Megill wrote: > > We have been calling [. A / x ]. ph "explicit" (because it has an explicit >> substitution symbol) and "x = A -> ( ph <-> p

Re: [Metamath] How to do substitutions in Metamath?

On Sunday, June 2, 2019 at 6:44:56 AM UTC-4, Tony wrote: > > I don't understand how to handle substitutions in Metamath. If I use > > stdpc7 ⊢ (푥 = 푦 → ([푥 / 푦]휑 → 휑)), > > how do I then actually change y to x in 휑? > > I don't see any suitable theorems to use. Like for instance: > > [푥 / 푦] (휑 ↔

Re: [Metamath] Removing dependencies on some logically redundant axioms

On Tuesday, May 28, 2019 at 12:10:24 PM UTC-4, Benoit wrote: > > On Tuesday, May 28, 2019 at 6:02:38 PM UTC+2, Mario Carneiro wrote: >> >> I'm okay with the alternative df-bj-nf definition. If the use of the >> definition E. is undesirable, here are some more alternatives: >> >> $a |- ( F/1 x ph

<    1   2   3