bitsmod - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > bitsmod		Unicode version

Theorem bitsmod 12123

Description: Truncating the bit sequence after some

is equivalent to reducing the argument

. (Contributed by Mario Carneiro, 6-Sep-2016.)

**Assertion**
Ref	Expression
bitsmod	$/\$ bits bits ..^

Proof of Theorem bitsmod Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 109	. . . . . . . 8 $/\$
2		2nn 9154	. . . . . . . . . 10
3	2	a1i 9	. . . . . . . . 9 $/\$
4		simpr 110	. . . . . . . . 9 $/\$
5	3, 4	nnexpcld 10789	. . . . . . . 8 $/\$
6	1, 5	zmodcld 10439	. . . . . . 7 $/\$
7	6	nn0zd 9448	. . . . . 6 $/\$
8	7	biantrurd 305	. . . . 5 $/\$ $/\$ $/\$ $/\$
9	1	ad2antrr 488	. . . . . . . . . . 11 $/\$ $/\$ $/\$
10		simplr 528	. . . . . . . . . . 11 $/\$ $/\$ $/\$
11		bitsval2 12111	. . . . . . . . . . 11 $/\$ bits
12	9, 10, 11	syl2anc 411	. . . . . . . . . 10 $/\$ $/\$ $/\$ bits
13		simpr 110	. . . . . . . . . . 11 $/\$ $/\$ $/\$
14	13	biantrud 304	. . . . . . . . . 10 $/\$ $/\$ $/\$ bits bits $/\$
15		2z 9356	. . . . . . . . . . . . 13
16	15	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
17	2	a1i 9	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
18	17, 10	nnexpcld 10789	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
19		znq 9700	. . . . . . . . . . . . . 14 $/\$
20	9, 18, 19	syl2anc 411	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
21	20	flqcld 10369	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
22	7	ad2antrr 488	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
23		znq 9700	. . . . . . . . . . . . . 14 $/\$
24	22, 18, 23	syl2anc 411	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
25	24	flqcld 10369	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
26	18	nnzd 9449	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
27	26, 16	zmulcld 9456	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
28	5	ad2antrr 488	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
29	28	nnzd 9449	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
30	9, 22	zsubcld 9455	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
31		2cnd 9065	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
32	31, 10	expp1d 10768	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
33		1nn0 9267	. . . . . . . . . . . . . . . . . . . 20
34	33	a1i 9	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
35	10, 34	nn0addcld 9308	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
36	35	nn0zd 9448	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
37		simplr 528	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
38	37	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
39	38	nn0zd 9448	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
40		nn0ltp1le 9390	. . . . . . . . . . . . . . . . . . . . 21 $/\$
41	10, 38, 40	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
42	13, 41	mpbid 147	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
43		eluz2 9609	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
44	36, 39, 42, 43	syl3anbrc 1183	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
45		dvdsexp 12028	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
46	16, 35, 44, 45	syl3anc 1249	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
47	32, 46	eqbrtrrd 4058	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
48		zq 9702	. . . . . . . . . . . . . . . . . . 19
49	9, 48	syl 14	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
50		nnq 9709	. . . . . . . . . . . . . . . . . . 19
51	28, 50	syl 14	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
52	28	nngt0d 9036	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
53		modqdifz 10430	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
54	49, 51, 52, 53	syl3anc 1249	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
55	28	nnne0d 9037	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
56		dvdsval2 11957	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
57	29, 55, 30, 56	syl3anc 1249	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
58	54, 57	mpbird 167	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
59	27, 29, 30, 47, 58	dvdstrd 11997	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
60	30	zcnd 9451	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
61	18	nncnd 9006	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
62	18	nnap0d 9038	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ #
63	60, 61, 62	divcanap2d 8821	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
64	59, 63	breqtrrd 4062	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
65	10	nn0zd 9448	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
66	10	nn0red 9305	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
67	38	nn0red 9305	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
68	66, 67, 13	ltled 8147	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
69		eluz2 9609	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
70	65, 39, 68, 69	syl3anbrc 1183	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
71		dvdsexp 12028	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
72	16, 10, 70, 71	syl3anc 1249	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
73	26, 29, 30, 72, 58	dvdstrd 11997	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
74	18	nnne0d 9037	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
75		dvdsval2 11957	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
76	26, 74, 30, 75	syl3anc 1249	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
77	73, 76	mpbid 147	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
78		dvdscmulr 11987	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
79	16, 77, 26, 74, 78	syl112anc 1253	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
80	64, 79	mpbid 147	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
81	25	zcnd 9451	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
82	77	zcnd 9451	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
83	22	zcnd 9451	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
84	9	zcnd 9451	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
85	83, 84	pncan3d 8342	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
86	85	oveq1d 5938	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
87	83, 60, 61, 62	divdirapd 8858	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
88	86, 87	eqtr3d 2231	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
89	88	fveq2d 5563	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
90		flqaddz 10389	. . . . . . . . . . . . . . . 16 $/\$
91	24, 77, 90	syl2anc 411	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
92	89, 91	eqtrd 2229	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
93	81, 82, 92	mvrladdd 8395	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
94	80, 93	breqtrrd 4062	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
95		dvdssub2 12002	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
96	16, 21, 25, 94, 95	syl31anc 1252	. . . . . . . . . . 11 $/\$ $/\$ $/\$
97	96	notbid 668	. . . . . . . . . 10 $/\$ $/\$ $/\$
98	12, 14, 97	3bitr3d 218	. . . . . . . . 9 $/\$ $/\$ $/\$ bits $/\$
99		simpr 110	. . . . . . . . . . 11 $/\$ $/\$ $/\$
100	99	intnand 932	. . . . . . . . . 10 $/\$ $/\$ $/\$ bits $/\$
101		z0even 12078	. . . . . . . . . . . 12
102	1	ad2antrr 488	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
103	102, 48	syl 14	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
104	5	ad2antrr 488	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
105	104, 50	syl 14	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
106		2rp 9735	. . . . . . . . . . . . . . . . . . 19
107	106	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
108	37	nn0zd 9448	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
109	108	adantr 276	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
110	107, 109	rpexpcld 10791	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
111	110	rpgt0d 9776	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
112	103, 105, 111	modqcld 10422	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
113		qre 9701	. . . . . . . . . . . . . . 15
114	112, 113	syl 14	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
115		simplr 528	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
116	115	nn0zd 9448	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
117	107, 116	rpexpcld 10791	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
118	6	ad2antrr 488	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
119	118	nn0ge0d 9307	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
120	114, 117, 119	divge0d 9814	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
121	110	rpred 9773	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
122	117	rpred 9773	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
123		modqlt 10427	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
124	103, 105, 111, 123	syl3anc 1249	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
125	107	rpred 9773	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
126		1le2 9201	. . . . . . . . . . . . . . . . . . 19
127	126	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
128	109	zred 9450	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
129	115	nn0red 9305	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
130	128, 129, 99	nltled 8149	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
131		eluz2 9609	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
132	109, 116, 130, 131	syl3anbrc 1183	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
133	125, 127, 132	leexp2ad 10796	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
134	114, 121, 122, 124, 133	ltletrd 8452	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
135	117	rpcnd 9775	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
136	135	mulridd 8045	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
137	134, 136	breqtrrd 4062	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
138		1red 8043	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
139	114, 138, 117	ltdivmuld 9825	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
140	137, 139	mpbird 167	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
141		1e0p1 9500	. . . . . . . . . . . . . 14
142	140, 141	breqtrdi 4075	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
143	7	ad2antrr 488	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
144	2	a1i 9	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
145	144, 115	nnexpcld 10789	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
146	143, 145, 23	syl2anc 411	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
147		0z 9339	. . . . . . . . . . . . . 14
148		flqbi 10382	. . . . . . . . . . . . . 14 $/\$ $/\$
149	146, 147, 148	sylancl 413	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
150	120, 142, 149	mpbir2and 946	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
151	101, 150	breqtrrid 4072	. . . . . . . . . . 11 $/\$ $/\$ $/\$
152	151	notnotd 631	. . . . . . . . . 10 $/\$ $/\$ $/\$
153	100, 152	2falsed 703	. . . . . . . . 9 $/\$ $/\$ $/\$ bits $/\$
154		nn0z 9348	. . . . . . . . . . 11
155		zdclt 9405	. . . . . . . . . . 11 $/\$ DECID
156	154, 108, 155	syl2an2 594	. . . . . . . . . 10 $/\$ $/\$ DECID
157		exmiddc 837	. . . . . . . . . 10 DECID $\/$
158	156, 157	syl 14	. . . . . . . . 9 $/\$ $/\$ $\/$
159	98, 153, 158	mpjaodan 799	. . . . . . . 8 $/\$ $/\$ bits $/\$
160	108	biantrurd 305	. . . . . . . 8 $/\$ $/\$ bits $/\$ $/\$ bits $/\$
161	159, 160	bitr3d 190	. . . . . . 7 $/\$ $/\$ $/\$ bits $/\$
162		an12 561	. . . . . . 7 $/\$ bits $/\$ bits $/\$ $/\$
163	161, 162	bitrdi 196	. . . . . 6 $/\$ $/\$ bits $/\$ $/\$
164	163	pm5.32da 452	. . . . 5 $/\$ $/\$ $/\$ bits $/\$ $/\$
165	8, 164	bitr3d 190	. . . 4 $/\$ $/\$ $/\$ $/\$ bits $/\$ $/\$
166		3anass 984	. . . 4 $/\$ $/\$ $/\$ $/\$
167		elfzo2 10227	. . . . . . 7 ..^ $/\$ $/\$
168		elnn0uz 9641	. . . . . . . 8
169	168	3anbi1i 1192	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
170		3anass 984	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
171	167, 169, 170	3bitr2i 208	. . . . . 6 ..^ $/\$ $/\$
172	171	anbi2i 457	. . . . 5 bits $/\$ ..^ bits $/\$ $/\$ $/\$
173		an12 561	. . . . 5 bits $/\$ $/\$ $/\$ $/\$ bits $/\$ $/\$
174	172, 173	bitri 184	. . . 4 bits $/\$ ..^ $/\$ bits $/\$ $/\$
175	165, 166, 174	3bitr4g 223	. . 3 $/\$ $/\$ $/\$ bits $/\$ ..^
176		bitsval 12110	. . 3 bits $/\$ $/\$
177		elin 3347	. . 3 bits ..^ bits $/\$ ..^
178	175, 176, 177	3bitr4g 223	. 2 $/\$ bits bits ..^
179	178	eqrdv 2194	1 $/\$ bits bits ..^

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 709 DECID wdc 835 $/\$ w3a 980

