Step | Hyp | Ref
| Expression |
1 | | rpvmasum2.g |
. . . 4
⊢ 𝐺 = (DChr‘𝑁) |
2 | | rpvmasum.z |
. . . 4
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
3 | | rpvmasum2.d |
. . . 4
⊢ 𝐷 = (Base‘𝐺) |
4 | | eqid 2622 |
. . . 4
⊢
(Base‘𝑍) =
(Base‘𝑍) |
5 | | rpvmasum2.w |
. . . . . . 7
⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} |
6 | | ssrab2 3687 |
. . . . . . 7
⊢ {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} ⊆ (𝐷 ∖ { 1 }) |
7 | 5, 6 | eqsstri 3635 |
. . . . . 6
⊢ 𝑊 ⊆ (𝐷 ∖ { 1 }) |
8 | | dchrisum0.b |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑊) |
9 | 7, 8 | sseldi 3601 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ (𝐷 ∖ { 1 })) |
10 | 9 | eldifad 3586 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
11 | 1, 2, 3, 4, 10 | dchrf 24967 |
. . 3
⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℂ) |
12 | 11 | ffnd 6046 |
. 2
⊢ (𝜑 → 𝑋 Fn (Base‘𝑍)) |
13 | 11 | ffvelrnda 6359 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → (𝑋‘𝑥) ∈ ℂ) |
14 | | fvco3 6275 |
. . . . . 6
⊢ ((𝑋:(Base‘𝑍)⟶ℂ ∧ 𝑥 ∈ (Base‘𝑍)) → ((∗ ∘ 𝑋)‘𝑥) = (∗‘(𝑋‘𝑥))) |
15 | 11, 14 | sylan 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → ((∗ ∘ 𝑋)‘𝑥) = (∗‘(𝑋‘𝑥))) |
16 | | logno1 24382 |
. . . . . . . 8
⊢ ¬
(𝑥 ∈
ℝ+ ↦ (log‘𝑥)) ∈ 𝑂(1) |
17 | | 1red 10055 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) → 1 ∈ ℝ) |
18 | | rpvmasum.l |
. . . . . . . . . . . . 13
⊢ 𝐿 = (ℤRHom‘𝑍) |
19 | | rpvmasum.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℕ) |
20 | | rpvmasum2.1 |
. . . . . . . . . . . . 13
⊢ 1 =
(0g‘𝐺) |
21 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(Unit‘𝑍) =
(Unit‘𝑍) |
22 | 19 | nnnn0d 11351 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
23 | 2 | zncrng 19893 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 𝑍 ∈
CRing) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑍 ∈ CRing) |
25 | | crngring 18558 |
. . . . . . . . . . . . . . 15
⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑍 ∈ Ring) |
27 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(1r‘𝑍) = (1r‘𝑍) |
28 | 21, 27 | 1unit 18658 |
. . . . . . . . . . . . . 14
⊢ (𝑍 ∈ Ring →
(1r‘𝑍)
∈ (Unit‘𝑍)) |
29 | 26, 28 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1r‘𝑍) ∈ (Unit‘𝑍)) |
30 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (◡𝐿 “ {(1r‘𝑍)}) = (◡𝐿 “ {(1r‘𝑍)}) |
31 | | eqidd 2623 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑊) → (1r‘𝑍) = (1r‘𝑍)) |
32 | 2, 18, 19, 1, 3, 20, 5, 21, 29, 30, 31 | rpvmasum2 25201 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊))))) ∈
𝑂(1)) |
33 | 32 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) → (𝑥 ∈ ℝ+ ↦
(((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊))))) ∈
𝑂(1)) |
34 | 19 | phicld 15477 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℕ) |
35 | 34 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℕ0) |
36 | 35 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(ϕ‘𝑁) ∈
ℕ0) |
37 | 36 | nn0red 11352 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(ϕ‘𝑁) ∈
ℝ) |
38 | | fzfid 12772 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘𝑥))
∈ Fin) |
39 | | inss1 3833 |
. . . . . . . . . . . . . . . . 17
⊢
((1...(⌊‘𝑥)) ∩ (◡𝐿 “ {(1r‘𝑍)})) ⊆
(1...(⌊‘𝑥)) |
40 | | ssfi 8180 |
. . . . . . . . . . . . . . . . 17
⊢
(((1...(⌊‘𝑥)) ∈ Fin ∧
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)})) ⊆
(1...(⌊‘𝑥)))
→ ((1...(⌊‘𝑥)) ∩ (◡𝐿 “ {(1r‘𝑍)})) ∈
Fin) |
41 | 38, 39, 40 | sylancl 694 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)})) ∈
Fin) |
42 | | elinel1 3799 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)})) → 𝑛 ∈ (1...(⌊‘𝑥))) |
43 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
44 | 43 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
45 | 42, 44 | sylan2 491 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))) → 𝑛 ∈ ℕ) |
46 | | vmacl 24844 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
47 | | nndivre 11056 |
. . . . . . . . . . . . . . . . . 18
⊢
(((Λ‘𝑛)
∈ ℝ ∧ 𝑛
∈ ℕ) → ((Λ‘𝑛) / 𝑛) ∈ ℝ) |
48 | 46, 47 | mpancom 703 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ →
((Λ‘𝑛) / 𝑛) ∈
ℝ) |
49 | 45, 48 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))) →
((Λ‘𝑛) / 𝑛) ∈
ℝ) |
50 | 41, 49 | fsumrecl 14465 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛) ∈ ℝ) |
51 | 37, 50 | remulcld 10070 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛)) ∈ ℝ) |
52 | | relogcl 24322 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
53 | 52 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℝ) |
54 | | 1re 10039 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ |
55 | 1, 3 | dchrfi 24980 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ → 𝐷 ∈ Fin) |
56 | 19, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐷 ∈ Fin) |
57 | | difss 3737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐷 ∖ { 1 }) ⊆ 𝐷 |
58 | 7, 57 | sstri 3612 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑊 ⊆ 𝐷 |
59 | | ssfi 8180 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ Fin ∧ 𝑊 ⊆ 𝐷) → 𝑊 ∈ Fin) |
60 | 56, 58, 59 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑊 ∈ Fin) |
61 | | hashcl 13147 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑊 ∈ Fin →
(#‘𝑊) ∈
ℕ0) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (#‘𝑊) ∈
ℕ0) |
63 | 62 | nn0red 11352 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (#‘𝑊) ∈ ℝ) |
64 | | resubcl 10345 |
. . . . . . . . . . . . . . . . 17
⊢ ((1
∈ ℝ ∧ (#‘𝑊) ∈ ℝ) → (1 −
(#‘𝑊)) ∈
ℝ) |
65 | 54, 63, 64 | sylancr 695 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 − (#‘𝑊)) ∈
ℝ) |
66 | 65 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1
− (#‘𝑊)) ∈
ℝ) |
67 | 53, 66 | remulcld 10070 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · (1
− (#‘𝑊)))
∈ ℝ) |
68 | 51, 67 | resubcld 10458 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊)))) ∈
ℝ) |
69 | 68 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊)))) ∈
ℂ) |
70 | 69 | adantlr 751 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ 𝑥 ∈ ℝ+) →
(((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊)))) ∈
ℂ) |
71 | 52 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℝ) |
72 | 71 | recnd 10068 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℂ) |
73 | 52 | ad2antrl 764 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (log‘𝑥) ∈
ℝ) |
74 | 67 | ad2ant2r 783 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
((log‘𝑥) · (1
− (#‘𝑊)))
∈ ℝ) |
75 | 73, 74 | readdcld 10069 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
((log‘𝑥) +
((log‘𝑥) · (1
− (#‘𝑊))))
∈ ℝ) |
76 | | 0red 10041 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 0 ∈
ℝ) |
77 | 51 | ad2ant2r 783 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛)) ∈ ℝ) |
78 | | 2re 11090 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ |
79 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 2 ∈
ℝ) |
80 | 63 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (#‘𝑊) ∈
ℝ) |
81 | 79, 80 | resubcld 10458 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (2 −
(#‘𝑊)) ∈
ℝ) |
82 | | log1 24332 |
. . . . . . . . . . . . . . . . 17
⊢
(log‘1) = 0 |
83 | | simprr 796 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 1 ≤ 𝑥) |
84 | | 1rp 11836 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ+ |
85 | | simprl 794 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑥 ∈
ℝ+) |
86 | | logleb 24349 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℝ+ ∧ 𝑥 ∈ ℝ+) → (1 ≤
𝑥 ↔ (log‘1) ≤
(log‘𝑥))) |
87 | 84, 85, 86 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (1 ≤ 𝑥 ↔ (log‘1) ≤
(log‘𝑥))) |
88 | 83, 87 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (log‘1)
≤ (log‘𝑥)) |
89 | 82, 88 | syl5eqbrr 4689 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 0 ≤
(log‘𝑥)) |
90 | | simplr 792 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (∗
∘ 𝑋) ≠ 𝑋) |
91 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(invg‘𝐺) = (invg‘𝐺) |
92 | 1, 3, 10, 91 | dchrinv 24986 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 →
((invg‘𝐺)‘𝑋) = (∗ ∘ 𝑋)) |
93 | 1 | dchrabl 24979 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel) |
94 | 19, 93 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐺 ∈ Abel) |
95 | | ablgrp 18198 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐺 ∈ Grp) |
97 | 3, 91 | grpinvcl 17467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐷) → ((invg‘𝐺)‘𝑋) ∈ 𝐷) |
98 | 96, 10, 97 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 →
((invg‘𝐺)‘𝑋) ∈ 𝐷) |
99 | 92, 98 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (∗ ∘ 𝑋) ∈ 𝐷) |
100 | | eldifsni 4320 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑋 ∈ (𝐷 ∖ { 1 }) → 𝑋 ≠ 1 ) |
101 | 9, 100 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑋 ≠ 1 ) |
102 | 3, 20 | grpidcl 17450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐺 ∈ Grp → 1 ∈ 𝐷) |
103 | 96, 102 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 1 ∈ 𝐷) |
104 | 3, 91, 96, 10, 103 | grpinv11 17484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 →
(((invg‘𝐺)‘𝑋) = ((invg‘𝐺)‘ 1 ) ↔ 𝑋 = 1 )) |
105 | 104 | necon3bid 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 →
(((invg‘𝐺)‘𝑋) ≠ ((invg‘𝐺)‘ 1 ) ↔ 𝑋 ≠ 1 )) |
106 | 101, 105 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 →
((invg‘𝐺)‘𝑋) ≠ ((invg‘𝐺)‘ 1 )) |
107 | 20, 91 | grpinvid 17476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐺 ∈ Grp →
((invg‘𝐺)‘ 1 ) = 1 ) |
108 | 96, 107 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 →
((invg‘𝐺)‘ 1 ) = 1 ) |
109 | 106, 92, 108 | 3netr3d 2870 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (∗ ∘ 𝑋) ≠ 1 ) |
110 | | eldifsn 4317 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((∗ ∘ 𝑋) ∈ (𝐷 ∖ { 1 }) ↔ ((∗
∘ 𝑋) ∈ 𝐷 ∧ (∗ ∘ 𝑋) ≠ 1 )) |
111 | 99, 109, 110 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (∗ ∘ 𝑋) ∈ (𝐷 ∖ { 1 })) |
112 | | nnuz 11723 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ℕ =
(ℤ≥‘1) |
113 | | 1zzd 11408 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 1 ∈
ℤ) |
114 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑛 = 𝑚 → (𝐿‘𝑛) = (𝐿‘𝑚)) |
115 | 114 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = 𝑚 → (𝑋‘(𝐿‘𝑛)) = (𝑋‘(𝐿‘𝑚))) |
116 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = 𝑚 → 𝑛 = 𝑚) |
117 | 115, 116 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = 𝑚 → ((𝑋‘(𝐿‘𝑛)) / 𝑛) = ((𝑋‘(𝐿‘𝑚)) / 𝑚)) |
118 | 117 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 = 𝑚 → (∗‘((𝑋‘(𝐿‘𝑛)) / 𝑛)) = (∗‘((𝑋‘(𝐿‘𝑚)) / 𝑚))) |
119 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 ∈ ℕ ↦
(∗‘((𝑋‘(𝐿‘𝑛)) / 𝑛))) = (𝑛 ∈ ℕ ↦
(∗‘((𝑋‘(𝐿‘𝑛)) / 𝑛))) |
120 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∗‘((𝑋‘(𝐿‘𝑚)) / 𝑚)) ∈ V |
121 | 118, 119,
120 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦
(∗‘((𝑋‘(𝐿‘𝑛)) / 𝑛)))‘𝑚) = (∗‘((𝑋‘(𝐿‘𝑚)) / 𝑚))) |
122 | 121 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦
(∗‘((𝑋‘(𝐿‘𝑛)) / 𝑛)))‘𝑚) = (∗‘((𝑋‘(𝐿‘𝑚)) / 𝑚))) |
123 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ) |
124 | 123 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ) |
125 | 124 | cjred 13966 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (∗‘𝑚) = 𝑚) |
126 | 125 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
((∗‘(𝑋‘(𝐿‘𝑚))) / (∗‘𝑚)) = ((∗‘(𝑋‘(𝐿‘𝑚))) / 𝑚)) |
127 | 11 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑋:(Base‘𝑍)⟶ℂ) |
128 | 2, 4, 18 | znzrhfo 19896 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 ∈ ℕ0
→ 𝐿:ℤ–onto→(Base‘𝑍)) |
129 | 22, 128 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝐿:ℤ–onto→(Base‘𝑍)) |
130 | | fof 6115 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍)) |
131 | 129, 130 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑍)) |
132 | | nnz 11399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℤ) |
133 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐿:ℤ⟶(Base‘𝑍) ∧ 𝑚 ∈ ℤ) → (𝐿‘𝑚) ∈ (Base‘𝑍)) |
134 | 131, 132,
133 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐿‘𝑚) ∈ (Base‘𝑍)) |
135 | 127, 134 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ) |
136 | | nncn 11028 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) |
137 | 136 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ) |
138 | | nnne0 11053 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑚 ∈ ℕ → 𝑚 ≠ 0) |
139 | 138 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ≠ 0) |
140 | 135, 137,
139 | cjdivd 13963 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∗‘((𝑋‘(𝐿‘𝑚)) / 𝑚)) = ((∗‘(𝑋‘(𝐿‘𝑚))) / (∗‘𝑚))) |
141 | | fvco3 6275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑋:(Base‘𝑍)⟶ℂ ∧ (𝐿‘𝑚) ∈ (Base‘𝑍)) → ((∗ ∘ 𝑋)‘(𝐿‘𝑚)) = (∗‘(𝑋‘(𝐿‘𝑚)))) |
142 | 127, 134,
141 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((∗ ∘
𝑋)‘(𝐿‘𝑚)) = (∗‘(𝑋‘(𝐿‘𝑚)))) |
143 | 142 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((∗ ∘
𝑋)‘(𝐿‘𝑚)) / 𝑚) = ((∗‘(𝑋‘(𝐿‘𝑚))) / 𝑚)) |
144 | 126, 140,
143 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∗‘((𝑋‘(𝐿‘𝑚)) / 𝑚)) = (((∗ ∘ 𝑋)‘(𝐿‘𝑚)) / 𝑚)) |
145 | 122, 144 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑛 ∈ ℕ ↦
(∗‘((𝑋‘(𝐿‘𝑛)) / 𝑛)))‘𝑚) = (((∗ ∘ 𝑋)‘(𝐿‘𝑚)) / 𝑚)) |
146 | 135 | cjcld 13936 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∗‘(𝑋‘(𝐿‘𝑚))) ∈ ℂ) |
147 | 146, 137,
139 | divcld 10801 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
((∗‘(𝑋‘(𝐿‘𝑚))) / 𝑚) ∈ ℂ) |
148 | 143, 147 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((∗ ∘
𝑋)‘(𝐿‘𝑚)) / 𝑚) ∈ ℂ) |
149 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) |
150 | 2, 18, 19, 1, 3, 20, 10, 101, 149 | dchrmusumlema 25182 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦))) |
151 | | simprrl 804 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡) |
152 | 8 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑋 ∈ 𝑊) |
153 | 19 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑁 ∈ ℕ) |
154 | 10 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑋 ∈ 𝐷) |
155 | 101 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑋 ≠ 1 ) |
156 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑐 ∈ (0[,)+∞)) |
157 | | simprrr 805 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) |
158 | 2, 18, 153, 1, 3, 20, 154, 155, 149, 156, 151, 157, 5 | dchrvmaeq0 25193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑋 ∈ 𝑊 ↔ 𝑡 = 0)) |
159 | 152, 158 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑡 = 0) |
160 | 151, 159 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 0) |
161 | 160 | rexlimdvaa 3032 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 0)) |
162 | 161 | exlimdv 1861 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 0)) |
163 | 150, 162 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 0) |
164 | | seqex 12803 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
(∗‘((𝑋‘(𝐿‘𝑛)) / 𝑛)))) ∈ V |
165 | 164 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦
(∗‘((𝑋‘(𝐿‘𝑛)) / 𝑛)))) ∈ V) |
166 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑎 = 𝑚 → (𝐿‘𝑎) = (𝐿‘𝑚)) |
167 | 166 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑎 = 𝑚 → (𝑋‘(𝐿‘𝑎)) = (𝑋‘(𝐿‘𝑚))) |
168 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑎 = 𝑚 → 𝑎 = 𝑚) |
169 | 167, 168 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑎 = 𝑚 → ((𝑋‘(𝐿‘𝑎)) / 𝑎) = ((𝑋‘(𝐿‘𝑚)) / 𝑚)) |
170 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑋‘(𝐿‘𝑚)) / 𝑚) ∈ V |
171 | 169, 149,
170 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑚 ∈ ℕ → ((𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))‘𝑚) = ((𝑋‘(𝐿‘𝑚)) / 𝑚)) |
172 | 171 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))‘𝑚) = ((𝑋‘(𝐿‘𝑚)) / 𝑚)) |
173 | 135, 137,
139 | divcld 10801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑋‘(𝐿‘𝑚)) / 𝑚) ∈ ℂ) |
174 | 172, 173 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))‘𝑚) ∈ ℂ) |
175 | 112, 113,
174 | serf 12829 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))):ℕ⟶ℂ) |
176 | 175 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘𝑘) ∈ ℂ) |
177 | | fzfid 12772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1...𝑘) ∈ Fin) |
178 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝜑) |
179 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑚 ∈ (1...𝑘) → 𝑚 ∈ ℕ) |
180 | 178, 179,
173 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → ((𝑋‘(𝐿‘𝑚)) / 𝑚) ∈ ℂ) |
181 | 177, 180 | fsumcj 14542 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(∗‘Σ𝑚
∈ (1...𝑘)((𝑋‘(𝐿‘𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...𝑘)(∗‘((𝑋‘(𝐿‘𝑚)) / 𝑚))) |
182 | 178, 179,
172 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → ((𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))‘𝑚) = ((𝑋‘(𝐿‘𝑚)) / 𝑚)) |
183 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
184 | 183, 112 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
(ℤ≥‘1)) |
185 | 182, 184,
180 | fsumser 14461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)((𝑋‘(𝐿‘𝑚)) / 𝑚) = (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘𝑘)) |
186 | 185 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(∗‘Σ𝑚
∈ (1...𝑘)((𝑋‘(𝐿‘𝑚)) / 𝑚)) = (∗‘(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘𝑘))) |
187 | 178, 179,
122 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → ((𝑛 ∈ ℕ ↦
(∗‘((𝑋‘(𝐿‘𝑛)) / 𝑛)))‘𝑚) = (∗‘((𝑋‘(𝐿‘𝑚)) / 𝑚))) |
188 | 173 | cjcld 13936 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∗‘((𝑋‘(𝐿‘𝑚)) / 𝑚)) ∈ ℂ) |
189 | 178, 179,
188 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (∗‘((𝑋‘(𝐿‘𝑚)) / 𝑚)) ∈ ℂ) |
190 | 187, 184,
189 | fsumser 14461 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)(∗‘((𝑋‘(𝐿‘𝑚)) / 𝑚)) = (seq1( + , (𝑛 ∈ ℕ ↦
(∗‘((𝑋‘(𝐿‘𝑛)) / 𝑛))))‘𝑘)) |
191 | 181, 186,
190 | 3eqtr3rd 2665 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , (𝑛 ∈ ℕ ↦
(∗‘((𝑋‘(𝐿‘𝑛)) / 𝑛))))‘𝑘) = (∗‘(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘𝑘))) |
192 | 112, 163,
165, 113, 176, 191 | climcj 14335 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦
(∗‘((𝑋‘(𝐿‘𝑛)) / 𝑛)))) ⇝
(∗‘0)) |
193 | | cj0 13898 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∗‘0) = 0 |
194 | 192, 193 | syl6breq 4694 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦
(∗‘((𝑋‘(𝐿‘𝑛)) / 𝑛)))) ⇝ 0) |
195 | 112, 113,
145, 148, 194 | isumclim 14488 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → Σ𝑚 ∈ ℕ (((∗ ∘ 𝑋)‘(𝐿‘𝑚)) / 𝑚) = 0) |
196 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = (∗ ∘ 𝑋) → (𝑦‘(𝐿‘𝑚)) = ((∗ ∘ 𝑋)‘(𝐿‘𝑚))) |
197 | 196 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = (∗ ∘ 𝑋) → ((𝑦‘(𝐿‘𝑚)) / 𝑚) = (((∗ ∘ 𝑋)‘(𝐿‘𝑚)) / 𝑚)) |
198 | 197 | sumeq2sdv 14435 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = (∗ ∘ 𝑋) → Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = Σ𝑚 ∈ ℕ (((∗ ∘ 𝑋)‘(𝐿‘𝑚)) / 𝑚)) |
199 | 198 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = (∗ ∘ 𝑋) → (Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0 ↔ Σ𝑚 ∈ ℕ (((∗ ∘ 𝑋)‘(𝐿‘𝑚)) / 𝑚) = 0)) |
200 | 199, 5 | elrab2 3366 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((∗ ∘ 𝑋) ∈ 𝑊 ↔ ((∗ ∘ 𝑋) ∈ (𝐷 ∖ { 1 }) ∧ Σ𝑚 ∈ ℕ (((∗
∘ 𝑋)‘(𝐿‘𝑚)) / 𝑚) = 0)) |
201 | 111, 195,
200 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (∗ ∘ 𝑋) ∈ 𝑊) |
202 | 201 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (∗
∘ 𝑋) ∈ 𝑊) |
203 | 8 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑋 ∈ 𝑊) |
204 | | hashprg 13182 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((∗ ∘ 𝑋) ∈ 𝑊 ∧ 𝑋 ∈ 𝑊) → ((∗ ∘ 𝑋) ≠ 𝑋 ↔ (#‘{(∗ ∘ 𝑋), 𝑋}) = 2)) |
205 | 202, 203,
204 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → ((∗
∘ 𝑋) ≠ 𝑋 ↔ (#‘{(∗
∘ 𝑋), 𝑋}) = 2)) |
206 | 90, 205 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(#‘{(∗ ∘ 𝑋), 𝑋}) = 2) |
207 | 60 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑊 ∈ Fin) |
208 | 202, 203 | prssd 4354 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → {(∗
∘ 𝑋), 𝑋} ⊆ 𝑊) |
209 | | ssdomg 8001 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑊 ∈ Fin → ({(∗
∘ 𝑋), 𝑋} ⊆ 𝑊 → {(∗ ∘ 𝑋), 𝑋} ≼ 𝑊)) |
210 | 207, 208,
209 | sylc 65 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → {(∗
∘ 𝑋), 𝑋} ≼ 𝑊) |
211 | | hashdomi 13169 |
. . . . . . . . . . . . . . . . . . 19
⊢
({(∗ ∘ 𝑋), 𝑋} ≼ 𝑊 → (#‘{(∗ ∘ 𝑋), 𝑋}) ≤ (#‘𝑊)) |
212 | 210, 211 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(#‘{(∗ ∘ 𝑋), 𝑋}) ≤ (#‘𝑊)) |
213 | 206, 212 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 2 ≤
(#‘𝑊)) |
214 | | suble0 10542 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℝ ∧ (#‘𝑊) ∈ ℝ) → ((2 −
(#‘𝑊)) ≤ 0 ↔
2 ≤ (#‘𝑊))) |
215 | 78, 80, 214 | sylancr 695 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → ((2 −
(#‘𝑊)) ≤ 0 ↔
2 ≤ (#‘𝑊))) |
216 | 213, 215 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (2 −
(#‘𝑊)) ≤
0) |
217 | 81, 76, 73, 89, 216 | lemul2ad 10964 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
((log‘𝑥) · (2
− (#‘𝑊))) ≤
((log‘𝑥) ·
0)) |
218 | | df-2 11079 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 = (1 +
1) |
219 | 218 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . 18
⊢ (2
− (#‘𝑊)) = ((1
+ 1) − (#‘𝑊)) |
220 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 1 ∈
ℂ) |
221 | 80 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (#‘𝑊) ∈
ℂ) |
222 | 220, 220,
221 | addsubassd 10412 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → ((1 + 1) −
(#‘𝑊)) = (1 + (1
− (#‘𝑊)))) |
223 | 219, 222 | syl5eq 2668 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (2 −
(#‘𝑊)) = (1 + (1
− (#‘𝑊)))) |
224 | 223 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
((log‘𝑥) · (2
− (#‘𝑊))) =
((log‘𝑥) · (1
+ (1 − (#‘𝑊))))) |
225 | 72 | adantrr 753 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (log‘𝑥) ∈
ℂ) |
226 | 65 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (1 −
(#‘𝑊)) ∈
ℝ) |
227 | 226 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (1 −
(#‘𝑊)) ∈
ℂ) |
228 | 225, 220,
227 | adddid 10064 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
((log‘𝑥) · (1
+ (1 − (#‘𝑊))))
= (((log‘𝑥) ·
1) + ((log‘𝑥)
· (1 − (#‘𝑊))))) |
229 | 225 | mulid1d 10057 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
((log‘𝑥) · 1)
= (log‘𝑥)) |
230 | 229 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(((log‘𝑥) · 1)
+ ((log‘𝑥) ·
(1 − (#‘𝑊)))) =
((log‘𝑥) +
((log‘𝑥) · (1
− (#‘𝑊))))) |
231 | 224, 228,
230 | 3eqtrd 2660 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
((log‘𝑥) · (2
− (#‘𝑊))) =
((log‘𝑥) +
((log‘𝑥) · (1
− (#‘𝑊))))) |
232 | 225 | mul01d 10235 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
((log‘𝑥) · 0)
= 0) |
233 | 217, 231,
232 | 3brtr3d 4684 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
((log‘𝑥) +
((log‘𝑥) · (1
− (#‘𝑊)))) ≤
0) |
234 | 34 | nnred 11035 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℝ) |
235 | 234 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(ϕ‘𝑁) ∈
ℝ) |
236 | 50 | ad2ant2r 783 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛) ∈ ℝ) |
237 | 35 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(ϕ‘𝑁) ∈
ℕ0) |
238 | 237 | nn0ge0d 11354 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 0 ≤
(ϕ‘𝑁)) |
239 | 45, 46 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))) →
(Λ‘𝑛) ∈
ℝ) |
240 | | vmage0 24847 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → 0 ≤
(Λ‘𝑛)) |
241 | 45, 240 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))) → 0 ≤
(Λ‘𝑛)) |
242 | 45 | nnred 11035 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))) → 𝑛 ∈ ℝ) |
243 | 45 | nngt0d 11064 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))) → 0 < 𝑛) |
244 | | divge0 10892 |
. . . . . . . . . . . . . . . . . 18
⊢
((((Λ‘𝑛) ∈ ℝ ∧ 0 ≤
(Λ‘𝑛)) ∧
(𝑛 ∈ ℝ ∧ 0
< 𝑛)) → 0 ≤
((Λ‘𝑛) / 𝑛)) |
245 | 239, 241,
242, 243, 244 | syl22anc 1327 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))) → 0 ≤
((Λ‘𝑛) / 𝑛)) |
246 | 41, 49, 245 | fsumge0 14527 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 0 ≤
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛)) |
247 | 246 | ad2ant2r 783 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 0 ≤
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛)) |
248 | 235, 236,
238, 247 | mulge0d 10604 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 0 ≤
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛))) |
249 | 75, 76, 77, 233, 248 | letrd 10194 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
((log‘𝑥) +
((log‘𝑥) · (1
− (#‘𝑊)))) ≤
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛))) |
250 | | leaddsub 10504 |
. . . . . . . . . . . . . 14
⊢
(((log‘𝑥)
∈ ℝ ∧ ((log‘𝑥) · (1 − (#‘𝑊))) ∈ ℝ ∧
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛)) ∈ ℝ) → (((log‘𝑥) + ((log‘𝑥) · (1 −
(#‘𝑊)))) ≤
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛)) ↔ (log‘𝑥) ≤ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊)))))) |
251 | 73, 74, 77, 250 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(((log‘𝑥) +
((log‘𝑥) · (1
− (#‘𝑊)))) ≤
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛)) ↔ (log‘𝑥) ≤ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊)))))) |
252 | 249, 251 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (log‘𝑥) ≤ (((ϕ‘𝑁) · Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊))))) |
253 | 73, 89 | absidd 14161 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘(log‘𝑥)) =
(log‘𝑥)) |
254 | 68 | ad2ant2r 783 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊)))) ∈
ℝ) |
255 | 76, 73, 254, 89, 252 | letrd 10194 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 0 ≤
(((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊))))) |
256 | 254, 255 | absidd 14161 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘(((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊))))) = (((ϕ‘𝑁) · Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊))))) |
257 | 252, 253,
256 | 3brtr4d 4685 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘(log‘𝑥))
≤ (abs‘(((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ (◡𝐿 “ {(1r‘𝑍)}))((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊)))))) |
258 | 17, 33, 70, 72, 257 | o1le 14383 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (∗ ∘ 𝑋) ≠ 𝑋) → (𝑥 ∈ ℝ+ ↦
(log‘𝑥)) ∈
𝑂(1)) |
259 | 258 | ex 450 |
. . . . . . . . 9
⊢ (𝜑 → ((∗ ∘ 𝑋) ≠ 𝑋 → (𝑥 ∈ ℝ+ ↦
(log‘𝑥)) ∈
𝑂(1))) |
260 | 259 | necon1bd 2812 |
. . . . . . . 8
⊢ (𝜑 → (¬ (𝑥 ∈ ℝ+ ↦
(log‘𝑥)) ∈
𝑂(1) → (∗ ∘ 𝑋) = 𝑋)) |
261 | 16, 260 | mpi 20 |
. . . . . . 7
⊢ (𝜑 → (∗ ∘ 𝑋) = 𝑋) |
262 | 261 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → (∗ ∘ 𝑋) = 𝑋) |
263 | 262 | fveq1d 6193 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → ((∗ ∘ 𝑋)‘𝑥) = (𝑋‘𝑥)) |
264 | 15, 263 | eqtr3d 2658 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → (∗‘(𝑋‘𝑥)) = (𝑋‘𝑥)) |
265 | 13, 264 | cjrebd 13942 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → (𝑋‘𝑥) ∈ ℝ) |
266 | 265 | ralrimiva 2966 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑍)(𝑋‘𝑥) ∈ ℝ) |
267 | | ffnfv 6388 |
. 2
⊢ (𝑋:(Base‘𝑍)⟶ℝ ↔ (𝑋 Fn (Base‘𝑍) ∧ ∀𝑥 ∈ (Base‘𝑍)(𝑋‘𝑥) ∈ ℝ)) |
268 | 12, 266, 267 | sylanbrc 698 |
1
⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ) |