sadasslem - Metamath Proof Explorer

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

Theorem sadasslem 12937

Description: Lemma for sadass 12938. (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 3521	. . . . . . . . . . 11 ..^
2		sadasslem.1	. . . . . . . . . . 11
3	1, 2	syl5ss 3319	. . . . . . . . . 10 ..^
4		fzofi 11268	. . . . . . . . . . . 12 ..^
5	4	a1i 11	. . . . . . . . . . 11 ..^
6		inss2 3522	. . . . . . . . . . 11 ..^ ..^
7		ssfi 7288	. . . . . . . . . . 11 ..^ $/\$ ..^ ..^ ..^
8	5, 6, 7	sylancl 644	. . . . . . . . . 10 ..^
9		elfpw 7366	. . . . . . . . . 10 ..^ ..^ $/\$ ..^
10	3, 8, 9	sylanbrc 646	. . . . . . . . 9 ..^
11		bitsf1o 12912	. . . . . . . . . . 11 bits
12		f1ocnv 5646	. . . . . . . . . . 11 bits bits
13		f1of 5633	. . . . . . . . . . 11 bits bits
14	11, 12, 13	mp2b 10	. . . . . . . . . 10 bits
15	14	ffvelrni 5828	. . . . . . . . 9 ..^ bits ..^
16	10, 15	syl 16	. . . . . . . 8 bits ..^
17	16	nn0cnd 10232	. . . . . . 7 bits ..^
18		inss1 3521	. . . . . . . . . . 11 ..^
19		sadasslem.2	. . . . . . . . . . 11
20	18, 19	syl5ss 3319	. . . . . . . . . 10 ..^
21		inss2 3522	. . . . . . . . . . 11 ..^ ..^
22		ssfi 7288	. . . . . . . . . . 11 ..^ $/\$ ..^ ..^ ..^
23	5, 21, 22	sylancl 644	. . . . . . . . . 10 ..^
24		elfpw 7366	. . . . . . . . . 10 ..^ ..^ $/\$ ..^
25	20, 23, 24	sylanbrc 646	. . . . . . . . 9 ..^
26	14	ffvelrni 5828	. . . . . . . . 9 ..^ bits ..^
27	25, 26	syl 16	. . . . . . . 8 bits ..^
28	27	nn0cnd 10232	. . . . . . 7 bits ..^
29		inss1 3521	. . . . . . . . . . 11 ..^
30		sadasslem.3	. . . . . . . . . . 11
31	29, 30	syl5ss 3319	. . . . . . . . . 10 ..^
32		inss2 3522	. . . . . . . . . . 11 ..^ ..^
33		ssfi 7288	. . . . . . . . . . 11 ..^ $/\$ ..^ ..^ ..^
34	5, 32, 33	sylancl 644	. . . . . . . . . 10 ..^
35		elfpw 7366	. . . . . . . . . 10 ..^ ..^ $/\$ ..^
36	31, 34, 35	sylanbrc 646	. . . . . . . . 9 ..^
37	14	ffvelrni 5828	. . . . . . . . 9 ..^ bits ..^
38	36, 37	syl 16	. . . . . . . 8 bits ..^
39	38	nn0cnd 10232	. . . . . . 7 bits ..^
40	17, 28, 39	addassd 9066	. . . . . 6 bits ..^ bits ..^ bits ..^ bits ..^ bits ..^ bits ..^
41	40	oveq1d 6055	. . . . 5 bits ..^ bits ..^ bits ..^ bits ..^ bits ..^ bits ..^
42		inss1 3521	. . . . . . . . . 10 sadd ..^ sadd
43		sadcl 12929	. . . . . . . . . . 11 $/\$ sadd
44	2, 19, 43	syl2anc 643	. . . . . . . . . 10 sadd
45	42, 44	syl5ss 3319	. . . . . . . . 9 sadd ..^
46		inss2 3522	. . . . . . . . . 10 sadd ..^ ..^
47		ssfi 7288	. . . . . . . . . 10 ..^ $/\$ sadd ..^ ..^ sadd ..^
48	5, 46, 47	sylancl 644	. . . . . . . . 9 sadd ..^
49		elfpw 7366	. . . . . . . . 9 sadd ..^ sadd ..^ $/\$ sadd ..^
50	45, 48, 49	sylanbrc 646	. . . . . . . 8 sadd ..^
51	14	ffvelrni 5828	. . . . . . . 8 sadd ..^ bits sadd ..^
52	50, 51	syl 16	. . . . . . 7 bits sadd ..^
53	52	nn0red 10231	. . . . . 6 bits sadd ..^
54	16	nn0red 10231	. . . . . . 7 bits ..^
55	27	nn0red 10231	. . . . . . 7 bits ..^
56	54, 55	readdcld 9071	. . . . . 6 bits ..^ bits ..^
57	38	nn0red 10231	. . . . . 6 bits ..^
58		2rp 10573	. . . . . . . 8
59	58	a1i 11	. . . . . . 7
60		sadasslem.4	. . . . . . . 8
61	60	nn0zd 10329	. . . . . . 7
62	59, 61	rpexpcld 11501	. . . . . 6
63		eqid 2404	. . . . . . 7 cadd cadd
64		eqid 2404	. . . . . . 7 bits bits
65	2, 19, 63, 60, 64	sadadd3 12928	. . . . . 6 bits sadd ..^ bits ..^ bits ..^
66		eqidd 2405	. . . . . 6 bits ..^ bits ..^
67	53, 56, 57, 57, 62, 65, 66	modadd12d 11237	. . . . 5 bits sadd ..^ bits ..^ bits ..^ bits ..^ bits ..^
68		inss1 3521	. . . . . . . . . 10 sadd ..^ sadd
69		sadcl 12929	. . . . . . . . . . 11 $/\$ sadd
70	19, 30, 69	syl2anc 643	. . . . . . . . . 10 sadd
71	68, 70	syl5ss 3319	. . . . . . . . 9 sadd ..^
72		inss2 3522	. . . . . . . . . 10 sadd ..^ ..^
73		ssfi 7288	. . . . . . . . . 10 ..^ $/\$ sadd ..^ ..^ sadd ..^
74	5, 72, 73	sylancl 644	. . . . . . . . 9 sadd ..^
75		elfpw 7366	. . . . . . . . 9 sadd ..^ sadd ..^ $/\$ sadd ..^
76	71, 74, 75	sylanbrc 646	. . . . . . . 8 sadd ..^
77	14	ffvelrni 5828	. . . . . . . 8 sadd ..^ bits sadd ..^
78	76, 77	syl 16	. . . . . . 7 bits sadd ..^
79	78	nn0red 10231	. . . . . 6 bits sadd ..^
80	55, 57	readdcld 9071	. . . . . 6 bits ..^ bits ..^
81		eqidd 2405	. . . . . 6 bits ..^ bits ..^
82		eqid 2404	. . . . . . 7 cadd cadd
83	19, 30, 82, 60, 64	sadadd3 12928	. . . . . 6 bits sadd ..^ bits ..^ bits ..^
84	54, 54, 79, 80, 62, 81, 83	modadd12d 11237	. . . . 5 bits ..^ bits sadd ..^ bits ..^ bits ..^ bits ..^
85	41, 67, 84	3eqtr4d 2446	. . . 4 bits sadd ..^ bits ..^ bits ..^ bits sadd ..^
86		eqid 2404	. . . . 5 cadd sadd cadd sadd
87	44, 30, 86, 60, 64	sadadd3 12928	. . . 4 bits sadd sadd ..^ bits sadd ..^ bits ..^
88		eqid 2404	. . . . 5 cadd sadd cadd sadd
89	2, 70, 88, 60, 64	sadadd3 12928	. . . 4 bits sadd sadd ..^ bits ..^ bits sadd ..^
90	85, 87, 89	3eqtr4d 2446	. . 3 bits sadd sadd ..^ bits sadd sadd ..^
91		inss1 3521	. . . . . . . 8 sadd sadd ..^ sadd sadd
92		sadcl 12929	. . . . . . . . 9 sadd $/\$ sadd sadd
93	44, 30, 92	syl2anc 643	. . . . . . . 8 sadd sadd
94	91, 93	syl5ss 3319	. . . . . . 7 sadd sadd ..^
95		inss2 3522	. . . . . . . 8 sadd sadd ..^ ..^
96		ssfi 7288	. . . . . . . 8 ..^ $/\$ sadd sadd ..^ ..^ sadd sadd ..^
97	5, 95, 96	sylancl 644	. . . . . . 7 sadd sadd ..^
98		elfpw 7366	. . . . . . 7 sadd sadd ..^ sadd sadd ..^ $/\$ sadd sadd ..^
99	94, 97, 98	sylanbrc 646	. . . . . 6 sadd sadd ..^
100	14	ffvelrni 5828	. . . . . 6 sadd sadd ..^ bits sadd sadd ..^
101	99, 100	syl 16	. . . . 5 bits sadd sadd ..^
102	101	nn0red 10231	. . . 4 bits sadd sadd ..^
103	101	nn0ge0d 10233	. . . 4 bits sadd sadd ..^
104		fvres 5704	. . . . . . . . 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 5974	. . . . . . . . 9 bits $/\$ sadd sadd ..^ bits bits sadd sadd ..^ sadd sadd ..^
107	11, 99, 106	sylancr 645	. . . . . . . 8 bits bits sadd sadd ..^ sadd sadd ..^
108	105, 107	eqtr3d 2438	. . . . . . 7 bitsbits sadd sadd ..^ sadd sadd ..^
109	108, 95	syl6eqss 3358	. . . . . 6 bitsbits sadd sadd ..^ ..^
110	101	nn0zd 10329	. . . . . . 7 bits sadd sadd ..^
111		bitsfzo 12902	. . . . . . 7 bits sadd sadd ..^ $/\$ bits sadd sadd ..^ ..^ bitsbits sadd sadd ..^ ..^
112	110, 60, 111	syl2anc 643	. . . . . 6 bits sadd sadd ..^ ..^ bitsbits sadd sadd ..^ ..^
113	109, 112	mpbird 224	. . . . 5 bits sadd sadd ..^ ..^
114		elfzolt2 11103	. . . . 5 bits sadd sadd ..^ ..^ bits sadd sadd ..^
115	113, 114	syl 16	. . . 4 bits sadd sadd ..^
116		modid 11225	. . . 4 bits sadd sadd ..^ $/\$ $/\$ bits sadd sadd ..^ $/\$ bits sadd sadd ..^ bits sadd sadd ..^ bits sadd sadd ..^
117	102, 62, 103, 115, 116	syl22anc 1185	. . 3 bits sadd sadd ..^ bits sadd sadd ..^
118		inss1 3521	. . . . . . . 8 sadd sadd ..^ sadd sadd
119		sadcl 12929	. . . . . . . . 9 $/\$ sadd sadd sadd
120	2, 70, 119	syl2anc 643	. . . . . . . 8 sadd sadd
121	118, 120	syl5ss 3319	. . . . . . 7 sadd sadd ..^
122		inss2 3522	. . . . . . . 8 sadd sadd ..^ ..^
123		ssfi 7288	. . . . . . . 8 ..^ $/\$ sadd sadd ..^ ..^ sadd sadd ..^
124	5, 122, 123	sylancl 644	. . . . . . 7 sadd sadd ..^
125		elfpw 7366	. . . . . . 7 sadd sadd ..^ sadd sadd ..^ $/\$ sadd sadd ..^
126	121, 124, 125	sylanbrc 646	. . . . . 6 sadd sadd ..^
127	14	ffvelrni 5828	. . . . . 6 sadd sadd ..^ bits sadd sadd ..^
128	126, 127	syl 16	. . . . 5 bits sadd sadd ..^
129	128	nn0red 10231	. . . 4 bits sadd sadd ..^
130		2nn 10089	. . . . . . 7
131	130	a1i 11	. . . . . 6
132	131, 60	nnexpcld 11499	. . . . 5
133	132	nnrpd 10603	. . . 4
134	128	nn0ge0d 10233	. . . 4 bits sadd sadd ..^
135		fvres 5704	. . . . . . . . 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 5974	. . . . . . . . 9 bits $/\$ sadd sadd ..^ bits bits sadd sadd ..^ sadd sadd ..^
138	11, 126, 137	sylancr 645	. . . . . . . 8 bits bits sadd sadd ..^ sadd sadd ..^
139	136, 138	eqtr3d 2438	. . . . . . 7 bitsbits sadd sadd ..^ sadd sadd ..^
140	139, 122	syl6eqss 3358	. . . . . 6 bitsbits sadd sadd ..^ ..^
141	128	nn0zd 10329	. . . . . . 7 bits sadd sadd ..^
142		bitsfzo 12902	. . . . . . 7 bits sadd sadd ..^ $/\$ bits sadd sadd ..^ ..^ bitsbits sadd sadd ..^ ..^
143	141, 60, 142	syl2anc 643	. . . . . 6 bits sadd sadd ..^ ..^ bitsbits sadd sadd ..^ ..^
144	140, 143	mpbird 224	. . . . 5 bits sadd sadd ..^ ..^
145		elfzolt2 11103	. . . . 5 bits sadd sadd ..^ ..^ bits sadd sadd ..^
146	144, 145	syl 16	. . . 4 bits sadd sadd ..^
147		modid 11225	. . . 4 bits sadd sadd ..^ $/\$ $/\$ bits sadd sadd ..^ $/\$ bits sadd sadd ..^ bits sadd sadd ..^ bits sadd sadd ..^
148	129, 133, 134, 146, 147	syl22anc 1185	. . 3 bits sadd sadd ..^ bits sadd sadd ..^
149	90, 117, 148	3eqtr3d 2444	. 2 bits sadd sadd ..^ bits sadd sadd ..^
150		f1of1 5632	. . . . 5 bits bits
151	11, 12, 150	mp2b 10	. . . 4 bits
152		f1fveq 5967	. . . 4 bits $/\$ sadd sadd ..^ $/\$ sadd sadd ..^ bits sadd sadd ..^ bits sadd sadd ..^ sadd sadd ..^ sadd sadd ..^
153	151, 152	mpan 652	. . 3 sadd sadd ..^ $/\$ sadd sadd ..^ bits sadd sadd ..^ bits sadd sadd ..^ sadd sadd ..^ sadd sadd ..^
154	99, 126, 153	syl2anc 643	. 2 bits sadd sadd ..^ bits sadd sadd ..^ sadd sadd ..^ sadd sadd ..^
155	149, 154	mpbid 202	1 sadd sadd ..^ sadd sadd ..^

Colors of variables: wff set class

Syntax hints:

wi 4

wb 177 $/\$ wa 359 caddwcad 1385

wceq 1649

wcel 1721

cin 3279

wss 3280

c0 3588

cif 3699

cpw 3759 class class class wbr 4172

cmpt 4226

ccnv 4836

cres 4839

wf 5409

wf1 5410

wf1o 5412

cfv 5413 (class class class)co 6040

cmpt2 6042

c1o 6676

c2o 6677

cfn 7068

cr 8945

cc0 8946

c1 8947

caddc 8949

clt 9076

cle 9077

cmin 9247

cn 9956

c2 10005

cn0 10177

cz 10238

crp 10568 ..^cfzo 11090

cmo 11205

cseq 11278

cexp 11337 bitscbits 12886 sadd csad 12887

This theorem is referenced by: sadass 12938

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-xor 1311 df-tru 1325 df-had 1386 df-cad 1387 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-disj 4143 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-2o 6684 df-oadd 6687 df-er 6864 df-map 6979 df-pm 6980 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-sup 7404 df-oi 7435 df-card 7782 df-cda 8004 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-n0 10178 df-z 10239 df-uz 10445 df-rp 10569 df-fz 11000 df-fzo 11091 df-fl 11157 df-mod 11206 df-seq 11279 df-exp 11338 df-hash 11574 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-clim 12237 df-sum 12435 df-dvds 12808 df-bits 12889 df-sad 12918

W3C validator