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

 Description: The core of the proof of sadadd2 12653. 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 8833 . . . . . . . . 9
2 ifcl 3603 . . . . . . . . 9
31, 2mpan2 652 . . . . . . . 8
43ad2antrr 706 . . . . . . 7
5 simpll 730 . . . . . . 7
64, 5, 5add12d 9035 . . . . . 6
75, 4, 5addassd 8859 . . . . . 6
86, 7eqtr4d 2320 . . . . 5
9 pm5.501 330 . . . . . . . . 9
109adantl 452 . . . . . . . 8
1110bicomd 192 . . . . . . 7
1211ifbid 3585 . . . . . 6
13 simpr 447 . . . . . . . . 9
1413orcd 381 . . . . . . . 8
15 iftrue 3573 . . . . . . . 8
1614, 15syl 15 . . . . . . 7
1752timesd 9956 . . . . . . 7
1816, 17eqtrd 2317 . . . . . 6
1912, 18oveq12d 5878 . . . . 5
20 iftrue 3573 . . . . . . . 8
2120adantl 452 . . . . . . 7
2221oveq1d 5875 . . . . . 6
2322oveq1d 5875 . . . . 5
248, 19, 233eqtr4d 2327 . . . 4
25 iffalse 3574 . . . . . . . . 9
2625adantl 452 . . . . . . . 8
2726oveq1d 5875 . . . . . . 7
283ad2antrr 706 . . . . . . . 8
2928addid2d 9015 . . . . . . 7
3027, 29eqtrd 2317 . . . . . 6
3130oveq1d 5875 . . . . 5
32 2cn 9818 . . . . . . . . . . . . 13
3332a1i 10 . . . . . . . . . . . 12
34 id 19 . . . . . . . . . . . 12
3533, 34mulcld 8857 . . . . . . . . . . 11
3635addid2d 9015 . . . . . . . . . 10
37 2times 9845 . . . . . . . . . 10
3836, 37eqtrd 2317 . . . . . . . . 9
3938adantr 451 . . . . . . . 8
40 iftrue 3573 . . . . . . . . . 10
4140adantl 452 . . . . . . . . 9
42 iftrue 3573 . . . . . . . . . 10
4342adantl 452 . . . . . . . . 9
4441, 43oveq12d 5878 . . . . . . . 8
45 iftrue 3573 . . . . . . . . . 10
4645adantl 452 . . . . . . . . 9
4746oveq1d 5875 . . . . . . . 8
4839, 44, 473eqtr4d 2327 . . . . . . 7
49 simpl 443 . . . . . . . . 9
501a1i 10 . . . . . . . . 9
5149, 50addcomd 9016 . . . . . . . 8
52 iffalse 3574 . . . . . . . . . 10
5352adantl 452 . . . . . . . . 9
54 iffalse 3574 . . . . . . . . . 10
5554adantl 452 . . . . . . . . 9
5653, 55oveq12d 5878 . . . . . . . 8
57 iffalse 3574 . . . . . . . . . 10
5857adantl 452 . . . . . . . . 9
5958oveq1d 5875 . . . . . . . 8
6051, 56, 593eqtr4d 2327 . . . . . . 7
6148, 60pm2.61dan 766 . . . . . 6
6261ad2antrr 706 . . . . 5
63 ifnot 3605 . . . . . . 7
64 nbn2 334 . . . . . . . . 9
6564adantl 452 . . . . . . . 8
6665ifbid 3585 . . . . . . 7
6763, 66syl5eqr 2331 . . . . . 6
68 biorf 394 . . . . . . . 8
6968adantl 452 . . . . . . 7
7069ifbid 3585 . . . . . 6
7167, 70oveq12d 5878 . . . . 5
7231, 62, 713eqtr2rd 2324 . . . 4
7324, 72pm2.61dan 766 . . 3
7674, 75syl5bbr 250 . . . . . 6 hadd
7877ifbid 3585 . . . 4 hadd
8180ifbid 3585 . . . 4 cadd
83 iftrue 3573 . . . . 5
8483adantl 452 . . . 4
8584oveq2d 5876 . . 3
8746oveq2d 5876 . . . . . . . 8
8839, 44, 873eqtr4d 2327 . . . . . . 7
8955, 58eqtr4d 2320 . . . . . . . 8
9053, 89oveq12d 5878 . . . . . . 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 3585 . . . . . . . 8
9863, 97syl5eqr 2331 . . . . . . 7
99 ibar 490 . . . . . . . . 9
10099adantl 452 . . . . . . . 8
101100ifbid 3585 . . . . . . 7
10298, 101oveq12d 5878 . . . . . 6
103102eqcomd 2290 . . . . 5
10420adantl 452 . . . . . 6
105104oveq1d 5875 . . . . 5
10692, 103, 1053eqtr4d 2327 . . . 4
107 simplll 734 . . . . . . 7
1081a1i 10 . . . . . . 7
109107, 108ifclda 3594 . . . . . 6
1101a1i 10 . . . . . 6
111109, 110addcomd 9016 . . . . 5
11264adantl 452 . . . . . . . . 9
113112con1bid 320 . . . . . . . 8
11495, 113syl5bb 248 . . . . . . 7
115114ifbid 3585 . . . . . 6
116 simpr 447 . . . . . . . 8
117 simpl 443 . . . . . . . 8
118116, 117nsyl 113 . . . . . . 7
119 iffalse 3574 . . . . . . 7
120118, 119syl 15 . . . . . 6
121115, 120oveq12d 5878 . . . . 5
12225adantl 452 . . . . . 6
123122oveq1d 5875 . . . . 5
124111, 121, 1233eqtr4d 2327 . . . 4
125106, 124pm2.61dan 766 . . 3
12774, 126syl5bbr 250 . . . . . 6 hadd
129128ifbid 3585 . . . 4 hadd