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 )