nn0constr

Description: Nonnegative integers are constructible. (Contributed by Thierry Arnoux, 2-Nov-2025)

		Ref	Expression
	Hypothesis	nn0constr.1	$⊢ φ \to N \in ℕ_{0}$
	Assertion	nn0constr	$⊢ φ \to N \in Constr$

Proof

Step	Hyp	Ref	Expression
1		nn0constr.1	$⊢ φ \to N \in ℕ_{0}$
2		eleq1	$⊢ m = 0 \to (m \in Constr \leftrightarrow 0 \in Constr)$
3		eleq1	$⊢ m = n \to (m \in Constr \leftrightarrow n \in Constr)$
4		eleq1	$⊢ m = n + 1 \to (m \in Constr \leftrightarrow n + 1 \in Constr)$
5		eleq1	$⊢ m = N \to (m \in Constr \leftrightarrow N \in Constr)$
6		peano1	$⊢ \emptyset \in ω$
7	6	a1i	$⊢ φ \to \emptyset \in ω$
8		fveq2	$⊢ u = \emptyset \to rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) (u) = rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) (\emptyset)$
9	8	eleq2d	$⊢ u = \emptyset \to (0 \in rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) (u) \leftrightarrow 0 \in rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) (\emptyset))$
10	9	adantl	$⊢ (φ \land u = \emptyset) \to (0 \in rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) (u) \leftrightarrow 0 \in rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) (\emptyset))$
11		c0ex	$⊢ 0 \in V$
12	11	prid1	$⊢ 0 \in \{0, 1\}$
13	12	a1i	$⊢ φ \to 0 \in \{0, 1\}$
14		constrcbvlem	$⊢ rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) = rec ((s \in V ⟼ \{x \in ℂ \| (\exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists t \in ℝ \exists r \in ℝ (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in s \exists b \in s \exists c \in s \exists e \in s \exists f \in s \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists e \in s \exists f \in s (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\}), \{0, 1\})$
15	14	constr0	$⊢ rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) (\emptyset) = \{0, 1\}$
16	13 15	eleqtrrdi	$⊢ φ \to 0 \in rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) (\emptyset)$
17	7 10 16	rspcedvd	$⊢ φ \to \exists u \in ω 0 \in rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) (u)$
18	14	isconstr	$⊢ 0 \in Constr \leftrightarrow \exists u \in ω 0 \in rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) (u)$
19	17 18	sylibr	$⊢ φ \to 0 \in Constr$
20	19	ad2antrr	$⊢ ((φ \land n \in ℕ_{0}) \land n \in Constr) \to 0 \in Constr$
21	8	eleq2d	$⊢ u = \emptyset \to (1 \in rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) (u) \leftrightarrow 1 \in rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) (\emptyset))$
22	21	adantl	$⊢ (φ \land u = \emptyset) \to (1 \in rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) (u) \leftrightarrow 1 \in rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) (\emptyset))$
23		1ex	$⊢ 1 \in V$
24	23	prid2	$⊢ 1 \in \{0, 1\}$
25	24	a1i	$⊢ φ \to 1 \in \{0, 1\}$
26	25 15	eleqtrrdi	$⊢ φ \to 1 \in rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) (\emptyset)$
27	7 22 26	rspcedvd	$⊢ φ \to \exists u \in ω 1 \in rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) (u)$
28	14	isconstr	$⊢ 1 \in Constr \leftrightarrow \exists u \in ω 1 \in rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) (u)$
29	27 28	sylibr	$⊢ φ \to 1 \in Constr$
30	29	ad2antrr	$⊢ ((φ \land n \in ℕ_{0}) \land n \in Constr) \to 1 \in Constr$
31		simpr	$⊢ ((φ \land n \in ℕ_{0}) \land n \in Constr) \to n \in Constr$
32		peano2nn0	$⊢ n \in ℕ_{0} \to n + 1 \in ℕ_{0}$
33	32	ad2antlr	$⊢ ((φ \land n \in ℕ_{0}) \land n \in Constr) \to n + 1 \in ℕ_{0}$
34	33	nn0red	$⊢ ((φ \land n \in ℕ_{0}) \land n \in Constr) \to n + 1 \in ℝ$
35	34	recnd	$⊢ ((φ \land n \in ℕ_{0}) \land n \in Constr) \to n + 1 \in ℂ$
36		nn0cn	$⊢ n \in ℕ_{0} \to n \in ℂ$
37		1cnd	$⊢ n \in ℕ_{0} \to 1 \in ℂ$
38	36 37	addcld	$⊢ n \in ℕ_{0} \to n + 1 \in ℂ$
39	37	subid1d	$⊢ n \in ℕ_{0} \to 1 - 0 = 1$
40	39 37	eqeltrd	$⊢ n \in ℕ_{0} \to 1 - 0 \in ℂ$
41	38 40	mulcld	$⊢ n \in ℕ_{0} \to (n + 1) (1 - 0) \in ℂ$
42	41	addlidd	$⊢ n \in ℕ_{0} \to 0 + (n + 1) (1 - 0) = (n + 1) (1 - 0)$
43	39	oveq2d	$⊢ n \in ℕ_{0} \to (n + 1) (1 - 0) = (n + 1) \cdot 1$
44	38	mulridd	$⊢ n \in ℕ_{0} \to (n + 1) \cdot 1 = n + 1$
45	42 43 44	3eqtrrd	$⊢ n \in ℕ_{0} \to n + 1 = 0 + (n + 1) (1 - 0)$
46	45	ad2antlr	$⊢ ((φ \land n \in ℕ_{0}) \land n \in Constr) \to n + 1 = 0 + (n + 1) (1 - 0)$
47	36 37	pncan2d	$⊢ n \in ℕ_{0} \to n + 1 - n = 1$
48	47 39	eqtr4d	$⊢ n \in ℕ_{0} \to n + 1 - n = 1 - 0$
49	48	fveq2d	$⊢ n \in ℕ_{0} \to \|n + 1 - n\| = \|1 - 0\|$
50	49	ad2antlr	$⊢ ((φ \land n \in ℕ_{0}) \land n \in Constr) \to \|n + 1 - n\| = \|1 - 0\|$
51	20 30 31 30 20 34 35 46 50	constrlccl	$⊢ ((φ \land n \in ℕ_{0}) \land n \in Constr) \to n + 1 \in Constr$
52	2 3 4 5 19 51	nn0indd	$⊢ (φ \land N \in ℕ_{0}) \to N \in Constr$
53	1 52	mpdan	$⊢ φ \to N \in Constr$

Metamath Proof Explorer

Theorem nn0constr

Proof