Step | Hyp | Ref
| Expression |
1 | | breq2 5034 |
. . 3
⊢ ((𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))) = if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) → ((abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))) ↔ (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))))) |
2 | | breq2 5034 |
. . 3
⊢ (((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)) = if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) → ((abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)) ↔ (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))))) |
3 | | lgamgulm.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ ℕ) |
4 | 3 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑅 ∈ ℕ) |
5 | 4 | adantr 484 |
. . . 4
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) ∧ (2 · 𝑅) ≤ 𝑛) → 𝑅 ∈ ℕ) |
6 | | lgamgulm.u |
. . . . 5
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} |
7 | | fveq2 6674 |
. . . . . . . 8
⊢ (𝑥 = 𝑡 → (abs‘𝑥) = (abs‘𝑡)) |
8 | 7 | breq1d 5040 |
. . . . . . 7
⊢ (𝑥 = 𝑡 → ((abs‘𝑥) ≤ 𝑅 ↔ (abs‘𝑡) ≤ 𝑅)) |
9 | | fvoveq1 7193 |
. . . . . . . . 9
⊢ (𝑥 = 𝑡 → (abs‘(𝑥 + 𝑘)) = (abs‘(𝑡 + 𝑘))) |
10 | 9 | breq2d 5042 |
. . . . . . . 8
⊢ (𝑥 = 𝑡 → ((1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝑡 + 𝑘)))) |
11 | 10 | ralbidv 3109 |
. . . . . . 7
⊢ (𝑥 = 𝑡 → (∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑡 + 𝑘)))) |
12 | 8, 11 | anbi12d 634 |
. . . . . 6
⊢ (𝑥 = 𝑡 → (((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘))) ↔ ((abs‘𝑡) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑡 + 𝑘))))) |
13 | 12 | cbvrabv 3393 |
. . . . 5
⊢ {𝑥 ∈ ℂ ∣
((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 /
𝑅) ≤ (abs‘(𝑥 + 𝑘)))} = {𝑡 ∈ ℂ ∣ ((abs‘𝑡) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑡 + 𝑘)))} |
14 | 6, 13 | eqtri 2761 |
. . . 4
⊢ 𝑈 = {𝑡 ∈ ℂ ∣ ((abs‘𝑡) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑡 + 𝑘)))} |
15 | | simplrl 777 |
. . . 4
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) ∧ (2 · 𝑅) ≤ 𝑛) → 𝑛 ∈ ℕ) |
16 | | simprr 773 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈) |
17 | 16 | adantr 484 |
. . . 4
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) ∧ (2 · 𝑅) ≤ 𝑛) → 𝑦 ∈ 𝑈) |
18 | | simpr 488 |
. . . 4
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) ∧ (2 · 𝑅) ≤ 𝑛) → (2 · 𝑅) ≤ 𝑛) |
19 | 5, 14, 15, 17, 18 | lgamgulmlem3 25768 |
. . 3
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) ∧ (2 · 𝑅) ≤ 𝑛) → (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2)))) |
20 | 3, 6 | lgamgulmlem1 25766 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ⊆ (ℂ ∖ (ℤ ∖
ℕ))) |
21 | 20 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑈 ⊆ (ℂ ∖ (ℤ ∖
ℕ))) |
22 | 21, 16 | sseldd 3878 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
23 | 22 | eldifad 3855 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ ℂ) |
24 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑛 ∈ ℕ) |
25 | 24 | peano2nnd 11733 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑛 + 1) ∈ ℕ) |
26 | 25 | nnrpd 12512 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑛 + 1) ∈
ℝ+) |
27 | 24 | nnrpd 12512 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑛 ∈ ℝ+) |
28 | 26, 27 | rpdivcld 12531 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑛 + 1) / 𝑛) ∈
ℝ+) |
29 | 28 | relogcld 25366 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘((𝑛 + 1) / 𝑛)) ∈ ℝ) |
30 | 29 | recnd 10747 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘((𝑛 + 1) / 𝑛)) ∈ ℂ) |
31 | 23, 30 | mulcld 10739 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑦 · (log‘((𝑛 + 1) / 𝑛))) ∈ ℂ) |
32 | 24 | nncnd 11732 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑛 ∈ ℂ) |
33 | 24 | nnne0d 11766 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑛 ≠ 0) |
34 | 23, 32, 33 | divcld 11494 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑦 / 𝑛) ∈ ℂ) |
35 | | 1cnd 10714 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 1 ∈ ℂ) |
36 | 34, 35 | addcld 10738 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑦 / 𝑛) + 1) ∈ ℂ) |
37 | 22, 24 | dmgmdivn0 25765 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑦 / 𝑛) + 1) ≠ 0) |
38 | 36, 37 | logcld 25314 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘((𝑦 / 𝑛) + 1)) ∈ ℂ) |
39 | 31, 38 | subcld 11075 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1))) ∈ ℂ) |
40 | 39 | abscld 14886 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ∈ ℝ) |
41 | 31 | abscld 14886 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 · (log‘((𝑛 + 1) / 𝑛)))) ∈ ℝ) |
42 | 38 | abscld 14886 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(log‘((𝑦 / 𝑛) + 1))) ∈ ℝ) |
43 | 41, 42 | readdcld 10748 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘(𝑦 · (log‘((𝑛 + 1) / 𝑛)))) + (abs‘(log‘((𝑦 / 𝑛) + 1)))) ∈ ℝ) |
44 | 4 | nnred 11731 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑅 ∈ ℝ) |
45 | 44, 29 | remulcld 10749 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 · (log‘((𝑛 + 1) / 𝑛))) ∈ ℝ) |
46 | 4 | peano2nnd 11733 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 + 1) ∈ ℕ) |
47 | 46 | nnrpd 12512 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 + 1) ∈
ℝ+) |
48 | 47, 27 | rpmulcld 12530 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑅 + 1) · 𝑛) ∈
ℝ+) |
49 | 48 | relogcld 25366 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘((𝑅 + 1) · 𝑛)) ∈ ℝ) |
50 | | pire 25203 |
. . . . . . . 8
⊢ π
∈ ℝ |
51 | 50 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → π ∈
ℝ) |
52 | 49, 51 | readdcld 10748 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((log‘((𝑅 + 1) · 𝑛)) + π) ∈ ℝ) |
53 | 45, 52 | readdcld 10748 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)) ∈ ℝ) |
54 | 31, 38 | abs2dif2d 14908 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ ((abs‘(𝑦 · (log‘((𝑛 + 1) / 𝑛)))) + (abs‘(log‘((𝑦 / 𝑛) + 1))))) |
55 | 23, 30 | absmuld 14904 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 · (log‘((𝑛 + 1) / 𝑛)))) = ((abs‘𝑦) · (abs‘(log‘((𝑛 + 1) / 𝑛))))) |
56 | 28 | rpred 12514 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑛 + 1) / 𝑛) ∈ ℝ) |
57 | 32 | mulid2d 10737 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 · 𝑛) = 𝑛) |
58 | 24 | nnred 11731 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑛 ∈ ℝ) |
59 | 58 | lep1d 11649 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑛 ≤ (𝑛 + 1)) |
60 | 57, 59 | eqbrtrd 5052 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 · 𝑛) ≤ (𝑛 + 1)) |
61 | | 1red 10720 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 1 ∈ ℝ) |
62 | 58, 61 | readdcld 10748 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑛 + 1) ∈ ℝ) |
63 | 61, 62, 27 | lemuldivd 12563 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((1 · 𝑛) ≤ (𝑛 + 1) ↔ 1 ≤ ((𝑛 + 1) / 𝑛))) |
64 | 60, 63 | mpbid 235 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 1 ≤ ((𝑛 + 1) / 𝑛)) |
65 | 56, 64 | logge0d 25373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 0 ≤ (log‘((𝑛 + 1) / 𝑛))) |
66 | 29, 65 | absidd 14872 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(log‘((𝑛 + 1) / 𝑛))) = (log‘((𝑛 + 1) / 𝑛))) |
67 | 66 | oveq2d 7186 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘𝑦) · (abs‘(log‘((𝑛 + 1) / 𝑛)))) = ((abs‘𝑦) · (log‘((𝑛 + 1) / 𝑛)))) |
68 | 55, 67 | eqtrd 2773 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 · (log‘((𝑛 + 1) / 𝑛)))) = ((abs‘𝑦) · (log‘((𝑛 + 1) / 𝑛)))) |
69 | 23 | abscld 14886 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘𝑦) ∈ ℝ) |
70 | | fveq2 6674 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (abs‘𝑥) = (abs‘𝑦)) |
71 | 70 | breq1d 5040 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ((abs‘𝑥) ≤ 𝑅 ↔ (abs‘𝑦) ≤ 𝑅)) |
72 | | fvoveq1 7193 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (abs‘(𝑥 + 𝑘)) = (abs‘(𝑦 + 𝑘))) |
73 | 72 | breq2d 5042 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘)))) |
74 | 73 | ralbidv 3109 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘)))) |
75 | 71, 74 | anbi12d 634 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘))) ↔ ((abs‘𝑦) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘))))) |
76 | 75, 6 | elrab2 3591 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑈 ↔ (𝑦 ∈ ℂ ∧ ((abs‘𝑦) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘))))) |
77 | 76 | simprbi 500 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑈 → ((abs‘𝑦) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘)))) |
78 | 77 | ad2antll 729 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘𝑦) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘)))) |
79 | 78 | simpld 498 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘𝑦) ≤ 𝑅) |
80 | 69, 44, 29, 65, 79 | lemul1ad 11657 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘𝑦) · (log‘((𝑛 + 1) / 𝑛))) ≤ (𝑅 · (log‘((𝑛 + 1) / 𝑛)))) |
81 | 68, 80 | eqbrtrd 5052 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 · (log‘((𝑛 + 1) / 𝑛)))) ≤ (𝑅 · (log‘((𝑛 + 1) / 𝑛)))) |
82 | 36, 37 | absrpcld 14898 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 / 𝑛) + 1)) ∈
ℝ+) |
83 | 82 | relogcld 25366 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘(abs‘((𝑦 / 𝑛) + 1))) ∈ ℝ) |
84 | 83 | recnd 10747 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘(abs‘((𝑦 / 𝑛) + 1))) ∈ ℂ) |
85 | 84 | abscld 14886 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) →
(abs‘(log‘(abs‘((𝑦 / 𝑛) + 1)))) ∈ ℝ) |
86 | 85, 51 | readdcld 10748 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) →
((abs‘(log‘(abs‘((𝑦 / 𝑛) + 1)))) + π) ∈
ℝ) |
87 | | abslogle 25361 |
. . . . . . . 8
⊢ ((((𝑦 / 𝑛) + 1) ∈ ℂ ∧ ((𝑦 / 𝑛) + 1) ≠ 0) →
(abs‘(log‘((𝑦 /
𝑛) + 1))) ≤
((abs‘(log‘(abs‘((𝑦 / 𝑛) + 1)))) + π)) |
88 | 36, 37, 87 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(log‘((𝑦 / 𝑛) + 1))) ≤
((abs‘(log‘(abs‘((𝑦 / 𝑛) + 1)))) + π)) |
89 | | 1rp 12476 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ+ |
90 | | relogdiv 25336 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ+ ∧ ((𝑅 + 1) · 𝑛) ∈ ℝ+) →
(log‘(1 / ((𝑅 + 1)
· 𝑛))) =
((log‘1) − (log‘((𝑅 + 1) · 𝑛)))) |
91 | 89, 48, 90 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘(1 / ((𝑅 + 1) · 𝑛))) = ((log‘1) −
(log‘((𝑅 + 1)
· 𝑛)))) |
92 | | log1 25329 |
. . . . . . . . . . . . 13
⊢
(log‘1) = 0 |
93 | 92 | oveq1i 7180 |
. . . . . . . . . . . 12
⊢
((log‘1) − (log‘((𝑅 + 1) · 𝑛))) = (0 − (log‘((𝑅 + 1) · 𝑛))) |
94 | | df-neg 10951 |
. . . . . . . . . . . 12
⊢
-(log‘((𝑅 + 1)
· 𝑛)) = (0 −
(log‘((𝑅 + 1)
· 𝑛))) |
95 | 93, 94 | eqtr4i 2764 |
. . . . . . . . . . 11
⊢
((log‘1) − (log‘((𝑅 + 1) · 𝑛))) = -(log‘((𝑅 + 1) · 𝑛)) |
96 | 91, 95 | eqtr2di 2790 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → -(log‘((𝑅 + 1) · 𝑛)) = (log‘(1 / ((𝑅 + 1) · 𝑛)))) |
97 | 46 | nnrecred 11767 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 / (𝑅 + 1)) ∈ ℝ) |
98 | 23, 32 | addcld 10738 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑦 + 𝑛) ∈ ℂ) |
99 | 98 | abscld 14886 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 + 𝑛)) ∈ ℝ) |
100 | 4 | nnrecred 11767 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 / 𝑅) ∈ ℝ) |
101 | 4 | nnrpd 12512 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑅 ∈
ℝ+) |
102 | | 0le1 11241 |
. . . . . . . . . . . . . . . 16
⊢ 0 ≤
1 |
103 | 102 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 0 ≤ 1) |
104 | 44 | lep1d 11649 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑅 ≤ (𝑅 + 1)) |
105 | 101, 47, 61, 103, 104 | lediv2ad 12536 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 / (𝑅 + 1)) ≤ (1 / 𝑅)) |
106 | | oveq2 7178 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑛 → (𝑦 + 𝑘) = (𝑦 + 𝑛)) |
107 | 106 | fveq2d 6678 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → (abs‘(𝑦 + 𝑘)) = (abs‘(𝑦 + 𝑛))) |
108 | 107 | breq2d 5042 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → ((1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑛)))) |
109 | 78 | simprd 499 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘))) |
110 | 24 | nnnn0d 12036 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑛 ∈ ℕ0) |
111 | 108, 109,
110 | rspcdva 3528 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑛))) |
112 | 97, 100, 99, 105, 111 | letrd 10875 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 / (𝑅 + 1)) ≤ (abs‘(𝑦 + 𝑛))) |
113 | 97, 99, 27, 112 | lediv1dd 12572 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((1 / (𝑅 + 1)) / 𝑛) ≤ ((abs‘(𝑦 + 𝑛)) / 𝑛)) |
114 | 46 | nncnd 11732 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 + 1) ∈ ℂ) |
115 | 46 | nnne0d 11766 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 + 1) ≠ 0) |
116 | 114, 32, 115, 33 | recdiv2d 11512 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((1 / (𝑅 + 1)) / 𝑛) = (1 / ((𝑅 + 1) · 𝑛))) |
117 | 23, 32, 32, 33 | divdird 11532 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑦 + 𝑛) / 𝑛) = ((𝑦 / 𝑛) + (𝑛 / 𝑛))) |
118 | 32, 33 | dividd 11492 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑛 / 𝑛) = 1) |
119 | 118 | oveq2d 7186 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑦 / 𝑛) + (𝑛 / 𝑛)) = ((𝑦 / 𝑛) + 1)) |
120 | 117, 119 | eqtr2d 2774 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑦 / 𝑛) + 1) = ((𝑦 + 𝑛) / 𝑛)) |
121 | 120 | fveq2d 6678 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 / 𝑛) + 1)) = (abs‘((𝑦 + 𝑛) / 𝑛))) |
122 | 98, 32, 33 | absdivd 14905 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 + 𝑛) / 𝑛)) = ((abs‘(𝑦 + 𝑛)) / (abs‘𝑛))) |
123 | 27 | rpge0d 12518 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 0 ≤ 𝑛) |
124 | 58, 123 | absidd 14872 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘𝑛) = 𝑛) |
125 | 124 | oveq2d 7186 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘(𝑦 + 𝑛)) / (abs‘𝑛)) = ((abs‘(𝑦 + 𝑛)) / 𝑛)) |
126 | 121, 122,
125 | 3eqtrrd 2778 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘(𝑦 + 𝑛)) / 𝑛) = (abs‘((𝑦 / 𝑛) + 1))) |
127 | 113, 116,
126 | 3brtr3d 5061 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 / ((𝑅 + 1) · 𝑛)) ≤ (abs‘((𝑦 / 𝑛) + 1))) |
128 | 48 | rpreccld 12524 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 / ((𝑅 + 1) · 𝑛)) ∈
ℝ+) |
129 | 128, 82 | logled 25370 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((1 / ((𝑅 + 1) · 𝑛)) ≤ (abs‘((𝑦 / 𝑛) + 1)) ↔ (log‘(1 / ((𝑅 + 1) · 𝑛))) ≤
(log‘(abs‘((𝑦 /
𝑛) +
1))))) |
130 | 127, 129 | mpbid 235 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘(1 / ((𝑅 + 1) · 𝑛))) ≤
(log‘(abs‘((𝑦 /
𝑛) + 1)))) |
131 | 96, 130 | eqbrtrd 5052 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → -(log‘((𝑅 + 1) · 𝑛)) ≤ (log‘(abs‘((𝑦 / 𝑛) + 1)))) |
132 | 36 | abscld 14886 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 / 𝑛) + 1)) ∈ ℝ) |
133 | 44, 61 | readdcld 10748 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 + 1) ∈ ℝ) |
134 | 48 | rpred 12514 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑅 + 1) · 𝑛) ∈ ℝ) |
135 | 34 | abscld 14886 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 / 𝑛)) ∈ ℝ) |
136 | 135, 61 | readdcld 10748 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘(𝑦 / 𝑛)) + 1) ∈ ℝ) |
137 | 34, 35 | abstrid 14906 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 / 𝑛) + 1)) ≤ ((abs‘(𝑦 / 𝑛)) + (abs‘1))) |
138 | | abs1 14747 |
. . . . . . . . . . . . . 14
⊢
(abs‘1) = 1 |
139 | 138 | oveq2i 7181 |
. . . . . . . . . . . . 13
⊢
((abs‘(𝑦 /
𝑛)) + (abs‘1)) =
((abs‘(𝑦 / 𝑛)) + 1) |
140 | 137, 139 | breqtrdi 5071 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 / 𝑛) + 1)) ≤ ((abs‘(𝑦 / 𝑛)) + 1)) |
141 | 89 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 1 ∈
ℝ+) |
142 | 23 | absge0d 14894 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 0 ≤ (abs‘𝑦)) |
143 | 24 | nnge1d 11764 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 1 ≤ 𝑛) |
144 | 69, 44, 141, 58, 142, 79, 143 | lediv12ad 12573 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘𝑦) / 𝑛) ≤ (𝑅 / 1)) |
145 | 23, 32, 33 | absdivd 14905 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 / 𝑛)) = ((abs‘𝑦) / (abs‘𝑛))) |
146 | 124 | oveq2d 7186 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘𝑦) / (abs‘𝑛)) = ((abs‘𝑦) / 𝑛)) |
147 | 145, 146 | eqtr2d 2774 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘𝑦) / 𝑛) = (abs‘(𝑦 / 𝑛))) |
148 | 4 | nncnd 11732 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑅 ∈ ℂ) |
149 | 148 | div1d 11486 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 / 1) = 𝑅) |
150 | 144, 147,
149 | 3brtr3d 5061 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 / 𝑛)) ≤ 𝑅) |
151 | 135, 44, 61, 150 | leadd1dd 11332 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘(𝑦 / 𝑛)) + 1) ≤ (𝑅 + 1)) |
152 | 132, 136,
133, 140, 151 | letrd 10875 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 / 𝑛) + 1)) ≤ (𝑅 + 1)) |
153 | 47 | rpge0d 12518 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 0 ≤ (𝑅 + 1)) |
154 | 133, 58, 153, 143 | lemulge11d 11655 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 + 1) ≤ ((𝑅 + 1) · 𝑛)) |
155 | 132, 133,
134, 152, 154 | letrd 10875 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 / 𝑛) + 1)) ≤ ((𝑅 + 1) · 𝑛)) |
156 | 82, 48 | logled 25370 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘((𝑦 / 𝑛) + 1)) ≤ ((𝑅 + 1) · 𝑛) ↔ (log‘(abs‘((𝑦 / 𝑛) + 1))) ≤ (log‘((𝑅 + 1) · 𝑛)))) |
157 | 155, 156 | mpbid 235 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘(abs‘((𝑦 / 𝑛) + 1))) ≤ (log‘((𝑅 + 1) · 𝑛))) |
158 | 83, 49 | absled 14880 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) →
((abs‘(log‘(abs‘((𝑦 / 𝑛) + 1)))) ≤ (log‘((𝑅 + 1) · 𝑛)) ↔ (-(log‘((𝑅 + 1) · 𝑛)) ≤ (log‘(abs‘((𝑦 / 𝑛) + 1))) ∧ (log‘(abs‘((𝑦 / 𝑛) + 1))) ≤ (log‘((𝑅 + 1) · 𝑛))))) |
159 | 131, 157,
158 | mpbir2and 713 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) →
(abs‘(log‘(abs‘((𝑦 / 𝑛) + 1)))) ≤ (log‘((𝑅 + 1) · 𝑛))) |
160 | 85, 49, 51, 159 | leadd1dd 11332 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) →
((abs‘(log‘(abs‘((𝑦 / 𝑛) + 1)))) + π) ≤ ((log‘((𝑅 + 1) · 𝑛)) + π)) |
161 | 42, 86, 52, 88, 160 | letrd 10875 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(log‘((𝑦 / 𝑛) + 1))) ≤ ((log‘((𝑅 + 1) · 𝑛)) + π)) |
162 | 41, 42, 45, 52, 81, 161 | le2addd 11337 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘(𝑦 · (log‘((𝑛 + 1) / 𝑛)))) + (abs‘(log‘((𝑦 / 𝑛) + 1)))) ≤ ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) |
163 | 40, 43, 53, 54, 162 | letrd 10875 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) |
164 | 163 | adantr 484 |
. . 3
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) ∧ ¬ (2 · 𝑅) ≤ 𝑛) → (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) |
165 | 1, 2, 19, 164 | ifbothda 4452 |
. 2
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)))) |
166 | | oveq1 7177 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1)) |
167 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → 𝑚 = 𝑛) |
168 | 166, 167 | oveq12d 7188 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → ((𝑚 + 1) / 𝑚) = ((𝑛 + 1) / 𝑛)) |
169 | 168 | fveq2d 6678 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (log‘((𝑚 + 1) / 𝑚)) = (log‘((𝑛 + 1) / 𝑛))) |
170 | 169 | oveq2d 7186 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (𝑧 · (log‘((𝑚 + 1) / 𝑚))) = (𝑧 · (log‘((𝑛 + 1) / 𝑛)))) |
171 | | oveq2 7178 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (𝑧 / 𝑚) = (𝑧 / 𝑛)) |
172 | 171 | fvoveq1d 7192 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (log‘((𝑧 / 𝑚) + 1)) = (log‘((𝑧 / 𝑛) + 1))) |
173 | 170, 172 | oveq12d 7188 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) = ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1)))) |
174 | 173 | mpteq2dv 5126 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))) = (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))))) |
175 | | lgamgulm.g |
. . . . . . 7
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) |
176 | | cnex 10696 |
. . . . . . . . 9
⊢ ℂ
∈ V |
177 | 6, 176 | rabex2 5202 |
. . . . . . . 8
⊢ 𝑈 ∈ V |
178 | 177 | mptex 6996 |
. . . . . . 7
⊢ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1)))) ∈ V |
179 | 174, 175,
178 | fvmpt 6775 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → (𝐺‘𝑛) = (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))))) |
180 | 179 | ad2antrl 728 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝐺‘𝑛) = (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))))) |
181 | 180 | fveq1d 6676 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝐺‘𝑛)‘𝑦) = ((𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))))‘𝑦)) |
182 | | oveq1 7177 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → (𝑧 · (log‘((𝑛 + 1) / 𝑛))) = (𝑦 · (log‘((𝑛 + 1) / 𝑛)))) |
183 | | oveq1 7177 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → (𝑧 / 𝑛) = (𝑦 / 𝑛)) |
184 | 183 | fvoveq1d 7192 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → (log‘((𝑧 / 𝑛) + 1)) = (log‘((𝑦 / 𝑛) + 1))) |
185 | 182, 184 | oveq12d 7188 |
. . . . . 6
⊢ (𝑧 = 𝑦 → ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) = ((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) |
186 | | eqid 2738 |
. . . . . 6
⊢ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1)))) = (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1)))) |
187 | | ovex 7203 |
. . . . . 6
⊢ ((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1))) ∈ V |
188 | 185, 186,
187 | fvmpt 6775 |
. . . . 5
⊢ (𝑦 ∈ 𝑈 → ((𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))))‘𝑦) = ((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) |
189 | 188 | ad2antll 729 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))))‘𝑦) = ((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) |
190 | 181, 189 | eqtrd 2773 |
. . 3
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝐺‘𝑛)‘𝑦) = ((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) |
191 | 190 | fveq2d 6678 |
. 2
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝐺‘𝑛)‘𝑦)) = (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1))))) |
192 | | breq2 5034 |
. . . . 5
⊢ (𝑚 = 𝑛 → ((2 · 𝑅) ≤ 𝑚 ↔ (2 · 𝑅) ≤ 𝑛)) |
193 | | oveq1 7177 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (𝑚↑2) = (𝑛↑2)) |
194 | 193 | oveq2d 7186 |
. . . . . 6
⊢ (𝑚 = 𝑛 → ((2 · (𝑅 + 1)) / (𝑚↑2)) = ((2 · (𝑅 + 1)) / (𝑛↑2))) |
195 | 194 | oveq2d 7186 |
. . . . 5
⊢ (𝑚 = 𝑛 → (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))) = (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2)))) |
196 | 169 | oveq2d 7186 |
. . . . . 6
⊢ (𝑚 = 𝑛 → (𝑅 · (log‘((𝑚 + 1) / 𝑚))) = (𝑅 · (log‘((𝑛 + 1) / 𝑛)))) |
197 | | oveq2 7178 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → ((𝑅 + 1) · 𝑚) = ((𝑅 + 1) · 𝑛)) |
198 | 197 | fveq2d 6678 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (log‘((𝑅 + 1) · 𝑚)) = (log‘((𝑅 + 1) · 𝑛))) |
199 | 198 | oveq1d 7185 |
. . . . . 6
⊢ (𝑚 = 𝑛 → ((log‘((𝑅 + 1) · 𝑚)) + π) = ((log‘((𝑅 + 1) · 𝑛)) + π)) |
200 | 196, 199 | oveq12d 7188 |
. . . . 5
⊢ (𝑚 = 𝑛 → ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π)) = ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) |
201 | 192, 195,
200 | ifbieq12d 4442 |
. . . 4
⊢ (𝑚 = 𝑛 → if((2 · 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π))) = if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)))) |
202 | | lgamgulm.t |
. . . 4
⊢ 𝑇 = (𝑚 ∈ ℕ ↦ if((2 · 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π)))) |
203 | | ovex 7203 |
. . . . 5
⊢ (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))) ∈ V |
204 | | ovex 7203 |
. . . . 5
⊢ ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)) ∈ V |
205 | 203, 204 | ifex 4464 |
. . . 4
⊢ if((2
· 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) ∈ V |
206 | 201, 202,
205 | fvmpt 6775 |
. . 3
⊢ (𝑛 ∈ ℕ → (𝑇‘𝑛) = if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)))) |
207 | 206 | ad2antrl 728 |
. 2
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑇‘𝑛) = if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)))) |
208 | 165, 191,
207 | 3brtr4d 5062 |
1
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝐺‘𝑛)‘𝑦)) ≤ (𝑇‘𝑛)) |