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

Metamath Proof Explorer

Theorem lemul1

Description: Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 21-Feb-2005)

Ref Expression
Assertion lemul1 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 ltmul1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 < 𝐵 ↔ ( 𝐴 · 𝐶 ) < ( 𝐵 · 𝐶 ) ) )
2 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
3 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
4 recn ⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℂ )
5 4 adantr ⊢ ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) → 𝐶 ∈ ℂ )
6 gt0ne0 ⊢ ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) → 𝐶 ≠ 0 )
7 5 6 jca ⊢ ( ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) → ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) )
8 mulcan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) ↔ 𝐴 = 𝐵 ) )
9 2 3 7 8 syl3an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) ↔ 𝐴 = 𝐵 ) )
10 9 bicomd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 = 𝐵 ↔ ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) ) )
11 1 10 orbi12d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ) ↔ ( ( 𝐴 · 𝐶 ) < ( 𝐵 · 𝐶 ) ∨ ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) ) ) )
12 leloe ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ) ) )
13 12 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ) ) )
14 remulcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 𝐶 ) ∈ ℝ )
15 14 3adant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 𝐶 ) ∈ ℝ )
16 remulcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 · 𝐶 ) ∈ ℝ )
17 16 3adant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 · 𝐶 ) ∈ ℝ )
18 15 17 leloed ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ↔ ( ( 𝐴 · 𝐶 ) < ( 𝐵 · 𝐶 ) ∨ ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) ) ) )
19 18 3adant3r ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ↔ ( ( 𝐴 · 𝐶 ) < ( 𝐵 · 𝐶 ) ∨ ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) ) ) )
20 11 13 19 3bitr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ) )