sadasslem - Metamath Proof Explorer

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

Theorem sadasslem 14131

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

**Hypotheses**
Ref	Expression
sadasslem.1
sadasslem.2
sadasslem.3
sadasslem.4

**Assertion**
Ref	Expression
sadasslem	sadd sadd ..^ sadd sadd ..^

Proof of Theorem sadasslem Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		inss1 3714	. . . . . . . . . . 11 ..^
2		sadasslem.1	. . . . . . . . . . 11
3	1, 2	syl5ss 3510	. . . . . . . . . 10 ..^
4		fzofi 12086	. . . . . . . . . . . 12 ..^
5	4	a1i 11	. . . . . . . . . . 11 ..^
6		inss2 3715	. . . . . . . . . . 11 ..^ ..^
7		ssfi 7759	. . . . . . . . . . 11 ..^ $/\$ ..^ ..^ ..^
8	5, 6, 7	sylancl 662	. . . . . . . . . 10 ..^
9		elfpw 7840	. . . . . . . . . 10 ..^ ..^ $/\$ ..^
10	3, 8, 9	sylanbrc 664	. . . . . . . . 9 ..^
11		bitsf1o 14106	. . . . . . . . . . 11 bits
12		f1ocnv 5834	. . . . . . . . . . 11 bits bits
13		f1of 5822	. . . . . . . . . . 11 bits bits
14	11, 12, 13	mp2b 10	. . . . . . . . . 10 bits
15	14	ffvelrni 6031	. . . . . . . . 9 ..^ bits ..^
16	10, 15	syl 16	. . . . . . . 8 bits ..^
17	16	nn0cnd 10875	. . . . . . 7 bits ..^
18		inss1 3714	. . . . . . . . . . 11 ..^
19		sadasslem.2	. . . . . . . . . . 11
20	18, 19	syl5ss 3510	. . . . . . . . . 10 ..^
21		inss2 3715	. . . . . . . . . . 11 ..^ ..^
22		ssfi 7759	. . . . . . . . . . 11 ..^ $/\$ ..^ ..^ ..^
23	5, 21, 22	sylancl 662	. . . . . . . . . 10 ..^
24		elfpw 7840	. . . . . . . . . 10 ..^ ..^ $/\$ ..^
25	20, 23, 24	sylanbrc 664	. . . . . . . . 9 ..^
26	14	ffvelrni 6031	. . . . . . . . 9 ..^ bits ..^
27	25, 26	syl 16	. . . . . . . 8 bits ..^
28	27	nn0cnd 10875	. . . . . . 7 bits ..^
29		inss1 3714	. . . . . . . . . . 11 ..^
30		sadasslem.3	. . . . . . . . . . 11
31	29, 30	syl5ss 3510	. . . . . . . . . 10 ..^
32		inss2 3715	. . . . . . . . . . 11 ..^ ..^
33		ssfi 7759	. . . . . . . . . . 11 ..^ $/\$ ..^ ..^ ..^
34	5, 32, 33	sylancl 662	. . . . . . . . . 10 ..^
35		elfpw 7840	. . . . . . . . . 10 ..^ ..^ $/\$ ..^
36	31, 34, 35	sylanbrc 664	. . . . . . . . 9 ..^
37	14	ffvelrni 6031	. . . . . . . . 9 ..^ bits ..^
38	36, 37	syl 16	. . . . . . . 8 bits ..^
39	38	nn0cnd 10875	. . . . . . 7 bits ..^
40	17, 28, 39	addassd 9635	. . . . . 6 bits ..^ bits ..^ bits ..^ bits ..^ bits ..^ bits ..^
41	40	oveq1d 6311	. . . . 5 bits ..^ bits ..^ bits ..^ bits ..^ bits ..^ bits ..^
42		inss1 3714	. . . . . . . . . 10 sadd ..^ sadd
43		sadcl 14123	. . . . . . . . . . 11 $/\$ sadd
44	2, 19, 43	syl2anc 661	. . . . . . . . . 10 sadd
45	42, 44	syl5ss 3510	. . . . . . . . 9 sadd ..^
46		inss2 3715	. . . . . . . . . 10 sadd ..^ ..^
47		ssfi 7759	. . . . . . . . . 10 ..^ $/\$ sadd ..^ ..^ sadd ..^
48	5, 46, 47	sylancl 662	. . . . . . . . 9 sadd ..^
49		elfpw 7840	. . . . . . . . 9 sadd ..^ sadd ..^ $/\$ sadd ..^
50	45, 48, 49	sylanbrc 664	. . . . . . . 8 sadd ..^
51	14	ffvelrni 6031	. . . . . . . 8 sadd ..^ bits sadd ..^
52	50, 51	syl 16	. . . . . . 7 bits sadd ..^
53	52	nn0red 10874	. . . . . 6 bits sadd ..^
54	16	nn0red 10874	. . . . . . 7 bits ..^
55	27	nn0red 10874	. . . . . . 7 bits ..^
56	54, 55	readdcld 9640	. . . . . 6 bits ..^ bits ..^
57	38	nn0red 10874	. . . . . 6 bits ..^
58		2rp 11250	. . . . . . . 8
59	58	a1i 11	. . . . . . 7
60		sadasslem.4	. . . . . . . 8
61	60	nn0zd 10988	. . . . . . 7
62	59, 61	rpexpcld 12335	. . . . . 6
63		eqid 2457	. . . . . . 7 cadd cadd
64		eqid 2457	. . . . . . 7 bits bits
65	2, 19, 63, 60, 64	sadadd3 14122	. . . . . 6 bits sadd ..^ bits ..^ bits ..^
66		eqidd 2458	. . . . . 6 bits ..^ bits ..^
67	53, 56, 57, 57, 62, 65, 66	modadd12d 12045	. . . . 5 bits sadd ..^ bits ..^ bits ..^ bits ..^ bits ..^
68		inss1 3714	. . . . . . . . . 10 sadd ..^ sadd
69		sadcl 14123	. . . . . . . . . . 11 $/\$ sadd
70	19, 30, 69	syl2anc 661	. . . . . . . . . 10 sadd
71	68, 70	syl5ss 3510	. . . . . . . . 9 sadd ..^
72		inss2 3715	. . . . . . . . . 10 sadd ..^ ..^
73		ssfi 7759	. . . . . . . . . 10 ..^ $/\$ sadd ..^ ..^ sadd ..^
74	5, 72, 73	sylancl 662	. . . . . . . . 9 sadd ..^
75		elfpw 7840	. . . . . . . . 9 sadd ..^ sadd ..^ $/\$ sadd ..^
76	71, 74, 75	sylanbrc 664	. . . . . . . 8 sadd ..^
77	14	ffvelrni 6031	. . . . . . . 8 sadd ..^ bits sadd ..^
78	76, 77	syl 16	. . . . . . 7 bits sadd ..^
79	78	nn0red 10874	. . . . . 6 bits sadd ..^
80	55, 57	readdcld 9640	. . . . . 6 bits ..^ bits ..^
81		eqidd 2458	. . . . . 6 bits ..^ bits ..^
82		eqid 2457	. . . . . . 7 cadd cadd
83	19, 30, 82, 60, 64	sadadd3 14122	. . . . . 6 bits sadd ..^ bits ..^ bits ..^
84	54, 54, 79, 80, 62, 81, 83	modadd12d 12045	. . . . 5 bits ..^ bits sadd ..^ bits ..^ bits ..^ bits ..^
85	41, 67, 84	3eqtr4d 2508	. . . 4 bits sadd ..^ bits ..^ bits ..^ bits sadd ..^
86		eqid 2457	. . . . 5 cadd sadd cadd sadd
87	44, 30, 86, 60, 64	sadadd3 14122	. . . 4 bits sadd sadd ..^ bits sadd ..^ bits ..^
88		eqid 2457	. . . . 5 cadd sadd cadd sadd
89	2, 70, 88, 60, 64	sadadd3 14122	. . . 4 bits sadd sadd ..^ bits ..^ bits sadd ..^
90	85, 87, 89	3eqtr4d 2508	. . 3 bits sadd sadd ..^ bits sadd sadd ..^
91		inss1 3714	. . . . . . . 8 sadd sadd ..^ sadd sadd
92		sadcl 14123	. . . . . . . . 9 sadd $/\$ sadd sadd
93	44, 30, 92	syl2anc 661	. . . . . . . 8 sadd sadd
94	91, 93	syl5ss 3510	. . . . . . 7 sadd sadd ..^
95		inss2 3715	. . . . . . . 8 sadd sadd ..^ ..^
96		ssfi 7759	. . . . . . . 8 ..^ $/\$ sadd sadd ..^ ..^ sadd sadd ..^
97	5, 95, 96	sylancl 662	. . . . . . 7 sadd sadd ..^
98		elfpw 7840	. . . . . . 7 sadd sadd ..^ sadd sadd ..^ $/\$ sadd sadd ..^
99	94, 97, 98	sylanbrc 664	. . . . . 6 sadd sadd ..^
100	14	ffvelrni 6031	. . . . . 6 sadd sadd ..^ bits sadd sadd ..^
101	99, 100	syl 16	. . . . 5 bits sadd sadd ..^
102	101	nn0red 10874	. . . 4 bits sadd sadd ..^
103	101	nn0ge0d 10876	. . . 4 bits sadd sadd ..^
104		fvres 5886	. . . . . . . . 9 bits sadd sadd ..^ bits bits sadd sadd ..^ bitsbits sadd sadd ..^
105	101, 104	syl 16	. . . . . . . 8 bits bits sadd sadd ..^ bitsbits sadd sadd ..^
106		f1ocnvfv2 6184	. . . . . . . . 9 bits $/\$ sadd sadd ..^ bits bits sadd sadd ..^ sadd sadd ..^
107	11, 99, 106	sylancr 663	. . . . . . . 8 bits bits sadd sadd ..^ sadd sadd ..^
108	105, 107	eqtr3d 2500	. . . . . . 7 bitsbits sadd sadd ..^ sadd sadd ..^
109	108, 95	syl6eqss 3549	. . . . . 6 bitsbits sadd sadd ..^ ..^
110	101	nn0zd 10988	. . . . . . 7 bits sadd sadd ..^
111		bitsfzo 14096	. . . . . . 7 bits sadd sadd ..^ $/\$ bits sadd sadd ..^ ..^ bitsbits sadd sadd ..^ ..^
112	110, 60, 111	syl2anc 661	. . . . . 6 bits sadd sadd ..^ ..^ bitsbits sadd sadd ..^ ..^
113	109, 112	mpbird 232	. . . . 5 bits sadd sadd ..^ ..^
114		elfzolt2 11834	. . . . 5 bits sadd sadd ..^ ..^ bits sadd sadd ..^
115	113, 114	syl 16	. . . 4 bits sadd sadd ..^
116		modid 12022	. . . 4 bits sadd sadd ..^ $/\$ $/\$ bits sadd sadd ..^ $/\$ bits sadd sadd ..^ bits sadd sadd ..^ bits sadd sadd ..^
117	102, 62, 103, 115, 116	syl22anc 1229	. . 3 bits sadd sadd ..^ bits sadd sadd ..^
118		inss1 3714	. . . . . . . 8 sadd sadd ..^ sadd sadd
119		sadcl 14123	. . . . . . . . 9 $/\$ sadd sadd sadd
120	2, 70, 119	syl2anc 661	. . . . . . . 8 sadd sadd
121	118, 120	syl5ss 3510	. . . . . . 7 sadd sadd ..^
122		inss2 3715	. . . . . . . 8 sadd sadd ..^ ..^
123		ssfi 7759	. . . . . . . 8 ..^ $/\$ sadd sadd ..^ ..^ sadd sadd ..^
124	5, 122, 123	sylancl 662	. . . . . . 7 sadd sadd ..^
125		elfpw 7840	. . . . . . 7 sadd sadd ..^ sadd sadd ..^ $/\$ sadd sadd ..^
126	121, 124, 125	sylanbrc 664	. . . . . 6 sadd sadd ..^
127	14	ffvelrni 6031	. . . . . 6 sadd sadd ..^ bits sadd sadd ..^
128	126, 127	syl 16	. . . . 5 bits sadd sadd ..^
129	128	nn0red 10874	. . . 4 bits sadd sadd ..^
130		2nn 10714	. . . . . . 7
131	130	a1i 11	. . . . . 6
132	131, 60	nnexpcld 12333	. . . . 5
133	132	nnrpd 11280	. . . 4
134	128	nn0ge0d 10876	. . . 4 bits sadd sadd ..^
135		fvres 5886	. . . . . . . . 9 bits sadd sadd ..^ bits bits sadd sadd ..^ bitsbits sadd sadd ..^
136	128, 135	syl 16	. . . . . . . 8 bits bits sadd sadd ..^ bitsbits sadd sadd ..^
137		f1ocnvfv2 6184	. . . . . . . . 9 bits $/\$ sadd sadd ..^ bits bits sadd sadd ..^ sadd sadd ..^
138	11, 126, 137	sylancr 663	. . . . . . . 8 bits bits sadd sadd ..^ sadd sadd ..^
139	136, 138	eqtr3d 2500	. . . . . . 7 bitsbits sadd sadd ..^ sadd sadd ..^
140	139, 122	syl6eqss 3549	. . . . . 6 bitsbits sadd sadd ..^ ..^
141	128	nn0zd 10988	. . . . . . 7 bits sadd sadd ..^
142		bitsfzo 14096	. . . . . . 7 bits sadd sadd ..^ $/\$ bits sadd sadd ..^ ..^ bitsbits sadd sadd ..^ ..^
143	141, 60, 142	syl2anc 661	. . . . . 6 bits sadd sadd ..^ ..^ bitsbits sadd sadd ..^ ..^
144	140, 143	mpbird 232	. . . . 5 bits sadd sadd ..^ ..^
145		elfzolt2 11834	. . . . 5 bits sadd sadd ..^ ..^ bits sadd sadd ..^
146	144, 145	syl 16	. . . 4 bits sadd sadd ..^
147		modid 12022	. . . 4 bits sadd sadd ..^ $/\$ $/\$ bits sadd sadd ..^ $/\$ bits sadd sadd ..^ bits sadd sadd ..^ bits sadd sadd ..^
148	129, 133, 134, 146, 147	syl22anc 1229	. . 3 bits sadd sadd ..^ bits sadd sadd ..^
149	90, 117, 148	3eqtr3d 2506	. 2 bits sadd sadd ..^ bits sadd sadd ..^
150		f1of1 5821	. . . . 5 bits bits
151	11, 12, 150	mp2b 10	. . . 4 bits
152		f1fveq 6171	. . . 4 bits $/\$ sadd sadd ..^ $/\$ sadd sadd ..^ bits sadd sadd ..^ bits sadd sadd ..^ sadd sadd ..^ sadd sadd ..^
153	151, 152	mpan 670	. . 3 sadd sadd ..^ $/\$ sadd sadd ..^ bits sadd sadd ..^ bits sadd sadd ..^ sadd sadd ..^ sadd sadd ..^
154	99, 126, 153	syl2anc 661	. 2 bits sadd sadd ..^ bits sadd sadd ..^ sadd sadd ..^ sadd sadd ..^
155	149, 154	mpbid 210	1 sadd sadd ..^ sadd sadd ..^

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369

