sadasslem - Metamath Proof Explorer

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

Theorem sadasslem 13687

Description: Lemma for sadass 13688. (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 3591	. . . . . . . . . . 11 ..^
2		sadasslem.1	. . . . . . . . . . 11
3	1, 2	syl5ss 3388	. . . . . . . . . 10 ..^
4		fzofi 11817	. . . . . . . . . . . 12 ..^
5	4	a1i 11	. . . . . . . . . . 11 ..^
6		inss2 3592	. . . . . . . . . . 11 ..^ ..^
7		ssfi 7554	. . . . . . . . . . 11 ..^ $/\$ ..^ ..^ ..^
8	5, 6, 7	sylancl 662	. . . . . . . . . 10 ..^
9		elfpw 7634	. . . . . . . . . 10 ..^ ..^ $/\$ ..^
10	3, 8, 9	sylanbrc 664	. . . . . . . . 9 ..^
11		bitsf1o 13662	. . . . . . . . . . 11 bits
12		f1ocnv 5674	. . . . . . . . . . 11 bits bits
13		f1of 5662	. . . . . . . . . . 11 bits bits
14	11, 12, 13	mp2b 10	. . . . . . . . . 10 bits
15	14	ffvelrni 5863	. . . . . . . . 9 ..^ bits ..^
16	10, 15	syl 16	. . . . . . . 8 bits ..^
17	16	nn0cnd 10659	. . . . . . 7 bits ..^
18		inss1 3591	. . . . . . . . . . 11 ..^
19		sadasslem.2	. . . . . . . . . . 11
20	18, 19	syl5ss 3388	. . . . . . . . . 10 ..^
21		inss2 3592	. . . . . . . . . . 11 ..^ ..^
22		ssfi 7554	. . . . . . . . . . 11 ..^ $/\$ ..^ ..^ ..^
23	5, 21, 22	sylancl 662	. . . . . . . . . 10 ..^
24		elfpw 7634	. . . . . . . . . 10 ..^ ..^ $/\$ ..^
25	20, 23, 24	sylanbrc 664	. . . . . . . . 9 ..^
26	14	ffvelrni 5863	. . . . . . . . 9 ..^ bits ..^
27	25, 26	syl 16	. . . . . . . 8 bits ..^
28	27	nn0cnd 10659	. . . . . . 7 bits ..^
29		inss1 3591	. . . . . . . . . . 11 ..^
30		sadasslem.3	. . . . . . . . . . 11
31	29, 30	syl5ss 3388	. . . . . . . . . 10 ..^
32		inss2 3592	. . . . . . . . . . 11 ..^ ..^
33		ssfi 7554	. . . . . . . . . . 11 ..^ $/\$ ..^ ..^ ..^
34	5, 32, 33	sylancl 662	. . . . . . . . . 10 ..^
35		elfpw 7634	. . . . . . . . . 10 ..^ ..^ $/\$ ..^
36	31, 34, 35	sylanbrc 664	. . . . . . . . 9 ..^
37	14	ffvelrni 5863	. . . . . . . . 9 ..^ bits ..^
38	36, 37	syl 16	. . . . . . . 8 bits ..^
39	38	nn0cnd 10659	. . . . . . 7 bits ..^
40	17, 28, 39	addassd 9429	. . . . . 6 bits ..^ bits ..^ bits ..^ bits ..^ bits ..^ bits ..^
41	40	oveq1d 6127	. . . . 5 bits ..^ bits ..^ bits ..^ bits ..^ bits ..^ bits ..^
42		inss1 3591	. . . . . . . . . 10 sadd ..^ sadd
43		sadcl 13679	. . . . . . . . . . 11 $/\$ sadd
44	2, 19, 43	syl2anc 661	. . . . . . . . . 10 sadd
45	42, 44	syl5ss 3388	. . . . . . . . 9 sadd ..^
46		inss2 3592	. . . . . . . . . 10 sadd ..^ ..^
47		ssfi 7554	. . . . . . . . . 10 ..^ $/\$ sadd ..^ ..^ sadd ..^
48	5, 46, 47	sylancl 662	. . . . . . . . 9 sadd ..^
49		elfpw 7634	. . . . . . . . 9 sadd ..^ sadd ..^ $/\$ sadd ..^
50	45, 48, 49	sylanbrc 664	. . . . . . . 8 sadd ..^
51	14	ffvelrni 5863	. . . . . . . 8 sadd ..^ bits sadd ..^
52	50, 51	syl 16	. . . . . . 7 bits sadd ..^
53	52	nn0red 10658	. . . . . 6 bits sadd ..^
54	16	nn0red 10658	. . . . . . 7 bits ..^
55	27	nn0red 10658	. . . . . . 7 bits ..^
56	54, 55	readdcld 9434	. . . . . 6 bits ..^ bits ..^
57	38	nn0red 10658	. . . . . 6 bits ..^
58		2rp 11017	. . . . . . . 8
59	58	a1i 11	. . . . . . 7
60		sadasslem.4	. . . . . . . 8
61	60	nn0zd 10766	. . . . . . 7
62	59, 61	rpexpcld 12052	. . . . . 6
63		eqid 2443	. . . . . . 7 cadd cadd
64		eqid 2443	. . . . . . 7 bits bits
65	2, 19, 63, 60, 64	sadadd3 13678	. . . . . 6 bits sadd ..^ bits ..^ bits ..^
66		eqidd 2444	. . . . . 6 bits ..^ bits ..^
67	53, 56, 57, 57, 62, 65, 66	modadd12d 11776	. . . . 5 bits sadd ..^ bits ..^ bits ..^ bits ..^ bits ..^
68		inss1 3591	. . . . . . . . . 10 sadd ..^ sadd
69		sadcl 13679	. . . . . . . . . . 11 $/\$ sadd
70	19, 30, 69	syl2anc 661	. . . . . . . . . 10 sadd
71	68, 70	syl5ss 3388	. . . . . . . . 9 sadd ..^
72		inss2 3592	. . . . . . . . . 10 sadd ..^ ..^
73		ssfi 7554	. . . . . . . . . 10 ..^ $/\$ sadd ..^ ..^ sadd ..^
74	5, 72, 73	sylancl 662	. . . . . . . . 9 sadd ..^
75		elfpw 7634	. . . . . . . . 9 sadd ..^ sadd ..^ $/\$ sadd ..^
76	71, 74, 75	sylanbrc 664	. . . . . . . 8 sadd ..^
77	14	ffvelrni 5863	. . . . . . . 8 sadd ..^ bits sadd ..^
78	76, 77	syl 16	. . . . . . 7 bits sadd ..^
79	78	nn0red 10658	. . . . . 6 bits sadd ..^
80	55, 57	readdcld 9434	. . . . . 6 bits ..^ bits ..^
81		eqidd 2444	. . . . . 6 bits ..^ bits ..^
82		eqid 2443	. . . . . . 7 cadd cadd
83	19, 30, 82, 60, 64	sadadd3 13678	. . . . . 6 bits sadd ..^ bits ..^ bits ..^
84	54, 54, 79, 80, 62, 81, 83	modadd12d 11776	. . . . 5 bits ..^ bits sadd ..^ bits ..^ bits ..^ bits ..^
85	41, 67, 84	3eqtr4d 2485	. . . 4 bits sadd ..^ bits ..^ bits ..^ bits sadd ..^
86		eqid 2443	. . . . 5 cadd sadd cadd sadd
87	44, 30, 86, 60, 64	sadadd3 13678	. . . 4 bits sadd sadd ..^ bits sadd ..^ bits ..^
88		eqid 2443	. . . . 5 cadd sadd cadd sadd
89	2, 70, 88, 60, 64	sadadd3 13678	. . . 4 bits sadd sadd ..^ bits ..^ bits sadd ..^
90	85, 87, 89	3eqtr4d 2485	. . 3 bits sadd sadd ..^ bits sadd sadd ..^
91		inss1 3591	. . . . . . . 8 sadd sadd ..^ sadd sadd
92		sadcl 13679	. . . . . . . . 9 sadd $/\$ sadd sadd
93	44, 30, 92	syl2anc 661	. . . . . . . 8 sadd sadd
94	91, 93	syl5ss 3388	. . . . . . 7 sadd sadd ..^
95		inss2 3592	. . . . . . . 8 sadd sadd ..^ ..^
96		ssfi 7554	. . . . . . . 8 ..^ $/\$ sadd sadd ..^ ..^ sadd sadd ..^
97	5, 95, 96	sylancl 662	. . . . . . 7 sadd sadd ..^
98		elfpw 7634	. . . . . . 7 sadd sadd ..^ sadd sadd ..^ $/\$ sadd sadd ..^
99	94, 97, 98	sylanbrc 664	. . . . . 6 sadd sadd ..^
100	14	ffvelrni 5863	. . . . . 6 sadd sadd ..^ bits sadd sadd ..^
101	99, 100	syl 16	. . . . 5 bits sadd sadd ..^
102	101	nn0red 10658	. . . 4 bits sadd sadd ..^
103	101	nn0ge0d 10660	. . . 4 bits sadd sadd ..^
104		fvres 5725	. . . . . . . . 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 6005	. . . . . . . . 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 2477	. . . . . . 7 bitsbits sadd sadd ..^ sadd sadd ..^
109	108, 95	syl6eqss 3427	. . . . . 6 bitsbits sadd sadd ..^ ..^
110	101	nn0zd 10766	. . . . . . 7 bits sadd sadd ..^
111		bitsfzo 13652	. . . . . . 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 11582	. . . . 5 bits sadd sadd ..^ ..^ bits sadd sadd ..^
115	113, 114	syl 16	. . . 4 bits sadd sadd ..^
116		modid 11753	. . . 4 bits sadd sadd ..^ $/\$ $/\$ bits sadd sadd ..^ $/\$ bits sadd sadd ..^ bits sadd sadd ..^ bits sadd sadd ..^
117	102, 62, 103, 115, 116	syl22anc 1219	. . 3 bits sadd sadd ..^ bits sadd sadd ..^
118		inss1 3591	. . . . . . . 8 sadd sadd ..^ sadd sadd
119		sadcl 13679	. . . . . . . . 9 $/\$ sadd sadd sadd
120	2, 70, 119	syl2anc 661	. . . . . . . 8 sadd sadd
121	118, 120	syl5ss 3388	. . . . . . 7 sadd sadd ..^
122		inss2 3592	. . . . . . . 8 sadd sadd ..^ ..^
123		ssfi 7554	. . . . . . . 8 ..^ $/\$ sadd sadd ..^ ..^ sadd sadd ..^
124	5, 122, 123	sylancl 662	. . . . . . 7 sadd sadd ..^
125		elfpw 7634	. . . . . . 7 sadd sadd ..^ sadd sadd ..^ $/\$ sadd sadd ..^
126	121, 124, 125	sylanbrc 664	. . . . . 6 sadd sadd ..^
127	14	ffvelrni 5863	. . . . . 6 sadd sadd ..^ bits sadd sadd ..^
128	126, 127	syl 16	. . . . 5 bits sadd sadd ..^
129	128	nn0red 10658	. . . 4 bits sadd sadd ..^
130		2nn 10500	. . . . . . 7
131	130	a1i 11	. . . . . 6
132	131, 60	nnexpcld 12050	. . . . 5
133	132	nnrpd 11047	. . . 4
134	128	nn0ge0d 10660	. . . 4 bits sadd sadd ..^
135		fvres 5725	. . . . . . . . 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 6005	. . . . . . . . 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 2477	. . . . . . 7 bitsbits sadd sadd ..^ sadd sadd ..^
140	139, 122	syl6eqss 3427	. . . . . 6 bitsbits sadd sadd ..^ ..^
141	128	nn0zd 10766	. . . . . . 7 bits sadd sadd ..^
142		bitsfzo 13652	. . . . . . 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 11582	. . . . 5 bits sadd sadd ..^ ..^ bits sadd sadd ..^
146	144, 145	syl 16	. . . 4 bits sadd sadd ..^
147		modid 11753	. . . 4 bits sadd sadd ..^ $/\$ $/\$ bits sadd sadd ..^ $/\$ bits sadd sadd ..^ bits sadd sadd ..^ bits sadd sadd ..^
148	129, 133, 134, 146, 147	syl22anc 1219	. . 3 bits sadd sadd ..^ bits sadd sadd ..^
149	90, 117, 148	3eqtr3d 2483	. 2 bits sadd sadd ..^ bits sadd sadd ..^
150		f1of1 5661	. . . . 5 bits bits
151	11, 12, 150	mp2b 10	. . . 4 bits
152		f1fveq 5996	. . . 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 1369 caddwcad 1420

wcel 1756

cin 3348

wss 3349

c0 3658

cif 3812

cpw 3881 class class class wbr 4313

cmpt 4371

ccnv 4860

cres 4863

wf 5435

wf1 5436

wf1o 5438

cfv 5439 (class class class)co 6112

cmpt2 6114

c1o 6934

c2o 6935

cfn 7331

cr 9302

cc0 9303

c1 9304

caddc 9306

clt 9439

cle 9440

cmin 9616

cn 10343

c2 10392

cn0 10600

cz 10667

crp 11012 ..^cfzo 11569

cmo 11729

cseq 11827

cexp 11886 bitscbits 13636 sadd csad 13637

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4424 ax-sep 4434 ax-nul 4442 ax-pow 4491 ax-pr 4552 ax-un 6393 ax-inf2 7868 ax-cnex 9359 ax-resscn 9360 ax-1cn 9361 ax-icn 9362 ax-addcl 9363 ax-addrcl 9364 ax-mulcl 9365 ax-mulrcl 9366 ax-mulcom 9367 ax-addass 9368 ax-mulass 9369 ax-distr 9370 ax-i2m1 9371 ax-1ne0 9372 ax-1rid 9373 ax-rnegex 9374 ax-rrecex 9375 ax-cnre 9376 ax-pre-lttri 9377 ax-pre-lttrn 9378 ax-pre-ltadd 9379 ax-pre-mulgt0 9380 ax-pre-sup 9381

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-xor 1351 df-tru 1372 df-fal 1375 df-had 1421 df-cad 1422 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2577 df-ne 2622 df-nel 2623 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 2995 df-sbc 3208 df-csb 3310 df-dif 3352 df-un 3354 df-in 3356 df-ss 3363 df-pss 3365 df-nul 3659 df-if 3813 df-pw 3883 df-sn 3899 df-pr 3901 df-tp 3903 df-op 3905 df-uni 4113 df-int 4150 df-iun 4194 df-disj 4284 df-br 4314 df-opab 4372 df-mpt 4373 df-tr 4407 df-eprel 4653 df-id 4657 df-po 4662 df-so 4663 df-fr 4700 df-se 4701 df-we 4702 df-ord 4743 df-on 4744 df-lim 4745 df-suc 4746 df-xp 4867 df-rel 4868 df-cnv 4869 df-co 4870 df-dm 4871 df-rn 4872 df-res 4873 df-ima 4874 df-iota 5402 df-fun 5441 df-fn 5442 df-f 5443 df-f1 5444 df-fo 5445 df-f1o 5446 df-fv 5447 df-isom 5448 df-riota 6073 df-ov 6115 df-oprab 6116 df-mpt2 6117 df-om 6498 df-1st 6598 df-2nd 6599 df-recs 6853 df-rdg 6887 df-1o 6941 df-2o 6942 df-oadd 6945 df-er 7122 df-map 7237 df-pm 7238 df-en 7332 df-dom 7333 df-sdom 7334 df-fin 7335 df-sup 7712 df-oi 7745 df-card 8130 df-cda 8358 df-pnf 9441 df-mnf 9442 df-xr 9443 df-ltxr 9444 df-le 9445 df-sub 9618 df-neg 9619 df-div 10015 df-nn 10344 df-2 10401 df-3 10402 df-n0 10601 df-z 10668 df-uz 10883 df-rp 11013 df-fz 11459 df-fzo 11570 df-fl 11663 df-mod 11730 df-seq 11828 df-exp 11887 df-hash 12125 df-cj 12609 df-re 12610 df-im 12611 df-sqr 12745 df-abs 12746 df-clim 12987 df-sum 13185 df-dvds 13557 df-bits 13639 df-sad 13668

This theorem is referenced by: sadass 13688

W3C validator