Theorem prmdvdsfmtnof1lem1

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

	Ref	Expression
Hypotheses	prmdvdsfmtnof1lem1.i	⊢ 𝐼 = inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } , ℝ , < )
	prmdvdsfmtnof1lem1.j	⊢ 𝐽 = inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } , ℝ , < )
Assertion	prmdvdsfmtnof1lem1	⊢ ( ( 𝐹 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐼 = 𝐽 → ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		prmdvdsfmtnof1lem1.i	⊢ 𝐼 = inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } , ℝ , < )
2		prmdvdsfmtnof1lem1.j	⊢ 𝐽 = inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } , ℝ , < )
3		ltso	⊢ < Or ℝ
4	3	a1i	⊢ ( ( 𝐹 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) → < Or ℝ )
5		eluz2nn	⊢ ( 𝐹 ∈ ( ℤ≥ ‘ 2 ) → 𝐹 ∈ ℕ )
6	5	adantr	⊢ ( ( 𝐹 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐹 ∈ ℕ )
7		prmdvdsfi	⊢ ( 𝐹 ∈ ℕ → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } ∈ Fin )
8	6 7	syl	⊢ ( ( 𝐹 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } ∈ Fin )
9		exprmfct	⊢ ( 𝐹 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝐹 )
10	9	adantr	⊢ ( ( 𝐹 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝐹 )
11		rabn0	⊢ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } ≠ ∅ ↔ ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝐹 )
12	10 11	sylibr	⊢ ( ( 𝐹 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } ≠ ∅ )
13		ssrab2	⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } ⊆ ℙ
14		prmssnn	⊢ ℙ ⊆ ℕ
15		nnssre	⊢ ℕ ⊆ ℝ
16	14 15	sstri	⊢ ℙ ⊆ ℝ
17	13 16	sstri	⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } ⊆ ℝ
18	17	a1i	⊢ ( ( 𝐹 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } ⊆ ℝ )
19		fiinfcl	⊢ ( ( < Or ℝ ∧ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } ∈ Fin ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } ≠ ∅ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } ⊆ ℝ ) ) → inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } , ℝ , < ) ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } )
20	4 8 12 18 19	syl13anc	⊢ ( ( 𝐹 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) → inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } , ℝ , < ) ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } )
21	1	eleq1i	⊢ ( 𝐼 ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } ↔ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } , ℝ , < ) ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } )
22		eluz2nn	⊢ ( 𝐺 ∈ ( ℤ≥ ‘ 2 ) → 𝐺 ∈ ℕ )
23	22	adantl	⊢ ( ( 𝐹 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐺 ∈ ℕ )
24		prmdvdsfi	⊢ ( 𝐺 ∈ ℕ → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } ∈ Fin )
25	23 24	syl	⊢ ( ( 𝐹 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } ∈ Fin )
26		exprmfct	⊢ ( 𝐺 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝐺 )
27	26	adantl	⊢ ( ( 𝐹 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝐺 )
28		rabn0	⊢ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } ≠ ∅ ↔ ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝐺 )
29	27 28	sylibr	⊢ ( ( 𝐹 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } ≠ ∅ )
30		ssrab2	⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } ⊆ ℙ
31	30 16	sstri	⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } ⊆ ℝ
32	31	a1i	⊢ ( ( 𝐹 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } ⊆ ℝ )
33		fiinfcl	⊢ ( ( < Or ℝ ∧ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } ∈ Fin ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } ≠ ∅ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } ⊆ ℝ ) ) → inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } , ℝ , < ) ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } )
34	4 25 29 32 33	syl13anc	⊢ ( ( 𝐹 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) → inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } , ℝ , < ) ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } )
35	2	eleq1i	⊢ ( 𝐽 ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } ↔ inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } , ℝ , < ) ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } )
36		nfrab1	⊢ Ⅎ 𝑝 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 }
37		nfcv	⊢ Ⅎ 𝑝 ℝ
38		nfcv	⊢ Ⅎ 𝑝 <
39	36 37 38	nfinf	⊢ Ⅎ 𝑝 inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } , ℝ , < )
40	2 39	nfcxfr	⊢ Ⅎ 𝑝 𝐽
41		nfcv	⊢ Ⅎ 𝑝 ℙ
42		nfcv	⊢ Ⅎ 𝑝 ∥
43		nfcv	⊢ Ⅎ 𝑝 𝐺
44	40 42 43	nfbr	⊢ Ⅎ 𝑝 𝐽 ∥ 𝐺
45		breq1	⊢ ( 𝑝 = 𝐽 → ( 𝑝 ∥ 𝐺 ↔ 𝐽 ∥ 𝐺 ) )
46	40 41 44 45	elrabf	⊢ ( 𝐽 ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } ↔ ( 𝐽 ∈ ℙ ∧ 𝐽 ∥ 𝐺 ) )
47		nfrab1	⊢ Ⅎ 𝑝 { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 }
48	47 37 38	nfinf	⊢ Ⅎ 𝑝 inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } , ℝ , < )
49	1 48	nfcxfr	⊢ Ⅎ 𝑝 𝐼
50		nfcv	⊢ Ⅎ 𝑝 𝐹
51	49 42 50	nfbr	⊢ Ⅎ 𝑝 𝐼 ∥ 𝐹
52		breq1	⊢ ( 𝑝 = 𝐼 → ( 𝑝 ∥ 𝐹 ↔ 𝐼 ∥ 𝐹 ) )
53	49 41 51 52	elrabf	⊢ ( 𝐼 ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } ↔ ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ) )
54		simp2l	⊢ ( ( ( 𝐽 ∈ ℙ ∧ 𝐽 ∥ 𝐺 ) ∧ ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ) ∧ 𝐼 = 𝐽 ) → 𝐼 ∈ ℙ )
55		simp2r	⊢ ( ( ( 𝐽 ∈ ℙ ∧ 𝐽 ∥ 𝐺 ) ∧ ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ) ∧ 𝐼 = 𝐽 ) → 𝐼 ∥ 𝐹 )
56		simp1r	⊢ ( ( ( 𝐽 ∈ ℙ ∧ 𝐽 ∥ 𝐺 ) ∧ ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ) ∧ 𝐼 = 𝐽 ) → 𝐽 ∥ 𝐺 )
57		breq1	⊢ ( 𝐼 = 𝐽 → ( 𝐼 ∥ 𝐺 ↔ 𝐽 ∥ 𝐺 ) )
58	57	3ad2ant3	⊢ ( ( ( 𝐽 ∈ ℙ ∧ 𝐽 ∥ 𝐺 ) ∧ ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ) ∧ 𝐼 = 𝐽 ) → ( 𝐼 ∥ 𝐺 ↔ 𝐽 ∥ 𝐺 ) )
59	56 58	mpbird	⊢ ( ( ( 𝐽 ∈ ℙ ∧ 𝐽 ∥ 𝐺 ) ∧ ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ) ∧ 𝐼 = 𝐽 ) → 𝐼 ∥ 𝐺 )
60	54 55 59	3jca	⊢ ( ( ( 𝐽 ∈ ℙ ∧ 𝐽 ∥ 𝐺 ) ∧ ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ) ∧ 𝐼 = 𝐽 ) → ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) )
61	60	3exp	⊢ ( ( 𝐽 ∈ ℙ ∧ 𝐽 ∥ 𝐺 ) → ( ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ) → ( 𝐼 = 𝐽 → ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) ) ) )
62	53 61	syl5bi	⊢ ( ( 𝐽 ∈ ℙ ∧ 𝐽 ∥ 𝐺 ) → ( 𝐼 ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } → ( 𝐼 = 𝐽 → ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) ) ) )
63	46 62	sylbi	⊢ ( 𝐽 ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } → ( 𝐼 ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } → ( 𝐼 = 𝐽 → ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) ) ) )
64	63	a1i	⊢ ( ( 𝐹 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐽 ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } → ( 𝐼 ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } → ( 𝐼 = 𝐽 → ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) ) ) ) )
65	35 64	syl5bir	⊢ ( ( 𝐹 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) → ( inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } , ℝ , < ) ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺 } → ( 𝐼 ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } → ( 𝐼 = 𝐽 → ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) ) ) ) )
66	34 65	mpd	⊢ ( ( 𝐹 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐼 ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } → ( 𝐼 = 𝐽 → ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) ) ) )
67	21 66	syl5bir	⊢ ( ( 𝐹 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) → ( inf ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } , ℝ , < ) ∈ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹 } → ( 𝐼 = 𝐽 → ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) ) ) )
68	20 67	mpd	⊢ ( ( 𝐹 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐼 = 𝐽 → ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) ) )