Metamath Proof Explorer

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 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑁 )