Metamath Proof Explorer

Theorem dec2dvds

Description: Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015)

Ref Expression
Hypotheses dec2dvds.1 ⊢ 𝐴 ∈ ℕ0
dec2dvds.2 ⊢ 𝐵 ∈ ℕ0
dec2dvds.3 ⊢ ( 𝐵 · 2 ) = 𝐶
dec2dvds.4 ⊢ 𝐷 = ( 𝐶 + 1 )
Assertion dec2dvds ¬ 2 ∥ 𝐴 𝐷

Proof

Step Hyp Ref Expression
1 dec2dvds.1 ⊢ 𝐴 ∈ ℕ0
2 dec2dvds.2 ⊢ 𝐵 ∈ ℕ0
3 dec2dvds.3 ⊢ ( 𝐵 · 2 ) = 𝐶
4 dec2dvds.4 ⊢ 𝐷 = ( 𝐶 + 1 )
5 5nn0 ⊢ 5 ∈ ℕ0
6 5 nn0zi ⊢ 5 ∈ ℤ
7 2z ⊢ 2 ∈ ℤ
8 dvdsmul2 ⊢ ( ( 5 ∈ ℤ ∧ 2 ∈ ℤ ) → 2 ∥ ( 5 · 2 ) )
9 6 7 8 mp2an ⊢ 2 ∥ ( 5 · 2 )
10 5t2e10 ⊢ ( 5 · 2 ) = 1 0
11 9 10 breqtri ⊢ 2 ∥ 1 0
12 10nn0 ⊢ 1 0 ∈ ℕ0
13 12 nn0zi ⊢ 1 0 ∈ ℤ
14 1 nn0zi ⊢ 𝐴 ∈ ℤ
15 dvdsmultr1 ⊢ ( ( 2 ∈ ℤ ∧ 1 0 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 2 ∥ 1 0 → 2 ∥ ( 1 0 · 𝐴 ) ) )
16 7 13 14 15 mp3an ⊢ ( 2 ∥ 1 0 → 2 ∥ ( 1 0 · 𝐴 ) )
17 11 16 ax-mp ⊢ 2 ∥ ( 1 0 · 𝐴 )
18 2 nn0zi ⊢ 𝐵 ∈ ℤ
19 dvdsmul2 ⊢ ( ( 𝐵 ∈ ℤ ∧ 2 ∈ ℤ ) → 2 ∥ ( 𝐵 · 2 ) )
20 18 7 19 mp2an ⊢ 2 ∥ ( 𝐵 · 2 )
21 20 3 breqtri ⊢ 2 ∥ 𝐶
22 12 1 nn0mulcli ⊢ ( 1 0 · 𝐴 ) ∈ ℕ0
23 22 nn0zi ⊢ ( 1 0 · 𝐴 ) ∈ ℤ
24 2nn0 ⊢ 2 ∈ ℕ0
25 2 24 nn0mulcli ⊢ ( 𝐵 · 2 ) ∈ ℕ0
26 3 25 eqeltrri ⊢ 𝐶 ∈ ℕ0
27 26 nn0zi ⊢ 𝐶 ∈ ℤ
28 dvds2add ⊢ ( ( 2 ∈ ℤ ∧ ( 1 0 · 𝐴 ) ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( 2 ∥ ( 1 0 · 𝐴 ) ∧ 2 ∥ 𝐶 ) → 2 ∥ ( ( 1 0 · 𝐴 ) + 𝐶 ) ) )
29 7 23 27 28 mp3an ⊢ ( ( 2 ∥ ( 1 0 · 𝐴 ) ∧ 2 ∥ 𝐶 ) → 2 ∥ ( ( 1 0 · 𝐴 ) + 𝐶 ) )
30 17 21 29 mp2an ⊢ 2 ∥ ( ( 1 0 · 𝐴 ) + 𝐶 )
31 dfdec10 ⊢ 𝐴 𝐶 = ( ( 1 0 · 𝐴 ) + 𝐶 )
32 30 31 breqtrri ⊢ 2 ∥ 𝐴 𝐶
33 1 26 deccl ⊢ 𝐴 𝐶 ∈ ℕ0
34 33 nn0zi ⊢ 𝐴 𝐶 ∈ ℤ
35 2nn ⊢ 2 ∈ ℕ
36 1lt2 ⊢ 1 < 2
37 ndvdsp1 ⊢ ( ( 𝐴 𝐶 ∈ ℤ ∧ 2 ∈ ℕ ∧ 1 < 2 ) → ( 2 ∥ 𝐴 𝐶 → ¬ 2 ∥ ( 𝐴 𝐶 + 1 ) ) )
38 34 35 36 37 mp3an ⊢ ( 2 ∥ 𝐴 𝐶 → ¬ 2 ∥ ( 𝐴 𝐶 + 1 ) )
39 32 38 ax-mp ⊢ ¬ 2 ∥ ( 𝐴 𝐶 + 1 )
40 4 eqcomi ⊢ ( 𝐶 + 1 ) = 𝐷
41 eqid ⊢ 𝐴 𝐶 = 𝐴 𝐶
42 1 26 40 41 decsuc ⊢ ( 𝐴 𝐶 + 1 ) = 𝐴 𝐷
43 42 breq2i ⊢ ( 2 ∥ ( 𝐴 𝐶 + 1 ) ↔ 2 ∥ 𝐴 𝐷 )
44 39 43 mtbi ⊢ ¬ 2 ∥ 𝐴 𝐷