Theorem wwlemuld

Description: Natural deduction form of lemul2d . (Contributed by Stanislas Polu, 9-Mar-2020)

	Ref	Expression
Hypotheses	wwlemuld.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	wwlemuld.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	wwlemuld.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	wwlemuld.4	⊢ ( 𝜑 → ( 𝐶 · 𝐴 ) ≤ ( 𝐶 · 𝐵 ) )
	wwlemuld.5	⊢ ( 𝜑 → 0 < 𝐶 )
Assertion	wwlemuld	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		wwlemuld.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		wwlemuld.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		wwlemuld.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		wwlemuld.4	⊢ ( 𝜑 → ( 𝐶 · 𝐴 ) ≤ ( 𝐶 · 𝐵 ) )
5		wwlemuld.5	⊢ ( 𝜑 → 0 < 𝐶 )
6	3 5	elrpd	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
7	1 2 6	lemul2d	⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ( 𝐶 · 𝐴 ) ≤ ( 𝐶 · 𝐵 ) ) )
8	4 7	mpbird	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )