Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sad Unicode version

 Description: Define the addition of two bit sequences, using df-had 1447 and df-cad 1448 bit operations. (Contributed by Mario Carneiro, 5-Sep-2016.)
Assertion
Ref Expression
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-sad
StepHypRef Expression
1 csad 14070 . 2
2 vx . . 3
3 vy . . 3
4 cn0 10820 . . . 4
54cpw 4012 . . 3
6 vk . . . . . 6
76, 2wel 1819 . . . . 5
86, 3wel 1819 . . . . 5
9 c0 3784 . . . . . 6
106cv 1394 . . . . . . 7
11 vc . . . . . . . . 9
12 vm . . . . . . . . 9
13 c2o 7143 . . . . . . . . 9
1412, 2wel 1819 . . . . . . . . . . 11
1512, 3wel 1819 . . . . . . . . . . 11
1611cv 1394 . . . . . . . . . . . 12
179, 16wcel 1818 . . . . . . . . . . 11
1814, 15, 17wcad 1446 . . . . . . . . . 10
19 c1o 7142 . . . . . . . . . 10
2018, 19, 9cif 3941 . . . . . . . . 9
2111, 12, 13, 4, 20cmpt2 6298 . . . . . . . 8
22 vn . . . . . . . . 9
2322cv 1394 . . . . . . . . . . 11
24 cc0 9513 . . . . . . . . . . 11
2523, 24wceq 1395 . . . . . . . . . 10
26 c1 9514 . . . . . . . . . . 11
27 cmin 9828 . . . . . . . . . . 11
2823, 26, 27co 6296 . . . . . . . . . 10
2925, 9, 28cif 3941 . . . . . . . . 9
3022, 4, 29cmpt 4510 . . . . . . . 8
3121, 30, 24cseq 12107 . . . . . . 7
3210, 31cfv 5593 . . . . . 6
339, 32wcel 1818 . . . . 5
347, 8, 33whad 1445 . . . 4
3534, 6, 4crab 2811 . . 3
362, 3, 5, 5, 35cmpt2 6298 . 2
371, 36wceq 1395 1
 Colors of variables: wff setvar class This definition is referenced by:  sadfval  14102
 Copyright terms: Public domain W3C validator