Metamath Proof Explorer

Theorem sadcadd

Description: Non-recursive definition of the carry sequence. (Contributed by Mario Carneiro, 8-Sep-2016)

Ref Expression
Hypotheses sadval.a 
|- ( ph -> A C_ NN0 )
sadval.b 
|- ( ph -> B C_ NN0 )
sadval.c 
|- C = seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
sadcp1.n 
|- ( ph -> N e. NN0 )
sadcadd.k 
|- K = `' ( bits |` NN0 )
Assertion sadcadd 
|- ( ph -> ( (/) e. ( C ` N ) <-> ( 2 ^ N ) <_ ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 sadval.a 
 |-  ( ph -> A C_ NN0 )
2 sadval.b 
 |-  ( ph -> B C_ NN0 )
3 sadval.c 
 |-  C = seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
4 sadcp1.n 
 |-  ( ph -> N e. NN0 )
5 sadcadd.k 
 |-  K = `' ( bits |` NN0 )
6 fveq2 
 |-  ( x = 0 -> ( C ` x ) = ( C ` 0 ) )
7 6 eleq2d 
 |-  ( x = 0 -> ( (/) e. ( C ` x ) <-> (/) e. ( C ` 0 ) ) )
8 oveq2 
 |-  ( x = 0 -> ( 2 ^ x ) = ( 2 ^ 0 ) )
9 2cn 
 |-  2 e. CC
10 exp0 
 |-  ( 2 e. CC -> ( 2 ^ 0 ) = 1 )
11 9 10 ax-mp 
 |-  ( 2 ^ 0 ) = 1
12 8 11 eqtrdi 
 |-  ( x = 0 -> ( 2 ^ x ) = 1 )
13 oveq2 
 |-  ( x = 0 -> ( 0 ..^ x ) = ( 0 ..^ 0 ) )
14 fzo0 
 |-  ( 0 ..^ 0 ) = (/)
15 13 14 eqtrdi 
 |-  ( x = 0 -> ( 0 ..^ x ) = (/) )
16 15 ineq2d 
 |-  ( x = 0 -> ( A i^i ( 0 ..^ x ) ) = ( A i^i (/) ) )
17 in0 
 |-  ( A i^i (/) ) = (/)
18 16 17 eqtrdi 
 |-  ( x = 0 -> ( A i^i ( 0 ..^ x ) ) = (/) )
19 18 fveq2d 
 |-  ( x = 0 -> ( K ` ( A i^i ( 0 ..^ x ) ) ) = ( K ` (/) ) )
20 0nn0 
 |-  0 e. NN0
21 fvres 
 |-  ( 0 e. NN0 -> ( ( bits |` NN0 ) ` 0 ) = ( bits ` 0 ) )
22 20 21 ax-mp 
 |-  ( ( bits |` NN0 ) ` 0 ) = ( bits ` 0 )
23 0bits 
 |-  ( bits ` 0 ) = (/)
24 22 23 eqtr2i 
 |-  (/) = ( ( bits |` NN0 ) ` 0 )
25 5 24 fveq12i 
 |-  ( K ` (/) ) = ( `' ( bits |` NN0 ) ` ( ( bits |` NN0 ) ` 0 ) )
26 bitsf1o 
 |-  ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin )
27 f1ocnvfv1 
 |-  ( ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) /\ 0 e. NN0 ) -> ( `' ( bits |` NN0 ) ` ( ( bits |` NN0 ) ` 0 ) ) = 0 )
28 26 20 27 mp2an 
 |-  ( `' ( bits |` NN0 ) ` ( ( bits |` NN0 ) ` 0 ) ) = 0
29 25 28 eqtri 
 |-  ( K ` (/) ) = 0
30 19 29 eqtrdi 
 |-  ( x = 0 -> ( K ` ( A i^i ( 0 ..^ x ) ) ) = 0 )
31 15 ineq2d 
 |-  ( x = 0 -> ( B i^i ( 0 ..^ x ) ) = ( B i^i (/) ) )
32 in0 
 |-  ( B i^i (/) ) = (/)
33 31 32 eqtrdi 
 |-  ( x = 0 -> ( B i^i ( 0 ..^ x ) ) = (/) )
34 33 fveq2d 
 |-  ( x = 0 -> ( K ` ( B i^i ( 0 ..^ x ) ) ) = ( K ` (/) ) )
35 34 29 eqtrdi 
 |-  ( x = 0 -> ( K ` ( B i^i ( 0 ..^ x ) ) ) = 0 )
