Metamath Proof Explorer


Theorem mulgt1d

Description: The product of two numbers greater than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses ltp1d.1 φA
divgt0d.2 φB
mulgt1d.3 φ1<A
mulgt1d.4 φ1<B
Assertion mulgt1d φ1<AB

Proof

Step Hyp Ref Expression
1 ltp1d.1 φA
2 divgt0d.2 φB
3 mulgt1d.3 φ1<A
4 mulgt1d.4 φ1<B
5 mulgt1 AB1<A1<B1<AB
6 1 2 3 4 5 syl22anc φ1<AB