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 |
|
dchrisum0.b |
⊢ ( 𝜑 → 𝑋 ∈ 𝑊 ) |
9 |
|
eqid |
⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 ) |
10 |
7
|
ssrab3 |
⊢ 𝑊 ⊆ ( 𝐷 ∖ { 1 } ) |
11 |
10 8
|
sselid |
⊢ ( 𝜑 → 𝑋 ∈ ( 𝐷 ∖ { 1 } ) ) |
12 |
11
|
eldifad |
⊢ ( 𝜑 → 𝑋 ∈ 𝐷 ) |
13 |
4 1 5 9 12
|
dchrf |
⊢ ( 𝜑 → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ ) |
14 |
13
|
ffnd |
⊢ ( 𝜑 → 𝑋 Fn ( Base ‘ 𝑍 ) ) |
15 |
13
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( 𝑋 ‘ 𝑥 ) ∈ ℂ ) |
16 |
|
fvco3 |
⊢ ( ( 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ ∧ 𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) = ( ∗ ‘ ( 𝑋 ‘ 𝑥 ) ) ) |
17 |
13 16
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) = ( ∗ ‘ ( 𝑋 ‘ 𝑥 ) ) ) |
18 |
|
logno1 |
⊢ ¬ ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) |
19 |
|
1red |
⊢ ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) → 1 ∈ ℝ ) |
20 |
|
eqid |
⊢ ( Unit ‘ 𝑍 ) = ( Unit ‘ 𝑍 ) |
21 |
3
|
nnnn0d |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
22 |
1
|
zncrng |
⊢ ( 𝑁 ∈ ℕ0 → 𝑍 ∈ CRing ) |
23 |
21 22
|
syl |
⊢ ( 𝜑 → 𝑍 ∈ CRing ) |
24 |
|
crngring |
⊢ ( 𝑍 ∈ CRing → 𝑍 ∈ Ring ) |
25 |
23 24
|
syl |
⊢ ( 𝜑 → 𝑍 ∈ Ring ) |
26 |
|
eqid |
⊢ ( 1r ‘ 𝑍 ) = ( 1r ‘ 𝑍 ) |
27 |
20 26
|
1unit |
⊢ ( 𝑍 ∈ Ring → ( 1r ‘ 𝑍 ) ∈ ( Unit ‘ 𝑍 ) ) |
28 |
25 27
|
syl |
⊢ ( 𝜑 → ( 1r ‘ 𝑍 ) ∈ ( Unit ‘ 𝑍 ) ) |
29 |
|
eqid |
⊢ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) = ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) |
30 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑊 ) → ( 1r ‘ 𝑍 ) = ( 1r ‘ 𝑍 ) ) |
31 |
1 2 3 4 5 6 7 20 28 29 30
|
rpvmasum2 |
⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) ∈ 𝑂(1) ) |
32 |
31
|
adantr |
⊢ ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) ∈ 𝑂(1) ) |
33 |
3
|
phicld |
⊢ ( 𝜑 → ( ϕ ‘ 𝑁 ) ∈ ℕ ) |
34 |
33
|
nnnn0d |
⊢ ( 𝜑 → ( ϕ ‘ 𝑁 ) ∈ ℕ0 ) |
35 |
34
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ϕ ‘ 𝑁 ) ∈ ℕ0 ) |
36 |
35
|
nn0red |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ϕ ‘ 𝑁 ) ∈ ℝ ) |
37 |
|
fzfid |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ) |
38 |
|
inss1 |
⊢ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) |
39 |
|
ssfi |
⊢ ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ∧ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ∈ Fin ) |
40 |
37 38 39
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ∈ Fin ) |
41 |
|
elinel1 |
⊢ ( 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) → 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) |
42 |
|
elfznn |
⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ ) |
43 |
42
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ ) |
44 |
41 43
|
sylan2 |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ) → 𝑛 ∈ ℕ ) |
45 |
|
vmacl |
⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ ) |
46 |
|
nndivre |
⊢ ( ( ( Λ ‘ 𝑛 ) ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ ) |
47 |
45 46
|
mpancom |
⊢ ( 𝑛 ∈ ℕ → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ ) |
48 |
44 47
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ ) |
49 |
40 48
|
fsumrecl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ ) |
50 |
36 49
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℝ ) |
51 |
|
relogcl |
⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ ) |
52 |
51
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℝ ) |
53 |
|
1re |
⊢ 1 ∈ ℝ |
54 |
4 5
|
dchrfi |
⊢ ( 𝑁 ∈ ℕ → 𝐷 ∈ Fin ) |
55 |
3 54
|
syl |
⊢ ( 𝜑 → 𝐷 ∈ Fin ) |
56 |
|
difss |
⊢ ( 𝐷 ∖ { 1 } ) ⊆ 𝐷 |
57 |
10 56
|
sstri |
⊢ 𝑊 ⊆ 𝐷 |
58 |
|
ssfi |
⊢ ( ( 𝐷 ∈ Fin ∧ 𝑊 ⊆ 𝐷 ) → 𝑊 ∈ Fin ) |
59 |
55 57 58
|
sylancl |
⊢ ( 𝜑 → 𝑊 ∈ Fin ) |
60 |
|
hashcl |
⊢ ( 𝑊 ∈ Fin → ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) |
61 |
59 60
|
syl |
⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) |
62 |
61
|
nn0red |
⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℝ ) |
63 |
|
resubcl |
⊢ ( ( 1 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) → ( 1 − ( ♯ ‘ 𝑊 ) ) ∈ ℝ ) |
64 |
53 62 63
|
sylancr |
⊢ ( 𝜑 → ( 1 − ( ♯ ‘ 𝑊 ) ) ∈ ℝ ) |
65 |
64
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 − ( ♯ ‘ 𝑊 ) ) ∈ ℝ ) |
66 |
52 65
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ∈ ℝ ) |
67 |
50 66
|
resubcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ∈ ℝ ) |
68 |
67
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ∈ ℂ ) |
69 |
68
|
adantlr |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ∈ ℂ ) |
70 |
51
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℝ ) |
71 |
70
|
recnd |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ ) |
72 |
51
|
ad2antrl |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( log ‘ 𝑥 ) ∈ ℝ ) |
73 |
66
|
ad2ant2r |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ∈ ℝ ) |
74 |
72 73
|
readdcld |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) + ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ∈ ℝ ) |
75 |
|
0red |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 0 ∈ ℝ ) |
76 |
50
|
ad2ant2r |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℝ ) |
77 |
|
2re |
⊢ 2 ∈ ℝ |
78 |
77
|
a1i |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 2 ∈ ℝ ) |
79 |
62
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℝ ) |
80 |
78 79
|
resubcld |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 2 − ( ♯ ‘ 𝑊 ) ) ∈ ℝ ) |
81 |
|
log1 |
⊢ ( log ‘ 1 ) = 0 |
82 |
|
simprr |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ≤ 𝑥 ) |
83 |
|
1rp |
⊢ 1 ∈ ℝ+ |
84 |
|
simprl |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ+ ) |
85 |
|
logleb |
⊢ ( ( 1 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → ( 1 ≤ 𝑥 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝑥 ) ) ) |
86 |
83 84 85
|
sylancr |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 1 ≤ 𝑥 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝑥 ) ) ) |
87 |
82 86
|
mpbid |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( log ‘ 1 ) ≤ ( log ‘ 𝑥 ) ) |
88 |
81 87
|
eqbrtrrid |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 0 ≤ ( log ‘ 𝑥 ) ) |
89 |
59
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑊 ∈ Fin ) |
90 |
|
eqid |
⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 ) |
91 |
4 5 12 90
|
dchrinv |
⊢ ( 𝜑 → ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) = ( ∗ ∘ 𝑋 ) ) |
92 |
4
|
dchrabl |
⊢ ( 𝑁 ∈ ℕ → 𝐺 ∈ Abel ) |
93 |
3 92
|
syl |
⊢ ( 𝜑 → 𝐺 ∈ Abel ) |
94 |
|
ablgrp |
⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp ) |
95 |
93 94
|
syl |
⊢ ( 𝜑 → 𝐺 ∈ Grp ) |
96 |
5 90
|
grpinvcl |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐷 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ∈ 𝐷 ) |
97 |
95 12 96
|
syl2anc |
⊢ ( 𝜑 → ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ∈ 𝐷 ) |
98 |
91 97
|
eqeltrrd |
⊢ ( 𝜑 → ( ∗ ∘ 𝑋 ) ∈ 𝐷 ) |
99 |
|
eldifsni |
⊢ ( 𝑋 ∈ ( 𝐷 ∖ { 1 } ) → 𝑋 ≠ 1 ) |
100 |
11 99
|
syl |
⊢ ( 𝜑 → 𝑋 ≠ 1 ) |
101 |
5 6
|
grpidcl |
⊢ ( 𝐺 ∈ Grp → 1 ∈ 𝐷 ) |
102 |
95 101
|
syl |
⊢ ( 𝜑 → 1 ∈ 𝐷 ) |
103 |
5 90 95 12 102
|
grpinv11 |
⊢ ( 𝜑 → ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) = ( ( invg ‘ 𝐺 ) ‘ 1 ) ↔ 𝑋 = 1 ) ) |
104 |
103
|
necon3bid |
⊢ ( 𝜑 → ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ≠ ( ( invg ‘ 𝐺 ) ‘ 1 ) ↔ 𝑋 ≠ 1 ) ) |
105 |
100 104
|
mpbird |
⊢ ( 𝜑 → ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ≠ ( ( invg ‘ 𝐺 ) ‘ 1 ) ) |
106 |
6 90
|
grpinvid |
⊢ ( 𝐺 ∈ Grp → ( ( invg ‘ 𝐺 ) ‘ 1 ) = 1 ) |
107 |
95 106
|
syl |
⊢ ( 𝜑 → ( ( invg ‘ 𝐺 ) ‘ 1 ) = 1 ) |
108 |
105 91 107
|
3netr3d |
⊢ ( 𝜑 → ( ∗ ∘ 𝑋 ) ≠ 1 ) |
109 |
|
eldifsn |
⊢ ( ( ∗ ∘ 𝑋 ) ∈ ( 𝐷 ∖ { 1 } ) ↔ ( ( ∗ ∘ 𝑋 ) ∈ 𝐷 ∧ ( ∗ ∘ 𝑋 ) ≠ 1 ) ) |
110 |
98 108 109
|
sylanbrc |
⊢ ( 𝜑 → ( ∗ ∘ 𝑋 ) ∈ ( 𝐷 ∖ { 1 } ) ) |
111 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
112 |
|
1zzd |
⊢ ( 𝜑 → 1 ∈ ℤ ) |
113 |
|
2fveq3 |
⊢ ( 𝑛 = 𝑚 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) |
114 |
|
id |
⊢ ( 𝑛 = 𝑚 → 𝑛 = 𝑚 ) |
115 |
113 114
|
oveq12d |
⊢ ( 𝑛 = 𝑚 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) |
116 |
115
|
fveq2d |
⊢ ( 𝑛 = 𝑚 → ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ) = ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) |
117 |
|
eqid |
⊢ ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ) ) |
118 |
|
fvex |
⊢ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ∈ V |
119 |
116 117 118
|
fvmpt |
⊢ ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ) ) ‘ 𝑚 ) = ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) |
120 |
119
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ) ) ‘ 𝑚 ) = ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) |
121 |
|
nnre |
⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ ) |
122 |
121
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℝ ) |
123 |
122
|
cjred |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ∗ ‘ 𝑚 ) = 𝑚 ) |
124 |
123
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ∗ ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) / ( ∗ ‘ 𝑚 ) ) = ( ( ∗ ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) / 𝑚 ) ) |
125 |
13
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ ) |
126 |
1 9 2
|
znzrhfo |
⊢ ( 𝑁 ∈ ℕ0 → 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) ) |
127 |
21 126
|
syl |
⊢ ( 𝜑 → 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) ) |
128 |
|
fof |
⊢ ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ) |
129 |
127 128
|
syl |
⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ) |
130 |
|
nnz |
⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℤ ) |
131 |
|
ffvelrn |
⊢ ( ( 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ∧ 𝑚 ∈ ℤ ) → ( 𝐿 ‘ 𝑚 ) ∈ ( Base ‘ 𝑍 ) ) |
132 |
129 130 131
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐿 ‘ 𝑚 ) ∈ ( Base ‘ 𝑍 ) ) |
133 |
125 132
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℂ ) |
134 |
|
nncn |
⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℂ ) |
135 |
134
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℂ ) |
136 |
|
nnne0 |
⊢ ( 𝑚 ∈ ℕ → 𝑚 ≠ 0 ) |
137 |
136
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ≠ 0 ) |
138 |
133 135 137
|
cjdivd |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = ( ( ∗ ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) / ( ∗ ‘ 𝑚 ) ) ) |
139 |
|
fvco3 |
⊢ ( ( 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ ∧ ( 𝐿 ‘ 𝑚 ) ∈ ( Base ‘ 𝑍 ) ) → ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿 ‘ 𝑚 ) ) = ( ∗ ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) ) |
140 |
125 132 139
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿 ‘ 𝑚 ) ) = ( ∗ ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) ) |
141 |
140
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = ( ( ∗ ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) / 𝑚 ) ) |
142 |
124 138 141
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = ( ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) |
143 |
120 142
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ) ) ‘ 𝑚 ) = ( ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) |
144 |
133
|
cjcld |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ∗ ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) ∈ ℂ ) |
145 |
144 135 137
|
divcld |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ∗ ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) / 𝑚 ) ∈ ℂ ) |
146 |
141 145
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ∈ ℂ ) |
147 |
|
eqid |
⊢ ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) |
148 |
1 2 3 4 5 6 12 100 147
|
dchrmusumlema |
⊢ ( 𝜑 → ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) |
149 |
|
simprrl |
⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ) |
150 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑋 ∈ 𝑊 ) |
151 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑁 ∈ ℕ ) |
152 |
12
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑋 ∈ 𝐷 ) |
153 |
100
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑋 ≠ 1 ) |
154 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑐 ∈ ( 0 [,) +∞ ) ) |
155 |
|
simprrr |
⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) |
156 |
1 2 151 4 5 6 152 153 147 154 149 155 7
|
dchrvmaeq0 |
⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → ( 𝑋 ∈ 𝑊 ↔ 𝑡 = 0 ) ) |
157 |
150 156
|
mpbid |
⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑡 = 0 ) |
158 |
149 157
|
breqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 0 ) |
159 |
158
|
rexlimdvaa |
⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) → seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 0 ) ) |
160 |
159
|
exlimdv |
⊢ ( 𝜑 → ( ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) → seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 0 ) ) |
161 |
148 160
|
mpd |
⊢ ( 𝜑 → seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 0 ) |
162 |
|
seqex |
⊢ seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ) ) ) ∈ V |
163 |
162
|
a1i |
⊢ ( 𝜑 → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ) ) ) ∈ V ) |
164 |
|
2fveq3 |
⊢ ( 𝑎 = 𝑚 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) |
165 |
|
id |
⊢ ( 𝑎 = 𝑚 → 𝑎 = 𝑚 ) |
166 |
164 165
|
oveq12d |
⊢ ( 𝑎 = 𝑚 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) |
167 |
|
ovex |
⊢ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ∈ V |
168 |
166 147 167
|
fvmpt |
⊢ ( 𝑚 ∈ ℕ → ( ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ‘ 𝑚 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) |
169 |
168
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ‘ 𝑚 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) |
170 |
133 135 137
|
divcld |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ∈ ℂ ) |
171 |
169 170
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ‘ 𝑚 ) ∈ ℂ ) |
172 |
111 112 171
|
serf |
⊢ ( 𝜑 → seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) : ℕ ⟶ ℂ ) |
173 |
172
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ 𝑘 ) ∈ ℂ ) |
174 |
|
fzfid |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1 ... 𝑘 ) ∈ Fin ) |
175 |
|
simpl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝜑 ) |
176 |
|
elfznn |
⊢ ( 𝑚 ∈ ( 1 ... 𝑘 ) → 𝑚 ∈ ℕ ) |
177 |
175 176 170
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ∈ ℂ ) |
178 |
174 177
|
fsumcj |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ∗ ‘ Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) |
179 |
175 176 169
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ‘ 𝑚 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) |
180 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ ) |
181 |
180 111
|
eleqtrdi |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) |
182 |
179 181 177
|
fsumser |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ 𝑘 ) ) |
183 |
182
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ∗ ‘ Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = ( ∗ ‘ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ 𝑘 ) ) ) |
184 |
175 176 120
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ) ) ‘ 𝑚 ) = ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) |
185 |
170
|
cjcld |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ∈ ℂ ) |
186 |
175 176 185
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ∈ ℂ ) |
187 |
184 181 186
|
fsumser |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ) ) ) ‘ 𝑘 ) ) |
188 |
178 183 187
|
3eqtr3rd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ) ) ) ‘ 𝑘 ) = ( ∗ ‘ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ 𝑘 ) ) ) |
189 |
111 161 163 112 173 188
|
climcj |
⊢ ( 𝜑 → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ) ) ) ⇝ ( ∗ ‘ 0 ) ) |
190 |
|
cj0 |
⊢ ( ∗ ‘ 0 ) = 0 |
191 |
189 190
|
breqtrdi |
⊢ ( 𝜑 → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ) ) ) ⇝ 0 ) |
192 |
111 112 143 146 191
|
isumclim |
⊢ ( 𝜑 → Σ 𝑚 ∈ ℕ ( ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 ) |
193 |
|
fveq1 |
⊢ ( 𝑦 = ( ∗ ∘ 𝑋 ) → ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) = ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿 ‘ 𝑚 ) ) ) |
194 |
193
|
oveq1d |
⊢ ( 𝑦 = ( ∗ ∘ 𝑋 ) → ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = ( ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) |
195 |
194
|
sumeq2sdv |
⊢ ( 𝑦 = ( ∗ ∘ 𝑋 ) → Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = Σ 𝑚 ∈ ℕ ( ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) |
196 |
195
|
eqeq1d |
⊢ ( 𝑦 = ( ∗ ∘ 𝑋 ) → ( Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 ↔ Σ 𝑚 ∈ ℕ ( ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 ) ) |
197 |
196 7
|
elrab2 |
⊢ ( ( ∗ ∘ 𝑋 ) ∈ 𝑊 ↔ ( ( ∗ ∘ 𝑋 ) ∈ ( 𝐷 ∖ { 1 } ) ∧ Σ 𝑚 ∈ ℕ ( ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 ) ) |
198 |
110 192 197
|
sylanbrc |
⊢ ( 𝜑 → ( ∗ ∘ 𝑋 ) ∈ 𝑊 ) |
199 |
198
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ∗ ∘ 𝑋 ) ∈ 𝑊 ) |
200 |
8
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑋 ∈ 𝑊 ) |
201 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) |
202 |
89 199 200 201
|
nehash2 |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 2 ≤ ( ♯ ‘ 𝑊 ) ) |
203 |
|
suble0 |
⊢ ( ( 2 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) → ( ( 2 − ( ♯ ‘ 𝑊 ) ) ≤ 0 ↔ 2 ≤ ( ♯ ‘ 𝑊 ) ) ) |
204 |
77 79 203
|
sylancr |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( 2 − ( ♯ ‘ 𝑊 ) ) ≤ 0 ↔ 2 ≤ ( ♯ ‘ 𝑊 ) ) ) |
205 |
202 204
|
mpbird |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 2 − ( ♯ ‘ 𝑊 ) ) ≤ 0 ) |
206 |
80 75 72 88 205
|
lemul2ad |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) · ( 2 − ( ♯ ‘ 𝑊 ) ) ) ≤ ( ( log ‘ 𝑥 ) · 0 ) ) |
207 |
|
df-2 |
⊢ 2 = ( 1 + 1 ) |
208 |
207
|
oveq1i |
⊢ ( 2 − ( ♯ ‘ 𝑊 ) ) = ( ( 1 + 1 ) − ( ♯ ‘ 𝑊 ) ) |
209 |
|
1cnd |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ∈ ℂ ) |
210 |
79
|
recnd |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℂ ) |
211 |
209 209 210
|
addsubassd |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( 1 + 1 ) − ( ♯ ‘ 𝑊 ) ) = ( 1 + ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) |
212 |
208 211
|
syl5eq |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 2 − ( ♯ ‘ 𝑊 ) ) = ( 1 + ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) |
213 |
212
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) · ( 2 − ( ♯ ‘ 𝑊 ) ) ) = ( ( log ‘ 𝑥 ) · ( 1 + ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) |
214 |
71
|
adantrr |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( log ‘ 𝑥 ) ∈ ℂ ) |
215 |
64
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 1 − ( ♯ ‘ 𝑊 ) ) ∈ ℝ ) |
216 |
215
|
recnd |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 1 − ( ♯ ‘ 𝑊 ) ) ∈ ℂ ) |
217 |
214 209 216
|
adddid |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) · ( 1 + ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) = ( ( ( log ‘ 𝑥 ) · 1 ) + ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) |
218 |
214
|
mulid1d |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) · 1 ) = ( log ‘ 𝑥 ) ) |
219 |
218
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( log ‘ 𝑥 ) · 1 ) + ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) = ( ( log ‘ 𝑥 ) + ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) |
220 |
213 217 219
|
3eqtrd |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) · ( 2 − ( ♯ ‘ 𝑊 ) ) ) = ( ( log ‘ 𝑥 ) + ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) |
221 |
214
|
mul01d |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) · 0 ) = 0 ) |
222 |
206 220 221
|
3brtr3d |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) + ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ≤ 0 ) |
223 |
33
|
nnred |
⊢ ( 𝜑 → ( ϕ ‘ 𝑁 ) ∈ ℝ ) |
224 |
223
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ϕ ‘ 𝑁 ) ∈ ℝ ) |
225 |
49
|
ad2ant2r |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ ) |
226 |
34
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ϕ ‘ 𝑁 ) ∈ ℕ0 ) |
227 |
226
|
nn0ge0d |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 0 ≤ ( ϕ ‘ 𝑁 ) ) |
228 |
44 45
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ ) |
229 |
|
vmage0 |
⊢ ( 𝑛 ∈ ℕ → 0 ≤ ( Λ ‘ 𝑛 ) ) |
230 |
44 229
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ) → 0 ≤ ( Λ ‘ 𝑛 ) ) |
231 |
44
|
nnred |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ) → 𝑛 ∈ ℝ ) |
232 |
44
|
nngt0d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ) → 0 < 𝑛 ) |
233 |
|
divge0 |
⊢ ( ( ( ( Λ ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( Λ ‘ 𝑛 ) ) ∧ ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) ) → 0 ≤ ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) |
234 |
228 230 231 232 233
|
syl22anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ) → 0 ≤ ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) |
235 |
40 48 234
|
fsumge0 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 0 ≤ Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) |
236 |
235
|
ad2ant2r |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 0 ≤ Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) |
237 |
224 225 227 236
|
mulge0d |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 0 ≤ ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) |
238 |
74 75 76 222 237
|
letrd |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) + ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ≤ ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) |
239 |
|
leaddsub |
⊢ ( ( ( log ‘ 𝑥 ) ∈ ℝ ∧ ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ∈ ℝ ∧ ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℝ ) → ( ( ( log ‘ 𝑥 ) + ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ≤ ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ↔ ( log ‘ 𝑥 ) ≤ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) ) |
240 |
72 73 76 239
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( log ‘ 𝑥 ) + ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ≤ ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ↔ ( log ‘ 𝑥 ) ≤ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) ) |
241 |
238 240
|
mpbid |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( log ‘ 𝑥 ) ≤ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) |
242 |
72 88
|
absidd |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( log ‘ 𝑥 ) ) = ( log ‘ 𝑥 ) ) |
243 |
67
|
ad2ant2r |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ∈ ℝ ) |
244 |
75 72 243 88 241
|
letrd |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 0 ≤ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) |
245 |
243 244
|
absidd |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) = ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) |
246 |
241 242 245
|
3brtr4d |
⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( log ‘ 𝑥 ) ) ≤ ( abs ‘ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ◡ 𝐿 “ { ( 1r ‘ 𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) ) |
247 |
19 32 69 71 246
|
o1le |
⊢ ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) → ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) ) |
248 |
247
|
ex |
⊢ ( 𝜑 → ( ( ∗ ∘ 𝑋 ) ≠ 𝑋 → ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) ) ) |
249 |
248
|
necon1bd |
⊢ ( 𝜑 → ( ¬ ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) → ( ∗ ∘ 𝑋 ) = 𝑋 ) ) |
250 |
18 249
|
mpi |
⊢ ( 𝜑 → ( ∗ ∘ 𝑋 ) = 𝑋 ) |
251 |
250
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( ∗ ∘ 𝑋 ) = 𝑋 ) |
252 |
251
|
fveq1d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) = ( 𝑋 ‘ 𝑥 ) ) |
253 |
17 252
|
eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( ∗ ‘ ( 𝑋 ‘ 𝑥 ) ) = ( 𝑋 ‘ 𝑥 ) ) |
254 |
15 253
|
cjrebd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( 𝑋 ‘ 𝑥 ) ∈ ℝ ) |
255 |
254
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝑍 ) ( 𝑋 ‘ 𝑥 ) ∈ ℝ ) |
256 |
|
ffnfv |
⊢ ( 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ ↔ ( 𝑋 Fn ( Base ‘ 𝑍 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑍 ) ( 𝑋 ‘ 𝑥 ) ∈ ℝ ) ) |
257 |
14 255 256
|
sylanbrc |
⊢ ( 𝜑 → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ ) |