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

Proof

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