bitsmod - Intuitionistic Logic Explorer

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

Theorem bitsmod 12337

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 9213	. . . . . . . . . 10
3	2	a1i 9	. . . . . . . . 9 $/\$
4		simpr 110	. . . . . . . . 9 $/\$
5	3, 4	nnexpcld 10857	. . . . . . . 8 $/\$
6	1, 5	zmodcld 10507	. . . . . . 7 $/\$
7	6	nn0zd 9508	. . . . . 6 $/\$
8	7	biantrurd 305	. . . . 5 $/\$ $/\$ $/\$ $/\$
9	1	ad2antrr 488	. . . . . . . . . . 11 $/\$ $/\$ $/\$
10		simplr 528	. . . . . . . . . . 11 $/\$ $/\$ $/\$
11		bitsval2 12325	. . . . . . . . . . 11 $/\$ bits
12	9, 10, 11	syl2anc 411	. . . . . . . . . 10 $/\$ $/\$ $/\$ bits
13		simpr 110	. . . . . . . . . . 11 $/\$ $/\$ $/\$
14	13	biantrud 304	. . . . . . . . . 10 $/\$ $/\$ $/\$ bits bits $/\$
15		2z 9415	. . . . . . . . . . . . 13
16	15	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
17	2	a1i 9	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
18	17, 10	nnexpcld 10857	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
19		znq 9760	. . . . . . . . . . . . . 14 $/\$
20	9, 18, 19	syl2anc 411	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
21	20	flqcld 10437	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
22	7	ad2antrr 488	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
23		znq 9760	. . . . . . . . . . . . . 14 $/\$
24	22, 18, 23	syl2anc 411	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
25	24	flqcld 10437	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
26	18	nnzd 9509	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
27	26, 16	zmulcld 9516	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
28	5	ad2antrr 488	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
29	28	nnzd 9509	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
30	9, 22	zsubcld 9515	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
31		2cnd 9124	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
32	31, 10	expp1d 10836	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
33		1nn0 9326	. . . . . . . . . . . . . . . . . . . 20
34	33	a1i 9	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
35	10, 34	nn0addcld 9367	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
36	35	nn0zd 9508	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
37		simplr 528	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
38	37	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
39	38	nn0zd 9508	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
40		nn0ltp1le 9450	. . . . . . . . . . . . . . . . . . . . 21 $/\$
41	10, 38, 40	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
42	13, 41	mpbid 147	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
43		eluz2 9669	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
44	36, 39, 42, 43	syl3anbrc 1184	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
45		dvdsexp 12242	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
46	16, 35, 44, 45	syl3anc 1250	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
47	32, 46	eqbrtrrd 4074	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
48		zq 9762	. . . . . . . . . . . . . . . . . . 19
49	9, 48	syl 14	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
50		nnq 9769	. . . . . . . . . . . . . . . . . . 19
51	28, 50	syl 14	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
52	28	nngt0d 9095	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
53		modqdifz 10498	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
54	49, 51, 52, 53	syl3anc 1250	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
55	28	nnne0d 9096	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
56		dvdsval2 12171	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
57	29, 55, 30, 56	syl3anc 1250	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
58	54, 57	mpbird 167	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
59	27, 29, 30, 47, 58	dvdstrd 12211	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
60	30	zcnd 9511	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
61	18	nncnd 9065	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
62	18	nnap0d 9097	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ #
63	60, 61, 62	divcanap2d 8880	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
64	59, 63	breqtrrd 4078	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
65	10	nn0zd 9508	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
66	10	nn0red 9364	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
67	38	nn0red 9364	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
68	66, 67, 13	ltled 8206	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
69		eluz2 9669	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
70	65, 39, 68, 69	syl3anbrc 1184	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
71		dvdsexp 12242	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
72	16, 10, 70, 71	syl3anc 1250	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
73	26, 29, 30, 72, 58	dvdstrd 12211	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
74	18	nnne0d 9096	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
75		dvdsval2 12171	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
76	26, 74, 30, 75	syl3anc 1250	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
77	73, 76	mpbid 147	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
78		dvdscmulr 12201	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
79	16, 77, 26, 74, 78	syl112anc 1254	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
80	64, 79	mpbid 147	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
81	25	zcnd 9511	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
82	77	zcnd 9511	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
83	22	zcnd 9511	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
84	9	zcnd 9511	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
85	83, 84	pncan3d 8401	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
86	85	oveq1d 5971	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
87	83, 60, 61, 62	divdirapd 8917	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
88	86, 87	eqtr3d 2241	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
89	88	fveq2d 5592	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
90		flqaddz 10457	. . . . . . . . . . . . . . . 16 $/\$
91	24, 77, 90	syl2anc 411	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
92	89, 91	eqtrd 2239	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
93	81, 82, 92	mvrladdd 8454	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
94	80, 93	breqtrrd 4078	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
95		dvdssub2 12216	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
96	16, 21, 25, 94, 95	syl31anc 1253	. . . . . . . . . . 11 $/\$ $/\$ $/\$
97	96	notbid 669	. . . . . . . . . 10 $/\$ $/\$ $/\$
98	12, 14, 97	3bitr3d 218	. . . . . . . . 9 $/\$ $/\$ $/\$ bits $/\$
99		simpr 110	. . . . . . . . . . 11 $/\$ $/\$ $/\$
100	99	intnand 933	. . . . . . . . . 10 $/\$ $/\$ $/\$ bits $/\$
101		z0even 12292	. . . . . . . . . . . 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 9795	. . . . . . . . . . . . . . . . . . 19
107	106	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
108	37	nn0zd 9508	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
109	108	adantr 276	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
110	107, 109	rpexpcld 10859	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
111	110	rpgt0d 9836	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
112	103, 105, 111	modqcld 10490	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
113		qre 9761	. . . . . . . . . . . . . . 15
114	112, 113	syl 14	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
115		simplr 528	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
116	115	nn0zd 9508	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
117	107, 116	rpexpcld 10859	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
118	6	ad2antrr 488	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
119	118	nn0ge0d 9366	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
120	114, 117, 119	divge0d 9874	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
121	110	rpred 9833	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
122	117	rpred 9833	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
123		modqlt 10495	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
124	103, 105, 111, 123	syl3anc 1250	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
125	107	rpred 9833	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
126		1le2 9260	. . . . . . . . . . . . . . . . . . 19
127	126	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
128	109	zred 9510	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
129	115	nn0red 9364	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
130	128, 129, 99	nltled 8208	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
131		eluz2 9669	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
132	109, 116, 130, 131	syl3anbrc 1184	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
133	125, 127, 132	leexp2ad 10864	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
134	114, 121, 122, 124, 133	ltletrd 8511	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
135	117	rpcnd 9835	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
136	135	mulridd 8104	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
137	134, 136	breqtrrd 4078	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
138		1red 8102	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
139	114, 138, 117	ltdivmuld 9885	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
140	137, 139	mpbird 167	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
141		1e0p1 9560	. . . . . . . . . . . . . 14
142	140, 141	breqtrdi 4091	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
143	7	ad2antrr 488	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
144	2	a1i 9	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
145	144, 115	nnexpcld 10857	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
146	143, 145, 23	syl2anc 411	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
147		0z 9398	. . . . . . . . . . . . . 14
148		flqbi 10450	. . . . . . . . . . . . . 14 $/\$ $/\$
149	146, 147, 148	sylancl 413	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
150	120, 142, 149	mpbir2and 947	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
151	101, 150	breqtrrid 4088	. . . . . . . . . . 11 $/\$ $/\$ $/\$
152	151	notnotd 631	. . . . . . . . . 10 $/\$ $/\$ $/\$
153	100, 152	2falsed 704	. . . . . . . . 9 $/\$ $/\$ $/\$ bits $/\$
154		nn0z 9407	. . . . . . . . . . 11
155		zdclt 9465	. . . . . . . . . . 11 $/\$ DECID
156	154, 108, 155	syl2an2 594	. . . . . . . . . 10 $/\$ $/\$ DECID
157		exmiddc 838	. . . . . . . . . 10 DECID $\/$
158	156, 157	syl 14	. . . . . . . . 9 $/\$ $/\$ $\/$
159	98, 153, 158	mpjaodan 800	. . . . . . . 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 985	. . . 4 $/\$ $/\$ $/\$ $/\$
167		elfzo2 10287	. . . . . . 7 ..^ $/\$ $/\$
168		elnn0uz 9701	. . . . . . . 8
169	168	3anbi1i 1193	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
170		3anass 985	. . . . . . 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 12324	. . 3 bits $/\$ $/\$
177		elin 3360	. . 3 bits ..^ bits $/\$ ..^
178	175, 176, 177	3bitr4g 223	. 2 $/\$ bits bits ..^
179	178	eqrdv 2204	1 $/\$ bits bits ..^

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 710 DECID wdc 836 $/\$ w3a 981

