Proof of Theorem k0004val0
Step | Hyp | Ref
| Expression |
1 | | 0nn0 11724 |
. . 3
⊢ 0 ∈
ℕ0 |
2 | | k0004.a |
. . . 4
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ {𝑡 ∈ ((0[,]1)
↑𝑚 (1...(𝑛 + 1))) ∣ Σ𝑘 ∈ (1...(𝑛 + 1))(𝑡‘𝑘) = 1}) |
3 | 2 | k0004val 39860 |
. . 3
⊢ (0 ∈
ℕ0 → (𝐴‘0) = {𝑡 ∈ ((0[,]1) ↑𝑚
(1...(0 + 1))) ∣ Σ𝑘 ∈ (1...(0 + 1))(𝑡‘𝑘) = 1}) |
4 | 1, 3 | ax-mp 5 |
. 2
⊢ (𝐴‘0) = {𝑡 ∈ ((0[,]1) ↑𝑚
(1...(0 + 1))) ∣ Σ𝑘 ∈ (1...(0 + 1))(𝑡‘𝑘) = 1} |
5 | | 0p1e1 11569 |
. . . . . . . 8
⊢ (0 + 1) =
1 |
6 | 5 | oveq2i 6987 |
. . . . . . 7
⊢ (1...(0 +
1)) = (1...1) |
7 | | 1z 11825 |
. . . . . . . 8
⊢ 1 ∈
ℤ |
8 | | fzsn 12765 |
. . . . . . . 8
⊢ (1 ∈
ℤ → (1...1) = {1}) |
9 | 7, 8 | ax-mp 5 |
. . . . . . 7
⊢ (1...1) =
{1} |
10 | 6, 9 | eqtri 2803 |
. . . . . 6
⊢ (1...(0 +
1)) = {1} |
11 | 10 | oveq2i 6987 |
. . . . 5
⊢ ((0[,]1)
↑𝑚 (1...(0 + 1))) = ((0[,]1) ↑𝑚
{1}) |
12 | | rabeq 3407 |
. . . . 5
⊢ (((0[,]1)
↑𝑚 (1...(0 + 1))) = ((0[,]1) ↑𝑚
{1}) → {𝑡 ∈
((0[,]1) ↑𝑚 (1...(0 + 1))) ∣ Σ𝑘 ∈ (1...(0 + 1))(𝑡‘𝑘) = 1} = {𝑡 ∈ ((0[,]1) ↑𝑚
{1}) ∣ Σ𝑘
∈ (1...(0 + 1))(𝑡‘𝑘) = 1}) |
13 | 11, 12 | ax-mp 5 |
. . . 4
⊢ {𝑡 ∈ ((0[,]1)
↑𝑚 (1...(0 + 1))) ∣ Σ𝑘 ∈ (1...(0 + 1))(𝑡‘𝑘) = 1} = {𝑡 ∈ ((0[,]1) ↑𝑚
{1}) ∣ Σ𝑘
∈ (1...(0 + 1))(𝑡‘𝑘) = 1} |
14 | 10 | sumeq1i 14915 |
. . . . . . 7
⊢
Σ𝑘 ∈
(1...(0 + 1))(𝑡‘𝑘) = Σ𝑘 ∈ {1} (𝑡‘𝑘) |
15 | | elmapi 8228 |
. . . . . . . . 9
⊢ (𝑡 ∈ ((0[,]1)
↑𝑚 {1}) → 𝑡:{1}⟶(0[,]1)) |
16 | | fsn2g 6723 |
. . . . . . . . . . 11
⊢ (1 ∈
ℤ → (𝑡:{1}⟶(0[,]1) ↔ ((𝑡‘1) ∈ (0[,]1) ∧
𝑡 = {〈1, (𝑡‘1)〉}))) |
17 | 7, 16 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑡:{1}⟶(0[,]1) ↔
((𝑡‘1) ∈ (0[,]1)
∧ 𝑡 = {〈1, (𝑡‘1)〉})) |
18 | 17 | biimpi 208 |
. . . . . . . . 9
⊢ (𝑡:{1}⟶(0[,]1) →
((𝑡‘1) ∈ (0[,]1)
∧ 𝑡 = {〈1, (𝑡‘1)〉})) |
19 | | unitssre 12701 |
. . . . . . . . . . . 12
⊢ (0[,]1)
⊆ ℝ |
20 | | ax-resscn 10392 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ |
21 | 19, 20 | sstri 3868 |
. . . . . . . . . . 11
⊢ (0[,]1)
⊆ ℂ |
22 | 21 | sseli 3855 |
. . . . . . . . . 10
⊢ ((𝑡‘1) ∈ (0[,]1) →
(𝑡‘1) ∈
ℂ) |
23 | 22 | adantr 473 |
. . . . . . . . 9
⊢ (((𝑡‘1) ∈ (0[,]1) ∧
𝑡 = {〈1, (𝑡‘1)〉}) → (𝑡‘1) ∈
ℂ) |
24 | 15, 18, 23 | 3syl 18 |
. . . . . . . 8
⊢ (𝑡 ∈ ((0[,]1)
↑𝑚 {1}) → (𝑡‘1) ∈ ℂ) |
25 | | fveq2 6499 |
. . . . . . . . 9
⊢ (𝑘 = 1 → (𝑡‘𝑘) = (𝑡‘1)) |
26 | 25 | sumsn 14961 |
. . . . . . . 8
⊢ ((1
∈ ℤ ∧ (𝑡‘1) ∈ ℂ) → Σ𝑘 ∈ {1} (𝑡‘𝑘) = (𝑡‘1)) |
27 | 7, 24, 26 | sylancr 578 |
. . . . . . 7
⊢ (𝑡 ∈ ((0[,]1)
↑𝑚 {1}) → Σ𝑘 ∈ {1} (𝑡‘𝑘) = (𝑡‘1)) |
28 | 14, 27 | syl5eq 2827 |
. . . . . 6
⊢ (𝑡 ∈ ((0[,]1)
↑𝑚 {1}) → Σ𝑘 ∈ (1...(0 + 1))(𝑡‘𝑘) = (𝑡‘1)) |
29 | 28 | eqeq1d 2781 |
. . . . 5
⊢ (𝑡 ∈ ((0[,]1)
↑𝑚 {1}) → (Σ𝑘 ∈ (1...(0 + 1))(𝑡‘𝑘) = 1 ↔ (𝑡‘1) = 1)) |
30 | 29 | rabbiia 3399 |
. . . 4
⊢ {𝑡 ∈ ((0[,]1)
↑𝑚 {1}) ∣ Σ𝑘 ∈ (1...(0 + 1))(𝑡‘𝑘) = 1} = {𝑡 ∈ ((0[,]1) ↑𝑚
{1}) ∣ (𝑡‘1) =
1} |
31 | 13, 30 | eqtri 2803 |
. . 3
⊢ {𝑡 ∈ ((0[,]1)
↑𝑚 (1...(0 + 1))) ∣ Σ𝑘 ∈ (1...(0 + 1))(𝑡‘𝑘) = 1} = {𝑡 ∈ ((0[,]1) ↑𝑚
{1}) ∣ (𝑡‘1) =
1} |
32 | | rabeqsn 4478 |
. . . 4
⊢ ({𝑡 ∈ ((0[,]1)
↑𝑚 {1}) ∣ (𝑡‘1) = 1} = {{〈1, 1〉}} ↔
∀𝑡((𝑡 ∈ ((0[,]1)
↑𝑚 {1}) ∧ (𝑡‘1) = 1) ↔ 𝑡 = {〈1, 1〉})) |
33 | | ovex 7008 |
. . . . 5
⊢ (0[,]1)
∈ V |
34 | | 1elunit 12672 |
. . . . 5
⊢ 1 ∈
(0[,]1) |
35 | | k0004lem3 39859 |
. . . . 5
⊢ ((1
∈ ℤ ∧ (0[,]1) ∈ V ∧ 1 ∈ (0[,]1)) → ((𝑡 ∈ ((0[,]1)
↑𝑚 {1}) ∧ (𝑡‘1) = 1) ↔ 𝑡 = {〈1, 1〉})) |
36 | 7, 33, 34, 35 | mp3an 1440 |
. . . 4
⊢ ((𝑡 ∈ ((0[,]1)
↑𝑚 {1}) ∧ (𝑡‘1) = 1) ↔ 𝑡 = {〈1, 1〉}) |
37 | 32, 36 | mpgbir 1762 |
. . 3
⊢ {𝑡 ∈ ((0[,]1)
↑𝑚 {1}) ∣ (𝑡‘1) = 1} = {{〈1,
1〉}} |
38 | 31, 37 | eqtri 2803 |
. 2
⊢ {𝑡 ∈ ((0[,]1)
↑𝑚 (1...(0 + 1))) ∣ Σ𝑘 ∈ (1...(0 + 1))(𝑡‘𝑘) = 1} = {{〈1,
1〉}} |
39 | 4, 38 | eqtri 2803 |
1
⊢ (𝐴‘0) = {{〈1,
1〉}} |