This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 𝐺 ) ∈ ℕ0 )
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 𝐺 ) ∈ ℕ0 ↔ ( ( 𝑋 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 ⊢ ( 𝜑 → 𝐺 ∥ 𝑋 )