Step | Hyp | Ref
| Expression |
1 | | lgamucov.u |
. . 3
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))} |
2 | | lgamucov.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
3 | 1, 2 | lgamucov2 24565 |
. 2
⊢ (𝜑 → ∃𝑟 ∈ ℕ 𝐴 ∈ 𝑈) |
4 | | fveq2 6103 |
. . . . 5
⊢ (𝑧 = 𝐴 → (log Γ‘𝑧) = (log Γ‘𝐴)) |
5 | 4 | eleq1d 2672 |
. . . 4
⊢ (𝑧 = 𝐴 → ((log Γ‘𝑧) ∈ ℂ ↔ (log
Γ‘𝐴) ∈
ℂ)) |
6 | | simprl 790 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → 𝑟 ∈ ℕ) |
7 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑡 → (abs‘𝑥) = (abs‘𝑡)) |
8 | 7 | breq1d 4593 |
. . . . . . . . 9
⊢ (𝑥 = 𝑡 → ((abs‘𝑥) ≤ 𝑟 ↔ (abs‘𝑡) ≤ 𝑟)) |
9 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑡 → (𝑥 + 𝑘) = (𝑡 + 𝑘)) |
10 | 9 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑡 → (abs‘(𝑥 + 𝑘)) = (abs‘(𝑡 + 𝑘))) |
11 | 10 | breq2d 4595 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑡 → ((1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)) ↔ (1 / 𝑟) ≤ (abs‘(𝑡 + 𝑘)))) |
12 | 11 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑥 = 𝑡 → (∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)) ↔ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑡 + 𝑘)))) |
13 | 8, 12 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑥 = 𝑡 → (((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘))) ↔ ((abs‘𝑡) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑡 + 𝑘))))) |
14 | 13 | cbvrabv 3172 |
. . . . . . 7
⊢ {𝑥 ∈ ℂ ∣
((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 /
𝑟) ≤ (abs‘(𝑥 + 𝑘)))} = {𝑡 ∈ ℂ ∣ ((abs‘𝑡) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑡 + 𝑘)))} |
15 | 1, 14 | eqtri 2632 |
. . . . . 6
⊢ 𝑈 = {𝑡 ∈ ℂ ∣ ((abs‘𝑡) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑡 + 𝑘)))} |
16 | | eqid 2610 |
. . . . . 6
⊢ (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) |
17 | 6, 15, 16 | lgamgulm2 24562 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → (∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ ∧ seq1(
∘𝑓 + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) +
1))))))(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))))) |
18 | 17 | simpld 474 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → ∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ) |
19 | | simprr 792 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → 𝐴 ∈ 𝑈) |
20 | 5, 18, 19 | rspcdva 3288 |
. . 3
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → (log Γ‘𝐴) ∈
ℂ) |
21 | | nnuz 11599 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
22 | | 1zzd 11285 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → 1 ∈ ℤ) |
23 | | 1z 11284 |
. . . . . . . 8
⊢ 1 ∈
ℤ |
24 | | seqfn 12675 |
. . . . . . . 8
⊢ (1 ∈
ℤ → seq1( ∘𝑓 + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))) Fn
(ℤ≥‘1)) |
25 | 23, 24 | ax-mp 5 |
. . . . . . 7
⊢ seq1(
∘𝑓 + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))) Fn
(ℤ≥‘1) |
26 | 21 | fneq2i 5900 |
. . . . . . 7
⊢ (seq1(
∘𝑓 + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))) Fn ℕ ↔ seq1(
∘𝑓 + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))) Fn
(ℤ≥‘1)) |
27 | 25, 26 | mpbir 220 |
. . . . . 6
⊢ seq1(
∘𝑓 + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))) Fn ℕ |
28 | 17 | simprd 478 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → seq1( ∘𝑓
+ , (𝑚 ∈ ℕ
↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) +
1))))))(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))) |
29 | | ulmf2 23942 |
. . . . . 6
⊢ ((seq1(
∘𝑓 + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))) Fn ℕ ∧ seq1(
∘𝑓 + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) +
1))))))(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))) → seq1(
∘𝑓 + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))):ℕ⟶(ℂ
↑𝑚 𝑈)) |
30 | 27, 28, 29 | sylancr 694 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → seq1( ∘𝑓
+ , (𝑚 ∈ ℕ
↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))):ℕ⟶(ℂ
↑𝑚 𝑈)) |
31 | | seqex 12665 |
. . . . . 6
⊢ seq1( + ,
𝐺) ∈
V |
32 | 31 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → seq1( + , 𝐺) ∈ V) |
33 | | cnex 9896 |
. . . . . . . . 9
⊢ ℂ
∈ V |
34 | 1, 33 | rabex2 4742 |
. . . . . . . 8
⊢ 𝑈 ∈ V |
35 | 34 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → 𝑈 ∈ V) |
36 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
37 | 36, 21 | syl6eleq 2698 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
(ℤ≥‘1)) |
38 | | fz1ssnn 12243 |
. . . . . . . 8
⊢
(1...𝑛) ⊆
ℕ |
39 | 38 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ⊆
ℕ) |
40 | | ovex 6577 |
. . . . . . . 8
⊢ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) ∈ V |
41 | 40 | a1i 11 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ (𝑚 ∈ ℕ ∧ 𝑧 ∈ 𝑈)) → ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) ∈ V) |
42 | 35, 37, 39, 41 | seqof2 12721 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → (seq1(
∘𝑓 + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))))‘𝑛) = (𝑧 ∈ 𝑈 ↦ (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛))) |
43 | | simplr 788 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) ∧ 𝑚 ∈ ℕ) → 𝑧 = 𝐴) |
44 | 43 | oveq1d 6564 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) ∧ 𝑚 ∈ ℕ) → (𝑧 · (log‘((𝑚 + 1) / 𝑚))) = (𝐴 · (log‘((𝑚 + 1) / 𝑚)))) |
45 | 43 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) ∧ 𝑚 ∈ ℕ) → (𝑧 / 𝑚) = (𝐴 / 𝑚)) |
46 | 45 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) ∧ 𝑚 ∈ ℕ) → ((𝑧 / 𝑚) + 1) = ((𝐴 / 𝑚) + 1)) |
47 | 46 | fveq2d 6107 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) ∧ 𝑚 ∈ ℕ) → (log‘((𝑧 / 𝑚) + 1)) = (log‘((𝐴 / 𝑚) + 1))) |
48 | 44, 47 | oveq12d 6567 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) ∧ 𝑚 ∈ ℕ) → ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) = ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) |
49 | 48 | mpteq2dva 4672 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) → (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))) = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))) |
50 | | lgamcvglem.g |
. . . . . . . . 9
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) |
51 | 49, 50 | syl6eqr 2662 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) → (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))) = 𝐺) |
52 | 51 | seqeq3d 12671 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) → seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) = seq1( + , 𝐺)) |
53 | 52 | fveq1d 6105 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) → (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛) = (seq1( + , 𝐺)‘𝑛)) |
54 | | simplrr 797 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ 𝑈) |
55 | | fvex 6113 |
. . . . . . 7
⊢ (seq1( +
, 𝐺)‘𝑛) ∈ V |
56 | 55 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → (seq1( + , 𝐺)‘𝑛) ∈ V) |
57 | 42, 53, 54, 56 | fvmptd 6197 |
. . . . 5
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → ((seq1(
∘𝑓 + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))))‘𝑛)‘𝐴) = (seq1( + , 𝐺)‘𝑛)) |
58 | 21, 22, 30, 19, 32, 57, 28 | ulmclm 23945 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → seq1( + , 𝐺) ⇝ ((𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))‘𝐴)) |
59 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → (log‘𝑧) = (log‘𝐴)) |
60 | 4, 59 | oveq12d 6567 |
. . . . . 6
⊢ (𝑧 = 𝐴 → ((log Γ‘𝑧) + (log‘𝑧)) = ((log Γ‘𝐴) + (log‘𝐴))) |
61 | | eqid 2610 |
. . . . . 6
⊢ (𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))) = (𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))) |
62 | | ovex 6577 |
. . . . . 6
⊢ ((log
Γ‘𝐴) +
(log‘𝐴)) ∈
V |
63 | 60, 61, 62 | fvmpt 6191 |
. . . . 5
⊢ (𝐴 ∈ 𝑈 → ((𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))‘𝐴) = ((log Γ‘𝐴) + (log‘𝐴))) |
64 | 19, 63 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → ((𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))‘𝐴) = ((log Γ‘𝐴) + (log‘𝐴))) |
65 | 58, 64 | breqtrd 4609 |
. . 3
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → seq1( + , 𝐺) ⇝ ((log Γ‘𝐴) + (log‘𝐴))) |
66 | 20, 65 | jca 553 |
. 2
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → ((log Γ‘𝐴) ∈ ℂ ∧ seq1( + ,
𝐺) ⇝ ((log
Γ‘𝐴) +
(log‘𝐴)))) |
67 | 3, 66 | rexlimddv 3017 |
1
⊢ (𝜑 → ((log Γ‘𝐴) ∈ ℂ ∧ seq1( + ,
𝐺) ⇝ ((log
Γ‘𝐴) +
(log‘𝐴)))) |