Metamath Proof Explorer

Theorem aareccl

Description: The reciprocal of an algebraic number is algebraic. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Assertion aareccl ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ 𝔸 )

Proof

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 ffvelcdmd ⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 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 eqtrid ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 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 ffvelcdm ⊢ ( ( ( 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 addlidd ⊢ ( ( ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ≠ 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 / 𝐴 ) ∈ 𝔸 )