Theorem 11prm

Description: 11 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by Mario Carneiro, 20-Apr-2015)

	Ref	Expression
Assertion	11prm	$$⊢11\in \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		1nn0	$$⊢1\in {\mathbb{N}}_0$$
2		1nn	$$⊢1\in \mathbb{N}$$
3	1 2	decnncl	$$⊢11\in \mathbb{N}$$
4		1lt10	$$⊢1<10$$
5	2 1 1 4	declti	$$⊢1<11$$
6		0nn0	$$⊢0\in {\mathbb{N}}_0$$
7		2cn	$$⊢2\in ℂ$$
8	7	mul02i	$$⊢0\cdot 2=0$$
9		1e0p1	$$⊢1=0+1$$
10	1 6 8 9	dec2dvds	$$⊢\neg 2\parallel 11$$
11		3nn	$$⊢3\in \mathbb{N}$$
12		3nn0	$$⊢3\in {\mathbb{N}}_0$$
13		2nn	$$⊢2\in \mathbb{N}$$
14		3t3e9	$$⊢3\cdot 3=9$$
15	14	oveq1i	$$⊢3\cdot 3+2=9+2$$
16		9p2e11	$$⊢9+2=11$$
17	15 16	eqtri	$$⊢3\cdot 3+2=11$$
18		2lt3	$$⊢2<3$$
19	11 12 13 17 18	ndvdsi	$$⊢\neg 3\parallel 11$$
20		2nn0	$$⊢2\in {\mathbb{N}}_0$$
21		5nn0	$$⊢5\in {\mathbb{N}}_0$$
22		1lt2	$$⊢1<2$$
23	1 20 1 21 4 22	decltc	$$⊢11<25$$
24	3 5 10 19 23	prmlem1	$$⊢11\in \mathbb{P}$$