You are right, Glauco, it is possible to prove A=/=B
${
$d A x $.
$d B x $.
$d F x $.
AneB.1 $e |- ( ph -> X = { x e. RR | ( F ` x ) = 4 } ) $.
AneB.2 $e |- ( ph -> A e. X ) $.
AneB.3 $e |- ( ph -> B e. X ) $.
AneB.4 $e |- ( ph -> ( ( ( A - B ) ^ 2 ) + ( ( ( F ` A ) - ( F ` B ) )
^ 2 ) ) = ( 6 ^ 2 ) ) $.
AneB $p |- ( ph -> A =/= B )
$= ( cr wcel cfv c4 wceq cv crab wa eleqtrd fveqeq2 elrab sylib
simpld
recnd cmin co cc0 c2 cexp c6 caddc subcld sqcld addid1d sq0 oveq2i
4cn
subidi oveq1i simprd oveq2d oveq1d eqtr3d eqtr3id cn 6nn a1i
nnsqcld
nnne0d eqnetrd sq0i adantl mteqand subne0ad )
ACDACACKZLZCEMZNZOZACBPZEMVROZBVOQZLVPVSRACFWBHGSW
AVSBCVOVTCVRETUAUBZUCUDZADADVOLZDEMZVROZADWBLWEWGR
ADFWBIGSWAWGBDVOVTDVRETUAUBZUCUDZACDUEZUFZUGZWKUHZ
UIZUFZWLAWOUJZWMWNUFZWLAWOWLUKZUFZWOWQAWOAWKACDWDW
IULUMUNAWSWOWLWMWNUFZWRUFZWQWTWLWOWRUOUPAXAWOVRVRW
JUFZWMWNUFZWRUFZWQXCWTWOWRXBWLWMWNVRUQURUSUPAWOVRW
FWJUFZWMWNUFZWRUFZXDWQAXFXCWOWRAXEXBWMWNAWFVRVRWJA
WEWGWHUTVAVBVAAWOVQWFWJUFZWMWNUFZWRUFXGWQAXIXFWOWR
AXHXEWMWNAVQVRWFWJAVPVSWCUTVBVBVAJVCVCVDVDVCAWQAWP
WPVELAVFVGVHVIVJWKWLOWOWLOAWKVKVLVMVN $.
$}
The complete proof table is attached.
Thank you for your response!
-
Igor
On Tuesday, November 5, 2024 at 12:46:10 PM UTC+1 Glauco wrote:
> Hi Igor,
>
> unfortunately, for a few days I'll not have the chance to test what I'm
> writing, so take it with a grain of salt.
>
> it makes the theorem less general, but we tend to write hyp5 without the
> antecedent (as a "pure" local definition)
>
> hyp5 |- F = ( x e. RR |-> ( ( K x. ( x ^ 2 ) ) + ( ( -u ( 2 x. K ) x. x )
> + L ) ) )
>
> By writing
>
> |- ( ph -> { x e. RR | ( F ` x ) = 4 } = { A , B } )
>
> you are "stating" that { x e. RR | ( F ` x ) = 4 } has at most two
> elements (I guess you don't want it in the hyp; maybe you can prove it, but
> you don't want it in a hyp)
>
> In place of hyp 6,7,8 You probably want something like
>
> |- X = { x e. RR | ( F ` x ) = 4 }
> |- ( ph -> A e. X )
> |- ( ph -> B e. X )
>
> In both cases, with hyp9 you can prove that A =/= B
>
--
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/c6b6a6bc-1012-4aca-a442-a6614e9732ffn%40googlegroups.com.
--- AneB
-------------------------------------------------------------------------------------------------------------------------------------------
1| | AneB.2 | |- ( ph -> A e. X )
2| | AneB.1 | |- ( ph -> X = { x e. RR | ( F ` x ) = 4 } )
3| 1,2 | eleqtrd | |- ( ph -> A e. { x e. RR | ( F ` x ) = 4 } )
4| | fveqeq2 | |- ( x = A -> ( ( F ` x ) = 4 <-> ( F ` A ) = 4 ) )
5| 4 | elrab | |- ( A e. { x e. RR | ( F ` x ) = 4 } <-> ( A e. RR
/\ ( F ` A ) = 4 ) )
6| 3,5 | sylib | |- ( ph -> ( A e. RR /\ ( F ` A ) = 4 ) )
7| 6 | simpld | |- ( ph -> A e. RR )
8| 7 | recnd | |- ( ph -> A e. CC )
9| | AneB.3 | |- ( ph -> B e. X )
10| 9,2 | eleqtrd | |- ( ph -> B e. { x e. RR | ( F ` x ) = 4 } )
11| | fveqeq2 | |- ( x = B -> ( ( F ` x ) = 4 <-> ( F ` B ) = 4 ) )
12| 11 | elrab | |- ( B e. { x e. RR | ( F ` x ) = 4 } <-> ( B e. RR
/\ ( F ` B ) = 4 ) )
13| 10,12 | sylib | |- ( ph -> ( B e. RR /\ ( F ` B ) = 4 ) )
14| 13 | simpld | |- ( ph -> B e. RR )
15| 14 | recnd | |- ( ph -> B e. CC )
16| 8,15 | subcld | |- ( ph -> ( A - B ) e. CC )
17| 16 | sqcld | |- ( ph -> ( ( A - B ) ^ 2 ) e. CC )
18| 17 | addid1d | |- ( ph -> ( ( ( A - B ) ^ 2 ) + 0 ) = ( ( A - B ) ^
2 ) )
19| | sq0 | |- ( 0 ^ 2 ) = 0
20| 19 | oveq2i | |- ( ( ( A - B ) ^ 2 ) + ( 0 ^ 2 ) ) = ( ( ( A - B )
^ 2 ) + 0 )
21| | 4cn | |- 4 e. CC
22| 21 | subidi | |- ( 4 - 4 ) = 0
23| 22 | oveq1i | |- ( ( 4 - 4 ) ^ 2 ) = ( 0 ^ 2 )
24| 23 | oveq2i | |- ( ( ( A - B ) ^ 2 ) + ( ( 4 - 4 ) ^ 2 ) ) = ( ( (
A - B ) ^ 2 ) + ( 0 ^ 2 ) )
25| 13 | simprd | |- ( ph -> ( F ` B ) = 4 )
26| 25 | oveq2d | |- ( ph -> ( 4 - ( F ` B ) ) = ( 4 - 4 ) )
27| 26 | oveq1d | |- ( ph -> ( ( 4 - ( F ` B ) ) ^ 2 ) = ( ( 4 - 4 ) ^
2 ) )
28| 27 | oveq2d | |- ( ph -> ( ( ( A - B ) ^ 2 ) + ( ( 4 - ( F ` B ) )
^ 2 ) ) = ( ( ( A - B ) ^ 2 ) + ( ( 4 - 4 ) ^ 2 ) ) )
29| 6 | simprd | |- ( ph -> ( F ` A ) = 4 )
30| 29 | oveq1d | |- ( ph -> ( ( F ` A ) - ( F ` B ) ) = ( 4 - ( F ` B
) ) )
31| 30 | oveq1d | |- ( ph -> ( ( ( F ` A ) - ( F ` B ) ) ^ 2 ) = ( ( 4
- ( F ` B ) ) ^ 2 ) )
32| 31 | oveq2d | |- ( ph -> ( ( ( A - B ) ^ 2 ) + ( ( ( F ` A ) - ( F
` B ) ) ^ 2 ) ) = ( ( ( A - B ) ^ 2 ) + ( ( 4 - ( F ` B ) ) ^ 2 ) ) )
33| | AneB.4 | |- ( ph -> ( ( ( A - B ) ^ 2 ) + ( ( ( F ` A ) - ( F
` B ) ) ^ 2 ) ) = ( 6 ^ 2 ) )
34| 32,33 | eqtr3d | |- ( ph -> ( ( ( A - B ) ^ 2 ) + ( ( 4 - ( F ` B ) )
^ 2 ) ) = ( 6 ^ 2 ) )
35| 28,34 | eqtr3d | |- ( ph -> ( ( ( A - B ) ^ 2 ) + ( ( 4 - 4 ) ^ 2 ) )
= ( 6 ^ 2 ) )
36| 24,35 | eqtr3id | |- ( ph -> ( ( ( A - B ) ^ 2 ) + ( 0 ^ 2 ) ) = ( 6 ^
2 ) )
37| 20,36 | eqtr3id | |- ( ph -> ( ( ( A - B ) ^ 2 ) + 0 ) = ( 6 ^ 2 ) )
38| 18,37 | eqtr3d | |- ( ph -> ( ( A - B ) ^ 2 ) = ( 6 ^ 2 ) )
39| | 6nn | |- 6 e. NN
40| 39 | a1i | |- ( ph -> 6 e. NN )
41| 40 | nnsqcld | |- ( ph -> ( 6 ^ 2 ) e. NN )
42| 41 | nnne0d | |- ( ph -> ( 6 ^ 2 ) =/= 0 )
43| 38,42 | eqnetrd | |- ( ph -> ( ( A - B ) ^ 2 ) =/= 0 )
44| | sq0i | |- ( ( A - B ) = 0 -> ( ( A - B ) ^ 2 ) = 0 )
45| 44 | adantl | |- ( ( ph /\ ( A - B ) = 0 ) -> ( ( A - B ) ^ 2 ) = 0
)
46| 43,45 | mteqand | |- ( ph -> ( A - B ) =/= 0 )
47| 8,15,46 | subne0ad | |- ( ph -> A =/= B )
----------------------------------------------------------------------------------------------------------------------------------------------------
