Metamath Proof Explorer

Theorem mzpexpmpt

Description: Raise a polynomial function to a (fixed) exponent. (Contributed by Stefan O'Rear, 5-Oct-2014)

Ref Expression
Assertion mzpexpmpt ⊢ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V ∧ D ∈ ℕ 0 → x ∈ ℤ V ⟼ A D ∈ mzPoly ⁡ V

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ a = 0 → A a = A 0
2 1 mpteq2dv ⊢ a = 0 → x ∈ ℤ V ⟼ A a = x ∈ ℤ V ⟼ A 0
3 2 eleq1d ⊢ a = 0 → x ∈ ℤ V ⟼ A a ∈ mzPoly ⁡ V ↔ x ∈ ℤ V ⟼ A 0 ∈ mzPoly ⁡ V
4 3 imbi2d ⊢ a = 0 → x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A a ∈ mzPoly ⁡ V ↔ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A 0 ∈ mzPoly ⁡ V
5 oveq2 ⊢ a = b → A a = A b
6 5 mpteq2dv ⊢ a = b → x ∈ ℤ V ⟼ A a = x ∈ ℤ V ⟼ A b
7 6 eleq1d ⊢ a = b → x ∈ ℤ V ⟼ A a ∈ mzPoly ⁡ V ↔ x ∈ ℤ V ⟼ A b ∈ mzPoly ⁡ V
8 7 imbi2d ⊢ a = b → x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A a ∈ mzPoly ⁡ V ↔ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A b ∈ mzPoly ⁡ V
9 oveq2 ⊢ a = b + 1 → A a = A b + 1
10 9 mpteq2dv ⊢ a = b + 1 → x ∈ ℤ V ⟼ A a = x ∈ ℤ V ⟼ A b + 1
11 10 eleq1d ⊢ a = b + 1 → x ∈ ℤ V ⟼ A a ∈ mzPoly ⁡ V ↔ x ∈ ℤ V ⟼ A b + 1 ∈ mzPoly ⁡ V
12 11 imbi2d ⊢ a = b + 1 → x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A a ∈ mzPoly ⁡ V ↔ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A b + 1 ∈ mzPoly ⁡ V
13 oveq2 ⊢ a = D → A a = A D
14 13 mpteq2dv ⊢ a = D → x ∈ ℤ V ⟼ A a = x ∈ ℤ V ⟼ A D
15 14 eleq1d ⊢ a = D → x ∈ ℤ V ⟼ A a ∈ mzPoly ⁡ V ↔ x ∈ ℤ V ⟼ A D ∈ mzPoly ⁡ V
16 15 imbi2d ⊢ a = D → x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A a ∈ mzPoly ⁡ V ↔ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A D ∈ mzPoly ⁡ V
17 mzpf ⊢ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A : ℤ V ⟶ ℤ
18 zsscn ⊢ ℤ ⊆ ℂ
19 fss ⊢ x ∈ ℤ V ⟼ A : ℤ V ⟶ ℤ ∧ ℤ ⊆ ℂ → x ∈ ℤ V ⟼ A : ℤ V ⟶ ℂ
20 17 18 19 sylancl ⊢ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A : ℤ V ⟶ ℂ
21 eqid ⊢ x ∈ ℤ V ⟼ A = x ∈ ℤ V ⟼ A
22 21 fmpt ⊢ ∀ x ∈ ℤ V A ∈ ℂ ↔ x ∈ ℤ V ⟼ A : ℤ V ⟶ ℂ
23 20 22 sylibr ⊢ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → ∀ x ∈ ℤ V A ∈ ℂ
24 nfra1 ⊢ Ⅎ x ∀ x ∈ ℤ V A ∈ ℂ
25 rspa ⊢ ∀ x ∈ ℤ V A ∈ ℂ ∧ x ∈ ℤ V → A ∈ ℂ
26 25 exp0d ⊢ ∀ x ∈ ℤ V A ∈ ℂ ∧ x ∈ ℤ V → A 0 = 1
27 24 26 mpteq2da ⊢ ∀ x ∈ ℤ V A ∈ ℂ → x ∈ ℤ V ⟼ A 0 = x ∈ ℤ V ⟼ 1
28 23 27 syl ⊢ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A 0 = x ∈ ℤ V ⟼ 1
29 elfvex ⊢ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → V ∈ V
30 1z ⊢ 1 ∈ ℤ
31 mzpconstmpt ⊢ V ∈ V ∧ 1 ∈ ℤ → x ∈ ℤ V ⟼ 1 ∈ mzPoly ⁡ V
32 29 30 31 sylancl ⊢ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ 1 ∈ mzPoly ⁡ V
33 28 32 eqeltrd ⊢ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A 0 ∈ mzPoly ⁡ V
34 23 3ad2ant2 ⊢ b ∈ ℕ 0 ∧ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V ∧ x ∈ ℤ V ⟼ A b ∈ mzPoly ⁡ V → ∀ x ∈ ℤ V A ∈ ℂ
35 simp1 ⊢ b ∈ ℕ 0 ∧ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V ∧ x ∈ ℤ V ⟼ A b ∈ mzPoly ⁡ V → b ∈ ℕ 0
36 nfv ⊢ Ⅎ x b ∈ ℕ 0
37 24 36 nfan ⊢ Ⅎ x ∀ x ∈ ℤ V A ∈ ℂ ∧ b ∈ ℕ 0
38 25 adantlr ⊢ ∀ x ∈ ℤ V A ∈ ℂ ∧ b ∈ ℕ 0 ∧ x ∈ ℤ V → A ∈ ℂ
39 simplr ⊢ ∀ x ∈ ℤ V A ∈ ℂ ∧ b ∈ ℕ 0 ∧ x ∈ ℤ V → b ∈ ℕ 0
40 38 39 expp1d ⊢ ∀ x ∈ ℤ V A ∈ ℂ ∧ b ∈ ℕ 0 ∧ x ∈ ℤ V → A b + 1 = A b ⁢ A
41 37 40 mpteq2da ⊢ ∀ x ∈ ℤ V A ∈ ℂ ∧ b ∈ ℕ 0 → x ∈ ℤ V ⟼ A b + 1 = x ∈ ℤ V ⟼ A b ⁢ A
42 34 35 41 syl2anc ⊢ b ∈ ℕ 0 ∧ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V ∧ x ∈ ℤ V ⟼ A b ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A b + 1 = x ∈ ℤ V ⟼ A b ⁢ A
43 simp3 ⊢ b ∈ ℕ 0 ∧ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V ∧ x ∈ ℤ V ⟼ A b ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A b ∈ mzPoly ⁡ V
44 simp2 ⊢ b ∈ ℕ 0 ∧ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V ∧ x ∈ ℤ V ⟼ A b ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V
45 mzpmulmpt ⊢ x ∈ ℤ V ⟼ A b ∈ mzPoly ⁡ V ∧ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A b ⁢ A ∈ mzPoly ⁡ V
46 43 44 45 syl2anc ⊢ b ∈ ℕ 0 ∧ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V ∧ x ∈ ℤ V ⟼ A b ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A b ⁢ A ∈ mzPoly ⁡ V
47 42 46 eqeltrd ⊢ b ∈ ℕ 0 ∧ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V ∧ x ∈ ℤ V ⟼ A b ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A b + 1 ∈ mzPoly ⁡ V
48 47 3exp ⊢ b ∈ ℕ 0 → x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A b ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A b + 1 ∈ mzPoly ⁡ V
49 48 a2d ⊢ b ∈ ℕ 0 → x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A b ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A b + 1 ∈ mzPoly ⁡ V
50 4 8 12 16 33 49 nn0ind ⊢ D ∈ ℕ 0 → x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V → x ∈ ℤ V ⟼ A D ∈ mzPoly ⁡ V
51 50 impcom ⊢ x ∈ ℤ V ⟼ A ∈ mzPoly ⁡ V ∧ D ∈ ℕ 0 → x ∈ ℤ V ⟼ A D ∈ mzPoly ⁡ V