Metamath Proof Explorer

Theorem zlmodzxznm

Description: Example of a linearly dependent set whose elements are not linear combinations of the others, see note in Roman p. 112). (Contributed by AV, 23-May-2019) (Revised by AV, 10-Jun-2019)

Ref Expression
Hypotheses zlmodzxzequa.z ⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
zlmodzxzequa.o ⊢ 0 = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
zlmodzxzequa.t ⊢ ∙ = ( ·𝑠 ‘ 𝑍 )
zlmodzxzequa.m ⊢ − = ( -g ‘ 𝑍 )
zlmodzxzequa.a ⊢ 𝐴 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ }
zlmodzxzequa.b ⊢ 𝐵 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ }
Assertion zlmodzxznm ∀ 𝑖 ∈ ℤ ( ( 𝑖 ∙ 𝐴 ) ≠ 𝐵 ∧ ( 𝑖 ∙ 𝐵 ) ≠ 𝐴 )

Proof

Step Hyp Ref Expression
1 zlmodzxzequa.z ⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
2 zlmodzxzequa.o ⊢ 0 = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
3 zlmodzxzequa.t ⊢ ∙ = ( ·𝑠 ‘ 𝑍 )
4 zlmodzxzequa.m ⊢ − = ( -g ‘ 𝑍 )
5 zlmodzxzequa.a ⊢ 𝐴 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ }
6 zlmodzxzequa.b ⊢ 𝐵 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ }
7 3prm ⊢ 3 ∈ ℙ
8 2prm ⊢ 2 ∈ ℙ
9 ztprmneprm ⊢ ( ( 𝑖 ∈ ℤ ∧ 3 ∈ ℙ ∧ 2 ∈ ℙ ) → ( ( 𝑖 · 3 ) = 2 → 3 = 2 ) )
10 7 8 9 mp3an23 ⊢ ( 𝑖 ∈ ℤ → ( ( 𝑖 · 3 ) = 2 → 3 = 2 ) )
11 2re ⊢ 2 ∈ ℝ
12 2lt3 ⊢ 2 < 3
13 11 12 ltneii ⊢ 2 ≠ 3
14 eqneqall ⊢ ( 2 = 3 → ( 2 ≠ 3 → ( 𝑖 · 3 ) ≠ 2 ) )
15 13 14 mpi ⊢ ( 2 = 3 → ( 𝑖 · 3 ) ≠ 2 )
16 15 eqcoms ⊢ ( 3 = 2 → ( 𝑖 · 3 ) ≠ 2 )
17 10 16 syl6com ⊢ ( ( 𝑖 · 3 ) = 2 → ( 𝑖 ∈ ℤ → ( 𝑖 · 3 ) ≠ 2 ) )
18 ax-1 ⊢ ( ( 𝑖 · 3 ) ≠ 2 → ( 𝑖 ∈ ℤ → ( 𝑖 · 3 ) ≠ 2 ) )
19 17 18 pm2.61ine ⊢ ( 𝑖 ∈ ℤ → ( 𝑖 · 3 ) ≠ 2 )
20 19 olcd ⊢ ( 𝑖 ∈ ℤ → ( 0 ≠ 0 ∨ ( 𝑖 · 3 ) ≠ 2 ) )
21 c0ex ⊢ 0 ∈ V
22 ovex ⊢ ( 𝑖 · 3 ) ∈ V
23 21 22 pm3.2i ⊢ ( 0 ∈ V ∧ ( 𝑖 · 3 ) ∈ V )
24 opthneg ⊢ ( ( 0 ∈ V ∧ ( 𝑖 · 3 ) ∈ V ) → ( ⟨ 0 , ( 𝑖 · 3 ) ⟩ ≠ ⟨ 0 , 2 ⟩ ↔ ( 0 ≠ 0 ∨ ( 𝑖 · 3 ) ≠ 2 ) ) )
25 23 24 mp1i ⊢ ( 𝑖 ∈ ℤ → ( ⟨ 0 , ( 𝑖 · 3 ) ⟩ ≠ ⟨ 0 , 2 ⟩ ↔ ( 0 ≠ 0 ∨ ( 𝑖 · 3 ) ≠ 2 ) ) )
26 20 25 mpbird ⊢ ( 𝑖 ∈ ℤ → ⟨ 0 , ( 𝑖 · 3 ) ⟩ ≠ ⟨ 0 , 2 ⟩ )
27 0ne1 ⊢ 0 ≠ 1
28 27 a1i ⊢ ( 𝑖 ∈ ℤ → 0 ≠ 1 )
29 28 orcd ⊢ ( 𝑖 ∈ ℤ → ( 0 ≠ 1 ∨ ( 𝑖 · 3 ) ≠ 4 ) )
30 opthneg ⊢ ( ( 0 ∈ V ∧ ( 𝑖 · 3 ) ∈ V ) → ( ⟨ 0 , ( 𝑖 · 3 ) ⟩ ≠ ⟨ 1 , 4 ⟩ ↔ ( 0 ≠ 1 ∨ ( 𝑖 · 3 ) ≠ 4 ) ) )
31 23 30 mp1i ⊢ ( 𝑖 ∈ ℤ → ( ⟨ 0 , ( 𝑖 · 3 ) ⟩ ≠ ⟨ 1 , 4 ⟩ ↔ ( 0 ≠ 1 ∨ ( 𝑖 · 3 ) ≠ 4 ) ) )
32 29 31 mpbird ⊢ ( 𝑖 ∈ ℤ → ⟨ 0 , ( 𝑖 · 3 ) ⟩ ≠ ⟨ 1 , 4 ⟩ )
33 26 32 jca ⊢ ( 𝑖 ∈ ℤ → ( ⟨ 0 , ( 𝑖 · 3 ) ⟩ ≠ ⟨ 0 , 2 ⟩ ∧ ⟨ 0 , ( 𝑖 · 3 ) ⟩ ≠ ⟨ 1 , 4 ⟩ ) )
34 33 orcd ⊢ ( 𝑖 ∈ ℤ → ( ( ⟨ 0 , ( 𝑖 · 3 ) ⟩ ≠ ⟨ 0 , 2 ⟩ ∧ ⟨ 0 , ( 𝑖 · 3 ) ⟩ ≠ ⟨ 1 , 4 ⟩ ) ∨ ( ⟨ 1 , ( 𝑖 · 6 ) ⟩ ≠ ⟨ 0 , 2 ⟩ ∧ ⟨ 1 , ( 𝑖 · 6 ) ⟩ ≠ ⟨ 1 , 4 ⟩ ) ) )
35 opex ⊢ ⟨ 0 , ( 𝑖 · 3 ) ⟩ ∈ V
36 opex ⊢ ⟨ 1 , ( 𝑖 · 6 ) ⟩ ∈ V
37 35 36 pm3.2i ⊢ ( ⟨ 0 , ( 𝑖 · 3 ) ⟩ ∈ V ∧ ⟨ 1 , ( 𝑖 · 6 ) ⟩ ∈ V )
38 37 a1i ⊢ ( 𝑖 ∈ ℤ → ( ⟨ 0 , ( 𝑖 · 3 ) ⟩ ∈ V ∧ ⟨ 1 , ( 𝑖 · 6 ) ⟩ ∈ V ) )
39 opex ⊢ ⟨ 0 , 2 ⟩ ∈ V
40 opex ⊢ ⟨ 1 , 4 ⟩ ∈ V
41 39 40 pm3.2i ⊢ ( ⟨ 0 , 2 ⟩ ∈ V ∧ ⟨ 1 , 4 ⟩ ∈ V )
42 41 a1i ⊢ ( 𝑖 ∈ ℤ → ( ⟨ 0 , 2 ⟩ ∈ V ∧ ⟨ 1 , 4 ⟩ ∈ V ) )
43 28 orcd ⊢ ( 𝑖 ∈ ℤ → ( 0 ≠ 1 ∨ ( 𝑖 · 3 ) ≠ ( 𝑖 · 6 ) ) )
44 opthneg ⊢ ( ( 0 ∈ V ∧ ( 𝑖 · 3 ) ∈ V ) → ( ⟨ 0 , ( 𝑖 · 3 ) ⟩ ≠ ⟨ 1 , ( 𝑖 · 6 ) ⟩ ↔ ( 0 ≠ 1 ∨ ( 𝑖 · 3 ) ≠ ( 𝑖 · 6 ) ) ) )
45 23 44 mp1i ⊢ ( 𝑖 ∈ ℤ → ( ⟨ 0 , ( 𝑖 · 3 ) ⟩ ≠ ⟨ 1 , ( 𝑖 · 6 ) ⟩ ↔ ( 0 ≠ 1 ∨ ( 𝑖 · 3 ) ≠ ( 𝑖 · 6 ) ) ) )
46 43 45 mpbird ⊢ ( 𝑖 ∈ ℤ → ⟨ 0 , ( 𝑖 · 3 ) ⟩ ≠ ⟨ 1 , ( 𝑖 · 6 ) ⟩ )
47 prnebg ⊢ ( ( ( ⟨ 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 ⟩ } ) )
48 47 bicomd ⊢ ( ( ( ⟨ 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 ⟩ ) ) ) )
49 38 42 46 48 syl3anc ⊢ ( 𝑖 ∈ ℤ → ( { ⟨ 0 , ( 𝑖 · 3 ) ⟩ , ⟨ 1 , ( 𝑖 · 6 ) ⟩ } ≠ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ↔ ( ( ⟨ 0 , ( 𝑖 · 3 ) ⟩ ≠ ⟨ 0 , 2 ⟩ ∧ ⟨ 0 , ( 𝑖 · 3 ) ⟩ ≠ ⟨ 1 , 4 ⟩ ) ∨ ( ⟨ 1 , ( 𝑖 · 6 ) ⟩ ≠ ⟨ 0 , 2 ⟩ ∧ ⟨ 1 , ( 𝑖 · 6 ) ⟩ ≠ ⟨ 1 , 4 ⟩ ) ) ) )
50 34 49 mpbird ⊢ ( 𝑖 ∈ ℤ → { ⟨ 0 , ( 𝑖 · 3 ) ⟩ , ⟨ 1 , ( 𝑖 · 6 ) ⟩ } ≠ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } )
51 5 oveq2i ⊢ ( 𝑖 ∙ 𝐴 ) = ( 𝑖 ∙ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } )
52 3z ⊢ 3 ∈ ℤ
53 6nn ⊢ 6 ∈ ℕ
54 53 nnzi ⊢ 6 ∈ ℤ
55 1 3 zlmodzxzscm ⊢ ( ( 𝑖 ∈ ℤ ∧ 3 ∈ ℤ ∧ 6 ∈ ℤ ) → ( 𝑖 ∙ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ) = { ⟨ 0 , ( 𝑖 · 3 ) ⟩ , ⟨ 1 , ( 𝑖 · 6 ) ⟩ } )
56 52 54 55 mp3an23 ⊢ ( 𝑖 ∈ ℤ → ( 𝑖 ∙ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ) = { ⟨ 0 , ( 𝑖 · 3 ) ⟩ , ⟨ 1 , ( 𝑖 · 6 ) ⟩ } )
57 51 56 eqtrid ⊢ ( 𝑖 ∈ ℤ → ( 𝑖 ∙ 𝐴 ) = { ⟨ 0 , ( 𝑖 · 3 ) ⟩ , ⟨ 1 , ( 𝑖 · 6 ) ⟩ } )
58 6 a1i ⊢ ( 𝑖 ∈ ℤ → 𝐵 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } )
59 50 57 58 3netr4d ⊢ ( 𝑖 ∈ ℤ → ( 𝑖 ∙ 𝐴 ) ≠ 𝐵 )
60 ztprmneprm ⊢ ( ( 𝑖 ∈ ℤ ∧ 2 ∈ ℙ ∧ 3 ∈ ℙ ) → ( ( 𝑖 · 2 ) = 3 → 2 = 3 ) )
61 8 7 60 mp3an23 ⊢ ( 𝑖 ∈ ℤ → ( ( 𝑖 · 2 ) = 3 → 2 = 3 ) )
62 eqneqall ⊢ ( 2 = 3 → ( 2 ≠ 3 → ( 𝑖 · 2 ) ≠ 3 ) )
63 13 62 mpi ⊢ ( 2 = 3 → ( 𝑖 · 2 ) ≠ 3 )
64 61 63 syl6com ⊢ ( ( 𝑖 · 2 ) = 3 → ( 𝑖 ∈ ℤ → ( 𝑖 · 2 ) ≠ 3 ) )
65 ax-1 ⊢ ( ( 𝑖 · 2 ) ≠ 3 → ( 𝑖 ∈ ℤ → ( 𝑖 · 2 ) ≠ 3 ) )
66 64 65 pm2.61ine ⊢ ( 𝑖 ∈ ℤ → ( 𝑖 · 2 ) ≠ 3 )
67 66 olcd ⊢ ( 𝑖 ∈ ℤ → ( 0 ≠ 0 ∨ ( 𝑖 · 2 ) ≠ 3 ) )
68 ovex ⊢ ( 𝑖 · 2 ) ∈ V
69 21 68 pm3.2i ⊢ ( 0 ∈ V ∧ ( 𝑖 · 2 ) ∈ V )
70 opthneg ⊢ ( ( 0 ∈ V ∧ ( 𝑖 · 2 ) ∈ V ) → ( ⟨ 0 , ( 𝑖 · 2 ) ⟩ ≠ ⟨ 0 , 3 ⟩ ↔ ( 0 ≠ 0 ∨ ( 𝑖 · 2 ) ≠ 3 ) ) )
71 69 70 mp1i ⊢ ( 𝑖 ∈ ℤ → ( ⟨ 0 , ( 𝑖 · 2 ) ⟩ ≠ ⟨ 0 , 3 ⟩ ↔ ( 0 ≠ 0 ∨ ( 𝑖 · 2 ) ≠ 3 ) ) )
72 67 71 mpbird ⊢ ( 𝑖 ∈ ℤ → ⟨ 0 , ( 𝑖 · 2 ) ⟩ ≠ ⟨ 0 , 3 ⟩ )
73 28 orcd ⊢ ( 𝑖 ∈ ℤ → ( 0 ≠ 1 ∨ ( 𝑖 · 2 ) ≠ 6 ) )
74 opthneg ⊢ ( ( 0 ∈ V ∧ ( 𝑖 · 2 ) ∈ V ) → ( ⟨ 0 , ( 𝑖 · 2 ) ⟩ ≠ ⟨ 1 , 6 ⟩ ↔ ( 0 ≠ 1 ∨ ( 𝑖 · 2 ) ≠ 6 ) ) )
75 69 74 mp1i ⊢ ( 𝑖 ∈ ℤ → ( ⟨ 0 , ( 𝑖 · 2 ) ⟩ ≠ ⟨ 1 , 6 ⟩ ↔ ( 0 ≠ 1 ∨ ( 𝑖 · 2 ) ≠ 6 ) ) )
76 73 75 mpbird ⊢ ( 𝑖 ∈ ℤ → ⟨ 0 , ( 𝑖 · 2 ) ⟩ ≠ ⟨ 1 , 6 ⟩ )
77 72 76 jca ⊢ ( 𝑖 ∈ ℤ → ( ⟨ 0 , ( 𝑖 · 2 ) ⟩ ≠ ⟨ 0 , 3 ⟩ ∧ ⟨ 0 , ( 𝑖 · 2 ) ⟩ ≠ ⟨ 1 , 6 ⟩ ) )
78 77 orcd ⊢ ( 𝑖 ∈ ℤ → ( ( ⟨ 0 , ( 𝑖 · 2 ) ⟩ ≠ ⟨ 0 , 3 ⟩ ∧ ⟨ 0 , ( 𝑖 · 2 ) ⟩ ≠ ⟨ 1 , 6 ⟩ ) ∨ ( ⟨ 1 , ( 𝑖 · 4 ) ⟩ ≠ ⟨ 0 , 3 ⟩ ∧ ⟨ 1 , ( 𝑖 · 4 ) ⟩ ≠ ⟨ 1 , 6 ⟩ ) ) )
79 opex ⊢ ⟨ 0 , ( 𝑖 · 2 ) ⟩ ∈ V
80 opex ⊢ ⟨ 1 , ( 𝑖 · 4 ) ⟩ ∈ V
81 79 80 pm3.2i ⊢ ( ⟨ 0 , ( 𝑖 · 2 ) ⟩ ∈ V ∧ ⟨ 1 , ( 𝑖 · 4 ) ⟩ ∈ V )
82 81 a1i ⊢ ( 𝑖 ∈ ℤ → ( ⟨ 0 , ( 𝑖 · 2 ) ⟩ ∈ V ∧ ⟨ 1 , ( 𝑖 · 4 ) ⟩ ∈ V ) )
83 opex ⊢ ⟨ 0 , 3 ⟩ ∈ V
84 opex ⊢ ⟨ 1 , 6 ⟩ ∈ V
85 83 84 pm3.2i ⊢ ( ⟨ 0 , 3 ⟩ ∈ V ∧ ⟨ 1 , 6 ⟩ ∈ V )
86 85 a1i ⊢ ( 𝑖 ∈ ℤ → ( ⟨ 0 , 3 ⟩ ∈ V ∧ ⟨ 1 , 6 ⟩ ∈ V ) )
87 28 orcd ⊢ ( 𝑖 ∈ ℤ → ( 0 ≠ 1 ∨ ( 𝑖 · 2 ) ≠ ( 𝑖 · 4 ) ) )
88 opthneg ⊢ ( ( 0 ∈ V ∧ ( 𝑖 · 2 ) ∈ V ) → ( ⟨ 0 , ( 𝑖 · 2 ) ⟩ ≠ ⟨ 1 , ( 𝑖 · 4 ) ⟩ ↔ ( 0 ≠ 1 ∨ ( 𝑖 · 2 ) ≠ ( 𝑖 · 4 ) ) ) )
89 69 88 mp1i ⊢ ( 𝑖 ∈ ℤ → ( ⟨ 0 , ( 𝑖 · 2 ) ⟩ ≠ ⟨ 1 , ( 𝑖 · 4 ) ⟩ ↔ ( 0 ≠ 1 ∨ ( 𝑖 · 2 ) ≠ ( 𝑖 · 4 ) ) ) )
90 87 89 mpbird ⊢ ( 𝑖 ∈ ℤ → ⟨ 0 , ( 𝑖 · 2 ) ⟩ ≠ ⟨ 1 , ( 𝑖 · 4 ) ⟩ )
91 prnebg ⊢ ( ( ( ⟨ 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 ⟩ } ) )
92 91 bicomd ⊢ ( ( ( ⟨ 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 ⟩ ) ) ) )
93 82 86 90 92 syl3anc ⊢ ( 𝑖 ∈ ℤ → ( { ⟨ 0 , ( 𝑖 · 2 ) ⟩ , ⟨ 1 , ( 𝑖 · 4 ) ⟩ } ≠ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ↔ ( ( ⟨ 0 , ( 𝑖 · 2 ) ⟩ ≠ ⟨ 0 , 3 ⟩ ∧ ⟨ 0 , ( 𝑖 · 2 ) ⟩ ≠ ⟨ 1 , 6 ⟩ ) ∨ ( ⟨ 1 , ( 𝑖 · 4 ) ⟩ ≠ ⟨ 0 , 3 ⟩ ∧ ⟨ 1 , ( 𝑖 · 4 ) ⟩ ≠ ⟨ 1 , 6 ⟩ ) ) ) )
94 78 93 mpbird ⊢ ( 𝑖 ∈ ℤ → { ⟨ 0 , ( 𝑖 · 2 ) ⟩ , ⟨ 1 , ( 𝑖 · 4 ) ⟩ } ≠ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } )
95 6 oveq2i ⊢ ( 𝑖 ∙ 𝐵 ) = ( 𝑖 ∙ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } )
96 2z ⊢ 2 ∈ ℤ
97 4z ⊢ 4 ∈ ℤ
98 1 3 zlmodzxzscm ⊢ ( ( 𝑖 ∈ ℤ ∧ 2 ∈ ℤ ∧ 4 ∈ ℤ ) → ( 𝑖 ∙ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ) = { ⟨ 0 , ( 𝑖 · 2 ) ⟩ , ⟨ 1 , ( 𝑖 · 4 ) ⟩ } )
99 96 97 98 mp3an23 ⊢ ( 𝑖 ∈ ℤ → ( 𝑖 ∙ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ) = { ⟨ 0 , ( 𝑖 · 2 ) ⟩ , ⟨ 1 , ( 𝑖 · 4 ) ⟩ } )
100 95 99 eqtrid ⊢ ( 𝑖 ∈ ℤ → ( 𝑖 ∙ 𝐵 ) = { ⟨ 0 , ( 𝑖 · 2 ) ⟩ , ⟨ 1 , ( 𝑖 · 4 ) ⟩ } )
101 5 a1i ⊢ ( 𝑖 ∈ ℤ → 𝐴 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } )
102 94 100 101 3netr4d ⊢ ( 𝑖 ∈ ℤ → ( 𝑖 ∙ 𝐵 ) ≠ 𝐴 )
103 59 102 jca ⊢ ( 𝑖 ∈ ℤ → ( ( 𝑖 ∙ 𝐴 ) ≠ 𝐵 ∧ ( 𝑖 ∙ 𝐵 ) ≠ 𝐴 ) )
104 103 rgen ⊢ ∀ 𝑖 ∈ ℤ ( ( 𝑖 ∙ 𝐴 ) ≠ 𝐵 ∧ ( 𝑖 ∙ 𝐵 ) ≠ 𝐴 )