Theorem ltwenn0

Description: "Less than" is a well-order on the nonnegative integers. (Contributed by Thierry Arnoux, 29-Oct-2026)

	Ref	Expression
Assertion	ltwenn0	$$⊢<\mathrm{We}{\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		ltweuz	$$⊢<\mathrm{We}{\mathbb{Z}}_{\ge 0}$$
2		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
3		weeq2	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}\to \left(<\mathrm{We}{\mathbb{N}}_0\leftrightarrow <\mathrm{We}{\mathbb{Z}}_{\ge 0}\right)$$
4	2 3	ax-mp	$$⊢<\mathrm{We}{\mathbb{N}}_0\leftrightarrow <\mathrm{We}{\mathbb{Z}}_{\ge 0}$$
5	1 4	mpbir	$$⊢<\mathrm{We}{\mathbb{N}}_0$$