36 30 35 oveq12d 
 |-  ( x = 0 -> ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) = ( 0 + 0 ) )
37 00id 
 |-  ( 0 + 0 ) = 0
38 36 37 eqtrdi 
 |-  ( x = 0 -> ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) = 0 )
39 12 38 breq12d 
 |-  ( x = 0 -> ( ( 2 ^ x ) <_ ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) <-> 1 <_ 0 ) )
40 7 39 bibi12d 
 |-  ( x = 0 -> ( ( (/) e. ( C ` x ) <-> ( 2 ^ x ) <_ ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) ) <-> ( (/) e. ( C ` 0 ) <-> 1 <_ 0 ) ) )
41 40 imbi2d 
 |-  ( x = 0 -> ( ( ph -> ( (/) e. ( C ` x ) <-> ( 2 ^ x ) <_ ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) ) ) <-> ( ph -> ( (/) e. ( C ` 0 ) <-> 1 <_ 0 ) ) ) )
42 fveq2 
 |-  ( x = k -> ( C ` x ) = ( C ` k ) )
43 42 eleq2d 
 |-  ( x = k -> ( (/) e. ( C ` x ) <-> (/) e. ( C ` k ) ) )
44 oveq2 
 |-  ( x = k -> ( 2 ^ x ) = ( 2 ^ k ) )
45 oveq2 
 |-  ( x = k -> ( 0 ..^ x ) = ( 0 ..^ k ) )
46 45 ineq2d 
 |-  ( x = k -> ( A i^i ( 0 ..^ x ) ) = ( A i^i ( 0 ..^ k ) ) )
47 46 fveq2d 
 |-  ( x = k -> ( K ` ( A i^i ( 0 ..^ x ) ) ) = ( K ` ( A i^i ( 0 ..^ k ) ) ) )
48 45 ineq2d 
 |-  ( x = k -> ( B i^i ( 0 ..^ x ) ) = ( B i^i ( 0 ..^ k ) ) )
49 48 fveq2d 
 |-  ( x = k -> ( K ` ( B i^i ( 0 ..^ x ) ) ) = ( K ` ( B i^i ( 0 ..^ k ) ) ) )
50 47 49 oveq12d 
 |-  ( x = k -> ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) = ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) )
51 44 50 breq12d 
 |-  ( x = k -> ( ( 2 ^ x ) <_ ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) <-> ( 2 ^ k ) <_ ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) ) )
52 43 51 bibi12d 
 |-  ( x = k -> ( ( (/) e. ( C ` x ) <-> ( 2 ^ x ) <_ ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) ) <-> ( (/) e. ( C ` k ) <-> ( 2 ^ k ) <_ ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) ) ) )
53 52 imbi2d 
 |-  ( x = k -> ( ( ph -> ( (/) e. ( C ` x ) <-> ( 2 ^ x ) <_ ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) ) ) <-> ( ph -> ( (/) e. ( C ` k ) <-> ( 2 ^ k ) <_ ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) ) ) ) )
54 fveq2 
 |-  ( x = ( k + 1 ) -> ( C ` x ) = ( C ` ( k + 1 ) ) )
55 54 eleq2d 
 |-  ( x = ( k + 1 ) -> ( (/) e. ( C ` x ) <-> (/) e. ( C ` ( k + 1 ) ) ) )
56 oveq2 
 |-  ( x = ( k + 1 ) -> ( 2 ^ x ) = ( 2 ^ ( k + 1 ) ) )
57 oveq2 
 |-  ( x = ( k + 1 ) -> ( 0 ..^ x ) = ( 0 ..^ ( k + 1 ) ) )
58 57 ineq2d 
 |-  ( x = ( k + 1 ) -> ( A i^i ( 0 ..^ x ) ) = ( A i^i ( 0 ..^ ( k + 1 ) ) ) )
