Groups keyboard shortcuts have been updated
Dismiss
See shortcuts

Question about a specific problem probably unrelated with metamath

334 views
Skip to first unread message

jagra

unread,
Jul 28, 2024, 2:07:46 PM7/28/24
to Metamath
Understand this is not a common, and probably not even wanted, topic on this group.

Trying to translate to metamath a simple problem from AIMO train dataset, just out of curiosity.

The problem statement is:

Let $k, l > 0$ be parameters. The parabola $y = kx^2 - 2kx + l$ intersects the line $y = 4$ at two points $A$ and $B$. These points are distance 6 apart. What is the sum of the squares of the distances from $A$ and $B$ to the origin?

Trying to come up a direct construction of the conditions and statement to prove and blocking, from my ignorance most certainly, on some embarassing road blocks.

  1. Define function y=4
  2. Define parabola function in terms of k and l
  3. Connect 1 & 2 with points A and B
  4. Define distance between A and B
  5. Define the goal in terms of A and B
Really understand this is probably a basic question and I'm offsetting my due dilligence, so, no problem if no one takes the time to answer this :)

Best regards,
Jorge Agra  

Mario Carneiro

unread,
Jul 28, 2024, 2:24:41 PM7/28/24
to meta...@googlegroups.com
I would do something like this (which is not exactly metamath syntax but not too hard to write precisely):

0 < k,
0 < l,
F = (x e. RR |-> k*x^2 - 2*k*x + l),
{ x | F(x) = 4 } = {A, B},
(A - B)^2 + (F(A) - F(B))^2 = 6
|- (A^2 + F(A)^2) + (B^2 + F(B)^2) = ?

although to actually prove it you have to first fill in the ? with the answer.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/6f644425-c9fd-4516-b8f3-76b104c2be4fn%40googlegroups.com.

jagra

unread,
Jul 28, 2024, 4:03:17 PM7/28/24
to Metamath
Thank you for feedback.

Your last comment touched a very relevant point.

From a tooling perspective, mmj2 for instance, do you think it would be possible to replace the ? for a &C1 and work on some proof elaboration steps that will produce the value for &C1, eventually promoting it to a hyp? 

Best regards.

Mario Carneiro

unread,
Jul 28, 2024, 4:05:18 PM7/28/24
to meta...@googlegroups.com
Yes, you can certainly state that as a subgoal in mmj2 (with a &C1 work variable) and try to prove it, and when you get to the end and know what it has been assigned to you can edit the theorem statement to use the correct value.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/b3b85824-1085-470e-848a-45e2b751f267n%40googlegroups.com.

Glauco

unread,
Jul 28, 2024, 5:43:54 PM7/28/24
to Metamath
I maybe wrong, but my feeling is that what Jagra calls A , in Mario's translation is actually < A , 4 >   (or < A, F(A) > , if you prefer).

And Jagra's B , is actually Mario's < B , 4 >

If that's the case, an adaptation could be

{ x | F(x) = 4 } = { ( 1st ` A ) ,  ( 1st ` B ) }

and the other formulas should be similarly adapted.

To simplify a bit, you could use 4 in place of F(A) and F(B), thus, for instance, Mario's

(A - B)^2 + (F(A) - F(B))^2 = 6

would become

( ( 1st ` A ) -  ( 1st ` B ) )^2 = 6

because (F(A) - F(B))^2 is zero

Mario Carneiro

unread,
Jul 28, 2024, 5:54:47 PM7/28/24
to meta...@googlegroups.com
On Sun, Jul 28, 2024 at 11:43 PM Glauco <glaform...@gmail.com> wrote:
I maybe wrong, but my feeling is that what Jagra calls A , in Mario's translation is actually < A , 4 >   (or < A, F(A) > , if you prefer).

I meant it to be interpreted as <A, F(A)>, and part of the proof would be showing that F(A) = 4 so that the rest of the statement simplifies. (But that would seem to be part of the proof, not the formalization of the statement, if we want to read it literally.)

Igor Ieskov

unread,
Oct 14, 2024, 6:40:47 AM10/14/24
to Metamath

I wanted to check how far I can get in formalizing this problem and its solution. But I stuck in the very beginning.


Firstly, I formalized the initial conditions as Mario suggested:


hyp1: |- 0 < k

hyp2: |- 0 < l

hyp3: |- F = ( x e. RR |-> ( ( ( k x. ( x ^ 2 ) ) - ( ( 2 x. k ) x. x ) ) + l ) )

