sadasslem - Metamath Proof Explorer

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

Theorem sadasslem 14444

Description: Lemma for sadass 14445. (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 3652	. . . . . . . . . . 11 ..^
2		sadasslem.1	. . . . . . . . . . 11
3	1, 2	syl5ss 3443	. . . . . . . . . 10 ..^
4		fzofi 12187	. . . . . . . . . . . 12 ..^
5	4	a1i 11	. . . . . . . . . . 11 ..^
6		inss2 3653	. . . . . . . . . . 11 ..^ ..^
7		ssfi 7792	. . . . . . . . . . 11 ..^ $/\$ ..^ ..^ ..^
8	5, 6, 7	sylancl 668	. . . . . . . . . 10 ..^
9		elfpw 7876	. . . . . . . . . 10 ..^ ..^ $/\$ ..^
10	3, 8, 9	sylanbrc 670	. . . . . . . . 9 ..^
11		bitsf1o 14419	. . . . . . . . . . 11 bits
12		f1ocnv 5826	. . . . . . . . . . 11 bits bits
13		f1of 5814	. . . . . . . . . . 11 bits bits
14	11, 12, 13	mp2b 10	. . . . . . . . . 10 bits
15	14	ffvelrni 6021	. . . . . . . . 9 ..^ bits ..^
16	10, 15	syl 17	. . . . . . . 8 bits ..^
17	16	nn0cnd 10927	. . . . . . 7 bits ..^
18		inss1 3652	. . . . . . . . . . 11 ..^
19		sadasslem.2	. . . . . . . . . . 11
20	18, 19	syl5ss 3443	. . . . . . . . . 10 ..^
21		inss2 3653	. . . . . . . . . . 11 ..^ ..^
22		ssfi 7792	. . . . . . . . . . 11 ..^ $/\$ ..^ ..^ ..^
23	5, 21, 22	sylancl 668	. . . . . . . . . 10 ..^
24		elfpw 7876	. . . . . . . . . 10 ..^ ..^ $/\$ ..^
25	20, 23, 24	sylanbrc 670	. . . . . . . . 9 ..^
26	14	ffvelrni 6021	. . . . . . . . 9 ..^ bits ..^
27	25, 26	syl 17	. . . . . . . 8 bits ..^
28	27	nn0cnd 10927	. . . . . . 7 bits ..^
29		inss1 3652	. . . . . . . . . . 11 ..^
30		sadasslem.3	. . . . . . . . . . 11
31	29, 30	syl5ss 3443	. . . . . . . . . 10 ..^
32		inss2 3653	. . . . . . . . . . 11 ..^ ..^
33		ssfi 7792	. . . . . . . . . . 11 ..^ $/\$ ..^ ..^ ..^
34	5, 32, 33	sylancl 668	. . . . . . . . . 10 ..^
35		elfpw 7876	. . . . . . . . . 10 ..^ ..^ $/\$ ..^
36	31, 34, 35	sylanbrc 670	. . . . . . . . 9 ..^
37	14	ffvelrni 6021	. . . . . . . . 9 ..^ bits ..^
38	36, 37	syl 17	. . . . . . . 8 bits ..^
39	38	nn0cnd 10927	. . . . . . 7 bits ..^
40	17, 28, 39	addassd 9665	. . . . . 6 bits ..^ bits ..^ bits ..^ bits ..^ bits ..^ bits ..^
41	40	oveq1d 6305	. . . . 5 bits ..^ bits ..^ bits ..^ bits ..^ bits ..^ bits ..^
42		inss1 3652	. . . . . . . . . 10 sadd ..^ sadd
43		sadcl 14436	. . . . . . . . . . 11 $/\$ sadd
44	2, 19, 43	syl2anc 667	. . . . . . . . . 10 sadd
45	42, 44	syl5ss 3443	. . . . . . . . 9 sadd ..^
46		inss2 3653	. . . . . . . . . 10 sadd ..^ ..^
47		ssfi 7792	. . . . . . . . . 10 ..^ $/\$ sadd ..^ ..^ sadd ..^
48	5, 46, 47	sylancl 668	. . . . . . . . 9 sadd ..^
49		elfpw 7876	. . . . . . . . 9 sadd ..^ sadd ..^ $/\$ sadd ..^
50	45, 48, 49	sylanbrc 670	. . . . . . . 8 sadd ..^
51	14	ffvelrni 6021	. . . . . . . 8 sadd ..^ bits sadd ..^
52	50, 51	syl 17	. . . . . . 7 bits sadd ..^
53	52	nn0red 10926	. . . . . 6 bits sadd ..^
54	16	nn0red 10926	. . . . . . 7 bits ..^
55	27	nn0red 10926	. . . . . . 7 bits ..^
56	54, 55	readdcld 9670	. . . . . 6 bits ..^ bits ..^
57	38	nn0red 10926	. . . . . 6 bits ..^
58		2rp 11307	. . . . . . . 8
59	58	a1i 11	. . . . . . 7
60		sadasslem.4	. . . . . . . 8
61	60	nn0zd 11038	. . . . . . 7
62	59, 61	rpexpcld 12439	. . . . . 6
63		eqid 2451	. . . . . . 7 cadd cadd
64		eqid 2451	. . . . . . 7 bits bits
65	2, 19, 63, 60, 64	sadadd3 14435	. . . . . 6 bits sadd ..^ bits ..^ bits ..^
66		eqidd 2452	. . . . . 6 bits ..^ bits ..^
67	53, 56, 57, 57, 62, 65, 66	modadd12d 12146	. . . . 5 bits sadd ..^ bits ..^ bits ..^ bits ..^ bits ..^
68		inss1 3652	. . . . . . . . . 10 sadd ..^ sadd
69		sadcl 14436	. . . . . . . . . . 11 $/\$ sadd
70	19, 30, 69	syl2anc 667	. . . . . . . . . 10 sadd
71	68, 70	syl5ss 3443	. . . . . . . . 9 sadd ..^
72		inss2 3653	. . . . . . . . . 10 sadd ..^ ..^
73		ssfi 7792	. . . . . . . . . 10 ..^ $/\$ sadd ..^ ..^ sadd ..^
74	5, 72, 73	sylancl 668	. . . . . . . . 9 sadd ..^
75		elfpw 7876	. . . . . . . . 9 sadd ..^ sadd ..^ $/\$ sadd ..^
76	71, 74, 75	sylanbrc 670	. . . . . . . 8 sadd ..^
77	14	ffvelrni 6021	. . . . . . . 8 sadd ..^ bits sadd ..^
78	76, 77	syl 17	. . . . . . 7 bits sadd ..^
79	78	nn0red 10926	. . . . . 6 bits sadd ..^
80	55, 57	readdcld 9670	. . . . . 6 bits ..^ bits ..^
81		eqidd 2452	. . . . . 6 bits ..^ bits ..^
82		eqid 2451	. . . . . . 7 cadd cadd
83	19, 30, 82, 60, 64	sadadd3 14435	. . . . . 6 bits sadd ..^ bits ..^ bits ..^
84	54, 54, 79, 80, 62, 81, 83	modadd12d 12146	. . . . 5 bits ..^ bits sadd ..^ bits ..^ bits ..^ bits ..^
85	41, 67, 84	3eqtr4d 2495	. . . 4 bits sadd ..^ bits ..^ bits ..^ bits sadd ..^
86		eqid 2451	. . . . 5 cadd sadd cadd sadd
87	44, 30, 86, 60, 64	sadadd3 14435	. . . 4 bits sadd sadd ..^ bits sadd ..^ bits ..^
88		eqid 2451	. . . . 5 cadd sadd cadd sadd
89	2, 70, 88, 60, 64	sadadd3 14435	. . . 4 bits sadd sadd ..^ bits ..^ bits sadd ..^
90	85, 87, 89	3eqtr4d 2495	. . 3 bits sadd sadd ..^ bits sadd sadd ..^
91		inss1 3652	. . . . . . . 8 sadd sadd ..^ sadd sadd
92		sadcl 14436	. . . . . . . . 9 sadd $/\$ sadd sadd
93	44, 30, 92	syl2anc 667	. . . . . . . 8 sadd sadd
94	91, 93	syl5ss 3443	. . . . . . 7 sadd sadd ..^
95		inss2 3653	. . . . . . . 8 sadd sadd ..^ ..^
96		ssfi 7792	. . . . . . . 8 ..^ $/\$ sadd sadd ..^ ..^ sadd sadd ..^
97	5, 95, 96	sylancl 668	. . . . . . 7 sadd sadd ..^
98		elfpw 7876	. . . . . . 7 sadd sadd ..^ sadd sadd ..^ $/\$ sadd sadd ..^
99	94, 97, 98	sylanbrc 670	. . . . . 6 sadd sadd ..^
100	14	ffvelrni 6021	. . . . . 6 sadd sadd ..^ bits sadd sadd ..^
101	99, 100	syl 17	. . . . 5 bits sadd sadd ..^
102	101	nn0red 10926	. . . 4 bits sadd sadd ..^
103	101	nn0ge0d 10928	. . . 4 bits sadd sadd ..^
104		fvres 5879	. . . . . . . . 9 bits sadd sadd ..^ bits bits sadd sadd ..^ bitsbits sadd sadd ..^
105	101, 104	syl 17	. . . . . . . 8 bits bits sadd sadd ..^ bitsbits sadd sadd ..^
106		f1ocnvfv2 6176	. . . . . . . . 9 bits $/\$ sadd sadd ..^ bits bits sadd sadd ..^ sadd sadd ..^
107	11, 99, 106	sylancr 669	. . . . . . . 8 bits bits sadd sadd ..^ sadd sadd ..^
108	105, 107	eqtr3d 2487	. . . . . . 7 bitsbits sadd sadd ..^ sadd sadd ..^
109	108, 95	syl6eqss 3482	. . . . . 6 bitsbits sadd sadd ..^ ..^
110	101	nn0zd 11038	. . . . . . 7 bits sadd sadd ..^
111		bitsfzo 14409	. . . . . . 7 bits sadd sadd ..^ $/\$ bits sadd sadd ..^ ..^ bitsbits sadd sadd ..^ ..^
112	110, 60, 111	syl2anc 667	. . . . . 6 bits sadd sadd ..^ ..^ bitsbits sadd sadd ..^ ..^
113	109, 112	mpbird 236	. . . . 5 bits sadd sadd ..^ ..^
114		elfzolt2 11929	. . . . 5 bits sadd sadd ..^ ..^ bits sadd sadd ..^
115	113, 114	syl 17	. . . 4 bits sadd sadd ..^
116		modid 12121	. . . 4 bits sadd sadd ..^ $/\$ $/\$ bits sadd sadd ..^ $/\$ bits sadd sadd ..^ bits sadd sadd ..^ bits sadd sadd ..^
117	102, 62, 103, 115, 116	syl22anc 1269	. . 3 bits sadd sadd ..^ bits sadd sadd ..^
118		inss1 3652	. . . . . . . 8 sadd sadd ..^ sadd sadd
119		sadcl 14436	. . . . . . . . 9 $/\$ sadd sadd sadd
120	2, 70, 119	syl2anc 667	. . . . . . . 8 sadd sadd
121	118, 120	syl5ss 3443	. . . . . . 7 sadd sadd ..^
122		inss2 3653	. . . . . . . 8 sadd sadd ..^ ..^
123		ssfi 7792	. . . . . . . 8 ..^ $/\$ sadd sadd ..^ ..^ sadd sadd ..^
124	5, 122, 123	sylancl 668	. . . . . . 7 sadd sadd ..^
125		elfpw 7876	. . . . . . 7 sadd sadd ..^ sadd sadd ..^ $/\$ sadd sadd ..^
126	121, 124, 125	sylanbrc 670	. . . . . 6 sadd sadd ..^
127	14	ffvelrni 6021	. . . . . 6 sadd sadd ..^ bits sadd sadd ..^
128	126, 127	syl 17	. . . . 5 bits sadd sadd ..^
129	128	nn0red 10926	. . . 4 bits sadd sadd ..^
130		2nn 10767	. . . . . . 7
131	130	a1i 11	. . . . . 6
132	131, 60	nnexpcld 12437	. . . . 5
133	132	nnrpd 11339	. . . 4
134	128	nn0ge0d 10928	. . . 4 bits sadd sadd ..^
135		fvres 5879	. . . . . . . . 9 bits sadd sadd ..^ bits bits sadd sadd ..^ bitsbits sadd sadd ..^
136	128, 135	syl 17	. . . . . . . 8 bits bits sadd sadd ..^ bitsbits sadd sadd ..^
137		f1ocnvfv2 6176	. . . . . . . . 9 bits $/\$ sadd sadd ..^ bits bits sadd sadd ..^ sadd sadd ..^
138	11, 126, 137	sylancr 669	. . . . . . . 8 bits bits sadd sadd ..^ sadd sadd ..^
139	136, 138	eqtr3d 2487	. . . . . . 7 bitsbits sadd sadd ..^ sadd sadd ..^
140	139, 122	syl6eqss 3482	. . . . . 6 bitsbits sadd sadd ..^ ..^
141	128	nn0zd 11038	. . . . . . 7 bits sadd sadd ..^
142		bitsfzo 14409	. . . . . . 7 bits sadd sadd ..^ $/\$ bits sadd sadd ..^ ..^ bitsbits sadd sadd ..^ ..^
143	141, 60, 142	syl2anc 667	. . . . . 6 bits sadd sadd ..^ ..^ bitsbits sadd sadd ..^ ..^
144	140, 143	mpbird 236	. . . . 5 bits sadd sadd ..^ ..^
145		elfzolt2 11929	. . . . 5 bits sadd sadd ..^ ..^ bits sadd sadd ..^
146	144, 145	syl 17	. . . 4 bits sadd sadd ..^
147		modid 12121	. . . 4 bits sadd sadd ..^ $/\$ $/\$ bits sadd sadd ..^ $/\$ bits sadd sadd ..^ bits sadd sadd ..^ bits sadd sadd ..^
148	129, 133, 134, 146, 147	syl22anc 1269	. . 3 bits sadd sadd ..^ bits sadd sadd ..^
149	90, 117, 148	3eqtr3d 2493	. 2 bits sadd sadd ..^ bits sadd sadd ..^
150		f1of1 5813	. . . . 5 bits bits
151	11, 12, 150	mp2b 10	. . . 4 bits
152		f1fveq 6163	. . . 4 bits $/\$ sadd sadd ..^ $/\$ sadd sadd ..^ bits sadd sadd ..^ bits sadd sadd ..^ sadd sadd ..^ sadd sadd ..^
153	151, 152	mpan 676	. . 3 sadd sadd ..^ $/\$ sadd sadd ..^ bits sadd sadd ..^ bits sadd sadd ..^ sadd sadd ..^ sadd sadd ..^
154	99, 126, 153	syl2anc 667	. 2 bits sadd sadd ..^ bits sadd sadd ..^ sadd sadd ..^ sadd sadd ..^
155	149, 154	mpbid 214	1 sadd sadd ..^ sadd sadd ..^

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371

wceq 1444 caddwcad 1509

wcel 1887

cin 3403

wss 3404

c0 3731

cif 3881

cpw 3951 class class class wbr 4402

cmpt 4461

ccnv 4833

cres 4836

wf 5578

wf1 5579

wf1o 5581

cfv 5582 (class class class)co 6290

cmpt2 6292

c1o 7175

c2o 7176

cfn 7569

cr 9538

cc0 9539

c1 9540

caddc 9542

clt 9675

cle 9676

cmin 9860

cn 10609

c2 10659

cn0 10869

cz 10937

crp 11302 ..^cfzo 11915

cmo 12096

cseq 12213

cexp 12272 bitscbits 14392 sadd csad 14393

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-inf2 8146 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-xor 1406 df-tru 1447 df-fal 1450 df-had 1497 df-cad 1510 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-disj 4374 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-se 4794 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-isom 5591 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-2o 7183 df-oadd 7186 df-er 7363 df-map 7474 df-pm 7475 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-sup 7956 df-inf 7957 df-oi 8025 df-card 8373 df-cda 8598 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-2 10668 df-3 10669 df-n0 10870 df-z 10938 df-uz 11160 df-rp 11303 df-fz 11785 df-fzo 11916 df-fl 12028 df-mod 12097 df-seq 12214 df-exp 12273 df-hash 12516 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299 df-clim 13552 df-sum 13753 df-dvds 14306 df-bits 14395 df-sad 14425

This theorem is referenced by: sadass 14445

W3C validator