59 58 fveq2d 
 |-  ( x = ( k + 1 ) -> ( K ` ( A i^i ( 0 ..^ x ) ) ) = ( K ` ( A i^i ( 0 ..^ ( k + 1 ) ) ) ) )
60 57 ineq2d 
 |-  ( x = ( k + 1 ) -> ( B i^i ( 0 ..^ x ) ) = ( B i^i ( 0 ..^ ( k + 1 ) ) ) )
61 60 fveq2d 
 |-  ( x = ( k + 1 ) -> ( K ` ( B i^i ( 0 ..^ x ) ) ) = ( K ` ( B i^i ( 0 ..^ ( k + 1 ) ) ) ) )
62 59 61 oveq12d 
 |-  ( x = ( k + 1 ) -> ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) = ( ( K ` ( A i^i ( 0 ..^ ( k + 1 ) ) ) ) + ( K ` ( B i^i ( 0 ..^ ( k + 1 ) ) ) ) ) )
63 56 62 breq12d 
 |-  ( x = ( k + 1 ) -> ( ( 2 ^ x ) <_ ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) <-> ( 2 ^ ( k + 1 ) ) <_ ( ( K ` ( A i^i ( 0 ..^ ( k + 1 ) ) ) ) + ( K ` ( B i^i ( 0 ..^ ( k + 1 ) ) ) ) ) ) )
64 55 63 bibi12d 
 |-  ( x = ( k + 1 ) -> ( ( (/) e. ( C ` x ) <-> ( 2 ^ x ) <_ ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) ) <-> ( (/) e. ( C ` ( k + 1 ) ) <-> ( 2 ^ ( k + 1 ) ) <_ ( ( K ` ( A i^i ( 0 ..^ ( k + 1 ) ) ) ) + ( K ` ( B i^i ( 0 ..^ ( k + 1 ) ) ) ) ) ) ) )
65 64 imbi2d 
 |-  ( x = ( k + 1 ) -> ( ( ph -> ( (/) e. ( C ` x ) <-> ( 2 ^ x ) <_ ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) ) ) <-> ( ph -> ( (/) e. ( C ` ( k + 1 ) ) <-> ( 2 ^ ( k + 1 ) ) <_ ( ( K ` ( A i^i ( 0 ..^ ( k + 1 ) ) ) ) + ( K ` ( B i^i ( 0 ..^ ( k + 1 ) ) ) ) ) ) ) ) )
66 fveq2 
 |-  ( x = N -> ( C ` x ) = ( C ` N ) )
67 66 eleq2d 
 |-  ( x = N -> ( (/) e. ( C ` x ) <-> (/) e. ( C ` N ) ) )
68 oveq2 
 |-  ( x = N -> ( 2 ^ x ) = ( 2 ^ N ) )
69 oveq2 
 |-  ( x = N -> ( 0 ..^ x ) = ( 0 ..^ N ) )
70 69 ineq2d 
 |-  ( x = N -> ( A i^i ( 0 ..^ x ) ) = ( A i^i ( 0 ..^ N ) ) )
71 70 fveq2d 
 |-  ( x = N -> ( K ` ( A i^i ( 0 ..^ x ) ) ) = ( K ` ( A i^i ( 0 ..^ N ) ) ) )
72 69 ineq2d 
 |-  ( x = N -> ( B i^i ( 0 ..^ x ) ) = ( B i^i ( 0 ..^ N ) ) )
73 72 fveq2d 
 |-  ( x = N -> ( K ` ( B i^i ( 0 ..^ x ) ) ) = ( K ` ( B i^i ( 0 ..^ N ) ) ) )
74 71 73 oveq12d 
 |-  ( x = N -> ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) = ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) )
75 68 74 breq12d 
 |-  ( x = N -> ( ( 2 ^ x ) <_ ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) <-> ( 2 ^ N ) <_ ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) ) )
76 67 75 bibi12d 
 |-  ( x = N -> ( ( (/) e. ( C ` x ) <-> ( 2 ^ x ) <_ ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) ) <-> ( (/) e. ( C ` N ) <-> ( 2 ^ N ) <_ ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) ) ) )
