Theorem prmdvdsfmtnof1lem1

Description: Lemma 1 for prmdvdsfmtnof1 . (Contributed by AV, 3-Aug-2021)

	Ref	Expression
Hypotheses	prmdvdsfmtnof1lem1.i	$$⊢I=sup\left(\left\{p\in \mathbb{P}|p\parallel F\right\},ℝ,<\right)$$
	prmdvdsfmtnof1lem1.j	$$⊢J=sup\left(\left\{p\in \mathbb{P}|p\parallel G\right\},ℝ,<\right)$$
Assertion	prmdvdsfmtnof1lem1	$$⊢\left(F\in {\mathbb{Z}}_{\ge 2}\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\to \left(I=J\to \left(I\in \mathbb{P}\wedge I\parallel F\wedge I\parallel G\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		prmdvdsfmtnof1lem1.i	$$⊢I=sup\left(\left\{p\in \mathbb{P}|p\parallel F\right\},ℝ,<\right)$$
2		prmdvdsfmtnof1lem1.j	$$⊢J=sup\left(\left\{p\in \mathbb{P}|p\parallel G\right\},ℝ,<\right)$$
3		ltso	$$⊢<\mathrm{Or}ℝ$$
4	3	a1i	$$⊢\left(F\in {\mathbb{Z}}_{\ge 2}\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\to <\mathrm{Or}ℝ$$
5		eluz2nn	$$⊢F\in {\mathbb{Z}}_{\ge 2}\to F\in \mathbb{N}$$
6	5	adantr	$$⊢\left(F\in {\mathbb{Z}}_{\ge 2}\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\to F\in \mathbb{N}$$
7		prmdvdsfi	$$⊢F\in \mathbb{N}\to \left\{p\in \mathbb{P}|p\parallel F\right\}\in \mathrm{Fin}$$
8	6 7	syl	$$⊢\left(F\in {\mathbb{Z}}_{\ge 2}\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\to \left\{p\in \mathbb{P}|p\parallel F\right\}\in \mathrm{Fin}$$
9		exprmfct	$$⊢F\in {\mathbb{Z}}_{\ge 2}\to \exists p\in \mathbb{P}p\parallel F$$
10	9	adantr	$$⊢\left(F\in {\mathbb{Z}}_{\ge 2}\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\to \exists p\in \mathbb{P}p\parallel F$$
11		rabn0	$$⊢\left\{p\in \mathbb{P}|p\parallel F\right\}\ne \varnothing \leftrightarrow \exists p\in \mathbb{P}p\parallel F$$
12	10 11	sylibr	$$⊢\left(F\in {\mathbb{Z}}_{\ge 2}\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\to \left\{p\in \mathbb{P}|p\parallel F\right\}\ne \varnothing$$
13		ssrab2	$$⊢\left\{p\in \mathbb{P}|p\parallel F\right\}\subseteq \mathbb{P}$$
14		prmssnn	$$⊢\mathbb{P}\subseteq \mathbb{N}$$
15		nnssre	$$⊢\mathbb{N}\subseteq ℝ$$
16	14 15	sstri	$$⊢\mathbb{P}\subseteq ℝ$$
17	13 16	sstri	$$⊢\left\{p\in \mathbb{P}|p\parallel F\right\}\subseteq ℝ$$
18	17	a1i	$$⊢\left(F\in {\mathbb{Z}}_{\ge 2}\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\to \left\{p\in \mathbb{P}|p\parallel F\right\}\subseteq ℝ$$
19		fiinfcl	$$⊢\left(<\mathrm{Or}ℝ\wedge \left(\left\{p\in \mathbb{P}|p\parallel F\right\}\in \mathrm{Fin}\wedge \left\{p\in \mathbb{P}|p\parallel F\right\}\ne \varnothing \wedge \left\{p\in \mathbb{P}|p\parallel F\right\}\subseteq ℝ\right)\right)\to sup\left(\left\{p\in \mathbb{P}|p\parallel F\right\},ℝ,<\right)\in \left\{p\in \mathbb{P}|p\parallel F\right\}$$
20	4 8 12 18 19	syl13anc	$$⊢\left(F\in {\mathbb{Z}}_{\ge 2}\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\to sup\left(\left\{p\in \mathbb{P}|p\parallel F\right\},ℝ,<\right)\in \left\{p\in \mathbb{P}|p\parallel F\right\}$$
21	1	eleq1i	$$⊢I\in \left\{p\in \mathbb{P}|p\parallel F\right\}\leftrightarrow sup\left(\left\{p\in \mathbb{P}|p\parallel F\right\},ℝ,<\right)\in \left\{p\in \mathbb{P}|p\parallel F\right\}$$
22		eluz2nn	$$⊢G\in {\mathbb{Z}}_{\ge 2}\to G\in \mathbb{N}$$
23	22	adantl	$$⊢\left(F\in {\mathbb{Z}}_{\ge 2}\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\to G\in \mathbb{N}$$
24		prmdvdsfi	$$⊢G\in \mathbb{N}\to \left\{p\in \mathbb{P}|p\parallel G\right\}\in \mathrm{Fin}$$
25	23 24	syl	$$⊢\left(F\in {\mathbb{Z}}_{\ge 2}\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\to \left\{p\in \mathbb{P}|p\parallel G\right\}\in \mathrm{Fin}$$
26		exprmfct	$$⊢G\in {\mathbb{Z}}_{\ge 2}\to \exists p\in \mathbb{P}p\parallel G$$
27	26	adantl	$$⊢\left(F\in {\mathbb{Z}}_{\ge 2}\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\to \exists p\in \mathbb{P}p\parallel G$$
28		rabn0	$$⊢\left\{p\in \mathbb{P}|p\parallel G\right\}\ne \varnothing \leftrightarrow \exists p\in \mathbb{P}p\parallel G$$
29	27 28	sylibr	$$⊢\left(F\in {\mathbb{Z}}_{\ge 2}\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\to \left\{p\in \mathbb{P}|p\parallel G\right\}\ne \varnothing$$
30		ssrab2	$$⊢\left\{p\in \mathbb{P}|p\parallel G\right\}\subseteq \mathbb{P}$$
31	30 16	sstri	$$⊢\left\{p\in \mathbb{P}|p\parallel G\right\}\subseteq ℝ$$
32	31	a1i	$$⊢\left(F\in {\mathbb{Z}}_{\ge 2}\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\to \left\{p\in \mathbb{P}|p\parallel G\right\}\subseteq ℝ$$
33		fiinfcl	$$⊢\left(<\mathrm{Or}ℝ\wedge \left(\left\{p\in \mathbb{P}|p\parallel G\right\}\in \mathrm{Fin}\wedge \left\{p\in \mathbb{P}|p\parallel G\right\}\ne \varnothing \wedge \left\{p\in \mathbb{P}|p\parallel G\right\}\subseteq ℝ\right)\right)\to sup\left(\left\{p\in \mathbb{P}|p\parallel G\right\},ℝ,<\right)\in \left\{p\in \mathbb{P}|p\parallel G\right\}$$
34	4 25 29 32 33	syl13anc	$$⊢\left(F\in {\mathbb{Z}}_{\ge 2}\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\to sup\left(\left\{p\in \mathbb{P}|p\parallel G\right\},ℝ,<\right)\in \left\{p\in \mathbb{P}|p\parallel G\right\}$$
35	2	eleq1i	$$⊢J\in \left\{p\in \mathbb{P}|p\parallel G\right\}\leftrightarrow sup\left(\left\{p\in \mathbb{P}|p\parallel G\right\},ℝ,<\right)\in \left\{p\in \mathbb{P}|p\parallel G\right\}$$
36		nfrab1	$$⊢\underset{\_}{Ⅎ}p\left\{p\in \mathbb{P}|p\parallel G\right\}$$
37		nfcv	$$⊢\underset{\_}{Ⅎ}pℝ$$
38		nfcv	$$⊢\underset{\_}{Ⅎ}p<$$
39	36 37 38	nfinf	$$⊢\underset{\_}{Ⅎ}psup\left(\left\{p\in \mathbb{P}|p\parallel G\right\},ℝ,<\right)$$
40	2 39	nfcxfr	$$⊢\underset{\_}{Ⅎ}pJ$$
41		nfcv	$$⊢\underset{\_}{Ⅎ}p\mathbb{P}$$
42		nfcv	$$⊢\underset{\_}{Ⅎ}p\parallel$$
43		nfcv	$$⊢\underset{\_}{Ⅎ}pG$$
44	40 42 43	nfbr	$$⊢ℲpJ\parallel G$$
45		breq1	$$⊢p=J\to \left(p\parallel G\leftrightarrow J\parallel G\right)$$
46	40 41 44 45	elrabf	$$⊢J\in \left\{p\in \mathbb{P}|p\parallel G\right\}\leftrightarrow \left(J\in \mathbb{P}\wedge J\parallel G\right)$$
47		nfrab1	$$⊢\underset{\_}{Ⅎ}p\left\{p\in \mathbb{P}|p\parallel F\right\}$$
48	47 37 38	nfinf	$$⊢\underset{\_}{Ⅎ}psup\left(\left\{p\in \mathbb{P}|p\parallel F\right\},ℝ,<\right)$$
49	1 48	nfcxfr	$$⊢\underset{\_}{Ⅎ}pI$$
50		nfcv	$$⊢\underset{\_}{Ⅎ}pF$$
51	49 42 50	nfbr	$$⊢ℲpI\parallel F$$
52		breq1	$$⊢p=I\to \left(p\parallel F\leftrightarrow I\parallel F\right)$$
53	49 41 51 52	elrabf	$$⊢I\in \left\{p\in \mathbb{P}|p\parallel F\right\}\leftrightarrow \left(I\in \mathbb{P}\wedge I\parallel F\right)$$
54		simp2l	$$⊢\left(\left(J\in \mathbb{P}\wedge J\parallel G\right)\wedge \left(I\in \mathbb{P}\wedge I\parallel F\right)\wedge I=J\right)\to I\in \mathbb{P}$$
55		simp2r	$$⊢\left(\left(J\in \mathbb{P}\wedge J\parallel G\right)\wedge \left(I\in \mathbb{P}\wedge I\parallel F\right)\wedge I=J\right)\to I\parallel F$$
56		simp1r	$$⊢\left(\left(J\in \mathbb{P}\wedge J\parallel G\right)\wedge \left(I\in \mathbb{P}\wedge I\parallel F\right)\wedge I=J\right)\to J\parallel G$$
57		breq1	$$⊢I=J\to \left(I\parallel G\leftrightarrow J\parallel G\right)$$
58	57	3ad2ant3	$$⊢\left(\left(J\in \mathbb{P}\wedge J\parallel G\right)\wedge \left(I\in \mathbb{P}\wedge I\parallel F\right)\wedge I=J\right)\to \left(I\parallel G\leftrightarrow J\parallel G\right)$$
59	56 58	mpbird	$$⊢\left(\left(J\in \mathbb{P}\wedge J\parallel G\right)\wedge \left(I\in \mathbb{P}\wedge I\parallel F\right)\wedge I=J\right)\to I\parallel G$$
60	54 55 59	3jca	$$⊢\left(\left(J\in \mathbb{P}\wedge J\parallel G\right)\wedge \left(I\in \mathbb{P}\wedge I\parallel F\right)\wedge I=J\right)\to \left(I\in \mathbb{P}\wedge I\parallel F\wedge I\parallel G\right)$$
61	60	3exp	$$⊢\left(J\in \mathbb{P}\wedge J\parallel G\right)\to \left(\left(I\in \mathbb{P}\wedge I\parallel F\right)\to \left(I=J\to \left(I\in \mathbb{P}\wedge I\parallel F\wedge I\parallel G\right)\right)\right)$$
62	53 61	biimtrid	$$⊢\left(J\in \mathbb{P}\wedge J\parallel G\right)\to \left(I\in \left\{p\in \mathbb{P}|p\parallel F\right\}\to \left(I=J\to \left(I\in \mathbb{P}\wedge I\parallel F\wedge I\parallel G\right)\right)\right)$$
63	46 62	sylbi	$$⊢J\in \left\{p\in \mathbb{P}|p\parallel G\right\}\to \left(I\in \left\{p\in \mathbb{P}|p\parallel F\right\}\to \left(I=J\to \left(I\in \mathbb{P}\wedge I\parallel F\wedge I\parallel G\right)\right)\right)$$
64	63	a1i	$$⊢\left(F\in {\mathbb{Z}}_{\ge 2}\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\to \left(J\in \left\{p\in \mathbb{P}|p\parallel G\right\}\to \left(I\in \left\{p\in \mathbb{P}|p\parallel F\right\}\to \left(I=J\to \left(I\in \mathbb{P}\wedge I\parallel F\wedge I\parallel G\right)\right)\right)\right)$$
65	35 64	biimtrrid	$$⊢\left(F\in {\mathbb{Z}}_{\ge 2}\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\to \left(sup\left(\left\{p\in \mathbb{P}|p\parallel G\right\},ℝ,<\right)\in \left\{p\in \mathbb{P}|p\parallel G\right\}\to \left(I\in \left\{p\in \mathbb{P}|p\parallel F\right\}\to \left(I=J\to \left(I\in \mathbb{P}\wedge I\parallel F\wedge I\parallel G\right)\right)\right)\right)$$
66	34 65	mpd	$$⊢\left(F\in {\mathbb{Z}}_{\ge 2}\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\to \left(I\in \left\{p\in \mathbb{P}|p\parallel F\right\}\to \left(I=J\to \left(I\in \mathbb{P}\wedge I\parallel F\wedge I\parallel G\right)\right)\right)$$
67	21 66	biimtrrid	$$⊢\left(F\in {\mathbb{Z}}_{\ge 2}\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\to \left(sup\left(\left\{p\in \mathbb{P}|p\parallel F\right\},ℝ,<\right)\in \left\{p\in \mathbb{P}|p\parallel F\right\}\to \left(I=J\to \left(I\in \mathbb{P}\wedge I\parallel F\wedge I\parallel G\right)\right)\right)$$
68	20 67	mpd	$$⊢\left(F\in {\mathbb{Z}}_{\ge 2}\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\to \left(I=J\to \left(I\in \mathbb{P}\wedge I\parallel F\wedge I\parallel G\right)\right)$$