hyp4: |- { x | ( F ` x ) = 4 } = { a , b }

hyp5: |- ( ( ( a - b ) ^ 2 ) + ( ( ( F ` a ) - ( F ` b ) ) ^ 2 ) ) = ( 6 ^ 2 )

hyp6: |- ( ( ( a ^ 2 ) + ( ( F ` a ) ^ 2 ) ) + ( ( b ^ 2 ) + ( ( F ` b ) ^ 2 ) ) ) = c


I used { a , b } instead of { A , B } because then I can easily prove |- a e. _V, which is used in the proof below. Also, as I understand, a and b represent x-coordinates of the corresponding points.


Next, I wanted to simplify hyp5, by proving that F(a) = F(b) = 4, so the hyp5 would be |- ( ( a - b ) ^ 2 ) = ( 6 ^ 2 ). But that’s where I am stuck. I can prove |- [ a / x ] ( F ` x ) = 4 which looks a right direction to move in:


1|     | vex     | |- a e. _V

2| 1   | prid1   | |- a e. { a , b }

3|     | hyp4    | |- { x | ( F ` x ) = 4 } = { a , b }

4| 3   | eleq2i  | |- ( a e. { x | ( F ` x ) = 4 } <-> a e. { a , b } )

5| 2,4 | mpbir   | |- a e. { x | ( F ` x ) = 4 }

6|     | df-clab | |- ( a e. { x | ( F ` x ) = 4 } <-> [ a / x ] ( F ` x ) = 4 )

7| 5,6 | mpbi    | |- [ a / x ] ( F ` x ) = 4


But I still cannot prove |- ( F ` a ) = 4. Any suggestions what approaches I can try to prove this?

Glauco

unread,
Oct 14, 2024, 7:42:45 AM10/14/24
to Metamath
Hi Jorge,

with Yamma you get something like this  (I doubt you can get away with { x | ( F ` x ) = 4 }, for instance ( F ` +oo ) is not "well-defined" )

```
$theorem temp3

* comments

h1::temp3.1           |- { x e. RR | ( F ` x ) = 4 } = { a , b }
2::fveq2               |- ( x = a -> ( F ` x ) = ( F ` a ) )
3:2:eqeq1d            |- ( x = a -> ( ( F ` x ) = 4 <-> ( F ` a ) = 4 ) )
4:3:elrab            |- ( a e. { x e. RR | ( F ` x ) = 4 } <-> ( a e. RR /\ ( F ` a ) = 4 ) )
5::vex                 |- a e. _V
6:5:prid1             |- a e. { a , b }
7:6,1:eleqtrri       |- a e. { x e. RR | ( F ` x ) = 4 }
8:7,4:mpbi          |- ( a e. RR /\ ( F ` a ) = 4 )
qed:8:simpri       |- ( F ` a ) = 4

$= ( cv cr wcel cfv c4 wceq crab wa cpr vex prid1 eleqtrri fveq2 eqeq1d elrab
   mpbi simpri ) CFZGHZUCBIZJKZUCAFZBIZJKZAGLZHUDUFMUCUCDFZNUJUCUKCOPEQUIUFAUCG
   UGUCKUHUEJUGUCBRSTUAUB $.

$d F x
$d a x
```   

Glauco

unread,
Oct 14, 2024, 7:53:35 AM10/14/24
to Metamath
Since the

$d F x

constraint would conflict with your F definition, here is an alternative version


h1::temp3.1              |- F = ( x e. RR |-> ( ( ( k x. ( x ^ 2 ) ) - ( ( 2 x. k ) x. x ) ) + l ) )
h2::temp3.2           |- { x e. RR | ( F ` x ) = 4 } = { a , b }
3::fveq2               |- ( x = a -> ( F ` x ) = ( F ` a ) )
4:3:eqeq1d            |- ( x = a -> ( ( F ` x ) = 4 <-> ( F ` a ) = 4 ) )
5::nfcv                 |- F/_ x a
6::nfcv               |- F/_ x RR
7::nfmpt1                |- F/_ x ( x e. RR |-> ( ( ( k x. ( x ^ 2 ) ) - ( ( 2 x. k ) x. x ) ) + l ) )
8:1,7:nfcxfr            |- F/_ x F
9:8,5:nffv             |- F/_ x ( F ` a )
10:9:nfeq1            |- F/ x ( F ` a ) = 4
11:5,6,10,4:elrabf   |- ( a e. { x e. RR | ( F ` x ) = 4 } <-> ( a e. RR /\ ( F ` a ) = 4 ) )
12::vex                |- a e. _V
13:12:prid1           |- a e. { a , b }
14:13,2:eleqtrri     |- a e. { x e. RR | ( F ` x ) = 4 }
15:14,11:mpbi       |- ( a e. RR /\ ( F ` a ) = 4 )
qed:15:simpri      |- ( F ` a ) = 4

$= ( cv cr wcel cfv c4 wceq crab wa nfcv c2 co cmul cpr vex prid1 eleqtrri cexp
   cmin caddc cmpt nfmpt1 nfcxfr nffv nfeq1 fveq2 eqeq1d elrabf mpbi simpri ) D
   IZJKZURCLZMNZURAIZCLZMNZAJOZKUSVAPURUREIZUAVEURVFDUBUCHUDVDVAAURJAURQZAJQAUT
   MAURCACAJBIZVBRUESTSRVHTSVBTSUFSFIUGSZUHGAJVIUIUJVGUKULVBURNVCUTMVBURCUMUNUO
   UPUQ $.

$d a x

Glauco

unread,
Oct 14, 2024, 8:12:08 AM10/14/24
to Metamath
I take it back, you can get away with  { x | ( F ` x ) = 4 } , here's the proof  (but for your larger goal, I doubt it's enough)

