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

 Description: The core of the proof of sadadd2 14513. The intuitive justification for this is that cadd is true if at least two arguments are true, and hadd is true if an odd number of arguments are true, so altogether the result is where is the number of true arguments, which is equivalently obtained by adding together one for each true argument, on the right side. (Contributed by Mario Carneiro, 8-Sep-2016.)
Assertion
Ref Expression

StepHypRef Expression
1 0cn 9653 . . . . . . . . 9
2 ifcl 3914 . . . . . . . . 9
31, 2mpan2 685 . . . . . . . 8
43ad2antrr 740 . . . . . . 7
5 simpll 768 . . . . . . 7
64, 5, 5add12d 9876 . . . . . 6
75, 4, 5addassd 9683 . . . . . 6
86, 7eqtr4d 2508 . . . . 5
9 pm5.501 348 . . . . . . . . 9
109adantl 473 . . . . . . . 8
1110bicomd 206 . . . . . . 7
1211ifbid 3894 . . . . . 6
13 simpr 468 . . . . . . . . 9
1413orcd 399 . . . . . . . 8
15 iftrue 3878 . . . . . . . 8
1614, 15syl 17 . . . . . . 7
1752timesd 10878 . . . . . . 7
1816, 17eqtrd 2505 . . . . . 6
1912, 18oveq12d 6326 . . . . 5
20 iftrue 3878 . . . . . . . 8
2120adantl 473 . . . . . . 7
2221oveq1d 6323 . . . . . 6
2322oveq1d 6323 . . . . 5
248, 19, 233eqtr4d 2515 . . . 4
25 iffalse 3881 . . . . . . . . 9
2625adantl 473 . . . . . . . 8
2726oveq1d 6323 . . . . . . 7
283ad2antrr 740 . . . . . . . 8
2928addid2d 9852 . . . . . . 7
3027, 29eqtrd 2505 . . . . . 6
3130oveq1d 6323 . . . . 5
32 2cnd 10704 . . . . . . . . . . . 12
33 id 22 . . . . . . . . . . . 12
3432, 33mulcld 9681 . . . . . . . . . . 11
3534addid2d 9852 . . . . . . . . . 10
36 2times 10751 . . . . . . . . . 10
3735, 36eqtrd 2505 . . . . . . . . 9
3837adantr 472 . . . . . . . 8
39 iftrue 3878 . . . . . . . . . 10
4039adantl 473 . . . . . . . . 9
41 iftrue 3878 . . . . . . . . . 10
4241adantl 473 . . . . . . . . 9
4340, 42oveq12d 6326 . . . . . . . 8
44 iftrue 3878 . . . . . . . . . 10
4544adantl 473 . . . . . . . . 9
4645oveq1d 6323 . . . . . . . 8
4738, 43, 463eqtr4d 2515 . . . . . . 7
48 simpl 464 . . . . . . . . 9
49 0cnd 9654 . . . . . . . . 9
5048, 49addcomd 9853 . . . . . . . 8
51 iffalse 3881 . . . . . . . . . 10
5251adantl 473 . . . . . . . . 9
53 iffalse 3881 . . . . . . . . . 10
5453adantl 473 . . . . . . . . 9
5552, 54oveq12d 6326 . . . . . . . 8
56 iffalse 3881 . . . . . . . . . 10
5756adantl 473 . . . . . . . . 9
5857oveq1d 6323 . . . . . . . 8
5950, 55, 583eqtr4d 2515 . . . . . . 7
6047, 59pm2.61dan 808 . . . . . 6
6160ad2antrr 740 . . . . 5
62 ifnot 3917 . . . . . . 7
63 nbn2 352 . . . . . . . . 9
6463adantl 473 . . . . . . . 8
6564ifbid 3894 . . . . . . 7
6662, 65syl5eqr 2519 . . . . . 6
67 biorf 412 . . . . . . . 8
6867adantl 473 . . . . . . 7
6968ifbid 3894 . . . . . 6
7066, 69oveq12d 6326 . . . . 5
7131, 61, 703eqtr2rd 2512 . . . 4
7224, 71pm2.61dan 808 . . 3
7573, 74syl5bbr 267 . . . . . 6 hadd
7776ifbid 3894 . . . 4 hadd
8079ifbid 3894 . . . 4 cadd
82 iftrue 3878 . . . . 5
8382adantl 473 . . . 4
8483oveq2d 6324 . . 3
8620adantl 473 . . . . . 6
8786oveq1d 6323 . . . . 5
8845oveq2d 6324 . . . . . . . 8
8938, 43, 883eqtr4d 2515 . . . . . . 7
9054, 57eqtr4d 2508 . . . . . . . 8
9152, 90oveq12d 6326 . . . . . . 7
9289, 91pm2.61dan 808 . . . . . 6
9392ad2antrr 740 . . . . 5
949adantl 473 . . . . . . . . . 10
9594notbid 301 . . . . . . . . 9
96 df-xor 1431 . . . . . . . . 9
9795, 96syl6bbr 271 . . . . . . . 8
9897ifbid 3894 . . . . . . 7
9962, 98syl5eqr 2519 . . . . . 6
100 ibar 512 . . . . . . . 8
101100adantl 473 . . . . . . 7
102101ifbid 3894 . . . . . 6
10399, 102oveq12d 6326 . . . . 5
10487, 93, 1033eqtr2rd 2512 . . . 4
105 simplll 776 . . . . . . 7
106 0cnd 9654 . . . . . . 7
107105, 106ifclda 3904 . . . . . 6
108 0cnd 9654 . . . . . 6
109107, 108addcomd 9853 . . . . 5
11063adantl 473 . . . . . . . . 9
111110con1bid 337 . . . . . . . 8
11296, 111syl5bb 265 . . . . . . 7
113112ifbid 3894 . . . . . 6
114 simpr 468 . . . . . . . 8
115114intnanrd 931 . . . . . . 7
116 iffalse 3881 . . . . . . 7
117115, 116syl 17 . . . . . 6
118113, 117oveq12d 6326 . . . . 5
11925adantl 473 . . . . . 6
120119oveq1d 6323 . . . . 5
121109, 118, 1203eqtr4d 2515 . . . 4
122104, 121pm2.61dan 808 . . 3
12473, 123syl5bbr 267 . . . . . 6 hadd
126125ifbid 3894 . . . 4 hadd