Metamath Proof Explorer


Theorem int-ineqmvtd

Description: IneqMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020)

Ref Expression
Hypotheses int-ineqmvtd.1 ( 𝜑𝐵 ∈ ℝ )
int-ineqmvtd.2 ( 𝜑𝐶 ∈ ℝ )
int-ineqmvtd.3 ( 𝜑𝐷 ∈ ℝ )
int-ineqmvtd.4 ( 𝜑𝐵𝐴 )
int-ineqmvtd.5 ( 𝜑𝐴 = ( 𝐶 + 𝐷 ) )
Assertion int-ineqmvtd ( 𝜑 → ( 𝐵𝐷 ) ≤ 𝐶 )

Proof

Step Hyp Ref Expression
1 int-ineqmvtd.1 ( 𝜑𝐵 ∈ ℝ )
2 int-ineqmvtd.2 ( 𝜑𝐶 ∈ ℝ )
3 int-ineqmvtd.3 ( 𝜑𝐷 ∈ ℝ )
4 int-ineqmvtd.4 ( 𝜑𝐵𝐴 )
5 int-ineqmvtd.5 ( 𝜑𝐴 = ( 𝐶 + 𝐷 ) )
6 4 5 breqtrd ( 𝜑𝐵 ≤ ( 𝐶 + 𝐷 ) )
7 1 3 2 lesubaddd ( 𝜑 → ( ( 𝐵𝐷 ) ≤ 𝐶𝐵 ≤ ( 𝐶 + 𝐷 ) ) )
8 6 7 mpbird ( 𝜑 → ( 𝐵𝐷 ) ≤ 𝐶 )