Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  prmdvdsfmtnof1lem1 Structured version   Visualization version   GIF version

Theorem prmdvdsfmtnof1lem1 44040
 Description: Lemma 1 for prmdvdsfmtnof1 44043. (Contributed by AV, 3-Aug-2021.)
Hypotheses
Ref Expression
prmdvdsfmtnof1lem1.i 𝐼 = inf({𝑝 ∈ ℙ ∣ 𝑝𝐹}, ℝ, < )
prmdvdsfmtnof1lem1.j 𝐽 = inf({𝑝 ∈ ℙ ∣ 𝑝𝐺}, ℝ, < )
Assertion
Ref Expression
prmdvdsfmtnof1lem1 ((𝐹 ∈ (ℤ‘2) ∧ 𝐺 ∈ (ℤ‘2)) → (𝐼 = 𝐽 → (𝐼 ∈ ℙ ∧ 𝐼𝐹𝐼𝐺)))
Distinct variable groups:   𝐹,𝑝   𝐺,𝑝
Allowed substitution hints:   𝐼(𝑝)   𝐽(𝑝)

Proof of Theorem prmdvdsfmtnof1lem1
StepHypRef Expression
1 ltso 10710 . . . 4 < Or ℝ
21a1i 11 . . 3 ((𝐹 ∈ (ℤ‘2) ∧ 𝐺 ∈ (ℤ‘2)) → < Or ℝ)
3 eluz2nn 12272 . . . . 5 (𝐹 ∈ (ℤ‘2) → 𝐹 ∈ ℕ)
43adantr 484 . . . 4 ((𝐹 ∈ (ℤ‘2) ∧ 𝐺 ∈ (ℤ‘2)) → 𝐹 ∈ ℕ)
5 prmdvdsfi 25690 . . . 4 (𝐹 ∈ ℕ → {𝑝 ∈ ℙ ∣ 𝑝𝐹} ∈ Fin)
64, 5syl 17 . . 3 ((𝐹 ∈ (ℤ‘2) ∧ 𝐺 ∈ (ℤ‘2)) → {𝑝 ∈ ℙ ∣ 𝑝𝐹} ∈ Fin)
7 exprmfct 16037 . . . . 5 (𝐹 ∈ (ℤ‘2) → ∃𝑝 ∈ ℙ 𝑝𝐹)
87adantr 484 . . . 4 ((𝐹 ∈ (ℤ‘2) ∧ 𝐺 ∈ (ℤ‘2)) → ∃𝑝 ∈ ℙ 𝑝𝐹)
9 rabn0 4311 . . . 4 ({𝑝 ∈ ℙ ∣ 𝑝𝐹} ≠ ∅ ↔ ∃𝑝 ∈ ℙ 𝑝𝐹)
108, 9sylibr 237 . . 3 ((𝐹 ∈ (ℤ‘2) ∧ 𝐺 ∈ (ℤ‘2)) → {𝑝 ∈ ℙ ∣ 𝑝𝐹} ≠ ∅)
11 ssrab2 4031 . . . . 5 {𝑝 ∈ ℙ ∣ 𝑝𝐹} ⊆ ℙ
12 prmssnn 16009 . . . . . 6 ℙ ⊆ ℕ
13 nnssre 11629 . . . . . 6 ℕ ⊆ ℝ
1412, 13sstri 3951 . . . . 5 ℙ ⊆ ℝ
1511, 14sstri 3951 . . . 4 {𝑝 ∈ ℙ ∣ 𝑝𝐹} ⊆ ℝ
1615a1i 11 . . 3 ((𝐹 ∈ (ℤ‘2) ∧ 𝐺 ∈ (ℤ‘2)) → {𝑝 ∈ ℙ ∣ 𝑝𝐹} ⊆ ℝ)
17 fiinfcl 8953 . . 3 (( < Or ℝ ∧ ({𝑝 ∈ ℙ ∣ 𝑝𝐹} ∈ Fin ∧ {𝑝 ∈ ℙ ∣ 𝑝𝐹} ≠ ∅ ∧ {𝑝 ∈ ℙ ∣ 𝑝𝐹} ⊆ ℝ)) → inf({𝑝 ∈ ℙ ∣ 𝑝𝐹}, ℝ, < ) ∈ {𝑝 ∈ ℙ ∣ 𝑝𝐹})
182, 6, 10, 16, 17syl13anc 1369 . 2 ((𝐹 ∈ (ℤ‘2) ∧ 𝐺 ∈ (ℤ‘2)) → inf({𝑝 ∈ ℙ ∣ 𝑝𝐹}, ℝ, < ) ∈ {𝑝 ∈ ℙ ∣ 𝑝𝐹})
19 prmdvdsfmtnof1lem1.i . . . 4 𝐼 = inf({𝑝 ∈ ℙ ∣ 𝑝𝐹}, ℝ, < )
2019eleq1i 2904 . . 3 (𝐼 ∈ {𝑝 ∈ ℙ ∣ 𝑝𝐹} ↔ inf({𝑝 ∈ ℙ ∣ 𝑝𝐹}, ℝ, < ) ∈ {𝑝 ∈ ℙ ∣ 𝑝𝐹})
21 eluz2nn 12272 . . . . . . 7 (𝐺 ∈ (ℤ‘2) → 𝐺 ∈ ℕ)
2221adantl 485 . . . . . 6 ((𝐹 ∈ (ℤ‘2) ∧ 𝐺 ∈ (ℤ‘2)) → 𝐺 ∈ ℕ)
23 prmdvdsfi 25690 . . . . . 6 (𝐺 ∈ ℕ → {𝑝 ∈ ℙ ∣ 𝑝𝐺} ∈ Fin)
2422, 23syl 17 . . . . 5 ((𝐹 ∈ (ℤ‘2) ∧ 𝐺 ∈ (ℤ‘2)) → {𝑝 ∈ ℙ ∣ 𝑝𝐺} ∈ Fin)
25 exprmfct 16037 . . . . . . 7 (𝐺 ∈ (ℤ‘2) → ∃𝑝 ∈ ℙ 𝑝𝐺)
2625adantl 485 . . . . . 6 ((𝐹 ∈ (ℤ‘2) ∧ 𝐺 ∈ (ℤ‘2)) → ∃𝑝 ∈ ℙ 𝑝𝐺)
27 rabn0 4311 . . . . . 6 ({𝑝 ∈ ℙ ∣ 𝑝𝐺} ≠ ∅ ↔ ∃𝑝 ∈ ℙ 𝑝𝐺)
2826, 27sylibr 237 . . . . 5 ((𝐹 ∈ (ℤ‘2) ∧ 𝐺 ∈ (ℤ‘2)) → {𝑝 ∈ ℙ ∣ 𝑝𝐺} ≠ ∅)
29 ssrab2 4031 . . . . . . 7 {𝑝 ∈ ℙ ∣ 𝑝𝐺} ⊆ ℙ
3029, 14sstri 3951 . . . . . 6 {𝑝 ∈ ℙ ∣ 𝑝𝐺} ⊆ ℝ
3130a1i 11 . . . . 5 ((𝐹 ∈ (ℤ‘2) ∧ 𝐺 ∈ (ℤ‘2)) → {𝑝 ∈ ℙ ∣ 𝑝𝐺} ⊆ ℝ)
32 fiinfcl 8953 . . . . 5 (( < Or ℝ ∧ ({𝑝 ∈ ℙ ∣ 𝑝𝐺} ∈ Fin ∧ {𝑝 ∈ ℙ ∣ 𝑝𝐺} ≠ ∅ ∧ {𝑝 ∈ ℙ ∣ 𝑝𝐺} ⊆ ℝ)) → inf({𝑝 ∈ ℙ ∣ 𝑝𝐺}, ℝ, < ) ∈ {𝑝 ∈ ℙ ∣ 𝑝𝐺})
332, 24, 28, 31, 32syl13anc 1369 . . . 4 ((𝐹 ∈ (ℤ‘2) ∧ 𝐺 ∈ (ℤ‘2)) → inf({𝑝 ∈ ℙ ∣ 𝑝𝐺}, ℝ, < ) ∈ {𝑝 ∈ ℙ ∣ 𝑝𝐺})
34 prmdvdsfmtnof1lem1.j . . . . . 6 𝐽 = inf({𝑝 ∈ ℙ ∣ 𝑝𝐺}, ℝ, < )
3534eleq1i 2904 . . . . 5 (𝐽 ∈ {𝑝 ∈ ℙ ∣ 𝑝𝐺} ↔ inf({𝑝 ∈ ℙ ∣ 𝑝𝐺}, ℝ, < ) ∈ {𝑝 ∈ ℙ ∣ 𝑝𝐺})
36 nfrab1 3365 . . . . . . . . . 10 𝑝{𝑝 ∈ ℙ ∣ 𝑝𝐺}
37 nfcv 2979 . . . . . . . . . 10 𝑝
38 nfcv 2979 . . . . . . . . . 10 𝑝 <
3936, 37, 38nfinf 8934 . . . . . . . . 9 𝑝inf({𝑝 ∈ ℙ ∣ 𝑝𝐺}, ℝ, < )
4034, 39nfcxfr 2977 . . . . . . . 8 𝑝𝐽
41 nfcv 2979 . . . . . . . 8 𝑝
42 nfcv 2979 . . . . . . . . 9 𝑝
43 nfcv 2979 . . . . . . . . 9 𝑝𝐺
4440, 42, 43nfbr 5089 . . . . . . . 8 𝑝 𝐽𝐺
45 breq1 5045 . . . . . . . 8 (𝑝 = 𝐽 → (𝑝𝐺𝐽𝐺))
4640, 41, 44, 45elrabf 3651 . . . . . . 7 (𝐽 ∈ {𝑝 ∈ ℙ ∣ 𝑝𝐺} ↔ (𝐽 ∈ ℙ ∧ 𝐽𝐺))
47 nfrab1 3365 . . . . . . . . . . 11 𝑝{𝑝 ∈ ℙ ∣ 𝑝𝐹}
4847, 37, 38nfinf 8934 . . . . . . . . . 10 𝑝inf({𝑝 ∈ ℙ ∣ 𝑝𝐹}, ℝ, < )
4919, 48nfcxfr 2977 . . . . . . . . 9 𝑝𝐼
50 nfcv 2979 . . . . . . . . . 10 𝑝𝐹
5149, 42, 50nfbr 5089 . . . . . . . . 9 𝑝 𝐼𝐹
52 breq1 5045 . . . . . . . . 9 (𝑝 = 𝐼 → (𝑝𝐹𝐼𝐹))
5349, 41, 51, 52elrabf 3651 . . . . . . . 8 (𝐼 ∈ {𝑝 ∈ ℙ ∣ 𝑝𝐹} ↔ (𝐼 ∈ ℙ ∧ 𝐼𝐹))
54 simp2l 1196 . . . . . . . . . 10 (((𝐽 ∈ ℙ ∧ 𝐽𝐺) ∧ (𝐼 ∈ ℙ ∧ 𝐼𝐹) ∧ 𝐼 = 𝐽) → 𝐼 ∈ ℙ)
55 simp2r 1197 . . . . . . . . . 10 (((𝐽 ∈ ℙ ∧ 𝐽𝐺) ∧ (𝐼 ∈ ℙ ∧ 𝐼𝐹) ∧ 𝐼 = 𝐽) → 𝐼𝐹)
56 simp1r 1195 . . . . . . . . . . 11 (((𝐽 ∈ ℙ ∧ 𝐽𝐺) ∧ (𝐼 ∈ ℙ ∧ 𝐼𝐹) ∧ 𝐼 = 𝐽) → 𝐽𝐺)
57 breq1 5045 . . . . . . . . . . . 12 (𝐼 = 𝐽 → (𝐼𝐺𝐽𝐺))
58573ad2ant3 1132 . . . . . . . . . . 11 (((𝐽 ∈ ℙ ∧ 𝐽𝐺) ∧ (𝐼 ∈ ℙ ∧ 𝐼𝐹) ∧ 𝐼 = 𝐽) → (𝐼𝐺𝐽𝐺))
5956, 58mpbird 260 . . . . . . . . . 10 (((𝐽 ∈ ℙ ∧ 𝐽𝐺) ∧ (𝐼 ∈ ℙ ∧ 𝐼𝐹) ∧ 𝐼 = 𝐽) → 𝐼𝐺)
6054, 55, 593jca 1125 . . . . . . . . 9 (((𝐽 ∈ ℙ ∧ 𝐽𝐺) ∧ (𝐼 ∈ ℙ ∧ 𝐼𝐹) ∧ 𝐼 = 𝐽) → (𝐼 ∈ ℙ ∧ 𝐼𝐹𝐼𝐺))
61603exp 1116 . . . . . . . 8 ((𝐽 ∈ ℙ ∧ 𝐽𝐺) → ((𝐼 ∈ ℙ ∧ 𝐼𝐹) → (𝐼 = 𝐽 → (𝐼 ∈ ℙ ∧ 𝐼𝐹𝐼𝐺))))
6253, 61syl5bi 245 . . . . . . 7 ((𝐽 ∈ ℙ ∧ 𝐽𝐺) → (𝐼 ∈ {𝑝 ∈ ℙ ∣ 𝑝𝐹} → (𝐼 = 𝐽 → (𝐼 ∈ ℙ ∧ 𝐼𝐹𝐼𝐺))))
6346, 62sylbi 220 . . . . . 6 (𝐽 ∈ {𝑝 ∈ ℙ ∣ 𝑝𝐺} → (𝐼 ∈ {𝑝 ∈ ℙ ∣ 𝑝𝐹} → (𝐼 = 𝐽 → (𝐼 ∈ ℙ ∧ 𝐼𝐹𝐼𝐺))))
6463a1i 11 . . . . 5 ((𝐹 ∈ (ℤ‘2) ∧ 𝐺 ∈ (ℤ‘2)) → (𝐽 ∈ {𝑝 ∈ ℙ ∣ 𝑝𝐺} → (𝐼 ∈ {𝑝 ∈ ℙ ∣ 𝑝𝐹} → (𝐼 = 𝐽 → (𝐼 ∈ ℙ ∧ 𝐼𝐹𝐼𝐺)))))
6535, 64syl5bir 246 . . . 4 ((𝐹 ∈ (ℤ‘2) ∧ 𝐺 ∈ (ℤ‘2)) → (inf({𝑝 ∈ ℙ ∣ 𝑝𝐺}, ℝ, < ) ∈ {𝑝 ∈ ℙ ∣ 𝑝𝐺} → (𝐼 ∈ {𝑝 ∈ ℙ ∣ 𝑝𝐹} → (𝐼 = 𝐽 → (𝐼 ∈ ℙ ∧ 𝐼𝐹𝐼𝐺)))))
6633, 65mpd 15 . . 3 ((𝐹 ∈ (ℤ‘2) ∧ 𝐺 ∈ (ℤ‘2)) → (𝐼 ∈ {𝑝 ∈ ℙ ∣ 𝑝𝐹} → (𝐼 = 𝐽 → (𝐼 ∈ ℙ ∧ 𝐼𝐹𝐼𝐺))))
6720, 66syl5bir 246 . 2 ((𝐹 ∈ (ℤ‘2) ∧ 𝐺 ∈ (ℤ‘2)) → (inf({𝑝 ∈ ℙ ∣ 𝑝𝐹}, ℝ, < ) ∈ {𝑝 ∈ ℙ ∣ 𝑝𝐹} → (𝐼 = 𝐽 → (𝐼 ∈ ℙ ∧ 𝐼𝐹𝐼𝐺))))
6818, 67mpd 15 1 ((𝐹 ∈ (ℤ‘2) ∧ 𝐺 ∈ (ℤ‘2)) → (𝐼 = 𝐽 → (𝐼 ∈ ℙ ∧ 𝐼𝐹𝐼𝐺)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2114   ≠ wne 3011  ∃wrex 3131  {crab 3134   ⊆ wss 3908  ∅c0 4265   class class class wbr 5042   Or wor 5450  ‘cfv 6334  Fincfn 8496  infcinf 8893  ℝcr 10525   < clt 10664  ℕcn 11625  2c2 11680  ℤ≥cuz 12231   ∥ cdvds 15598  ℙcprime 16004 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rmo 3138  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-om 7566  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-sup 8894  df-inf 8895  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-n0 11886  df-z 11970  df-uz 12232  df-rp 12378  df-fz 12886  df-seq 13365  df-exp 13426  df-cj 14449  df-re 14450  df-im 14451  df-sqrt 14585  df-abs 14586  df-dvds 15599  df-prm 16005 This theorem is referenced by:  prmdvdsfmtnof1  44043
 Copyright terms: Public domain W3C validator