Theorem prmlem1a

Description: Lemma for prmlem1 and prmlem2 . (Contributed by Mario Carneiro, 18-Feb-2014)

	Ref	Expression
Hypotheses	prmlem1.n	⊢ 𝑁 ∈ ℕ
	prmlem1.gt	⊢ 1 < 𝑁
	prmlem1.2	⊢ ¬ 2 ∥ 𝑁
	prmlem1.3	⊢ ¬ 3 ∥ 𝑁
	prmlem1a.x	⊢ ( ( ¬ 2 ∥ 5 ∧ 𝑥 ∈ ( ℤ≥ ‘ 5 ) ) → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) )
Assertion	prmlem1a	⊢ 𝑁 ∈ ℙ

Proof

Step	Hyp	Ref	Expression
1		prmlem1.n	⊢ 𝑁 ∈ ℕ
2		prmlem1.gt	⊢ 1 < 𝑁
3		prmlem1.2	⊢ ¬ 2 ∥ 𝑁
4		prmlem1.3	⊢ ¬ 3 ∥ 𝑁
5		prmlem1a.x	⊢ ( ( ¬ 2 ∥ 5 ∧ 𝑥 ∈ ( ℤ≥ ‘ 5 ) ) → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) )
6		eluz2b2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) )
7	1 2 6	mpbir2an	⊢ 𝑁 ∈ ( ℤ≥ ‘ 2 )
8		breq1	⊢ ( 𝑥 = 2 → ( 𝑥 ∥ 𝑁 ↔ 2 ∥ 𝑁 ) )
9	8	notbid	⊢ ( 𝑥 = 2 → ( ¬ 𝑥 ∥ 𝑁 ↔ ¬ 2 ∥ 𝑁 ) )
10	9	imbi2d	⊢ ( 𝑥 = 2 → ( ( ( 𝑥 ↑ 2 ) ≤ 𝑁 → ¬ 𝑥 ∥ 𝑁 ) ↔ ( ( 𝑥 ↑ 2 ) ≤ 𝑁 → ¬ 2 ∥ 𝑁 ) ) )
11		prmnn	⊢ ( 𝑥 ∈ ℙ → 𝑥 ∈ ℕ )
12	11	adantr	⊢ ( ( 𝑥 ∈ ℙ ∧ 𝑥 ≠ 2 ) → 𝑥 ∈ ℕ )
13		eldifsn	⊢ ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑥 ∈ ℙ ∧ 𝑥 ≠ 2 ) )
14		n2dvds1	⊢ ¬ 2 ∥ 1
15	4	a1i	⊢ ( 3 ∈ ℙ → ¬ 3 ∥ 𝑁 )
16		3p2e5	⊢ ( 3 + 2 ) = 5
17	5 15 16	prmlem0	⊢ ( ( ¬ 2 ∥ 3 ∧ 𝑥 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) )
18		1nprm	⊢ ¬ 1 ∈ ℙ
19	18	pm2.21i	⊢ ( 1 ∈ ℙ → ¬ 1 ∥ 𝑁 )
20		1p2e3	⊢ ( 1 + 2 ) = 3
21	17 19 20	prmlem0	⊢ ( ( ¬ 2 ∥ 1 ∧ 𝑥 ∈ ( ℤ≥ ‘ 1 ) ) → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) )
22	14 21	mpan	⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 1 ) → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) )
23		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
24	22 23	eleq2s	⊢ ( 𝑥 ∈ ℕ → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) )
25	24	expd	⊢ ( 𝑥 ∈ ℕ → ( 𝑥 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑥 ↑ 2 ) ≤ 𝑁 → ¬ 𝑥 ∥ 𝑁 ) ) )
26	13 25	biimtrrid	⊢ ( 𝑥 ∈ ℕ → ( ( 𝑥 ∈ ℙ ∧ 𝑥 ≠ 2 ) → ( ( 𝑥 ↑ 2 ) ≤ 𝑁 → ¬ 𝑥 ∥ 𝑁 ) ) )
27	12 26	mpcom	⊢ ( ( 𝑥 ∈ ℙ ∧ 𝑥 ≠ 2 ) → ( ( 𝑥 ↑ 2 ) ≤ 𝑁 → ¬ 𝑥 ∥ 𝑁 ) )
28	3	2a1i	⊢ ( 𝑥 ∈ ℙ → ( ( 𝑥 ↑ 2 ) ≤ 𝑁 → ¬ 2 ∥ 𝑁 ) )
29	10 27 28	pm2.61ne	⊢ ( 𝑥 ∈ ℙ → ( ( 𝑥 ↑ 2 ) ≤ 𝑁 → ¬ 𝑥 ∥ 𝑁 ) )
30	29	rgen	⊢ ∀ 𝑥 ∈ ℙ ( ( 𝑥 ↑ 2 ) ≤ 𝑁 → ¬ 𝑥 ∥ 𝑁 )
31		isprm5	⊢ ( 𝑁 ∈ ℙ ↔ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑥 ∈ ℙ ( ( 𝑥 ↑ 2 ) ≤ 𝑁 → ¬ 𝑥 ∥ 𝑁 ) ) )
32	7 30 31	mpbir2an	⊢ 𝑁 ∈ ℙ