Step | Hyp | Ref
| Expression |
1 | | lgamucov.u |
. . 3
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))} |
2 | | lgamucov.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
3 | 1, 2 | lgamucov2 25921 |
. 2
⊢ (𝜑 → ∃𝑟 ∈ ℕ 𝐴 ∈ 𝑈) |
4 | | fveq2 6717 |
. . . . 5
⊢ (𝑧 = 𝐴 → (log Γ‘𝑧) = (log Γ‘𝐴)) |
5 | 4 | eleq1d 2822 |
. . . 4
⊢ (𝑧 = 𝐴 → ((log Γ‘𝑧) ∈ ℂ ↔ (log
Γ‘𝐴) ∈
ℂ)) |
6 | | simprl 771 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → 𝑟 ∈ ℕ) |
7 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑡 → (abs‘𝑥) = (abs‘𝑡)) |
8 | 7 | breq1d 5063 |
. . . . . . . . 9
⊢ (𝑥 = 𝑡 → ((abs‘𝑥) ≤ 𝑟 ↔ (abs‘𝑡) ≤ 𝑟)) |
9 | | fvoveq1 7236 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑡 → (abs‘(𝑥 + 𝑘)) = (abs‘(𝑡 + 𝑘))) |
10 | 9 | breq2d 5065 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑡 → ((1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)) ↔ (1 / 𝑟) ≤ (abs‘(𝑡 + 𝑘)))) |
11 | 10 | ralbidv 3118 |
. . . . . . . . 9
⊢ (𝑥 = 𝑡 → (∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)) ↔ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑡 + 𝑘)))) |
12 | 8, 11 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑥 = 𝑡 → (((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘))) ↔ ((abs‘𝑡) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑡 + 𝑘))))) |
13 | 12 | cbvrabv 3402 |
. . . . . . 7
⊢ {𝑥 ∈ ℂ ∣
((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 /
𝑟) ≤ (abs‘(𝑥 + 𝑘)))} = {𝑡 ∈ ℂ ∣ ((abs‘𝑡) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑡 + 𝑘)))} |
14 | 1, 13 | eqtri 2765 |
. . . . . 6
⊢ 𝑈 = {𝑡 ∈ ℂ ∣ ((abs‘𝑡) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑡 + 𝑘)))} |
15 | | eqid 2737 |
. . . . . 6
⊢ (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) |
16 | 6, 14, 15 | lgamgulm2 25918 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → (∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ ∧ seq1(
∘f + , (𝑚
∈ ℕ ↦ (𝑧
∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) +
1))))))(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))))) |
17 | 16 | simpld 498 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → ∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ) |
18 | | simprr 773 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → 𝐴 ∈ 𝑈) |
19 | 5, 17, 18 | rspcdva 3539 |
. . 3
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → (log Γ‘𝐴) ∈
ℂ) |
20 | | nnuz 12477 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
21 | | 1zzd 12208 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → 1 ∈ ℤ) |
22 | | 1z 12207 |
. . . . . . . 8
⊢ 1 ∈
ℤ |
23 | | seqfn 13586 |
. . . . . . . 8
⊢ (1 ∈
ℤ → seq1( ∘f + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))) Fn
(ℤ≥‘1)) |
24 | 22, 23 | ax-mp 5 |
. . . . . . 7
⊢ seq1(
∘f + , (𝑚
∈ ℕ ↦ (𝑧
∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))) Fn
(ℤ≥‘1) |
25 | 20 | fneq2i 6477 |
. . . . . . 7
⊢ (seq1(
∘f + , (𝑚
∈ ℕ ↦ (𝑧
∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))) Fn ℕ ↔ seq1(
∘f + , (𝑚
∈ ℕ ↦ (𝑧
∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))) Fn
(ℤ≥‘1)) |
26 | 24, 25 | mpbir 234 |
. . . . . 6
⊢ seq1(
∘f + , (𝑚
∈ ℕ ↦ (𝑧
∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))) Fn ℕ |
27 | 16 | simprd 499 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → seq1( ∘f + ,
(𝑚 ∈ ℕ ↦
(𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) +
1))))))(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))) |
28 | | ulmf2 25276 |
. . . . . 6
⊢ ((seq1(
∘f + , (𝑚
∈ ℕ ↦ (𝑧
∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))) Fn ℕ ∧ seq1(
∘f + , (𝑚
∈ ℕ ↦ (𝑧
∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) +
1))))))(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))) → seq1(
∘f + , (𝑚
∈ ℕ ↦ (𝑧
∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))):ℕ⟶(ℂ
↑m 𝑈)) |
29 | 26, 27, 28 | sylancr 590 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → seq1( ∘f + ,
(𝑚 ∈ ℕ ↦
(𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))):ℕ⟶(ℂ
↑m 𝑈)) |
30 | | seqex 13576 |
. . . . . 6
⊢ seq1( + ,
𝐺) ∈
V |
31 | 30 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → seq1( + , 𝐺) ∈ V) |
32 | | cnex 10810 |
. . . . . . . . 9
⊢ ℂ
∈ V |
33 | 1, 32 | rabex2 5227 |
. . . . . . . 8
⊢ 𝑈 ∈ V |
34 | 33 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → 𝑈 ∈ V) |
35 | | simpr 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
36 | 35, 20 | eleqtrdi 2848 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
(ℤ≥‘1)) |
37 | | fz1ssnn 13143 |
. . . . . . . 8
⊢
(1...𝑛) ⊆
ℕ |
38 | 37 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ⊆
ℕ) |
39 | | ovexd 7248 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ (𝑚 ∈ ℕ ∧ 𝑧 ∈ 𝑈)) → ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) ∈ V) |
40 | 34, 36, 38, 39 | seqof2 13634 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → (seq1(
∘f + , (𝑚
∈ ℕ ↦ (𝑧
∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))))‘𝑛) = (𝑧 ∈ 𝑈 ↦ (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛))) |
41 | | simplr 769 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) ∧ 𝑚 ∈ ℕ) → 𝑧 = 𝐴) |
42 | 41 | oveq1d 7228 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) ∧ 𝑚 ∈ ℕ) → (𝑧 · (log‘((𝑚 + 1) / 𝑚))) = (𝐴 · (log‘((𝑚 + 1) / 𝑚)))) |
43 | 41 | oveq1d 7228 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) ∧ 𝑚 ∈ ℕ) → (𝑧 / 𝑚) = (𝐴 / 𝑚)) |
44 | 43 | fvoveq1d 7235 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) ∧ 𝑚 ∈ ℕ) → (log‘((𝑧 / 𝑚) + 1)) = (log‘((𝐴 / 𝑚) + 1))) |
45 | 42, 44 | oveq12d 7231 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) ∧ 𝑚 ∈ ℕ) → ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) = ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) |
46 | 45 | mpteq2dva 5150 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) → (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))) = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))) |
47 | | lgamcvglem.g |
. . . . . . . . 9
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) |
48 | 46, 47 | eqtr4di 2796 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) → (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))) = 𝐺) |
49 | 48 | seqeq3d 13582 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) → seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) = seq1( + , 𝐺)) |
50 | 49 | fveq1d 6719 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) → (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛) = (seq1( + , 𝐺)‘𝑛)) |
51 | | simplrr 778 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ 𝑈) |
52 | | fvexd 6732 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → (seq1( + , 𝐺)‘𝑛) ∈ V) |
53 | 40, 50, 51, 52 | fvmptd 6825 |
. . . . 5
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → ((seq1(
∘f + , (𝑚
∈ ℕ ↦ (𝑧
∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))))‘𝑛)‘𝐴) = (seq1( + , 𝐺)‘𝑛)) |
54 | 20, 21, 29, 18, 31, 53, 27 | ulmclm 25279 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → seq1( + , 𝐺) ⇝ ((𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))‘𝐴)) |
55 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → (log‘𝑧) = (log‘𝐴)) |
56 | 4, 55 | oveq12d 7231 |
. . . . . 6
⊢ (𝑧 = 𝐴 → ((log Γ‘𝑧) + (log‘𝑧)) = ((log Γ‘𝐴) + (log‘𝐴))) |
57 | | eqid 2737 |
. . . . . 6
⊢ (𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))) = (𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))) |
58 | | ovex 7246 |
. . . . . 6
⊢ ((log
Γ‘𝐴) +
(log‘𝐴)) ∈
V |
59 | 56, 57, 58 | fvmpt 6818 |
. . . . 5
⊢ (𝐴 ∈ 𝑈 → ((𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))‘𝐴) = ((log Γ‘𝐴) + (log‘𝐴))) |
60 | 18, 59 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → ((𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))‘𝐴) = ((log Γ‘𝐴) + (log‘𝐴))) |
61 | 54, 60 | breqtrd 5079 |
. . 3
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → seq1( + , 𝐺) ⇝ ((log Γ‘𝐴) + (log‘𝐴))) |
62 | 19, 61 | jca 515 |
. 2
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → ((log Γ‘𝐴) ∈ ℂ ∧ seq1( + ,
𝐺) ⇝ ((log
Γ‘𝐴) +
(log‘𝐴)))) |
63 | 3, 62 | rexlimddv 3210 |
1
⊢ (𝜑 → ((log Γ‘𝐴) ∈ ℂ ∧ seq1( + ,
𝐺) ⇝ ((log
Γ‘𝐴) +
(log‘𝐴)))) |