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 ) |