Proof of Theorem zlmodzxznm
Step | Hyp | Ref
| Expression |
1 | | 3prm 16147 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℙ |
2 | | 2prm 16145 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℙ |
3 | | ztprmneprm 45264 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ ℤ ∧ 3 ∈
ℙ ∧ 2 ∈ ℙ) → ((𝑖 · 3) = 2 → 3 =
2)) |
4 | 1, 2, 3 | mp3an23 1454 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℤ → ((𝑖 · 3) = 2 → 3 =
2)) |
5 | | 2re 11802 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ |
6 | | 2lt3 11900 |
. . . . . . . . . . . . . 14
⊢ 2 <
3 |
7 | 5, 6 | ltneii 10843 |
. . . . . . . . . . . . 13
⊢ 2 ≠
3 |
8 | | eqneqall 2946 |
. . . . . . . . . . . . 13
⊢ (2 = 3
→ (2 ≠ 3 → (𝑖
· 3) ≠ 2)) |
9 | 7, 8 | mpi 20 |
. . . . . . . . . . . 12
⊢ (2 = 3
→ (𝑖 · 3) ≠
2) |
10 | 9 | eqcoms 2747 |
. . . . . . . . . . 11
⊢ (3 = 2
→ (𝑖 · 3) ≠
2) |
11 | 4, 10 | syl6com 37 |
. . . . . . . . . 10
⊢ ((𝑖 · 3) = 2 → (𝑖 ∈ ℤ → (𝑖 · 3) ≠
2)) |
12 | | ax-1 6 |
. . . . . . . . . 10
⊢ ((𝑖 · 3) ≠ 2 →
(𝑖 ∈ ℤ →
(𝑖 · 3) ≠
2)) |
13 | 11, 12 | pm2.61ine 3018 |
. . . . . . . . 9
⊢ (𝑖 ∈ ℤ → (𝑖 · 3) ≠
2) |
14 | 13 | olcd 873 |
. . . . . . . 8
⊢ (𝑖 ∈ ℤ → (0 ≠ 0
∨ (𝑖 · 3) ≠
2)) |
15 | | c0ex 10725 |
. . . . . . . . . 10
⊢ 0 ∈
V |
16 | | ovex 7215 |
. . . . . . . . . 10
⊢ (𝑖 · 3) ∈
V |
17 | 15, 16 | pm3.2i 474 |
. . . . . . . . 9
⊢ (0 ∈
V ∧ (𝑖 · 3)
∈ V) |
18 | | opthneg 5349 |
. . . . . . . . 9
⊢ ((0
∈ V ∧ (𝑖 ·
3) ∈ V) → (〈0, (𝑖 · 3)〉 ≠ 〈0, 2〉
↔ (0 ≠ 0 ∨ (𝑖
· 3) ≠ 2))) |
19 | 17, 18 | mp1i 13 |
. . . . . . . 8
⊢ (𝑖 ∈ ℤ → (〈0,
(𝑖 · 3)〉 ≠
〈0, 2〉 ↔ (0 ≠ 0 ∨ (𝑖 · 3) ≠ 2))) |
20 | 14, 19 | mpbird 260 |
. . . . . . 7
⊢ (𝑖 ∈ ℤ → 〈0,
(𝑖 · 3)〉 ≠
〈0, 2〉) |
21 | | 0ne1 11799 |
. . . . . . . . . 10
⊢ 0 ≠
1 |
22 | 21 | a1i 11 |
. . . . . . . . 9
⊢ (𝑖 ∈ ℤ → 0 ≠
1) |
23 | 22 | orcd 872 |
. . . . . . . 8
⊢ (𝑖 ∈ ℤ → (0 ≠ 1
∨ (𝑖 · 3) ≠
4)) |
24 | | opthneg 5349 |
. . . . . . . . 9
⊢ ((0
∈ V ∧ (𝑖 ·
3) ∈ V) → (〈0, (𝑖 · 3)〉 ≠ 〈1, 4〉
↔ (0 ≠ 1 ∨ (𝑖
· 3) ≠ 4))) |
25 | 17, 24 | mp1i 13 |
. . . . . . . 8
⊢ (𝑖 ∈ ℤ → (〈0,
(𝑖 · 3)〉 ≠
〈1, 4〉 ↔ (0 ≠ 1 ∨ (𝑖 · 3) ≠ 4))) |
26 | 23, 25 | mpbird 260 |
. . . . . . 7
⊢ (𝑖 ∈ ℤ → 〈0,
(𝑖 · 3)〉 ≠
〈1, 4〉) |
27 | 20, 26 | jca 515 |
. . . . . 6
⊢ (𝑖 ∈ ℤ → (〈0,
(𝑖 · 3)〉 ≠
〈0, 2〉 ∧ 〈0, (𝑖 · 3)〉 ≠ 〈1,
4〉)) |
28 | 27 | orcd 872 |
. . . . 5
⊢ (𝑖 ∈ ℤ →
((〈0, (𝑖 ·
3)〉 ≠ 〈0, 2〉 ∧ 〈0, (𝑖 · 3)〉 ≠ 〈1, 4〉)
∨ (〈1, (𝑖 ·
6)〉 ≠ 〈0, 2〉 ∧ 〈1, (𝑖 · 6)〉 ≠ 〈1,
4〉))) |
29 | | opex 5332 |
. . . . . . . 8
⊢ 〈0,
(𝑖 · 3)〉 ∈
V |
30 | | opex 5332 |
. . . . . . . 8
⊢ 〈1,
(𝑖 · 6)〉 ∈
V |
31 | 29, 30 | pm3.2i 474 |
. . . . . . 7
⊢ (〈0,
(𝑖 · 3)〉 ∈
V ∧ 〈1, (𝑖
· 6)〉 ∈ V) |
32 | 31 | a1i 11 |
. . . . . 6
⊢ (𝑖 ∈ ℤ → (〈0,
(𝑖 · 3)〉 ∈
V ∧ 〈1, (𝑖
· 6)〉 ∈ V)) |
33 | | opex 5332 |
. . . . . . . 8
⊢ 〈0,
2〉 ∈ V |
34 | | opex 5332 |
. . . . . . . 8
⊢ 〈1,
4〉 ∈ V |
35 | 33, 34 | pm3.2i 474 |
. . . . . . 7
⊢ (〈0,
2〉 ∈ V ∧ 〈1, 4〉 ∈ V) |
36 | 35 | a1i 11 |
. . . . . 6
⊢ (𝑖 ∈ ℤ → (〈0,
2〉 ∈ V ∧ 〈1, 4〉 ∈ V)) |
37 | 22 | orcd 872 |
. . . . . . 7
⊢ (𝑖 ∈ ℤ → (0 ≠ 1
∨ (𝑖 · 3) ≠
(𝑖 ·
6))) |
38 | | opthneg 5349 |
. . . . . . . 8
⊢ ((0
∈ V ∧ (𝑖 ·
3) ∈ V) → (〈0, (𝑖 · 3)〉 ≠ 〈1, (𝑖 · 6)〉 ↔ (0
≠ 1 ∨ (𝑖 · 3)
≠ (𝑖 ·
6)))) |
39 | 17, 38 | mp1i 13 |
. . . . . . 7
⊢ (𝑖 ∈ ℤ → (〈0,
(𝑖 · 3)〉 ≠
〈1, (𝑖 ·
6)〉 ↔ (0 ≠ 1 ∨ (𝑖 · 3) ≠ (𝑖 · 6)))) |
40 | 37, 39 | mpbird 260 |
. . . . . 6
⊢ (𝑖 ∈ ℤ → 〈0,
(𝑖 · 3)〉 ≠
〈1, (𝑖 ·
6)〉) |
41 | | prnebg 4751 |
. . . . . . 7
⊢
(((〈0, (𝑖
· 3)〉 ∈ V ∧ 〈1, (𝑖 · 6)〉 ∈ V) ∧ (〈0,
2〉 ∈ V ∧ 〈1, 4〉 ∈ V) ∧ 〈0, (𝑖 · 3)〉 ≠ 〈1,
(𝑖 · 6)〉)
→ (((〈0, (𝑖
· 3)〉 ≠ 〈0, 2〉 ∧ 〈0, (𝑖 · 3)〉 ≠ 〈1, 4〉)
∨ (〈1, (𝑖 ·
6)〉 ≠ 〈0, 2〉 ∧ 〈1, (𝑖 · 6)〉 ≠ 〈1, 4〉))
↔ {〈0, (𝑖
· 3)〉, 〈1, (𝑖 · 6)〉} ≠ {〈0, 2〉,
〈1, 4〉})) |
42 | 41 | bicomd 226 |
. . . . . 6
⊢
(((〈0, (𝑖
· 3)〉 ∈ V ∧ 〈1, (𝑖 · 6)〉 ∈ V) ∧ (〈0,
2〉 ∈ V ∧ 〈1, 4〉 ∈ V) ∧ 〈0, (𝑖 · 3)〉 ≠ 〈1,
(𝑖 · 6)〉)
→ ({〈0, (𝑖
· 3)〉, 〈1, (𝑖 · 6)〉} ≠ {〈0, 2〉,
〈1, 4〉} ↔ ((〈0, (𝑖 · 3)〉 ≠ 〈0, 2〉
∧ 〈0, (𝑖 ·
3)〉 ≠ 〈1, 4〉) ∨ (〈1, (𝑖 · 6)〉 ≠ 〈0, 2〉
∧ 〈1, (𝑖 ·
6)〉 ≠ 〈1, 4〉)))) |
43 | 32, 36, 40, 42 | syl3anc 1372 |
. . . . 5
⊢ (𝑖 ∈ ℤ →
({〈0, (𝑖 ·
3)〉, 〈1, (𝑖
· 6)〉} ≠ {〈0, 2〉, 〈1, 4〉} ↔ ((〈0,
(𝑖 · 3)〉 ≠
〈0, 2〉 ∧ 〈0, (𝑖 · 3)〉 ≠ 〈1, 4〉)
∨ (〈1, (𝑖 ·
6)〉 ≠ 〈0, 2〉 ∧ 〈1, (𝑖 · 6)〉 ≠ 〈1,
4〉)))) |
44 | 28, 43 | mpbird 260 |
. . . 4
⊢ (𝑖 ∈ ℤ → {〈0,
(𝑖 · 3)〉,
〈1, (𝑖 ·
6)〉} ≠ {〈0, 2〉, 〈1, 4〉}) |
45 | | zlmodzxzequa.a |
. . . . . 6
⊢ 𝐴 = {〈0, 3〉, 〈1,
6〉} |
46 | 45 | oveq2i 7193 |
. . . . 5
⊢ (𝑖 ∙ 𝐴) = (𝑖 ∙ {〈0, 3〉,
〈1, 6〉}) |
47 | | 3z 12108 |
. . . . . 6
⊢ 3 ∈
ℤ |
48 | | 6nn 11817 |
. . . . . . 7
⊢ 6 ∈
ℕ |
49 | 48 | nnzi 12099 |
. . . . . 6
⊢ 6 ∈
ℤ |
50 | | zlmodzxzequa.z |
. . . . . . 7
⊢ 𝑍 = (ℤring
freeLMod {0, 1}) |
51 | | zlmodzxzequa.t |
. . . . . . 7
⊢ ∙ = (
·𝑠 ‘𝑍) |
52 | 50, 51 | zlmodzxzscm 45274 |
. . . . . 6
⊢ ((𝑖 ∈ ℤ ∧ 3 ∈
ℤ ∧ 6 ∈ ℤ) → (𝑖 ∙ {〈0, 3〉,
〈1, 6〉}) = {〈0, (𝑖 · 3)〉, 〈1, (𝑖 ·
6)〉}) |
53 | 47, 49, 52 | mp3an23 1454 |
. . . . 5
⊢ (𝑖 ∈ ℤ → (𝑖 ∙ {〈0, 3〉,
〈1, 6〉}) = {〈0, (𝑖 · 3)〉, 〈1, (𝑖 ·
6)〉}) |
54 | 46, 53 | syl5eq 2786 |
. . . 4
⊢ (𝑖 ∈ ℤ → (𝑖 ∙ 𝐴) = {〈0, (𝑖 · 3)〉, 〈1, (𝑖 ·
6)〉}) |
55 | | zlmodzxzequa.b |
. . . . 5
⊢ 𝐵 = {〈0, 2〉, 〈1,
4〉} |
56 | 55 | a1i 11 |
. . . 4
⊢ (𝑖 ∈ ℤ → 𝐵 = {〈0, 2〉, 〈1,
4〉}) |
57 | 44, 54, 56 | 3netr4d 3012 |
. . 3
⊢ (𝑖 ∈ ℤ → (𝑖 ∙ 𝐴) ≠ 𝐵) |
58 | | ztprmneprm 45264 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ ℤ ∧ 2 ∈
ℙ ∧ 3 ∈ ℙ) → ((𝑖 · 2) = 3 → 2 =
3)) |
59 | 2, 1, 58 | mp3an23 1454 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℤ → ((𝑖 · 2) = 3 → 2 =
3)) |
60 | | eqneqall 2946 |
. . . . . . . . . . . 12
⊢ (2 = 3
→ (2 ≠ 3 → (𝑖
· 2) ≠ 3)) |
61 | 7, 60 | mpi 20 |
. . . . . . . . . . 11
⊢ (2 = 3
→ (𝑖 · 2) ≠
3) |
62 | 59, 61 | syl6com 37 |
. . . . . . . . . 10
⊢ ((𝑖 · 2) = 3 → (𝑖 ∈ ℤ → (𝑖 · 2) ≠
3)) |
63 | | ax-1 6 |
. . . . . . . . . 10
⊢ ((𝑖 · 2) ≠ 3 →
(𝑖 ∈ ℤ →
(𝑖 · 2) ≠
3)) |
64 | 62, 63 | pm2.61ine 3018 |
. . . . . . . . 9
⊢ (𝑖 ∈ ℤ → (𝑖 · 2) ≠
3) |
65 | 64 | olcd 873 |
. . . . . . . 8
⊢ (𝑖 ∈ ℤ → (0 ≠ 0
∨ (𝑖 · 2) ≠
3)) |
66 | | ovex 7215 |
. . . . . . . . . 10
⊢ (𝑖 · 2) ∈
V |
67 | 15, 66 | pm3.2i 474 |
. . . . . . . . 9
⊢ (0 ∈
V ∧ (𝑖 · 2)
∈ V) |
68 | | opthneg 5349 |
. . . . . . . . 9
⊢ ((0
∈ V ∧ (𝑖 ·
2) ∈ V) → (〈0, (𝑖 · 2)〉 ≠ 〈0, 3〉
↔ (0 ≠ 0 ∨ (𝑖
· 2) ≠ 3))) |
69 | 67, 68 | mp1i 13 |
. . . . . . . 8
⊢ (𝑖 ∈ ℤ → (〈0,
(𝑖 · 2)〉 ≠
〈0, 3〉 ↔ (0 ≠ 0 ∨ (𝑖 · 2) ≠ 3))) |
70 | 65, 69 | mpbird 260 |
. . . . . . 7
⊢ (𝑖 ∈ ℤ → 〈0,
(𝑖 · 2)〉 ≠
〈0, 3〉) |
71 | 22 | orcd 872 |
. . . . . . . 8
⊢ (𝑖 ∈ ℤ → (0 ≠ 1
∨ (𝑖 · 2) ≠
6)) |
72 | | opthneg 5349 |
. . . . . . . . 9
⊢ ((0
∈ V ∧ (𝑖 ·
2) ∈ V) → (〈0, (𝑖 · 2)〉 ≠ 〈1, 6〉
↔ (0 ≠ 1 ∨ (𝑖
· 2) ≠ 6))) |
73 | 67, 72 | mp1i 13 |
. . . . . . . 8
⊢ (𝑖 ∈ ℤ → (〈0,
(𝑖 · 2)〉 ≠
〈1, 6〉 ↔ (0 ≠ 1 ∨ (𝑖 · 2) ≠ 6))) |
74 | 71, 73 | mpbird 260 |
. . . . . . 7
⊢ (𝑖 ∈ ℤ → 〈0,
(𝑖 · 2)〉 ≠
〈1, 6〉) |
75 | 70, 74 | jca 515 |
. . . . . 6
⊢ (𝑖 ∈ ℤ → (〈0,
(𝑖 · 2)〉 ≠
〈0, 3〉 ∧ 〈0, (𝑖 · 2)〉 ≠ 〈1,
6〉)) |
76 | 75 | orcd 872 |
. . . . 5
⊢ (𝑖 ∈ ℤ →
((〈0, (𝑖 ·
2)〉 ≠ 〈0, 3〉 ∧ 〈0, (𝑖 · 2)〉 ≠ 〈1, 6〉)
∨ (〈1, (𝑖 ·
4)〉 ≠ 〈0, 3〉 ∧ 〈1, (𝑖 · 4)〉 ≠ 〈1,
6〉))) |
77 | | opex 5332 |
. . . . . . . 8
⊢ 〈0,
(𝑖 · 2)〉 ∈
V |
78 | | opex 5332 |
. . . . . . . 8
⊢ 〈1,
(𝑖 · 4)〉 ∈
V |
79 | 77, 78 | pm3.2i 474 |
. . . . . . 7
⊢ (〈0,
(𝑖 · 2)〉 ∈
V ∧ 〈1, (𝑖
· 4)〉 ∈ V) |
80 | 79 | a1i 11 |
. . . . . 6
⊢ (𝑖 ∈ ℤ → (〈0,
(𝑖 · 2)〉 ∈
V ∧ 〈1, (𝑖
· 4)〉 ∈ V)) |
81 | | opex 5332 |
. . . . . . . 8
⊢ 〈0,
3〉 ∈ V |
82 | | opex 5332 |
. . . . . . . 8
⊢ 〈1,
6〉 ∈ V |
83 | 81, 82 | pm3.2i 474 |
. . . . . . 7
⊢ (〈0,
3〉 ∈ V ∧ 〈1, 6〉 ∈ V) |
84 | 83 | a1i 11 |
. . . . . 6
⊢ (𝑖 ∈ ℤ → (〈0,
3〉 ∈ V ∧ 〈1, 6〉 ∈ V)) |
85 | 22 | orcd 872 |
. . . . . . 7
⊢ (𝑖 ∈ ℤ → (0 ≠ 1
∨ (𝑖 · 2) ≠
(𝑖 ·
4))) |
86 | | opthneg 5349 |
. . . . . . . 8
⊢ ((0
∈ V ∧ (𝑖 ·
2) ∈ V) → (〈0, (𝑖 · 2)〉 ≠ 〈1, (𝑖 · 4)〉 ↔ (0
≠ 1 ∨ (𝑖 · 2)
≠ (𝑖 ·
4)))) |
87 | 67, 86 | mp1i 13 |
. . . . . . 7
⊢ (𝑖 ∈ ℤ → (〈0,
(𝑖 · 2)〉 ≠
〈1, (𝑖 ·
4)〉 ↔ (0 ≠ 1 ∨ (𝑖 · 2) ≠ (𝑖 · 4)))) |
88 | 85, 87 | mpbird 260 |
. . . . . 6
⊢ (𝑖 ∈ ℤ → 〈0,
(𝑖 · 2)〉 ≠
〈1, (𝑖 ·
4)〉) |
89 | | prnebg 4751 |
. . . . . . 7
⊢
(((〈0, (𝑖
· 2)〉 ∈ V ∧ 〈1, (𝑖 · 4)〉 ∈ V) ∧ (〈0,
3〉 ∈ V ∧ 〈1, 6〉 ∈ V) ∧ 〈0, (𝑖 · 2)〉 ≠ 〈1,
(𝑖 · 4)〉)
→ (((〈0, (𝑖
· 2)〉 ≠ 〈0, 3〉 ∧ 〈0, (𝑖 · 2)〉 ≠ 〈1, 6〉)
∨ (〈1, (𝑖 ·
4)〉 ≠ 〈0, 3〉 ∧ 〈1, (𝑖 · 4)〉 ≠ 〈1, 6〉))
↔ {〈0, (𝑖
· 2)〉, 〈1, (𝑖 · 4)〉} ≠ {〈0, 3〉,
〈1, 6〉})) |
90 | 89 | bicomd 226 |
. . . . . 6
⊢
(((〈0, (𝑖
· 2)〉 ∈ V ∧ 〈1, (𝑖 · 4)〉 ∈ V) ∧ (〈0,
3〉 ∈ V ∧ 〈1, 6〉 ∈ V) ∧ 〈0, (𝑖 · 2)〉 ≠ 〈1,
(𝑖 · 4)〉)
→ ({〈0, (𝑖
· 2)〉, 〈1, (𝑖 · 4)〉} ≠ {〈0, 3〉,
〈1, 6〉} ↔ ((〈0, (𝑖 · 2)〉 ≠ 〈0, 3〉
∧ 〈0, (𝑖 ·
2)〉 ≠ 〈1, 6〉) ∨ (〈1, (𝑖 · 4)〉 ≠ 〈0, 3〉
∧ 〈1, (𝑖 ·
4)〉 ≠ 〈1, 6〉)))) |
91 | 80, 84, 88, 90 | syl3anc 1372 |
. . . . 5
⊢ (𝑖 ∈ ℤ →
({〈0, (𝑖 ·
2)〉, 〈1, (𝑖
· 4)〉} ≠ {〈0, 3〉, 〈1, 6〉} ↔ ((〈0,
(𝑖 · 2)〉 ≠
〈0, 3〉 ∧ 〈0, (𝑖 · 2)〉 ≠ 〈1, 6〉)
∨ (〈1, (𝑖 ·
4)〉 ≠ 〈0, 3〉 ∧ 〈1, (𝑖 · 4)〉 ≠ 〈1,
6〉)))) |
92 | 76, 91 | mpbird 260 |
. . . 4
⊢ (𝑖 ∈ ℤ → {〈0,
(𝑖 · 2)〉,
〈1, (𝑖 ·
4)〉} ≠ {〈0, 3〉, 〈1, 6〉}) |
93 | 55 | oveq2i 7193 |
. . . . 5
⊢ (𝑖 ∙ 𝐵) = (𝑖 ∙ {〈0, 2〉,
〈1, 4〉}) |
94 | | 2z 12107 |
. . . . . 6
⊢ 2 ∈
ℤ |
95 | | 4z 12109 |
. . . . . 6
⊢ 4 ∈
ℤ |
96 | 50, 51 | zlmodzxzscm 45274 |
. . . . . 6
⊢ ((𝑖 ∈ ℤ ∧ 2 ∈
ℤ ∧ 4 ∈ ℤ) → (𝑖 ∙ {〈0, 2〉,
〈1, 4〉}) = {〈0, (𝑖 · 2)〉, 〈1, (𝑖 ·
4)〉}) |
97 | 94, 95, 96 | mp3an23 1454 |
. . . . 5
⊢ (𝑖 ∈ ℤ → (𝑖 ∙ {〈0, 2〉,
〈1, 4〉}) = {〈0, (𝑖 · 2)〉, 〈1, (𝑖 ·
4)〉}) |
98 | 93, 97 | syl5eq 2786 |
. . . 4
⊢ (𝑖 ∈ ℤ → (𝑖 ∙ 𝐵) = {〈0, (𝑖 · 2)〉, 〈1, (𝑖 ·
4)〉}) |
99 | 45 | a1i 11 |
. . . 4
⊢ (𝑖 ∈ ℤ → 𝐴 = {〈0, 3〉, 〈1,
6〉}) |
100 | 92, 98, 99 | 3netr4d 3012 |
. . 3
⊢ (𝑖 ∈ ℤ → (𝑖 ∙ 𝐵) ≠ 𝐴) |
101 | 57, 100 | jca 515 |
. 2
⊢ (𝑖 ∈ ℤ → ((𝑖 ∙ 𝐴) ≠ 𝐵 ∧ (𝑖 ∙ 𝐵) ≠ 𝐴)) |
102 | 101 | rgen 3064 |
1
⊢
∀𝑖 ∈
ℤ ((𝑖 ∙ 𝐴) ≠ 𝐵 ∧ (𝑖 ∙ 𝐵) ≠ 𝐴) |