Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sadcp1 Structured version   Visualization version   Unicode version

 Description: The carry sequence (which is a sequence of wffs, encoded as 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.)
Hypotheses
Ref Expression
Assertion
Ref Expression
Distinct variable groups:   ,,   ,,   ,,   ,
Allowed substitution hints:   (,,)   ()   ()   (,,)   (,)

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sadcp1.n . . . . . . 7
2 nn0uz 11217 . . . . . . 7
31, 2syl6eleq 2559 . . . . . 6
76fveq1i 5880 . . . . 5 cadd
86fveq1i 5880 . . . . . 6 cadd
105, 7, 93eqtr4g 2530 . . . 4 cadd
11 peano2nn0 10934 . . . . . . 7
12 eqeq1 2475 . . . . . . . . 9
13 oveq1 6315 . . . . . . . . 9
1412, 13ifbieq2d 3897 . . . . . . . 8
15 eqid 2471 . . . . . . . 8
16 0ex 4528 . . . . . . . . 9
17 ovex 6336 . . . . . . . . 9
1816, 17ifex 3940 . . . . . . . 8
1914, 15, 18fvmpt 5963 . . . . . . 7
201, 11, 193syl 18 . . . . . 6
21 nn0p1nn 10933 . . . . . . . . 9
221, 21syl 17 . . . . . . . 8
2322nnne0d 10676 . . . . . . 7
24 ifnefalse 3884 . . . . . . 7
2523, 24syl 17 . . . . . 6
261nn0cnd 10951 . . . . . . 7
27 1cnd 9677 . . . . . . 7
2826, 27pncand 10006 . . . . . 6
2920, 25, 283eqtrd 2509 . . . . 5
31 sadval.a . . . . . . 7
32 sadval.b . . . . . . 7
3331, 32, 6sadcf 14506 . . . . . 6
3433, 1ffvelrnd 6038 . . . . 5
35 simpr 468 . . . . . . . . 9
3635eleq1d 2533 . . . . . . . 8
3735eleq1d 2533 . . . . . . . 8
38 simpl 464 . . . . . . . . 9
3938eleq2d 2534 . . . . . . . 8
42 biidd 245 . . . . . . . . 9
43 biidd 245 . . . . . . . . 9
44 eleq2 2538 . . . . . . . . 9
47 eleq1 2537 . . . . . . . . 9
48 eleq1 2537 . . . . . . . . 9
49 biidd 245 . . . . . . . . 9
53 1on 7207 . . . . . . . 8
5453elexi 3041 . . . . . . 7
5554, 16ifex 3940 . . . . . 6 cadd
5810, 30, 573eqtrd 2509 . . 3 cadd