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

Metamath Proof Explorer

Theorem zaddcomlem

Description: Lemma for zaddcom . (Contributed by SN, 1-Feb-2025)

Ref Expression
Assertion zaddcomlem ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → 𝐵 ∈ ℕ0 )
2 1 nn0cnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
3 rernegcl ⊢ ( 𝐴 ∈ ℝ → ( 0 −ℝ 𝐴 ) ∈ ℝ )
4 3 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( 0 −ℝ 𝐴 ) ∈ ℝ )
5 4 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( 0 −ℝ 𝐴 ) ∈ ℂ )
6 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → 𝐴 ∈ ℝ )
7 6 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
8 2 5 7 addassd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐵 + ( 0 −ℝ 𝐴 ) ) + 𝐴 ) = ( 𝐵 + ( ( 0 −ℝ 𝐴 ) + 𝐴 ) ) )
9 renegid2 ⊢ ( 𝐴 ∈ ℝ → ( ( 0 −ℝ 𝐴 ) + 𝐴 ) = 0 )
10 9 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( ( 0 −ℝ 𝐴 ) + 𝐴 ) = 0 )
11 10 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( 𝐵 + ( ( 0 −ℝ 𝐴 ) + 𝐴 ) ) = ( 𝐵 + 0 ) )
12 nn0re ⊢ ( 𝐵 ∈ ℕ0 → 𝐵 ∈ ℝ )
13 readdrid ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 + 0 ) = 𝐵 )
14 12 13 syl ⊢ ( 𝐵 ∈ ℕ0 → ( 𝐵 + 0 ) = 𝐵 )
15 14 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( 𝐵 + 0 ) = 𝐵 )
16 8 11 15 3eqtrrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → 𝐵 = ( ( 𝐵 + ( 0 −ℝ 𝐴 ) ) + 𝐴 ) )
17 9 oveq1d ⊢ ( 𝐴 ∈ ℝ → ( ( ( 0 −ℝ 𝐴 ) + 𝐴 ) + 𝐵 ) = ( 0 + 𝐵 ) )
18 17 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) → ( ( ( 0 −ℝ 𝐴 ) + 𝐴 ) + 𝐵 ) = ( 0 + 𝐵 ) )
19 readdlid ⊢ ( 𝐵 ∈ ℝ → ( 0 + 𝐵 ) = 𝐵 )
20 12 19 syl ⊢ ( 𝐵 ∈ ℕ0 → ( 0 + 𝐵 ) = 𝐵 )
21 18 20 sylan9eq ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( ( ( 0 −ℝ 𝐴 ) + 𝐴 ) + 𝐵 ) = 𝐵 )
22 nnnn0 ⊢ ( ( 0 −ℝ 𝐴 ) ∈ ℕ → ( 0 −ℝ 𝐴 ) ∈ ℕ0 )
23 nn0addcom ⊢ ( ( ( 0 −ℝ 𝐴 ) ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 0 −ℝ 𝐴 ) + 𝐵 ) = ( 𝐵 + ( 0 −ℝ 𝐴 ) ) )
24 22 23 sylan ⊢ ( ( ( 0 −ℝ 𝐴 ) ∈ ℕ ∧ 𝐵 ∈ ℕ0 ) → ( ( 0 −ℝ 𝐴 ) + 𝐵 ) = ( 𝐵 + ( 0 −ℝ 𝐴 ) ) )
25 24 adantll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( ( 0 −ℝ 𝐴 ) + 𝐵 ) = ( 𝐵 + ( 0 −ℝ 𝐴 ) ) )
26 25 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( ( ( 0 −ℝ 𝐴 ) + 𝐵 ) + 𝐴 ) = ( ( 𝐵 + ( 0 −ℝ 𝐴 ) ) + 𝐴 ) )
27 16 21 26 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( ( ( 0 −ℝ 𝐴 ) + 𝐴 ) + 𝐵 ) = ( ( ( 0 −ℝ 𝐴 ) + 𝐵 ) + 𝐴 ) )
28 5 7 2 addassd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( ( ( 0 −ℝ 𝐴 ) + 𝐴 ) + 𝐵 ) = ( ( 0 −ℝ 𝐴 ) + ( 𝐴 + 𝐵 ) ) )
29 5 2 7 addassd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( ( ( 0 −ℝ 𝐴 ) + 𝐵 ) + 𝐴 ) = ( ( 0 −ℝ 𝐴 ) + ( 𝐵 + 𝐴 ) ) )
30 27 28 29 3eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( ( 0 −ℝ 𝐴 ) + ( 𝐴 + 𝐵 ) ) = ( ( 0 −ℝ 𝐴 ) + ( 𝐵 + 𝐴 ) ) )
31 7 2 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
32 2 7 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( 𝐵 + 𝐴 ) ∈ ℂ )
33 5 31 32 sn-addcand ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( ( ( 0 −ℝ 𝐴 ) + ( 𝐴 + 𝐵 ) ) = ( ( 0 −ℝ 𝐴 ) + ( 𝐵 + 𝐴 ) ) ↔ ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) ) )
34 30 33 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )