nndiffz1

Description: Upper set of the positive integers. (Contributed by Thierry Arnoux, 22-Aug-2017)

		Ref	Expression
	Assertion	nndiffz1	$⊢ N \in ℕ_{0} \to ℕ ∖ (1 \dots N) = ℤ_{\geq (N + 1)}$

Proof

Step	Hyp	Ref	Expression
1		1z	$⊢ 1 \in ℤ$
2		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
3		elfz1	$⊢ (1 \in ℤ \land N \in ℤ) \to (j \in (1 \dots N) \leftrightarrow (j \in ℤ \land 1 \leq j \land j \leq N))$
4	1 2 3	sylancr	$⊢ N \in ℕ_{0} \to (j \in (1 \dots N) \leftrightarrow (j \in ℤ \land 1 \leq j \land j \leq N))$
5		3anass	$⊢ (j \in ℤ \land 1 \leq j \land j \leq N) \leftrightarrow (j \in ℤ \land (1 \leq j \land j \leq N))$
6	4 5	bitrdi	$⊢ N \in ℕ_{0} \to (j \in (1 \dots N) \leftrightarrow (j \in ℤ \land (1 \leq j \land j \leq N)))$
7	6	baibd	$⊢ (N \in ℕ_{0} \land j \in ℤ) \to (j \in (1 \dots N) \leftrightarrow (1 \leq j \land j \leq N))$
8	7	baibd	$⊢ ((N \in ℕ_{0} \land j \in ℤ) \land 1 \leq j) \to (j \in (1 \dots N) \leftrightarrow j \leq N)$
9	8	notbid	$⊢ ((N \in ℕ_{0} \land j \in ℤ) \land 1 \leq j) \to (\neg j \in (1 \dots N) \leftrightarrow \neg j \leq N)$
10		simpl	$⊢ (N \in ℤ \land j \in ℤ) \to N \in ℤ$
11	10	zred	$⊢ (N \in ℤ \land j \in ℤ) \to N \in ℝ$
12		simpr	$⊢ (N \in ℤ \land j \in ℤ) \to j \in ℤ$
13	12	zred	$⊢ (N \in ℤ \land j \in ℤ) \to j \in ℝ$
14	11 13	ltnled	$⊢ (N \in ℤ \land j \in ℤ) \to (N < j \leftrightarrow \neg j \leq N)$
15		zltp1le	$⊢ (N \in ℤ \land j \in ℤ) \to (N < j \leftrightarrow N + 1 \leq j)$
16	14 15	bitr3d	$⊢ (N \in ℤ \land j \in ℤ) \to (\neg j \leq N \leftrightarrow N + 1 \leq j)$
17	2 16	sylan	$⊢ (N \in ℕ_{0} \land j \in ℤ) \to (\neg j \leq N \leftrightarrow N + 1 \leq j)$
18	17	adantr	$⊢ ((N \in ℕ_{0} \land j \in ℤ) \land 1 \leq j) \to (\neg j \leq N \leftrightarrow N + 1 \leq j)$
19	9 18	bitrd	$⊢ ((N \in ℕ_{0} \land j \in ℤ) \land 1 \leq j) \to (\neg j \in (1 \dots N) \leftrightarrow N + 1 \leq j)$
20	19	pm5.32da	$⊢ (N \in ℕ_{0} \land j \in ℤ) \to ((1 \leq j \land \neg j \in (1 \dots N)) \leftrightarrow (1 \leq j \land N + 1 \leq j))$
21		1red	$⊢ ((N \in ℕ_{0} \land j \in ℤ) \land N + 1 \leq j) \to 1 \in ℝ$
22		simpll	$⊢ ((N \in ℕ_{0} \land j \in ℤ) \land N + 1 \leq j) \to N \in ℕ_{0}$
23	22	nn0red	$⊢ ((N \in ℕ_{0} \land j \in ℤ) \land N + 1 \leq j) \to N \in ℝ$
24	23 21	readdcld	$⊢ ((N \in ℕ_{0} \land j \in ℤ) \land N + 1 \leq j) \to N + 1 \in ℝ$
25		simplr	$⊢ ((N \in ℕ_{0} \land j \in ℤ) \land N + 1 \leq j) \to j \in ℤ$
26	25	zred	$⊢ ((N \in ℕ_{0} \land j \in ℤ) \land N + 1 \leq j) \to j \in ℝ$
27		0p1e1	$⊢ 0 + 1 = 1$
28		0red	$⊢ ((N \in ℕ_{0} \land j \in ℤ) \land N + 1 \leq j) \to 0 \in ℝ$
29	22	nn0ge0d	$⊢ ((N \in ℕ_{0} \land j \in ℤ) \land N + 1 \leq j) \to 0 \leq N$
30	28 23 21 29	leadd1dd	$⊢ ((N \in ℕ_{0} \land j \in ℤ) \land N + 1 \leq j) \to 0 + 1 \leq N + 1$
31	27 30	eqbrtrrid	$⊢ ((N \in ℕ_{0} \land j \in ℤ) \land N + 1 \leq j) \to 1 \leq N + 1$
32		simpr	$⊢ ((N \in ℕ_{0} \land j \in ℤ) \land N + 1 \leq j) \to N + 1 \leq j$
33	21 24 26 31 32	letrd	$⊢ ((N \in ℕ_{0} \land j \in ℤ) \land N + 1 \leq j) \to 1 \leq j$
34	33	ex	$⊢ (N \in ℕ_{0} \land j \in ℤ) \to (N + 1 \leq j \to 1 \leq j)$
35	34	pm4.71rd	$⊢ (N \in ℕ_{0} \land j \in ℤ) \to (N + 1 \leq j \leftrightarrow (1 \leq j \land N + 1 \leq j))$
36	20 35	bitr4d	$⊢ (N \in ℕ_{0} \land j \in ℤ) \to ((1 \leq j \land \neg j \in (1 \dots N)) \leftrightarrow N + 1 \leq j)$
37	36	pm5.32da	$⊢ N \in ℕ_{0} \to ((j \in ℤ \land (1 \leq j \land \neg j \in (1 \dots N))) \leftrightarrow (j \in ℤ \land N + 1 \leq j))$
38		eldif	$⊢ j \in (ℕ ∖ (1 \dots N)) \leftrightarrow (j \in ℕ \land \neg j \in (1 \dots N))$
39		elnnz1	$⊢ j \in ℕ \leftrightarrow (j \in ℤ \land 1 \leq j)$
40	39	anbi1i	$⊢ (j \in ℕ \land \neg j \in (1 \dots N)) \leftrightarrow ((j \in ℤ \land 1 \leq j) \land \neg j \in (1 \dots N))$
41		anass	$⊢ ((j \in ℤ \land 1 \leq j) \land \neg j \in (1 \dots N)) \leftrightarrow (j \in ℤ \land (1 \leq j \land \neg j \in (1 \dots N)))$
42	38 40 41	3bitri	$⊢ j \in (ℕ ∖ (1 \dots N)) \leftrightarrow (j \in ℤ \land (1 \leq j \land \neg j \in (1 \dots N)))$
43	42	a1i	$⊢ N \in ℕ_{0} \to (j \in (ℕ ∖ (1 \dots N)) \leftrightarrow (j \in ℤ \land (1 \leq j \land \neg j \in (1 \dots N))))$
44		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
45	44	nn0zd	$⊢ N \in ℕ_{0} \to N + 1 \in ℤ$
46		eluz1	$⊢ N + 1 \in ℤ \to (j \in ℤ_{\geq (N + 1)} \leftrightarrow (j \in ℤ \land N + 1 \leq j))$
47	45 46	syl	$⊢ N \in ℕ_{0} \to (j \in ℤ_{\geq (N + 1)} \leftrightarrow (j \in ℤ \land N + 1 \leq j))$
48	37 43 47	3bitr4d	$⊢ N \in ℕ_{0} \to (j \in (ℕ ∖ (1 \dots N)) \leftrightarrow j \in ℤ_{\geq (N + 1)})$
49	48	eqrdv	$⊢ N \in ℕ_{0} \to ℕ ∖ (1 \dots N) = ℤ_{\geq (N + 1)}$

Metamath Proof Explorer

Theorem nndiffz1

Proof