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

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 ⊢ A ∈ ℕ 0
dec5dvds.2 ⊢ B ∈ ℕ
dec5dvds.3 ⊢ B < 5
dec5dvds2.4 ⊢ 5 + B = C
Assertion dec5dvds2 Could not format assertion : No typesetting found for |- -. 5 || ; A C with typecode |-

Proof

Step Hyp Ref Expression
1 dec5dvds.1 ⊢ A ∈ ℕ 0
2 dec5dvds.2 ⊢ B ∈ ℕ
3 dec5dvds.3 ⊢ B < 5
4 dec5dvds2.4 ⊢ 5 + B = C
5 1 2 3 dec5dvds Could not format -. 5 || ; A B : No typesetting found for |- -. 5 || ; A B with typecode |-
6 5nn0 ⊢ 5 ∈ ℕ 0
7 6 nn0zi ⊢ 5 ∈ ℤ
8 2 nnnn0i ⊢ B ∈ ℕ 0
9 1 8 deccl Could not format ; A B e. NN0 : No typesetting found for |- ; A B e. NN0 with typecode |-
10 9 nn0zi Could not format ; A B e. ZZ : No typesetting found for |- ; A B e. ZZ with typecode |-
11 dvdsadd Could not format ( ( 5 e. ZZ /\ ; A B e. ZZ ) -> ( 5 || ; A B <-> 5 || ( 5 + ; A B ) ) ) : No typesetting found for |- ( ( 5 e. ZZ /\ ; A B e. ZZ ) -> ( 5 || ; A B <-> 5 || ( 5 + ; A B ) ) ) with typecode |-
12 7 10 11 mp2an Could not format ( 5 || ; A B <-> 5 || ( 5 + ; A B ) ) : No typesetting found for |- ( 5 || ; A B <-> 5 || ( 5 + ; A B ) ) with typecode |-
13 0nn0 ⊢ 0 ∈ ℕ 0
14 6 dec0h ⊢ 5 = 05
15 eqid Could not format ; A B = ; A B : No typesetting found for |- ; A B = ; A B with typecode |-
16 1 nn0cni ⊢ A ∈ ℂ
17 16 addlidi ⊢ 0 + A = A
18 13 6 1 8 14 15 17 4 decadd Could not format ( 5 + ; A B ) = ; A C : No typesetting found for |- ( 5 + ; A B ) = ; A C with typecode |-
19 18 breq2i Could not format ( 5 || ( 5 + ; A B ) <-> 5 || ; A C ) : No typesetting found for |- ( 5 || ( 5 + ; A B ) <-> 5 || ; A C ) with typecode |-
20 12 19 bitri Could not format ( 5 || ; A B <-> 5 || ; A C ) : No typesetting found for |- ( 5 || ; A B <-> 5 || ; A C ) with typecode |-
21 5 20 mtbi Could not format -. 5 || ; A C : No typesetting found for |- -. 5 || ; A C with typecode |-