Description: Obsolete version of 1lt10 as of 10-Jun-2026. (Contributed by NM, 7-Nov-2012) (Revised by Mario Carneiro, 9-Mar-2015) (Revised by AV, 8-Sep-2021) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 1lt10OLD | |- 1 < ; 1 0 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1lt2 | |- 1 < 2 |
|
| 2 | 2lt10 | |- 2 < ; 1 0 |
|
| 3 | 1re | |- 1 e. RR |
|
| 4 | 2re | |- 2 e. RR |
|
| 5 | 10re | |- ; 1 0 e. RR |
|
| 6 | 3 4 5 | lttri | |- ( ( 1 < 2 /\ 2 < ; 1 0 ) -> 1 < ; 1 0 ) |
| 7 | 1 2 6 | mp2an | |- 1 < ; 1 0 |