Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sadcp1 Structured 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 10512 . . . . . . 7
31, 2syl6eleq 2525 . . . . . 6
76fveq1i 5721 . . . . 5 cadd
86fveq1i 5721 . . . . . 6 cadd
105, 7, 93eqtr4g 2492 . . . 4 cadd
11 peano2nn0 10252 . . . . . . 7
12 eqeq1 2441 . . . . . . . . 9
13 oveq1 6080 . . . . . . . . 9
1412, 13ifbieq2d 3751 . . . . . . . 8
15 eqid 2435 . . . . . . . 8
16 0ex 4331 . . . . . . . . 9
17 ovex 6098 . . . . . . . . 9
1816, 17ifex 3789 . . . . . . . 8
1914, 15, 18fvmpt 5798 . . . . . . 7
201, 11, 193syl 19 . . . . . 6
21 nn0p1nn 10251 . . . . . . . . 9
221, 21syl 16 . . . . . . . 8
2322nnne0d 10036 . . . . . . 7
24 ifnefalse 3739 . . . . . . 7
2523, 24syl 16 . . . . . 6
261nn0cnd 10268 . . . . . . 7
27 ax-1cn 9040 . . . . . . . 8
2827a1i 11 . . . . . . 7
2926, 28pncand 9404 . . . . . 6
3020, 25, 293eqtrd 2471 . . . . 5
32 sadval.a . . . . . . 7
33 sadval.b . . . . . . 7
3432, 33, 6sadcf 12957 . . . . . 6
3534, 1ffvelrnd 5863 . . . . 5
36 simpr 448 . . . . . . . . 9
3736eleq1d 2501 . . . . . . . 8
3836eleq1d 2501 . . . . . . . 8
39 simpl 444 . . . . . . . . 9
4039eleq2d 2502 . . . . . . . 8
43 biidd 229 . . . . . . . . 9
44 biidd 229 . . . . . . . . 9
45 eleq2 2496 . . . . . . . . 9
48 eleq1 2495 . . . . . . . . 9
49 eleq1 2495 . . . . . . . . 9
50 biidd 229 . . . . . . . . 9
54 1on 6723 . . . . . . . 8
5554elexi 2957 . . . . . . 7
5655, 16ifex 3789 . . . . . 6 cadd
5910, 31, 583eqtrd 2471 . . 3 cadd