dec5nprm

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

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

Step	Hyp	Ref	Expression
1		dec5nprm.1	$⊢ A \in ℕ$
2		2nn	$⊢ 2 \in ℕ$
3	2 1	nnmulcli	$⊢ 2 A \in ℕ$
4		peano2nn	$⊢ 2 A \in ℕ \to 2 A + 1 \in ℕ$
5	3 4	ax-mp	$⊢ 2 A + 1 \in ℕ$
6		5nn	$⊢ 5 \in ℕ$
7		1nn0	$⊢ 1 \in ℕ_{0}$
8		1lt2	$⊢ 1 < 2$
9	2 1 7 7 8	numlti	$⊢ 1 < 2 A + 1$
10		1lt5	$⊢ 1 < 5$
11	2	nncni	$⊢ 2 \in ℂ$
12	1	nncni	$⊢ A \in ℂ$
13		5cn	$⊢ 5 \in ℂ$
14	11 12 13	mul32i	$⊢ 2 A \cdot 5 = 2 \cdot 5 A$
15		5t2e10	$⊢ 5 \cdot 2 = 10$
16	13 11 15	mulcomli	$⊢ 2 \cdot 5 = 10$
17	16	oveq1i	$⊢ 2 \cdot 5 A = 10 A$
18	14 17	eqtri	$⊢ 2 A \cdot 5 = 10 A$
19	13	mullidi	$⊢ 1 \cdot 5 = 5$
20	18 19	oveq12i	$⊢ 2 A \cdot 5 + 1 \cdot 5 = 10 A + 5$
21	3	nncni	$⊢ 2 A \in ℂ$
22		ax-1cn	$⊢ 1 \in ℂ$
23	21 22 13	adddiri	$⊢ (2 A + 1) \cdot 5 = 2 A \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 \|-

Metamath Proof Explorer