zaddcom

Description: Addition is commutative for integers. Proven without ax-mulcom . (Contributed by SN, 25-Jan-2025)

		Ref	Expression
	Assertion	zaddcom	$⊢ (A \in ℤ \land B \in ℤ) \to A + B = B + A$

Proof

Step	Hyp	Ref	Expression
1		reelznn0nn	$⊢ A \in ℤ \leftrightarrow (A \in ℕ_{0} \lor (A \in ℝ \land 0 -_{ℝ} A \in ℕ))$
2		reelznn0nn	$⊢ B \in ℤ \leftrightarrow (B \in ℕ_{0} \lor (B \in ℝ \land 0 -_{ℝ} B \in ℕ))$
3		nn0addcom	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to A + B = B + A$
4		zaddcomlem	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land B \in ℕ_{0}) \to A + B = B + A$
5		zaddcomlem	$⊢ ((B \in ℝ \land 0 -_{ℝ} B \in ℕ) \land A \in ℕ_{0}) \to B + A = A + B$
6	5	eqcomd	$⊢ ((B \in ℝ \land 0 -_{ℝ} B \in ℕ) \land A \in ℕ_{0}) \to A + B = B + A$
7	6	ancoms	$⊢ (A \in ℕ_{0} \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to A + B = B + A$
8		renegid2	$⊢ B \in ℝ \to (0 -_{ℝ} B) + B = 0$
9	8	ad2antrl	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to (0 -_{ℝ} B) + B = 0$
10		renegid2	$⊢ A \in ℝ \to (0 -_{ℝ} A) + A = 0$
11	10	ad2antrr	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to (0 -_{ℝ} A) + A = 0$
12	11	oveq1d	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to (0 -_{ℝ} A) + A + B = 0 + B$
13		simplr	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to 0 -_{ℝ} A \in ℕ$
14	13	nncnd	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to 0 -_{ℝ} A \in ℂ$
15		simpll	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to A \in ℝ$
16	15	recnd	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to A \in ℂ$
17		simprl	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to B \in ℝ$
18	17	recnd	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to B \in ℂ$
19	14 16 18	addassd	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to (0 -_{ℝ} A) + A + B = (0 -_{ℝ} A) + A + B$
20		readdlid	$⊢ B \in ℝ \to 0 + B = B$
21	20	ad2antrl	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to 0 + B = B$
22	12 19 21	3eqtr3d	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to (0 -_{ℝ} A) + A + B = B$
23	22	oveq2d	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to (0 -_{ℝ} B) + (0 -_{ℝ} A) + (A + B) = (0 -_{ℝ} B) + B$
24	9 23 11	3eqtr4d	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to (0 -_{ℝ} B) + (0 -_{ℝ} A) + (A + B) = (0 -_{ℝ} A) + A$
25		simprr	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to 0 -_{ℝ} B \in ℕ$
26	25	nncnd	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to 0 -_{ℝ} B \in ℂ$
27	16 18	addcld	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to A + B \in ℂ$
28	26 14 27	addassd	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to (0 -_{ℝ} B) + (0 -_{ℝ} A) + A + B = (0 -_{ℝ} B) + (0 -_{ℝ} A) + (A + B)$
29	9	oveq1d	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to (0 -_{ℝ} B) + B + A = 0 + A$
30	26 18 16	addassd	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to (0 -_{ℝ} B) + B + A = (0 -_{ℝ} B) + B + A$
31		readdlid	$⊢ A \in ℝ \to 0 + A = A$
32	31	ad2antrr	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to 0 + A = A$
33	29 30 32	3eqtr3d	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to (0 -_{ℝ} B) + B + A = A$
34	33	oveq2d	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to (0 -_{ℝ} A) + (0 -_{ℝ} B) + (B + A) = (0 -_{ℝ} A) + A$
35	24 28 34	3eqtr4d	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to (0 -_{ℝ} B) + (0 -_{ℝ} A) + A + B = (0 -_{ℝ} A) + (0 -_{ℝ} B) + (B + A)$
36		nnaddcom	$⊢ (0 -_{ℝ} A \in ℕ \land 0 -_{ℝ} B \in ℕ) \to (0 -_{ℝ} A) + (0 -_{ℝ} B) = (0 -_{ℝ} B) + (0 -_{ℝ} A)$
37	36	ad2ant2l	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to (0 -_{ℝ} A) + (0 -_{ℝ} B) = (0 -_{ℝ} B) + (0 -_{ℝ} A)$
38	37	oveq1d	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to (0 -_{ℝ} A) + (0 -_{ℝ} B) + A + B = (0 -_{ℝ} B) + (0 -_{ℝ} A) + A + B$
39	18 16	addcld	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to B + A \in ℂ$
40	14 26 39	addassd	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to (0 -_{ℝ} A) + (0 -_{ℝ} B) + B + A = (0 -_{ℝ} A) + (0 -_{ℝ} B) + (B + A)$
41	35 38 40	3eqtr4d	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to (0 -_{ℝ} A) + (0 -_{ℝ} B) + A + B = (0 -_{ℝ} A) + (0 -_{ℝ} B) + B + A$
42	13 25	nnaddcld	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to (0 -_{ℝ} A) + (0 -_{ℝ} B) \in ℕ$
43	42	nncnd	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to (0 -_{ℝ} A) + (0 -_{ℝ} B) \in ℂ$
44	43 27 39	sn-addcand	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to ((0 -_{ℝ} A) + (0 -_{ℝ} B) + A + B = (0 -_{ℝ} A) + (0 -_{ℝ} B) + B + A \leftrightarrow A + B = B + A)$
45	41 44	mpbid	$⊢ ((A \in ℝ \land 0 -_{ℝ} A \in ℕ) \land (B \in ℝ \land 0 -_{ℝ} B \in ℕ)) \to A + B = B + A$
46	3 4 7 45	ccase	$⊢ ((A \in ℕ_{0} \lor (A \in ℝ \land 0 -_{ℝ} A \in ℕ)) \land (B \in ℕ_{0} \lor (B \in ℝ \land 0 -_{ℝ} B \in ℕ))) \to A + B = B + A$
47	1 2 46	syl2anb	$⊢ (A \in ℤ \land B \in ℤ) \to A + B = B + A$

Metamath Proof Explorer

Theorem zaddcom

Proof