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.
