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 ∈ ℙ

Proof

Step	Hyp	Ref	Expression
1		1nn0	⊢ 1 ∈ ℕ0
2		1nn	⊢ 1 ∈ ℕ
3	1 2	decnncl	⊢ ; 1 1 ∈ ℕ
4		1lt10	⊢ 1 < ; 1 0
5	2 1 1 4	declti	⊢ 1 < ; 1 1
6		0nn0	⊢ 0 ∈ ℕ0
7		2cn	⊢ 2 ∈ ℂ
8	7	mul02i	⊢ ( 0 · 2 ) = 0
9		1e0p1	⊢ 1 = ( 0 + 1 )
10	1 6 8 9	dec2dvds	⊢ ¬ 2 ∥ ; 1 1
11		3nn	⊢ 3 ∈ ℕ
12		3nn0	⊢ 3 ∈ ℕ0
13		2nn	⊢ 2 ∈ ℕ
14		3t3e9	⊢ ( 3 · 3 ) = 9
15	14	oveq1i	⊢ ( ( 3 · 3 ) + 2 ) = ( 9 + 2 )
16		9p2e11	⊢ ( 9 + 2 ) = ; 1 1
17	15 16	eqtri	⊢ ( ( 3 · 3 ) + 2 ) = ; 1 1
18		2lt3	⊢ 2 < 3
19	11 12 13 17 18	ndvdsi	⊢ ¬ 3 ∥ ; 1 1
20		2nn0	⊢ 2 ∈ ℕ0
21		5nn0	⊢ 5 ∈ ℕ0
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 ∈ ℙ