sadaddlem - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > sadaddlem		Structured version Unicode version

Theorem sadaddlem 14414

Description: Lemma for sadadd 14415. (Contributed by Mario Carneiro, 9-Sep-2016.)

**Hypotheses**
Ref	Expression
sadaddlem.c	cadd bits bits
sadaddlem.k	bits
sadaddlem.1
sadaddlem.2
sadaddlem.3

**Assertion**
Ref	Expression
sadaddlem	bits sadd bits ..^ bits

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

**Proof of Theorem sadaddlem**
Step	Hyp	Ref	Expression
1		sadaddlem.k	. . . . . . . . . . . . 13 bits
2	1	fveq1i 5882	. . . . . . . . . . . 12 bits ..^ bits bits ..^
3		sadaddlem.1	. . . . . . . . . . . . . . . 16
4		2nn 10767	. . . . . . . . . . . . . . . . . 18
5	4	a1i 11	. . . . . . . . . . . . . . . . 17
6		sadaddlem.3	. . . . . . . . . . . . . . . . 17
7	5, 6	nnexpcld 12434	. . . . . . . . . . . . . . . 16
8	3, 7	zmodcld 12114	. . . . . . . . . . . . . . 15
9		fvres 5895	. . . . . . . . . . . . . . 15 bits bits
10	8, 9	syl 17	. . . . . . . . . . . . . 14 bits bits
11		bitsmod 14384	. . . . . . . . . . . . . . 15 $/\$ bits bits ..^
12	3, 6, 11	syl2anc 665	. . . . . . . . . . . . . 14 bits bits ..^
13	10, 12	eqtrd 2470	. . . . . . . . . . . . 13 bits bits ..^
14		bitsf1o 14393	. . . . . . . . . . . . . 14 bits
15		f1ocnvfv 6192	. . . . . . . . . . . . . 14 bits $/\$ bits bits ..^ bits bits ..^
16	14, 8, 15	sylancr 667	. . . . . . . . . . . . 13 bits bits ..^ bits bits ..^
17	13, 16	mpd 15	. . . . . . . . . . . 12 bits bits ..^
18	2, 17	syl5eq 2482	. . . . . . . . . . 11 bits ..^
19	18	oveq2d 6321	. . . . . . . . . 10 bits ..^
20	19	oveq1d 6320	. . . . . . . . 9 bits ..^
21	3	zred 11040	. . . . . . . . . 10
22	7	nnrpd 11339	. . . . . . . . . 10
23		moddifz 12106	. . . . . . . . . 10 $/\$
24	21, 22, 23	syl2anc 665	. . . . . . . . 9
25	20, 24	eqeltrd 2517	. . . . . . . 8 bits ..^
26	7	nnzd 11039	. . . . . . . . 9
27	7	nnne0d 10654	. . . . . . . . 9
28		inss1 3688	. . . . . . . . . . . . . 14 bits ..^ bits
29		bitsss 14374	. . . . . . . . . . . . . 14 bits
30	28, 29	sstri 3479	. . . . . . . . . . . . 13 bits ..^
31		fzofi 12184	. . . . . . . . . . . . . 14 ..^
32		inss2 3689	. . . . . . . . . . . . . 14 bits ..^ ..^
33		ssfi 7798	. . . . . . . . . . . . . 14 ..^ $/\$ bits ..^ ..^ bits ..^
34	31, 32, 33	mp2an 676	. . . . . . . . . . . . 13 bits ..^
35		elfpw 7882	. . . . . . . . . . . . 13 bits ..^ bits ..^ $/\$ bits ..^
36	30, 34, 35	mpbir2an 928	. . . . . . . . . . . 12 bits ..^
37		f1ocnv 5843	. . . . . . . . . . . . . . 15 bits bits
38		f1of 5831	. . . . . . . . . . . . . . 15 bits bits
39	14, 37, 38	mp2b 10	. . . . . . . . . . . . . 14 bits
40	1	feq1i 5738	. . . . . . . . . . . . . 14 bits
41	39, 40	mpbir 212	. . . . . . . . . . . . 13
42	41	ffvelrni 6036	. . . . . . . . . . . 12 bits ..^ bits ..^
43	36, 42	mp1i 13	. . . . . . . . . . 11 bits ..^
44	43	nn0zd 11038	. . . . . . . . . 10 bits ..^
45	3, 44	zsubcld 11045	. . . . . . . . 9 bits ..^
46		dvdsval2 14286	. . . . . . . . 9 $/\$ $/\$ bits ..^ bits ..^ bits ..^
47	26, 27, 45, 46	syl3anc 1264	. . . . . . . 8 bits ..^ bits ..^
48	25, 47	mpbird 235	. . . . . . 7 bits ..^
49	1	fveq1i 5882	. . . . . . . . . . . 12 bits ..^ bits bits ..^
50		sadaddlem.2	. . . . . . . . . . . . . . . 16
51	50, 7	zmodcld 12114	. . . . . . . . . . . . . . 15
52		fvres 5895	. . . . . . . . . . . . . . 15 bits bits
53	51, 52	syl 17	. . . . . . . . . . . . . 14 bits bits
54		bitsmod 14384	. . . . . . . . . . . . . . 15 $/\$ bits bits ..^
55	50, 6, 54	syl2anc 665	. . . . . . . . . . . . . 14 bits bits ..^
56	53, 55	eqtrd 2470	. . . . . . . . . . . . 13 bits bits ..^
57		f1ocnvfv 6192	. . . . . . . . . . . . . 14 bits $/\$ bits bits ..^ bits bits ..^
58	14, 51, 57	sylancr 667	. . . . . . . . . . . . 13 bits bits ..^ bits bits ..^
59	56, 58	mpd 15	. . . . . . . . . . . 12 bits bits ..^
60	49, 59	syl5eq 2482	. . . . . . . . . . 11 bits ..^
61	60	oveq2d 6321	. . . . . . . . . 10 bits ..^
62	61	oveq1d 6320	. . . . . . . . 9 bits ..^
63	50	zred 11040	. . . . . . . . . 10
64		moddifz 12106	. . . . . . . . . 10 $/\$
65	63, 22, 64	syl2anc 665	. . . . . . . . 9
66	62, 65	eqeltrd 2517	. . . . . . . 8 bits ..^
67		inss1 3688	. . . . . . . . . . . . . 14 bits ..^ bits
68		bitsss 14374	. . . . . . . . . . . . . 14 bits
69	67, 68	sstri 3479	. . . . . . . . . . . . 13 bits ..^
70		inss2 3689	. . . . . . . . . . . . . 14 bits ..^ ..^
71		ssfi 7798	. . . . . . . . . . . . . 14 ..^ $/\$ bits ..^ ..^ bits ..^
72	31, 70, 71	mp2an 676	. . . . . . . . . . . . 13 bits ..^
73		elfpw 7882	. . . . . . . . . . . . 13 bits ..^ bits ..^ $/\$ bits ..^
74	69, 72, 73	mpbir2an 928	. . . . . . . . . . . 12 bits ..^
75	41	ffvelrni 6036	. . . . . . . . . . . 12 bits ..^ bits ..^
76	74, 75	mp1i 13	. . . . . . . . . . 11 bits ..^
77	76	nn0zd 11038	. . . . . . . . . 10 bits ..^
78	50, 77	zsubcld 11045	. . . . . . . . 9 bits ..^
79		dvdsval2 14286	. . . . . . . . 9 $/\$ $/\$ bits ..^ bits ..^ bits ..^
80	26, 27, 78, 79	syl3anc 1264	. . . . . . . 8 bits ..^ bits ..^
81	66, 80	mpbird 235	. . . . . . 7 bits ..^
82		dvds2add 14312	. . . . . . . 8 $/\$ bits ..^ $/\$ bits ..^ bits ..^ $/\$ bits ..^ bits ..^ bits ..^
83	26, 45, 78, 82	syl3anc 1264	. . . . . . 7 bits ..^ $/\$ bits ..^ bits ..^ bits ..^
84	48, 81, 83	mp2and 683	. . . . . 6 bits ..^ bits ..^
85	3	zcnd 11041	. . . . . . 7
86	50	zcnd 11041	. . . . . . 7
87	43	nn0cnd 10927	. . . . . . 7 bits ..^
88	76	nn0cnd 10927	. . . . . . 7 bits ..^
89	85, 86, 87, 88	addsub4d 10032	. . . . . 6 bits ..^ bits ..^ bits ..^ bits ..^
90	84, 89	breqtrrd 4452	. . . . 5 bits ..^ bits ..^
91	3, 50	zaddcld 11044	. . . . . 6
92	44, 77	zaddcld 11044	. . . . . 6 bits ..^ bits ..^
93		moddvds 14290	. . . . . 6 $/\$ $/\$ bits ..^ bits ..^ bits ..^ bits ..^ bits ..^ bits ..^
94	7, 91, 92, 93	syl3anc 1264	. . . . 5 bits ..^ bits ..^ bits ..^ bits ..^
95	90, 94	mpbird 235	. . . 4 bits ..^ bits ..^
96	29	a1i 11	. . . . 5 bits
97	68	a1i 11	. . . . 5 bits
98		sadaddlem.c	. . . . 5 cadd bits bits
99	96, 97, 98, 6, 1	sadadd3 14409	. . . 4 bits sadd bits ..^ bits ..^ bits ..^
100		inss1 3688	. . . . . . . . 9 bits sadd bits ..^ bits sadd bits
101		sadcl 14410	. . . . . . . . . 10 bits $/\$ bits bits sadd bits
102	29, 68, 101	mp2an 676	. . . . . . . . 9 bits sadd bits
103	100, 102	sstri 3479	. . . . . . . 8 bits sadd bits ..^
104		inss2 3689	. . . . . . . . 9 bits sadd bits ..^ ..^
105		ssfi 7798	. . . . . . . . 9 ..^ $/\$ bits sadd bits ..^ ..^ bits sadd bits ..^
106	31, 104, 105	mp2an 676	. . . . . . . 8 bits sadd bits ..^
107		elfpw 7882	. . . . . . . 8 bits sadd bits ..^ bits sadd bits ..^ $/\$ bits sadd bits ..^
108	103, 106, 107	mpbir2an 928	. . . . . . 7 bits sadd bits ..^
109	41	ffvelrni 6036	. . . . . . 7 bits sadd bits ..^ bits sadd bits ..^
110	108, 109	mp1i 13	. . . . . 6 bits sadd bits ..^
111	110	nn0red 10926	. . . . 5 bits sadd bits ..^
112	110	nn0ge0d 10928	. . . . 5 bits sadd bits ..^
113	1	fveq1i 5882	. . . . . . . . . 10 bits sadd bits ..^ bits bits sadd bits ..^
114	113	fveq2i 5884	. . . . . . . . 9 bits bits sadd bits ..^ bits bits bits sadd bits ..^
115		fvres 5895	. . . . . . . . . 10 bits sadd bits ..^ bits bits sadd bits ..^ bitsbits sadd bits ..^
116	110, 115	syl 17	. . . . . . . . 9 bits bits sadd bits ..^ bitsbits sadd bits ..^
117	108	a1i 11	. . . . . . . . . 10 bits sadd bits ..^
118		f1ocnvfv2 6191	. . . . . . . . . 10 bits $/\$ bits sadd bits ..^ bits bits bits sadd bits ..^ bits sadd bits ..^
119	14, 117, 118	sylancr 667	. . . . . . . . 9 bits bits bits sadd bits ..^ bits sadd bits ..^
120	114, 116, 119	3eqtr3a 2494	. . . . . . . 8 bitsbits sadd bits ..^ bits sadd bits ..^
121	120, 104	syl6eqss 3520	. . . . . . 7 bitsbits sadd bits ..^ ..^
122	110	nn0zd 11038	. . . . . . . 8 bits sadd bits ..^
123		bitsfzo 14383	. . . . . . . 8 bits sadd bits ..^ $/\$ bits sadd bits ..^ ..^ bitsbits sadd bits ..^ ..^
124	122, 6, 123	syl2anc 665	. . . . . . 7 bits sadd bits ..^ ..^ bitsbits sadd bits ..^ ..^
125	121, 124	mpbird 235	. . . . . 6 bits sadd bits ..^ ..^
126		elfzolt2 11927	. . . . . 6 bits sadd bits ..^ ..^ bits sadd bits ..^
127	125, 126	syl 17	. . . . 5 bits sadd bits ..^
128		modid 12118	. . . . 5 bits sadd bits ..^ $/\$ $/\$ bits sadd bits ..^ $/\$ bits sadd bits ..^ bits sadd bits ..^ bits sadd bits ..^
129	111, 22, 112, 127, 128	syl22anc 1265	. . . 4 bits sadd bits ..^ bits sadd bits ..^
130	95, 99, 129	3eqtr2d 2476	. . 3 bits sadd bits ..^
131	130	fveq2d 5885	. 2 bits bitsbits sadd bits ..^
132	131, 120	eqtr2d 2471	1 bits sadd bits ..^ bits

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 187 $/\$ wa 370

