Metamath Proof Explorer

Theorem readdcan

Description: Cancellation law for addition over the reals. (Contributed by Scott Fenton, 3-Jan-2013) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion readdcan ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C + A = C + B ↔ A = B

Proof

Step Hyp Ref Expression
1 ltadd2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < B ↔ C + A < C + B
2 1 notbid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → ¬ A < B ↔ ¬ C + A < C + B
3 simp2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ∈ ℝ
4 simp1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ∈ ℝ
5 simp3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℝ
6 3 4 5 ltadd2d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B < A ↔ C + B < C + A
7 6 notbid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → ¬ B < A ↔ ¬ C + B < C + A
8 2 7 anbi12d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → ¬ A < B ∧ ¬ B < A ↔ ¬ C + A < C + B ∧ ¬ C + B < C + A
9 4 3 lttri3d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A = B ↔ ¬ A < B ∧ ¬ B < A
10 5 4 readdcld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C + A ∈ ℝ
11 5 3 readdcld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C + B ∈ ℝ
12 10 11 lttri3d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C + A = C + B ↔ ¬ C + A < C + B ∧ ¬ C + B < C + A
13 8 9 12 3bitr4rd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C + A = C + B ↔ A = B