Metamath Proof Explorer

Theorem dec5dvds2

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

Ref Expression
Hypotheses dec5dvds.1 ⊢ 𝐴 ∈ ℕ0
dec5dvds.2 ⊢ 𝐵 ∈ ℕ
dec5dvds.3 ⊢ 𝐵 < 5
dec5dvds2.4 ⊢ ( 5 + 𝐵 ) = 𝐶
Assertion dec5dvds2 ¬ 5 ∥ 𝐴 𝐶

Proof

Step Hyp Ref Expression
1 dec5dvds.1 ⊢ 𝐴 ∈ ℕ0
2 dec5dvds.2 ⊢ 𝐵 ∈ ℕ
3 dec5dvds.3 ⊢ 𝐵 < 5
4 dec5dvds2.4 ⊢ ( 5 + 𝐵 ) = 𝐶
5 1 2 3 dec5dvds ⊢ ¬ 5 ∥ 𝐴 𝐵
6 5nn0 ⊢ 5 ∈ ℕ0
7 6 nn0zi ⊢ 5 ∈ ℤ
8 2 nnnn0i ⊢ 𝐵 ∈ ℕ0
9 1 8 deccl ⊢ 𝐴 𝐵 ∈ ℕ0
10 9 nn0zi ⊢ 𝐴 𝐵 ∈ ℤ
11 dvdsadd ⊢ ( ( 5 ∈ ℤ ∧ 𝐴 𝐵 ∈ ℤ ) → ( 5 ∥ 𝐴 𝐵 ↔ 5 ∥ ( 5 + 𝐴 𝐵 ) ) )
12 7 10 11 mp2an ⊢ ( 5 ∥ 𝐴 𝐵 ↔ 5 ∥ ( 5 + 𝐴 𝐵 ) )
13 0nn0 ⊢ 0 ∈ ℕ0
14 6 dec0h ⊢ 5 = 0 5
15 eqid ⊢ 𝐴 𝐵 = 𝐴 𝐵
16 1 nn0cni ⊢ 𝐴 ∈ ℂ
17 16 addlidi ⊢ ( 0 + 𝐴 ) = 𝐴
18 13 6 1 8 14 15 17 4 decadd ⊢ ( 5 + 𝐴 𝐵 ) = 𝐴 𝐶
19 18 breq2i ⊢ ( 5 ∥ ( 5 + 𝐴 𝐵 ) ↔ 5 ∥ 𝐴 𝐶 )
20 12 19 bitri ⊢ ( 5 ∥ 𝐴 𝐵 ↔ 5 ∥ 𝐴 𝐶 )
21 5 20 mtbi ⊢ ¬ 5 ∥ 𝐴 𝐶