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

Metamath Proof Explorer

Theorem zncrng

Description: Z/nZ is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypothesis zncrng.y ⊢ Y = ℤ/Nℤ
Assertion zncrng ⊢ N ∈ ℕ 0 → Y ∈ CRing

Proof

Step Hyp Ref Expression
1 zncrng.y ⊢ Y = ℤ/Nℤ
2 nn0z ⊢ N ∈ ℕ 0 → N ∈ ℤ
3 eqid ⊢ RSpan ⁡ ℤ ring = RSpan ⁡ ℤ ring
4 eqid ⊢ ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N = ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N
5 3 4 zncrng2 ⊢ N ∈ ℤ → ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N ∈ CRing
6 2 5 syl ⊢ N ∈ ℕ 0 → ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N ∈ CRing
7 eqidd ⊢ N ∈ ℕ 0 → Base ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N = Base ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N
8 3 4 1 znbas2 ⊢ N ∈ ℕ 0 → Base ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N = Base Y
9 3 4 1 znadd ⊢ N ∈ ℕ 0 → + ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N = + Y
10 9 oveqdr ⊢ N ∈ ℕ 0 ∧ x ∈ Base ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N ∧ y ∈ Base ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N → x + ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N y = x + Y y
11 3 4 1 znmul ⊢ N ∈ ℕ 0 → ⋅ ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N = ⋅ Y
12 11 oveqdr ⊢ N ∈ ℕ 0 ∧ x ∈ Base ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N ∧ y ∈ Base ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N → x ⋅ ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N y = x ⋅ Y y
13 7 8 10 12 crngpropd ⊢ N ∈ ℕ 0 → ℤ ring / 𝑠 ℤ ring ~ QG RSpan ⁡ ℤ ring ⁡ N ∈ CRing ↔ Y ∈ CRing
14 6 13 mpbid ⊢ N ∈ ℕ 0 → Y ∈ CRing