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...): https://chatgpt.com/share/670d3203-1d2c-8010-bb5b-2e4105fc5379 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 Il giorno lunedì 14 ottobre 2024 alle 16:25:31 UTC+2 [email protected] ha scritto: > 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. > > On Mon, Oct 14, 2024 at 3:24 PM Glauco <[email protected]> wrote: > >> 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 >> >> >> Il giorno lunedì 14 ottobre 2024 alle 15:02:42 UTC+2 Glauco ha scritto: >> >>> 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 >>> >>> >>> Il giorno lunedì 14 ottobre 2024 alle 14:28:43 UTC+2 [email protected] >>> ha scritto: >>> >>>> 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/4c4161e9-ccfc-4289-a19d-1bdcb701bbfbn%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/4c4161e9-ccfc-4289-a19d-1bdcb701bbfbn%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/1e68bb9a-fda0-423a-9811-86e4d0bc9a20n%40googlegroups.com.
