Description: Natural deduction form of lemul2d . (Contributed by Stanislas Polu, 9-Mar-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | wwlemuld.1 | |- ( ph -> A e. RR ) |
|
wwlemuld.2 | |- ( ph -> B e. RR ) |
||
wwlemuld.3 | |- ( ph -> C e. RR ) |
||
wwlemuld.4 | |- ( ph -> ( C x. A ) <_ ( C x. B ) ) |
||
wwlemuld.5 | |- ( ph -> 0 < C ) |
||
Assertion | wwlemuld | |- ( ph -> A <_ B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wwlemuld.1 | |- ( ph -> A e. RR ) |
|
2 | wwlemuld.2 | |- ( ph -> B e. RR ) |
|
3 | wwlemuld.3 | |- ( ph -> C e. RR ) |
|
4 | wwlemuld.4 | |- ( ph -> ( C x. A ) <_ ( C x. B ) ) |
|
5 | wwlemuld.5 | |- ( ph -> 0 < C ) |
|
6 | 3 5 | elrpd | |- ( ph -> C e. RR+ ) |
7 | 1 2 6 | lemul2d | |- ( ph -> ( A <_ B <-> ( C x. A ) <_ ( C x. B ) ) ) |
8 | 4 7 | mpbird | |- ( ph -> A <_ B ) |