Step | Hyp | Ref
| Expression |
1 | | lgamgulm.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ ℕ) |
2 | | lgamgulm.u |
. . . . . . 7
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} |
3 | 1, 2 | lgamgulmlem1 26178 |
. . . . . 6
⊢ (𝜑 → 𝑈 ⊆ (ℂ ∖ (ℤ ∖
ℕ))) |
4 | 3 | sselda 3921 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
5 | | ovex 7308 |
. . . . 5
⊢
(Σ𝑛 ∈
ℕ ((𝑧 ·
(log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) − (log‘𝑧)) ∈ V |
6 | | df-lgam 26168 |
. . . . . 6
⊢ log
Γ = (𝑧 ∈
(ℂ ∖ (ℤ ∖ ℕ)) ↦ (Σ𝑛 ∈ ℕ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) − (log‘𝑧))) |
7 | 6 | fvmpt2 6886 |
. . . . 5
⊢ ((𝑧 ∈ (ℂ ∖
(ℤ ∖ ℕ)) ∧ (Σ𝑛 ∈ ℕ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) − (log‘𝑧)) ∈ V) → (log
Γ‘𝑧) =
(Σ𝑛 ∈ ℕ
((𝑧 ·
(log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) − (log‘𝑧))) |
8 | 4, 5, 7 | sylancl 586 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (log Γ‘𝑧) = (Σ𝑛 ∈ ℕ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) − (log‘𝑧))) |
9 | | nnuz 12621 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
10 | | 1zzd 12351 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 1 ∈ ℤ) |
11 | | oveq1 7282 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1)) |
12 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → 𝑚 = 𝑛) |
13 | 11, 12 | oveq12d 7293 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → ((𝑚 + 1) / 𝑚) = ((𝑛 + 1) / 𝑛)) |
14 | 13 | fveq2d 6778 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (log‘((𝑚 + 1) / 𝑚)) = (log‘((𝑛 + 1) / 𝑛))) |
15 | 14 | oveq2d 7291 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (𝑧 · (log‘((𝑚 + 1) / 𝑚))) = (𝑧 · (log‘((𝑛 + 1) / 𝑛)))) |
16 | | oveq2 7283 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (𝑧 / 𝑚) = (𝑧 / 𝑛)) |
17 | 16 | fvoveq1d 7297 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (log‘((𝑧 / 𝑚) + 1)) = (log‘((𝑧 / 𝑛) + 1))) |
18 | 15, 17 | oveq12d 7293 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) = ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1)))) |
19 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))) = (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))) |
20 | | ovex 7308 |
. . . . . . . . 9
⊢ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) ∈ V |
21 | 18, 19, 20 | fvmpt 6875 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))‘𝑛) = ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1)))) |
22 | 21 | adantl 482 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))‘𝑛) = ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1)))) |
23 | 4 | eldifad 3899 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ ℂ) |
24 | 23 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → 𝑧 ∈ ℂ) |
25 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
26 | 25 | peano2nnd 11990 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ) |
27 | 26 | nnrpd 12770 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈
ℝ+) |
28 | 25 | nnrpd 12770 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ+) |
29 | 27, 28 | rpdivcld 12789 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → ((𝑛 + 1) / 𝑛) ∈
ℝ+) |
30 | 29 | relogcld 25778 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → (log‘((𝑛 + 1) / 𝑛)) ∈ ℝ) |
31 | 30 | recnd 11003 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → (log‘((𝑛 + 1) / 𝑛)) ∈ ℂ) |
32 | 24, 31 | mulcld 10995 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → (𝑧 · (log‘((𝑛 + 1) / 𝑛))) ∈ ℂ) |
33 | 25 | nncnd 11989 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ) |
34 | 25 | nnne0d 12023 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0) |
35 | 24, 33, 34 | divcld 11751 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → (𝑧 / 𝑛) ∈ ℂ) |
36 | | 1cnd 10970 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → 1 ∈
ℂ) |
37 | 35, 36 | addcld 10994 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → ((𝑧 / 𝑛) + 1) ∈ ℂ) |
38 | 4 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → 𝑧 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
39 | 38, 25 | dmgmdivn0 26177 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → ((𝑧 / 𝑛) + 1) ≠ 0) |
40 | 37, 39 | logcld 25726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → (log‘((𝑧 / 𝑛) + 1)) ∈ ℂ) |
41 | 32, 40 | subcld 11332 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) ∈ ℂ) |
42 | | 1z 12350 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
43 | | seqfn 13733 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℤ → seq1( ∘f + , 𝐺) Fn
(ℤ≥‘1)) |
44 | 42, 43 | ax-mp 5 |
. . . . . . . . . . 11
⊢ seq1(
∘f + , 𝐺)
Fn (ℤ≥‘1) |
45 | 9 | fneq2i 6531 |
. . . . . . . . . . 11
⊢ (seq1(
∘f + , 𝐺)
Fn ℕ ↔ seq1( ∘f + , 𝐺) Fn
(ℤ≥‘1)) |
46 | 44, 45 | mpbir 230 |
. . . . . . . . . 10
⊢ seq1(
∘f + , 𝐺)
Fn ℕ |
47 | | lgamgulm.g |
. . . . . . . . . . . 12
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) |
48 | 1, 2, 47 | lgamgulm 26184 |
. . . . . . . . . . 11
⊢ (𝜑 → seq1( ∘f
+ , 𝐺) ∈ dom
(⇝𝑢‘𝑈)) |
49 | | ulmdm 25552 |
. . . . . . . . . . 11
⊢ (seq1(
∘f + , 𝐺)
∈ dom (⇝𝑢‘𝑈) ↔ seq1( ∘f + , 𝐺)(⇝𝑢‘𝑈)((⇝𝑢‘𝑈)‘seq1(
∘f + , 𝐺))) |
50 | 48, 49 | sylib 217 |
. . . . . . . . . 10
⊢ (𝜑 → seq1( ∘f
+ , 𝐺)(⇝𝑢‘𝑈)((⇝𝑢‘𝑈)‘seq1(
∘f + , 𝐺))) |
51 | | ulmf2 25543 |
. . . . . . . . . 10
⊢ ((seq1(
∘f + , 𝐺)
Fn ℕ ∧ seq1( ∘f + , 𝐺)(⇝𝑢‘𝑈)((⇝𝑢‘𝑈)‘seq1(
∘f + , 𝐺))) → seq1( ∘f + ,
𝐺):ℕ⟶(ℂ
↑m 𝑈)) |
52 | 46, 50, 51 | sylancr 587 |
. . . . . . . . 9
⊢ (𝜑 → seq1( ∘f
+ , 𝐺):ℕ⟶(ℂ ↑m
𝑈)) |
53 | 52 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → seq1( ∘f + , 𝐺):ℕ⟶(ℂ
↑m 𝑈)) |
54 | | simpr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ 𝑈) |
55 | | seqex 13723 |
. . . . . . . . 9
⊢ seq1( + ,
(𝑚 ∈ ℕ ↦
((𝑧 ·
(log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) ∈ V |
56 | 55 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) ∈ V) |
57 | 47 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))) |
58 | 57 | seqeq3d 13729 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → seq1(
∘f + , 𝐺)
= seq1( ∘f + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))))) |
59 | 58 | fveq1d 6776 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → (seq1(
∘f + , 𝐺)‘𝑛) = (seq1( ∘f + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))))‘𝑛)) |
60 | | cnex 10952 |
. . . . . . . . . . . . . . 15
⊢ ℂ
∈ V |
61 | 2, 60 | rabex2 5258 |
. . . . . . . . . . . . . 14
⊢ 𝑈 ∈ V |
62 | 61 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑈 ∈ V) |
63 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
64 | 63, 9 | eleqtrdi 2849 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
(ℤ≥‘1)) |
65 | | fz1ssnn 13287 |
. . . . . . . . . . . . . 14
⊢
(1...𝑛) ⊆
ℕ |
66 | 65 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...𝑛) ⊆
ℕ) |
67 | | ovexd 7310 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑚 ∈ ℕ ∧ 𝑧 ∈ 𝑈)) → ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) ∈ V) |
68 | 62, 64, 66, 67 | seqof2 13781 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1(
∘f + , (𝑚
∈ ℕ ↦ (𝑧
∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))))‘𝑛) = (𝑧 ∈ 𝑈 ↦ (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛))) |
69 | 68 | adantlr 712 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → (seq1(
∘f + , (𝑚
∈ ℕ ↦ (𝑧
∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))))‘𝑛) = (𝑧 ∈ 𝑈 ↦ (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛))) |
70 | 59, 69 | eqtrd 2778 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → (seq1(
∘f + , 𝐺)‘𝑛) = (𝑧 ∈ 𝑈 ↦ (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛))) |
71 | 70 | fveq1d 6776 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → ((seq1(
∘f + , 𝐺)‘𝑛)‘𝑧) = ((𝑧 ∈ 𝑈 ↦ (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛))‘𝑧)) |
72 | 54 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → 𝑧 ∈ 𝑈) |
73 | | fvex 6787 |
. . . . . . . . . 10
⊢ (seq1( +
, (𝑚 ∈ ℕ ↦
((𝑧 ·
(log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛) ∈ V |
74 | | eqid 2738 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑈 ↦ (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛)) = (𝑧 ∈ 𝑈 ↦ (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛)) |
75 | 74 | fvmpt2 6886 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑈 ∧ (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛) ∈ V) → ((𝑧 ∈ 𝑈 ↦ (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛))‘𝑧) = (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛)) |
76 | 72, 73, 75 | sylancl 586 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → ((𝑧 ∈ 𝑈 ↦ (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛))‘𝑧) = (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛)) |
77 | 71, 76 | eqtrd 2778 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → ((seq1(
∘f + , 𝐺)‘𝑛)‘𝑧) = (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛)) |
78 | 50 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → seq1( ∘f + , 𝐺)(⇝𝑢‘𝑈)((⇝𝑢‘𝑈)‘seq1(
∘f + , 𝐺))) |
79 | 9, 10, 53, 54, 56, 77, 78 | ulmclm 25546 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) ⇝
(((⇝𝑢‘𝑈)‘seq1( ∘f + , 𝐺))‘𝑧)) |
80 | 9, 10, 22, 41, 79 | isumclim 15469 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → Σ𝑛 ∈ ℕ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) =
(((⇝𝑢‘𝑈)‘seq1( ∘f + , 𝐺))‘𝑧)) |
81 | | ulmcl 25540 |
. . . . . . . 8
⊢ (seq1(
∘f + , 𝐺)(⇝𝑢‘𝑈)((⇝𝑢‘𝑈)‘seq1(
∘f + , 𝐺))
→ ((⇝𝑢‘𝑈)‘seq1( ∘f + , 𝐺)):𝑈⟶ℂ) |
82 | 50, 81 | syl 17 |
. . . . . . 7
⊢ (𝜑 →
((⇝𝑢‘𝑈)‘seq1( ∘f + , 𝐺)):𝑈⟶ℂ) |
83 | 82 | ffvelrnda 6961 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) →
(((⇝𝑢‘𝑈)‘seq1( ∘f + , 𝐺))‘𝑧) ∈ ℂ) |
84 | 80, 83 | eqeltrd 2839 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → Σ𝑛 ∈ ℕ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) ∈ ℂ) |
85 | 4 | dmgmn0 26175 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ≠ 0) |
86 | 23, 85 | logcld 25726 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (log‘𝑧) ∈ ℂ) |
87 | 84, 86 | subcld 11332 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ𝑛 ∈ ℕ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) − (log‘𝑧)) ∈
ℂ) |
88 | 8, 87 | eqeltrd 2839 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (log Γ‘𝑧) ∈
ℂ) |
89 | 88 | ralrimiva 3103 |
. 2
⊢ (𝜑 → ∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ) |
90 | | ffn 6600 |
. . . . . 6
⊢
(((⇝𝑢‘𝑈)‘seq1( ∘f + , 𝐺)):𝑈⟶ℂ →
((⇝𝑢‘𝑈)‘seq1( ∘f + , 𝐺)) Fn 𝑈) |
91 | 50, 81, 90 | 3syl 18 |
. . . . 5
⊢ (𝜑 →
((⇝𝑢‘𝑈)‘seq1( ∘f + , 𝐺)) Fn 𝑈) |
92 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑧(⇝𝑢‘𝑈) |
93 | | nfcv 2907 |
. . . . . . . 8
⊢
Ⅎ𝑧1 |
94 | | nfcv 2907 |
. . . . . . . 8
⊢
Ⅎ𝑧
∘f + |
95 | | nfcv 2907 |
. . . . . . . . . 10
⊢
Ⅎ𝑧ℕ |
96 | | nfmpt1 5182 |
. . . . . . . . . 10
⊢
Ⅎ𝑧(𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))) |
97 | 95, 96 | nfmpt 5181 |
. . . . . . . . 9
⊢
Ⅎ𝑧(𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) |
98 | 47, 97 | nfcxfr 2905 |
. . . . . . . 8
⊢
Ⅎ𝑧𝐺 |
99 | 93, 94, 98 | nfseq 13731 |
. . . . . . 7
⊢
Ⅎ𝑧seq1(
∘f + , 𝐺) |
100 | 92, 99 | nffv 6784 |
. . . . . 6
⊢
Ⅎ𝑧((⇝𝑢‘𝑈)‘seq1(
∘f + , 𝐺)) |
101 | 100 | dffn5f 6840 |
. . . . 5
⊢
(((⇝𝑢‘𝑈)‘seq1( ∘f + , 𝐺)) Fn 𝑈 ↔
((⇝𝑢‘𝑈)‘seq1( ∘f + , 𝐺)) = (𝑧 ∈ 𝑈 ↦
(((⇝𝑢‘𝑈)‘seq1( ∘f + , 𝐺))‘𝑧))) |
102 | 91, 101 | sylib 217 |
. . . 4
⊢ (𝜑 →
((⇝𝑢‘𝑈)‘seq1( ∘f + , 𝐺)) = (𝑧 ∈ 𝑈 ↦
(((⇝𝑢‘𝑈)‘seq1( ∘f + , 𝐺))‘𝑧))) |
103 | 8 | oveq1d 7290 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((log Γ‘𝑧) + (log‘𝑧)) = ((Σ𝑛 ∈ ℕ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) − (log‘𝑧)) + (log‘𝑧))) |
104 | 84, 86 | npcand 11336 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((Σ𝑛 ∈ ℕ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) − (log‘𝑧)) + (log‘𝑧)) = Σ𝑛 ∈ ℕ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1)))) |
105 | 103, 104,
80 | 3eqtrrd 2783 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) →
(((⇝𝑢‘𝑈)‘seq1( ∘f + , 𝐺))‘𝑧) = ((log Γ‘𝑧) + (log‘𝑧))) |
106 | 105 | mpteq2dva 5174 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ 𝑈 ↦
(((⇝𝑢‘𝑈)‘seq1( ∘f + , 𝐺))‘𝑧)) = (𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))) |
107 | 102, 106 | eqtrd 2778 |
. . 3
⊢ (𝜑 →
((⇝𝑢‘𝑈)‘seq1( ∘f + , 𝐺)) = (𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))) |
108 | 50, 107 | breqtrd 5100 |
. 2
⊢ (𝜑 → seq1( ∘f
+ , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))) |
109 | 89, 108 | jca 512 |
1
⊢ (𝜑 → (∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ ∧ seq1(
∘f + , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))))) |