Step | Hyp | Ref
| Expression |
1 | | inss1 3833 |
. . . . . . . . . . 11
..^ |
2 | | sadasslem.1 |
. . . . . . . . . . 11
|
3 | 1, 2 | syl5ss 3614 |
. . . . . . . . . 10
..^ |
4 | | fzofi 12773 |
. . . . . . . . . . . 12
..^ |
5 | 4 | a1i 11 |
. . . . . . . . . . 11
..^ |
6 | | inss2 3834 |
. . . . . . . . . . 11
..^ ..^ |
7 | | ssfi 8180 |
. . . . . . . . . . 11
..^ ..^ ..^ ..^ |
8 | 5, 6, 7 | sylancl 694 |
. . . . . . . . . 10
..^ |
9 | | elfpw 8268 |
. . . . . . . . . 10
..^ ..^
..^ |
10 | 3, 8, 9 | sylanbrc 698 |
. . . . . . . . 9
..^ |
11 | | bitsf1o 15167 |
. . . . . . . . . . 11
bits |
12 | | f1ocnv 6149 |
. . . . . . . . . . 11
bits bits
|
13 | | f1of 6137 |
. . . . . . . . . . 11
bits
bits |
14 | 11, 12, 13 | mp2b 10 |
. . . . . . . . . 10
bits |
15 | 14 | ffvelrni 6358 |
. . . . . . . . 9
..^
bits
..^ |
16 | 10, 15 | syl 17 |
. . . . . . . 8
bits ..^ |
17 | 16 | nn0cnd 11353 |
. . . . . . 7
bits ..^ |
18 | | inss1 3833 |
. . . . . . . . . . 11
..^ |
19 | | sadasslem.2 |
. . . . . . . . . . 11
|
20 | 18, 19 | syl5ss 3614 |
. . . . . . . . . 10
..^ |
21 | | inss2 3834 |
. . . . . . . . . . 11
..^ ..^ |
22 | | ssfi 8180 |
. . . . . . . . . . 11
..^ ..^ ..^ ..^ |
23 | 5, 21, 22 | sylancl 694 |
. . . . . . . . . 10
..^ |
24 | | elfpw 8268 |
. . . . . . . . . 10
..^ ..^
..^ |
25 | 20, 23, 24 | sylanbrc 698 |
. . . . . . . . 9
..^ |
26 | 14 | ffvelrni 6358 |
. . . . . . . . 9
..^
bits
..^ |
27 | 25, 26 | syl 17 |
. . . . . . . 8
bits ..^ |
28 | 27 | nn0cnd 11353 |
. . . . . . 7
bits ..^ |
29 | | inss1 3833 |
. . . . . . . . . . 11
..^ |
30 | | sadasslem.3 |
. . . . . . . . . . 11
|
31 | 29, 30 | syl5ss 3614 |
. . . . . . . . . 10
..^ |
32 | | inss2 3834 |
. . . . . . . . . . 11
..^ ..^ |
33 | | ssfi 8180 |
. . . . . . . . . . 11
..^ ..^ ..^ ..^ |
34 | 5, 32, 33 | sylancl 694 |
. . . . . . . . . 10
..^ |
35 | | elfpw 8268 |
. . . . . . . . . 10
..^ ..^
..^ |
36 | 31, 34, 35 | sylanbrc 698 |
. . . . . . . . 9
..^ |
37 | 14 | ffvelrni 6358 |
. . . . . . . . 9
..^
bits
..^ |
38 | 36, 37 | syl 17 |
. . . . . . . 8
bits ..^ |
39 | 38 | nn0cnd 11353 |
. . . . . . 7
bits ..^ |
40 | 17, 28, 39 | addassd 10062 |
. . . . . 6
bits
..^ bits
..^ bits
..^ bits ..^ bits
..^ bits
..^ |
41 | 40 | oveq1d 6665 |
. . . . 5
bits
..^ bits
..^ bits
..^ bits ..^ bits
..^ bits
..^ |
42 | | inss1 3833 |
. . . . . . . . . 10
sadd ..^
sadd |
43 | | sadcl 15184 |
. . . . . . . . . . 11
sadd |
44 | 2, 19, 43 | syl2anc 693 |
. . . . . . . . . 10
sadd |
45 | 42, 44 | syl5ss 3614 |
. . . . . . . . 9
sadd
..^ |
46 | | inss2 3834 |
. . . . . . . . . 10
sadd ..^
..^ |
47 | | ssfi 8180 |
. . . . . . . . . 10
..^ sadd
..^
..^ sadd
..^ |
48 | 5, 46, 47 | sylancl 694 |
. . . . . . . . 9
sadd
..^ |
49 | | elfpw 8268 |
. . . . . . . . 9
sadd ..^ sadd ..^
sadd
..^ |
50 | 45, 48, 49 | sylanbrc 698 |
. . . . . . . 8
sadd
..^ |
51 | 14 | ffvelrni 6358 |
. . . . . . . 8
sadd ..^ bits sadd
..^ |
52 | 50, 51 | syl 17 |
. . . . . . 7
bits sadd
..^ |
53 | 52 | nn0red 11352 |
. . . . . 6
bits sadd
..^ |
54 | 16 | nn0red 11352 |
. . . . . . 7
bits ..^ |
55 | 27 | nn0red 11352 |
. . . . . . 7
bits ..^ |
56 | 54, 55 | readdcld 10069 |
. . . . . 6
bits ..^ bits ..^ |
57 | 38 | nn0red 11352 |
. . . . . 6
bits ..^ |
58 | | 2rp 11837 |
. . . . . . . 8
|
59 | 58 | a1i 11 |
. . . . . . 7
|
60 | | sadasslem.4 |
. . . . . . . 8
|
61 | 60 | nn0zd 11480 |
. . . . . . 7
|
62 | 59, 61 | rpexpcld 13032 |
. . . . . 6
|
63 | | eqid 2622 |
. . . . . . 7
cadd
cadd |
64 | | eqid 2622 |
. . . . . . 7
bits bits |
65 | 2, 19, 63, 60, 64 | sadadd3 15183 |
. . . . . 6
bits sadd
..^ bits ..^ bits
..^ |
66 | | eqidd 2623 |
. . . . . 6
bits ..^ bits ..^ |
67 | 53, 56, 57, 57, 62, 65, 66 | modadd12d 12726 |
. . . . 5
bits sadd
..^ bits ..^ bits
..^ bits
..^ bits
..^ |
68 | | inss1 3833 |
. . . . . . . . . 10
sadd ..^
sadd |
69 | | sadcl 15184 |
. . . . . . . . . . 11
sadd |
70 | 19, 30, 69 | syl2anc 693 |
. . . . . . . . . 10
sadd |
71 | 68, 70 | syl5ss 3614 |
. . . . . . . . 9
sadd
..^ |
72 | | inss2 3834 |
. . . . . . . . . 10
sadd ..^
..^ |
73 | | ssfi 8180 |
. . . . . . . . . 10
..^ sadd
..^
..^ sadd
..^ |
74 | 5, 72, 73 | sylancl 694 |
. . . . . . . . 9
sadd
..^ |
75 | | elfpw 8268 |
. . . . . . . . 9
sadd ..^ sadd ..^
sadd
..^ |
76 | 71, 74, 75 | sylanbrc 698 |
. . . . . . . 8
sadd
..^ |
77 | 14 | ffvelrni 6358 |
. . . . . . . 8
sadd ..^ bits sadd
..^ |
78 | 76, 77 | syl 17 |
. . . . . . 7
bits sadd
..^ |
79 | 78 | nn0red 11352 |
. . . . . 6
bits sadd
..^ |
80 | 55, 57 | readdcld 10069 |
. . . . . 6
bits ..^ bits ..^ |
81 | | eqidd 2623 |
. . . . . 6
bits ..^ bits ..^ |
82 | | eqid 2622 |
. . . . . . 7
cadd
cadd |
83 | 19, 30, 82, 60, 64 | sadadd3 15183 |
. . . . . 6
bits sadd
..^ bits ..^ bits
..^ |
84 | 54, 54, 79, 80, 62, 81, 83 | modadd12d 12726 |
. . . . 5
bits
..^ bits sadd
..^ bits
..^ bits
..^ bits
..^ |
85 | 41, 67, 84 | 3eqtr4d 2666 |
. . . 4
bits sadd
..^ bits ..^ bits
..^ bits sadd
..^ |
86 | | eqid 2622 |
. . . . 5
cadd sadd cadd sadd |
87 | 44, 30, 86, 60, 64 | sadadd3 15183 |
. . . 4
bits sadd sadd ..^ bits
sadd
..^ bits ..^ |
88 | | eqid 2622 |
. . . . 5
cadd
sadd cadd
sadd |
89 | 2, 70, 88, 60, 64 | sadadd3 15183 |
. . . 4
bits sadd
sadd ..^ bits
..^ bits sadd
..^ |
90 | 85, 87, 89 | 3eqtr4d 2666 |
. . 3
bits sadd sadd ..^ bits sadd sadd ..^ |
91 | | inss1 3833 |
. . . . . . . 8
sadd sadd ..^ sadd sadd |
92 | | sadcl 15184 |
. . . . . . . . 9
sadd
sadd sadd |
93 | 44, 30, 92 | syl2anc 693 |
. . . . . . . 8
sadd sadd |
94 | 91, 93 | syl5ss 3614 |
. . . . . . 7
sadd sadd ..^ |
95 | | inss2 3834 |
. . . . . . . 8
sadd sadd ..^ ..^ |
96 | | ssfi 8180 |
. . . . . . . 8
..^ sadd sadd ..^ ..^ sadd sadd ..^ |
97 | 5, 95, 96 | sylancl 694 |
. . . . . . 7
sadd sadd ..^ |
98 | | elfpw 8268 |
. . . . . . 7
sadd sadd ..^
sadd sadd ..^
sadd sadd ..^ |
99 | 94, 97, 98 | sylanbrc 698 |
. . . . . 6
sadd sadd ..^ |
100 | 14 | ffvelrni 6358 |
. . . . . 6
sadd sadd ..^ bits
sadd sadd ..^ |
101 | 99, 100 | syl 17 |
. . . . 5
bits sadd sadd ..^ |
102 | 101 | nn0red 11352 |
. . . 4
bits sadd sadd ..^ |
103 | 101 | nn0ge0d 11354 |
. . . 4
bits sadd sadd ..^ |
104 | | fvres 6207 |
. . . . . . . . 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 6533 |
. . . . . . . . 9
bits sadd sadd
..^ bits bits
sadd sadd ..^ sadd sadd
..^ |
107 | 11, 99, 106 | sylancr 695 |
. . . . . . . 8
bits bits sadd sadd ..^ sadd sadd
..^ |
108 | 105, 107 | eqtr3d 2658 |
. . . . . . 7
bitsbits sadd sadd ..^ sadd sadd
..^ |
109 | 108, 95 | syl6eqss 3655 |
. . . . . 6
bitsbits sadd sadd ..^ ..^ |
110 | 101 | nn0zd 11480 |
. . . . . . 7
bits sadd sadd ..^ |
111 | | bitsfzo 15157 |
. . . . . . 7
bits sadd sadd ..^ bits sadd sadd ..^ ..^ bitsbits sadd sadd ..^ ..^ |
112 | 110, 60, 111 | syl2anc 693 |
. . . . . 6
bits sadd sadd ..^ ..^
bitsbits
sadd sadd ..^ ..^ |
113 | 109, 112 | mpbird 247 |
. . . . 5
bits sadd sadd ..^ ..^ |
114 | | elfzolt2 12479 |
. . . . 5
bits
sadd sadd ..^ ..^ bits sadd sadd ..^ |
115 | 113, 114 | syl 17 |
. . . 4
bits sadd sadd ..^ |
116 | | modid 12695 |
. . . 4
bits sadd sadd ..^ bits
sadd sadd ..^ bits
sadd sadd ..^ bits sadd sadd ..^ bits sadd sadd ..^ |
117 | 102, 62, 103, 115, 116 | syl22anc 1327 |
. . 3
bits sadd sadd ..^ bits sadd sadd ..^ |
118 | | inss1 3833 |
. . . . . . . 8
sadd sadd ..^ sadd sadd |
119 | | sadcl 15184 |
. . . . . . . . 9
sadd sadd sadd |
120 | 2, 70, 119 | syl2anc 693 |
. . . . . . . 8
sadd sadd |
121 | 118, 120 | syl5ss 3614 |
. . . . . . 7
sadd sadd ..^
|
122 | | inss2 3834 |
. . . . . . . 8
sadd sadd ..^ ..^ |
123 | | ssfi 8180 |
. . . . . . . 8
..^ sadd
sadd ..^ ..^ sadd
sadd ..^ |
124 | 5, 122, 123 | sylancl 694 |
. . . . . . 7
sadd sadd ..^ |
125 | | elfpw 8268 |
. . . . . . 7
sadd sadd ..^
sadd sadd ..^
sadd
sadd ..^ |
126 | 121, 124,
125 | sylanbrc 698 |
. . . . . 6
sadd sadd ..^
|
127 | 14 | ffvelrni 6358 |
. . . . . 6
sadd sadd ..^
bits sadd sadd ..^ |
128 | 126, 127 | syl 17 |
. . . . 5
bits sadd sadd ..^ |
129 | 128 | nn0red 11352 |
. . . 4
bits sadd sadd ..^ |
130 | | 2nn 11185 |
. . . . . . 7
|
131 | 130 | a1i 11 |
. . . . . 6
|
132 | 131, 60 | nnexpcld 13030 |
. . . . 5
|
133 | 132 | nnrpd 11870 |
. . . 4
|
134 | 128 | nn0ge0d 11354 |
. . . 4
bits sadd sadd ..^ |
135 | | fvres 6207 |
. . . . . . . . 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 6533 |
. . . . . . . . 9
bits sadd sadd ..^ bits bits
sadd sadd ..^ sadd sadd ..^ |
138 | 11, 126, 137 | sylancr 695 |
. . . . . . . 8
bits bits sadd sadd ..^ sadd sadd ..^ |
139 | 136, 138 | eqtr3d 2658 |
. . . . . . 7
bitsbits sadd sadd ..^ sadd sadd ..^ |
140 | 139, 122 | syl6eqss 3655 |
. . . . . 6
bitsbits sadd sadd ..^ ..^ |
141 | 128 | nn0zd 11480 |
. . . . . . 7
bits sadd sadd ..^ |
142 | | bitsfzo 15157 |
. . . . . . 7
bits sadd sadd ..^ bits sadd
sadd ..^ ..^
bitsbits
sadd sadd ..^ ..^ |
143 | 141, 60, 142 | syl2anc 693 |
. . . . . 6
bits sadd
sadd ..^ ..^
bitsbits
sadd sadd ..^ ..^ |
144 | 140, 143 | mpbird 247 |
. . . . 5
bits sadd sadd ..^ ..^ |
145 | | elfzolt2 12479 |
. . . . 5
bits
sadd sadd ..^ ..^ bits sadd sadd ..^ |
146 | 144, 145 | syl 17 |
. . . 4
bits sadd sadd ..^ |
147 | | modid 12695 |
. . . 4
bits sadd
sadd ..^ bits
sadd sadd ..^ bits
sadd sadd ..^ bits sadd sadd ..^ bits sadd sadd ..^ |
148 | 129, 133,
134, 146, 147 | syl22anc 1327 |
. . 3
bits sadd
sadd ..^ bits sadd
sadd ..^ |
149 | 90, 117, 148 | 3eqtr3d 2664 |
. 2
bits sadd sadd ..^ bits sadd sadd ..^ |
150 | | f1of1 6136 |
. . . . 5
bits
bits |
151 | 11, 12, 150 | mp2b 10 |
. . . 4
bits |
152 | | f1fveq 6519 |
. . . 4
bits
sadd sadd
..^ sadd sadd ..^ bits sadd sadd ..^ bits sadd sadd ..^
sadd
sadd ..^ sadd sadd ..^ |
153 | 151, 152 | mpan 706 |
. . 3
sadd sadd ..^ sadd sadd ..^ bits sadd sadd ..^ bits sadd sadd ..^
sadd
sadd ..^ sadd sadd ..^ |
154 | 99, 126, 153 | syl2anc 693 |
. 2
bits sadd sadd ..^ bits sadd sadd ..^
sadd
sadd ..^ sadd sadd ..^ |
155 | 149, 154 | mpbid 222 |
1
sadd sadd ..^ sadd sadd ..^ |