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	sselid	⊢ ( ( 𝐴 ∈ ( ( ℕ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	ffvelcdmda	⊢ ( ( 𝐴 ∈ ( ( ℕ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	ffvelcdmi	⊢ ( 𝐴 ∈ ( ( ℕ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		ffvelcdm	⊢ ( ( 𝐴 : ℕ ⟶ ℕ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 ↑ 𝑛 ) · 𝑡 ) ≤ ( 𝑆 ‘ 𝐴 ) )