Theorem dec5nprm

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

	Ref	Expression
Hypothesis	dec5nprm.1	|- A e. NN
Assertion	dec5nprm	|- -. ; A 5 e. Prime

Proof

Step	Hyp	Ref	Expression
1		dec5nprm.1	|- A e. NN
2		2nn	|- 2 e. NN
3	2 1	nnmulcli	|- ( 2 x. A ) e. NN
4		peano2nn	|- ( ( 2 x. A ) e. NN -> ( ( 2 x. A ) + 1 ) e. NN )
5	3 4	ax-mp	|- ( ( 2 x. A ) + 1 ) e. NN
6		5nn	|- 5 e. NN
7		1nn0	|- 1 e. NN0
8		1lt2	|- 1 < 2
9	2 1 7 7 8	numlti	|- 1 < ( ( 2 x. A ) + 1 )
10		1lt5	|- 1 < 5
11	2	nncni	|- 2 e. CC
12	1	nncni	|- A e. CC
13		5cn	|- 5 e. CC
14	11 12 13	mul32i	|- ( ( 2 x. A ) x. 5 ) = ( ( 2 x. 5 ) x. A )
15		5t2e10	|- ( 5 x. 2 ) = ; 1 0
16	13 11 15	mulcomli	|- ( 2 x. 5 ) = ; 1 0
17	16	oveq1i	|- ( ( 2 x. 5 ) x. A ) = ( ; 1 0 x. A )
18	14 17	eqtri	|- ( ( 2 x. A ) x. 5 ) = ( ; 1 0 x. A )
19	13	mulid2i	|- ( 1 x. 5 ) = 5
20	18 19	oveq12i	|- ( ( ( 2 x. A ) x. 5 ) + ( 1 x. 5 ) ) = ( ( ; 1 0 x. A ) + 5 )
21	3	nncni	|- ( 2 x. A ) e. CC
22		ax-1cn	|- 1 e. CC
23	21 22 13	adddiri	|- ( ( ( 2 x. A ) + 1 ) x. 5 ) = ( ( ( 2 x. A ) x. 5 ) + ( 1 x. 5 ) )
24		dfdec10	|- ; A 5 = ( ( ; 1 0 x. A ) + 5 )
25	20 23 24	3eqtr4i	|- ( ( ( 2 x. A ) + 1 ) x. 5 ) = ; A 5
26	5 6 9 10 25	nprmi	|- -. ; A 5 e. Prime