Theorem leneq0 ≪ | index | src | ≫

theorem leneq0 (n: nat): $ len n = 0 <-> n = 0 $;

Step	Hyp	Ref	Expression
1		ax_3	(~n = 0 -> ~len n = 0) -> len n = 0 -> n = 0
2		sucne0	len n = suc (len (snd (n - 1))) -> len n != 0
3	2	conv ne	len n = suc (len (snd (n - 1))) -> ~len n = 0
4		lenS	len (fst (n - 1) : snd (n - 1)) = suc (len (snd (n - 1)))
5		consfstsnd	n != 0 -> fst (n - 1) : snd (n - 1) = n
6	5	conv ne	~n = 0 -> fst (n - 1) : snd (n - 1) = n
7	6	eqcomd	~n = 0 -> n = fst (n - 1) : snd (n - 1)
8	7	leneqd	~n = 0 -> len n = len (fst (n - 1) : snd (n - 1))
9	4, 8	syl6eq	~n = 0 -> len n = suc (len (snd (n - 1)))
10	3, 9	syl	~n = 0 -> ~len n = 0
11	1, 10	ax_mp	len n = 0 -> n = 0
12		len0	len 0 = 0
13		leneq	n = 0 -> len n = len 0
14	12, 13	syl6eq	n = 0 -> len n = 0
15	11, 14	ibii	len n = 0 <-> n = 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_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)