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

 Description: Define the addition of two bit sequences, using df-had 1390 and df-cad 1391 bit operations. (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
2 nn0ex 10229 . . . 4
32elpw2 4366 . . 3
41, 3sylibr 205 . 2
62elpw2 4366 . . 3
75, 6sylibr 205 . 2
8 simpl 445 . . . . . 6
98eleq2d 2505 . . . . 5
10 simpr 449 . . . . . 6
1110eleq2d 2505 . . . . 5
12 simp1l 982 . . . . . . . . . . . . 13
1312eleq2d 2505 . . . . . . . . . . . 12
14 simp1r 983 . . . . . . . . . . . . 13
1514eleq2d 2505 . . . . . . . . . . . 12
16 biidd 230 . . . . . . . . . . . 12
1713, 15, 16cadbi123d 1393 . . . . . . . . . . 11 cadd cadd
1817ifbid 3759 . . . . . . . . . 10 cadd cadd
1918mpt2eq3dva 6140 . . . . . . . . 9 cadd cadd
2019seqeq2d 11332 . . . . . . . 8 cadd cadd