This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 1 < A ∧ 1 < B → 1 < A ⁢ B

Proof

Step Hyp Ref Expression
1 1red ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 1 < A ∧ 1 < B → 1 ∈ ℝ
2 simpll ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 1 < A ∧ 1 < B → A ∈ ℝ
3 remulcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ⁢ B ∈ ℝ
4 3 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 1 < A ∧ 1 < B → A ⁢ B ∈ ℝ
5 simprl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 1 < A ∧ 1 < B → 1 < A
6 simprr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 1 < A ∧ 1 < B → 1 < B
7 0red ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 1 < A ∧ 1 < B → 0 ∈ ℝ
8 0lt1 ⊢ 0 < 1
9 8 a1i ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 1 < A ∧ 1 < B → 0 < 1
10 7 1 2 9 5 lttrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 1 < A ∧ 1 < B → 0 < A
11 ltmulgt11 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < A → 1 < B ↔ A < A ⁢ B
12 11 3expa ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < A → 1 < B ↔ A < A ⁢ B
13 10 12 syldan ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 1 < A ∧ 1 < B → 1 < B ↔ A < A ⁢ B
14 6 13 mpbid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 1 < A ∧ 1 < B → A < A ⁢ B
15 1 2 4 5 14 lttrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 1 < A ∧ 1 < B → 1 < A ⁢ B