Description: The product of two numbers greater than 1 is greater than 1. (Contributed by NM, 13-Feb-2005) (Proof shortened by SN, 29-Jun-2025)
Ref | Expression | ||
---|---|---|---|
Assertion | mulgt1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1red | |
|
2 | simpll | |
|
3 | remulcl | |
|
4 | 3 | adantr | |
5 | simprl | |
|
6 | simprr | |
|
7 | 0red | |
|
8 | 0lt1 | |
|
9 | 8 | a1i | |
10 | 7 1 2 9 5 | lttrd | |
11 | ltmulgt11 | |
|
12 | 11 | 3expa | |
13 | 10 12 | syldan | |
14 | 6 13 | mpbid | |
15 | 1 2 4 5 14 | lttrd | |