h1::temp3.1             |- F = ( x e. RR |-> ( ( ( k x. ( x ^ 2 ) ) - ( ( 2 x. k ) x. x ) ) + l ) )
h2::temp3.2          |- { x | ( F ` x ) = 4 } = { a , b }

3::fveq2              |- ( x = a -> ( F ` x ) = ( F ` a ) )
4:3:eqeq1d           |- ( x = a -> ( ( F ` x ) = 4 <-> ( F ` a ) = 4 ) )
5::vex               |- a e. _V
6::nfmpt1               |- F/_ x ( x e. RR |-> ( ( ( k x. ( x ^ 2 ) ) - ( ( 2 x. k ) x. x ) ) + l ) )
7:1,6:nfcxfr           |- F/_ x F
8::nfcv                |- F/_ x a
9:7,8:nffv            |- F/_ x ( F ` a )

10:9:nfeq1           |- F/ x ( F ` a ) = 4
11:10,5,4:elabf     |- ( a e. { x | ( F ` x ) = 4 } <-> ( F ` a ) = 4 )

12::vex               |- a e. _V
13:12:prid1          |- a e. { a , b }
14:13,2:eleqtrri    |- a e. { x | ( F ` x ) = 4 }
qed:14,11:mpbi     |- ( F ` a ) = 4

$= ( cv cfv c4 wceq cab wcel cpr vex cr c2 co cmul prid1 cexp cmin caddc nfmpt1
   eleqtrri cmpt nfcxfr nfcv nffv nfeq1 fveq2 eqeq1d elabf mpbi ) DIZAIZCJZKLZA
   MZNUPCJZKLZUPUPEIZOUTUPVCDPZUAHUFUSVBAUPAVAKAUPCACAQBIZUQRUBSTSRVETSUQTSUCSF
   IUDSZUGGAQVFUEUHAUPUIUJUKVDUQUPLURVAKUQUPCULUMUNUO $.

$d a x

Mario Carneiro

unread,
Oct 14, 2024, 8:28:43 AM10/14/24
to meta...@googlegroups.com
It's not safe to make an assumption of the form |- { x e. RR | ( F ` x ) = 4 } = { a , b } because the variables a,b are implicitly universally quantified in the hypothesis, which means you can prove a contradiction from it. (Consider what happens if you use vtocl on the hypothesis to replace a by +oo.) You should either use class variables A,B as I indicated, or add a context ph -> before every assumption (which is *not* assumed to be disjoint from a,b).

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/161f583c-22bf-4699-b663-92652793f9c3n%40googlegroups.com.

Glauco

unread,
Oct 14, 2024, 9:02:42 AM10/14/24
to Metamath
Hi Mario,

I'm sure you're right, and in fact I would use a class A and something like ph -> A e. V as an additional hyp.

But I cannot reproduce the contradiction off the top of my head; it would be interesting to see it, to gain a deeper understanding.

Can you please show a short proof?  (do you proof something like +oo e. RR ? )

Thank you
Glauco

Glauco

unread,
Oct 14, 2024, 9:24:49 AM10/14/24
to Metamath
I think I got it. Thank you very much for the insight.

h1::temp4.1         |- { x e. RR | ( F ` x ) = 4 } = { a , b }
2::pnfex            |- +oo e. _V
3::preq1             |- ( a = +oo -> { a , b } = { +oo , b } )
4:3:eqeq2d          |- ( a = +oo -> ( { x e. RR | ( F ` x ) = 4 } = { a , b } <-> { x e. RR | ( F ` x ) = 4 } = { +oo , b } ) )
qed:2,4,1:vtocl    |- { x e. RR | ( F ` x ) = 4 } = { +oo , b }

$= ( cv cfv c4 wceq cr crab cpr cpnf pnfex preq1 eqeq2d vtocl ) AFBGHIAJKZCFZDF
   ZLZIRMTLZICMNSMIUAUBRSMTOPEQ $.

$d a x
$d a b
$d F a

Mario Carneiro

unread,
Oct 14, 2024, 10:25:31 AM10/14/24
to meta...@googlegroups.com
That's the first part of the proof. The second part of the proof is to show a contradiction from this, because +oo is in the RHS but not the LHS of that equality.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4c4161e9-ccfc-4289-a19d-1bdcb701bbfbn%40googlegroups.com.

Glauco

unread,
Oct 14, 2024, 11:05:35 AM10/14/24
to Metamath
Below is a full contradiction derived.


It's amazing to see how ChatGPT can understand set.mm even though I guess there's not much content, when compared to other subjects.

Here's a brief "conversation" (not perfect, but close...):




h1::temp4.1            |- { x e. RR | ( F ` x ) = 4 } = { a , b }
2::pnfex               |- +oo e. _V
3::preq1                |- ( a = +oo -> { a , b } = { +oo , b } )
4:3:eqeq2d             |- ( a = +oo -> ( { x e. RR | ( F ` x ) = 4 } = { a , b } <-> { x e. RR | ( F ` x ) = 4 } = { +oo , b } ) )
5:2,4,1:vtocl         |- { x e. RR | ( F ` x ) = 4 } = { +oo , b }
6:2:prid1             |- +oo e. { +oo , b }
7:6,5:eleqtrri       |- +oo e. { x e. RR | ( F ` x ) = 4 }
8::elrabi            |- ( +oo e. { x e. RR | ( F ` x ) = 4 } -> +oo e. RR )
9:7,8:ax-mp         |- +oo e. RR
10::pnfnre2         |- -. +oo e. RR
qed:9,10:pm2.24ii  |- F.

$= ( cpnf cr wcel wfal cv cfv c4 wceq crab cpr pnfex prid1 preq1 eqeq2d vtocl
   eleqtrri elrabi ax-mp pnfnre2 pm2.24ii ) FGHZIFAJBKLMZAGNZHUFFFDJZOZUHFUIPQU
   HCJZUIOZMUHUJMCFPUKFMULUJUHUKFUIRSETUAUGAFGUBUCUDUE $.


