Theorem ntheqd ≪ | index | src | ≫

theorem ntheqd (_G: wff) (_n1 _n2 _l1 _l2: nat):
  $ _G -> _n1 = _n2 $ >
  $ _G -> _l1 = _l2 $ >
  $ _G -> nth _n1 _l1 = nth _n2 _l2 $;


_G -> _n1 = _n2
_G -> _l1 = _l2
_G -> len _l1 = len _l2
_G -> (_n1 < len _l1 <-> _n2 < len _l2)
_G -> listfn _l1 = listfn _l2
_G -> listfn _l1 == listfn _l2
_G -> listfn _l1 @ _n1 = listfn _l2 @ _n2
_G -> suc (listfn _l1 @ _n1) = suc (listfn _l2 @ _n2)
_G -> 0 = 0
_G -> if (_n1 < len _l1) (suc (listfn _l1 @ _n1)) 0 = if (_n2 < len _l2) (suc (listfn _l2 @ _n2)) 0
_G -> nth _n1 _l1 = nth _n2 _l2

Step	Hyp	Ref	Expression
1		hyp _nh	_G -> _n1 = _n2
2		hyp _lh	_G -> _l1 = _l2
3	2	leneqd	_G -> len _l1 = len _l2
4	1, 3	lteqd	_G -> (_n1 < len _l1 <-> _n2 < len _l2)
5	2	listfneqd	_G -> listfn _l1 = listfn _l2
6	5	nseqd	_G -> listfn _l1 == listfn _l2
7	6, 1	appeqd	_G -> listfn _l1 @ _n1 = listfn _l2 @ _n2
8	7	suceqd	_G -> suc (listfn _l1 @ _n1) = suc (listfn _l2 @ _n2)
9		eqidd	_G -> 0 = 0
10	4, 8, 9	ifeqd	_G -> if (_n1 < len _l1) (suc (listfn _l1 @ _n1)) 0 = if (_n2 < len _l2) (suc (listfn _l2 @ _n2)) 0
11	10	conv nth	_G -> nth _n1 _l1 = nth _n2 _l2

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 (peano2, addeq, muleq)