# Metamath Proof Explorer

## Theorem dec5dvds

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

Ref Expression
Hypotheses dec5dvds.1 ${⊢}{A}\in {ℕ}_{0}$
dec5dvds.2 ${⊢}{B}\in ℕ$
dec5dvds.3 ${⊢}{B}<5$
Assertion dec5dvds Could not format assertion : No typesetting found for |- -. 5 || ; A B with typecode |-

### Proof

Step Hyp Ref Expression
1 dec5dvds.1 ${⊢}{A}\in {ℕ}_{0}$
2 dec5dvds.2 ${⊢}{B}\in ℕ$
3 dec5dvds.3 ${⊢}{B}<5$
4 5nn ${⊢}5\in ℕ$
5 2nn0 ${⊢}2\in {ℕ}_{0}$
6 5 1 nn0mulcli ${⊢}2{A}\in {ℕ}_{0}$
7 5cn ${⊢}5\in ℂ$
8 2cn ${⊢}2\in ℂ$
9 1 nn0cni ${⊢}{A}\in ℂ$
10 7 8 9 mulassi ${⊢}5\cdot 2{A}=52{A}$
11 5t2e10 ${⊢}5\cdot 2=10$
12 11 oveq1i ${⊢}5\cdot 2{A}=10{A}$
13 10 12 eqtr3i ${⊢}52{A}=10{A}$
14 13 oveq1i ${⊢}52{A}+{B}=10{A}+{B}$
15 dfdec10 Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-
16 14 15 eqtr4i Could not format ( ( 5 x. ( 2 x. A ) ) + B ) = ; A B : No typesetting found for |- ( ( 5 x. ( 2 x. A ) ) + B ) = ; A B with typecode |-
17 4 6 2 16 3 ndvdsi Could not format -. 5 || ; A B : No typesetting found for |- -. 5 || ; A B with typecode |-