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	|- ; 1 1 e. Prime

Proof

Step	Hyp	Ref	Expression
1		1nn0	|- 1 e. NN0
2		1nn	|- 1 e. NN
3	1 2	decnncl	|- ; 1 1 e. NN
4		1lt10	|- 1 < ; 1 0
5	2 1 1 4	declti	|- 1 < ; 1 1
6		0nn0	|- 0 e. NN0
7		2cn	|- 2 e. CC
8	7	mul02i	|- ( 0 x. 2 ) = 0
9		1e0p1	|- 1 = ( 0 + 1 )
10	1 6 8 9	dec2dvds	|- -. 2 || ; 1 1
11		3nn	|- 3 e. NN
12		3nn0	|- 3 e. NN0
13		2nn	|- 2 e. NN
14		3t3e9	|- ( 3 x. 3 ) = 9
15	14	oveq1i	|- ( ( 3 x. 3 ) + 2 ) = ( 9 + 2 )
16		9p2e11	|- ( 9 + 2 ) = ; 1 1
17	15 16	eqtri	|- ( ( 3 x. 3 ) + 2 ) = ; 1 1
18		2lt3	|- 2 < 3
19	11 12 13 17 18	ndvdsi	|- -. 3 || ; 1 1
20		2nn0	|- 2 e. NN0
21		5nn0	|- 5 e. NN0
22		1lt2	|- 1 < 2
23	1 20 1 21 4 22	decltc	|- ; 1 1 < ; 2 5
24	3 5 10 19 23	prmlem1	|- ; 1 1 e. Prime