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

Metamath Proof Explorer

Theorem lesub2

Description: Subtraction of both sides of 'less than or equal to'. (Contributed by NM, 29-Sep-2005) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion lesub2 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐶 − 𝐵 ) ≤ ( 𝐶 − 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 leadd2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐶 + 𝐴 ) ≤ ( 𝐶 + 𝐵 ) ) )
2 simp3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
3 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
4 2 3 readdcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 + 𝐴 ) ∈ ℝ )
5 simp2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
6 lesubadd ⊢ ( ( ( 𝐶 + 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐶 + 𝐴 ) − 𝐵 ) ≤ 𝐶 ↔ ( 𝐶 + 𝐴 ) ≤ ( 𝐶 + 𝐵 ) ) )
7 4 5 2 6 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐶 + 𝐴 ) − 𝐵 ) ≤ 𝐶 ↔ ( 𝐶 + 𝐴 ) ≤ ( 𝐶 + 𝐵 ) ) )
8 2 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℂ )
9 3 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℂ )
10 5 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
11 8 9 10 addsubd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐶 + 𝐴 ) − 𝐵 ) = ( ( 𝐶 − 𝐵 ) + 𝐴 ) )
12 11 breq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐶 + 𝐴 ) − 𝐵 ) ≤ 𝐶 ↔ ( ( 𝐶 − 𝐵 ) + 𝐴 ) ≤ 𝐶 ) )
13 1 7 12 3bitr2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ( ( 𝐶 − 𝐵 ) + 𝐴 ) ≤ 𝐶 ) )
14 2 5 resubcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
15 leaddsub ⊢ ( ( ( 𝐶 − 𝐵 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐶 − 𝐵 ) + 𝐴 ) ≤ 𝐶 ↔ ( 𝐶 − 𝐵 ) ≤ ( 𝐶 − 𝐴 ) ) )
16 14 3 2 15 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐶 − 𝐵 ) + 𝐴 ) ≤ 𝐶 ↔ ( 𝐶 − 𝐵 ) ≤ ( 𝐶 − 𝐴 ) ) )
17 13 16 bitrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐶 − 𝐵 ) ≤ ( 𝐶 − 𝐴 ) ) )