Step | Hyp | Ref
| Expression |
1 | | 2nn 12233 |
. . . 4
β’ 2 β
β |
2 | 1 | a1i 11 |
. . 3
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β 2 β β) |
3 | | 0nn0 12435 |
. . . 4
β’ 0 β
β0 |
4 | 3 | a1i 11 |
. . 3
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β 0 β β0) |
5 | | nn0rp0 13379 |
. . . 4
β’ (π β β0
β π β
(0[,)+β)) |
6 | 5 | adantr 482 |
. . 3
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β π β (0[,)+β)) |
7 | | nn0digval 46760 |
. . 3
β’ ((2
β β β§ 0 β β0 β§ π β (0[,)+β)) β
(0(digitβ2)π) =
((ββ(π /
(2β0))) mod 2)) |
8 | 2, 4, 6, 7 | syl3anc 1372 |
. 2
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β (0(digitβ2)π) = ((ββ(π / (2β0))) mod 2)) |
9 | | 2cn 12235 |
. . . . . . . 8
β’ 2 β
β |
10 | | exp0 13978 |
. . . . . . . 8
β’ (2 β
β β (2β0) = 1) |
11 | 9, 10 | mp1i 13 |
. . . . . . 7
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β (2β0) = 1) |
12 | 11 | oveq2d 7378 |
. . . . . 6
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β (π / (2β0)) = (π / 1)) |
13 | | nn0cn 12430 |
. . . . . . . 8
β’ (π β β0
β π β
β) |
14 | 13 | div1d 11930 |
. . . . . . 7
β’ (π β β0
β (π / 1) = π) |
15 | 14 | adantr 482 |
. . . . . 6
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β (π / 1) = π) |
16 | 12, 15 | eqtrd 2777 |
. . . . 5
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β (π / (2β0)) = π) |
17 | 16 | fveq2d 6851 |
. . . 4
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β (ββ(π / (2β0))) = (ββπ)) |
18 | 17 | oveq1d 7377 |
. . 3
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β ((ββ(π / (2β0))) mod 2) =
((ββπ) mod
2)) |
19 | | nn0z 12531 |
. . . . . . 7
β’ (π β β0
β π β
β€) |
20 | | flid 13720 |
. . . . . . 7
β’ (π β β€ β
(ββπ) = π) |
21 | 19, 20 | syl 17 |
. . . . . 6
β’ (π β β0
β (ββπ) =
π) |
22 | 21 | oveq1d 7377 |
. . . . 5
β’ (π β β0
β ((ββπ)
mod 2) = (π mod
2)) |
23 | 22 | adantr 482 |
. . . 4
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β ((ββπ) mod 2) = (π mod 2)) |
24 | | nn0z 12531 |
. . . . . . . 8
β’ (((π + 1) / 2) β
β0 β ((π + 1) / 2) β β€) |
25 | 24 | adantl 483 |
. . . . . . 7
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β ((π + 1) / 2) β β€) |
26 | | 2z 12542 |
. . . . . . . . 9
β’ 2 β
β€ |
27 | 26 | a1i 11 |
. . . . . . . 8
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β 2 β β€) |
28 | | 2ne0 12264 |
. . . . . . . . 9
β’ 2 β
0 |
29 | 28 | a1i 11 |
. . . . . . . 8
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β 2 β 0) |
30 | | peano2nn0 12460 |
. . . . . . . . . 10
β’ (π β β0
β (π + 1) β
β0) |
31 | 30 | nn0zd 12532 |
. . . . . . . . 9
β’ (π β β0
β (π + 1) β
β€) |
32 | 31 | adantr 482 |
. . . . . . . 8
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β (π + 1) β β€) |
33 | | dvdsval2 16146 |
. . . . . . . 8
β’ ((2
β β€ β§ 2 β 0 β§ (π + 1) β β€) β (2 β₯
(π + 1) β ((π + 1) / 2) β
β€)) |
34 | 27, 29, 32, 33 | syl3anc 1372 |
. . . . . . 7
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β (2 β₯ (π + 1) β ((π + 1) / 2) β β€)) |
35 | 25, 34 | mpbird 257 |
. . . . . 6
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β 2 β₯ (π + 1)) |
36 | | oddp1even 16233 |
. . . . . . . 8
β’ (π β β€ β (Β¬ 2
β₯ π β 2 β₯
(π + 1))) |
37 | 19, 36 | syl 17 |
. . . . . . 7
β’ (π β β0
β (Β¬ 2 β₯ π
β 2 β₯ (π +
1))) |
38 | 37 | adantr 482 |
. . . . . 6
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β (Β¬ 2 β₯ π β 2 β₯ (π + 1))) |
39 | 35, 38 | mpbird 257 |
. . . . 5
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β Β¬ 2 β₯ π) |
40 | 19 | adantr 482 |
. . . . . 6
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β π β β€) |
41 | | mod2eq1n2dvds 16236 |
. . . . . 6
β’ (π β β€ β ((π mod 2) = 1 β Β¬ 2
β₯ π)) |
42 | 40, 41 | syl 17 |
. . . . 5
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β ((π mod 2) = 1 β Β¬ 2 β₯ π)) |
43 | 39, 42 | mpbird 257 |
. . . 4
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β (π mod 2) = 1) |
44 | 23, 43 | eqtrd 2777 |
. . 3
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β ((ββπ) mod 2) = 1) |
45 | 18, 44 | eqtrd 2777 |
. 2
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β ((ββ(π / (2β0))) mod 2) = 1) |
46 | 8, 45 | eqtrd 2777 |
1
β’ ((π β β0
β§ ((π + 1) / 2) β
β0) β (0(digitβ2)π) = 1) |