Theorem zringlpirlem3 21410

Description: Lemma for zringlpir 21413. 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

Step	Hyp	Ref	Expression
1		zringlpirlem.i	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘ℤring))
2		zringbas 21399	. . . . . . . . . 10 ⊢ ℤ = (Base‘ℤring)
3		eqid 2734	. . . . . . . . . 10 ⊢ (LIdeal‘ℤring) = (LIdeal‘ℤring)
4	2, 3	lidlss 21158	. . . . . . . . 9 ⊢ (𝐼 ∈ (LIdeal‘ℤring) → 𝐼 ⊆ ℤ)
5	1, 4	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ⊆ ℤ)
6		zringlpirlem.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝐼)
7	5, 6	sseldd 3957	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ℤ)
8	7	zred 12689	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ℝ)
9		zringlpirlem.g	. . . . . . . . 9 ⊢ 𝐺 = inf((𝐼 ∩ ℕ), ℝ, < )
10		inss2 4211	. . . . . . . . . . 11 ⊢ (𝐼 ∩ ℕ) ⊆ ℕ
11		nnuz 12887	. . . . . . . . . . 11 ⊢ ℕ = (ℤ≥‘1)
12	10, 11	sseqtri 4005	. . . . . . . . . 10 ⊢ (𝐼 ∩ ℕ) ⊆ (ℤ≥‘1)
13		zringlpirlem.n0	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ≠ {0})
14	1, 13	zringlpirlem1 21408	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼 ∩ ℕ) ≠ ∅)
15		infssuzcl 12940	. . . . . . . . . 10 ⊢ (((𝐼 ∩ ℕ) ⊆ (ℤ≥‘1) ∧ (𝐼 ∩ ℕ) ≠ ∅) → inf((𝐼 ∩ ℕ), ℝ, < ) ∈ (𝐼 ∩ ℕ))
16	12, 14, 15	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → inf((𝐼 ∩ ℕ), ℝ, < ) ∈ (𝐼 ∩ ℕ))
17	9, 16	eqeltrid 2837	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (𝐼 ∩ ℕ))
18	17	elin2d 4178	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ ℕ)
19	18	nnrpd 13041	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ ℝ+)
20		modlt 13886	. . . . . 6 ⊢ ((𝑋 ∈ ℝ ∧ 𝐺 ∈ ℝ+) → (𝑋 mod 𝐺) < 𝐺)
21	8, 19, 20	syl2anc 584	. . . . 5 ⊢ (𝜑 → (𝑋 mod 𝐺) < 𝐺)
22	7, 18	zmodcld 13898	. . . . . . 7 ⊢ (𝜑 → (𝑋 mod 𝐺) ∈ ℕ0)
23	22	nn0red 12555	. . . . . 6 ⊢ (𝜑 → (𝑋 mod 𝐺) ∈ ℝ)
24	18	nnred 12247	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ ℝ)
25	23, 24	ltnled 11374	. . . . 5 ⊢ (𝜑 → ((𝑋 mod 𝐺) < 𝐺 ↔ ¬ 𝐺 ≤ (𝑋 mod 𝐺)))
26	21, 25	mpbid 232	. . . 4 ⊢ (𝜑 → ¬ 𝐺 ≤ (𝑋 mod 𝐺))
27	7	zcnd 12690	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ ℂ)
28	18	nncnd 12248	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 ∈ ℂ)
29	8, 18	nndivred 12286	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 / 𝐺) ∈ ℝ)
30	29	flcld 13804	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⌊‘(𝑋 / 𝐺)) ∈ ℤ)
31	30	zcnd 12690	. . . . . . . . . . . 12 ⊢ (𝜑 → (⌊‘(𝑋 / 𝐺)) ∈ ℂ)
32	28, 31	mulcld 11247	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 · (⌊‘(𝑋 / 𝐺))) ∈ ℂ)
33	27, 32	negsubd 11592	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 + -(𝐺 · (⌊‘(𝑋 / 𝐺)))) = (𝑋 − (𝐺 · (⌊‘(𝑋 / 𝐺)))))
34	30	znegcld 12691	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -(⌊‘(𝑋 / 𝐺)) ∈ ℤ)
35	34	zcnd 12690	. . . . . . . . . . . . 13 ⊢ (𝜑 → -(⌊‘(𝑋 / 𝐺)) ∈ ℂ)
36	35, 28	mulcomd 11248	. . . . . . . . . . . 12 ⊢ (𝜑 → (-(⌊‘(𝑋 / 𝐺)) · 𝐺) = (𝐺 · -(⌊‘(𝑋 / 𝐺))))
37	28, 31	mulneg2d 11683	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 · -(⌊‘(𝑋 / 𝐺))) = -(𝐺 · (⌊‘(𝑋 / 𝐺))))
38	36, 37	eqtrd 2769	. . . . . . . . . . 11 ⊢ (𝜑 → (-(⌊‘(𝑋 / 𝐺)) · 𝐺) = -(𝐺 · (⌊‘(𝑋 / 𝐺))))
39	38	oveq2d 7415	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 + (-(⌊‘(𝑋 / 𝐺)) · 𝐺)) = (𝑋 + -(𝐺 · (⌊‘(𝑋 / 𝐺)))))
40		modval 13877	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℝ ∧ 𝐺 ∈ ℝ+) → (𝑋 mod 𝐺) = (𝑋 − (𝐺 · (⌊‘(𝑋 / 𝐺)))))
41	8, 19, 40	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 mod 𝐺) = (𝑋 − (𝐺 · (⌊‘(𝑋 / 𝐺)))))
42	33, 39, 41	3eqtr4rd 2780	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 mod 𝐺) = (𝑋 + (-(⌊‘(𝑋 / 𝐺)) · 𝐺)))
43		zringring 21395	. . . . . . . . . . 11 ⊢ ℤring ∈ Ring
44	43	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℤring ∈ Ring)
45	1, 13, 9	zringlpirlem2 21409	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ 𝐼)
46		zringmulr 21403	. . . . . . . . . . . 12 ⊢ · = (.r‘ℤring)
47	3, 2, 46	lidlmcl 21171	. . . . . . . . . . 11 ⊢ (((ℤring ∈ Ring ∧ 𝐼 ∈ (LIdeal‘ℤring)) ∧ (-(⌊‘(𝑋 / 𝐺)) ∈ ℤ ∧ 𝐺 ∈ 𝐼)) → (-(⌊‘(𝑋 / 𝐺)) · 𝐺) ∈ 𝐼)
48	44, 1, 34, 45, 47	syl22anc 838	. . . . . . . . . 10 ⊢ (𝜑 → (-(⌊‘(𝑋 / 𝐺)) · 𝐺) ∈ 𝐼)
49		zringplusg 21400	. . . . . . . . . . 11 ⊢ + = (+g‘ℤring)
50	3, 49	lidlacl 21167	. . . . . . . . . 10 ⊢ (((ℤring ∈ Ring ∧ 𝐼 ∈ (LIdeal‘ℤring)) ∧ (𝑋 ∈ 𝐼 ∧ (-(⌊‘(𝑋 / 𝐺)) · 𝐺) ∈ 𝐼)) → (𝑋 + (-(⌊‘(𝑋 / 𝐺)) · 𝐺)) ∈ 𝐼)
51	44, 1, 6, 48, 50	syl22anc 838	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 + (-(⌊‘(𝑋 / 𝐺)) · 𝐺)) ∈ 𝐼)
52	42, 51	eqeltrd 2833	. . . . . . . 8 ⊢ (𝜑 → (𝑋 mod 𝐺) ∈ 𝐼)
53	52	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 mod 𝐺) ∈ ℕ) → (𝑋 mod 𝐺) ∈ 𝐼)
54		simpr 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 mod 𝐺) ∈ ℕ) → (𝑋 mod 𝐺) ∈ ℕ)
55	53, 54	elind 4173	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 mod 𝐺) ∈ ℕ) → (𝑋 mod 𝐺) ∈ (𝐼 ∩ ℕ))
56		infssuzle 12939	. . . . . 6 ⊢ (((𝐼 ∩ ℕ) ⊆ (ℤ≥‘1) ∧ (𝑋 mod 𝐺) ∈ (𝐼 ∩ ℕ)) → inf((𝐼 ∩ ℕ), ℝ, < ) ≤ (𝑋 mod 𝐺))
57	12, 55, 56	sylancr 587	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 mod 𝐺) ∈ ℕ) → inf((𝐼 ∩ ℕ), ℝ, < ) ≤ (𝑋 mod 𝐺))
58	9, 57	eqbrtrid 5151	. . . 4 ⊢ ((𝜑 ∧ (𝑋 mod 𝐺) ∈ ℕ) → 𝐺 ≤ (𝑋 mod 𝐺))
59	26, 58	mtand 815	. . 3 ⊢ (𝜑 → ¬ (𝑋 mod 𝐺) ∈ ℕ)
60		elnn0 12495	. . . 4 ⊢ ((𝑋 mod 𝐺) ∈ ℕ0 ↔ ((𝑋 mod 𝐺) ∈ ℕ ∨ (𝑋 mod 𝐺) = 0))
61	22, 60	sylib 218	. . 3 ⊢ (𝜑 → ((𝑋 mod 𝐺) ∈ ℕ ∨ (𝑋 mod 𝐺) = 0))
62		orel1 888	. . 3 ⊢ (¬ (𝑋 mod 𝐺) ∈ ℕ → (((𝑋 mod 𝐺) ∈ ℕ ∨ (𝑋 mod 𝐺) = 0) → (𝑋 mod 𝐺) = 0))
63	59, 61, 62	sylc 65	. 2 ⊢ (𝜑 → (𝑋 mod 𝐺) = 0)
64		dvdsval3 16261	. . 3 ⊢ ((𝐺 ∈ ℕ ∧ 𝑋 ∈ ℤ) → (𝐺 ∥ 𝑋 ↔ (𝑋 mod 𝐺) = 0))
65	18, 7, 64	syl2anc 584	. 2 ⊢ (𝜑 → (𝐺 ∥ 𝑋 ↔ (𝑋 mod 𝐺) = 0))
66	63, 65	mpbird 257	1 ⊢ (𝜑 → 𝐺 ∥ 𝑋)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1539   ∈ wcel 2107   ≠ wne 2931   ∩ cin 3923   ⊆ wss 3924  ∅c0 4306  {csn 4599   class class class wbr 5116  ‘cfv 6527  (class class class)co 7399  infcinf 9447  ℝcr 11120  0cc0 11121  1c1 11122   + caddc 11124   · cmul 11126   < clt 11261   ≤ cle 11262   − cmin 11458  -cneg 11459   / cdiv 11886  ℕcn 12232  ℕ₀cn0 12493  ℤcz 12580  ℤ_≥cuz 12844  ℝ⁺crp 13000  ⌊cfl 13796   mod cmo 13875   ∥ cdvds 16257  Ringcrg 20178  LIdealclidl 21152  ℤ_ringczring 21392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5246  ax-sep 5263  ax-nul 5273  ax-pow 5332  ax-pr 5399  ax-un 7723  ax-cnex 11177  ax-resscn 11178  ax-1cn 11179  ax-icn 11180  ax-addcl 11181  ax-addrcl 11182  ax-mulcl 11183  ax-mulrcl 11184  ax-mulcom 11185  ax-addass 11186  ax-mulass 11187  ax-distr 11188  ax-i2m1 11189  ax-1ne0 11190  ax-1rid 11191  ax-rnegex 11192  ax-rrecex 11193  ax-cnre 11194  ax-pre-lttri 11195  ax-pre-lttrn 11196  ax-pre-ltadd 11197  ax-pre-mulgt0 11198  ax-pre-sup 11199  ax-addf 11200  ax-mulf 11201

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3357  df-reu 3358  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-pss 3944  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-tp 4604  df-op 4606  df-uni 4881  df-iun 4966  df-br 5117  df-opab 5179  df-mpt 5199  df-tr 5227  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6287  df-ord 6352  df-on 6353  df-lim 6354  df-suc 6355  df-iota 6480  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-riota 7356  df-ov 7402  df-oprab 7403  df-mpo 7404  df-om 7856  df-1st 7982  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8379  df-rdg 8418  df-1o 8474  df-er 8713  df-en 8954  df-dom 8955  df-sdom 8956  df-fin 8957  df-sup 9448  df-inf 9449  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-sub 11460  df-neg 11461  df-div 11887  df-nn 12233  df-2 12295  df-3 12296  df-4 12297  df-5 12298  df-6 12299  df-7 12300  df-8 12301  df-9 12302  df-n0 12494  df-z 12581  df-dec 12701  df-uz 12845  df-rp 13001  df-fz 13514  df-fl 13798  df-mod 13876  df-seq 14009  df-exp 14069  df-cj 15105  df-re 15106  df-im 15107  df-sqrt 15241  df-abs 15242  df-dvds 16258  df-struct 17151  df-sets 17168  df-slot 17186  df-ndx 17198  df-base 17214  df-ress 17237  df-plusg 17269  df-mulr 17270  df-starv 17271  df-sca 17272  df-vsca 17273  df-ip 17274  df-tset 17275  df-ple 17276  df-ds 17278  df-unif 17279  df-0g 17440  df-mgm 18603  df-sgrp 18682  df-mnd 18698  df-grp 18904  df-minusg 18905  df-sbg 18906  df-subg 19091  df-cmn 19748  df-abl 19749  df-mgp 20086  df-rng 20098  df-ur 20127  df-ring 20180  df-cring 20181  df-subrng 20491  df-subrg 20515  df-lmod 20804  df-lss 20874  df-sra 21116  df-rgmod 21117  df-lidl 21154  df-cnfld 21301  df-zring 21393

This theorem is referenced by:  zringlpir  21413