Theorem addeq0 ≪ | index | src | ≫

theorem addeq0 (a b: nat): $ a + b = 0 <-> a = 0 /\ b = 0 $;

Step	Hyp	Ref	Expression
1		le02	a <= 0 <-> a = 0
2		leaddid1	a <= a + b
3		leeq2	a + b = 0 -> (a <= a + b <-> a <= 0)
4	2, 3	mpbii	a + b = 0 -> a <= 0
5	1, 4	sylib	a + b = 0 -> a = 0
6		le02	b <= 0 <-> b = 0
7		leaddid2	b <= a + b
8		leeq2	a + b = 0 -> (b <= a + b <-> b <= 0)
9	7, 8	mpbii	a + b = 0 -> b <= 0
10	6, 9	sylib	a + b = 0 -> b = 0
11	5, 10	iand	a + b = 0 -> a = 0 /\ b = 0
12		add0	0 + 0 = 0
13		addeq	a = 0 -> b = 0 -> a + b = 0 + 0
14	13	imp	a = 0 /\ b = 0 -> a + b = 0 + 0
15	12, 14	syl6eq	a = 0 /\ b = 0 -> a + b = 0
16	11, 15	ibii	a + b = 0 <-> a = 0 /\ b = 0

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_peano (peano1, peano2, peano5, addeq, add0, addS)