This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 3dvdsdec

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 ⊢ A ∈ ℕ 0
3dvdsdec.b ⊢ B ∈ ℕ 0
Assertion 3dvdsdec Could not format assertion : No typesetting found for |- ( 3 || ; A B <-> 3 || ( A + B ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 3dvdsdec.a ⊢ A ∈ ℕ 0
2 3dvdsdec.b ⊢ B ∈ ℕ 0
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 ⊢ 9 + 1 = 10
5 4 eqcomi ⊢ 10 = 9 + 1
6 5 oveq1i ⊢ 10 ⁢ A = 9 + 1 ⁢ A
7 9cn ⊢ 9 ∈ ℂ
8 ax-1cn ⊢ 1 ∈ ℂ
9 1 nn0cni ⊢ A ∈ ℂ
10 7 8 9 adddiri ⊢ 9 + 1 ⁢ A = 9 ⁢ A + 1 ⁢ A
11 9 mullidi ⊢ 1 ⁢ A = A
12 11 oveq2i ⊢ 9 ⁢ A + 1 ⁢ A = 9 ⁢ A + A
13 6 10 12 3eqtri ⊢ 10 ⁢ A = 9 ⁢ A + A
14 13 oveq1i ⊢ 10 ⁢ A + B = 9 ⁢ A + A + B
15 7 9 mulcli ⊢ 9 ⁢ A ∈ ℂ
16 2 nn0cni ⊢ B ∈ ℂ
17 15 9 16 addassi ⊢ 9 ⁢ A + A + B = 9 ⁢ A + A + B
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 ⊢ 3 ∈ ℤ
21 1 nn0zi ⊢ A ∈ ℤ
22 2 nn0zi ⊢ B ∈ ℤ
23 zaddcl ⊢ A ∈ ℤ ∧ B ∈ ℤ → A + B ∈ ℤ
24 21 22 23 mp2an ⊢ A + B ∈ ℤ
25 9nn ⊢ 9 ∈ ℕ
26 25 nnzi ⊢ 9 ∈ ℤ
27 zmulcl ⊢ 9 ∈ ℤ ∧ A ∈ ℤ → 9 ⁢ A ∈ ℤ
28 26 21 27 mp2an ⊢ 9 ⁢ A ∈ ℤ
29 zmulcl ⊢ 3 ∈ ℤ ∧ A ∈ ℤ → 3 ⁢ A ∈ ℤ
30 20 21 29 mp2an ⊢ 3 ⁢ A ∈ ℤ
31 dvdsmul1 ⊢ 3 ∈ ℤ ∧ 3 ⁢ A ∈ ℤ → 3 ∥ 3 ⁢ 3 ⁢ A
32 20 30 31 mp2an ⊢ 3 ∥ 3 ⁢ 3 ⁢ A
33 3t3e9 ⊢ 3 ⋅ 3 = 9
34 33 eqcomi ⊢ 9 = 3 ⋅ 3
35 34 oveq1i ⊢ 9 ⁢ A = 3 ⋅ 3 ⁢ A
36 3cn ⊢ 3 ∈ ℂ
37 36 36 9 mulassi ⊢ 3 ⋅ 3 ⁢ A = 3 ⁢ 3 ⁢ A
38 35 37 eqtri ⊢ 9 ⁢ A = 3 ⁢ 3 ⁢ A
39 32 38 breqtrri ⊢ 3 ∥ 9 ⁢ A
40 28 39 pm3.2i ⊢ 9 ⁢ A ∈ ℤ ∧ 3 ∥ 9 ⁢ A
41 dvdsadd2b ⊢ 3 ∈ ℤ ∧ A + B ∈ ℤ ∧ 9 ⁢ A ∈ ℤ ∧ 3 ∥ 9 ⁢ A → 3 ∥ A + B ↔ 3 ∥ 9 ⁢ A + A + B
42 20 24 40 41 mp3an ⊢ 3 ∥ A + B ↔ 3 ∥ 9 ⁢ A + A + B
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 |-