Step | Hyp | Ref
| Expression |
1 | | nnre 12165 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ) |
2 | | nnnn0 12425 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ0) |
3 | 2 | nn0ge0d 12481 |
. . . . . . . 8
โข (๐ โ โ โ 0 โค
๐) |
4 | 1, 3 | ge0p1rpd 12992 |
. . . . . . 7
โข (๐ โ โ โ (๐ + 1) โ
โ+) |
5 | | nnrp 12931 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ+) |
6 | 4, 5 | rpdivcld 12979 |
. . . . . 6
โข (๐ โ โ โ ((๐ + 1) / ๐) โ
โ+) |
7 | 6 | rpsqrtcld 15302 |
. . . . 5
โข (๐ โ โ โ
(โโ((๐ + 1) /
๐)) โ
โ+) |
8 | | nnz 12525 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โค) |
9 | 6, 8 | rpexpcld 14156 |
. . . . 5
โข (๐ โ โ โ (((๐ + 1) / ๐)โ๐) โ
โ+) |
10 | 7, 9 | rpmulcld 12978 |
. . . 4
โข (๐ โ โ โ
((โโ((๐ + 1) /
๐)) ยท (((๐ + 1) / ๐)โ๐)) โ
โ+) |
11 | | epr 16095 |
. . . . 5
โข e โ
โ+ |
12 | 11 | a1i 11 |
. . . 4
โข (๐ โ โ โ e โ
โ+) |
13 | 10, 12 | relogdivd 25997 |
. . 3
โข (๐ โ โ โ
(logโ(((โโ((๐ + 1) / ๐)) ยท (((๐ + 1) / ๐)โ๐)) / e)) =
((logโ((โโ((๐ + 1) / ๐)) ยท (((๐ + 1) / ๐)โ๐))) โ (logโe))) |
14 | 7, 9 | relogmuld 25996 |
. . . . . 6
โข (๐ โ โ โ
(logโ((โโ((๐ + 1) / ๐)) ยท (((๐ + 1) / ๐)โ๐))) = ((logโ(โโ((๐ + 1) / ๐))) + (logโ(((๐ + 1) / ๐)โ๐)))) |
15 | | logsqrt 26075 |
. . . . . . . 8
โข (((๐ + 1) / ๐) โ โ+ โ
(logโ(โโ((๐ + 1) / ๐))) = ((logโ((๐ + 1) / ๐)) / 2)) |
16 | 6, 15 | syl 17 |
. . . . . . 7
โข (๐ โ โ โ
(logโ(โโ((๐ + 1) / ๐))) = ((logโ((๐ + 1) / ๐)) / 2)) |
17 | | relogexp 25967 |
. . . . . . . 8
โข ((((๐ + 1) / ๐) โ โ+ โง ๐ โ โค) โ
(logโ(((๐ + 1) /
๐)โ๐)) = (๐ ยท (logโ((๐ + 1) / ๐)))) |
18 | 6, 8, 17 | syl2anc 585 |
. . . . . . 7
โข (๐ โ โ โ
(logโ(((๐ + 1) /
๐)โ๐)) = (๐ ยท (logโ((๐ + 1) / ๐)))) |
19 | 16, 18 | oveq12d 7376 |
. . . . . 6
โข (๐ โ โ โ
((logโ(โโ((๐ + 1) / ๐))) + (logโ(((๐ + 1) / ๐)โ๐))) = (((logโ((๐ + 1) / ๐)) / 2) + (๐ ยท (logโ((๐ + 1) / ๐))))) |
20 | 14, 19 | eqtrd 2773 |
. . . . 5
โข (๐ โ โ โ
(logโ((โโ((๐ + 1) / ๐)) ยท (((๐ + 1) / ๐)โ๐))) = (((logโ((๐ + 1) / ๐)) / 2) + (๐ ยท (logโ((๐ + 1) / ๐))))) |
21 | | peano2nn 12170 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ + 1) โ
โ) |
22 | 21 | nncnd 12174 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ + 1) โ
โ) |
23 | | nncn 12166 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
24 | | nnne0 12192 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ 0) |
25 | 22, 23, 24 | divcld 11936 |
. . . . . . . 8
โข (๐ โ โ โ ((๐ + 1) / ๐) โ โ) |
26 | 21 | nnne0d 12208 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ + 1) โ 0) |
27 | 22, 23, 26, 24 | divne0d 11952 |
. . . . . . . 8
โข (๐ โ โ โ ((๐ + 1) / ๐) โ 0) |
28 | 25, 27 | logcld 25942 |
. . . . . . 7
โข (๐ โ โ โ
(logโ((๐ + 1) / ๐)) โ
โ) |
29 | | 2cnd 12236 |
. . . . . . 7
โข (๐ โ โ โ 2 โ
โ) |
30 | | 2rp 12925 |
. . . . . . . . 9
โข 2 โ
โ+ |
31 | 30 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ โ 2 โ
โ+) |
32 | 31 | rpne0d 12967 |
. . . . . . 7
โข (๐ โ โ โ 2 โ
0) |
33 | 28, 29, 32 | divrec2d 11940 |
. . . . . 6
โข (๐ โ โ โ
((logโ((๐ + 1) /
๐)) / 2) = ((1 / 2)
ยท (logโ((๐ +
1) / ๐)))) |
34 | 33 | oveq1d 7373 |
. . . . 5
โข (๐ โ โ โ
(((logโ((๐ + 1) /
๐)) / 2) + (๐ ยท (logโ((๐ + 1) / ๐)))) = (((1 / 2) ยท (logโ((๐ + 1) / ๐))) + (๐ ยท (logโ((๐ + 1) / ๐))))) |
35 | | 1cnd 11155 |
. . . . . . . 8
โข (๐ โ โ โ 1 โ
โ) |
36 | 35 | halfcld 12403 |
. . . . . . 7
โข (๐ โ โ โ (1 / 2)
โ โ) |
37 | 36, 23, 28 | adddird 11185 |
. . . . . 6
โข (๐ โ โ โ (((1 / 2)
+ ๐) ยท
(logโ((๐ + 1) / ๐))) = (((1 / 2) ยท
(logโ((๐ + 1) / ๐))) + (๐ ยท (logโ((๐ + 1) / ๐))))) |
38 | 23, 29, 32 | divcan4d 11942 |
. . . . . . . . . 10
โข (๐ โ โ โ ((๐ ยท 2) / 2) = ๐) |
39 | 23, 29 | mulcomd 11181 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ ยท 2) = (2 ยท ๐)) |
40 | 39 | oveq1d 7373 |
. . . . . . . . . 10
โข (๐ โ โ โ ((๐ ยท 2) / 2) = ((2 ยท
๐) / 2)) |
41 | 38, 40 | eqtr3d 2775 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ = ((2 ยท ๐) / 2)) |
42 | 41 | oveq2d 7374 |
. . . . . . . 8
โข (๐ โ โ โ ((1 / 2)
+ ๐) = ((1 / 2) + ((2
ยท ๐) /
2))) |
43 | 29, 23 | mulcld 11180 |
. . . . . . . . 9
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
44 | 35, 43, 29, 32 | divdird 11974 |
. . . . . . . 8
โข (๐ โ โ โ ((1 + (2
ยท ๐)) / 2) = ((1 /
2) + ((2 ยท ๐) /
2))) |
45 | 42, 44 | eqtr4d 2776 |
. . . . . . 7
โข (๐ โ โ โ ((1 / 2)
+ ๐) = ((1 + (2 ยท
๐)) / 2)) |
46 | 45 | oveq1d 7373 |
. . . . . 6
โข (๐ โ โ โ (((1 / 2)
+ ๐) ยท
(logโ((๐ + 1) / ๐))) = (((1 + (2 ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐)))) |
47 | 37, 46 | eqtr3d 2775 |
. . . . 5
โข (๐ โ โ โ (((1 / 2)
ยท (logโ((๐ +
1) / ๐))) + (๐ ยท (logโ((๐ + 1) / ๐)))) = (((1 + (2 ยท ๐)) / 2) ยท (logโ((๐ + 1) / ๐)))) |
48 | 20, 34, 47 | 3eqtrd 2777 |
. . . 4
โข (๐ โ โ โ
(logโ((โโ((๐ + 1) / ๐)) ยท (((๐ + 1) / ๐)โ๐))) = (((1 + (2 ยท ๐)) / 2) ยท (logโ((๐ + 1) / ๐)))) |
49 | | loge 25958 |
. . . . 5
โข
(logโe) = 1 |
50 | 49 | a1i 11 |
. . . 4
โข (๐ โ โ โ
(logโe) = 1) |
51 | 48, 50 | oveq12d 7376 |
. . 3
โข (๐ โ โ โ
((logโ((โโ((๐ + 1) / ๐)) ยท (((๐ + 1) / ๐)โ๐))) โ (logโe)) = ((((1 + (2
ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1)) |
52 | 13, 51 | eqtrd 2773 |
. 2
โข (๐ โ โ โ
(logโ(((โโ((๐ + 1) / ๐)) ยท (((๐ + 1) / ๐)โ๐)) / e)) = ((((1 + (2 ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1)) |
53 | | stirlinglem4.1 |
. . . . . . 7
โข ๐ด = (๐ โ โ โฆ ((!โ๐) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐)))) |
54 | 53 | stirlinglem2 44402 |
. . . . . 6
โข (๐ โ โ โ (๐ดโ๐) โ
โ+) |
55 | 54 | relogcld 25994 |
. . . . 5
โข (๐ โ โ โ
(logโ(๐ดโ๐)) โ
โ) |
56 | | nfcv 2904 |
. . . . . 6
โข
โฒ๐๐ |
57 | | nfcv 2904 |
. . . . . . 7
โข
โฒ๐log |
58 | | nfmpt1 5214 |
. . . . . . . . 9
โข
โฒ๐(๐ โ โ โฆ ((!โ๐) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐)))) |
59 | 53, 58 | nfcxfr 2902 |
. . . . . . . 8
โข
โฒ๐๐ด |
60 | 59, 56 | nffv 6853 |
. . . . . . 7
โข
โฒ๐(๐ดโ๐) |
61 | 57, 60 | nffv 6853 |
. . . . . 6
โข
โฒ๐(logโ(๐ดโ๐)) |
62 | | 2fveq3 6848 |
. . . . . 6
โข (๐ = ๐ โ (logโ(๐ดโ๐)) = (logโ(๐ดโ๐))) |
63 | | stirlinglem4.2 |
. . . . . 6
โข ๐ต = (๐ โ โ โฆ (logโ(๐ดโ๐))) |
64 | 56, 61, 62, 63 | fvmptf 6970 |
. . . . 5
โข ((๐ โ โ โง
(logโ(๐ดโ๐)) โ โ) โ (๐ตโ๐) = (logโ(๐ดโ๐))) |
65 | 55, 64 | mpdan 686 |
. . . 4
โข (๐ โ โ โ (๐ตโ๐) = (logโ(๐ดโ๐))) |
66 | | nfcv 2904 |
. . . . . . . 8
โข
โฒ๐(logโ(๐ดโ๐)) |
67 | | nfcv 2904 |
. . . . . . . . . 10
โข
โฒ๐๐ |
68 | 59, 67 | nffv 6853 |
. . . . . . . . 9
โข
โฒ๐(๐ดโ๐) |
69 | 57, 68 | nffv 6853 |
. . . . . . . 8
โข
โฒ๐(logโ(๐ดโ๐)) |
70 | | 2fveq3 6848 |
. . . . . . . 8
โข (๐ = ๐ โ (logโ(๐ดโ๐)) = (logโ(๐ดโ๐))) |
71 | 66, 69, 70 | cbvmpt 5217 |
. . . . . . 7
โข (๐ โ โ โฆ
(logโ(๐ดโ๐))) = (๐ โ โ โฆ (logโ(๐ดโ๐))) |
72 | 63, 71 | eqtri 2761 |
. . . . . 6
โข ๐ต = (๐ โ โ โฆ (logโ(๐ดโ๐))) |
73 | 72 | a1i 11 |
. . . . 5
โข (๐ โ โ โ ๐ต = (๐ โ โ โฆ (logโ(๐ดโ๐)))) |
74 | | simpr 486 |
. . . . . . 7
โข ((๐ โ โ โง ๐ = (๐ + 1)) โ ๐ = (๐ + 1)) |
75 | 74 | fveq2d 6847 |
. . . . . 6
โข ((๐ โ โ โง ๐ = (๐ + 1)) โ (๐ดโ๐) = (๐ดโ(๐ + 1))) |
76 | 75 | fveq2d 6847 |
. . . . 5
โข ((๐ โ โ โง ๐ = (๐ + 1)) โ (logโ(๐ดโ๐)) = (logโ(๐ดโ(๐ + 1)))) |
77 | 53 | stirlinglem2 44402 |
. . . . . . 7
โข ((๐ + 1) โ โ โ
(๐ดโ(๐ + 1)) โ
โ+) |
78 | 21, 77 | syl 17 |
. . . . . 6
โข (๐ โ โ โ (๐ดโ(๐ + 1)) โ
โ+) |
79 | 78 | relogcld 25994 |
. . . . 5
โข (๐ โ โ โ
(logโ(๐ดโ(๐ + 1))) โ
โ) |
80 | 73, 76, 21, 79 | fvmptd 6956 |
. . . 4
โข (๐ โ โ โ (๐ตโ(๐ + 1)) = (logโ(๐ดโ(๐ + 1)))) |
81 | 65, 80 | oveq12d 7376 |
. . 3
โข (๐ โ โ โ ((๐ตโ๐) โ (๐ตโ(๐ + 1))) = ((logโ(๐ดโ๐)) โ (logโ(๐ดโ(๐ + 1))))) |
82 | 54, 78 | relogdivd 25997 |
. . 3
โข (๐ โ โ โ
(logโ((๐ดโ๐) / (๐ดโ(๐ + 1)))) = ((logโ(๐ดโ๐)) โ (logโ(๐ดโ(๐ + 1))))) |
83 | | faccl 14189 |
. . . . . . . . 9
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
84 | | nnrp 12931 |
. . . . . . . . 9
โข
((!โ๐) โ
โ โ (!โ๐)
โ โ+) |
85 | 2, 83, 84 | 3syl 18 |
. . . . . . . 8
โข (๐ โ โ โ
(!โ๐) โ
โ+) |
86 | 31, 5 | rpmulcld 12978 |
. . . . . . . . . 10
โข (๐ โ โ โ (2
ยท ๐) โ
โ+) |
87 | 86 | rpsqrtcld 15302 |
. . . . . . . . 9
โข (๐ โ โ โ
(โโ(2 ยท ๐)) โ
โ+) |
88 | 5, 12 | rpdivcld 12979 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ / e) โ
โ+) |
89 | 88, 8 | rpexpcld 14156 |
. . . . . . . . 9
โข (๐ โ โ โ ((๐ / e)โ๐) โ
โ+) |
90 | 87, 89 | rpmulcld 12978 |
. . . . . . . 8
โข (๐ โ โ โ
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)) โ
โ+) |
91 | 85, 90 | rpdivcld 12979 |
. . . . . . 7
โข (๐ โ โ โ
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ
โ+) |
92 | 53 | a1i 11 |
. . . . . . . 8
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ ๐ด = (๐ โ โ โฆ ((!โ๐) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐))))) |
93 | | simpr 486 |
. . . . . . . . . 10
โข (((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โง ๐ = ๐) โ ๐ = ๐) |
94 | 93 | fveq2d 6847 |
. . . . . . . . 9
โข (((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โง ๐ = ๐) โ (!โ๐) = (!โ๐)) |
95 | 93 | oveq2d 7374 |
. . . . . . . . . . 11
โข (((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โง ๐ = ๐) โ (2 ยท ๐) = (2 ยท ๐)) |
96 | 95 | fveq2d 6847 |
. . . . . . . . . 10
โข (((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โง ๐ = ๐) โ (โโ(2 ยท ๐)) = (โโ(2 ยท
๐))) |
97 | 93 | oveq1d 7373 |
. . . . . . . . . . 11
โข (((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โง ๐ = ๐) โ (๐ / e) = (๐ / e)) |
98 | 97, 93 | oveq12d 7376 |
. . . . . . . . . 10
โข (((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โง ๐ = ๐) โ ((๐ / e)โ๐) = ((๐ / e)โ๐)) |
99 | 96, 98 | oveq12d 7376 |
. . . . . . . . 9
โข (((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โง ๐ = ๐) โ ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)) = ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) |
100 | 94, 99 | oveq12d 7376 |
. . . . . . . 8
โข (((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โง ๐ = ๐) โ ((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) = ((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))) |
101 | | simpl 484 |
. . . . . . . 8
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ ๐ โ
โ) |
102 | 85 | rpcnd 12964 |
. . . . . . . . . 10
โข (๐ โ โ โ
(!โ๐) โ
โ) |
103 | 102 | adantr 482 |
. . . . . . . . 9
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ
(!โ๐) โ
โ) |
104 | | 2cnd 12236 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ 2
โ โ) |
105 | 101 | nncnd 12174 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ ๐ โ
โ) |
106 | 104, 105 | mulcld 11180 |
. . . . . . . . . . 11
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ (2
ยท ๐) โ
โ) |
107 | 106 | sqrtcld 15328 |
. . . . . . . . . 10
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ
(โโ(2 ยท ๐)) โ โ) |
108 | | ere 15976 |
. . . . . . . . . . . . . 14
โข e โ
โ |
109 | 108 | recni 11174 |
. . . . . . . . . . . . 13
โข e โ
โ |
110 | 109 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ e
โ โ) |
111 | | 0re 11162 |
. . . . . . . . . . . . . 14
โข 0 โ
โ |
112 | | epos 16094 |
. . . . . . . . . . . . . 14
โข 0 <
e |
113 | 111, 112 | gtneii 11272 |
. . . . . . . . . . . . 13
โข e โ
0 |
114 | 113 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ e
โ 0) |
115 | 105, 110,
114 | divcld 11936 |
. . . . . . . . . . 11
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ
(๐ / e) โ
โ) |
116 | 101 | nnnn0d 12478 |
. . . . . . . . . . 11
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ ๐ โ
โ0) |
117 | 115, 116 | expcld 14057 |
. . . . . . . . . 10
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ
((๐ / e)โ๐) โ
โ) |
118 | 107, 117 | mulcld 11180 |
. . . . . . . . 9
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)) โ โ) |
119 | 87 | rpne0d 12967 |
. . . . . . . . . . 11
โข (๐ โ โ โ
(โโ(2 ยท ๐)) โ 0) |
120 | 119 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ
(โโ(2 ยท ๐)) โ 0) |
121 | 101 | nnne0d 12208 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ ๐ โ 0) |
122 | 105, 110,
121, 114 | divne0d 11952 |
. . . . . . . . . . 11
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ
(๐ / e) โ
0) |
123 | 101 | nnzd 12531 |
. . . . . . . . . . 11
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ ๐ โ
โค) |
124 | 115, 122,
123 | expne0d 14063 |
. . . . . . . . . 10
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ
((๐ / e)โ๐) โ 0) |
125 | 107, 117,
120, 124 | mulne0d 11812 |
. . . . . . . . 9
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)) โ 0) |
126 | 103, 118,
125 | divcld 11936 |
. . . . . . . 8
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ) |
127 | 92, 100, 101, 126 | fvmptd 6956 |
. . . . . . 7
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ+) โ
(๐ดโ๐) = ((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))) |
128 | 91, 127 | mpdan 686 |
. . . . . 6
โข (๐ โ โ โ (๐ดโ๐) = ((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))) |
129 | | nfcv 2904 |
. . . . . . . . . 10
โข
โฒ๐((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) |
130 | | nfcv 2904 |
. . . . . . . . . 10
โข
โฒ๐((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) |
131 | | fveq2 6843 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (!โ๐) = (!โ๐)) |
132 | | oveq2 7366 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (2 ยท ๐) = (2 ยท ๐)) |
133 | 132 | fveq2d 6847 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (โโ(2 ยท ๐)) = (โโ(2 ยท
๐))) |
134 | | oveq1 7365 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ / e) = (๐ / e)) |
135 | | id 22 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ ๐ = ๐) |
136 | 134, 135 | oveq12d 7376 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((๐ / e)โ๐) = ((๐ / e)โ๐)) |
137 | 133, 136 | oveq12d 7376 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)) = ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) |
138 | 131, 137 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) = ((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))) |
139 | 129, 130,
138 | cbvmpt 5217 |
. . . . . . . . 9
โข (๐ โ โ โฆ
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))) = (๐ โ โ โฆ ((!โ๐) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐)))) |
140 | 53, 139 | eqtri 2761 |
. . . . . . . 8
โข ๐ด = (๐ โ โ โฆ ((!โ๐) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐)))) |
141 | 140 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ ๐ด = (๐ โ โ โฆ ((!โ๐) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐))))) |
142 | 74 | fveq2d 6847 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ = (๐ + 1)) โ (!โ๐) = (!โ(๐ + 1))) |
143 | 74 | oveq2d 7374 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ = (๐ + 1)) โ (2 ยท ๐) = (2 ยท (๐ + 1))) |
144 | 143 | fveq2d 6847 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ = (๐ + 1)) โ (โโ(2 ยท
๐)) = (โโ(2
ยท (๐ +
1)))) |
145 | 74 | oveq1d 7373 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ = (๐ + 1)) โ (๐ / e) = ((๐ + 1) / e)) |
146 | 145, 74 | oveq12d 7376 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ = (๐ + 1)) โ ((๐ / e)โ๐) = (((๐ + 1) / e)โ(๐ + 1))) |
147 | 144, 146 | oveq12d 7376 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ = (๐ + 1)) โ ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐)) = ((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1)))) |
148 | 142, 147 | oveq12d 7376 |
. . . . . . 7
โข ((๐ โ โ โง ๐ = (๐ + 1)) โ ((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) = ((!โ(๐ + 1)) / ((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))))) |
149 | 21 | nnnn0d 12478 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ + 1) โ
โ0) |
150 | | faccl 14189 |
. . . . . . . . 9
โข ((๐ + 1) โ โ0
โ (!โ(๐ + 1))
โ โ) |
151 | | nnrp 12931 |
. . . . . . . . 9
โข
((!โ(๐ + 1))
โ โ โ (!โ(๐ + 1)) โ
โ+) |
152 | 149, 150,
151 | 3syl 18 |
. . . . . . . 8
โข (๐ โ โ โ
(!โ(๐ + 1)) โ
โ+) |
153 | 31, 4 | rpmulcld 12978 |
. . . . . . . . . 10
โข (๐ โ โ โ (2
ยท (๐ + 1)) โ
โ+) |
154 | 153 | rpsqrtcld 15302 |
. . . . . . . . 9
โข (๐ โ โ โ
(โโ(2 ยท (๐ + 1))) โ
โ+) |
155 | 4, 12 | rpdivcld 12979 |
. . . . . . . . . 10
โข (๐ โ โ โ ((๐ + 1) / e) โ
โ+) |
156 | 8 | peano2zd 12615 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ + 1) โ
โค) |
157 | 155, 156 | rpexpcld 14156 |
. . . . . . . . 9
โข (๐ โ โ โ (((๐ + 1) / e)โ(๐ + 1)) โ
โ+) |
158 | 154, 157 | rpmulcld 12978 |
. . . . . . . 8
โข (๐ โ โ โ
((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))) โ
โ+) |
159 | 152, 158 | rpdivcld 12979 |
. . . . . . 7
โข (๐ โ โ โ
((!โ(๐ + 1)) /
((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1)))) โ
โ+) |
160 | 141, 148,
21, 159 | fvmptd 6956 |
. . . . . 6
โข (๐ โ โ โ (๐ดโ(๐ + 1)) = ((!โ(๐ + 1)) / ((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))))) |
161 | 128, 160 | oveq12d 7376 |
. . . . 5
โข (๐ โ โ โ ((๐ดโ๐) / (๐ดโ(๐ + 1))) = (((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) / ((!โ(๐ + 1)) / ((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1)))))) |
162 | | facp1 14184 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (!โ(๐ + 1)) =
((!โ๐) ยท
(๐ + 1))) |
163 | 2, 162 | syl 17 |
. . . . . . . . 9
โข (๐ โ โ โ
(!โ(๐ + 1)) =
((!โ๐) ยท
(๐ + 1))) |
164 | 163 | oveq1d 7373 |
. . . . . . . 8
โข (๐ โ โ โ
((!โ(๐ + 1)) /
((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1)))) = (((!โ๐) ยท (๐ + 1)) / ((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))))) |
165 | 158 | rpcnd 12964 |
. . . . . . . . 9
โข (๐ โ โ โ
((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))) โ โ) |
166 | 158 | rpne0d 12967 |
. . . . . . . . 9
โข (๐ โ โ โ
((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))) โ 0) |
167 | 102, 22, 165, 166 | divassd 11971 |
. . . . . . . 8
โข (๐ โ โ โ
(((!โ๐) ยท
(๐ + 1)) /
((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1)))) = ((!โ๐) ยท ((๐ + 1) / ((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1)))))) |
168 | 164, 167 | eqtrd 2773 |
. . . . . . 7
โข (๐ โ โ โ
((!โ(๐ + 1)) /
((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1)))) = ((!โ๐) ยท ((๐ + 1) / ((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1)))))) |
169 | 168 | oveq2d 7374 |
. . . . . 6
โข (๐ โ โ โ
(((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) / ((!โ(๐ + 1)) / ((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))))) = (((!โ๐) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐))) / ((!โ๐) ยท ((๐ + 1) / ((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))))))) |
170 | 90 | rpcnd 12964 |
. . . . . . 7
โข (๐ โ โ โ
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)) โ โ) |
171 | 22, 165, 166 | divcld 11936 |
. . . . . . . 8
โข (๐ โ โ โ ((๐ + 1) / ((โโ(2
ยท (๐ + 1))) ยท
(((๐ + 1) / e)โ(๐ + 1)))) โ
โ) |
172 | 102, 171 | mulcld 11180 |
. . . . . . 7
โข (๐ โ โ โ
((!โ๐) ยท
((๐ + 1) /
((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))))) โ โ) |
173 | 90 | rpne0d 12967 |
. . . . . . 7
โข (๐ โ โ โ
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)) โ 0) |
174 | 85 | rpne0d 12967 |
. . . . . . . 8
โข (๐ โ โ โ
(!โ๐) โ
0) |
175 | 22, 165, 26, 166 | divne0d 11952 |
. . . . . . . 8
โข (๐ โ โ โ ((๐ + 1) / ((โโ(2
ยท (๐ + 1))) ยท
(((๐ + 1) / e)โ(๐ + 1)))) โ
0) |
176 | 102, 171,
174, 175 | mulne0d 11812 |
. . . . . . 7
โข (๐ โ โ โ
((!โ๐) ยท
((๐ + 1) /
((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))))) โ 0) |
177 | 102, 170,
172, 173, 176 | divdiv32d 11961 |
. . . . . 6
โข (๐ โ โ โ
(((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) / ((!โ๐) ยท ((๐ + 1) / ((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1)))))) = (((!โ๐) / ((!โ๐) ยท ((๐ + 1) / ((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1)))))) / ((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐)))) |
178 | 102, 102,
171, 174, 175 | divdiv1d 11967 |
. . . . . . . . 9
โข (๐ โ โ โ
(((!โ๐) /
(!โ๐)) / ((๐ + 1) / ((โโ(2
ยท (๐ + 1))) ยท
(((๐ + 1) / e)โ(๐ + 1))))) = ((!โ๐) / ((!โ๐) ยท ((๐ + 1) / ((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))))))) |
179 | 178 | eqcomd 2739 |
. . . . . . . 8
โข (๐ โ โ โ
((!โ๐) /
((!โ๐) ยท
((๐ + 1) /
((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1)))))) = (((!โ๐) / (!โ๐)) / ((๐ + 1) / ((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1)))))) |
180 | 179 | oveq1d 7373 |
. . . . . . 7
โข (๐ โ โ โ
(((!โ๐) /
((!โ๐) ยท
((๐ + 1) /
((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1)))))) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐))) = ((((!โ๐) / (!โ๐)) / ((๐ + 1) / ((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))))) / ((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐)))) |
181 | 102, 174 | dividd 11934 |
. . . . . . . . 9
โข (๐ โ โ โ
((!โ๐) /
(!โ๐)) =
1) |
182 | 181 | oveq1d 7373 |
. . . . . . . 8
โข (๐ โ โ โ
(((!โ๐) /
(!โ๐)) / ((๐ + 1) / ((โโ(2
ยท (๐ + 1))) ยท
(((๐ + 1) / e)โ(๐ + 1))))) = (1 / ((๐ + 1) / ((โโ(2
ยท (๐ + 1))) ยท
(((๐ + 1) / e)โ(๐ + 1)))))) |
183 | 182 | oveq1d 7373 |
. . . . . . 7
โข (๐ โ โ โ
((((!โ๐) /
(!โ๐)) / ((๐ + 1) / ((โโ(2
ยท (๐ + 1))) ยท
(((๐ + 1) / e)โ(๐ + 1))))) / ((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐))) = ((1 / ((๐ + 1) / ((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))))) / ((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐)))) |
184 | 22, 165, 26, 166 | recdivd 11953 |
. . . . . . . . 9
โข (๐ โ โ โ (1 /
((๐ + 1) /
((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))))) = (((โโ(2 ยท
(๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))) / (๐ + 1))) |
185 | 184 | oveq1d 7373 |
. . . . . . . 8
โข (๐ โ โ โ ((1 /
((๐ + 1) /
((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))))) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐))) = ((((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))) / (๐ + 1)) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))) |
186 | 165, 22, 26 | divcld 11936 |
. . . . . . . . . 10
โข (๐ โ โ โ
(((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))) / (๐ + 1)) โ โ) |
187 | 87 | rpcnd 12964 |
. . . . . . . . . 10
โข (๐ โ โ โ
(โโ(2 ยท ๐)) โ โ) |
188 | 89 | rpcnd 12964 |
. . . . . . . . . 10
โข (๐ โ โ โ ((๐ / e)โ๐) โ โ) |
189 | 89 | rpne0d 12967 |
. . . . . . . . . 10
โข (๐ โ โ โ ((๐ / e)โ๐) โ 0) |
190 | 186, 187,
188, 119, 189 | divdiv1d 11967 |
. . . . . . . . 9
โข (๐ โ โ โ
(((((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))) / (๐ + 1)) / (โโ(2 ยท ๐))) / ((๐ / e)โ๐)) = ((((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))) / (๐ + 1)) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))) |
191 | 165, 22, 187, 26, 119 | divdiv32d 11961 |
. . . . . . . . . . 11
โข (๐ โ โ โ
((((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))) / (๐ + 1)) / (โโ(2 ยท ๐))) = ((((โโ(2
ยท (๐ + 1))) ยท
(((๐ + 1) / e)โ(๐ + 1))) / (โโ(2
ยท ๐))) / (๐ + 1))) |
192 | 154 | rpcnd 12964 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ
(โโ(2 ยท (๐ + 1))) โ โ) |
193 | 157 | rpcnd 12964 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (((๐ + 1) / e)โ(๐ + 1)) โ
โ) |
194 | 192, 193,
187, 119 | div23d 11973 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
(((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))) / (โโ(2 ยท ๐))) = (((โโ(2
ยท (๐ + 1))) /
(โโ(2 ยท ๐))) ยท (((๐ + 1) / e)โ(๐ + 1)))) |
195 | 31 | rpred 12962 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ 2 โ
โ) |
196 | 31 | rpge0d 12966 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ 0 โค
2) |
197 | 21 | nnred 12173 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ (๐ + 1) โ
โ) |
198 | 149 | nn0ge0d 12481 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ 0 โค
(๐ + 1)) |
199 | 195, 196,
197, 198 | sqrtmuld 15315 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ
(โโ(2 ยท (๐ + 1))) = ((โโ2) ยท
(โโ(๐ +
1)))) |
200 | 195, 196,
1, 3 | sqrtmuld 15315 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ
(โโ(2 ยท ๐)) = ((โโ2) ยท
(โโ๐))) |
201 | 199, 200 | oveq12d 7376 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ
((โโ(2 ยท (๐ + 1))) / (โโ(2 ยท ๐))) = (((โโ2)
ยท (โโ(๐
+ 1))) / ((โโ2) ยท (โโ๐)))) |
202 | 29 | sqrtcld 15328 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ
(โโ2) โ โ) |
203 | 22 | sqrtcld 15328 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ
(โโ(๐ + 1))
โ โ) |
204 | 23 | sqrtcld 15328 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ
(โโ๐) โ
โ) |
205 | 31 | rpsqrtcld 15302 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ
(โโ2) โ โ+) |
206 | 205 | rpne0d 12967 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ
(โโ2) โ 0) |
207 | 5 | rpsqrtcld 15302 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ
(โโ๐) โ
โ+) |
208 | 207 | rpne0d 12967 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ
(โโ๐) โ
0) |
209 | 202, 202,
203, 204, 206, 208 | divmuldivd 11977 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ
(((โโ2) / (โโ2)) ยท ((โโ(๐ + 1)) / (โโ๐))) = (((โโ2)
ยท (โโ(๐
+ 1))) / ((โโ2) ยท (โโ๐)))) |
210 | 202, 206 | dividd 11934 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ
((โโ2) / (โโ2)) = 1) |
211 | 197, 198,
5 | sqrtdivd 15314 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ
(โโ((๐ + 1) /
๐)) =
((โโ(๐ + 1)) /
(โโ๐))) |
212 | 211 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ
((โโ(๐ + 1)) /
(โโ๐)) =
(โโ((๐ + 1) /
๐))) |
213 | 210, 212 | oveq12d 7376 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ
(((โโ2) / (โโ2)) ยท ((โโ(๐ + 1)) / (โโ๐))) = (1 ยท
(โโ((๐ + 1) /
๐)))) |
214 | 201, 209,
213 | 3eqtr2d 2779 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ
((โโ(2 ยท (๐ + 1))) / (โโ(2 ยท ๐))) = (1 ยท
(โโ((๐ + 1) /
๐)))) |
215 | 214 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
(((โโ(2 ยท (๐ + 1))) / (โโ(2 ยท ๐))) ยท (((๐ + 1) / e)โ(๐ + 1))) = ((1 ยท
(โโ((๐ + 1) /
๐))) ยท (((๐ + 1) / e)โ(๐ + 1)))) |
216 | 25 | sqrtcld 15328 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ
(โโ((๐ + 1) /
๐)) โ
โ) |
217 | 216 | mulid2d 11178 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (1
ยท (โโ((๐
+ 1) / ๐))) =
(โโ((๐ + 1) /
๐))) |
218 | 217 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((1
ยท (โโ((๐
+ 1) / ๐))) ยท
(((๐ + 1) / e)โ(๐ + 1))) =
((โโ((๐ + 1) /
๐)) ยท (((๐ + 1) / e)โ(๐ + 1)))) |
219 | 194, 215,
218 | 3eqtrd 2777 |
. . . . . . . . . . . 12
โข (๐ โ โ โ
(((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))) / (โโ(2 ยท ๐))) = ((โโ((๐ + 1) / ๐)) ยท (((๐ + 1) / e)โ(๐ + 1)))) |
220 | 219 | oveq1d 7373 |
. . . . . . . . . . 11
โข (๐ โ โ โ
((((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))) / (โโ(2 ยท ๐))) / (๐ + 1)) = (((โโ((๐ + 1) / ๐)) ยท (((๐ + 1) / e)โ(๐ + 1))) / (๐ + 1))) |
221 | 191, 220 | eqtrd 2773 |
. . . . . . . . . 10
โข (๐ โ โ โ
((((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))) / (๐ + 1)) / (โโ(2 ยท ๐))) = (((โโ((๐ + 1) / ๐)) ยท (((๐ + 1) / e)โ(๐ + 1))) / (๐ + 1))) |
222 | 221 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ โ โ โ
(((((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))) / (๐ + 1)) / (โโ(2 ยท ๐))) / ((๐ / e)โ๐)) = ((((โโ((๐ + 1) / ๐)) ยท (((๐ + 1) / e)โ(๐ + 1))) / (๐ + 1)) / ((๐ / e)โ๐))) |
223 | 190, 222 | eqtr3d 2775 |
. . . . . . . 8
โข (๐ โ โ โ
((((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))) / (๐ + 1)) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) = ((((โโ((๐ + 1) / ๐)) ยท (((๐ + 1) / e)โ(๐ + 1))) / (๐ + 1)) / ((๐ / e)โ๐))) |
224 | 216, 193 | mulcld 11180 |
. . . . . . . . . 10
โข (๐ โ โ โ
((โโ((๐ + 1) /
๐)) ยท (((๐ + 1) / e)โ(๐ + 1))) โ
โ) |
225 | 224, 22, 188, 26, 189 | divdiv32d 11961 |
. . . . . . . . 9
โข (๐ โ โ โ
((((โโ((๐ + 1)
/ ๐)) ยท (((๐ + 1) / e)โ(๐ + 1))) / (๐ + 1)) / ((๐ / e)โ๐)) = ((((โโ((๐ + 1) / ๐)) ยท (((๐ + 1) / e)โ(๐ + 1))) / ((๐ / e)โ๐)) / (๐ + 1))) |
226 | 216, 193,
188, 189 | divassd 11971 |
. . . . . . . . . . 11
โข (๐ โ โ โ
(((โโ((๐ + 1) /
๐)) ยท (((๐ + 1) / e)โ(๐ + 1))) / ((๐ / e)โ๐)) = ((โโ((๐ + 1) / ๐)) ยท ((((๐ + 1) / e)โ(๐ + 1)) / ((๐ / e)โ๐)))) |
227 | 12 | rpcnd 12964 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ e โ
โ) |
228 | 12 | rpne0d 12967 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ e โ
0) |
229 | 22, 227, 228, 149 | expdivd 14071 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (((๐ + 1) / e)โ(๐ + 1)) = (((๐ + 1)โ(๐ + 1)) / (eโ(๐ + 1)))) |
230 | 23, 227, 228, 2 | expdivd 14071 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((๐ / e)โ๐) = ((๐โ๐) / (eโ๐))) |
231 | 229, 230 | oveq12d 7376 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((((๐ + 1) / e)โ(๐ + 1)) / ((๐ / e)โ๐)) = ((((๐ + 1)โ(๐ + 1)) / (eโ(๐ + 1))) / ((๐โ๐) / (eโ๐)))) |
232 | 231 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ โ โ โ
((โโ((๐ + 1) /
๐)) ยท ((((๐ + 1) / e)โ(๐ + 1)) / ((๐ / e)โ๐))) = ((โโ((๐ + 1) / ๐)) ยท ((((๐ + 1)โ(๐ + 1)) / (eโ(๐ + 1))) / ((๐โ๐) / (eโ๐))))) |
233 | 22, 149 | expcld 14057 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ((๐ + 1)โ(๐ + 1)) โ โ) |
234 | 227, 149 | expcld 14057 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ
(eโ(๐ + 1)) โ
โ) |
235 | 23, 2 | expcld 14057 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (๐โ๐) โ โ) |
236 | 227, 2 | expcld 14057 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ
(eโ๐) โ
โ) |
237 | 227, 228,
156 | expne0d 14063 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ
(eโ(๐ + 1)) โ
0) |
238 | 227, 228,
8 | expne0d 14063 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ
(eโ๐) โ
0) |
239 | 23, 24, 8 | expne0d 14063 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (๐โ๐) โ 0) |
240 | 233, 234,
235, 236, 237, 238, 239 | divdivdivd 11983 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((((๐ + 1)โ(๐ + 1)) / (eโ(๐ + 1))) / ((๐โ๐) / (eโ๐))) = ((((๐ + 1)โ(๐ + 1)) ยท (eโ๐)) / ((eโ(๐ + 1)) ยท (๐โ๐)))) |
241 | 233, 236 | mulcomd 11181 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (((๐ + 1)โ(๐ + 1)) ยท (eโ๐)) = ((eโ๐) ยท ((๐ + 1)โ(๐ + 1)))) |
242 | 241 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((((๐ + 1)โ(๐ + 1)) ยท (eโ๐)) / ((eโ(๐ + 1)) ยท (๐โ๐))) = (((eโ๐) ยท ((๐ + 1)โ(๐ + 1))) / ((eโ(๐ + 1)) ยท (๐โ๐)))) |
243 | 236, 234,
233, 235, 237, 239 | divmuldivd 11977 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ
(((eโ๐) /
(eโ(๐ + 1))) ยท
(((๐ + 1)โ(๐ + 1)) / (๐โ๐))) = (((eโ๐) ยท ((๐ + 1)โ(๐ + 1))) / ((eโ(๐ + 1)) ยท (๐โ๐)))) |
244 | 227, 2 | expp1d 14058 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ
(eโ(๐ + 1)) =
((eโ๐) ยท
e)) |
245 | 244 | oveq2d 7374 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ
((eโ๐) /
(eโ(๐ + 1))) =
((eโ๐) /
((eโ๐) ยท
e))) |
246 | 236, 236,
227, 238, 228 | divdiv1d 11967 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ
(((eโ๐) /
(eโ๐)) / e) =
((eโ๐) /
((eโ๐) ยท
e))) |
247 | 236, 238 | dividd 11934 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ
((eโ๐) / (eโ๐)) = 1) |
248 | 247 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ
(((eโ๐) /
(eโ๐)) / e) = (1 /
e)) |
249 | 245, 246,
248 | 3eqtr2d 2779 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ
((eโ๐) /
(eโ(๐ + 1))) = (1 /
e)) |
250 | 249 | oveq1d 7373 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ
(((eโ๐) /
(eโ(๐ + 1))) ยท
(((๐ + 1)โ(๐ + 1)) / (๐โ๐))) = ((1 / e) ยท (((๐ + 1)โ(๐ + 1)) / (๐โ๐)))) |
251 | 243, 250 | eqtr3d 2775 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
(((eโ๐) ยท
((๐ + 1)โ(๐ + 1))) / ((eโ(๐ + 1)) ยท (๐โ๐))) = ((1 / e) ยท (((๐ + 1)โ(๐ + 1)) / (๐โ๐)))) |
252 | 240, 242,
251 | 3eqtrd 2777 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((((๐ + 1)โ(๐ + 1)) / (eโ(๐ + 1))) / ((๐โ๐) / (eโ๐))) = ((1 / e) ยท (((๐ + 1)โ(๐ + 1)) / (๐โ๐)))) |
253 | 252 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ โ โ โ
((โโ((๐ + 1) /
๐)) ยท ((((๐ + 1)โ(๐ + 1)) / (eโ(๐ + 1))) / ((๐โ๐) / (eโ๐)))) = ((โโ((๐ + 1) / ๐)) ยท ((1 / e) ยท (((๐ + 1)โ(๐ + 1)) / (๐โ๐))))) |
254 | 226, 232,
253 | 3eqtrd 2777 |
. . . . . . . . . 10
โข (๐ โ โ โ
(((โโ((๐ + 1) /
๐)) ยท (((๐ + 1) / e)โ(๐ + 1))) / ((๐ / e)โ๐)) = ((โโ((๐ + 1) / ๐)) ยท ((1 / e) ยท (((๐ + 1)โ(๐ + 1)) / (๐โ๐))))) |
255 | 254 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ โ โ โ
((((โโ((๐ + 1)
/ ๐)) ยท (((๐ + 1) / e)โ(๐ + 1))) / ((๐ / e)โ๐)) / (๐ + 1)) = (((โโ((๐ + 1) / ๐)) ยท ((1 / e) ยท (((๐ + 1)โ(๐ + 1)) / (๐โ๐)))) / (๐ + 1))) |
256 | 233, 235,
239 | divcld 11936 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (((๐ + 1)โ(๐ + 1)) / (๐โ๐)) โ โ) |
257 | 35, 227, 256, 228 | div32d 11959 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((1 / e)
ยท (((๐ +
1)โ(๐ + 1)) / (๐โ๐))) = (1 ยท ((((๐ + 1)โ(๐ + 1)) / (๐โ๐)) / e))) |
258 | 256, 227,
228 | divcld 11936 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((((๐ + 1)โ(๐ + 1)) / (๐โ๐)) / e) โ โ) |
259 | 258 | mulid2d 11178 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (1
ยท ((((๐ +
1)โ(๐ + 1)) / (๐โ๐)) / e)) = ((((๐ + 1)โ(๐ + 1)) / (๐โ๐)) / e)) |
260 | 257, 259 | eqtrd 2773 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((1 / e)
ยท (((๐ +
1)โ(๐ + 1)) / (๐โ๐))) = ((((๐ + 1)โ(๐ + 1)) / (๐โ๐)) / e)) |
261 | 260 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ โ โ โ
(((โโ((๐ + 1) /
๐)) / (๐ + 1)) ยท ((1 / e) ยท (((๐ + 1)โ(๐ + 1)) / (๐โ๐)))) = (((โโ((๐ + 1) / ๐)) / (๐ + 1)) ยท ((((๐ + 1)โ(๐ + 1)) / (๐โ๐)) / e))) |
262 | 227, 228 | reccld 11929 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (1 / e)
โ โ) |
263 | 262, 256 | mulcld 11180 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((1 / e)
ยท (((๐ +
1)โ(๐ + 1)) / (๐โ๐))) โ โ) |
264 | 216, 263,
22, 26 | div23d 11973 |
. . . . . . . . . 10
โข (๐ โ โ โ
(((โโ((๐ + 1) /
๐)) ยท ((1 / e)
ยท (((๐ +
1)โ(๐ + 1)) / (๐โ๐)))) / (๐ + 1)) = (((โโ((๐ + 1) / ๐)) / (๐ + 1)) ยท ((1 / e) ยท (((๐ + 1)โ(๐ + 1)) / (๐โ๐))))) |
265 | 216, 22, 26 | divcld 11936 |
. . . . . . . . . . 11
โข (๐ โ โ โ
((โโ((๐ + 1) /
๐)) / (๐ + 1)) โ โ) |
266 | 265, 256,
227, 228 | divassd 11971 |
. . . . . . . . . 10
โข (๐ โ โ โ
((((โโ((๐ + 1)
/ ๐)) / (๐ + 1)) ยท (((๐ + 1)โ(๐ + 1)) / (๐โ๐))) / e) = (((โโ((๐ + 1) / ๐)) / (๐ + 1)) ยท ((((๐ + 1)โ(๐ + 1)) / (๐โ๐)) / e))) |
267 | 261, 264,
266 | 3eqtr4d 2783 |
. . . . . . . . 9
โข (๐ โ โ โ
(((โโ((๐ + 1) /
๐)) ยท ((1 / e)
ยท (((๐ +
1)โ(๐ + 1)) / (๐โ๐)))) / (๐ + 1)) = ((((โโ((๐ + 1) / ๐)) / (๐ + 1)) ยท (((๐ + 1)โ(๐ + 1)) / (๐โ๐))) / e)) |
268 | 225, 255,
267 | 3eqtrd 2777 |
. . . . . . . 8
โข (๐ โ โ โ
((((โโ((๐ + 1)
/ ๐)) ยท (((๐ + 1) / e)โ(๐ + 1))) / (๐ + 1)) / ((๐ / e)โ๐)) = ((((โโ((๐ + 1) / ๐)) / (๐ + 1)) ยท (((๐ + 1)โ(๐ + 1)) / (๐โ๐))) / e)) |
269 | 185, 223,
268 | 3eqtrd 2777 |
. . . . . . 7
โข (๐ โ โ โ ((1 /
((๐ + 1) /
((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))))) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐))) = ((((โโ((๐ + 1) / ๐)) / (๐ + 1)) ยท (((๐ + 1)โ(๐ + 1)) / (๐โ๐))) / e)) |
270 | 180, 183,
269 | 3eqtrd 2777 |
. . . . . 6
โข (๐ โ โ โ
(((!โ๐) /
((!โ๐) ยท
((๐ + 1) /
((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1)))))) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐))) = ((((โโ((๐ + 1) / ๐)) / (๐ + 1)) ยท (((๐ + 1)โ(๐ + 1)) / (๐โ๐))) / e)) |
271 | 169, 177,
270 | 3eqtrd 2777 |
. . . . 5
โข (๐ โ โ โ
(((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) / ((!โ(๐ + 1)) / ((โโ(2 ยท (๐ + 1))) ยท (((๐ + 1) / e)โ(๐ + 1))))) =
((((โโ((๐ + 1)
/ ๐)) / (๐ + 1)) ยท (((๐ + 1)โ(๐ + 1)) / (๐โ๐))) / e)) |
272 | 216, 22, 256, 26 | div32d 11959 |
. . . . . . 7
โข (๐ โ โ โ
(((โโ((๐ + 1) /
๐)) / (๐ + 1)) ยท (((๐ + 1)โ(๐ + 1)) / (๐โ๐))) = ((โโ((๐ + 1) / ๐)) ยท ((((๐ + 1)โ(๐ + 1)) / (๐โ๐)) / (๐ + 1)))) |
273 | 22, 2 | expp1d 14058 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((๐ + 1)โ(๐ + 1)) = (((๐ + 1)โ๐) ยท (๐ + 1))) |
274 | 273 | oveq1d 7373 |
. . . . . . . . . . 11
โข (๐ โ โ โ (((๐ + 1)โ(๐ + 1)) / (๐ + 1)) = ((((๐ + 1)โ๐) ยท (๐ + 1)) / (๐ + 1))) |
275 | 22, 2 | expcld 14057 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((๐ + 1)โ๐) โ โ) |
276 | 275, 22, 26 | divcan4d 11942 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((((๐ + 1)โ๐) ยท (๐ + 1)) / (๐ + 1)) = ((๐ + 1)โ๐)) |
277 | 274, 276 | eqtrd 2773 |
. . . . . . . . . 10
โข (๐ โ โ โ (((๐ + 1)โ(๐ + 1)) / (๐ + 1)) = ((๐ + 1)โ๐)) |
278 | 277 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ โ โ โ ((((๐ + 1)โ(๐ + 1)) / (๐ + 1)) / (๐โ๐)) = (((๐ + 1)โ๐) / (๐โ๐))) |
279 | 233, 235,
22, 239, 26 | divdiv32d 11961 |
. . . . . . . . 9
โข (๐ โ โ โ ((((๐ + 1)โ(๐ + 1)) / (๐โ๐)) / (๐ + 1)) = ((((๐ + 1)โ(๐ + 1)) / (๐ + 1)) / (๐โ๐))) |
280 | 22, 23, 24, 2 | expdivd 14071 |
. . . . . . . . 9
โข (๐ โ โ โ (((๐ + 1) / ๐)โ๐) = (((๐ + 1)โ๐) / (๐โ๐))) |
281 | 278, 279,
280 | 3eqtr4d 2783 |
. . . . . . . 8
โข (๐ โ โ โ ((((๐ + 1)โ(๐ + 1)) / (๐โ๐)) / (๐ + 1)) = (((๐ + 1) / ๐)โ๐)) |
282 | 281 | oveq2d 7374 |
. . . . . . 7
โข (๐ โ โ โ
((โโ((๐ + 1) /
๐)) ยท ((((๐ + 1)โ(๐ + 1)) / (๐โ๐)) / (๐ + 1))) = ((โโ((๐ + 1) / ๐)) ยท (((๐ + 1) / ๐)โ๐))) |
283 | 272, 282 | eqtrd 2773 |
. . . . . 6
โข (๐ โ โ โ
(((โโ((๐ + 1) /
๐)) / (๐ + 1)) ยท (((๐ + 1)โ(๐ + 1)) / (๐โ๐))) = ((โโ((๐ + 1) / ๐)) ยท (((๐ + 1) / ๐)โ๐))) |
284 | 283 | oveq1d 7373 |
. . . . 5
โข (๐ โ โ โ
((((โโ((๐ + 1)
/ ๐)) / (๐ + 1)) ยท (((๐ + 1)โ(๐ + 1)) / (๐โ๐))) / e) = (((โโ((๐ + 1) / ๐)) ยท (((๐ + 1) / ๐)โ๐)) / e)) |
285 | 161, 271,
284 | 3eqtrd 2777 |
. . . 4
โข (๐ โ โ โ ((๐ดโ๐) / (๐ดโ(๐ + 1))) = (((โโ((๐ + 1) / ๐)) ยท (((๐ + 1) / ๐)โ๐)) / e)) |
286 | 285 | fveq2d 6847 |
. . 3
โข (๐ โ โ โ
(logโ((๐ดโ๐) / (๐ดโ(๐ + 1)))) =
(logโ(((โโ((๐ + 1) / ๐)) ยท (((๐ + 1) / ๐)โ๐)) / e))) |
287 | 81, 82, 286 | 3eqtr2d 2779 |
. 2
โข (๐ โ โ โ ((๐ตโ๐) โ (๐ตโ(๐ + 1))) =
(logโ(((โโ((๐ + 1) / ๐)) ยท (((๐ + 1) / ๐)โ๐)) / e))) |
288 | 35, 43 | addcld 11179 |
. . . . . 6
โข (๐ โ โ โ (1 + (2
ยท ๐)) โ
โ) |
289 | 288 | halfcld 12403 |
. . . . 5
โข (๐ โ โ โ ((1 + (2
ยท ๐)) / 2) โ
โ) |
290 | 289, 28 | mulcld 11180 |
. . . 4
โข (๐ โ โ โ (((1 + (2
ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ
โ) |
291 | 290, 35 | subcld 11517 |
. . 3
โข (๐ โ โ โ ((((1 +
(2 ยท ๐)) / 2)
ยท (logโ((๐ +
1) / ๐))) โ 1) โ
โ) |
292 | | stirlinglem4.3 |
. . . . 5
โข ๐ฝ = (๐ โ โ โฆ ((((1 + (2 ยท
๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1)) |
293 | 292 | a1i 11 |
. . . 4
โข ((๐ โ โ โง ((((1 + (2
ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1) โ โ)
โ ๐ฝ = (๐ โ โ โฆ ((((1 +
(2 ยท ๐)) / 2)
ยท (logโ((๐ +
1) / ๐))) โ
1))) |
294 | | simpr 486 |
. . . . . . . . 9
โข (((๐ โ โ โง ((((1 + (2
ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1) โ โ)
โง ๐ = ๐) โ ๐ = ๐) |
295 | 294 | oveq2d 7374 |
. . . . . . . 8
โข (((๐ โ โ โง ((((1 + (2
ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1) โ โ)
โง ๐ = ๐) โ (2 ยท ๐) = (2 ยท ๐)) |
296 | 295 | oveq2d 7374 |
. . . . . . 7
โข (((๐ โ โ โง ((((1 + (2
ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1) โ โ)
โง ๐ = ๐) โ (1 + (2 ยท ๐)) = (1 + (2 ยท ๐))) |
297 | 296 | oveq1d 7373 |
. . . . . 6
โข (((๐ โ โ โง ((((1 + (2
ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1) โ โ)
โง ๐ = ๐) โ ((1 + (2 ยท ๐)) / 2) = ((1 + (2 ยท
๐)) / 2)) |
298 | 294 | oveq1d 7373 |
. . . . . . . 8
โข (((๐ โ โ โง ((((1 + (2
ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1) โ โ)
โง ๐ = ๐) โ (๐ + 1) = (๐ + 1)) |
299 | 298, 294 | oveq12d 7376 |
. . . . . . 7
โข (((๐ โ โ โง ((((1 + (2
ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1) โ โ)
โง ๐ = ๐) โ ((๐ + 1) / ๐) = ((๐ + 1) / ๐)) |
300 | 299 | fveq2d 6847 |
. . . . . 6
โข (((๐ โ โ โง ((((1 + (2
ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1) โ โ)
โง ๐ = ๐) โ (logโ((๐ + 1) / ๐)) = (logโ((๐ + 1) / ๐))) |
301 | 297, 300 | oveq12d 7376 |
. . . . 5
โข (((๐ โ โ โง ((((1 + (2
ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1) โ โ)
โง ๐ = ๐) โ (((1 + (2 ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) = (((1 + (2 ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐)))) |
302 | 301 | oveq1d 7373 |
. . . 4
โข (((๐ โ โ โง ((((1 + (2
ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1) โ โ)
โง ๐ = ๐) โ ((((1 + (2 ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1) = ((((1 + (2
ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1)) |
303 | | simpl 484 |
. . . 4
โข ((๐ โ โ โง ((((1 + (2
ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1) โ โ)
โ ๐ โ
โ) |
304 | | simpr 486 |
. . . 4
โข ((๐ โ โ โง ((((1 + (2
ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1) โ โ)
โ ((((1 + (2 ยท ๐)) / 2) ยท (logโ((๐ + 1) / ๐))) โ 1) โ
โ) |
305 | 293, 302,
303, 304 | fvmptd 6956 |
. . 3
โข ((๐ โ โ โง ((((1 + (2
ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1) โ โ)
โ (๐ฝโ๐) = ((((1 + (2 ยท ๐)) / 2) ยท
(logโ((๐ + 1) / ๐))) โ 1)) |
306 | 291, 305 | mpdan 686 |
. 2
โข (๐ โ โ โ (๐ฝโ๐) = ((((1 + (2 ยท ๐)) / 2) ยท (logโ((๐ + 1) / ๐))) โ 1)) |
307 | 52, 287, 306 | 3eqtr4d 2783 |
1
โข (๐ โ โ โ ((๐ตโ๐) โ (๐ตโ(๐ + 1))) = (๐ฝโ๐)) |