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).On Mon, Oct 14, 2024 at 2:12 PM Glauco <[email protected]> wrote: > 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 > > Il giorno lunedì 14 ottobre 2024 alle 13:53:35 UTC+2 Glauco ha scritto: > >> 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 >> >> Il giorno lunedì 14 ottobre 2024 alle 13:42:45 UTC+2 Glauco ha scritto: >> >>> 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 >>> ``` >>> >>> >>> >>> >>> Il giorno lunedì 14 ottobre 2024 alle 12:40:47 UTC+2 [email protected] >>> ha scritto: >>> >>>> 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? >>>> >>>> On Sunday, July 28, 2024 at 11:54:47 PM UTC+2 [email protected] wrote: >>>> >>>>> On Sun, Jul 28, 2024 at 11:43 PM Glauco <[email protected]> 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.) >>>>> >>>>> -- > 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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/161f583c-22bf-4699-b663-92652793f9c3n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/161f583c-22bf-4699-b663-92652793f9c3n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvD%3D0m%3DXybGC2TxZRyc6D06fQvXqkvDp0qFFhHw6hUVow%40mail.gmail.com.
