Metamath Proof Explorer


Theorem xmulasslem

Description: Lemma for xmulass . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses xmulasslem.1
|- ( x = D -> ( ps <-> X = Y ) )
xmulasslem.2
|- ( x = -e D -> ( ps <-> E = F ) )
xmulasslem.x
|- ( ph -> X e. RR* )
xmulasslem.y
|- ( ph -> Y e. RR* )
xmulasslem.d
|- ( ph -> D e. RR* )
xmulasslem.ps
|- ( ( ph /\ ( x e. RR* /\ 0 < x ) ) -> ps )
xmulasslem.0
|- ( ph -> ( x = 0 -> ps ) )
xmulasslem.e
|- ( ph -> E = -e X )
xmulasslem.f
|- ( ph -> F = -e Y )
Assertion xmulasslem
|- ( ph -> X = Y )

Proof

Step Hyp Ref Expression
1 xmulasslem.1
 |-  ( x = D -> ( ps <-> X = Y ) )
2 xmulasslem.2
 |-  ( x = -e D -> ( ps <-> E = F ) )
3 xmulasslem.x
 |-  ( ph -> X e. RR* )
4 xmulasslem.y
 |-  ( ph -> Y e. RR* )
5 xmulasslem.d
 |-  ( ph -> D e. RR* )
6 xmulasslem.ps
 |-  ( ( ph /\ ( x e. RR* /\ 0 < x ) ) -> ps )
7 xmulasslem.0
 |-  ( ph -> ( x = 0 -> ps ) )
8 xmulasslem.e
 |-  ( ph -> E = -e X )
9 xmulasslem.f
 |-  ( ph -> F = -e Y )
10 0xr
 |-  0 e. RR*
11 xrltso
 |-  < Or RR*
12 solin
 |-  ( ( < Or RR* /\ ( D e. RR* /\ 0 e. RR* ) ) -> ( D < 0 \/ D = 0 \/ 0 < D ) )
13 11 12 mpan
 |-  ( ( D e. RR* /\ 0 e. RR* ) -> ( D < 0 \/ D = 0 \/ 0 < D ) )
14 5 10 13 sylancl
 |-  ( ph -> ( D < 0 \/ D = 0 \/ 0 < D ) )
15 xlt0neg1
 |-  ( D e. RR* -> ( D < 0 <-> 0 < -e D ) )
16 5 15 syl
 |-  ( ph -> ( D < 0 <-> 0 < -e D ) )
17 xnegcl
 |-  ( D e. RR* -> -e D e. RR* )
18 5 17 syl
 |-  ( ph -> -e D e. RR* )
19 breq2
 |-  ( x = -e D -> ( 0 < x <-> 0 < -e D ) )
20 19 2 imbi12d
 |-  ( x = -e D -> ( ( 0 < x -> ps ) <-> ( 0 < -e D -> E = F ) ) )
21 20 imbi2d
 |-  ( x = -e D -> ( ( ph -> ( 0 < x -> ps ) ) <-> ( ph -> ( 0 < -e D -> E = F ) ) ) )
22 6 exp32
 |-  ( ph -> ( x e. RR* -> ( 0 < x -> ps ) ) )
23 22 com12
 |-  ( x e. RR* -> ( ph -> ( 0 < x -> ps ) ) )
24 21 23 vtoclga
 |-  ( -e D e. RR* -> ( ph -> ( 0 < -e D -> E = F ) ) )
25 18 24 mpcom
 |-  ( ph -> ( 0 < -e D -> E = F ) )
26 16 25 sylbid
 |-  ( ph -> ( D < 0 -> E = F ) )
27 8 9 eqeq12d
 |-  ( ph -> ( E = F <-> -e X = -e Y ) )
28 xneg11
 |-  ( ( X e. RR* /\ Y e. RR* ) -> ( -e X = -e Y <-> X = Y ) )
29 3 4 28 syl2anc
 |-  ( ph -> ( -e X = -e Y <-> X = Y ) )
30 27 29 bitrd
 |-  ( ph -> ( E = F <-> X = Y ) )
31 26 30 sylibd
 |-  ( ph -> ( D < 0 -> X = Y ) )
32 eqeq1
 |-  ( x = D -> ( x = 0 <-> D = 0 ) )
33 32 1 imbi12d
 |-  ( x = D -> ( ( x = 0 -> ps ) <-> ( D = 0 -> X = Y ) ) )
34 33 imbi2d
 |-  ( x = D -> ( ( ph -> ( x = 0 -> ps ) ) <-> ( ph -> ( D = 0 -> X = Y ) ) ) )
35 34 7 vtoclg
 |-  ( D e. RR* -> ( ph -> ( D = 0 -> X = Y ) ) )
36 5 35 mpcom
 |-  ( ph -> ( D = 0 -> X = Y ) )
37 breq2
 |-  ( x = D -> ( 0 < x <-> 0 < D ) )
38 37 1 imbi12d
 |-  ( x = D -> ( ( 0 < x -> ps ) <-> ( 0 < D -> X = Y ) ) )
39 38 imbi2d
 |-  ( x = D -> ( ( ph -> ( 0 < x -> ps ) ) <-> ( ph -> ( 0 < D -> X = Y ) ) ) )
40 39 23 vtoclga
 |-  ( D e. RR* -> ( ph -> ( 0 < D -> X = Y ) ) )
41 5 40 mpcom
 |-  ( ph -> ( 0 < D -> X = Y ) )
42 31 36 41 3jaod
 |-  ( ph -> ( ( D < 0 \/ D = 0 \/ 0 < D ) -> X = Y ) )
43 14 42 mpd
 |-  ( ph -> X = Y )