Theorem dec5nprm

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

	Ref	Expression
Hypothesis	dec5nprm.1	⊢ 𝐴 ∈ ℕ
Assertion	dec5nprm	⊢ ¬ ; 𝐴 5 ∈ ℙ

Proof

Step	Hyp	Ref	Expression
1		dec5nprm.1	⊢ 𝐴 ∈ ℕ
2		2nn	⊢ 2 ∈ ℕ
3	2 1	nnmulcli	⊢ ( 2 · 𝐴 ) ∈ ℕ
4		peano2nn	⊢ ( ( 2 · 𝐴 ) ∈ ℕ → ( ( 2 · 𝐴 ) + 1 ) ∈ ℕ )
5	3 4	ax-mp	⊢ ( ( 2 · 𝐴 ) + 1 ) ∈ ℕ
6		5nn	⊢ 5 ∈ ℕ
7		1nn0	⊢ 1 ∈ ℕ0
8		1lt2	⊢ 1 < 2
9	2 1 7 7 8	numlti	⊢ 1 < ( ( 2 · 𝐴 ) + 1 )
10		1lt5	⊢ 1 < 5
11	2	nncni	⊢ 2 ∈ ℂ
12	1	nncni	⊢ 𝐴 ∈ ℂ
13		5cn	⊢ 5 ∈ ℂ
14	11 12 13	mul32i	⊢ ( ( 2 · 𝐴 ) · 5 ) = ( ( 2 · 5 ) · 𝐴 )
15		5t2e10	⊢ ( 5 · 2 ) = ; 1 0
16	13 11 15	mulcomli	⊢ ( 2 · 5 ) = ; 1 0
17	16	oveq1i	⊢ ( ( 2 · 5 ) · 𝐴 ) = ( ; 1 0 · 𝐴 )
18	14 17	eqtri	⊢ ( ( 2 · 𝐴 ) · 5 ) = ( ; 1 0 · 𝐴 )
19	13	mulid2i	⊢ ( 1 · 5 ) = 5
20	18 19	oveq12i	⊢ ( ( ( 2 · 𝐴 ) · 5 ) + ( 1 · 5 ) ) = ( ( ; 1 0 · 𝐴 ) + 5 )
21	3	nncni	⊢ ( 2 · 𝐴 ) ∈ ℂ
22		ax-1cn	⊢ 1 ∈ ℂ
23	21 22 13	adddiri	⊢ ( ( ( 2 · 𝐴 ) + 1 ) · 5 ) = ( ( ( 2 · 𝐴 ) · 5 ) + ( 1 · 5 ) )
24		dfdec10	⊢ ; 𝐴 5 = ( ( ; 1 0 · 𝐴 ) + 5 )
25	20 23 24	3eqtr4i	⊢ ( ( ( 2 · 𝐴 ) + 1 ) · 5 ) = ; 𝐴 5
26	5 6 9 10 25	nprmi	⊢ ¬ ; 𝐴 5 ∈ ℙ