Metamath Proof Explorer

Theorem maxprmfct

Description: The set of prime factors of an integer greater than or equal to 2 satisfies the conditions to have a supremum, and that supremum is a member of the set. (Contributed by Paul Chapman, 17-Nov-2012)

Ref Expression
Hypothesis maxprmfct.1 ⊢ S = z ∈ ℙ | z ∥ N
Assertion maxprmfct ⊢ N ∈ ℤ ≥ 2 → S ⊆ ℤ ∧ S ≠ ∅ ∧ ∃ x ∈ ℤ ∀ y ∈ S y ≤ x ∧ sup S ℝ < ∈ S

Proof

Step Hyp Ref Expression
1 maxprmfct.1 ⊢ S = z ∈ ℙ | z ∥ N
2 1 ssrab3 ⊢ S ⊆ ℙ
3 prmz ⊢ y ∈ ℙ → y ∈ ℤ
4 3 ssriv ⊢ ℙ ⊆ ℤ
5 2 4 sstri ⊢ S ⊆ ℤ
6 5 a1i ⊢ N ∈ ℤ ≥ 2 → S ⊆ ℤ
7 exprmfct ⊢ N ∈ ℤ ≥ 2 → ∃ y ∈ ℙ y ∥ N
8 breq1 ⊢ z = y → z ∥ N ↔ y ∥ N
9 8 1 elrab2 ⊢ y ∈ S ↔ y ∈ ℙ ∧ y ∥ N
10 9 exbii ⊢ ∃ y y ∈ S ↔ ∃ y y ∈ ℙ ∧ y ∥ N
11 n0 ⊢ S ≠ ∅ ↔ ∃ y y ∈ S
12 df-rex ⊢ ∃ y ∈ ℙ y ∥ N ↔ ∃ y y ∈ ℙ ∧ y ∥ N
13 10 11 12 3bitr4ri ⊢ ∃ y ∈ ℙ y ∥ N ↔ S ≠ ∅
14 7 13 sylib ⊢ N ∈ ℤ ≥ 2 → S ≠ ∅
15 eluzelz ⊢ N ∈ ℤ ≥ 2 → N ∈ ℤ
16 eluz2nn ⊢ N ∈ ℤ ≥ 2 → N ∈ ℕ
17 3 anim1i ⊢ y ∈ ℙ ∧ y ∥ N → y ∈ ℤ ∧ y ∥ N
18 9 17 sylbi ⊢ y ∈ S → y ∈ ℤ ∧ y ∥ N
19 dvdsle ⊢ y ∈ ℤ ∧ N ∈ ℕ → y ∥ N → y ≤ N
20 19 expcom ⊢ N ∈ ℕ → y ∈ ℤ → y ∥ N → y ≤ N
21 20 impd ⊢ N ∈ ℕ → y ∈ ℤ ∧ y ∥ N → y ≤ N
22 18 21 syl5 ⊢ N ∈ ℕ → y ∈ S → y ≤ N
23 22 ralrimiv ⊢ N ∈ ℕ → ∀ y ∈ S y ≤ N
24 16 23 syl ⊢ N ∈ ℤ ≥ 2 → ∀ y ∈ S y ≤ N
25 brralrspcev ⊢ N ∈ ℤ ∧ ∀ y ∈ S y ≤ N → ∃ x ∈ ℤ ∀ y ∈ S y ≤ x
26 15 24 25 syl2anc ⊢ N ∈ ℤ ≥ 2 → ∃ x ∈ ℤ ∀ y ∈ S y ≤ x
27 6 14 26 3jca ⊢ N ∈ ℤ ≥ 2 → S ⊆ ℤ ∧ S ≠ ∅ ∧ ∃ x ∈ ℤ ∀ y ∈ S y ≤ x
28 suprzcl2 ⊢ S ⊆ ℤ ∧ S ≠ ∅ ∧ ∃ x ∈ ℤ ∀ y ∈ S y ≤ x → sup S ℝ < ∈ S
29 27 28 jccir ⊢ N ∈ ℤ ≥ 2 → S ⊆ ℤ ∧ S ≠ ∅ ∧ ∃ x ∈ ℤ ∀ y ∈ S y ≤ x ∧ sup S ℝ < ∈ S