Proof of Theorem zlmodzxznm
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 3prm 16731 | . . . . . . . . . . . 12
⊢ 3 ∈
ℙ | 
| 2 |  | 2prm 16729 | . . . . . . . . . . . 12
⊢ 2 ∈
ℙ | 
| 3 |  | ztprmneprm 48263 | . . . . . . . . . . . 12
⊢ ((𝑖 ∈ ℤ ∧ 3 ∈
ℙ ∧ 2 ∈ ℙ) → ((𝑖 · 3) = 2 → 3 =
2)) | 
| 4 | 1, 2, 3 | mp3an23 1455 | . . . . . . . . . . 11
⊢ (𝑖 ∈ ℤ → ((𝑖 · 3) = 2 → 3 =
2)) | 
| 5 |  | 2re 12340 | . . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ | 
| 6 |  | 2lt3 12438 | . . . . . . . . . . . . . 14
⊢ 2 <
3 | 
| 7 | 5, 6 | ltneii 11374 | . . . . . . . . . . . . 13
⊢ 2 ≠
3 | 
| 8 |  | eqneqall 2951 | . . . . . . . . . . . . 13
⊢ (2 = 3
→ (2 ≠ 3 → (𝑖
· 3) ≠ 2)) | 
| 9 | 7, 8 | mpi 20 | . . . . . . . . . . . 12
⊢ (2 = 3
→ (𝑖 · 3) ≠
2) | 
| 10 | 9 | eqcoms 2745 | . . . . . . . . . . 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 3025 | . . . . . . . . 9
⊢ (𝑖 ∈ ℤ → (𝑖 · 3) ≠
2) | 
| 14 | 13 | olcd 875 | . . . . . . . 8
⊢ (𝑖 ∈ ℤ → (0 ≠ 0
∨ (𝑖 · 3) ≠
2)) | 
| 15 |  | c0ex 11255 | . . . . . . . . . 10
⊢ 0 ∈
V | 
| 16 |  | ovex 7464 | . . . . . . . . . 10
⊢ (𝑖 · 3) ∈
V | 
| 17 | 15, 16 | pm3.2i 470 | . . . . . . . . 9
⊢ (0 ∈
V ∧ (𝑖 · 3)
∈ V) | 
| 18 |  | opthneg 5486 | . . . . . . . . 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 257 | . . . . . . 7
⊢ (𝑖 ∈ ℤ → 〈0,
(𝑖 · 3)〉 ≠
〈0, 2〉) | 
| 21 |  | 0ne1 12337 | . . . . . . . . . 10
⊢ 0 ≠
1 | 
| 22 | 21 | a1i 11 | . . . . . . . . 9
⊢ (𝑖 ∈ ℤ → 0 ≠
1) | 
| 23 | 22 | orcd 874 | . . . . . . . 8
⊢ (𝑖 ∈ ℤ → (0 ≠ 1
∨ (𝑖 · 3) ≠
4)) | 
| 24 |  | opthneg 5486 | . . . . . . . . 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 257 | . . . . . . 7
⊢ (𝑖 ∈ ℤ → 〈0,
(𝑖 · 3)〉 ≠
〈1, 4〉) | 
| 27 | 20, 26 | jca 511 | . . . . . 6
⊢ (𝑖 ∈ ℤ → (〈0,
(𝑖 · 3)〉 ≠
〈0, 2〉 ∧ 〈0, (𝑖 · 3)〉 ≠ 〈1,
4〉)) | 
| 28 | 27 | orcd 874 | . . . . 5
⊢ (𝑖 ∈ ℤ →
((〈0, (𝑖 ·
3)〉 ≠ 〈0, 2〉 ∧ 〈0, (𝑖 · 3)〉 ≠ 〈1, 4〉)
∨ (〈1, (𝑖 ·
6)〉 ≠ 〈0, 2〉 ∧ 〈1, (𝑖 · 6)〉 ≠ 〈1,
4〉))) | 
| 29 |  | opex 5469 | . . . . . . . 8
⊢ 〈0,
(𝑖 · 3)〉 ∈
V | 
| 30 |  | opex 5469 | . . . . . . . 8
⊢ 〈1,
(𝑖 · 6)〉 ∈
V | 
| 31 | 29, 30 | pm3.2i 470 | . . . . . . 7
⊢ (〈0,
(𝑖 · 3)〉 ∈
V ∧ 〈1, (𝑖
· 6)〉 ∈ V) | 
| 32 | 31 | a1i 11 | . . . . . 6
⊢ (𝑖 ∈ ℤ → (〈0,
(𝑖 · 3)〉 ∈
V ∧ 〈1, (𝑖
· 6)〉 ∈ V)) | 
| 33 |  | opex 5469 | . . . . . . . 8
⊢ 〈0,
2〉 ∈ V | 
| 34 |  | opex 5469 | . . . . . . . 8
⊢ 〈1,
4〉 ∈ V | 
| 35 | 33, 34 | pm3.2i 470 | . . . . . . 7
⊢ (〈0,
2〉 ∈ V ∧ 〈1, 4〉 ∈ V) | 
| 36 | 35 | a1i 11 | . . . . . 6
⊢ (𝑖 ∈ ℤ → (〈0,
2〉 ∈ V ∧ 〈1, 4〉 ∈ V)) | 
| 37 | 22 | orcd 874 | . . . . . . 7
⊢ (𝑖 ∈ ℤ → (0 ≠ 1
∨ (𝑖 · 3) ≠
(𝑖 ·
6))) | 
| 38 |  | opthneg 5486 | . . . . . . . 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 257 | . . . . . 6
⊢ (𝑖 ∈ ℤ → 〈0,
(𝑖 · 3)〉 ≠
〈1, (𝑖 ·
6)〉) | 
| 41 |  | prnebg 4856 | . . . . . . 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 223 | . . . . . 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 1373 | . . . . 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 257 | . . . 4
⊢ (𝑖 ∈ ℤ → {〈0,
(𝑖 · 3)〉,
〈1, (𝑖 ·
6)〉} ≠ {〈0, 2〉, 〈1, 4〉}) | 
| 45 |  | zlmodzxzequa.a | . . . . . 6
⊢ 𝐴 = {〈0, 3〉, 〈1,
6〉} | 
| 46 | 45 | oveq2i 7442 | . . . . 5
⊢ (𝑖 ∙ 𝐴) = (𝑖 ∙ {〈0, 3〉,
〈1, 6〉}) | 
| 47 |  | 3z 12650 | . . . . . 6
⊢ 3 ∈
ℤ | 
| 48 |  | 6nn 12355 | . . . . . . 7
⊢ 6 ∈
ℕ | 
| 49 | 48 | nnzi 12641 | . . . . . 6
⊢ 6 ∈
ℤ | 
| 50 |  | zlmodzxzequa.z | . . . . . . 7
⊢ 𝑍 = (ℤring
freeLMod {0, 1}) | 
| 51 |  | zlmodzxzequa.t | . . . . . . 7
⊢  ∙ = (
·𝑠 ‘𝑍) | 
| 52 | 50, 51 | zlmodzxzscm 48273 | . . . . . 6
⊢ ((𝑖 ∈ ℤ ∧ 3 ∈
ℤ ∧ 6 ∈ ℤ) → (𝑖 ∙ {〈0, 3〉,
〈1, 6〉}) = {〈0, (𝑖 · 3)〉, 〈1, (𝑖 ·
6)〉}) | 
| 53 | 47, 49, 52 | mp3an23 1455 | . . . . 5
⊢ (𝑖 ∈ ℤ → (𝑖 ∙ {〈0, 3〉,
〈1, 6〉}) = {〈0, (𝑖 · 3)〉, 〈1, (𝑖 ·
6)〉}) | 
| 54 | 46, 53 | eqtrid 2789 | . . . 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 3018 | . . 3
⊢ (𝑖 ∈ ℤ → (𝑖 ∙ 𝐴) ≠ 𝐵) | 
| 58 |  | ztprmneprm 48263 | . . . . . . . . . . . 12
⊢ ((𝑖 ∈ ℤ ∧ 2 ∈
ℙ ∧ 3 ∈ ℙ) → ((𝑖 · 2) = 3 → 2 =
3)) | 
| 59 | 2, 1, 58 | mp3an23 1455 | . . . . . . . . . . 11
⊢ (𝑖 ∈ ℤ → ((𝑖 · 2) = 3 → 2 =
3)) | 
| 60 |  | eqneqall 2951 | . . . . . . . . . . . 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 3025 | . . . . . . . . 9
⊢ (𝑖 ∈ ℤ → (𝑖 · 2) ≠
3) | 
| 65 | 64 | olcd 875 | . . . . . . . 8
⊢ (𝑖 ∈ ℤ → (0 ≠ 0
∨ (𝑖 · 2) ≠
3)) | 
| 66 |  | ovex 7464 | . . . . . . . . . 10
⊢ (𝑖 · 2) ∈
V | 
| 67 | 15, 66 | pm3.2i 470 | . . . . . . . . 9
⊢ (0 ∈
V ∧ (𝑖 · 2)
∈ V) | 
| 68 |  | opthneg 5486 | . . . . . . . . 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 257 | . . . . . . 7
⊢ (𝑖 ∈ ℤ → 〈0,
(𝑖 · 2)〉 ≠
〈0, 3〉) | 
| 71 | 22 | orcd 874 | . . . . . . . 8
⊢ (𝑖 ∈ ℤ → (0 ≠ 1
∨ (𝑖 · 2) ≠
6)) | 
| 72 |  | opthneg 5486 | . . . . . . . . 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 257 | . . . . . . 7
⊢ (𝑖 ∈ ℤ → 〈0,
(𝑖 · 2)〉 ≠
〈1, 6〉) | 
| 75 | 70, 74 | jca 511 | . . . . . 6
⊢ (𝑖 ∈ ℤ → (〈0,
(𝑖 · 2)〉 ≠
〈0, 3〉 ∧ 〈0, (𝑖 · 2)〉 ≠ 〈1,
6〉)) | 
| 76 | 75 | orcd 874 | . . . . 5
⊢ (𝑖 ∈ ℤ →
((〈0, (𝑖 ·
2)〉 ≠ 〈0, 3〉 ∧ 〈0, (𝑖 · 2)〉 ≠ 〈1, 6〉)
∨ (〈1, (𝑖 ·
4)〉 ≠ 〈0, 3〉 ∧ 〈1, (𝑖 · 4)〉 ≠ 〈1,
6〉))) | 
| 77 |  | opex 5469 | . . . . . . . 8
⊢ 〈0,
(𝑖 · 2)〉 ∈
V | 
| 78 |  | opex 5469 | . . . . . . . 8
⊢ 〈1,
(𝑖 · 4)〉 ∈
V | 
| 79 | 77, 78 | pm3.2i 470 | . . . . . . 7
⊢ (〈0,
(𝑖 · 2)〉 ∈
V ∧ 〈1, (𝑖
· 4)〉 ∈ V) | 
| 80 | 79 | a1i 11 | . . . . . 6
⊢ (𝑖 ∈ ℤ → (〈0,
(𝑖 · 2)〉 ∈
V ∧ 〈1, (𝑖
· 4)〉 ∈ V)) | 
| 81 |  | opex 5469 | . . . . . . . 8
⊢ 〈0,
3〉 ∈ V | 
| 82 |  | opex 5469 | . . . . . . . 8
⊢ 〈1,
6〉 ∈ V | 
| 83 | 81, 82 | pm3.2i 470 | . . . . . . 7
⊢ (〈0,
3〉 ∈ V ∧ 〈1, 6〉 ∈ V) | 
| 84 | 83 | a1i 11 | . . . . . 6
⊢ (𝑖 ∈ ℤ → (〈0,
3〉 ∈ V ∧ 〈1, 6〉 ∈ V)) | 
| 85 | 22 | orcd 874 | . . . . . . 7
⊢ (𝑖 ∈ ℤ → (0 ≠ 1
∨ (𝑖 · 2) ≠
(𝑖 ·
4))) | 
| 86 |  | opthneg 5486 | . . . . . . . 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 257 | . . . . . 6
⊢ (𝑖 ∈ ℤ → 〈0,
(𝑖 · 2)〉 ≠
〈1, (𝑖 ·
4)〉) | 
| 89 |  | prnebg 4856 | . . . . . . 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 223 | . . . . . 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 1373 | . . . . 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 257 | . . . 4
⊢ (𝑖 ∈ ℤ → {〈0,
(𝑖 · 2)〉,
〈1, (𝑖 ·
4)〉} ≠ {〈0, 3〉, 〈1, 6〉}) | 
| 93 | 55 | oveq2i 7442 | . . . . 5
⊢ (𝑖 ∙ 𝐵) = (𝑖 ∙ {〈0, 2〉,
〈1, 4〉}) | 
| 94 |  | 2z 12649 | . . . . . 6
⊢ 2 ∈
ℤ | 
| 95 |  | 4z 12651 | . . . . . 6
⊢ 4 ∈
ℤ | 
| 96 | 50, 51 | zlmodzxzscm 48273 | . . . . . 6
⊢ ((𝑖 ∈ ℤ ∧ 2 ∈
ℤ ∧ 4 ∈ ℤ) → (𝑖 ∙ {〈0, 2〉,
〈1, 4〉}) = {〈0, (𝑖 · 2)〉, 〈1, (𝑖 ·
4)〉}) | 
| 97 | 94, 95, 96 | mp3an23 1455 | . . . . 5
⊢ (𝑖 ∈ ℤ → (𝑖 ∙ {〈0, 2〉,
〈1, 4〉}) = {〈0, (𝑖 · 2)〉, 〈1, (𝑖 ·
4)〉}) | 
| 98 | 93, 97 | eqtrid 2789 | . . . 4
⊢ (𝑖 ∈ ℤ → (𝑖 ∙ 𝐵) = {〈0, (𝑖 · 2)〉, 〈1, (𝑖 ·
4)〉}) | 
| 99 | 45 | a1i 11 | . . . 4
⊢ (𝑖 ∈ ℤ → 𝐴 = {〈0, 3〉, 〈1,
6〉}) | 
| 100 | 92, 98, 99 | 3netr4d 3018 | . . 3
⊢ (𝑖 ∈ ℤ → (𝑖 ∙ 𝐵) ≠ 𝐴) | 
| 101 | 57, 100 | jca 511 | . 2
⊢ (𝑖 ∈ ℤ → ((𝑖 ∙ 𝐴) ≠ 𝐵 ∧ (𝑖 ∙ 𝐵) ≠ 𝐴)) | 
| 102 | 101 | rgen 3063 | 1
⊢
∀𝑖 ∈
ℤ ((𝑖 ∙ 𝐴) ≠ 𝐵 ∧ (𝑖 ∙ 𝐵) ≠ 𝐴) |