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 ⊢ 𝐴 ∈ ℕ0
3dvdsdec.b ⊢ 𝐵 ∈ ℕ0
Assertion 3dvdsdec ( 3 ∥ 𝐴 𝐵 ↔ 3 ∥ ( 𝐴 + 𝐵 ) )

Proof

Step Hyp Ref Expression
1 3dvdsdec.a ⊢ 𝐴 ∈ ℕ0
2 3dvdsdec.b ⊢ 𝐵 ∈ ℕ0
3 dfdec10 ⊢ 𝐴 𝐵 = ( ( 1 0 · 𝐴 ) + 𝐵 )
4 9p1e10 ⊢ ( 9 + 1 ) = 1 0
5 4 eqcomi ⊢ 1 0 = ( 9 + 1 )
6 5 oveq1i ⊢ ( 1 0 · 𝐴 ) = ( ( 9 + 1 ) · 𝐴 )
7 9cn ⊢ 9 ∈ ℂ
8 ax-1cn ⊢ 1 ∈ ℂ
9 1 nn0cni ⊢ 𝐴 ∈ ℂ
10 7 8 9 adddiri ⊢ ( ( 9 + 1 ) · 𝐴 ) = ( ( 9 · 𝐴 ) + ( 1 · 𝐴 ) )
11 9 mullidi ⊢ ( 1 · 𝐴 ) = 𝐴
12 11 oveq2i ⊢ ( ( 9 · 𝐴 ) + ( 1 · 𝐴 ) ) = ( ( 9 · 𝐴 ) + 𝐴 )
13 6 10 12 3eqtri ⊢ ( 1 0 · 𝐴 ) = ( ( 9 · 𝐴 ) + 𝐴 )
14 13 oveq1i ⊢ ( ( 1 0 · 𝐴 ) + 𝐵 ) = ( ( ( 9 · 𝐴 ) + 𝐴 ) + 𝐵 )
15 7 9 mulcli ⊢ ( 9 · 𝐴 ) ∈ ℂ
16 2 nn0cni ⊢ 𝐵 ∈ ℂ
17 15 9 16 addassi ⊢ ( ( ( 9 · 𝐴 ) + 𝐴 ) + 𝐵 ) = ( ( 9 · 𝐴 ) + ( 𝐴 + 𝐵 ) )
18 3 14 17 3eqtri ⊢ 𝐴 𝐵 = ( ( 9 · 𝐴 ) + ( 𝐴 + 𝐵 ) )
19 18 breq2i ⊢ ( 3 ∥ 𝐴 𝐵 ↔ 3 ∥ ( ( 9 · 𝐴 ) + ( 𝐴 + 𝐵 ) ) )
20 3z ⊢ 3 ∈ ℤ
21 1 nn0zi ⊢ 𝐴 ∈ ℤ
22 2 nn0zi ⊢ 𝐵 ∈ ℤ
23 zaddcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + 𝐵 ) ∈ ℤ )
24 21 22 23 mp2an ⊢ ( 𝐴 + 𝐵 ) ∈ ℤ
25 9nn ⊢ 9 ∈ ℕ
26 25 nnzi ⊢ 9 ∈ ℤ
27 zmulcl ⊢ ( ( 9 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 9 · 𝐴 ) ∈ ℤ )
28 26 21 27 mp2an ⊢ ( 9 · 𝐴 ) ∈ ℤ
29 zmulcl ⊢ ( ( 3 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 3 · 𝐴 ) ∈ ℤ )
30 20 21 29 mp2an ⊢ ( 3 · 𝐴 ) ∈ ℤ
31 dvdsmul1 ⊢ ( ( 3 ∈ ℤ ∧ ( 3 · 𝐴 ) ∈ ℤ ) → 3 ∥ ( 3 · ( 3 · 𝐴 ) ) )
32 20 30 31 mp2an ⊢ 3 ∥ ( 3 · ( 3 · 𝐴 ) )
33 3t3e9 ⊢ ( 3 · 3 ) = 9
34 33 eqcomi ⊢ 9 = ( 3 · 3 )
35 34 oveq1i ⊢ ( 9 · 𝐴 ) = ( ( 3 · 3 ) · 𝐴 )
36 3cn ⊢ 3 ∈ ℂ
37 36 36 9 mulassi ⊢ ( ( 3 · 3 ) · 𝐴 ) = ( 3 · ( 3 · 𝐴 ) )
38 35 37 eqtri ⊢ ( 9 · 𝐴 ) = ( 3 · ( 3 · 𝐴 ) )
39 32 38 breqtrri ⊢ 3 ∥ ( 9 · 𝐴 )
40 28 39 pm3.2i ⊢ ( ( 9 · 𝐴 ) ∈ ℤ ∧ 3 ∥ ( 9 · 𝐴 ) )
41 dvdsadd2b ⊢ ( ( 3 ∈ ℤ ∧ ( 𝐴 + 𝐵 ) ∈ ℤ ∧ ( ( 9 · 𝐴 ) ∈ ℤ ∧ 3 ∥ ( 9 · 𝐴 ) ) ) → ( 3 ∥ ( 𝐴 + 𝐵 ) ↔ 3 ∥ ( ( 9 · 𝐴 ) + ( 𝐴 + 𝐵 ) ) ) )
42 20 24 40 41 mp3an ⊢ ( 3 ∥ ( 𝐴 + 𝐵 ) ↔ 3 ∥ ( ( 9 · 𝐴 ) + ( 𝐴 + 𝐵 ) ) )
43 19 42 bitr4i ⊢ ( 3 ∥ 𝐴 𝐵 ↔ 3 ∥ ( 𝐴 + 𝐵 ) )