Metamath Proof Explorer

Theorem elqaalem3

Description: Lemma for elqaa . (Contributed by Mario Carneiro, 23-Jul-2014) (Revised by AV, 3-Oct-2020)

Ref Expression
Hypotheses elqaa.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
elqaa.2 ⊢ ( 𝜑 → 𝐹 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) )
elqaa.3 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 0 )
elqaa.4 ⊢ 𝐵 = ( coeff ‘ 𝐹 )
elqaa.5 ⊢ 𝑁 = ( 𝑘 ∈ ℕ0 ↦ inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑘 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) )
elqaa.6 ⊢ 𝑅 = ( seq 0 ( · , 𝑁 ) ‘ ( deg ‘ 𝐹 ) )
Assertion elqaalem3 ( 𝜑 → 𝐴 ∈ 𝔸 )

Proof

Step Hyp Ref Expression
1 elqaa.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 elqaa.2 ⊢ ( 𝜑 → 𝐹 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) )
3 elqaa.3 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 0 )
4 elqaa.4 ⊢ 𝐵 = ( coeff ‘ 𝐹 )
5 elqaa.5 ⊢ 𝑁 = ( 𝑘 ∈ ℕ0 ↦ inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑘 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) )
6 elqaa.6 ⊢ 𝑅 = ( seq 0 ( · , 𝑁 ) ‘ ( deg ‘ 𝐹 ) )
7 cnex ⊢ ℂ ∈ V
8 7 a1i ⊢ ( 𝜑 → ℂ ∈ V )
9 6 fvexi ⊢ 𝑅 ∈ V
10 9 a1i ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑅 ∈ V )
11 fvexd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 𝐹 ‘ 𝑧 ) ∈ V )
12 fconstmpt ⊢ ( ℂ × { 𝑅 } ) = ( 𝑧 ∈ ℂ ↦ 𝑅 )
13 12 a1i ⊢ ( 𝜑 → ( ℂ × { 𝑅 } ) = ( 𝑧 ∈ ℂ ↦ 𝑅 ) )
14 2 eldifad ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℚ ) )
15 plyf ⊢ ( 𝐹 ∈ ( Poly ‘ ℚ ) → 𝐹 : ℂ ⟶ ℂ )
16 14 15 syl ⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ )
17 16 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ 𝑧 ) ) )
18 8 10 11 13 17 offval2 ⊢ ( 𝜑 → ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) = ( 𝑧 ∈ ℂ ↦ ( 𝑅 · ( 𝐹 ‘ 𝑧 ) ) ) )
19 fzfid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 0 ... ( deg ‘ 𝐹 ) ) ∈ Fin )
20 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
21 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
22 ssrab2 ⊢ { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } ⊆ ℕ
23 fveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑚 ) )
24 23 oveq1d ⊢ ( 𝑘 = 𝑚 → ( ( 𝐵 ‘ 𝑘 ) · 𝑛 ) = ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) )
25 24 eleq1d ⊢ ( 𝑘 = 𝑚 → ( ( ( 𝐵 ‘ 𝑘 ) · 𝑛 ) ∈ ℤ ↔ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ ) )
26 25 rabbidv ⊢ ( 𝑘 = 𝑚 → { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑘 ) · 𝑛 ) ∈ ℤ } = { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } )
27 26 infeq1d ⊢ ( 𝑘 = 𝑚 → inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑘 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) = inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) )
28 ltso ⊢ < Or ℝ
29 28 infex ⊢ inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) ∈ V
30 27 5 29 fvmpt ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑁 ‘ 𝑚 ) = inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) )
31 30 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑁 ‘ 𝑚 ) = inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) )
32 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
33 22 32 sseqtri ⊢ { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } ⊆ ( ℤ≥ ‘ 1 )
34 0z ⊢ 0 ∈ ℤ
35 zq ⊢ ( 0 ∈ ℤ → 0 ∈ ℚ )
36 34 35 ax-mp ⊢ 0 ∈ ℚ
37 4 coef2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℚ ) ∧ 0 ∈ ℚ ) → 𝐵 : ℕ0 ⟶ ℚ )
38 14 36 37 sylancl ⊢ ( 𝜑 → 𝐵 : ℕ0 ⟶ ℚ )
39 38 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝐵 ‘ 𝑚 ) ∈ ℚ )
40 qmulz ⊢ ( ( 𝐵 ‘ 𝑚 ) ∈ ℚ → ∃ 𝑛 ∈ ℕ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ )
41 39 40 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ∃ 𝑛 ∈ ℕ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ )
42 rabn0 ⊢ ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } ≠ ∅ ↔ ∃ 𝑛 ∈ ℕ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ )
43 41 42 sylibr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } ≠ ∅ )
44 infssuzcl ⊢ ( ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } ⊆ ( ℤ≥ ‘ 1 ) ∧ { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } ≠ ∅ ) → inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) ∈ { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } )
45 33 43 44 sylancr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → inf ( { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) ∈ { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } )
46 31 45 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑁 ‘ 𝑚 ) ∈ { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } )
47 22 46 sselid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑁 ‘ 𝑚 ) ∈ ℕ )
48 nnmulcl ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝑚 · 𝑘 ) ∈ ℕ )
49 48 adantl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( 𝑚 · 𝑘 ) ∈ ℕ )
50 20 21 47 49 seqf ⊢ ( 𝜑 → seq 0 ( · , 𝑁 ) : ℕ0 ⟶ ℕ )
51 dgrcl ⊢ ( 𝐹 ∈ ( Poly ‘ ℚ ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
52 14 51 syl ⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ∈ ℕ0 )
53 50 52 ffvelcdmd ⊢ ( 𝜑 → ( seq 0 ( · , 𝑁 ) ‘ ( deg ‘ 𝐹 ) ) ∈ ℕ )
54 6 53 eqeltrid ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
55 54 nncnd ⊢ ( 𝜑 → 𝑅 ∈ ℂ )
56 55 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑅 ∈ ℂ )
57 elfznn0 ⊢ ( 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) → 𝑚 ∈ ℕ0 )
58 4 coef3 ⊢ ( 𝐹 ∈ ( Poly ‘ ℚ ) → 𝐵 : ℕ0 ⟶ ℂ )
59 14 58 syl ⊢ ( 𝜑 → 𝐵 : ℕ0 ⟶ ℂ )
60 59 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝐵 : ℕ0 ⟶ ℂ )
61 60 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝐵 ‘ 𝑚 ) ∈ ℂ )
62 expcl ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑚 ∈ ℕ0 ) → ( 𝑧 ↑ 𝑚 ) ∈ ℂ )
63 62 adantll ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝑧 ↑ 𝑚 ) ∈ ℂ )
64 61 63 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝐵 ‘ 𝑚 ) · ( 𝑧 ↑ 𝑚 ) ) ∈ ℂ )
65 57 64 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( 𝐵 ‘ 𝑚 ) · ( 𝑧 ↑ 𝑚 ) ) ∈ ℂ )
66 19 56 65 fsummulc2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 𝑅 · Σ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( 𝐵 ‘ 𝑚 ) · ( 𝑧 ↑ 𝑚 ) ) ) = Σ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( 𝑅 · ( ( 𝐵 ‘ 𝑚 ) · ( 𝑧 ↑ 𝑚 ) ) ) )
67 eqid ⊢ ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 )
68 4 67 coeid2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℚ ) ∧ 𝑧 ∈ ℂ ) → ( 𝐹 ‘ 𝑧 ) = Σ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( 𝐵 ‘ 𝑚 ) · ( 𝑧 ↑ 𝑚 ) ) )
69 14 68 sylan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 𝐹 ‘ 𝑧 ) = Σ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( 𝐵 ‘ 𝑚 ) · ( 𝑧 ↑ 𝑚 ) ) )
70 69 oveq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 𝑅 · ( 𝐹 ‘ 𝑧 ) ) = ( 𝑅 · Σ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( 𝐵 ‘ 𝑚 ) · ( 𝑧 ↑ 𝑚 ) ) ) )
71 56 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑚 ∈ ℕ0 ) → 𝑅 ∈ ℂ )
72 71 61 63 mulassd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑅 · ( 𝐵 ‘ 𝑚 ) ) · ( 𝑧 ↑ 𝑚 ) ) = ( 𝑅 · ( ( 𝐵 ‘ 𝑚 ) · ( 𝑧 ↑ 𝑚 ) ) ) )
73 57 72 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( 𝑅 · ( 𝐵 ‘ 𝑚 ) ) · ( 𝑧 ↑ 𝑚 ) ) = ( 𝑅 · ( ( 𝐵 ‘ 𝑚 ) · ( 𝑧 ↑ 𝑚 ) ) ) )
74 73 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( 𝑅 · ( 𝐵 ‘ 𝑚 ) ) · ( 𝑧 ↑ 𝑚 ) ) = Σ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( 𝑅 · ( ( 𝐵 ‘ 𝑚 ) · ( 𝑧 ↑ 𝑚 ) ) ) )
75 66 70 74 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 𝑅 · ( 𝐹 ‘ 𝑧 ) ) = Σ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( 𝑅 · ( 𝐵 ‘ 𝑚 ) ) · ( 𝑧 ↑ 𝑚 ) ) )
76 75 mpteq2dva ⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ ( 𝑅 · ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( 𝑅 · ( 𝐵 ‘ 𝑚 ) ) · ( 𝑧 ↑ 𝑚 ) ) ) )
77 18 76 eqtrd ⊢ ( 𝜑 → ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( 𝑅 · ( 𝐵 ‘ 𝑚 ) ) · ( 𝑧 ↑ 𝑚 ) ) ) )
78 zsscn ⊢ ℤ ⊆ ℂ
79 78 a1i ⊢ ( 𝜑 → ℤ ⊆ ℂ )
80 55 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝑅 ∈ ℂ )
81 47 nncnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑁 ‘ 𝑚 ) ∈ ℂ )
82 47 nnne0d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑁 ‘ 𝑚 ) ≠ 0 )
83 80 81 82 divcan2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑁 ‘ 𝑚 ) · ( 𝑅 / ( 𝑁 ‘ 𝑚 ) ) ) = 𝑅 )
84 83 oveq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝐵 ‘ 𝑚 ) · ( ( 𝑁 ‘ 𝑚 ) · ( 𝑅 / ( 𝑁 ‘ 𝑚 ) ) ) ) = ( ( 𝐵 ‘ 𝑚 ) · 𝑅 ) )
85 59 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝐵 ‘ 𝑚 ) ∈ ℂ )
86 80 81 82 divcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑅 / ( 𝑁 ‘ 𝑚 ) ) ∈ ℂ )
87 85 81 86 mulassd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( ( 𝐵 ‘ 𝑚 ) · ( 𝑁 ‘ 𝑚 ) ) · ( 𝑅 / ( 𝑁 ‘ 𝑚 ) ) ) = ( ( 𝐵 ‘ 𝑚 ) · ( ( 𝑁 ‘ 𝑚 ) · ( 𝑅 / ( 𝑁 ‘ 𝑚 ) ) ) ) )
88 80 85 mulcomd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑅 · ( 𝐵 ‘ 𝑚 ) ) = ( ( 𝐵 ‘ 𝑚 ) · 𝑅 ) )
89 84 87 88 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑅 · ( 𝐵 ‘ 𝑚 ) ) = ( ( ( 𝐵 ‘ 𝑚 ) · ( 𝑁 ‘ 𝑚 ) ) · ( 𝑅 / ( 𝑁 ‘ 𝑚 ) ) ) )
90 57 89 sylan2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑅 · ( 𝐵 ‘ 𝑚 ) ) = ( ( ( 𝐵 ‘ 𝑚 ) · ( 𝑁 ‘ 𝑚 ) ) · ( 𝑅 / ( 𝑁 ‘ 𝑚 ) ) ) )
91 oveq2 ⊢ ( 𝑛 = ( 𝑁 ‘ 𝑚 ) → ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) = ( ( 𝐵 ‘ 𝑚 ) · ( 𝑁 ‘ 𝑚 ) ) )
92 91 eleq1d ⊢ ( 𝑛 = ( 𝑁 ‘ 𝑚 ) → ( ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ ↔ ( ( 𝐵 ‘ 𝑚 ) · ( 𝑁 ‘ 𝑚 ) ) ∈ ℤ ) )
93 92 elrab ⊢ ( ( 𝑁 ‘ 𝑚 ) ∈ { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } ↔ ( ( 𝑁 ‘ 𝑚 ) ∈ ℕ ∧ ( ( 𝐵 ‘ 𝑚 ) · ( 𝑁 ‘ 𝑚 ) ) ∈ ℤ ) )
94 93 simprbi ⊢ ( ( 𝑁 ‘ 𝑚 ) ∈ { 𝑛 ∈ ℕ ∣ ( ( 𝐵 ‘ 𝑚 ) · 𝑛 ) ∈ ℤ } → ( ( 𝐵 ‘ 𝑚 ) · ( 𝑁 ‘ 𝑚 ) ) ∈ ℤ )
95 46 94 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝐵 ‘ 𝑚 ) · ( 𝑁 ‘ 𝑚 ) ) ∈ ℤ )
96 57 95 sylan2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( 𝐵 ‘ 𝑚 ) · ( 𝑁 ‘ 𝑚 ) ) ∈ ℤ )
97 eqid ⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( ( 𝑥 · 𝑦 ) mod ( 𝑁 ‘ 𝑚 ) ) ) = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( ( 𝑥 · 𝑦 ) mod ( 𝑁 ‘ 𝑚 ) ) )
98 1 2 3 4 5 6 97 elqaalem2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑅 mod ( 𝑁 ‘ 𝑚 ) ) = 0 )
99 54 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → 𝑅 ∈ ℕ )
100 57 47 sylan2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑁 ‘ 𝑚 ) ∈ ℕ )
101 nnre ⊢ ( 𝑅 ∈ ℕ → 𝑅 ∈ ℝ )
102 nnrp ⊢ ( ( 𝑁 ‘ 𝑚 ) ∈ ℕ → ( 𝑁 ‘ 𝑚 ) ∈ ℝ+ )
103 mod0 ⊢ ( ( 𝑅 ∈ ℝ ∧ ( 𝑁 ‘ 𝑚 ) ∈ ℝ+ ) → ( ( 𝑅 mod ( 𝑁 ‘ 𝑚 ) ) = 0 ↔ ( 𝑅 / ( 𝑁 ‘ 𝑚 ) ) ∈ ℤ ) )
104 101 102 103 syl2an ⊢ ( ( 𝑅 ∈ ℕ ∧ ( 𝑁 ‘ 𝑚 ) ∈ ℕ ) → ( ( 𝑅 mod ( 𝑁 ‘ 𝑚 ) ) = 0 ↔ ( 𝑅 / ( 𝑁 ‘ 𝑚 ) ) ∈ ℤ ) )
105 99 100 104 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( 𝑅 mod ( 𝑁 ‘ 𝑚 ) ) = 0 ↔ ( 𝑅 / ( 𝑁 ‘ 𝑚 ) ) ∈ ℤ ) )
106 98 105 mpbid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑅 / ( 𝑁 ‘ 𝑚 ) ) ∈ ℤ )
107 96 106 zmulcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( ( 𝐵 ‘ 𝑚 ) · ( 𝑁 ‘ 𝑚 ) ) · ( 𝑅 / ( 𝑁 ‘ 𝑚 ) ) ) ∈ ℤ )
108 90 107 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( 𝑅 · ( 𝐵 ‘ 𝑚 ) ) ∈ ℤ )
109 79 52 108 elplyd ⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑚 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( 𝑅 · ( 𝐵 ‘ 𝑚 ) ) · ( 𝑧 ↑ 𝑚 ) ) ) ∈ ( Poly ‘ ℤ ) )
110 77 109 eqeltrd ⊢ ( 𝜑 → ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) ∈ ( Poly ‘ ℤ ) )
111 eldifsn ⊢ ( 𝐹 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ↔ ( 𝐹 ∈ ( Poly ‘ ℚ ) ∧ 𝐹 ≠ 0𝑝 ) )
112 2 111 sylib ⊢ ( 𝜑 → ( 𝐹 ∈ ( Poly ‘ ℚ ) ∧ 𝐹 ≠ 0𝑝 ) )
113 112 simprd ⊢ ( 𝜑 → 𝐹 ≠ 0𝑝 )
114 oveq1 ⊢ ( ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) = 0𝑝 → ( ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) ∘f / ( ℂ × { 𝑅 } ) ) = ( 0𝑝 ∘f / ( ℂ × { 𝑅 } ) ) )
115 16 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
116 54 nnne0d ⊢ ( 𝜑 → 𝑅 ≠ 0 )
117 116 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑅 ≠ 0 )
118 115 56 117 divcan3d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( ( 𝑅 · ( 𝐹 ‘ 𝑧 ) ) / 𝑅 ) = ( 𝐹 ‘ 𝑧 ) )
119 118 mpteq2dva ⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ ( ( 𝑅 · ( 𝐹 ‘ 𝑧 ) ) / 𝑅 ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝐹 ‘ 𝑧 ) ) )
120 ovexd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 𝑅 · ( 𝐹 ‘ 𝑧 ) ) ∈ V )
121 8 120 10 18 13 offval2 ⊢ ( 𝜑 → ( ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) ∘f / ( ℂ × { 𝑅 } ) ) = ( 𝑧 ∈ ℂ ↦ ( ( 𝑅 · ( 𝐹 ‘ 𝑧 ) ) / 𝑅 ) ) )
122 119 121 17 3eqtr4d ⊢ ( 𝜑 → ( ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) ∘f / ( ℂ × { 𝑅 } ) ) = 𝐹 )
123 55 116 div0d ⊢ ( 𝜑 → ( 0 / 𝑅 ) = 0 )
124 123 mpteq2dv ⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ ( 0 / 𝑅 ) ) = ( 𝑧 ∈ ℂ ↦ 0 ) )
125 0cnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 0 ∈ ℂ )
126 df-0p ⊢ 0𝑝 = ( ℂ × { 0 } )
127 fconstmpt ⊢ ( ℂ × { 0 } ) = ( 𝑧 ∈ ℂ ↦ 0 )
128 126 127 eqtri ⊢ 0𝑝 = ( 𝑧 ∈ ℂ ↦ 0 )
129 128 a1i ⊢ ( 𝜑 → 0𝑝 = ( 𝑧 ∈ ℂ ↦ 0 ) )
130 8 125 10 129 13 offval2 ⊢ ( 𝜑 → ( 0𝑝 ∘f / ( ℂ × { 𝑅 } ) ) = ( 𝑧 ∈ ℂ ↦ ( 0 / 𝑅 ) ) )
131 124 130 129 3eqtr4d ⊢ ( 𝜑 → ( 0𝑝 ∘f / ( ℂ × { 𝑅 } ) ) = 0𝑝 )
132 122 131 eqeq12d ⊢ ( 𝜑 → ( ( ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) ∘f / ( ℂ × { 𝑅 } ) ) = ( 0𝑝 ∘f / ( ℂ × { 𝑅 } ) ) ↔ 𝐹 = 0𝑝 ) )
133 114 132 imbitrid ⊢ ( 𝜑 → ( ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) = 0𝑝 → 𝐹 = 0𝑝 ) )
134 133 necon3d ⊢ ( 𝜑 → ( 𝐹 ≠ 0𝑝 → ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) ≠ 0𝑝 ) )
135 113 134 mpd ⊢ ( 𝜑 → ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) ≠ 0𝑝 )
136 eldifsn ⊢ ( ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ↔ ( ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) ∈ ( Poly ‘ ℤ ) ∧ ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) ≠ 0𝑝 ) )
137 110 135 136 sylanbrc ⊢ ( 𝜑 → ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) )
138 9 fconst ⊢ ( ℂ × { 𝑅 } ) : ℂ ⟶ { 𝑅 }
139 ffn ⊢ ( ( ℂ × { 𝑅 } ) : ℂ ⟶ { 𝑅 } → ( ℂ × { 𝑅 } ) Fn ℂ )
140 138 139 mp1i ⊢ ( 𝜑 → ( ℂ × { 𝑅 } ) Fn ℂ )
141 16 ffnd ⊢ ( 𝜑 → 𝐹 Fn ℂ )
142 inidm ⊢ ( ℂ ∩ ℂ ) = ℂ
143 9 fvconst2 ⊢ ( 𝐴 ∈ ℂ → ( ( ℂ × { 𝑅 } ) ‘ 𝐴 ) = 𝑅 )
144 143 adantl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) → ( ( ℂ × { 𝑅 } ) ‘ 𝐴 ) = 𝑅 )
145 3 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) → ( 𝐹 ‘ 𝐴 ) = 0 )
146 140 141 8 8 142 144 145 ofval ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) → ( ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) ‘ 𝐴 ) = ( 𝑅 · 0 ) )
147 1 146 mpdan ⊢ ( 𝜑 → ( ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) ‘ 𝐴 ) = ( 𝑅 · 0 ) )
148 55 mul01d ⊢ ( 𝜑 → ( 𝑅 · 0 ) = 0 )
149 147 148 eqtrd ⊢ ( 𝜑 → ( ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) ‘ 𝐴 ) = 0 )
150 fveq1 ⊢ ( 𝑓 = ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) → ( 𝑓 ‘ 𝐴 ) = ( ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) ‘ 𝐴 ) )
151 150 eqeq1d ⊢ ( 𝑓 = ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) → ( ( 𝑓 ‘ 𝐴 ) = 0 ↔ ( ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) ‘ 𝐴 ) = 0 ) )
152 151 rspcev ⊢ ( ( ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( ( ( ℂ × { 𝑅 } ) ∘f · 𝐹 ) ‘ 𝐴 ) = 0 ) → ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 )
153 137 149 152 syl2anc ⊢ ( 𝜑 → ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 )
154 elaa ⊢ ( 𝐴 ∈ 𝔸 ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) )
155 1 153 154 sylanbrc ⊢ ( 𝜑 → 𝐴 ∈ 𝔸 )