Step | Hyp | Ref
| Expression |
1 | | stirlinglem3.4 |
. 2
โข ๐ = (๐ โ โ โฆ ((((2โ(4
ยท ๐)) ยท
((!โ๐)โ4)) /
((!โ(2 ยท ๐))โ2)) / ((2 ยท ๐) + 1))) |
2 | | nnnn0 12427 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ0) |
3 | | faccl 14190 |
. . . . . . . . . . . . 13
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
4 | | nncn 12168 |
. . . . . . . . . . . . 13
โข
((!โ๐) โ
โ โ (!โ๐)
โ โ) |
5 | 2, 3, 4 | 3syl 18 |
. . . . . . . . . . . 12
โข (๐ โ โ โ
(!โ๐) โ
โ) |
6 | | 2cnd 12238 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ 2 โ
โ) |
7 | | nncn 12168 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ
โ) |
8 | 6, 7 | mulcld 11182 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
9 | 8 | sqrtcld 15329 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
(โโ(2 ยท ๐)) โ โ) |
10 | | ere 15978 |
. . . . . . . . . . . . . . . . 17
โข e โ
โ |
11 | 10 | recni 11176 |
. . . . . . . . . . . . . . . 16
โข e โ
โ |
12 | 11 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ e โ
โ) |
13 | | epos 16096 |
. . . . . . . . . . . . . . . . 17
โข 0 <
e |
14 | 10, 13 | gt0ne0ii 11698 |
. . . . . . . . . . . . . . . 16
โข e โ
0 |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ e โ
0) |
16 | 7, 12, 15 | divcld 11938 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (๐ / e) โ
โ) |
17 | 16, 2 | expcld 14058 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((๐ / e)โ๐) โ โ) |
18 | 9, 17 | mulcld 11182 |
. . . . . . . . . . . 12
โข (๐ โ โ โ
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)) โ โ) |
19 | | 2rp 12927 |
. . . . . . . . . . . . . . . . 17
โข 2 โ
โ+ |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ 2 โ
โ+) |
21 | | nnrp 12933 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ๐ โ
โ+) |
22 | 20, 21 | rpmulcld 12980 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (2
ยท ๐) โ
โ+) |
23 | 22 | sqrtgt0d 15304 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ 0 <
(โโ(2 ยท ๐))) |
24 | 23 | gt0ne0d 11726 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
(โโ(2 ยท ๐)) โ 0) |
25 | | nnne0 12194 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ 0) |
26 | 7, 12, 25, 15 | divne0d 11954 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (๐ / e) โ 0) |
27 | | nnz 12527 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โค) |
28 | 16, 26, 27 | expne0d 14064 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((๐ / e)โ๐) โ 0) |
29 | 9, 17, 24, 28 | mulne0d 11814 |
. . . . . . . . . . . 12
โข (๐ โ โ โ
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)) โ 0) |
30 | 5, 18, 29 | divcld 11938 |
. . . . . . . . . . 11
โข (๐ โ โ โ
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ) |
31 | | stirlinglem3.1 |
. . . . . . . . . . . 12
โข ๐ด = (๐ โ โ โฆ ((!โ๐) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐)))) |
32 | 31 | fvmpt2 6964 |
. . . . . . . . . . 11
โข ((๐ โ โ โง
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) โ โ) โ (๐ดโ๐) = ((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))) |
33 | 30, 32 | mpdan 686 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ดโ๐) = ((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))) |
34 | 33 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ โ โ โ ((๐ดโ๐)โ4) = (((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))โ4)) |
35 | | stirlinglem3.3 |
. . . . . . . . . . . 12
โข ๐ธ = (๐ โ โ โฆ ((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐))) |
36 | 35 | fvmpt2 6964 |
. . . . . . . . . . 11
โข ((๐ โ โ โง
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)) โ โ) โ (๐ธโ๐) = ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) |
37 | 18, 36 | mpdan 686 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ธโ๐) = ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) |
38 | 37 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ โ โ โ ((๐ธโ๐)โ4) = (((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐))โ4)) |
39 | 34, 38 | oveq12d 7380 |
. . . . . . . 8
โข (๐ โ โ โ (((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4)) = ((((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))โ4) ยท (((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐))โ4))) |
40 | | 4nn0 12439 |
. . . . . . . . . . 11
โข 4 โ
โ0 |
41 | 40 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โ โ 4 โ
โ0) |
42 | 5, 18, 29, 41 | expdivd 14072 |
. . . . . . . . 9
โข (๐ โ โ โ
(((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))โ4) = (((!โ๐)โ4) / (((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐))โ4))) |
43 | 42 | oveq1d 7377 |
. . . . . . . 8
โข (๐ โ โ โ
((((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))โ4) ยท (((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐))โ4)) = ((((!โ๐)โ4) / (((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐))โ4)) ยท
(((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))โ4))) |
44 | 5, 41 | expcld 14058 |
. . . . . . . . 9
โข (๐ โ โ โ
((!โ๐)โ4) โ
โ) |
45 | 18, 41 | expcld 14058 |
. . . . . . . . 9
โข (๐ โ โ โ
(((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))โ4) โ โ) |
46 | 41 | nn0zd 12532 |
. . . . . . . . . 10
โข (๐ โ โ โ 4 โ
โค) |
47 | 18, 29, 46 | expne0d 14064 |
. . . . . . . . 9
โข (๐ โ โ โ
(((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))โ4) โ 0) |
48 | 44, 45, 47 | divcan1d 11939 |
. . . . . . . 8
โข (๐ โ โ โ
((((!โ๐)โ4) /
(((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))โ4)) ยท (((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐))โ4)) = ((!โ๐)โ4)) |
49 | 39, 43, 48 | 3eqtrd 2781 |
. . . . . . 7
โข (๐ โ โ โ (((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4)) = ((!โ๐)โ4)) |
50 | 49 | eqcomd 2743 |
. . . . . 6
โข (๐ โ โ โ
((!โ๐)โ4) =
(((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4))) |
51 | 50 | oveq2d 7378 |
. . . . 5
โข (๐ โ โ โ
((2โ(4 ยท ๐))
ยท ((!โ๐)โ4)) = ((2โ(4 ยท ๐)) ยท (((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4)))) |
52 | | 2nn0 12437 |
. . . . . . . . . . . . 13
โข 2 โ
โ0 |
53 | 52 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 2 โ
โ0) |
54 | 53, 2 | nn0mulcld 12485 |
. . . . . . . . . . 11
โข (๐ โ โ โ (2
ยท ๐) โ
โ0) |
55 | | faccl 14190 |
. . . . . . . . . . 11
โข ((2
ยท ๐) โ
โ0 โ (!โ(2 ยท ๐)) โ โ) |
56 | | nncn 12168 |
. . . . . . . . . . 11
โข
((!โ(2 ยท ๐)) โ โ โ (!โ(2 ยท
๐)) โ
โ) |
57 | 54, 55, 56 | 3syl 18 |
. . . . . . . . . 10
โข (๐ โ โ โ
(!โ(2 ยท ๐))
โ โ) |
58 | 57 | sqcld 14056 |
. . . . . . . . 9
โข (๐ โ โ โ
((!โ(2 ยท ๐))โ2) โ โ) |
59 | 6, 8 | mulcld 11182 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (2
ยท (2 ยท ๐))
โ โ) |
60 | 59 | sqrtcld 15329 |
. . . . . . . . . . 11
โข (๐ โ โ โ
(โโ(2 ยท (2 ยท ๐))) โ โ) |
61 | 8, 12, 15 | divcld 11938 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((2
ยท ๐) / e) โ
โ) |
62 | 61, 54 | expcld 14058 |
. . . . . . . . . . 11
โข (๐ โ โ โ (((2
ยท ๐) / e)โ(2
ยท ๐)) โ
โ) |
63 | 60, 62 | mulcld 11182 |
. . . . . . . . . 10
โข (๐ โ โ โ
((โโ(2 ยท (2 ยท ๐))) ยท (((2 ยท ๐) / e)โ(2 ยท ๐))) โ โ) |
64 | 63 | sqcld 14056 |
. . . . . . . . 9
โข (๐ โ โ โ
(((โโ(2 ยท (2 ยท ๐))) ยท (((2 ยท ๐) / e)โ(2 ยท ๐)))โ2) โ โ) |
65 | 20, 22 | rpmulcld 12980 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (2
ยท (2 ยท ๐))
โ โ+) |
66 | 65 | sqrtgt0d 15304 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 0 <
(โโ(2 ยท (2 ยท ๐)))) |
67 | 66 | gt0ne0d 11726 |
. . . . . . . . . . 11
โข (๐ โ โ โ
(โโ(2 ยท (2 ยท ๐))) โ 0) |
68 | 20 | rpne0d 12969 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ 2 โ
0) |
69 | 6, 7, 68, 25 | mulne0d 11814 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (2
ยท ๐) โ
0) |
70 | 8, 12, 69, 15 | divne0d 11954 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((2
ยท ๐) / e) โ
0) |
71 | | 2z 12542 |
. . . . . . . . . . . . . 14
โข 2 โ
โค |
72 | 71 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ 2 โ
โค) |
73 | 72, 27 | zmulcld 12620 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (2
ยท ๐) โ
โค) |
74 | 61, 70, 73 | expne0d 14064 |
. . . . . . . . . . 11
โข (๐ โ โ โ (((2
ยท ๐) / e)โ(2
ยท ๐)) โ
0) |
75 | 60, 62, 67, 74 | mulne0d 11814 |
. . . . . . . . . 10
โข (๐ โ โ โ
((โโ(2 ยท (2 ยท ๐))) ยท (((2 ยท ๐) / e)โ(2 ยท ๐))) โ 0) |
76 | 63, 75, 72 | expne0d 14064 |
. . . . . . . . 9
โข (๐ โ โ โ
(((โโ(2 ยท (2 ยท ๐))) ยท (((2 ยท ๐) / e)โ(2 ยท ๐)))โ2) โ 0) |
77 | 58, 64, 76 | divcan1d 11939 |
. . . . . . . 8
โข (๐ โ โ โ
((((!โ(2 ยท ๐))โ2) / (((โโ(2 ยท (2
ยท ๐))) ยท (((2
ยท ๐) / e)โ(2
ยท ๐)))โ2))
ยท (((โโ(2 ยท (2 ยท ๐))) ยท (((2 ยท ๐) / e)โ(2 ยท ๐)))โ2)) = ((!โ(2 ยท ๐))โ2)) |
78 | 57, 63, 75, 53 | expdivd 14072 |
. . . . . . . . . 10
โข (๐ โ โ โ
(((!โ(2 ยท ๐))
/ ((โโ(2 ยท (2 ยท ๐))) ยท (((2 ยท ๐) / e)โ(2 ยท ๐))))โ2) = (((!โ(2 ยท ๐))โ2) / (((โโ(2
ยท (2 ยท ๐)))
ยท (((2 ยท ๐) /
e)โ(2 ยท ๐)))โ2))) |
79 | 78 | eqcomd 2743 |
. . . . . . . . 9
โข (๐ โ โ โ
(((!โ(2 ยท ๐))โ2) / (((โโ(2 ยท (2
ยท ๐))) ยท (((2
ยท ๐) / e)โ(2
ยท ๐)))โ2)) =
(((!โ(2 ยท ๐))
/ ((โโ(2 ยท (2 ยท ๐))) ยท (((2 ยท ๐) / e)โ(2 ยท ๐))))โ2)) |
80 | 79 | oveq1d 7377 |
. . . . . . . 8
โข (๐ โ โ โ
((((!โ(2 ยท ๐))โ2) / (((โโ(2 ยท (2
ยท ๐))) ยท (((2
ยท ๐) / e)โ(2
ยท ๐)))โ2))
ยท (((โโ(2 ยท (2 ยท ๐))) ยท (((2 ยท ๐) / e)โ(2 ยท ๐)))โ2)) = ((((!โ(2 ยท ๐)) / ((โโ(2 ยท
(2 ยท ๐))) ยท
(((2 ยท ๐) /
e)โ(2 ยท ๐))))โ2) ยท (((โโ(2
ยท (2 ยท ๐)))
ยท (((2 ยท ๐) /
e)โ(2 ยท ๐)))โ2))) |
81 | 77, 80 | eqtr3d 2779 |
. . . . . . 7
โข (๐ โ โ โ
((!โ(2 ยท ๐))โ2) = ((((!โ(2 ยท ๐)) / ((โโ(2 ยท
(2 ยท ๐))) ยท
(((2 ยท ๐) /
e)โ(2 ยท ๐))))โ2) ยท (((โโ(2
ยท (2 ยท ๐)))
ยท (((2 ยท ๐) /
e)โ(2 ยท ๐)))โ2))) |
82 | | fveq2 6847 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ (!โ๐) = (!โ๐)) |
83 | | oveq2 7370 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ (2 ยท ๐) = (2 ยท ๐)) |
84 | 83 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ (โโ(2 ยท ๐)) = (โโ(2 ยท
๐))) |
85 | | oveq1 7369 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ (๐ / e) = (๐ / e)) |
86 | | id 22 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ ๐ = ๐) |
87 | 85, 86 | oveq12d 7380 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ ((๐ / e)โ๐) = ((๐ / e)โ๐)) |
88 | 84, 87 | oveq12d 7380 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)) = ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) |
89 | 82, 88 | oveq12d 7380 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ ((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) = ((!โ๐) / ((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))) |
90 | 89 | cbvmptv 5223 |
. . . . . . . . . . . 12
โข (๐ โ โ โฆ
((!โ๐) /
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))) = (๐ โ โ โฆ ((!โ๐) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐)))) |
91 | 31, 90 | eqtri 2765 |
. . . . . . . . . . 11
โข ๐ด = (๐ โ โ โฆ ((!โ๐) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐)))) |
92 | | fveq2 6847 |
. . . . . . . . . . . 12
โข (๐ = (2 ยท ๐) โ (!โ๐) = (!โ(2 ยท ๐))) |
93 | | oveq2 7370 |
. . . . . . . . . . . . . 14
โข (๐ = (2 ยท ๐) โ (2 ยท ๐) = (2 ยท (2 ยท
๐))) |
94 | 93 | fveq2d 6851 |
. . . . . . . . . . . . 13
โข (๐ = (2 ยท ๐) โ (โโ(2
ยท ๐)) =
(โโ(2 ยท (2 ยท ๐)))) |
95 | | oveq1 7369 |
. . . . . . . . . . . . . 14
โข (๐ = (2 ยท ๐) โ (๐ / e) = ((2 ยท ๐) / e)) |
96 | | id 22 |
. . . . . . . . . . . . . 14
โข (๐ = (2 ยท ๐) โ ๐ = (2 ยท ๐)) |
97 | 95, 96 | oveq12d 7380 |
. . . . . . . . . . . . 13
โข (๐ = (2 ยท ๐) โ ((๐ / e)โ๐) = (((2 ยท ๐) / e)โ(2 ยท ๐))) |
98 | 94, 97 | oveq12d 7380 |
. . . . . . . . . . . 12
โข (๐ = (2 ยท ๐) โ ((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐)) = ((โโ(2 ยท
(2 ยท ๐))) ยท
(((2 ยท ๐) /
e)โ(2 ยท ๐)))) |
99 | 92, 98 | oveq12d 7380 |
. . . . . . . . . . 11
โข (๐ = (2 ยท ๐) โ ((!โ๐) / ((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐))) = ((!โ(2 ยท ๐)) / ((โโ(2 ยท
(2 ยท ๐))) ยท
(((2 ยท ๐) /
e)โ(2 ยท ๐))))) |
100 | | 2nn 12233 |
. . . . . . . . . . . . 13
โข 2 โ
โ |
101 | 100 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 2 โ
โ) |
102 | | id 22 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ) |
103 | 101, 102 | nnmulcld 12213 |
. . . . . . . . . . 11
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
104 | 57, 63, 75 | divcld 11938 |
. . . . . . . . . . 11
โข (๐ โ โ โ
((!โ(2 ยท ๐)) /
((โโ(2 ยท (2 ยท ๐))) ยท (((2 ยท ๐) / e)โ(2 ยท ๐)))) โ โ) |
105 | 91, 99, 103, 104 | fvmptd3 6976 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ดโ(2 ยท ๐)) = ((!โ(2 ยท ๐)) / ((โโ(2 ยท
(2 ยท ๐))) ยท
(((2 ยท ๐) /
e)โ(2 ยท ๐))))) |
106 | 105 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ โ โ โ ((๐ดโ(2 ยท ๐))โ2) = (((!โ(2
ยท ๐)) /
((โโ(2 ยท (2 ยท ๐))) ยท (((2 ยท ๐) / e)โ(2 ยท ๐))))โ2)) |
107 | 106 | eqcomd 2743 |
. . . . . . . 8
โข (๐ โ โ โ
(((!โ(2 ยท ๐))
/ ((โโ(2 ยท (2 ยท ๐))) ยท (((2 ยท ๐) / e)โ(2 ยท ๐))))โ2) = ((๐ดโ(2 ยท ๐))โ2)) |
108 | 107 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ โ โ
((((!โ(2 ยท ๐))
/ ((โโ(2 ยท (2 ยท ๐))) ยท (((2 ยท ๐) / e)โ(2 ยท ๐))))โ2) ยท (((โโ(2
ยท (2 ยท ๐)))
ยท (((2 ยท ๐) /
e)โ(2 ยท ๐)))โ2)) = (((๐ดโ(2 ยท ๐))โ2) ยท (((โโ(2
ยท (2 ยท ๐)))
ยท (((2 ยท ๐) /
e)โ(2 ยท ๐)))โ2))) |
109 | | eqidd 2738 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ โ โ โฆ
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) = (๐ โ โ โฆ ((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐)))) |
110 | 98 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ = (2 ยท ๐)) โ ((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐)) = ((โโ(2 ยท
(2 ยท ๐))) ยท
(((2 ยท ๐) /
e)โ(2 ยท ๐)))) |
111 | 109, 110,
103, 63 | fvmptd 6960 |
. . . . . . . . . 10
โข (๐ โ โ โ ((๐ โ โ โฆ
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))โ(2 ยท ๐)) = ((โโ(2 ยท (2 ยท
๐))) ยท (((2 ยท
๐) / e)โ(2 ยท
๐)))) |
112 | 111 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ โ โ โ (((๐ โ โ โฆ
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))โ(2 ยท ๐))โ2) = (((โโ(2 ยท (2
ยท ๐))) ยท (((2
ยท ๐) / e)โ(2
ยท ๐)))โ2)) |
113 | 112 | eqcomd 2743 |
. . . . . . . 8
โข (๐ โ โ โ
(((โโ(2 ยท (2 ยท ๐))) ยท (((2 ยท ๐) / e)โ(2 ยท ๐)))โ2) = (((๐ โ โ โฆ ((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐)))โ(2 ยท ๐))โ2)) |
114 | 113 | oveq2d 7378 |
. . . . . . 7
โข (๐ โ โ โ (((๐ดโ(2 ยท ๐))โ2) ยท
(((โโ(2 ยท (2 ยท ๐))) ยท (((2 ยท ๐) / e)โ(2 ยท ๐)))โ2)) = (((๐ดโ(2 ยท ๐))โ2) ยท (((๐ โ โ โฆ ((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐)))โ(2 ยท ๐))โ2))) |
115 | 81, 108, 114 | 3eqtrd 2781 |
. . . . . 6
โข (๐ โ โ โ
((!โ(2 ยท ๐))โ2) = (((๐ดโ(2 ยท ๐))โ2) ยท (((๐ โ โ โฆ ((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐)))โ(2 ยท ๐))โ2))) |
116 | 88 | cbvmptv 5223 |
. . . . . . . . . . 11
โข (๐ โ โ โฆ
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) = (๐ โ โ โฆ ((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐))) |
117 | 116 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ โ โ โฆ
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))) = (๐ โ โ โฆ ((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐)))) |
118 | 117 | fveq1d 6849 |
. . . . . . . . 9
โข (๐ โ โ โ ((๐ โ โ โฆ
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))โ(2 ยท ๐)) = ((๐ โ โ โฆ ((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐)))โ(2 ยท ๐))) |
119 | 118 | eqcomd 2743 |
. . . . . . . 8
โข (๐ โ โ โ ((๐ โ โ โฆ
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))โ(2 ยท ๐)) = ((๐ โ โ โฆ ((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐)))โ(2 ยท ๐))) |
120 | 119 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ โ โ (((๐ โ โ โฆ
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))โ(2 ยท ๐))โ2) = (((๐ โ โ โฆ ((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐)))โ(2 ยท ๐))โ2)) |
121 | 120 | oveq2d 7378 |
. . . . . 6
โข (๐ โ โ โ (((๐ดโ(2 ยท ๐))โ2) ยท (((๐ โ โ โฆ
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))โ(2 ยท ๐))โ2)) = (((๐ดโ(2 ยท ๐))โ2) ยท (((๐ โ โ โฆ ((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐)))โ(2 ยท ๐))โ2))) |
122 | 105, 104 | eqeltrd 2838 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ดโ(2 ยท ๐)) โ
โ) |
123 | | stirlinglem3.2 |
. . . . . . . . . . 11
โข ๐ท = (๐ โ โ โฆ (๐ดโ(2 ยท ๐))) |
124 | 123 | fvmpt2 6964 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐ดโ(2 ยท ๐)) โ โ) โ (๐ทโ๐) = (๐ดโ(2 ยท ๐))) |
125 | 122, 124 | mpdan 686 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ทโ๐) = (๐ดโ(2 ยท ๐))) |
126 | 125 | eqcomd 2743 |
. . . . . . . 8
โข (๐ โ โ โ (๐ดโ(2 ยท ๐)) = (๐ทโ๐)) |
127 | 126 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ โ โ ((๐ดโ(2 ยท ๐))โ2) = ((๐ทโ๐)โ2)) |
128 | 35 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ธ = (๐ โ โ โฆ ((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐)))) |
129 | 128 | fveq1d 6849 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ธโ(2 ยท ๐)) = ((๐ โ โ โฆ ((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐)))โ(2 ยท ๐))) |
130 | 129 | eqcomd 2743 |
. . . . . . . 8
โข (๐ โ โ โ ((๐ โ โ โฆ
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))โ(2 ยท ๐)) = (๐ธโ(2 ยท ๐))) |
131 | 130 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ โ โ (((๐ โ โ โฆ
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))โ(2 ยท ๐))โ2) = ((๐ธโ(2 ยท ๐))โ2)) |
132 | 127, 131 | oveq12d 7380 |
. . . . . 6
โข (๐ โ โ โ (((๐ดโ(2 ยท ๐))โ2) ยท (((๐ โ โ โฆ
((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐)))โ(2 ยท ๐))โ2)) = (((๐ทโ๐)โ2) ยท ((๐ธโ(2 ยท ๐))โ2))) |
133 | 115, 121,
132 | 3eqtrd 2781 |
. . . . 5
โข (๐ โ โ โ
((!โ(2 ยท ๐))โ2) = (((๐ทโ๐)โ2) ยท ((๐ธโ(2 ยท ๐))โ2))) |
134 | 51, 133 | oveq12d 7380 |
. . . 4
โข (๐ โ โ โ
(((2โ(4 ยท ๐))
ยท ((!โ๐)โ4)) / ((!โ(2 ยท ๐))โ2)) = (((2โ(4
ยท ๐)) ยท
(((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4))) / (((๐ทโ๐)โ2) ยท ((๐ธโ(2 ยท ๐))โ2)))) |
135 | 134 | oveq1d 7377 |
. . 3
โข (๐ โ โ โ
((((2โ(4 ยท ๐))
ยท ((!โ๐)โ4)) / ((!โ(2 ยท ๐))โ2)) / ((2 ยท ๐) + 1)) = ((((2โ(4 ยท
๐)) ยท (((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4))) / (((๐ทโ๐)โ2) ยท ((๐ธโ(2 ยท ๐))โ2))) / ((2 ยท ๐) + 1))) |
136 | 135 | mpteq2ia 5213 |
. 2
โข (๐ โ โ โฆ
((((2โ(4 ยท ๐))
ยท ((!โ๐)โ4)) / ((!โ(2 ยท ๐))โ2)) / ((2 ยท ๐) + 1))) = (๐ โ โ โฆ ((((2โ(4
ยท ๐)) ยท
(((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4))) / (((๐ทโ๐)โ2) ยท ((๐ธโ(2 ยท ๐))โ2))) / ((2 ยท ๐) + 1))) |
137 | 41, 2 | nn0mulcld 12485 |
. . . . . . . 8
โข (๐ โ โ โ (4
ยท ๐) โ
โ0) |
138 | 6, 137 | expcld 14058 |
. . . . . . 7
โข (๐ โ โ โ
(2โ(4 ยท ๐))
โ โ) |
139 | 49, 44 | eqeltrd 2838 |
. . . . . . 7
โข (๐ โ โ โ (((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4)) โ โ) |
140 | 138, 139 | mulcomd 11183 |
. . . . . 6
โข (๐ โ โ โ
((2โ(4 ยท ๐))
ยท (((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4))) = ((((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4)) ยท (2โ(4 ยท ๐)))) |
141 | 140 | oveq1d 7377 |
. . . . 5
โข (๐ โ โ โ
(((2โ(4 ยท ๐))
ยท (((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4))) / (((๐ทโ๐)โ2) ยท ((๐ธโ(2 ยท ๐))โ2))) = (((((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4)) ยท (2โ(4 ยท ๐))) / (((๐ทโ๐)โ2) ยท ((๐ธโ(2 ยท ๐))โ2)))) |
142 | 141 | oveq1d 7377 |
. . . 4
โข (๐ โ โ โ
((((2โ(4 ยท ๐))
ยท (((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4))) / (((๐ทโ๐)โ2) ยท ((๐ธโ(2 ยท ๐))โ2))) / ((2 ยท ๐) + 1)) = ((((((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4)) ยท (2โ(4 ยท ๐))) / (((๐ทโ๐)โ2) ยท ((๐ธโ(2 ยท ๐))โ2))) / ((2 ยท ๐) + 1))) |
143 | 125, 122 | eqeltrd 2838 |
. . . . . . . 8
โข (๐ โ โ โ (๐ทโ๐) โ โ) |
144 | 143 | sqcld 14056 |
. . . . . . 7
โข (๐ โ โ โ ((๐ทโ๐)โ2) โ โ) |
145 | 128, 117 | eqtrd 2777 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ธ = (๐ โ โ โฆ ((โโ(2
ยท ๐)) ยท
((๐ / e)โ๐)))) |
146 | 145, 110,
103, 63 | fvmptd 6960 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ธโ(2 ยท ๐)) = ((โโ(2 ยท
(2 ยท ๐))) ยท
(((2 ยท ๐) /
e)โ(2 ยท ๐)))) |
147 | 146, 63 | eqeltrd 2838 |
. . . . . . . 8
โข (๐ โ โ โ (๐ธโ(2 ยท ๐)) โ
โ) |
148 | 147 | sqcld 14056 |
. . . . . . 7
โข (๐ โ โ โ ((๐ธโ(2 ยท ๐))โ2) โ
โ) |
149 | | nnne0 12194 |
. . . . . . . . . . . 12
โข
((!โ(2 ยท ๐)) โ โ โ (!โ(2 ยท
๐)) โ
0) |
150 | 54, 55, 149 | 3syl 18 |
. . . . . . . . . . 11
โข (๐ โ โ โ
(!โ(2 ยท ๐))
โ 0) |
151 | 57, 63, 150, 75 | divne0d 11954 |
. . . . . . . . . 10
โข (๐ โ โ โ
((!โ(2 ยท ๐)) /
((โโ(2 ยท (2 ยท ๐))) ยท (((2 ยท ๐) / e)โ(2 ยท ๐)))) โ 0) |
152 | 105, 151 | eqnetrd 3012 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ดโ(2 ยท ๐)) โ 0) |
153 | 125, 152 | eqnetrd 3012 |
. . . . . . . 8
โข (๐ โ โ โ (๐ทโ๐) โ 0) |
154 | 143, 153,
72 | expne0d 14064 |
. . . . . . 7
โข (๐ โ โ โ ((๐ทโ๐)โ2) โ 0) |
155 | 146, 75 | eqnetrd 3012 |
. . . . . . . 8
โข (๐ โ โ โ (๐ธโ(2 ยท ๐)) โ 0) |
156 | 147, 155,
72 | expne0d 14064 |
. . . . . . 7
โข (๐ โ โ โ ((๐ธโ(2 ยท ๐))โ2) โ
0) |
157 | 139, 144,
138, 148, 154, 156 | divmuldivd 11979 |
. . . . . 6
โข (๐ โ โ โ
(((((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4)) / ((๐ทโ๐)โ2)) ยท ((2โ(4 ยท
๐)) / ((๐ธโ(2 ยท ๐))โ2))) = (((((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4)) ยท (2โ(4 ยท ๐))) / (((๐ทโ๐)โ2) ยท ((๐ธโ(2 ยท ๐))โ2)))) |
158 | 157 | eqcomd 2743 |
. . . . 5
โข (๐ โ โ โ
(((((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4)) ยท (2โ(4 ยท ๐))) / (((๐ทโ๐)โ2) ยท ((๐ธโ(2 ยท ๐))โ2))) = (((((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4)) / ((๐ทโ๐)โ2)) ยท ((2โ(4 ยท
๐)) / ((๐ธโ(2 ยท ๐))โ2)))) |
159 | 158 | oveq1d 7377 |
. . . 4
โข (๐ โ โ โ
((((((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4)) ยท (2โ(4 ยท ๐))) / (((๐ทโ๐)โ2) ยท ((๐ธโ(2 ยท ๐))โ2))) / ((2 ยท ๐) + 1)) = ((((((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4)) / ((๐ทโ๐)โ2)) ยท ((2โ(4 ยท
๐)) / ((๐ธโ(2 ยท ๐))โ2))) / ((2 ยท ๐) + 1))) |
160 | 33, 30 | eqeltrd 2838 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ดโ๐) โ โ) |
161 | 160, 41 | expcld 14058 |
. . . . . . . 8
โข (๐ โ โ โ ((๐ดโ๐)โ4) โ โ) |
162 | 38, 45 | eqeltrd 2838 |
. . . . . . . 8
โข (๐ โ โ โ ((๐ธโ๐)โ4) โ โ) |
163 | 161, 162,
144, 154 | div23d 11975 |
. . . . . . 7
โข (๐ โ โ โ ((((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4)) / ((๐ทโ๐)โ2)) = ((((๐ดโ๐)โ4) / ((๐ทโ๐)โ2)) ยท ((๐ธโ๐)โ4))) |
164 | 163 | oveq1d 7377 |
. . . . . 6
โข (๐ โ โ โ
(((((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4)) / ((๐ทโ๐)โ2)) ยท ((2โ(4 ยท
๐)) / ((๐ธโ(2 ยท ๐))โ2))) = (((((๐ดโ๐)โ4) / ((๐ทโ๐)โ2)) ยท ((๐ธโ๐)โ4)) ยท ((2โ(4 ยท
๐)) / ((๐ธโ(2 ยท ๐))โ2)))) |
165 | 164 | oveq1d 7377 |
. . . . 5
โข (๐ โ โ โ
((((((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4)) / ((๐ทโ๐)โ2)) ยท ((2โ(4 ยท
๐)) / ((๐ธโ(2 ยท ๐))โ2))) / ((2 ยท ๐) + 1)) = ((((((๐ดโ๐)โ4) / ((๐ทโ๐)โ2)) ยท ((๐ธโ๐)โ4)) ยท ((2โ(4 ยท
๐)) / ((๐ธโ(2 ยท ๐))โ2))) / ((2 ยท ๐) + 1))) |
166 | 161, 144,
154 | divcld 11938 |
. . . . . . 7
โข (๐ โ โ โ (((๐ดโ๐)โ4) / ((๐ทโ๐)โ2)) โ โ) |
167 | 138, 148,
156 | divcld 11938 |
. . . . . . 7
โข (๐ โ โ โ
((2โ(4 ยท ๐)) /
((๐ธโ(2 ยท ๐))โ2)) โ
โ) |
168 | 166, 162,
167 | mulassd 11185 |
. . . . . 6
โข (๐ โ โ โ
(((((๐ดโ๐)โ4) / ((๐ทโ๐)โ2)) ยท ((๐ธโ๐)โ4)) ยท ((2โ(4 ยท
๐)) / ((๐ธโ(2 ยท ๐))โ2))) = ((((๐ดโ๐)โ4) / ((๐ทโ๐)โ2)) ยท (((๐ธโ๐)โ4) ยท ((2โ(4 ยท ๐)) / ((๐ธโ(2 ยท ๐))โ2))))) |
169 | 168 | oveq1d 7377 |
. . . . 5
โข (๐ โ โ โ
((((((๐ดโ๐)โ4) / ((๐ทโ๐)โ2)) ยท ((๐ธโ๐)โ4)) ยท ((2โ(4 ยท
๐)) / ((๐ธโ(2 ยท ๐))โ2))) / ((2 ยท ๐) + 1)) = (((((๐ดโ๐)โ4) / ((๐ทโ๐)โ2)) ยท (((๐ธโ๐)โ4) ยท ((2โ(4 ยท ๐)) / ((๐ธโ(2 ยท ๐))โ2)))) / ((2 ยท ๐) + 1))) |
170 | 162, 167 | mulcld 11182 |
. . . . . . 7
โข (๐ โ โ โ (((๐ธโ๐)โ4) ยท ((2โ(4 ยท ๐)) / ((๐ธโ(2 ยท ๐))โ2))) โ โ) |
171 | | 1cnd 11157 |
. . . . . . . 8
โข (๐ โ โ โ 1 โ
โ) |
172 | 8, 171 | addcld 11181 |
. . . . . . 7
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
โ) |
173 | | 0red 11165 |
. . . . . . . . 9
โข (๐ โ โ โ 0 โ
โ) |
174 | 103 | nnred 12175 |
. . . . . . . . 9
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
175 | | 2re 12234 |
. . . . . . . . . . . 12
โข 2 โ
โ |
176 | 175 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ โ โ 2 โ
โ) |
177 | | nnre 12167 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
178 | 176, 177 | remulcld 11192 |
. . . . . . . . . 10
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
179 | | 1red 11163 |
. . . . . . . . . 10
โข (๐ โ โ โ 1 โ
โ) |
180 | 178, 179 | readdcld 11191 |
. . . . . . . . 9
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
โ) |
181 | 103 | nngt0d 12209 |
. . . . . . . . 9
โข (๐ โ โ โ 0 < (2
ยท ๐)) |
182 | 174 | ltp1d 12092 |
. . . . . . . . 9
โข (๐ โ โ โ (2
ยท ๐) < ((2
ยท ๐) +
1)) |
183 | 173, 174,
180, 181, 182 | lttrd 11323 |
. . . . . . . 8
โข (๐ โ โ โ 0 <
((2 ยท ๐) +
1)) |
184 | 183 | gt0ne0d 11726 |
. . . . . . 7
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
0) |
185 | 166, 170,
172, 184 | divassd 11973 |
. . . . . 6
โข (๐ โ โ โ
(((((๐ดโ๐)โ4) / ((๐ทโ๐)โ2)) ยท (((๐ธโ๐)โ4) ยท ((2โ(4 ยท ๐)) / ((๐ธโ(2 ยท ๐))โ2)))) / ((2 ยท ๐) + 1)) = ((((๐ดโ๐)โ4) / ((๐ทโ๐)โ2)) ยท ((((๐ธโ๐)โ4) ยท ((2โ(4 ยท ๐)) / ((๐ธโ(2 ยท ๐))โ2))) / ((2 ยท ๐) + 1)))) |
186 | 162, 138,
148, 156 | div12d 11974 |
. . . . . . . . . 10
โข (๐ โ โ โ (((๐ธโ๐)โ4) ยท ((2โ(4 ยท ๐)) / ((๐ธโ(2 ยท ๐))โ2))) = ((2โ(4 ยท ๐)) ยท (((๐ธโ๐)โ4) / ((๐ธโ(2 ยท ๐))โ2)))) |
187 | 9, 17, 41 | mulexpd 14073 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
(((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))โ4) = (((โโ(2 ยท
๐))โ4) ยท
(((๐ / e)โ๐)โ4))) |
188 | 60, 62 | sqmuld 14070 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
(((โโ(2 ยท (2 ยท ๐))) ยท (((2 ยท ๐) / e)โ(2 ยท ๐)))โ2) = (((โโ(2 ยท (2
ยท ๐)))โ2)
ยท ((((2 ยท ๐)
/ e)โ(2 ยท ๐))โ2))) |
189 | 187, 188 | oveq12d 7380 |
. . . . . . . . . . . 12
โข (๐ โ โ โ
((((โโ(2 ยท ๐)) ยท ((๐ / e)โ๐))โ4) / (((โโ(2 ยท (2
ยท ๐))) ยท (((2
ยท ๐) / e)โ(2
ยท ๐)))โ2)) =
((((โโ(2 ยท ๐))โ4) ยท (((๐ / e)โ๐)โ4)) / (((โโ(2 ยท (2
ยท ๐)))โ2)
ยท ((((2 ยท ๐)
/ e)โ(2 ยท ๐))โ2)))) |
190 | 146 | oveq1d 7377 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((๐ธโ(2 ยท ๐))โ2) = (((โโ(2
ยท (2 ยท ๐)))
ยท (((2 ยท ๐) /
e)โ(2 ยท ๐)))โ2)) |
191 | 38, 190 | oveq12d 7380 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (((๐ธโ๐)โ4) / ((๐ธโ(2 ยท ๐))โ2)) = ((((โโ(2 ยท
๐)) ยท ((๐ / e)โ๐))โ4) / (((โโ(2 ยท (2
ยท ๐))) ยท (((2
ยท ๐) / e)โ(2
ยท ๐)))โ2))) |
192 | 9, 41 | expcld 14058 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
((โโ(2 ยท ๐))โ4) โ โ) |
193 | 60 | sqcld 14056 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
((โโ(2 ยท (2 ยท ๐)))โ2) โ โ) |
194 | 17, 41 | expcld 14058 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (((๐ / e)โ๐)โ4) โ โ) |
195 | 62 | sqcld 14056 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((((2
ยท ๐) / e)โ(2
ยท ๐))โ2) โ
โ) |
196 | 60, 67, 72 | expne0d 14064 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
((โโ(2 ยท (2 ยท ๐)))โ2) โ 0) |
197 | 62, 74, 72 | expne0d 14064 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((((2
ยท ๐) / e)โ(2
ยท ๐))โ2) โ
0) |
198 | 192, 193,
194, 195, 196, 197 | divmuldivd 11979 |
. . . . . . . . . . . 12
โข (๐ โ โ โ
((((โโ(2 ยท ๐))โ4) / ((โโ(2 ยท (2
ยท ๐)))โ2))
ยท ((((๐ /
e)โ๐)โ4) / ((((2
ยท ๐) / e)โ(2
ยท ๐))โ2))) =
((((โโ(2 ยท ๐))โ4) ยท (((๐ / e)โ๐)โ4)) / (((โโ(2 ยท (2
ยท ๐)))โ2)
ยท ((((2 ยท ๐)
/ e)โ(2 ยท ๐))โ2)))) |
199 | 189, 191,
198 | 3eqtr4d 2787 |
. . . . . . . . . . 11
โข (๐ โ โ โ (((๐ธโ๐)โ4) / ((๐ธโ(2 ยท ๐))โ2)) = ((((โโ(2 ยท
๐))โ4) /
((โโ(2 ยท (2 ยท ๐)))โ2)) ยท ((((๐ / e)โ๐)โ4) / ((((2 ยท ๐) / e)โ(2 ยท ๐))โ2)))) |
200 | 199 | oveq2d 7378 |
. . . . . . . . . 10
โข (๐ โ โ โ
((2โ(4 ยท ๐))
ยท (((๐ธโ๐)โ4) / ((๐ธโ(2 ยท ๐))โ2))) = ((2โ(4 ยท ๐)) ยท ((((โโ(2
ยท ๐))โ4) /
((โโ(2 ยท (2 ยท ๐)))โ2)) ยท ((((๐ / e)โ๐)โ4) / ((((2 ยท ๐) / e)โ(2 ยท ๐))โ2))))) |
201 | 65 | rprege0d 12971 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ((2
ยท (2 ยท ๐))
โ โ โง 0 โค (2 ยท (2 ยท ๐)))) |
202 | | resqrtth 15147 |
. . . . . . . . . . . . . . . 16
โข (((2
ยท (2 ยท ๐))
โ โ โง 0 โค (2 ยท (2 ยท ๐))) โ ((โโ(2 ยท (2
ยท ๐)))โ2) = (2
ยท (2 ยท ๐))) |
203 | 201, 202 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ
((โโ(2 ยท (2 ยท ๐)))โ2) = (2 ยท (2 ยท ๐))) |
204 | 203 | oveq2d 7378 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ
(((โโ(2 ยท ๐))โ4) / ((โโ(2 ยท (2
ยท ๐)))โ2)) =
(((โโ(2 ยท ๐))โ4) / (2 ยท (2 ยท ๐)))) |
205 | | 2t2e4 12324 |
. . . . . . . . . . . . . . . . . . 19
โข (2
ยท 2) = 4 |
206 | 205 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . 18
โข 4 = (2
ยท 2) |
207 | 206 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ 4 = (2
ยท 2)) |
208 | 207 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ
((โโ(2 ยท ๐))โ4) = ((โโ(2 ยท
๐))โ(2 ยท
2))) |
209 | 9, 53, 53 | expmuld 14061 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ
((โโ(2 ยท ๐))โ(2 ยท 2)) = (((โโ(2
ยท ๐))โ2)โ2)) |
210 | 22 | rprege0d 12971 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ ((2
ยท ๐) โ โ
โง 0 โค (2 ยท ๐))) |
211 | | resqrtth 15147 |
. . . . . . . . . . . . . . . . . 18
โข (((2
ยท ๐) โ โ
โง 0 โค (2 ยท ๐)) โ ((โโ(2 ยท ๐))โ2) = (2 ยท ๐)) |
212 | 210, 211 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ
((โโ(2 ยท ๐))โ2) = (2 ยท ๐)) |
213 | 212 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ
(((โโ(2 ยท ๐))โ2)โ2) = ((2 ยท ๐)โ2)) |
214 | 208, 209,
213 | 3eqtrd 2781 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ
((โโ(2 ยท ๐))โ4) = ((2 ยท ๐)โ2)) |
215 | 6, 6, 7 | mulassd 11185 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ((2
ยท 2) ยท ๐) =
(2 ยท (2 ยท ๐))) |
216 | 205 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ (2
ยท 2) = 4) |
217 | 216 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ((2
ยท 2) ยท ๐) =
(4 ยท ๐)) |
218 | 215, 217 | eqtr3d 2779 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (2
ยท (2 ยท ๐)) =
(4 ยท ๐)) |
219 | 214, 218 | oveq12d 7380 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ
(((โโ(2 ยท ๐))โ4) / (2 ยท (2 ยท ๐))) = (((2 ยท ๐)โ2) / (4 ยท ๐))) |
220 | 6, 7 | sqmuld 14070 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ ((2
ยท ๐)โ2) =
((2โ2) ยท (๐โ2))) |
221 | | sq2 14108 |
. . . . . . . . . . . . . . . . . . 19
โข
(2โ2) = 4 |
222 | 221 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ
(2โ2) = 4) |
223 | 222 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ
((2โ2) ยท (๐โ2)) = (4 ยท (๐โ2))) |
224 | 220, 223 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ((2
ยท ๐)โ2) = (4
ยท (๐โ2))) |
225 | 224 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (((2
ยท ๐)โ2) / (4
ยท ๐)) = ((4 ยท
(๐โ2)) / (4 ยท
๐))) |
226 | | 4cn 12245 |
. . . . . . . . . . . . . . . . . . 19
โข 4 โ
โ |
227 | | 4ne0 12268 |
. . . . . . . . . . . . . . . . . . 19
โข 4 โ
0 |
228 | 226, 227 | dividi 11895 |
. . . . . . . . . . . . . . . . . 18
โข (4 / 4) =
1 |
229 | 228 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ (4 / 4) =
1) |
230 | 7 | sqvald 14055 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ (๐โ2) = (๐ ยท ๐)) |
231 | 230 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ ((๐โ2) / ๐) = ((๐ ยท ๐) / ๐)) |
232 | 7, 7, 25 | divcan4d 11944 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ ((๐ ยท ๐) / ๐) = ๐) |
233 | 231, 232 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ ((๐โ2) / ๐) = ๐) |
234 | 229, 233 | oveq12d 7380 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ((4 / 4)
ยท ((๐โ2) /
๐)) = (1 ยท ๐)) |
235 | 41 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ 4 โ
โ) |
236 | 7 | sqcld 14056 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ (๐โ2) โ
โ) |
237 | 227 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ 4 โ
0) |
238 | 235, 235,
236, 7, 237, 25 | divmuldivd 11979 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ((4 / 4)
ยท ((๐โ2) /
๐)) = ((4 ยท (๐โ2)) / (4 ยท ๐))) |
239 | 7 | mulid2d 11180 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (1
ยท ๐) = ๐) |
240 | 234, 238,
239 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ((4
ยท (๐โ2)) / (4
ยท ๐)) = ๐) |
241 | 225, 240 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (((2
ยท ๐)โ2) / (4
ยท ๐)) = ๐) |
242 | 204, 219,
241 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
(((โโ(2 ยท ๐))โ4) / ((โโ(2 ยท (2
ยท ๐)))โ2)) =
๐) |
243 | 7, 235 | mulcomd 11183 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ (๐ ยท 4) = (4 ยท ๐)) |
244 | 243 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ((๐ / e)โ(๐ ยท 4)) = ((๐ / e)โ(4 ยท ๐))) |
245 | 16, 41, 2 | expmuld 14061 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ((๐ / e)โ(๐ ยท 4)) = (((๐ / e)โ๐)โ4)) |
246 | 7, 12, 15, 137 | expdivd 14072 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ((๐ / e)โ(4 ยท ๐)) = ((๐โ(4 ยท ๐)) / (eโ(4 ยท ๐)))) |
247 | 244, 245,
246 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (((๐ / e)โ๐)โ4) = ((๐โ(4 ยท ๐)) / (eโ(4 ยท ๐)))) |
248 | 6, 7, 6 | mul32d 11372 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ ((2
ยท ๐) ยท 2) =
((2 ยท 2) ยท ๐)) |
249 | 248, 217 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ ((2
ยท ๐) ยท 2) =
(4 ยท ๐)) |
250 | 249 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (((2
ยท ๐) / e)โ((2
ยท ๐) ยท 2)) =
(((2 ยท ๐) /
e)โ(4 ยท ๐))) |
251 | 61, 53, 54 | expmuld 14061 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (((2
ยท ๐) / e)โ((2
ยท ๐) ยท 2)) =
((((2 ยท ๐) /
e)โ(2 ยท ๐))โ2)) |
252 | 8, 12, 15, 137 | expdivd 14072 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (((2
ยท ๐) / e)โ(4
ยท ๐)) = (((2
ยท ๐)โ(4
ยท ๐)) / (eโ(4
ยท ๐)))) |
253 | 250, 251,
252 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ((((2
ยท ๐) / e)โ(2
ยท ๐))โ2) = (((2
ยท ๐)โ(4
ยท ๐)) / (eโ(4
ยท ๐)))) |
254 | 247, 253 | oveq12d 7380 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ((((๐ / e)โ๐)โ4) / ((((2 ยท ๐) / e)โ(2 ยท ๐))โ2)) = (((๐โ(4 ยท ๐)) / (eโ(4 ยท ๐))) / (((2 ยท ๐)โ(4 ยท ๐)) / (eโ(4 ยท ๐))))) |
255 | 247, 194 | eqeltrrd 2839 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ((๐โ(4 ยท ๐)) / (eโ(4 ยท ๐))) โ
โ) |
256 | 8, 137 | expcld 14058 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ((2
ยท ๐)โ(4
ยท ๐)) โ
โ) |
257 | 12, 137 | expcld 14058 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ
(eโ(4 ยท ๐))
โ โ) |
258 | 46, 27 | zmulcld 12620 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (4
ยท ๐) โ
โค) |
259 | 8, 69, 258 | expne0d 14064 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ((2
ยท ๐)โ(4
ยท ๐)) โ
0) |
260 | 12, 15, 258 | expne0d 14064 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ
(eโ(4 ยท ๐))
โ 0) |
261 | 255, 256,
257, 259, 260 | divdiv2d 11970 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (((๐โ(4 ยท ๐)) / (eโ(4 ยท ๐))) / (((2 ยท ๐)โ(4 ยท ๐)) / (eโ(4 ยท ๐)))) = ((((๐โ(4 ยท ๐)) / (eโ(4 ยท ๐))) ยท (eโ(4 ยท ๐))) / ((2 ยท ๐)โ(4 ยท ๐)))) |
262 | 7, 137 | expcld 14058 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ (๐โ(4 ยท ๐)) โ
โ) |
263 | 262, 257,
260 | divcan1d 11939 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (((๐โ(4 ยท ๐)) / (eโ(4 ยท ๐))) ยท (eโ(4 ยท
๐))) = (๐โ(4 ยท ๐))) |
264 | 263 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ((((๐โ(4 ยท ๐)) / (eโ(4 ยท ๐))) ยท (eโ(4 ยท
๐))) / ((2 ยท ๐)โ(4 ยท ๐))) = ((๐โ(4 ยท ๐)) / ((2 ยท ๐)โ(4 ยท ๐)))) |
265 | 6, 7, 137 | mulexpd 14073 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ((2
ยท ๐)โ(4
ยท ๐)) = ((2โ(4
ยท ๐)) ยท
(๐โ(4 ยท ๐)))) |
266 | 265 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ((๐โ(4 ยท ๐)) / ((2 ยท ๐)โ(4 ยท ๐))) = ((๐โ(4 ยท ๐)) / ((2โ(4 ยท ๐)) ยท (๐โ(4 ยท ๐))))) |
267 | 138, 262 | mulcomd 11183 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ
((2โ(4 ยท ๐))
ยท (๐โ(4
ยท ๐))) = ((๐โ(4 ยท ๐)) ยท (2โ(4 ยท
๐)))) |
268 | 267 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ((๐โ(4 ยท ๐)) / ((2โ(4 ยท ๐)) ยท (๐โ(4 ยท ๐)))) = ((๐โ(4 ยท ๐)) / ((๐โ(4 ยท ๐)) ยท (2โ(4 ยท ๐))))) |
269 | 7, 25, 258 | expne0d 14064 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ (๐โ(4 ยท ๐)) โ 0) |
270 | 6, 68, 258 | expne0d 14064 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ
(2โ(4 ยท ๐))
โ 0) |
271 | 262, 262,
138, 269, 270 | divdiv1d 11969 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (((๐โ(4 ยท ๐)) / (๐โ(4 ยท ๐))) / (2โ(4 ยท ๐))) = ((๐โ(4 ยท ๐)) / ((๐โ(4 ยท ๐)) ยท (2โ(4 ยท ๐))))) |
272 | 262, 269 | dividd 11936 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ ((๐โ(4 ยท ๐)) / (๐โ(4 ยท ๐))) = 1) |
273 | 272 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (((๐โ(4 ยท ๐)) / (๐โ(4 ยท ๐))) / (2โ(4 ยท ๐))) = (1 / (2โ(4 ยท ๐)))) |
274 | 268, 271,
273 | 3eqtr2d 2783 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ((๐โ(4 ยท ๐)) / ((2โ(4 ยท ๐)) ยท (๐โ(4 ยท ๐)))) = (1 / (2โ(4 ยท ๐)))) |
275 | 264, 266,
274 | 3eqtrd 2781 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ((((๐โ(4 ยท ๐)) / (eโ(4 ยท ๐))) ยท (eโ(4 ยท
๐))) / ((2 ยท ๐)โ(4 ยท ๐))) = (1 / (2โ(4 ยท
๐)))) |
276 | 254, 261,
275 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((((๐ / e)โ๐)โ4) / ((((2 ยท ๐) / e)โ(2 ยท ๐))โ2)) = (1 / (2โ(4 ยท ๐)))) |
277 | 242, 276 | oveq12d 7380 |
. . . . . . . . . . . 12
โข (๐ โ โ โ
((((โโ(2 ยท ๐))โ4) / ((โโ(2 ยท (2
ยท ๐)))โ2))
ยท ((((๐ /
e)โ๐)โ4) / ((((2
ยท ๐) / e)โ(2
ยท ๐))โ2))) =
(๐ ยท (1 / (2โ(4
ยท ๐))))) |
278 | 277 | oveq2d 7378 |
. . . . . . . . . . 11
โข (๐ โ โ โ
((2โ(4 ยท ๐))
ยท ((((โโ(2 ยท ๐))โ4) / ((โโ(2 ยท (2
ยท ๐)))โ2))
ยท ((((๐ /
e)โ๐)โ4) / ((((2
ยท ๐) / e)โ(2
ยท ๐))โ2)))) =
((2โ(4 ยท ๐))
ยท (๐ ยท (1 /
(2โ(4 ยท ๐)))))) |
279 | 138, 270 | reccld 11931 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (1 /
(2โ(4 ยท ๐)))
โ โ) |
280 | 138, 7, 279 | mul12d 11371 |
. . . . . . . . . . 11
โข (๐ โ โ โ
((2โ(4 ยท ๐))
ยท (๐ ยท (1 /
(2โ(4 ยท ๐)))))
= (๐ ยท ((2โ(4
ยท ๐)) ยท (1 /
(2โ(4 ยท ๐)))))) |
281 | 7 | mulid1d 11179 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (๐ ยท 1) = ๐) |
282 | 138, 270 | recidd 11933 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
((2โ(4 ยท ๐))
ยท (1 / (2โ(4 ยท ๐)))) = 1) |
283 | 282 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (๐ ยท ((2โ(4 ยท
๐)) ยท (1 /
(2โ(4 ยท ๐)))))
= (๐ ยท
1)) |
284 | 281, 283,
233 | 3eqtr4d 2787 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ ยท ((2โ(4 ยท
๐)) ยท (1 /
(2โ(4 ยท ๐)))))
= ((๐โ2) / ๐)) |
285 | 278, 280,
284 | 3eqtrd 2781 |
. . . . . . . . . 10
โข (๐ โ โ โ
((2โ(4 ยท ๐))
ยท ((((โโ(2 ยท ๐))โ4) / ((โโ(2 ยท (2
ยท ๐)))โ2))
ยท ((((๐ /
e)โ๐)โ4) / ((((2
ยท ๐) / e)โ(2
ยท ๐))โ2)))) =
((๐โ2) / ๐)) |
286 | 186, 200,
285 | 3eqtrd 2781 |
. . . . . . . . 9
โข (๐ โ โ โ (((๐ธโ๐)โ4) ยท ((2โ(4 ยท ๐)) / ((๐ธโ(2 ยท ๐))โ2))) = ((๐โ2) / ๐)) |
287 | 286 | oveq1d 7377 |
. . . . . . . 8
โข (๐ โ โ โ ((((๐ธโ๐)โ4) ยท ((2โ(4 ยท ๐)) / ((๐ธโ(2 ยท ๐))โ2))) / ((2 ยท ๐) + 1)) = (((๐โ2) / ๐) / ((2 ยท ๐) + 1))) |
288 | 236, 7, 172, 25, 184 | divdiv1d 11969 |
. . . . . . . 8
โข (๐ โ โ โ (((๐โ2) / ๐) / ((2 ยท ๐) + 1)) = ((๐โ2) / (๐ ยท ((2 ยท ๐) + 1)))) |
289 | 287, 288 | eqtrd 2777 |
. . . . . . 7
โข (๐ โ โ โ ((((๐ธโ๐)โ4) ยท ((2โ(4 ยท ๐)) / ((๐ธโ(2 ยท ๐))โ2))) / ((2 ยท ๐) + 1)) = ((๐โ2) / (๐ ยท ((2 ยท ๐) + 1)))) |
290 | 289 | oveq2d 7378 |
. . . . . 6
โข (๐ โ โ โ ((((๐ดโ๐)โ4) / ((๐ทโ๐)โ2)) ยท ((((๐ธโ๐)โ4) ยท ((2โ(4 ยท ๐)) / ((๐ธโ(2 ยท ๐))โ2))) / ((2 ยท ๐) + 1))) = ((((๐ดโ๐)โ4) / ((๐ทโ๐)โ2)) ยท ((๐โ2) / (๐ ยท ((2 ยท ๐) + 1))))) |
291 | 185, 290 | eqtrd 2777 |
. . . . 5
โข (๐ โ โ โ
(((((๐ดโ๐)โ4) / ((๐ทโ๐)โ2)) ยท (((๐ธโ๐)โ4) ยท ((2โ(4 ยท ๐)) / ((๐ธโ(2 ยท ๐))โ2)))) / ((2 ยท ๐) + 1)) = ((((๐ดโ๐)โ4) / ((๐ทโ๐)โ2)) ยท ((๐โ2) / (๐ ยท ((2 ยท ๐) + 1))))) |
292 | 165, 169,
291 | 3eqtrd 2781 |
. . . 4
โข (๐ โ โ โ
((((((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4)) / ((๐ทโ๐)โ2)) ยท ((2โ(4 ยท
๐)) / ((๐ธโ(2 ยท ๐))โ2))) / ((2 ยท ๐) + 1)) = ((((๐ดโ๐)โ4) / ((๐ทโ๐)โ2)) ยท ((๐โ2) / (๐ ยท ((2 ยท ๐) + 1))))) |
293 | 142, 159,
292 | 3eqtrd 2781 |
. . 3
โข (๐ โ โ โ
((((2โ(4 ยท ๐))
ยท (((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4))) / (((๐ทโ๐)โ2) ยท ((๐ธโ(2 ยท ๐))โ2))) / ((2 ยท ๐) + 1)) = ((((๐ดโ๐)โ4) / ((๐ทโ๐)โ2)) ยท ((๐โ2) / (๐ ยท ((2 ยท ๐) + 1))))) |
294 | 293 | mpteq2ia 5213 |
. 2
โข (๐ โ โ โฆ
((((2โ(4 ยท ๐))
ยท (((๐ดโ๐)โ4) ยท ((๐ธโ๐)โ4))) / (((๐ทโ๐)โ2) ยท ((๐ธโ(2 ยท ๐))โ2))) / ((2 ยท ๐) + 1))) = (๐ โ โ โฆ ((((๐ดโ๐)โ4) / ((๐ทโ๐)โ2)) ยท ((๐โ2) / (๐ ยท ((2 ยท ๐) + 1))))) |
295 | 1, 136, 294 | 3eqtri 2769 |
1
โข ๐ = (๐ โ โ โฆ ((((๐ดโ๐)โ4) / ((๐ทโ๐)โ2)) ยท ((๐โ2) / (๐ ยท ((2 ยท ๐) + 1))))) |