Theorem zlmodzxznm 32808

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

Hypotheses

Ref	Expression
zlmodzxzequa.z	|- Z = (ℤring freeLMod { 0 , 1 } )
zlmodzxzequa.o	|- .0. = { <. 0 , 0 >. , <. 1 , 0 >. }
zlmodzxzequa.t	|- .xb = ( .s ` Z )
zlmodzxzequa.m	|- .- = ( -g ` Z )
zlmodzxzequa.a	|- A = { <. 0 , 3 >. , <. 1 , 6 >. }
zlmodzxzequa.b	|- B = { <. 0 , 2 >. , <. 1 , 4 >. }

Assertion

Ref	Expression
zlmodzxznm	|- A. i e. ZZ ( ( i .xb A ) =/= B /\ ( i .xb B ) =/= A )

Proof of Theorem zlmodzxznm

Step	Hyp	Ref	Expression
1		3prm 14106	. . . . . . . . . . . 12 |- 3 e. Prime
2		2prm 14105	. . . . . . . . . . . 12 |- 2 e. Prime
3		ztprmneprm 32644	. . . . . . . . . . . 12 |- ( ( i e. ZZ /\ 3 e. Prime /\ 2 e. Prime ) -> ( ( i x. 3 ) = 2 -> 3 = 2 ) )
4	1, 2, 3	mp3an23 1315	. . . . . . . . . . 11 |- ( i e. ZZ -> ( ( i x. 3 ) = 2 -> 3 = 2 ) )
5		2re 10606	. . . . . . . . . . . . . 14 |- 2 e. RR
6		2lt3 10704	. . . . . . . . . . . . . 14 |- 2 < 3
7	5, 6	ltneii 9695	. . . . . . . . . . . . 13 |- 2 =/= 3
8		eqneqall 2648	. . . . . . . . . . . . 13 |- ( 2 = 3 -> ( 2 =/= 3 -> ( i x. 3 ) =/= 2 ) )
9	7, 8	mpi 17	. . . . . . . . . . . 12 |- ( 2 = 3 -> ( i x. 3 ) =/= 2 )
10	9	eqcoms 2453	. . . . . . . . . . 11 |- ( 3 = 2 -> ( i x. 3 ) =/= 2 )
11	4, 10	syl6com 35	. . . . . . . . . 10 |- ( ( i x. 3 ) = 2 -> ( i e. ZZ -> ( i x. 3 ) =/= 2 ) )
12		ax-1 6	. . . . . . . . . 10 |- ( ( i x. 3 ) =/= 2 -> ( i e. ZZ -> ( i x. 3 ) =/= 2 ) )
13	11, 12	pm2.61ine 2754	. . . . . . . . 9 |- ( i e. ZZ -> ( i x. 3 ) =/= 2 )
14	13	olcd 393	. . . . . . . 8 |- ( i e. ZZ -> ( 0 =/= 0 \/ ( i x. 3 ) =/= 2 ) )
15		c0ex 9588	. . . . . . . . . 10 |- 0 e. _V
16		ovex 6305	. . . . . . . . . 10 |- ( i x. 3 ) e. _V
17	15, 16	pm3.2i 455	. . . . . . . . 9 |- ( 0 e. _V /\ ( i x. 3 ) e. _V )
18		opthneg 4712	. . . . . . . . 9 |- ( ( 0 e. _V /\ ( i x. 3 ) e. _V ) -> ( <. 0 , ( i x. 3 ) >. =/= <. 0 , 2 >. <-> ( 0 =/= 0 \/ ( i x. 3 ) =/= 2 ) ) )
19	17, 18	mp1i 12	. . . . . . . 8 |- ( i e. ZZ -> ( <. 0 , ( i x. 3 ) >. =/= <. 0 , 2 >. <-> ( 0 =/= 0 \/ ( i x. 3 ) =/= 2 ) ) )
20	14, 19	mpbird 232	. . . . . . 7 |- ( i e. ZZ -> <. 0 , ( i x. 3 ) >. =/= <. 0 , 2 >. )
21		0ne1 10604	. . . . . . . . . 10 |- 0 =/= 1
22	21	a1i 11	. . . . . . . . 9 |- ( i e. ZZ -> 0 =/= 1 )
23	22	orcd 392	. . . . . . . 8 |- ( i e. ZZ -> ( 0 =/= 1 \/ ( i x. 3 ) =/= 4 ) )
24		opthneg 4712	. . . . . . . . 9 |- ( ( 0 e. _V /\ ( i x. 3 ) e. _V ) -> ( <. 0 , ( i x. 3 ) >. =/= <. 1 , 4 >. <-> ( 0 =/= 1 \/ ( i x. 3 ) =/= 4 ) ) )
25	17, 24	mp1i 12	. . . . . . . 8 |- ( i e. ZZ -> ( <. 0 , ( i x. 3 ) >. =/= <. 1 , 4 >. <-> ( 0 =/= 1 \/ ( i x. 3 ) =/= 4 ) ) )
26	23, 25	mpbird 232	. . . . . . 7 |- ( i e. ZZ -> <. 0 , ( i x. 3 ) >. =/= <. 1 , 4 >. )
27	20, 26	jca 532	. . . . . 6 |- ( i e. ZZ -> ( <. 0 , ( i x. 3 ) >. =/= <. 0 , 2 >. /\ <. 0 , ( i x. 3 ) >. =/= <. 1 , 4 >. ) )
28	27	orcd 392	. . . . 5 |- ( i e. ZZ -> ( ( <. 0 , ( i x. 3 ) >. =/= <. 0 , 2 >. /\ <. 0 , ( i x. 3 ) >. =/= <. 1 , 4 >. ) \/ ( <. 1 , ( i x. 6 ) >. =/= <. 0 , 2 >. /\ <. 1 , ( i x. 6 ) >. =/= <. 1 , 4 >. ) ) )
29		opex 4697	. . . . . . . 8 |- <. 0 , ( i x. 3 ) >. e. _V
30		opex 4697	. . . . . . . 8 |- <. 1 , ( i x. 6 ) >. e. _V
31	29, 30	pm3.2i 455	. . . . . . 7 |- ( <. 0 , ( i x. 3 ) >. e. _V /\ <. 1 , ( i x. 6 ) >. e. _V )
32	31	a1i 11	. . . . . 6 |- ( i e. ZZ -> ( <. 0 , ( i x. 3 ) >. e. _V /\ <. 1 , ( i x. 6 ) >. e. _V ) )
33		opex 4697	. . . . . . . 8 |- <. 0 , 2 >. e. _V
34		opex 4697	. . . . . . . 8 |- <. 1 , 4 >. e. _V
35	33, 34	pm3.2i 455	. . . . . . 7 |- ( <. 0 , 2 >. e. _V /\ <. 1 , 4 >. e. _V )
36	35	a1i 11	. . . . . 6 |- ( i e. ZZ -> ( <. 0 , 2 >. e. _V /\ <. 1 , 4 >. e. _V ) )
37	22	orcd 392	. . . . . . 7 |- ( i e. ZZ -> ( 0 =/= 1 \/ ( i x. 3 ) =/= ( i x. 6 ) ) )
38		opthneg 4712	. . . . . . . 8 |- ( ( 0 e. _V /\ ( i x. 3 ) e. _V ) -> ( <. 0 , ( i x. 3 ) >. =/= <. 1 , ( i x. 6 ) >. <-> ( 0 =/= 1 \/ ( i x. 3 ) =/= ( i x. 6 ) ) ) )
39	17, 38	mp1i 12	. . . . . . 7 |- ( i e. ZZ -> ( <. 0 , ( i x. 3 ) >. =/= <. 1 , ( i x. 6 ) >. <-> ( 0 =/= 1 \/ ( i x. 3 ) =/= ( i x. 6 ) ) ) )
40	37, 39	mpbird 232	. . . . . 6 |- ( i e. ZZ -> <. 0 , ( i x. 3 ) >. =/= <. 1 , ( i x. 6 ) >. )
41		prnebg 4193	. . . . . . 7 |- ( ( ( <. 0 , ( i x. 3 ) >. e. _V /\ <. 1 , ( i x. 6 ) >. e. _V ) /\ ( <. 0 , 2 >. e. _V /\ <. 1 , 4 >. e. _V ) /\ <. 0 , ( i x. 3 ) >. =/= <. 1 , ( i x. 6 ) >. ) -> ( ( ( <. 0 , ( i x. 3 ) >. =/= <. 0 , 2 >. /\ <. 0 , ( i x. 3 ) >. =/= <. 1 , 4 >. ) \/ ( <. 1 , ( i x. 6 ) >. =/= <. 0 , 2 >. /\ <. 1 , ( i x. 6 ) >. =/= <. 1 , 4 >. ) ) <-> { <. 0 , ( i x. 3 ) >. , <. 1 , ( i x. 6 ) >. } =/= { <. 0 , 2 >. , <. 1 , 4 >. } ) )
42	41	bicomd 201	. . . . . 6 |- ( ( ( <. 0 , ( i x. 3 ) >. e. _V /\ <. 1 , ( i x. 6 ) >. e. _V ) /\ ( <. 0 , 2 >. e. _V /\ <. 1 , 4 >. e. _V ) /\ <. 0 , ( i x. 3 ) >. =/= <. 1 , ( i x. 6 ) >. ) -> ( { <. 0 , ( i x. 3 ) >. , <. 1 , ( i x. 6 ) >. } =/= { <. 0 , 2 >. , <. 1 , 4 >. } <-> ( ( <. 0 , ( i x. 3 ) >. =/= <. 0 , 2 >. /\ <. 0 , ( i x. 3 ) >. =/= <. 1 , 4 >. ) \/ ( <. 1 , ( i x. 6 ) >. =/= <. 0 , 2 >. /\ <. 1 , ( i x. 6 ) >. =/= <. 1 , 4 >. ) ) ) )
43	32, 36, 40, 42	syl3anc 1227	. . . . 5 |- ( i e. ZZ -> ( { <. 0 , ( i x. 3 ) >. , <. 1 , ( i x. 6 ) >. } =/= { <. 0 , 2 >. , <. 1 , 4 >. } <-> ( ( <. 0 , ( i x. 3 ) >. =/= <. 0 , 2 >. /\ <. 0 , ( i x. 3 ) >. =/= <. 1 , 4 >. ) \/ ( <. 1 , ( i x. 6 ) >. =/= <. 0 , 2 >. /\ <. 1 , ( i x. 6 ) >. =/= <. 1 , 4 >. ) ) ) )
44	28, 43	mpbird 232	. . . 4 |- ( i e. ZZ -> { <. 0 , ( i x. 3 ) >. , <. 1 , ( i x. 6 ) >. } =/= { <. 0 , 2 >. , <. 1 , 4 >. } )
45		zlmodzxzequa.a	. . . . . 6 |- A = { <. 0 , 3 >. , <. 1 , 6 >. }
46	45	oveq2i 6288	. . . . 5 |- ( i .xb A ) = ( i .xb { <. 0 , 3 >. , <. 1 , 6 >. } )
47		3z 10898	. . . . . 6 |- 3 e. ZZ
48		6nn 10698	. . . . . . 7 |- 6 e. NN
49	48	nnzi 10889	. . . . . 6 |- 6 e. ZZ
50		zlmodzxzequa.z	. . . . . . 7 |- Z = (ℤring freeLMod { 0 , 1 } )
51		zlmodzxzequa.t	. . . . . . 7 |- .xb = ( .s ` Z )
52	50, 51	zlmodzxzscm 32654	. . . . . 6 |- ( ( i e. ZZ /\ 3 e. ZZ /\ 6 e. ZZ ) -> ( i .xb { <. 0 , 3 >. , <. 1 , 6 >. } ) = { <. 0 , ( i x. 3 ) >. , <. 1 , ( i x. 6 ) >. } )
53	47, 49, 52	mp3an23 1315	. . . . 5 |- ( i e. ZZ -> ( i .xb { <. 0 , 3 >. , <. 1 , 6 >. } ) = { <. 0 , ( i x. 3 ) >. , <. 1 , ( i x. 6 ) >. } )
54	46, 53	syl5eq 2494	. . . 4 |- ( i e. ZZ -> ( i .xb A ) = { <. 0 , ( i x. 3 ) >. , <. 1 , ( i x. 6 ) >. } )
55		zlmodzxzequa.b	. . . . 5 |- B = { <. 0 , 2 >. , <. 1 , 4 >. }
56	55	a1i 11	. . . 4 |- ( i e. ZZ -> B = { <. 0 , 2 >. , <. 1 , 4 >. } )
57	44, 54, 56	3netr4d 2746	. . 3 |- ( i e. ZZ -> ( i .xb A ) =/= B )
58		ztprmneprm 32644	. . . . . . . . . . . 12 |- ( ( i e. ZZ /\ 2 e. Prime /\ 3 e. Prime ) -> ( ( i x. 2 ) = 3 -> 2 = 3 ) )
59	2, 1, 58	mp3an23 1315	. . . . . . . . . . 11 |- ( i e. ZZ -> ( ( i x. 2 ) = 3 -> 2 = 3 ) )
60		eqneqall 2648	. . . . . . . . . . . 12 |- ( 2 = 3 -> ( 2 =/= 3 -> ( i x. 2 ) =/= 3 ) )
61	7, 60	mpi 17	. . . . . . . . . . 11 |- ( 2 = 3 -> ( i x. 2 ) =/= 3 )
62	59, 61	syl6com 35	. . . . . . . . . 10 |- ( ( i x. 2 ) = 3 -> ( i e. ZZ -> ( i x. 2 ) =/= 3 ) )
63		ax-1 6	. . . . . . . . . 10 |- ( ( i x. 2 ) =/= 3 -> ( i e. ZZ -> ( i x. 2 ) =/= 3 ) )
64	62, 63	pm2.61ine 2754	. . . . . . . . 9 |- ( i e. ZZ -> ( i x. 2 ) =/= 3 )
65	64	olcd 393	. . . . . . . 8 |- ( i e. ZZ -> ( 0 =/= 0 \/ ( i x. 2 ) =/= 3 ) )
66		ovex 6305	. . . . . . . . . 10 |- ( i x. 2 ) e. _V
67	15, 66	pm3.2i 455	. . . . . . . . 9 |- ( 0 e. _V /\ ( i x. 2 ) e. _V )
68		opthneg 4712	. . . . . . . . 9 |- ( ( 0 e. _V /\ ( i x. 2 ) e. _V ) -> ( <. 0 , ( i x. 2 ) >. =/= <. 0 , 3 >. <-> ( 0 =/= 0 \/ ( i x. 2 ) =/= 3 ) ) )
69	67, 68	mp1i 12	. . . . . . . 8 |- ( i e. ZZ -> ( <. 0 , ( i x. 2 ) >. =/= <. 0 , 3 >. <-> ( 0 =/= 0 \/ ( i x. 2 ) =/= 3 ) ) )
70	65, 69	mpbird 232	. . . . . . 7 |- ( i e. ZZ -> <. 0 , ( i x. 2 ) >. =/= <. 0 , 3 >. )
71	22	orcd 392	. . . . . . . 8 |- ( i e. ZZ -> ( 0 =/= 1 \/ ( i x. 2 ) =/= 6 ) )
72		opthneg 4712	. . . . . . . . 9 |- ( ( 0 e. _V /\ ( i x. 2 ) e. _V ) -> ( <. 0 , ( i x. 2 ) >. =/= <. 1 , 6 >. <-> ( 0 =/= 1 \/ ( i x. 2 ) =/= 6 ) ) )
73	67, 72	mp1i 12	. . . . . . . 8 |- ( i e. ZZ -> ( <. 0 , ( i x. 2 ) >. =/= <. 1 , 6 >. <-> ( 0 =/= 1 \/ ( i x. 2 ) =/= 6 ) ) )
74	71, 73	mpbird 232	. . . . . . 7 |- ( i e. ZZ -> <. 0 , ( i x. 2 ) >. =/= <. 1 , 6 >. )
75	70, 74	jca 532	. . . . . 6 |- ( i e. ZZ -> ( <. 0 , ( i x. 2 ) >. =/= <. 0 , 3 >. /\ <. 0 , ( i x. 2 ) >. =/= <. 1 , 6 >. ) )
76	75	orcd 392	. . . . 5 |- ( i e. ZZ -> ( ( <. 0 , ( i x. 2 ) >. =/= <. 0 , 3 >. /\ <. 0 , ( i x. 2 ) >. =/= <. 1 , 6 >. ) \/ ( <. 1 , ( i x. 4 ) >. =/= <. 0 , 3 >. /\ <. 1 , ( i x. 4 ) >. =/= <. 1 , 6 >. ) ) )
77		opex 4697	. . . . . . . 8 |- <. 0 , ( i x. 2 ) >. e. _V
78		opex 4697	. . . . . . . 8 |- <. 1 , ( i x. 4 ) >. e. _V
79	77, 78	pm3.2i 455	. . . . . . 7 |- ( <. 0 , ( i x. 2 ) >. e. _V /\ <. 1 , ( i x. 4 ) >. e. _V )
80	79	a1i 11	. . . . . 6 |- ( i e. ZZ -> ( <. 0 , ( i x. 2 ) >. e. _V /\ <. 1 , ( i x. 4 ) >. e. _V ) )
81		opex 4697	. . . . . . . 8 |- <. 0 , 3 >. e. _V
82		opex 4697	. . . . . . . 8 |- <. 1 , 6 >. e. _V
83	81, 82	pm3.2i 455	. . . . . . 7 |- ( <. 0 , 3 >. e. _V /\ <. 1 , 6 >. e. _V )
84	83	a1i 11	. . . . . 6 |- ( i e. ZZ -> ( <. 0 , 3 >. e. _V /\ <. 1 , 6 >. e. _V ) )
85	22	orcd 392	. . . . . . 7 |- ( i e. ZZ -> ( 0 =/= 1 \/ ( i x. 2 ) =/= ( i x. 4 ) ) )
86		opthneg 4712	. . . . . . . 8 |- ( ( 0 e. _V /\ ( i x. 2 ) e. _V ) -> ( <. 0 , ( i x. 2 ) >. =/= <. 1 , ( i x. 4 ) >. <-> ( 0 =/= 1 \/ ( i x. 2 ) =/= ( i x. 4 ) ) ) )
87	67, 86	mp1i 12	. . . . . . 7 |- ( i e. ZZ -> ( <. 0 , ( i x. 2 ) >. =/= <. 1 , ( i x. 4 ) >. <-> ( 0 =/= 1 \/ ( i x. 2 ) =/= ( i x. 4 ) ) ) )
88	85, 87	mpbird 232	. . . . . 6 |- ( i e. ZZ -> <. 0 , ( i x. 2 ) >. =/= <. 1 , ( i x. 4 ) >. )
89		prnebg 4193	. . . . . . 7 |- ( ( ( <. 0 , ( i x. 2 ) >. e. _V /\ <. 1 , ( i x. 4 ) >. e. _V ) /\ ( <. 0 , 3 >. e. _V /\ <. 1 , 6 >. e. _V ) /\ <. 0 , ( i x. 2 ) >. =/= <. 1 , ( i x. 4 ) >. ) -> ( ( ( <. 0 , ( i x. 2 ) >. =/= <. 0 , 3 >. /\ <. 0 , ( i x. 2 ) >. =/= <. 1 , 6 >. ) \/ ( <. 1 , ( i x. 4 ) >. =/= <. 0 , 3 >. /\ <. 1 , ( i x. 4 ) >. =/= <. 1 , 6 >. ) ) <-> { <. 0 , ( i x. 2 ) >. , <. 1 , ( i x. 4 ) >. } =/= { <. 0 , 3 >. , <. 1 , 6 >. } ) )
90	89	bicomd 201	. . . . . 6 |- ( ( ( <. 0 , ( i x. 2 ) >. e. _V /\ <. 1 , ( i x. 4 ) >. e. _V ) /\ ( <. 0 , 3 >. e. _V /\ <. 1 , 6 >. e. _V ) /\ <. 0 , ( i x. 2 ) >. =/= <. 1 , ( i x. 4 ) >. ) -> ( { <. 0 , ( i x. 2 ) >. , <. 1 , ( i x. 4 ) >. } =/= { <. 0 , 3 >. , <. 1 , 6 >. } <-> ( ( <. 0 , ( i x. 2 ) >. =/= <. 0 , 3 >. /\ <. 0 , ( i x. 2 ) >. =/= <. 1 , 6 >. ) \/ ( <. 1 , ( i x. 4 ) >. =/= <. 0 , 3 >. /\ <. 1 , ( i x. 4 ) >. =/= <. 1 , 6 >. ) ) ) )
91	80, 84, 88, 90	syl3anc 1227	. . . . 5 |- ( i e. ZZ -> ( { <. 0 , ( i x. 2 ) >. , <. 1 , ( i x. 4 ) >. } =/= { <. 0 , 3 >. , <. 1 , 6 >. } <-> ( ( <. 0 , ( i x. 2 ) >. =/= <. 0 , 3 >. /\ <. 0 , ( i x. 2 ) >. =/= <. 1 , 6 >. ) \/ ( <. 1 , ( i x. 4 ) >. =/= <. 0 , 3 >. /\ <. 1 , ( i x. 4 ) >. =/= <. 1 , 6 >. ) ) ) )
92	76, 91	mpbird 232	. . . 4 |- ( i e. ZZ -> { <. 0 , ( i x. 2 ) >. , <. 1 , ( i x. 4 ) >. } =/= { <. 0 , 3 >. , <. 1 , 6 >. } )
93	55	oveq2i 6288	. . . . 5 |- ( i .xb B ) = ( i .xb { <. 0 , 2 >. , <. 1 , 4 >. } )
94		2z 10897	. . . . . 6 |- 2 e. ZZ
95		4nn 10696	. . . . . . 7 |- 4 e. NN
96	95	nnzi 10889	. . . . . 6 |- 4 e. ZZ
97	50, 51	zlmodzxzscm 32654	. . . . . 6 |- ( ( i e. ZZ /\ 2 e. ZZ /\ 4 e. ZZ ) -> ( i .xb { <. 0 , 2 >. , <. 1 , 4 >. } ) = { <. 0 , ( i x. 2 ) >. , <. 1 , ( i x. 4 ) >. } )
98	94, 96, 97	mp3an23 1315	. . . . 5 |- ( i e. ZZ -> ( i .xb { <. 0 , 2 >. , <. 1 , 4 >. } ) = { <. 0 , ( i x. 2 ) >. , <. 1 , ( i x. 4 ) >. } )
99	93, 98	syl5eq 2494	. . . 4 |- ( i e. ZZ -> ( i .xb B ) = { <. 0 , ( i x. 2 ) >. , <. 1 , ( i x. 4 ) >. } )
100	45	a1i 11	. . . 4 |- ( i e. ZZ -> A = { <. 0 , 3 >. , <. 1 , 6 >. } )
101	92, 99, 100	3netr4d 2746	. . 3 |- ( i e. ZZ -> ( i .xb B ) =/= A )
102	57, 101	jca 532	. 2 |- ( i e. ZZ -> ( ( i .xb A ) =/= B /\ ( i .xb B ) =/= A ) )
103	102	rgen 2801	1 |- A. i e. ZZ ( ( i .xb A ) =/= B /\ ( i .xb B ) =/= A )

Syntax hints:   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   /\ w3a 972   = wceq 1381   e. wcel 1802   =/= wne 2636   A.wral 2791   _Vcvv 3093   {cpr 4012   <.cop 4016   ` cfv 5574  (class class class)co 6277   0cc0 9490   1c1 9491   x. cmul 9495   2c2 10586   3c3 10587   4c4 10588   6c6 10590   ZZcz 10865   Primecprime 14089   .scvsca 14573   -gcsg 15924  ℤ_ringzring 18356   freeLMod cfrlm 18644

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-rep 4544  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567  ax-pre-sup 9568  ax-addf 9569  ax-mulf 9570

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-uni 4231  df-int 4268  df-iun 4313  df-br 4434  df-opab 4492  df-mpt 4493  df-tr 4527  df-eprel 4777  df-id 4781  df-po 4786  df-so 4787  df-fr 4824  df-we 4826  df-ord 4867  df-on 4868  df-lim 4869  df-suc 4870  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-riota 6238  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-of 6521  df-om 6682  df-1st 6781  df-2nd 6782  df-supp 6900  df-recs 7040  df-rdg 7074  df-1o 7128  df-2o 7129  df-oadd 7132  df-er 7309  df-map 7420  df-ixp 7468  df-en 7515  df-dom 7516  df-sdom 7517  df-fin 7518  df-fsupp 7828  df-sup 7899  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9807  df-neg 9808  df-div 10208  df-nn 10538  df-2 10595  df-3 10596  df-4 10597  df-5 10598  df-6 10599  df-7 10600  df-8 10601  df-9 10602  df-10 10603  df-n0 10797  df-z 10866  df-dec 10980  df-uz 11086  df-rp 11225  df-fz 11677  df-seq 12082  df-exp 12141  df-cj 12906  df-re 12907  df-im 12908  df-sqrt 13042  df-abs 13043  df-dvds 13859  df-prm 14090  df-struct 14506  df-ndx 14507  df-slot 14508  df-base 14509  df-sets 14510  df-ress 14511  df-plusg 14582  df-mulr 14583  df-starv 14584  df-sca 14585  df-vsca 14586  df-ip 14587  df-tset 14588  df-ple 14589  df-ds 14591  df-unif 14592  df-hom 14593  df-cco 14594  df-0g 14711  df-prds 14717  df-pws 14719  df-mgm 15741  df-sgrp 15780  df-mnd 15790  df-grp 15926  df-minusg 15927  df-subg 16067  df-cmn 16669  df-mgp 17010  df-ur 17022  df-ring 17068  df-cring 17069  df-subrg 17295  df-sra 17686  df-rgmod 17687  df-cnfld 18289  df-zring 18357  df-dsmm 18630  df-frlm 18645

This theorem is referenced by:  ldepsnlinclem1  32816  ldepsnlinclem2  32817