Metamath Proof Explorer

Theorem eulerpartlems

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 6-Aug-2018) (Revised by Thierry Arnoux, 1-Sep-2019)

Ref Expression
Hypotheses eulerpartlems.r ⊢ 𝑅 = { 𝑓 ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
eulerpartlems.s ⊢ 𝑆 = ( 𝑓 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ↦ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) )
Assertion eulerpartlems ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℤ≥ ‘ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ) ) → ( 𝐴 ‘ 𝑡 ) = 0 )

Proof

Step Hyp Ref Expression
1 eulerpartlems.r ⊢ 𝑅 = { 𝑓 ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2 eulerpartlems.s ⊢ 𝑆 = ( 𝑓 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ↦ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) )
3 1 2 eulerpartlemsf ⊢ 𝑆 : ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ⟶ ℕ0
4 3 ffvelcdmi ⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 )
5 nndiffz1 ⊢ ( ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 → ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) = ( ℤ≥ ‘ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ) )
6 5 eleq2d ⊢ ( ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 → ( 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ↔ 𝑡 ∈ ( ℤ≥ ‘ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ) ) )
7 4 6 syl ⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ↔ 𝑡 ∈ ( ℤ≥ ‘ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ) ) )
8 7 pm5.32i ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) ↔ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℤ≥ ‘ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ) ) )
9 eldif ⊢ ( 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ↔ ( 𝑡 ∈ ℕ ∧ ¬ 𝑡 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) )
10 9 bilani ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → ( 𝑡 ∈ ℕ ∧ ¬ 𝑡 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) )
11 10 simpld ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → 𝑡 ∈ ℕ )
12 1 2 eulerpartlemelr ⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ) )
13 12 simpld ⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → 𝐴 : ℕ ⟶ ℕ0 )
14 13 ffvelcdmda ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) → ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 )
15 11 14 syldan ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 )
16 simpl ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) )
17 4 adantr ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 )
18 10 simprd ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → ¬ 𝑡 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) )
19 simpl ⊢ ( ( 𝑡 ∈ ℕ ∧ ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 ) → 𝑡 ∈ ℕ )
20 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
21 19 20 eleqtrdi ⊢ ( ( 𝑡 ∈ ℕ ∧ ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 ) → 𝑡 ∈ ( ℤ≥ ‘ 1 ) )
22 simpr ⊢ ( ( 𝑡 ∈ ℕ ∧ ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 ) → ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 )
23 22 nn0zd ⊢ ( ( 𝑡 ∈ ℕ ∧ ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 ) → ( 𝑆 ‘ 𝐴 ) ∈ ℤ )
24 elfz5 ⊢ ( ( 𝑡 ∈ ( ℤ≥ ‘ 1 ) ∧ ( 𝑆 ‘ 𝐴 ) ∈ ℤ ) → ( 𝑡 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ↔ 𝑡 ≤ ( 𝑆 ‘ 𝐴 ) ) )
25 21 23 24 syl2anc ⊢ ( ( 𝑡 ∈ ℕ ∧ ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 ) → ( 𝑡 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ↔ 𝑡 ≤ ( 𝑆 ‘ 𝐴 ) ) )
26 25 notbid ⊢ ( ( 𝑡 ∈ ℕ ∧ ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 ) → ( ¬ 𝑡 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ↔ ¬ 𝑡 ≤ ( 𝑆 ‘ 𝐴 ) ) )
27 22 nn0red ⊢ ( ( 𝑡 ∈ ℕ ∧ ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 ) → ( 𝑆 ‘ 𝐴 ) ∈ ℝ )
28 19 nnred ⊢ ( ( 𝑡 ∈ ℕ ∧ ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 ) → 𝑡 ∈ ℝ )
29 27 28 ltnled ⊢ ( ( 𝑡 ∈ ℕ ∧ ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝐴 ) < 𝑡 ↔ ¬ 𝑡 ≤ ( 𝑆 ‘ 𝐴 ) ) )
30 26 29 bitr4d ⊢ ( ( 𝑡 ∈ ℕ ∧ ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 ) → ( ¬ 𝑡 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ↔ ( 𝑆 ‘ 𝐴 ) < 𝑡 ) )
31 30 biimpa ⊢ ( ( ( 𝑡 ∈ ℕ ∧ ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 ) ∧ ¬ 𝑡 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → ( 𝑆 ‘ 𝐴 ) < 𝑡 )
32 11 17 18 31 syl21anc ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → ( 𝑆 ‘ 𝐴 ) < 𝑡 )
33 1 2 eulerpartlemsv1 ⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ 𝐴 ) = Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
34 fveq2 ⊢ ( 𝑘 = 𝑡 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑡 ) )
35 id ⊢ ( 𝑘 = 𝑡 → 𝑘 = 𝑡 )
36 34 35 oveq12d ⊢ ( 𝑘 = 𝑡 → ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) )
37 36 cbvsumv ⊢ Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = Σ 𝑡 ∈ ℕ ( ( 𝐴 ‘ 𝑡 ) · 𝑡 )
38 33 37 eqtr2di ⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → Σ 𝑡 ∈ ℕ ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) = ( 𝑆 ‘ 𝐴 ) )
39 breq2 ⊢ ( 𝑡 = 𝑙 → ( ( 𝑆 ‘ 𝐴 ) < 𝑡 ↔ ( 𝑆 ‘ 𝐴 ) < 𝑙 ) )
40 fveq2 ⊢ ( 𝑡 = 𝑙 → ( 𝐴 ‘ 𝑡 ) = ( 𝐴 ‘ 𝑙 ) )
41 40 breq2d ⊢ ( 𝑡 = 𝑙 → ( 0 < ( 𝐴 ‘ 𝑡 ) ↔ 0 < ( 𝐴 ‘ 𝑙 ) ) )
42 39 41 anbi12d ⊢ ( 𝑡 = 𝑙 → ( ( ( 𝑆 ‘ 𝐴 ) < 𝑡 ∧ 0 < ( 𝐴 ‘ 𝑡 ) ) ↔ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) )
43 42 cbvrexvw ⊢ ( ∃ 𝑡 ∈ ℕ ( ( 𝑆 ‘ 𝐴 ) < 𝑡 ∧ 0 < ( 𝐴 ‘ 𝑡 ) ) ↔ ∃ 𝑙 ∈ ℕ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) )
44 4 adantr ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ∃ 𝑙 ∈ ℕ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) → ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 )
45 44 nn0red ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ∃ 𝑙 ∈ ℕ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) → ( 𝑆 ‘ 𝐴 ) ∈ ℝ )
46 4 ad2antrr ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) → ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 )
47 46 nn0red ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) → ( 𝑆 ‘ 𝐴 ) ∈ ℝ )
48 simpr ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → 𝑙 ∈ ℕ )
49 48 adantr ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) → 𝑙 ∈ ℕ )
50 49 nnred ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) → 𝑙 ∈ ℝ )
51 1zzd ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → 1 ∈ ℤ )
52 13 ad2antrr ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ 𝑡 ∈ ℕ ) → 𝐴 : ℕ ⟶ ℕ0 )
53 simpr ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ 𝑡 ∈ ℕ ) → 𝑡 ∈ ℕ )
54 eqidd ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑡 ∈ ℕ ) → ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) )
55 simpr ⊢ ( ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑡 ∈ ℕ ) ∧ 𝑚 = 𝑡 ) → 𝑚 = 𝑡 )
56 55 fveq2d ⊢ ( ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑡 ∈ ℕ ) ∧ 𝑚 = 𝑡 ) → ( 𝐴 ‘ 𝑚 ) = ( 𝐴 ‘ 𝑡 ) )
57 56 55 oveq12d ⊢ ( ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑡 ∈ ℕ ) ∧ 𝑚 = 𝑡 ) → ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) = ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) )
58 simpr ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑡 ∈ ℕ ) → 𝑡 ∈ ℕ )
59 ffvelcdm ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑡 ∈ ℕ ) → ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 )
60 58 nnnn0d ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑡 ∈ ℕ ) → 𝑡 ∈ ℕ0 )
61 59 60 nn0mulcld ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑡 ∈ ℕ ) → ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ∈ ℕ0 )
62 54 57 58 61 fvmptd ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑡 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) ‘ 𝑡 ) = ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) )
63 52 53 62 syl2anc ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ 𝑡 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) ‘ 𝑡 ) = ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) )
64 13 adantr ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → 𝐴 : ℕ ⟶ ℕ0 )
65 64 ffvelcdmda ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ 𝑡 ∈ ℕ ) → ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 )
66 53 nnnn0d ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ 𝑡 ∈ ℕ ) → 𝑡 ∈ ℕ0 )
67 65 66 nn0mulcld ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ 𝑡 ∈ ℕ ) → ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ∈ ℕ0 )
68 67 nn0red ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ 𝑡 ∈ ℕ ) → ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ∈ ℝ )
69 fveq2 ⊢ ( 𝑚 = 𝑡 → ( 𝐴 ‘ 𝑚 ) = ( 𝐴 ‘ 𝑡 ) )
70 id ⊢ ( 𝑚 = 𝑡 → 𝑚 = 𝑡 )
71 69 70 oveq12d ⊢ ( 𝑚 = 𝑡 → ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) = ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) )
72 71 cbvmptv ⊢ ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) = ( 𝑡 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) )
73 67 72 fmptd ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) : ℕ ⟶ ℕ0 )
74 nn0sscn ⊢ ℕ0 ⊆ ℂ
75 fss ⊢ ( ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) : ℕ ⟶ ℕ0 ∧ ℕ0 ⊆ ℂ ) → ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) : ℕ ⟶ ℂ )
76 73 74 75 sylancl ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) : ℕ ⟶ ℂ )
77 nnex ⊢ ℕ ∈ V
78 0nn0 ⊢ 0 ∈ ℕ0
79 eqid ⊢ ( ℂ ∖ { 0 } ) = ( ℂ ∖ { 0 } )
80 79 ffs2 ⊢ ( ( ℕ ∈ V ∧ 0 ∈ ℕ0 ∧ ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) : ℕ ⟶ ℂ ) → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) supp 0 ) = ( ◡ ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) “ ( ℂ ∖ { 0 } ) ) )
81 77 78 80 mp3an12 ⊢ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) : ℕ ⟶ ℂ → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) supp 0 ) = ( ◡ ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) “ ( ℂ ∖ { 0 } ) ) )
82 76 81 syl ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) supp 0 ) = ( ◡ ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) “ ( ℂ ∖ { 0 } ) ) )
83 fcdmnn0supp ⊢ ( ( ℕ ∈ V ∧ 𝐴 : ℕ ⟶ ℕ0 ) → ( 𝐴 supp 0 ) = ( ◡ 𝐴 “ ℕ ) )
84 77 64 83 sylancr ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → ( 𝐴 supp 0 ) = ( ◡ 𝐴 “ ℕ ) )
85 12 simprd ⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( ◡ 𝐴 “ ℕ ) ∈ Fin )
86 85 adantr ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → ( ◡ 𝐴 “ ℕ ) ∈ Fin )
87 84 86 eqeltrd ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → ( 𝐴 supp 0 ) ∈ Fin )
88 77 a1i ⊢ ( 𝐴 : ℕ ⟶ ℕ0 → ℕ ∈ V )
89 78 a1i ⊢ ( 𝐴 : ℕ ⟶ ℕ0 → 0 ∈ ℕ0 )
90 ffn ⊢ ( 𝐴 : ℕ ⟶ ℕ0 → 𝐴 Fn ℕ )
91 simp3 ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑡 ∈ ℕ ∧ ( 𝐴 ‘ 𝑡 ) = 0 ) → ( 𝐴 ‘ 𝑡 ) = 0 )
92 91 oveq1d ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑡 ∈ ℕ ∧ ( 𝐴 ‘ 𝑡 ) = 0 ) → ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) = ( 0 · 𝑡 ) )
93 simp2 ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑡 ∈ ℕ ∧ ( 𝐴 ‘ 𝑡 ) = 0 ) → 𝑡 ∈ ℕ )
94 93 nncnd ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑡 ∈ ℕ ∧ ( 𝐴 ‘ 𝑡 ) = 0 ) → 𝑡 ∈ ℂ )
95 94 mul02d ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑡 ∈ ℕ ∧ ( 𝐴 ‘ 𝑡 ) = 0 ) → ( 0 · 𝑡 ) = 0 )
96 92 95 eqtrd ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑡 ∈ ℕ ∧ ( 𝐴 ‘ 𝑡 ) = 0 ) → ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) = 0 )
97 72 88 89 90 96 suppss3 ⊢ ( 𝐴 : ℕ ⟶ ℕ0 → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) supp 0 ) ⊆ ( 𝐴 supp 0 ) )
98 64 97 syl ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) supp 0 ) ⊆ ( 𝐴 supp 0 ) )
99 ssfi ⊢ ( ( ( 𝐴 supp 0 ) ∈ Fin ∧ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) supp 0 ) ⊆ ( 𝐴 supp 0 ) ) → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) supp 0 ) ∈ Fin )
100 87 98 99 syl2anc ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) supp 0 ) ∈ Fin )
101 82 100 eqeltrrd ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → ( ◡ ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) “ ( ℂ ∖ { 0 } ) ) ∈ Fin )
102 20 51 76 101 fsumcvg4 ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑚 ) · 𝑚 ) ) ) ∈ dom ⇝ )
103 20 51 63 68 102 isumrecl ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → Σ 𝑡 ∈ ℕ ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ∈ ℝ )
104 103 adantr ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) → Σ 𝑡 ∈ ℕ ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ∈ ℝ )
105 simprl ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) → ( 𝑆 ‘ 𝐴 ) < 𝑙 )
106 13 ffvelcdmda ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → ( 𝐴 ‘ 𝑙 ) ∈ ℕ0 )
107 106 adantr ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) → ( 𝐴 ‘ 𝑙 ) ∈ ℕ0 )
108 107 nn0red ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) → ( 𝐴 ‘ 𝑙 ) ∈ ℝ )
109 108 50 remulcld ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) → ( ( 𝐴 ‘ 𝑙 ) · 𝑙 ) ∈ ℝ )
110 49 nnnn0d ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) → 𝑙 ∈ ℕ0 )
111 110 nn0ge0d ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) → 0 ≤ 𝑙 )
112 simprr ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) → 0 < ( 𝐴 ‘ 𝑙 ) )
113 elnnnn0b ⊢ ( ( 𝐴 ‘ 𝑙 ) ∈ ℕ ↔ ( ( 𝐴 ‘ 𝑙 ) ∈ ℕ0 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) )
114 nnge1 ⊢ ( ( 𝐴 ‘ 𝑙 ) ∈ ℕ → 1 ≤ ( 𝐴 ‘ 𝑙 ) )
115 113 114 sylbir ⊢ ( ( ( 𝐴 ‘ 𝑙 ) ∈ ℕ0 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) → 1 ≤ ( 𝐴 ‘ 𝑙 ) )
116 107 112 115 syl2anc ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) → 1 ≤ ( 𝐴 ‘ 𝑙 ) )
117 50 108 111 116 lemulge12d ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) → 𝑙 ≤ ( ( 𝐴 ‘ 𝑙 ) · 𝑙 ) )
118 106 nn0cnd ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → ( 𝐴 ‘ 𝑙 ) ∈ ℂ )
119 48 nncnd ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → 𝑙 ∈ ℂ )
120 118 119 mulcld ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → ( ( 𝐴 ‘ 𝑙 ) · 𝑙 ) ∈ ℂ )
121 id ⊢ ( 𝑡 = 𝑙 → 𝑡 = 𝑙 )
122 40 121 oveq12d ⊢ ( 𝑡 = 𝑙 → ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) = ( ( 𝐴 ‘ 𝑙 ) · 𝑙 ) )
123 122 sumsn ⊢ ( ( 𝑙 ∈ ℕ ∧ ( ( 𝐴 ‘ 𝑙 ) · 𝑙 ) ∈ ℂ ) → Σ 𝑡 ∈ { 𝑙 } ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) = ( ( 𝐴 ‘ 𝑙 ) · 𝑙 ) )
124 48 120 123 syl2anc ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → Σ 𝑡 ∈ { 𝑙 } ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) = ( ( 𝐴 ‘ 𝑙 ) · 𝑙 ) )
125 snfi ⊢ { 𝑙 } ∈ Fin
126 125 a1i ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → { 𝑙 } ∈ Fin )
127 48 snssd ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → { 𝑙 } ⊆ ℕ )
128 67 nn0ge0d ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ 𝑡 ∈ ℕ ) → 0 ≤ ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) )
129 20 51 126 127 63 68 128 102 isumless ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → Σ 𝑡 ∈ { 𝑙 } ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ≤ Σ 𝑡 ∈ ℕ ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) )
130 124 129 eqbrtrrd ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) → ( ( 𝐴 ‘ 𝑙 ) · 𝑙 ) ≤ Σ 𝑡 ∈ ℕ ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) )
131 130 adantr ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) → ( ( 𝐴 ‘ 𝑙 ) · 𝑙 ) ≤ Σ 𝑡 ∈ ℕ ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) )
132 50 109 104 117 131 letrd ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) → 𝑙 ≤ Σ 𝑡 ∈ ℕ ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) )
133 47 50 104 105 132 ltletrd ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑙 ∈ ℕ ) ∧ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) → ( 𝑆 ‘ 𝐴 ) < Σ 𝑡 ∈ ℕ ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) )
134 133 r19.29an ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ∃ 𝑙 ∈ ℕ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) → ( 𝑆 ‘ 𝐴 ) < Σ 𝑡 ∈ ℕ ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) )
135 45 134 gtned ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ∃ 𝑙 ∈ ℕ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) ) → Σ 𝑡 ∈ ℕ ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ≠ ( 𝑆 ‘ 𝐴 ) )
136 135 ex ⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( ∃ 𝑙 ∈ ℕ ( ( 𝑆 ‘ 𝐴 ) < 𝑙 ∧ 0 < ( 𝐴 ‘ 𝑙 ) ) → Σ 𝑡 ∈ ℕ ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ≠ ( 𝑆 ‘ 𝐴 ) ) )
137 43 136 biimtrid ⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( ∃ 𝑡 ∈ ℕ ( ( 𝑆 ‘ 𝐴 ) < 𝑡 ∧ 0 < ( 𝐴 ‘ 𝑡 ) ) → Σ 𝑡 ∈ ℕ ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ≠ ( 𝑆 ‘ 𝐴 ) ) )
138 137 necon2bd ⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( Σ 𝑡 ∈ ℕ ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) = ( 𝑆 ‘ 𝐴 ) → ¬ ∃ 𝑡 ∈ ℕ ( ( 𝑆 ‘ 𝐴 ) < 𝑡 ∧ 0 < ( 𝐴 ‘ 𝑡 ) ) ) )
139 38 138 mpd ⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ¬ ∃ 𝑡 ∈ ℕ ( ( 𝑆 ‘ 𝐴 ) < 𝑡 ∧ 0 < ( 𝐴 ‘ 𝑡 ) ) )
140 ralnex ⊢ ( ∀ 𝑡 ∈ ℕ ¬ ( ( 𝑆 ‘ 𝐴 ) < 𝑡 ∧ 0 < ( 𝐴 ‘ 𝑡 ) ) ↔ ¬ ∃ 𝑡 ∈ ℕ ( ( 𝑆 ‘ 𝐴 ) < 𝑡 ∧ 0 < ( 𝐴 ‘ 𝑡 ) ) )
141 139 140 sylibr ⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ∀ 𝑡 ∈ ℕ ¬ ( ( 𝑆 ‘ 𝐴 ) < 𝑡 ∧ 0 < ( 𝐴 ‘ 𝑡 ) ) )
142 imnan ⊢ ( ( ( 𝑆 ‘ 𝐴 ) < 𝑡 → ¬ 0 < ( 𝐴 ‘ 𝑡 ) ) ↔ ¬ ( ( 𝑆 ‘ 𝐴 ) < 𝑡 ∧ 0 < ( 𝐴 ‘ 𝑡 ) ) )
143 142 ralbii ⊢ ( ∀ 𝑡 ∈ ℕ ( ( 𝑆 ‘ 𝐴 ) < 𝑡 → ¬ 0 < ( 𝐴 ‘ 𝑡 ) ) ↔ ∀ 𝑡 ∈ ℕ ¬ ( ( 𝑆 ‘ 𝐴 ) < 𝑡 ∧ 0 < ( 𝐴 ‘ 𝑡 ) ) )
144 141 143 sylibr ⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ∀ 𝑡 ∈ ℕ ( ( 𝑆 ‘ 𝐴 ) < 𝑡 → ¬ 0 < ( 𝐴 ‘ 𝑡 ) ) )
145 144 r19.21bi ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) → ( ( 𝑆 ‘ 𝐴 ) < 𝑡 → ¬ 0 < ( 𝐴 ‘ 𝑡 ) ) )
146 145 imp ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ ( 𝑆 ‘ 𝐴 ) < 𝑡 ) → ¬ 0 < ( 𝐴 ‘ 𝑡 ) )
147 16 11 32 146 syl21anc ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → ¬ 0 < ( 𝐴 ‘ 𝑡 ) )
148 nn0re ⊢ ( ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 → ( 𝐴 ‘ 𝑡 ) ∈ ℝ )
149 0red ⊢ ( ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 → 0 ∈ ℝ )
150 148 149 lenltd ⊢ ( ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 → ( ( 𝐴 ‘ 𝑡 ) ≤ 0 ↔ ¬ 0 < ( 𝐴 ‘ 𝑡 ) ) )
151 nn0le0eq0 ⊢ ( ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 → ( ( 𝐴 ‘ 𝑡 ) ≤ 0 ↔ ( 𝐴 ‘ 𝑡 ) = 0 ) )
152 150 151 bitr3d ⊢ ( ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 → ( ¬ 0 < ( 𝐴 ‘ 𝑡 ) ↔ ( 𝐴 ‘ 𝑡 ) = 0 ) )
153 152 biimpa ⊢ ( ( ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 ∧ ¬ 0 < ( 𝐴 ‘ 𝑡 ) ) → ( 𝐴 ‘ 𝑡 ) = 0 )
154 15 147 153 syl2anc ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → ( 𝐴 ‘ 𝑡 ) = 0 )
155 8 154 sylbir ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℤ≥ ‘ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ) ) → ( 𝐴 ‘ 𝑡 ) = 0 )