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

 Description: The core of the proof of sadadd2 12651. 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 8831 . . . . . . . . 9
2 ifcl 3601 . . . . . . . . 9
31, 2mpan2 652 . . . . . . . 8
43ad2antrr 706 . . . . . . 7
5 simpll 730 . . . . . . 7
64, 5, 5add12d 9033 . . . . . 6
75, 4, 5addassd 8857 . . . . . 6
86, 7eqtr4d 2318 . . . . 5
9 pm5.501 330 . . . . . . . . 9
109adantl 452 . . . . . . . 8
1110bicomd 192 . . . . . . 7
1211ifbid 3583 . . . . . 6
13 simpr 447 . . . . . . . . 9
1413orcd 381 . . . . . . . 8
15 iftrue 3571 . . . . . . . 8
1614, 15syl 15 . . . . . . 7
1752timesd 9954 . . . . . . 7
1816, 17eqtrd 2315 . . . . . 6
1912, 18oveq12d 5876 . . . . 5
20 iftrue 3571 . . . . . . . 8
2120adantl 452 . . . . . . 7
2221oveq1d 5873 . . . . . 6
2322oveq1d 5873 . . . . 5
248, 19, 233eqtr4d 2325 . . . 4
25 iffalse 3572 . . . . . . . . 9
2625adantl 452 . . . . . . . 8
2726oveq1d 5873 . . . . . . 7
283ad2antrr 706 . . . . . . . 8
2928addid2d 9013 . . . . . . 7
3027, 29eqtrd 2315 . . . . . 6
3130oveq1d 5873 . . . . 5
32 2cn 9816 . . . . . . . . . . . . 13
3332a1i 10 . . . . . . . . . . . 12
34 id 19 . . . . . . . . . . . 12
3533, 34mulcld 8855 . . . . . . . . . . 11
3635addid2d 9013 . . . . . . . . . 10
37 2times 9843 . . . . . . . . . 10
3836, 37eqtrd 2315 . . . . . . . . 9
3938adantr 451 . . . . . . . 8
40 iftrue 3571 . . . . . . . . . 10
4140adantl 452 . . . . . . . . 9
42 iftrue 3571 . . . . . . . . . 10
4342adantl 452 . . . . . . . . 9
4441, 43oveq12d 5876 . . . . . . . 8
45 iftrue 3571 . . . . . . . . . 10
4645adantl 452 . . . . . . . . 9
4746oveq1d 5873 . . . . . . . 8
4839, 44, 473eqtr4d 2325 . . . . . . 7
49 simpl 443 . . . . . . . . 9
501a1i 10 . . . . . . . . 9
5149, 50addcomd 9014 . . . . . . . 8
52 iffalse 3572 . . . . . . . . . 10
5352adantl 452 . . . . . . . . 9
54 iffalse 3572 . . . . . . . . . 10
5554adantl 452 . . . . . . . . 9
5653, 55oveq12d 5876 . . . . . . . 8
57 iffalse 3572 . . . . . . . . . 10
5857adantl 452 . . . . . . . . 9
5958oveq1d 5873 . . . . . . . 8
6051, 56, 593eqtr4d 2325 . . . . . . 7
6148, 60pm2.61dan 766 . . . . . 6
6261ad2antrr 706 . . . . 5
63 ifnot 3603 . . . . . . 7
64 nbn2 334 . . . . . . . . 9
6564adantl 452 . . . . . . . 8
6665ifbid 3583 . . . . . . 7
6763, 66syl5eqr 2329 . . . . . 6
68 biorf 394 . . . . . . . 8
6968adantl 452 . . . . . . 7
7069ifbid 3583 . . . . . 6
7167, 70oveq12d 5876 . . . . 5
7231, 62, 713eqtr2rd 2322 . . . 4
7324, 72pm2.61dan 766 . . 3
74 hadrot 1380 . . . . . . 7 hadd hadd
75 had1 1392 . . . . . . 7 hadd
7674, 75syl5bbr 250 . . . . . 6 hadd
7776adantl 452 . . . . 5 hadd
7877ifbid 3583 . . . 4 hadd
79 cad1 1388 . . . . . 6 cadd
8079adantl 452 . . . . 5 cadd
8180ifbid 3583 . . . 4 cadd
8278, 81oveq12d 5876 . . 3 hadd cadd
83 iftrue 3571 . . . . 5
8483adantl 452 . . . 4
8584oveq2d 5874 . . 3
8673, 82, 853eqtr4d 2325 . 2 hadd cadd
8746oveq2d 5874 . . . . . . . 8
8839, 44, 873eqtr4d 2325 . . . . . . 7
8955, 58eqtr4d 2318 . . . . . . . 8
9053, 89oveq12d 5876 . . . . . . 7
9188, 90pm2.61dan 766 . . . . . 6
9291ad2antrr 706 . . . . 5
939adantl 452 . . . . . . . . . . 11
9493notbid 285 . . . . . . . . . 10
95 df-xor 1296 . . . . . . . . . 10
9694, 95syl6bbr 254 . . . . . . . . 9
9796ifbid 3583 . . . . . . . 8
9863, 97syl5eqr 2329 . . . . . . 7
99 ibar 490 . . . . . . . . 9
10099adantl 452 . . . . . . . 8
101100ifbid 3583 . . . . . . 7
10298, 101oveq12d 5876 . . . . . 6
103102eqcomd 2288 . . . . 5
10420adantl 452 . . . . . 6
105104oveq1d 5873 . . . . 5
10692, 103, 1053eqtr4d 2325 . . . 4
107 simplll 734 . . . . . . 7
1081a1i 10 . . . . . . 7
109107, 108ifclda 3592 . . . . . 6
1101a1i 10 . . . . . 6
111109, 110addcomd 9014 . . . . 5
11264adantl 452 . . . . . . . . 9
113112con1bid 320 . . . . . . . 8
11495, 113syl5bb 248 . . . . . . 7
115114ifbid 3583 . . . . . 6
116 simpr 447 . . . . . . . 8
117 simpl 443 . . . . . . . 8
118116, 117nsyl 113 . . . . . . 7
119 iffalse 3572 . . . . . . 7
120118, 119syl 15 . . . . . 6
121115, 120oveq12d 5876 . . . . 5
12225adantl 452 . . . . . 6
123122oveq1d 5873 . . . . 5
124111, 121, 1233eqtr4d 2325 . . . 4
125106, 124pm2.61dan 766 . . 3
126 had0 1393 . . . . . . 7 hadd
12774, 126syl5bbr 250 . . . . . 6 hadd
128127adantl 452 . . . . 5 hadd
129128ifbid 3583 . . . 4 hadd
130 cad0 1390 . . . . . 6 cadd
131130adantl 452 . . . . 5 cadd
132131ifbid 3583 . . . 4 cadd
133129, 132oveq12d 5876 . . 3 hadd cadd
134 iffalse 3572 . . . . 5
135134oveq2d 5874 . . . 4
136 ifcl 3601 . . . . . . 7
1371, 136mpan2 652 . . . . . 6
138137, 3addcld 8854 . . . . 5
139138addid1d 9012 . . . 4
140135, 139sylan9eqr 2337 . . 3
141125, 133, 1403eqtr4d 2325 . 2 hadd cadd