$d a x
$d a b
$d F a

Igor Ieskov

unread,
Oct 14, 2024, 4:48:36 PM10/14/24
to Metamath

Thank you Glauco and Mario for helpful answers. I will need some time to analyze and understand everything you wrote. 


For now, I have one question. Glauco, you mentioned that you developed this proof using Yamma. Can you explain at a high level what steps you’ve done in Yamma to come up with such a proof? I am asking for the proof of |- ( F ` a ) = 4. No need to explain how to set up Yamma, it can be found in its readme. I am more interested in how much of this proof was constructed by Yamma and how much was manual work. I didn’t have time yet to try to prove this in Yamma, but I will surely try. So, what I think would be interesting for me (and probably for others) is a high level list of actions you’ve done to create this proof. For example:


1) put all required hypotheses and the goal statement to Yamma.

2) I know that for such kind of proofs elrab assertion is usually used, so type its name in and unify (press CTRL+U). New steps appeared. 

3) …


I will be very surprised if you’ve just provided the hypotheses and the goal statement and Yamma found everything else!


Sorry, if I am requesting too much. You can respond as high level or detailed depending on how much free time you have. I am asking because I tried to prove this using mm-lamp. Since I don’t know set.mm assertions well, I just searched for assertions which I thought could be used in the proof and tried to combine them somehow. I am interested in how you came up with this proof (how much automation you used and how much your experience with set.mm).


BTW, it is Igor writing :)


-

Igor

Glauco

unread,
Oct 15, 2024, 5:50:12 PM10/15/24
to Metamath
Hi Igor,

with regard to your question, yamma, for now, is similar to mmj2. Do you have some experience with mmj2?

I tend to proof backwards, thus yamma may have a bias toward this approach.

Did you see this simple video?


As you can see, when it has to prove

|- E. x x e. { 1 }

if you hit ctrl+space , intellisense shows you the labels that are more likely to move you in the right direction.

The one I chose is the 6th one, that is ceqsexv2d   (intellisense details clearly show me that's the one I'm looking for)

I would not be able to know it myself, so it saves me some search time.

eximii , the first one suggested, is not the right one, but I can easily see why it's, in general, a good candidate for the given statement

HTH
Glauco

Igor Ieskov

unread,
Oct 16, 2024, 3:41:26 AM10/16/24
to Metamath

Hi Glauco,


Yes, this answers my question. Thank you very much. Also I found this thread contains other shortcuts used in the video.


I don’t have much experience with mmj2. I used it to repeat proofs from David’s video tutorials, but not for creating my own proofs.


-

Igor

Jorge Agra

unread,
Oct 16, 2024, 6:28:21 AM10/16/24
to meta...@googlegroups.com
Hi Igor,

I haven't tried the proof myself, a little short on time right now, but I have doubts about why you are trying to prove F(a) = 4 or F(b). It seems to me this is given, an hypothesis, right?

Regards,
Jorge



To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/0466031a-8f6f-4d1d-8a69-8ff2351dc4f6n%40googlegroups.com.

Igor Ieskov

unread,
Oct 16, 2024, 11:28:18 AM10/16/24
to Metamath

Hi Jorge,


I am not sure what you mean by saying that it is given as a hypothesis. So, I will explain as detailed as I can. It may seem obvious that F(a) = 4 from the original edition of the problem formulated in the “human language”. But it is not explicitly given in the collection of hypotheses I chose. The closest hypothesis in my collection is hyp4: |- { x | ( F ` x ) = 4 } = { A , B }  (I switched back to class variables). However, Metamath doesn’t understand meaning of statements. It can only compare statements symbol by symbol. That’s why I have to prove |- ( F ` A ) = 4 before I can use it in my proof. 


The same problem may be formalized in many ways, and you can choose another approach, which will explicitly include F(a) = 4 and maybe some obvious calculations done. For example:


|- 0 < k

|- 0 < l

|- F = ( x e. RR |-> ( ( ( k x. ( x ^ 2 ) ) - ( ( 2 x. k ) x. x ) ) + l ) )

|- ( F ` A ) = 4

|- ( F ` B ) = 4

|- ( abs ` ( A - B ) ) = 6

|- ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ; 3 2 ) = C


