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 < ( 𝐴 · 𝐵 ) )