sadaddlem - Metamath Proof Explorer

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

Theorem sadaddlem 13975

Description: Lemma for sadadd 13976. (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 5867	. . . . . . . . . . . 12 bits ..^ bits bits ..^
3		sadaddlem.1	. . . . . . . . . . . . . . . 16
4		2nn 10693	. . . . . . . . . . . . . . . . . 18
5	4	a1i 11	. . . . . . . . . . . . . . . . 17
6		sadaddlem.3	. . . . . . . . . . . . . . . . 17
7	5, 6	nnexpcld 12299	. . . . . . . . . . . . . . . 16
8	3, 7	zmodcld 11984	. . . . . . . . . . . . . . 15
9		fvres 5880	. . . . . . . . . . . . . . 15 bits bits
10	8, 9	syl 16	. . . . . . . . . . . . . 14 bits bits
11		bitsmod 13945	. . . . . . . . . . . . . . 15 $/\$ bits bits ..^
12	3, 6, 11	syl2anc 661	. . . . . . . . . . . . . 14 bits bits ..^
13	10, 12	eqtrd 2508	. . . . . . . . . . . . 13 bits bits ..^
14		bitsf1o 13954	. . . . . . . . . . . . . 14 bits
15		f1ocnvfv 6172	. . . . . . . . . . . . . 14 bits $/\$ bits bits ..^ bits bits ..^
16	14, 8, 15	sylancr 663	. . . . . . . . . . . . 13 bits bits ..^ bits bits ..^
17	13, 16	mpd 15	. . . . . . . . . . . 12 bits bits ..^
18	2, 17	syl5eq 2520	. . . . . . . . . . 11 bits ..^
19	18	oveq2d 6300	. . . . . . . . . 10 bits ..^
20	19	oveq1d 6299	. . . . . . . . 9 bits ..^
21	3	zred 10966	. . . . . . . . . 10
22	7	nnrpd 11255	. . . . . . . . . 10
23		moddifz 11976	. . . . . . . . . 10 $/\$
24	21, 22, 23	syl2anc 661	. . . . . . . . 9
25	20, 24	eqeltrd 2555	. . . . . . . 8 bits ..^
26	7	nnzd 10965	. . . . . . . . 9
27	7	nnne0d 10580	. . . . . . . . 9
28		inss1 3718	. . . . . . . . . . . . . 14 bits ..^ bits
29		bitsss 13935	. . . . . . . . . . . . . 14 bits
30	28, 29	sstri 3513	. . . . . . . . . . . . 13 bits ..^
31		fzofi 12052	. . . . . . . . . . . . . 14 ..^
32		inss2 3719	. . . . . . . . . . . . . 14 bits ..^ ..^
33		ssfi 7740	. . . . . . . . . . . . . 14 ..^ $/\$ bits ..^ ..^ bits ..^
34	31, 32, 33	mp2an 672	. . . . . . . . . . . . 13 bits ..^
35		elfpw 7822	. . . . . . . . . . . . 13 bits ..^ bits ..^ $/\$ bits ..^
36	30, 34, 35	mpbir2an 918	. . . . . . . . . . . 12 bits ..^
37		f1ocnv 5828	. . . . . . . . . . . . . . 15 bits bits
38		f1of 5816	. . . . . . . . . . . . . . 15 bits bits
39	14, 37, 38	mp2b 10	. . . . . . . . . . . . . 14 bits
40	1	feq1i 5723	. . . . . . . . . . . . . 14 bits
41	39, 40	mpbir 209	. . . . . . . . . . . . 13
42	41	ffvelrni 6020	. . . . . . . . . . . 12 bits ..^ bits ..^
43	36, 42	mp1i 12	. . . . . . . . . . 11 bits ..^
44	43	nn0zd 10964	. . . . . . . . . 10 bits ..^
45	3, 44	zsubcld 10971	. . . . . . . . 9 bits ..^
46		dvdsval2 13850	. . . . . . . . 9 $/\$ $/\$ bits ..^ bits ..^ bits ..^
47	26, 27, 45, 46	syl3anc 1228	. . . . . . . 8 bits ..^ bits ..^
48	25, 47	mpbird 232	. . . . . . 7 bits ..^
49	1	fveq1i 5867	. . . . . . . . . . . 12 bits ..^ bits bits ..^
50		sadaddlem.2	. . . . . . . . . . . . . . . 16
51	50, 7	zmodcld 11984	. . . . . . . . . . . . . . 15
52		fvres 5880	. . . . . . . . . . . . . . 15 bits bits
53	51, 52	syl 16	. . . . . . . . . . . . . 14 bits bits
54		bitsmod 13945	. . . . . . . . . . . . . . 15 $/\$ bits bits ..^
55	50, 6, 54	syl2anc 661	. . . . . . . . . . . . . 14 bits bits ..^
56	53, 55	eqtrd 2508	. . . . . . . . . . . . 13 bits bits ..^
57		f1ocnvfv 6172	. . . . . . . . . . . . . 14 bits $/\$ bits bits ..^ bits bits ..^
58	14, 51, 57	sylancr 663	. . . . . . . . . . . . 13 bits bits ..^ bits bits ..^
59	56, 58	mpd 15	. . . . . . . . . . . 12 bits bits ..^
60	49, 59	syl5eq 2520	. . . . . . . . . . 11 bits ..^
61	60	oveq2d 6300	. . . . . . . . . 10 bits ..^
62	61	oveq1d 6299	. . . . . . . . 9 bits ..^
63	50	zred 10966	. . . . . . . . . 10
64		moddifz 11976	. . . . . . . . . 10 $/\$
65	63, 22, 64	syl2anc 661	. . . . . . . . 9
66	62, 65	eqeltrd 2555	. . . . . . . 8 bits ..^
67		inss1 3718	. . . . . . . . . . . . . 14 bits ..^ bits
68		bitsss 13935	. . . . . . . . . . . . . 14 bits
69	67, 68	sstri 3513	. . . . . . . . . . . . 13 bits ..^
70		inss2 3719	. . . . . . . . . . . . . 14 bits ..^ ..^
71		ssfi 7740	. . . . . . . . . . . . . 14 ..^ $/\$ bits ..^ ..^ bits ..^
72	31, 70, 71	mp2an 672	. . . . . . . . . . . . 13 bits ..^
73		elfpw 7822	. . . . . . . . . . . . 13 bits ..^ bits ..^ $/\$ bits ..^
74	69, 72, 73	mpbir2an 918	. . . . . . . . . . . 12 bits ..^
75	41	ffvelrni 6020	. . . . . . . . . . . 12 bits ..^ bits ..^
76	74, 75	mp1i 12	. . . . . . . . . . 11 bits ..^
77	76	nn0zd 10964	. . . . . . . . . 10 bits ..^
78	50, 77	zsubcld 10971	. . . . . . . . 9 bits ..^
79		dvdsval2 13850	. . . . . . . . 9 $/\$ $/\$ bits ..^ bits ..^ bits ..^
80	26, 27, 78, 79	syl3anc 1228	. . . . . . . 8 bits ..^ bits ..^
81	66, 80	mpbird 232	. . . . . . 7 bits ..^
82		dvds2add 13876	. . . . . . . 8 $/\$ bits ..^ $/\$ bits ..^ bits ..^ $/\$ bits ..^ bits ..^ bits ..^
83	26, 45, 78, 82	syl3anc 1228	. . . . . . 7 bits ..^ $/\$ bits ..^ bits ..^ bits ..^
84	48, 81, 83	mp2and 679	. . . . . 6 bits ..^ bits ..^
85	3	zcnd 10967	. . . . . . 7
86	50	zcnd 10967	. . . . . . 7
87	43	nn0cnd 10854	. . . . . . 7 bits ..^
88	76	nn0cnd 10854	. . . . . . 7 bits ..^
89	85, 86, 87, 88	addsub4d 9977	. . . . . 6 bits ..^ bits ..^ bits ..^ bits ..^
90	84, 89	breqtrrd 4473	. . . . 5 bits ..^ bits ..^
91	3, 50	zaddcld 10970	. . . . . 6
92	44, 77	zaddcld 10970	. . . . . 6 bits ..^ bits ..^
93		moddvds 13854	. . . . . 6 $/\$ $/\$ bits ..^ bits ..^ bits ..^ bits ..^ bits ..^ bits ..^
94	7, 91, 92, 93	syl3anc 1228	. . . . 5 bits ..^ bits ..^ bits ..^ bits ..^
95	90, 94	mpbird 232	. . . 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 13970	. . . 4 bits sadd bits ..^ bits ..^ bits ..^
100		inss1 3718	. . . . . . . . 9 bits sadd bits ..^ bits sadd bits
101		sadcl 13971	. . . . . . . . . 10 bits $/\$ bits bits sadd bits
102	29, 68, 101	mp2an 672	. . . . . . . . 9 bits sadd bits
103	100, 102	sstri 3513	. . . . . . . 8 bits sadd bits ..^
104		inss2 3719	. . . . . . . . 9 bits sadd bits ..^ ..^
105		ssfi 7740	. . . . . . . . 9 ..^ $/\$ bits sadd bits ..^ ..^ bits sadd bits ..^
106	31, 104, 105	mp2an 672	. . . . . . . 8 bits sadd bits ..^
107		elfpw 7822	. . . . . . . 8 bits sadd bits ..^ bits sadd bits ..^ $/\$ bits sadd bits ..^
108	103, 106, 107	mpbir2an 918	. . . . . . 7 bits sadd bits ..^
109	41	ffvelrni 6020	. . . . . . 7 bits sadd bits ..^ bits sadd bits ..^
110	108, 109	mp1i 12	. . . . . 6 bits sadd bits ..^
111	110	nn0red 10853	. . . . 5 bits sadd bits ..^
112	110	nn0ge0d 10855	. . . . 5 bits sadd bits ..^
113	1	fveq1i 5867	. . . . . . . . . 10 bits sadd bits ..^ bits bits sadd bits ..^
114	113	fveq2i 5869	. . . . . . . . 9 bits bits sadd bits ..^ bits bits bits sadd bits ..^
115		fvres 5880	. . . . . . . . . 10 bits sadd bits ..^ bits bits sadd bits ..^ bitsbits sadd bits ..^
116	110, 115	syl 16	. . . . . . . . 9 bits bits sadd bits ..^ bitsbits sadd bits ..^
117	108	a1i 11	. . . . . . . . . 10 bits sadd bits ..^
118		f1ocnvfv2 6171	. . . . . . . . . 10 bits $/\$ bits sadd bits ..^ bits bits bits sadd bits ..^ bits sadd bits ..^
119	14, 117, 118	sylancr 663	. . . . . . . . 9 bits bits bits sadd bits ..^ bits sadd bits ..^
120	114, 116, 119	3eqtr3a 2532	. . . . . . . 8 bitsbits sadd bits ..^ bits sadd bits ..^
121	120, 104	syl6eqss 3554	. . . . . . 7 bitsbits sadd bits ..^ ..^
122	110	nn0zd 10964	. . . . . . . 8 bits sadd bits ..^
123		bitsfzo 13944	. . . . . . . 8 bits sadd bits ..^ $/\$ bits sadd bits ..^ ..^ bitsbits sadd bits ..^ ..^
124	122, 6, 123	syl2anc 661	. . . . . . 7 bits sadd bits ..^ ..^ bitsbits sadd bits ..^ ..^
125	121, 124	mpbird 232	. . . . . 6 bits sadd bits ..^ ..^
126		elfzolt2 11805	. . . . . 6 bits sadd bits ..^ ..^ bits sadd bits ..^
127	125, 126	syl 16	. . . . 5 bits sadd bits ..^
128		modid 11988	. . . . 5 bits sadd bits ..^ $/\$ $/\$ bits sadd bits ..^ $/\$ bits sadd bits ..^ bits sadd bits ..^ bits sadd bits ..^
129	111, 22, 112, 127, 128	syl22anc 1229	. . . 4 bits sadd bits ..^ bits sadd bits ..^
130	95, 99, 129	3eqtr2d 2514	. . 3 bits sadd bits ..^
131	130	fveq2d 5870	. 2 bits bitsbits sadd bits ..^
132	131, 120	eqtr2d 2509	1 bits sadd bits ..^ bits

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369

wceq 1379 caddwcad 1430

wcel 1767

wne 2662

cin 3475

wss 3476

c0 3785

cif 3939

cpw 4010 class class class wbr 4447

cmpt 4505

ccnv 4998

cres 5001

wf 5584

wf1o 5587

cfv 5588 (class class class)co 6284

cmpt2 6286

c1o 7123

c2o 7124

cfn 7516

cr 9491

cc0 9492

c1 9493

caddc 9495

clt 9628

cle 9629

cmin 9805

cdiv 10206

cn 10536

c2 10585

cn0 10795

cz 10864

crp 11220 ..^cfzo 11792

cmo 11964

cseq 12075

cexp 12134

cdivides 13847 bitscbits 13928 sadd csad 13929

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6576 ax-inf2 8058 ax-cnex 9548 ax-resscn 9549 ax-1cn 9550 ax-icn 9551 ax-addcl 9552 ax-addrcl 9553 ax-mulcl 9554 ax-mulrcl 9555 ax-mulcom 9556 ax-addass 9557 ax-mulass 9558 ax-distr 9559 ax-i2m1 9560 ax-1ne0 9561 ax-1rid 9562 ax-rnegex 9563 ax-rrecex 9564 ax-cnre 9565 ax-pre-lttri 9566 ax-pre-lttrn 9567 ax-pre-ltadd 9568 ax-pre-mulgt0 9569 ax-pre-sup 9570

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-xor 1361 df-tru 1382 df-fal 1385 df-had 1431 df-cad 1432 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-disj 4418 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-isom 5597 df-riota 6245 df-ov 6287 df-oprab 6288 df-mpt2 6289 df-om 6685 df-1st 6784 df-2nd 6785 df-recs 7042 df-rdg 7076 df-1o 7130 df-2o 7131 df-oadd 7134 df-er 7311 df-map 7422 df-pm 7423 df-en 7517 df-dom 7518 df-sdom 7519 df-fin 7520 df-sup 7901 df-oi 7935 df-card 8320 df-cda 8548 df-pnf 9630 df-mnf 9631 df-xr 9632 df-ltxr 9633 df-le 9634 df-sub 9807 df-neg 9808 df-div 10207 df-nn 10537 df-2 10594 df-3 10595 df-n0 10796 df-z 10865 df-uz 11083 df-rp 11221 df-fz 11673 df-fzo 11793 df-fl 11897 df-mod 11965 df-seq 12076 df-exp 12135 df-hash 12374 df-cj 12895 df-re 12896 df-im 12897 df-sqrt 13031 df-abs 13032 df-clim 13274 df-sum 13472 df-dvds 13848 df-bits 13931 df-sad 13960

This theorem is referenced by: sadadd 13976

W3C validator