Theorem ntheq0 ≪ | index | src | ≫

theorem ntheq0 (l n: nat): $ nth n l = 0 <-> len l <= n $;

Step	Hyp	Ref	Expression
1		bicom	(len l <= n <-> nth n l = 0) -> (nth n l = 0 <-> len l <= n)
2		bitr	(len l <= n <-> ~n < len l) -> (~n < len l <-> nth n l = 0) -> (len l <= n <-> nth n l = 0)
3		lenlt	len l <= n <-> ~n < len l
4	3	bitr*	(~n < len l <-> nth n l = 0) -> (len l <= n <-> nth n l = 0)
5		con1b	(~nth n l = 0 <-> n < len l) -> (~n < len l <-> nth n l = 0)
6		nthne0	nth n l != 0 <-> n < len l
7	6	conv ne	~nth n l = 0 <-> n < len l
8	7	con1b*	~n < len l <-> nth n l = 0
9	3, 8	bitr*	len l <= n <-> nth n l = 0
10	9	bicom*	nth n l = 0 <-> len l <= n

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), axs_peano (peano1, peano2, peano5, addeq, add0, addS)