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:   (,,)   ()   ()   (,,)   (,)

Proof of Theorem sadcp1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sadcp1.n . . . . . . 7
2 nn0uz 11115 . . . . . . 7
31, 2syl6eleq 2565 . . . . . 6
4 seqp1 12089 . . . . . 6 cadd cadd cadd
53, 4syl 16 . . . . 5 cadd cadd cadd
6 sadval.c . . . . . 6 cadd
76fveq1i 5866 . . . . 5 cadd
86fveq1i 5866 . . . . . 6 cadd
98oveq1i 6293 . . . . 5 cadd cadd cadd
105, 7, 93eqtr4g 2533 . . . 4 cadd
11 peano2nn0 10835 . . . . . . 7
12 eqeq1 2471 . . . . . . . . 9
13 oveq1 6290 . . . . . . . . 9
1412, 13ifbieq2d 3964 . . . . . . . 8
15 eqid 2467 . . . . . . . 8
16 0ex 4577 . . . . . . . . 9
17 ovex 6308 . . . . . . . . 9
1816, 17ifex 4008 . . . . . . . 8
1914, 15, 18fvmpt 5949 . . . . . . 7
201, 11, 193syl 20 . . . . . 6
21 nn0p1nn 10834 . . . . . . . . 9
221, 21syl 16 . . . . . . . 8
2322nnne0d 10579 . . . . . . 7
24 ifnefalse 3951 . . . . . . 7
2523, 24syl 16 . . . . . 6
261nn0cnd 10853 . . . . . . 7
27 ax-1cn 9549 . . . . . . . 8
2827a1i 11 . . . . . . 7
2926, 28pncand 9930 . . . . . 6
3020, 25, 293eqtrd 2512 . . . . 5
3130oveq2d 6299 . . . 4 cadd cadd
32 sadval.a . . . . . . 7
33 sadval.b . . . . . . 7
3432, 33, 6sadcf 13961 . . . . . 6
3534, 1ffvelrnd 6021 . . . . 5
36 simpr 461 . . . . . . . . 9
3736eleq1d 2536 . . . . . . . 8
3836eleq1d 2536 . . . . . . . 8
39 simpl 457 . . . . . . . . 9
4039eleq2d 2537 . . . . . . . 8
4137, 38, 40cadbi123d 1434 . . . . . . 7 cadd cadd
4241ifbid 3961 . . . . . 6 cadd cadd
43 biidd 237 . . . . . . . . 9
44 biidd 237 . . . . . . . . 9
45 eleq2 2540 . . . . . . . . 9
4643, 44, 45cadbi123d 1434 . . . . . . . 8 cadd cadd
4746ifbid 3961 . . . . . . 7 cadd cadd
48 eleq1 2539 . . . . . . . . 9
49 eleq1 2539 . . . . . . . . 9
50 biidd 237 . . . . . . . . 9
5148, 49, 50cadbi123d 1434 . . . . . . . 8 cadd cadd
5251ifbid 3961 . . . . . . 7 cadd cadd
5347, 52cbvmpt2v 6360 . . . . . 6 cadd cadd
54 1on 7137 . . . . . . . 8
5554elexi 3123 . . . . . . 7
5655, 16ifex 4008 . . . . . 6 cadd
5742, 53, 56ovmpt2a 6416 . . . . 5 cadd cadd
5835, 1, 57syl2anc 661 . . . 4 cadd cadd
5910, 31, 583eqtrd 2512 . . 3 cadd
6059eleq2d 2537 . 2 cadd
61 noel 3789 . . . . 5
62 iffalse 3948 . . . . . 6 cadd cadd
6362eleq2d 2537 . . . . 5 cadd cadd
6461, 63mtbiri 303 . . . 4 cadd cadd
6564con4i 130 . . 3 cadd cadd
66 0lt1o 7154 . . . 4
67 iftrue 3945 . . . 4 cadd cadd
6866, 67syl5eleqr 2562 . . 3 cadd cadd
6965, 68impbii 188 . 2 cadd cadd
7060, 69syl6bb 261 1 cadd