77 76 imbi2d 
 |-  ( x = N -> ( ( ph -> ( (/) e. ( C ` x ) <-> ( 2 ^ x ) <_ ( ( K ` ( A i^i ( 0 ..^ x ) ) ) + ( K ` ( B i^i ( 0 ..^ x ) ) ) ) ) ) <-> ( ph -> ( (/) e. ( C ` N ) <-> ( 2 ^ N ) <_ ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) ) ) ) )
78 1 2 3 sadc0 
 |-  ( ph -> -. (/) e. ( C ` 0 ) )
79 0lt1 
 |-  0 < 1
80 0re 
 |-  0 e. RR
81 1re 
 |-  1 e. RR
82 80 81 ltnlei 
 |-  ( 0 < 1 <-> -. 1 <_ 0 )
83 79 82 mpbi 
 |-  -. 1 <_ 0
84 83 a1i 
 |-  ( ph -> -. 1 <_ 0 )
85 78 84 2falsed 
 |-  ( ph -> ( (/) e. ( C ` 0 ) <-> 1 <_ 0 ) )
86 1 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( (/) e. ( C ` k ) <-> ( 2 ^ k ) <_ ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) ) ) -> A C_ NN0 )
87 2 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( (/) e. ( C ` k ) <-> ( 2 ^ k ) <_ ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) ) ) -> B C_ NN0 )
88 simplr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( (/) e. ( C ` k ) <-> ( 2 ^ k ) <_ ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) ) ) -> k e. NN0 )
89 simpr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( (/) e. ( C ` k ) <-> ( 2 ^ k ) <_ ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) ) ) -> ( (/) e. ( C ` k ) <-> ( 2 ^ k ) <_ ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) ) )
90 86 87 3 88 5 89 sadcaddlem 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( (/) e. ( C ` k ) <-> ( 2 ^ k ) <_ ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) ) ) -> ( (/) e. ( C ` ( k + 1 ) ) <-> ( 2 ^ ( k + 1 ) ) <_ ( ( K ` ( A i^i ( 0 ..^ ( k + 1 ) ) ) ) + ( K ` ( B i^i ( 0 ..^ ( k + 1 ) ) ) ) ) ) )
91 90 ex 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( (/) e. ( C ` k ) <-> ( 2 ^ k ) <_ ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) ) -> ( (/) e. ( C ` ( k + 1 ) ) <-> ( 2 ^ ( k + 1 ) ) <_ ( ( K ` ( A i^i ( 0 ..^ ( k + 1 ) ) ) ) + ( K ` ( B i^i ( 0 ..^ ( k + 1 ) ) ) ) ) ) ) )
92 91 expcom 
 |-  ( k e. NN0 -> ( ph -> ( ( (/) e. ( C ` k ) <-> ( 2 ^ k ) <_ ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) ) -> ( (/) e. ( C ` ( k + 1 ) ) <-> ( 2 ^ ( k + 1 ) ) <_ ( ( K ` ( A i^i ( 0 ..^ ( k + 1 ) ) ) ) + ( K ` ( B i^i ( 0 ..^ ( k + 1 ) ) ) ) ) ) ) ) )
93 92 a2d 
 |-  ( k e. NN0 -> ( ( ph -> ( (/) e. ( C ` k ) <-> ( 2 ^ k ) <_ ( ( K ` ( A i^i ( 0 ..^ k ) ) ) + ( K ` ( B i^i ( 0 ..^ k ) ) ) ) ) ) -> ( ph -> ( (/) e. ( C ` ( k + 1 ) ) <-> ( 2 ^ ( k + 1 ) ) <_ ( ( K ` ( A i^i ( 0 ..^ ( k + 1 ) ) ) ) + ( K ` ( B i^i ( 0 ..^ ( k + 1 ) ) ) ) ) ) ) ) )
94 41 53 65 77 85 93 nn0ind 
 |-  ( N e. NN0 -> ( ph -> ( (/) e. ( C ` N ) <-> ( 2 ^ N ) <_ ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) ) ) )
95 4 94 mpcom 
 |-  ( ph -> ( (/) e. ( C ` N ) <-> ( 2 ^ N ) <_ ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + ( K ` ( B i^i ( 0 ..^ N ) ) ) ) ) )