zringlpirlem3

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

	Ref	Expression
Hypotheses	zringlpirlem.i	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ ℤ_ring ) )
	zringlpirlem.n0	⊢ ( 𝜑 → 𝐼 ≠ { 0 } )
	zringlpirlem.g	⊢ 𝐺 = inf ( ( 𝐼 ∩ ℕ ) , ℝ , < )
	zringlpirlem.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
Assertion	zringlpirlem3	⊢ ( 𝜑 → 𝐺 ∥ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		zringlpirlem.i	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ ℤ_ring ) )
2		zringlpirlem.n0	⊢ ( 𝜑 → 𝐼 ≠ { 0 } )
3		zringlpirlem.g	⊢ 𝐺 = inf ( ( 𝐼 ∩ ℕ ) , ℝ , < )
4		zringlpirlem.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
5		zringbas	⊢ ℤ = ( Base ‘ ℤ_ring )
6		eqid	⊢ ( LIdeal ‘ ℤ_ring ) = ( LIdeal ‘ ℤ_ring )
7	5 6	lidlss	⊢ ( 𝐼 ∈ ( LIdeal ‘ ℤ_ring ) → 𝐼 ⊆ ℤ )
8	1 7	syl	⊢ ( 𝜑 → 𝐼 ⊆ ℤ )
9	8 4	sseldd	⊢ ( 𝜑 → 𝑋 ∈ ℤ )
10	9	zred	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
11		inss2	⊢ ( 𝐼 ∩ ℕ ) ⊆ ℕ
12		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
13	11 12	sseqtri	⊢ ( 𝐼 ∩ ℕ ) ⊆ ( ℤ_≥ ‘ 1 )
14	1 2	zringlpirlem1	⊢ ( 𝜑 → ( 𝐼 ∩ ℕ ) ≠ ∅ )
15		infssuzcl	⊢ ( ( ( 𝐼 ∩ ℕ ) ⊆ ( ℤ_≥ ‘ 1 ) ∧ ( 𝐼 ∩ ℕ ) ≠ ∅ ) → inf ( ( 𝐼 ∩ ℕ ) , ℝ , < ) ∈ ( 𝐼 ∩ ℕ ) )
16	13 14 15	sylancr	⊢ ( 𝜑 → inf ( ( 𝐼 ∩ ℕ ) , ℝ , < ) ∈ ( 𝐼 ∩ ℕ ) )
17	3 16	eqeltrid	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐼 ∩ ℕ ) )
18	17	elin2d	⊢ ( 𝜑 → 𝐺 ∈ ℕ )
19	18	nnrpd	⊢ ( 𝜑 → 𝐺 ∈ ℝ⁺ )
20		modlt	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐺 ∈ ℝ⁺ ) → ( 𝑋 mod 𝐺 ) < 𝐺 )
21	10 19 20	syl2anc	⊢ ( 𝜑 → ( 𝑋 mod 𝐺 ) < 𝐺 )
22	9 18	zmodcld	⊢ ( 𝜑 → ( 𝑋 mod 𝐺 ) ∈ ℕ₀ )
23	22	nn0red	⊢ ( 𝜑 → ( 𝑋 mod 𝐺 ) ∈ ℝ )
24	18	nnred	⊢ ( 𝜑 → 𝐺 ∈ ℝ )
25	23 24	ltnled	⊢ ( 𝜑 → ( ( 𝑋 mod 𝐺 ) < 𝐺 ↔ ¬ 𝐺 ≤ ( 𝑋 mod 𝐺 ) ) )
26	21 25	mpbid	⊢ ( 𝜑 → ¬ 𝐺 ≤ ( 𝑋 mod 𝐺 ) )
27	9	zcnd	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
28	18	nncnd	⊢ ( 𝜑 → 𝐺 ∈ ℂ )
29	10 18	nndivred	⊢ ( 𝜑 → ( 𝑋 / 𝐺 ) ∈ ℝ )
30	29	flcld	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) ∈ ℤ )
31	30	zcnd	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) ∈ ℂ )
32	28 31	mulcld	⊢ ( 𝜑 → ( 𝐺 · ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) ) ∈ ℂ )
33	27 32	negsubd	⊢ ( 𝜑 → ( 𝑋 + - ( 𝐺 · ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) ) ) = ( 𝑋 − ( 𝐺 · ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) ) ) )
34	30	znegcld	⊢ ( 𝜑 → - ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) ∈ ℤ )
35	34	zcnd	⊢ ( 𝜑 → - ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) ∈ ℂ )
36	35 28	mulcomd	⊢ ( 𝜑 → ( - ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) · 𝐺 ) = ( 𝐺 · - ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) ) )
37	28 31	mulneg2d	⊢ ( 𝜑 → ( 𝐺 · - ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) ) = - ( 𝐺 · ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) ) )
38	36 37	eqtrd	⊢ ( 𝜑 → ( - ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) · 𝐺 ) = - ( 𝐺 · ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) ) )
39	38	oveq2d	⊢ ( 𝜑 → ( 𝑋 + ( - ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) · 𝐺 ) ) = ( 𝑋 + - ( 𝐺 · ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) ) ) )
40		modval	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐺 ∈ ℝ⁺ ) → ( 𝑋 mod 𝐺 ) = ( 𝑋 − ( 𝐺 · ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) ) ) )
41	10 19 40	syl2anc	⊢ ( 𝜑 → ( 𝑋 mod 𝐺 ) = ( 𝑋 − ( 𝐺 · ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) ) ) )
42	33 39 41	3eqtr4rd	⊢ ( 𝜑 → ( 𝑋 mod 𝐺 ) = ( 𝑋 + ( - ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) · 𝐺 ) ) )
43		zringring	⊢ ℤ_ring ∈ Ring
44	43	a1i	⊢ ( 𝜑 → ℤ_ring ∈ Ring )
45	1 2 3	zringlpirlem2	⊢ ( 𝜑 → 𝐺 ∈ 𝐼 )
46		zringmulr	⊢ · = ( ._r ‘ ℤ_ring )
47	6 5 46	lidlmcl	⊢ ( ( ( ℤ_ring ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ ℤ_ring ) ) ∧ ( - ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) ∈ ℤ ∧ 𝐺 ∈ 𝐼 ) ) → ( - ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) · 𝐺 ) ∈ 𝐼 )
48	44 1 34 45 47	syl22anc	⊢ ( 𝜑 → ( - ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) · 𝐺 ) ∈ 𝐼 )
49		zringplusg	⊢ + = ( +_g ‘ ℤ_ring )
50	6 49	lidlacl	⊢ ( ( ( ℤ_ring ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ ℤ_ring ) ) ∧ ( 𝑋 ∈ 𝐼 ∧ ( - ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) · 𝐺 ) ∈ 𝐼 ) ) → ( 𝑋 + ( - ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) · 𝐺 ) ) ∈ 𝐼 )
51	44 1 4 48 50	syl22anc	⊢ ( 𝜑 → ( 𝑋 + ( - ( ⌊ ‘ ( 𝑋 / 𝐺 ) ) · 𝐺 ) ) ∈ 𝐼 )
52	42 51	eqeltrd	⊢ ( 𝜑 → ( 𝑋 mod 𝐺 ) ∈ 𝐼 )
53	52	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 mod 𝐺 ) ∈ ℕ ) → ( 𝑋 mod 𝐺 ) ∈ 𝐼 )
54		simpr	⊢ ( ( 𝜑 ∧ ( 𝑋 mod 𝐺 ) ∈ ℕ ) → ( 𝑋 mod 𝐺 ) ∈ ℕ )
55	53 54	elind	⊢ ( ( 𝜑 ∧ ( 𝑋 mod 𝐺 ) ∈ ℕ ) → ( 𝑋 mod 𝐺 ) ∈ ( 𝐼 ∩ ℕ ) )
56		infssuzle	⊢ ( ( ( 𝐼 ∩ ℕ ) ⊆ ( ℤ_≥ ‘ 1 ) ∧ ( 𝑋 mod 𝐺 ) ∈ ( 𝐼 ∩ ℕ ) ) → inf ( ( 𝐼 ∩ ℕ ) , ℝ , < ) ≤ ( 𝑋 mod 𝐺 ) )
57	13 55 56	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑋 mod 𝐺 ) ∈ ℕ ) → inf ( ( 𝐼 ∩ ℕ ) , ℝ , < ) ≤ ( 𝑋 mod 𝐺 ) )
58	3 57	eqbrtrid	⊢ ( ( 𝜑 ∧ ( 𝑋 mod 𝐺 ) ∈ ℕ ) → 𝐺 ≤ ( 𝑋 mod 𝐺 ) )
59	26 58	mtand	⊢ ( 𝜑 → ¬ ( 𝑋 mod 𝐺 ) ∈ ℕ )
60		elnn0	⊢ ( ( 𝑋 mod 𝐺 ) ∈ ℕ₀ ↔ ( ( 𝑋 mod 𝐺 ) ∈ ℕ ∨ ( 𝑋 mod 𝐺 ) = 0 ) )
61	22 60	sylib	⊢ ( 𝜑 → ( ( 𝑋 mod 𝐺 ) ∈ ℕ ∨ ( 𝑋 mod 𝐺 ) = 0 ) )
62		orel1	⊢ ( ¬ ( 𝑋 mod 𝐺 ) ∈ ℕ → ( ( ( 𝑋 mod 𝐺 ) ∈ ℕ ∨ ( 𝑋 mod 𝐺 ) = 0 ) → ( 𝑋 mod 𝐺 ) = 0 ) )
63	59 61 62	sylc	⊢ ( 𝜑 → ( 𝑋 mod 𝐺 ) = 0 )
64		dvdsval3	⊢ ( ( 𝐺 ∈ ℕ ∧ 𝑋 ∈ ℤ ) → ( 𝐺 ∥ 𝑋 ↔ ( 𝑋 mod 𝐺 ) = 0 ) )
65	18 9 64	syl2anc	⊢ ( 𝜑 → ( 𝐺 ∥ 𝑋 ↔ ( 𝑋 mod 𝐺 ) = 0 ) )
66	63 65	mpbird	⊢ ( 𝜑 → 𝐺 ∥ 𝑋 )

Metamath Proof Explorer

Theorem zringlpirlem3

Proof