Step | Hyp | Ref
| Expression |
1 | | inass 3823 |
. . . . . . . 8
..^ ..^ ..^ ..^ |
2 | | inidm 3822 |
. . . . . . . . 9
..^ ..^ ..^ |
3 | 2 | ineq2i 3811 |
. . . . . . . 8
..^ ..^ ..^ |
4 | 1, 3 | eqtri 2644 |
. . . . . . 7
..^ ..^ ..^ |
5 | 4 | fveq2i 6194 |
. . . . . 6
bits ..^ ..^ bits ..^ |
6 | | inass 3823 |
. . . . . . . 8
..^ ..^ ..^ ..^ |
7 | 2 | ineq2i 3811 |
. . . . . . . 8
..^ ..^ ..^ |
8 | 6, 7 | eqtri 2644 |
. . . . . . 7
..^ ..^ ..^ |
9 | 8 | fveq2i 6194 |
. . . . . 6
bits ..^ ..^ bits ..^ |
10 | 5, 9 | oveq12i 6662 |
. . . . 5
bits
..^ ..^ bits ..^ ..^ bits
..^ bits
..^ |
11 | 10 | oveq1i 6660 |
. . . 4
bits ..^ ..^ bits ..^ ..^ bits
..^ bits
..^ |
12 | | inss1 3833 |
. . . . . 6
..^ |
13 | | sadeq.a |
. . . . . 6
|
14 | 12, 13 | syl5ss 3614 |
. . . . 5
..^ |
15 | | inss1 3833 |
. . . . . 6
..^ |
16 | | sadeq.b |
. . . . . 6
|
17 | 15, 16 | syl5ss 3614 |
. . . . 5
..^ |
18 | | eqid 2622 |
. . . . 5
cadd ..^ ..^
cadd ..^ ..^
|
19 | | sadeq.n |
. . . . 5
|
20 | | eqid 2622 |
. . . . 5
bits bits |
21 | 14, 17, 18, 19, 20 | sadadd3 15183 |
. . . 4
bits ..^ sadd ..^ ..^ bits ..^ ..^ bits ..^ ..^ |
22 | | eqid 2622 |
. . . . 5
cadd
cadd |
23 | 13, 16, 22, 19, 20 | sadadd3 15183 |
. . . 4
bits sadd
..^ bits ..^ bits
..^ |
24 | 11, 21, 23 | 3eqtr4a 2682 |
. . 3
bits ..^ sadd ..^ ..^ bits sadd
..^ |
25 | | inss1 3833 |
. . . . . . . 8
..^ sadd ..^ ..^ ..^ sadd ..^ |
26 | | sadcl 15184 |
. . . . . . . . 9
..^
..^ ..^ sadd ..^
|
27 | 14, 17, 26 | syl2anc 693 |
. . . . . . . 8
..^ sadd ..^
|
28 | 25, 27 | syl5ss 3614 |
. . . . . . 7
..^ sadd ..^ ..^
|
29 | | fzofi 12773 |
. . . . . . . . 9
..^ |
30 | 29 | a1i 11 |
. . . . . . . 8
..^ |
31 | | inss2 3834 |
. . . . . . . 8
..^ sadd ..^ ..^ ..^ |
32 | | ssfi 8180 |
. . . . . . . 8
..^ ..^ sadd ..^ ..^ ..^ ..^ sadd ..^ ..^ |
33 | 30, 31, 32 | sylancl 694 |
. . . . . . 7
..^ sadd ..^ ..^ |
34 | | elfpw 8268 |
. . . . . . 7
..^ sadd ..^ ..^ ..^ sadd ..^ ..^ ..^ sadd ..^ ..^ |
35 | 28, 33, 34 | sylanbrc 698 |
. . . . . 6
..^ sadd ..^ ..^
|
36 | | bitsf1o 15167 |
. . . . . . . 8
bits |
37 | | f1ocnv 6149 |
. . . . . . . 8
bits bits
|
38 | | f1of 6137 |
. . . . . . . 8
bits
bits |
39 | 36, 37, 38 | mp2b 10 |
. . . . . . 7
bits |
40 | 39 | ffvelrni 6358 |
. . . . . 6
..^ sadd ..^ ..^
bits ..^ sadd ..^ ..^ |
41 | 35, 40 | syl 17 |
. . . . 5
bits ..^ sadd ..^ ..^ |
42 | 41 | nn0red 11352 |
. . . 4
bits ..^ sadd ..^ ..^ |
43 | | 2rp 11837 |
. . . . . 6
|
44 | 43 | a1i 11 |
. . . . 5
|
45 | 19 | nn0zd 11480 |
. . . . 5
|
46 | 44, 45 | rpexpcld 13032 |
. . . 4
|
47 | 41 | nn0ge0d 11354 |
. . . 4
bits ..^ sadd ..^ ..^ |
48 | | fvres 6207 |
. . . . . . . . 9
bits
..^ sadd ..^ ..^ bits bits ..^ sadd ..^ ..^ bitsbits ..^ sadd ..^ ..^ |
49 | 41, 48 | syl 17 |
. . . . . . . 8
bits bits ..^ sadd ..^ ..^ bitsbits ..^ sadd ..^ ..^ |
50 | | f1ocnvfv2 6533 |
. . . . . . . . 9
bits ..^ sadd ..^ ..^
bits bits
..^ sadd ..^ ..^ ..^ sadd ..^ ..^ |
51 | 36, 35, 50 | sylancr 695 |
. . . . . . . 8
bits bits ..^ sadd ..^ ..^ ..^ sadd ..^ ..^ |
52 | 49, 51 | eqtr3d 2658 |
. . . . . . 7
bitsbits ..^ sadd ..^ ..^ ..^ sadd ..^ ..^ |
53 | 52, 31 | syl6eqss 3655 |
. . . . . 6
bitsbits ..^ sadd ..^ ..^ ..^ |
54 | 41 | nn0zd 11480 |
. . . . . . 7
bits ..^ sadd ..^ ..^ |
55 | | bitsfzo 15157 |
. . . . . . 7
bits ..^ sadd ..^ ..^ bits ..^ sadd ..^ ..^ ..^ bitsbits ..^ sadd ..^ ..^ ..^ |
56 | 54, 19, 55 | syl2anc 693 |
. . . . . 6
bits ..^ sadd ..^ ..^ ..^ bitsbits ..^ sadd ..^ ..^ ..^ |
57 | 53, 56 | mpbird 247 |
. . . . 5
bits ..^ sadd ..^ ..^ ..^ |
58 | | elfzolt2 12479 |
. . . . 5
bits
..^ sadd ..^ ..^ ..^ bits ..^ sadd ..^ ..^ |
59 | 57, 58 | syl 17 |
. . . 4
bits ..^ sadd ..^ ..^ |
60 | | modid 12695 |
. . . 4
bits ..^ sadd ..^ ..^
bits ..^ sadd ..^ ..^ bits
..^ sadd ..^ ..^ bits ..^ sadd ..^ ..^ bits ..^ sadd ..^ ..^ |
61 | 42, 46, 47, 59, 60 | syl22anc 1327 |
. . 3
bits ..^ sadd ..^ ..^ bits ..^ sadd ..^ ..^ |
62 | | inss1 3833 |
. . . . . . . 8
sadd ..^
sadd |
63 | | sadcl 15184 |
. . . . . . . . 9
sadd |
64 | 13, 16, 63 | syl2anc 693 |
. . . . . . . 8
sadd |
65 | 62, 64 | syl5ss 3614 |
. . . . . . 7
sadd
..^ |
66 | | inss2 3834 |
. . . . . . . 8
sadd ..^
..^ |
67 | | ssfi 8180 |
. . . . . . . 8
..^ sadd
..^
..^ sadd
..^ |
68 | 30, 66, 67 | sylancl 694 |
. . . . . . 7
sadd
..^ |
69 | | elfpw 8268 |
. . . . . . 7
sadd ..^ sadd ..^
sadd
..^ |
70 | 65, 68, 69 | sylanbrc 698 |
. . . . . 6
sadd
..^ |
71 | 39 | ffvelrni 6358 |
. . . . . 6
sadd ..^ bits sadd
..^ |
72 | 70, 71 | syl 17 |
. . . . 5
bits sadd
..^ |
73 | 72 | nn0red 11352 |
. . . 4
bits sadd
..^ |
74 | 72 | nn0ge0d 11354 |
. . . 4
bits sadd
..^ |
75 | | fvres 6207 |
. . . . . . . . 9
bits
sadd
..^
bits bits
sadd
..^ bitsbits
sadd
..^ |
76 | 72, 75 | syl 17 |
. . . . . . . 8
bits bits sadd
..^ bitsbits
sadd
..^ |
77 | | f1ocnvfv2 6533 |
. . . . . . . . 9
bits sadd ..^ bits bits sadd
..^ sadd ..^ |
78 | 36, 70, 77 | sylancr 695 |
. . . . . . . 8
bits bits sadd
..^ sadd ..^ |
79 | 76, 78 | eqtr3d 2658 |
. . . . . . 7
bitsbits sadd
..^ sadd ..^ |
80 | 79, 66 | syl6eqss 3655 |
. . . . . 6
bitsbits sadd
..^
..^ |
81 | 72 | nn0zd 11480 |
. . . . . . 7
bits sadd
..^ |
82 | | bitsfzo 15157 |
. . . . . . 7
bits sadd
..^ bits sadd
..^ ..^ bitsbits sadd
..^
..^ |
83 | 81, 19, 82 | syl2anc 693 |
. . . . . 6
bits sadd
..^ ..^
bitsbits
sadd
..^
..^ |
84 | 80, 83 | mpbird 247 |
. . . . 5
bits sadd
..^ ..^ |
85 | | elfzolt2 12479 |
. . . . 5
bits
sadd
..^ ..^
bits sadd
..^ |
86 | 84, 85 | syl 17 |
. . . 4
bits sadd
..^ |
87 | | modid 12695 |
. . . 4
bits sadd
..^ bits
sadd
..^ bits sadd
..^ bits sadd
..^ bits sadd
..^ |
88 | 73, 46, 74, 86, 87 | syl22anc 1327 |
. . 3
bits sadd
..^ bits sadd
..^ |
89 | 24, 61, 88 | 3eqtr3rd 2665 |
. 2
bits sadd
..^ bits ..^ sadd ..^ ..^ |
90 | | f1of1 6136 |
. . . . 5
bits
bits |
91 | 36, 37, 90 | mp2b 10 |
. . . 4
bits |
92 | | f1fveq 6519 |
. . . 4
bits
sadd ..^ ..^ sadd ..^ ..^ bits sadd
..^ bits
..^ sadd ..^ ..^
sadd ..^ ..^ sadd ..^ ..^ |
93 | 91, 92 | mpan 706 |
. . 3
sadd
..^ ..^ sadd ..^ ..^ bits sadd
..^ bits ..^ sadd ..^ ..^ sadd
..^ ..^ sadd ..^ ..^ |
94 | 70, 35, 93 | syl2anc 693 |
. 2
bits sadd
..^ bits
..^ sadd ..^ ..^
sadd ..^ ..^ sadd ..^ ..^ |
95 | 89, 94 | mpbid 222 |
1
sadd
..^ ..^ sadd ..^ ..^ |