Theorem exprmfct

Description: Every integer greater than or equal to 2 has a prime factor. (Contributed by Paul Chapman, 26-Oct-2012) (Proof shortened by Mario Carneiro, 20-Jun-2015)

	Ref	Expression
Assertion	exprmfct	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		eluz2nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ )
2		eleq1	⊢ ( 𝑥 = 1 → ( 𝑥 ∈ ( ℤ≥ ‘ 2 ) ↔ 1 ∈ ( ℤ≥ ‘ 2 ) ) )
3	2	imbi1d	⊢ ( 𝑥 = 1 → ( ( 𝑥 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑥 ) ↔ ( 1 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑥 ) ) )
4		eleq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ( ℤ≥ ‘ 2 ) ↔ 𝑦 ∈ ( ℤ≥ ‘ 2 ) ) )
5		breq2	⊢ ( 𝑥 = 𝑦 → ( 𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝑦 ) )
6	5	rexbidv	⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑥 ↔ ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑦 ) )
7	4 6	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑥 ) ↔ ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑦 ) ) )
8		eleq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ ( ℤ≥ ‘ 2 ) ↔ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) )
9		breq2	⊢ ( 𝑥 = 𝑧 → ( 𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝑧 ) )
10	9	rexbidv	⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑥 ↔ ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑧 ) )
11	8 10	imbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑥 ) ↔ ( 𝑧 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑧 ) ) )
12		eleq1	⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → ( 𝑥 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑦 · 𝑧 ) ∈ ( ℤ≥ ‘ 2 ) ) )
13		breq2	⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → ( 𝑝 ∥ 𝑥 ↔ 𝑝 ∥ ( 𝑦 · 𝑧 ) ) )
14	13	rexbidv	⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → ( ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑥 ↔ ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( 𝑦 · 𝑧 ) ) )
15	12 14	imbi12d	⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → ( ( 𝑥 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑥 ) ↔ ( ( 𝑦 · 𝑧 ) ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( 𝑦 · 𝑧 ) ) ) )
16		eleq1	⊢ ( 𝑥 = 𝑁 → ( 𝑥 ∈ ( ℤ≥ ‘ 2 ) ↔ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) )
17		breq2	⊢ ( 𝑥 = 𝑁 → ( 𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝑁 ) )
18	17	rexbidv	⊢ ( 𝑥 = 𝑁 → ( ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑥 ↔ ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑁 ) )
19	16 18	imbi12d	⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑥 ) ↔ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑁 ) ) )
20		1m1e0	⊢ ( 1 − 1 ) = 0
21		uz2m1nn	⊢ ( 1 ∈ ( ℤ≥ ‘ 2 ) → ( 1 − 1 ) ∈ ℕ )
22	20 21	eqeltrrid	⊢ ( 1 ∈ ( ℤ≥ ‘ 2 ) → 0 ∈ ℕ )
23		0nnn	⊢ ¬ 0 ∈ ℕ
24	23	pm2.21i	⊢ ( 0 ∈ ℕ → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑥 )
25	22 24	syl	⊢ ( 1 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑥 )
26		prmz	⊢ ( 𝑥 ∈ ℙ → 𝑥 ∈ ℤ )
27		iddvds	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∥ 𝑥 )
28	26 27	syl	⊢ ( 𝑥 ∈ ℙ → 𝑥 ∥ 𝑥 )
29		breq1	⊢ ( 𝑝 = 𝑥 → ( 𝑝 ∥ 𝑥 ↔ 𝑥 ∥ 𝑥 ) )
30	29	rspcev	⊢ ( ( 𝑥 ∈ ℙ ∧ 𝑥 ∥ 𝑥 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑥 )
31	28 30	mpdan	⊢ ( 𝑥 ∈ ℙ → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑥 )
32	31	a1d	⊢ ( 𝑥 ∈ ℙ → ( 𝑥 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑥 ) )
33		simpl	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑦 ∈ ( ℤ≥ ‘ 2 ) )
34		eluzelz	⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) → 𝑦 ∈ ℤ )
35	34	ad2antrr	⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑦 ∈ ℤ )
36		eluzelz	⊢ ( 𝑧 ∈ ( ℤ≥ ‘ 2 ) → 𝑧 ∈ ℤ )
37	36	ad2antlr	⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑧 ∈ ℤ )
38		dvdsmul1	⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → 𝑦 ∥ ( 𝑦 · 𝑧 ) )
39	35 37 38	syl2anc	⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑦 ∥ ( 𝑦 · 𝑧 ) )
40		prmz	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
41	40	adantl	⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℤ )
42	35 37	zmulcld	⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑦 · 𝑧 ) ∈ ℤ )
43		dvdstr	⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ ( 𝑦 · 𝑧 ) ∈ ℤ ) → ( ( 𝑝 ∥ 𝑦 ∧ 𝑦 ∥ ( 𝑦 · 𝑧 ) ) → 𝑝 ∥ ( 𝑦 · 𝑧 ) ) )
44	41 35 42 43	syl3anc	⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ 𝑦 ∧ 𝑦 ∥ ( 𝑦 · 𝑧 ) ) → 𝑝 ∥ ( 𝑦 · 𝑧 ) ) )
45	39 44	mpan2d	⊢ ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ 𝑦 → 𝑝 ∥ ( 𝑦 · 𝑧 ) ) )
46	45	reximdva	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑦 → ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( 𝑦 · 𝑧 ) ) )
47	33 46	embantd	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑦 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( 𝑦 · 𝑧 ) ) )
48	47	a1dd	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑦 ) → ( ( 𝑦 · 𝑧 ) ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( 𝑦 · 𝑧 ) ) ) )
49	48	adantrd	⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( 𝑦 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑦 ) ∧ ( 𝑧 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑧 ) ) → ( ( 𝑦 · 𝑧 ) ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ ( 𝑦 · 𝑧 ) ) ) )
50	3 7 11 15 19 25 32 49	prmind	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑁 ) )
51	1 50	mpcom	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑁 )