Step | Hyp | Ref
| Expression |
1 | | nnre 12165 |
. . . . . 6
β’ (π β β β π β
β) |
2 | 1 | ad2antrr 725 |
. . . . 5
β’ (((π β β β§ π β β) β§ Β¬
(π mod (2 Β· Ο)) =
0) β π β
β) |
3 | | 1red 11161 |
. . . . . 6
β’ (((π β β β§ π β β) β§ Β¬
(π mod (2 Β· Ο)) =
0) β 1 β β) |
4 | 3 | rehalfcld 12405 |
. . . . 5
β’ (((π β β β§ π β β) β§ Β¬
(π mod (2 Β· Ο)) =
0) β (1 / 2) β β) |
5 | 2, 4 | readdcld 11189 |
. . . 4
β’ (((π β β β§ π β β) β§ Β¬
(π mod (2 Β· Ο)) =
0) β (π + (1 / 2))
β β) |
6 | | simplr 768 |
. . . 4
β’ (((π β β β§ π β β) β§ Β¬
(π mod (2 Β· Ο)) =
0) β π β
β) |
7 | 5, 6 | remulcld 11190 |
. . 3
β’ (((π β β β§ π β β) β§ Β¬
(π mod (2 Β· Ο)) =
0) β ((π + (1 / 2))
Β· π) β
β) |
8 | 7 | resincld 16030 |
. 2
β’ (((π β β β§ π β β) β§ Β¬
(π mod (2 Β· Ο)) =
0) β (sinβ((π +
(1 / 2)) Β· π))
β β) |
9 | | 2re 12232 |
. . . . 5
β’ 2 β
β |
10 | 9 | a1i 11 |
. . . 4
β’ (((π β β β§ π β β) β§ Β¬
(π mod (2 Β· Ο)) =
0) β 2 β β) |
11 | | pire 25831 |
. . . . 5
β’ Ο
β β |
12 | 11 | a1i 11 |
. . . 4
β’ (((π β β β§ π β β) β§ Β¬
(π mod (2 Β· Ο)) =
0) β Ο β β) |
13 | 10, 12 | remulcld 11190 |
. . 3
β’ (((π β β β§ π β β) β§ Β¬
(π mod (2 Β· Ο)) =
0) β (2 Β· Ο) β β) |
14 | 6 | rehalfcld 12405 |
. . . 4
β’ (((π β β β§ π β β) β§ Β¬
(π mod (2 Β· Ο)) =
0) β (π / 2) β
β) |
15 | 14 | resincld 16030 |
. . 3
β’ (((π β β β§ π β β) β§ Β¬
(π mod (2 Β· Ο)) =
0) β (sinβ(π /
2)) β β) |
16 | 13, 15 | remulcld 11190 |
. 2
β’ (((π β β β§ π β β) β§ Β¬
(π mod (2 Β· Ο)) =
0) β ((2 Β· Ο) Β· (sinβ(π / 2))) β β) |
17 | | 2cnd 12236 |
. . . . 5
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β 2 β β) |
18 | | picn 25832 |
. . . . . 6
β’ Ο
β β |
19 | 18 | a1i 11 |
. . . . 5
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β Ο β β) |
20 | 17, 19 | mulcld 11180 |
. . . 4
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β (2 Β· Ο) β β) |
21 | | recn 11146 |
. . . . . . 7
β’ (π β β β π β
β) |
22 | 21 | adantr 482 |
. . . . . 6
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β π β
β) |
23 | 22 | halfcld 12403 |
. . . . 5
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β (π / 2) β
β) |
24 | 23 | sincld 16017 |
. . . 4
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β (sinβ(π /
2)) β β) |
25 | | 2ne0 12262 |
. . . . . 6
β’ 2 β
0 |
26 | 25 | a1i 11 |
. . . . 5
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β 2 β 0) |
27 | | 0re 11162 |
. . . . . . 7
β’ 0 β
β |
28 | | pipos 25833 |
. . . . . . 7
β’ 0 <
Ο |
29 | 27, 28 | gtneii 11272 |
. . . . . 6
β’ Ο β
0 |
30 | 29 | a1i 11 |
. . . . 5
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β Ο β 0) |
31 | 17, 19, 26, 30 | mulne0d 11812 |
. . . 4
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β (2 Β· Ο) β 0) |
32 | 22, 17, 19, 26, 30 | divdiv1d 11967 |
. . . . . . 7
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β ((π / 2) / Ο)
= (π / (2 Β·
Ο))) |
33 | | simpr 486 |
. . . . . . . 8
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β Β¬ (π mod (2
Β· Ο)) = 0) |
34 | | 2rp 12925 |
. . . . . . . . . . 11
β’ 2 β
β+ |
35 | | pirp 25834 |
. . . . . . . . . . 11
β’ Ο
β β+ |
36 | | rpmulcl 12943 |
. . . . . . . . . . 11
β’ ((2
β β+ β§ Ο β β+) β (2
Β· Ο) β β+) |
37 | 34, 35, 36 | mp2an 691 |
. . . . . . . . . 10
β’ (2
Β· Ο) β β+ |
38 | | mod0 13787 |
. . . . . . . . . 10
β’ ((π β β β§ (2
Β· Ο) β β+) β ((π mod (2 Β· Ο)) = 0 β (π / (2 Β· Ο)) β
β€)) |
39 | 37, 38 | mpan2 690 |
. . . . . . . . 9
β’ (π β β β ((π mod (2 Β· Ο)) = 0
β (π / (2 Β·
Ο)) β β€)) |
40 | 39 | adantr 482 |
. . . . . . . 8
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β ((π mod (2
Β· Ο)) = 0 β (π / (2 Β· Ο)) β
β€)) |
41 | 33, 40 | mtbid 324 |
. . . . . . 7
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β Β¬ (π / (2
Β· Ο)) β β€) |
42 | 32, 41 | eqneltrd 2854 |
. . . . . 6
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β Β¬ ((π / 2) /
Ο) β β€) |
43 | | sineq0 25896 |
. . . . . . 7
β’ ((π / 2) β β β
((sinβ(π / 2)) = 0
β ((π / 2) / Ο)
β β€)) |
44 | 23, 43 | syl 17 |
. . . . . 6
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β ((sinβ(π /
2)) = 0 β ((π / 2) /
Ο) β β€)) |
45 | 42, 44 | mtbird 325 |
. . . . 5
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β Β¬ (sinβ(π / 2)) = 0) |
46 | 45 | neqned 2947 |
. . . 4
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β (sinβ(π /
2)) β 0) |
47 | 20, 24, 31, 46 | mulne0d 11812 |
. . 3
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β ((2 Β· Ο) Β· (sinβ(π / 2))) β 0) |
48 | 47 | adantll 713 |
. 2
β’ (((π β β β§ π β β) β§ Β¬
(π mod (2 Β· Ο)) =
0) β ((2 Β· Ο) Β· (sinβ(π / 2))) β 0) |
49 | 8, 16, 48 | redivcld 11988 |
1
β’ (((π β β β§ π β β) β§ Β¬
(π mod (2 Β· Ο)) =
0) β ((sinβ((π +
(1 / 2)) Β· π)) / ((2
Β· Ο) Β· (sinβ(π / 2)))) β β) |