Theorem recnauxfst ≪ | index | src | ≫

theorem recnauxfst (S: set) (n z: nat): $ fst (recnaux z S n) = n $;


_1 = n -> _1 = n
_1 = n -> recnaux z S _1 = recnaux z S n
_1 = n -> fst (recnaux z S _1) = fst (recnaux z S n)
_1 = n -> (fst (recnaux z S _1) = _1 <-> fst (recnaux z S n) = n)
_1 = 0 -> _1 = 0
_1 = 0 -> recnaux z S _1 = recnaux z S 0
_1 = 0 -> fst (recnaux z S _1) = fst (recnaux z S 0)
_1 = 0 -> (fst (recnaux z S _1) = _1 <-> fst (recnaux z S 0) = 0)
_1 = a1 -> _1 = a1
_1 = a1 -> recnaux z S _1 = recnaux z S a1
_1 = a1 -> fst (recnaux z S _1) = fst (recnaux z S a1)
_1 = a1 -> (fst (recnaux z S _1) = _1 <-> fst (recnaux z S a1) = a1)
_1 = suc a1 -> _1 = suc a1
_1 = suc a1 -> recnaux z S _1 = recnaux z S (suc a1)
_1 = suc a1 -> fst (recnaux z S _1) = fst (recnaux z S (suc a1))
_1 = suc a1 -> (fst (recnaux z S _1) = _1 <-> fst (recnaux z S (suc a1)) = suc a1)
fst (recnaux z S 0) = fst (0, z) -> fst (0, z) = 0 -> fst (recnaux z S 0) = 0
recnaux z S 0 = 0, z -> fst (recnaux z S 0) = fst (0, z)
recnaux z S 0 = 0, z
fst (recnaux z S 0) = fst (0, z)
fst (0, z) = 0 -> fst (recnaux z S 0) = 0
fst (0, z) = 0
fst (recnaux z S 0) = 0
fst (recnaux z S (suc a1)) = fst (suc (fst (recnaux z S a1)), S @ recnaux z S a1) ->
  fst (suc (fst (recnaux z S a1)), S @ recnaux z S a1) = suc (fst (recnaux z S a1)) ->
  fst (recnaux z S (suc a1)) = suc (fst (recnaux z S a1))
recnaux z S (suc a1) = suc (fst (recnaux z S a1)), S @ recnaux z S a1 -> fst (recnaux z S (suc a1)) = fst (suc (fst (recnaux z S a1)), S @ recnaux z S a1)
recnaux z S (suc a1) = suc (fst (recnaux z S a1)), S @ recnaux z S a1
fst (recnaux z S (suc a1)) = fst (suc (fst (recnaux z S a1)), S @ recnaux z S a1)
fst (suc (fst (recnaux z S a1)), S @ recnaux z S a1) = suc (fst (recnaux z S a1)) -> fst (recnaux z S (suc a1)) = suc (fst (recnaux z S a1))
fst (suc (fst (recnaux z S a1)), S @ recnaux z S a1) = suc (fst (recnaux z S a1))
fst (recnaux z S (suc a1)) = suc (fst (recnaux z S a1))
fst (recnaux z S a1) = a1 -> suc (fst (recnaux z S a1)) = suc a1
fst (recnaux z S a1) = a1 -> fst (recnaux z S (suc a1)) = suc a1
fst (recnaux z S n) = n

Step	Hyp	Ref	Expression
1		id	_1 = n -> _1 = n
2	1	recnauxeq3d	_1 = n -> recnaux z S _1 = recnaux z S n
3	2	fsteqd	_1 = n -> fst (recnaux z S _1) = fst (recnaux z S n)
4	3, 1	eqeqd	_1 = n -> (fst (recnaux z S _1) = _1 <-> fst (recnaux z S n) = n)
5		id	_1 = 0 -> _1 = 0
6	5	recnauxeq3d	_1 = 0 -> recnaux z S _1 = recnaux z S 0
7	6	fsteqd	_1 = 0 -> fst (recnaux z S _1) = fst (recnaux z S 0)
8	7, 5	eqeqd	_1 = 0 -> (fst (recnaux z S _1) = _1 <-> fst (recnaux z S 0) = 0)
9		id	_1 = a1 -> _1 = a1
10	9	recnauxeq3d	_1 = a1 -> recnaux z S _1 = recnaux z S a1
11	10	fsteqd	_1 = a1 -> fst (recnaux z S _1) = fst (recnaux z S a1)
12	11, 9	eqeqd	_1 = a1 -> (fst (recnaux z S _1) = _1 <-> fst (recnaux z S a1) = a1)
13		id	_1 = suc a1 -> _1 = suc a1
14	13	recnauxeq3d	_1 = suc a1 -> recnaux z S _1 = recnaux z S (suc a1)
15	14	fsteqd	_1 = suc a1 -> fst (recnaux z S _1) = fst (recnaux z S (suc a1))
16	15, 13	eqeqd	_1 = suc a1 -> (fst (recnaux z S _1) = _1 <-> fst (recnaux z S (suc a1)) = suc a1)
17		eqtr	fst (recnaux z S 0) = fst (0, z) -> fst (0, z) = 0 -> fst (recnaux z S 0) = 0
18		fsteq	recnaux z S 0 = 0, z -> fst (recnaux z S 0) = fst (0, z)
19		recnaux0	recnaux z S 0 = 0, z
20	18, 19	ax_mp	fst (recnaux z S 0) = fst (0, z)
21	17, 20	ax_mp	fst (0, z) = 0 -> fst (recnaux z S 0) = 0
22		fstpr	fst (0, z) = 0
23	21, 22	ax_mp	fst (recnaux z S 0) = 0
24		eqtr	fst (recnaux z S (suc a1)) = fst (suc (fst (recnaux z S a1)), S @ recnaux z S a1) -> fst (suc (fst (recnaux z S a1)), S @ recnaux z S a1) = suc (fst (recnaux z S a1)) -> fst (recnaux z S (suc a1)) = suc (fst (recnaux z S a1))
25		fsteq	recnaux z S (suc a1) = suc (fst (recnaux z S a1)), S @ recnaux z S a1 -> fst (recnaux z S (suc a1)) = fst (suc (fst (recnaux z S a1)), S @ recnaux z S a1)
26		recnauxS2	recnaux z S (suc a1) = suc (fst (recnaux z S a1)), S @ recnaux z S a1
27	25, 26	ax_mp	fst (recnaux z S (suc a1)) = fst (suc (fst (recnaux z S a1)), S @ recnaux z S a1)
28	24, 27	ax_mp	fst (suc (fst (recnaux z S a1)), S @ recnaux z S a1) = suc (fst (recnaux z S a1)) -> fst (recnaux z S (suc a1)) = suc (fst (recnaux z S a1))
29		fstpr	fst (suc (fst (recnaux z S a1)), S @ recnaux z S a1) = suc (fst (recnaux z S a1))
30	28, 29	ax_mp	fst (recnaux z S (suc a1)) = suc (fst (recnaux z S a1))
31		suceq	fst (recnaux z S a1) = a1 -> suc (fst (recnaux z S a1)) = suc a1
32	30, 31	syl5eq	fst (recnaux z S a1) = a1 -> fst (recnaux z S (suc a1)) = suc a1
33	4, 8, 12, 16, 23, 32	ind	fst (recnaux z S n) = 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, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)