Metamath Proof Explorer

Theorem prmdvdsfmtnof1lem1

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

Ref Expression
Hypotheses prmdvdsfmtnof1lem1.i 
|- I = inf ( { p e. Prime | p || F } , RR , < )
prmdvdsfmtnof1lem1.j 
|- J = inf ( { p e. Prime | p || G } , RR , < )
Assertion prmdvdsfmtnof1lem1 
|- ( ( F e. ( ZZ>= ` 2 ) /\ G e. ( ZZ>= ` 2 ) ) -> ( I = J -> ( I e. Prime /\ I || F /\ I || G ) ) )

Proof

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