MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zringlpirlem3 Structured version   Visualization version   GIF version

Theorem zringlpirlem3 20153
Description: Lemma for zringlpir 20156. All elements of a nonzero ideal of integers are divided by the least one. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.) (Proof shortened by AV, 27-Sep-2020.)
Hypotheses
Ref Expression
zringlpirlem.i (𝜑𝐼 ∈ (LIdeal‘ℤring))
zringlpirlem.n0 (𝜑𝐼 ≠ {0})
zringlpirlem.g 𝐺 = inf((𝐼 ∩ ℕ), ℝ, < )
zringlpirlem.x (𝜑𝑋𝐼)
Assertion
Ref Expression
zringlpirlem3 (𝜑𝐺𝑋)

Proof of Theorem zringlpirlem3
StepHypRef Expression
1 zringlpirlem.i . . . . . . . . 9 (𝜑𝐼 ∈ (LIdeal‘ℤring))
2 zringbas 20143 . . . . . . . . . 10 ℤ = (Base‘ℤring)
3 eqid 2797 . . . . . . . . . 10 (LIdeal‘ℤring) = (LIdeal‘ℤring)
42, 3lidlss 19530 . . . . . . . . 9 (𝐼 ∈ (LIdeal‘ℤring) → 𝐼 ⊆ ℤ)
51, 4syl 17 . . . . . . . 8 (𝜑𝐼 ⊆ ℤ)
6 zringlpirlem.x . . . . . . . 8 (𝜑𝑋𝐼)
75, 6sseldd 3797 . . . . . . 7 (𝜑𝑋 ∈ ℤ)
87zred 11768 . . . . . 6 (𝜑𝑋 ∈ ℝ)
9 inss2 4027 . . . . . . . 8 (𝐼 ∩ ℕ) ⊆ ℕ
10 zringlpirlem.g . . . . . . . . 9 𝐺 = inf((𝐼 ∩ ℕ), ℝ, < )
11 nnuz 11963 . . . . . . . . . . 11 ℕ = (ℤ‘1)
129, 11sseqtri 3831 . . . . . . . . . 10 (𝐼 ∩ ℕ) ⊆ (ℤ‘1)
13 zringlpirlem.n0 . . . . . . . . . . 11 (𝜑𝐼 ≠ {0})
141, 13zringlpirlem1 20151 . . . . . . . . . 10 (𝜑 → (𝐼 ∩ ℕ) ≠ ∅)
15 infssuzcl 12013 . . . . . . . . . 10 (((𝐼 ∩ ℕ) ⊆ (ℤ‘1) ∧ (𝐼 ∩ ℕ) ≠ ∅) → inf((𝐼 ∩ ℕ), ℝ, < ) ∈ (𝐼 ∩ ℕ))
1612, 14, 15sylancr 582 . . . . . . . . 9 (𝜑 → inf((𝐼 ∩ ℕ), ℝ, < ) ∈ (𝐼 ∩ ℕ))
1710, 16syl5eqel 2880 . . . . . . . 8 (𝜑𝐺 ∈ (𝐼 ∩ ℕ))
189, 17sseldi 3794 . . . . . . 7 (𝜑𝐺 ∈ ℕ)
1918nnrpd 12111 . . . . . 6 (𝜑𝐺 ∈ ℝ+)
20 modlt 12930 . . . . . 6 ((𝑋 ∈ ℝ ∧ 𝐺 ∈ ℝ+) → (𝑋 mod 𝐺) < 𝐺)
218, 19, 20syl2anc 580 . . . . 5 (𝜑 → (𝑋 mod 𝐺) < 𝐺)
227, 18zmodcld 12942 . . . . . . 7 (𝜑 → (𝑋 mod 𝐺) ∈ ℕ0)
2322nn0red 11637 . . . . . 6 (𝜑 → (𝑋 mod 𝐺) ∈ ℝ)
2418nnred 11327 . . . . . 6 (𝜑𝐺 ∈ ℝ)
2523, 24ltnled 10472 . . . . 5 (𝜑 → ((𝑋 mod 𝐺) < 𝐺 ↔ ¬ 𝐺 ≤ (𝑋 mod 𝐺)))
2621, 25mpbid 224 . . . 4 (𝜑 → ¬ 𝐺 ≤ (𝑋 mod 𝐺))
277zcnd 11769 . . . . . . . . . . 11 (𝜑𝑋 ∈ ℂ)
2818nncnd 11328 . . . . . . . . . . . 12 (𝜑𝐺 ∈ ℂ)
298, 18nndivred 11363 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 / 𝐺) ∈ ℝ)
3029flcld 12850 . . . . . . . . . . . . 13 (𝜑 → (⌊‘(𝑋 / 𝐺)) ∈ ℤ)
3130zcnd 11769 . . . . . . . . . . . 12 (𝜑 → (⌊‘(𝑋 / 𝐺)) ∈ ℂ)
3228, 31mulcld 10347 . . . . . . . . . . 11 (𝜑 → (𝐺 · (⌊‘(𝑋 / 𝐺))) ∈ ℂ)
3327, 32negsubd 10688 . . . . . . . . . 10 (𝜑 → (𝑋 + -(𝐺 · (⌊‘(𝑋 / 𝐺)))) = (𝑋 − (𝐺 · (⌊‘(𝑋 / 𝐺)))))
3430znegcld 11770 . . . . . . . . . . . . . 14 (𝜑 → -(⌊‘(𝑋 / 𝐺)) ∈ ℤ)
3534zcnd 11769 . . . . . . . . . . . . 13 (𝜑 → -(⌊‘(𝑋 / 𝐺)) ∈ ℂ)
3635, 28mulcomd 10348 . . . . . . . . . . . 12 (𝜑 → (-(⌊‘(𝑋 / 𝐺)) · 𝐺) = (𝐺 · -(⌊‘(𝑋 / 𝐺))))
3728, 31mulneg2d 10774 . . . . . . . . . . . 12 (𝜑 → (𝐺 · -(⌊‘(𝑋 / 𝐺))) = -(𝐺 · (⌊‘(𝑋 / 𝐺))))
3836, 37eqtrd 2831 . . . . . . . . . . 11 (𝜑 → (-(⌊‘(𝑋 / 𝐺)) · 𝐺) = -(𝐺 · (⌊‘(𝑋 / 𝐺))))
3938oveq2d 6892 . . . . . . . . . 10 (𝜑 → (𝑋 + (-(⌊‘(𝑋 / 𝐺)) · 𝐺)) = (𝑋 + -(𝐺 · (⌊‘(𝑋 / 𝐺)))))
40 modval 12921 . . . . . . . . . . 11 ((𝑋 ∈ ℝ ∧ 𝐺 ∈ ℝ+) → (𝑋 mod 𝐺) = (𝑋 − (𝐺 · (⌊‘(𝑋 / 𝐺)))))
418, 19, 40syl2anc 580 . . . . . . . . . 10 (𝜑 → (𝑋 mod 𝐺) = (𝑋 − (𝐺 · (⌊‘(𝑋 / 𝐺)))))
4233, 39, 413eqtr4rd 2842 . . . . . . . . 9 (𝜑 → (𝑋 mod 𝐺) = (𝑋 + (-(⌊‘(𝑋 / 𝐺)) · 𝐺)))
43 zringring 20140 . . . . . . . . . . 11 ring ∈ Ring
4443a1i 11 . . . . . . . . . 10 (𝜑 → ℤring ∈ Ring)
451, 13, 10zringlpirlem2 20152 . . . . . . . . . . 11 (𝜑𝐺𝐼)
46 zringmulr 20146 . . . . . . . . . . . 12 · = (.r‘ℤring)
473, 2, 46lidlmcl 19537 . . . . . . . . . . 11 (((ℤring ∈ Ring ∧ 𝐼 ∈ (LIdeal‘ℤring)) ∧ (-(⌊‘(𝑋 / 𝐺)) ∈ ℤ ∧ 𝐺𝐼)) → (-(⌊‘(𝑋 / 𝐺)) · 𝐺) ∈ 𝐼)
4844, 1, 34, 45, 47syl22anc 868 . . . . . . . . . 10 (𝜑 → (-(⌊‘(𝑋 / 𝐺)) · 𝐺) ∈ 𝐼)
49 zringplusg 20144 . . . . . . . . . . 11 + = (+g‘ℤring)
503, 49lidlacl 19533 . . . . . . . . . 10 (((ℤring ∈ Ring ∧ 𝐼 ∈ (LIdeal‘ℤring)) ∧ (𝑋𝐼 ∧ (-(⌊‘(𝑋 / 𝐺)) · 𝐺) ∈ 𝐼)) → (𝑋 + (-(⌊‘(𝑋 / 𝐺)) · 𝐺)) ∈ 𝐼)
5144, 1, 6, 48, 50syl22anc 868 . . . . . . . . 9 (𝜑 → (𝑋 + (-(⌊‘(𝑋 / 𝐺)) · 𝐺)) ∈ 𝐼)
5242, 51eqeltrd 2876 . . . . . . . 8 (𝜑 → (𝑋 mod 𝐺) ∈ 𝐼)
5352adantr 473 . . . . . . 7 ((𝜑 ∧ (𝑋 mod 𝐺) ∈ ℕ) → (𝑋 mod 𝐺) ∈ 𝐼)
54 simpr 478 . . . . . . 7 ((𝜑 ∧ (𝑋 mod 𝐺) ∈ ℕ) → (𝑋 mod 𝐺) ∈ ℕ)
5553, 54elind 3994 . . . . . 6 ((𝜑 ∧ (𝑋 mod 𝐺) ∈ ℕ) → (𝑋 mod 𝐺) ∈ (𝐼 ∩ ℕ))
56 infssuzle 12012 . . . . . 6 (((𝐼 ∩ ℕ) ⊆ (ℤ‘1) ∧ (𝑋 mod 𝐺) ∈ (𝐼 ∩ ℕ)) → inf((𝐼 ∩ ℕ), ℝ, < ) ≤ (𝑋 mod 𝐺))
5712, 55, 56sylancr 582 . . . . 5 ((𝜑 ∧ (𝑋 mod 𝐺) ∈ ℕ) → inf((𝐼 ∩ ℕ), ℝ, < ) ≤ (𝑋 mod 𝐺))
5810, 57syl5eqbr 4876 . . . 4 ((𝜑 ∧ (𝑋 mod 𝐺) ∈ ℕ) → 𝐺 ≤ (𝑋 mod 𝐺))
5926, 58mtand 851 . . 3 (𝜑 → ¬ (𝑋 mod 𝐺) ∈ ℕ)
60 elnn0 11578 . . . 4 ((𝑋 mod 𝐺) ∈ ℕ0 ↔ ((𝑋 mod 𝐺) ∈ ℕ ∨ (𝑋 mod 𝐺) = 0))
6122, 60sylib 210 . . 3 (𝜑 → ((𝑋 mod 𝐺) ∈ ℕ ∨ (𝑋 mod 𝐺) = 0))
62 orel1 913 . . 3 (¬ (𝑋 mod 𝐺) ∈ ℕ → (((𝑋 mod 𝐺) ∈ ℕ ∨ (𝑋 mod 𝐺) = 0) → (𝑋 mod 𝐺) = 0))
6359, 61, 62sylc 65 . 2 (𝜑 → (𝑋 mod 𝐺) = 0)
64 dvdsval3 15320 . . 3 ((𝐺 ∈ ℕ ∧ 𝑋 ∈ ℤ) → (𝐺𝑋 ↔ (𝑋 mod 𝐺) = 0))
6518, 7, 64syl2anc 580 . 2 (𝜑 → (𝐺𝑋 ↔ (𝑋 mod 𝐺) = 0))
6663, 65mpbird 249 1 (𝜑𝐺𝑋)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 385  wo 874   = wceq 1653  wcel 2157  wne 2969  cin 3766  wss 3767  c0 4113  {csn 4366   class class class wbr 4841  cfv 6099  (class class class)co 6876  infcinf 8587  cr 10221  0cc0 10222  1c1 10223   + caddc 10225   · cmul 10227   < clt 10361  cle 10362  cmin 10554  -cneg 10555   / cdiv 10974  cn 11310  0cn0 11576  cz 11662  cuz 11926  +crp 12070  cfl 12842   mod cmo 12919  cdvds 15316  Ringcrg 18860  LIdealclidl 19490  ringzring 20137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2354  ax-ext 2775  ax-rep 4962  ax-sep 4973  ax-nul 4981  ax-pow 5033  ax-pr 5095  ax-un 7181  ax-cnex 10278  ax-resscn 10279  ax-1cn 10280  ax-icn 10281  ax-addcl 10282  ax-addrcl 10283  ax-mulcl 10284  ax-mulrcl 10285  ax-mulcom 10286  ax-addass 10287  ax-mulass 10288  ax-distr 10289  ax-i2m1 10290  ax-1ne0 10291  ax-1rid 10292  ax-rnegex 10293  ax-rrecex 10294  ax-cnre 10295  ax-pre-lttri 10296  ax-pre-lttrn 10297  ax-pre-ltadd 10298  ax-pre-mulgt0 10299  ax-pre-sup 10300  ax-addf 10301  ax-mulf 10302
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2590  df-eu 2607  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ne 2970  df-nel 3073  df-ral 3092  df-rex 3093  df-reu 3094  df-rmo 3095  df-rab 3096  df-v 3385  df-sbc 3632  df-csb 3727  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-pss 3783  df-nul 4114  df-if 4276  df-pw 4349  df-sn 4367  df-pr 4369  df-tp 4371  df-op 4373  df-uni 4627  df-int 4666  df-iun 4710  df-br 4842  df-opab 4904  df-mpt 4921  df-tr 4944  df-id 5218  df-eprel 5223  df-po 5231  df-so 5232  df-fr 5269  df-we 5271  df-xp 5316  df-rel 5317  df-cnv 5318  df-co 5319  df-dm 5320  df-rn 5321  df-res 5322  df-ima 5323  df-pred 5896  df-ord 5942  df-on 5943  df-lim 5944  df-suc 5945  df-iota 6062  df-fun 6101  df-fn 6102  df-f 6103  df-f1 6104  df-fo 6105  df-f1o 6106  df-fv 6107  df-riota 6837  df-ov 6879  df-oprab 6880  df-mpt2 6881  df-om 7298  df-1st 7399  df-2nd 7400  df-wrecs 7643  df-recs 7705  df-rdg 7743  df-1o 7797  df-oadd 7801  df-er 7980  df-en 8194  df-dom 8195  df-sdom 8196  df-fin 8197  df-sup 8588  df-inf 8589  df-pnf 10363  df-mnf 10364  df-xr 10365  df-ltxr 10366  df-le 10367  df-sub 10556  df-neg 10557  df-div 10975  df-nn 11311  df-2 11372  df-3 11373  df-4 11374  df-5 11375  df-6 11376  df-7 11377  df-8 11378  df-9 11379  df-n0 11577  df-z 11663  df-dec 11780  df-uz 11927  df-rp 12071  df-fz 12577  df-fl 12844  df-mod 12920  df-seq 13052  df-exp 13111  df-cj 14177  df-re 14178  df-im 14179  df-sqrt 14313  df-abs 14314  df-dvds 15317  df-struct 16183  df-ndx 16184  df-slot 16185  df-base 16187  df-sets 16188  df-ress 16189  df-plusg 16277  df-mulr 16278  df-starv 16279  df-sca 16280  df-vsca 16281  df-ip 16282  df-tset 16283  df-ple 16284  df-ds 16286  df-unif 16287  df-0g 16414  df-mgm 17554  df-sgrp 17596  df-mnd 17607  df-grp 17738  df-minusg 17739  df-sbg 17740  df-subg 17901  df-cmn 18507  df-mgp 18803  df-ur 18815  df-ring 18862  df-cring 18863  df-subrg 19093  df-lmod 19180  df-lss 19248  df-sra 19492  df-rgmod 19493  df-lidl 19494  df-cnfld 20066  df-zring 20138
This theorem is referenced by:  zringlpir  20156
  Copyright terms: Public domain W3C validator