| Step | Hyp | Ref
| Expression |
| 1 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑡 𝑁 ∈
ℕ0 |
| 2 | | nfmpt1 5250 |
. . . . . . . . 9
⊢
Ⅎ𝑡(𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴) |
| 3 | 2 | nfel1 2922 |
. . . . . . . 8
⊢
Ⅎ𝑡(𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)) |
| 4 | 1, 3 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑡(𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))) |
| 5 | | zex 12622 |
. . . . . . . . . . . . . 14
⊢ ℤ
∈ V |
| 6 | | nn0ssz 12636 |
. . . . . . . . . . . . . 14
⊢
ℕ0 ⊆ ℤ |
| 7 | | mapss 8929 |
. . . . . . . . . . . . . 14
⊢ ((ℤ
∈ V ∧ ℕ0 ⊆ ℤ) → (ℕ0
↑m (1...𝑁))
⊆ (ℤ ↑m (1...𝑁))) |
| 8 | 5, 6, 7 | mp2an 692 |
. . . . . . . . . . . . 13
⊢
(ℕ0 ↑m (1...𝑁)) ⊆ (ℤ ↑m
(1...𝑁)) |
| 9 | 8 | sseli 3979 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ (ℕ0
↑m (1...𝑁))
→ 𝑡 ∈ (ℤ
↑m (1...𝑁))) |
| 10 | 9 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑m (1...𝑁))) → 𝑡 ∈ (ℤ ↑m
(1...𝑁))) |
| 11 | | mzpf 42747 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
→ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴):(ℤ
↑m (1...𝑁))⟶ℤ) |
| 12 | | mptfcl 42731 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴):(ℤ
↑m (1...𝑁))⟶ℤ → (𝑡 ∈ (ℤ ↑m
(1...𝑁)) → 𝐴 ∈
ℤ)) |
| 13 | 12 | imp 406 |
. . . . . . . . . . . . 13
⊢ (((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴):(ℤ
↑m (1...𝑁))⟶ℤ ∧ 𝑡 ∈ (ℤ ↑m
(1...𝑁))) → 𝐴 ∈
ℤ) |
| 14 | 11, 9, 13 | syl2an 596 |
. . . . . . . . . . . 12
⊢ (((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ 𝑡 ∈
(ℕ0 ↑m (1...𝑁))) → 𝐴 ∈ ℤ) |
| 15 | 14 | adantll 714 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑m (1...𝑁))) → 𝐴 ∈ ℤ) |
| 16 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) = (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) |
| 17 | 16 | fvmpt2 7027 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ (ℤ
↑m (1...𝑁))
∧ 𝐴 ∈ ℤ)
→ ((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴)‘𝑡) = 𝐴) |
| 18 | 10, 15, 17 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑m (1...𝑁))) → ((𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴)‘𝑡) = 𝐴) |
| 19 | 18 | eqcomd 2743 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑m (1...𝑁))) → 𝐴 = ((𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴)‘𝑡)) |
| 20 | 19 | eqeq1d 2739 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
∧ 𝑡 ∈
(ℕ0 ↑m (1...𝑁))) → (𝐴 = 0 ↔ ((𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴)‘𝑡) = 0)) |
| 21 | 20 | ex 412 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ (𝑡 ∈
(ℕ0 ↑m (1...𝑁)) → (𝐴 = 0 ↔ ((𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴)‘𝑡) = 0))) |
| 22 | 4, 21 | ralrimi 3257 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ ∀𝑡 ∈
(ℕ0 ↑m (1...𝑁))(𝐴 = 0 ↔ ((𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴)‘𝑡) = 0)) |
| 23 | | rabbi 3467 |
. . . . . 6
⊢
(∀𝑡 ∈
(ℕ0 ↑m (1...𝑁))(𝐴 = 0 ↔ ((𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴)‘𝑡) = 0) ↔ {𝑡 ∈ (ℕ0
↑m (1...𝑁))
∣ 𝐴 = 0} = {𝑡 ∈ (ℕ0
↑m (1...𝑁))
∣ ((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴)‘𝑡) = 0}) |
| 24 | 22, 23 | sylib 218 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑m (1...𝑁)) ∣ 𝐴 = 0} = {𝑡 ∈ (ℕ0
↑m (1...𝑁))
∣ ((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴)‘𝑡) = 0}) |
| 25 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑡(ℕ0 ↑m
(1...𝑁)) |
| 26 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑎(ℕ0 ↑m
(1...𝑁)) |
| 27 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑎((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴)‘𝑡) = 0 |
| 28 | | nffvmpt1 6917 |
. . . . . . 7
⊢
Ⅎ𝑡((𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴)‘𝑎) |
| 29 | 28 | nfeq1 2921 |
. . . . . 6
⊢
Ⅎ𝑡((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴)‘𝑎) = 0 |
| 30 | | fveqeq2 6915 |
. . . . . 6
⊢ (𝑡 = 𝑎 → (((𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴)‘𝑡) = 0 ↔ ((𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴)‘𝑎) = 0)) |
| 31 | 25, 26, 27, 29, 30 | cbvrabw 3473 |
. . . . 5
⊢ {𝑡 ∈ (ℕ0
↑m (1...𝑁))
∣ ((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴)‘𝑡) = 0} = {𝑎 ∈ (ℕ0
↑m (1...𝑁))
∣ ((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴)‘𝑎) = 0} |
| 32 | 24, 31 | eqtrdi 2793 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑m (1...𝑁)) ∣ 𝐴 = 0} = {𝑎 ∈ (ℕ0
↑m (1...𝑁))
∣ ((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴)‘𝑎) = 0}) |
| 33 | | df-rab 3437 |
. . . 4
⊢ {𝑎 ∈ (ℕ0
↑m (1...𝑁))
∣ ((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴)‘𝑎) = 0} = {𝑎 ∣ (𝑎 ∈ (ℕ0
↑m (1...𝑁))
∧ ((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴)‘𝑎) = 0)} |
| 34 | 32, 33 | eqtrdi 2793 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑m (1...𝑁)) ∣ 𝐴 = 0} = {𝑎 ∣ (𝑎 ∈ (ℕ0
↑m (1...𝑁))
∧ ((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴)‘𝑎) = 0)}) |
| 35 | | elmapi 8889 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (ℕ0
↑m (1...𝑁))
→ 𝑏:(1...𝑁)⟶ℕ0) |
| 36 | | ffn 6736 |
. . . . . . . . . 10
⊢ (𝑏:(1...𝑁)⟶ℕ0 → 𝑏 Fn (1...𝑁)) |
| 37 | | fnresdm 6687 |
. . . . . . . . . 10
⊢ (𝑏 Fn (1...𝑁) → (𝑏 ↾ (1...𝑁)) = 𝑏) |
| 38 | 35, 36, 37 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑏 ∈ (ℕ0
↑m (1...𝑁))
→ (𝑏 ↾
(1...𝑁)) = 𝑏) |
| 39 | 38 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑏 ∈ (ℕ0
↑m (1...𝑁))
→ (𝑎 = (𝑏 ↾ (1...𝑁)) ↔ 𝑎 = 𝑏)) |
| 40 | | equcom 2017 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 ↔ 𝑏 = 𝑎) |
| 41 | 39, 40 | bitrdi 287 |
. . . . . . 7
⊢ (𝑏 ∈ (ℕ0
↑m (1...𝑁))
→ (𝑎 = (𝑏 ↾ (1...𝑁)) ↔ 𝑏 = 𝑎)) |
| 42 | 41 | anbi1d 631 |
. . . . . 6
⊢ (𝑏 ∈ (ℕ0
↑m (1...𝑁))
→ ((𝑎 = (𝑏 ↾ (1...𝑁)) ∧ ((𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0) ↔ (𝑏 = 𝑎 ∧ ((𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0))) |
| 43 | 42 | rexbiia 3092 |
. . . . 5
⊢
(∃𝑏 ∈
(ℕ0 ↑m (1...𝑁))(𝑎 = (𝑏 ↾ (1...𝑁)) ∧ ((𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0) ↔ ∃𝑏 ∈ (ℕ0
↑m (1...𝑁))(𝑏 = 𝑎 ∧ ((𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0)) |
| 44 | | fveqeq2 6915 |
. . . . . 6
⊢ (𝑏 = 𝑎 → (((𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0 ↔ ((𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴)‘𝑎) = 0)) |
| 45 | 44 | ceqsrexbv 3656 |
. . . . 5
⊢
(∃𝑏 ∈
(ℕ0 ↑m (1...𝑁))(𝑏 = 𝑎 ∧ ((𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0) ↔ (𝑎 ∈ (ℕ0
↑m (1...𝑁))
∧ ((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴)‘𝑎) = 0)) |
| 46 | 43, 45 | bitr2i 276 |
. . . 4
⊢ ((𝑎 ∈ (ℕ0
↑m (1...𝑁))
∧ ((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴)‘𝑎) = 0) ↔ ∃𝑏 ∈ (ℕ0
↑m (1...𝑁))(𝑎 = (𝑏 ↾ (1...𝑁)) ∧ ((𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0)) |
| 47 | 46 | abbii 2809 |
. . 3
⊢ {𝑎 ∣ (𝑎 ∈ (ℕ0
↑m (1...𝑁))
∧ ((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴)‘𝑎) = 0)} = {𝑎 ∣ ∃𝑏 ∈ (ℕ0
↑m (1...𝑁))(𝑎 = (𝑏 ↾ (1...𝑁)) ∧ ((𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0)} |
| 48 | 34, 47 | eqtrdi 2793 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑m (1...𝑁)) ∣ 𝐴 = 0} = {𝑎 ∣ ∃𝑏 ∈ (ℕ0
↑m (1...𝑁))(𝑎 = (𝑏 ↾ (1...𝑁)) ∧ ((𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0)}) |
| 49 | | simpl 482 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ 𝑁 ∈
ℕ0) |
| 50 | | nn0z 12638 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
| 51 | | uzid 12893 |
. . . . 5
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
(ℤ≥‘𝑁)) |
| 52 | 50, 51 | syl 17 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
(ℤ≥‘𝑁)) |
| 53 | 52 | adantr 480 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ 𝑁 ∈
(ℤ≥‘𝑁)) |
| 54 | | simpr 484 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))) |
| 55 | | eldioph 42769 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘𝑁) ∧ (𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ {𝑎 ∣
∃𝑏 ∈
(ℕ0 ↑m (1...𝑁))(𝑎 = (𝑏 ↾ (1...𝑁)) ∧ ((𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0)} ∈ (Dioph‘𝑁)) |
| 56 | 49, 53, 54, 55 | syl3anc 1373 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ {𝑎 ∣
∃𝑏 ∈
(ℕ0 ↑m (1...𝑁))(𝑎 = (𝑏 ↾ (1...𝑁)) ∧ ((𝑡 ∈ (ℤ ↑m
(1...𝑁)) ↦ 𝐴)‘𝑏) = 0)} ∈ (Dioph‘𝑁)) |
| 57 | 48, 56 | eqeltrd 2841 |
1
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑m (1...𝑁)) ∣ 𝐴 = 0} ∈ (Dioph‘𝑁)) |