Description: The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, justified by theorem axpre-mulgt0 . Normally new proofs would use axmulgt0 . (New usage is discouraged.) (Contributed by NM, 13-Oct-2005)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax-pre-mulgt0 | |- ( ( A e. RR /\ B e. RR ) -> ( ( 0 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cA | |- A |
|
| 1 | cr | |- RR |
|
| 2 | 0 1 | wcel | |- A e. RR |
| 3 | cB | |- B |
|
| 4 | 3 1 | wcel | |- B e. RR |
| 5 | 2 4 | wa | |- ( A e. RR /\ B e. RR ) |
| 6 | cc0 | |- 0 |
|
| 7 | cltrr | |- |
|
| 8 | 6 0 7 | wbr | |- 0 |
| 9 | 6 3 7 | wbr | |- 0 |
| 10 | 8 9 | wa | |- ( 0 |
| 11 | cmul | |- x. |
|
| 12 | 0 3 11 | co | |- ( A x. B ) |
| 13 | 6 12 7 | wbr | |- 0 |
| 14 | 10 13 | wi | |- ( ( 0 |
| 15 | 5 14 | wi | |- ( ( A e. RR /\ B e. RR ) -> ( ( 0 |