prmdvdsfmtnof1lem1

	Ref	Expression
Hypotheses	prmdvdsfmtnof1lem1.i	$⊢ I = inf (\{p \in ℙ \| p ∥ F\} ℝ <)$
	prmdvdsfmtnof1lem1.j	$⊢ J = inf (\{p \in ℙ \| p ∥ G\} ℝ <)$
Assertion	prmdvdsfmtnof1lem1	$⊢ (F \in ℤ_{\geq 2} \land G \in ℤ_{\geq 2}) \to (I = J \to (I \in ℙ \land I ∥ F \land I ∥ G))$

Proof

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

Metamath Proof Explorer

Theorem prmdvdsfmtnof1lem1

Proof