Metamath Proof Explorer


Theorem mulgt1

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 AB1<A1<B1<AB

Proof

Step Hyp Ref Expression
1 1red AB1<A1<B1
2 simpll AB1<A1<BA
3 remulcl ABAB
4 3 adantr AB1<A1<BAB
5 simprl AB1<A1<B1<A
6 simprr AB1<A1<B1<B
7 0red AB1<A1<B0
8 0lt1 0<1
9 8 a1i AB1<A1<B0<1
10 7 1 2 9 5 lttrd AB1<A1<B0<A
11 ltmulgt11 AB0<A1<BA<AB
12 11 3expa AB0<A1<BA<AB
13 10 12 syldan AB1<A1<B1<BA<AB
14 6 13 mpbid AB1<A1<BA<AB
15 1 2 4 5 14 lttrd AB1<A1<B1<AB