Step | Hyp | Ref
| Expression |
1 | | nfv 1883 |
. . . . . . . 8
⊢
Ⅎ𝑡 𝑁 ∈
ℕ0 |
2 | | nfmpt1 4780 |
. . . . . . . . 9
⊢
Ⅎ𝑡(𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴) |
3 | 2 | nfel1 2808 |
. . . . . . . 8
⊢
Ⅎ𝑡(𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) |
4 | 1, 3 | nfan 1868 |
. . . . . . 7
⊢
Ⅎ𝑡(𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) |
5 | | zex 11424 |
. . . . . . . . . . . . . 14
⊢ ℤ
∈ V |
6 | | nn0ssz 11436 |
. . . . . . . . . . . . . 14
⊢
ℕ0 ⊆ ℤ |
7 | | mapss 7942 |
. . . . . . . . . . . . . 14
⊢ ((ℤ
∈ V ∧ ℕ0 ⊆ ℤ) → (ℕ0
↑𝑚 (1...𝑁)) ⊆ (ℤ
↑𝑚 (1...𝑁))) |
8 | 5, 6, 7 | mp2an 708 |
. . . . . . . . . . . . 13
⊢
(ℕ0 ↑𝑚 (1...𝑁)) ⊆ (ℤ
↑𝑚 (1...𝑁)) |
9 | 8 | sseli 3632 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) → 𝑡 ∈ (ℤ ↑𝑚
(1...𝑁))) |
10 | 9 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) ∧ 𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁))) → 𝑡 ∈ (ℤ ↑𝑚
(1...𝑁))) |
11 | | mzpf 37616 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) → (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴):(ℤ
↑𝑚 (1...𝑁))⟶ℤ) |
12 | | mptfcl 37600 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴):(ℤ ↑𝑚
(1...𝑁))⟶ℤ
→ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) → 𝐴 ∈ ℤ)) |
13 | 12 | imp 444 |
. . . . . . . . . . . . 13
⊢ (((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴):(ℤ ↑𝑚
(1...𝑁))⟶ℤ
∧ 𝑡 ∈ (ℤ
↑𝑚 (1...𝑁))) → 𝐴 ∈ ℤ) |
14 | 11, 9, 13 | syl2an 493 |
. . . . . . . . . . . 12
⊢ (((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ 𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁))) → 𝐴 ∈ ℤ) |
15 | 14 | adantll 750 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) ∧ 𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁))) → 𝐴 ∈ ℤ) |
16 | | eqid 2651 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) = (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴) |
17 | 16 | fvmpt2 6330 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ∧ 𝐴 ∈ ℤ) → ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑡) = 𝐴) |
18 | 10, 15, 17 | syl2anc 694 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) ∧ 𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁))) → ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑡) = 𝐴) |
19 | 18 | eqcomd 2657 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) ∧ 𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁))) → 𝐴 = ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑡)) |
20 | 19 | eqeq1d 2653 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) ∧ 𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁))) → (𝐴 = 0 ↔ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑡) = 0)) |
21 | 20 | ex 449 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) → (𝐴 = 0 ↔ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑡) = 0))) |
22 | 4, 21 | ralrimi 2986 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → ∀𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁))(𝐴 = 0 ↔ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑡) = 0)) |
23 | | rabbi 3150 |
. . . . . 6
⊢
(∀𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁))(𝐴 = 0 ↔ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑡) = 0) ↔ {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ 𝐴 = 0} = {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑡) = 0}) |
24 | 22, 23 | sylib 208 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ 𝐴 = 0} = {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑡) = 0}) |
25 | | nfcv 2793 |
. . . . . 6
⊢
Ⅎ𝑡(ℕ0
↑𝑚 (1...𝑁)) |
26 | | nfcv 2793 |
. . . . . 6
⊢
Ⅎ𝑎(ℕ0
↑𝑚 (1...𝑁)) |
27 | | nfv 1883 |
. . . . . 6
⊢
Ⅎ𝑎((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴)‘𝑡) = 0 |
28 | | nffvmpt1 6237 |
. . . . . . 7
⊢
Ⅎ𝑡((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑎) |
29 | 28 | nfeq1 2807 |
. . . . . 6
⊢
Ⅎ𝑡((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴)‘𝑎) = 0 |
30 | | fveq2 6229 |
. . . . . . 7
⊢ (𝑡 = 𝑎 → ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑡) = ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑎)) |
31 | 30 | eqeq1d 2653 |
. . . . . 6
⊢ (𝑡 = 𝑎 → (((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑡) = 0 ↔ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑎) = 0)) |
32 | 25, 26, 27, 29, 31 | cbvrab 3229 |
. . . . 5
⊢ {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑡) = 0} = {𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑎) = 0} |
33 | 24, 32 | syl6eq 2701 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ 𝐴 = 0} = {𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑎) = 0}) |
34 | | df-rab 2950 |
. . . 4
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑎) = 0} = {𝑎 ∣ (𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑎) = 0)} |
35 | 33, 34 | syl6eq 2701 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ 𝐴 = 0} = {𝑎 ∣ (𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑎) = 0)}) |
36 | | elmapi 7921 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (ℕ0
↑𝑚 (1...𝑁)) → 𝑏:(1...𝑁)⟶ℕ0) |
37 | | ffn 6083 |
. . . . . . . . . 10
⊢ (𝑏:(1...𝑁)⟶ℕ0 → 𝑏 Fn (1...𝑁)) |
38 | | fnresdm 6038 |
. . . . . . . . . 10
⊢ (𝑏 Fn (1...𝑁) → (𝑏 ↾ (1...𝑁)) = 𝑏) |
39 | 36, 37, 38 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑏 ∈ (ℕ0
↑𝑚 (1...𝑁)) → (𝑏 ↾ (1...𝑁)) = 𝑏) |
40 | 39 | eqeq2d 2661 |
. . . . . . . 8
⊢ (𝑏 ∈ (ℕ0
↑𝑚 (1...𝑁)) → (𝑎 = (𝑏 ↾ (1...𝑁)) ↔ 𝑎 = 𝑏)) |
41 | | equcom 1991 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 ↔ 𝑏 = 𝑎) |
42 | 40, 41 | syl6bb 276 |
. . . . . . 7
⊢ (𝑏 ∈ (ℕ0
↑𝑚 (1...𝑁)) → (𝑎 = (𝑏 ↾ (1...𝑁)) ↔ 𝑏 = 𝑎)) |
43 | 42 | anbi1d 741 |
. . . . . 6
⊢ (𝑏 ∈ (ℕ0
↑𝑚 (1...𝑁)) → ((𝑎 = (𝑏 ↾ (1...𝑁)) ∧ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0) ↔ (𝑏 = 𝑎 ∧ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0))) |
44 | 43 | rexbiia 3069 |
. . . . 5
⊢
(∃𝑏 ∈
(ℕ0 ↑𝑚 (1...𝑁))(𝑎 = (𝑏 ↾ (1...𝑁)) ∧ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0) ↔ ∃𝑏 ∈ (ℕ0
↑𝑚 (1...𝑁))(𝑏 = 𝑎 ∧ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0)) |
45 | | fveq2 6229 |
. . . . . . 7
⊢ (𝑏 = 𝑎 → ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑏) = ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑎)) |
46 | 45 | eqeq1d 2653 |
. . . . . 6
⊢ (𝑏 = 𝑎 → (((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0 ↔ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑎) = 0)) |
47 | 46 | ceqsrexbv 3368 |
. . . . 5
⊢
(∃𝑏 ∈
(ℕ0 ↑𝑚 (1...𝑁))(𝑏 = 𝑎 ∧ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0) ↔ (𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑎) = 0)) |
48 | 44, 47 | bitr2i 265 |
. . . 4
⊢ ((𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑎) = 0) ↔ ∃𝑏 ∈ (ℕ0
↑𝑚 (1...𝑁))(𝑎 = (𝑏 ↾ (1...𝑁)) ∧ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0)) |
49 | 48 | abbii 2768 |
. . 3
⊢ {𝑎 ∣ (𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑎) = 0)} = {𝑎 ∣ ∃𝑏 ∈ (ℕ0
↑𝑚 (1...𝑁))(𝑎 = (𝑏 ↾ (1...𝑁)) ∧ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0)} |
50 | 35, 49 | syl6eq 2701 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ 𝐴 = 0} = {𝑎 ∣ ∃𝑏 ∈ (ℕ0
↑𝑚 (1...𝑁))(𝑎 = (𝑏 ↾ (1...𝑁)) ∧ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0)}) |
51 | | simpl 472 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → 𝑁 ∈
ℕ0) |
52 | | nn0z 11438 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
53 | | uzid 11740 |
. . . . 5
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
(ℤ≥‘𝑁)) |
54 | 52, 53 | syl 17 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
(ℤ≥‘𝑁)) |
55 | 54 | adantr 480 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → 𝑁 ∈ (ℤ≥‘𝑁)) |
56 | | simpr 476 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴) ∈
(mzPoly‘(1...𝑁))) |
57 | | eldioph 37638 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘𝑁) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ {𝑎 ∣
∃𝑏 ∈
(ℕ0 ↑𝑚 (1...𝑁))(𝑎 = (𝑏 ↾ (1...𝑁)) ∧ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0)} ∈ (Dioph‘𝑁)) |
58 | 51, 55, 56, 57 | syl3anc 1366 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → {𝑎 ∣ ∃𝑏 ∈ (ℕ0
↑𝑚 (1...𝑁))(𝑎 = (𝑏 ↾ (1...𝑁)) ∧ ((𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0)} ∈ (Dioph‘𝑁)) |
59 | 50, 58 | eqeltrd 2730 |
1
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ 𝐴 = 0} ∈ (Dioph‘𝑁)) |