lzenom

Description: Lower integers are countably infinite. (Contributed by Stefan O'Rear, 10-Oct-2014)

		Ref	Expression
	Assertion	lzenom	$⊢ N \in ℤ \to (ℤ ∖ ℤ_{\geq (N + 1)}) \approx ω$

Proof

Step	Hyp	Ref	Expression
1		zex	$⊢ ℤ \in V$
2		difexg	$⊢ ℤ \in V \to ℤ ∖ ℤ_{\geq (N + 1)} \in V$
3	1 2	mp1i	$⊢ N \in ℤ \to ℤ ∖ ℤ_{\geq (N + 1)} \in V$
4		nnex	$⊢ ℕ \in V$
5	4	a1i	$⊢ N \in ℤ \to ℕ \in V$
6		ovex	$⊢ N + 1 - a \in V$
7	6	2a1i	$⊢ N \in ℤ \to (a \in (ℤ ∖ ℤ_{\geq (N + 1)}) \to N + 1 - a \in V)$
8		ovex	$⊢ N + 1 - b \in V$
9	8	2a1i	$⊢ N \in ℤ \to (b \in ℕ \to N + 1 - b \in V)$
10		simpl	$⊢ (N \in ℤ \land (a \in ℤ \land a \leq N)) \to N \in ℤ$
11	10	peano2zd	$⊢ (N \in ℤ \land (a \in ℤ \land a \leq N)) \to N + 1 \in ℤ$
12		simprl	$⊢ (N \in ℤ \land (a \in ℤ \land a \leq N)) \to a \in ℤ$
13	11 12	zsubcld	$⊢ (N \in ℤ \land (a \in ℤ \land a \leq N)) \to N + 1 - a \in ℤ$
14		zre	$⊢ a \in ℤ \to a \in ℝ$
15	14	ad2antrl	$⊢ (N \in ℤ \land (a \in ℤ \land a \leq N)) \to a \in ℝ$
16	11	zred	$⊢ (N \in ℤ \land (a \in ℤ \land a \leq N)) \to N + 1 \in ℝ$
17		1red	$⊢ (N \in ℤ \land (a \in ℤ \land a \leq N)) \to 1 \in ℝ$
18		simprr	$⊢ (N \in ℤ \land (a \in ℤ \land a \leq N)) \to a \leq N$
19		zcn	$⊢ N \in ℤ \to N \in ℂ$
20	19	adantr	$⊢ (N \in ℤ \land (a \in ℤ \land a \leq N)) \to N \in ℂ$
21		ax-1cn	$⊢ 1 \in ℂ$
22		pncan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N + 1 - 1 = N$
23	20 21 22	sylancl	$⊢ (N \in ℤ \land (a \in ℤ \land a \leq N)) \to N + 1 - 1 = N$
24	18 23	breqtrrd	$⊢ (N \in ℤ \land (a \in ℤ \land a \leq N)) \to a \leq N + 1 - 1$
25	15 16 17 24	lesubd	$⊢ (N \in ℤ \land (a \in ℤ \land a \leq N)) \to 1 \leq N + 1 - a$
26	11	zcnd	$⊢ (N \in ℤ \land (a \in ℤ \land a \leq N)) \to N + 1 \in ℂ$
27		zcn	$⊢ a \in ℤ \to a \in ℂ$
28	27	ad2antrl	$⊢ (N \in ℤ \land (a \in ℤ \land a \leq N)) \to a \in ℂ$
29	26 28	nncand	$⊢ (N \in ℤ \land (a \in ℤ \land a \leq N)) \to N + 1 - (N + 1 - a) = a$
30	29	eqcomd	$⊢ (N \in ℤ \land (a \in ℤ \land a \leq N)) \to a = N + 1 - (N + 1 - a)$
31	13 25 30	jca31	$⊢ (N \in ℤ \land (a \in ℤ \land a \leq N)) \to ((N + 1 - a \in ℤ \land 1 \leq N + 1 - a) \land a = N + 1 - (N + 1 - a))$
32	31	adantrr	$⊢ (N \in ℤ \land ((a \in ℤ \land a \leq N) \land b = N + 1 - a)) \to ((N + 1 - a \in ℤ \land 1 \leq N + 1 - a) \land a = N + 1 - (N + 1 - a))$
33		eleq1	$⊢ b = N + 1 - a \to (b \in ℤ \leftrightarrow N + 1 - a \in ℤ)$
34		breq2	$⊢ b = N + 1 - a \to (1 \leq b \leftrightarrow 1 \leq N + 1 - a)$
35	33 34	anbi12d	$⊢ b = N + 1 - a \to ((b \in ℤ \land 1 \leq b) \leftrightarrow (N + 1 - a \in ℤ \land 1 \leq N + 1 - a))$
36		oveq2	$⊢ b = N + 1 - a \to N + 1 - b = N + 1 - (N + 1 - a)$
37	36	eqeq2d	$⊢ b = N + 1 - a \to (a = N + 1 - b \leftrightarrow a = N + 1 - (N + 1 - a))$
38	35 37	anbi12d	$⊢ b = N + 1 - a \to (((b \in ℤ \land 1 \leq b) \land a = N + 1 - b) \leftrightarrow ((N + 1 - a \in ℤ \land 1 \leq N + 1 - a) \land a = N + 1 - (N + 1 - a)))$
39	38	ad2antll	$⊢ (N \in ℤ \land ((a \in ℤ \land a \leq N) \land b = N + 1 - a)) \to (((b \in ℤ \land 1 \leq b) \land a = N + 1 - b) \leftrightarrow ((N + 1 - a \in ℤ \land 1 \leq N + 1 - a) \land a = N + 1 - (N + 1 - a)))$
40	32 39	mpbird	$⊢ (N \in ℤ \land ((a \in ℤ \land a \leq N) \land b = N + 1 - a)) \to ((b \in ℤ \land 1 \leq b) \land a = N + 1 - b)$
41		simpl	$⊢ (N \in ℤ \land (b \in ℤ \land 1 \leq b)) \to N \in ℤ$
42	41	peano2zd	$⊢ (N \in ℤ \land (b \in ℤ \land 1 \leq b)) \to N + 1 \in ℤ$
43		simprl	$⊢ (N \in ℤ \land (b \in ℤ \land 1 \leq b)) \to b \in ℤ$
44	42 43	zsubcld	$⊢ (N \in ℤ \land (b \in ℤ \land 1 \leq b)) \to N + 1 - b \in ℤ$
45	42	zred	$⊢ (N \in ℤ \land (b \in ℤ \land 1 \leq b)) \to N + 1 \in ℝ$
46		zre	$⊢ N \in ℤ \to N \in ℝ$
47	46	adantr	$⊢ (N \in ℤ \land (b \in ℤ \land 1 \leq b)) \to N \in ℝ$
48		zre	$⊢ b \in ℤ \to b \in ℝ$
49	48	ad2antrl	$⊢ (N \in ℤ \land (b \in ℤ \land 1 \leq b)) \to b \in ℝ$
50	47	recnd	$⊢ (N \in ℤ \land (b \in ℤ \land 1 \leq b)) \to N \in ℂ$
51		pncan2	$⊢ (N \in ℂ \land 1 \in ℂ) \to N + 1 - N = 1$
52	50 21 51	sylancl	$⊢ (N \in ℤ \land (b \in ℤ \land 1 \leq b)) \to N + 1 - N = 1$
53		simprr	$⊢ (N \in ℤ \land (b \in ℤ \land 1 \leq b)) \to 1 \leq b$
54	52 53	eqbrtrd	$⊢ (N \in ℤ \land (b \in ℤ \land 1 \leq b)) \to N + 1 - N \leq b$
55	45 47 49 54	subled	$⊢ (N \in ℤ \land (b \in ℤ \land 1 \leq b)) \to N + 1 - b \leq N$
56	42	zcnd	$⊢ (N \in ℤ \land (b \in ℤ \land 1 \leq b)) \to N + 1 \in ℂ$
57		zcn	$⊢ b \in ℤ \to b \in ℂ$
58	57	ad2antrl	$⊢ (N \in ℤ \land (b \in ℤ \land 1 \leq b)) \to b \in ℂ$
59	56 58	nncand	$⊢ (N \in ℤ \land (b \in ℤ \land 1 \leq b)) \to N + 1 - (N + 1 - b) = b$
60	59	eqcomd	$⊢ (N \in ℤ \land (b \in ℤ \land 1 \leq b)) \to b = N + 1 - (N + 1 - b)$
61	44 55 60	jca31	$⊢ (N \in ℤ \land (b \in ℤ \land 1 \leq b)) \to ((N + 1 - b \in ℤ \land N + 1 - b \leq N) \land b = N + 1 - (N + 1 - b))$
62	61	adantrr	$⊢ (N \in ℤ \land ((b \in ℤ \land 1 \leq b) \land a = N + 1 - b)) \to ((N + 1 - b \in ℤ \land N + 1 - b \leq N) \land b = N + 1 - (N + 1 - b))$
63		eleq1	$⊢ a = N + 1 - b \to (a \in ℤ \leftrightarrow N + 1 - b \in ℤ)$
64		breq1	$⊢ a = N + 1 - b \to (a \leq N \leftrightarrow N + 1 - b \leq N)$
65	63 64	anbi12d	$⊢ a = N + 1 - b \to ((a \in ℤ \land a \leq N) \leftrightarrow (N + 1 - b \in ℤ \land N + 1 - b \leq N))$
66		oveq2	$⊢ a = N + 1 - b \to N + 1 - a = N + 1 - (N + 1 - b)$
67	66	eqeq2d	$⊢ a = N + 1 - b \to (b = N + 1 - a \leftrightarrow b = N + 1 - (N + 1 - b))$
68	65 67	anbi12d	$⊢ a = N + 1 - b \to (((a \in ℤ \land a \leq N) \land b = N + 1 - a) \leftrightarrow ((N + 1 - b \in ℤ \land N + 1 - b \leq N) \land b = N + 1 - (N + 1 - b)))$
69	68	ad2antll	$⊢ (N \in ℤ \land ((b \in ℤ \land 1 \leq b) \land a = N + 1 - b)) \to (((a \in ℤ \land a \leq N) \land b = N + 1 - a) \leftrightarrow ((N + 1 - b \in ℤ \land N + 1 - b \leq N) \land b = N + 1 - (N + 1 - b)))$
70	62 69	mpbird	$⊢ (N \in ℤ \land ((b \in ℤ \land 1 \leq b) \land a = N + 1 - b)) \to ((a \in ℤ \land a \leq N) \land b = N + 1 - a)$
71	40 70	impbida	$⊢ N \in ℤ \to (((a \in ℤ \land a \leq N) \land b = N + 1 - a) \leftrightarrow ((b \in ℤ \land 1 \leq b) \land a = N + 1 - b))$
72		ellz1	$⊢ N \in ℤ \to (a \in (ℤ ∖ ℤ_{\geq (N + 1)}) \leftrightarrow (a \in ℤ \land a \leq N))$
73	72	anbi1d	$⊢ N \in ℤ \to ((a \in (ℤ ∖ ℤ_{\geq (N + 1)}) \land b = N + 1 - a) \leftrightarrow ((a \in ℤ \land a \leq N) \land b = N + 1 - a))$
74		elnnz1	$⊢ b \in ℕ \leftrightarrow (b \in ℤ \land 1 \leq b)$
75	74	a1i	$⊢ N \in ℤ \to (b \in ℕ \leftrightarrow (b \in ℤ \land 1 \leq b))$
76	75	anbi1d	$⊢ N \in ℤ \to ((b \in ℕ \land a = N + 1 - b) \leftrightarrow ((b \in ℤ \land 1 \leq b) \land a = N + 1 - b))$
77	71 73 76	3bitr4d	$⊢ N \in ℤ \to ((a \in (ℤ ∖ ℤ_{\geq (N + 1)}) \land b = N + 1 - a) \leftrightarrow (b \in ℕ \land a = N + 1 - b))$
78	3 5 7 9 77	en2d	$⊢ N \in ℤ \to (ℤ ∖ ℤ_{\geq (N + 1)}) \approx ℕ$
79		nnenom	$⊢ ℕ \approx ω$
80		entr	$⊢ ((ℤ ∖ ℤ_{\geq (N + 1)}) \approx ℕ \land ℕ \approx ω) \to (ℤ ∖ ℤ_{\geq (N + 1)}) \approx ω$
81	78 79 80	sylancl	$⊢ N \in ℤ \to (ℤ ∖ ℤ_{\geq (N + 1)}) \approx ω$

Metamath Proof Explorer

Theorem lzenom

Proof