Step | Hyp | Ref
| Expression |
1 | | breq2 4657 |
. . 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 4657 |
. . 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 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑅 ∈ ℕ) |
5 | 4 | adantr 481 |
. . . 4
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) ∧ (2 · 𝑅) ≤ 𝑛) → 𝑅 ∈ ℕ) |
6 | | lgamgulm.u |
. . . . 5
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))} |
7 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = 𝑡 → (abs‘𝑥) = (abs‘𝑡)) |
8 | 7 | breq1d 4663 |
. . . . . . 7
⊢ (𝑥 = 𝑡 → ((abs‘𝑥) ≤ 𝑅 ↔ (abs‘𝑡) ≤ 𝑅)) |
9 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑡 → (𝑥 + 𝑘) = (𝑡 + 𝑘)) |
10 | 9 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑥 = 𝑡 → (abs‘(𝑥 + 𝑘)) = (abs‘(𝑡 + 𝑘))) |
11 | 10 | breq2d 4665 |
. . . . . . . 8
⊢ (𝑥 = 𝑡 → ((1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝑡 + 𝑘)))) |
12 | 11 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑥 = 𝑡 → (∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑡 + 𝑘)))) |
13 | 8, 12 | anbi12d 747 |
. . . . . 6
⊢ (𝑥 = 𝑡 → (((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘))) ↔ ((abs‘𝑡) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑡 + 𝑘))))) |
14 | 13 | cbvrabv 3199 |
. . . . 5
⊢ {𝑥 ∈ ℂ ∣
((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 /
𝑅) ≤ (abs‘(𝑥 + 𝑘)))} = {𝑡 ∈ ℂ ∣ ((abs‘𝑡) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑡 + 𝑘)))} |
15 | 6, 14 | eqtri 2644 |
. . . 4
⊢ 𝑈 = {𝑡 ∈ ℂ ∣ ((abs‘𝑡) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑡 + 𝑘)))} |
16 | | simplrl 800 |
. . . 4
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) ∧ (2 · 𝑅) ≤ 𝑛) → 𝑛 ∈ ℕ) |
17 | | simprr 796 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈) |
18 | 17 | adantr 481 |
. . . 4
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) ∧ (2 · 𝑅) ≤ 𝑛) → 𝑦 ∈ 𝑈) |
19 | | simpr 477 |
. . . 4
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) ∧ (2 · 𝑅) ≤ 𝑛) → (2 · 𝑅) ≤ 𝑛) |
20 | 5, 15, 16, 18, 19 | lgamgulmlem3 24757 |
. . 3
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) ∧ (2 · 𝑅) ≤ 𝑛) → (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2)))) |
21 | 3, 6 | lgamgulmlem1 24755 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ⊆ (ℂ ∖ (ℤ ∖
ℕ))) |
22 | 21 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑈 ⊆ (ℂ ∖ (ℤ ∖
ℕ))) |
23 | 22, 17 | sseldd 3604 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
24 | 23 | eldifad 3586 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ ℂ) |
25 | | simprl 794 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑛 ∈ ℕ) |
26 | 25 | peano2nnd 11037 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑛 + 1) ∈ ℕ) |
27 | 26 | nnrpd 11870 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑛 + 1) ∈
ℝ+) |
28 | 25 | nnrpd 11870 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑛 ∈ ℝ+) |
29 | 27, 28 | rpdivcld 11889 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑛 + 1) / 𝑛) ∈
ℝ+) |
30 | 29 | relogcld 24369 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘((𝑛 + 1) / 𝑛)) ∈ ℝ) |
31 | 30 | recnd 10068 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘((𝑛 + 1) / 𝑛)) ∈ ℂ) |
32 | 24, 31 | mulcld 10060 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑦 · (log‘((𝑛 + 1) / 𝑛))) ∈ ℂ) |
33 | 25 | nncnd 11036 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑛 ∈ ℂ) |
34 | 25 | nnne0d 11065 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑛 ≠ 0) |
35 | 24, 33, 34 | divcld 10801 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑦 / 𝑛) ∈ ℂ) |
36 | | 1cnd 10056 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 1 ∈ ℂ) |
37 | 35, 36 | addcld 10059 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑦 / 𝑛) + 1) ∈ ℂ) |
38 | 23, 25 | dmgmdivn0 24754 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑦 / 𝑛) + 1) ≠ 0) |
39 | 37, 38 | logcld 24317 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘((𝑦 / 𝑛) + 1)) ∈ ℂ) |
40 | 32, 39 | subcld 10392 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1))) ∈ ℂ) |
41 | 40 | abscld 14175 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ∈ ℝ) |
42 | 32 | abscld 14175 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 · (log‘((𝑛 + 1) / 𝑛)))) ∈ ℝ) |
43 | 39 | abscld 14175 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(log‘((𝑦 / 𝑛) + 1))) ∈ ℝ) |
44 | 42, 43 | readdcld 10069 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘(𝑦 · (log‘((𝑛 + 1) / 𝑛)))) + (abs‘(log‘((𝑦 / 𝑛) + 1)))) ∈ ℝ) |
45 | 4 | nnred 11035 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑅 ∈ ℝ) |
46 | 45, 30 | remulcld 10070 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 · (log‘((𝑛 + 1) / 𝑛))) ∈ ℝ) |
47 | 4 | peano2nnd 11037 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 + 1) ∈ ℕ) |
48 | 47 | nnrpd 11870 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 + 1) ∈
ℝ+) |
49 | 48, 28 | rpmulcld 11888 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑅 + 1) · 𝑛) ∈
ℝ+) |
50 | 49 | relogcld 24369 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘((𝑅 + 1) · 𝑛)) ∈ ℝ) |
51 | | pire 24210 |
. . . . . . . 8
⊢ π
∈ ℝ |
52 | 51 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → π ∈
ℝ) |
53 | 50, 52 | readdcld 10069 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((log‘((𝑅 + 1) · 𝑛)) + π) ∈ ℝ) |
54 | 46, 53 | readdcld 10069 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)) ∈ ℝ) |
55 | 32, 39 | abs2dif2d 14197 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ ((abs‘(𝑦 · (log‘((𝑛 + 1) / 𝑛)))) + (abs‘(log‘((𝑦 / 𝑛) + 1))))) |
56 | 24, 31 | absmuld 14193 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 · (log‘((𝑛 + 1) / 𝑛)))) = ((abs‘𝑦) · (abs‘(log‘((𝑛 + 1) / 𝑛))))) |
57 | 29 | rpred 11872 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑛 + 1) / 𝑛) ∈ ℝ) |
58 | 33 | mulid2d 10058 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 · 𝑛) = 𝑛) |
59 | 25 | nnred 11035 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑛 ∈ ℝ) |
60 | 59 | lep1d 10955 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑛 ≤ (𝑛 + 1)) |
61 | 58, 60 | eqbrtrd 4675 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 · 𝑛) ≤ (𝑛 + 1)) |
62 | | 1red 10055 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 1 ∈ ℝ) |
63 | 59, 62 | readdcld 10069 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑛 + 1) ∈ ℝ) |
64 | 62, 63, 28 | lemuldivd 11921 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((1 · 𝑛) ≤ (𝑛 + 1) ↔ 1 ≤ ((𝑛 + 1) / 𝑛))) |
65 | 61, 64 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 1 ≤ ((𝑛 + 1) / 𝑛)) |
66 | 57, 65 | logge0d 24376 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 0 ≤ (log‘((𝑛 + 1) / 𝑛))) |
67 | 30, 66 | absidd 14161 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(log‘((𝑛 + 1) / 𝑛))) = (log‘((𝑛 + 1) / 𝑛))) |
68 | 67 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘𝑦) · (abs‘(log‘((𝑛 + 1) / 𝑛)))) = ((abs‘𝑦) · (log‘((𝑛 + 1) / 𝑛)))) |
69 | 56, 68 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 · (log‘((𝑛 + 1) / 𝑛)))) = ((abs‘𝑦) · (log‘((𝑛 + 1) / 𝑛)))) |
70 | 24 | abscld 14175 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘𝑦) ∈ ℝ) |
71 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (abs‘𝑥) = (abs‘𝑦)) |
72 | 71 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ((abs‘𝑥) ≤ 𝑅 ↔ (abs‘𝑦) ≤ 𝑅)) |
73 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝑥 + 𝑘) = (𝑦 + 𝑘)) |
74 | 73 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (abs‘(𝑥 + 𝑘)) = (abs‘(𝑦 + 𝑘))) |
75 | 74 | breq2d 4665 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘)))) |
76 | 75 | ralbidv 2986 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘)))) |
77 | 72, 76 | anbi12d 747 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘))) ↔ ((abs‘𝑦) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘))))) |
78 | 77, 6 | elrab2 3366 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑈 ↔ (𝑦 ∈ ℂ ∧ ((abs‘𝑦) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘))))) |
79 | 78 | simprbi 480 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑈 → ((abs‘𝑦) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘)))) |
80 | 79 | ad2antll 765 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘𝑦) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘)))) |
81 | 80 | simpld 475 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘𝑦) ≤ 𝑅) |
82 | 70, 45, 30, 66, 81 | lemul1ad 10963 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘𝑦) · (log‘((𝑛 + 1) / 𝑛))) ≤ (𝑅 · (log‘((𝑛 + 1) / 𝑛)))) |
83 | 69, 82 | eqbrtrd 4675 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 · (log‘((𝑛 + 1) / 𝑛)))) ≤ (𝑅 · (log‘((𝑛 + 1) / 𝑛)))) |
84 | 37, 38 | absrpcld 14187 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 / 𝑛) + 1)) ∈
ℝ+) |
85 | 84 | relogcld 24369 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘(abs‘((𝑦 / 𝑛) + 1))) ∈ ℝ) |
86 | 85 | recnd 10068 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘(abs‘((𝑦 / 𝑛) + 1))) ∈ ℂ) |
87 | 86 | abscld 14175 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) →
(abs‘(log‘(abs‘((𝑦 / 𝑛) + 1)))) ∈ ℝ) |
88 | 87, 52 | readdcld 10069 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) →
((abs‘(log‘(abs‘((𝑦 / 𝑛) + 1)))) + π) ∈
ℝ) |
89 | | abslogle 24364 |
. . . . . . . 8
⊢ ((((𝑦 / 𝑛) + 1) ∈ ℂ ∧ ((𝑦 / 𝑛) + 1) ≠ 0) →
(abs‘(log‘((𝑦 /
𝑛) + 1))) ≤
((abs‘(log‘(abs‘((𝑦 / 𝑛) + 1)))) + π)) |
90 | 37, 38, 89 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(log‘((𝑦 / 𝑛) + 1))) ≤
((abs‘(log‘(abs‘((𝑦 / 𝑛) + 1)))) + π)) |
91 | | 1rp 11836 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ+ |
92 | | relogdiv 24339 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ+ ∧ ((𝑅 + 1) · 𝑛) ∈ ℝ+) →
(log‘(1 / ((𝑅 + 1)
· 𝑛))) =
((log‘1) − (log‘((𝑅 + 1) · 𝑛)))) |
93 | 91, 49, 92 | sylancr 695 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘(1 / ((𝑅 + 1) · 𝑛))) = ((log‘1) −
(log‘((𝑅 + 1)
· 𝑛)))) |
94 | | log1 24332 |
. . . . . . . . . . . . 13
⊢
(log‘1) = 0 |
95 | 94 | oveq1i 6660 |
. . . . . . . . . . . 12
⊢
((log‘1) − (log‘((𝑅 + 1) · 𝑛))) = (0 − (log‘((𝑅 + 1) · 𝑛))) |
96 | | df-neg 10269 |
. . . . . . . . . . . 12
⊢
-(log‘((𝑅 + 1)
· 𝑛)) = (0 −
(log‘((𝑅 + 1)
· 𝑛))) |
97 | 95, 96 | eqtr4i 2647 |
. . . . . . . . . . 11
⊢
((log‘1) − (log‘((𝑅 + 1) · 𝑛))) = -(log‘((𝑅 + 1) · 𝑛)) |
98 | 93, 97 | syl6req 2673 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → -(log‘((𝑅 + 1) · 𝑛)) = (log‘(1 / ((𝑅 + 1) · 𝑛)))) |
99 | 47 | nnrecred 11066 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 / (𝑅 + 1)) ∈ ℝ) |
100 | 24, 33 | addcld 10059 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑦 + 𝑛) ∈ ℂ) |
101 | 100 | abscld 14175 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 + 𝑛)) ∈ ℝ) |
102 | 4 | nnrecred 11066 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 / 𝑅) ∈ ℝ) |
103 | 4 | nnrpd 11870 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑅 ∈
ℝ+) |
104 | | 0le1 10551 |
. . . . . . . . . . . . . . . 16
⊢ 0 ≤
1 |
105 | 104 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 0 ≤ 1) |
106 | 45 | lep1d 10955 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑅 ≤ (𝑅 + 1)) |
107 | 103, 48, 62, 105, 106 | lediv2ad 11894 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 / (𝑅 + 1)) ≤ (1 / 𝑅)) |
108 | 25 | nnnn0d 11351 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑛 ∈ ℕ0) |
109 | 80 | simprd 479 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘))) |
110 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑛 → (𝑦 + 𝑘) = (𝑦 + 𝑛)) |
111 | 110 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑛 → (abs‘(𝑦 + 𝑘)) = (abs‘(𝑦 + 𝑛))) |
112 | 111 | breq2d 4665 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → ((1 / 𝑅) ≤ (abs‘(𝑦 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑛)))) |
113 | 112 | rspcv 3305 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ0
→ (∀𝑘 ∈
ℕ0 (1 / 𝑅)
≤ (abs‘(𝑦 + 𝑘)) → (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑛)))) |
114 | 108, 109,
113 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 / 𝑅) ≤ (abs‘(𝑦 + 𝑛))) |
115 | 99, 102, 101, 107, 114 | letrd 10194 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 / (𝑅 + 1)) ≤ (abs‘(𝑦 + 𝑛))) |
116 | 99, 101, 28, 115 | lediv1dd 11930 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((1 / (𝑅 + 1)) / 𝑛) ≤ ((abs‘(𝑦 + 𝑛)) / 𝑛)) |
117 | 47 | nncnd 11036 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 + 1) ∈ ℂ) |
118 | 47 | nnne0d 11065 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 + 1) ≠ 0) |
119 | 117, 33, 118, 34 | recdiv2d 10819 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((1 / (𝑅 + 1)) / 𝑛) = (1 / ((𝑅 + 1) · 𝑛))) |
120 | 24, 33, 33, 34 | divdird 10839 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑦 + 𝑛) / 𝑛) = ((𝑦 / 𝑛) + (𝑛 / 𝑛))) |
121 | 33, 34 | dividd 10799 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑛 / 𝑛) = 1) |
122 | 121 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑦 / 𝑛) + (𝑛 / 𝑛)) = ((𝑦 / 𝑛) + 1)) |
123 | 120, 122 | eqtr2d 2657 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑦 / 𝑛) + 1) = ((𝑦 + 𝑛) / 𝑛)) |
124 | 123 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 / 𝑛) + 1)) = (abs‘((𝑦 + 𝑛) / 𝑛))) |
125 | 100, 33, 34 | absdivd 14194 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 + 𝑛) / 𝑛)) = ((abs‘(𝑦 + 𝑛)) / (abs‘𝑛))) |
126 | 28 | rpge0d 11876 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 0 ≤ 𝑛) |
127 | 59, 126 | absidd 14161 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘𝑛) = 𝑛) |
128 | 127 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘(𝑦 + 𝑛)) / (abs‘𝑛)) = ((abs‘(𝑦 + 𝑛)) / 𝑛)) |
129 | 124, 125,
128 | 3eqtrrd 2661 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘(𝑦 + 𝑛)) / 𝑛) = (abs‘((𝑦 / 𝑛) + 1))) |
130 | 116, 119,
129 | 3brtr3d 4684 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 / ((𝑅 + 1) · 𝑛)) ≤ (abs‘((𝑦 / 𝑛) + 1))) |
131 | 49 | rpreccld 11882 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (1 / ((𝑅 + 1) · 𝑛)) ∈
ℝ+) |
132 | 131, 84 | logled 24373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((1 / ((𝑅 + 1) · 𝑛)) ≤ (abs‘((𝑦 / 𝑛) + 1)) ↔ (log‘(1 / ((𝑅 + 1) · 𝑛))) ≤
(log‘(abs‘((𝑦 /
𝑛) +
1))))) |
133 | 130, 132 | mpbid 222 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘(1 / ((𝑅 + 1) · 𝑛))) ≤
(log‘(abs‘((𝑦 /
𝑛) + 1)))) |
134 | 98, 133 | eqbrtrd 4675 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → -(log‘((𝑅 + 1) · 𝑛)) ≤ (log‘(abs‘((𝑦 / 𝑛) + 1)))) |
135 | 37 | abscld 14175 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 / 𝑛) + 1)) ∈ ℝ) |
136 | 45, 62 | readdcld 10069 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 + 1) ∈ ℝ) |
137 | 49 | rpred 11872 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑅 + 1) · 𝑛) ∈ ℝ) |
138 | 35 | abscld 14175 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 / 𝑛)) ∈ ℝ) |
139 | 138, 62 | readdcld 10069 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘(𝑦 / 𝑛)) + 1) ∈ ℝ) |
140 | 35, 36 | abstrid 14195 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 / 𝑛) + 1)) ≤ ((abs‘(𝑦 / 𝑛)) + (abs‘1))) |
141 | | abs1 14037 |
. . . . . . . . . . . . . 14
⊢
(abs‘1) = 1 |
142 | 141 | oveq2i 6661 |
. . . . . . . . . . . . 13
⊢
((abs‘(𝑦 /
𝑛)) + (abs‘1)) =
((abs‘(𝑦 / 𝑛)) + 1) |
143 | 140, 142 | syl6breq 4694 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 / 𝑛) + 1)) ≤ ((abs‘(𝑦 / 𝑛)) + 1)) |
144 | 91 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 1 ∈
ℝ+) |
145 | 24 | absge0d 14183 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 0 ≤ (abs‘𝑦)) |
146 | 25 | nnge1d 11063 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 1 ≤ 𝑛) |
147 | 70, 45, 144, 59, 145, 81, 146 | lediv12ad 11931 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘𝑦) / 𝑛) ≤ (𝑅 / 1)) |
148 | 24, 33, 34 | absdivd 14194 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 / 𝑛)) = ((abs‘𝑦) / (abs‘𝑛))) |
149 | 127 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘𝑦) / (abs‘𝑛)) = ((abs‘𝑦) / 𝑛)) |
150 | 148, 149 | eqtr2d 2657 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘𝑦) / 𝑛) = (abs‘(𝑦 / 𝑛))) |
151 | 4 | nncnd 11036 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 𝑅 ∈ ℂ) |
152 | 151 | div1d 10793 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 / 1) = 𝑅) |
153 | 147, 150,
152 | 3brtr3d 4684 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(𝑦 / 𝑛)) ≤ 𝑅) |
154 | 138, 45, 62, 153 | leadd1dd 10641 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘(𝑦 / 𝑛)) + 1) ≤ (𝑅 + 1)) |
155 | 135, 139,
136, 143, 154 | letrd 10194 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 / 𝑛) + 1)) ≤ (𝑅 + 1)) |
156 | 48 | rpge0d 11876 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → 0 ≤ (𝑅 + 1)) |
157 | 136, 59, 156, 146 | lemulge11d 10961 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑅 + 1) ≤ ((𝑅 + 1) · 𝑛)) |
158 | 135, 136,
137, 155, 157 | letrd 10194 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 / 𝑛) + 1)) ≤ ((𝑅 + 1) · 𝑛)) |
159 | 84, 49 | logled 24373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘((𝑦 / 𝑛) + 1)) ≤ ((𝑅 + 1) · 𝑛) ↔ (log‘(abs‘((𝑦 / 𝑛) + 1))) ≤ (log‘((𝑅 + 1) · 𝑛)))) |
160 | 158, 159 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (log‘(abs‘((𝑦 / 𝑛) + 1))) ≤ (log‘((𝑅 + 1) · 𝑛))) |
161 | 85, 50 | absled 14169 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) →
((abs‘(log‘(abs‘((𝑦 / 𝑛) + 1)))) ≤ (log‘((𝑅 + 1) · 𝑛)) ↔ (-(log‘((𝑅 + 1) · 𝑛)) ≤ (log‘(abs‘((𝑦 / 𝑛) + 1))) ∧ (log‘(abs‘((𝑦 / 𝑛) + 1))) ≤ (log‘((𝑅 + 1) · 𝑛))))) |
162 | 134, 160,
161 | mpbir2and 957 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) →
(abs‘(log‘(abs‘((𝑦 / 𝑛) + 1)))) ≤ (log‘((𝑅 + 1) · 𝑛))) |
163 | 87, 50, 52, 162 | leadd1dd 10641 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) →
((abs‘(log‘(abs‘((𝑦 / 𝑛) + 1)))) + π) ≤ ((log‘((𝑅 + 1) · 𝑛)) + π)) |
164 | 43, 88, 53, 90, 163 | letrd 10194 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘(log‘((𝑦 / 𝑛) + 1))) ≤ ((log‘((𝑅 + 1) · 𝑛)) + π)) |
165 | 42, 43, 46, 53, 83, 164 | le2addd 10646 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((abs‘(𝑦 · (log‘((𝑛 + 1) / 𝑛)))) + (abs‘(log‘((𝑦 / 𝑛) + 1)))) ≤ ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) |
166 | 41, 44, 54, 55, 165 | letrd 10194 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) |
167 | 166 | adantr 481 |
. . 3
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) ∧ ¬ (2 · 𝑅) ≤ 𝑛) → (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) |
168 | 1, 2, 20, 167 | ifbothda 4123 |
. 2
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) ≤ if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)))) |
169 | | oveq1 6657 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1)) |
170 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → 𝑚 = 𝑛) |
171 | 169, 170 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → ((𝑚 + 1) / 𝑚) = ((𝑛 + 1) / 𝑛)) |
172 | 171 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (log‘((𝑚 + 1) / 𝑚)) = (log‘((𝑛 + 1) / 𝑛))) |
173 | 172 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (𝑧 · (log‘((𝑚 + 1) / 𝑚))) = (𝑧 · (log‘((𝑛 + 1) / 𝑛)))) |
174 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (𝑧 / 𝑚) = (𝑧 / 𝑛)) |
175 | 174 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((𝑧 / 𝑚) + 1) = ((𝑧 / 𝑛) + 1)) |
176 | 175 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (log‘((𝑧 / 𝑚) + 1)) = (log‘((𝑧 / 𝑛) + 1))) |
177 | 173, 176 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) = ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1)))) |
178 | 177 | mpteq2dv 4745 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))) = (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))))) |
179 | | lgamgulm.g |
. . . . . . 7
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) |
180 | | cnex 10017 |
. . . . . . . . 9
⊢ ℂ
∈ V |
181 | 6, 180 | rabex2 4815 |
. . . . . . . 8
⊢ 𝑈 ∈ V |
182 | 181 | mptex 6486 |
. . . . . . 7
⊢ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1)))) ∈ V |
183 | 178, 179,
182 | fvmpt 6282 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → (𝐺‘𝑛) = (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))))) |
184 | 183 | ad2antrl 764 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝐺‘𝑛) = (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))))) |
185 | 184 | fveq1d 6193 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝐺‘𝑛)‘𝑦) = ((𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))))‘𝑦)) |
186 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → (𝑧 · (log‘((𝑛 + 1) / 𝑛))) = (𝑦 · (log‘((𝑛 + 1) / 𝑛)))) |
187 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → (𝑧 / 𝑛) = (𝑦 / 𝑛)) |
188 | 187 | oveq1d 6665 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → ((𝑧 / 𝑛) + 1) = ((𝑦 / 𝑛) + 1)) |
189 | 188 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → (log‘((𝑧 / 𝑛) + 1)) = (log‘((𝑦 / 𝑛) + 1))) |
190 | 186, 189 | oveq12d 6668 |
. . . . . 6
⊢ (𝑧 = 𝑦 → ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))) = ((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) |
191 | | eqid 2622 |
. . . . . 6
⊢ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1)))) = (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1)))) |
192 | | ovex 6678 |
. . . . . 6
⊢ ((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1))) ∈ V |
193 | 190, 191,
192 | fvmpt 6282 |
. . . . 5
⊢ (𝑦 ∈ 𝑈 → ((𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))))‘𝑦) = ((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) |
194 | 193 | ad2antll 765 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑧 / 𝑛) + 1))))‘𝑦) = ((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) |
195 | 185, 194 | eqtrd 2656 |
. . 3
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → ((𝐺‘𝑛)‘𝑦) = ((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1)))) |
196 | 195 | fveq2d 6195 |
. 2
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝐺‘𝑛)‘𝑦)) = (abs‘((𝑦 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝑦 / 𝑛) + 1))))) |
197 | | breq2 4657 |
. . . . 5
⊢ (𝑚 = 𝑛 → ((2 · 𝑅) ≤ 𝑚 ↔ (2 · 𝑅) ≤ 𝑛)) |
198 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (𝑚↑2) = (𝑛↑2)) |
199 | 198 | oveq2d 6666 |
. . . . . 6
⊢ (𝑚 = 𝑛 → ((2 · (𝑅 + 1)) / (𝑚↑2)) = ((2 · (𝑅 + 1)) / (𝑛↑2))) |
200 | 199 | oveq2d 6666 |
. . . . 5
⊢ (𝑚 = 𝑛 → (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))) = (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2)))) |
201 | 172 | oveq2d 6666 |
. . . . . 6
⊢ (𝑚 = 𝑛 → (𝑅 · (log‘((𝑚 + 1) / 𝑚))) = (𝑅 · (log‘((𝑛 + 1) / 𝑛)))) |
202 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → ((𝑅 + 1) · 𝑚) = ((𝑅 + 1) · 𝑛)) |
203 | 202 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (log‘((𝑅 + 1) · 𝑚)) = (log‘((𝑅 + 1) · 𝑛))) |
204 | 203 | oveq1d 6665 |
. . . . . 6
⊢ (𝑚 = 𝑛 → ((log‘((𝑅 + 1) · 𝑚)) + π) = ((log‘((𝑅 + 1) · 𝑛)) + π)) |
205 | 201, 204 | oveq12d 6668 |
. . . . 5
⊢ (𝑚 = 𝑛 → ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π)) = ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) |
206 | 197, 200,
205 | ifbieq12d 4113 |
. . . 4
⊢ (𝑚 = 𝑛 → if((2 · 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π))) = if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)))) |
207 | | lgamgulm.t |
. . . 4
⊢ 𝑇 = (𝑚 ∈ ℕ ↦ if((2 · 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π)))) |
208 | | ovex 6678 |
. . . . 5
⊢ (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))) ∈ V |
209 | | ovex 6678 |
. . . . 5
⊢ ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)) ∈ V |
210 | 208, 209 | ifex 4156 |
. . . 4
⊢ if((2
· 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) ∈ V |
211 | 206, 207,
210 | fvmpt 6282 |
. . 3
⊢ (𝑛 ∈ ℕ → (𝑇‘𝑛) = if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)))) |
212 | 211 | ad2antrl 764 |
. 2
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (𝑇‘𝑛) = if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)))) |
213 | 168, 196,
212 | 3brtr4d 4685 |
1
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝐺‘𝑛)‘𝑦)) ≤ (𝑇‘𝑛)) |