These hypotheses also should describe the same problem, but they explicitly include |- ( F ` A ) = 4 and you will not have to prove it. (actually these two collections of hypotheses may be not exactly equivalent, but I hope it is clear what I mean)


-

Igor

Glauco

unread,
Oct 19, 2024, 2:29:25 PM10/19/24
to Metamath
Hi Igor,

as Mario pointed out, we'd better be careful with free setvars in hyps.

For instance, from hyp

|- 0 < k

you can derive everything. Here's an example

h1::temp4.1          |- 0 < k
2::negex             |- -u 1 e. _V
3::breq2             |- ( k = -u 1 -> ( 0 < k <-> 0 < -u 1 ) )
4:2,3,1:vtocl       |- 0 < -u 1
5::lenlt               |- ( ( -u 1 e. RR /\ 0 e. RR ) -> ( -u 1 <_ 0 <-> -. 0 < -u 1 ) )
6::neg1rr             |- -u 1 e. RR
7::0re                |- 0 e. RR
8::neg1lt0            |- -u 1 < 0
9:6,7,8:ltleii       |- -u 1 <_ 0
10::neg1rr             |- -u 1 e. RR
11::0re                |- 0 e. RR
12:10,11,5:mp2an      |- ( -u 1 <_ 0 <-> -. 0 < -u 1 )
13:12:biimpi         |- ( -u 1 <_ 0 -> -. 0 < -u 1 )
14:9,13:ax-mp       |- -. 0 < -u 1
qed:4,14:pm2.24ii  |- 1 e. (/)

$= ( cc0 c1 cneg clt wbr c0 wcel cv negex breq2 vtocl cle wn neg1rr 0re neg1lt0
   ltleii cr wb lenlt mp2an biimpi ax-mp pm2.24ii ) CDEZFGZDHICAJZFGUHAUGDKUIUG
   CFLBMUGCNGZUHOZUGCPQRSUJUKUGTICTIUJUKUAPQUGCUBUCUDUEUF $.


Igor Ieskov

unread,
Oct 20, 2024, 4:01:12 AM10/20/24
to Metamath

Thanks Glauco for showing this example. I didn’t expect that |- 0 < k implies |- 0 < -u 1 .


-

Igor

Mario Carneiro

unread,
Oct 20, 2024, 9:25:38 AM10/20/24
to meta...@googlegroups.com
You should read any statement starting |- and having a set variable in it as universally quantified over those variables. So when you see |- 0 < k that's saying "0 < k is derivable in the empty context" which is a strong statement, equivalent to "for all k, 0 < k" which is of course false.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3bf568bf-cae2-4853-9735-555598676ef5n%40googlegroups.com.

Igor Ieskov

unread,
Nov 5, 2024, 6:03:53 AM11/5/24
to Metamath

Thanks Mario. I also found useful explanations on setvar and class variables on the Metamath Proof Explorer Home Page. For example, setvar variables “often serve as bound or dummy variables in expressions, i.e. the first argument of the ∀ quantifier connective”.


So, taking all the above discussions into account I refactored my hypotheses:


hyp1 |- ( ph -> L e. RR )

hyp2 |- ( ph -> K e. RR )

hyp3 |- ( ph -> 0 < L )

hyp4 |- ( ph -> 0 < K )

hyp5 |- ( ph -> F = ( x e. RR |-> ( ( K x. ( x ^ 2 ) ) + ( ( -u ( 2 x. K ) x. x ) + L ) ) ) )

hyp6 |- ( ph -> A e. _V )

hyp7 |- ( ph -> B e. _V )

hyp8 |- ( ph -> { x e. RR | ( F ` x ) = 4 } = { A , B } )

hyp9 |- ( ph -> ( ( ( A - B ) ^ 2 ) + ( ( ( F ` A ) - ( F ` B ) ) ^ 2 ) ) = ( 6 ^ 2 ) )


Are they correct now? Don’t they introduce any contradiction?


What about A e. _V and B e. _V, is it really needed?


Can we use A e. CC and B e. CC instead of A e. _V and B e. _V? (that should simplify some proofs)


Also, I think that adding |- A e. RR and |- B e. RR as hypotheses is incorrect, because it may happen that roots of the quadratic equation are imaginary numbers and then we would have a contradiction: |- A e. RR (as a hypothesis) and |- A e. ( CC \ RR ). Am I right? Or the fact that hyp5 mentions "x e. RR" makes usage of |- A e. RR and |- B e. RR as hypotheses safe?


-

Igor

Glauco

unread,
Nov 5, 2024, 6:46:10 AM11/5/24
to Metamath
Hi Igor,

unfortunately, for a few days I'll not have the chance to test what I'm writing, so take it with a grain of salt.

it makes the theorem less general, but we tend to write hyp5 without the antecedent (as a "pure" local definition)

hyp5 |- F = ( x e. RR |-> ( ( K x. ( x ^ 2 ) ) + ( ( -u ( 2 x. K ) x. x ) + L ) ) )

By writing