wceq 1395 caddwcad 1446

wcel 1819

cin 3470

wss 3471

c0 3793

cif 3944

cpw 4015 class class class wbr 4456

cmpt 4515

ccnv 5007

cres 5010

wf 5590

wf1 5591

wf1o 5593

cfv 5594 (class class class)co 6296

cmpt2 6298

c1o 7141

c2o 7142

cfn 7535

cr 9508

cc0 9509

c1 9510

caddc 9512

clt 9645

cle 9646

cmin 9824

cn 10556

c2 10606

cn0 10816

cz 10885

crp 11245 ..^cfzo 11820

cmo 11998

cseq 12109

cexp 12168 bitscbits 14080 sadd csad 14081

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-inf2 8075 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-xor 1364 df-tru 1398 df-fal 1401 df-had 1447 df-cad 1448 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-disj 4428 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-se 4848 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-isom 5603 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-1o 7148 df-2o 7149 df-oadd 7152 df-er 7329 df-map 7440 df-pm 7441 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-sup 7919 df-oi 7953 df-card 8337 df-cda 8565 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-n0 10817 df-z 10886 df-uz 11107 df-rp 11246 df-fz 11698 df-fzo 11821 df-fl 11931 df-mod 11999 df-seq 12110 df-exp 12169 df-hash 12408 df-cj 12943 df-re 12944 df-im 12945 df-sqrt 13079 df-abs 13080 df-clim 13322 df-sum 13520 df-dvds 13998 df-bits 14083 df-sad 14112

This theorem is referenced by: sadass 14132

W3C validator