Step | Hyp | Ref
| Expression |
1 | | lgamgulm.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ ℕ) |
2 | | lgamgulm.u |
. . . . . . 7
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} |
3 | 1, 2 | lgamgulmlem1 24555 |
. . . . . 6
⊢ (𝜑 → 𝑈 ⊆ (ℂ ∖ (ℤ ∖
ℕ))) |
4 | 3 | sselda 3568 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
5 | | ovex 6577 |
. . . . 5
⊢
(Σ𝑛 ∈
ℕ ((𝑧 ·
(log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) − (log‘𝑧)) ∈ V |
6 | | df-lgam 24545 |
. . . . . 6
⊢ log
Γ = (𝑧 ∈
(ℂ ∖ (ℤ ∖ ℕ)) ↦ (Σ𝑛 ∈ ℕ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) − (log‘𝑧))) |
7 | 6 | fvmpt2 6200 |
. . . . 5
⊢ ((𝑧 ∈ (ℂ ∖
(ℤ ∖ ℕ)) ∧ (Σ𝑛 ∈ ℕ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) − (log‘𝑧)) ∈ V) → (log
Γ‘𝑧) =
(Σ𝑛 ∈ ℕ
((𝑧 ·
(log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) − (log‘𝑧))) |
8 | 4, 5, 7 | sylancl 693 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (log Γ‘𝑧) = (Σ𝑛 ∈ ℕ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) − (log‘𝑧))) |
9 | | nnuz 11599 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
10 | | 1zzd 11285 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 1 ∈ ℤ) |
11 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1)) |
12 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → 𝑚 = 𝑛) |
13 | 11, 12 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → ((𝑚 + 1) / 𝑚) = ((𝑛 + 1) / 𝑛)) |
14 | 13 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (log‘((𝑚 + 1) / 𝑚)) = (log‘((𝑛 + 1) / 𝑛))) |
15 | 14 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (𝑧 · (log‘((𝑚 + 1) / 𝑚))) = (𝑧 · (log‘((𝑛 + 1) / 𝑛)))) |
16 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝑧 / 𝑚) = (𝑧 / 𝑛)) |
17 | 16 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → ((𝑧 / 𝑚) + 1) = ((𝑧 / 𝑛) + 1)) |
18 | 17 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (log‘((𝑧 / 𝑚) + 1)) = (log‘((𝑧 / 𝑛) + 1))) |
19 | 15, 18 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) = ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1)))) |
20 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))) = (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))) |
21 | | ovex 6577 |
. . . . . . . . 9
⊢ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) ∈ V |
22 | 19, 20, 21 | fvmpt 6191 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))‘𝑛) = ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1)))) |
23 | 22 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))‘𝑛) = ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1)))) |
24 | 4 | eldifad 3552 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ ℂ) |
25 | 24 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → 𝑧 ∈ ℂ) |
26 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
27 | 26 | peano2nnd 10914 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ) |
28 | 27 | nnrpd 11746 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈
ℝ+) |
29 | 26 | nnrpd 11746 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ+) |
30 | 28, 29 | rpdivcld 11765 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → ((𝑛 + 1) / 𝑛) ∈
ℝ+) |
31 | 30 | relogcld 24173 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → (log‘((𝑛 + 1) / 𝑛)) ∈ ℝ) |
32 | 31 | recnd 9947 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → (log‘((𝑛 + 1) / 𝑛)) ∈ ℂ) |
33 | 25, 32 | mulcld 9939 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → (𝑧 · (log‘((𝑛 + 1) / 𝑛))) ∈ ℂ) |
34 | 26 | nncnd 10913 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ) |
35 | 26 | nnne0d 10942 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0) |
36 | 25, 34, 35 | divcld 10680 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → (𝑧 / 𝑛) ∈ ℂ) |
37 | | 1cnd 9935 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → 1 ∈
ℂ) |
38 | 36, 37 | addcld 9938 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → ((𝑧 / 𝑛) + 1) ∈ ℂ) |
39 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → 𝑧 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
40 | 39, 26 | dmgmdivn0 24554 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → ((𝑧 / 𝑛) + 1) ≠ 0) |
41 | 38, 40 | logcld 24121 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → (log‘((𝑧 / 𝑛) + 1)) ∈ ℂ) |
42 | 33, 41 | subcld 10271 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) ∈ ℂ) |
43 | | 1z 11284 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
44 | | seqfn 12675 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℤ → seq1( ∘𝑓 + , 𝐺) Fn
(ℤ≥‘1)) |
45 | 43, 44 | ax-mp 5 |
. . . . . . . . . . 11
⊢ seq1(
∘𝑓 + , 𝐺) Fn
(ℤ≥‘1) |
46 | 9 | fneq2i 5900 |
. . . . . . . . . . 11
⊢ (seq1(
∘𝑓 + , 𝐺) Fn ℕ ↔ seq1(
∘𝑓 + , 𝐺) Fn
(ℤ≥‘1)) |
47 | 45, 46 | mpbir 220 |
. . . . . . . . . 10
⊢ seq1(
∘𝑓 + , 𝐺) Fn ℕ |
48 | | lgamgulm.g |
. . . . . . . . . . . 12
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) |
49 | 1, 2, 48 | lgamgulm 24561 |
. . . . . . . . . . 11
⊢ (𝜑 → seq1(
∘𝑓 + , 𝐺) ∈ dom
(⇝𝑢‘𝑈)) |
50 | | ulmdm 23951 |
. . . . . . . . . . 11
⊢ (seq1(
∘𝑓 + , 𝐺) ∈ dom
(⇝𝑢‘𝑈) ↔ seq1( ∘𝑓 +
, 𝐺)(⇝𝑢‘𝑈)((⇝𝑢‘𝑈)‘seq1(
∘𝑓 + , 𝐺))) |
51 | 49, 50 | sylib 207 |
. . . . . . . . . 10
⊢ (𝜑 → seq1(
∘𝑓 + , 𝐺)(⇝𝑢‘𝑈)((⇝𝑢‘𝑈)‘seq1(
∘𝑓 + , 𝐺))) |
52 | | ulmf2 23942 |
. . . . . . . . . 10
⊢ ((seq1(
∘𝑓 + , 𝐺) Fn ℕ ∧ seq1(
∘𝑓 + , 𝐺)(⇝𝑢‘𝑈)((⇝𝑢‘𝑈)‘seq1(
∘𝑓 + , 𝐺))) → seq1( ∘𝑓
+ , 𝐺):ℕ⟶(ℂ
↑𝑚 𝑈)) |
53 | 47, 51, 52 | sylancr 694 |
. . . . . . . . 9
⊢ (𝜑 → seq1(
∘𝑓 + , 𝐺):ℕ⟶(ℂ
↑𝑚 𝑈)) |
54 | 53 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → seq1( ∘𝑓 +
, 𝐺):ℕ⟶(ℂ
↑𝑚 𝑈)) |
55 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ 𝑈) |
56 | | seqex 12665 |
. . . . . . . . 9
⊢ seq1( + ,
(𝑚 ∈ ℕ ↦
((𝑧 ·
(log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) ∈ V |
57 | 56 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) ∈ V) |
58 | 48 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))) |
59 | 58 | seqeq3d 12671 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → seq1(
∘𝑓 + , 𝐺) = seq1( ∘𝑓 + ,
(𝑚 ∈ ℕ ↦
(𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))))) |
60 | 59 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → (seq1(
∘𝑓 + , 𝐺)‘𝑛) = (seq1( ∘𝑓 + ,
(𝑚 ∈ ℕ ↦
(𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))))‘𝑛)) |
61 | | cnex 9896 |
. . . . . . . . . . . . . . 15
⊢ ℂ
∈ V |
62 | 2, 61 | rabex2 4742 |
. . . . . . . . . . . . . 14
⊢ 𝑈 ∈ V |
63 | 62 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑈 ∈ V) |
64 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
65 | 64, 9 | syl6eleq 2698 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
(ℤ≥‘1)) |
66 | | fz1ssnn 12243 |
. . . . . . . . . . . . . 14
⊢
(1...𝑛) ⊆
ℕ |
67 | 66 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...𝑛) ⊆
ℕ) |
68 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) ∈ V |
69 | 68 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑚 ∈ ℕ ∧ 𝑧 ∈ 𝑈)) → ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) ∈ V) |
70 | 63, 65, 67, 69 | seqof2 12721 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1(
∘𝑓 + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))))‘𝑛) = (𝑧 ∈ 𝑈 ↦ (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛))) |
71 | 70 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → (seq1(
∘𝑓 + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))))‘𝑛) = (𝑧 ∈ 𝑈 ↦ (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛))) |
72 | 60, 71 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → (seq1(
∘𝑓 + , 𝐺)‘𝑛) = (𝑧 ∈ 𝑈 ↦ (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛))) |
73 | 72 | fveq1d 6105 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → ((seq1(
∘𝑓 + , 𝐺)‘𝑛)‘𝑧) = ((𝑧 ∈ 𝑈 ↦ (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛))‘𝑧)) |
74 | 55 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → 𝑧 ∈ 𝑈) |
75 | | fvex 6113 |
. . . . . . . . . 10
⊢ (seq1( +
, (𝑚 ∈ ℕ ↦
((𝑧 ·
(log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛) ∈ V |
76 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑈 ↦ (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛)) = (𝑧 ∈ 𝑈 ↦ (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛)) |
77 | 76 | fvmpt2 6200 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑈 ∧ (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛) ∈ V) → ((𝑧 ∈ 𝑈 ↦ (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛))‘𝑧) = (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛)) |
78 | 74, 75, 77 | sylancl 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → ((𝑧 ∈ 𝑈 ↦ (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛))‘𝑧) = (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛)) |
79 | 73, 78 | eqtrd 2644 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑛 ∈ ℕ) → ((seq1(
∘𝑓 + , 𝐺)‘𝑛)‘𝑧) = (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛)) |
80 | 51 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → seq1( ∘𝑓 +
, 𝐺)(⇝𝑢‘𝑈)((⇝𝑢‘𝑈)‘seq1(
∘𝑓 + , 𝐺))) |
81 | 9, 10, 54, 55, 57, 79, 80 | ulmclm 23945 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) ⇝
(((⇝𝑢‘𝑈)‘seq1( ∘𝑓 +
, 𝐺))‘𝑧)) |
82 | 9, 10, 23, 42, 81 | isumclim 14330 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → Σ𝑛 ∈ ℕ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) =
(((⇝𝑢‘𝑈)‘seq1( ∘𝑓 +
, 𝐺))‘𝑧)) |
83 | | ulmcl 23939 |
. . . . . . . 8
⊢ (seq1(
∘𝑓 + , 𝐺)(⇝𝑢‘𝑈)((⇝𝑢‘𝑈)‘seq1(
∘𝑓 + , 𝐺)) →
((⇝𝑢‘𝑈)‘seq1( ∘𝑓 +
, 𝐺)):𝑈⟶ℂ) |
84 | 51, 83 | syl 17 |
. . . . . . 7
⊢ (𝜑 →
((⇝𝑢‘𝑈)‘seq1( ∘𝑓 +
, 𝐺)):𝑈⟶ℂ) |
85 | 84 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) →
(((⇝𝑢‘𝑈)‘seq1( ∘𝑓 +
, 𝐺))‘𝑧) ∈
ℂ) |
86 | 82, 85 | eqeltrd 2688 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → Σ𝑛 ∈ ℕ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) ∈ ℂ) |
87 | 4 | dmgmn0 24552 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ≠ 0) |
88 | 24, 87 | logcld 24121 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (log‘𝑧) ∈ ℂ) |
89 | 86, 88 | subcld 10271 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ𝑛 ∈ ℕ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) − (log‘𝑧)) ∈
ℂ) |
90 | 8, 89 | eqeltrd 2688 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (log Γ‘𝑧) ∈
ℂ) |
91 | 90 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ) |
92 | | ffn 5958 |
. . . . . 6
⊢
(((⇝𝑢‘𝑈)‘seq1( ∘𝑓 +
, 𝐺)):𝑈⟶ℂ →
((⇝𝑢‘𝑈)‘seq1( ∘𝑓 +
, 𝐺)) Fn 𝑈) |
93 | 51, 83, 92 | 3syl 18 |
. . . . 5
⊢ (𝜑 →
((⇝𝑢‘𝑈)‘seq1( ∘𝑓 +
, 𝐺)) Fn 𝑈) |
94 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑧(⇝𝑢‘𝑈) |
95 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑧1 |
96 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑧
∘𝑓 + |
97 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑧ℕ |
98 | | nfmpt1 4675 |
. . . . . . . . . 10
⊢
Ⅎ𝑧(𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))) |
99 | 97, 98 | nfmpt 4674 |
. . . . . . . . 9
⊢
Ⅎ𝑧(𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) |
100 | 48, 99 | nfcxfr 2749 |
. . . . . . . 8
⊢
Ⅎ𝑧𝐺 |
101 | 95, 96, 100 | nfseq 12673 |
. . . . . . 7
⊢
Ⅎ𝑧seq1(
∘𝑓 + , 𝐺) |
102 | 94, 101 | nffv 6110 |
. . . . . 6
⊢
Ⅎ𝑧((⇝𝑢‘𝑈)‘seq1(
∘𝑓 + , 𝐺)) |
103 | 102 | dffn5f 6162 |
. . . . 5
⊢
(((⇝𝑢‘𝑈)‘seq1( ∘𝑓 +
, 𝐺)) Fn 𝑈 ↔
((⇝𝑢‘𝑈)‘seq1( ∘𝑓 +
, 𝐺)) = (𝑧 ∈ 𝑈 ↦
(((⇝𝑢‘𝑈)‘seq1( ∘𝑓 +
, 𝐺))‘𝑧))) |
104 | 93, 103 | sylib 207 |
. . . 4
⊢ (𝜑 →
((⇝𝑢‘𝑈)‘seq1( ∘𝑓 +
, 𝐺)) = (𝑧 ∈ 𝑈 ↦
(((⇝𝑢‘𝑈)‘seq1( ∘𝑓 +
, 𝐺))‘𝑧))) |
105 | 8 | oveq1d 6564 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((log Γ‘𝑧) + (log‘𝑧)) = ((Σ𝑛 ∈ ℕ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) − (log‘𝑧)) + (log‘𝑧))) |
106 | 86, 88 | npcand 10275 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((Σ𝑛 ∈ ℕ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) − (log‘𝑧)) + (log‘𝑧)) = Σ𝑛 ∈ ℕ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1)))) |
107 | 105, 106,
82 | 3eqtrrd 2649 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) →
(((⇝𝑢‘𝑈)‘seq1( ∘𝑓 +
, 𝐺))‘𝑧) = ((log Γ‘𝑧) + (log‘𝑧))) |
108 | 107 | mpteq2dva 4672 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ 𝑈 ↦
(((⇝𝑢‘𝑈)‘seq1( ∘𝑓 +
, 𝐺))‘𝑧)) = (𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))) |
109 | 104, 108 | eqtrd 2644 |
. . 3
⊢ (𝜑 →
((⇝𝑢‘𝑈)‘seq1( ∘𝑓 +
, 𝐺)) = (𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))) |
110 | 51, 109 | breqtrd 4609 |
. 2
⊢ (𝜑 → seq1(
∘𝑓 + , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))) |
111 | 91, 110 | jca 553 |
1
⊢ (𝜑 → (∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ ∧ seq1(
∘𝑓 + , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))))) |