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/c9ffb883-513b-4d10-9adc-6eac81346ce4n%40googlegroups.com.
