Step | Hyp | Ref
| Expression |
1 | | 3prm 16631 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℙ |
2 | | 2prm 16629 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℙ |
3 | | ztprmneprm 47023 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ ℤ ∧ 3 ∈
ℙ ∧ 2 ∈ ℙ) → ((𝑖 · 3) = 2 → 3 =
2)) |
4 | 1, 2, 3 | mp3an23 1454 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℤ → ((𝑖 · 3) = 2 → 3 =
2)) |
5 | | 2re 12286 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ |
6 | | 2lt3 12384 |
. . . . . . . . . . . . . 14
⊢ 2 <
3 |
7 | 5, 6 | ltneii 11327 |
. . . . . . . . . . . . 13
⊢ 2 ≠
3 |
8 | | eqneqall 2952 |
. . . . . . . . . . . . 13
⊢ (2 = 3
→ (2 ≠ 3 → (𝑖
· 3) ≠ 2)) |
9 | 7, 8 | mpi 20 |
. . . . . . . . . . . 12
⊢ (2 = 3
→ (𝑖 · 3) ≠
2) |
10 | 9 | eqcoms 2741 |
. . . . . . . . . . 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 3026 |
. . . . . . . . 9
⊢ (𝑖 ∈ ℤ → (𝑖 · 3) ≠
2) |
14 | 13 | olcd 873 |
. . . . . . . 8
⊢ (𝑖 ∈ ℤ → (0 ≠ 0
∨ (𝑖 · 3) ≠
2)) |
15 | | c0ex 11208 |
. . . . . . . . . 10
⊢ 0 ∈
V |
16 | | ovex 7442 |
. . . . . . . . . 10
⊢ (𝑖 · 3) ∈
V |
17 | 15, 16 | pm3.2i 472 |
. . . . . . . . 9
⊢ (0 ∈
V ∧ (𝑖 · 3)
∈ V) |
18 | | opthneg 5482 |
. . . . . . . . 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 12283 |
. . . . . . . . . 10
⊢ 0 ≠
1 |
22 | 21 | a1i 11 |
. . . . . . . . 9
⊢ (𝑖 ∈ ℤ → 0 ≠
1) |
23 | 22 | orcd 872 |
. . . . . . . 8
⊢ (𝑖 ∈ ℤ → (0 ≠ 1
∨ (𝑖 · 3) ≠
4)) |
24 | | opthneg 5482 |
. . . . . . . . 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 513 |
. . . . . 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 5465 |
. . . . . . . 8
⊢ ⟨0,
(𝑖 · 3)⟩ ∈
V |
30 | | opex 5465 |
. . . . . . . 8
⊢ ⟨1,
(𝑖 · 6)⟩ ∈
V |
31 | 29, 30 | pm3.2i 472 |
. . . . . . 7
⊢ (⟨0,
(𝑖 · 3)⟩ ∈
V ∧ ⟨1, (𝑖
· 6)⟩ ∈ V) |
32 | 31 | a1i 11 |
. . . . . 6
⊢ (𝑖 ∈ ℤ → (⟨0,
(𝑖 · 3)⟩ ∈
V ∧ ⟨1, (𝑖
· 6)⟩ ∈ V)) |
33 | | opex 5465 |
. . . . . . . 8
⊢ ⟨0,
2⟩ ∈ V |
34 | | opex 5465 |
. . . . . . . 8
⊢ ⟨1,
4⟩ ∈ V |
35 | 33, 34 | pm3.2i 472 |
. . . . . . 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 5482 |
. . . . . . . 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 4857 |
. . . . . . 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 222 |
. . . . . 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 257 |
. . . 4
⊢ (𝑖 ∈ ℤ → {⟨0,
(𝑖 · 3)⟩,
⟨1, (𝑖 ·
6)⟩} ≠ {⟨0, 2⟩, ⟨1, 4⟩}) |
45 | | zlmodzxzequa.a |
. . . . . 6
⊢ 𝐴 = {⟨0, 3⟩, ⟨1,
6⟩} |
46 | 45 | oveq2i 7420 |
. . . . 5
⊢ (𝑖 ∙ 𝐴) = (𝑖 ∙ {⟨0, 3⟩,
⟨1, 6⟩}) |
47 | | 3z 12595 |
. . . . . 6
⊢ 3 ∈
ℤ |
48 | | 6nn 12301 |
. . . . . . 7
⊢ 6 ∈
ℕ |
49 | 48 | nnzi 12586 |
. . . . . 6
⊢ 6 ∈
ℤ |
50 | | zlmodzxzequa.z |
. . . . . . 7
⊢ 𝑍 = (ℤring
freeLMod {0, 1}) |
51 | | zlmodzxzequa.t |
. . . . . . 7
⊢ ∙ = (
·𝑠 ‘𝑍) |
52 | 50, 51 | zlmodzxzscm 47033 |
. . . . . 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 | eqtrid 2785 |
. . . 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 3019 |
. . 3
⊢ (𝑖 ∈ ℤ → (𝑖 ∙ 𝐴) ≠ 𝐵) |
58 | | ztprmneprm 47023 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ ℤ ∧ 2 ∈
ℙ ∧ 3 ∈ ℙ) → ((𝑖 · 2) = 3 → 2 =
3)) |
59 | 2, 1, 58 | mp3an23 1454 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℤ → ((𝑖 · 2) = 3 → 2 =
3)) |
60 | | eqneqall 2952 |
. . . . . . . . . . . 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 3026 |
. . . . . . . . 9
⊢ (𝑖 ∈ ℤ → (𝑖 · 2) ≠
3) |
65 | 64 | olcd 873 |
. . . . . . . 8
⊢ (𝑖 ∈ ℤ → (0 ≠ 0
∨ (𝑖 · 2) ≠
3)) |
66 | | ovex 7442 |
. . . . . . . . . 10
⊢ (𝑖 · 2) ∈
V |
67 | 15, 66 | pm3.2i 472 |
. . . . . . . . 9
⊢ (0 ∈
V ∧ (𝑖 · 2)
∈ V) |
68 | | opthneg 5482 |
. . . . . . . . 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 872 |
. . . . . . . 8
⊢ (𝑖 ∈ ℤ → (0 ≠ 1
∨ (𝑖 · 2) ≠
6)) |
72 | | opthneg 5482 |
. . . . . . . . 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 513 |
. . . . . 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 5465 |
. . . . . . . 8
⊢ ⟨0,
(𝑖 · 2)⟩ ∈
V |
78 | | opex 5465 |
. . . . . . . 8
⊢ ⟨1,
(𝑖 · 4)⟩ ∈
V |
79 | 77, 78 | pm3.2i 472 |
. . . . . . 7
⊢ (⟨0,
(𝑖 · 2)⟩ ∈
V ∧ ⟨1, (𝑖
· 4)⟩ ∈ V) |
80 | 79 | a1i 11 |
. . . . . 6
⊢ (𝑖 ∈ ℤ → (⟨0,
(𝑖 · 2)⟩ ∈
V ∧ ⟨1, (𝑖
· 4)⟩ ∈ V)) |
81 | | opex 5465 |
. . . . . . . 8
⊢ ⟨0,
3⟩ ∈ V |
82 | | opex 5465 |
. . . . . . . 8
⊢ ⟨1,
6⟩ ∈ V |
83 | 81, 82 | pm3.2i 472 |
. . . . . . 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 5482 |
. . . . . . . 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 4857 |
. . . . . . 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 222 |
. . . . . 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 257 |
. . . 4
⊢ (𝑖 ∈ ℤ → {⟨0,
(𝑖 · 2)⟩,
⟨1, (𝑖 ·
4)⟩} ≠ {⟨0, 3⟩, ⟨1, 6⟩}) |
93 | 55 | oveq2i 7420 |
. . . . 5
⊢ (𝑖 ∙ 𝐵) = (𝑖 ∙ {⟨0, 2⟩,
⟨1, 4⟩}) |
94 | | 2z 12594 |
. . . . . 6
⊢ 2 ∈
ℤ |
95 | | 4z 12596 |
. . . . . 6
⊢ 4 ∈
ℤ |
96 | 50, 51 | zlmodzxzscm 47033 |
. . . . . 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 | eqtrid 2785 |
. . . 4
⊢ (𝑖 ∈ ℤ → (𝑖 ∙ 𝐵) = {⟨0, (𝑖 · 2)⟩, ⟨1, (𝑖 ·
4)⟩}) |
99 | 45 | a1i 11 |
. . . 4
⊢ (𝑖 ∈ ℤ → 𝐴 = {⟨0, 3⟩, ⟨1,
6⟩}) |
100 | 92, 98, 99 | 3netr4d 3019 |
. . 3
⊢ (𝑖 ∈ ℤ → (𝑖 ∙ 𝐵) ≠ 𝐴) |
101 | 57, 100 | jca 513 |
. 2
⊢ (𝑖 ∈ ℤ → ((𝑖 ∙ 𝐴) ≠ 𝐵 ∧ (𝑖 ∙ 𝐵) ≠ 𝐴)) |
102 | 101 | rgen 3064 |
1
⊢
∀𝑖 ∈
ℤ ((𝑖 ∙ 𝐴) ≠ 𝐵 ∧ (𝑖 ∙ 𝐵) ≠ 𝐴) |