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	$⊢ φ \to I \in LIdeal (ℤ_{ring})$
	zringlpirlem.n0	$⊢ φ \to I \neq \{0\}$
	zringlpirlem.g	$⊢ G = sup (I \cap ℕ ℝ <)$
	zringlpirlem.x	$⊢ φ \to X \in I$
Assertion	zringlpirlem3	$⊢ φ \to G ∥ X$

Proof

Step	Hyp	Ref	Expression
1		zringlpirlem.i	$⊢ φ \to I \in LIdeal (ℤ_{ring})$
2		zringlpirlem.n0	$⊢ φ \to I \neq \{0\}$
3		zringlpirlem.g	$⊢ G = sup (I \cap ℕ ℝ <)$
4		zringlpirlem.x	$⊢ φ \to X \in I$
5		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
6		eqid	$⊢ LIdeal (ℤ_{ring}) = LIdeal (ℤ_{ring})$
7	5 6	lidlss	$⊢ I \in LIdeal (ℤ_{ring}) \to I \subseteq ℤ$
8	1 7	syl	$⊢ φ \to I \subseteq ℤ$
9	8 4	sseldd	$⊢ φ \to X \in ℤ$
10	9	zred	$⊢ φ \to X \in ℝ$
11		inss2	$⊢ I \cap ℕ \subseteq ℕ$
12		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
13	11 12	sseqtri	$⊢ I \cap ℕ \subseteq ℤ_{\geq 1}$
14	1 2	zringlpirlem1	$⊢ φ \to I \cap ℕ \neq \emptyset$
15		infssuzcl	$⊢ (I \cap ℕ \subseteq ℤ_{\geq 1} \land I \cap ℕ \neq \emptyset) \to sup (I \cap ℕ ℝ <) \in (I \cap ℕ)$
16	13 14 15	sylancr	$⊢ φ \to sup (I \cap ℕ ℝ <) \in (I \cap ℕ)$
17	3 16	eqeltrid	$⊢ φ \to G \in (I \cap ℕ)$
18	17	elin2d	$⊢ φ \to G \in ℕ$
19	18	nnrpd	$⊢ φ \to G \in ℝ^{+}$
20		modlt	$⊢ (X \in ℝ \land G \in ℝ^{+}) \to X \mod G < G$
21	10 19 20	syl2anc	$⊢ φ \to X \mod G < G$
22	9 18	zmodcld	$⊢ φ \to X \mod G \in ℕ_{0}$
23	22	nn0red	$⊢ φ \to X \mod G \in ℝ$
24	18	nnred	$⊢ φ \to G \in ℝ$
25	23 24	ltnled	$⊢ φ \to (X \mod G < G \leftrightarrow \neg G \leq X \mod G)$
26	21 25	mpbid	$⊢ φ \to \neg G \leq X \mod G$
27	9	zcnd	$⊢ φ \to X \in ℂ$
28	18	nncnd	$⊢ φ \to G \in ℂ$
29	10 18	nndivred	$⊢ φ \to \frac{X}{G} \in ℝ$
30	29	flcld	$⊢ φ \to ⌊\frac{X}{G}⌋ \in ℤ$
31	30	zcnd	$⊢ φ \to ⌊\frac{X}{G}⌋ \in ℂ$
32	28 31	mulcld	$⊢ φ \to G ⌊\frac{X}{G}⌋ \in ℂ$
33	27 32	negsubd	$⊢ φ \to X + (- G ⌊\frac{X}{G}⌋) = X - G ⌊\frac{X}{G}⌋$
34	30	znegcld	$⊢ φ \to - ⌊\frac{X}{G}⌋ \in ℤ$
35	34	zcnd	$⊢ φ \to - ⌊\frac{X}{G}⌋ \in ℂ$
36	35 28	mulcomd	$⊢ φ \to (- ⌊\frac{X}{G}⌋) G = G (- ⌊\frac{X}{G}⌋)$
37	28 31	mulneg2d	$⊢ φ \to G (- ⌊\frac{X}{G}⌋) = - G ⌊\frac{X}{G}⌋$
38	36 37	eqtrd	$⊢ φ \to (- ⌊\frac{X}{G}⌋) G = - G ⌊\frac{X}{G}⌋$
39	38	oveq2d	$⊢ φ \to X + (- ⌊\frac{X}{G}⌋) G = X + (- G ⌊\frac{X}{G}⌋)$
40		modval	$⊢ (X \in ℝ \land G \in ℝ^{+}) \to X \mod G = X - G ⌊\frac{X}{G}⌋$
41	10 19 40	syl2anc	$⊢ φ \to X \mod G = X - G ⌊\frac{X}{G}⌋$
42	33 39 41	3eqtr4rd	$⊢ φ \to X \mod G = X + (- ⌊\frac{X}{G}⌋) G$
43		zringring	$⊢ ℤ_{ring} \in Ring$
44	43	a1i	$⊢ φ \to ℤ_{ring} \in Ring$
45	1 2 3	zringlpirlem2	$⊢ φ \to G \in I$
46		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
47	6 5 46	lidlmcl	$⊢ ((ℤ_{ring} \in Ring \land I \in LIdeal (ℤ_{ring})) \land (- ⌊\frac{X}{G}⌋ \in ℤ \land G \in I)) \to (- ⌊\frac{X}{G}⌋) G \in I$
48	44 1 34 45 47	syl22anc	$⊢ φ \to (- ⌊\frac{X}{G}⌋) G \in I$
49		zringplusg	$⊢ + = +_{ℤ_{ring}}$
50	6 49	lidlacl	$⊢ ((ℤ_{ring} \in Ring \land I \in LIdeal (ℤ_{ring})) \land (X \in I \land (- ⌊\frac{X}{G}⌋) G \in I)) \to X + (- ⌊\frac{X}{G}⌋) G \in I$
51	44 1 4 48 50	syl22anc	$⊢ φ \to X + (- ⌊\frac{X}{G}⌋) G \in I$
52	42 51	eqeltrd	$⊢ φ \to X \mod G \in I$
53	52	adantr	$⊢ (φ \land X \mod G \in ℕ) \to X \mod G \in I$
54		simpr	$⊢ (φ \land X \mod G \in ℕ) \to X \mod G \in ℕ$
55	53 54	elind	$⊢ (φ \land X \mod G \in ℕ) \to X \mod G \in (I \cap ℕ)$
56		infssuzle	$⊢ (I \cap ℕ \subseteq ℤ_{\geq 1} \land X \mod G \in (I \cap ℕ)) \to sup (I \cap ℕ ℝ <) \leq X \mod G$
57	13 55 56	sylancr	$⊢ (φ \land X \mod G \in ℕ) \to sup (I \cap ℕ ℝ <) \leq X \mod G$
58	3 57	eqbrtrid	$⊢ (φ \land X \mod G \in ℕ) \to G \leq X \mod G$
59	26 58	mtand	$⊢ φ \to \neg X \mod G \in ℕ$
60		elnn0	$⊢ X \mod G \in ℕ_{0} \leftrightarrow (X \mod G \in ℕ \lor X \mod G = 0)$
61	22 60	sylib	$⊢ φ \to (X \mod G \in ℕ \lor X \mod G = 0)$
62		orel1	$⊢ \neg X \mod G \in ℕ \to ((X \mod G \in ℕ \lor X \mod G = 0) \to X \mod G = 0)$
63	59 61 62	sylc	$⊢ φ \to X \mod G = 0$
64		dvdsval3	$⊢ (G \in ℕ \land X \in ℤ) \to (G ∥ X \leftrightarrow X \mod G = 0)$
65	18 9 64	syl2anc	$⊢ φ \to (G ∥ X \leftrightarrow X \mod G = 0)$
66	63 65	mpbird	$⊢ φ \to G ∥ X$

Metamath Proof Explorer

Theorem zringlpirlem3

Proof