| Step |
Hyp |
Ref |
Expression |
| 1 |
|
elaa |
⊢ ( 𝐴 ∈ 𝔸 ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) ) |
| 2 |
1
|
simprbi |
⊢ ( 𝐴 ∈ 𝔸 → ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) |
| 3 |
2
|
adantr |
⊢ ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) → ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) |
| 4 |
|
aacn |
⊢ ( 𝐴 ∈ 𝔸 → 𝐴 ∈ ℂ ) |
| 5 |
|
reccl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ ℂ ) |
| 6 |
4 5
|
sylan |
⊢ ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ ℂ ) |
| 7 |
6
|
adantr |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 1 / 𝐴 ) ∈ ℂ ) |
| 8 |
|
zsscn |
⊢ ℤ ⊆ ℂ |
| 9 |
8
|
a1i |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ℤ ⊆ ℂ ) |
| 10 |
|
simprl |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ) |
| 11 |
|
eldifsn |
⊢ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ↔ ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ 𝑓 ≠ 0𝑝 ) ) |
| 12 |
10 11
|
sylib |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ 𝑓 ≠ 0𝑝 ) ) |
| 13 |
12
|
simpld |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → 𝑓 ∈ ( Poly ‘ ℤ ) ) |
| 14 |
|
dgrcl |
⊢ ( 𝑓 ∈ ( Poly ‘ ℤ ) → ( deg ‘ 𝑓 ) ∈ ℕ0 ) |
| 15 |
13 14
|
syl |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( deg ‘ 𝑓 ) ∈ ℕ0 ) |
| 16 |
13
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → 𝑓 ∈ ( Poly ‘ ℤ ) ) |
| 17 |
|
0z |
⊢ 0 ∈ ℤ |
| 18 |
|
eqid |
⊢ ( coeff ‘ 𝑓 ) = ( coeff ‘ 𝑓 ) |
| 19 |
18
|
coef2 |
⊢ ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ 0 ∈ ℤ ) → ( coeff ‘ 𝑓 ) : ℕ0 ⟶ ℤ ) |
| 20 |
16 17 19
|
sylancl |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( coeff ‘ 𝑓 ) : ℕ0 ⟶ ℤ ) |
| 21 |
|
fznn0sub |
⊢ ( 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) → ( ( deg ‘ 𝑓 ) − 𝑘 ) ∈ ℕ0 ) |
| 22 |
21
|
adantl |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( ( deg ‘ 𝑓 ) − 𝑘 ) ∈ ℕ0 ) |
| 23 |
20 22
|
ffvelrnd |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) ∈ ℤ ) |
| 24 |
9 15 23
|
elplyd |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ ℤ ) ) |
| 25 |
|
0cn |
⊢ 0 ∈ ℂ |
| 26 |
|
eqid |
⊢ ( coeff ‘ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ) = ( coeff ‘ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
| 27 |
26
|
coefv0 |
⊢ ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ ℤ ) → ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ 0 ) = ( ( coeff ‘ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ‘ 0 ) ) |
| 28 |
24 27
|
syl |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ 0 ) = ( ( coeff ‘ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ‘ 0 ) ) |
| 29 |
23
|
zcnd |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) ∈ ℂ ) |
| 30 |
|
eqidd |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ) |
| 31 |
24 15 29 30
|
coeeq2 |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( coeff ‘ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ ( deg ‘ 𝑓 ) , ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) , 0 ) ) ) |
| 32 |
31
|
fveq1d |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( ( coeff ‘ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ‘ 0 ) = ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ ( deg ‘ 𝑓 ) , ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) , 0 ) ) ‘ 0 ) ) |
| 33 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
| 34 |
|
breq1 |
⊢ ( 𝑘 = 0 → ( 𝑘 ≤ ( deg ‘ 𝑓 ) ↔ 0 ≤ ( deg ‘ 𝑓 ) ) ) |
| 35 |
|
oveq2 |
⊢ ( 𝑘 = 0 → ( ( deg ‘ 𝑓 ) − 𝑘 ) = ( ( deg ‘ 𝑓 ) − 0 ) ) |
| 36 |
35
|
fveq2d |
⊢ ( 𝑘 = 0 → ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) = ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 0 ) ) ) |
| 37 |
34 36
|
ifbieq1d |
⊢ ( 𝑘 = 0 → if ( 𝑘 ≤ ( deg ‘ 𝑓 ) , ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) , 0 ) = if ( 0 ≤ ( deg ‘ 𝑓 ) , ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 0 ) ) , 0 ) ) |
| 38 |
|
eqid |
⊢ ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ ( deg ‘ 𝑓 ) , ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) , 0 ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ ( deg ‘ 𝑓 ) , ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) , 0 ) ) |
| 39 |
|
fvex |
⊢ ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 0 ) ) ∈ V |
| 40 |
|
c0ex |
⊢ 0 ∈ V |
| 41 |
39 40
|
ifex |
⊢ if ( 0 ≤ ( deg ‘ 𝑓 ) , ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 0 ) ) , 0 ) ∈ V |
| 42 |
37 38 41
|
fvmpt |
⊢ ( 0 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ ( deg ‘ 𝑓 ) , ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) , 0 ) ) ‘ 0 ) = if ( 0 ≤ ( deg ‘ 𝑓 ) , ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 0 ) ) , 0 ) ) |
| 43 |
33 42
|
ax-mp |
⊢ ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ ( deg ‘ 𝑓 ) , ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) , 0 ) ) ‘ 0 ) = if ( 0 ≤ ( deg ‘ 𝑓 ) , ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 0 ) ) , 0 ) |
| 44 |
15
|
nn0ge0d |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → 0 ≤ ( deg ‘ 𝑓 ) ) |
| 45 |
44
|
iftrued |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → if ( 0 ≤ ( deg ‘ 𝑓 ) , ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 0 ) ) , 0 ) = ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 0 ) ) ) |
| 46 |
15
|
nn0cnd |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( deg ‘ 𝑓 ) ∈ ℂ ) |
| 47 |
46
|
subid1d |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( ( deg ‘ 𝑓 ) − 0 ) = ( deg ‘ 𝑓 ) ) |
| 48 |
47
|
fveq2d |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 0 ) ) = ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) |
| 49 |
45 48
|
eqtrd |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → if ( 0 ≤ ( deg ‘ 𝑓 ) , ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 0 ) ) , 0 ) = ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) |
| 50 |
43 49
|
syl5eq |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ≤ ( deg ‘ 𝑓 ) , ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) , 0 ) ) ‘ 0 ) = ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) |
| 51 |
28 32 50
|
3eqtrd |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ 0 ) = ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) |
| 52 |
12
|
simprd |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → 𝑓 ≠ 0𝑝 ) |
| 53 |
|
eqid |
⊢ ( deg ‘ 𝑓 ) = ( deg ‘ 𝑓 ) |
| 54 |
53 18
|
dgreq0 |
⊢ ( 𝑓 ∈ ( Poly ‘ ℤ ) → ( 𝑓 = 0𝑝 ↔ ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) = 0 ) ) |
| 55 |
13 54
|
syl |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 𝑓 = 0𝑝 ↔ ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) = 0 ) ) |
| 56 |
55
|
necon3bid |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 𝑓 ≠ 0𝑝 ↔ ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ≠ 0 ) ) |
| 57 |
52 56
|
mpbid |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ≠ 0 ) |
| 58 |
51 57
|
eqnetrd |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ 0 ) ≠ 0 ) |
| 59 |
|
ne0p |
⊢ ( ( 0 ∈ ℂ ∧ ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ 0 ) ≠ 0 ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ≠ 0𝑝 ) |
| 60 |
25 58 59
|
sylancr |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ≠ 0𝑝 ) |
| 61 |
|
eldifsn |
⊢ ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ↔ ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ ℤ ) ∧ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ≠ 0𝑝 ) ) |
| 62 |
24 60 61
|
sylanbrc |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ) |
| 63 |
|
oveq1 |
⊢ ( 𝑧 = ( 1 / 𝐴 ) → ( 𝑧 ↑ 𝑘 ) = ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) |
| 64 |
63
|
oveq2d |
⊢ ( 𝑧 = ( 1 / 𝐴 ) → ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) ) |
| 65 |
64
|
sumeq2sdv |
⊢ ( 𝑧 = ( 1 / 𝐴 ) → Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) ) |
| 66 |
|
eqid |
⊢ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) |
| 67 |
|
sumex |
⊢ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) ∈ V |
| 68 |
65 66 67
|
fvmpt |
⊢ ( ( 1 / 𝐴 ) ∈ ℂ → ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ ( 1 / 𝐴 ) ) = Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) ) |
| 69 |
7 68
|
syl |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ ( 1 / 𝐴 ) ) = Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) ) |
| 70 |
18
|
coef3 |
⊢ ( 𝑓 ∈ ( Poly ‘ ℤ ) → ( coeff ‘ 𝑓 ) : ℕ0 ⟶ ℂ ) |
| 71 |
13 70
|
syl |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( coeff ‘ 𝑓 ) : ℕ0 ⟶ ℂ ) |
| 72 |
|
elfznn0 |
⊢ ( 𝑛 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) → 𝑛 ∈ ℕ0 ) |
| 73 |
|
ffvelrn |
⊢ ( ( ( coeff ‘ 𝑓 ) : ℕ0 ⟶ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( ( coeff ‘ 𝑓 ) ‘ 𝑛 ) ∈ ℂ ) |
| 74 |
71 72 73
|
syl2an |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑛 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( ( coeff ‘ 𝑓 ) ‘ 𝑛 ) ∈ ℂ ) |
| 75 |
4
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → 𝐴 ∈ ℂ ) |
| 76 |
|
expcl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑛 ) ∈ ℂ ) |
| 77 |
75 72 76
|
syl2an |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑛 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( 𝐴 ↑ 𝑛 ) ∈ ℂ ) |
| 78 |
74 77
|
mulcld |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑛 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( ( ( coeff ‘ 𝑓 ) ‘ 𝑛 ) · ( 𝐴 ↑ 𝑛 ) ) ∈ ℂ ) |
| 79 |
75 15
|
expcld |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ∈ ℂ ) |
| 80 |
79
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑛 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ∈ ℂ ) |
| 81 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → 𝐴 ≠ 0 ) |
| 82 |
15
|
nn0zd |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( deg ‘ 𝑓 ) ∈ ℤ ) |
| 83 |
75 81 82
|
expne0d |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ≠ 0 ) |
| 84 |
83
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑛 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ≠ 0 ) |
| 85 |
78 80 84
|
divcld |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑛 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( ( ( ( coeff ‘ 𝑓 ) ‘ 𝑛 ) · ( 𝐴 ↑ 𝑛 ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) ∈ ℂ ) |
| 86 |
|
fveq2 |
⊢ ( 𝑛 = ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) → ( ( coeff ‘ 𝑓 ) ‘ 𝑛 ) = ( ( coeff ‘ 𝑓 ) ‘ ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) ) ) |
| 87 |
|
oveq2 |
⊢ ( 𝑛 = ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) → ( 𝐴 ↑ 𝑛 ) = ( 𝐴 ↑ ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) ) ) |
| 88 |
86 87
|
oveq12d |
⊢ ( 𝑛 = ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) → ( ( ( coeff ‘ 𝑓 ) ‘ 𝑛 ) · ( 𝐴 ↑ 𝑛 ) ) = ( ( ( coeff ‘ 𝑓 ) ‘ ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) ) · ( 𝐴 ↑ ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) ) ) ) |
| 89 |
88
|
oveq1d |
⊢ ( 𝑛 = ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) → ( ( ( ( coeff ‘ 𝑓 ) ‘ 𝑛 ) · ( 𝐴 ↑ 𝑛 ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) = ( ( ( ( coeff ‘ 𝑓 ) ‘ ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) ) · ( 𝐴 ↑ ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) ) |
| 90 |
85 89
|
fsumrev2 |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → Σ 𝑛 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( ( coeff ‘ 𝑓 ) ‘ 𝑛 ) · ( 𝐴 ↑ 𝑛 ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( ( coeff ‘ 𝑓 ) ‘ ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) ) · ( 𝐴 ↑ ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) ) |
| 91 |
46
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( deg ‘ 𝑓 ) ∈ ℂ ) |
| 92 |
91
|
addid2d |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( 0 + ( deg ‘ 𝑓 ) ) = ( deg ‘ 𝑓 ) ) |
| 93 |
92
|
oveq1d |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) = ( ( deg ‘ 𝑓 ) − 𝑘 ) ) |
| 94 |
93
|
fveq2d |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( ( coeff ‘ 𝑓 ) ‘ ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) ) = ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) ) |
| 95 |
93
|
oveq2d |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( 𝐴 ↑ ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) ) = ( 𝐴 ↑ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) ) |
| 96 |
75
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → 𝐴 ∈ ℂ ) |
| 97 |
81
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → 𝐴 ≠ 0 ) |
| 98 |
|
elfznn0 |
⊢ ( 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) → 𝑘 ∈ ℕ0 ) |
| 99 |
98
|
adantl |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → 𝑘 ∈ ℕ0 ) |
| 100 |
99
|
nn0zd |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → 𝑘 ∈ ℤ ) |
| 101 |
82
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( deg ‘ 𝑓 ) ∈ ℤ ) |
| 102 |
96 97 100 101
|
expsubd |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( 𝐴 ↑ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) = ( ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) / ( 𝐴 ↑ 𝑘 ) ) ) |
| 103 |
95 102
|
eqtrd |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( 𝐴 ↑ ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) ) = ( ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) / ( 𝐴 ↑ 𝑘 ) ) ) |
| 104 |
94 103
|
oveq12d |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( ( ( coeff ‘ 𝑓 ) ‘ ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) ) · ( 𝐴 ↑ ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) ) ) = ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) / ( 𝐴 ↑ 𝑘 ) ) ) ) |
| 105 |
104
|
oveq1d |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( ( ( ( coeff ‘ 𝑓 ) ‘ ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) ) · ( 𝐴 ↑ ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) = ( ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) / ( 𝐴 ↑ 𝑘 ) ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) ) |
| 106 |
79
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ∈ ℂ ) |
| 107 |
|
expcl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ ) |
| 108 |
75 98 107
|
syl2an |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ ) |
| 109 |
96 97 100
|
expne0d |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( 𝐴 ↑ 𝑘 ) ≠ 0 ) |
| 110 |
106 108 109
|
divcld |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) / ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ ) |
| 111 |
83
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ≠ 0 ) |
| 112 |
29 110 106 111
|
divassd |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) / ( 𝐴 ↑ 𝑘 ) ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) = ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( ( ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) / ( 𝐴 ↑ 𝑘 ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) ) ) |
| 113 |
106 111
|
dividd |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) = 1 ) |
| 114 |
113
|
oveq1d |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( ( ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) / ( 𝐴 ↑ 𝑘 ) ) = ( 1 / ( 𝐴 ↑ 𝑘 ) ) ) |
| 115 |
106 108 106 109 111
|
divdiv32d |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( ( ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) / ( 𝐴 ↑ 𝑘 ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) = ( ( ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) / ( 𝐴 ↑ 𝑘 ) ) ) |
| 116 |
96 97 100
|
exprecd |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( ( 1 / 𝐴 ) ↑ 𝑘 ) = ( 1 / ( 𝐴 ↑ 𝑘 ) ) ) |
| 117 |
114 115 116
|
3eqtr4d |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( ( ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) / ( 𝐴 ↑ 𝑘 ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) = ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) |
| 118 |
117
|
oveq2d |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( ( ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) / ( 𝐴 ↑ 𝑘 ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) ) = ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) ) |
| 119 |
105 112 118
|
3eqtrd |
⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) ∧ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ) → ( ( ( ( coeff ‘ 𝑓 ) ‘ ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) ) · ( 𝐴 ↑ ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) = ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) ) |
| 120 |
119
|
sumeq2dv |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( ( coeff ‘ 𝑓 ) ‘ ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) ) · ( 𝐴 ↑ ( ( 0 + ( deg ‘ 𝑓 ) ) − 𝑘 ) ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) ) |
| 121 |
90 120
|
eqtrd |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → Σ 𝑛 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( ( coeff ‘ 𝑓 ) ‘ 𝑛 ) · ( 𝐴 ↑ 𝑛 ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) ) |
| 122 |
18 53
|
coeid2 |
⊢ ( ( 𝑓 ∈ ( Poly ‘ ℤ ) ∧ 𝐴 ∈ ℂ ) → ( 𝑓 ‘ 𝐴 ) = Σ 𝑛 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ 𝑛 ) · ( 𝐴 ↑ 𝑛 ) ) ) |
| 123 |
13 75 122
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 𝑓 ‘ 𝐴 ) = Σ 𝑛 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ 𝑛 ) · ( 𝐴 ↑ 𝑛 ) ) ) |
| 124 |
|
simprr |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 𝑓 ‘ 𝐴 ) = 0 ) |
| 125 |
123 124
|
eqtr3d |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → Σ 𝑛 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ 𝑛 ) · ( 𝐴 ↑ 𝑛 ) ) = 0 ) |
| 126 |
125
|
oveq1d |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( Σ 𝑛 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ 𝑛 ) · ( 𝐴 ↑ 𝑛 ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) = ( 0 / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) ) |
| 127 |
|
fzfid |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 0 ... ( deg ‘ 𝑓 ) ) ∈ Fin ) |
| 128 |
127 79 78 83
|
fsumdivc |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( Σ 𝑛 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ 𝑛 ) · ( 𝐴 ↑ 𝑛 ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) = Σ 𝑛 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( ( coeff ‘ 𝑓 ) ‘ 𝑛 ) · ( 𝐴 ↑ 𝑛 ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) ) |
| 129 |
79 83
|
div0d |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 0 / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) = 0 ) |
| 130 |
126 128 129
|
3eqtr3d |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → Σ 𝑛 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( ( coeff ‘ 𝑓 ) ‘ 𝑛 ) · ( 𝐴 ↑ 𝑛 ) ) / ( 𝐴 ↑ ( deg ‘ 𝑓 ) ) ) = 0 ) |
| 131 |
69 121 130
|
3eqtr2d |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ ( 1 / 𝐴 ) ) = 0 ) |
| 132 |
|
fveq1 |
⊢ ( 𝑔 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) → ( 𝑔 ‘ ( 1 / 𝐴 ) ) = ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ ( 1 / 𝐴 ) ) ) |
| 133 |
132
|
eqeq1d |
⊢ ( 𝑔 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) → ( ( 𝑔 ‘ ( 1 / 𝐴 ) ) = 0 ↔ ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ ( 1 / 𝐴 ) ) = 0 ) ) |
| 134 |
133
|
rspcev |
⊢ ( ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ ( 1 / 𝐴 ) ) = 0 ) → ∃ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑔 ‘ ( 1 / 𝐴 ) ) = 0 ) |
| 135 |
62 131 134
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ∃ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑔 ‘ ( 1 / 𝐴 ) ) = 0 ) |
| 136 |
|
elaa |
⊢ ( ( 1 / 𝐴 ) ∈ 𝔸 ↔ ( ( 1 / 𝐴 ) ∈ ℂ ∧ ∃ 𝑔 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑔 ‘ ( 1 / 𝐴 ) ) = 0 ) ) |
| 137 |
7 135 136
|
sylanbrc |
⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) ∧ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) → ( 1 / 𝐴 ) ∈ 𝔸 ) |
| 138 |
3 137
|
rexlimddv |
⊢ ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ 𝔸 ) |