wceq 1373

wcel 2177

wne 2377

cin 3169 class class class wbr 4050

cfv 5279 (class class class)co 5956

cr 7939

cc0 7940

c1 7941

caddc 7943

cmul 7945

clt 8122

cle 8123

cmin 8258

cdiv 8760

cn 9051

c2 9102

cn0 9310

cz 9387

cuz 9663

cq 9755

crp 9790 ..^cfzo 10279

cfl 10428

cmo 10484

cexp 10700

cdvds 12168 bitscbits 12321

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 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-coll 4166 ax-sep 4169 ax-nul 4177 ax-pow 4225 ax-pr 4260 ax-un 4487 ax-setind 4592 ax-iinf 4643 ax-cnex 8031 ax-resscn 8032 ax-1cn 8033 ax-1re 8034 ax-icn 8035 ax-addcl 8036 ax-addrcl 8037 ax-mulcl 8038 ax-mulrcl 8039 ax-addcom 8040 ax-mulcom 8041 ax-addass 8042 ax-mulass 8043 ax-distr 8044 ax-i2m1 8045 ax-0lt1 8046 ax-1rid 8047 ax-0id 8048 ax-rnegex 8049 ax-precex 8050 ax-cnre 8051 ax-pre-ltirr 8052 ax-pre-ltwlin 8053 ax-pre-lttrn 8054 ax-pre-apti 8055 ax-pre-ltadd 8056 ax-pre-mulgt0 8057 ax-pre-mulext 8058 ax-arch 8059

