Step |
Hyp |
Ref |
Expression |
1 |
|
rpvmasum.z |
⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 ) |
2 |
|
rpvmasum.l |
⊢ 𝐿 = ( ℤRHom ‘ 𝑍 ) |
3 |
|
rpvmasum.a |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
4 |
|
rpvmasum2.g |
⊢ 𝐺 = ( DChr ‘ 𝑁 ) |
5 |
|
rpvmasum2.d |
⊢ 𝐷 = ( Base ‘ 𝐺 ) |
6 |
|
rpvmasum2.1 |
⊢ 1 = ( 0g ‘ 𝐺 ) |
7 |
|
rpvmasum2.w |
⊢ 𝑊 = { 𝑦 ∈ ( 𝐷 ∖ { 1 } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } |
8 |
|
rpvmasum2.u |
⊢ 𝑈 = ( Unit ‘ 𝑍 ) |
9 |
|
rpvmasum2.b |
⊢ ( 𝜑 → 𝐴 ∈ 𝑈 ) |
10 |
|
rpvmasum2.t |
⊢ 𝑇 = ( ◡ 𝐿 “ { 𝐴 } ) |
11 |
|
rpvmasum2.z1 |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑊 ) → 𝐴 = ( 1r ‘ 𝑍 ) ) |
12 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑁 ∈ ℕ ) |
13 |
4 5
|
dchrfi |
⊢ ( 𝑁 ∈ ℕ → 𝐷 ∈ Fin ) |
14 |
12 13
|
syl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐷 ∈ Fin ) |
15 |
|
fzfid |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ) |
16 |
|
eqid |
⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 ) |
17 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑓 ∈ 𝐷 ) |
18 |
4 1 5 16 17
|
dchrf |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑓 : ( Base ‘ 𝑍 ) ⟶ ℂ ) |
19 |
16 8
|
unitss |
⊢ 𝑈 ⊆ ( Base ‘ 𝑍 ) |
20 |
19 9
|
sselid |
⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝑍 ) ) |
21 |
20
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝐴 ∈ ( Base ‘ 𝑍 ) ) |
22 |
18 21
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( 𝑓 ‘ 𝐴 ) ∈ ℂ ) |
23 |
22
|
cjcld |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ∈ ℂ ) |
24 |
23
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ∈ ℂ ) |
25 |
24
|
adantrl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑓 ∈ 𝐷 ) ) → ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ∈ ℂ ) |
26 |
18
|
ad4ant14 |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → 𝑓 : ( Base ‘ 𝑍 ) ⟶ ℂ ) |
27 |
3
|
nnnn0d |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
28 |
1 16 2
|
znzrhfo |
⊢ ( 𝑁 ∈ ℕ0 → 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) ) |
29 |
|
fof |
⊢ ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ) |
30 |
27 28 29
|
3syl |
⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ) |
31 |
30
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ) |
32 |
|
elfzelz |
⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℤ ) |
33 |
|
ffvelrn |
⊢ ( ( 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ∧ 𝑛 ∈ ℤ ) → ( 𝐿 ‘ 𝑛 ) ∈ ( Base ‘ 𝑍 ) ) |
34 |
31 32 33
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐿 ‘ 𝑛 ) ∈ ( Base ‘ 𝑍 ) ) |
35 |
34
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( 𝐿 ‘ 𝑛 ) ∈ ( Base ‘ 𝑍 ) ) |
36 |
26 35
|
ffvelrnd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ ) |
37 |
36
|
anasss |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑓 ∈ 𝐷 ) ) → ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ ) |
38 |
|
elfznn |
⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ ) |
39 |
38
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ ) |
40 |
|
vmacl |
⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ ) |
41 |
39 40
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ ) |
42 |
41 39
|
nndivred |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ ) |
43 |
42
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ ) |
44 |
43
|
adantrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑓 ∈ 𝐷 ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ ) |
45 |
37 44
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑓 ∈ 𝐷 ) ) → ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ ) |
46 |
25 45
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑓 ∈ 𝐷 ) ) → ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ∈ ℂ ) |
47 |
46
|
anass1rs |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ∈ ℂ ) |
48 |
15 47
|
fsumcl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ∈ ℂ ) |
49 |
|
relogcl |
⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ ) |
50 |
49
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℝ ) |
51 |
50
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ ) |
52 |
51
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → ( log ‘ 𝑥 ) ∈ ℂ ) |
53 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
54 |
|
neg1cn |
⊢ - 1 ∈ ℂ |
55 |
|
0cn |
⊢ 0 ∈ ℂ |
56 |
54 55
|
ifcli |
⊢ if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ∈ ℂ |
57 |
53 56
|
ifcli |
⊢ if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ∈ ℂ |
58 |
|
mulcl |
⊢ ( ( ( log ‘ 𝑥 ) ∈ ℂ ∧ if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ∈ ℂ ) → ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ∈ ℂ ) |
59 |
52 57 58
|
sylancl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ∈ ℂ ) |
60 |
14 48 59
|
fsumsub |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑓 ∈ 𝐷 ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) = ( Σ 𝑓 ∈ 𝐷 Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) − Σ 𝑓 ∈ 𝐷 ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) |
61 |
45
|
anass1rs |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ ) |
62 |
15 61
|
fsumcl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ ) |
63 |
24 62 59
|
subdid |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) = ( ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) − ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) ) |
64 |
15 24 61
|
fsummulc2 |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ) |
65 |
57
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ∈ ℂ ) |
66 |
24 52 65
|
mul12d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) = ( ( log ‘ 𝑥 ) · ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) |
67 |
|
ovif2 |
⊢ ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) = if ( 𝑓 = 1 , ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · 1 ) , ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) |
68 |
|
fveq1 |
⊢ ( 𝑓 = 1 → ( 𝑓 ‘ 𝐴 ) = ( 1 ‘ 𝐴 ) ) |
69 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → 𝑁 ∈ ℕ ) |
70 |
9
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → 𝐴 ∈ 𝑈 ) |
71 |
4 1 6 8 69 70
|
dchr1 |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → ( 1 ‘ 𝐴 ) = 1 ) |
72 |
68 71
|
sylan9eqr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 = 1 ) → ( 𝑓 ‘ 𝐴 ) = 1 ) |
73 |
72
|
fveq2d |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 = 1 ) → ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) = ( ∗ ‘ 1 ) ) |
74 |
|
1re |
⊢ 1 ∈ ℝ |
75 |
|
cjre |
⊢ ( 1 ∈ ℝ → ( ∗ ‘ 1 ) = 1 ) |
76 |
74 75
|
ax-mp |
⊢ ( ∗ ‘ 1 ) = 1 |
77 |
73 76
|
eqtrdi |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 = 1 ) → ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) = 1 ) |
78 |
77
|
oveq1d |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 = 1 ) → ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · 1 ) = ( 1 · 1 ) ) |
79 |
|
1t1e1 |
⊢ ( 1 · 1 ) = 1 |
80 |
78 79
|
eqtrdi |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 = 1 ) → ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · 1 ) = 1 ) |
81 |
|
df-ne |
⊢ ( 𝑓 ≠ 1 ↔ ¬ 𝑓 = 1 ) |
82 |
|
ovif2 |
⊢ ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) = if ( 𝑓 ∈ 𝑊 , ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · - 1 ) , ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · 0 ) ) |
83 |
11
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑊 ) → ( 𝑓 ‘ 𝐴 ) = ( 𝑓 ‘ ( 1r ‘ 𝑍 ) ) ) |
84 |
83
|
ad5ant15 |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊 ) → ( 𝑓 ‘ 𝐴 ) = ( 𝑓 ‘ ( 1r ‘ 𝑍 ) ) ) |
85 |
4 1 5
|
dchrmhm |
⊢ 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) |
86 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → 𝑓 ∈ 𝐷 ) |
87 |
85 86
|
sselid |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → 𝑓 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) |
88 |
|
eqid |
⊢ ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 ) |
89 |
|
eqid |
⊢ ( 1r ‘ 𝑍 ) = ( 1r ‘ 𝑍 ) |
90 |
88 89
|
ringidval |
⊢ ( 1r ‘ 𝑍 ) = ( 0g ‘ ( mulGrp ‘ 𝑍 ) ) |
91 |
|
eqid |
⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld ) |
92 |
|
cnfld1 |
⊢ 1 = ( 1r ‘ ℂfld ) |
93 |
91 92
|
ringidval |
⊢ 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) ) |
94 |
90 93
|
mhm0 |
⊢ ( 𝑓 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) → ( 𝑓 ‘ ( 1r ‘ 𝑍 ) ) = 1 ) |
95 |
87 94
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → ( 𝑓 ‘ ( 1r ‘ 𝑍 ) ) = 1 ) |
96 |
95
|
ad2antrr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊 ) → ( 𝑓 ‘ ( 1r ‘ 𝑍 ) ) = 1 ) |
97 |
84 96
|
eqtrd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊 ) → ( 𝑓 ‘ 𝐴 ) = 1 ) |
98 |
97
|
fveq2d |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊 ) → ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) = ( ∗ ‘ 1 ) ) |
99 |
98 76
|
eqtrdi |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊 ) → ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) = 1 ) |
100 |
99
|
oveq1d |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊 ) → ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · - 1 ) = ( 1 · - 1 ) ) |
101 |
54
|
mulid2i |
⊢ ( 1 · - 1 ) = - 1 |
102 |
100 101
|
eqtrdi |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊 ) → ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · - 1 ) = - 1 ) |
103 |
102
|
ifeq1da |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) → if ( 𝑓 ∈ 𝑊 , ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · - 1 ) , ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · 0 ) ) = if ( 𝑓 ∈ 𝑊 , - 1 , ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · 0 ) ) ) |
104 |
24
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) → ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ∈ ℂ ) |
105 |
104
|
mul01d |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) → ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · 0 ) = 0 ) |
106 |
105
|
ifeq2d |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) → if ( 𝑓 ∈ 𝑊 , - 1 , ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · 0 ) ) = if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) |
107 |
103 106
|
eqtrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) → if ( 𝑓 ∈ 𝑊 , ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · - 1 ) , ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · 0 ) ) = if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) |
108 |
82 107
|
syl5eq |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) → ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) = if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) |
109 |
81 108
|
sylan2br |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ 𝑓 = 1 ) → ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) = if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) |
110 |
80 109
|
ifeq12da |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → if ( 𝑓 = 1 , ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · 1 ) , ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) = if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) |
111 |
67 110
|
syl5eq |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) = if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) |
112 |
111
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → ( ( log ‘ 𝑥 ) · ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) = ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) |
113 |
66 112
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) = ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) |
114 |
64 113
|
oveq12d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → ( ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) − ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) |
115 |
63 114
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) |
116 |
115
|
sumeq2dv |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑓 ∈ 𝐷 ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) = Σ 𝑓 ∈ 𝐷 ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) |
117 |
|
fzfid |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ) |
118 |
|
inss1 |
⊢ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) |
119 |
|
ssfi |
⊢ ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ∧ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ∈ Fin ) |
120 |
117 118 119
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ∈ Fin ) |
121 |
12
|
phicld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ϕ ‘ 𝑁 ) ∈ ℕ ) |
122 |
121
|
nncnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ϕ ‘ 𝑁 ) ∈ ℂ ) |
123 |
118
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) |
124 |
123
|
sselda |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ) → 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) |
125 |
124 43
|
syldan |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ ) |
126 |
120 122 125
|
fsummulc2 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) |
127 |
122
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ϕ ‘ 𝑁 ) ∈ ℂ ) |
128 |
127 43
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ ) |
129 |
124 128
|
syldan |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ) → ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ ) |
130 |
129
|
ralrimiva |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∀ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ ) |
131 |
117
|
olcd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ) ) |
132 |
|
sumss2 |
⊢ ( ( ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ∀ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ ) ∧ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ) ) → Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) if ( 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) , ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) , 0 ) ) |
133 |
123 130 131 132
|
syl21anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) if ( 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) , ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) , 0 ) ) |
134 |
|
elin |
⊢ ( 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ↔ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ 𝑇 ) ) |
135 |
134
|
baib |
⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → ( 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ↔ 𝑛 ∈ 𝑇 ) ) |
136 |
135
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ↔ 𝑛 ∈ 𝑇 ) ) |
137 |
10
|
eleq2i |
⊢ ( 𝑛 ∈ 𝑇 ↔ 𝑛 ∈ ( ◡ 𝐿 “ { 𝐴 } ) ) |
138 |
31
|
ffnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐿 Fn ℤ ) |
139 |
|
fniniseg |
⊢ ( 𝐿 Fn ℤ → ( 𝑛 ∈ ( ◡ 𝐿 “ { 𝐴 } ) ↔ ( 𝑛 ∈ ℤ ∧ ( 𝐿 ‘ 𝑛 ) = 𝐴 ) ) ) |
140 |
139
|
baibd |
⊢ ( ( 𝐿 Fn ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑛 ∈ ( ◡ 𝐿 “ { 𝐴 } ) ↔ ( 𝐿 ‘ 𝑛 ) = 𝐴 ) ) |
141 |
138 32 140
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 ∈ ( ◡ 𝐿 “ { 𝐴 } ) ↔ ( 𝐿 ‘ 𝑛 ) = 𝐴 ) ) |
142 |
137 141
|
syl5bb |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 ∈ 𝑇 ↔ ( 𝐿 ‘ 𝑛 ) = 𝐴 ) ) |
143 |
136 142
|
bitr2d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝐿 ‘ 𝑛 ) = 𝐴 ↔ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ) ) |
144 |
43
|
mul02d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 0 · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = 0 ) |
145 |
143 144
|
ifbieq2d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → if ( ( 𝐿 ‘ 𝑛 ) = 𝐴 , ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) , ( 0 · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) = if ( 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) , ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) , 0 ) ) |
146 |
|
ovif |
⊢ ( if ( ( 𝐿 ‘ 𝑛 ) = 𝐴 , ( ϕ ‘ 𝑁 ) , 0 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = if ( ( 𝐿 ‘ 𝑛 ) = 𝐴 , ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) , ( 0 · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) |
147 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑁 ∈ ℕ ) |
148 |
147 13
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐷 ∈ Fin ) |
149 |
23
|
ad4ant14 |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ∈ ℂ ) |
150 |
36 149
|
mulcld |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ) ∈ ℂ ) |
151 |
148 43 150
|
fsummulc1 |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑓 ∈ 𝐷 ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑓 ∈ 𝐷 ( ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) |
152 |
9
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐴 ∈ 𝑈 ) |
153 |
4 5 1 16 8 147 34 152
|
sum2dchr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑓 ∈ 𝐷 ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ) = if ( ( 𝐿 ‘ 𝑛 ) = 𝐴 , ( ϕ ‘ 𝑁 ) , 0 ) ) |
154 |
153
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑓 ∈ 𝐷 ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = ( if ( ( 𝐿 ‘ 𝑛 ) = 𝐴 , ( ϕ ‘ 𝑁 ) , 0 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) |
155 |
43
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ ) |
156 |
|
mulass |
⊢ ( ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ ∧ ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ∈ ℂ ∧ ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ ) → ( ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ) |
157 |
|
mul12 |
⊢ ( ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ ∧ ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ∈ ℂ ∧ ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ ) → ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) = ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ) |
158 |
156 157
|
eqtrd |
⊢ ( ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ ∧ ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ∈ ℂ ∧ ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ ) → ( ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ) |
159 |
36 149 155 158
|
syl3anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ) |
160 |
159
|
sumeq2dv |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑓 ∈ 𝐷 ( ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑓 ∈ 𝐷 ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ) |
161 |
151 154 160
|
3eqtr3d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( if ( ( 𝐿 ‘ 𝑛 ) = 𝐴 , ( ϕ ‘ 𝑁 ) , 0 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑓 ∈ 𝐷 ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ) |
162 |
146 161
|
eqtr3id |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → if ( ( 𝐿 ‘ 𝑛 ) = 𝐴 , ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) , ( 0 · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) = Σ 𝑓 ∈ 𝐷 ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ) |
163 |
145 162
|
eqtr3d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → if ( 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) , ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) , 0 ) = Σ 𝑓 ∈ 𝐷 ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ) |
164 |
163
|
sumeq2dv |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) if ( 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) , ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) , 0 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑓 ∈ 𝐷 ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ) |
165 |
126 133 164
|
3eqtrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑓 ∈ 𝐷 ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ) |
166 |
117 14 46
|
fsumcom |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑓 ∈ 𝐷 ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) = Σ 𝑓 ∈ 𝐷 Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ) |
167 |
165 166
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑓 ∈ 𝐷 Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ) |
168 |
4
|
dchrabl |
⊢ ( 𝑁 ∈ ℕ → 𝐺 ∈ Abel ) |
169 |
|
ablgrp |
⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp ) |
170 |
5 6
|
grpidcl |
⊢ ( 𝐺 ∈ Grp → 1 ∈ 𝐷 ) |
171 |
12 168 169 170
|
4syl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 1 ∈ 𝐷 ) |
172 |
51
|
mulid1d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · 1 ) = ( log ‘ 𝑥 ) ) |
173 |
172 51
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · 1 ) ∈ ℂ ) |
174 |
|
iftrue |
⊢ ( 𝑓 = 1 → if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) = 1 ) |
175 |
174
|
oveq2d |
⊢ ( 𝑓 = 1 → ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) = ( ( log ‘ 𝑥 ) · 1 ) ) |
176 |
175
|
sumsn |
⊢ ( ( 1 ∈ 𝐷 ∧ ( ( log ‘ 𝑥 ) · 1 ) ∈ ℂ ) → Σ 𝑓 ∈ { 1 } ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) = ( ( log ‘ 𝑥 ) · 1 ) ) |
177 |
171 173 176
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑓 ∈ { 1 } ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) = ( ( log ‘ 𝑥 ) · 1 ) ) |
178 |
|
eldifsn |
⊢ ( 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ↔ ( 𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 ) ) |
179 |
|
ifnefalse |
⊢ ( 𝑓 ≠ 1 → if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) = if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) |
180 |
179
|
ad2antll |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 ) ) → if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) = if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) |
181 |
|
negeq |
⊢ ( if ( 𝑓 ∈ 𝑊 , 1 , 0 ) = 1 → - if ( 𝑓 ∈ 𝑊 , 1 , 0 ) = - 1 ) |
182 |
|
negeq |
⊢ ( if ( 𝑓 ∈ 𝑊 , 1 , 0 ) = 0 → - if ( 𝑓 ∈ 𝑊 , 1 , 0 ) = - 0 ) |
183 |
|
neg0 |
⊢ - 0 = 0 |
184 |
182 183
|
eqtrdi |
⊢ ( if ( 𝑓 ∈ 𝑊 , 1 , 0 ) = 0 → - if ( 𝑓 ∈ 𝑊 , 1 , 0 ) = 0 ) |
185 |
181 184
|
ifsb |
⊢ - if ( 𝑓 ∈ 𝑊 , 1 , 0 ) = if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) |
186 |
180 185
|
eqtr4di |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 ) ) → if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) = - if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ) |
187 |
186
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 ) ) → ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) = ( ( log ‘ 𝑥 ) · - if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ) ) |
188 |
51
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 ) ) → ( log ‘ 𝑥 ) ∈ ℂ ) |
189 |
53 55
|
ifcli |
⊢ if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ∈ ℂ |
190 |
|
mulneg2 |
⊢ ( ( ( log ‘ 𝑥 ) ∈ ℂ ∧ if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ∈ ℂ ) → ( ( log ‘ 𝑥 ) · - if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ) = - ( ( log ‘ 𝑥 ) · if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ) ) |
191 |
188 189 190
|
sylancl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 ) ) → ( ( log ‘ 𝑥 ) · - if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ) = - ( ( log ‘ 𝑥 ) · if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ) ) |
192 |
187 191
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 ) ) → ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) = - ( ( log ‘ 𝑥 ) · if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ) ) |
193 |
178 192
|
sylan2b |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ) → ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) = - ( ( log ‘ 𝑥 ) · if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ) ) |
194 |
193
|
sumeq2dv |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) = Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) - ( ( log ‘ 𝑥 ) · if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ) ) |
195 |
|
diffi |
⊢ ( 𝐷 ∈ Fin → ( 𝐷 ∖ { 1 } ) ∈ Fin ) |
196 |
14 195
|
syl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝐷 ∖ { 1 } ) ∈ Fin ) |
197 |
51
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ) → ( log ‘ 𝑥 ) ∈ ℂ ) |
198 |
|
mulcl |
⊢ ( ( ( log ‘ 𝑥 ) ∈ ℂ ∧ if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ∈ ℂ ) → ( ( log ‘ 𝑥 ) · if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ) ∈ ℂ ) |
199 |
197 189 198
|
sylancl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ) → ( ( log ‘ 𝑥 ) · if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ) ∈ ℂ ) |
200 |
196 199
|
fsumneg |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) - ( ( log ‘ 𝑥 ) · if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ) = - Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ( ( log ‘ 𝑥 ) · if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ) ) |
201 |
189
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ) → if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ∈ ℂ ) |
202 |
196 51 201
|
fsummulc2 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ) = Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ( ( log ‘ 𝑥 ) · if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ) ) |
203 |
7
|
ssrab3 |
⊢ 𝑊 ⊆ ( 𝐷 ∖ { 1 } ) |
204 |
|
difss |
⊢ ( 𝐷 ∖ { 1 } ) ⊆ 𝐷 |
205 |
203 204
|
sstri |
⊢ 𝑊 ⊆ 𝐷 |
206 |
|
ssfi |
⊢ ( ( 𝐷 ∈ Fin ∧ 𝑊 ⊆ 𝐷 ) → 𝑊 ∈ Fin ) |
207 |
14 205 206
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑊 ∈ Fin ) |
208 |
|
fsumconst |
⊢ ( ( 𝑊 ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑓 ∈ 𝑊 1 = ( ( ♯ ‘ 𝑊 ) · 1 ) ) |
209 |
207 53 208
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑓 ∈ 𝑊 1 = ( ( ♯ ‘ 𝑊 ) · 1 ) ) |
210 |
203
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑊 ⊆ ( 𝐷 ∖ { 1 } ) ) |
211 |
53
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 1 ∈ ℂ ) |
212 |
211
|
ralrimivw |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∀ 𝑓 ∈ 𝑊 1 ∈ ℂ ) |
213 |
196
|
olcd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐷 ∖ { 1 } ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( 𝐷 ∖ { 1 } ) ∈ Fin ) ) |
214 |
|
sumss2 |
⊢ ( ( ( 𝑊 ⊆ ( 𝐷 ∖ { 1 } ) ∧ ∀ 𝑓 ∈ 𝑊 1 ∈ ℂ ) ∧ ( ( 𝐷 ∖ { 1 } ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( 𝐷 ∖ { 1 } ) ∈ Fin ) ) → Σ 𝑓 ∈ 𝑊 1 = Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ) |
215 |
210 212 213 214
|
syl21anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑓 ∈ 𝑊 1 = Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ) |
216 |
|
hashcl |
⊢ ( 𝑊 ∈ Fin → ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) |
217 |
207 216
|
syl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) |
218 |
217
|
nn0cnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ♯ ‘ 𝑊 ) ∈ ℂ ) |
219 |
218
|
mulid1d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ♯ ‘ 𝑊 ) · 1 ) = ( ♯ ‘ 𝑊 ) ) |
220 |
209 215 219
|
3eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) if ( 𝑓 ∈ 𝑊 , 1 , 0 ) = ( ♯ ‘ 𝑊 ) ) |
221 |
220
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ) = ( ( log ‘ 𝑥 ) · ( ♯ ‘ 𝑊 ) ) ) |
222 |
202 221
|
eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ( ( log ‘ 𝑥 ) · if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ) = ( ( log ‘ 𝑥 ) · ( ♯ ‘ 𝑊 ) ) ) |
223 |
222
|
negeqd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → - Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ( ( log ‘ 𝑥 ) · if ( 𝑓 ∈ 𝑊 , 1 , 0 ) ) = - ( ( log ‘ 𝑥 ) · ( ♯ ‘ 𝑊 ) ) ) |
224 |
194 200 223
|
3eqtrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) = - ( ( log ‘ 𝑥 ) · ( ♯ ‘ 𝑊 ) ) ) |
225 |
177 224
|
oveq12d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑓 ∈ { 1 } ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) + Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) = ( ( ( log ‘ 𝑥 ) · 1 ) + - ( ( log ‘ 𝑥 ) · ( ♯ ‘ 𝑊 ) ) ) ) |
226 |
51 218
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · ( ♯ ‘ 𝑊 ) ) ∈ ℂ ) |
227 |
173 226
|
negsubd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( log ‘ 𝑥 ) · 1 ) + - ( ( log ‘ 𝑥 ) · ( ♯ ‘ 𝑊 ) ) ) = ( ( ( log ‘ 𝑥 ) · 1 ) − ( ( log ‘ 𝑥 ) · ( ♯ ‘ 𝑊 ) ) ) ) |
228 |
225 227
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑓 ∈ { 1 } ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) + Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) = ( ( ( log ‘ 𝑥 ) · 1 ) − ( ( log ‘ 𝑥 ) · ( ♯ ‘ 𝑊 ) ) ) ) |
229 |
|
disjdif |
⊢ ( { 1 } ∩ ( 𝐷 ∖ { 1 } ) ) = ∅ |
230 |
229
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( { 1 } ∩ ( 𝐷 ∖ { 1 } ) ) = ∅ ) |
231 |
|
undif2 |
⊢ ( { 1 } ∪ ( 𝐷 ∖ { 1 } ) ) = ( { 1 } ∪ 𝐷 ) |
232 |
171
|
snssd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → { 1 } ⊆ 𝐷 ) |
233 |
|
ssequn1 |
⊢ ( { 1 } ⊆ 𝐷 ↔ ( { 1 } ∪ 𝐷 ) = 𝐷 ) |
234 |
232 233
|
sylib |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( { 1 } ∪ 𝐷 ) = 𝐷 ) |
235 |
231 234
|
eqtr2id |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐷 = ( { 1 } ∪ ( 𝐷 ∖ { 1 } ) ) ) |
236 |
230 235 14 59
|
fsumsplit |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑓 ∈ 𝐷 ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) = ( Σ 𝑓 ∈ { 1 } ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) + Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) |
237 |
51 211 218
|
subdid |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) = ( ( ( log ‘ 𝑥 ) · 1 ) − ( ( log ‘ 𝑥 ) · ( ♯ ‘ 𝑊 ) ) ) ) |
238 |
228 236 237
|
3eqtr4rd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) = Σ 𝑓 ∈ 𝐷 ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) |
239 |
167 238
|
oveq12d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) = ( Σ 𝑓 ∈ 𝐷 Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) − Σ 𝑓 ∈ 𝐷 ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) |
240 |
60 116 239
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑓 ∈ 𝐷 ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) = ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) |
241 |
240
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑓 ∈ 𝐷 ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) ) |
242 |
|
rpssre |
⊢ ℝ+ ⊆ ℝ |
243 |
242
|
a1i |
⊢ ( 𝜑 → ℝ+ ⊆ ℝ ) |
244 |
3 13
|
syl |
⊢ ( 𝜑 → 𝐷 ∈ Fin ) |
245 |
22
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → ( 𝑓 ‘ 𝐴 ) ∈ ℂ ) |
246 |
245
|
cjcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ∈ ℂ ) |
247 |
62 59
|
subcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ∈ ℂ ) |
248 |
246 247
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) ∈ ℂ ) |
249 |
248
|
anasss |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑓 ∈ 𝐷 ) ) → ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) ∈ ℂ ) |
250 |
23
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ∈ ℂ ) |
251 |
247
|
an32s |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ∈ ℂ ) |
252 |
|
o1const |
⊢ ( ( ℝ+ ⊆ ℝ ∧ ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ) ∈ 𝑂(1) ) |
253 |
242 23 252
|
sylancr |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( 𝑥 ∈ ℝ+ ↦ ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) ) ∈ 𝑂(1) ) |
254 |
|
fveq1 |
⊢ ( 𝑓 = 1 → ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) = ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) |
255 |
254
|
oveq1d |
⊢ ( 𝑓 = 1 → ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) |
256 |
255
|
sumeq2sdv |
⊢ ( 𝑓 = 1 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) |
257 |
256 175
|
oveq12d |
⊢ ( 𝑓 = 1 → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · 1 ) ) ) |
258 |
257
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 = 1 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · 1 ) ) ) |
259 |
49
|
recnd |
⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℂ ) |
260 |
259
|
mulid1d |
⊢ ( 𝑥 ∈ ℝ+ → ( ( log ‘ 𝑥 ) · 1 ) = ( log ‘ 𝑥 ) ) |
261 |
260
|
oveq2d |
⊢ ( 𝑥 ∈ ℝ+ → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · 1 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) ) |
262 |
258 261
|
sylan9eq |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 = 1 ) ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) ) |
263 |
262
|
mpteq2dva |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 = 1 ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) ) ) |
264 |
1 2 3 4 5 6
|
rpvmasumlem |
⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) |
265 |
264
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 = 1 ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) |
266 |
263 265
|
eqeltrd |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 = 1 ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) ∈ 𝑂(1) ) |
267 |
179
|
oveq2d |
⊢ ( 𝑓 ≠ 1 → ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) = ( ( log ‘ 𝑥 ) · if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) |
268 |
267
|
oveq2d |
⊢ ( 𝑓 ≠ 1 → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) |
269 |
51
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ ) |
270 |
|
mulcom |
⊢ ( ( ( log ‘ 𝑥 ) ∈ ℂ ∧ - 1 ∈ ℂ ) → ( ( log ‘ 𝑥 ) · - 1 ) = ( - 1 · ( log ‘ 𝑥 ) ) ) |
271 |
269 54 270
|
sylancl |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · - 1 ) = ( - 1 · ( log ‘ 𝑥 ) ) ) |
272 |
269
|
mulm1d |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( - 1 · ( log ‘ 𝑥 ) ) = - ( log ‘ 𝑥 ) ) |
273 |
271 272
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · - 1 ) = - ( log ‘ 𝑥 ) ) |
274 |
269
|
mul01d |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · 0 ) = 0 ) |
275 |
273 274
|
ifeq12d |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → if ( 𝑓 ∈ 𝑊 , ( ( log ‘ 𝑥 ) · - 1 ) , ( ( log ‘ 𝑥 ) · 0 ) ) = if ( 𝑓 ∈ 𝑊 , - ( log ‘ 𝑥 ) , 0 ) ) |
276 |
|
ovif2 |
⊢ ( ( log ‘ 𝑥 ) · if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) = if ( 𝑓 ∈ 𝑊 , ( ( log ‘ 𝑥 ) · - 1 ) , ( ( log ‘ 𝑥 ) · 0 ) ) |
277 |
|
negeq |
⊢ ( if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) = ( log ‘ 𝑥 ) → - if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) = - ( log ‘ 𝑥 ) ) |
278 |
|
negeq |
⊢ ( if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) = 0 → - if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) = - 0 ) |
279 |
278 183
|
eqtrdi |
⊢ ( if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) = 0 → - if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) = 0 ) |
280 |
277 279
|
ifsb |
⊢ - if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) = if ( 𝑓 ∈ 𝑊 , - ( log ‘ 𝑥 ) , 0 ) |
281 |
275 276 280
|
3eqtr4g |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) = - if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) ) |
282 |
281
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − - if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) ) ) |
283 |
62
|
an32s |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ ) |
284 |
|
ifcl |
⊢ ( ( ( log ‘ 𝑥 ) ∈ ℂ ∧ 0 ∈ ℂ ) → if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) ∈ ℂ ) |
285 |
269 55 284
|
sylancl |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) ∈ ℂ ) |
286 |
283 285
|
subnegd |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − - if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) ) ) |
287 |
282 286
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) ) ) |
288 |
268 287
|
sylan9eqr |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ≠ 1 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) ) ) |
289 |
288
|
an32s |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) ) ) |
290 |
289
|
mpteq2dva |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) ) ) ) |
291 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) → 𝑁 ∈ ℕ ) |
292 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) → 𝑓 ∈ 𝐷 ) |
293 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) → 𝑓 ≠ 1 ) |
294 |
|
eqid |
⊢ ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) = ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) |
295 |
1 2 291 4 5 6 292 293 294
|
dchrmusumlema |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) → ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) |
296 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑁 ∈ ℕ ) |
297 |
296
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑁 ∈ ℕ ) |
298 |
292
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑓 ∈ 𝐷 ) |
299 |
|
simplr |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑓 ≠ 1 ) |
300 |
|
simprl |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑐 ∈ ( 0 [,) +∞ ) ) |
301 |
|
simprrl |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ) |
302 |
|
simprrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) |
303 |
1 2 297 4 5 6 298 299 294 300 301 302 7
|
dchrvmaeq0 |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → ( 𝑓 ∈ 𝑊 ↔ 𝑡 = 0 ) ) |
304 |
|
ifbi |
⊢ ( ( 𝑓 ∈ 𝑊 ↔ 𝑡 = 0 ) → if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) = if ( 𝑡 = 0 , ( log ‘ 𝑥 ) , 0 ) ) |
305 |
304
|
oveq2d |
⊢ ( ( 𝑓 ∈ 𝑊 ↔ 𝑡 = 0 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑡 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) |
306 |
305
|
mpteq2dv |
⊢ ( ( 𝑓 ∈ 𝑊 ↔ 𝑡 = 0 ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑡 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) ) |
307 |
303 306
|
syl |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑡 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) ) |
308 |
1 2 297 4 5 6 298 299 294 300 301 302
|
dchrvmasumif |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑡 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) ) |
309 |
307 308
|
eqeltrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) ) |
310 |
309
|
rexlimdvaa |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) → ( ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) ) ) |
311 |
310
|
exlimdv |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) → ( ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) ) ) |
312 |
295 311
|
mpd |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓 ∈ 𝑊 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) ) |
313 |
290 312
|
eqeltrd |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ≠ 1 ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) ∈ 𝑂(1) ) |
314 |
266 313
|
pm2.61dane |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) ∈ 𝑂(1) ) |
315 |
250 251 253 314
|
o1mul2 |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( 𝑥 ∈ ℝ+ ↦ ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) ) ∈ 𝑂(1) ) |
316 |
243 244 249 315
|
fsumo1 |
⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑓 ∈ 𝐷 ( ( ∗ ‘ ( 𝑓 ‘ 𝐴 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓 ∈ 𝑊 , - 1 , 0 ) ) ) ) ) ) ∈ 𝑂(1) ) |
317 |
241 316
|
eqeltrrd |
⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) ∈ 𝑂(1) ) |