Theorem dec5dvds2

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$$
	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\in {\mathbb{N}}_0$$
2		dec5dvds.2	$$⊢B\in \mathbb{N}$$
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\in {\mathbb{N}}_0$$
7	6	nn0zi	$$⊢5\in \mathbb{Z}$$
8	2	nnnn0i	$$⊢B\in {\mathbb{N}}_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\in {\mathbb{N}}_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\in ℂ$$
17	16	addid2i	$$⊢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 |-