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	⊢ 𝑆 = { 𝑧 ∈ ℙ ∣ 𝑧 ∥ 𝑁 }
Assertion	maxprmfct	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑆 ⊆ ℤ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) ∧ sup ( 𝑆 , ℝ , < ) ∈ 𝑆 ) )

Proof

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