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

Metamath Proof Explorer

Theorem renpncan3

Description: Cancellation law for real subtraction. Compare npncan3 . (Contributed by Steven Nguyen, 28-Jan-2023)

Ref Expression
Assertion renpncan3 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐵 ) + ( 𝐶 −ℝ 𝐴 ) ) = ( 𝐶 −ℝ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
2 rersubcl ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐶 −ℝ 𝐴 ) ∈ ℝ )
3 2 ancoms ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 −ℝ 𝐴 ) ∈ ℝ )
4 3 3adant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 −ℝ 𝐴 ) ∈ ℝ )
5 simp2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
6 readdsub ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 −ℝ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + ( 𝐶 −ℝ 𝐴 ) ) −ℝ 𝐵 ) = ( ( 𝐴 −ℝ 𝐵 ) + ( 𝐶 −ℝ 𝐴 ) ) )
7 1 4 5 6 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 + ( 𝐶 −ℝ 𝐴 ) ) −ℝ 𝐵 ) = ( ( 𝐴 −ℝ 𝐵 ) + ( 𝐶 −ℝ 𝐴 ) ) )
8 repncan3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + ( 𝐶 −ℝ 𝐴 ) ) = 𝐶 )
9 8 3adant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + ( 𝐶 −ℝ 𝐴 ) ) = 𝐶 )
10 9 oveq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 + ( 𝐶 −ℝ 𝐴 ) ) −ℝ 𝐵 ) = ( 𝐶 −ℝ 𝐵 ) )
11 7 10 eqtr3d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐵 ) + ( 𝐶 −ℝ 𝐴 ) ) = ( 𝐶 −ℝ 𝐵 ) )