Step | Hyp | Ref
| Expression |
1 | | bpos.3 |
. . . . . 6
β’ πΉ = (π β β β¦ if(π β β, (πβ(π pCnt ((2 Β· π)Cπ))), 1)) |
2 | | id 22 |
. . . . . . . 8
β’ (π β β β π β
β) |
3 | | 5nn 12246 |
. . . . . . . . . . 11
β’ 5 β
β |
4 | | bpos.1 |
. . . . . . . . . . 11
β’ (π β π β
(β€β₯β5)) |
5 | | eluznn 12850 |
. . . . . . . . . . 11
β’ ((5
β β β§ π
β (β€β₯β5)) β π β β) |
6 | 3, 4, 5 | sylancr 588 |
. . . . . . . . . 10
β’ (π β π β β) |
7 | 6 | nnnn0d 12480 |
. . . . . . . . 9
β’ (π β π β
β0) |
8 | | fzctr 13560 |
. . . . . . . . 9
β’ (π β β0
β π β (0...(2
Β· π))) |
9 | | bccl2 14230 |
. . . . . . . . 9
β’ (π β (0...(2 Β· π)) β ((2 Β· π)Cπ) β β) |
10 | 7, 8, 9 | 3syl 18 |
. . . . . . . 8
β’ (π β ((2 Β· π)Cπ) β β) |
11 | | pccl 16728 |
. . . . . . . 8
β’ ((π β β β§ ((2
Β· π)Cπ) β β) β (π pCnt ((2 Β· π)Cπ)) β
β0) |
12 | 2, 10, 11 | syl2anr 598 |
. . . . . . 7
β’ ((π β§ π β β) β (π pCnt ((2 Β· π)Cπ)) β
β0) |
13 | 12 | ralrimiva 3144 |
. . . . . 6
β’ (π β βπ β β (π pCnt ((2 Β· π)Cπ)) β
β0) |
14 | 1, 13 | pcmptcl 16770 |
. . . . 5
β’ (π β (πΉ:ββΆβ β§ seq1( Β·
, πΉ):ββΆβ)) |
15 | 14 | simprd 497 |
. . . 4
β’ (π β seq1( Β· , πΉ):ββΆβ) |
16 | | 3nn 12239 |
. . . . 5
β’ 3 β
β |
17 | | bpos.5 |
. . . . . 6
β’ π =
(ββ(ββ(2 Β· π))) |
18 | | 2z 12542 |
. . . . . . . . . . 11
β’ 2 β
β€ |
19 | 6 | nnzd 12533 |
. . . . . . . . . . 11
β’ (π β π β β€) |
20 | | zmulcl 12559 |
. . . . . . . . . . 11
β’ ((2
β β€ β§ π
β β€) β (2 Β· π) β β€) |
21 | 18, 19, 20 | sylancr 588 |
. . . . . . . . . 10
β’ (π β (2 Β· π) β
β€) |
22 | 21 | zred 12614 |
. . . . . . . . 9
β’ (π β (2 Β· π) β
β) |
23 | | 2nn 12233 |
. . . . . . . . . . . 12
β’ 2 β
β |
24 | | nnmulcl 12184 |
. . . . . . . . . . . 12
β’ ((2
β β β§ π
β β) β (2 Β· π) β β) |
25 | 23, 6, 24 | sylancr 588 |
. . . . . . . . . . 11
β’ (π β (2 Β· π) β
β) |
26 | 25 | nnrpd 12962 |
. . . . . . . . . 10
β’ (π β (2 Β· π) β
β+) |
27 | 26 | rpge0d 12968 |
. . . . . . . . 9
β’ (π β 0 β€ (2 Β· π)) |
28 | 22, 27 | resqrtcld 15309 |
. . . . . . . 8
β’ (π β (ββ(2 Β·
π)) β
β) |
29 | 28 | flcld 13710 |
. . . . . . 7
β’ (π β
(ββ(ββ(2 Β· π))) β β€) |
30 | | sqrt9 15165 |
. . . . . . . . 9
β’
(ββ9) = 3 |
31 | | 9re 12259 |
. . . . . . . . . . . 12
β’ 9 β
β |
32 | 31 | a1i 11 |
. . . . . . . . . . 11
β’ (π β 9 β
β) |
33 | | 10re 12644 |
. . . . . . . . . . . 12
β’ ;10 β β |
34 | 33 | a1i 11 |
. . . . . . . . . . 11
β’ (π β ;10 β β) |
35 | | lep1 12003 |
. . . . . . . . . . . . . 14
β’ (9 β
β β 9 β€ (9 + 1)) |
36 | 31, 35 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ 9 β€ (9
+ 1) |
37 | | 9p1e10 12627 |
. . . . . . . . . . . . 13
β’ (9 + 1) =
;10 |
38 | 36, 37 | breqtri 5135 |
. . . . . . . . . . . 12
β’ 9 β€
;10 |
39 | 38 | a1i 11 |
. . . . . . . . . . 11
β’ (π β 9 β€ ;10) |
40 | | 5cn 12248 |
. . . . . . . . . . . . 13
β’ 5 β
β |
41 | | 2cn 12235 |
. . . . . . . . . . . . 13
β’ 2 β
β |
42 | | 5t2e10 12725 |
. . . . . . . . . . . . 13
β’ (5
Β· 2) = ;10 |
43 | 40, 41, 42 | mulcomli 11171 |
. . . . . . . . . . . 12
β’ (2
Β· 5) = ;10 |
44 | | eluzle 12783 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯β5) β 5 β€ π) |
45 | 4, 44 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β 5 β€ π) |
46 | 6 | nnred 12175 |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
47 | | 5re 12247 |
. . . . . . . . . . . . . . 15
β’ 5 β
β |
48 | | 2re 12234 |
. . . . . . . . . . . . . . . 16
β’ 2 β
β |
49 | | 2pos 12263 |
. . . . . . . . . . . . . . . 16
β’ 0 <
2 |
50 | 48, 49 | pm3.2i 472 |
. . . . . . . . . . . . . . 15
β’ (2 β
β β§ 0 < 2) |
51 | | lemul2 12015 |
. . . . . . . . . . . . . . 15
β’ ((5
β β β§ π
β β β§ (2 β β β§ 0 < 2)) β (5 β€ π β (2 Β· 5) β€ (2
Β· π))) |
52 | 47, 50, 51 | mp3an13 1453 |
. . . . . . . . . . . . . 14
β’ (π β β β (5 β€
π β (2 Β· 5)
β€ (2 Β· π))) |
53 | 46, 52 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (5 β€ π β (2 Β· 5) β€ (2 Β·
π))) |
54 | 45, 53 | mpbid 231 |
. . . . . . . . . . . 12
β’ (π β (2 Β· 5) β€ (2
Β· π)) |
55 | 43, 54 | eqbrtrrid 5146 |
. . . . . . . . . . 11
β’ (π β ;10 β€ (2 Β· π)) |
56 | 32, 34, 22, 39, 55 | letrd 11319 |
. . . . . . . . . 10
β’ (π β 9 β€ (2 Β· π)) |
57 | | 0re 11164 |
. . . . . . . . . . . . 13
β’ 0 β
β |
58 | | 9pos 12273 |
. . . . . . . . . . . . 13
β’ 0 <
9 |
59 | 57, 31, 58 | ltleii 11285 |
. . . . . . . . . . . 12
β’ 0 β€
9 |
60 | 31, 59 | pm3.2i 472 |
. . . . . . . . . . 11
β’ (9 β
β β§ 0 β€ 9) |
61 | 22, 27 | jca 513 |
. . . . . . . . . . 11
β’ (π β ((2 Β· π) β β β§ 0 β€ (2
Β· π))) |
62 | | sqrtle 15152 |
. . . . . . . . . . 11
β’ (((9
β β β§ 0 β€ 9) β§ ((2 Β· π) β β β§ 0 β€ (2 Β·
π))) β (9 β€ (2
Β· π) β
(ββ9) β€ (ββ(2 Β· π)))) |
63 | 60, 61, 62 | sylancr 588 |
. . . . . . . . . 10
β’ (π β (9 β€ (2 Β· π) β (ββ9) β€
(ββ(2 Β· π)))) |
64 | 56, 63 | mpbid 231 |
. . . . . . . . 9
β’ (π β (ββ9) β€
(ββ(2 Β· π))) |
65 | 30, 64 | eqbrtrrid 5146 |
. . . . . . . 8
β’ (π β 3 β€ (ββ(2
Β· π))) |
66 | | 3z 12543 |
. . . . . . . . 9
β’ 3 β
β€ |
67 | | flge 13717 |
. . . . . . . . 9
β’
(((ββ(2 Β· π)) β β β§ 3 β β€)
β (3 β€ (ββ(2 Β· π)) β 3 β€
(ββ(ββ(2 Β· π))))) |
68 | 28, 66, 67 | sylancl 587 |
. . . . . . . 8
β’ (π β (3 β€ (ββ(2
Β· π)) β 3 β€
(ββ(ββ(2 Β· π))))) |
69 | 65, 68 | mpbid 231 |
. . . . . . 7
β’ (π β 3 β€
(ββ(ββ(2 Β· π)))) |
70 | 66 | eluz1i 12778 |
. . . . . . 7
β’
((ββ(ββ(2 Β· π))) β (β€β₯β3)
β ((ββ(ββ(2 Β· π))) β β€ β§ 3 β€
(ββ(ββ(2 Β· π))))) |
71 | 29, 69, 70 | sylanbrc 584 |
. . . . . 6
β’ (π β
(ββ(ββ(2 Β· π))) β
(β€β₯β3)) |
72 | 17, 71 | eqeltrid 2842 |
. . . . 5
β’ (π β π β
(β€β₯β3)) |
73 | | eluznn 12850 |
. . . . 5
β’ ((3
β β β§ π
β (β€β₯β3)) β π β β) |
74 | 16, 72, 73 | sylancr 588 |
. . . 4
β’ (π β π β β) |
75 | 15, 74 | ffvelcdmd 7041 |
. . 3
β’ (π β (seq1( Β· , πΉ)βπ) β β) |
76 | 75 | nnred 12175 |
. 2
β’ (π β (seq1( Β· , πΉ)βπ) β β) |
77 | 74 | nnred 12175 |
. . . . 5
β’ (π β π β β) |
78 | | ppicl 26496 |
. . . . 5
β’ (π β β β
(Οβπ)
β β0) |
79 | 77, 78 | syl 17 |
. . . 4
β’ (π β (Οβπ) β
β0) |
80 | 25, 79 | nnexpcld 14155 |
. . 3
β’ (π β ((2 Β· π)β(Οβπ)) β
β) |
81 | 80 | nnred 12175 |
. 2
β’ (π β ((2 Β· π)β(Οβπ)) β
β) |
82 | | nndivre 12201 |
. . . . 5
β’
(((ββ(2 Β· π)) β β β§ 3 β β)
β ((ββ(2 Β· π)) / 3) β β) |
83 | 28, 16, 82 | sylancl 587 |
. . . 4
β’ (π β ((ββ(2
Β· π)) / 3) β
β) |
84 | | readdcl 11141 |
. . . 4
β’
((((ββ(2 Β· π)) / 3) β β β§ 2 β
β) β (((ββ(2 Β· π)) / 3) + 2) β
β) |
85 | 83, 48, 84 | sylancl 587 |
. . 3
β’ (π β (((ββ(2
Β· π)) / 3) + 2)
β β) |
86 | 22, 27, 85 | recxpcld 26094 |
. 2
β’ (π β ((2 Β· π)βπ(((ββ(2
Β· π)) / 3) + 2))
β β) |
87 | | fveq2 6847 |
. . . . . 6
β’ (π₯ = 1 β (seq1( Β· ,
πΉ)βπ₯) = (seq1( Β· , πΉ)β1)) |
88 | | fveq2 6847 |
. . . . . . . 8
β’ (π₯ = 1 β
(Οβπ₯) =
(Οβ1)) |
89 | | ppi1 26529 |
. . . . . . . 8
β’
(Οβ1) = 0 |
90 | 88, 89 | eqtrdi 2793 |
. . . . . . 7
β’ (π₯ = 1 β
(Οβπ₯) =
0) |
91 | 90 | oveq2d 7378 |
. . . . . 6
β’ (π₯ = 1 β ((2 Β· π)β(Οβπ₯)) = ((2 Β· π)β0)) |
92 | 87, 91 | breq12d 5123 |
. . . . 5
β’ (π₯ = 1 β ((seq1( Β· ,
πΉ)βπ₯) β€ ((2 Β· π)β(Οβπ₯)) β (seq1( Β· , πΉ)β1) β€ ((2 Β· π)β0))) |
93 | 92 | imbi2d 341 |
. . . 4
β’ (π₯ = 1 β ((π β (seq1( Β· , πΉ)βπ₯) β€ ((2 Β· π)β(Οβπ₯))) β (π β (seq1( Β· , πΉ)β1) β€ ((2 Β· π)β0)))) |
94 | | fveq2 6847 |
. . . . . 6
β’ (π₯ = π β (seq1( Β· , πΉ)βπ₯) = (seq1( Β· , πΉ)βπ)) |
95 | | fveq2 6847 |
. . . . . . 7
β’ (π₯ = π β (Οβπ₯) = (Οβπ)) |
96 | 95 | oveq2d 7378 |
. . . . . 6
β’ (π₯ = π β ((2 Β· π)β(Οβπ₯)) = ((2 Β· π)β(Οβπ))) |
97 | 94, 96 | breq12d 5123 |
. . . . 5
β’ (π₯ = π β ((seq1( Β· , πΉ)βπ₯) β€ ((2 Β· π)β(Οβπ₯)) β (seq1( Β· , πΉ)βπ) β€ ((2 Β· π)β(Οβπ)))) |
98 | 97 | imbi2d 341 |
. . . 4
β’ (π₯ = π β ((π β (seq1( Β· , πΉ)βπ₯) β€ ((2 Β· π)β(Οβπ₯))) β (π β (seq1( Β· , πΉ)βπ) β€ ((2 Β· π)β(Οβπ))))) |
99 | | fveq2 6847 |
. . . . . 6
β’ (π₯ = (π + 1) β (seq1( Β· , πΉ)βπ₯) = (seq1( Β· , πΉ)β(π + 1))) |
100 | | fveq2 6847 |
. . . . . . 7
β’ (π₯ = (π + 1) β (Οβπ₯) = (Οβ(π + 1))) |
101 | 100 | oveq2d 7378 |
. . . . . 6
β’ (π₯ = (π + 1) β ((2 Β· π)β(Οβπ₯)) = ((2 Β· π)β(Οβ(π + 1)))) |
102 | 99, 101 | breq12d 5123 |
. . . . 5
β’ (π₯ = (π + 1) β ((seq1( Β· , πΉ)βπ₯) β€ ((2 Β· π)β(Οβπ₯)) β (seq1( Β· , πΉ)β(π + 1)) β€ ((2 Β· π)β(Οβ(π + 1))))) |
103 | 102 | imbi2d 341 |
. . . 4
β’ (π₯ = (π + 1) β ((π β (seq1( Β· , πΉ)βπ₯) β€ ((2 Β· π)β(Οβπ₯))) β (π β (seq1( Β· , πΉ)β(π + 1)) β€ ((2 Β· π)β(Οβ(π + 1)))))) |
104 | | fveq2 6847 |
. . . . . 6
β’ (π₯ = π β (seq1( Β· , πΉ)βπ₯) = (seq1( Β· , πΉ)βπ)) |
105 | | fveq2 6847 |
. . . . . . 7
β’ (π₯ = π β (Οβπ₯) = (Οβπ)) |
106 | 105 | oveq2d 7378 |
. . . . . 6
β’ (π₯ = π β ((2 Β· π)β(Οβπ₯)) = ((2 Β· π)β(Οβπ))) |
107 | 104, 106 | breq12d 5123 |
. . . . 5
β’ (π₯ = π β ((seq1( Β· , πΉ)βπ₯) β€ ((2 Β· π)β(Οβπ₯)) β (seq1( Β· , πΉ)βπ) β€ ((2 Β· π)β(Οβπ)))) |
108 | 107 | imbi2d 341 |
. . . 4
β’ (π₯ = π β ((π β (seq1( Β· , πΉ)βπ₯) β€ ((2 Β· π)β(Οβπ₯))) β (π β (seq1( Β· , πΉ)βπ) β€ ((2 Β· π)β(Οβπ))))) |
109 | | 1z 12540 |
. . . . . . . 8
β’ 1 β
β€ |
110 | | seq1 13926 |
. . . . . . . 8
β’ (1 β
β€ β (seq1( Β· , πΉ)β1) = (πΉβ1)) |
111 | 109, 110 | ax-mp 5 |
. . . . . . 7
β’ (seq1(
Β· , πΉ)β1) =
(πΉβ1) |
112 | | 1nn 12171 |
. . . . . . . 8
β’ 1 β
β |
113 | | 1nprm 16562 |
. . . . . . . . . . 11
β’ Β¬ 1
β β |
114 | | eleq1 2826 |
. . . . . . . . . . 11
β’ (π = 1 β (π β β β 1 β
β)) |
115 | 113, 114 | mtbiri 327 |
. . . . . . . . . 10
β’ (π = 1 β Β¬ π β
β) |
116 | 115 | iffalsed 4502 |
. . . . . . . . 9
β’ (π = 1 β if(π β β, (πβ(π pCnt ((2 Β· π)Cπ))), 1) = 1) |
117 | | 1ex 11158 |
. . . . . . . . 9
β’ 1 β
V |
118 | 116, 1, 117 | fvmpt 6953 |
. . . . . . . 8
β’ (1 β
β β (πΉβ1)
= 1) |
119 | 112, 118 | ax-mp 5 |
. . . . . . 7
β’ (πΉβ1) = 1 |
120 | 111, 119 | eqtri 2765 |
. . . . . 6
β’ (seq1(
Β· , πΉ)β1) =
1 |
121 | | 1le1 11790 |
. . . . . 6
β’ 1 β€
1 |
122 | 120, 121 | eqbrtri 5131 |
. . . . 5
β’ (seq1(
Β· , πΉ)β1) β€
1 |
123 | 21 | zcnd 12615 |
. . . . . 6
β’ (π β (2 Β· π) β
β) |
124 | 123 | exp0d 14052 |
. . . . 5
β’ (π β ((2 Β· π)β0) = 1) |
125 | 122, 124 | breqtrrid 5148 |
. . . 4
β’ (π β (seq1( Β· , πΉ)β1) β€ ((2 Β·
π)β0)) |
126 | 15 | ffvelcdmda 7040 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (seq1( Β· ,
πΉ)βπ) β β) |
127 | 126 | nnred 12175 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (seq1( Β· ,
πΉ)βπ) β β) |
128 | 127 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π + 1) β β) β (seq1( Β·
, πΉ)βπ) β
β) |
129 | 25 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (π + 1) β β) β (2 Β·
π) β
β) |
130 | | nnre 12167 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β) |
131 | 130 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ (π + 1) β β) β π β
β) |
132 | | ppicl 26496 |
. . . . . . . . . . . . 13
β’ (π β β β
(Οβπ)
β β0) |
133 | 131, 132 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (π + 1) β β) β
(Οβπ)
β β0) |
134 | 129, 133 | nnexpcld 14155 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (π + 1) β β) β ((2 Β·
π)β(Οβπ)) β β) |
135 | 134 | nnred 12175 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π + 1) β β) β ((2 Β·
π)β(Οβπ)) β β) |
136 | | nnre 12167 |
. . . . . . . . . . . . 13
β’ ((2
Β· π) β β
β (2 Β· π)
β β) |
137 | | nngt0 12191 |
. . . . . . . . . . . . 13
β’ ((2
Β· π) β β
β 0 < (2 Β· π)) |
138 | 136, 137 | jca 513 |
. . . . . . . . . . . 12
β’ ((2
Β· π) β β
β ((2 Β· π)
β β β§ 0 < (2 Β· π))) |
139 | 25, 138 | syl 17 |
. . . . . . . . . . 11
β’ (π β ((2 Β· π) β β β§ 0 < (2
Β· π))) |
140 | 139 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π + 1) β β) β ((2 Β·
π) β β β§ 0
< (2 Β· π))) |
141 | | lemul1 12014 |
. . . . . . . . . 10
β’ (((seq1(
Β· , πΉ)βπ) β β β§ ((2
Β· π)β(Οβπ)) β β β§ ((2 Β· π) β β β§ 0 < (2
Β· π))) β
((seq1( Β· , πΉ)βπ) β€ ((2 Β· π)β(Οβπ)) β ((seq1( Β· , πΉ)βπ) Β· (2 Β· π)) β€ (((2 Β· π)β(Οβπ)) Β· (2 Β· π)))) |
142 | 128, 135,
140, 141 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (π + 1) β β) β ((seq1( Β·
, πΉ)βπ) β€ ((2 Β· π)β(Οβπ)) β ((seq1( Β· ,
πΉ)βπ) Β· (2 Β· π)) β€ (((2 Β· π)β(Οβπ)) Β· (2 Β· π)))) |
143 | | nnz 12527 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β€) |
144 | 143 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π β β€) |
145 | | ppiprm 26516 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ (π + 1) β β) β
(Οβ(π + 1))
= ((Οβπ) +
1)) |
146 | 144, 145 | sylan 581 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (π + 1) β β) β
(Οβ(π + 1))
= ((Οβπ) +
1)) |
147 | 146 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (π + 1) β β) β ((2 Β·
π)β(Οβ(π + 1))) = ((2 Β· π)β((Οβπ) + 1))) |
148 | 123 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (π + 1) β β) β (2 Β·
π) β
β) |
149 | 148, 133 | expp1d 14059 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (π + 1) β β) β ((2 Β·
π)β((Οβπ) + 1)) = (((2 Β· π)β(Οβπ)) Β· (2 Β· π))) |
150 | 147, 149 | eqtrd 2777 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π + 1) β β) β ((2 Β·
π)β(Οβ(π + 1))) = (((2 Β· π)β(Οβπ)) Β· (2 Β· π))) |
151 | 150 | breq2d 5122 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (π + 1) β β) β (((seq1(
Β· , πΉ)βπ) Β· (2 Β· π)) β€ ((2 Β· π)β(Οβ(π + 1))) β ((seq1( Β·
, πΉ)βπ) Β· (2 Β· π)) β€ (((2 Β· π)β(Οβπ)) Β· (2 Β· π)))) |
152 | 142, 151 | bitr4d 282 |
. . . . . . . 8
β’ (((π β§ π β β) β§ (π + 1) β β) β ((seq1( Β·
, πΉ)βπ) β€ ((2 Β· π)β(Οβπ)) β ((seq1( Β· ,
πΉ)βπ) Β· (2 Β· π)) β€ ((2 Β· π)β(Οβ(π + 1))))) |
153 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π β β) |
154 | | nnuz 12813 |
. . . . . . . . . . . . 13
β’ β =
(β€β₯β1) |
155 | 153, 154 | eleqtrdi 2848 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β
(β€β₯β1)) |
156 | | seqp1 13928 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β1) β (seq1( Β· , πΉ)β(π + 1)) = ((seq1( Β· , πΉ)βπ) Β· (πΉβ(π + 1)))) |
157 | 155, 156 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (seq1( Β· ,
πΉ)β(π + 1)) = ((seq1( Β· ,
πΉ)βπ) Β· (πΉβ(π + 1)))) |
158 | 157 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π + 1) β β) β (seq1( Β·
, πΉ)β(π + 1)) = ((seq1( Β· ,
πΉ)βπ) Β· (πΉβ(π + 1)))) |
159 | | peano2nn 12172 |
. . . . . . . . . . . . . . 15
β’ (π β β β (π + 1) β
β) |
160 | 159 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (π + 1) β β) |
161 | | eleq1 2826 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + 1) β (π β β β (π + 1) β β)) |
162 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π + 1) β π = (π + 1)) |
163 | | oveq1 7369 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π + 1) β (π pCnt ((2 Β· π)Cπ)) = ((π + 1) pCnt ((2 Β· π)Cπ))) |
164 | 162, 163 | oveq12d 7380 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + 1) β (πβ(π pCnt ((2 Β· π)Cπ))) = ((π + 1)β((π + 1) pCnt ((2 Β· π)Cπ)))) |
165 | 161, 164 | ifbieq1d 4515 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β if(π β β, (πβ(π pCnt ((2 Β· π)Cπ))), 1) = if((π + 1) β β, ((π + 1)β((π + 1) pCnt ((2 Β· π)Cπ))), 1)) |
166 | | ovex 7395 |
. . . . . . . . . . . . . . . 16
β’ ((π + 1)β((π + 1) pCnt ((2 Β· π)Cπ))) β V |
167 | 166, 117 | ifex 4541 |
. . . . . . . . . . . . . . 15
β’ if((π + 1) β β, ((π + 1)β((π + 1) pCnt ((2 Β· π)Cπ))), 1) β V |
168 | 165, 1, 167 | fvmpt 6953 |
. . . . . . . . . . . . . 14
β’ ((π + 1) β β β
(πΉβ(π + 1)) = if((π + 1) β β, ((π + 1)β((π + 1) pCnt ((2 Β· π)Cπ))), 1)) |
169 | 160, 168 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πΉβ(π + 1)) = if((π + 1) β β, ((π + 1)β((π + 1) pCnt ((2 Β· π)Cπ))), 1)) |
170 | | iftrue 4497 |
. . . . . . . . . . . . 13
β’ ((π + 1) β β β
if((π + 1) β β,
((π + 1)β((π + 1) pCnt ((2 Β· π)Cπ))), 1) = ((π + 1)β((π + 1) pCnt ((2 Β· π)Cπ)))) |
171 | 169, 170 | sylan9eq 2797 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (π + 1) β β) β (πΉβ(π + 1)) = ((π + 1)β((π + 1) pCnt ((2 Β· π)Cπ)))) |
172 | 6 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π β β) |
173 | | bposlem1 26648 |
. . . . . . . . . . . . 13
β’ ((π β β β§ (π + 1) β β) β
((π + 1)β((π + 1) pCnt ((2 Β· π)Cπ))) β€ (2 Β· π)) |
174 | 172, 173 | sylan 581 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (π + 1) β β) β ((π + 1)β((π + 1) pCnt ((2 Β· π)Cπ))) β€ (2 Β· π)) |
175 | 171, 174 | eqbrtrd 5132 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (π + 1) β β) β (πΉβ(π + 1)) β€ (2 Β· π)) |
176 | 14 | simpld 496 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ:ββΆβ) |
177 | | ffvelcdm 7037 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:ββΆβ β§
(π + 1) β β)
β (πΉβ(π + 1)) β
β) |
178 | 176, 159,
177 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (πΉβ(π + 1)) β β) |
179 | 178 | nnred 12175 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πΉβ(π + 1)) β β) |
180 | 179 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (π + 1) β β) β (πΉβ(π + 1)) β β) |
181 | 22 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (π + 1) β β) β (2 Β·
π) β
β) |
182 | | nnre 12167 |
. . . . . . . . . . . . . . 15
β’ ((seq1(
Β· , πΉ)βπ) β β β (seq1(
Β· , πΉ)βπ) β
β) |
183 | | nngt0 12191 |
. . . . . . . . . . . . . . 15
β’ ((seq1(
Β· , πΉ)βπ) β β β 0 <
(seq1( Β· , πΉ)βπ)) |
184 | 182, 183 | jca 513 |
. . . . . . . . . . . . . 14
β’ ((seq1(
Β· , πΉ)βπ) β β β ((seq1(
Β· , πΉ)βπ) β β β§ 0 <
(seq1( Β· , πΉ)βπ))) |
185 | 126, 184 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((seq1( Β· ,
πΉ)βπ) β β β§ 0 < (seq1( Β·
, πΉ)βπ))) |
186 | 185 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (π + 1) β β) β ((seq1( Β·
, πΉ)βπ) β β β§ 0 <
(seq1( Β· , πΉ)βπ))) |
187 | | lemul2 12015 |
. . . . . . . . . . . 12
β’ (((πΉβ(π + 1)) β β β§ (2 Β· π) β β β§ ((seq1(
Β· , πΉ)βπ) β β β§ 0 <
(seq1( Β· , πΉ)βπ))) β ((πΉβ(π + 1)) β€ (2 Β· π) β ((seq1( Β· , πΉ)βπ) Β· (πΉβ(π + 1))) β€ ((seq1( Β· , πΉ)βπ) Β· (2 Β· π)))) |
188 | 180, 181,
186, 187 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (π + 1) β β) β ((πΉβ(π + 1)) β€ (2 Β· π) β ((seq1( Β· , πΉ)βπ) Β· (πΉβ(π + 1))) β€ ((seq1( Β· , πΉ)βπ) Β· (2 Β· π)))) |
189 | 175, 188 | mpbid 231 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π + 1) β β) β ((seq1( Β·
, πΉ)βπ) Β· (πΉβ(π + 1))) β€ ((seq1( Β· , πΉ)βπ) Β· (2 Β· π))) |
190 | 158, 189 | eqbrtrd 5132 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (π + 1) β β) β (seq1( Β·
, πΉ)β(π + 1)) β€ ((seq1( Β· ,
πΉ)βπ) Β· (2 Β· π))) |
191 | | ffvelcdm 7037 |
. . . . . . . . . . . . 13
β’ ((seq1(
Β· , πΉ):ββΆβ β§ (π + 1) β β) β
(seq1( Β· , πΉ)β(π + 1)) β β) |
192 | 15, 159, 191 | syl2an 597 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (seq1( Β· ,
πΉ)β(π + 1)) β
β) |
193 | 192 | nnred 12175 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (seq1( Β· ,
πΉ)β(π + 1)) β
β) |
194 | 25 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (2 Β· π) β
β) |
195 | 126, 194 | nnmulcld 12213 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((seq1( Β· ,
πΉ)βπ) Β· (2 Β· π)) β β) |
196 | 195 | nnred 12175 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((seq1( Β· ,
πΉ)βπ) Β· (2 Β· π)) β β) |
197 | 160 | nnred 12175 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (π + 1) β β) |
198 | | ppicl 26496 |
. . . . . . . . . . . . . 14
β’ ((π + 1) β β β
(Οβ(π + 1))
β β0) |
199 | 197, 198 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β
(Οβ(π + 1))
β β0) |
200 | 194, 199 | nnexpcld 14155 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((2 Β· π)β(Οβ(π + 1))) β
β) |
201 | 200 | nnred 12175 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((2 Β· π)β(Οβ(π + 1))) β
β) |
202 | | letr 11256 |
. . . . . . . . . . 11
β’ (((seq1(
Β· , πΉ)β(π + 1)) β β β§
((seq1( Β· , πΉ)βπ) Β· (2 Β· π)) β β β§ ((2 Β· π)β(Οβ(π + 1))) β β) β
(((seq1( Β· , πΉ)β(π + 1)) β€ ((seq1( Β· , πΉ)βπ) Β· (2 Β· π)) β§ ((seq1( Β· , πΉ)βπ) Β· (2 Β· π)) β€ ((2 Β· π)β(Οβ(π + 1)))) β (seq1( Β·
, πΉ)β(π + 1)) β€ ((2 Β· π)β(Οβ(π + 1))))) |
203 | 193, 196,
201, 202 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (((seq1( Β· ,
πΉ)β(π + 1)) β€ ((seq1( Β· ,
πΉ)βπ) Β· (2 Β· π)) β§ ((seq1( Β· , πΉ)βπ) Β· (2 Β· π)) β€ ((2 Β· π)β(Οβ(π + 1)))) β (seq1( Β·
, πΉ)β(π + 1)) β€ ((2 Β· π)β(Οβ(π + 1))))) |
204 | 203 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (π + 1) β β) β (((seq1(
Β· , πΉ)β(π + 1)) β€ ((seq1( Β· ,
πΉ)βπ) Β· (2 Β· π)) β§ ((seq1( Β· , πΉ)βπ) Β· (2 Β· π)) β€ ((2 Β· π)β(Οβ(π + 1)))) β (seq1( Β·
, πΉ)β(π + 1)) β€ ((2 Β· π)β(Οβ(π + 1))))) |
205 | 190, 204 | mpand 694 |
. . . . . . . 8
β’ (((π β§ π β β) β§ (π + 1) β β) β (((seq1(
Β· , πΉ)βπ) Β· (2 Β· π)) β€ ((2 Β· π)β(Οβ(π + 1))) β (seq1( Β· ,
πΉ)β(π + 1)) β€ ((2 Β· π)β(Οβ(π + 1))))) |
206 | 152, 205 | sylbid 239 |
. . . . . . 7
β’ (((π β§ π β β) β§ (π + 1) β β) β ((seq1( Β·
, πΉ)βπ) β€ ((2 Β· π)β(Οβπ)) β (seq1( Β· ,
πΉ)β(π + 1)) β€ ((2 Β· π)β(Οβ(π + 1))))) |
207 | 157 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ Β¬ (π + 1) β β) β
(seq1( Β· , πΉ)β(π + 1)) = ((seq1( Β· , πΉ)βπ) Β· (πΉβ(π + 1)))) |
208 | | iffalse 4500 |
. . . . . . . . . . . 12
β’ (Β¬
(π + 1) β β
β if((π + 1) β
β, ((π +
1)β((π + 1) pCnt ((2
Β· π)Cπ))), 1) = 1) |
209 | 169, 208 | sylan9eq 2797 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ Β¬ (π + 1) β β) β
(πΉβ(π + 1)) = 1) |
210 | 209 | oveq2d 7378 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ Β¬ (π + 1) β β) β
((seq1( Β· , πΉ)βπ) Β· (πΉβ(π + 1))) = ((seq1( Β· , πΉ)βπ) Β· 1)) |
211 | 126 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ Β¬ (π + 1) β β) β
(seq1( Β· , πΉ)βπ) β β) |
212 | 211 | nncnd 12176 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ Β¬ (π + 1) β β) β
(seq1( Β· , πΉ)βπ) β β) |
213 | 212 | mulid1d 11179 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ Β¬ (π + 1) β β) β
((seq1( Β· , πΉ)βπ) Β· 1) = (seq1( Β· , πΉ)βπ)) |
214 | 207, 210,
213 | 3eqtrd 2781 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ Β¬ (π + 1) β β) β
(seq1( Β· , πΉ)β(π + 1)) = (seq1( Β· , πΉ)βπ)) |
215 | | ppinprm 26517 |
. . . . . . . . . . 11
β’ ((π β β€ β§ Β¬
(π + 1) β β)
β (Οβ(π + 1)) = (Οβπ)) |
216 | 144, 215 | sylan 581 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ Β¬ (π + 1) β β) β
(Οβ(π + 1))
= (Οβπ)) |
217 | 216 | oveq2d 7378 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ Β¬ (π + 1) β β) β ((2
Β· π)β(Οβ(π + 1))) = ((2 Β· π)β(Οβπ))) |
218 | 214, 217 | breq12d 5123 |
. . . . . . . 8
β’ (((π β§ π β β) β§ Β¬ (π + 1) β β) β
((seq1( Β· , πΉ)β(π + 1)) β€ ((2 Β· π)β(Οβ(π + 1))) β (seq1( Β· ,
πΉ)βπ) β€ ((2 Β· π)β(Οβπ)))) |
219 | 218 | biimprd 248 |
. . . . . . 7
β’ (((π β§ π β β) β§ Β¬ (π + 1) β β) β
((seq1( Β· , πΉ)βπ) β€ ((2 Β· π)β(Οβπ)) β (seq1( Β· , πΉ)β(π + 1)) β€ ((2 Β· π)β(Οβ(π + 1))))) |
220 | 206, 219 | pm2.61dan 812 |
. . . . . 6
β’ ((π β§ π β β) β ((seq1( Β· ,
πΉ)βπ) β€ ((2 Β· π)β(Οβπ)) β (seq1( Β· , πΉ)β(π + 1)) β€ ((2 Β· π)β(Οβ(π + 1))))) |
221 | 220 | expcom 415 |
. . . . 5
β’ (π β β β (π β ((seq1( Β· , πΉ)βπ) β€ ((2 Β· π)β(Οβπ)) β (seq1( Β· , πΉ)β(π + 1)) β€ ((2 Β· π)β(Οβ(π + 1)))))) |
222 | 221 | a2d 29 |
. . . 4
β’ (π β β β ((π β (seq1( Β· , πΉ)βπ) β€ ((2 Β· π)β(Οβπ))) β (π β (seq1( Β· , πΉ)β(π + 1)) β€ ((2 Β· π)β(Οβ(π + 1)))))) |
223 | 93, 98, 103, 108, 125, 222 | nnind 12178 |
. . 3
β’ (π β β β (π β (seq1( Β· , πΉ)βπ) β€ ((2 Β· π)β(Οβπ)))) |
224 | 74, 223 | mpcom 38 |
. 2
β’ (π β (seq1( Β· , πΉ)βπ) β€ ((2 Β· π)β(Οβπ))) |
225 | | cxpexp 26039 |
. . . 4
β’ (((2
Β· π) β β
β§ (Οβπ)
β β0) β ((2 Β· π)βπ(Οβπ)) = ((2 Β· π)β(Οβπ))) |
226 | 123, 79, 225 | syl2anc 585 |
. . 3
β’ (π β ((2 Β· π)βπ(Οβπ)) = ((2 Β· π)β(Οβπ))) |
227 | 79 | nn0red 12481 |
. . . . 5
β’ (π β (Οβπ) β
β) |
228 | | nndivre 12201 |
. . . . . . 7
β’ ((π β β β§ 3 β
β) β (π / 3)
β β) |
229 | 77, 16, 228 | sylancl 587 |
. . . . . 6
β’ (π β (π / 3) β β) |
230 | | readdcl 11141 |
. . . . . 6
β’ (((π / 3) β β β§ 2
β β) β ((π
/ 3) + 2) β β) |
231 | 229, 48, 230 | sylancl 587 |
. . . . 5
β’ (π β ((π / 3) + 2) β β) |
232 | 74 | nnnn0d 12480 |
. . . . . . 7
β’ (π β π β
β0) |
233 | 232 | nn0ge0d 12483 |
. . . . . 6
β’ (π β 0 β€ π) |
234 | | ppiub 26568 |
. . . . . 6
β’ ((π β β β§ 0 β€
π) β
(Οβπ) β€
((π / 3) +
2)) |
235 | 77, 233, 234 | syl2anc 585 |
. . . . 5
β’ (π β (Οβπ) β€ ((π / 3) + 2)) |
236 | 48 | a1i 11 |
. . . . . 6
β’ (π β 2 β
β) |
237 | | flle 13711 |
. . . . . . . . 9
β’
((ββ(2 Β· π)) β β β
(ββ(ββ(2 Β· π))) β€ (ββ(2 Β· π))) |
238 | 28, 237 | syl 17 |
. . . . . . . 8
β’ (π β
(ββ(ββ(2 Β· π))) β€ (ββ(2 Β· π))) |
239 | 17, 238 | eqbrtrid 5145 |
. . . . . . 7
β’ (π β π β€ (ββ(2 Β· π))) |
240 | | 3re 12240 |
. . . . . . . . . 10
β’ 3 β
β |
241 | | 3pos 12265 |
. . . . . . . . . 10
β’ 0 <
3 |
242 | 240, 241 | pm3.2i 472 |
. . . . . . . . 9
β’ (3 β
β β§ 0 < 3) |
243 | 242 | a1i 11 |
. . . . . . . 8
β’ (π β (3 β β β§ 0
< 3)) |
244 | | lediv1 12027 |
. . . . . . . 8
β’ ((π β β β§
(ββ(2 Β· π)) β β β§ (3 β β
β§ 0 < 3)) β (π
β€ (ββ(2 Β· π)) β (π / 3) β€ ((ββ(2 Β· π)) / 3))) |
245 | 77, 28, 243, 244 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π β€ (ββ(2 Β· π)) β (π / 3) β€ ((ββ(2 Β· π)) / 3))) |
246 | 239, 245 | mpbid 231 |
. . . . . 6
β’ (π β (π / 3) β€ ((ββ(2 Β· π)) / 3)) |
247 | 229, 83, 236, 246 | leadd1dd 11776 |
. . . . 5
β’ (π β ((π / 3) + 2) β€ (((ββ(2 Β·
π)) / 3) +
2)) |
248 | 227, 231,
85, 235, 247 | letrd 11319 |
. . . 4
β’ (π β (Οβπ) β€ (((ββ(2
Β· π)) / 3) +
2)) |
249 | | 2t1e2 12323 |
. . . . . . . 8
β’ (2
Β· 1) = 2 |
250 | 6 | nnge1d 12208 |
. . . . . . . . 9
β’ (π β 1 β€ π) |
251 | | 1re 11162 |
. . . . . . . . . . 11
β’ 1 β
β |
252 | | lemul2 12015 |
. . . . . . . . . . 11
β’ ((1
β β β§ π
β β β§ (2 β β β§ 0 < 2)) β (1 β€ π β (2 Β· 1) β€ (2
Β· π))) |
253 | 251, 50, 252 | mp3an13 1453 |
. . . . . . . . . 10
β’ (π β β β (1 β€
π β (2 Β· 1)
β€ (2 Β· π))) |
254 | 46, 253 | syl 17 |
. . . . . . . . 9
β’ (π β (1 β€ π β (2 Β· 1) β€ (2 Β·
π))) |
255 | 250, 254 | mpbid 231 |
. . . . . . . 8
β’ (π β (2 Β· 1) β€ (2
Β· π)) |
256 | 249, 255 | eqbrtrrid 5146 |
. . . . . . 7
β’ (π β 2 β€ (2 Β· π)) |
257 | 18 | eluz1i 12778 |
. . . . . . 7
β’ ((2
Β· π) β
(β€β₯β2) β ((2 Β· π) β β€ β§ 2 β€ (2 Β·
π))) |
258 | 21, 256, 257 | sylanbrc 584 |
. . . . . 6
β’ (π β (2 Β· π) β
(β€β₯β2)) |
259 | | eluz2gt1 12852 |
. . . . . 6
β’ ((2
Β· π) β
(β€β₯β2) β 1 < (2 Β· π)) |
260 | 258, 259 | syl 17 |
. . . . 5
β’ (π β 1 < (2 Β· π)) |
261 | 22, 260, 227, 85 | cxpled 26091 |
. . . 4
β’ (π β ((Οβπ) β€ (((ββ(2
Β· π)) / 3) + 2)
β ((2 Β· π)βπ(Οβπ)) β€ ((2 Β· π)βπ(((ββ(2
Β· π)) / 3) +
2)))) |
262 | 248, 261 | mpbid 231 |
. . 3
β’ (π β ((2 Β· π)βπ(Οβπ)) β€ ((2 Β· π)βπ(((ββ(2
Β· π)) / 3) +
2))) |
263 | 226, 262 | eqbrtrrd 5134 |
. 2
β’ (π β ((2 Β· π)β(Οβπ)) β€ ((2 Β· π)βπ(((ββ(2
Β· π)) / 3) +
2))) |
264 | 76, 81, 86, 224, 263 | letrd 11319 |
1
β’ (π β (seq1( Β· , πΉ)βπ) β€ ((2 Β· π)βπ(((ββ(2
Β· π)) / 3) +
2))) |