Step | Hyp | Ref
| Expression |
1 | | nn0cn 12481 |
. . . . . . 7
β’ (π΄ β β0
β π΄ β
β) |
2 | 1 | 3ad2ant2 1134 |
. . . . . 6
β’ (((π΄ / 2) β β0
β§ π΄ β
β0 β§ πΌ
β β0) β π΄ β β) |
3 | | 2cnne0 12421 |
. . . . . . 7
β’ (2 β
β β§ 2 β 0) |
4 | 3 | a1i 11 |
. . . . . 6
β’ (((π΄ / 2) β β0
β§ π΄ β
β0 β§ πΌ
β β0) β (2 β β β§ 2 β
0)) |
5 | | 2nn0 12488 |
. . . . . . . . . . 11
β’ 2 β
β0 |
6 | 5 | a1i 11 |
. . . . . . . . . 10
β’ (πΌ β β0
β 2 β β0) |
7 | | id 22 |
. . . . . . . . . 10
β’ (πΌ β β0
β πΌ β
β0) |
8 | 6, 7 | nn0expcld 14208 |
. . . . . . . . 9
β’ (πΌ β β0
β (2βπΌ) β
β0) |
9 | 8 | nn0cnd 12533 |
. . . . . . . 8
β’ (πΌ β β0
β (2βπΌ) β
β) |
10 | | 2cnd 12289 |
. . . . . . . . 9
β’ (πΌ β β0
β 2 β β) |
11 | | 2ne0 12315 |
. . . . . . . . . 10
β’ 2 β
0 |
12 | 11 | a1i 11 |
. . . . . . . . 9
β’ (πΌ β β0
β 2 β 0) |
13 | | nn0z 12582 |
. . . . . . . . 9
β’ (πΌ β β0
β πΌ β
β€) |
14 | 10, 12, 13 | expne0d 14116 |
. . . . . . . 8
β’ (πΌ β β0
β (2βπΌ) β
0) |
15 | 9, 14 | jca 512 |
. . . . . . 7
β’ (πΌ β β0
β ((2βπΌ) β
β β§ (2βπΌ)
β 0)) |
16 | 15 | 3ad2ant3 1135 |
. . . . . 6
β’ (((π΄ / 2) β β0
β§ π΄ β
β0 β§ πΌ
β β0) β ((2βπΌ) β β β§ (2βπΌ) β 0)) |
17 | | divdiv1 11924 |
. . . . . 6
β’ ((π΄ β β β§ (2 β
β β§ 2 β 0) β§ ((2βπΌ) β β β§ (2βπΌ) β 0)) β ((π΄ / 2) / (2βπΌ)) = (π΄ / (2 Β· (2βπΌ)))) |
18 | 2, 4, 16, 17 | syl3anc 1371 |
. . . . 5
β’ (((π΄ / 2) β β0
β§ π΄ β
β0 β§ πΌ
β β0) β ((π΄ / 2) / (2βπΌ)) = (π΄ / (2 Β· (2βπΌ)))) |
19 | 10, 9 | mulcomd 11234 |
. . . . . . . 8
β’ (πΌ β β0
β (2 Β· (2βπΌ)) = ((2βπΌ) Β· 2)) |
20 | 19 | 3ad2ant3 1135 |
. . . . . . 7
β’ (((π΄ / 2) β β0
β§ π΄ β
β0 β§ πΌ
β β0) β (2 Β· (2βπΌ)) = ((2βπΌ) Β· 2)) |
21 | | 2cnd 12289 |
. . . . . . . 8
β’ (((π΄ / 2) β β0
β§ π΄ β
β0 β§ πΌ
β β0) β 2 β β) |
22 | | simp3 1138 |
. . . . . . . 8
β’ (((π΄ / 2) β β0
β§ π΄ β
β0 β§ πΌ
β β0) β πΌ β
β0) |
23 | 21, 22 | expp1d 14111 |
. . . . . . 7
β’ (((π΄ / 2) β β0
β§ π΄ β
β0 β§ πΌ
β β0) β (2β(πΌ + 1)) = ((2βπΌ) Β· 2)) |
24 | 20, 23 | eqtr4d 2775 |
. . . . . 6
β’ (((π΄ / 2) β β0
β§ π΄ β
β0 β§ πΌ
β β0) β (2 Β· (2βπΌ)) = (2β(πΌ + 1))) |
25 | 24 | oveq2d 7424 |
. . . . 5
β’ (((π΄ / 2) β β0
β§ π΄ β
β0 β§ πΌ
β β0) β (π΄ / (2 Β· (2βπΌ))) = (π΄ / (2β(πΌ + 1)))) |
26 | 18, 25 | eqtr2d 2773 |
. . . 4
β’ (((π΄ / 2) β β0
β§ π΄ β
β0 β§ πΌ
β β0) β (π΄ / (2β(πΌ + 1))) = ((π΄ / 2) / (2βπΌ))) |
27 | 26 | fveq2d 6895 |
. . 3
β’ (((π΄ / 2) β β0
β§ π΄ β
β0 β§ πΌ
β β0) β (ββ(π΄ / (2β(πΌ + 1)))) = (ββ((π΄ / 2) / (2βπΌ)))) |
28 | 27 | oveq1d 7423 |
. 2
β’ (((π΄ / 2) β β0
β§ π΄ β
β0 β§ πΌ
β β0) β ((ββ(π΄ / (2β(πΌ + 1)))) mod 2) = ((ββ((π΄ / 2) / (2βπΌ))) mod 2)) |
29 | | 2nn 12284 |
. . . 4
β’ 2 β
β |
30 | 29 | a1i 11 |
. . 3
β’ (((π΄ / 2) β β0
β§ π΄ β
β0 β§ πΌ
β β0) β 2 β β) |
31 | | peano2nn0 12511 |
. . . 4
β’ (πΌ β β0
β (πΌ + 1) β
β0) |
32 | 31 | 3ad2ant3 1135 |
. . 3
β’ (((π΄ / 2) β β0
β§ π΄ β
β0 β§ πΌ
β β0) β (πΌ + 1) β
β0) |
33 | | nn0rp0 13431 |
. . . 4
β’ (π΄ β β0
β π΄ β
(0[,)+β)) |
34 | 33 | 3ad2ant2 1134 |
. . 3
β’ (((π΄ / 2) β β0
β§ π΄ β
β0 β§ πΌ
β β0) β π΄ β (0[,)+β)) |
35 | | nn0digval 47276 |
. . 3
β’ ((2
β β β§ (πΌ +
1) β β0 β§ π΄ β (0[,)+β)) β ((πΌ + 1)(digitβ2)π΄) = ((ββ(π΄ / (2β(πΌ + 1)))) mod 2)) |
36 | 30, 32, 34, 35 | syl3anc 1371 |
. 2
β’ (((π΄ / 2) β β0
β§ π΄ β
β0 β§ πΌ
β β0) β ((πΌ + 1)(digitβ2)π΄) = ((ββ(π΄ / (2β(πΌ + 1)))) mod 2)) |
37 | | nn0rp0 13431 |
. . . 4
β’ ((π΄ / 2) β β0
β (π΄ / 2) β
(0[,)+β)) |
38 | 37 | 3ad2ant1 1133 |
. . 3
β’ (((π΄ / 2) β β0
β§ π΄ β
β0 β§ πΌ
β β0) β (π΄ / 2) β
(0[,)+β)) |
39 | | nn0digval 47276 |
. . 3
β’ ((2
β β β§ πΌ
β β0 β§ (π΄ / 2) β (0[,)+β)) β (πΌ(digitβ2)(π΄ / 2)) = ((ββ((π΄ / 2) / (2βπΌ))) mod 2)) |
40 | 30, 22, 38, 39 | syl3anc 1371 |
. 2
β’ (((π΄ / 2) β β0
β§ π΄ β
β0 β§ πΌ
β β0) β (πΌ(digitβ2)(π΄ / 2)) = ((ββ((π΄ / 2) / (2βπΌ))) mod 2)) |
41 | 28, 36, 40 | 3eqtr4d 2782 |
1
β’ (((π΄ / 2) β β0
β§ π΄ β
β0 β§ πΌ
β β0) β ((πΌ + 1)(digitβ2)π΄) = (πΌ(digitβ2)(π΄ / 2))) |