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 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → 1 < ( 𝐴 · 𝐵 ) )

Proof

Step Hyp Ref Expression
1 1red ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → 1 ∈ ℝ )
2 simpll ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → 𝐴 ∈ ℝ )
3 remulcl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 𝐵 ) ∈ ℝ )
4 3 adantr ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → ( 𝐴 · 𝐵 ) ∈ ℝ )
5 simprl ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → 1 < 𝐴 )
6 simprr ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → 1 < 𝐵 )
7 0red ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → 0 ∈ ℝ )
8 0lt1 0 < 1
9 8 a1i ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → 0 < 1 )
10 7 1 2 9 5 lttrd ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → 0 < 𝐴 )
11 ltmulgt11 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐴 ) → ( 1 < 𝐵𝐴 < ( 𝐴 · 𝐵 ) ) )
12 11 3expa ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 0 < 𝐴 ) → ( 1 < 𝐵𝐴 < ( 𝐴 · 𝐵 ) ) )
13 10 12 syldan ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → ( 1 < 𝐵𝐴 < ( 𝐴 · 𝐵 ) ) )
14 6 13 mpbid ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → 𝐴 < ( 𝐴 · 𝐵 ) )
15 1 2 4 5 14 lttrd ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < 𝐴 ∧ 1 < 𝐵 ) ) → 1 < ( 𝐴 · 𝐵 ) )