Step | Hyp | Ref
| Expression |
1 | | unrab 3398 |
. . 3
⊢ ({𝑧 ∈ ℤ ∣ 𝑧 ∈ ℕ} ∪ {𝑧 ∈ ℤ ∣ -𝑧 ∈ ℕ0}) =
{𝑧 ∈ ℤ ∣
(𝑧 ∈ ℕ ∨
-𝑧 ∈
ℕ0)} |
2 | | nnssz 9216 |
. . . . . 6
⊢ ℕ
⊆ ℤ |
3 | | dfss1 3331 |
. . . . . 6
⊢ (ℕ
⊆ ℤ ↔ (ℤ ∩ ℕ) = ℕ) |
4 | 2, 3 | mpbi 144 |
. . . . 5
⊢ (ℤ
∩ ℕ) = ℕ |
5 | | dfin5 3128 |
. . . . 5
⊢ (ℤ
∩ ℕ) = {𝑧 ∈
ℤ ∣ 𝑧 ∈
ℕ} |
6 | 4, 5 | eqtr3i 2193 |
. . . 4
⊢ ℕ =
{𝑧 ∈ ℤ ∣
𝑧 ∈
ℕ} |
7 | 6 | uneq1i 3277 |
. . 3
⊢ (ℕ
∪ {𝑧 ∈ ℤ
∣ -𝑧 ∈
ℕ0}) = ({𝑧
∈ ℤ ∣ 𝑧
∈ ℕ} ∪ {𝑧
∈ ℤ ∣ -𝑧
∈ ℕ0}) |
8 | | rabid2 2646 |
. . . 4
⊢ (ℤ
= {𝑧 ∈ ℤ ∣
(𝑧 ∈ ℕ ∨
-𝑧 ∈
ℕ0)} ↔ ∀𝑧 ∈ ℤ (𝑧 ∈ ℕ ∨ -𝑧 ∈
ℕ0)) |
9 | | elznn 9215 |
. . . . 5
⊢ (𝑧 ∈ ℤ ↔ (𝑧 ∈ ℝ ∧ (𝑧 ∈ ℕ ∨ -𝑧 ∈
ℕ0))) |
10 | 9 | simprbi 273 |
. . . 4
⊢ (𝑧 ∈ ℤ → (𝑧 ∈ ℕ ∨ -𝑧 ∈
ℕ0)) |
11 | 8, 10 | mprgbir 2528 |
. . 3
⊢ ℤ =
{𝑧 ∈ ℤ ∣
(𝑧 ∈ ℕ ∨
-𝑧 ∈
ℕ0)} |
12 | 1, 7, 11 | 3eqtr4ri 2202 |
. 2
⊢ ℤ =
(ℕ ∪ {𝑧 ∈
ℤ ∣ -𝑧 ∈
ℕ0}) |
13 | | nnex 8871 |
. . . 4
⊢ ℕ
∈ V |
14 | 13 | enref 6739 |
. . 3
⊢ ℕ
≈ ℕ |
15 | | zex 9208 |
. . . . . 6
⊢ ℤ
∈ V |
16 | 15 | rabex 4131 |
. . . . 5
⊢ {𝑧 ∈ ℤ ∣ -𝑧 ∈ ℕ0}
∈ V |
17 | | nn0ex 9128 |
. . . . 5
⊢
ℕ0 ∈ V |
18 | | negeq 8099 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → -𝑧 = -𝑥) |
19 | 18 | eleq1d 2239 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → (-𝑧 ∈ ℕ0 ↔ -𝑥 ∈
ℕ0)) |
20 | 19 | elrab 2886 |
. . . . . 6
⊢ (𝑥 ∈ {𝑧 ∈ ℤ ∣ -𝑧 ∈ ℕ0} ↔ (𝑥 ∈ ℤ ∧ -𝑥 ∈
ℕ0)) |
21 | 20 | simprbi 273 |
. . . . 5
⊢ (𝑥 ∈ {𝑧 ∈ ℤ ∣ -𝑧 ∈ ℕ0} → -𝑥 ∈
ℕ0) |
22 | | negeq 8099 |
. . . . . . 7
⊢ (𝑧 = -𝑦 → -𝑧 = --𝑦) |
23 | 22 | eleq1d 2239 |
. . . . . 6
⊢ (𝑧 = -𝑦 → (-𝑧 ∈ ℕ0 ↔ --𝑦 ∈
ℕ0)) |
24 | | nn0negz 9233 |
. . . . . 6
⊢ (𝑦 ∈ ℕ0
→ -𝑦 ∈
ℤ) |
25 | | nn0cn 9132 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℂ) |
26 | 25 | negnegd 8208 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ0
→ --𝑦 = 𝑦) |
27 | 26 | eleq1d 2239 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ0
→ (--𝑦 ∈
ℕ0 ↔ 𝑦 ∈
ℕ0)) |
28 | 27 | ibir 176 |
. . . . . 6
⊢ (𝑦 ∈ ℕ0
→ --𝑦 ∈
ℕ0) |
29 | 23, 24, 28 | elrabd 2888 |
. . . . 5
⊢ (𝑦 ∈ ℕ0
→ -𝑦 ∈ {𝑧 ∈ ℤ ∣ -𝑧 ∈
ℕ0}) |
30 | | elrabi 2883 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑧 ∈ ℤ ∣ -𝑧 ∈ ℕ0} → 𝑥 ∈
ℤ) |
31 | 30 | adantr 274 |
. . . . . . 7
⊢ ((𝑥 ∈ {𝑧 ∈ ℤ ∣ -𝑧 ∈ ℕ0} ∧ 𝑦 ∈ ℕ0)
→ 𝑥 ∈
ℤ) |
32 | 31 | zcnd 9322 |
. . . . . 6
⊢ ((𝑥 ∈ {𝑧 ∈ ℤ ∣ -𝑧 ∈ ℕ0} ∧ 𝑦 ∈ ℕ0)
→ 𝑥 ∈
ℂ) |
33 | 25 | adantl 275 |
. . . . . 6
⊢ ((𝑥 ∈ {𝑧 ∈ ℤ ∣ -𝑧 ∈ ℕ0} ∧ 𝑦 ∈ ℕ0)
→ 𝑦 ∈
ℂ) |
34 | | negcon2 8159 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 = -𝑦 ↔ 𝑦 = -𝑥)) |
35 | 32, 33, 34 | syl2anc 409 |
. . . . 5
⊢ ((𝑥 ∈ {𝑧 ∈ ℤ ∣ -𝑧 ∈ ℕ0} ∧ 𝑦 ∈ ℕ0)
→ (𝑥 = -𝑦 ↔ 𝑦 = -𝑥)) |
36 | 16, 17, 21, 29, 35 | en3i 6745 |
. . . 4
⊢ {𝑧 ∈ ℤ ∣ -𝑧 ∈ ℕ0}
≈ ℕ0 |
37 | | nn0ennn 10376 |
. . . 4
⊢
ℕ0 ≈ ℕ |
38 | 36, 37 | entri 6760 |
. . 3
⊢ {𝑧 ∈ ℤ ∣ -𝑧 ∈ ℕ0}
≈ ℕ |
39 | | inrab2 3400 |
. . . 4
⊢ ({𝑧 ∈ ℤ ∣ -𝑧 ∈ ℕ0}
∩ ℕ) = {𝑧 ∈
(ℤ ∩ ℕ) ∣ -𝑧 ∈ ℕ0} |
40 | | incom 3319 |
. . . 4
⊢ ({𝑧 ∈ ℤ ∣ -𝑧 ∈ ℕ0}
∩ ℕ) = (ℕ ∩ {𝑧 ∈ ℤ ∣ -𝑧 ∈
ℕ0}) |
41 | | rabeq0 3443 |
. . . . 5
⊢ ({𝑧 ∈ (ℤ ∩ ℕ)
∣ -𝑧 ∈
ℕ0} = ∅ ↔ ∀𝑧 ∈ (ℤ ∩ ℕ) ¬ -𝑧 ∈
ℕ0) |
42 | | 0red 7908 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℕ ∧ -𝑧 ∈ ℕ0)
→ 0 ∈ ℝ) |
43 | | simpl 108 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℕ ∧ -𝑧 ∈ ℕ0)
→ 𝑧 ∈
ℕ) |
44 | 43 | nnred 8878 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℕ ∧ -𝑧 ∈ ℕ0)
→ 𝑧 ∈
ℝ) |
45 | | nngt0 8890 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℕ → 0 <
𝑧) |
46 | 45 | adantr 274 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℕ ∧ -𝑧 ∈ ℕ0)
→ 0 < 𝑧) |
47 | | nn0ge0 9147 |
. . . . . . . . . 10
⊢ (-𝑧 ∈ ℕ0
→ 0 ≤ -𝑧) |
48 | 47 | adantl 275 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℕ ∧ -𝑧 ∈ ℕ0)
→ 0 ≤ -𝑧) |
49 | 44 | le0neg1d 8423 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℕ ∧ -𝑧 ∈ ℕ0)
→ (𝑧 ≤ 0 ↔ 0
≤ -𝑧)) |
50 | 48, 49 | mpbird 166 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℕ ∧ -𝑧 ∈ ℕ0)
→ 𝑧 ≤
0) |
51 | 42, 44, 42, 46, 50 | ltletrd 8329 |
. . . . . . 7
⊢ ((𝑧 ∈ ℕ ∧ -𝑧 ∈ ℕ0)
→ 0 < 0) |
52 | 42 | ltnrd 8018 |
. . . . . . 7
⊢ ((𝑧 ∈ ℕ ∧ -𝑧 ∈ ℕ0)
→ ¬ 0 < 0) |
53 | 51, 52 | pm2.65da 656 |
. . . . . 6
⊢ (𝑧 ∈ ℕ → ¬
-𝑧 ∈
ℕ0) |
54 | 53, 4 | eleq2s 2265 |
. . . . 5
⊢ (𝑧 ∈ (ℤ ∩ ℕ)
→ ¬ -𝑧 ∈
ℕ0) |
55 | 41, 54 | mprgbir 2528 |
. . . 4
⊢ {𝑧 ∈ (ℤ ∩ ℕ)
∣ -𝑧 ∈
ℕ0} = ∅ |
56 | 39, 40, 55 | 3eqtr3i 2199 |
. . 3
⊢ (ℕ
∩ {𝑧 ∈ ℤ
∣ -𝑧 ∈
ℕ0}) = ∅ |
57 | | unennn 12339 |
. . 3
⊢ ((ℕ
≈ ℕ ∧ {𝑧
∈ ℤ ∣ -𝑧
∈ ℕ0} ≈ ℕ ∧ (ℕ ∩ {𝑧 ∈ ℤ ∣ -𝑧 ∈ ℕ0}) =
∅) → (ℕ ∪ {𝑧 ∈ ℤ ∣ -𝑧 ∈ ℕ0}) ≈
ℕ) |
58 | 14, 38, 56, 57 | mp3an 1332 |
. 2
⊢ (ℕ
∪ {𝑧 ∈ ℤ
∣ -𝑧 ∈
ℕ0}) ≈ ℕ |
59 | 12, 58 | eqbrtri 4008 |
1
⊢ ℤ
≈ ℕ |