Step |
Hyp |
Ref |
Expression |
1 |
|
elaa2lem.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝔸 ) |
2 |
|
elaa2lem.an0 |
⊢ ( 𝜑 → 𝐴 ≠ 0 ) |
3 |
|
elaa2lem.g |
⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ ℤ ) ) |
4 |
|
elaa2lem.gn0 |
⊢ ( 𝜑 → 𝐺 ≠ 0𝑝 ) |
5 |
|
elaa2lem.ga |
⊢ ( 𝜑 → ( 𝐺 ‘ 𝐴 ) = 0 ) |
6 |
|
elaa2lem.m |
⊢ 𝑀 = inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < ) |
7 |
|
elaa2lem.i |
⊢ 𝐼 = ( 𝑘 ∈ ℕ0 ↦ ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ) |
8 |
|
elaa2lem.f |
⊢ 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( 𝐼 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) |
9 |
8
|
a1i |
⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( 𝐼 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
10 |
|
zsscn |
⊢ ℤ ⊆ ℂ |
11 |
10
|
a1i |
⊢ ( 𝜑 → ℤ ⊆ ℂ ) |
12 |
|
dgrcl |
⊢ ( 𝐺 ∈ ( Poly ‘ ℤ ) → ( deg ‘ 𝐺 ) ∈ ℕ0 ) |
13 |
3 12
|
syl |
⊢ ( 𝜑 → ( deg ‘ 𝐺 ) ∈ ℕ0 ) |
14 |
13
|
nn0zd |
⊢ ( 𝜑 → ( deg ‘ 𝐺 ) ∈ ℤ ) |
15 |
|
ssrab2 |
⊢ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ⊆ ℕ0 |
16 |
|
nn0uz |
⊢ ℕ0 = ( ℤ≥ ‘ 0 ) |
17 |
15 16
|
sseqtri |
⊢ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ⊆ ( ℤ≥ ‘ 0 ) |
18 |
17
|
a1i |
⊢ ( 𝜑 → { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ⊆ ( ℤ≥ ‘ 0 ) ) |
19 |
4
|
neneqd |
⊢ ( 𝜑 → ¬ 𝐺 = 0𝑝 ) |
20 |
|
eqid |
⊢ ( deg ‘ 𝐺 ) = ( deg ‘ 𝐺 ) |
21 |
|
eqid |
⊢ ( coeff ‘ 𝐺 ) = ( coeff ‘ 𝐺 ) |
22 |
20 21
|
dgreq0 |
⊢ ( 𝐺 ∈ ( Poly ‘ ℤ ) → ( 𝐺 = 0𝑝 ↔ ( ( coeff ‘ 𝐺 ) ‘ ( deg ‘ 𝐺 ) ) = 0 ) ) |
23 |
3 22
|
syl |
⊢ ( 𝜑 → ( 𝐺 = 0𝑝 ↔ ( ( coeff ‘ 𝐺 ) ‘ ( deg ‘ 𝐺 ) ) = 0 ) ) |
24 |
19 23
|
mtbid |
⊢ ( 𝜑 → ¬ ( ( coeff ‘ 𝐺 ) ‘ ( deg ‘ 𝐺 ) ) = 0 ) |
25 |
24
|
neqned |
⊢ ( 𝜑 → ( ( coeff ‘ 𝐺 ) ‘ ( deg ‘ 𝐺 ) ) ≠ 0 ) |
26 |
13 25
|
jca |
⊢ ( 𝜑 → ( ( deg ‘ 𝐺 ) ∈ ℕ0 ∧ ( ( coeff ‘ 𝐺 ) ‘ ( deg ‘ 𝐺 ) ) ≠ 0 ) ) |
27 |
|
fveq2 |
⊢ ( 𝑛 = ( deg ‘ 𝐺 ) → ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) = ( ( coeff ‘ 𝐺 ) ‘ ( deg ‘ 𝐺 ) ) ) |
28 |
27
|
neeq1d |
⊢ ( 𝑛 = ( deg ‘ 𝐺 ) → ( ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 ↔ ( ( coeff ‘ 𝐺 ) ‘ ( deg ‘ 𝐺 ) ) ≠ 0 ) ) |
29 |
28
|
elrab |
⊢ ( ( deg ‘ 𝐺 ) ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ↔ ( ( deg ‘ 𝐺 ) ∈ ℕ0 ∧ ( ( coeff ‘ 𝐺 ) ‘ ( deg ‘ 𝐺 ) ) ≠ 0 ) ) |
30 |
26 29
|
sylibr |
⊢ ( 𝜑 → ( deg ‘ 𝐺 ) ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ) |
31 |
30
|
ne0d |
⊢ ( 𝜑 → { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ≠ ∅ ) |
32 |
|
infssuzcl |
⊢ ( ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ⊆ ( ℤ≥ ‘ 0 ) ∧ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ≠ ∅ ) → inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ) |
33 |
18 31 32
|
syl2anc |
⊢ ( 𝜑 → inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ) |
34 |
15 33
|
sseldi |
⊢ ( 𝜑 → inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ∈ ℕ0 ) |
35 |
6 34
|
eqeltrid |
⊢ ( 𝜑 → 𝑀 ∈ ℕ0 ) |
36 |
35
|
nn0zd |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
37 |
14 36
|
zsubcld |
⊢ ( 𝜑 → ( ( deg ‘ 𝐺 ) − 𝑀 ) ∈ ℤ ) |
38 |
6
|
a1i |
⊢ ( 𝜑 → 𝑀 = inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ) |
39 |
|
infssuzle |
⊢ ( ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ⊆ ( ℤ≥ ‘ 0 ) ∧ ( deg ‘ 𝐺 ) ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ) → inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ≤ ( deg ‘ 𝐺 ) ) |
40 |
18 30 39
|
syl2anc |
⊢ ( 𝜑 → inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ≤ ( deg ‘ 𝐺 ) ) |
41 |
38 40
|
eqbrtrd |
⊢ ( 𝜑 → 𝑀 ≤ ( deg ‘ 𝐺 ) ) |
42 |
13
|
nn0red |
⊢ ( 𝜑 → ( deg ‘ 𝐺 ) ∈ ℝ ) |
43 |
35
|
nn0red |
⊢ ( 𝜑 → 𝑀 ∈ ℝ ) |
44 |
42 43
|
subge0d |
⊢ ( 𝜑 → ( 0 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ↔ 𝑀 ≤ ( deg ‘ 𝐺 ) ) ) |
45 |
41 44
|
mpbird |
⊢ ( 𝜑 → 0 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) |
46 |
37 45
|
jca |
⊢ ( 𝜑 → ( ( ( deg ‘ 𝐺 ) − 𝑀 ) ∈ ℤ ∧ 0 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) |
47 |
|
elnn0z |
⊢ ( ( ( deg ‘ 𝐺 ) − 𝑀 ) ∈ ℕ0 ↔ ( ( ( deg ‘ 𝐺 ) − 𝑀 ) ∈ ℤ ∧ 0 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) |
48 |
46 47
|
sylibr |
⊢ ( 𝜑 → ( ( deg ‘ 𝐺 ) − 𝑀 ) ∈ ℕ0 ) |
49 |
|
0zd |
⊢ ( 𝐺 ∈ ( Poly ‘ ℤ ) → 0 ∈ ℤ ) |
50 |
21
|
coef2 |
⊢ ( ( 𝐺 ∈ ( Poly ‘ ℤ ) ∧ 0 ∈ ℤ ) → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℤ ) |
51 |
3 49 50
|
syl2anc2 |
⊢ ( 𝜑 → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℤ ) |
52 |
51
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℤ ) |
53 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 ) |
54 |
35
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ ℕ0 ) |
55 |
53 54
|
nn0addcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 + 𝑀 ) ∈ ℕ0 ) |
56 |
52 55
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ∈ ℤ ) |
57 |
56 7
|
fmptd |
⊢ ( 𝜑 → 𝐼 : ℕ0 ⟶ ℤ ) |
58 |
|
elplyr |
⊢ ( ( ℤ ⊆ ℂ ∧ ( ( deg ‘ 𝐺 ) − 𝑀 ) ∈ ℕ0 ∧ 𝐼 : ℕ0 ⟶ ℤ ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( 𝐼 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ ℤ ) ) |
59 |
11 48 57 58
|
syl3anc |
⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( 𝐼 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ ℤ ) ) |
60 |
9 59
|
eqeltrd |
⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℤ ) ) |
61 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) |
62 |
61
|
iftrued |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → if ( 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) , ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) , 0 ) = ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ) |
63 |
|
iffalse |
⊢ ( ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) → if ( 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) , ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) , 0 ) = 0 ) |
64 |
63
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → if ( 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) , ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) , 0 ) = 0 ) |
65 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) |
66 |
42
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( deg ‘ 𝐺 ) ∈ ℝ ) |
67 |
43
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → 𝑀 ∈ ℝ ) |
68 |
66 67
|
resubcld |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( ( deg ‘ 𝐺 ) − 𝑀 ) ∈ ℝ ) |
69 |
|
nn0re |
⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ ) |
70 |
69
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → 𝑘 ∈ ℝ ) |
71 |
68 70
|
ltnled |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( ( ( deg ‘ 𝐺 ) − 𝑀 ) < 𝑘 ↔ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) |
72 |
65 71
|
mpbird |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( ( deg ‘ 𝐺 ) − 𝑀 ) < 𝑘 ) |
73 |
66 67 70
|
ltsubaddd |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( ( ( deg ‘ 𝐺 ) − 𝑀 ) < 𝑘 ↔ ( deg ‘ 𝐺 ) < ( 𝑘 + 𝑀 ) ) ) |
74 |
72 73
|
mpbid |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( deg ‘ 𝐺 ) < ( 𝑘 + 𝑀 ) ) |
75 |
|
olc |
⊢ ( ( deg ‘ 𝐺 ) < ( 𝑘 + 𝑀 ) → ( 𝐺 = 0𝑝 ∨ ( deg ‘ 𝐺 ) < ( 𝑘 + 𝑀 ) ) ) |
76 |
74 75
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( 𝐺 = 0𝑝 ∨ ( deg ‘ 𝐺 ) < ( 𝑘 + 𝑀 ) ) ) |
77 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → 𝐺 ∈ ( Poly ‘ ℤ ) ) |
78 |
55
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( 𝑘 + 𝑀 ) ∈ ℕ0 ) |
79 |
20 21
|
dgrlt |
⊢ ( ( 𝐺 ∈ ( Poly ‘ ℤ ) ∧ ( 𝑘 + 𝑀 ) ∈ ℕ0 ) → ( ( 𝐺 = 0𝑝 ∨ ( deg ‘ 𝐺 ) < ( 𝑘 + 𝑀 ) ) ↔ ( ( deg ‘ 𝐺 ) ≤ ( 𝑘 + 𝑀 ) ∧ ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) = 0 ) ) ) |
80 |
77 78 79
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( ( 𝐺 = 0𝑝 ∨ ( deg ‘ 𝐺 ) < ( 𝑘 + 𝑀 ) ) ↔ ( ( deg ‘ 𝐺 ) ≤ ( 𝑘 + 𝑀 ) ∧ ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) = 0 ) ) ) |
81 |
76 80
|
mpbid |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( ( deg ‘ 𝐺 ) ≤ ( 𝑘 + 𝑀 ) ∧ ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) = 0 ) ) |
82 |
81
|
simprd |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) = 0 ) |
83 |
64 82
|
eqtr4d |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → if ( 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) , ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) , 0 ) = ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ) |
84 |
62 83
|
pm2.61dan |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) , ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) , 0 ) = ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ) |
85 |
84
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) , ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) , 0 ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ) ) |
86 |
51 11
|
fssd |
⊢ ( 𝜑 → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℂ ) |
87 |
86
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℂ ) |
88 |
|
elfznn0 |
⊢ ( 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) → 𝑘 ∈ ℕ0 ) |
89 |
88
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → 𝑘 ∈ ℕ0 ) |
90 |
35
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → 𝑀 ∈ ℕ0 ) |
91 |
89 90
|
nn0addcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( 𝑘 + 𝑀 ) ∈ ℕ0 ) |
92 |
87 91
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ∈ ℂ ) |
93 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) = ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) |
94 |
|
simpl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → 𝜑 ) |
95 |
7
|
a1i |
⊢ ( 𝜑 → 𝐼 = ( 𝑘 ∈ ℕ0 ↦ ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ) ) |
96 |
95 56
|
fvmpt2d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐼 ‘ 𝑘 ) = ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ) |
97 |
94 89 96
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( 𝐼 ‘ 𝑘 ) = ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ) |
98 |
97
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( 𝐼 ‘ 𝑘 ) = ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ) |
99 |
98
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( ( 𝐼 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) |
100 |
93 99
|
sumeq12rdv |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( 𝐼 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) |
101 |
100
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( 𝐼 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
102 |
9 101
|
eqtrd |
⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
103 |
60 48 92 102
|
coeeq2 |
⊢ ( 𝜑 → ( coeff ‘ 𝐹 ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ ( ( deg ‘ 𝐺 ) − 𝑀 ) , ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) , 0 ) ) ) |
104 |
85 103 95
|
3eqtr4d |
⊢ ( 𝜑 → ( coeff ‘ 𝐹 ) = 𝐼 ) |
105 |
104
|
fveq1d |
⊢ ( 𝜑 → ( ( coeff ‘ 𝐹 ) ‘ 0 ) = ( 𝐼 ‘ 0 ) ) |
106 |
|
oveq1 |
⊢ ( 𝑘 = 0 → ( 𝑘 + 𝑀 ) = ( 0 + 𝑀 ) ) |
107 |
106
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → ( 𝑘 + 𝑀 ) = ( 0 + 𝑀 ) ) |
108 |
10 36
|
sseldi |
⊢ ( 𝜑 → 𝑀 ∈ ℂ ) |
109 |
108
|
addid2d |
⊢ ( 𝜑 → ( 0 + 𝑀 ) = 𝑀 ) |
110 |
109
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → ( 0 + 𝑀 ) = 𝑀 ) |
111 |
107 110
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → ( 𝑘 + 𝑀 ) = 𝑀 ) |
112 |
111
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) ) |
113 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
114 |
113
|
a1i |
⊢ ( 𝜑 → 0 ∈ ℕ0 ) |
115 |
51 35
|
ffvelrnd |
⊢ ( 𝜑 → ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) ∈ ℤ ) |
116 |
95 112 114 115
|
fvmptd |
⊢ ( 𝜑 → ( 𝐼 ‘ 0 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) ) |
117 |
|
eqidd |
⊢ ( 𝜑 → ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) ) |
118 |
105 116 117
|
3eqtrd |
⊢ ( 𝜑 → ( ( coeff ‘ 𝐹 ) ‘ 0 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) ) |
119 |
38 33
|
eqeltrd |
⊢ ( 𝜑 → 𝑀 ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ) |
120 |
|
fveq2 |
⊢ ( 𝑛 = 𝑀 → ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) ) |
121 |
120
|
neeq1d |
⊢ ( 𝑛 = 𝑀 → ( ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 ↔ ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) ≠ 0 ) ) |
122 |
121
|
elrab |
⊢ ( 𝑀 ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ↔ ( 𝑀 ∈ ℕ0 ∧ ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) ≠ 0 ) ) |
123 |
119 122
|
sylib |
⊢ ( 𝜑 → ( 𝑀 ∈ ℕ0 ∧ ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) ≠ 0 ) ) |
124 |
123
|
simprd |
⊢ ( 𝜑 → ( ( coeff ‘ 𝐺 ) ‘ 𝑀 ) ≠ 0 ) |
125 |
118 124
|
eqnetrd |
⊢ ( 𝜑 → ( ( coeff ‘ 𝐹 ) ‘ 0 ) ≠ 0 ) |
126 |
3 49
|
syl |
⊢ ( 𝜑 → 0 ∈ ℤ ) |
127 |
|
aasscn |
⊢ 𝔸 ⊆ ℂ |
128 |
127 1
|
sseldi |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
129 |
94 128
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → 𝐴 ∈ ℂ ) |
130 |
129 89
|
expcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ ) |
131 |
92 130
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ ) |
132 |
|
fvoveq1 |
⊢ ( 𝑘 = ( 𝑗 − 𝑀 ) → ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) = ( ( coeff ‘ 𝐺 ) ‘ ( ( 𝑗 − 𝑀 ) + 𝑀 ) ) ) |
133 |
|
oveq2 |
⊢ ( 𝑘 = ( 𝑗 − 𝑀 ) → ( 𝐴 ↑ 𝑘 ) = ( 𝐴 ↑ ( 𝑗 − 𝑀 ) ) ) |
134 |
132 133
|
oveq12d |
⊢ ( 𝑘 = ( 𝑗 − 𝑀 ) → ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝐴 ↑ 𝑘 ) ) = ( ( ( coeff ‘ 𝐺 ) ‘ ( ( 𝑗 − 𝑀 ) + 𝑀 ) ) · ( 𝐴 ↑ ( 𝑗 − 𝑀 ) ) ) ) |
135 |
36 126 37 131 134
|
fsumshft |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝐴 ↑ 𝑘 ) ) = Σ 𝑗 ∈ ( ( 0 + 𝑀 ) ... ( ( ( deg ‘ 𝐺 ) − 𝑀 ) + 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( ( 𝑗 − 𝑀 ) + 𝑀 ) ) · ( 𝐴 ↑ ( 𝑗 − 𝑀 ) ) ) ) |
136 |
10 14
|
sseldi |
⊢ ( 𝜑 → ( deg ‘ 𝐺 ) ∈ ℂ ) |
137 |
136 108
|
npcand |
⊢ ( 𝜑 → ( ( ( deg ‘ 𝐺 ) − 𝑀 ) + 𝑀 ) = ( deg ‘ 𝐺 ) ) |
138 |
109 137
|
oveq12d |
⊢ ( 𝜑 → ( ( 0 + 𝑀 ) ... ( ( ( deg ‘ 𝐺 ) − 𝑀 ) + 𝑀 ) ) = ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) |
139 |
138
|
sumeq1d |
⊢ ( 𝜑 → Σ 𝑗 ∈ ( ( 0 + 𝑀 ) ... ( ( ( deg ‘ 𝐺 ) − 𝑀 ) + 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( ( 𝑗 − 𝑀 ) + 𝑀 ) ) · ( 𝐴 ↑ ( 𝑗 − 𝑀 ) ) ) = Σ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( ( 𝑗 − 𝑀 ) + 𝑀 ) ) · ( 𝐴 ↑ ( 𝑗 − 𝑀 ) ) ) ) |
140 |
|
elfzelz |
⊢ ( 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) → 𝑗 ∈ ℤ ) |
141 |
140
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑗 ∈ ℤ ) |
142 |
10 141
|
sseldi |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑗 ∈ ℂ ) |
143 |
108
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑀 ∈ ℂ ) |
144 |
142 143
|
npcand |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( 𝑗 − 𝑀 ) + 𝑀 ) = 𝑗 ) |
145 |
144
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( coeff ‘ 𝐺 ) ‘ ( ( 𝑗 − 𝑀 ) + 𝑀 ) ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) ) |
146 |
145
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( ( coeff ‘ 𝐺 ) ‘ ( ( 𝑗 − 𝑀 ) + 𝑀 ) ) · ( 𝐴 ↑ ( 𝑗 − 𝑀 ) ) ) = ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ ( 𝑗 − 𝑀 ) ) ) ) |
147 |
128
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝐴 ∈ ℂ ) |
148 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝐴 ≠ 0 ) |
149 |
36
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑀 ∈ ℤ ) |
150 |
147 148 149 141
|
expsubd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( 𝐴 ↑ ( 𝑗 − 𝑀 ) ) = ( ( 𝐴 ↑ 𝑗 ) / ( 𝐴 ↑ 𝑀 ) ) ) |
151 |
150
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ ( 𝑗 − 𝑀 ) ) ) = ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( ( 𝐴 ↑ 𝑗 ) / ( 𝐴 ↑ 𝑀 ) ) ) ) |
152 |
86
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℂ ) |
153 |
|
0red |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 0 ∈ ℝ ) |
154 |
43
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑀 ∈ ℝ ) |
155 |
141
|
zred |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑗 ∈ ℝ ) |
156 |
35
|
nn0ge0d |
⊢ ( 𝜑 → 0 ≤ 𝑀 ) |
157 |
156
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 0 ≤ 𝑀 ) |
158 |
|
elfzle1 |
⊢ ( 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) → 𝑀 ≤ 𝑗 ) |
159 |
158
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑀 ≤ 𝑗 ) |
160 |
153 154 155 157 159
|
letrd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 0 ≤ 𝑗 ) |
161 |
141 160
|
jca |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( 𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ) ) |
162 |
|
elnn0z |
⊢ ( 𝑗 ∈ ℕ0 ↔ ( 𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ) ) |
163 |
161 162
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑗 ∈ ℕ0 ) |
164 |
152 163
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) ∈ ℂ ) |
165 |
147 163
|
expcld |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( 𝐴 ↑ 𝑗 ) ∈ ℂ ) |
166 |
128 35
|
expcld |
⊢ ( 𝜑 → ( 𝐴 ↑ 𝑀 ) ∈ ℂ ) |
167 |
166
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( 𝐴 ↑ 𝑀 ) ∈ ℂ ) |
168 |
147 148 149
|
expne0d |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( 𝐴 ↑ 𝑀 ) ≠ 0 ) |
169 |
164 165 167 168
|
divassd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) / ( 𝐴 ↑ 𝑀 ) ) = ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( ( 𝐴 ↑ 𝑗 ) / ( 𝐴 ↑ 𝑀 ) ) ) ) |
170 |
169
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( ( 𝐴 ↑ 𝑗 ) / ( 𝐴 ↑ 𝑀 ) ) ) = ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) / ( 𝐴 ↑ 𝑀 ) ) ) |
171 |
151 170
|
eqtr2d |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) / ( 𝐴 ↑ 𝑀 ) ) = ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ ( 𝑗 − 𝑀 ) ) ) ) |
172 |
146 171
|
eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( ( coeff ‘ 𝐺 ) ‘ ( ( 𝑗 − 𝑀 ) + 𝑀 ) ) · ( 𝐴 ↑ ( 𝑗 − 𝑀 ) ) ) = ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) / ( 𝐴 ↑ 𝑀 ) ) ) |
173 |
172
|
sumeq2dv |
⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( ( 𝑗 − 𝑀 ) + 𝑀 ) ) · ( 𝐴 ↑ ( 𝑗 − 𝑀 ) ) ) = Σ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) / ( 𝐴 ↑ 𝑀 ) ) ) |
174 |
139 173
|
eqtrd |
⊢ ( 𝜑 → Σ 𝑗 ∈ ( ( 0 + 𝑀 ) ... ( ( ( deg ‘ 𝐺 ) − 𝑀 ) + 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( ( 𝑗 − 𝑀 ) + 𝑀 ) ) · ( 𝐴 ↑ ( 𝑗 − 𝑀 ) ) ) = Σ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) / ( 𝐴 ↑ 𝑀 ) ) ) |
175 |
35 16
|
eleqtrdi |
⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) ) |
176 |
|
fzss1 |
⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → ( 𝑀 ... ( deg ‘ 𝐺 ) ) ⊆ ( 0 ... ( deg ‘ 𝐺 ) ) ) |
177 |
175 176
|
syl |
⊢ ( 𝜑 → ( 𝑀 ... ( deg ‘ 𝐺 ) ) ⊆ ( 0 ... ( deg ‘ 𝐺 ) ) ) |
178 |
164 165
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) ∈ ℂ ) |
179 |
178 167 168
|
divcld |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) / ( 𝐴 ↑ 𝑀 ) ) ∈ ℂ ) |
180 |
36
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → 𝑀 ∈ ℤ ) |
181 |
14
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → ( deg ‘ 𝐺 ) ∈ ℤ ) |
182 |
|
eldifi |
⊢ ( 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ) |
183 |
182
|
elfzelzd |
⊢ ( 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑗 ∈ ℤ ) |
184 |
183
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → 𝑗 ∈ ℤ ) |
185 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → ¬ 𝑗 < 𝑀 ) |
186 |
43
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → 𝑀 ∈ ℝ ) |
187 |
184
|
zred |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → 𝑗 ∈ ℝ ) |
188 |
186 187
|
lenltd |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → ( 𝑀 ≤ 𝑗 ↔ ¬ 𝑗 < 𝑀 ) ) |
189 |
185 188
|
mpbird |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → 𝑀 ≤ 𝑗 ) |
190 |
|
elfzle2 |
⊢ ( 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) → 𝑗 ≤ ( deg ‘ 𝐺 ) ) |
191 |
182 190
|
syl |
⊢ ( 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑗 ≤ ( deg ‘ 𝐺 ) ) |
192 |
191
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → 𝑗 ≤ ( deg ‘ 𝐺 ) ) |
193 |
180 181 184 189 192
|
elfzd |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) |
194 |
|
eldifn |
⊢ ( 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → ¬ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) |
195 |
194
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ 𝑗 < 𝑀 ) → ¬ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) |
196 |
193 195
|
condan |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → 𝑗 < 𝑀 ) |
197 |
196
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → 𝑗 < 𝑀 ) |
198 |
6
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → 𝑀 = inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ) |
199 |
17
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ⊆ ( ℤ≥ ‘ 0 ) ) |
200 |
|
elfznn0 |
⊢ ( 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) → 𝑗 ∈ ℕ0 ) |
201 |
182 200
|
syl |
⊢ ( 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑗 ∈ ℕ0 ) |
202 |
201
|
adantr |
⊢ ( ( 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → 𝑗 ∈ ℕ0 ) |
203 |
|
neqne |
⊢ ( ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 → ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) ≠ 0 ) |
204 |
203
|
adantl |
⊢ ( ( 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) ≠ 0 ) |
205 |
202 204
|
jca |
⊢ ( ( 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → ( 𝑗 ∈ ℕ0 ∧ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) ≠ 0 ) ) |
206 |
|
fveq2 |
⊢ ( 𝑛 = 𝑗 → ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) = ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) ) |
207 |
206
|
neeq1d |
⊢ ( 𝑛 = 𝑗 → ( ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 ↔ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) ≠ 0 ) ) |
208 |
207
|
elrab |
⊢ ( 𝑗 ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ↔ ( 𝑗 ∈ ℕ0 ∧ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) ≠ 0 ) ) |
209 |
205 208
|
sylibr |
⊢ ( ( 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → 𝑗 ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ) |
210 |
209
|
adantll |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → 𝑗 ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ) |
211 |
|
infssuzle |
⊢ ( ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ⊆ ( ℤ≥ ‘ 0 ) ∧ 𝑗 ∈ { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } ) → inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ≤ 𝑗 ) |
212 |
199 210 211
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → inf ( { 𝑛 ∈ ℕ0 ∣ ( ( coeff ‘ 𝐺 ) ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ≤ 𝑗 ) |
213 |
198 212
|
eqbrtrd |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → 𝑀 ≤ 𝑗 ) |
214 |
43
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → 𝑀 ∈ ℝ ) |
215 |
183
|
zred |
⊢ ( 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) → 𝑗 ∈ ℝ ) |
216 |
215
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → 𝑗 ∈ ℝ ) |
217 |
214 216
|
lenltd |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → ( 𝑀 ≤ 𝑗 ↔ ¬ 𝑗 < 𝑀 ) ) |
218 |
213 217
|
mpbid |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) ∧ ¬ ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) → ¬ 𝑗 < 𝑀 ) |
219 |
197 218
|
condan |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) = 0 ) |
220 |
219
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) = ( 0 · ( 𝐴 ↑ 𝑗 ) ) ) |
221 |
128
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → 𝐴 ∈ ℂ ) |
222 |
201
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → 𝑗 ∈ ℕ0 ) |
223 |
221 222
|
expcld |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → ( 𝐴 ↑ 𝑗 ) ∈ ℂ ) |
224 |
223
|
mul02d |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → ( 0 · ( 𝐴 ↑ 𝑗 ) ) = 0 ) |
225 |
220 224
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) = 0 ) |
226 |
225
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) / ( 𝐴 ↑ 𝑀 ) ) = ( 0 / ( 𝐴 ↑ 𝑀 ) ) ) |
227 |
128 2 36
|
expne0d |
⊢ ( 𝜑 → ( 𝐴 ↑ 𝑀 ) ≠ 0 ) |
228 |
166 227
|
div0d |
⊢ ( 𝜑 → ( 0 / ( 𝐴 ↑ 𝑀 ) ) = 0 ) |
229 |
228
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → ( 0 / ( 𝐴 ↑ 𝑀 ) ) = 0 ) |
230 |
226 229
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... ( deg ‘ 𝐺 ) ) ∖ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ) ) → ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) / ( 𝐴 ↑ 𝑀 ) ) = 0 ) |
231 |
|
fzfid |
⊢ ( 𝜑 → ( 0 ... ( deg ‘ 𝐺 ) ) ∈ Fin ) |
232 |
177 179 230 231
|
fsumss |
⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... ( deg ‘ 𝐺 ) ) ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) / ( 𝐴 ↑ 𝑀 ) ) = Σ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) / ( 𝐴 ↑ 𝑀 ) ) ) |
233 |
135 174 232
|
3eqtrd |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝐴 ↑ 𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) / ( 𝐴 ↑ 𝑀 ) ) ) |
234 |
89 56
|
syldan |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ∈ ℤ ) |
235 |
7
|
fvmpt2 |
⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ∈ ℤ ) → ( 𝐼 ‘ 𝑘 ) = ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ) |
236 |
89 234 235
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( 𝐼 ‘ 𝑘 ) = ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ) |
237 |
236
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑧 = 𝐴 ) ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( 𝐼 ‘ 𝑘 ) = ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) ) |
238 |
|
oveq1 |
⊢ ( 𝑧 = 𝐴 → ( 𝑧 ↑ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) ) |
239 |
238
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑧 = 𝐴 ) ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( 𝑧 ↑ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) ) |
240 |
237 239
|
oveq12d |
⊢ ( ( ( 𝜑 ∧ 𝑧 = 𝐴 ) ∧ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ) → ( ( 𝐼 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝐴 ↑ 𝑘 ) ) ) |
241 |
240
|
sumeq2dv |
⊢ ( ( 𝜑 ∧ 𝑧 = 𝐴 ) → Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( 𝐼 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝐴 ↑ 𝑘 ) ) ) |
242 |
|
fzfid |
⊢ ( 𝜑 → ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ∈ Fin ) |
243 |
242 131
|
fsumcl |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ ) |
244 |
9 241 128 243
|
fvmptd |
⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = Σ 𝑘 ∈ ( 0 ... ( ( deg ‘ 𝐺 ) − 𝑀 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ ( 𝑘 + 𝑀 ) ) · ( 𝐴 ↑ 𝑘 ) ) ) |
245 |
21 20
|
coeid2 |
⊢ ( ( 𝐺 ∈ ( Poly ‘ ℤ ) ∧ 𝐴 ∈ ℂ ) → ( 𝐺 ‘ 𝐴 ) = Σ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) ) |
246 |
3 128 245
|
syl2anc |
⊢ ( 𝜑 → ( 𝐺 ‘ 𝐴 ) = Σ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) ) |
247 |
246
|
oveq1d |
⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝐴 ) / ( 𝐴 ↑ 𝑀 ) ) = ( Σ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) / ( 𝐴 ↑ 𝑀 ) ) ) |
248 |
86
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ) → ( coeff ‘ 𝐺 ) : ℕ0 ⟶ ℂ ) |
249 |
200
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ) → 𝑗 ∈ ℕ0 ) |
250 |
248 249
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ) → ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) ∈ ℂ ) |
251 |
128
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ) → 𝐴 ∈ ℂ ) |
252 |
251 249
|
expcld |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ) → ( 𝐴 ↑ 𝑗 ) ∈ ℂ ) |
253 |
250 252
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ) → ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) ∈ ℂ ) |
254 |
231 166 253 227
|
fsumdivc |
⊢ ( 𝜑 → ( Σ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) / ( 𝐴 ↑ 𝑀 ) ) = Σ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) / ( 𝐴 ↑ 𝑀 ) ) ) |
255 |
247 254
|
eqtrd |
⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝐴 ) / ( 𝐴 ↑ 𝑀 ) ) = Σ 𝑗 ∈ ( 0 ... ( deg ‘ 𝐺 ) ) ( ( ( ( coeff ‘ 𝐺 ) ‘ 𝑗 ) · ( 𝐴 ↑ 𝑗 ) ) / ( 𝐴 ↑ 𝑀 ) ) ) |
256 |
233 244 255
|
3eqtr4d |
⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = ( ( 𝐺 ‘ 𝐴 ) / ( 𝐴 ↑ 𝑀 ) ) ) |
257 |
5
|
oveq1d |
⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝐴 ) / ( 𝐴 ↑ 𝑀 ) ) = ( 0 / ( 𝐴 ↑ 𝑀 ) ) ) |
258 |
256 257 228
|
3eqtrd |
⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 0 ) |
259 |
125 258
|
jca |
⊢ ( 𝜑 → ( ( ( coeff ‘ 𝐹 ) ‘ 0 ) ≠ 0 ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ) |
260 |
|
fveq2 |
⊢ ( 𝑓 = 𝐹 → ( coeff ‘ 𝑓 ) = ( coeff ‘ 𝐹 ) ) |
261 |
260
|
fveq1d |
⊢ ( 𝑓 = 𝐹 → ( ( coeff ‘ 𝑓 ) ‘ 0 ) = ( ( coeff ‘ 𝐹 ) ‘ 0 ) ) |
262 |
261
|
neeq1d |
⊢ ( 𝑓 = 𝐹 → ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ↔ ( ( coeff ‘ 𝐹 ) ‘ 0 ) ≠ 0 ) ) |
263 |
|
fveq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ) |
264 |
263
|
eqeq1d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝐴 ) = 0 ↔ ( 𝐹 ‘ 𝐴 ) = 0 ) ) |
265 |
262 264
|
anbi12d |
⊢ ( 𝑓 = 𝐹 → ( ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ↔ ( ( ( coeff ‘ 𝐹 ) ‘ 0 ) ≠ 0 ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ) ) |
266 |
265
|
rspcev |
⊢ ( ( 𝐹 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝐹 ) ‘ 0 ) ≠ 0 ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ) → ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) |
267 |
60 259 266
|
syl2anc |
⊢ ( 𝜑 → ∃ 𝑓 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) ≠ 0 ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) |