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 {\mathbb{N}}_0$$
	dec5dvds.2	$$⊢B\in \mathbb{N}$$
	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 {\mathbb{N}}_0$$
2		dec5dvds.2	$$⊢B\in \mathbb{N}$$
3		dec5dvds.3	$$⊢B<5$$
4		5nn	$$⊢5\in \mathbb{N}$$
5		2nn0	$$⊢2\in {\mathbb{N}}_0$$
6	5 1	nn0mulcli	$$⊢2A\in {\mathbb{N}}_0$$
7		5cn	$$⊢5\in ℂ$$
8		2cn	$$⊢2\in ℂ$$
9	1	nn0cni	$$⊢A\in ℂ$$
10	7 8 9	mulassi	$$⊢5\cdot 2A=52A$$
11		5t2e10	$$⊢5\cdot 2=10$$
12	11	oveq1i	$$⊢5\cdot 2A=10A$$
13	10 12	eqtr3i	$$⊢52A=10A$$
14	13	oveq1i	$$⊢52A+B=10A+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 |-