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