Theorem dec5dvds2

Description: Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015)

	Ref	Expression
Hypotheses	dec5dvds.1	|- A e. NN0
	dec5dvds.2	|- B e. NN
	dec5dvds.3	|- B < 5
	dec5dvds2.4	|- ( 5 + B ) = C
Assertion	dec5dvds2	|- -. 5 || ; A C

Proof

Step	Hyp	Ref	Expression
1		dec5dvds.1	|- A e. NN0
2		dec5dvds.2	|- B e. NN
3		dec5dvds.3	|- B < 5
4		dec5dvds2.4	|- ( 5 + B ) = C
5	1 2 3	dec5dvds	|- -. 5 || ; A B
6		5nn0	|- 5 e. NN0
7	6	nn0zi	|- 5 e. ZZ
8	2	nnnn0i	|- B e. NN0
9	1 8	deccl	|- ; A B e. NN0
10	9	nn0zi	|- ; A B e. ZZ
11		dvdsadd	|- ( ( 5 e. ZZ /\ ; A B e. ZZ ) -> ( 5 || ; A B <-> 5 || ( 5 + ; A B ) ) )
12	7 10 11	mp2an	|- ( 5 || ; A B <-> 5 || ( 5 + ; A B ) )
13		0nn0	|- 0 e. NN0
14	6	dec0h	|- 5 = ; 0 5
15		eqid	|- ; A B = ; A B
16	1	nn0cni	|- A e. CC
17	16	addid2i	|- ( 0 + A ) = A
18	13 6 1 8 14 15 17 4	decadd	|- ( 5 + ; A B ) = ; A C
19	18	breq2i	|- ( 5 || ( 5 + ; A B ) <-> 5 || ; A C )
20	12 19	bitri	|- ( 5 || ; A B <-> 5 || ; A C )
21	5 20	mtbi	|- -. 5 || ; A C