Step | Hyp | Ref
| Expression |
1 | | fzfid 13546 |
. . 3
⊢ (𝐴 ∈ ℕ →
(2...𝐴) ∈
Fin) |
2 | | elfzuz 13108 |
. . . . . . . 8
⊢ (𝑛 ∈ (2...𝐴) → 𝑛 ∈
(ℤ≥‘2)) |
3 | | eluz2nn 12480 |
. . . . . . . 8
⊢ (𝑛 ∈
(ℤ≥‘2) → 𝑛 ∈ ℕ) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ (𝑛 ∈ (2...𝐴) → 𝑛 ∈ ℕ) |
5 | 4 | adantl 485 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 𝑛 ∈ ℕ) |
6 | 5 | nnrpd 12626 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 𝑛 ∈ ℝ+) |
7 | 6 | relogcld 25511 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (log‘𝑛) ∈ ℝ) |
8 | 2 | adantl 485 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 𝑛 ∈
(ℤ≥‘2)) |
9 | | uz2m1nn 12519 |
. . . . . 6
⊢ (𝑛 ∈
(ℤ≥‘2) → (𝑛 − 1) ∈ ℕ) |
10 | 8, 9 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (𝑛 − 1) ∈ ℕ) |
11 | 5, 10 | nnmulcld 11883 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (𝑛 · (𝑛 − 1)) ∈ ℕ) |
12 | 7, 11 | nndivred 11884 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((log‘𝑛) / (𝑛 · (𝑛 − 1))) ∈
ℝ) |
13 | 1, 12 | fsumrecl 15298 |
. 2
⊢ (𝐴 ∈ ℕ →
Σ𝑛 ∈ (2...𝐴)((log‘𝑛) / (𝑛 · (𝑛 − 1))) ∈
ℝ) |
14 | | 2re 11904 |
. . . . 5
⊢ 2 ∈
ℝ |
15 | 10 | nnrpd 12626 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (𝑛 − 1) ∈
ℝ+) |
16 | 15 | rpsqrtcld 14975 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (√‘(𝑛 − 1)) ∈
ℝ+) |
17 | | rerpdivcl 12616 |
. . . . 5
⊢ ((2
∈ ℝ ∧ (√‘(𝑛 − 1)) ∈ ℝ+)
→ (2 / (√‘(𝑛 − 1))) ∈
ℝ) |
18 | 14, 16, 17 | sylancr 590 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (2 / (√‘(𝑛 − 1))) ∈
ℝ) |
19 | 6 | rpsqrtcld 14975 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (√‘𝑛) ∈
ℝ+) |
20 | | rerpdivcl 12616 |
. . . . 5
⊢ ((2
∈ ℝ ∧ (√‘𝑛) ∈ ℝ+) → (2 /
(√‘𝑛)) ∈
ℝ) |
21 | 14, 19, 20 | sylancr 590 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (2 / (√‘𝑛)) ∈
ℝ) |
22 | 18, 21 | resubcld 11260 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((2 / (√‘(𝑛 − 1))) − (2 /
(√‘𝑛))) ∈
ℝ) |
23 | 1, 22 | fsumrecl 15298 |
. 2
⊢ (𝐴 ∈ ℕ →
Σ𝑛 ∈ (2...𝐴)((2 / (√‘(𝑛 − 1))) − (2 /
(√‘𝑛))) ∈
ℝ) |
24 | 14 | a1i 11 |
. 2
⊢ (𝐴 ∈ ℕ → 2 ∈
ℝ) |
25 | 16 | rpred 12628 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (√‘(𝑛 − 1)) ∈ ℝ) |
26 | 5 | nnred 11845 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 𝑛 ∈ ℝ) |
27 | | peano2rem 11145 |
. . . . . . . 8
⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈
ℝ) |
28 | 26, 27 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (𝑛 − 1) ∈ ℝ) |
29 | 26, 28 | remulcld 10863 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (𝑛 · (𝑛 − 1)) ∈ ℝ) |
30 | 29, 22 | remulcld 10863 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((𝑛 · (𝑛 − 1)) · ((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛)))) ∈ ℝ) |
31 | 5 | nncnd 11846 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 𝑛 ∈ ℂ) |
32 | | ax-1cn 10787 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
33 | | npcan 11087 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 −
1) + 1) = 𝑛) |
34 | 31, 32, 33 | sylancl 589 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((𝑛 − 1) + 1) = 𝑛) |
35 | 34 | fveq2d 6721 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (log‘((𝑛 − 1) + 1)) = (log‘𝑛)) |
36 | 15 | rpge0d 12632 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 0 ≤ (𝑛 − 1)) |
37 | | loglesqrt 25644 |
. . . . . . 7
⊢ (((𝑛 − 1) ∈ ℝ ∧
0 ≤ (𝑛 − 1))
→ (log‘((𝑛
− 1) + 1)) ≤ (√‘(𝑛 − 1))) |
38 | 28, 36, 37 | syl2anc 587 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (log‘((𝑛 − 1) + 1)) ≤ (√‘(𝑛 − 1))) |
39 | 35, 38 | eqbrtrrd 5077 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (log‘𝑛) ≤ (√‘(𝑛 − 1))) |
40 | 19 | rpred 12628 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (√‘𝑛) ∈ ℝ) |
41 | 40, 25 | readdcld 10862 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) + (√‘(𝑛 − 1))) ∈
ℝ) |
42 | | remulcl 10814 |
. . . . . . . . . . 11
⊢
(((√‘𝑛)
∈ ℝ ∧ 2 ∈ ℝ) → ((√‘𝑛) · 2) ∈
ℝ) |
43 | 40, 14, 42 | sylancl 589 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) · 2) ∈
ℝ) |
44 | 40, 25 | resubcld 11260 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) − (√‘(𝑛 − 1))) ∈
ℝ) |
45 | 26 | lem1d 11765 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (𝑛 − 1) ≤ 𝑛) |
46 | 6 | rpge0d 12632 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 0 ≤ 𝑛) |
47 | 28, 36, 26, 46 | sqrtled 14990 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((𝑛 − 1) ≤ 𝑛 ↔ (√‘(𝑛 − 1)) ≤ (√‘𝑛))) |
48 | 45, 47 | mpbid 235 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (√‘(𝑛 − 1)) ≤ (√‘𝑛)) |
49 | 40, 25 | subge0d 11422 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (0 ≤ ((√‘𝑛) − (√‘(𝑛 − 1))) ↔
(√‘(𝑛 −
1)) ≤ (√‘𝑛))) |
50 | 48, 49 | mpbird 260 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 0 ≤ ((√‘𝑛) − (√‘(𝑛 − 1)))) |
51 | 25, 40, 40, 48 | leadd2dd 11447 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) + (√‘(𝑛 − 1))) ≤ ((√‘𝑛) + (√‘𝑛))) |
52 | 19 | rpcnd 12630 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (√‘𝑛) ∈ ℂ) |
53 | 52 | times2d 12074 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) · 2) = ((√‘𝑛) + (√‘𝑛))) |
54 | 51, 53 | breqtrrd 5081 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) + (√‘(𝑛 − 1))) ≤ ((√‘𝑛) · 2)) |
55 | 41, 43, 44, 50, 54 | lemul1ad 11771 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((√‘𝑛) + (√‘(𝑛 − 1))) ·
((√‘𝑛) −
(√‘(𝑛 −
1)))) ≤ (((√‘𝑛) · 2) · ((√‘𝑛) − (√‘(𝑛 − 1))))) |
56 | 31 | sqsqrtd 15003 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛)↑2) = 𝑛) |
57 | | subcl 11077 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑛 −
1) ∈ ℂ) |
58 | 31, 32, 57 | sylancl 589 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (𝑛 − 1) ∈ ℂ) |
59 | 58 | sqsqrtd 15003 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘(𝑛 − 1))↑2) = (𝑛 − 1)) |
60 | 56, 59 | oveq12d 7231 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((√‘𝑛)↑2) −
((√‘(𝑛 −
1))↑2)) = (𝑛 −
(𝑛 −
1))) |
61 | 16 | rpcnd 12630 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (√‘(𝑛 − 1)) ∈ ℂ) |
62 | | subsq 13778 |
. . . . . . . . . . 11
⊢
(((√‘𝑛)
∈ ℂ ∧ (√‘(𝑛 − 1)) ∈ ℂ) →
(((√‘𝑛)↑2)
− ((√‘(𝑛
− 1))↑2)) = (((√‘𝑛) + (√‘(𝑛 − 1))) · ((√‘𝑛) − (√‘(𝑛 − 1))))) |
63 | 52, 61, 62 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((√‘𝑛)↑2) −
((√‘(𝑛 −
1))↑2)) = (((√‘𝑛) + (√‘(𝑛 − 1))) · ((√‘𝑛) − (√‘(𝑛 − 1))))) |
64 | | nncan 11107 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑛 −
(𝑛 − 1)) =
1) |
65 | 31, 32, 64 | sylancl 589 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (𝑛 − (𝑛 − 1)) = 1) |
66 | 60, 63, 65 | 3eqtr3d 2785 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((√‘𝑛) + (√‘(𝑛 − 1))) ·
((√‘𝑛) −
(√‘(𝑛 −
1)))) = 1) |
67 | | 2cn 11905 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
68 | 67 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 2 ∈ ℂ) |
69 | 44 | recnd 10861 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) − (√‘(𝑛 − 1))) ∈
ℂ) |
70 | 52, 68, 69 | mulassd 10856 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((√‘𝑛) · 2) ·
((√‘𝑛) −
(√‘(𝑛 −
1)))) = ((√‘𝑛)
· (2 · ((√‘𝑛) − (√‘(𝑛 − 1)))))) |
71 | 55, 66, 70 | 3brtr3d 5084 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 1 ≤ ((√‘𝑛) · (2 ·
((√‘𝑛) −
(√‘(𝑛 −
1)))))) |
72 | | 1red 10834 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 1 ∈ ℝ) |
73 | | remulcl 10814 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ ((√‘𝑛) − (√‘(𝑛 − 1))) ∈ ℝ) → (2
· ((√‘𝑛)
− (√‘(𝑛
− 1)))) ∈ ℝ) |
74 | 14, 44, 73 | sylancr 590 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (2 · ((√‘𝑛) − (√‘(𝑛 − 1)))) ∈
ℝ) |
75 | 40, 74 | remulcld 10863 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) · (2 · ((√‘𝑛) − (√‘(𝑛 − 1))))) ∈
ℝ) |
76 | 72, 75, 16 | lemul1d 12671 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (1 ≤ ((√‘𝑛) · (2 ·
((√‘𝑛) −
(√‘(𝑛 −
1))))) ↔ (1 · (√‘(𝑛 − 1))) ≤ (((√‘𝑛) · (2 ·
((√‘𝑛) −
(√‘(𝑛 −
1))))) · (√‘(𝑛 − 1))))) |
77 | 71, 76 | mpbid 235 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (1 · (√‘(𝑛 − 1))) ≤
(((√‘𝑛)
· (2 · ((√‘𝑛) − (√‘(𝑛 − 1))))) ·
(√‘(𝑛 −
1)))) |
78 | 61 | mulid2d 10851 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (1 · (√‘(𝑛 − 1))) =
(√‘(𝑛 −
1))) |
79 | 74 | recnd 10861 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (2 · ((√‘𝑛) − (√‘(𝑛 − 1)))) ∈
ℂ) |
80 | 52, 79, 61 | mul32d 11042 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((√‘𝑛) · (2 ·
((√‘𝑛) −
(√‘(𝑛 −
1))))) · (√‘(𝑛 − 1))) = (((√‘𝑛) · (√‘(𝑛 − 1))) · (2
· ((√‘𝑛)
− (√‘(𝑛
− 1)))))) |
81 | 77, 78, 80 | 3brtr3d 5084 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (√‘(𝑛 − 1)) ≤ (((√‘𝑛) · (√‘(𝑛 − 1))) · (2
· ((√‘𝑛)
− (√‘(𝑛
− 1)))))) |
82 | | remsqsqrt 14820 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℝ ∧ 0 ≤
𝑛) →
((√‘𝑛) ·
(√‘𝑛)) = 𝑛) |
83 | 26, 46, 82 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) · (√‘𝑛)) = 𝑛) |
84 | | remsqsqrt 14820 |
. . . . . . . . . . 11
⊢ (((𝑛 − 1) ∈ ℝ ∧
0 ≤ (𝑛 − 1))
→ ((√‘(𝑛
− 1)) · (√‘(𝑛 − 1))) = (𝑛 − 1)) |
85 | 28, 36, 84 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘(𝑛 − 1)) ·
(√‘(𝑛 −
1))) = (𝑛 −
1)) |
86 | 83, 85 | oveq12d 7231 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((√‘𝑛) · (√‘𝑛)) ·
((√‘(𝑛 −
1)) · (√‘(𝑛 − 1)))) = (𝑛 · (𝑛 − 1))) |
87 | 52, 52, 61, 61 | mul4d 11044 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((√‘𝑛) · (√‘𝑛)) ·
((√‘(𝑛 −
1)) · (√‘(𝑛 − 1)))) = (((√‘𝑛) · (√‘(𝑛 − 1))) ·
((√‘𝑛) ·
(√‘(𝑛 −
1))))) |
88 | 86, 87 | eqtr3d 2779 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (𝑛 · (𝑛 − 1)) = (((√‘𝑛) · (√‘(𝑛 − 1))) ·
((√‘𝑛) ·
(√‘(𝑛 −
1))))) |
89 | 16 | rpcnne0d 12637 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘(𝑛 − 1)) ∈ ℂ
∧ (√‘(𝑛
− 1)) ≠ 0)) |
90 | 19 | rpcnne0d 12637 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) ∈ ℂ ∧ (√‘𝑛) ≠ 0)) |
91 | | divsubdiv 11548 |
. . . . . . . . . 10
⊢ (((2
∈ ℂ ∧ 2 ∈ ℂ) ∧ (((√‘(𝑛 − 1)) ∈ ℂ
∧ (√‘(𝑛
− 1)) ≠ 0) ∧ ((√‘𝑛) ∈ ℂ ∧ (√‘𝑛) ≠ 0))) → ((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛))) = (((2 · (√‘𝑛)) − (2 ·
(√‘(𝑛 −
1)))) / ((√‘(𝑛
− 1)) · (√‘𝑛)))) |
92 | 68, 68, 89, 90, 91 | syl22anc 839 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((2 / (√‘(𝑛 − 1))) − (2 /
(√‘𝑛))) = (((2
· (√‘𝑛))
− (2 · (√‘(𝑛 − 1)))) / ((√‘(𝑛 − 1)) ·
(√‘𝑛)))) |
93 | 68, 52, 61 | subdid 11288 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (2 · ((√‘𝑛) − (√‘(𝑛 − 1)))) = ((2 ·
(√‘𝑛)) −
(2 · (√‘(𝑛 − 1))))) |
94 | 52, 61 | mulcomd 10854 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) · (√‘(𝑛 − 1))) = ((√‘(𝑛 − 1)) ·
(√‘𝑛))) |
95 | 93, 94 | oveq12d 7231 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((2 · ((√‘𝑛) − (√‘(𝑛 − 1)))) /
((√‘𝑛) ·
(√‘(𝑛 −
1)))) = (((2 · (√‘𝑛)) − (2 · (√‘(𝑛 − 1)))) /
((√‘(𝑛 −
1)) · (√‘𝑛)))) |
96 | 92, 95 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((2 / (√‘(𝑛 − 1))) − (2 /
(√‘𝑛))) = ((2
· ((√‘𝑛)
− (√‘(𝑛
− 1)))) / ((√‘𝑛) · (√‘(𝑛 − 1))))) |
97 | 88, 96 | oveq12d 7231 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((𝑛 · (𝑛 − 1)) · ((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛)))) = ((((√‘𝑛) · (√‘(𝑛 − 1))) · ((√‘𝑛) · (√‘(𝑛 − 1)))) · ((2
· ((√‘𝑛)
− (√‘(𝑛
− 1)))) / ((√‘𝑛) · (√‘(𝑛 − 1)))))) |
98 | 52, 61 | mulcld 10853 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) · (√‘(𝑛 − 1))) ∈
ℂ) |
99 | 19, 16 | rpmulcld 12644 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) · (√‘(𝑛 − 1))) ∈
ℝ+) |
100 | 74, 99 | rerpdivcld 12659 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((2 · ((√‘𝑛) − (√‘(𝑛 − 1)))) /
((√‘𝑛) ·
(√‘(𝑛 −
1)))) ∈ ℝ) |
101 | 100 | recnd 10861 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((2 · ((√‘𝑛) − (√‘(𝑛 − 1)))) /
((√‘𝑛) ·
(√‘(𝑛 −
1)))) ∈ ℂ) |
102 | 98, 98, 101 | mulassd 10856 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((((√‘𝑛) · (√‘(𝑛 − 1))) ·
((√‘𝑛) ·
(√‘(𝑛 −
1)))) · ((2 · ((√‘𝑛) − (√‘(𝑛 − 1)))) / ((√‘𝑛) · (√‘(𝑛 − 1))))) =
(((√‘𝑛)
· (√‘(𝑛
− 1))) · (((√‘𝑛) · (√‘(𝑛 − 1))) · ((2 ·
((√‘𝑛) −
(√‘(𝑛 −
1)))) / ((√‘𝑛)
· (√‘(𝑛
− 1))))))) |
103 | 99 | rpne0d 12633 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) · (√‘(𝑛 − 1))) ≠ 0) |
104 | 79, 98, 103 | divcan2d 11610 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((√‘𝑛) · (√‘(𝑛 − 1))) · ((2
· ((√‘𝑛)
− (√‘(𝑛
− 1)))) / ((√‘𝑛) · (√‘(𝑛 − 1))))) = (2 ·
((√‘𝑛) −
(√‘(𝑛 −
1))))) |
105 | 104 | oveq2d 7229 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((√‘𝑛) · (√‘(𝑛 − 1))) ·
(((√‘𝑛)
· (√‘(𝑛
− 1))) · ((2 · ((√‘𝑛) − (√‘(𝑛 − 1)))) / ((√‘𝑛) · (√‘(𝑛 − 1)))))) =
(((√‘𝑛)
· (√‘(𝑛
− 1))) · (2 · ((√‘𝑛) − (√‘(𝑛 − 1)))))) |
106 | 97, 102, 105 | 3eqtrd 2781 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((𝑛 · (𝑛 − 1)) · ((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛)))) = (((√‘𝑛) · (√‘(𝑛 − 1))) · (2 ·
((√‘𝑛) −
(√‘(𝑛 −
1)))))) |
107 | 81, 106 | breqtrrd 5081 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (√‘(𝑛 − 1)) ≤ ((𝑛 · (𝑛 − 1)) · ((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛))))) |
108 | 7, 25, 30, 39, 107 | letrd 10989 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (log‘𝑛) ≤ ((𝑛 · (𝑛 − 1)) · ((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛))))) |
109 | 11 | nngt0d 11879 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 0 < (𝑛 · (𝑛 − 1))) |
110 | | ledivmul 11708 |
. . . . 5
⊢
(((log‘𝑛)
∈ ℝ ∧ ((2 / (√‘(𝑛 − 1))) − (2 /
(√‘𝑛))) ∈
ℝ ∧ ((𝑛 ·
(𝑛 − 1)) ∈
ℝ ∧ 0 < (𝑛
· (𝑛 − 1))))
→ (((log‘𝑛) /
(𝑛 · (𝑛 − 1))) ≤ ((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛))) ↔ (log‘𝑛) ≤ ((𝑛 · (𝑛 − 1)) · ((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛)))))) |
111 | 7, 22, 29, 109, 110 | syl112anc 1376 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((log‘𝑛) / (𝑛 · (𝑛 − 1))) ≤ ((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛))) ↔ (log‘𝑛) ≤ ((𝑛 · (𝑛 − 1)) · ((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛)))))) |
112 | 108, 111 | mpbird 260 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((log‘𝑛) / (𝑛 · (𝑛 − 1))) ≤ ((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛)))) |
113 | 1, 12, 22, 112 | fsumle 15363 |
. 2
⊢ (𝐴 ∈ ℕ →
Σ𝑛 ∈ (2...𝐴)((log‘𝑛) / (𝑛 · (𝑛 − 1))) ≤ Σ𝑛 ∈ (2...𝐴)((2 / (√‘(𝑛 − 1))) − (2 /
(√‘𝑛)))) |
114 | | fvoveq1 7236 |
. . . . . 6
⊢ (𝑘 = 𝑛 → (√‘(𝑘 − 1)) = (√‘(𝑛 − 1))) |
115 | 114 | oveq2d 7229 |
. . . . 5
⊢ (𝑘 = 𝑛 → (2 / (√‘(𝑘 − 1))) = (2 /
(√‘(𝑛 −
1)))) |
116 | | fvoveq1 7236 |
. . . . . 6
⊢ (𝑘 = (𝑛 + 1) → (√‘(𝑘 − 1)) =
(√‘((𝑛 + 1)
− 1))) |
117 | 116 | oveq2d 7229 |
. . . . 5
⊢ (𝑘 = (𝑛 + 1) → (2 / (√‘(𝑘 − 1))) = (2 /
(√‘((𝑛 + 1)
− 1)))) |
118 | | oveq1 7220 |
. . . . . . . . . 10
⊢ (𝑘 = 2 → (𝑘 − 1) = (2 − 1)) |
119 | | 2m1e1 11956 |
. . . . . . . . . 10
⊢ (2
− 1) = 1 |
120 | 118, 119 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (𝑘 = 2 → (𝑘 − 1) = 1) |
121 | 120 | fveq2d 6721 |
. . . . . . . 8
⊢ (𝑘 = 2 →
(√‘(𝑘 −
1)) = (√‘1)) |
122 | | sqrt1 14835 |
. . . . . . . 8
⊢
(√‘1) = 1 |
123 | 121, 122 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝑘 = 2 →
(√‘(𝑘 −
1)) = 1) |
124 | 123 | oveq2d 7229 |
. . . . . 6
⊢ (𝑘 = 2 → (2 /
(√‘(𝑘 −
1))) = (2 / 1)) |
125 | 67 | div1i 11560 |
. . . . . 6
⊢ (2 / 1) =
2 |
126 | 124, 125 | eqtrdi 2794 |
. . . . 5
⊢ (𝑘 = 2 → (2 /
(√‘(𝑘 −
1))) = 2) |
127 | | fvoveq1 7236 |
. . . . . 6
⊢ (𝑘 = (𝐴 + 1) → (√‘(𝑘 − 1)) =
(√‘((𝐴 + 1)
− 1))) |
128 | 127 | oveq2d 7229 |
. . . . 5
⊢ (𝑘 = (𝐴 + 1) → (2 / (√‘(𝑘 − 1))) = (2 /
(√‘((𝐴 + 1)
− 1)))) |
129 | | nnz 12199 |
. . . . 5
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℤ) |
130 | | eluzp1p1 12466 |
. . . . . . 7
⊢ (𝐴 ∈
(ℤ≥‘1) → (𝐴 + 1) ∈
(ℤ≥‘(1 + 1))) |
131 | | nnuz 12477 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
132 | 130, 131 | eleq2s 2856 |
. . . . . 6
⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈
(ℤ≥‘(1 + 1))) |
133 | | df-2 11893 |
. . . . . . 7
⊢ 2 = (1 +
1) |
134 | 133 | fveq2i 6720 |
. . . . . 6
⊢
(ℤ≥‘2) = (ℤ≥‘(1 +
1)) |
135 | 132, 134 | eleqtrrdi 2849 |
. . . . 5
⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈
(ℤ≥‘2)) |
136 | | elfzuz 13108 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (2...(𝐴 + 1)) → 𝑘 ∈
(ℤ≥‘2)) |
137 | | uz2m1nn 12519 |
. . . . . . . . . . 11
⊢ (𝑘 ∈
(ℤ≥‘2) → (𝑘 − 1) ∈ ℕ) |
138 | 136, 137 | syl 17 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (2...(𝐴 + 1)) → (𝑘 − 1) ∈ ℕ) |
139 | 138 | adantl 485 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (2...(𝐴 + 1))) → (𝑘 − 1) ∈ ℕ) |
140 | 139 | nnrpd 12626 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (2...(𝐴 + 1))) → (𝑘 − 1) ∈
ℝ+) |
141 | 140 | rpsqrtcld 14975 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (2...(𝐴 + 1))) → (√‘(𝑘 − 1)) ∈
ℝ+) |
142 | | rerpdivcl 12616 |
. . . . . . 7
⊢ ((2
∈ ℝ ∧ (√‘(𝑘 − 1)) ∈ ℝ+)
→ (2 / (√‘(𝑘 − 1))) ∈
ℝ) |
143 | 14, 141, 142 | sylancr 590 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (2...(𝐴 + 1))) → (2 / (√‘(𝑘 − 1))) ∈
ℝ) |
144 | 143 | recnd 10861 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (2...(𝐴 + 1))) → (2 / (√‘(𝑘 − 1))) ∈
ℂ) |
145 | 115, 117,
126, 128, 129, 135, 144 | telfsum 15368 |
. . . 4
⊢ (𝐴 ∈ ℕ →
Σ𝑛 ∈ (2...𝐴)((2 / (√‘(𝑛 − 1))) − (2 /
(√‘((𝑛 + 1)
− 1)))) = (2 − (2 / (√‘((𝐴 + 1) − 1))))) |
146 | | pncan 11084 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 + 1)
− 1) = 𝑛) |
147 | 31, 32, 146 | sylancl 589 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((𝑛 + 1) − 1) = 𝑛) |
148 | 147 | fveq2d 6721 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (√‘((𝑛 + 1) − 1)) =
(√‘𝑛)) |
149 | 148 | oveq2d 7229 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (2 / (√‘((𝑛 + 1) − 1))) = (2 /
(√‘𝑛))) |
150 | 149 | oveq2d 7229 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((2 / (√‘(𝑛 − 1))) − (2 /
(√‘((𝑛 + 1)
− 1)))) = ((2 / (√‘(𝑛 − 1))) − (2 /
(√‘𝑛)))) |
151 | 150 | sumeq2dv 15267 |
. . . 4
⊢ (𝐴 ∈ ℕ →
Σ𝑛 ∈ (2...𝐴)((2 / (√‘(𝑛 − 1))) − (2 /
(√‘((𝑛 + 1)
− 1)))) = Σ𝑛
∈ (2...𝐴)((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛)))) |
152 | | nncn 11838 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℂ) |
153 | | pncan 11084 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐴 + 1)
− 1) = 𝐴) |
154 | 152, 32, 153 | sylancl 589 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ → ((𝐴 + 1) − 1) = 𝐴) |
155 | 154 | fveq2d 6721 |
. . . . . 6
⊢ (𝐴 ∈ ℕ →
(√‘((𝐴 + 1)
− 1)) = (√‘𝐴)) |
156 | 155 | oveq2d 7229 |
. . . . 5
⊢ (𝐴 ∈ ℕ → (2 /
(√‘((𝐴 + 1)
− 1))) = (2 / (√‘𝐴))) |
157 | 156 | oveq2d 7229 |
. . . 4
⊢ (𝐴 ∈ ℕ → (2
− (2 / (√‘((𝐴 + 1) − 1)))) = (2 − (2 /
(√‘𝐴)))) |
158 | 145, 151,
157 | 3eqtr3d 2785 |
. . 3
⊢ (𝐴 ∈ ℕ →
Σ𝑛 ∈ (2...𝐴)((2 / (√‘(𝑛 − 1))) − (2 /
(√‘𝑛))) = (2
− (2 / (√‘𝐴)))) |
159 | | 2rp 12591 |
. . . . . 6
⊢ 2 ∈
ℝ+ |
160 | | nnrp 12597 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ+) |
161 | 160 | rpsqrtcld 14975 |
. . . . . 6
⊢ (𝐴 ∈ ℕ →
(√‘𝐴) ∈
ℝ+) |
162 | | rpdivcl 12611 |
. . . . . 6
⊢ ((2
∈ ℝ+ ∧ (√‘𝐴) ∈ ℝ+) → (2 /
(√‘𝐴)) ∈
ℝ+) |
163 | 159, 161,
162 | sylancr 590 |
. . . . 5
⊢ (𝐴 ∈ ℕ → (2 /
(√‘𝐴)) ∈
ℝ+) |
164 | 163 | rpge0d 12632 |
. . . 4
⊢ (𝐴 ∈ ℕ → 0 ≤ (2
/ (√‘𝐴))) |
165 | 163 | rpred 12628 |
. . . . 5
⊢ (𝐴 ∈ ℕ → (2 /
(√‘𝐴)) ∈
ℝ) |
166 | | subge02 11348 |
. . . . 5
⊢ ((2
∈ ℝ ∧ (2 / (√‘𝐴)) ∈ ℝ) → (0 ≤ (2 /
(√‘𝐴)) ↔
(2 − (2 / (√‘𝐴))) ≤ 2)) |
167 | 14, 165, 166 | sylancr 590 |
. . . 4
⊢ (𝐴 ∈ ℕ → (0 ≤
(2 / (√‘𝐴))
↔ (2 − (2 / (√‘𝐴))) ≤ 2)) |
168 | 164, 167 | mpbid 235 |
. . 3
⊢ (𝐴 ∈ ℕ → (2
− (2 / (√‘𝐴))) ≤ 2) |
169 | 158, 168 | eqbrtrd 5075 |
. 2
⊢ (𝐴 ∈ ℕ →
Σ𝑛 ∈ (2...𝐴)((2 / (√‘(𝑛 − 1))) − (2 /
(√‘𝑛))) ≤
2) |
170 | 13, 23, 24, 113, 169 | letrd 10989 |
1
⊢ (𝐴 ∈ ℕ →
Σ𝑛 ∈ (2...𝐴)((log‘𝑛) / (𝑛 · (𝑛 − 1))) ≤ 2) |