sadasslem - Metamath Proof Explorer

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

Theorem sadasslem 13979

Description: Lemma for sadass 13980. (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 3718	. . . . . . . . . . 11 ..^
2		sadasslem.1	. . . . . . . . . . 11
3	1, 2	syl5ss 3515	. . . . . . . . . 10 ..^
4		fzofi 12052	. . . . . . . . . . . 12 ..^
5	4	a1i 11	. . . . . . . . . . 11 ..^
6		inss2 3719	. . . . . . . . . . 11 ..^ ..^
7		ssfi 7740	. . . . . . . . . . 11 ..^ $/\$ ..^ ..^ ..^
8	5, 6, 7	sylancl 662	. . . . . . . . . 10 ..^
9		elfpw 7822	. . . . . . . . . 10 ..^ ..^ $/\$ ..^
10	3, 8, 9	sylanbrc 664	. . . . . . . . 9 ..^
11		bitsf1o 13954	. . . . . . . . . . 11 bits
12		f1ocnv 5828	. . . . . . . . . . 11 bits bits
13		f1of 5816	. . . . . . . . . . 11 bits bits
14	11, 12, 13	mp2b 10	. . . . . . . . . 10 bits
15	14	ffvelrni 6020	. . . . . . . . 9 ..^ bits ..^
16	10, 15	syl 16	. . . . . . . 8 bits ..^
17	16	nn0cnd 10854	. . . . . . 7 bits ..^
18		inss1 3718	. . . . . . . . . . 11 ..^
19		sadasslem.2	. . . . . . . . . . 11
20	18, 19	syl5ss 3515	. . . . . . . . . 10 ..^
21		inss2 3719	. . . . . . . . . . 11 ..^ ..^
22		ssfi 7740	. . . . . . . . . . 11 ..^ $/\$ ..^ ..^ ..^
23	5, 21, 22	sylancl 662	. . . . . . . . . 10 ..^
24		elfpw 7822	. . . . . . . . . 10 ..^ ..^ $/\$ ..^
25	20, 23, 24	sylanbrc 664	. . . . . . . . 9 ..^
26	14	ffvelrni 6020	. . . . . . . . 9 ..^ bits ..^
27	25, 26	syl 16	. . . . . . . 8 bits ..^
28	27	nn0cnd 10854	. . . . . . 7 bits ..^
29		inss1 3718	. . . . . . . . . . 11 ..^
30		sadasslem.3	. . . . . . . . . . 11
31	29, 30	syl5ss 3515	. . . . . . . . . 10 ..^
32		inss2 3719	. . . . . . . . . . 11 ..^ ..^
33		ssfi 7740	. . . . . . . . . . 11 ..^ $/\$ ..^ ..^ ..^
34	5, 32, 33	sylancl 662	. . . . . . . . . 10 ..^
35		elfpw 7822	. . . . . . . . . 10 ..^ ..^ $/\$ ..^
36	31, 34, 35	sylanbrc 664	. . . . . . . . 9 ..^
37	14	ffvelrni 6020	. . . . . . . . 9 ..^ bits ..^
38	36, 37	syl 16	. . . . . . . 8 bits ..^
39	38	nn0cnd 10854	. . . . . . 7 bits ..^
40	17, 28, 39	addassd 9618	. . . . . 6 bits ..^ bits ..^ bits ..^ bits ..^ bits ..^ bits ..^
41	40	oveq1d 6299	. . . . 5 bits ..^ bits ..^ bits ..^ bits ..^ bits ..^ bits ..^
42		inss1 3718	. . . . . . . . . 10 sadd ..^ sadd
43		sadcl 13971	. . . . . . . . . . 11 $/\$ sadd
44	2, 19, 43	syl2anc 661	. . . . . . . . . 10 sadd
45	42, 44	syl5ss 3515	. . . . . . . . 9 sadd ..^
46		inss2 3719	. . . . . . . . . 10 sadd ..^ ..^
47		ssfi 7740	. . . . . . . . . 10 ..^ $/\$ sadd ..^ ..^ sadd ..^
48	5, 46, 47	sylancl 662	. . . . . . . . 9 sadd ..^
49		elfpw 7822	. . . . . . . . 9 sadd ..^ sadd ..^ $/\$ sadd ..^
50	45, 48, 49	sylanbrc 664	. . . . . . . 8 sadd ..^
51	14	ffvelrni 6020	. . . . . . . 8 sadd ..^ bits sadd ..^
52	50, 51	syl 16	. . . . . . 7 bits sadd ..^
53	52	nn0red 10853	. . . . . 6 bits sadd ..^
54	16	nn0red 10853	. . . . . . 7 bits ..^
55	27	nn0red 10853	. . . . . . 7 bits ..^
56	54, 55	readdcld 9623	. . . . . 6 bits ..^ bits ..^
57	38	nn0red 10853	. . . . . 6 bits ..^
58		2rp 11225	. . . . . . . 8
59	58	a1i 11	. . . . . . 7
60		sadasslem.4	. . . . . . . 8
61	60	nn0zd 10964	. . . . . . 7
62	59, 61	rpexpcld 12301	. . . . . 6
63		eqid 2467	. . . . . . 7 cadd cadd
64		eqid 2467	. . . . . . 7 bits bits
65	2, 19, 63, 60, 64	sadadd3 13970	. . . . . 6 bits sadd ..^ bits ..^ bits ..^
66		eqidd 2468	. . . . . 6 bits ..^ bits ..^
67	53, 56, 57, 57, 62, 65, 66	modadd12d 12011	. . . . 5 bits sadd ..^ bits ..^ bits ..^ bits ..^ bits ..^
68		inss1 3718	. . . . . . . . . 10 sadd ..^ sadd
69		sadcl 13971	. . . . . . . . . . 11 $/\$ sadd
70	19, 30, 69	syl2anc 661	. . . . . . . . . 10 sadd
71	68, 70	syl5ss 3515	. . . . . . . . 9 sadd ..^
72		inss2 3719	. . . . . . . . . 10 sadd ..^ ..^
73		ssfi 7740	. . . . . . . . . 10 ..^ $/\$ sadd ..^ ..^ sadd ..^
74	5, 72, 73	sylancl 662	. . . . . . . . 9 sadd ..^
75		elfpw 7822	. . . . . . . . 9 sadd ..^ sadd ..^ $/\$ sadd ..^
76	71, 74, 75	sylanbrc 664	. . . . . . . 8 sadd ..^
77	14	ffvelrni 6020	. . . . . . . 8 sadd ..^ bits sadd ..^
78	76, 77	syl 16	. . . . . . 7 bits sadd ..^
79	78	nn0red 10853	. . . . . 6 bits sadd ..^
80	55, 57	readdcld 9623	. . . . . 6 bits ..^ bits ..^
81		eqidd 2468	. . . . . 6 bits ..^ bits ..^
82		eqid 2467	. . . . . . 7 cadd cadd
83	19, 30, 82, 60, 64	sadadd3 13970	. . . . . 6 bits sadd ..^ bits ..^ bits ..^
84	54, 54, 79, 80, 62, 81, 83	modadd12d 12011	. . . . 5 bits ..^ bits sadd ..^ bits ..^ bits ..^ bits ..^
85	41, 67, 84	3eqtr4d 2518	. . . 4 bits sadd ..^ bits ..^ bits ..^ bits sadd ..^
86		eqid 2467	. . . . 5 cadd sadd cadd sadd
87	44, 30, 86, 60, 64	sadadd3 13970	. . . 4 bits sadd sadd ..^ bits sadd ..^ bits ..^
88		eqid 2467	. . . . 5 cadd sadd cadd sadd
89	2, 70, 88, 60, 64	sadadd3 13970	. . . 4 bits sadd sadd ..^ bits ..^ bits sadd ..^
90	85, 87, 89	3eqtr4d 2518	. . 3 bits sadd sadd ..^ bits sadd sadd ..^
91		inss1 3718	. . . . . . . 8 sadd sadd ..^ sadd sadd
92		sadcl 13971	. . . . . . . . 9 sadd $/\$ sadd sadd
93	44, 30, 92	syl2anc 661	. . . . . . . 8 sadd sadd
94	91, 93	syl5ss 3515	. . . . . . 7 sadd sadd ..^
95		inss2 3719	. . . . . . . 8 sadd sadd ..^ ..^
96		ssfi 7740	. . . . . . . 8 ..^ $/\$ sadd sadd ..^ ..^ sadd sadd ..^
97	5, 95, 96	sylancl 662	. . . . . . 7 sadd sadd ..^
98		elfpw 7822	. . . . . . 7 sadd sadd ..^ sadd sadd ..^ $/\$ sadd sadd ..^
99	94, 97, 98	sylanbrc 664	. . . . . 6 sadd sadd ..^
100	14	ffvelrni 6020	. . . . . 6 sadd sadd ..^ bits sadd sadd ..^
101	99, 100	syl 16	. . . . 5 bits sadd sadd ..^
102	101	nn0red 10853	. . . 4 bits sadd sadd ..^
103	101	nn0ge0d 10855	. . . 4 bits sadd sadd ..^
104		fvres 5880	. . . . . . . . 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 6171	. . . . . . . . 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 2510	. . . . . . 7 bitsbits sadd sadd ..^ sadd sadd ..^
109	108, 95	syl6eqss 3554	. . . . . 6 bitsbits sadd sadd ..^ ..^
110	101	nn0zd 10964	. . . . . . 7 bits sadd sadd ..^
111		bitsfzo 13944	. . . . . . 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 11805	. . . . 5 bits sadd sadd ..^ ..^ bits sadd sadd ..^
115	113, 114	syl 16	. . . 4 bits sadd sadd ..^
116		modid 11988	. . . 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 3718	. . . . . . . 8 sadd sadd ..^ sadd sadd
119		sadcl 13971	. . . . . . . . 9 $/\$ sadd sadd sadd
120	2, 70, 119	syl2anc 661	. . . . . . . 8 sadd sadd
121	118, 120	syl5ss 3515	. . . . . . 7 sadd sadd ..^
122		inss2 3719	. . . . . . . 8 sadd sadd ..^ ..^
123		ssfi 7740	. . . . . . . 8 ..^ $/\$ sadd sadd ..^ ..^ sadd sadd ..^
124	5, 122, 123	sylancl 662	. . . . . . 7 sadd sadd ..^
125		elfpw 7822	. . . . . . 7 sadd sadd ..^ sadd sadd ..^ $/\$ sadd sadd ..^
126	121, 124, 125	sylanbrc 664	. . . . . 6 sadd sadd ..^
127	14	ffvelrni 6020	. . . . . 6 sadd sadd ..^ bits sadd sadd ..^
128	126, 127	syl 16	. . . . 5 bits sadd sadd ..^
129	128	nn0red 10853	. . . 4 bits sadd sadd ..^
130		2nn 10693	. . . . . . 7
131	130	a1i 11	. . . . . 6
132	131, 60	nnexpcld 12299	. . . . 5
133	132	nnrpd 11255	. . . 4
134	128	nn0ge0d 10855	. . . 4 bits sadd sadd ..^
135		fvres 5880	. . . . . . . . 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 6171	. . . . . . . . 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 2510	. . . . . . 7 bitsbits sadd sadd ..^ sadd sadd ..^
140	139, 122	syl6eqss 3554	. . . . . 6 bitsbits sadd sadd ..^ ..^
141	128	nn0zd 10964	. . . . . . 7 bits sadd sadd ..^
142		bitsfzo 13944	. . . . . . 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 11805	. . . . 5 bits sadd sadd ..^ ..^ bits sadd sadd ..^
146	144, 145	syl 16	. . . 4 bits sadd sadd ..^
147		modid 11988	. . . 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 2516	. 2 bits sadd sadd ..^ bits sadd sadd ..^
150		f1of1 5815	. . . . 5 bits bits
151	11, 12, 150	mp2b 10	. . . 4 bits
152		f1fveq 6158	. . . 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 1379 caddwcad 1430

wcel 1767

cin 3475

wss 3476

c0 3785

cif 3939

cpw 4010 class class class wbr 4447

cmpt 4505

ccnv 4998

cres 5001

wf 5584

wf1 5585

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

cn 10536

c2 10585

cn0 10795

cz 10864

crp 11220 ..^cfzo 11792

cmo 11964

cseq 12075

cexp 12134 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: sadass 13980

W3C validator