Theorem sadcp1

Description: The carry sequence (which is a sequence of wffs, encoded as 1o and (/) ) is defined recursively as the carry operation applied to the previous carry and the two current inputs. (Contributed by Mario Carneiro, 5-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 )
Assertion	sadcp1	|- ( ph -> ( (/) e. ( C ` ( N + 1 ) ) <-> cadd ( N e. A , N e. B , (/) e. ( C ` 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		nn0uz	|- NN0 = ( ZZ>= ` 0 )
6	4 5	eleqtrdi	|- ( ph -> N e. ( ZZ>= ` 0 ) )
7		seqp1	|- ( N e. ( ZZ>= ` 0 ) -> ( 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 ) ) ) ) ` ( N + 1 ) ) = ( ( 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 ) ) ) ) ` N ) ( 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 ) ) ) ` ( N + 1 ) ) ) )
8	6 7	syl	|- ( ph -> ( 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 ) ) ) ) ` ( N + 1 ) ) = ( ( 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 ) ) ) ) ` N ) ( 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 ) ) ) ` ( N + 1 ) ) ) )
9	3	fveq1i	|- ( C ` ( N + 1 ) ) = ( 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 ) ) ) ) ` ( N + 1 ) )
10	3	fveq1i	|- ( C ` N ) = ( 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 ) ) ) ) ` N )
11	10	oveq1i	|- ( ( C ` N ) ( 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 ) ) ) ` ( N + 1 ) ) ) = ( ( 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 ) ) ) ) ` N ) ( 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 ) ) ) ` ( N + 1 ) ) )
12	8 9 11	3eqtr4g	|- ( ph -> ( C ` ( N + 1 ) ) = ( ( C ` N ) ( 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 ) ) ) ` ( N + 1 ) ) ) )
13		peano2nn0	|- ( N e. NN0 -> ( N + 1 ) e. NN0 )
14		eqeq1	|- ( n = ( N + 1 ) -> ( n = 0 <-> ( N + 1 ) = 0 ) )
15		oveq1	|- ( n = ( N + 1 ) -> ( n - 1 ) = ( ( N + 1 ) - 1 ) )
16	14 15	ifbieq2d	|- ( n = ( N + 1 ) -> if ( n = 0 , (/) , ( n - 1 ) ) = if ( ( N + 1 ) = 0 , (/) , ( ( N + 1 ) - 1 ) ) )
17		eqid	|- ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) = ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) )
18		0ex	|- (/) e. _V
19		ovex	|- ( ( N + 1 ) - 1 ) e. _V
20	18 19	ifex	|- if ( ( N + 1 ) = 0 , (/) , ( ( N + 1 ) - 1 ) ) e. _V
21	16 17 20	fvmpt	|- ( ( N + 1 ) e. NN0 -> ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` ( N + 1 ) ) = if ( ( N + 1 ) = 0 , (/) , ( ( N + 1 ) - 1 ) ) )
22	4 13 21	3syl	|- ( ph -> ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` ( N + 1 ) ) = if ( ( N + 1 ) = 0 , (/) , ( ( N + 1 ) - 1 ) ) )
23		nn0p1nn	|- ( N e. NN0 -> ( N + 1 ) e. NN )
24	4 23	syl	|- ( ph -> ( N + 1 ) e. NN )
25	24	nnne0d	|- ( ph -> ( N + 1 ) =/= 0 )
26		ifnefalse	|- ( ( N + 1 ) =/= 0 -> if ( ( N + 1 ) = 0 , (/) , ( ( N + 1 ) - 1 ) ) = ( ( N + 1 ) - 1 ) )
27	25 26	syl	|- ( ph -> if ( ( N + 1 ) = 0 , (/) , ( ( N + 1 ) - 1 ) ) = ( ( N + 1 ) - 1 ) )
28	4	nn0cnd	|- ( ph -> N e. CC )
29		1cnd	|- ( ph -> 1 e. CC )
30	28 29	pncand	|- ( ph -> ( ( N + 1 ) - 1 ) = N )
31	22 27 30	3eqtrd	|- ( ph -> ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` ( N + 1 ) ) = N )
32	31	oveq2d	|- ( ph -> ( ( C ` N ) ( 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 ) ) ) ` ( N + 1 ) ) ) = ( ( C ` N ) ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) N ) )
33	1 2 3	sadcf	|- ( ph -> C : NN0 --> 2o )
34	33 4	ffvelrnd	|- ( ph -> ( C ` N ) e. 2o )
35		simpr	|- ( ( x = ( C ` N ) /\ y = N ) -> y = N )
36	35	eleq1d	|- ( ( x = ( C ` N ) /\ y = N ) -> ( y e. A <-> N e. A ) )
37	35	eleq1d	|- ( ( x = ( C ` N ) /\ y = N ) -> ( y e. B <-> N e. B ) )
38		simpl	|- ( ( x = ( C ` N ) /\ y = N ) -> x = ( C ` N ) )
39	38	eleq2d	|- ( ( x = ( C ` N ) /\ y = N ) -> ( (/) e. x <-> (/) e. ( C ` N ) ) )
40	36 37 39	cadbi123d	|- ( ( x = ( C ` N ) /\ y = N ) -> ( cadd ( y e. A , y e. B , (/) e. x ) <-> cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) ) )
41	40	ifbid	|- ( ( x = ( C ` N ) /\ y = N ) -> if ( cadd ( y e. A , y e. B , (/) e. x ) , 1o , (/) ) = if ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , 1o , (/) ) )
42		biidd	|- ( c = x -> ( m e. A <-> m e. A ) )
43		biidd	|- ( c = x -> ( m e. B <-> m e. B ) )
44		eleq2w	|- ( c = x -> ( (/) e. c <-> (/) e. x ) )
45	42 43 44	cadbi123d	|- ( c = x -> ( cadd ( m e. A , m e. B , (/) e. c ) <-> cadd ( m e. A , m e. B , (/) e. x ) ) )
46	45	ifbid	|- ( c = x -> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) = if ( cadd ( m e. A , m e. B , (/) e. x ) , 1o , (/) ) )
47		eleq1w	|- ( m = y -> ( m e. A <-> y e. A ) )
48		eleq1w	|- ( m = y -> ( m e. B <-> y e. B ) )
49		biidd	|- ( m = y -> ( (/) e. x <-> (/) e. x ) )
50	47 48 49	cadbi123d	|- ( m = y -> ( cadd ( m e. A , m e. B , (/) e. x ) <-> cadd ( y e. A , y e. B , (/) e. x ) ) )
51	50	ifbid	|- ( m = y -> if ( cadd ( m e. A , m e. B , (/) e. x ) , 1o , (/) ) = if ( cadd ( y e. A , y e. B , (/) e. x ) , 1o , (/) ) )
52	46 51	cbvmpov	|- ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) = ( x e. 2o , y e. NN0 |-> if ( cadd ( y e. A , y e. B , (/) e. x ) , 1o , (/) ) )
53		1oex	|- 1o e. _V
54	53 18	ifex	|- if ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , 1o , (/) ) e. _V
55	41 52 54	ovmpoa	|- ( ( ( C ` N ) e. 2o /\ N e. NN0 ) -> ( ( C ` N ) ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) N ) = if ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , 1o , (/) ) )
56	34 4 55	syl2anc	|- ( ph -> ( ( C ` N ) ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) N ) = if ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , 1o , (/) ) )
57	12 32 56	3eqtrd	|- ( ph -> ( C ` ( N + 1 ) ) = if ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , 1o , (/) ) )
58	57	eleq2d	|- ( ph -> ( (/) e. ( C ` ( N + 1 ) ) <-> (/) e. if ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , 1o , (/) ) ) )
59		noel	|- -. (/) e. (/)
60		iffalse	|- ( -. cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) -> if ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , 1o , (/) ) = (/) )
61	60	eleq2d	|- ( -. cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) -> ( (/) e. if ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , 1o , (/) ) <-> (/) e. (/) ) )
62	59 61	mtbiri	|- ( -. cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) -> -. (/) e. if ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , 1o , (/) ) )
63	62	con4i	|- ( (/) e. if ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , 1o , (/) ) -> cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) )
64		0lt1o	|- (/) e. 1o
65		iftrue	|- ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) -> if ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , 1o , (/) ) = 1o )
66	64 65	eleqtrrid	|- ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) -> (/) e. if ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , 1o , (/) ) )
67	63 66	impbii	|- ( (/) e. if ( cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) , 1o , (/) ) <-> cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) )
68	58 67	bitrdi	|- ( ph -> ( (/) e. ( C ` ( N + 1 ) ) <-> cadd ( N e. A , N e. B , (/) e. ( C ` N ) ) ) )