Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sadcp1 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 10262 . . . . . . 7
31, 2syl6eleq 2373 . . . . . 6
76fveq1i 5526 . . . . 5 cadd
86fveq1i 5526 . . . . . 6 cadd
105, 7, 93eqtr4g 2340 . . . 4 cadd
11 peano2nn0 10004 . . . . . . . 8
121, 11syl 15 . . . . . . 7
13 eqeq1 2289 . . . . . . . . 9
14 oveq1 5865 . . . . . . . . 9
1513, 14ifbieq2d 3585 . . . . . . . 8
16 eqid 2283 . . . . . . . 8
17 0ex 4150 . . . . . . . . 9
18 ovex 5883 . . . . . . . . 9
1917, 18ifex 3623 . . . . . . . 8
2015, 16, 19fvmpt 5602 . . . . . . 7
2112, 20syl 15 . . . . . 6
22 nn0p1nn 10003 . . . . . . . . 9
231, 22syl 15 . . . . . . . 8
2423nnne0d 9790 . . . . . . 7
25 ifnefalse 3573 . . . . . . 7
2624, 25syl 15 . . . . . 6
271nn0cnd 10020 . . . . . . 7
28 ax-1cn 8795 . . . . . . . 8
2928a1i 10 . . . . . . 7
3027, 29pncand 9158 . . . . . 6
3121, 26, 303eqtrd 2319 . . . . 5
33 sadval.a . . . . . . 7
34 sadval.b . . . . . . 7
3533, 34, 6sadcf 12644 . . . . . 6
36 ffvelrn 5663 . . . . . 6
3735, 1, 36syl2anc 642 . . . . 5
38 simpr 447 . . . . . . . . 9
3938eleq1d 2349 . . . . . . . 8
4038eleq1d 2349 . . . . . . . 8
41 simpl 443 . . . . . . . . 9
4241eleq2d 2350 . . . . . . . 8
45 biidd 228 . . . . . . . . 9
46 biidd 228 . . . . . . . . 9
47 eleq2 2344 . . . . . . . . 9
50 eleq1 2343 . . . . . . . . 9
51 eleq1 2343 . . . . . . . . 9
52 biidd 228 . . . . . . . . 9
56 1on 6486 . . . . . . . 8
5756elexi 2797 . . . . . . 7
5857, 17ifex 3623 . . . . . 6 cadd
6110, 32, 603eqtrd 2319 . . 3 cadd