Theorem sizeupto ≪ | index | src | ≫

theorem sizeupto (n: nat): $ size (upto n) = n $;


size (upto n) <= n -> n <= size (upto n) -> size (upto n) = n
finite (upto n) -> (upto n C_ upto n <-> size (upto n) <= n)
finite (upto n)
upto n C_ upto n <-> size (upto n) <= n
upto n C_ upto n
size (upto n) <= n
n <= size (upto n) -> size (upto n) = n
upto n C_ upto (size (upto n)) <-> n <= size (upto n)
finite (upto n) <-> upto n C_ upto (size (upto n))
upto n C_ upto (size (upto n))
n <= size (upto n)
size (upto n) = n

Step	Hyp	Ref	Expression
1		leasym	size (upto n) <= n -> n <= size (upto n) -> size (upto n) = n
2		sizess	finite (upto n) -> (upto n C_ upto n <-> size (upto n) <= n)
3		finns	finite (upto n)
4	2, 3	ax_mp	upto n C_ upto n <-> size (upto n) <= n
5		ssid	upto n C_ upto n
6	4, 5	mpbi	size (upto n) <= n
7	1, 6	ax_mp	n <= size (upto n) -> size (upto n) = n
8		uptoss	upto n C_ upto (size (upto n)) <-> n <= size (upto n)
9		sssize	finite (upto n) <-> upto n C_ upto (size (upto n))
10	9, 3	mpbi	upto n C_ upto (size (upto n))
11	8, 10	mpbi	n <= size (upto n)
12	7, 11	ax_mp	size (upto 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)