Step | Hyp | Ref
| Expression |
1 | | fzfid 12812 |
. . 3
⊢ (𝐴 ∈ ℕ →
(2...𝐴) ∈
Fin) |
2 | | elfzuz 12376 |
. . . . . . . 8
⊢ (𝑛 ∈ (2...𝐴) → 𝑛 ∈
(ℤ≥‘2)) |
3 | | eluz2nn 11764 |
. . . . . . . 8
⊢ (𝑛 ∈
(ℤ≥‘2) → 𝑛 ∈ ℕ) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ (𝑛 ∈ (2...𝐴) → 𝑛 ∈ ℕ) |
5 | 4 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 𝑛 ∈ ℕ) |
6 | 5 | nnrpd 11908 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 𝑛 ∈ ℝ+) |
7 | 6 | relogcld 24414 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (log‘𝑛) ∈ ℝ) |
8 | 2 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 𝑛 ∈
(ℤ≥‘2)) |
9 | | uz2m1nn 11801 |
. . . . . 6
⊢ (𝑛 ∈
(ℤ≥‘2) → (𝑛 − 1) ∈ ℕ) |
10 | 8, 9 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (𝑛 − 1) ∈ ℕ) |
11 | 5, 10 | nnmulcld 11106 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (𝑛 · (𝑛 − 1)) ∈ ℕ) |
12 | 7, 11 | nndivred 11107 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((log‘𝑛) / (𝑛 · (𝑛 − 1))) ∈
ℝ) |
13 | 1, 12 | fsumrecl 14509 |
. 2
⊢ (𝐴 ∈ ℕ →
Σ𝑛 ∈ (2...𝐴)((log‘𝑛) / (𝑛 · (𝑛 − 1))) ∈
ℝ) |
14 | | 2re 11128 |
. . . . 5
⊢ 2 ∈
ℝ |
15 | 10 | nnrpd 11908 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (𝑛 − 1) ∈
ℝ+) |
16 | 15 | rpsqrtcld 14194 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (√‘(𝑛 − 1)) ∈
ℝ+) |
17 | | rerpdivcl 11899 |
. . . . 5
⊢ ((2
∈ ℝ ∧ (√‘(𝑛 − 1)) ∈ ℝ+)
→ (2 / (√‘(𝑛 − 1))) ∈
ℝ) |
18 | 14, 16, 17 | sylancr 696 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (2 / (√‘(𝑛 − 1))) ∈
ℝ) |
19 | 6 | rpsqrtcld 14194 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (√‘𝑛) ∈
ℝ+) |
20 | | rerpdivcl 11899 |
. . . . 5
⊢ ((2
∈ ℝ ∧ (√‘𝑛) ∈ ℝ+) → (2 /
(√‘𝑛)) ∈
ℝ) |
21 | 14, 19, 20 | sylancr 696 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (2 / (√‘𝑛)) ∈
ℝ) |
22 | 18, 21 | resubcld 10496 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((2 / (√‘(𝑛 − 1))) − (2 /
(√‘𝑛))) ∈
ℝ) |
23 | 1, 22 | fsumrecl 14509 |
. 2
⊢ (𝐴 ∈ ℕ →
Σ𝑛 ∈ (2...𝐴)((2 / (√‘(𝑛 − 1))) − (2 /
(√‘𝑛))) ∈
ℝ) |
24 | 14 | a1i 11 |
. 2
⊢ (𝐴 ∈ ℕ → 2 ∈
ℝ) |
25 | 16 | rpred 11910 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (√‘(𝑛 − 1)) ∈ ℝ) |
26 | 5 | nnred 11073 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 𝑛 ∈ ℝ) |
27 | | peano2rem 10386 |
. . . . . . . 8
⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈
ℝ) |
28 | 26, 27 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (𝑛 − 1) ∈ ℝ) |
29 | 26, 28 | remulcld 10108 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (𝑛 · (𝑛 − 1)) ∈ ℝ) |
30 | 29, 22 | remulcld 10108 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((𝑛 · (𝑛 − 1)) · ((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛)))) ∈ ℝ) |
31 | 5 | nncnd 11074 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 𝑛 ∈ ℂ) |
32 | | ax-1cn 10032 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
33 | | npcan 10328 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 −
1) + 1) = 𝑛) |
34 | 31, 32, 33 | sylancl 695 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((𝑛 − 1) + 1) = 𝑛) |
35 | 34 | fveq2d 6233 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (log‘((𝑛 − 1) + 1)) = (log‘𝑛)) |
36 | 15 | rpge0d 11914 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 0 ≤ (𝑛 − 1)) |
37 | | loglesqrt 24544 |
. . . . . . 7
⊢ (((𝑛 − 1) ∈ ℝ ∧
0 ≤ (𝑛 − 1))
→ (log‘((𝑛
− 1) + 1)) ≤ (√‘(𝑛 − 1))) |
38 | 28, 36, 37 | syl2anc 694 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (log‘((𝑛 − 1) + 1)) ≤ (√‘(𝑛 − 1))) |
39 | 35, 38 | eqbrtrrd 4709 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (log‘𝑛) ≤ (√‘(𝑛 − 1))) |
40 | 19 | rpred 11910 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (√‘𝑛) ∈ ℝ) |
41 | 40, 25 | readdcld 10107 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) + (√‘(𝑛 − 1))) ∈
ℝ) |
42 | | remulcl 10059 |
. . . . . . . . . . 11
⊢
(((√‘𝑛)
∈ ℝ ∧ 2 ∈ ℝ) → ((√‘𝑛) · 2) ∈
ℝ) |
43 | 40, 14, 42 | sylancl 695 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) · 2) ∈
ℝ) |
44 | 40, 25 | resubcld 10496 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) − (√‘(𝑛 − 1))) ∈
ℝ) |
45 | 26 | lem1d 10995 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (𝑛 − 1) ≤ 𝑛) |
46 | 6 | rpge0d 11914 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 0 ≤ 𝑛) |
47 | 28, 36, 26, 46 | sqrtled 14209 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((𝑛 − 1) ≤ 𝑛 ↔ (√‘(𝑛 − 1)) ≤ (√‘𝑛))) |
48 | 45, 47 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (√‘(𝑛 − 1)) ≤ (√‘𝑛)) |
49 | 40, 25 | subge0d 10655 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (0 ≤ ((√‘𝑛) − (√‘(𝑛 − 1))) ↔
(√‘(𝑛 −
1)) ≤ (√‘𝑛))) |
50 | 48, 49 | mpbird 247 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 0 ≤ ((√‘𝑛) − (√‘(𝑛 − 1)))) |
51 | 25, 40, 40, 48 | leadd2dd 10680 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) + (√‘(𝑛 − 1))) ≤ ((√‘𝑛) + (√‘𝑛))) |
52 | 19 | rpcnd 11912 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (√‘𝑛) ∈ ℂ) |
53 | 52 | times2d 11314 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) · 2) = ((√‘𝑛) + (√‘𝑛))) |
54 | 51, 53 | breqtrrd 4713 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) + (√‘(𝑛 − 1))) ≤ ((√‘𝑛) · 2)) |
55 | 41, 43, 44, 50, 54 | lemul1ad 11001 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((√‘𝑛) + (√‘(𝑛 − 1))) ·
((√‘𝑛) −
(√‘(𝑛 −
1)))) ≤ (((√‘𝑛) · 2) · ((√‘𝑛) − (√‘(𝑛 − 1))))) |
56 | 31 | sqsqrtd 14222 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛)↑2) = 𝑛) |
57 | | subcl 10318 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑛 −
1) ∈ ℂ) |
58 | 31, 32, 57 | sylancl 695 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (𝑛 − 1) ∈ ℂ) |
59 | 58 | sqsqrtd 14222 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘(𝑛 − 1))↑2) = (𝑛 − 1)) |
60 | 56, 59 | oveq12d 6708 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((√‘𝑛)↑2) −
((√‘(𝑛 −
1))↑2)) = (𝑛 −
(𝑛 −
1))) |
61 | 16 | rpcnd 11912 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (√‘(𝑛 − 1)) ∈ ℂ) |
62 | | subsq 13012 |
. . . . . . . . . . 11
⊢
(((√‘𝑛)
∈ ℂ ∧ (√‘(𝑛 − 1)) ∈ ℂ) →
(((√‘𝑛)↑2)
− ((√‘(𝑛
− 1))↑2)) = (((√‘𝑛) + (√‘(𝑛 − 1))) · ((√‘𝑛) − (√‘(𝑛 − 1))))) |
63 | 52, 61, 62 | syl2anc 694 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((√‘𝑛)↑2) −
((√‘(𝑛 −
1))↑2)) = (((√‘𝑛) + (√‘(𝑛 − 1))) · ((√‘𝑛) − (√‘(𝑛 − 1))))) |
64 | | nncan 10348 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑛 −
(𝑛 − 1)) =
1) |
65 | 31, 32, 64 | sylancl 695 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (𝑛 − (𝑛 − 1)) = 1) |
66 | 60, 63, 65 | 3eqtr3d 2693 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((√‘𝑛) + (√‘(𝑛 − 1))) ·
((√‘𝑛) −
(√‘(𝑛 −
1)))) = 1) |
67 | | 2cn 11129 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
68 | 67 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 2 ∈ ℂ) |
69 | 44 | recnd 10106 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) − (√‘(𝑛 − 1))) ∈
ℂ) |
70 | 52, 68, 69 | mulassd 10101 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((√‘𝑛) · 2) ·
((√‘𝑛) −
(√‘(𝑛 −
1)))) = ((√‘𝑛)
· (2 · ((√‘𝑛) − (√‘(𝑛 − 1)))))) |
71 | 55, 66, 70 | 3brtr3d 4716 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 1 ≤ ((√‘𝑛) · (2 ·
((√‘𝑛) −
(√‘(𝑛 −
1)))))) |
72 | | 1red 10093 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 1 ∈ ℝ) |
73 | | remulcl 10059 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ ((√‘𝑛) − (√‘(𝑛 − 1))) ∈ ℝ) → (2
· ((√‘𝑛)
− (√‘(𝑛
− 1)))) ∈ ℝ) |
74 | 14, 44, 73 | sylancr 696 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (2 · ((√‘𝑛) − (√‘(𝑛 − 1)))) ∈
ℝ) |
75 | 40, 74 | remulcld 10108 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) · (2 · ((√‘𝑛) − (√‘(𝑛 − 1))))) ∈
ℝ) |
76 | 72, 75, 16 | lemul1d 11953 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (1 ≤ ((√‘𝑛) · (2 ·
((√‘𝑛) −
(√‘(𝑛 −
1))))) ↔ (1 · (√‘(𝑛 − 1))) ≤ (((√‘𝑛) · (2 ·
((√‘𝑛) −
(√‘(𝑛 −
1))))) · (√‘(𝑛 − 1))))) |
77 | 71, 76 | mpbid 222 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (1 · (√‘(𝑛 − 1))) ≤
(((√‘𝑛)
· (2 · ((√‘𝑛) − (√‘(𝑛 − 1))))) ·
(√‘(𝑛 −
1)))) |
78 | 61 | mulid2d 10096 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (1 · (√‘(𝑛 − 1))) =
(√‘(𝑛 −
1))) |
79 | 74 | recnd 10106 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (2 · ((√‘𝑛) − (√‘(𝑛 − 1)))) ∈
ℂ) |
80 | 52, 79, 61 | mul32d 10284 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((√‘𝑛) · (2 ·
((√‘𝑛) −
(√‘(𝑛 −
1))))) · (√‘(𝑛 − 1))) = (((√‘𝑛) · (√‘(𝑛 − 1))) · (2
· ((√‘𝑛)
− (√‘(𝑛
− 1)))))) |
81 | 77, 78, 80 | 3brtr3d 4716 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (√‘(𝑛 − 1)) ≤ (((√‘𝑛) · (√‘(𝑛 − 1))) · (2
· ((√‘𝑛)
− (√‘(𝑛
− 1)))))) |
82 | | remsqsqrt 14041 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℝ ∧ 0 ≤
𝑛) →
((√‘𝑛) ·
(√‘𝑛)) = 𝑛) |
83 | 26, 46, 82 | syl2anc 694 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) · (√‘𝑛)) = 𝑛) |
84 | | remsqsqrt 14041 |
. . . . . . . . . . 11
⊢ (((𝑛 − 1) ∈ ℝ ∧
0 ≤ (𝑛 − 1))
→ ((√‘(𝑛
− 1)) · (√‘(𝑛 − 1))) = (𝑛 − 1)) |
85 | 28, 36, 84 | syl2anc 694 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘(𝑛 − 1)) ·
(√‘(𝑛 −
1))) = (𝑛 −
1)) |
86 | 83, 85 | oveq12d 6708 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((√‘𝑛) · (√‘𝑛)) ·
((√‘(𝑛 −
1)) · (√‘(𝑛 − 1)))) = (𝑛 · (𝑛 − 1))) |
87 | 52, 52, 61, 61 | mul4d 10286 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((√‘𝑛) · (√‘𝑛)) ·
((√‘(𝑛 −
1)) · (√‘(𝑛 − 1)))) = (((√‘𝑛) · (√‘(𝑛 − 1))) ·
((√‘𝑛) ·
(√‘(𝑛 −
1))))) |
88 | 86, 87 | eqtr3d 2687 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (𝑛 · (𝑛 − 1)) = (((√‘𝑛) · (√‘(𝑛 − 1))) ·
((√‘𝑛) ·
(√‘(𝑛 −
1))))) |
89 | 16 | rpcnne0d 11919 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘(𝑛 − 1)) ∈ ℂ
∧ (√‘(𝑛
− 1)) ≠ 0)) |
90 | 19 | rpcnne0d 11919 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) ∈ ℂ ∧ (√‘𝑛) ≠ 0)) |
91 | | divsubdiv 10779 |
. . . . . . . . . 10
⊢ (((2
∈ ℂ ∧ 2 ∈ ℂ) ∧ (((√‘(𝑛 − 1)) ∈ ℂ
∧ (√‘(𝑛
− 1)) ≠ 0) ∧ ((√‘𝑛) ∈ ℂ ∧ (√‘𝑛) ≠ 0))) → ((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛))) = (((2 · (√‘𝑛)) − (2 ·
(√‘(𝑛 −
1)))) / ((√‘(𝑛
− 1)) · (√‘𝑛)))) |
92 | 68, 68, 89, 90, 91 | syl22anc 1367 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((2 / (√‘(𝑛 − 1))) − (2 /
(√‘𝑛))) = (((2
· (√‘𝑛))
− (2 · (√‘(𝑛 − 1)))) / ((√‘(𝑛 − 1)) ·
(√‘𝑛)))) |
93 | 68, 52, 61 | subdid 10524 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (2 · ((√‘𝑛) − (√‘(𝑛 − 1)))) = ((2 ·
(√‘𝑛)) −
(2 · (√‘(𝑛 − 1))))) |
94 | 52, 61 | mulcomd 10099 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) · (√‘(𝑛 − 1))) = ((√‘(𝑛 − 1)) ·
(√‘𝑛))) |
95 | 93, 94 | oveq12d 6708 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((2 · ((√‘𝑛) − (√‘(𝑛 − 1)))) /
((√‘𝑛) ·
(√‘(𝑛 −
1)))) = (((2 · (√‘𝑛)) − (2 · (√‘(𝑛 − 1)))) /
((√‘(𝑛 −
1)) · (√‘𝑛)))) |
96 | 92, 95 | eqtr4d 2688 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((2 / (√‘(𝑛 − 1))) − (2 /
(√‘𝑛))) = ((2
· ((√‘𝑛)
− (√‘(𝑛
− 1)))) / ((√‘𝑛) · (√‘(𝑛 − 1))))) |
97 | 88, 96 | oveq12d 6708 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((𝑛 · (𝑛 − 1)) · ((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛)))) = ((((√‘𝑛) · (√‘(𝑛 − 1))) · ((√‘𝑛) · (√‘(𝑛 − 1)))) · ((2
· ((√‘𝑛)
− (√‘(𝑛
− 1)))) / ((√‘𝑛) · (√‘(𝑛 − 1)))))) |
98 | 52, 61 | mulcld 10098 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) · (√‘(𝑛 − 1))) ∈
ℂ) |
99 | 19, 16 | rpmulcld 11926 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) · (√‘(𝑛 − 1))) ∈
ℝ+) |
100 | 74, 99 | rerpdivcld 11941 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((2 · ((√‘𝑛) − (√‘(𝑛 − 1)))) /
((√‘𝑛) ·
(√‘(𝑛 −
1)))) ∈ ℝ) |
101 | 100 | recnd 10106 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((2 · ((√‘𝑛) − (√‘(𝑛 − 1)))) /
((√‘𝑛) ·
(√‘(𝑛 −
1)))) ∈ ℂ) |
102 | 98, 98, 101 | mulassd 10101 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((((√‘𝑛) · (√‘(𝑛 − 1))) ·
((√‘𝑛) ·
(√‘(𝑛 −
1)))) · ((2 · ((√‘𝑛) − (√‘(𝑛 − 1)))) / ((√‘𝑛) · (√‘(𝑛 − 1))))) =
(((√‘𝑛)
· (√‘(𝑛
− 1))) · (((√‘𝑛) · (√‘(𝑛 − 1))) · ((2 ·
((√‘𝑛) −
(√‘(𝑛 −
1)))) / ((√‘𝑛)
· (√‘(𝑛
− 1))))))) |
103 | 99 | rpne0d 11915 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((√‘𝑛) · (√‘(𝑛 − 1))) ≠ 0) |
104 | 79, 98, 103 | divcan2d 10841 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((√‘𝑛) · (√‘(𝑛 − 1))) · ((2
· ((√‘𝑛)
− (√‘(𝑛
− 1)))) / ((√‘𝑛) · (√‘(𝑛 − 1))))) = (2 ·
((√‘𝑛) −
(√‘(𝑛 −
1))))) |
105 | 104 | oveq2d 6706 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((√‘𝑛) · (√‘(𝑛 − 1))) ·
(((√‘𝑛)
· (√‘(𝑛
− 1))) · ((2 · ((√‘𝑛) − (√‘(𝑛 − 1)))) / ((√‘𝑛) · (√‘(𝑛 − 1)))))) =
(((√‘𝑛)
· (√‘(𝑛
− 1))) · (2 · ((√‘𝑛) − (√‘(𝑛 − 1)))))) |
106 | 97, 102, 105 | 3eqtrd 2689 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((𝑛 · (𝑛 − 1)) · ((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛)))) = (((√‘𝑛) · (√‘(𝑛 − 1))) · (2 ·
((√‘𝑛) −
(√‘(𝑛 −
1)))))) |
107 | 81, 106 | breqtrrd 4713 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (√‘(𝑛 − 1)) ≤ ((𝑛 · (𝑛 − 1)) · ((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛))))) |
108 | 7, 25, 30, 39, 107 | letrd 10232 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (log‘𝑛) ≤ ((𝑛 · (𝑛 − 1)) · ((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛))))) |
109 | 11 | nngt0d 11102 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → 0 < (𝑛 · (𝑛 − 1))) |
110 | | ledivmul 10937 |
. . . . 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 1370 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (((log‘𝑛) / (𝑛 · (𝑛 − 1))) ≤ ((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛))) ↔ (log‘𝑛) ≤ ((𝑛 · (𝑛 − 1)) · ((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛)))))) |
112 | 108, 111 | mpbird 247 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((log‘𝑛) / (𝑛 · (𝑛 − 1))) ≤ ((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛)))) |
113 | 1, 12, 22, 112 | fsumle 14575 |
. 2
⊢ (𝐴 ∈ ℕ →
Σ𝑛 ∈ (2...𝐴)((log‘𝑛) / (𝑛 · (𝑛 − 1))) ≤ Σ𝑛 ∈ (2...𝐴)((2 / (√‘(𝑛 − 1))) − (2 /
(√‘𝑛)))) |
114 | | oveq1 6697 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → (𝑘 − 1) = (𝑛 − 1)) |
115 | 114 | fveq2d 6233 |
. . . . . 6
⊢ (𝑘 = 𝑛 → (√‘(𝑘 − 1)) = (√‘(𝑛 − 1))) |
116 | 115 | oveq2d 6706 |
. . . . 5
⊢ (𝑘 = 𝑛 → (2 / (√‘(𝑘 − 1))) = (2 /
(√‘(𝑛 −
1)))) |
117 | | oveq1 6697 |
. . . . . . 7
⊢ (𝑘 = (𝑛 + 1) → (𝑘 − 1) = ((𝑛 + 1) − 1)) |
118 | 117 | fveq2d 6233 |
. . . . . 6
⊢ (𝑘 = (𝑛 + 1) → (√‘(𝑘 − 1)) =
(√‘((𝑛 + 1)
− 1))) |
119 | 118 | oveq2d 6706 |
. . . . 5
⊢ (𝑘 = (𝑛 + 1) → (2 / (√‘(𝑘 − 1))) = (2 /
(√‘((𝑛 + 1)
− 1)))) |
120 | | oveq1 6697 |
. . . . . . . . . 10
⊢ (𝑘 = 2 → (𝑘 − 1) = (2 − 1)) |
121 | | 2m1e1 11173 |
. . . . . . . . . 10
⊢ (2
− 1) = 1 |
122 | 120, 121 | syl6eq 2701 |
. . . . . . . . 9
⊢ (𝑘 = 2 → (𝑘 − 1) = 1) |
123 | 122 | fveq2d 6233 |
. . . . . . . 8
⊢ (𝑘 = 2 →
(√‘(𝑘 −
1)) = (√‘1)) |
124 | | sqrt1 14056 |
. . . . . . . 8
⊢
(√‘1) = 1 |
125 | 123, 124 | syl6eq 2701 |
. . . . . . 7
⊢ (𝑘 = 2 →
(√‘(𝑘 −
1)) = 1) |
126 | 125 | oveq2d 6706 |
. . . . . 6
⊢ (𝑘 = 2 → (2 /
(√‘(𝑘 −
1))) = (2 / 1)) |
127 | 67 | div1i 10791 |
. . . . . 6
⊢ (2 / 1) =
2 |
128 | 126, 127 | syl6eq 2701 |
. . . . 5
⊢ (𝑘 = 2 → (2 /
(√‘(𝑘 −
1))) = 2) |
129 | | oveq1 6697 |
. . . . . . 7
⊢ (𝑘 = (𝐴 + 1) → (𝑘 − 1) = ((𝐴 + 1) − 1)) |
130 | 129 | fveq2d 6233 |
. . . . . 6
⊢ (𝑘 = (𝐴 + 1) → (√‘(𝑘 − 1)) =
(√‘((𝐴 + 1)
− 1))) |
131 | 130 | oveq2d 6706 |
. . . . 5
⊢ (𝑘 = (𝐴 + 1) → (2 / (√‘(𝑘 − 1))) = (2 /
(√‘((𝐴 + 1)
− 1)))) |
132 | | nnz 11437 |
. . . . 5
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℤ) |
133 | | eluzp1p1 11751 |
. . . . . . 7
⊢ (𝐴 ∈
(ℤ≥‘1) → (𝐴 + 1) ∈
(ℤ≥‘(1 + 1))) |
134 | | nnuz 11761 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
135 | 133, 134 | eleq2s 2748 |
. . . . . 6
⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈
(ℤ≥‘(1 + 1))) |
136 | | df-2 11117 |
. . . . . . 7
⊢ 2 = (1 +
1) |
137 | 136 | fveq2i 6232 |
. . . . . 6
⊢
(ℤ≥‘2) = (ℤ≥‘(1 +
1)) |
138 | 135, 137 | syl6eleqr 2741 |
. . . . 5
⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈
(ℤ≥‘2)) |
139 | | elfzuz 12376 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (2...(𝐴 + 1)) → 𝑘 ∈
(ℤ≥‘2)) |
140 | | uz2m1nn 11801 |
. . . . . . . . . . 11
⊢ (𝑘 ∈
(ℤ≥‘2) → (𝑘 − 1) ∈ ℕ) |
141 | 139, 140 | syl 17 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (2...(𝐴 + 1)) → (𝑘 − 1) ∈ ℕ) |
142 | 141 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (2...(𝐴 + 1))) → (𝑘 − 1) ∈ ℕ) |
143 | 142 | nnrpd 11908 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (2...(𝐴 + 1))) → (𝑘 − 1) ∈
ℝ+) |
144 | 143 | rpsqrtcld 14194 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (2...(𝐴 + 1))) → (√‘(𝑘 − 1)) ∈
ℝ+) |
145 | | rerpdivcl 11899 |
. . . . . . 7
⊢ ((2
∈ ℝ ∧ (√‘(𝑘 − 1)) ∈ ℝ+)
→ (2 / (√‘(𝑘 − 1))) ∈
ℝ) |
146 | 14, 144, 145 | sylancr 696 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (2...(𝐴 + 1))) → (2 / (√‘(𝑘 − 1))) ∈
ℝ) |
147 | 146 | recnd 10106 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (2...(𝐴 + 1))) → (2 / (√‘(𝑘 − 1))) ∈
ℂ) |
148 | 116, 119,
128, 131, 132, 138, 147 | telfsum 14580 |
. . . 4
⊢ (𝐴 ∈ ℕ →
Σ𝑛 ∈ (2...𝐴)((2 / (√‘(𝑛 − 1))) − (2 /
(√‘((𝑛 + 1)
− 1)))) = (2 − (2 / (√‘((𝐴 + 1) − 1))))) |
149 | | pncan 10325 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 + 1)
− 1) = 𝑛) |
150 | 31, 32, 149 | sylancl 695 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((𝑛 + 1) − 1) = 𝑛) |
151 | 150 | fveq2d 6233 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (√‘((𝑛 + 1) − 1)) =
(√‘𝑛)) |
152 | 151 | oveq2d 6706 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → (2 / (√‘((𝑛 + 1) − 1))) = (2 /
(√‘𝑛))) |
153 | 152 | oveq2d 6706 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑛 ∈ (2...𝐴)) → ((2 / (√‘(𝑛 − 1))) − (2 /
(√‘((𝑛 + 1)
− 1)))) = ((2 / (√‘(𝑛 − 1))) − (2 /
(√‘𝑛)))) |
154 | 153 | sumeq2dv 14477 |
. . . 4
⊢ (𝐴 ∈ ℕ →
Σ𝑛 ∈ (2...𝐴)((2 / (√‘(𝑛 − 1))) − (2 /
(√‘((𝑛 + 1)
− 1)))) = Σ𝑛
∈ (2...𝐴)((2 /
(√‘(𝑛 −
1))) − (2 / (√‘𝑛)))) |
155 | | nncn 11066 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℂ) |
156 | | pncan 10325 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐴 + 1)
− 1) = 𝐴) |
157 | 155, 32, 156 | sylancl 695 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ → ((𝐴 + 1) − 1) = 𝐴) |
158 | 157 | fveq2d 6233 |
. . . . . 6
⊢ (𝐴 ∈ ℕ →
(√‘((𝐴 + 1)
− 1)) = (√‘𝐴)) |
159 | 158 | oveq2d 6706 |
. . . . 5
⊢ (𝐴 ∈ ℕ → (2 /
(√‘((𝐴 + 1)
− 1))) = (2 / (√‘𝐴))) |
160 | 159 | oveq2d 6706 |
. . . 4
⊢ (𝐴 ∈ ℕ → (2
− (2 / (√‘((𝐴 + 1) − 1)))) = (2 − (2 /
(√‘𝐴)))) |
161 | 148, 154,
160 | 3eqtr3d 2693 |
. . 3
⊢ (𝐴 ∈ ℕ →
Σ𝑛 ∈ (2...𝐴)((2 / (√‘(𝑛 − 1))) − (2 /
(√‘𝑛))) = (2
− (2 / (√‘𝐴)))) |
162 | | 2rp 11875 |
. . . . . 6
⊢ 2 ∈
ℝ+ |
163 | | nnrp 11880 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ+) |
164 | 163 | rpsqrtcld 14194 |
. . . . . 6
⊢ (𝐴 ∈ ℕ →
(√‘𝐴) ∈
ℝ+) |
165 | | rpdivcl 11894 |
. . . . . 6
⊢ ((2
∈ ℝ+ ∧ (√‘𝐴) ∈ ℝ+) → (2 /
(√‘𝐴)) ∈
ℝ+) |
166 | 162, 164,
165 | sylancr 696 |
. . . . 5
⊢ (𝐴 ∈ ℕ → (2 /
(√‘𝐴)) ∈
ℝ+) |
167 | 166 | rpge0d 11914 |
. . . 4
⊢ (𝐴 ∈ ℕ → 0 ≤ (2
/ (√‘𝐴))) |
168 | 166 | rpred 11910 |
. . . . 5
⊢ (𝐴 ∈ ℕ → (2 /
(√‘𝐴)) ∈
ℝ) |
169 | | subge02 10582 |
. . . . 5
⊢ ((2
∈ ℝ ∧ (2 / (√‘𝐴)) ∈ ℝ) → (0 ≤ (2 /
(√‘𝐴)) ↔
(2 − (2 / (√‘𝐴))) ≤ 2)) |
170 | 14, 168, 169 | sylancr 696 |
. . . 4
⊢ (𝐴 ∈ ℕ → (0 ≤
(2 / (√‘𝐴))
↔ (2 − (2 / (√‘𝐴))) ≤ 2)) |
171 | 167, 170 | mpbid 222 |
. . 3
⊢ (𝐴 ∈ ℕ → (2
− (2 / (√‘𝐴))) ≤ 2) |
172 | 161, 171 | eqbrtrd 4707 |
. 2
⊢ (𝐴 ∈ ℕ →
Σ𝑛 ∈ (2...𝐴)((2 / (√‘(𝑛 − 1))) − (2 /
(√‘𝑛))) ≤
2) |
173 | 13, 23, 24, 113, 172 | letrd 10232 |
1
⊢ (𝐴 ∈ ℕ →
Σ𝑛 ∈ (2...𝐴)((log‘𝑛) / (𝑛 · (𝑛 − 1))) ≤ 2) |