Proof of Theorem zringlpirlem3
| Step | Hyp | Ref
| Expression |
| 1 | | zringlpirlem.i |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈
(LIdeal‘ℤring)) |
| 2 | | zringbas 21464 |
. . . . . . . . . 10
⊢ ℤ =
(Base‘ℤring) |
| 3 | | eqid 2737 |
. . . . . . . . . 10
⊢
(LIdeal‘ℤring) =
(LIdeal‘ℤring) |
| 4 | 2, 3 | lidlss 21222 |
. . . . . . . . 9
⊢ (𝐼 ∈
(LIdeal‘ℤring) → 𝐼 ⊆ ℤ) |
| 5 | 1, 4 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ⊆ ℤ) |
| 6 | | zringlpirlem.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝐼) |
| 7 | 5, 6 | sseldd 3984 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ ℤ) |
| 8 | 7 | zred 12722 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 9 | | zringlpirlem.g |
. . . . . . . . 9
⊢ 𝐺 = inf((𝐼 ∩ ℕ), ℝ, <
) |
| 10 | | inss2 4238 |
. . . . . . . . . . 11
⊢ (𝐼 ∩ ℕ) ⊆
ℕ |
| 11 | | nnuz 12921 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
| 12 | 10, 11 | sseqtri 4032 |
. . . . . . . . . 10
⊢ (𝐼 ∩ ℕ) ⊆
(ℤ≥‘1) |
| 13 | | zringlpirlem.n0 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ≠ {0}) |
| 14 | 1, 13 | zringlpirlem1 21473 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐼 ∩ ℕ) ≠
∅) |
| 15 | | infssuzcl 12974 |
. . . . . . . . . 10
⊢ (((𝐼 ∩ ℕ) ⊆
(ℤ≥‘1) ∧ (𝐼 ∩ ℕ) ≠ ∅) →
inf((𝐼 ∩ ℕ),
ℝ, < ) ∈ (𝐼
∩ ℕ)) |
| 16 | 12, 14, 15 | sylancr 587 |
. . . . . . . . 9
⊢ (𝜑 → inf((𝐼 ∩ ℕ), ℝ, < ) ∈
(𝐼 ∩
ℕ)) |
| 17 | 9, 16 | eqeltrid 2845 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ (𝐼 ∩ ℕ)) |
| 18 | 17 | elin2d 4205 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ ℕ) |
| 19 | 18 | nnrpd 13075 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈
ℝ+) |
| 20 | | modlt 13920 |
. . . . . 6
⊢ ((𝑋 ∈ ℝ ∧ 𝐺 ∈ ℝ+)
→ (𝑋 mod 𝐺) < 𝐺) |
| 21 | 8, 19, 20 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑋 mod 𝐺) < 𝐺) |
| 22 | 7, 18 | zmodcld 13932 |
. . . . . . 7
⊢ (𝜑 → (𝑋 mod 𝐺) ∈
ℕ0) |
| 23 | 22 | nn0red 12588 |
. . . . . 6
⊢ (𝜑 → (𝑋 mod 𝐺) ∈ ℝ) |
| 24 | 18 | nnred 12281 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ ℝ) |
| 25 | 23, 24 | ltnled 11408 |
. . . . 5
⊢ (𝜑 → ((𝑋 mod 𝐺) < 𝐺 ↔ ¬ 𝐺 ≤ (𝑋 mod 𝐺))) |
| 26 | 21, 25 | mpbid 232 |
. . . 4
⊢ (𝜑 → ¬ 𝐺 ≤ (𝑋 mod 𝐺)) |
| 27 | 7 | zcnd 12723 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ ℂ) |
| 28 | 18 | nncnd 12282 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ∈ ℂ) |
| 29 | 8, 18 | nndivred 12320 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 / 𝐺) ∈ ℝ) |
| 30 | 29 | flcld 13838 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (⌊‘(𝑋 / 𝐺)) ∈ ℤ) |
| 31 | 30 | zcnd 12723 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⌊‘(𝑋 / 𝐺)) ∈ ℂ) |
| 32 | 28, 31 | mulcld 11281 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 · (⌊‘(𝑋 / 𝐺))) ∈ ℂ) |
| 33 | 27, 32 | negsubd 11626 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 + -(𝐺 · (⌊‘(𝑋 / 𝐺)))) = (𝑋 − (𝐺 · (⌊‘(𝑋 / 𝐺))))) |
| 34 | 30 | znegcld 12724 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → -(⌊‘(𝑋 / 𝐺)) ∈ ℤ) |
| 35 | 34 | zcnd 12723 |
. . . . . . . . . . . . 13
⊢ (𝜑 → -(⌊‘(𝑋 / 𝐺)) ∈ ℂ) |
| 36 | 35, 28 | mulcomd 11282 |
. . . . . . . . . . . 12
⊢ (𝜑 → (-(⌊‘(𝑋 / 𝐺)) · 𝐺) = (𝐺 · -(⌊‘(𝑋 / 𝐺)))) |
| 37 | 28, 31 | mulneg2d 11717 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 · -(⌊‘(𝑋 / 𝐺))) = -(𝐺 · (⌊‘(𝑋 / 𝐺)))) |
| 38 | 36, 37 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝜑 → (-(⌊‘(𝑋 / 𝐺)) · 𝐺) = -(𝐺 · (⌊‘(𝑋 / 𝐺)))) |
| 39 | 38 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 + (-(⌊‘(𝑋 / 𝐺)) · 𝐺)) = (𝑋 + -(𝐺 · (⌊‘(𝑋 / 𝐺))))) |
| 40 | | modval 13911 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ℝ ∧ 𝐺 ∈ ℝ+)
→ (𝑋 mod 𝐺) = (𝑋 − (𝐺 · (⌊‘(𝑋 / 𝐺))))) |
| 41 | 8, 19, 40 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 mod 𝐺) = (𝑋 − (𝐺 · (⌊‘(𝑋 / 𝐺))))) |
| 42 | 33, 39, 41 | 3eqtr4rd 2788 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 mod 𝐺) = (𝑋 + (-(⌊‘(𝑋 / 𝐺)) · 𝐺))) |
| 43 | | zringring 21460 |
. . . . . . . . . . 11
⊢
ℤring ∈ Ring |
| 44 | 43 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℤring
∈ Ring) |
| 45 | 1, 13, 9 | zringlpirlem2 21474 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ 𝐼) |
| 46 | | zringmulr 21468 |
. . . . . . . . . . . 12
⊢ ·
= (.r‘ℤring) |
| 47 | 3, 2, 46 | lidlmcl 21235 |
. . . . . . . . . . 11
⊢
(((ℤring ∈ Ring ∧ 𝐼 ∈
(LIdeal‘ℤring)) ∧ (-(⌊‘(𝑋 / 𝐺)) ∈ ℤ ∧ 𝐺 ∈ 𝐼)) → (-(⌊‘(𝑋 / 𝐺)) · 𝐺) ∈ 𝐼) |
| 48 | 44, 1, 34, 45, 47 | syl22anc 839 |
. . . . . . . . . 10
⊢ (𝜑 → (-(⌊‘(𝑋 / 𝐺)) · 𝐺) ∈ 𝐼) |
| 49 | | zringplusg 21465 |
. . . . . . . . . . 11
⊢ + =
(+g‘ℤring) |
| 50 | 3, 49 | lidlacl 21231 |
. . . . . . . . . 10
⊢
(((ℤring ∈ Ring ∧ 𝐼 ∈
(LIdeal‘ℤring)) ∧ (𝑋 ∈ 𝐼 ∧ (-(⌊‘(𝑋 / 𝐺)) · 𝐺) ∈ 𝐼)) → (𝑋 + (-(⌊‘(𝑋 / 𝐺)) · 𝐺)) ∈ 𝐼) |
| 51 | 44, 1, 6, 48, 50 | syl22anc 839 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 + (-(⌊‘(𝑋 / 𝐺)) · 𝐺)) ∈ 𝐼) |
| 52 | 42, 51 | eqeltrd 2841 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 mod 𝐺) ∈ 𝐼) |
| 53 | 52 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 mod 𝐺) ∈ ℕ) → (𝑋 mod 𝐺) ∈ 𝐼) |
| 54 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 mod 𝐺) ∈ ℕ) → (𝑋 mod 𝐺) ∈ ℕ) |
| 55 | 53, 54 | elind 4200 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 mod 𝐺) ∈ ℕ) → (𝑋 mod 𝐺) ∈ (𝐼 ∩ ℕ)) |
| 56 | | infssuzle 12973 |
. . . . . 6
⊢ (((𝐼 ∩ ℕ) ⊆
(ℤ≥‘1) ∧ (𝑋 mod 𝐺) ∈ (𝐼 ∩ ℕ)) → inf((𝐼 ∩ ℕ), ℝ, < )
≤ (𝑋 mod 𝐺)) |
| 57 | 12, 55, 56 | sylancr 587 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 mod 𝐺) ∈ ℕ) → inf((𝐼 ∩ ℕ), ℝ, < )
≤ (𝑋 mod 𝐺)) |
| 58 | 9, 57 | eqbrtrid 5178 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 mod 𝐺) ∈ ℕ) → 𝐺 ≤ (𝑋 mod 𝐺)) |
| 59 | 26, 58 | mtand 816 |
. . 3
⊢ (𝜑 → ¬ (𝑋 mod 𝐺) ∈ ℕ) |
| 60 | | elnn0 12528 |
. . . 4
⊢ ((𝑋 mod 𝐺) ∈ ℕ0 ↔ ((𝑋 mod 𝐺) ∈ ℕ ∨ (𝑋 mod 𝐺) = 0)) |
| 61 | 22, 60 | sylib 218 |
. . 3
⊢ (𝜑 → ((𝑋 mod 𝐺) ∈ ℕ ∨ (𝑋 mod 𝐺) = 0)) |
| 62 | | orel1 889 |
. . 3
⊢ (¬
(𝑋 mod 𝐺) ∈ ℕ → (((𝑋 mod 𝐺) ∈ ℕ ∨ (𝑋 mod 𝐺) = 0) → (𝑋 mod 𝐺) = 0)) |
| 63 | 59, 61, 62 | sylc 65 |
. 2
⊢ (𝜑 → (𝑋 mod 𝐺) = 0) |
| 64 | | dvdsval3 16294 |
. . 3
⊢ ((𝐺 ∈ ℕ ∧ 𝑋 ∈ ℤ) → (𝐺 ∥ 𝑋 ↔ (𝑋 mod 𝐺) = 0)) |
| 65 | 18, 7, 64 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝐺 ∥ 𝑋 ↔ (𝑋 mod 𝐺) = 0)) |
| 66 | 63, 65 | mpbird 257 |
1
⊢ (𝜑 → 𝐺 ∥ 𝑋) |