Step | Hyp | Ref
| Expression |
1 | | sadcp1.n |
. 2
|
2 | | oveq2 6658 |
. . . . . . . . . . 11
..^ ..^ |
3 | | fzo0 12492 |
. . . . . . . . . . 11
..^ |
4 | 2, 3 | syl6eq 2672 |
. . . . . . . . . 10
..^ |
5 | 4 | ineq2d 3814 |
. . . . . . . . 9
sadd
..^ sadd |
6 | | in0 3968 |
. . . . . . . . 9
sadd
|
7 | 5, 6 | syl6eq 2672 |
. . . . . . . 8
sadd
..^ |
8 | 7 | fveq2d 6195 |
. . . . . . 7
sadd ..^ |
9 | | sadcadd.k |
. . . . . . . . 9
bits
|
10 | | 0nn0 11307 |
. . . . . . . . . . 11
|
11 | | fvres 6207 |
. . . . . . . . . . 11
bits bits |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . 10
bits bits |
13 | | 0bits 15161 |
. . . . . . . . . 10
bits |
14 | 12, 13 | eqtr2i 2645 |
. . . . . . . . 9
bits |
15 | 9, 14 | fveq12i 6196 |
. . . . . . . 8
bits
bits |
16 | | bitsf1o 15167 |
. . . . . . . . 9
bits |
17 | | f1ocnvfv1 6532 |
. . . . . . . . 9
bits bits bits |
18 | 16, 10, 17 | mp2an 708 |
. . . . . . . 8
bits bits
|
19 | 15, 18 | eqtri 2644 |
. . . . . . 7
|
20 | 8, 19 | syl6eq 2672 |
. . . . . 6
sadd ..^ |
21 | | fveq2 6191 |
. . . . . . . 8
|
22 | 21 | eleq2d 2687 |
. . . . . . 7
|
23 | | oveq2 6658 |
. . . . . . 7
|
24 | 22, 23 | ifbieq1d 4109 |
. . . . . 6
|
25 | 20, 24 | oveq12d 6668 |
. . . . 5
sadd
..^ |
26 | 4 | ineq2d 3814 |
. . . . . . . . . 10
..^ |
27 | | in0 3968 |
. . . . . . . . . 10
|
28 | 26, 27 | syl6eq 2672 |
. . . . . . . . 9
..^ |
29 | 28 | fveq2d 6195 |
. . . . . . . 8
..^ |
30 | 29, 19 | syl6eq 2672 |
. . . . . . 7
..^ |
31 | 4 | ineq2d 3814 |
. . . . . . . . . 10
..^ |
32 | | in0 3968 |
. . . . . . . . . 10
|
33 | 31, 32 | syl6eq 2672 |
. . . . . . . . 9
..^ |
34 | 33 | fveq2d 6195 |
. . . . . . . 8
..^ |
35 | 34, 19 | syl6eq 2672 |
. . . . . . 7
..^ |
36 | 30, 35 | oveq12d 6668 |
. . . . . 6
..^ ..^ |
37 | | 00id 10211 |
. . . . . 6
|
38 | 36, 37 | syl6eq 2672 |
. . . . 5
..^ ..^ |
39 | 25, 38 | eqeq12d 2637 |
. . . 4
sadd
..^
..^ ..^
|
40 | 39 | imbi2d 330 |
. . 3
sadd ..^ ..^ ..^
|
41 | | oveq2 6658 |
. . . . . . . 8
..^ ..^ |
42 | 41 | ineq2d 3814 |
. . . . . . 7
sadd
..^ sadd ..^ |
43 | 42 | fveq2d 6195 |
. . . . . 6
sadd ..^ sadd ..^ |
44 | | fveq2 6191 |
. . . . . . . 8
|
45 | 44 | eleq2d 2687 |
. . . . . . 7
|
46 | | oveq2 6658 |
. . . . . . 7
|
47 | 45, 46 | ifbieq1d 4109 |
. . . . . 6
|
48 | 43, 47 | oveq12d 6668 |
. . . . 5
sadd
..^ sadd ..^ |
49 | 41 | ineq2d 3814 |
. . . . . . 7
..^ ..^ |
50 | 49 | fveq2d 6195 |
. . . . . 6
..^ ..^ |
51 | 41 | ineq2d 3814 |
. . . . . . 7
..^ ..^ |
52 | 51 | fveq2d 6195 |
. . . . . 6
..^ ..^ |
53 | 50, 52 | oveq12d 6668 |
. . . . 5
..^ ..^ ..^ ..^ |
54 | 48, 53 | eqeq12d 2637 |
. . . 4
sadd
..^
..^ ..^
sadd ..^
..^ ..^ |
55 | 54 | imbi2d 330 |
. . 3
sadd ..^ ..^ ..^ sadd
..^ ..^ ..^ |
56 | | oveq2 6658 |
. . . . . . . 8
..^ ..^ |
57 | 56 | ineq2d 3814 |
. . . . . . 7
sadd
..^ sadd ..^ |
58 | 57 | fveq2d 6195 |
. . . . . 6
sadd ..^ sadd ..^ |
59 | | fveq2 6191 |
. . . . . . . 8
|
60 | 59 | eleq2d 2687 |
. . . . . . 7
|
61 | | oveq2 6658 |
. . . . . . 7
|
62 | 60, 61 | ifbieq1d 4109 |
. . . . . 6
|
63 | 58, 62 | oveq12d 6668 |
. . . . 5
sadd
..^ sadd ..^ |
64 | 56 | ineq2d 3814 |
. . . . . . 7
..^ ..^ |
65 | 64 | fveq2d 6195 |
. . . . . 6
..^ ..^ |
66 | 56 | ineq2d 3814 |
. . . . . . 7
..^ ..^ |
67 | 66 | fveq2d 6195 |
. . . . . 6
..^ ..^ |
68 | 65, 67 | oveq12d 6668 |
. . . . 5
..^ ..^ ..^ ..^ |
69 | 63, 68 | eqeq12d 2637 |
. . . 4
sadd
..^
..^ ..^
sadd ..^
..^ ..^ |
70 | 69 | imbi2d 330 |
. . 3
sadd ..^ ..^ ..^ sadd
..^ ..^ ..^ |
71 | | oveq2 6658 |
. . . . . . . 8
..^ ..^ |
72 | 71 | ineq2d 3814 |
. . . . . . 7
sadd
..^ sadd ..^ |
73 | 72 | fveq2d 6195 |
. . . . . 6
sadd ..^ sadd ..^ |
74 | | fveq2 6191 |
. . . . . . . 8
|
75 | 74 | eleq2d 2687 |
. . . . . . 7
|
76 | | oveq2 6658 |
. . . . . . 7
|
77 | 75, 76 | ifbieq1d 4109 |
. . . . . 6
|
78 | 73, 77 | oveq12d 6668 |
. . . . 5
sadd
..^ sadd ..^ |
79 | 71 | ineq2d 3814 |
. . . . . . 7
..^ ..^ |
80 | 79 | fveq2d 6195 |
. . . . . 6
..^ ..^ |
81 | 71 | ineq2d 3814 |
. . . . . . 7
..^ ..^ |
82 | 81 | fveq2d 6195 |
. . . . . 6
..^ ..^ |
83 | 80, 82 | oveq12d 6668 |
. . . . 5
..^ ..^ ..^ ..^ |
84 | 78, 83 | eqeq12d 2637 |
. . . 4
sadd
..^
..^ ..^
sadd ..^
..^ ..^ |
85 | 84 | imbi2d 330 |
. . 3
sadd ..^ ..^ ..^ sadd
..^ ..^ ..^ |
86 | | sadval.a |
. . . . . . 7
|
87 | | sadval.b |
. . . . . . 7
|
88 | | sadval.c |
. . . . . . 7
cadd
|
89 | 86, 87, 88 | sadc0 15176 |
. . . . . 6
|
90 | 89 | iffalsed 4097 |
. . . . 5
|
91 | 90 | oveq2d 6666 |
. . . 4
|
92 | 91, 37 | syl6eq 2672 |
. . 3
|
93 | 86 | ad2antrr 762 |
. . . . . . 7
sadd
..^ ..^ ..^
|
94 | 87 | ad2antrr 762 |
. . . . . . 7
sadd
..^ ..^ ..^
|
95 | | simplr 792 |
. . . . . . 7
sadd
..^ ..^ ..^
|
96 | | simpr 477 |
. . . . . . 7
sadd
..^ ..^ ..^
sadd ..^
..^ ..^ |
97 | 93, 94, 88, 95, 9, 96 | sadadd2lem 15181 |
. . . . . 6
sadd
..^ ..^ ..^
sadd ..^
..^ ..^ |
98 | 97 | ex 450 |
. . . . 5
sadd
..^ ..^ ..^ sadd ..^
..^ ..^ |
99 | 98 | expcom 451 |
. . . 4
sadd ..^
..^ ..^ sadd
..^ ..^ ..^ |
100 | 99 | a2d 29 |
. . 3
sadd ..^
..^ ..^
sadd ..^ ..^ ..^ |
101 | 40, 55, 70, 85, 92, 100 | nn0ind 11472 |
. 2
sadd
..^
..^ ..^ |
102 | 1, 101 | mpcom 38 |
1
sadd
..^
..^ ..^ |