Thanks Mario. I also found useful explanations on setvar and class
variables on the Metamath Proof Explorer Home Page
<https://us.metamath.org/mpeuni/mmset.html>. For example, setvar variables
“often
serve as bound or dummy variables in expressions, i.e. the first argument
of the ∀ quantifier connective”.
So, taking all the above discussions into account I refactored my
hypotheses:
hyp1 |- ( ph -> L e. RR )
hyp2 |- ( ph -> K e. RR )
hyp3 |- ( ph -> 0 < L )
hyp4 |- ( ph -> 0 < K )
hyp5 |- ( ph -> F = ( x e. RR |-> ( ( K x. ( x ^ 2 ) ) + ( ( -u ( 2 x. K )
x. x ) + L ) ) ) )
hyp6 |- ( ph -> A e. _V )
hyp7 |- ( ph -> B e. _V )
hyp8 |- ( ph -> { x e. RR | ( F ` x ) = 4 } = { A , B } )
hyp9 |- ( ph -> ( ( ( A - B ) ^ 2 ) + ( ( ( F ` A ) - ( F ` B ) ) ^ 2 ) ) =
( 6 ^ 2 ) )
Are they correct now? Don’t they introduce any contradiction?
What about A e. _V and B e. _V, is it really needed?
Can we use A e. CC and B e. CC instead of A e. _V and B e. _V? (that should
simplify some proofs)
Also, I think that adding |- A e. RR and |- B e. RR as hypotheses is
incorrect, because it may happen that roots of the quadratic equation are
imaginary numbers and then we would have a contradiction: |- A e. RR (as a
hypothesis) and |- A e. ( CC \ RR ). Am I right? Or the fact that hyp5
mentions "x e. RR" makes usage of |- A e. RR and |- B e. RR as hypotheses
safe?
-
Igor
On Sunday, October 20, 2024 at 3:25:38 PM UTC+2 [email protected] wrote:
> You should read any statement starting |- and having a set variable in it
> as universally quantified over those variables. So when you see |- 0 < k
> that's saying "0 < k is derivable in the empty context" which is a strong
> statement, equivalent to "for all k, 0 < k" which is of course false.
>
> On Sun, Oct 20, 2024 at 10:01 AM Igor Ieskov <[email protected]> wrote:
>
>> Thanks Glauco for showing this example. I didn’t expect that |- 0 < k
>> implies |- 0 < -u 1 .
>>
>>
>> -
>>
>> Igor
>>
>> On Saturday, October 19, 2024 at 8:29:25 PM UTC+2 Glauco wrote:
>>
>>> Hi Igor,
>>>
>>> as Mario pointed out, we'd better be careful with free setvars in hyps.
>>>
>>> For instance, from hyp
>>>
>>> |- 0 < k
>>>
>>> you can derive everything. Here's an example
>>>
>>> h1::temp4.1 |- 0 < k
>>> 2::negex |- -u 1 e. _V
>>> 3::breq2 |- ( k = -u 1 -> ( 0 < k <-> 0 < -u 1 ) )
>>> 4:2,3,1:vtocl |- 0 < -u 1
>>> 5::lenlt |- ( ( -u 1 e. RR /\ 0 e. RR ) -> ( -u 1 <_ 0 <->
>>> -. 0 < -u 1 ) )
>>> 6::neg1rr |- -u 1 e. RR
>>> 7::0re |- 0 e. RR
>>> 8::neg1lt0 |- -u 1 < 0
>>> 9:6,7,8:ltleii |- -u 1 <_ 0
>>> 10::neg1rr |- -u 1 e. RR
>>> 11::0re |- 0 e. RR
>>> 12:10,11,5:mp2an |- ( -u 1 <_ 0 <-> -. 0 < -u 1 )
>>> 13:12:biimpi |- ( -u 1 <_ 0 -> -. 0 < -u 1 )
>>> 14:9,13:ax-mp |- -. 0 < -u 1
>>> qed:4,14:pm2.24ii |- 1 e. (/)
>>>
>>> $= ( cc0 c1 cneg clt wbr c0 wcel cv negex breq2 vtocl cle wn neg1rr 0re
>>> neg1lt0
>>> ltleii cr wb lenlt mp2an biimpi ax-mp pm2.24ii )
>>> CDEZFGZDHICAJZFGUHAUGDKUIUG
>>> CFLBMUGCNGZUHOZUGCPQRSUJUKUGTICTIUJUKUAPQUGCUBUCUDUEUF $.
>>>
>>>
>>> --
>> 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/3bf568bf-cae2-4853-9735-555598676ef5n%40googlegroups.com
>>
>> <https://groups.google.com/d/msgid/metamath/3bf568bf-cae2-4853-9735-555598676ef5n%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 visit
https://groups.google.com/d/msgid/metamath/976ce07b-e849-45b3-ba78-532d6e368951n%40googlegroups.com.