wceq 1364

wcel 2167

wne 2367

cin 3156 class class class wbr 4034

cfv 5259 (class class class)co 5923

cr 7880

cc0 7881

c1 7882

caddc 7884

cmul 7886

clt 8063

cle 8064

cmin 8199

cdiv 8701

cn 8992

c2 9043

cn0 9251

cz 9328

cuz 9603

cq 9695

crp 9730 ..^cfzo 10219

cfl 10360

cmo 10416

cexp 10632

cdvds 11954 bitscbits 12107

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4149 ax-sep 4152 ax-nul 4160 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-setind 4574 ax-iinf 4625 ax-cnex 7972 ax-resscn 7973 ax-1cn 7974 ax-1re 7975 ax-icn 7976 ax-addcl 7977 ax-addrcl 7978 ax-mulcl 7979 ax-mulrcl 7980 ax-addcom 7981 ax-mulcom 7982 ax-addass 7983 ax-mulass 7984 ax-distr 7985 ax-i2m1 7986 ax-0lt1 7987 ax-1rid 7988 ax-0id 7989 ax-rnegex 7990 ax-precex 7991 ax-cnre 7992 ax-pre-ltirr 7993 ax-pre-ltwlin 7994 ax-pre-lttrn 7995 ax-pre-apti 7996 ax-pre-ltadd 7997 ax-pre-mulgt0 7998 ax-pre-mulext 7999 ax-arch 8000

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3452 df-if 3563 df-pw 3608 df-sn 3629 df-pr 3630 df-op 3632 df-uni 3841 df-int 3876 df-iun 3919 df-br 4035 df-opab 4096 df-mpt 4097 df-tr 4133 df-id 4329 df-po 4332 df-iso 4333 df-iord 4402 df-on 4404 df-ilim 4405 df-suc 4407 df-iom 4628 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-rn 4675 df-res 4676 df-ima 4677 df-iota 5220 df-fun 5261 df-fn 5262 df-f 5263 df-f1 5264 df-fo 5265 df-f1o 5266 df-fv 5267 df-riota 5878 df-ov 5926 df-oprab 5927 df-mpo 5928 df-1st 6199 df-2nd 6200 df-recs 6364 df-frec 6450 df-pnf 8065 df-mnf 8066 df-xr 8067 df-ltxr 8068 df-le 8069 df-sub 8201 df-neg 8202 df-reap 8604 df-ap 8611 df-div 8702 df-inn 8993 df-2 9051 df-n0 9252 df-z 9329 df-uz 9604 df-q 9696 df-rp 9731 df-fz 10086 df-fzo 10220 df-fl 10362 df-mod 10417 df-seqfrec 10542 df-exp 10633 df-dvds 11955 df-bits 12108

This theorem is referenced by: (None)

W3C validator