|- ( ph -> { x e. RR | ( F ` x ) = 4 } = { A , B } )

you are "stating" that  { x e. RR | ( F ` x ) = 4 } has at most two elements (I guess you don't want it in the hyp; maybe you can prove it, but you don't want it in a hyp)

In place of hyp 6,7,8 You probably want something like

|- X = { x e. RR | ( F ` x ) = 4 }
|- ( ph -> A e. X )
|- ( ph -> B e. X )

In both cases, with hyp9 you can prove that A =/= B

Igor Ieskov

unread,
Nov 5, 2024, 4:40:46 PM11/5/24
to Metamath

You are right, Glauco, it is possible to prove A=/=B


${

    $d A x $.

    $d B x $.

    $d F x $.

    AneB.1 $e |- ( ph -> X = { x e. RR | ( F ` x ) = 4 } ) $.

    AneB.2 $e |- ( ph -> A e. X ) $.

    AneB.3 $e |- ( ph -> B e. X ) $.

    AneB.4 $e |- ( ph -> ( ( ( A - B ) ^ 2 ) + ( ( ( F ` A ) - ( F ` B ) ) ^ 2 ) ) = ( 6 ^ 2 ) ) $.

    AneB $p |- ( ph -> A =/= B ) 

        $= ( cr wcel cfv c4 wceq cv crab wa eleqtrd fveqeq2 elrab sylib simpld 

        recnd cmin co cc0 c2 cexp c6 caddc subcld sqcld addid1d sq0 oveq2i 4cn 

        subidi oveq1i simprd oveq2d oveq1d eqtr3d eqtr3id cn 6nn a1i nnsqcld 

        nnne0d eqnetrd sq0i adantl mteqand subne0ad ) 

        ACDACACKZLZCEMZNZOZACBPZEMVROZBVOQZLVPVSRACFWBHGSW 

        AVSBCVOVTCVRETUAUBZUCUDZADADVOLZDEMZVROZADWBLWEWGR 

        ADFWBIGSWAWGBDVOVTDVRETUAUBZUCUDZACDUEZUFZUGZWKUHZ 

        UIZUFZWLAWOUJZWMWNUFZWLAWOWLUKZUFZWOWQAWOAWKACDWDW 

        IULUMUNAWSWOWLWMWNUFZWRUFZWQWTWLWOWRUOUPAXAWOVRVRW 

        JUFZWMWNUFZWRUFZWQXCWTWOWRXBWLWMWNVRUQURUSUPAWOVRW 

        FWJUFZWMWNUFZWRUFZXDWQAXFXCWOWRAXEXBWMWNAWFVRVRWJA 

        WEWGWHUTVAVBVAAWOVQWFWJUFZWMWNUFZWRUFXGWQAXIXFWOWR 

        AXHXEWMWNAVQVRWFWJAVPVSWCUTVBVBVAJVCVCVDVDVCAWQAWP 

        WPVELAVFVGVHVIVJWKWLOWOWLOAWKVKVLVMVN $.

$}



The complete proof table is attached.


Thank you for your response!


-

Igor

AneB_proof_table.txt

Igor Ieskov

unread,
Nov 11, 2024, 8:02:28 AM11/11/24
to Metamath

It was not easy, but I managed to create a proof for that task. The complete proof is attached (task1_v1.mm). It consists of three parts.

  1. The first part includes generic theorems used in the proof. Some of them are copied from a mathbox and renamed to make the entire proof independent of mathboxes.

  2. The second part includes different lemmas needed for the proof. It is actually the main part.

  3. The third part repeats the second part. But I added it to make the idea of the proof easier to understand.


What I proved is:
C = ( ; 3 6 - ( 2 x. ( ( L - 4 ) / K ) ) )

( L - 4 ) < K


Here is the third part of the proof with some text formatting to highlight the main parts:


