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=\left\{z\in \mathbb{P}|z\parallel N\right\}$$
Assertion	maxprmfct	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(\left(S\subseteq \mathbb{Z}\wedge S\ne \varnothing \wedge \exists x\in \mathbb{Z}\forall y\in Sy\le x\right)\wedge sup\left(S,ℝ,<\right)\in S\right)$$

Proof

Step	Hyp	Ref	Expression
1		maxprmfct.1	$$⊢S=\left\{z\in \mathbb{P}|z\parallel N\right\}$$
2	1	ssrab3	$$⊢S\subseteq \mathbb{P}$$
3		prmz	$$⊢y\in \mathbb{P}\to y\in \mathbb{Z}$$
4	3	ssriv	$$⊢\mathbb{P}\subseteq \mathbb{Z}$$
5	2 4	sstri	$$⊢S\subseteq \mathbb{Z}$$
6	5	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to S\subseteq \mathbb{Z}$$
7		exprmfct	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \exists y\in \mathbb{P}y\parallel N$$
8		breq1	$$⊢z=y\to \left(z\parallel N\leftrightarrow y\parallel N\right)$$
9	8 1	elrab2	$$⊢y\in S\leftrightarrow \left(y\in \mathbb{P}\wedge y\parallel N\right)$$
10	9	exbii	$$⊢\exists yy\in S\leftrightarrow \exists y\left(y\in \mathbb{P}\wedge y\parallel N\right)$$
11		n0	$$⊢S\ne \varnothing \leftrightarrow \exists yy\in S$$
12		df-rex	$$⊢\exists y\in \mathbb{P}y\parallel N\leftrightarrow \exists y\left(y\in \mathbb{P}\wedge y\parallel N\right)$$
13	10 11 12	3bitr4ri	$$⊢\exists y\in \mathbb{P}y\parallel N\leftrightarrow S\ne \varnothing$$
14	7 13	sylib	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to S\ne \varnothing$$
15		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in \mathbb{Z}$$
16		eluz2nn	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in \mathbb{N}$$
17	3	anim1i	$$⊢\left(y\in \mathbb{P}\wedge y\parallel N\right)\to \left(y\in \mathbb{Z}\wedge y\parallel N\right)$$
18	9 17	sylbi	$$⊢y\in S\to \left(y\in \mathbb{Z}\wedge y\parallel N\right)$$
19		dvdsle	$$⊢\left(y\in \mathbb{Z}\wedge N\in \mathbb{N}\right)\to \left(y\parallel N\to y\le N\right)$$
20	19	expcom	$$⊢N\in \mathbb{N}\to \left(y\in \mathbb{Z}\to \left(y\parallel N\to y\le N\right)\right)$$
21	20	impd	$$⊢N\in \mathbb{N}\to \left(\left(y\in \mathbb{Z}\wedge y\parallel N\right)\to y\le N\right)$$
22	18 21	syl5	$$⊢N\in \mathbb{N}\to \left(y\in S\to y\le N\right)$$
23	22	ralrimiv	$$⊢N\in \mathbb{N}\to \forall y\in Sy\le N$$
24	16 23	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \forall y\in Sy\le N$$
25		brralrspcev	$$⊢\left(N\in \mathbb{Z}\wedge \forall y\in Sy\le N\right)\to \exists x\in \mathbb{Z}\forall y\in Sy\le x$$
26	15 24 25	syl2anc	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \exists x\in \mathbb{Z}\forall y\in Sy\le x$$
27	6 14 26	3jca	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(S\subseteq \mathbb{Z}\wedge S\ne \varnothing \wedge \exists x\in \mathbb{Z}\forall y\in Sy\le x\right)$$
28		suprzcl2	$$⊢\left(S\subseteq \mathbb{Z}\wedge S\ne \varnothing \wedge \exists x\in \mathbb{Z}\forall y\in Sy\le x\right)\to sup\left(S,ℝ,<\right)\in S$$
29	27 28	jccir	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(\left(S\subseteq \mathbb{Z}\wedge S\ne \varnothing \wedge \exists x\in \mathbb{Z}\forall y\in Sy\le x\right)\wedge sup\left(S,ℝ,<\right)\in S\right)$$