Theorem eqb0 ≪ | index | src | ≫

theorem eqb0 (n: nat): $ ~odd n <-> n = b0 (n // 2) $;

Step	Hyp	Ref	Expression
1		con1	(~n = b0 (n // 2) -> odd n) -> ~odd n -> n = b0 (n // 2)
2		b0orb1	n = b0 (n // 2) \/ n = b1 (n // 2)
3	2	conv or	~n = b0 (n // 2) -> n = b1 (n // 2)
4		b1odd	odd (b1 (n // 2))
5		oddeq	n = b1 (n // 2) -> (odd n <-> odd (b1 (n // 2)))
6	4, 5	mpbiri	n = b1 (n // 2) -> odd n
7	3, 6	rsyl	~n = b0 (n // 2) -> odd n
8	1, 7	ax_mp	~odd n -> n = b0 (n // 2)
9		b0odd	~odd (b0 (n // 2))
10		oddeq	n = b0 (n // 2) -> (odd n <-> odd (b0 (n // 2)))
11	10	noteqd	n = b0 (n // 2) -> (~odd n <-> ~odd (b0 (n // 2)))
12	9, 11	mpbiri	n = b0 (n // 2) -> ~odd n
13	8, 12	ibii	~odd n <-> n = b0 (n // 2)

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)