This theorem depends on definitions: df-bi 117 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rmo 2493 df-rab 2494 df-v 2775 df-sbc 3003 df-csb 3098 df-dif 3172 df-un 3174 df-in 3176 df-ss 3183 df-nul 3465 df-if 3576 df-pw 3622 df-sn 3643 df-pr 3644 df-op 3646 df-uni 3856 df-int 3891 df-iun 3934 df-br 4051 df-opab 4113 df-mpt 4114 df-tr 4150 df-id 4347 df-po 4350 df-iso 4351 df-iord 4420 df-on 4422 df-ilim 4423 df-suc 4425 df-iom 4646 df-xp 4688 df-rel 4689 df-cnv 4690 df-co 4691 df-dm 4692 df-rn 4693 df-res 4694 df-ima 4695 df-iota 5240 df-fun 5281 df-fn 5282 df-f 5283 df-f1 5284 df-fo 5285 df-f1o 5286 df-fv 5287 df-riota 5911 df-ov 5959 df-oprab 5960 df-mpo 5961 df-1st 6238 df-2nd 6239 df-recs 6403 df-frec 6489 df-pnf 8124 df-mnf 8125 df-xr 8126 df-ltxr 8127 df-le 8128 df-sub 8260 df-neg 8261 df-reap 8663 df-ap 8670 df-div 8761 df-inn 9052 df-2 9110 df-n0 9311 df-z 9388 df-uz 9664 df-q 9756 df-rp 9791 df-fz 10146 df-fzo 10280 df-fl 10430 df-mod 10485 df-seqfrec 10610 df-exp 10701 df-dvds 12169 df-bits 12322

This theorem is referenced by: (None)

W3C validator