Theorem dec5dvds

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
Assertion	dec5dvds	|- -. 5 || ; A B

Proof

Step	Hyp	Ref	Expression
1		dec5dvds.1	|- A e. NN0
2		dec5dvds.2	|- B e. NN
3		dec5dvds.3	|- B < 5
4		5nn	|- 5 e. NN
5		2nn0	|- 2 e. NN0
6	5 1	nn0mulcli	|- ( 2 x. A ) e. NN0
7		5cn	|- 5 e. CC
8		2cn	|- 2 e. CC
9	1	nn0cni	|- A e. CC
10	7 8 9	mulassi	|- ( ( 5 x. 2 ) x. A ) = ( 5 x. ( 2 x. A ) )
11		5t2e10	|- ( 5 x. 2 ) = ; 1 0
12	11	oveq1i	|- ( ( 5 x. 2 ) x. A ) = ( ; 1 0 x. A )
13	10 12	eqtr3i	|- ( 5 x. ( 2 x. A ) ) = ( ; 1 0 x. A )
14	13	oveq1i	|- ( ( 5 x. ( 2 x. A ) ) + B ) = ( ( ; 1 0 x. A ) + B )
15		dfdec10	|- ; A B = ( ( ; 1 0 x. A ) + B )
16	14 15	eqtr4i	|- ( ( 5 x. ( 2 x. A ) ) + B ) = ; A B
17	4 6 2 16 3	ndvdsi	|- -. 5 || ; A B