This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ ℕ 0
dec5dvds.2 ⊢ B ∈ ℕ
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 ∈ ℕ 0
2 dec5dvds.2 ⊢ B ∈ ℕ
3 dec5dvds.3 ⊢ B < 5
4 5nn ⊢ 5 ∈ ℕ
5 2nn0 ⊢ 2 ∈ ℕ 0
6 5 1 nn0mulcli ⊢ 2 ⁢ A ∈ ℕ 0
7 5cn ⊢ 5 ∈ ℂ
8 2cn ⊢ 2 ∈ ℂ
9 1 nn0cni ⊢ A ∈ ℂ
10 7 8 9 mulassi ⊢ 5 ⋅ 2 ⁢ A = 5 ⁢ 2 ⁢ A
11 5t2e10 ⊢ 5 ⋅ 2 = 10
12 11 oveq1i ⊢ 5 ⋅ 2 ⁢ A = 10 ⁢ A
13 10 12 eqtr3i ⊢ 5 ⁢ 2 ⁢ A = 10 ⁢ A
14 13 oveq1i ⊢ 5 ⁢ 2 ⁢ 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 |-