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

Theorem sadasslem 14120
Description: Lemma for sadass 14121. (Contributed by Mario Carneiro, 9-Sep-2016.)
Hypotheses
Ref Expression
sadasslem.1
sadasslem.2
sadasslem.3
sadasslem.4
Assertion
Ref Expression
sadasslem

Proof of Theorem sadasslem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 inss1 3717 . . . . . . . . . . 11
2 sadasslem.1 . . . . . . . . . . 11
31, 2syl5ss 3514 . . . . . . . . . 10
4 fzofi 12084 . . . . . . . . . . . 12
54a1i 11 . . . . . . . . . . 11
6 inss2 3718 . . . . . . . . . . 11
7 ssfi 7760 . . . . . . . . . . 11
85, 6, 7sylancl 662 . . . . . . . . . 10
9 elfpw 7842 . . . . . . . . . 10
103, 8, 9sylanbrc 664 . . . . . . . . 9
11 bitsf1o 14095 . . . . . . . . . . 11
12 f1ocnv 5833 . . . . . . . . . . 11
13 f1of 5821 . . . . . . . . . . 11
1411, 12, 13mp2b 10 . . . . . . . . . 10
1514ffvelrni 6030 . . . . . . . . 9
1610, 15syl 16 . . . . . . . 8
1716nn0cnd 10879 . . . . . . 7
18 inss1 3717 . . . . . . . . . . 11
19 sadasslem.2 . . . . . . . . . . 11
2018, 19syl5ss 3514 . . . . . . . . . 10
21 inss2 3718 . . . . . . . . . . 11
22 ssfi 7760 . . . . . . . . . . 11
235, 21, 22sylancl 662 . . . . . . . . . 10
24 elfpw 7842 . . . . . . . . . 10
2520, 23, 24sylanbrc 664 . . . . . . . . 9
2614ffvelrni 6030 . . . . . . . . 9
2725, 26syl 16 . . . . . . . 8
2827nn0cnd 10879 . . . . . . 7
29 inss1 3717 . . . . . . . . . . 11
30 sadasslem.3 . . . . . . . . . . 11
3129, 30syl5ss 3514 . . . . . . . . . 10
32 inss2 3718 . . . . . . . . . . 11
33 ssfi 7760 . . . . . . . . . . 11
345, 32, 33sylancl 662 . . . . . . . . . 10
35 elfpw 7842 . . . . . . . . . 10
3631, 34, 35sylanbrc 664 . . . . . . . . 9
3714ffvelrni 6030 . . . . . . . . 9
3836, 37syl 16 . . . . . . . 8
3938nn0cnd 10879 . . . . . . 7
4017, 28, 39addassd 9639 . . . . . 6
4140oveq1d 6311 . . . . 5
42 inss1 3717 . . . . . . . . . 10
43 sadcl 14112 . . . . . . . . . . 11
442, 19, 43syl2anc 661 . . . . . . . . . 10
4542, 44syl5ss 3514 . . . . . . . . 9
46 inss2 3718 . . . . . . . . . 10
47 ssfi 7760 . . . . . . . . . 10
485, 46, 47sylancl 662 . . . . . . . . 9
49 elfpw 7842 . . . . . . . . 9
5045, 48, 49sylanbrc 664 . . . . . . . 8
5114ffvelrni 6030 . . . . . . . 8
5250, 51syl 16 . . . . . . 7
5352nn0red 10878 . . . . . 6
5416nn0red 10878 . . . . . . 7
5527nn0red 10878 . . . . . . 7
5654, 55readdcld 9644 . . . . . 6
5738nn0red 10878 . . . . . 6
58 2rp 11254 . . . . . . . 8
5958a1i 11 . . . . . . 7
60 sadasslem.4 . . . . . . . 8
6160nn0zd 10992 . . . . . . 7
6259, 61rpexpcld 12333 . . . . . 6
63 eqid 2457 . . . . . . 7
64 eqid 2457 . . . . . . 7
652, 19, 63, 60, 64sadadd3 14111 . . . . . 6
66 eqidd 2458 . . . . . 6
6753, 56, 57, 57, 62, 65, 66modadd12d 12043 . . . . 5
68 inss1 3717 . . . . . . . . . 10
69 sadcl 14112 . . . . . . . . . . 11
7019, 30, 69syl2anc 661 . . . . . . . . . 10
7168, 70syl5ss 3514 . . . . . . . . 9
72 inss2 3718 . . . . . . . . . 10
73 ssfi 7760 . . . . . . . . . 10
745, 72, 73sylancl 662 . . . . . . . . 9
75 elfpw 7842 . . . . . . . . 9
7671, 74, 75sylanbrc 664 . . . . . . . 8
7714ffvelrni 6030 . . . . . . . 8
7876, 77syl 16 . . . . . . 7
7978nn0red 10878 . . . . . 6
8055, 57readdcld 9644 . . . . . 6
81 eqidd 2458 . . . . . 6
82 eqid 2457 . . . . . . 7
8319, 30, 82, 60, 64sadadd3 14111 . . . . . 6
8454, 54, 79, 80, 62, 81, 83modadd12d 12043 . . . . 5
8541, 67, 843eqtr4d 2508 . . . 4
86 eqid 2457 . . . . 5
8744, 30, 86, 60, 64sadadd3 14111 . . . 4
88 eqid 2457 . . . . 5
892, 70, 88, 60, 64sadadd3 14111 . . . 4
9085, 87, 893eqtr4d 2508 . . 3
91 inss1 3717 . . . . . . . 8
92 sadcl 14112 . . . . . . . . 9
9344, 30, 92syl2anc 661 . . . . . . . 8
9491, 93syl5ss 3514 . . . . . . 7
95 inss2 3718 . . . . . . . 8
96 ssfi 7760 . . . . . . . 8
975, 95, 96sylancl 662 . . . . . . 7
98 elfpw 7842 . . . . . . 7
9994, 97, 98sylanbrc 664 . . . . . 6
10014ffvelrni 6030 . . . . . 6
10199, 100syl 16 . . . . 5
102101nn0red 10878 . . . 4
103101nn0ge0d 10880 . . . 4
104 fvres 5885 . . . . . . . . 9
105101, 104syl 16 . . . . . . . 8
106 f1ocnvfv2 6183 . . . . . . . . 9
10711, 99, 106sylancr 663 . . . . . . . 8
108105, 107eqtr3d 2500 . . . . . . 7
109108, 95syl6eqss 3553 . . . . . 6
110101nn0zd 10992 . . . . . . 7
111 bitsfzo 14085 . . . . . . 7
112110, 60, 111syl2anc 661 . . . . . 6
113109, 112mpbird 232 . . . . 5
114 elfzolt2 11837 . . . . 5
115113, 114syl 16 . . . 4
116 modid 12020 . . . 4
117102, 62, 103, 115, 116syl22anc 1229 . . 3
118 inss1 3717 . . . . . . . 8
119 sadcl 14112 . . . . . . . . 9
1202, 70, 119syl2anc 661 . . . . . . . 8
121118, 120syl5ss 3514 . . . . . . 7
122 inss2 3718 . . . . . . . 8
123 ssfi 7760 . . . . . . . 8
1245, 122, 123sylancl 662 . . . . . . 7
125 elfpw 7842 . . . . . . 7
126121, 124, 125sylanbrc 664 . . . . . 6
12714ffvelrni 6030 . . . . . 6
128126, 127syl 16 . . . . 5
129128nn0red 10878 . . . 4
130 2nn 10718 . . . . . . 7
131130a1i 11 . . . . . 6
132131, 60nnexpcld 12331 . . . . 5
133132nnrpd 11284 . . . 4
134128nn0ge0d 10880 . . . 4
135 fvres 5885 . . . . . . . . 9
136128, 135syl 16 . . . . . . . 8
137 f1ocnvfv2 6183 . . . . . . . . 9
13811, 126, 137sylancr 663 . . . . . . . 8
139136, 138eqtr3d 2500 . . . . . . 7
140139, 122syl6eqss 3553 . . . . . 6
141128nn0zd 10992 . . . . . . 7
142 bitsfzo 14085 . . . . . . 7
143141, 60, 142syl2anc 661 . . . . . 6
144140, 143mpbird 232 . . . . 5
145 elfzolt2 11837 . . . . 5
146144, 145syl 16 . . . 4
147 modid 12020 . . . 4
148129, 133, 134, 146, 147syl22anc 1229 . . 3
14990, 117, 1483eqtr3d 2506 . 2
150 f1of1 5820 . . . . 5