Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . 3
β’ (π΅ β β β π΅ β
β) |
2 | | eldifi 4125 |
. . 3
β’ (πΎ β (β€ β
β0) β πΎ β β€) |
3 | | nn0re 12477 |
. . . 4
β’ (π β β0
β π β
β) |
4 | | nn0ge0 12493 |
. . . 4
β’ (π β β0
β 0 β€ π) |
5 | | elrege0 13427 |
. . . 4
β’ (π β (0[,)+β) β
(π β β β§ 0
β€ π)) |
6 | 3, 4, 5 | sylanbrc 583 |
. . 3
β’ (π β β0
β π β
(0[,)+β)) |
7 | | digval 47237 |
. . 3
β’ ((π΅ β β β§ πΎ β β€ β§ π β (0[,)+β)) β
(πΎ(digitβπ΅)π) = ((ββ((π΅β-πΎ) Β· π)) mod π΅)) |
8 | 1, 2, 6, 7 | syl3an 1160 |
. 2
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β (πΎ(digitβπ΅)π) = ((ββ((π΅β-πΎ) Β· π)) mod π΅)) |
9 | | nnz 12575 |
. . . . . . . 8
β’ (π΅ β β β π΅ β
β€) |
10 | | eldif 3957 |
. . . . . . . . . 10
β’ (πΎ β (β€ β
β0) β (πΎ β β€ β§ Β¬ πΎ β
β0)) |
11 | | znnn0nn 12669 |
. . . . . . . . . 10
β’ ((πΎ β β€ β§ Β¬
πΎ β
β0) β -πΎ β β) |
12 | 10, 11 | sylbi 216 |
. . . . . . . . 9
β’ (πΎ β (β€ β
β0) β -πΎ β β) |
13 | 12 | nnnn0d 12528 |
. . . . . . . 8
β’ (πΎ β (β€ β
β0) β -πΎ β
β0) |
14 | | zexpcl 14038 |
. . . . . . . 8
β’ ((π΅ β β€ β§ -πΎ β β0)
β (π΅β-πΎ) β
β€) |
15 | 9, 13, 14 | syl2an 596 |
. . . . . . 7
β’ ((π΅ β β β§ πΎ β (β€ β
β0)) β (π΅β-πΎ) β β€) |
16 | 15 | 3adant3 1132 |
. . . . . 6
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β (π΅β-πΎ) β β€) |
17 | | nn0z 12579 |
. . . . . . 7
β’ (π β β0
β π β
β€) |
18 | 17 | 3ad2ant3 1135 |
. . . . . 6
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β π β
β€) |
19 | 16, 18 | zmulcld 12668 |
. . . . 5
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β ((π΅β-πΎ) Β· π) β β€) |
20 | | flid 13769 |
. . . . 5
β’ (((π΅β-πΎ) Β· π) β β€ β
(ββ((π΅β-πΎ) Β· π)) = ((π΅β-πΎ) Β· π)) |
21 | 19, 20 | syl 17 |
. . . 4
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β
(ββ((π΅β-πΎ) Β· π)) = ((π΅β-πΎ) Β· π)) |
22 | 21 | oveq1d 7420 |
. . 3
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β
((ββ((π΅β-πΎ) Β· π)) mod π΅) = (((π΅β-πΎ) Β· π) mod π΅)) |
23 | | nnre 12215 |
. . . . . . . . . 10
β’ (π΅ β β β π΅ β
β) |
24 | | reexpcl 14040 |
. . . . . . . . . 10
β’ ((π΅ β β β§ -πΎ β β0)
β (π΅β-πΎ) β
β) |
25 | 23, 13, 24 | syl2an 596 |
. . . . . . . . 9
β’ ((π΅ β β β§ πΎ β (β€ β
β0)) β (π΅β-πΎ) β β) |
26 | 25 | recnd 11238 |
. . . . . . . 8
β’ ((π΅ β β β§ πΎ β (β€ β
β0)) β (π΅β-πΎ) β β) |
27 | 26 | 3adant3 1132 |
. . . . . . 7
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β (π΅β-πΎ) β β) |
28 | | nn0cn 12478 |
. . . . . . . 8
β’ (π β β0
β π β
β) |
29 | 28 | 3ad2ant3 1135 |
. . . . . . 7
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β π β
β) |
30 | | nncn 12216 |
. . . . . . . . 9
β’ (π΅ β β β π΅ β
β) |
31 | | nnne0 12242 |
. . . . . . . . 9
β’ (π΅ β β β π΅ β 0) |
32 | 30, 31 | jca 512 |
. . . . . . . 8
β’ (π΅ β β β (π΅ β β β§ π΅ β 0)) |
33 | 32 | 3ad2ant1 1133 |
. . . . . . 7
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β (π΅ β β β§ π΅ β 0)) |
34 | | div23 11887 |
. . . . . . 7
β’ (((π΅β-πΎ) β β β§ π β β β§ (π΅ β β β§ π΅ β 0)) β (((π΅β-πΎ) Β· π) / π΅) = (((π΅β-πΎ) / π΅) Β· π)) |
35 | 27, 29, 33, 34 | syl3anc 1371 |
. . . . . 6
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β (((π΅β-πΎ) Β· π) / π΅) = (((π΅β-πΎ) / π΅) Β· π)) |
36 | 30 | 3ad2ant1 1133 |
. . . . . . . . 9
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β π΅ β
β) |
37 | 31 | 3ad2ant1 1133 |
. . . . . . . . 9
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β π΅ β 0) |
38 | 12 | nnzd 12581 |
. . . . . . . . . 10
β’ (πΎ β (β€ β
β0) β -πΎ β β€) |
39 | 38 | 3ad2ant2 1134 |
. . . . . . . . 9
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β -πΎ β
β€) |
40 | 36, 37, 39 | expm1d 14117 |
. . . . . . . 8
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β (π΅β(-πΎ β 1)) = ((π΅β-πΎ) / π΅)) |
41 | 40 | eqcomd 2738 |
. . . . . . 7
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β ((π΅β-πΎ) / π΅) = (π΅β(-πΎ β 1))) |
42 | 41 | oveq1d 7420 |
. . . . . 6
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β (((π΅β-πΎ) / π΅) Β· π) = ((π΅β(-πΎ β 1)) Β· π)) |
43 | 35, 42 | eqtrd 2772 |
. . . . 5
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β (((π΅β-πΎ) Β· π) / π΅) = ((π΅β(-πΎ β 1)) Β· π)) |
44 | | nnm1nn0 12509 |
. . . . . . . . 9
β’ (-πΎ β β β (-πΎ β 1) β
β0) |
45 | 12, 44 | syl 17 |
. . . . . . . 8
β’ (πΎ β (β€ β
β0) β (-πΎ β 1) β
β0) |
46 | | zexpcl 14038 |
. . . . . . . 8
β’ ((π΅ β β€ β§ (-πΎ β 1) β
β0) β (π΅β(-πΎ β 1)) β
β€) |
47 | 9, 45, 46 | syl2an 596 |
. . . . . . 7
β’ ((π΅ β β β§ πΎ β (β€ β
β0)) β (π΅β(-πΎ β 1)) β
β€) |
48 | 47 | 3adant3 1132 |
. . . . . 6
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β (π΅β(-πΎ β 1)) β
β€) |
49 | 48, 18 | zmulcld 12668 |
. . . . 5
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β ((π΅β(-πΎ β 1)) Β· π) β β€) |
50 | 43, 49 | eqeltrd 2833 |
. . . 4
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β (((π΅β-πΎ) Β· π) / π΅) β β€) |
51 | 25 | 3adant3 1132 |
. . . . . 6
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β (π΅β-πΎ) β β) |
52 | 3 | 3ad2ant3 1135 |
. . . . . 6
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β π β
β) |
53 | 51, 52 | remulcld 11240 |
. . . . 5
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β ((π΅β-πΎ) Β· π) β β) |
54 | | nnrp 12981 |
. . . . . 6
β’ (π΅ β β β π΅ β
β+) |
55 | 54 | 3ad2ant1 1133 |
. . . . 5
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β π΅ β
β+) |
56 | | mod0 13837 |
. . . . 5
β’ ((((π΅β-πΎ) Β· π) β β β§ π΅ β β+) β
((((π΅β-πΎ) Β· π) mod π΅) = 0 β (((π΅β-πΎ) Β· π) / π΅) β β€)) |
57 | 53, 55, 56 | syl2anc 584 |
. . . 4
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β
((((π΅β-πΎ) Β· π) mod π΅) = 0 β (((π΅β-πΎ) Β· π) / π΅) β β€)) |
58 | 50, 57 | mpbird 256 |
. . 3
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β (((π΅β-πΎ) Β· π) mod π΅) = 0) |
59 | 22, 58 | eqtrd 2772 |
. 2
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β
((ββ((π΅β-πΎ) Β· π)) mod π΅) = 0) |
60 | 8, 59 | eqtrd 2772 |
1
β’ ((π΅ β β β§ πΎ β (β€ β
β0) β§ π β β0) β (πΎ(digitβπ΅)π) = 0) |