Description: A decimal number is divisible by three iff the sum of its two "digits" is divisible by three. The term "digits" in its narrow sense is only correct if A and B actually are digits (i.e. nonnegative integers less than 10). However, this theorem holds for arbitrary nonnegative integers A and B , especially if A is itself a decimal number, e.g., A = ; C D . (Contributed by AV, 14-Jun-2021) (Revised by AV, 8-Sep-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 3dvdsdec.a | |
|
3dvdsdec.b | |
||
Assertion | 3dvdsdec | Could not format assertion : No typesetting found for |- ( 3 || ; A B <-> 3 || ( A + B ) ) with typecode |- |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3dvdsdec.a | |
|
2 | 3dvdsdec.b | |
|
3 | dfdec10 | Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |- | |
4 | 9p1e10 | |
|
5 | 4 | eqcomi | |
6 | 5 | oveq1i | |
7 | 9cn | |
|
8 | ax-1cn | |
|
9 | 1 | nn0cni | |
10 | 7 8 9 | adddiri | |
11 | 9 | mulid2i | |
12 | 11 | oveq2i | |
13 | 6 10 12 | 3eqtri | |
14 | 13 | oveq1i | |
15 | 7 9 | mulcli | |
16 | 2 | nn0cni | |
17 | 15 9 16 | addassi | |
18 | 3 14 17 | 3eqtri | Could not format ; A B = ( ( 9 x. A ) + ( A + B ) ) : No typesetting found for |- ; A B = ( ( 9 x. A ) + ( A + B ) ) with typecode |- |
19 | 18 | breq2i | Could not format ( 3 || ; A B <-> 3 || ( ( 9 x. A ) + ( A + B ) ) ) : No typesetting found for |- ( 3 || ; A B <-> 3 || ( ( 9 x. A ) + ( A + B ) ) ) with typecode |- |
20 | 3z | |
|
21 | 1 | nn0zi | |
22 | 2 | nn0zi | |
23 | zaddcl | |
|
24 | 21 22 23 | mp2an | |
25 | 9nn | |
|
26 | 25 | nnzi | |
27 | zmulcl | |
|
28 | 26 21 27 | mp2an | |
29 | zmulcl | |
|
30 | 20 21 29 | mp2an | |
31 | dvdsmul1 | |
|
32 | 20 30 31 | mp2an | |
33 | 3t3e9 | |
|
34 | 33 | eqcomi | |
35 | 34 | oveq1i | |
36 | 3cn | |
|
37 | 36 36 9 | mulassi | |
38 | 35 37 | eqtri | |
39 | 32 38 | breqtrri | |
40 | 28 39 | pm3.2i | |
41 | dvdsadd2b | |
|
42 | 20 24 40 41 | mp3an | |
43 | 19 42 | bitr4i | Could not format ( 3 || ; A B <-> 3 || ( A + B ) ) : No typesetting found for |- ( 3 || ; A B <-> 3 || ( A + B ) ) with typecode |- |