Theorem dec5nprm

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

	Ref	Expression
Hypothesis	dec5nprm.1	$$⊢A\in \mathbb{N}$$
Assertion	dec5nprm	Could not format assertion : No typesetting found for |- -. ; A 5 e. Prime with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dec5nprm.1	$$⊢A\in \mathbb{N}$$
2		2nn	$$⊢2\in \mathbb{N}$$
3	2 1	nnmulcli	$$⊢2A\in \mathbb{N}$$
4		peano2nn	$$⊢2A\in \mathbb{N}\to 2A+1\in \mathbb{N}$$
5	3 4	ax-mp	$$⊢2A+1\in \mathbb{N}$$
6		5nn	$$⊢5\in \mathbb{N}$$
7		1nn0	$$⊢1\in {\mathbb{N}}_0$$
8		1lt2	$$⊢1<2$$
9	2 1 7 7 8	numlti	$$⊢1<2A+1$$
10		1lt5	$$⊢1<5$$
11	2	nncni	$$⊢2\in ℂ$$
12	1	nncni	$$⊢A\in ℂ$$
13		5cn	$$⊢5\in ℂ$$
14	11 12 13	mul32i	$$⊢2A\cdot 5=2\cdot 5A$$
15		5t2e10	$$⊢5\cdot 2=10$$
16	13 11 15	mulcomli	$$⊢2\cdot 5=10$$
17	16	oveq1i	$$⊢2\cdot 5A=10A$$
18	14 17	eqtri	$$⊢2A\cdot 5=10A$$
19	13	mulid2i	$$⊢1\cdot 5=5$$
20	18 19	oveq12i	$$⊢2A\cdot 5+1\cdot 5=10A+5$$
21	3	nncni	$$⊢2A\in ℂ$$
22		ax-1cn	$$⊢1\in ℂ$$
23	21 22 13	adddiri	$$⊢\left(2A+1\right)\cdot 5=2A\cdot 5+1\cdot 5$$
24		dfdec10	Could not format ; A 5 = ( ( ; 1 0 x. A ) + 5 ) : No typesetting found for |- ; A 5 = ( ( ; 1 0 x. A ) + 5 ) with typecode |-
25	20 23 24	3eqtr4i	Could not format ( ( ( 2 x. A ) + 1 ) x. 5 ) = ; A 5 : No typesetting found for |- ( ( ( 2 x. A ) + 1 ) x. 5 ) = ; A 5 with typecode |-
26	5 6 9 10 25	nprmi	Could not format -. ; A 5 e. Prime : No typesetting found for |- -. ; A 5 e. Prime with typecode |-