Metamath Proof Explorer

Theorem mulgt1OLD

Description: Obsolete version of mulgt1 as of 29-Jun-2025. (Contributed by NM, 13-Feb-2005) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion mulgt1OLD ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 1 < A ∧ 1 < B → 1 < A ⁢ B

Proof

Step Hyp Ref Expression
1 simpl ⊢ 1 < A ∧ 1 < B → 1 < A
2 1 a1i ⊢ A ∈ ℝ ∧ B ∈ ℝ → 1 < A ∧ 1 < B → 1 < A
3 0lt1 ⊢ 0 < 1
4 0re ⊢ 0 ∈ ℝ
5 1re ⊢ 1 ∈ ℝ
6 lttr ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ A ∈ ℝ → 0 < 1 ∧ 1 < A → 0 < A
7 4 5 6 mp3an12 ⊢ A ∈ ℝ → 0 < 1 ∧ 1 < A → 0 < A
8 3 7 mpani ⊢ A ∈ ℝ → 1 < A → 0 < A
9 8 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ → 1 < A → 0 < A
10 ltmul2 ⊢ 1 ∈ ℝ ∧ B ∈ ℝ ∧ A ∈ ℝ ∧ 0 < A → 1 < B ↔ A ⋅ 1 < A ⁢ B
11 10 biimpd ⊢ 1 ∈ ℝ ∧ B ∈ ℝ ∧ A ∈ ℝ ∧ 0 < A → 1 < B → A ⋅ 1 < A ⁢ B
12 5 11 mp3an1 ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ 0 < A → 1 < B → A ⋅ 1 < A ⁢ B
13 12 exp32 ⊢ B ∈ ℝ → A ∈ ℝ → 0 < A → 1 < B → A ⋅ 1 < A ⁢ B
14 13 impcom ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < A → 1 < B → A ⋅ 1 < A ⁢ B
15 9 14 syld ⊢ A ∈ ℝ ∧ B ∈ ℝ → 1 < A → 1 < B → A ⋅ 1 < A ⁢ B
16 15 impd ⊢ A ∈ ℝ ∧ B ∈ ℝ → 1 < A ∧ 1 < B → A ⋅ 1 < A ⁢ B
17 ax-1rid ⊢ A ∈ ℝ → A ⋅ 1 = A
18 17 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ⋅ 1 = A
19 18 breq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ⋅ 1 < A ⁢ B ↔ A < A ⁢ B
20 16 19 sylibd ⊢ A ∈ ℝ ∧ B ∈ ℝ → 1 < A ∧ 1 < B → A < A ⁢ B
21 2 20 jcad ⊢ A ∈ ℝ ∧ B ∈ ℝ → 1 < A ∧ 1 < B → 1 < A ∧ A < A ⁢ B
22 remulcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ⁢ B ∈ ℝ
23 lttr ⊢ 1 ∈ ℝ ∧ A ∈ ℝ ∧ A ⁢ B ∈ ℝ → 1 < A ∧ A < A ⁢ B → 1 < A ⁢ B
24 5 23 mp3an1 ⊢ A ∈ ℝ ∧ A ⁢ B ∈ ℝ → 1 < A ∧ A < A ⁢ B → 1 < A ⁢ B
25 22 24 syldan ⊢ A ∈ ℝ ∧ B ∈ ℝ → 1 < A ∧ A < A ⁢ B → 1 < A ⁢ B
26 21 25 syld ⊢ A ∈ ℝ ∧ B ∈ ℝ → 1 < A ∧ 1 < B → 1 < A ⁢ B
27 26 imp ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 1 < A ∧ 1 < B → 1 < A ⁢ B