Metamath Proof Explorer

Theorem plyeq0lem

Description: Lemma for plyeq0 . If A is the coefficient function for a nonzero polynomial such that P ( z ) = sum_ k e. NN0 A ( k ) x. z ^ k = 0 for every z e. CC and A ( M ) is the nonzero leading coefficient, then the function F ( z ) = P ( z ) / z ^ M is a sum of powers of 1 / z , and so the limit of this function as z ~> +oo is the constant term, A ( M ) . But F ( z ) = 0 everywhere, so this limit is also equal to zero so that A ( M ) = 0 , a contradiction. (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Hypotheses plyeq0.1 ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
plyeq0.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
plyeq0.3 ⊢ ( 𝜑 → 𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
plyeq0.4 ⊢ ( 𝜑 → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
plyeq0.5 ⊢ ( 𝜑 → 0𝑝 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
plyeq0.6 ⊢ 𝑀 = sup ( ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) , ℝ , < )
plyeq0.7 ⊢ ( 𝜑 → ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ )
Assertion plyeq0lem ¬ 𝜑

Proof

Step Hyp Ref Expression
1 plyeq0.1 ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
2 plyeq0.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
3 plyeq0.3 ⊢ ( 𝜑 → 𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
4 plyeq0.4 ⊢ ( 𝜑 → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
5 plyeq0.5 ⊢ ( 𝜑 → 0𝑝 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
6 plyeq0.6 ⊢ 𝑀 = sup ( ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) , ℝ , < )
7 plyeq0.7 ⊢ ( 𝜑 → ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ )
8 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
9 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
10 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ Fin )
11 1zzd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) → 1 ∈ ℤ )
12 0cn ⊢ 0 ∈ ℂ
13 12 a1i ⊢ ( 𝜑 → 0 ∈ ℂ )
14 13 snssd ⊢ ( 𝜑 → { 0 } ⊆ ℂ )
15 1 14 unssd ⊢ ( 𝜑 → ( 𝑆 ∪ { 0 } ) ⊆ ℂ )
16 cnex ⊢ ℂ ∈ V
17 ssexg ⊢ ( ( ( 𝑆 ∪ { 0 } ) ⊆ ℂ ∧ ℂ ∈ V ) → ( 𝑆 ∪ { 0 } ) ∈ V )
18 15 16 17 sylancl ⊢ ( 𝜑 → ( 𝑆 ∪ { 0 } ) ∈ V )
19 nn0ex ⊢ ℕ0 ∈ V
20 elmapg ⊢ ( ( ( 𝑆 ∪ { 0 } ) ∈ V ∧ ℕ0 ∈ V ) → ( 𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ↔ 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
21 18 19 20 sylancl ⊢ ( 𝜑 → ( 𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ↔ 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
22 3 21 mpbid ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
23 22 15 fssd ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
24 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
25 ffvelcdm ⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
26 23 24 25 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
27 26 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
28 27 abscld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) → ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ )
29 28 recnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) → ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℂ )
30 divcnv ⊢ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℂ → ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝑛 ) ) ⇝ 0 )
31 29 30 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) → ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝑛 ) ) ⇝ 0 )
32 nnex ⊢ ℕ ∈ V
33 32 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ∈ V
34 33 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) → ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ∈ V )
35 oveq2 ⊢ ( 𝑛 = 𝑚 → ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝑛 ) = ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝑚 ) )
36 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝑛 ) )
37 ovex ⊢ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝑚 ) ∈ V
38 35 36 37 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝑛 ) ) ‘ 𝑚 ) = ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝑚 ) )
39 38 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝑛 ) ) ‘ 𝑚 ) = ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝑚 ) )
40 nndivre ⊢ ( ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ ∧ 𝑚 ∈ ℕ ) → ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝑚 ) ∈ ℝ )
41 28 40 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝑚 ) ∈ ℝ )
42 39 41 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝑛 ) ) ‘ 𝑚 ) ∈ ℝ )
43 oveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) = ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) )
44 43 oveq2d ⊢ ( 𝑛 = 𝑚 → ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) = ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) )
45 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) )
46 ovex ⊢ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) ∈ V
47 44 45 46 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ‘ 𝑚 ) = ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) )
48 47 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ‘ 𝑚 ) = ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) )
49 26 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
50 49 abscld ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ )
51 nnrp ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ+ )
52 51 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℝ+ )
53 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℤ )
54 cnvimass ⊢ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ⊆ dom 𝐴
55 54 22 fssdm ⊢ ( 𝜑 → ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ⊆ ℕ0 )
56 nn0ssz ⊢ ℕ0 ⊆ ℤ
57 55 56 sstrdi ⊢ ( 𝜑 → ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ⊆ ℤ )
58 2 nn0red ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
59 22 ffnd ⊢ ( 𝜑 → 𝐴 Fn ℕ0 )
60 elpreima ⊢ ( 𝐴 Fn ℕ0 → ( 𝑧 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ↔ ( 𝑧 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑧 ) ∈ ( 𝑆 ∖ { 0 } ) ) ) )
61 59 60 syl ⊢ ( 𝜑 → ( 𝑧 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ↔ ( 𝑧 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑧 ) ∈ ( 𝑆 ∖ { 0 } ) ) ) )
62 61 simplbda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ) → ( 𝐴 ‘ 𝑧 ) ∈ ( 𝑆 ∖ { 0 } ) )
63 eldifsni ⊢ ( ( 𝐴 ‘ 𝑧 ) ∈ ( 𝑆 ∖ { 0 } ) → ( 𝐴 ‘ 𝑧 ) ≠ 0 )
64 62 63 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ) → ( 𝐴 ‘ 𝑧 ) ≠ 0 )
65 fveq2 ⊢ ( 𝑘 = 𝑧 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑧 ) )
66 65 neeq1d ⊢ ( 𝑘 = 𝑧 → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 ↔ ( 𝐴 ‘ 𝑧 ) ≠ 0 ) )
67 breq1 ⊢ ( 𝑘 = 𝑧 → ( 𝑘 ≤ 𝑁 ↔ 𝑧 ≤ 𝑁 ) )
68 66 67 imbi12d ⊢ ( 𝑘 = 𝑧 → ( ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) ↔ ( ( 𝐴 ‘ 𝑧 ) ≠ 0 → 𝑧 ≤ 𝑁 ) ) )
69 plyco0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 : ℕ0 ⟶ ℂ ) → ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) ) )
70 2 23 69 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) ) )
71 4 70 mpbid ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
72 71 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ) → ∀ 𝑘 ∈ ℕ0 ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
73 55 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ) → 𝑧 ∈ ℕ0 )
74 68 72 73 rspcdva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ) → ( ( 𝐴 ‘ 𝑧 ) ≠ 0 → 𝑧 ≤ 𝑁 ) )
75 64 74 mpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ) → 𝑧 ≤ 𝑁 )
76 75 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) 𝑧 ≤ 𝑁 )
77 brralrspcev ⊢ ( ( 𝑁 ∈ ℝ ∧ ∀ 𝑧 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) 𝑧 ≤ 𝑁 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) 𝑧 ≤ 𝑥 )
78 58 76 77 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) 𝑧 ≤ 𝑥 )
79 suprzcl ⊢ ( ( ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ⊆ ℤ ∧ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) 𝑧 ≤ 𝑥 ) → sup ( ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) , ℝ , < ) ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) )
80 57 7 78 79 syl3anc ⊢ ( 𝜑 → sup ( ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) , ℝ , < ) ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) )
81 6 80 eqeltrid ⊢ ( 𝜑 → 𝑀 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) )
82 55 81 sseldd ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
83 82 nn0zd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
84 zsubcl ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑘 − 𝑀 ) ∈ ℤ )
85 53 83 84 syl2anr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑘 − 𝑀 ) ∈ ℤ )
86 85 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( 𝑘 − 𝑀 ) ∈ ℤ )
87 52 86 rpexpcld ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ∈ ℝ+ )
88 87 rpred ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ∈ ℝ )
89 50 88 remulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) ∈ ℝ )
90 48 89 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ‘ 𝑚 ) ∈ ℝ )
91 nnrecre ⊢ ( 𝑚 ∈ ℕ → ( 1 / 𝑚 ) ∈ ℝ )
92 91 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( 1 / 𝑚 ) ∈ ℝ )
93 27 absge0d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) → 0 ≤ ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) )
94 93 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → 0 ≤ ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) )
95 nnre ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ )
96 95 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℝ )
97 nnge1 ⊢ ( 𝑚 ∈ ℕ → 1 ≤ 𝑚 )
98 97 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → 1 ≤ 𝑚 )
99 1red ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → 1 ∈ ℝ )
100 86 zred ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( 𝑘 − 𝑀 ) ∈ ℝ )
101 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → 𝑘 < 𝑀 )
102 53 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℤ )
103 102 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → 𝑘 ∈ ℤ )
104 83 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → 𝑀 ∈ ℤ )
105 zltp1le ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑘 < 𝑀 ↔ ( 𝑘 + 1 ) ≤ 𝑀 ) )
106 103 104 105 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( 𝑘 < 𝑀 ↔ ( 𝑘 + 1 ) ≤ 𝑀 ) )
107 101 106 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( 𝑘 + 1 ) ≤ 𝑀 )
108 24 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
109 108 nn0red ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℝ )
110 109 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → 𝑘 ∈ ℝ )
111 82 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑀 ∈ ℕ0 )
112 111 nn0red ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑀 ∈ ℝ )
113 112 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → 𝑀 ∈ ℝ )
114 110 99 113 leaddsub2d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑘 + 1 ) ≤ 𝑀 ↔ 1 ≤ ( 𝑀 − 𝑘 ) ) )
115 107 114 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → 1 ≤ ( 𝑀 − 𝑘 ) )
116 109 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℂ )
117 116 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → 𝑘 ∈ ℂ )
118 112 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑀 ∈ ℂ )
119 118 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → 𝑀 ∈ ℂ )
120 117 119 negsubdi2d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → - ( 𝑘 − 𝑀 ) = ( 𝑀 − 𝑘 ) )
121 115 120 breqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → 1 ≤ - ( 𝑘 − 𝑀 ) )
122 99 100 121 lenegcon2d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( 𝑘 − 𝑀 ) ≤ - 1 )
123 neg1z ⊢ - 1 ∈ ℤ
124 eluz ⊢ ( ( ( 𝑘 − 𝑀 ) ∈ ℤ ∧ - 1 ∈ ℤ ) → ( - 1 ∈ ( ℤ≥ ‘ ( 𝑘 − 𝑀 ) ) ↔ ( 𝑘 − 𝑀 ) ≤ - 1 ) )
125 86 123 124 sylancl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( - 1 ∈ ( ℤ≥ ‘ ( 𝑘 − 𝑀 ) ) ↔ ( 𝑘 − 𝑀 ) ≤ - 1 ) )
126 122 125 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → - 1 ∈ ( ℤ≥ ‘ ( 𝑘 − 𝑀 ) ) )
127 96 98 126 leexp2ad ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ≤ ( 𝑚 ↑ - 1 ) )
128 nncn ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℂ )
129 128 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℂ )
130 expn1 ⊢ ( 𝑚 ∈ ℂ → ( 𝑚 ↑ - 1 ) = ( 1 / 𝑚 ) )
131 129 130 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( 𝑚 ↑ - 1 ) = ( 1 / 𝑚 ) )
132 127 131 breqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ≤ ( 1 / 𝑚 ) )
133 88 92 50 94 132 lemul2ad ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) ≤ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 1 / 𝑚 ) ) )
134 29 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℂ )
135 nnne0 ⊢ ( 𝑚 ∈ ℕ → 𝑚 ≠ 0 )
136 135 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → 𝑚 ≠ 0 )
137 134 129 136 divrecd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝑚 ) = ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 1 / 𝑚 ) ) )
138 39 137 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝑛 ) ) ‘ 𝑚 ) = ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 1 / 𝑚 ) ) )
139 133 48 138 3brtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ‘ 𝑚 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) / 𝑛 ) ) ‘ 𝑚 ) )
140 87 rpge0d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → 0 ≤ ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) )
141 50 88 94 140 mulge0d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → 0 ≤ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) )
142 141 48 breqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → 0 ≤ ( ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ‘ 𝑚 ) )
143 8 11 31 34 42 90 139 142 climsqz2 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) → ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ⇝ 0 )
144 32 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ∈ V
145 144 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ∈ V )
146 43 oveq2d ⊢ ( 𝑛 = 𝑚 → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) )
147 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) )
148 ovex ⊢ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) ∈ V
149 146 147 148 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ‘ 𝑚 ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) )
150 149 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ‘ 𝑚 ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) )
151 23 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝐴 : ℕ0 ⟶ ℂ )
152 151 24 25 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
153 128 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑚 ∈ ℂ )
154 135 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑚 ≠ 0 )
155 83 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑀 ∈ ℤ )
156 53 155 84 syl2anr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑘 − 𝑀 ) ∈ ℤ )
157 153 154 156 expclzd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ∈ ℂ )
158 152 157 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) ∈ ℂ )
159 150 158 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ‘ 𝑚 ) ∈ ℂ )
160 159 an32s ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ‘ 𝑚 ) ∈ ℂ )
161 160 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ‘ 𝑚 ) ∈ ℂ )
162 88 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ∈ ℂ )
163 49 162 absmuld ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) ) = ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( abs ‘ ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) ) )
164 88 140 absidd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( abs ‘ ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) = ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) )
165 164 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( abs ‘ ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) ) = ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) )
166 163 165 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) ) = ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) )
167 149 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ‘ 𝑚 ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) )
168 167 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( abs ‘ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ‘ 𝑚 ) ) = ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) ) )
169 166 168 48 3eqtr4rd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ‘ 𝑚 ) = ( abs ‘ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ‘ 𝑚 ) ) )
170 8 11 145 34 161 169 climabs0 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ⇝ 0 ↔ ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ⇝ 0 ) )
171 143 170 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ⇝ 0 )
172 109 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) → 𝑘 ∈ ℝ )
173 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) → 𝑘 < 𝑀 )
174 172 173 ltned ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) → 𝑘 ≠ 𝑀 )
175 velsn ⊢ ( 𝑘 ∈ { 𝑀 } ↔ 𝑘 = 𝑀 )
176 175 necon3bbii ⊢ ( ¬ 𝑘 ∈ { 𝑀 } ↔ 𝑘 ≠ 𝑀 )
177 174 176 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) → ¬ 𝑘 ∈ { 𝑀 } )
178 177 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) → if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) = 0 )
179 171 178 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 < 𝑀 ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ⇝ if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) )
180 nncn ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
181 180 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) = 0 ) → 𝑛 ∈ ℂ )
182 nnne0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ≠ 0 )
183 182 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) = 0 ) → 𝑛 ≠ 0 )
184 85 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) = 0 ) → ( 𝑘 − 𝑀 ) ∈ ℤ )
185 181 183 184 expclzd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) = 0 ) → ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ∈ ℂ )
186 185 mul02d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) = 0 ) → ( 0 · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) = 0 )
187 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) = 0 ) → ( 𝐴 ‘ 𝑘 ) = 0 )
188 187 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) = 0 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) = ( 0 · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) )
189 187 ifeq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) = 0 ) → if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) = if ( 𝑘 ∈ { 𝑀 } , 0 , 0 ) )
190 ifid ⊢ if ( 𝑘 ∈ { 𝑀 } , 0 , 0 ) = 0
191 189 190 eqtrdi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) = 0 ) → if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) = 0 )
192 186 188 191 3eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) = 0 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) = if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) )
193 26 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
194 193 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
195 194 mulridd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → ( ( 𝐴 ‘ 𝑘 ) · 1 ) = ( 𝐴 ‘ 𝑘 ) )
196 nn0ssre ⊢ ℕ0 ⊆ ℝ
197 55 196 sstrdi ⊢ ( 𝜑 → ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ⊆ ℝ )
198 197 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ⊆ ℝ )
199 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ )
200 78 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) 𝑧 ≤ 𝑥 )
201 24 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → 𝑘 ∈ ℕ0 )
202 ffvelcdm ⊢ ( ( 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ( 𝑆 ∪ { 0 } ) )
203 22 24 202 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ( 𝑆 ∪ { 0 } ) )
204 203 anim1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → ( ( 𝐴 ‘ 𝑘 ) ∈ ( 𝑆 ∪ { 0 } ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) )
205 eldifsn ⊢ ( ( 𝐴 ‘ 𝑘 ) ∈ ( ( 𝑆 ∪ { 0 } ) ∖ { 0 } ) ↔ ( ( 𝐴 ‘ 𝑘 ) ∈ ( 𝑆 ∪ { 0 } ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) )
206 204 205 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ( ( 𝑆 ∪ { 0 } ) ∖ { 0 } ) )
207 difun2 ⊢ ( ( 𝑆 ∪ { 0 } ) ∖ { 0 } ) = ( 𝑆 ∖ { 0 } )
208 206 207 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ( 𝑆 ∖ { 0 } ) )
209 elpreima ⊢ ( 𝐴 Fn ℕ0 → ( 𝑘 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ↔ ( 𝑘 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑘 ) ∈ ( 𝑆 ∖ { 0 } ) ) ) )
210 59 209 syl ⊢ ( 𝜑 → ( 𝑘 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ↔ ( 𝑘 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑘 ) ∈ ( 𝑆 ∖ { 0 } ) ) ) )
211 210 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → ( 𝑘 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ↔ ( 𝑘 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑘 ) ∈ ( 𝑆 ∖ { 0 } ) ) ) )
212 201 208 211 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → 𝑘 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) )
213 198 199 200 212 suprubd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → 𝑘 ≤ sup ( ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) , ℝ , < ) )
214 213 6 breqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → 𝑘 ≤ 𝑀 )
215 214 ad4ant14 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → 𝑘 ≤ 𝑀 )
216 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → 𝑀 ≤ 𝑘 )
217 109 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → 𝑘 ∈ ℝ )
218 112 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → 𝑀 ∈ ℝ )
219 217 218 letri3d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → ( 𝑘 = 𝑀 ↔ ( 𝑘 ≤ 𝑀 ∧ 𝑀 ≤ 𝑘 ) ) )
220 215 216 219 mpbir2and ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → 𝑘 = 𝑀 )
221 220 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → ( 𝑘 − 𝑀 ) = ( 𝑀 − 𝑀 ) )
222 118 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → 𝑀 ∈ ℂ )
223 222 subidd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → ( 𝑀 − 𝑀 ) = 0 )
224 221 223 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → ( 𝑘 − 𝑀 ) = 0 )
225 224 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) = ( 𝑛 ↑ 0 ) )
226 180 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → 𝑛 ∈ ℂ )
227 226 exp0d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → ( 𝑛 ↑ 0 ) = 1 )
228 225 227 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) = 1 )
229 228 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) = ( ( 𝐴 ‘ 𝑘 ) · 1 ) )
230 220 175 sylibr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → 𝑘 ∈ { 𝑀 } )
231 230 iftrued ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) = ( 𝐴 ‘ 𝑘 ) )
232 195 229 231 3eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) = if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) )
233 192 232 pm2.61dane ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) = if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) )
234 233 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) ) )
235 fconstmpt ⊢ ( ℕ × { if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) } ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) )
236 234 235 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) = ( ℕ × { if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) } ) )
237 ifcl ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℂ ∧ 0 ∈ ℂ ) → if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) ∈ ℂ )
238 193 12 237 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) → if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) ∈ ℂ )
239 1z ⊢ 1 ∈ ℤ
240 8 eqimss2i ⊢ ( ℤ≥ ‘ 1 ) ⊆ ℕ
241 240 32 climconst2 ⊢ ( ( if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) ∈ ℂ ∧ 1 ∈ ℤ ) → ( ℕ × { if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) } ) ⇝ if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) )
242 238 239 241 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) → ( ℕ × { if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) } ) ⇝ if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) )
243 236 242 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑀 ≤ 𝑘 ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ⇝ if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) )
244 179 243 109 112 ltlecasei ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ⇝ if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) )
245 snex ⊢ { 0 } ∈ V
246 32 245 xpex ⊢ ( ℕ × { 0 } ) ∈ V
247 246 a1i ⊢ ( 𝜑 → ( ℕ × { 0 } ) ∈ V )
248 160 anasss ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑚 ∈ ℕ ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ‘ 𝑚 ) ∈ ℂ )
249 5 fveq1d ⊢ ( 𝜑 → ( 0𝑝 ‘ 𝑚 ) = ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ 𝑚 ) )
250 249 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 0𝑝 ‘ 𝑚 ) = ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ 𝑚 ) )
251 128 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℂ )
252 0pval ⊢ ( 𝑚 ∈ ℂ → ( 0𝑝 ‘ 𝑚 ) = 0 )
253 251 252 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 0𝑝 ‘ 𝑚 ) = 0 )
254 oveq1 ⊢ ( 𝑧 = 𝑚 → ( 𝑧 ↑ 𝑘 ) = ( 𝑚 ↑ 𝑘 ) )
255 254 oveq2d ⊢ ( 𝑧 = 𝑚 → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ 𝑘 ) ) )
256 255 sumeq2sdv ⊢ ( 𝑧 = 𝑚 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ 𝑘 ) ) )
257 eqid ⊢ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
258 sumex ⊢ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ 𝑘 ) ) ∈ V
259 256 257 258 fvmpt ⊢ ( 𝑚 ∈ ℂ → ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ 𝑚 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ 𝑘 ) ) )
260 251 259 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ‘ 𝑚 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ 𝑘 ) ) )
261 250 253 260 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 0 = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ 𝑘 ) ) )
262 261 oveq1d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 0 / ( 𝑚 ↑ 𝑀 ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ 𝑘 ) ) / ( 𝑚 ↑ 𝑀 ) ) )
263 expcl ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑚 ↑ 𝑀 ) ∈ ℂ )
264 128 82 263 syl2anr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑚 ↑ 𝑀 ) ∈ ℂ )
265 135 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ≠ 0 )
266 251 265 155 expne0d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑚 ↑ 𝑀 ) ≠ 0 )
267 264 266 div0d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 0 / ( 𝑚 ↑ 𝑀 ) ) = 0 )
268 fzfid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 0 ... 𝑁 ) ∈ Fin )
269 expcl ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑚 ↑ 𝑘 ) ∈ ℂ )
270 251 24 269 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑚 ↑ 𝑘 ) ∈ ℂ )
271 152 270 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ 𝑘 ) ) ∈ ℂ )
272 268 264 271 266 fsumdivc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ 𝑘 ) ) / ( 𝑚 ↑ 𝑀 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ 𝑘 ) ) / ( 𝑚 ↑ 𝑀 ) ) )
273 262 267 272 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 0 = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ 𝑘 ) ) / ( 𝑚 ↑ 𝑀 ) ) )
274 fvconst2g ⊢ ( ( 0 ∈ ℂ ∧ 𝑚 ∈ ℕ ) → ( ( ℕ × { 0 } ) ‘ 𝑚 ) = 0 )
275 13 274 sylan ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ℕ × { 0 } ) ‘ 𝑚 ) = 0 )
276 155 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑀 ∈ ℤ )
277 53 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℤ )
278 153 154 276 277 expsubd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) = ( ( 𝑚 ↑ 𝑘 ) / ( 𝑚 ↑ 𝑀 ) ) )
279 278 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ ( 𝑘 − 𝑀 ) ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑚 ↑ 𝑘 ) / ( 𝑚 ↑ 𝑀 ) ) ) )
280 264 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑚 ↑ 𝑀 ) ∈ ℂ )
281 266 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑚 ↑ 𝑀 ) ≠ 0 )
282 152 270 280 281 divassd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ 𝑘 ) ) / ( 𝑚 ↑ 𝑀 ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( ( 𝑚 ↑ 𝑘 ) / ( 𝑚 ↑ 𝑀 ) ) ) )
283 279 150 282 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ‘ 𝑚 ) = ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ 𝑘 ) ) / ( 𝑚 ↑ 𝑀 ) ) )
284 283 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ‘ 𝑚 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑚 ↑ 𝑘 ) ) / ( 𝑚 ↑ 𝑀 ) ) )
285 273 275 284 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ℕ × { 0 } ) ‘ 𝑚 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑛 ↑ ( 𝑘 − 𝑀 ) ) ) ) ‘ 𝑚 ) )
286 8 9 10 244 247 248 285 climfsum ⊢ ( 𝜑 → ( ℕ × { 0 } ) ⇝ Σ 𝑘 ∈ ( 0 ... 𝑁 ) if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) )
287 suprleub ⊢ ( ( ( ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ⊆ ℝ ∧ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) 𝑧 ≤ 𝑥 ) ∧ 𝑁 ∈ ℝ ) → ( sup ( ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) , ℝ , < ) ≤ 𝑁 ↔ ∀ 𝑧 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) 𝑧 ≤ 𝑁 ) )
288 197 7 78 58 287 syl31anc ⊢ ( 𝜑 → ( sup ( ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) , ℝ , < ) ≤ 𝑁 ↔ ∀ 𝑧 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) 𝑧 ≤ 𝑁 ) )
289 76 288 mpbird ⊢ ( 𝜑 → sup ( ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) , ℝ , < ) ≤ 𝑁 )
290 6 289 eqbrtrid ⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
291 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
292 82 291 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
293 2 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
294 elfz5 ⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∈ ( 0 ... 𝑁 ) ↔ 𝑀 ≤ 𝑁 ) )
295 292 293 294 syl2anc ⊢ ( 𝜑 → ( 𝑀 ∈ ( 0 ... 𝑁 ) ↔ 𝑀 ≤ 𝑁 ) )
296 290 295 mpbird ⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑁 ) )
297 296 snssd ⊢ ( 𝜑 → { 𝑀 } ⊆ ( 0 ... 𝑁 ) )
298 23 82 ffvelcdmd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑀 ) ∈ ℂ )
299 elsni ⊢ ( 𝑘 ∈ { 𝑀 } → 𝑘 = 𝑀 )
300 299 fveq2d ⊢ ( 𝑘 ∈ { 𝑀 } → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑀 ) )
301 300 eleq1d ⊢ ( 𝑘 ∈ { 𝑀 } → ( ( 𝐴 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐴 ‘ 𝑀 ) ∈ ℂ ) )
302 298 301 syl5ibrcom ⊢ ( 𝜑 → ( 𝑘 ∈ { 𝑀 } → ( 𝐴 ‘ 𝑘 ) ∈ ℂ ) )
303 302 ralrimiv ⊢ ( 𝜑 → ∀ 𝑘 ∈ { 𝑀 } ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
304 10 olcd ⊢ ( 𝜑 → ( ( 0 ... 𝑁 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 0 ... 𝑁 ) ∈ Fin ) )
305 sumss2 ⊢ ( ( ( { 𝑀 } ⊆ ( 0 ... 𝑁 ) ∧ ∀ 𝑘 ∈ { 𝑀 } ( 𝐴 ‘ 𝑘 ) ∈ ℂ ) ∧ ( ( 0 ... 𝑁 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 0 ... 𝑁 ) ∈ Fin ) ) → Σ 𝑘 ∈ { 𝑀 } ( 𝐴 ‘ 𝑘 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) )
306 297 303 304 305 syl21anc ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑀 } ( 𝐴 ‘ 𝑘 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) )
307 ltso ⊢ < Or ℝ
308 307 supex ⊢ sup ( ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) , ℝ , < ) ∈ V
309 6 308 eqeltri ⊢ 𝑀 ∈ V
310 fveq2 ⊢ ( 𝑘 = 𝑀 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑀 ) )
311 310 sumsn ⊢ ( ( 𝑀 ∈ V ∧ ( 𝐴 ‘ 𝑀 ) ∈ ℂ ) → Σ 𝑘 ∈ { 𝑀 } ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑀 ) )
312 309 298 311 sylancr ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑀 } ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑀 ) )
313 306 312 eqtr3d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) if ( 𝑘 ∈ { 𝑀 } , ( 𝐴 ‘ 𝑘 ) , 0 ) = ( 𝐴 ‘ 𝑀 ) )
314 286 313 breqtrd ⊢ ( 𝜑 → ( ℕ × { 0 } ) ⇝ ( 𝐴 ‘ 𝑀 ) )
315 240 32 climconst2 ⊢ ( ( 0 ∈ ℂ ∧ 1 ∈ ℤ ) → ( ℕ × { 0 } ) ⇝ 0 )
316 12 239 315 mp2an ⊢ ( ℕ × { 0 } ) ⇝ 0
317 climuni ⊢ ( ( ( ℕ × { 0 } ) ⇝ ( 𝐴 ‘ 𝑀 ) ∧ ( ℕ × { 0 } ) ⇝ 0 ) → ( 𝐴 ‘ 𝑀 ) = 0 )
318 314 316 317 sylancl ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑀 ) = 0 )
319 fvex ⊢ ( 𝐴 ‘ 𝑀 ) ∈ V
320 319 elsn ⊢ ( ( 𝐴 ‘ 𝑀 ) ∈ { 0 } ↔ ( 𝐴 ‘ 𝑀 ) = 0 )
321 318 320 sylibr ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑀 ) ∈ { 0 } )
322 elpreima ⊢ ( 𝐴 Fn ℕ0 → ( 𝑀 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ↔ ( 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ∈ ( 𝑆 ∖ { 0 } ) ) ) )
323 59 322 syl ⊢ ( 𝜑 → ( 𝑀 ∈ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ↔ ( 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ∈ ( 𝑆 ∖ { 0 } ) ) ) )
324 81 323 mpbid ⊢ ( 𝜑 → ( 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ∈ ( 𝑆 ∖ { 0 } ) ) )
325 324 simprd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑀 ) ∈ ( 𝑆 ∖ { 0 } ) )
326 325 eldifbd ⊢ ( 𝜑 → ¬ ( 𝐴 ‘ 𝑀 ) ∈ { 0 } )
327 321 326 pm2.65i ⊢ ¬ 𝜑