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 ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )