Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . . 6
⊢ (𝑎 = 0 → (𝐴↑𝑎) = (𝐴↑0)) |
2 | 1 | mpteq2dv 4745 |
. . . . 5
⊢ (𝑎 = 0 → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑎)) = (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑0))) |
3 | 2 | eleq1d 2686 |
. . . 4
⊢ (𝑎 = 0 → ((𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑎)) ∈ (mzPoly‘𝑉) ↔ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑0)) ∈
(mzPoly‘𝑉))) |
4 | 3 | imbi2d 330 |
. . 3
⊢ (𝑎 = 0 → (((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑎)) ∈ (mzPoly‘𝑉)) ↔ ((𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑0)) ∈
(mzPoly‘𝑉)))) |
5 | | oveq2 6658 |
. . . . . 6
⊢ (𝑎 = 𝑏 → (𝐴↑𝑎) = (𝐴↑𝑏)) |
6 | 5 | mpteq2dv 4745 |
. . . . 5
⊢ (𝑎 = 𝑏 → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑎)) = (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑏))) |
7 | 6 | eleq1d 2686 |
. . . 4
⊢ (𝑎 = 𝑏 → ((𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑎)) ∈ (mzPoly‘𝑉) ↔ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉))) |
8 | 7 | imbi2d 330 |
. . 3
⊢ (𝑎 = 𝑏 → (((𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑎)) ∈ (mzPoly‘𝑉)) ↔ ((𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉)))) |
9 | | oveq2 6658 |
. . . . . 6
⊢ (𝑎 = (𝑏 + 1) → (𝐴↑𝑎) = (𝐴↑(𝑏 + 1))) |
10 | 9 | mpteq2dv 4745 |
. . . . 5
⊢ (𝑎 = (𝑏 + 1) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑎)) = (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑(𝑏 + 1)))) |
11 | 10 | eleq1d 2686 |
. . . 4
⊢ (𝑎 = (𝑏 + 1) → ((𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑎)) ∈ (mzPoly‘𝑉) ↔ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑(𝑏 + 1))) ∈ (mzPoly‘𝑉))) |
12 | 11 | imbi2d 330 |
. . 3
⊢ (𝑎 = (𝑏 + 1) → (((𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑎)) ∈ (mzPoly‘𝑉)) ↔ ((𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑(𝑏 + 1))) ∈ (mzPoly‘𝑉)))) |
13 | | oveq2 6658 |
. . . . . 6
⊢ (𝑎 = 𝐷 → (𝐴↑𝑎) = (𝐴↑𝐷)) |
14 | 13 | mpteq2dv 4745 |
. . . . 5
⊢ (𝑎 = 𝐷 → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑎)) = (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝐷))) |
15 | 14 | eleq1d 2686 |
. . . 4
⊢ (𝑎 = 𝐷 → ((𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑎)) ∈ (mzPoly‘𝑉) ↔ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝐷)) ∈ (mzPoly‘𝑉))) |
16 | 15 | imbi2d 330 |
. . 3
⊢ (𝑎 = 𝐷 → (((𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑎)) ∈ (mzPoly‘𝑉)) ↔ ((𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝐷)) ∈ (mzPoly‘𝑉)))) |
17 | | mzpf 37299 |
. . . . . . 7
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐴):(ℤ
↑𝑚 𝑉)⟶ℤ) |
18 | | zsscn 11385 |
. . . . . . 7
⊢ ℤ
⊆ ℂ |
19 | | fss 6056 |
. . . . . . 7
⊢ (((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴):(ℤ ↑𝑚 𝑉)⟶ℤ ∧ ℤ
⊆ ℂ) → (𝑥
∈ (ℤ ↑𝑚 𝑉) ↦ 𝐴):(ℤ ↑𝑚 𝑉)⟶ℂ) |
20 | 17, 18, 19 | sylancl 694 |
. . . . . 6
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐴):(ℤ
↑𝑚 𝑉)⟶ℂ) |
21 | | eqid 2622 |
. . . . . . 7
⊢ (𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) = (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐴) |
22 | 21 | fmpt 6381 |
. . . . . 6
⊢
(∀𝑥 ∈
(ℤ ↑𝑚 𝑉)𝐴 ∈ ℂ ↔ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐴):(ℤ
↑𝑚 𝑉)⟶ℂ) |
23 | 20, 22 | sylibr 224 |
. . . . 5
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → ∀𝑥 ∈ (ℤ ↑𝑚
𝑉)𝐴 ∈ ℂ) |
24 | | nfra1 2941 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑥 ∈ (ℤ ↑𝑚
𝑉)𝐴 ∈ ℂ |
25 | | rspa 2930 |
. . . . . . 7
⊢
((∀𝑥 ∈
(ℤ ↑𝑚 𝑉)𝐴 ∈ ℂ ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → 𝐴 ∈
ℂ) |
26 | 25 | exp0d 13002 |
. . . . . 6
⊢
((∀𝑥 ∈
(ℤ ↑𝑚 𝑉)𝐴 ∈ ℂ ∧ 𝑥 ∈ (ℤ ↑𝑚
𝑉)) → (𝐴↑0) = 1) |
27 | 24, 26 | mpteq2da 4743 |
. . . . 5
⊢
(∀𝑥 ∈
(ℤ ↑𝑚 𝑉)𝐴 ∈ ℂ → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑0)) = (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦
1)) |
28 | 23, 27 | syl 17 |
. . . 4
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑0)) = (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦
1)) |
29 | | elfvex 6221 |
. . . . 5
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → 𝑉 ∈ V) |
30 | | 1z 11407 |
. . . . 5
⊢ 1 ∈
ℤ |
31 | | mzpconstmpt 37303 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 1 ∈
ℤ) → (𝑥 ∈
(ℤ ↑𝑚 𝑉) ↦ 1) ∈ (mzPoly‘𝑉)) |
32 | 29, 30, 31 | sylancl 694 |
. . . 4
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 1) ∈
(mzPoly‘𝑉)) |
33 | 28, 32 | eqeltrd 2701 |
. . 3
⊢ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑0)) ∈
(mzPoly‘𝑉)) |
34 | 23 | 3ad2ant2 1083 |
. . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ (𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉)) → ∀𝑥 ∈ (ℤ ↑𝑚
𝑉)𝐴 ∈ ℂ) |
35 | | simp1 1061 |
. . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ (𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉)) → 𝑏 ∈ ℕ0) |
36 | | nfv 1843 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑏 ∈
ℕ0 |
37 | 24, 36 | nfan 1828 |
. . . . . . . 8
⊢
Ⅎ𝑥(∀𝑥 ∈ (ℤ ↑𝑚
𝑉)𝐴 ∈ ℂ ∧ 𝑏 ∈ ℕ0) |
38 | 25 | adantlr 751 |
. . . . . . . . 9
⊢
(((∀𝑥 ∈
(ℤ ↑𝑚 𝑉)𝐴 ∈ ℂ ∧ 𝑏 ∈ ℕ0) ∧ 𝑥 ∈ (ℤ
↑𝑚 𝑉)) → 𝐴 ∈ ℂ) |
39 | | simplr 792 |
. . . . . . . . 9
⊢
(((∀𝑥 ∈
(ℤ ↑𝑚 𝑉)𝐴 ∈ ℂ ∧ 𝑏 ∈ ℕ0) ∧ 𝑥 ∈ (ℤ
↑𝑚 𝑉)) → 𝑏 ∈ ℕ0) |
40 | 38, 39 | expp1d 13009 |
. . . . . . . 8
⊢
(((∀𝑥 ∈
(ℤ ↑𝑚 𝑉)𝐴 ∈ ℂ ∧ 𝑏 ∈ ℕ0) ∧ 𝑥 ∈ (ℤ
↑𝑚 𝑉)) → (𝐴↑(𝑏 + 1)) = ((𝐴↑𝑏) · 𝐴)) |
41 | 37, 40 | mpteq2da 4743 |
. . . . . . 7
⊢
((∀𝑥 ∈
(ℤ ↑𝑚 𝑉)𝐴 ∈ ℂ ∧ 𝑏 ∈ ℕ0) → (𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝐴↑(𝑏 + 1))) = (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ ((𝐴↑𝑏) · 𝐴))) |
42 | 34, 35, 41 | syl2anc 693 |
. . . . . 6
⊢ ((𝑏 ∈ ℕ0
∧ (𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑(𝑏 + 1))) = (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ ((𝐴↑𝑏) · 𝐴))) |
43 | | simp3 1063 |
. . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ (𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉)) |
44 | | simp2 1062 |
. . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ (𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉)) |
45 | | mzpmulmpt 37305 |
. . . . . . 7
⊢ (((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ ((𝐴↑𝑏) · 𝐴)) ∈ (mzPoly‘𝑉)) |
46 | 43, 44, 45 | syl2anc 693 |
. . . . . 6
⊢ ((𝑏 ∈ ℕ0
∧ (𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ ((𝐴↑𝑏) · 𝐴)) ∈ (mzPoly‘𝑉)) |
47 | 42, 46 | eqeltrd 2701 |
. . . . 5
⊢ ((𝑏 ∈ ℕ0
∧ (𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉)) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑(𝑏 + 1))) ∈ (mzPoly‘𝑉)) |
48 | 47 | 3exp 1264 |
. . . 4
⊢ (𝑏 ∈ ℕ0
→ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → ((𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑(𝑏 + 1))) ∈ (mzPoly‘𝑉)))) |
49 | 48 | a2d 29 |
. . 3
⊢ (𝑏 ∈ ℕ0
→ (((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝑏)) ∈ (mzPoly‘𝑉)) → ((𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑(𝑏 + 1))) ∈ (mzPoly‘𝑉)))) |
50 | 4, 8, 12, 16, 33, 49 | nn0ind 11472 |
. 2
⊢ (𝐷 ∈ ℕ0
→ ((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) → (𝑥 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝐴↑𝐷)) ∈ (mzPoly‘𝑉))) |
51 | 50 | impcom 446 |
1
⊢ (((𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ 𝐴) ∈ (mzPoly‘𝑉) ∧ 𝐷 ∈ ℕ0) → (𝑥 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝐴↑𝐷)) ∈ (mzPoly‘𝑉)) |