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

Metamath Proof Explorer

Theorem resubidaddlidlem

Description: Lemma for resubidaddlid . A special case of npncan . (Contributed by Steven Nguyen, 8-Jan-2023)

Ref Expression
Hypotheses resubidaddridlem.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
resubidaddridlem.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
resubidaddridlem.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
resubidaddridlem.1 ⊢ ( 𝜑 → ( 𝐴 −ℝ 𝐵 ) = ( 𝐵 −ℝ 𝐶 ) )
Assertion resubidaddlidlem ( 𝜑 → ( ( 𝐴 −ℝ 𝐵 ) + ( 𝐵 −ℝ 𝐶 ) ) = ( 𝐴 −ℝ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 resubidaddridlem.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 resubidaddridlem.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 resubidaddridlem.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4 resubidaddridlem.1 ⊢ ( 𝜑 → ( 𝐴 −ℝ 𝐵 ) = ( 𝐵 −ℝ 𝐶 ) )
5 rersubcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 −ℝ 𝐵 ) ∈ ℝ )
6 1 2 5 syl2anc ⊢ ( 𝜑 → ( 𝐴 −ℝ 𝐵 ) ∈ ℝ )
7 rersubcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 −ℝ 𝐶 ) ∈ ℝ )
8 2 3 7 syl2anc ⊢ ( 𝜑 → ( 𝐵 −ℝ 𝐶 ) ∈ ℝ )
9 6 8 readdcld ⊢ ( 𝜑 → ( ( 𝐴 −ℝ 𝐵 ) + ( 𝐵 −ℝ 𝐶 ) ) ∈ ℝ )
10 4 eqcomd ⊢ ( 𝜑 → ( 𝐵 −ℝ 𝐶 ) = ( 𝐴 −ℝ 𝐵 ) )
11 2 3 6 resubaddd ⊢ ( 𝜑 → ( ( 𝐵 −ℝ 𝐶 ) = ( 𝐴 −ℝ 𝐵 ) ↔ ( 𝐶 + ( 𝐴 −ℝ 𝐵 ) ) = 𝐵 ) )
12 10 11 mpbid ⊢ ( 𝜑 → ( 𝐶 + ( 𝐴 −ℝ 𝐵 ) ) = 𝐵 )
13 12 oveq1d ⊢ ( 𝜑 → ( ( 𝐶 + ( 𝐴 −ℝ 𝐵 ) ) + ( 𝐵 −ℝ 𝐶 ) ) = ( 𝐵 + ( 𝐵 −ℝ 𝐶 ) ) )
14 3 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
15 6 recnd ⊢ ( 𝜑 → ( 𝐴 −ℝ 𝐵 ) ∈ ℂ )
16 8 recnd ⊢ ( 𝜑 → ( 𝐵 −ℝ 𝐶 ) ∈ ℂ )
17 14 15 16 addassd ⊢ ( 𝜑 → ( ( 𝐶 + ( 𝐴 −ℝ 𝐵 ) ) + ( 𝐵 −ℝ 𝐶 ) ) = ( 𝐶 + ( ( 𝐴 −ℝ 𝐵 ) + ( 𝐵 −ℝ 𝐶 ) ) ) )
18 1 2 8 resubaddd ⊢ ( 𝜑 → ( ( 𝐴 −ℝ 𝐵 ) = ( 𝐵 −ℝ 𝐶 ) ↔ ( 𝐵 + ( 𝐵 −ℝ 𝐶 ) ) = 𝐴 ) )
19 4 18 mpbid ⊢ ( 𝜑 → ( 𝐵 + ( 𝐵 −ℝ 𝐶 ) ) = 𝐴 )
20 13 17 19 3eqtr3d ⊢ ( 𝜑 → ( 𝐶 + ( ( 𝐴 −ℝ 𝐵 ) + ( 𝐵 −ℝ 𝐶 ) ) ) = 𝐴 )
21 3 9 20 reladdrsub ⊢ ( 𝜑 → ( ( 𝐴 −ℝ 𝐵 ) + ( 𝐵 −ℝ 𝐶 ) ) = ( 𝐴 −ℝ 𝐶 ) )