Proof of Theorem xnn0nnen
Step | Hyp | Ref
| Expression |
1 | | fnresi 5371 |
. . . . . . . 8
⊢ ( I
↾ ℕ0) Fn ℕ0 |
2 | | pnfex 8073 |
. . . . . . . . 9
⊢ +∞
∈ V |
3 | | neg1z 9349 |
. . . . . . . . . 10
⊢ -1 ∈
ℤ |
4 | 3 | elexi 2772 |
. . . . . . . . 9
⊢ -1 ∈
V |
5 | 2, 4 | fnsn 5308 |
. . . . . . . 8
⊢
{〈+∞, -1〉} Fn {+∞} |
6 | 1, 5 | pm3.2i 272 |
. . . . . . 7
⊢ (( I
↾ ℕ0) Fn ℕ0 ∧ {〈+∞,
-1〉} Fn {+∞}) |
7 | | disj 3495 |
. . . . . . . 8
⊢
((ℕ0 ∩ {+∞}) = ∅ ↔ ∀𝑥 ∈ ℕ0
¬ 𝑥 ∈
{+∞}) |
8 | | nn0nepnf 9311 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ0
→ 𝑥 ≠
+∞) |
9 | | nelsn 3653 |
. . . . . . . . 9
⊢ (𝑥 ≠ +∞ → ¬
𝑥 ∈
{+∞}) |
10 | 8, 9 | syl 14 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ0
→ ¬ 𝑥 ∈
{+∞}) |
11 | 7, 10 | mprgbir 2552 |
. . . . . . 7
⊢
(ℕ0 ∩ {+∞}) = ∅ |
12 | | fnun 5360 |
. . . . . . 7
⊢ (((( I
↾ ℕ0) Fn ℕ0 ∧ {〈+∞,
-1〉} Fn {+∞}) ∧ (ℕ0 ∩ {+∞}) =
∅) → (( I ↾ ℕ0) ∪ {〈+∞,
-1〉}) Fn (ℕ0 ∪ {+∞})) |
13 | 6, 11, 12 | mp2an 426 |
. . . . . 6
⊢ (( I
↾ ℕ0) ∪ {〈+∞, -1〉}) Fn
(ℕ0 ∪ {+∞}) |
14 | | uncom 3303 |
. . . . . . 7
⊢ (( I
↾ ℕ0) ∪ {〈+∞, -1〉}) =
({〈+∞, -1〉} ∪ ( I ↾
ℕ0)) |
15 | | df-xnn0 9304 |
. . . . . . . 8
⊢
ℕ0* = (ℕ0 ∪
{+∞}) |
16 | 15 | eqcomi 2197 |
. . . . . . 7
⊢
(ℕ0 ∪ {+∞}) =
ℕ0* |
17 | | fneq12 5347 |
. . . . . . 7
⊢ (((( I
↾ ℕ0) ∪ {〈+∞, -1〉}) =
({〈+∞, -1〉} ∪ ( I ↾ ℕ0)) ∧
(ℕ0 ∪ {+∞}) = ℕ0*)
→ ((( I ↾ ℕ0) ∪ {〈+∞, -1〉}) Fn
(ℕ0 ∪ {+∞}) ↔ ({〈+∞, -1〉} ∪
( I ↾ ℕ0)) Fn
ℕ0*)) |
18 | 14, 16, 17 | mp2an 426 |
. . . . . 6
⊢ ((( I
↾ ℕ0) ∪ {〈+∞, -1〉}) Fn
(ℕ0 ∪ {+∞}) ↔ ({〈+∞, -1〉} ∪
( I ↾ ℕ0)) Fn
ℕ0*) |
19 | 13, 18 | mpbi 145 |
. . . . 5
⊢
({〈+∞, -1〉} ∪ ( I ↾ ℕ0)) Fn
ℕ0* |
20 | 4, 2 | fnsn 5308 |
. . . . . . . . . 10
⊢
{〈-1, +∞〉} Fn {-1} |
21 | 20, 1 | pm3.2i 272 |
. . . . . . . . 9
⊢
({〈-1, +∞〉} Fn {-1} ∧ ( I ↾
ℕ0) Fn ℕ0) |
22 | | disj 3495 |
. . . . . . . . . 10
⊢ (({-1}
∩ ℕ0) = ∅ ↔ ∀𝑥 ∈ {-1} ¬ 𝑥 ∈ ℕ0) |
23 | | neg1lt0 9090 |
. . . . . . . . . . . 12
⊢ -1 <
0 |
24 | | nn0nlt0 9266 |
. . . . . . . . . . . 12
⊢ (-1
∈ ℕ0 → ¬ -1 < 0) |
25 | 23, 24 | mt2 641 |
. . . . . . . . . . 11
⊢ ¬ -1
∈ ℕ0 |
26 | | elsni 3636 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {-1} → 𝑥 = -1) |
27 | 26 | eleq1d 2262 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {-1} → (𝑥 ∈ ℕ0
↔ -1 ∈ ℕ0)) |
28 | 25, 27 | mtbiri 676 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {-1} → ¬ 𝑥 ∈
ℕ0) |
29 | 22, 28 | mprgbir 2552 |
. . . . . . . . 9
⊢ ({-1}
∩ ℕ0) = ∅ |
30 | | fnun 5360 |
. . . . . . . . 9
⊢
((({〈-1, +∞〉} Fn {-1} ∧ ( I ↾
ℕ0) Fn ℕ0) ∧ ({-1} ∩
ℕ0) = ∅) → ({〈-1, +∞〉} ∪ ( I
↾ ℕ0)) Fn ({-1} ∪
ℕ0)) |
31 | 21, 29, 30 | mp2an 426 |
. . . . . . . 8
⊢
({〈-1, +∞〉} ∪ ( I ↾ ℕ0)) Fn
({-1} ∪ ℕ0) |
32 | | cnvun 5071 |
. . . . . . . . . 10
⊢ ◡({〈+∞, -1〉} ∪ ( I
↾ ℕ0)) = (◡{〈+∞, -1〉} ∪ ◡( I ↾
ℕ0)) |
33 | 2, 4 | cnvsn 5148 |
. . . . . . . . . . 11
⊢ ◡{〈+∞, -1〉} = {〈-1,
+∞〉} |
34 | | cnvresid 5328 |
. . . . . . . . . . 11
⊢ ◡( I ↾ ℕ0) = ( I
↾ ℕ0) |
35 | 33, 34 | uneq12i 3311 |
. . . . . . . . . 10
⊢ (◡{〈+∞, -1〉} ∪ ◡( I ↾ ℕ0)) =
({〈-1, +∞〉} ∪ ( I ↾
ℕ0)) |
36 | 32, 35 | eqtri 2214 |
. . . . . . . . 9
⊢ ◡({〈+∞, -1〉} ∪ ( I
↾ ℕ0)) = ({〈-1, +∞〉} ∪ ( I ↾
ℕ0)) |
37 | 36 | fneq1i 5348 |
. . . . . . . 8
⊢ (◡({〈+∞, -1〉} ∪ ( I
↾ ℕ0)) Fn ({-1} ∪ ℕ0) ↔
({〈-1, +∞〉} ∪ ( I ↾ ℕ0)) Fn ({-1}
∪ ℕ0)) |
38 | 31, 37 | mpbir 146 |
. . . . . . 7
⊢ ◡({〈+∞, -1〉} ∪ ( I
↾ ℕ0)) Fn ({-1} ∪
ℕ0) |
39 | | fzosn 10272 |
. . . . . . . . . . 11
⊢ (-1
∈ ℤ → (-1..^(-1 + 1)) = {-1}) |
40 | 3, 39 | ax-mp 5 |
. . . . . . . . . 10
⊢ (-1..^(-1
+ 1)) = {-1} |
41 | | ax-1cn 7965 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
42 | 41, 41 | negsubdii 8304 |
. . . . . . . . . . . 12
⊢ -(1
− 1) = (-1 + 1) |
43 | | 1m1e0 9051 |
. . . . . . . . . . . . 13
⊢ (1
− 1) = 0 |
44 | 41, 41 | subcli 8295 |
. . . . . . . . . . . . . 14
⊢ (1
− 1) ∈ ℂ |
45 | | negeq0 8273 |
. . . . . . . . . . . . . 14
⊢ ((1
− 1) ∈ ℂ → ((1 − 1) = 0 ↔ -(1 − 1) =
0)) |
46 | 44, 45 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ((1
− 1) = 0 ↔ -(1 − 1) = 0) |
47 | 43, 46 | mpbi 145 |
. . . . . . . . . . . 12
⊢ -(1
− 1) = 0 |
48 | 42, 47 | eqtr3i 2216 |
. . . . . . . . . . 11
⊢ (-1 + 1)
= 0 |
49 | 48 | oveq2i 5929 |
. . . . . . . . . 10
⊢ (-1..^(-1
+ 1)) = (-1..^0) |
50 | 40, 49 | eqtr3i 2216 |
. . . . . . . . 9
⊢ {-1} =
(-1..^0) |
51 | | nn0uz 9627 |
. . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘0) |
52 | 50, 51 | uneq12i 3311 |
. . . . . . . 8
⊢ ({-1}
∪ ℕ0) = ((-1..^0) ∪
(ℤ≥‘0)) |
53 | 52 | fneq2i 5349 |
. . . . . . 7
⊢ (◡({〈+∞, -1〉} ∪ ( I
↾ ℕ0)) Fn ({-1} ∪ ℕ0) ↔ ◡({〈+∞, -1〉} ∪ ( I
↾ ℕ0)) Fn ((-1..^0) ∪
(ℤ≥‘0))) |
54 | 38, 53 | mpbi 145 |
. . . . . 6
⊢ ◡({〈+∞, -1〉} ∪ ( I
↾ ℕ0)) Fn ((-1..^0) ∪
(ℤ≥‘0)) |
55 | | 0z 9328 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
56 | | neg1rr 9088 |
. . . . . . . . . 10
⊢ -1 ∈
ℝ |
57 | | 0re 8019 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
58 | 56, 57, 23 | ltleii 8122 |
. . . . . . . . 9
⊢ -1 ≤
0 |
59 | | eluz2 9598 |
. . . . . . . . 9
⊢ (0 ∈
(ℤ≥‘-1) ↔ (-1 ∈ ℤ ∧ 0 ∈
ℤ ∧ -1 ≤ 0)) |
60 | 3, 55, 58, 59 | mpbir3an 1181 |
. . . . . . . 8
⊢ 0 ∈
(ℤ≥‘-1) |
61 | | fzouzsplit 10246 |
. . . . . . . 8
⊢ (0 ∈
(ℤ≥‘-1) → (ℤ≥‘-1) =
((-1..^0) ∪ (ℤ≥‘0))) |
62 | 60, 61 | ax-mp 5 |
. . . . . . 7
⊢
(ℤ≥‘-1) = ((-1..^0) ∪
(ℤ≥‘0)) |
63 | 62 | fneq2i 5349 |
. . . . . 6
⊢ (◡({〈+∞, -1〉} ∪ ( I
↾ ℕ0)) Fn (ℤ≥‘-1) ↔ ◡({〈+∞, -1〉} ∪ ( I
↾ ℕ0)) Fn ((-1..^0) ∪
(ℤ≥‘0))) |
64 | 54, 63 | mpbir 146 |
. . . . 5
⊢ ◡({〈+∞, -1〉} ∪ ( I
↾ ℕ0)) Fn
(ℤ≥‘-1) |
65 | 19, 64 | pm3.2i 272 |
. . . 4
⊢
(({〈+∞, -1〉} ∪ ( I ↾ ℕ0)) Fn
ℕ0* ∧ ◡({〈+∞, -1〉} ∪ ( I
↾ ℕ0)) Fn
(ℤ≥‘-1)) |
66 | | dff1o4 5508 |
. . . 4
⊢
(({〈+∞, -1〉} ∪ ( I ↾
ℕ0)):ℕ0*–1-1-onto→(ℤ≥‘-1) ↔
(({〈+∞, -1〉} ∪ ( I ↾ ℕ0)) Fn
ℕ0* ∧ ◡({〈+∞, -1〉} ∪ ( I
↾ ℕ0)) Fn
(ℤ≥‘-1))) |
67 | 65, 66 | mpbir 146 |
. . 3
⊢
({〈+∞, -1〉} ∪ ( I ↾
ℕ0)):ℕ0*–1-1-onto→(ℤ≥‘-1) |
68 | | nn0ex 9246 |
. . . . . 6
⊢
ℕ0 ∈ V |
69 | 2 | snex 4214 |
. . . . . 6
⊢
{+∞} ∈ V |
70 | 68, 69 | unex 4472 |
. . . . 5
⊢
(ℕ0 ∪ {+∞}) ∈ V |
71 | 15, 70 | eqeltri 2266 |
. . . 4
⊢
ℕ0* ∈ V |
72 | 71 | f1oen 6813 |
. . 3
⊢
(({〈+∞, -1〉} ∪ ( I ↾
ℕ0)):ℕ0*–1-1-onto→(ℤ≥‘-1) →
ℕ0* ≈
(ℤ≥‘-1)) |
73 | 67, 72 | ax-mp 5 |
. 2
⊢
ℕ0* ≈
(ℤ≥‘-1) |
74 | | uzennn 10507 |
. . 3
⊢ (-1
∈ ℤ → (ℤ≥‘-1) ≈
ℕ) |
75 | 3, 74 | ax-mp 5 |
. 2
⊢
(ℤ≥‘-1) ≈ ℕ |
76 | 73, 75 | entri 6840 |
1
⊢
ℕ0* ≈ ℕ |