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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ltnegd.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ltadd1d.3 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
lesub3d.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
lesub3d.g ⊢ ( 𝜑 → ( 𝑋 + 𝐶 ) ≤ 𝐴 )
lesub3d.l ⊢ ( 𝜑 → 𝐵 ≤ 𝑋 )
Assertion lesub3d ( 𝜑 → 𝐶 ≤ ( 𝐴 − 𝐵 ) )

Proof

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