Step | Hyp | Ref
| Expression |
1 | | 2nn 12233 |
. . . . . 6
β’ 2 β
β |
2 | | nnmulcl 12184 |
. . . . . 6
β’ ((2
β β β§ π
β β) β (2 Β· π) β β) |
3 | 1, 2 | mpan 689 |
. . . . 5
β’ (π β β β (2
Β· π) β
β) |
4 | 3 | nnred 12175 |
. . . 4
β’ (π β β β (2
Β· π) β
β) |
5 | | peano2rem 11475 |
. . . 4
β’ ((2
Β· π) β β
β ((2 Β· π)
β 1) β β) |
6 | 4, 5 | syl 17 |
. . 3
β’ (π β β β ((2
Β· π) β 1)
β β) |
7 | | chtcl 26474 |
. . 3
β’ (((2
Β· π) β 1)
β β β (ΞΈβ((2 Β· π) β 1)) β
β) |
8 | 6, 7 | syl 17 |
. 2
β’ (π β β β
(ΞΈβ((2 Β· π) β 1)) β
β) |
9 | | nnre 12167 |
. . . 4
β’ (π β β β π β
β) |
10 | | chtcl 26474 |
. . . 4
β’ (π β β β
(ΞΈβπ) β
β) |
11 | 9, 10 | syl 17 |
. . 3
β’ (π β β β
(ΞΈβπ) β
β) |
12 | | nnnn0 12427 |
. . . . . . 7
β’ (π β β β π β
β0) |
13 | | 2m1e1 12286 |
. . . . . . . . . . 11
β’ (2
β 1) = 1 |
14 | 13 | oveq2i 7373 |
. . . . . . . . . 10
β’ ((2
Β· π) β (2
β 1)) = ((2 Β· π) β 1) |
15 | 3 | nncnd 12176 |
. . . . . . . . . . . 12
β’ (π β β β (2
Β· π) β
β) |
16 | | 2cn 12235 |
. . . . . . . . . . . . 13
β’ 2 β
β |
17 | | ax-1cn 11116 |
. . . . . . . . . . . . 13
β’ 1 β
β |
18 | | subsub 11438 |
. . . . . . . . . . . . 13
β’ (((2
Β· π) β β
β§ 2 β β β§ 1 β β) β ((2 Β· π) β (2 β 1)) = (((2
Β· π) β 2) +
1)) |
19 | 16, 17, 18 | mp3an23 1454 |
. . . . . . . . . . . 12
β’ ((2
Β· π) β β
β ((2 Β· π)
β (2 β 1)) = (((2 Β· π) β 2) + 1)) |
20 | 15, 19 | syl 17 |
. . . . . . . . . . 11
β’ (π β β β ((2
Β· π) β (2
β 1)) = (((2 Β· π) β 2) + 1)) |
21 | | nncn 12168 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β) |
22 | | subdi 11595 |
. . . . . . . . . . . . . . 15
β’ ((2
β β β§ π
β β β§ 1 β β) β (2 Β· (π β 1)) = ((2 Β· π) β (2 Β·
1))) |
23 | 16, 17, 22 | mp3an13 1453 |
. . . . . . . . . . . . . 14
β’ (π β β β (2
Β· (π β 1)) =
((2 Β· π) β (2
Β· 1))) |
24 | 21, 23 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β β β (2
Β· (π β 1)) =
((2 Β· π) β (2
Β· 1))) |
25 | | 2t1e2 12323 |
. . . . . . . . . . . . . 14
β’ (2
Β· 1) = 2 |
26 | 25 | oveq2i 7373 |
. . . . . . . . . . . . 13
β’ ((2
Β· π) β (2
Β· 1)) = ((2 Β· π) β 2) |
27 | 24, 26 | eqtrdi 2793 |
. . . . . . . . . . . 12
β’ (π β β β (2
Β· (π β 1)) =
((2 Β· π) β
2)) |
28 | 27 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (π β β β ((2
Β· (π β 1)) +
1) = (((2 Β· π)
β 2) + 1)) |
29 | 20, 28 | eqtr4d 2780 |
. . . . . . . . . 10
β’ (π β β β ((2
Β· π) β (2
β 1)) = ((2 Β· (π β 1)) + 1)) |
30 | 14, 29 | eqtr3id 2791 |
. . . . . . . . 9
β’ (π β β β ((2
Β· π) β 1) =
((2 Β· (π β 1))
+ 1)) |
31 | | 2nn0 12437 |
. . . . . . . . . . 11
β’ 2 β
β0 |
32 | | nnm1nn0 12461 |
. . . . . . . . . . 11
β’ (π β β β (π β 1) β
β0) |
33 | | nn0mulcl 12456 |
. . . . . . . . . . 11
β’ ((2
β β0 β§ (π β 1) β β0)
β (2 Β· (π
β 1)) β β0) |
34 | 31, 32, 33 | sylancr 588 |
. . . . . . . . . 10
β’ (π β β β (2
Β· (π β 1))
β β0) |
35 | | nn0p1nn 12459 |
. . . . . . . . . 10
β’ ((2
Β· (π β 1))
β β0 β ((2 Β· (π β 1)) + 1) β
β) |
36 | 34, 35 | syl 17 |
. . . . . . . . 9
β’ (π β β β ((2
Β· (π β 1)) +
1) β β) |
37 | 30, 36 | eqeltrd 2838 |
. . . . . . . 8
β’ (π β β β ((2
Β· π) β 1)
β β) |
38 | | nnnn0 12427 |
. . . . . . . 8
β’ (((2
Β· π) β 1)
β β β ((2 Β· π) β 1) β
β0) |
39 | 37, 38 | syl 17 |
. . . . . . 7
β’ (π β β β ((2
Β· π) β 1)
β β0) |
40 | | 1re 11162 |
. . . . . . . . . . 11
β’ 1 β
β |
41 | 40 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β 1 β
β) |
42 | | nnge1 12188 |
. . . . . . . . . 10
β’ (π β β β 1 β€
π) |
43 | 41, 9, 9, 42 | leadd2dd 11777 |
. . . . . . . . 9
β’ (π β β β (π + 1) β€ (π + π)) |
44 | 21 | 2timesd 12403 |
. . . . . . . . 9
β’ (π β β β (2
Β· π) = (π + π)) |
45 | 43, 44 | breqtrrd 5138 |
. . . . . . . 8
β’ (π β β β (π + 1) β€ (2 Β· π)) |
46 | | leaddsub 11638 |
. . . . . . . . 9
β’ ((π β β β§ 1 β
β β§ (2 Β· π) β β) β ((π + 1) β€ (2 Β· π) β π β€ ((2 Β· π) β 1))) |
47 | 9, 41, 4, 46 | syl3anc 1372 |
. . . . . . . 8
β’ (π β β β ((π + 1) β€ (2 Β· π) β π β€ ((2 Β· π) β 1))) |
48 | 45, 47 | mpbid 231 |
. . . . . . 7
β’ (π β β β π β€ ((2 Β· π) β 1)) |
49 | | elfz2nn0 13539 |
. . . . . . 7
β’ (π β (0...((2 Β· π) β 1)) β (π β β0
β§ ((2 Β· π)
β 1) β β0 β§ π β€ ((2 Β· π) β 1))) |
50 | 12, 39, 48, 49 | syl3anbrc 1344 |
. . . . . 6
β’ (π β β β π β (0...((2 Β· π) β 1))) |
51 | | bccl2 14230 |
. . . . . 6
β’ (π β (0...((2 Β· π) β 1)) β (((2
Β· π) β
1)Cπ) β
β) |
52 | 50, 51 | syl 17 |
. . . . 5
β’ (π β β β (((2
Β· π) β
1)Cπ) β
β) |
53 | 52 | nnrpd 12962 |
. . . 4
β’ (π β β β (((2
Β· π) β
1)Cπ) β
β+) |
54 | 53 | relogcld 25994 |
. . 3
β’ (π β β β
(logβ(((2 Β· π)
β 1)Cπ)) β
β) |
55 | 11, 54 | readdcld 11191 |
. 2
β’ (π β β β
((ΞΈβπ) +
(logβ(((2 Β· π)
β 1)Cπ))) β
β) |
56 | | 4re 12244 |
. . . . . 6
β’ 4 β
β |
57 | | 4pos 12267 |
. . . . . 6
β’ 0 <
4 |
58 | 56, 57 | elrpii 12925 |
. . . . 5
β’ 4 β
β+ |
59 | | relogcl 25947 |
. . . . 5
β’ (4 β
β+ β (logβ4) β β) |
60 | 58, 59 | ax-mp 5 |
. . . 4
β’
(logβ4) β β |
61 | 32 | nn0red 12481 |
. . . 4
β’ (π β β β (π β 1) β
β) |
62 | | remulcl 11143 |
. . . 4
β’
(((logβ4) β β β§ (π β 1) β β) β
((logβ4) Β· (π
β 1)) β β) |
63 | 60, 61, 62 | sylancr 588 |
. . 3
β’ (π β β β
((logβ4) Β· (π
β 1)) β β) |
64 | 11, 63 | readdcld 11191 |
. 2
β’ (π β β β
((ΞΈβπ) +
((logβ4) Β· (π
β 1))) β β) |
65 | | iftrue 4497 |
. . . . . . . . . . . 12
β’ (π β€ ((2 Β· π) β 1) β if(π β€ ((2 Β· π) β 1), 1, 0) =
1) |
66 | 65 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β β β§ π β β) β§ π β€ ((2 Β· π) β 1)) β if(π β€ ((2 Β· π) β 1), 1, 0) =
1) |
67 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β) β π β
β) |
68 | 52 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β) β (((2
Β· π) β
1)Cπ) β
β) |
69 | 67, 68 | pccld 16729 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β) β (π pCnt (((2 Β· π) β 1)Cπ)) β
β0) |
70 | | nn0addge1 12466 |
. . . . . . . . . . . . . . 15
β’ ((1
β β β§ (π
pCnt (((2 Β· π)
β 1)Cπ)) β
β0) β 1 β€ (1 + (π pCnt (((2 Β· π) β 1)Cπ)))) |
71 | 40, 69, 70 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β) β 1 β€
(1 + (π pCnt (((2 Β·
π) β 1)Cπ)))) |
72 | | iftrue 4497 |
. . . . . . . . . . . . . . . 16
β’ (π β€ π β if(π β€ π, 1, 0) = 1) |
73 | 72 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
β’ (π β€ π β (if(π β€ π, 1, 0) + (π pCnt (((2 Β· π) β 1)Cπ))) = (1 + (π pCnt (((2 Β· π) β 1)Cπ)))) |
74 | 73 | breq2d 5122 |
. . . . . . . . . . . . . 14
β’ (π β€ π β (1 β€ (if(π β€ π, 1, 0) + (π pCnt (((2 Β· π) β 1)Cπ))) β 1 β€ (1 + (π pCnt (((2 Β· π) β 1)Cπ))))) |
75 | 71, 74 | syl5ibrcom 247 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β) β (π β€ π β 1 β€ (if(π β€ π, 1, 0) + (π pCnt (((2 Β· π) β 1)Cπ))))) |
76 | 75 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β β β§ π β β) β§ π β€ ((2 Β· π) β 1)) β (π β€ π β 1 β€ (if(π β€ π, 1, 0) + (π pCnt (((2 Β· π) β 1)Cπ))))) |
77 | | prmnn 16557 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β π β
β) |
78 | 77 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β π β β) |
79 | | simprl 770 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β π β€ ((2 Β· π) β 1)) |
80 | | prmz 16558 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β π β
β€) |
81 | 37 | nnzd 12533 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β ((2
Β· π) β 1)
β β€) |
82 | | eluz 12784 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β€ β§ ((2
Β· π) β 1)
β β€) β (((2 Β· π) β 1) β
(β€β₯βπ) β π β€ ((2 Β· π) β 1))) |
83 | 80, 81, 82 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β) β (((2
Β· π) β 1)
β (β€β₯βπ) β π β€ ((2 Β· π) β 1))) |
84 | 83 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β (((2 Β· π) β 1) β
(β€β₯βπ) β π β€ ((2 Β· π) β 1))) |
85 | 79, 84 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β ((2 Β· π) β 1) β
(β€β₯βπ)) |
86 | | dvdsfac 16215 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ ((2
Β· π) β 1)
β (β€β₯βπ)) β π β₯ (!β((2 Β· π) β 1))) |
87 | 78, 85, 86 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β π β₯ (!β((2 Β· π) β 1))) |
88 | | id 22 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β π β
β) |
89 | 39 | faccld 14191 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β
(!β((2 Β· π)
β 1)) β β) |
90 | | pcelnn 16749 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§
(!β((2 Β· π)
β 1)) β β) β ((π pCnt (!β((2 Β· π) β 1))) β β β π β₯ (!β((2 Β·
π) β
1)))) |
91 | 88, 89, 90 | syl2anr 598 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β β) β ((π pCnt (!β((2 Β·
π) β 1))) β
β β π β₯
(!β((2 Β· π)
β 1)))) |
92 | 91 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β ((π pCnt (!β((2 Β· π) β 1))) β β β π β₯ (!β((2 Β·
π) β
1)))) |
93 | 87, 92 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β (π pCnt (!β((2 Β· π) β 1))) β
β) |
94 | 93 | nnge1d 12208 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β 1 β€ (π pCnt (!β((2 Β· π) β 1)))) |
95 | | iffalse 4500 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
π β€ π β if(π β€ π, 1, 0) = 0) |
96 | 95 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
π β€ π β (if(π β€ π, 1, 0) + (π pCnt (((2 Β· π) β 1)Cπ))) = (0 + (π pCnt (((2 Β· π) β 1)Cπ)))) |
97 | 96 | ad2antll 728 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β (if(π β€ π, 1, 0) + (π pCnt (((2 Β· π) β 1)Cπ))) = (0 + (π pCnt (((2 Β· π) β 1)Cπ)))) |
98 | 69 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β β) β (π pCnt (((2 Β· π) β 1)Cπ)) β β) |
99 | 98 | addid2d 11363 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β) β (0 +
(π pCnt (((2 Β· π) β 1)Cπ))) = (π pCnt (((2 Β· π) β 1)Cπ))) |
100 | 99 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β (0 + (π pCnt (((2 Β· π) β 1)Cπ))) = (π pCnt (((2 Β· π) β 1)Cπ))) |
101 | | bcval2 14212 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (0...((2 Β· π) β 1)) β (((2
Β· π) β
1)Cπ) = ((!β((2
Β· π) β 1)) /
((!β(((2 Β· π)
β 1) β π))
Β· (!βπ)))) |
102 | 50, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β (((2
Β· π) β
1)Cπ) = ((!β((2
Β· π) β 1)) /
((!β(((2 Β· π)
β 1) β π))
Β· (!βπ)))) |
103 | 32 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β (π β 1) β
β) |
104 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β β 1 β
β) |
105 | 44 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β β ((2
Β· π) β 1) =
((π + π) β 1)) |
106 | 21, 21, 104, 105 | assraddsubd 11576 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β ((2
Β· π) β 1) =
(π + (π β 1))) |
107 | 21, 103, 106 | mvrladdd 11575 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β (((2
Β· π) β 1)
β π) = (π β 1)) |
108 | 107 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β
(!β(((2 Β· π)
β 1) β π)) =
(!β(π β
1))) |
109 | 108 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β β
((!β(((2 Β· π)
β 1) β π))
Β· (!βπ)) =
((!β(π β 1))
Β· (!βπ))) |
110 | 109 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β
((!β((2 Β· π)
β 1)) / ((!β(((2 Β· π) β 1) β π)) Β· (!βπ))) = ((!β((2 Β· π) β 1)) / ((!β(π β 1)) Β·
(!βπ)))) |
111 | 102, 110 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β (((2
Β· π) β
1)Cπ) = ((!β((2
Β· π) β 1)) /
((!β(π β 1))
Β· (!βπ)))) |
112 | 111 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β) β (((2
Β· π) β
1)Cπ) = ((!β((2
Β· π) β 1)) /
((!β(π β 1))
Β· (!βπ)))) |
113 | 112 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β β) β (π pCnt (((2 Β· π) β 1)Cπ)) = (π pCnt ((!β((2 Β· π) β 1)) / ((!β(π β 1)) Β·
(!βπ))))) |
114 | | nnz 12527 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((!β((2 Β· π) β 1)) β β β
(!β((2 Β· π)
β 1)) β β€) |
115 | | nnne0 12194 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((!β((2 Β· π) β 1)) β β β
(!β((2 Β· π)
β 1)) β 0) |
116 | 114, 115 | jca 513 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((!β((2 Β· π) β 1)) β β β
((!β((2 Β· π)
β 1)) β β€ β§ (!β((2 Β· π) β 1)) β 0)) |
117 | 89, 116 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β
((!β((2 Β· π)
β 1)) β β€ β§ (!β((2 Β· π) β 1)) β 0)) |
118 | 117 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β) β
((!β((2 Β· π)
β 1)) β β€ β§ (!β((2 Β· π) β 1)) β 0)) |
119 | 32 | faccld 14191 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β
(!β(π β 1))
β β) |
120 | 12 | faccld 14191 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β
(!βπ) β
β) |
121 | 119, 120 | nnmulcld 12213 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β
((!β(π β 1))
Β· (!βπ))
β β) |
122 | 121 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β) β
((!β(π β 1))
Β· (!βπ))
β β) |
123 | | pcdiv 16731 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§
((!β((2 Β· π)
β 1)) β β€ β§ (!β((2 Β· π) β 1)) β 0) β§ ((!β(π β 1)) Β·
(!βπ)) β
β) β (π pCnt
((!β((2 Β· π)
β 1)) / ((!β(π
β 1)) Β· (!βπ)))) = ((π pCnt (!β((2 Β· π) β 1))) β (π pCnt ((!β(π β 1)) Β· (!βπ))))) |
124 | 67, 118, 122, 123 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β β) β (π pCnt ((!β((2 Β·
π) β 1)) /
((!β(π β 1))
Β· (!βπ)))) =
((π pCnt (!β((2
Β· π) β 1)))
β (π pCnt
((!β(π β 1))
Β· (!βπ))))) |
125 | | nnz 12527 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((!β(π β
1)) β β β (!β(π β 1)) β
β€) |
126 | | nnne0 12194 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((!β(π β
1)) β β β (!β(π β 1)) β 0) |
127 | 125, 126 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((!β(π β
1)) β β β ((!β(π β 1)) β β€ β§
(!β(π β 1))
β 0)) |
128 | 119, 127 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β
((!β(π β 1))
β β€ β§ (!β(π β 1)) β 0)) |
129 | 128 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ π β β) β
((!β(π β 1))
β β€ β§ (!β(π β 1)) β 0)) |
130 | | nnz 12527 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((!βπ) β
β β (!βπ)
β β€) |
131 | | nnne0 12194 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((!βπ) β
β β (!βπ)
β 0) |
132 | 130, 131 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((!βπ) β
β β ((!βπ)
β β€ β§ (!βπ) β 0)) |
133 | 120, 132 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β
((!βπ) β β€
β§ (!βπ) β
0)) |
134 | 133 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ π β β) β
((!βπ) β β€
β§ (!βπ) β
0)) |
135 | | pcmul 16730 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§
((!β(π β 1))
β β€ β§ (!β(π β 1)) β 0) β§ ((!βπ) β β€ β§
(!βπ) β 0)) β
(π pCnt ((!β(π β 1)) Β·
(!βπ))) = ((π pCnt (!β(π β 1))) + (π pCnt (!βπ)))) |
136 | 67, 129, 134, 135 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β) β (π pCnt ((!β(π β 1)) Β·
(!βπ))) = ((π pCnt (!β(π β 1))) + (π pCnt (!βπ)))) |
137 | 136 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β β) β ((π pCnt (!β((2 Β·
π) β 1))) β
(π pCnt ((!β(π β 1)) Β·
(!βπ)))) = ((π pCnt (!β((2 Β·
π) β 1))) β
((π pCnt (!β(π β 1))) + (π pCnt (!βπ))))) |
138 | 113, 124,
137 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β β) β (π pCnt (((2 Β· π) β 1)Cπ)) = ((π pCnt (!β((2 Β· π) β 1))) β ((π pCnt (!β(π β 1))) + (π pCnt (!βπ))))) |
139 | 138 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β (π pCnt (((2 Β· π) β 1)Cπ)) = ((π pCnt (!β((2 Β· π) β 1))) β ((π pCnt (!β(π β 1))) + (π pCnt (!βπ))))) |
140 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β Β¬ π β€ π) |
141 | | prmfac1 16604 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β β0
β§ π β β
β§ π β₯
(!βπ)) β π β€ π) |
142 | 141 | 3expia 1122 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β β0
β§ π β β)
β (π β₯
(!βπ) β π β€ π)) |
143 | 12, 142 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ π β β) β (π β₯ (!βπ) β π β€ π)) |
144 | 143 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β (π β₯ (!βπ) β π β€ π)) |
145 | 140, 144 | mtod 197 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β Β¬ π β₯ (!βπ)) |
146 | 80 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β β β§ π β β) β π β
β€) |
147 | 129 | simpld 496 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β β β§ π β β) β
(!β(π β 1))
β β€) |
148 | | nnz 12527 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β π β
β€) |
149 | 148 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β β β§ π β β) β π β
β€) |
150 | | dvdsmultr1 16185 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β β€ β§
(!β(π β 1))
β β€ β§ π
β β€) β (π
β₯ (!β(π β
1)) β π β₯
((!β(π β 1))
Β· π))) |
151 | 146, 147,
149, 150 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ π β β) β (π β₯ (!β(π β 1)) β π β₯ ((!β(π β 1)) Β· π))) |
152 | | facnn2 14189 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β
(!βπ) =
((!β(π β 1))
Β· π)) |
153 | 152 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β β β§ π β β) β
(!βπ) =
((!β(π β 1))
Β· π)) |
154 | 153 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ π β β) β (π β₯ (!βπ) β π β₯ ((!β(π β 1)) Β· π))) |
155 | 151, 154 | sylibrd 259 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β β§ π β β) β (π β₯ (!β(π β 1)) β π β₯ (!βπ))) |
156 | 155 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β (π β₯ (!β(π β 1)) β π β₯ (!βπ))) |
157 | 145, 156 | mtod 197 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β Β¬ π β₯ (!β(π β 1))) |
158 | | pceq0 16750 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β β§
(!β(π β 1))
β β) β ((π
pCnt (!β(π β
1))) = 0 β Β¬ π
β₯ (!β(π β
1)))) |
159 | 88, 119, 158 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§ π β β) β ((π pCnt (!β(π β 1))) = 0 β Β¬
π β₯ (!β(π β 1)))) |
160 | 159 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β ((π pCnt (!β(π β 1))) = 0 β Β¬ π β₯ (!β(π β 1)))) |
161 | 157, 160 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β (π pCnt (!β(π β 1))) = 0) |
162 | | pceq0 16750 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β β§
(!βπ) β β)
β ((π pCnt
(!βπ)) = 0 β
Β¬ π β₯
(!βπ))) |
163 | 88, 120, 162 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§ π β β) β ((π pCnt (!βπ)) = 0 β Β¬ π β₯ (!βπ))) |
164 | 163 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β ((π pCnt (!βπ)) = 0 β Β¬ π β₯ (!βπ))) |
165 | 145, 164 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β (π pCnt (!βπ)) = 0) |
166 | 161, 165 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β ((π pCnt (!β(π β 1))) + (π pCnt (!βπ))) = (0 + 0)) |
167 | | 00id 11337 |
. . . . . . . . . . . . . . . . . 18
β’ (0 + 0) =
0 |
168 | 166, 167 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β ((π pCnt (!β(π β 1))) + (π pCnt (!βπ))) = 0) |
169 | 168 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β ((π pCnt (!β((2 Β· π) β 1))) β ((π pCnt (!β(π β 1))) + (π pCnt (!βπ)))) = ((π pCnt (!β((2 Β· π) β 1))) β 0)) |
170 | | pccl 16728 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§
(!β((2 Β· π)
β 1)) β β) β (π pCnt (!β((2 Β· π) β 1))) β
β0) |
171 | 88, 89, 170 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β) β (π pCnt (!β((2 Β·
π) β 1))) β
β0) |
172 | 171 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β β) β (π pCnt (!β((2 Β·
π) β 1))) β
β) |
173 | 172 | subid1d 11508 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β β) β ((π pCnt (!β((2 Β·
π) β 1))) β 0)
= (π pCnt (!β((2
Β· π) β
1)))) |
174 | 173 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β ((π pCnt (!β((2 Β· π) β 1))) β 0) = (π pCnt (!β((2 Β·
π) β
1)))) |
175 | 139, 169,
174 | 3eqtrd 2781 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β (π pCnt (((2 Β· π) β 1)Cπ)) = (π pCnt (!β((2 Β· π) β 1)))) |
176 | 97, 100, 175 | 3eqtrd 2781 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β (if(π β€ π, 1, 0) + (π pCnt (((2 Β· π) β 1)Cπ))) = (π pCnt (!β((2 Β· π) β 1)))) |
177 | 94, 176 | breqtrrd 5138 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β β) β§ (π β€ ((2 Β· π) β 1) β§ Β¬ π β€ π)) β 1 β€ (if(π β€ π, 1, 0) + (π pCnt (((2 Β· π) β 1)Cπ)))) |
178 | 177 | expr 458 |
. . . . . . . . . . . 12
β’ (((π β β β§ π β β) β§ π β€ ((2 Β· π) β 1)) β (Β¬
π β€ π β 1 β€ (if(π β€ π, 1, 0) + (π pCnt (((2 Β· π) β 1)Cπ))))) |
179 | 76, 178 | pm2.61d 179 |
. . . . . . . . . . 11
β’ (((π β β β§ π β β) β§ π β€ ((2 Β· π) β 1)) β 1 β€
(if(π β€ π, 1, 0) + (π pCnt (((2 Β· π) β 1)Cπ)))) |
180 | 66, 179 | eqbrtrd 5132 |
. . . . . . . . . 10
β’ (((π β β β§ π β β) β§ π β€ ((2 Β· π) β 1)) β if(π β€ ((2 Β· π) β 1), 1, 0) β€
(if(π β€ π, 1, 0) + (π pCnt (((2 Β· π) β 1)Cπ)))) |
181 | 180 | ex 414 |
. . . . . . . . 9
β’ ((π β β β§ π β β) β (π β€ ((2 Β· π) β 1) β if(π β€ ((2 Β· π) β 1), 1, 0) β€
(if(π β€ π, 1, 0) + (π pCnt (((2 Β· π) β 1)Cπ))))) |
182 | | 1nn0 12436 |
. . . . . . . . . . . . 13
β’ 1 β
β0 |
183 | | 0nn0 12435 |
. . . . . . . . . . . . 13
β’ 0 β
β0 |
184 | 182, 183 | ifcli 4538 |
. . . . . . . . . . . 12
β’ if(π β€ π, 1, 0) β
β0 |
185 | | nn0addcl 12455 |
. . . . . . . . . . . 12
β’
((if(π β€ π, 1, 0) β
β0 β§ (π pCnt (((2 Β· π) β 1)Cπ)) β β0) β
(if(π β€ π, 1, 0) + (π pCnt (((2 Β· π) β 1)Cπ))) β
β0) |
186 | 184, 69, 185 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β) β
(if(π β€ π, 1, 0) + (π pCnt (((2 Β· π) β 1)Cπ))) β
β0) |
187 | 186 | nn0ge0d 12483 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β 0 β€
(if(π β€ π, 1, 0) + (π pCnt (((2 Β· π) β 1)Cπ)))) |
188 | | iffalse 4500 |
. . . . . . . . . . 11
β’ (Β¬
π β€ ((2 Β· π) β 1) β if(π β€ ((2 Β· π) β 1), 1, 0) =
0) |
189 | 188 | breq1d 5120 |
. . . . . . . . . 10
β’ (Β¬
π β€ ((2 Β· π) β 1) β (if(π β€ ((2 Β· π) β 1), 1, 0) β€
(if(π β€ π, 1, 0) + (π pCnt (((2 Β· π) β 1)Cπ))) β 0 β€ (if(π β€ π, 1, 0) + (π pCnt (((2 Β· π) β 1)Cπ))))) |
190 | 187, 189 | syl5ibrcom 247 |
. . . . . . . . 9
β’ ((π β β β§ π β β) β (Β¬
π β€ ((2 Β· π) β 1) β if(π β€ ((2 Β· π) β 1), 1, 0) β€
(if(π β€ π, 1, 0) + (π pCnt (((2 Β· π) β 1)Cπ))))) |
191 | 181, 190 | pm2.61d 179 |
. . . . . . . 8
β’ ((π β β β§ π β β) β if(π β€ ((2 Β· π) β 1), 1, 0) β€
(if(π β€ π, 1, 0) + (π pCnt (((2 Β· π) β 1)Cπ)))) |
192 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (π β β β¦ if(π β β, π, 1)) = (π β β β¦ if(π β β, π, 1)) |
193 | 192 | prmorcht 26543 |
. . . . . . . . . . . 12
β’ (((2
Β· π) β 1)
β β β (expβ(ΞΈβ((2 Β· π) β 1))) = (seq1( Β· , (π β β β¦ if(π β β, π, 1)))β((2 Β· π) β 1))) |
194 | 37, 193 | syl 17 |
. . . . . . . . . . 11
β’ (π β β β
(expβ(ΞΈβ((2 Β· π) β 1))) = (seq1( Β· , (π β β β¦ if(π β β, π, 1)))β((2 Β· π) β 1))) |
195 | 194 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π β β β (π pCnt
(expβ(ΞΈβ((2 Β· π) β 1)))) = (π pCnt (seq1( Β· , (π β β β¦ if(π β β, π, 1)))β((2 Β· π) β 1)))) |
196 | 195 | adantr 482 |
. . . . . . . . 9
β’ ((π β β β§ π β β) β (π pCnt
(expβ(ΞΈβ((2 Β· π) β 1)))) = (π pCnt (seq1( Β· , (π β β β¦ if(π β β, π, 1)))β((2 Β· π) β 1)))) |
197 | | nncn 12168 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β) |
198 | 197 | exp1d 14053 |
. . . . . . . . . . . . 13
β’ (π β β β (πβ1) = π) |
199 | 198 | ifeq1d 4510 |
. . . . . . . . . . . 12
β’ (π β β β if(π β β, (πβ1), 1) = if(π β β, π, 1)) |
200 | 199 | mpteq2ia 5213 |
. . . . . . . . . . 11
β’ (π β β β¦ if(π β β, (πβ1), 1)) = (π β β β¦ if(π β β, π, 1)) |
201 | 200 | eqcomi 2746 |
. . . . . . . . . 10
β’ (π β β β¦ if(π β β, π, 1)) = (π β β β¦ if(π β β, (πβ1), 1)) |
202 | 182 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β β β§ π β β) β§ π β β) β 1 β
β0) |
203 | 202 | ralrimiva 3144 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β
βπ β β 1
β β0) |
204 | 37 | adantr 482 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β ((2
Β· π) β 1)
β β) |
205 | | eqidd 2738 |
. . . . . . . . . 10
β’ (π = π β 1 = 1) |
206 | 201, 203,
204, 67, 205 | pcmpt 16771 |
. . . . . . . . 9
β’ ((π β β β§ π β β) β (π pCnt (seq1( Β· , (π β β β¦ if(π β β, π, 1)))β((2 Β· π) β 1))) = if(π β€ ((2 Β· π) β 1), 1,
0)) |
207 | 196, 206 | eqtrd 2777 |
. . . . . . . 8
β’ ((π β β β§ π β β) β (π pCnt
(expβ(ΞΈβ((2 Β· π) β 1)))) = if(π β€ ((2 Β· π) β 1), 1, 0)) |
208 | | efchtcl 26476 |
. . . . . . . . . . . . 13
β’ (π β β β
(expβ(ΞΈβπ)) β β) |
209 | 9, 208 | syl 17 |
. . . . . . . . . . . 12
β’ (π β β β
(expβ(ΞΈβπ)) β β) |
210 | 209 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β) β
(expβ(ΞΈβπ)) β β) |
211 | | nnz 12527 |
. . . . . . . . . . . 12
β’
((expβ(ΞΈβπ)) β β β
(expβ(ΞΈβπ)) β β€) |
212 | | nnne0 12194 |
. . . . . . . . . . . 12
β’
((expβ(ΞΈβπ)) β β β
(expβ(ΞΈβπ)) β 0) |
213 | 211, 212 | jca 513 |
. . . . . . . . . . 11
β’
((expβ(ΞΈβπ)) β β β
((expβ(ΞΈβπ)) β β€ β§
(expβ(ΞΈβπ)) β 0)) |
214 | 210, 213 | syl 17 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β
((expβ(ΞΈβπ)) β β€ β§
(expβ(ΞΈβπ)) β 0)) |
215 | | nnz 12527 |
. . . . . . . . . . . 12
β’ ((((2
Β· π) β
1)Cπ) β β β
(((2 Β· π) β
1)Cπ) β
β€) |
216 | | nnne0 12194 |
. . . . . . . . . . . 12
β’ ((((2
Β· π) β
1)Cπ) β β β
(((2 Β· π) β
1)Cπ) β
0) |
217 | 215, 216 | jca 513 |
. . . . . . . . . . 11
β’ ((((2
Β· π) β
1)Cπ) β β β
((((2 Β· π) β
1)Cπ) β β€ β§
(((2 Β· π) β
1)Cπ) β
0)) |
218 | 68, 217 | syl 17 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β ((((2
Β· π) β
1)Cπ) β β€ β§
(((2 Β· π) β
1)Cπ) β
0)) |
219 | | pcmul 16730 |
. . . . . . . . . 10
β’ ((π β β β§
((expβ(ΞΈβπ)) β β€ β§
(expβ(ΞΈβπ)) β 0) β§ ((((2 Β· π) β 1)Cπ) β β€ β§ (((2 Β· π) β 1)Cπ) β 0)) β (π pCnt ((expβ(ΞΈβπ)) Β· (((2 Β· π) β 1)Cπ))) = ((π pCnt (expβ(ΞΈβπ))) + (π pCnt (((2 Β· π) β 1)Cπ)))) |
220 | 67, 214, 218, 219 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β β β§ π β β) β (π pCnt
((expβ(ΞΈβπ)) Β· (((2 Β· π) β 1)Cπ))) = ((π pCnt (expβ(ΞΈβπ))) + (π pCnt (((2 Β· π) β 1)Cπ)))) |
221 | 192 | prmorcht 26543 |
. . . . . . . . . . . . 13
β’ (π β β β
(expβ(ΞΈβπ)) = (seq1( Β· , (π β β β¦ if(π β β, π, 1)))βπ)) |
222 | 221 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (π β β β (π pCnt
(expβ(ΞΈβπ))) = (π pCnt (seq1( Β· , (π β β β¦ if(π β β, π, 1)))βπ))) |
223 | 222 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β) β (π pCnt
(expβ(ΞΈβπ))) = (π pCnt (seq1( Β· , (π β β β¦ if(π β β, π, 1)))βπ))) |
224 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β β) β π β
β) |
225 | 201, 203,
224, 67, 205 | pcmpt 16771 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β) β (π pCnt (seq1( Β· , (π β β β¦ if(π β β, π, 1)))βπ)) = if(π β€ π, 1, 0)) |
226 | 223, 225 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β (π pCnt
(expβ(ΞΈβπ))) = if(π β€ π, 1, 0)) |
227 | 226 | oveq1d 7377 |
. . . . . . . . 9
β’ ((π β β β§ π β β) β ((π pCnt
(expβ(ΞΈβπ))) + (π pCnt (((2 Β· π) β 1)Cπ))) = (if(π β€ π, 1, 0) + (π pCnt (((2 Β· π) β 1)Cπ)))) |
228 | 220, 227 | eqtrd 2777 |
. . . . . . . 8
β’ ((π β β β§ π β β) β (π pCnt
((expβ(ΞΈβπ)) Β· (((2 Β· π) β 1)Cπ))) = (if(π β€ π, 1, 0) + (π pCnt (((2 Β· π) β 1)Cπ)))) |
229 | 191, 207,
228 | 3brtr4d 5142 |
. . . . . . 7
β’ ((π β β β§ π β β) β (π pCnt
(expβ(ΞΈβ((2 Β· π) β 1)))) β€ (π pCnt ((expβ(ΞΈβπ)) Β· (((2 Β· π) β 1)Cπ)))) |
230 | 229 | ralrimiva 3144 |
. . . . . 6
β’ (π β β β
βπ β β
(π pCnt
(expβ(ΞΈβ((2 Β· π) β 1)))) β€ (π pCnt ((expβ(ΞΈβπ)) Β· (((2 Β· π) β 1)Cπ)))) |
231 | | efchtcl 26476 |
. . . . . . . . 9
β’ (((2
Β· π) β 1)
β β β (expβ(ΞΈβ((2 Β· π) β 1))) β
β) |
232 | 6, 231 | syl 17 |
. . . . . . . 8
β’ (π β β β
(expβ(ΞΈβ((2 Β· π) β 1))) β
β) |
233 | 232 | nnzd 12533 |
. . . . . . 7
β’ (π β β β
(expβ(ΞΈβ((2 Β· π) β 1))) β
β€) |
234 | 209, 52 | nnmulcld 12213 |
. . . . . . . 8
β’ (π β β β
((expβ(ΞΈβπ)) Β· (((2 Β· π) β 1)Cπ)) β β) |
235 | 234 | nnzd 12533 |
. . . . . . 7
β’ (π β β β
((expβ(ΞΈβπ)) Β· (((2 Β· π) β 1)Cπ)) β β€) |
236 | | pc2dvds 16758 |
. . . . . . 7
β’
(((expβ(ΞΈβ((2 Β· π) β 1))) β β€ β§
((expβ(ΞΈβπ)) Β· (((2 Β· π) β 1)Cπ)) β β€) β
((expβ(ΞΈβ((2 Β· π) β 1))) β₯
((expβ(ΞΈβπ)) Β· (((2 Β· π) β 1)Cπ)) β βπ β β (π pCnt (expβ(ΞΈβ((2 Β·
π) β 1)))) β€
(π pCnt
((expβ(ΞΈβπ)) Β· (((2 Β· π) β 1)Cπ))))) |
237 | 233, 235,
236 | syl2anc 585 |
. . . . . 6
β’ (π β β β
((expβ(ΞΈβ((2 Β· π) β 1))) β₯
((expβ(ΞΈβπ)) Β· (((2 Β· π) β 1)Cπ)) β βπ β β (π pCnt (expβ(ΞΈβ((2 Β·
π) β 1)))) β€
(π pCnt
((expβ(ΞΈβπ)) Β· (((2 Β· π) β 1)Cπ))))) |
238 | 230, 237 | mpbird 257 |
. . . . 5
β’ (π β β β
(expβ(ΞΈβ((2 Β· π) β 1))) β₯
((expβ(ΞΈβπ)) Β· (((2 Β· π) β 1)Cπ))) |
239 | | dvdsle 16199 |
. . . . . 6
β’
(((expβ(ΞΈβ((2 Β· π) β 1))) β β€ β§
((expβ(ΞΈβπ)) Β· (((2 Β· π) β 1)Cπ)) β β) β
((expβ(ΞΈβ((2 Β· π) β 1))) β₯
((expβ(ΞΈβπ)) Β· (((2 Β· π) β 1)Cπ)) β (expβ(ΞΈβ((2
Β· π) β 1)))
β€ ((expβ(ΞΈβπ)) Β· (((2 Β· π) β 1)Cπ)))) |
240 | 233, 234,
239 | syl2anc 585 |
. . . . 5
β’ (π β β β
((expβ(ΞΈβ((2 Β· π) β 1))) β₯
((expβ(ΞΈβπ)) Β· (((2 Β· π) β 1)Cπ)) β (expβ(ΞΈβ((2
Β· π) β 1)))
β€ ((expβ(ΞΈβπ)) Β· (((2 Β· π) β 1)Cπ)))) |
241 | 238, 240 | mpd 15 |
. . . 4
β’ (π β β β
(expβ(ΞΈβ((2 Β· π) β 1))) β€
((expβ(ΞΈβπ)) Β· (((2 Β· π) β 1)Cπ))) |
242 | 11 | recnd 11190 |
. . . . . 6
β’ (π β β β
(ΞΈβπ) β
β) |
243 | 54 | recnd 11190 |
. . . . . 6
β’ (π β β β
(logβ(((2 Β· π)
β 1)Cπ)) β
β) |
244 | | efadd 15983 |
. . . . . 6
β’
(((ΞΈβπ)
β β β§ (logβ(((2 Β· π) β 1)Cπ)) β β) β
(expβ((ΞΈβπ) + (logβ(((2 Β· π) β 1)Cπ)))) = ((expβ(ΞΈβπ)) Β·
(expβ(logβ(((2 Β· π) β 1)Cπ))))) |
245 | 242, 243,
244 | syl2anc 585 |
. . . . 5
β’ (π β β β
(expβ((ΞΈβπ) + (logβ(((2 Β· π) β 1)Cπ)))) = ((expβ(ΞΈβπ)) Β·
(expβ(logβ(((2 Β· π) β 1)Cπ))))) |
246 | 53 | reeflogd 25995 |
. . . . . 6
β’ (π β β β
(expβ(logβ(((2 Β· π) β 1)Cπ))) = (((2 Β· π) β 1)Cπ)) |
247 | 246 | oveq2d 7378 |
. . . . 5
β’ (π β β β
((expβ(ΞΈβπ)) Β· (expβ(logβ(((2
Β· π) β
1)Cπ)))) =
((expβ(ΞΈβπ)) Β· (((2 Β· π) β 1)Cπ))) |
248 | 245, 247 | eqtrd 2777 |
. . . 4
β’ (π β β β
(expβ((ΞΈβπ) + (logβ(((2 Β· π) β 1)Cπ)))) = ((expβ(ΞΈβπ)) Β· (((2 Β· π) β 1)Cπ))) |
249 | 241, 248 | breqtrrd 5138 |
. . 3
β’ (π β β β
(expβ(ΞΈβ((2 Β· π) β 1))) β€
(expβ((ΞΈβπ) + (logβ(((2 Β· π) β 1)Cπ))))) |
250 | | efle 16007 |
. . . 4
β’
(((ΞΈβ((2 Β· π) β 1)) β β β§
((ΞΈβπ) +
(logβ(((2 Β· π)
β 1)Cπ))) β
β) β ((ΞΈβ((2 Β· π) β 1)) β€ ((ΞΈβπ) + (logβ(((2 Β·
π) β 1)Cπ))) β
(expβ(ΞΈβ((2 Β· π) β 1))) β€
(expβ((ΞΈβπ) + (logβ(((2 Β· π) β 1)Cπ)))))) |
251 | 8, 55, 250 | syl2anc 585 |
. . 3
β’ (π β β β
((ΞΈβ((2 Β· π) β 1)) β€ ((ΞΈβπ) + (logβ(((2 Β·
π) β 1)Cπ))) β
(expβ(ΞΈβ((2 Β· π) β 1))) β€
(expβ((ΞΈβπ) + (logβ(((2 Β· π) β 1)Cπ)))))) |
252 | 249, 251 | mpbird 257 |
. 2
β’ (π β β β
(ΞΈβ((2 Β· π) β 1)) β€ ((ΞΈβπ) + (logβ(((2 Β·
π) β 1)Cπ)))) |
253 | | fzfid 13885 |
. . . . . . . . 9
β’ (π β β β (0...((2
Β· π) β 1))
β Fin) |
254 | | elfzelz 13448 |
. . . . . . . . . . 11
β’ (π β (0...((2 Β· π) β 1)) β π β
β€) |
255 | | bccl 14229 |
. . . . . . . . . . 11
β’ ((((2
Β· π) β 1)
β β0 β§ π β β€) β (((2 Β· π) β 1)Cπ) β
β0) |
256 | 39, 254, 255 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β β β§ π β (0...((2 Β· π) β 1))) β (((2
Β· π) β
1)Cπ) β
β0) |
257 | 256 | nn0red 12481 |
. . . . . . . . 9
β’ ((π β β β§ π β (0...((2 Β· π) β 1))) β (((2
Β· π) β
1)Cπ) β
β) |
258 | 256 | nn0ge0d 12483 |
. . . . . . . . 9
β’ ((π β β β§ π β (0...((2 Β· π) β 1))) β 0 β€
(((2 Β· π) β
1)Cπ)) |
259 | | nn0uz 12812 |
. . . . . . . . . . . 12
β’
β0 = (β€β₯β0) |
260 | 32, 259 | eleqtrdi 2848 |
. . . . . . . . . . 11
β’ (π β β β (π β 1) β
(β€β₯β0)) |
261 | | fzss1 13487 |
. . . . . . . . . . 11
β’ ((π β 1) β
(β€β₯β0) β ((π β 1)...π) β (0...π)) |
262 | 260, 261 | syl 17 |
. . . . . . . . . 10
β’ (π β β β ((π β 1)...π) β (0...π)) |
263 | | eluz 12784 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ ((2
Β· π) β 1)
β β€) β (((2 Β· π) β 1) β
(β€β₯βπ) β π β€ ((2 Β· π) β 1))) |
264 | 148, 81, 263 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β β β (((2
Β· π) β 1)
β (β€β₯βπ) β π β€ ((2 Β· π) β 1))) |
265 | 48, 264 | mpbird 257 |
. . . . . . . . . . 11
β’ (π β β β ((2
Β· π) β 1)
β (β€β₯βπ)) |
266 | | fzss2 13488 |
. . . . . . . . . . 11
β’ (((2
Β· π) β 1)
β (β€β₯βπ) β (0...π) β (0...((2 Β· π) β 1))) |
267 | 265, 266 | syl 17 |
. . . . . . . . . 10
β’ (π β β β
(0...π) β (0...((2
Β· π) β
1))) |
268 | 262, 267 | sstrd 3959 |
. . . . . . . . 9
β’ (π β β β ((π β 1)...π) β (0...((2 Β· π) β 1))) |
269 | 253, 257,
258, 268 | fsumless 15688 |
. . . . . . . 8
β’ (π β β β
Ξ£π β ((π β 1)...π)(((2 Β· π) β 1)Cπ) β€ Ξ£π β (0...((2 Β· π) β 1))(((2 Β· π) β 1)Cπ)) |
270 | 32 | nn0zd 12532 |
. . . . . . . . . . . 12
β’ (π β β β (π β 1) β
β€) |
271 | | bccmpl 14216 |
. . . . . . . . . . . . . . 15
β’ ((((2
Β· π) β 1)
β β0 β§ π β β€) β (((2 Β· π) β 1)Cπ) = (((2 Β· π) β 1)C(((2 Β· π) β 1) β π))) |
272 | 39, 148, 271 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β β β (((2
Β· π) β
1)Cπ) = (((2 Β· π) β 1)C(((2 Β· π) β 1) β π))) |
273 | 107 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (π β β β (((2
Β· π) β 1)C(((2
Β· π) β 1)
β π)) = (((2 Β·
π) β 1)C(π β 1))) |
274 | 272, 273 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (π β β β (((2
Β· π) β
1)Cπ) = (((2 Β· π) β 1)C(π β 1))) |
275 | 52 | nncnd 12176 |
. . . . . . . . . . . . 13
β’ (π β β β (((2
Β· π) β
1)Cπ) β
β) |
276 | 274, 275 | eqeltrrd 2839 |
. . . . . . . . . . . 12
β’ (π β β β (((2
Β· π) β
1)C(π β 1)) β
β) |
277 | | oveq2 7370 |
. . . . . . . . . . . . 13
β’ (π = (π β 1) β (((2 Β· π) β 1)Cπ) = (((2 Β· π) β 1)C(π β 1))) |
278 | 277 | fsum1 15639 |
. . . . . . . . . . . 12
β’ (((π β 1) β β€ β§
(((2 Β· π) β
1)C(π β 1)) β
β) β Ξ£π
β ((π β
1)...(π β 1))(((2
Β· π) β
1)Cπ) = (((2 Β· π) β 1)C(π β 1))) |
279 | 270, 276,
278 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β β β
Ξ£π β ((π β 1)...(π β 1))(((2 Β· π) β 1)Cπ) = (((2 Β· π) β 1)C(π β 1))) |
280 | 279, 274 | eqtr4d 2780 |
. . . . . . . . . 10
β’ (π β β β
Ξ£π β ((π β 1)...(π β 1))(((2 Β· π) β 1)Cπ) = (((2 Β· π) β 1)Cπ)) |
281 | 280 | oveq1d 7377 |
. . . . . . . . 9
β’ (π β β β
(Ξ£π β ((π β 1)...(π β 1))(((2 Β· π) β 1)Cπ) + (((2 Β· π) β 1)Cπ)) = ((((2 Β· π) β 1)Cπ) + (((2 Β· π) β 1)Cπ))) |
282 | 21, 104 | npcand 11523 |
. . . . . . . . . . 11
β’ (π β β β ((π β 1) + 1) = π) |
283 | | uzid 12785 |
. . . . . . . . . . . . 13
β’ ((π β 1) β β€
β (π β 1) β
(β€β₯β(π β 1))) |
284 | 270, 283 | syl 17 |
. . . . . . . . . . . 12
β’ (π β β β (π β 1) β
(β€β₯β(π β 1))) |
285 | | peano2uz 12833 |
. . . . . . . . . . . 12
β’ ((π β 1) β
(β€β₯β(π β 1)) β ((π β 1) + 1) β
(β€β₯β(π β 1))) |
286 | 284, 285 | syl 17 |
. . . . . . . . . . 11
β’ (π β β β ((π β 1) + 1) β
(β€β₯β(π β 1))) |
287 | 282, 286 | eqeltrrd 2839 |
. . . . . . . . . 10
β’ (π β β β π β
(β€β₯β(π β 1))) |
288 | 268 | sselda 3949 |
. . . . . . . . . . 11
β’ ((π β β β§ π β ((π β 1)...π)) β π β (0...((2 Β· π) β 1))) |
289 | 256 | nn0cnd 12482 |
. . . . . . . . . . 11
β’ ((π β β β§ π β (0...((2 Β· π) β 1))) β (((2
Β· π) β
1)Cπ) β
β) |
290 | 288, 289 | syldan 592 |
. . . . . . . . . 10
β’ ((π β β β§ π β ((π β 1)...π)) β (((2 Β· π) β 1)Cπ) β β) |
291 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π = π β (((2 Β· π) β 1)Cπ) = (((2 Β· π) β 1)Cπ)) |
292 | 287, 290,
291 | fsumm1 15643 |
. . . . . . . . 9
β’ (π β β β
Ξ£π β ((π β 1)...π)(((2 Β· π) β 1)Cπ) = (Ξ£π β ((π β 1)...(π β 1))(((2 Β· π) β 1)Cπ) + (((2 Β· π) β 1)Cπ))) |
293 | 275 | 2timesd 12403 |
. . . . . . . . 9
β’ (π β β β (2
Β· (((2 Β· π)
β 1)Cπ)) = ((((2
Β· π) β
1)Cπ) + (((2 Β· π) β 1)Cπ))) |
294 | 281, 292,
293 | 3eqtr4rd 2788 |
. . . . . . . 8
β’ (π β β β (2
Β· (((2 Β· π)
β 1)Cπ)) =
Ξ£π β ((π β 1)...π)(((2 Β· π) β 1)Cπ)) |
295 | | binom11 15724 |
. . . . . . . . 9
β’ (((2
Β· π) β 1)
β β0 β (2β((2 Β· π) β 1)) = Ξ£π β (0...((2 Β· π) β 1))(((2 Β· π) β 1)Cπ)) |
296 | 39, 295 | syl 17 |
. . . . . . . 8
β’ (π β β β
(2β((2 Β· π)
β 1)) = Ξ£π
β (0...((2 Β· π)
β 1))(((2 Β· π)
β 1)Cπ)) |
297 | 269, 294,
296 | 3brtr4d 5142 |
. . . . . . 7
β’ (π β β β (2
Β· (((2 Β· π)
β 1)Cπ)) β€
(2β((2 Β· π)
β 1))) |
298 | | mulcom 11144 |
. . . . . . . 8
β’ ((2
β β β§ (((2 Β· π) β 1)Cπ) β β) β (2 Β· (((2
Β· π) β
1)Cπ)) = ((((2 Β·
π) β 1)Cπ) Β· 2)) |
299 | 16, 275, 298 | sylancr 588 |
. . . . . . 7
β’ (π β β β (2
Β· (((2 Β· π)
β 1)Cπ)) = ((((2
Β· π) β
1)Cπ) Β·
2)) |
300 | 30 | oveq2d 7378 |
. . . . . . . 8
β’ (π β β β
(2β((2 Β· π)
β 1)) = (2β((2 Β· (π β 1)) + 1))) |
301 | | expp1 13981 |
. . . . . . . . 9
β’ ((2
β β β§ (2 Β· (π β 1)) β β0)
β (2β((2 Β· (π β 1)) + 1)) = ((2β(2 Β·
(π β 1))) Β·
2)) |
302 | 16, 34, 301 | sylancr 588 |
. . . . . . . 8
β’ (π β β β
(2β((2 Β· (π
β 1)) + 1)) = ((2β(2 Β· (π β 1))) Β· 2)) |
303 | 16 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β β 2 β
β) |
304 | 31 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β β 2 β
β0) |
305 | 303, 32, 304 | expmuld 14061 |
. . . . . . . . . 10
β’ (π β β β
(2β(2 Β· (π
β 1))) = ((2β2)β(π β 1))) |
306 | | sq2 14108 |
. . . . . . . . . . 11
β’
(2β2) = 4 |
307 | 306 | oveq1i 7372 |
. . . . . . . . . 10
β’
((2β2)β(π
β 1)) = (4β(π
β 1)) |
308 | 305, 307 | eqtrdi 2793 |
. . . . . . . . 9
β’ (π β β β
(2β(2 Β· (π
β 1))) = (4β(π
β 1))) |
309 | 308 | oveq1d 7377 |
. . . . . . . 8
β’ (π β β β
((2β(2 Β· (π
β 1))) Β· 2) = ((4β(π β 1)) Β· 2)) |
310 | 300, 302,
309 | 3eqtrd 2781 |
. . . . . . 7
β’ (π β β β
(2β((2 Β· π)
β 1)) = ((4β(π
β 1)) Β· 2)) |
311 | 297, 299,
310 | 3brtr3d 5141 |
. . . . . 6
β’ (π β β β ((((2
Β· π) β
1)Cπ) Β· 2) β€
((4β(π β 1))
Β· 2)) |
312 | 52 | nnred 12175 |
. . . . . . 7
β’ (π β β β (((2
Β· π) β
1)Cπ) β
β) |
313 | | reexpcl 13991 |
. . . . . . . 8
β’ ((4
β β β§ (π
β 1) β β0) β (4β(π β 1)) β
β) |
314 | 56, 32, 313 | sylancr 588 |
. . . . . . 7
β’ (π β β β
(4β(π β 1))
β β) |
315 | | 2re 12234 |
. . . . . . . . 9
β’ 2 β
β |
316 | | 2pos 12263 |
. . . . . . . . 9
β’ 0 <
2 |
317 | 315, 316 | pm3.2i 472 |
. . . . . . . 8
β’ (2 β
β β§ 0 < 2) |
318 | 317 | a1i 11 |
. . . . . . 7
β’ (π β β β (2 β
β β§ 0 < 2)) |
319 | | lemul1 12014 |
. . . . . . 7
β’ (((((2
Β· π) β
1)Cπ) β β β§
(4β(π β 1))
β β β§ (2 β β β§ 0 < 2)) β ((((2 Β·
π) β 1)Cπ) β€ (4β(π β 1)) β ((((2
Β· π) β
1)Cπ) Β· 2) β€
((4β(π β 1))
Β· 2))) |
320 | 312, 314,
318, 319 | syl3anc 1372 |
. . . . . 6
β’ (π β β β ((((2
Β· π) β
1)Cπ) β€ (4β(π β 1)) β ((((2
Β· π) β
1)Cπ) Β· 2) β€
((4β(π β 1))
Β· 2))) |
321 | 311, 320 | mpbird 257 |
. . . . 5
β’ (π β β β (((2
Β· π) β
1)Cπ) β€ (4β(π β 1))) |
322 | 60 | recni 11176 |
. . . . . . . 8
β’
(logβ4) β β |
323 | | mulcom 11144 |
. . . . . . . 8
β’
(((logβ4) β β β§ (π β 1) β β) β
((logβ4) Β· (π
β 1)) = ((π β
1) Β· (logβ4))) |
324 | 322, 103,
323 | sylancr 588 |
. . . . . . 7
β’ (π β β β
((logβ4) Β· (π
β 1)) = ((π β
1) Β· (logβ4))) |
325 | 324 | fveq2d 6851 |
. . . . . 6
β’ (π β β β
(expβ((logβ4) Β· (π β 1))) = (expβ((π β 1) Β·
(logβ4)))) |
326 | | reexplog 25966 |
. . . . . . 7
β’ ((4
β β+ β§ (π β 1) β β€) β
(4β(π β 1)) =
(expβ((π β 1)
Β· (logβ4)))) |
327 | 58, 270, 326 | sylancr 588 |
. . . . . 6
β’ (π β β β
(4β(π β 1)) =
(expβ((π β 1)
Β· (logβ4)))) |
328 | 325, 327 | eqtr4d 2780 |
. . . . 5
β’ (π β β β
(expβ((logβ4) Β· (π β 1))) = (4β(π β 1))) |
329 | 321, 246,
328 | 3brtr4d 5142 |
. . . 4
β’ (π β β β
(expβ(logβ(((2 Β· π) β 1)Cπ))) β€ (expβ((logβ4) Β·
(π β
1)))) |
330 | | efle 16007 |
. . . . 5
β’
(((logβ(((2 Β· π) β 1)Cπ)) β β β§ ((logβ4)
Β· (π β 1))
β β) β ((logβ(((2 Β· π) β 1)Cπ)) β€ ((logβ4) Β· (π β 1)) β
(expβ(logβ(((2 Β· π) β 1)Cπ))) β€ (expβ((logβ4) Β·
(π β
1))))) |
331 | 54, 63, 330 | syl2anc 585 |
. . . 4
β’ (π β β β
((logβ(((2 Β· π) β 1)Cπ)) β€ ((logβ4) Β· (π β 1)) β
(expβ(logβ(((2 Β· π) β 1)Cπ))) β€ (expβ((logβ4) Β·
(π β
1))))) |
332 | 329, 331 | mpbird 257 |
. . 3
β’ (π β β β
(logβ(((2 Β· π)
β 1)Cπ)) β€
((logβ4) Β· (π
β 1))) |
333 | 54, 63, 11, 332 | leadd2dd 11777 |
. 2
β’ (π β β β
((ΞΈβπ) +
(logβ(((2 Β· π)
β 1)Cπ))) β€
((ΞΈβπ) +
((logβ4) Β· (π
β 1)))) |
334 | 8, 55, 64, 252, 333 | letrd 11319 |
1
β’ (π β β β
(ΞΈβ((2 Β· π) β 1)) β€ ((ΞΈβπ) + ((logβ4) Β·
(π β
1)))) |