Theorem dec2nprm

Description: A decimal number greater than 10 and ending with an even digit is not a prime number. (Contributed by Mario Carneiro, 19-Apr-2015)

	Ref	Expression
Hypotheses	dec5nprm.1	⊢ 𝐴 ∈ ℕ
	dec2nprm.2	⊢ 𝐵 ∈ ℕ0
	dec2nprm.3	⊢ ( 𝐵 · 2 ) = 𝐶
Assertion	dec2nprm	⊢ ¬ ; 𝐴 𝐶 ∈ ℙ

Proof

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