Step | Hyp | Ref
| Expression |
1 | | 2re 12290 |
. . . . . . . 8
โข 2 โ
โ |
2 | | simpl 483 |
. . . . . . . 8
โข ((๐ โ โ โง ๐พ โ โค) โ ๐ โ
โ) |
3 | | nndivre 12257 |
. . . . . . . 8
โข ((2
โ โ โง ๐
โ โ) โ (2 / ๐) โ โ) |
4 | 1, 2, 3 | sylancr 587 |
. . . . . . 7
โข ((๐ โ โ โง ๐พ โ โค) โ (2 /
๐) โ
โ) |
5 | 4 | recnd 11246 |
. . . . . 6
โข ((๐ โ โ โง ๐พ โ โค) โ (2 /
๐) โ
โ) |
6 | | ax-icn 11171 |
. . . . . . . 8
โข i โ
โ |
7 | | picn 26193 |
. . . . . . . 8
โข ฯ
โ โ |
8 | 6, 7 | mulcli 11225 |
. . . . . . 7
โข (i
ยท ฯ) โ โ |
9 | 8 | a1i 11 |
. . . . . 6
โข ((๐ โ โ โง ๐พ โ โค) โ (i
ยท ฯ) โ โ) |
10 | 5, 9 | mulcld 11238 |
. . . . 5
โข ((๐ โ โ โง ๐พ โ โค) โ ((2 /
๐) ยท (i ยท
ฯ)) โ โ) |
11 | | efexp 16048 |
. . . . 5
โข ((((2 /
๐) ยท (i ยท
ฯ)) โ โ โง ๐พ โ โค) โ (expโ(๐พ ยท ((2 / ๐) ยท (i ยท ฯ))))
= ((expโ((2 / ๐)
ยท (i ยท ฯ)))โ๐พ)) |
12 | 10, 11 | sylancom 588 |
. . . 4
โข ((๐ โ โ โง ๐พ โ โค) โ
(expโ(๐พ ยท ((2
/ ๐) ยท (i ยท
ฯ)))) = ((expโ((2 / ๐) ยท (i ยท ฯ)))โ๐พ)) |
13 | | zcn 12567 |
. . . . . . . . 9
โข (๐พ โ โค โ ๐พ โ
โ) |
14 | 13 | adantl 482 |
. . . . . . . 8
โข ((๐ โ โ โง ๐พ โ โค) โ ๐พ โ
โ) |
15 | | nncn 12224 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
16 | 15 | adantr 481 |
. . . . . . . 8
โข ((๐ โ โ โง ๐พ โ โค) โ ๐ โ
โ) |
17 | | 2cn 12291 |
. . . . . . . . 9
โข 2 โ
โ |
18 | 17 | a1i 11 |
. . . . . . . 8
โข ((๐ โ โ โง ๐พ โ โค) โ 2 โ
โ) |
19 | | nnne0 12250 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ 0) |
20 | 19 | adantr 481 |
. . . . . . . 8
โข ((๐ โ โ โง ๐พ โ โค) โ ๐ โ 0) |
21 | 14, 16, 18, 20 | div32d 12017 |
. . . . . . 7
โข ((๐ โ โ โง ๐พ โ โค) โ ((๐พ / ๐) ยท 2) = (๐พ ยท (2 / ๐))) |
22 | 21 | oveq1d 7426 |
. . . . . 6
โข ((๐ โ โ โง ๐พ โ โค) โ (((๐พ / ๐) ยท 2) ยท (i ยท ฯ)) =
((๐พ ยท (2 / ๐)) ยท (i ยท
ฯ))) |
23 | 14, 16, 20 | divcld 11994 |
. . . . . . 7
โข ((๐ โ โ โง ๐พ โ โค) โ (๐พ / ๐) โ โ) |
24 | 23, 18, 9 | mulassd 11241 |
. . . . . 6
โข ((๐ โ โ โง ๐พ โ โค) โ (((๐พ / ๐) ยท 2) ยท (i ยท ฯ)) =
((๐พ / ๐) ยท (2 ยท (i ยท
ฯ)))) |
25 | 14, 5, 9 | mulassd 11241 |
. . . . . 6
โข ((๐ โ โ โง ๐พ โ โค) โ ((๐พ ยท (2 / ๐)) ยท (i ยท ฯ)) = (๐พ ยท ((2 / ๐) ยท (i ยท
ฯ)))) |
26 | 22, 24, 25 | 3eqtr3d 2780 |
. . . . 5
โข ((๐ โ โ โง ๐พ โ โค) โ ((๐พ / ๐) ยท (2 ยท (i ยท ฯ))) =
(๐พ ยท ((2 / ๐) ยท (i ยท
ฯ)))) |
27 | 26 | fveq2d 6895 |
. . . 4
โข ((๐ โ โ โง ๐พ โ โค) โ
(expโ((๐พ / ๐) ยท (2 ยท (i
ยท ฯ)))) = (expโ(๐พ ยท ((2 / ๐) ยท (i ยท
ฯ))))) |
28 | | neg1cn 12330 |
. . . . . . . 8
โข -1 โ
โ |
29 | 28 | a1i 11 |
. . . . . . 7
โข ((๐ โ โ โง ๐พ โ โค) โ -1
โ โ) |
30 | | neg1ne0 12332 |
. . . . . . . 8
โข -1 โ
0 |
31 | 30 | a1i 11 |
. . . . . . 7
โข ((๐ โ โ โง ๐พ โ โค) โ -1 โ
0) |
32 | 29, 31, 5 | cxpefd 26444 |
. . . . . 6
โข ((๐ โ โ โง ๐พ โ โค) โ
(-1โ๐(2 / ๐)) = (expโ((2 / ๐) ยท
(logโ-1)))) |
33 | | logm1 26321 |
. . . . . . . 8
โข
(logโ-1) = (i ยท ฯ) |
34 | 33 | oveq2i 7422 |
. . . . . . 7
โข ((2 /
๐) ยท (logโ-1))
= ((2 / ๐) ยท (i
ยท ฯ)) |
35 | 34 | fveq2i 6894 |
. . . . . 6
โข
(expโ((2 / ๐)
ยท (logโ-1))) = (expโ((2 / ๐) ยท (i ยท
ฯ))) |
36 | 32, 35 | eqtrdi 2788 |
. . . . 5
โข ((๐ โ โ โง ๐พ โ โค) โ
(-1โ๐(2 / ๐)) = (expโ((2 / ๐) ยท (i ยท
ฯ)))) |
37 | 36 | oveq1d 7426 |
. . . 4
โข ((๐ โ โ โง ๐พ โ โค) โ
((-1โ๐(2 / ๐))โ๐พ) = ((expโ((2 / ๐) ยท (i ยท ฯ)))โ๐พ)) |
38 | 12, 27, 37 | 3eqtr4rd 2783 |
. . 3
โข ((๐ โ โ โง ๐พ โ โค) โ
((-1โ๐(2 / ๐))โ๐พ) = (expโ((๐พ / ๐) ยท (2 ยท (i ยท
ฯ))))) |
39 | 38 | eqeq1d 2734 |
. 2
โข ((๐ โ โ โง ๐พ โ โค) โ
(((-1โ๐(2 / ๐))โ๐พ) = 1 โ (expโ((๐พ / ๐) ยท (2 ยท (i ยท ฯ))))
= 1)) |
40 | 17, 8 | mulcli 11225 |
. . . 4
โข (2
ยท (i ยท ฯ)) โ โ |
41 | | mulcl 11196 |
. . . 4
โข (((๐พ / ๐) โ โ โง (2 ยท (i
ยท ฯ)) โ โ) โ ((๐พ / ๐) ยท (2 ยท (i ยท ฯ)))
โ โ) |
42 | 23, 40, 41 | sylancl 586 |
. . 3
โข ((๐ โ โ โง ๐พ โ โค) โ ((๐พ / ๐) ยท (2 ยท (i ยท ฯ)))
โ โ) |
43 | | efeq1 26261 |
. . 3
โข (((๐พ / ๐) ยท (2 ยท (i ยท ฯ)))
โ โ โ ((expโ((๐พ / ๐) ยท (2 ยท (i ยท ฯ))))
= 1 โ (((๐พ / ๐) ยท (2 ยท (i
ยท ฯ))) / (i ยท (2 ยท ฯ))) โ
โค)) |
44 | 42, 43 | syl 17 |
. 2
โข ((๐ โ โ โง ๐พ โ โค) โ
((expโ((๐พ / ๐) ยท (2 ยท (i
ยท ฯ)))) = 1 โ (((๐พ / ๐) ยท (2 ยท (i ยท ฯ))) /
(i ยท (2 ยท ฯ))) โ โค)) |
45 | 6, 17, 7 | mul12i 11413 |
. . . . . 6
โข (i
ยท (2 ยท ฯ)) = (2 ยท (i ยท ฯ)) |
46 | 45 | oveq2i 7422 |
. . . . 5
โข (((๐พ / ๐) ยท (2 ยท (i ยท ฯ))) /
(i ยท (2 ยท ฯ))) = (((๐พ / ๐) ยท (2 ยท (i ยท ฯ))) /
(2 ยท (i ยท ฯ))) |
47 | 40 | a1i 11 |
. . . . . 6
โข ((๐ โ โ โง ๐พ โ โค) โ (2
ยท (i ยท ฯ)) โ โ) |
48 | | 2ne0 12320 |
. . . . . . . 8
โข 2 โ
0 |
49 | | ine0 11653 |
. . . . . . . . 9
โข i โ
0 |
50 | | pire 26192 |
. . . . . . . . . 10
โข ฯ
โ โ |
51 | | pipos 26194 |
. . . . . . . . . 10
โข 0 <
ฯ |
52 | 50, 51 | gt0ne0ii 11754 |
. . . . . . . . 9
โข ฯ โ
0 |
53 | 6, 7, 49, 52 | mulne0i 11861 |
. . . . . . . 8
โข (i
ยท ฯ) โ 0 |
54 | 17, 8, 48, 53 | mulne0i 11861 |
. . . . . . 7
โข (2
ยท (i ยท ฯ)) โ 0 |
55 | 54 | a1i 11 |
. . . . . 6
โข ((๐ โ โ โง ๐พ โ โค) โ (2
ยท (i ยท ฯ)) โ 0) |
56 | 23, 47, 55 | divcan4d 12000 |
. . . . 5
โข ((๐ โ โ โง ๐พ โ โค) โ (((๐พ / ๐) ยท (2 ยท (i ยท ฯ))) /
(2 ยท (i ยท ฯ))) = (๐พ / ๐)) |
57 | 46, 56 | eqtrid 2784 |
. . . 4
โข ((๐ โ โ โง ๐พ โ โค) โ (((๐พ / ๐) ยท (2 ยท (i ยท ฯ))) /
(i ยท (2 ยท ฯ))) = (๐พ / ๐)) |
58 | 57 | eleq1d 2818 |
. . 3
โข ((๐ โ โ โง ๐พ โ โค) โ
((((๐พ / ๐) ยท (2 ยท (i ยท ฯ))) /
(i ยท (2 ยท ฯ))) โ โค โ (๐พ / ๐) โ โค)) |
59 | | nnz 12583 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โค) |
60 | 59 | adantr 481 |
. . . 4
โข ((๐ โ โ โง ๐พ โ โค) โ ๐ โ
โค) |
61 | | simpr 485 |
. . . 4
โข ((๐ โ โ โง ๐พ โ โค) โ ๐พ โ
โค) |
62 | | dvdsval2 16204 |
. . . 4
โข ((๐ โ โค โง ๐ โ 0 โง ๐พ โ โค) โ (๐ โฅ ๐พ โ (๐พ / ๐) โ โค)) |
63 | 60, 20, 61, 62 | syl3anc 1371 |
. . 3
โข ((๐ โ โ โง ๐พ โ โค) โ (๐ โฅ ๐พ โ (๐พ / ๐) โ โค)) |
64 | 58, 63 | bitr4d 281 |
. 2
โข ((๐ โ โ โง ๐พ โ โค) โ
((((๐พ / ๐) ยท (2 ยท (i ยท ฯ))) /
(i ยท (2 ยท ฯ))) โ โค โ ๐ โฅ ๐พ)) |
65 | 39, 44, 64 | 3bitrd 304 |
1
โข ((๐ โ โ โง ๐พ โ โค) โ
(((-1โ๐(2 / ๐))โ๐พ) = 1 โ ๐ โฅ ๐พ)) |