wceq 1437 caddwcad 1504

wcel 1870

wne 2625

cin 3441

wss 3442

c0 3767

cif 3915

cpw 3985 class class class wbr 4426

cmpt 4484

ccnv 4853

cres 4856

wf 5597

wf1o 5600

cfv 5601 (class class class)co 6305

cmpt2 6307

c1o 7183

c2o 7184

cfn 7577

cr 9537

cc0 9538

c1 9539

caddc 9541

clt 9674

cle 9675

cmin 9859

cdiv 10268

cn 10609

c2 10659

cn0 10869

cz 10937

crp 11302 ..^cfzo 11913

cmo 12093

cseq 12210

cexp 12269

cdvds 14283 bitscbits 14367 sadd csad 14368

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1751 ax-6 1797 ax-7 1841 ax-8 1872 ax-9 1874 ax-10 1889 ax-11 1894 ax-12 1907 ax-13 2055 ax-ext 2407 ax-rep 4538 ax-sep 4548 ax-nul 4556 ax-pow 4603 ax-pr 4661 ax-un 6597 ax-inf2 8146 ax-cnex 9594 ax-resscn 9595 ax-1cn 9596 ax-icn 9597 ax-addcl 9598 ax-addrcl 9599 ax-mulcl 9600 ax-mulrcl 9601 ax-mulcom 9602 ax-addass 9603 ax-mulass 9604 ax-distr 9605 ax-i2m1 9606 ax-1ne0 9607 ax-1rid 9608 ax-rnegex 9609 ax-rrecex 9610 ax-cnre 9611 ax-pre-lttri 9612 ax-pre-lttrn 9613 ax-pre-ltadd 9614 ax-pre-mulgt0 9615 ax-pre-sup 9616

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-xor 1401 df-tru 1440 df-fal 1443 df-had 1492 df-cad 1505 df-ex 1660 df-nf 1664 df-sb 1790 df-eu 2270 df-mo 2271 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2579 df-ne 2627 df-nel 2628 df-ral 2787 df-rex 2788 df-reu 2789 df-rmo 2790 df-rab 2791 df-v 3089 df-sbc 3306 df-csb 3402 df-dif 3445 df-un 3447 df-in 3449 df-ss 3456 df-pss 3458 df-nul 3768 df-if 3916 df-pw 3987 df-sn 4003 df-pr 4005 df-tp 4007 df-op 4009 df-uni 4223 df-int 4259 df-iun 4304 df-disj 4398 df-br 4427 df-opab 4485 df-mpt 4486 df-tr 4521 df-eprel 4765 df-id 4769 df-po 4775 df-so 4776 df-fr 4813 df-se 4814 df-we 4815 df-xp 4860 df-rel 4861 df-cnv 4862 df-co 4863 df-dm 4864 df-rn 4865 df-res 4866 df-ima 4867 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-isom 5610 df-riota 6267 df-ov 6308 df-oprab 6309 df-mpt2 6310 df-om 6707 df-1st 6807 df-2nd 6808 df-wrecs 7036 df-recs 7098 df-rdg 7136 df-1o 7190 df-2o 7191 df-oadd 7194 df-er 7371 df-map 7482 df-pm 7483 df-en 7578 df-dom 7579 df-sdom 7580 df-fin 7581 df-sup 7962 df-oi 8025 df-card 8372 df-cda 8596 df-pnf 9676 df-mnf 9677 df-xr 9678 df-ltxr 9679 df-le 9680 df-sub 9861 df-neg 9862 df-div 10269 df-nn 10610 df-2 10668 df-3 10669 df-n0 10870 df-z 10938 df-uz 11160 df-rp 11303 df-fz 11783 df-fzo 11914 df-fl 12025 df-mod 12094 df-seq 12211 df-exp 12270 df-hash 12513 df-cj 13141 df-re 13142 df-im 13143 df-sqrt 13277 df-abs 13278 df-clim 13530 df-sum 13731 df-dvds 14284 df-bits 14370 df-sad 14399

This theorem is referenced by: sadadd 14415

W3C validator