Step | Hyp | Ref
| Expression |
1 | | eluzge2nn0 12867 |
. . . 4
β’ (π΄ β
(β€β₯β2) β π΄ β
β0) |
2 | | nn0eo 47167 |
. . . 4
β’ (π΄ β β0
β ((π΄ / 2) β
β0 β¨ ((π΄ + 1) / 2) β
β0)) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π΄ β
(β€β₯β2) β ((π΄ / 2) β β0 β¨
((π΄ + 1) / 2) β
β0)) |
4 | | dignn0ehalf 47256 |
. . . . . . 7
β’ (((π΄ / 2) β β0
β§ π΄ β
β0 β§ πΌ
β β0) β ((πΌ + 1)(digitβ2)π΄) = (πΌ(digitβ2)(π΄ / 2))) |
5 | 1, 4 | syl3an2 1164 |
. . . . . 6
β’ (((π΄ / 2) β β0
β§ π΄ β
(β€β₯β2) β§ πΌ β β0) β ((πΌ + 1)(digitβ2)π΄) = (πΌ(digitβ2)(π΄ / 2))) |
6 | | eluzelz 12828 |
. . . . . . . . . 10
β’ (π΄ β
(β€β₯β2) β π΄ β β€) |
7 | | nn0z 12579 |
. . . . . . . . . 10
β’ ((π΄ / 2) β β0
β (π΄ / 2) β
β€) |
8 | | zefldiv2 47169 |
. . . . . . . . . 10
β’ ((π΄ β β€ β§ (π΄ / 2) β β€) β
(ββ(π΄ / 2)) =
(π΄ / 2)) |
9 | 6, 7, 8 | syl2anr 597 |
. . . . . . . . 9
β’ (((π΄ / 2) β β0
β§ π΄ β
(β€β₯β2)) β (ββ(π΄ / 2)) = (π΄ / 2)) |
10 | 9 | eqcomd 2738 |
. . . . . . . 8
β’ (((π΄ / 2) β β0
β§ π΄ β
(β€β₯β2)) β (π΄ / 2) = (ββ(π΄ / 2))) |
11 | 10 | 3adant3 1132 |
. . . . . . 7
β’ (((π΄ / 2) β β0
β§ π΄ β
(β€β₯β2) β§ πΌ β β0) β (π΄ / 2) = (ββ(π΄ / 2))) |
12 | 11 | oveq2d 7421 |
. . . . . 6
β’ (((π΄ / 2) β β0
β§ π΄ β
(β€β₯β2) β§ πΌ β β0) β (πΌ(digitβ2)(π΄ / 2)) = (πΌ(digitβ2)(ββ(π΄ / 2)))) |
13 | 5, 12 | eqtrd 2772 |
. . . . 5
β’ (((π΄ / 2) β β0
β§ π΄ β
(β€β₯β2) β§ πΌ β β0) β ((πΌ + 1)(digitβ2)π΄) = (πΌ(digitβ2)(ββ(π΄ / 2)))) |
14 | 13 | 3exp 1119 |
. . . 4
β’ ((π΄ / 2) β β0
β (π΄ β
(β€β₯β2) β (πΌ β β0 β ((πΌ + 1)(digitβ2)π΄) = (πΌ(digitβ2)(ββ(π΄ / 2)))))) |
15 | 6 | 3ad2ant2 1134 |
. . . . . . . 8
β’ ((((π΄ + 1) / 2) β
β0 β§ π΄
β (β€β₯β2) β§ πΌ β β0) β π΄ β
β€) |
16 | | simp2 1137 |
. . . . . . . . 9
β’ ((((π΄ + 1) / 2) β
β0 β§ π΄
β (β€β₯β2) β§ πΌ β β0) β π΄ β
(β€β₯β2)) |
17 | | simp1 1136 |
. . . . . . . . 9
β’ ((((π΄ + 1) / 2) β
β0 β§ π΄
β (β€β₯β2) β§ πΌ β β0) β ((π΄ + 1) / 2) β
β0) |
18 | | nno 16321 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ ((π΄ + 1) / 2) β β0)
β ((π΄ β 1) / 2)
β β) |
19 | 16, 17, 18 | syl2anc 584 |
. . . . . . . 8
β’ ((((π΄ + 1) / 2) β
β0 β§ π΄
β (β€β₯β2) β§ πΌ β β0) β ((π΄ β 1) / 2) β
β) |
20 | | simp3 1138 |
. . . . . . . 8
β’ ((((π΄ + 1) / 2) β
β0 β§ π΄
β (β€β₯β2) β§ πΌ β β0) β πΌ β
β0) |
21 | | dignn0flhalflem2 47255 |
. . . . . . . 8
β’ ((π΄ β β€ β§ ((π΄ β 1) / 2) β β
β§ πΌ β
β0) β (ββ(π΄ / (2β(πΌ + 1)))) =
(ββ((ββ(π΄ / 2)) / (2βπΌ)))) |
22 | 15, 19, 20, 21 | syl3anc 1371 |
. . . . . . 7
β’ ((((π΄ + 1) / 2) β
β0 β§ π΄
β (β€β₯β2) β§ πΌ β β0) β
(ββ(π΄ /
(2β(πΌ + 1)))) =
(ββ((ββ(π΄ / 2)) / (2βπΌ)))) |
23 | 22 | oveq1d 7420 |
. . . . . 6
β’ ((((π΄ + 1) / 2) β
β0 β§ π΄
β (β€β₯β2) β§ πΌ β β0) β
((ββ(π΄ /
(2β(πΌ + 1)))) mod 2) =
((ββ((ββ(π΄ / 2)) / (2βπΌ))) mod 2)) |
24 | | 2nn 12281 |
. . . . . . . 8
β’ 2 β
β |
25 | 24 | a1i 11 |
. . . . . . 7
β’ ((((π΄ + 1) / 2) β
β0 β§ π΄
β (β€β₯β2) β§ πΌ β β0) β 2 β
β) |
26 | | peano2nn0 12508 |
. . . . . . . 8
β’ (πΌ β β0
β (πΌ + 1) β
β0) |
27 | 26 | 3ad2ant3 1135 |
. . . . . . 7
β’ ((((π΄ + 1) / 2) β
β0 β§ π΄
β (β€β₯β2) β§ πΌ β β0) β (πΌ + 1) β
β0) |
28 | | nn0rp0 13428 |
. . . . . . . . 9
β’ (π΄ β β0
β π΄ β
(0[,)+β)) |
29 | 1, 28 | syl 17 |
. . . . . . . 8
β’ (π΄ β
(β€β₯β2) β π΄ β (0[,)+β)) |
30 | 29 | 3ad2ant2 1134 |
. . . . . . 7
β’ ((((π΄ + 1) / 2) β
β0 β§ π΄
β (β€β₯β2) β§ πΌ β β0) β π΄ β
(0[,)+β)) |
31 | | nn0digval 47239 |
. . . . . . 7
β’ ((2
β β β§ (πΌ +
1) β β0 β§ π΄ β (0[,)+β)) β ((πΌ + 1)(digitβ2)π΄) = ((ββ(π΄ / (2β(πΌ + 1)))) mod 2)) |
32 | 25, 27, 30, 31 | syl3anc 1371 |
. . . . . 6
β’ ((((π΄ + 1) / 2) β
β0 β§ π΄
β (β€β₯β2) β§ πΌ β β0) β ((πΌ + 1)(digitβ2)π΄) = ((ββ(π΄ / (2β(πΌ + 1)))) mod 2)) |
33 | | eluzelre 12829 |
. . . . . . . . . . 11
β’ (π΄ β
(β€β₯β2) β π΄ β β) |
34 | 33 | rehalfcld 12455 |
. . . . . . . . . 10
β’ (π΄ β
(β€β₯β2) β (π΄ / 2) β β) |
35 | 1 | nn0ge0d 12531 |
. . . . . . . . . . 11
β’ (π΄ β
(β€β₯β2) β 0 β€ π΄) |
36 | | 2re 12282 |
. . . . . . . . . . . . 13
β’ 2 β
β |
37 | | 2pos 12311 |
. . . . . . . . . . . . 13
β’ 0 <
2 |
38 | 36, 37 | pm3.2i 471 |
. . . . . . . . . . . 12
β’ (2 β
β β§ 0 < 2) |
39 | 38 | a1i 11 |
. . . . . . . . . . 11
β’ (π΄ β
(β€β₯β2) β (2 β β β§ 0 <
2)) |
40 | | divge0 12079 |
. . . . . . . . . . 11
β’ (((π΄ β β β§ 0 β€
π΄) β§ (2 β β
β§ 0 < 2)) β 0 β€ (π΄ / 2)) |
41 | 33, 35, 39, 40 | syl21anc 836 |
. . . . . . . . . 10
β’ (π΄ β
(β€β₯β2) β 0 β€ (π΄ / 2)) |
42 | | flge0nn0 13781 |
. . . . . . . . . 10
β’ (((π΄ / 2) β β β§ 0
β€ (π΄ / 2)) β
(ββ(π΄ / 2))
β β0) |
43 | 34, 41, 42 | syl2anc 584 |
. . . . . . . . 9
β’ (π΄ β
(β€β₯β2) β (ββ(π΄ / 2)) β
β0) |
44 | 43 | 3ad2ant2 1134 |
. . . . . . . 8
β’ ((((π΄ + 1) / 2) β
β0 β§ π΄
β (β€β₯β2) β§ πΌ β β0) β
(ββ(π΄ / 2))
β β0) |
45 | | nn0rp0 13428 |
. . . . . . . 8
β’
((ββ(π΄ /
2)) β β0 β (ββ(π΄ / 2)) β
(0[,)+β)) |
46 | 44, 45 | syl 17 |
. . . . . . 7
β’ ((((π΄ + 1) / 2) β
β0 β§ π΄
β (β€β₯β2) β§ πΌ β β0) β
(ββ(π΄ / 2))
β (0[,)+β)) |
47 | | nn0digval 47239 |
. . . . . . 7
β’ ((2
β β β§ πΌ
β β0 β§ (ββ(π΄ / 2)) β (0[,)+β)) β (πΌ(digitβ2)(ββ(π΄ / 2))) =
((ββ((ββ(π΄ / 2)) / (2βπΌ))) mod 2)) |
48 | 25, 20, 46, 47 | syl3anc 1371 |
. . . . . 6
β’ ((((π΄ + 1) / 2) β
β0 β§ π΄
β (β€β₯β2) β§ πΌ β β0) β (πΌ(digitβ2)(ββ(π΄ / 2))) =
((ββ((ββ(π΄ / 2)) / (2βπΌ))) mod 2)) |
49 | 23, 32, 48 | 3eqtr4d 2782 |
. . . . 5
β’ ((((π΄ + 1) / 2) β
β0 β§ π΄
β (β€β₯β2) β§ πΌ β β0) β ((πΌ + 1)(digitβ2)π΄) = (πΌ(digitβ2)(ββ(π΄ / 2)))) |
50 | 49 | 3exp 1119 |
. . . 4
β’ (((π΄ + 1) / 2) β
β0 β (π΄ β (β€β₯β2)
β (πΌ β
β0 β ((πΌ + 1)(digitβ2)π΄) = (πΌ(digitβ2)(ββ(π΄ / 2)))))) |
51 | 14, 50 | jaoi 855 |
. . 3
β’ (((π΄ / 2) β β0
β¨ ((π΄ + 1) / 2) β
β0) β (π΄ β (β€β₯β2)
β (πΌ β
β0 β ((πΌ + 1)(digitβ2)π΄) = (πΌ(digitβ2)(ββ(π΄ / 2)))))) |
52 | 3, 51 | mpcom 38 |
. 2
β’ (π΄ β
(β€β₯β2) β (πΌ β β0 β ((πΌ + 1)(digitβ2)π΄) = (πΌ(digitβ2)(ββ(π΄ / 2))))) |
53 | 52 | imp 407 |
1
β’ ((π΄ β
(β€β₯β2) β§ πΌ β β0) β ((πΌ + 1)(digitβ2)π΄) = (πΌ(digitβ2)(ββ(π΄ / 2)))) |