${

    $d ph x $.

    $d A x $.

    $d B x $.

    $d F x $.

    $d K x $.

    $d L x $.

    task1.1 $e |- ( ph -> L e. RR+ ) $.

    task1.2 $e |- ( ph -> K e. RR+ ) $.

    task1.3 $e |- F = ( x e. RR |-> ( ( K x. ( x ^ 2 ) ) + ( ( -u ( 2 x. K ) x. x ) + L ) ) ) $.

    task1.4 $e |- X = { x e. RR | ( F ` x ) = 4 } $.

    task1.5 $e |- ( ph -> A e. X ) $.

    task1.6 $e |- ( ph -> B e. X ) $.

    task1.7 $e |- ( ph -> ( ( ( A - B ) ^ 2 ) + ( ( ( F ` A ) - ( F ` B ) ) ^ 2 ) ) = ( 6 ^ 2 ) ) $.

    task1.8 $e |- ( ph -> ( ( ( A ^ 2 ) + ( ( F ` A ) ^ 2 ) ) + ( ( B ^ 2 ) + ( ( F ` B ) ^ 2 ) ) ) = C ) $.

    

    $( It follows from task1.4, task1.5, and task1.6 that F(A) = F(B) = 4. $)

    task1_step1 

        $p |- ( ph -> ( F ` A ) = 4 ) 

        $= ( cv cfv c4 wceq cr crab a1i task1_lem1 ) ABCFIIBRFSTUABUBUCUAAMUDNUE $.

        

    task1_step2 

        $p |- ( ph -> ( F ` B ) = 4 ) 

        $= ( cv cfv c4 wceq cr crab a1i task1_lem1 ) ABDFIIBRFSTUABUBUCUAAMUDOUE $.

        

    $( Knowing that F(A) = F(B) = 4, we can simplify the expression for C: $)

    task1_step3 

        $p |- ( ph -> C = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ; 3 2 ) ) 

        $= ( cv cfv c4 wceq cr crab a1i task1_lem2 ) ABCDEFIIBRFSTUABUBUCUAAMUDNOQUE $.

    

    $( Using the equality F(A) = 4 and applying the actual formula for F, 

        we can construct a quadratic equation: 

    $)

    task1_step4 

        $p |- ( ph -> ( ( K x. ( A ^ 2 ) ) + ( ( -u ( 2 x. K ) x. A ) + ( L - 4 ) ) ) = 0 ) 

        $= ( cr cv c2 cexp co cmul cneg caddc cmpt wceq a1i cfv c4 crab task1_lem3 ) 

            ABCFGHIJKFBRZGBSZTZUAUBUCZUBUOGUPUBUDUNUPUBHUEZUBU QUBUFUGALUHIUNFUIUJUGBUMUKUGAMUHNUL $.

            

    ${

        $( This quadratic equation has the discriminant: $)

        task1.9 $e |- ( ph -> D = ( ( -u ( 2 x. K ) ^ 2 ) - ( 4 x. ( K x. ( L - 4 ) ) ) ) ) $.

        

        $( By solving that quadratic equation, we obtain two possible values for A: $)

        task1_step5 

            $p |- ( ph -> ( 

                A = ( 1 + ( ( sqrt ` D ) / ( 2 x. K ) ) ) 

                \/ 

                A = ( 1 - ( ( sqrt ` D ) / ( 2 x. K ) ) ) 

            ) ) 

            $= ( cr cv c2 cexp co cmul cneg caddc cmpt wceq a1i cfv c4 crab task1_lem4 ) 

            ABCFGHIJKLGBTZHBUAZUBZUCUDUEZUDUQHURUDUFUPURUDIUGZ UDUSUDUHUIAMUJJUPGUKULUIBUOUMUIANUJOSUN $.

            

        $( Analogously, we can construct a similar quadratic equation for B 

            and obtain two possible values: 

        $)

        task1_step6 

            $p |- ( ph -> ( 

                B = ( 1 + ( ( sqrt ` D ) / ( 2 x. K ) ) ) 

                \/ 

                B = ( 1 - ( ( sqrt ` D ) / ( 2 x. K ) ) ) 

            ) ) 

            $= ( cr cv c2 cexp co cmul cneg caddc cmpt wceq a1i cfv c4 crab task1_lem4 ) 

            ABDFGHIJKLGBTZHBUAZUBZUCUDUEZUDUQHURUDUFUPURUDIUGZ UDUSUDUHUIAMUJJUPGUKULUIBUOUMUIANUJPSUN $.

            

        $( From the fact that A and B are a distance 6 apart (task1.7) 

            it follows that A and B cannot be equal. 

        $)

        task1_step7 

            $p |- ( ph -> A =/= B ) 

            $= ( cv cfv c4 wceq cr crab a1i task1_lem5 ) ABCDGJJBTGUAUBUCBUDUEUCANUFOPQUG $.

            

        $( Since A and B must be different, we can have only two possible 

            pairs of values for A and B: 

        $)

        task1_step8 

            $p |- ( ph -> ( 

                ( 

                    A = ( 1 + ( ( sqrt ` D ) / ( 2 x. K ) ) ) 

                    /\ 

                    B = ( 1 - ( ( sqrt ` D ) / ( 2 x. K ) ) ) 

                ) 

                \/ 

                ( 

                    A = ( 1 - ( ( sqrt ` D ) / ( 2 x. K ) ) ) 

                    /\ 

                    B = ( 1 + ( ( sqrt ` D ) / ( 2 x. K ) ) ) 

                ) 

            ) ) 

            $= ( cr cv c2 cexp co cmul cneg caddc cmpt wceq a1i cfv c4 crab task1_lem6 ) 

                ABCDFGHIJKLGBTZHBUAZUBZUCUDUEZUDUQHURUDUFUPURUDIUG 

                ZUDUSUDUHUIAMUJJUPGUKULUIBUOUMUIANUJOPQSUN $.

            

        $( Also, since both A and B are real numbers, the discriminant must be positive.

            If the discriminant were 0, then A would be equal to B.

            If the discriminant were negative, then A and B would be complex numbers. 

        $)

        task1_step9 

            $p |- ( ph -> 0 < D ) 

            $= ( cr cv c2 cexp co cmul cneg caddc cmpt wceq a1i cfv c4 crab task1_lem7 ) 

                ABCDFGHIJKLGBTZHBUAZUBZUCUDUEZUDUQHURUDUFUPURUDIUG 

                ZUDUSUDUHUIAMUJJUPGUKULUIBUOUMUIANUJOPQSUN $.

    $}

    

    $( Knowing that 0 < D, we can simplify the expressions for A and B: $)

    task1_step10 

        $p |- ( ph -> ( 

            ( 

                A = ( 1 + ( sqrt ` ( 1 - ( ( L - 4 ) / K ) ) ) ) 

                /\ 

                B = ( 1 - ( sqrt ` ( 1 - ( ( L - 4 ) / K ) ) ) ) 

            ) 

            \/ 

            ( 

                A = ( 1 - ( sqrt ` ( 1 - ( ( L - 4 ) / K ) ) ) ) 

                /\ 

                B = ( 1 + ( sqrt ` ( 1 - ( ( L - 4 ) / K ) ) ) ) 

            ) 

        ) ) 

        $= ( cr cv c2 cexp co cmul cneg caddc cmpt wceq a1i cfv c4 crab task1_lem10 ) 

            ABCDFGHIJKFBRZGBSZTZUAUBUCZUBUOGUPUBUDUNUPUBHUEZUB UQUBUFUGALUHIUNFUIUJUGBUMUKUGAMUHNOPUL $.

            

    $( Regardless of which pair of values we take for A and B,

        we always get the same value for A^2+B^2:

    $)

    task1_step11 

        $p |- ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( 4 - ( 2 x. ( ( L - 4 ) / K ) ) ) ) 

        $= ( cr cv c2 cexp co cmul cneg caddc cmpt wceq a1i cfv c4 crab task1_lem15 ) 

            ABCDFGHIJKFBRZGBSZTZUAUBUCZUBUOGUPUBUDUNUPUBHUEZUB UQUBUFUGALUHIUNFUIUJUGBUMUKUGAMUHNOPUL $.

            

    $( Now we can simplify the expression for C from step3 $)

    task1_step12 

        $p |- ( ph -> C = ( ; 3 6 - ( 2 x. ( ( L - 4 ) / K ) ) ) ) 

        $= ( cr cv c2 cexp co cmul cneg caddc cmpt wceq a1i cfv c4 crab task1_lem16 ) 

        ABCDEFGHIJKFBRZGBSZTZUAUBUCZUBUOGUPUBUDUNUPUBHUEZU BUQUBUFUGALUHIUNFUIUJUGBUMUKUGAMUHNOPQUL $.

        

    $( Also, from 0 < D, it follows that K and L cannot be arbitrary positive numbers;

        they must satisfy the relation:

    $)

    task1_step13 

        $p |- ( ph -> ( L - 4 ) < K ) 

        $= ( cr cv c2 cexp co cmul cneg caddc cmpt wceq a1i cfv c4 crab task1_lem8 ) 

            ABCDFGHIJKFBRZGBSZTZUAUBUCZUBUOGUPUBUDUNUPUBHUEZUB UQUBUFUGALUHIUNFUIUJUGBUMUKUGAMUHNOPUL $.

$}


-

Igor

task1_v1.mm

Igor Ieskov

unread,
Nov 12, 2024, 3:55:58 AM11/12/24
to Metamath

It appears that my previous proof could be continued to get a simpler result. The complete proof is attached - task1_v2.mm.


The new result is as follows:


${

    $d ph x $.

    $d A x $.

    $d B x $.

    $d F x $.

    $d K x $.

    $d L x $.

    task1_v2.1 $e |- ( ph -> L e. RR+ ) $.

    task1_v2.2 $e |- ( ph -> K e. RR+ ) $.

    task1_v2.3 $e |- ( ph -> F = ( x e. RR |-> ( ( K x. ( x ^ 2 ) ) + ( ( -u ( 2 x. K ) x. x ) + L ) ) ) ) $.

    task1_v2.4 $e |- ( ph -> X = { x e. RR | ( F ` x ) = 4 } ) $.

    task1_v2.5 $e |- ( ph -> A e. X ) $.

    task1_v2.6 $e |- ( ph -> B e. X ) $.

    task1_v2.7 $e |- ( ph -> ( ( ( A - B ) ^ 2 ) + ( ( ( F ` A ) - ( F ` B ) ) ^ 2 ) ) = ( 6 ^ 2 ) ) $.

    task1_v2 

        $p |- ( ph -> ( ( ( A ^ 2 ) + ( ( F ` A ) ^ 2 ) ) + ( ( B ^ 2 ) + ( ( F ` B ) ^ 2 ) ) ) = ; 5 2 ) 

        $= ( c2 cexp co cfv caddc eqidd task1_lem20 ) ABCDCPZQZRCESUCUDRTZRDUCUDRDESUCUDRUERUERZEFGHIJKL MNOAUFUAUB $.

