Step | Hyp | Ref
| Expression |
1 | | fzfid 13938 |
. . 3
โข (๐ด โ โ โ
(2...๐ด) โ
Fin) |
2 | | elfzuz 13497 |
. . . . . . . 8
โข (๐ โ (2...๐ด) โ ๐ โ
(โคโฅโ2)) |
3 | | eluz2nn 12868 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
4 | 2, 3 | syl 17 |
. . . . . . 7
โข (๐ โ (2...๐ด) โ ๐ โ โ) |
5 | 4 | adantl 483 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ๐ โ โ) |
6 | 5 | nnrpd 13014 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ๐ โ โ+) |
7 | 6 | relogcld 26131 |
. . . 4
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (logโ๐) โ โ) |
8 | 2 | adantl 483 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ๐ โ
(โคโฅโ2)) |
9 | | uz2m1nn 12907 |
. . . . . 6
โข (๐ โ
(โคโฅโ2) โ (๐ โ 1) โ โ) |
10 | 8, 9 | syl 17 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (๐ โ 1) โ โ) |
11 | 5, 10 | nnmulcld 12265 |
. . . 4
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (๐ ยท (๐ โ 1)) โ โ) |
12 | 7, 11 | nndivred 12266 |
. . 3
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((logโ๐) / (๐ ยท (๐ โ 1))) โ
โ) |
13 | 1, 12 | fsumrecl 15680 |
. 2
โข (๐ด โ โ โ
ฮฃ๐ โ (2...๐ด)((logโ๐) / (๐ ยท (๐ โ 1))) โ
โ) |
14 | | 2re 12286 |
. . . . 5
โข 2 โ
โ |
15 | 10 | nnrpd 13014 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (๐ โ 1) โ
โ+) |
16 | 15 | rpsqrtcld 15358 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (โโ(๐ โ 1)) โ
โ+) |
17 | | rerpdivcl 13004 |
. . . . 5
โข ((2
โ โ โง (โโ(๐ โ 1)) โ โ+)
โ (2 / (โโ(๐ โ 1))) โ
โ) |
18 | 14, 16, 17 | sylancr 588 |
. . . 4
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (2 / (โโ(๐ โ 1))) โ
โ) |
19 | 6 | rpsqrtcld 15358 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (โโ๐) โ
โ+) |
20 | | rerpdivcl 13004 |
. . . . 5
โข ((2
โ โ โง (โโ๐) โ โ+) โ (2 /
(โโ๐)) โ
โ) |
21 | 14, 19, 20 | sylancr 588 |
. . . 4
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (2 / (โโ๐)) โ
โ) |
22 | 18, 21 | resubcld 11642 |
. . 3
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((2 / (โโ(๐ โ 1))) โ (2 /
(โโ๐))) โ
โ) |
23 | 1, 22 | fsumrecl 15680 |
. 2
โข (๐ด โ โ โ
ฮฃ๐ โ (2...๐ด)((2 / (โโ(๐ โ 1))) โ (2 /
(โโ๐))) โ
โ) |
24 | 14 | a1i 11 |
. 2
โข (๐ด โ โ โ 2 โ
โ) |
25 | 16 | rpred 13016 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (โโ(๐ โ 1)) โ โ) |
26 | 5 | nnred 12227 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ๐ โ โ) |
27 | | peano2rem 11527 |
. . . . . . . 8
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
28 | 26, 27 | syl 17 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (๐ โ 1) โ โ) |
29 | 26, 28 | remulcld 11244 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (๐ ยท (๐ โ 1)) โ โ) |
30 | 29, 22 | remulcld 11244 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((๐ ยท (๐ โ 1)) ยท ((2 /
(โโ(๐ โ
1))) โ (2 / (โโ๐)))) โ โ) |
31 | 5 | nncnd 12228 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ๐ โ โ) |
32 | | ax-1cn 11168 |
. . . . . . . 8
โข 1 โ
โ |
33 | | npcan 11469 |
. . . . . . . 8
โข ((๐ โ โ โง 1 โ
โ) โ ((๐ โ
1) + 1) = ๐) |
34 | 31, 32, 33 | sylancl 587 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((๐ โ 1) + 1) = ๐) |
35 | 34 | fveq2d 6896 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (logโ((๐ โ 1) + 1)) = (logโ๐)) |
36 | 15 | rpge0d 13020 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ 0 โค (๐ โ 1)) |
37 | | loglesqrt 26266 |
. . . . . . 7
โข (((๐ โ 1) โ โ โง
0 โค (๐ โ 1))
โ (logโ((๐
โ 1) + 1)) โค (โโ(๐ โ 1))) |
38 | 28, 36, 37 | syl2anc 585 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (logโ((๐ โ 1) + 1)) โค (โโ(๐ โ 1))) |
39 | 35, 38 | eqbrtrrd 5173 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (logโ๐) โค (โโ(๐ โ 1))) |
40 | 19 | rpred 13016 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (โโ๐) โ โ) |
41 | 40, 25 | readdcld 11243 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((โโ๐) + (โโ(๐ โ 1))) โ
โ) |
42 | | remulcl 11195 |
. . . . . . . . . . 11
โข
(((โโ๐)
โ โ โง 2 โ โ) โ ((โโ๐) ยท 2) โ
โ) |
43 | 40, 14, 42 | sylancl 587 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((โโ๐) ยท 2) โ
โ) |
44 | 40, 25 | resubcld 11642 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((โโ๐) โ (โโ(๐ โ 1))) โ
โ) |
45 | 26 | lem1d 12147 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (๐ โ 1) โค ๐) |
46 | 6 | rpge0d 13020 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ 0 โค ๐) |
47 | 28, 36, 26, 46 | sqrtled 15373 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((๐ โ 1) โค ๐ โ (โโ(๐ โ 1)) โค (โโ๐))) |
48 | 45, 47 | mpbid 231 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (โโ(๐ โ 1)) โค (โโ๐)) |
49 | 40, 25 | subge0d 11804 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (0 โค ((โโ๐) โ (โโ(๐ โ 1))) โ
(โโ(๐ โ
1)) โค (โโ๐))) |
50 | 48, 49 | mpbird 257 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ 0 โค ((โโ๐) โ (โโ(๐ โ 1)))) |
51 | 25, 40, 40, 48 | leadd2dd 11829 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((โโ๐) + (โโ(๐ โ 1))) โค ((โโ๐) + (โโ๐))) |
52 | 19 | rpcnd 13018 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (โโ๐) โ โ) |
53 | 52 | times2d 12456 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((โโ๐) ยท 2) = ((โโ๐) + (โโ๐))) |
54 | 51, 53 | breqtrrd 5177 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((โโ๐) + (โโ(๐ โ 1))) โค ((โโ๐) ยท 2)) |
55 | 41, 43, 44, 50, 54 | lemul1ad 12153 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (((โโ๐) + (โโ(๐ โ 1))) ยท
((โโ๐) โ
(โโ(๐ โ
1)))) โค (((โโ๐) ยท 2) ยท ((โโ๐) โ (โโ(๐ โ 1))))) |
56 | 31 | sqsqrtd 15386 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((โโ๐)โ2) = ๐) |
57 | | subcl 11459 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง 1 โ
โ) โ (๐ โ
1) โ โ) |
58 | 31, 32, 57 | sylancl 587 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (๐ โ 1) โ โ) |
59 | 58 | sqsqrtd 15386 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((โโ(๐ โ 1))โ2) = (๐ โ 1)) |
60 | 56, 59 | oveq12d 7427 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (((โโ๐)โ2) โ
((โโ(๐ โ
1))โ2)) = (๐ โ
(๐ โ
1))) |
61 | 16 | rpcnd 13018 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (โโ(๐ โ 1)) โ โ) |
62 | | subsq 14174 |
. . . . . . . . . . 11
โข
(((โโ๐)
โ โ โง (โโ(๐ โ 1)) โ โ) โ
(((โโ๐)โ2)
โ ((โโ(๐
โ 1))โ2)) = (((โโ๐) + (โโ(๐ โ 1))) ยท ((โโ๐) โ (โโ(๐ โ 1))))) |
63 | 52, 61, 62 | syl2anc 585 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (((โโ๐)โ2) โ
((โโ(๐ โ
1))โ2)) = (((โโ๐) + (โโ(๐ โ 1))) ยท ((โโ๐) โ (โโ(๐ โ 1))))) |
64 | | nncan 11489 |
. . . . . . . . . . 11
โข ((๐ โ โ โง 1 โ
โ) โ (๐ โ
(๐ โ 1)) =
1) |
65 | 31, 32, 64 | sylancl 587 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (๐ โ (๐ โ 1)) = 1) |
66 | 60, 63, 65 | 3eqtr3d 2781 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (((โโ๐) + (โโ(๐ โ 1))) ยท
((โโ๐) โ
(โโ(๐ โ
1)))) = 1) |
67 | | 2cn 12287 |
. . . . . . . . . . 11
โข 2 โ
โ |
68 | 67 | a1i 11 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ 2 โ โ) |
69 | 44 | recnd 11242 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((โโ๐) โ (โโ(๐ โ 1))) โ
โ) |
70 | 52, 68, 69 | mulassd 11237 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (((โโ๐) ยท 2) ยท
((โโ๐) โ
(โโ(๐ โ
1)))) = ((โโ๐)
ยท (2 ยท ((โโ๐) โ (โโ(๐ โ 1)))))) |
71 | 55, 66, 70 | 3brtr3d 5180 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ 1 โค ((โโ๐) ยท (2 ยท
((โโ๐) โ
(โโ(๐ โ
1)))))) |
72 | | 1red 11215 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ 1 โ โ) |
73 | | remulcl 11195 |
. . . . . . . . . . 11
โข ((2
โ โ โง ((โโ๐) โ (โโ(๐ โ 1))) โ โ) โ (2
ยท ((โโ๐)
โ (โโ(๐
โ 1)))) โ โ) |
74 | 14, 44, 73 | sylancr 588 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (2 ยท ((โโ๐) โ (โโ(๐ โ 1)))) โ
โ) |
75 | 40, 74 | remulcld 11244 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((โโ๐) ยท (2 ยท ((โโ๐) โ (โโ(๐ โ 1))))) โ
โ) |
76 | 72, 75, 16 | lemul1d 13059 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (1 โค ((โโ๐) ยท (2 ยท
((โโ๐) โ
(โโ(๐ โ
1))))) โ (1 ยท (โโ(๐ โ 1))) โค (((โโ๐) ยท (2 ยท
((โโ๐) โ
(โโ(๐ โ
1))))) ยท (โโ(๐ โ 1))))) |
77 | 71, 76 | mpbid 231 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (1 ยท (โโ(๐ โ 1))) โค
(((โโ๐)
ยท (2 ยท ((โโ๐) โ (โโ(๐ โ 1))))) ยท
(โโ(๐ โ
1)))) |
78 | 61 | mullidd 11232 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (1 ยท (โโ(๐ โ 1))) =
(โโ(๐ โ
1))) |
79 | 74 | recnd 11242 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (2 ยท ((โโ๐) โ (โโ(๐ โ 1)))) โ
โ) |
80 | 52, 79, 61 | mul32d 11424 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (((โโ๐) ยท (2 ยท
((โโ๐) โ
(โโ(๐ โ
1))))) ยท (โโ(๐ โ 1))) = (((โโ๐) ยท (โโ(๐ โ 1))) ยท (2
ยท ((โโ๐)
โ (โโ(๐
โ 1)))))) |
81 | 77, 78, 80 | 3brtr3d 5180 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (โโ(๐ โ 1)) โค (((โโ๐) ยท (โโ(๐ โ 1))) ยท (2
ยท ((โโ๐)
โ (โโ(๐
โ 1)))))) |
82 | | remsqsqrt 15203 |
. . . . . . . . . . 11
โข ((๐ โ โ โง 0 โค
๐) โ
((โโ๐) ยท
(โโ๐)) = ๐) |
83 | 26, 46, 82 | syl2anc 585 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((โโ๐) ยท (โโ๐)) = ๐) |
84 | | remsqsqrt 15203 |
. . . . . . . . . . 11
โข (((๐ โ 1) โ โ โง
0 โค (๐ โ 1))
โ ((โโ(๐
โ 1)) ยท (โโ(๐ โ 1))) = (๐ โ 1)) |
85 | 28, 36, 84 | syl2anc 585 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((โโ(๐ โ 1)) ยท
(โโ(๐ โ
1))) = (๐ โ
1)) |
86 | 83, 85 | oveq12d 7427 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (((โโ๐) ยท (โโ๐)) ยท
((โโ(๐ โ
1)) ยท (โโ(๐ โ 1)))) = (๐ ยท (๐ โ 1))) |
87 | 52, 52, 61, 61 | mul4d 11426 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (((โโ๐) ยท (โโ๐)) ยท
((โโ(๐ โ
1)) ยท (โโ(๐ โ 1)))) = (((โโ๐) ยท (โโ(๐ โ 1))) ยท
((โโ๐) ยท
(โโ(๐ โ
1))))) |
88 | 86, 87 | eqtr3d 2775 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (๐ ยท (๐ โ 1)) = (((โโ๐) ยท (โโ(๐ โ 1))) ยท
((โโ๐) ยท
(โโ(๐ โ
1))))) |
89 | 16 | rpcnne0d 13025 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((โโ(๐ โ 1)) โ โ
โง (โโ(๐
โ 1)) โ 0)) |
90 | 19 | rpcnne0d 13025 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((โโ๐) โ โ โง (โโ๐) โ 0)) |
91 | | divsubdiv 11930 |
. . . . . . . . . 10
โข (((2
โ โ โง 2 โ โ) โง (((โโ(๐ โ 1)) โ โ
โง (โโ(๐
โ 1)) โ 0) โง ((โโ๐) โ โ โง (โโ๐) โ 0))) โ ((2 /
(โโ(๐ โ
1))) โ (2 / (โโ๐))) = (((2 ยท (โโ๐)) โ (2 ยท
(โโ(๐ โ
1)))) / ((โโ(๐
โ 1)) ยท (โโ๐)))) |
92 | 68, 68, 89, 90, 91 | syl22anc 838 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((2 / (โโ(๐ โ 1))) โ (2 /
(โโ๐))) = (((2
ยท (โโ๐))
โ (2 ยท (โโ(๐ โ 1)))) / ((โโ(๐ โ 1)) ยท
(โโ๐)))) |
93 | 68, 52, 61 | subdid 11670 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (2 ยท ((โโ๐) โ (โโ(๐ โ 1)))) = ((2 ยท
(โโ๐)) โ
(2 ยท (โโ(๐ โ 1))))) |
94 | 52, 61 | mulcomd 11235 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((โโ๐) ยท (โโ(๐ โ 1))) = ((โโ(๐ โ 1)) ยท
(โโ๐))) |
95 | 93, 94 | oveq12d 7427 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((2 ยท ((โโ๐) โ (โโ(๐ โ 1)))) /
((โโ๐) ยท
(โโ(๐ โ
1)))) = (((2 ยท (โโ๐)) โ (2 ยท (โโ(๐ โ 1)))) /
((โโ(๐ โ
1)) ยท (โโ๐)))) |
96 | 92, 95 | eqtr4d 2776 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((2 / (โโ(๐ โ 1))) โ (2 /
(โโ๐))) = ((2
ยท ((โโ๐)
โ (โโ(๐
โ 1)))) / ((โโ๐) ยท (โโ(๐ โ 1))))) |
97 | 88, 96 | oveq12d 7427 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((๐ ยท (๐ โ 1)) ยท ((2 /
(โโ(๐ โ
1))) โ (2 / (โโ๐)))) = ((((โโ๐) ยท (โโ(๐ โ 1))) ยท ((โโ๐) ยท (โโ(๐ โ 1)))) ยท ((2
ยท ((โโ๐)
โ (โโ(๐
โ 1)))) / ((โโ๐) ยท (โโ(๐ โ 1)))))) |
98 | 52, 61 | mulcld 11234 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((โโ๐) ยท (โโ(๐ โ 1))) โ
โ) |
99 | 19, 16 | rpmulcld 13032 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((โโ๐) ยท (โโ(๐ โ 1))) โ
โ+) |
100 | 74, 99 | rerpdivcld 13047 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((2 ยท ((โโ๐) โ (โโ(๐ โ 1)))) /
((โโ๐) ยท
(โโ(๐ โ
1)))) โ โ) |
101 | 100 | recnd 11242 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((2 ยท ((โโ๐) โ (โโ(๐ โ 1)))) /
((โโ๐) ยท
(โโ(๐ โ
1)))) โ โ) |
102 | 98, 98, 101 | mulassd 11237 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((((โโ๐) ยท (โโ(๐ โ 1))) ยท
((โโ๐) ยท
(โโ(๐ โ
1)))) ยท ((2 ยท ((โโ๐) โ (โโ(๐ โ 1)))) / ((โโ๐) ยท (โโ(๐ โ 1))))) =
(((โโ๐)
ยท (โโ(๐
โ 1))) ยท (((โโ๐) ยท (โโ(๐ โ 1))) ยท ((2 ยท
((โโ๐) โ
(โโ(๐ โ
1)))) / ((โโ๐)
ยท (โโ(๐
โ 1))))))) |
103 | 99 | rpne0d 13021 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((โโ๐) ยท (โโ(๐ โ 1))) โ 0) |
104 | 79, 98, 103 | divcan2d 11992 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (((โโ๐) ยท (โโ(๐ โ 1))) ยท ((2
ยท ((โโ๐)
โ (โโ(๐
โ 1)))) / ((โโ๐) ยท (โโ(๐ โ 1))))) = (2 ยท
((โโ๐) โ
(โโ(๐ โ
1))))) |
105 | 104 | oveq2d 7425 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (((โโ๐) ยท (โโ(๐ โ 1))) ยท
(((โโ๐)
ยท (โโ(๐
โ 1))) ยท ((2 ยท ((โโ๐) โ (โโ(๐ โ 1)))) / ((โโ๐) ยท (โโ(๐ โ 1)))))) =
(((โโ๐)
ยท (โโ(๐
โ 1))) ยท (2 ยท ((โโ๐) โ (โโ(๐ โ 1)))))) |
106 | 97, 102, 105 | 3eqtrd 2777 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((๐ ยท (๐ โ 1)) ยท ((2 /
(โโ(๐ โ
1))) โ (2 / (โโ๐)))) = (((โโ๐) ยท (โโ(๐ โ 1))) ยท (2 ยท
((โโ๐) โ
(โโ(๐ โ
1)))))) |
107 | 81, 106 | breqtrrd 5177 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (โโ(๐ โ 1)) โค ((๐ ยท (๐ โ 1)) ยท ((2 /
(โโ(๐ โ
1))) โ (2 / (โโ๐))))) |
108 | 7, 25, 30, 39, 107 | letrd 11371 |
. . . 4
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (logโ๐) โค ((๐ ยท (๐ โ 1)) ยท ((2 /
(โโ(๐ โ
1))) โ (2 / (โโ๐))))) |
109 | 11 | nngt0d 12261 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ 0 < (๐ ยท (๐ โ 1))) |
110 | | ledivmul 12090 |
. . . . 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 1375 |
. . . 4
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (((logโ๐) / (๐ ยท (๐ โ 1))) โค ((2 /
(โโ(๐ โ
1))) โ (2 / (โโ๐))) โ (logโ๐) โค ((๐ ยท (๐ โ 1)) ยท ((2 /
(โโ(๐ โ
1))) โ (2 / (โโ๐)))))) |
112 | 108, 111 | mpbird 257 |
. . 3
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((logโ๐) / (๐ ยท (๐ โ 1))) โค ((2 /
(โโ(๐ โ
1))) โ (2 / (โโ๐)))) |
113 | 1, 12, 22, 112 | fsumle 15745 |
. 2
โข (๐ด โ โ โ
ฮฃ๐ โ (2...๐ด)((logโ๐) / (๐ ยท (๐ โ 1))) โค ฮฃ๐ โ (2...๐ด)((2 / (โโ(๐ โ 1))) โ (2 /
(โโ๐)))) |
114 | | fvoveq1 7432 |
. . . . . 6
โข (๐ = ๐ โ (โโ(๐ โ 1)) = (โโ(๐ โ 1))) |
115 | 114 | oveq2d 7425 |
. . . . 5
โข (๐ = ๐ โ (2 / (โโ(๐ โ 1))) = (2 /
(โโ(๐ โ
1)))) |
116 | | fvoveq1 7432 |
. . . . . 6
โข (๐ = (๐ + 1) โ (โโ(๐ โ 1)) =
(โโ((๐ + 1)
โ 1))) |
117 | 116 | oveq2d 7425 |
. . . . 5
โข (๐ = (๐ + 1) โ (2 / (โโ(๐ โ 1))) = (2 /
(โโ((๐ + 1)
โ 1)))) |
118 | | oveq1 7416 |
. . . . . . . . . 10
โข (๐ = 2 โ (๐ โ 1) = (2 โ 1)) |
119 | | 2m1e1 12338 |
. . . . . . . . . 10
โข (2
โ 1) = 1 |
120 | 118, 119 | eqtrdi 2789 |
. . . . . . . . 9
โข (๐ = 2 โ (๐ โ 1) = 1) |
121 | 120 | fveq2d 6896 |
. . . . . . . 8
โข (๐ = 2 โ
(โโ(๐ โ
1)) = (โโ1)) |
122 | | sqrt1 15218 |
. . . . . . . 8
โข
(โโ1) = 1 |
123 | 121, 122 | eqtrdi 2789 |
. . . . . . 7
โข (๐ = 2 โ
(โโ(๐ โ
1)) = 1) |
124 | 123 | oveq2d 7425 |
. . . . . 6
โข (๐ = 2 โ (2 /
(โโ(๐ โ
1))) = (2 / 1)) |
125 | 67 | div1i 11942 |
. . . . . 6
โข (2 / 1) =
2 |
126 | 124, 125 | eqtrdi 2789 |
. . . . 5
โข (๐ = 2 โ (2 /
(โโ(๐ โ
1))) = 2) |
127 | | fvoveq1 7432 |
. . . . . 6
โข (๐ = (๐ด + 1) โ (โโ(๐ โ 1)) =
(โโ((๐ด + 1)
โ 1))) |
128 | 127 | oveq2d 7425 |
. . . . 5
โข (๐ = (๐ด + 1) โ (2 / (โโ(๐ โ 1))) = (2 /
(โโ((๐ด + 1)
โ 1)))) |
129 | | nnz 12579 |
. . . . 5
โข (๐ด โ โ โ ๐ด โ
โค) |
130 | | eluzp1p1 12850 |
. . . . . . 7
โข (๐ด โ
(โคโฅโ1) โ (๐ด + 1) โ
(โคโฅโ(1 + 1))) |
131 | | nnuz 12865 |
. . . . . . 7
โข โ =
(โคโฅโ1) |
132 | 130, 131 | eleq2s 2852 |
. . . . . 6
โข (๐ด โ โ โ (๐ด + 1) โ
(โคโฅโ(1 + 1))) |
133 | | df-2 12275 |
. . . . . . 7
โข 2 = (1 +
1) |
134 | 133 | fveq2i 6895 |
. . . . . 6
โข
(โคโฅโ2) = (โคโฅโ(1 +
1)) |
135 | 132, 134 | eleqtrrdi 2845 |
. . . . 5
โข (๐ด โ โ โ (๐ด + 1) โ
(โคโฅโ2)) |
136 | | elfzuz 13497 |
. . . . . . . . . . 11
โข (๐ โ (2...(๐ด + 1)) โ ๐ โ
(โคโฅโ2)) |
137 | | uz2m1nn 12907 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ2) โ (๐ โ 1) โ โ) |
138 | 136, 137 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (2...(๐ด + 1)) โ (๐ โ 1) โ โ) |
139 | 138 | adantl 483 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ (2...(๐ด + 1))) โ (๐ โ 1) โ โ) |
140 | 139 | nnrpd 13014 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ (2...(๐ด + 1))) โ (๐ โ 1) โ
โ+) |
141 | 140 | rpsqrtcld 15358 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ (2...(๐ด + 1))) โ (โโ(๐ โ 1)) โ
โ+) |
142 | | rerpdivcl 13004 |
. . . . . . 7
โข ((2
โ โ โง (โโ(๐ โ 1)) โ โ+)
โ (2 / (โโ(๐ โ 1))) โ
โ) |
143 | 14, 141, 142 | sylancr 588 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ (2...(๐ด + 1))) โ (2 / (โโ(๐ โ 1))) โ
โ) |
144 | 143 | recnd 11242 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ (2...(๐ด + 1))) โ (2 / (โโ(๐ โ 1))) โ
โ) |
145 | 115, 117,
126, 128, 129, 135, 144 | telfsum 15750 |
. . . 4
โข (๐ด โ โ โ
ฮฃ๐ โ (2...๐ด)((2 / (โโ(๐ โ 1))) โ (2 /
(โโ((๐ + 1)
โ 1)))) = (2 โ (2 / (โโ((๐ด + 1) โ 1))))) |
146 | | pncan 11466 |
. . . . . . . . 9
โข ((๐ โ โ โง 1 โ
โ) โ ((๐ + 1)
โ 1) = ๐) |
147 | 31, 32, 146 | sylancl 587 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((๐ + 1) โ 1) = ๐) |
148 | 147 | fveq2d 6896 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (โโ((๐ + 1) โ 1)) =
(โโ๐)) |
149 | 148 | oveq2d 7425 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ (2 / (โโ((๐ + 1) โ 1))) = (2 /
(โโ๐))) |
150 | 149 | oveq2d 7425 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ (2...๐ด)) โ ((2 / (โโ(๐ โ 1))) โ (2 /
(โโ((๐ + 1)
โ 1)))) = ((2 / (โโ(๐ โ 1))) โ (2 /
(โโ๐)))) |
151 | 150 | sumeq2dv 15649 |
. . . 4
โข (๐ด โ โ โ
ฮฃ๐ โ (2...๐ด)((2 / (โโ(๐ โ 1))) โ (2 /
(โโ((๐ + 1)
โ 1)))) = ฮฃ๐
โ (2...๐ด)((2 /
(โโ(๐ โ
1))) โ (2 / (โโ๐)))) |
152 | | nncn 12220 |
. . . . . . . 8
โข (๐ด โ โ โ ๐ด โ
โ) |
153 | | pncan 11466 |
. . . . . . . 8
โข ((๐ด โ โ โง 1 โ
โ) โ ((๐ด + 1)
โ 1) = ๐ด) |
154 | 152, 32, 153 | sylancl 587 |
. . . . . . 7
โข (๐ด โ โ โ ((๐ด + 1) โ 1) = ๐ด) |
155 | 154 | fveq2d 6896 |
. . . . . 6
โข (๐ด โ โ โ
(โโ((๐ด + 1)
โ 1)) = (โโ๐ด)) |
156 | 155 | oveq2d 7425 |
. . . . 5
โข (๐ด โ โ โ (2 /
(โโ((๐ด + 1)
โ 1))) = (2 / (โโ๐ด))) |
157 | 156 | oveq2d 7425 |
. . . 4
โข (๐ด โ โ โ (2
โ (2 / (โโ((๐ด + 1) โ 1)))) = (2 โ (2 /
(โโ๐ด)))) |
158 | 145, 151,
157 | 3eqtr3d 2781 |
. . 3
โข (๐ด โ โ โ
ฮฃ๐ โ (2...๐ด)((2 / (โโ(๐ โ 1))) โ (2 /
(โโ๐))) = (2
โ (2 / (โโ๐ด)))) |
159 | | 2rp 12979 |
. . . . . 6
โข 2 โ
โ+ |
160 | | nnrp 12985 |
. . . . . . 7
โข (๐ด โ โ โ ๐ด โ
โ+) |
161 | 160 | rpsqrtcld 15358 |
. . . . . 6
โข (๐ด โ โ โ
(โโ๐ด) โ
โ+) |
162 | | rpdivcl 12999 |
. . . . . 6
โข ((2
โ โ+ โง (โโ๐ด) โ โ+) โ (2 /
(โโ๐ด)) โ
โ+) |
163 | 159, 161,
162 | sylancr 588 |
. . . . 5
โข (๐ด โ โ โ (2 /
(โโ๐ด)) โ
โ+) |
164 | 163 | rpge0d 13020 |
. . . 4
โข (๐ด โ โ โ 0 โค (2
/ (โโ๐ด))) |
165 | 163 | rpred 13016 |
. . . . 5
โข (๐ด โ โ โ (2 /
(โโ๐ด)) โ
โ) |
166 | | subge02 11730 |
. . . . 5
โข ((2
โ โ โง (2 / (โโ๐ด)) โ โ) โ (0 โค (2 /
(โโ๐ด)) โ
(2 โ (2 / (โโ๐ด))) โค 2)) |
167 | 14, 165, 166 | sylancr 588 |
. . . 4
โข (๐ด โ โ โ (0 โค
(2 / (โโ๐ด))
โ (2 โ (2 / (โโ๐ด))) โค 2)) |
168 | 164, 167 | mpbid 231 |
. . 3
โข (๐ด โ โ โ (2
โ (2 / (โโ๐ด))) โค 2) |
169 | 158, 168 | eqbrtrd 5171 |
. 2
โข (๐ด โ โ โ
ฮฃ๐ โ (2...๐ด)((2 / (โโ(๐ โ 1))) โ (2 /
(โโ๐))) โค
2) |
170 | 13, 23, 24, 113, 169 | letrd 11371 |
1
โข (๐ด โ โ โ
ฮฃ๐ โ (2...๐ด)((logโ๐) / (๐ ยท (๐ โ 1))) โค 2) |