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	$⊢ A \in ℕ$
	dec2nprm.2	$⊢ B \in ℕ_{0}$
	dec2nprm.3	$⊢ B \cdot 2 = C$
Assertion	dec2nprm	Could not format assertion : No typesetting found for \|- -. ; A C e. Prime with typecode \|-

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

Metamath Proof Explorer