$}


And here are the new steps with comments:


    $( Also, from 0 < D, it follows that K and L cannot be arbitrary positive numbers;

        they must satisfy the relation:

    $)

    task1_step13 

        $p |- ( ph -> ( L - 4 ) < K ) 

        $= ( cr cv c2 cexp co cmul cneg caddc cmpt wceq a1i cfv c4 crab task1_lem8 ) 

            ABCDFGHIJKFBRZGBSZTZUAUBUCZUBUOGUPUBUDUNUPUBHUEZUB UQUBUFUGALUHIUNFUIUJUGBUMUKUGAMUHNOPUL $.


    $( Analogous to step11, regardless of the values we choose for A and B,

        we always get the same result for (A-B)^2:

    $)

task1_step13 

        $p |- ( ph -> ( ( A - B ) ^ 2 ) = ( 4 x. ( 1 - ( ( L - 4 ) / K ) ) ) ) 

        $= ( cr cv c2 cexp co cmul cneg caddc cmpt wceq a1i cfv c4 crab task1_lem18 ) 

        ABCDFGHIJKFBRZGBSZTZUAUBUCZUBUOGUPUBUDUNUPUBHUEZUB UQUBUFUGALUHIUNFUIUJUGBUMUKUGAMUHNOPUL $.

        

    $( By substituting the above expression for (A-B)^2 into task1.7 and simplifying,

        we get: 

    $)

    task1_step14 

        $p |- ( ph -> ( ( L - 4 ) / K ) = -u 8 ) 

        $= ( cr cv c2 cexp co cmul cneg caddc cmpt wceq a1i cfv c4 crab task1_lem19 ) 

        ABCDFGHIJKFBRZGBSZTZUAUBUCZUBUOGUPUBUDUNUPUBHUEZUB UQUBUFUGALUHIUNFUIUJUGBUMUKUGAMUHNOPUL $.

            

    $( Now we can simplify the expression for C from step12 $)

    task1_step15 

        $p |- ( ph -> C = ; 5 2 ) 

        $= ( cr cv c2 cexp co cmul cneg caddc cmpt wceq a1i cfv c4 crab task1_lem20 ) 

        ABCDEFGHIJKFBRZGBSZTZUAUBUCZUBUOGUPUBUDUNUPUBHUEZU BUQUBUFUGALUHIUNFUIUJUGBUMUKUGAMUHNOPQUL $.

    

$}


-

Igor

task1_v2.mm
Reply all
Reply to author
Forward
0 new messages