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.
