Metamath Proof Explorer

Theorem eulerpartlemgc

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 9-Aug-2018)

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

Proof

Step Hyp Ref Expression
1 eulerpartlems.r ⊢ 𝑅 = { 𝑓 ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2 eulerpartlems.s ⊢ 𝑆 = ( 𝑓 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ↦ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) )
3 2re ⊢ 2 ∈ ℝ
4 3 a1i ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → 2 ∈ ℝ )
5 bitsss ⊢ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ⊆ ℕ0
6 simprr ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) )
7 5 6 sseldi ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → 𝑛 ∈ ℕ0 )
8 4 7 reexpcld ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( 2 ↑ 𝑛 ) ∈ ℝ )
9 simprl ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → 𝑡 ∈ ℕ )
10 9 nnred ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → 𝑡 ∈ ℝ )
11 8 10 remulcld ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( ( 2 ↑ 𝑛 ) · 𝑡 ) ∈ ℝ )
12 1 2 eulerpartlemelr ⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ) )
13 12 simpld ⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → 𝐴 : ℕ ⟶ ℕ0 )
14 13 ffvelrnda ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) → ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 )
15 14 adantrr ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 )
16 15 nn0red ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( 𝐴 ‘ 𝑡 ) ∈ ℝ )
17 16 10 remulcld ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ∈ ℝ )
18 1 2 eulerpartlemsf ⊢ 𝑆 : ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ⟶ ℕ0
19 18 ffvelrni ⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 )
20 19 adantr ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 )
21 20 nn0red ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( 𝑆 ‘ 𝐴 ) ∈ ℝ )
22 14 nn0red ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) → ( 𝐴 ‘ 𝑡 ) ∈ ℝ )
23 22 adantrr ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( 𝐴 ‘ 𝑡 ) ∈ ℝ )
24 9 nnrpd ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → 𝑡 ∈ ℝ+ )
25 24 rprege0d ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( 𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ) )
26 bitsfi ⊢ ( ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 → ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ∈ Fin )
27 15 26 syl ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ∈ Fin )
28 3 a1i ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ∧ 𝑖 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) → 2 ∈ ℝ )
29 5 a1i ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ⊆ ℕ0 )
30 29 sselda ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ∧ 𝑖 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) → 𝑖 ∈ ℕ0 )
31 28 30 reexpcld ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ∧ 𝑖 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) → ( 2 ↑ 𝑖 ) ∈ ℝ )
32 0le2 ⊢ 0 ≤ 2
33 32 a1i ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ∧ 𝑖 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) → 0 ≤ 2 )
34 28 30 33 expge0d ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ∧ 𝑖 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) → 0 ≤ ( 2 ↑ 𝑖 ) )
35 6 snssd ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → { 𝑛 } ⊆ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) )
36 27 31 34 35 fsumless ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → Σ 𝑖 ∈ { 𝑛 } ( 2 ↑ 𝑖 ) ≤ Σ 𝑖 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( 2 ↑ 𝑖 ) )
37 8 recnd ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( 2 ↑ 𝑛 ) ∈ ℂ )
38 oveq2 ⊢ ( 𝑖 = 𝑛 → ( 2 ↑ 𝑖 ) = ( 2 ↑ 𝑛 ) )
39 38 sumsn ⊢ ( ( 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ∧ ( 2 ↑ 𝑛 ) ∈ ℂ ) → Σ 𝑖 ∈ { 𝑛 } ( 2 ↑ 𝑖 ) = ( 2 ↑ 𝑛 ) )
40 6 37 39 syl2anc ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → Σ 𝑖 ∈ { 𝑛 } ( 2 ↑ 𝑖 ) = ( 2 ↑ 𝑛 ) )
41 bitsinv1 ⊢ ( ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 → Σ 𝑖 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( 2 ↑ 𝑖 ) = ( 𝐴 ‘ 𝑡 ) )
42 15 41 syl ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → Σ 𝑖 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( 2 ↑ 𝑖 ) = ( 𝐴 ‘ 𝑡 ) )
43 36 40 42 3brtr3d ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( 2 ↑ 𝑛 ) ≤ ( 𝐴 ‘ 𝑡 ) )
44 lemul1a ⊢ ( ( ( ( 2 ↑ 𝑛 ) ∈ ℝ ∧ ( 𝐴 ‘ 𝑡 ) ∈ ℝ ∧ ( 𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ) ) ∧ ( 2 ↑ 𝑛 ) ≤ ( 𝐴 ‘ 𝑡 ) ) → ( ( 2 ↑ 𝑛 ) · 𝑡 ) ≤ ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) )
45 8 23 25 43 44 syl31anc ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( ( 2 ↑ 𝑛 ) · 𝑡 ) ≤ ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) )
46 fzfid ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ∈ Fin )
47 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) → 𝑘 ∈ ℕ )
48 ffvelrn ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ‘ 𝑘 ) ∈ ℕ0 )
49 13 47 48 syl2an ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℕ0 )
50 49 nn0red ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
51 47 adantl ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → 𝑘 ∈ ℕ )
52 51 nnred ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → 𝑘 ∈ ℝ )
53 50 52 remulcld ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) ∈ ℝ )
54 53 adantlr ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) ∈ ℝ )
55 49 nn0ge0d ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → 0 ≤ ( 𝐴 ‘ 𝑘 ) )
56 0red ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → 0 ∈ ℝ )
57 51 nngt0d ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → 0 < 𝑘 )
58 56 52 57 ltled ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → 0 ≤ 𝑘 )
59 50 52 55 58 mulge0d ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → 0 ≤ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
60 59 adantlr ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → 0 ≤ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
61 fveq2 ⊢ ( 𝑘 = 𝑡 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑡 ) )
62 id ⊢ ( 𝑘 = 𝑡 → 𝑘 = 𝑡 )
63 61 62 oveq12d ⊢ ( 𝑘 = 𝑡 → ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) )
64 simpr ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → 𝑡 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) )
65 46 54 60 63 64 fsumge1 ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ≤ Σ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
66 65 adantlr ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ 𝑡 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ≤ Σ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
67 eldif ⊢ ( 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ↔ ( 𝑡 ∈ ℕ ∧ ¬ 𝑡 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) )
68 nndiffz1 ⊢ ( ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 → ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) = ( ℤ≥ ‘ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ) )
69 68 eleq2d ⊢ ( ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 → ( 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ↔ 𝑡 ∈ ( ℤ≥ ‘ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ) ) )
70 19 69 syl ⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ↔ 𝑡 ∈ ( ℤ≥ ‘ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ) ) )
71 70 pm5.32i ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) ↔ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℤ≥ ‘ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ) ) )
72 1 2 eulerpartlems ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℤ≥ ‘ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ) ) → ( 𝐴 ‘ 𝑡 ) = 0 )
73 71 72 sylbi ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → ( 𝐴 ‘ 𝑡 ) = 0 )
74 73 oveq1d ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) = ( 0 · 𝑡 ) )
75 simpr ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) )
76 75 eldifad ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → 𝑡 ∈ ℕ )
77 76 nncnd ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → 𝑡 ∈ ℂ )
78 77 mul02d ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → ( 0 · 𝑡 ) = 0 )
79 74 78 eqtrd ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) = 0 )
80 fzfid ⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ∈ Fin )
81 80 53 59 fsumge0 ⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → 0 ≤ Σ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
82 81 adantr ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → 0 ≤ Σ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
83 79 82 eqbrtrd ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ≤ Σ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
84 67 83 sylan2br ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ ¬ 𝑡 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ≤ Σ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
85 84 anassrs ⊢ ( ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) ∧ ¬ 𝑡 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ≤ Σ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
86 66 85 pm2.61dan ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) → ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ≤ Σ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
87 1 2 eulerpartlemsv3 ⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ 𝐴 ) = Σ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
88 87 adantr ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) → ( 𝑆 ‘ 𝐴 ) = Σ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
89 86 88 breqtrrd ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) → ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ≤ ( 𝑆 ‘ 𝐴 ) )
90 89 adantrr ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ≤ ( 𝑆 ‘ 𝐴 ) )
91 11 17 21 45 90 letrd ⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ ( 𝑡 ∈ ℕ ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( ( 2 ↑ 𝑛 ) · 𝑡 ) ≤ ( 𝑆 ‘ 𝐴 ) )