Theorem nattruele ≪ | index | src | ≫

theorem nattruele (n: nat): $ nat (true n) <= n $;


(nat (true n) <= n -> nat (true n) <= n) -> (n <= nat (true n) -> nat (true n) <= n) -> nat (true n) <= n \/ n <= nat (true n) -> nat (true n) <= n
nat (true n) <= n -> nat (true n) <= n
(n <= nat (true n) -> nat (true n) <= n) -> nat (true n) <= n \/ n <= nat (true n) -> nat (true n) <= n
nat (true n) = n -> nat (true n) <= n
bool n -> nat (true n) = n
bool (nat (true n))
n <= nat (true n) -> bool (nat (true n)) -> bool n
n <= nat (true n) -> bool n
n <= nat (true n) -> nat (true n) = n
n <= nat (true n) -> nat (true n) <= n
nat (true n) <= n \/ n <= nat (true n) -> nat (true n) <= n
nat (true n) <= n \/ n <= nat (true n)
nat (true n) <= n

Step	Hyp	Ref	Expression
1		eor	(nat (true n) <= n -> nat (true n) <= n) -> (n <= nat (true n) -> nat (true n) <= n) -> nat (true n) <= n \/ n <= nat (true n) -> nat (true n) <= n
2		id	nat (true n) <= n -> nat (true n) <= n
3	1, 2	ax_mp	(n <= nat (true n) -> nat (true n) <= n) -> nat (true n) <= n \/ n <= nat (true n) -> nat (true n) <= n
4		eqle	nat (true n) = n -> nat (true n) <= n
5		nattrue	bool n -> nat (true n) = n
6		boolnat	bool (nat (true n))
7		lebool	n <= nat (true n) -> bool (nat (true n)) -> bool n
8	6, 7	mpi	n <= nat (true n) -> bool n
9	5, 8	syl	n <= nat (true n) -> nat (true n) = n
10	4, 9	syl	n <= nat (true n) -> nat (true n) <= n
11	3, 10	ax_mp	nat (true n) <= n \/ n <= nat (true n) -> nat (true n) <= n
12		leorle	nat (true n) <= n \/ n <= nat (true n)
13	11, 12	ax_mp	nat (true 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, add0, addS)