Theorem zaddcomlem

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

	Ref	Expression
Assertion	zaddcomlem	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to A+B=B+A$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to B\in {\mathbb{N}}_0$$
2	1	nn0cnd	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to B\in ℂ$$
3		rernegcl	$$⊢A\in ℝ\to 0{-}_{ℝ}A\in ℝ$$
4	3	ad2antrr	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to 0{-}_{ℝ}A\in ℝ$$
5	4	recnd	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to 0{-}_{ℝ}A\in ℂ$$
6		simpll	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to A\in ℝ$$
7	6	recnd	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to A\in ℂ$$
8	2 5 7	addassd	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to B+\left(0{-}_{ℝ}A\right)+A=B+\left(0{-}_{ℝ}A\right)+A$$
9		renegid2	$$⊢A\in ℝ\to \left(0{-}_{ℝ}A\right)+A=0$$
10	9	ad2antrr	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to \left(0{-}_{ℝ}A\right)+A=0$$
11	10	oveq2d	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to B+\left(0{-}_{ℝ}A\right)+A=B+0$$
12		nn0re	$$⊢B\in {\mathbb{N}}_0\to B\in ℝ$$
13		readdrid	$$⊢B\in ℝ\to B+0=B$$
14	12 13	syl	$$⊢B\in {\mathbb{N}}_0\to B+0=B$$
15	14	adantl	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to B+0=B$$
16	8 11 15	3eqtrrd	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to B=B+\left(0{-}_{ℝ}A\right)+A$$
17	9	oveq1d	$$⊢A\in ℝ\to \left(0{-}_{ℝ}A\right)+A+B=0+B$$
18	17	adantr	$$⊢\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\to \left(0{-}_{ℝ}A\right)+A+B=0+B$$
19		readdlid	$$⊢B\in ℝ\to 0+B=B$$
20	12 19	syl	$$⊢B\in {\mathbb{N}}_0\to 0+B=B$$
21	18 20	sylan9eq	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to \left(0{-}_{ℝ}A\right)+A+B=B$$
22		nnnn0	$$⊢0{-}_{ℝ}A\in \mathbb{N}\to 0{-}_{ℝ}A\in {\mathbb{N}}_0$$
23		nn0addcom	$$⊢\left(0{-}_{ℝ}A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left(0{-}_{ℝ}A\right)+B=B+\left(0{-}_{ℝ}A\right)$$
24	22 23	sylan	$$⊢\left(0{-}_{ℝ}A\in \mathbb{N}\wedge B\in {\mathbb{N}}_0\right)\to \left(0{-}_{ℝ}A\right)+B=B+\left(0{-}_{ℝ}A\right)$$
25	24	adantll	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to \left(0{-}_{ℝ}A\right)+B=B+\left(0{-}_{ℝ}A\right)$$
26	25	oveq1d	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to \left(0{-}_{ℝ}A\right)+B+A=B+\left(0{-}_{ℝ}A\right)+A$$
27	16 21 26	3eqtr4d	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to \left(0{-}_{ℝ}A\right)+A+B=\left(0{-}_{ℝ}A\right)+B+A$$
28	5 7 2	addassd	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to \left(0{-}_{ℝ}A\right)+A+B=\left(0{-}_{ℝ}A\right)+A+B$$
29	5 2 7	addassd	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to \left(0{-}_{ℝ}A\right)+B+A=\left(0{-}_{ℝ}A\right)+B+A$$
30	27 28 29	3eqtr3d	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to \left(0{-}_{ℝ}A\right)+A+B=\left(0{-}_{ℝ}A\right)+B+A$$
31	7 2	addcld	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to A+B\in ℂ$$
32	2 7	addcld	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to B+A\in ℂ$$
33	5 31 32	sn-addcand	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to \left(\left(0{-}_{ℝ}A\right)+A+B=\left(0{-}_{ℝ}A\right)+B+A\leftrightarrow A+B=B+A\right)$$
34	30 33	mpbid	$$⊢\left(\left(A\in ℝ\wedge 0{-}_{ℝ}A\in \mathbb{N}\right)\wedge B\in {\mathbb{N}}_0\right)\to A+B=B+A$$