Theorem zlmodzxznm 42080

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
zlmodzxznm	⊢ ∀𝑖 ∈ ℤ ((𝑖 ∙ 𝐴) ≠ 𝐵 ∧ (𝑖 ∙ 𝐵) ≠ 𝐴)

Proof of Theorem zlmodzxznm

Step	Hyp	Ref	Expression
1		3prm 15244	. . . . . . . . . . . 12 ⊢ 3 ∈ ℙ
2		2prm 15243	. . . . . . . . . . . 12 ⊢ 2 ∈ ℙ
3		ztprmneprm 41918	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ ℤ ∧ 3 ∈ ℙ ∧ 2 ∈ ℙ) → ((𝑖 · 3) = 2 → 3 = 2))
4	1, 2, 3	mp3an23 1408	. . . . . . . . . . 11 ⊢ (𝑖 ∈ ℤ → ((𝑖 · 3) = 2 → 3 = 2))
5		2re 10967	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℝ
6		2lt3 11072	. . . . . . . . . . . . . 14 ⊢ 2 < 3
7	5, 6	ltneii 10029	. . . . . . . . . . . . 13 ⊢ 2 ≠ 3
8		eqneqall 2793	. . . . . . . . . . . . 13 ⊢ (2 = 3 → (2 ≠ 3 → (𝑖 · 3) ≠ 2))
9	7, 8	mpi 20	. . . . . . . . . . . 12 ⊢ (2 = 3 → (𝑖 · 3) ≠ 2)
10	9	eqcoms 2618	. . . . . . . . . . 11 ⊢ (3 = 2 → (𝑖 · 3) ≠ 2)
11	4, 10	syl6com 36	. . . . . . . . . 10 ⊢ ((𝑖 · 3) = 2 → (𝑖 ∈ ℤ → (𝑖 · 3) ≠ 2))
12		ax-1 6	. . . . . . . . . 10 ⊢ ((𝑖 · 3) ≠ 2 → (𝑖 ∈ ℤ → (𝑖 · 3) ≠ 2))
13	11, 12	pm2.61ine 2865	. . . . . . . . 9 ⊢ (𝑖 ∈ ℤ → (𝑖 · 3) ≠ 2)
14	13	olcd 407	. . . . . . . 8 ⊢ (𝑖 ∈ ℤ → (0 ≠ 0 ∨ (𝑖 · 3) ≠ 2))
15		c0ex 9913	. . . . . . . . . 10 ⊢ 0 ∈ V
16		ovex 6577	. . . . . . . . . 10 ⊢ (𝑖 · 3) ∈ V
17	15, 16	pm3.2i 470	. . . . . . . . 9 ⊢ (0 ∈ V ∧ (𝑖 · 3) ∈ V)
18		opthneg 4876	. . . . . . . . 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 246	. . . . . . 7 ⊢ (𝑖 ∈ ℤ → ⟨0, (𝑖 · 3)⟩ ≠ ⟨0, 2⟩)
21		0ne1 10965	. . . . . . . . . 10 ⊢ 0 ≠ 1
22	21	a1i 11	. . . . . . . . 9 ⊢ (𝑖 ∈ ℤ → 0 ≠ 1)
23	22	orcd 406	. . . . . . . 8 ⊢ (𝑖 ∈ ℤ → (0 ≠ 1 ∨ (𝑖 · 3) ≠ 4))
24		opthneg 4876	. . . . . . . . 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 246	. . . . . . 7 ⊢ (𝑖 ∈ ℤ → ⟨0, (𝑖 · 3)⟩ ≠ ⟨1, 4⟩)
27	20, 26	jca 553	. . . . . 6 ⊢ (𝑖 ∈ ℤ → (⟨0, (𝑖 · 3)⟩ ≠ ⟨0, 2⟩ ∧ ⟨0, (𝑖 · 3)⟩ ≠ ⟨1, 4⟩))
28	27	orcd 406	. . . . 5 ⊢ (𝑖 ∈ ℤ → ((⟨0, (𝑖 · 3)⟩ ≠ ⟨0, 2⟩ ∧ ⟨0, (𝑖 · 3)⟩ ≠ ⟨1, 4⟩) ∨ (⟨1, (𝑖 · 6)⟩ ≠ ⟨0, 2⟩ ∧ ⟨1, (𝑖 · 6)⟩ ≠ ⟨1, 4⟩)))
29		opex 4859	. . . . . . . 8 ⊢ ⟨0, (𝑖 · 3)⟩ ∈ V
30		opex 4859	. . . . . . . 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 4859	. . . . . . . 8 ⊢ ⟨0, 2⟩ ∈ V
34		opex 4859	. . . . . . . 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 406	. . . . . . 7 ⊢ (𝑖 ∈ ℤ → (0 ≠ 1 ∨ (𝑖 · 3) ≠ (𝑖 · 6)))
38		opthneg 4876	. . . . . . . 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 246	. . . . . 6 ⊢ (𝑖 ∈ ℤ → ⟨0, (𝑖 · 3)⟩ ≠ ⟨1, (𝑖 · 6)⟩)
41		prnebg 4329	. . . . . . 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 212	. . . . . 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 1318	. . . . 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 246	. . . 4 ⊢ (𝑖 ∈ ℤ → {⟨0, (𝑖 · 3)⟩, ⟨1, (𝑖 · 6)⟩} ≠ {⟨0, 2⟩, ⟨1, 4⟩})
45		zlmodzxzequa.a	. . . . . 6 ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}
46	45	oveq2i 6560	. . . . 5 ⊢ (𝑖 ∙ 𝐴) = (𝑖 ∙ {⟨0, 3⟩, ⟨1, 6⟩})
47		3z 11287	. . . . . 6 ⊢ 3 ∈ ℤ
48		6nn 11066	. . . . . . 7 ⊢ 6 ∈ ℕ
49	48	nnzi 11278	. . . . . 6 ⊢ 6 ∈ ℤ
50		zlmodzxzequa.z	. . . . . . 7 ⊢ 𝑍 = (ℤring freeLMod {0, 1})
51		zlmodzxzequa.t	. . . . . . 7 ⊢ ∙ = ( ·𝑠 ‘𝑍)
52	50, 51	zlmodzxzscm 41928	. . . . . 6 ⊢ ((𝑖 ∈ ℤ ∧ 3 ∈ ℤ ∧ 6 ∈ ℤ) → (𝑖 ∙ {⟨0, 3⟩, ⟨1, 6⟩}) = {⟨0, (𝑖 · 3)⟩, ⟨1, (𝑖 · 6)⟩})
53	47, 49, 52	mp3an23 1408	. . . . 5 ⊢ (𝑖 ∈ ℤ → (𝑖 ∙ {⟨0, 3⟩, ⟨1, 6⟩}) = {⟨0, (𝑖 · 3)⟩, ⟨1, (𝑖 · 6)⟩})
54	46, 53	syl5eq 2656	. . . 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 2859	. . 3 ⊢ (𝑖 ∈ ℤ → (𝑖 ∙ 𝐴) ≠ 𝐵)
58		ztprmneprm 41918	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ ℤ ∧ 2 ∈ ℙ ∧ 3 ∈ ℙ) → ((𝑖 · 2) = 3 → 2 = 3))
59	2, 1, 58	mp3an23 1408	. . . . . . . . . . 11 ⊢ (𝑖 ∈ ℤ → ((𝑖 · 2) = 3 → 2 = 3))
60		eqneqall 2793	. . . . . . . . . . . 12 ⊢ (2 = 3 → (2 ≠ 3 → (𝑖 · 2) ≠ 3))
61	7, 60	mpi 20	. . . . . . . . . . 11 ⊢ (2 = 3 → (𝑖 · 2) ≠ 3)
62	59, 61	syl6com 36	. . . . . . . . . 10 ⊢ ((𝑖 · 2) = 3 → (𝑖 ∈ ℤ → (𝑖 · 2) ≠ 3))
63		ax-1 6	. . . . . . . . . 10 ⊢ ((𝑖 · 2) ≠ 3 → (𝑖 ∈ ℤ → (𝑖 · 2) ≠ 3))
64	62, 63	pm2.61ine 2865	. . . . . . . . 9 ⊢ (𝑖 ∈ ℤ → (𝑖 · 2) ≠ 3)
65	64	olcd 407	. . . . . . . 8 ⊢ (𝑖 ∈ ℤ → (0 ≠ 0 ∨ (𝑖 · 2) ≠ 3))
66		ovex 6577	. . . . . . . . . 10 ⊢ (𝑖 · 2) ∈ V
67	15, 66	pm3.2i 470	. . . . . . . . 9 ⊢ (0 ∈ V ∧ (𝑖 · 2) ∈ V)
68		opthneg 4876	. . . . . . . . 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 246	. . . . . . 7 ⊢ (𝑖 ∈ ℤ → ⟨0, (𝑖 · 2)⟩ ≠ ⟨0, 3⟩)
71	22	orcd 406	. . . . . . . 8 ⊢ (𝑖 ∈ ℤ → (0 ≠ 1 ∨ (𝑖 · 2) ≠ 6))
72		opthneg 4876	. . . . . . . . 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 246	. . . . . . 7 ⊢ (𝑖 ∈ ℤ → ⟨0, (𝑖 · 2)⟩ ≠ ⟨1, 6⟩)
75	70, 74	jca 553	. . . . . 6 ⊢ (𝑖 ∈ ℤ → (⟨0, (𝑖 · 2)⟩ ≠ ⟨0, 3⟩ ∧ ⟨0, (𝑖 · 2)⟩ ≠ ⟨1, 6⟩))
76	75	orcd 406	. . . . 5 ⊢ (𝑖 ∈ ℤ → ((⟨0, (𝑖 · 2)⟩ ≠ ⟨0, 3⟩ ∧ ⟨0, (𝑖 · 2)⟩ ≠ ⟨1, 6⟩) ∨ (⟨1, (𝑖 · 4)⟩ ≠ ⟨0, 3⟩ ∧ ⟨1, (𝑖 · 4)⟩ ≠ ⟨1, 6⟩)))
77		opex 4859	. . . . . . . 8 ⊢ ⟨0, (𝑖 · 2)⟩ ∈ V
78		opex 4859	. . . . . . . 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 4859	. . . . . . . 8 ⊢ ⟨0, 3⟩ ∈ V
82		opex 4859	. . . . . . . 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 406	. . . . . . 7 ⊢ (𝑖 ∈ ℤ → (0 ≠ 1 ∨ (𝑖 · 2) ≠ (𝑖 · 4)))
86		opthneg 4876	. . . . . . . 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 246	. . . . . 6 ⊢ (𝑖 ∈ ℤ → ⟨0, (𝑖 · 2)⟩ ≠ ⟨1, (𝑖 · 4)⟩)
89		prnebg 4329	. . . . . . 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 212	. . . . . 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 1318	. . . . 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 246	. . . 4 ⊢ (𝑖 ∈ ℤ → {⟨0, (𝑖 · 2)⟩, ⟨1, (𝑖 · 4)⟩} ≠ {⟨0, 3⟩, ⟨1, 6⟩})
93	55	oveq2i 6560	. . . . 5 ⊢ (𝑖 ∙ 𝐵) = (𝑖 ∙ {⟨0, 2⟩, ⟨1, 4⟩})
94		2z 11286	. . . . . 6 ⊢ 2 ∈ ℤ
95		4z 11288	. . . . . 6 ⊢ 4 ∈ ℤ
96	50, 51	zlmodzxzscm 41928	. . . . . 6 ⊢ ((𝑖 ∈ ℤ ∧ 2 ∈ ℤ ∧ 4 ∈ ℤ) → (𝑖 ∙ {⟨0, 2⟩, ⟨1, 4⟩}) = {⟨0, (𝑖 · 2)⟩, ⟨1, (𝑖 · 4)⟩})
97	94, 95, 96	mp3an23 1408	. . . . 5 ⊢ (𝑖 ∈ ℤ → (𝑖 ∙ {⟨0, 2⟩, ⟨1, 4⟩}) = {⟨0, (𝑖 · 2)⟩, ⟨1, (𝑖 · 4)⟩})
98	93, 97	syl5eq 2656	. . . 4 ⊢ (𝑖 ∈ ℤ → (𝑖 ∙ 𝐵) = {⟨0, (𝑖 · 2)⟩, ⟨1, (𝑖 · 4)⟩})
99	45	a1i 11	. . . 4 ⊢ (𝑖 ∈ ℤ → 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩})
100	92, 98, 99	3netr4d 2859	. . 3 ⊢ (𝑖 ∈ ℤ → (𝑖 ∙ 𝐵) ≠ 𝐴)
101	57, 100	jca 553	. 2 ⊢ (𝑖 ∈ ℤ → ((𝑖 ∙ 𝐴) ≠ 𝐵 ∧ (𝑖 ∙ 𝐵) ≠ 𝐴))
102	101	rgen 2906	1 ⊢ ∀𝑖 ∈ ℤ ((𝑖 ∙ 𝐴) ≠ 𝐵 ∧ (𝑖 ∙ 𝐵) ≠ 𝐴)

Syntax hints:   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  Vcvv 3173  {cpr 4127  ⟨cop 4131  ‘cfv 5804  (class class class)co 6549  0cc0 9815  1c1 9816   · cmul 9820  2c2 10947  3c3 10948  4c4 10949  6c6 10951  ℤcz 11254  ℙcprime 15223   ·_𝑠 cvsca 15772  -_gcsg 17247  ℤ_ringzring 19637   freeLMod cfrlm 19909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-rp 11709  df-fz 12198  df-seq 12664  df-exp 12723  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-dvds 14822  df-prm 15224  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-hom 15793  df-cco 15794  df-0g 15925  df-prds 15931  df-pws 15933  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-grp 17248  df-minusg 17249  df-subg 17414  df-cmn 18018  df-mgp 18313  df-ur 18325  df-ring 18372  df-cring 18373  df-subrg 18601  df-sra 18993  df-rgmod 18994  df-cnfld 19568  df-zring 19638  df-dsmm 19895  df-frlm 19910

This theorem is referenced by:  ldepsnlinclem1  42088  ldepsnlinclem2  42089