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

Metamath Proof Explorer

Theorem lesub3d

Description: The result of subtracting a number less than or equal to an intermediate number from a number greater than or equal to a third number increased by the intermediate number is greater than or equal to the third number. (Contributed by AV, 13-Aug-2020)

Ref Expression
Hypotheses leidd.1 ⊢ φ → A ∈ ℝ
ltnegd.2 ⊢ φ → B ∈ ℝ
ltadd1d.3 ⊢ φ → C ∈ ℝ
lesub3d.x ⊢ φ → X ∈ ℝ
lesub3d.g ⊢ φ → X + C ≤ A
lesub3d.l ⊢ φ → B ≤ X
Assertion lesub3d ⊢ φ → C ≤ A − B

Proof

Step Hyp Ref Expression
1 leidd.1 ⊢ φ → A ∈ ℝ
2 ltnegd.2 ⊢ φ → B ∈ ℝ
3 ltadd1d.3 ⊢ φ → C ∈ ℝ
4 lesub3d.x ⊢ φ → X ∈ ℝ
5 lesub3d.g ⊢ φ → X + C ≤ A
6 lesub3d.l ⊢ φ → B ≤ X
7 3 2 readdcld ⊢ φ → C + B ∈ ℝ
8 4 3 readdcld ⊢ φ → X + C ∈ ℝ
9 3 recnd ⊢ φ → C ∈ ℂ
10 2 recnd ⊢ φ → B ∈ ℂ
11 9 10 addcomd ⊢ φ → C + B = B + C
12 2 4 3 6 leadd1dd ⊢ φ → B + C ≤ X + C
13 11 12 eqbrtrd ⊢ φ → C + B ≤ X + C
14 7 8 1 13 5 letrd ⊢ φ → C + B ≤ A
15 leaddsub ⊢ C ∈ ℝ ∧ B ∈ ℝ ∧ A ∈ ℝ → C + B ≤ A ↔ C ≤ A − B
16 3 2 1 15 syl3anc ⊢ φ → C + B ≤ A ↔ C ≤ A − B
17 14 16 mpbid ⊢ φ → C ≤ A − B