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 ⊢ 𝐴 ∈ ℕ0
dec5dvds.2 ⊢ 𝐵 ∈ ℕ
dec5dvds.3 ⊢ 𝐵 < 5
Assertion dec5dvds ¬ 5 ∥ 𝐴 𝐵

Proof

Step Hyp Ref Expression
1 dec5dvds.1 ⊢ 𝐴 ∈ ℕ0
2 dec5dvds.2 ⊢ 𝐵 ∈ ℕ
3 dec5dvds.3 ⊢ 𝐵 < 5
4 5nn ⊢ 5 ∈ ℕ
5 2nn0 ⊢ 2 ∈ ℕ0
6 5 1 nn0mulcli ⊢ ( 2 · 𝐴 ) ∈ ℕ0
7 5cn ⊢ 5 ∈ ℂ
8 2cn ⊢ 2 ∈ ℂ
9 1 nn0cni ⊢ 𝐴 ∈ ℂ
10 7 8 9 mulassi ⊢ ( ( 5 · 2 ) · 𝐴 ) = ( 5 · ( 2 · 𝐴 ) )
11 5t2e10 ⊢ ( 5 · 2 ) = 1 0
12 11 oveq1i ⊢ ( ( 5 · 2 ) · 𝐴 ) = ( 1 0 · 𝐴 )
13 10 12 eqtr3i ⊢ ( 5 · ( 2 · 𝐴 ) ) = ( 1 0 · 𝐴 )
14 13 oveq1i ⊢ ( ( 5 · ( 2 · 𝐴 ) ) + 𝐵 ) = ( ( 1 0 · 𝐴 ) + 𝐵 )
15 dfdec10 ⊢ 𝐴 𝐵 = ( ( 1 0 · 𝐴 ) + 𝐵 )
16 14 15 eqtr4i ⊢ ( ( 5 · ( 2 · 𝐴 ) ) + 𝐵 ) = 𝐴 𝐵
17 4 6 2 16 3 ndvdsi ⊢ ¬ 5 ∥ 𝐴 𝐵