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

Theorem sadadd2lem2 14100
Description: The core of the proof of sadadd2 14110. 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
sadadd2lem2

Proof of Theorem sadadd2lem2
StepHypRef Expression
1 0cn 9609 . . . . . . . . 9
2 ifcl 3983 . . . . . . . . 9
31, 2mpan2 671 . . . . . . . 8
43ad2antrr 725 . . . . . . 7
5 simpll 753 . . . . . . 7
64, 5, 5add12d 9824 . . . . . 6
75, 4, 5addassd 9639 . . . . . 6
86, 7eqtr4d 2501 . . . . 5
9 pm5.501 341 . . . . . . . . 9
109adantl 466 . . . . . . . 8
1110bicomd 201 . . . . . . 7
1211ifbid 3963 . . . . . 6
13 simpr 461 . . . . . . . . 9
1413orcd 392 . . . . . . . 8
15 iftrue 3947 . . . . . . . 8
1614, 15syl 16 . . . . . . 7
1752timesd 10806 . . . . . . 7
1816, 17eqtrd 2498 . . . . . 6
1912, 18oveq12d 6314 . . . . 5
20 iftrue 3947 . . . . . . . 8
2120adantl 466 . . . . . . 7
2221oveq1d 6311 . . . . . 6
2322oveq1d 6311 . . . . 5
248, 19, 233eqtr4d 2508 . . . 4
25 iffalse 3950 . . . . . . . . 9
2625adantl 466 . . . . . . . 8
2726oveq1d 6311 . . . . . . 7
283ad2antrr 725 . . . . . . . 8
2928addid2d 9802 . . . . . . 7
3027, 29eqtrd 2498 . . . . . 6
3130oveq1d 6311 . . . . 5
32 2cnd 10633 . . . . . . . . . . . 12
33 id 22 . . . . . . . . . . . 12
3432, 33mulcld 9637 . . . . . . . . . . 11
3534addid2d 9802 . . . . . . . . . 10
36 2times 10679 . . . . . . . . . 10
3735, 36eqtrd 2498 . . . . . . . . 9
3837adantr 465 . . . . . . . 8
39 iftrue 3947 . . . . . . . . . 10
4039adantl 466 . . . . . . . . 9
41 iftrue 3947 . . . . . . . . . 10
4241adantl 466 . . . . . . . . 9
4340, 42oveq12d 6314 . . . . . . . 8
44 iftrue 3947 . . . . . . . . . 10
4544adantl 466 . . . . . . . . 9
4645oveq1d 6311 . . . . . . . 8
4738, 43, 463eqtr4d 2508 . . . . . . 7
48 simpl 457 . . . . . . . . 9
49 0cnd 9610 . . . . . . . . 9
5048, 49addcomd 9803 . . . . . . . 8
51 iffalse 3950 . . . . . . . . . 10
5251adantl 466 . . . . . . . . 9
53 iffalse 3950 . . . . . . . . . 10
5453adantl 466 . . . . . . . . 9
5552, 54oveq12d 6314 . . . . . . . 8
56 iffalse 3950 . . . . . . . . . 10
5756adantl 466 . . . . . . . . 9
5857oveq1d 6311 . . . . . . . 8
5950, 55, 583eqtr4d 2508 . . . . . . 7
6047, 59pm2.61dan 791 . . . . . 6
6160ad2antrr 725 . . . . 5
62 ifnot 3986 . . . . . . 7
63 nbn2 345 . . . . . . . . 9
6463adantl 466 . . . . . . . 8
6564ifbid 3963 . . . . . . 7
6662, 65syl5eqr 2512 . . . . . 6
67 biorf 405 . . . . . . . 8
6867adantl 466 . . . . . . 7
6968ifbid 3963 . . . . . 6
7066, 69oveq12d 6314 . . . . 5
7131, 61, 703eqtr2rd 2505 . . . 4
7224, 71pm2.61dan 791 . . 3
73 hadrot 1457 . . . . . . 7
74 had1 1470 . . . . . . 7
7573, 74syl5bbr 259 . . . . . 6
7675adantl 466 . . . . 5
7776ifbid 3963 . . . 4
78 cad1 1465 . . . . . 6
7978adantl 466 . . . . 5
8079ifbid 3963 . . . 4
8177, 80oveq12d 6314 . . 3
82 iftrue 3947 . . . . 5
8382adantl 466 . . . 4
8483oveq2d 6312 . . 3
8572, 81, 843eqtr4d 2508 . 2
8620adantl 466 . . . . . 6
8786oveq1d 6311 . . . . 5
8845oveq2d 6312 . . . . . . . 8
8938, 43, 883eqtr4d 2508 . . . . . . 7
9054, 57eqtr4d 2501 . . . . . . . 8
9152, 90oveq12d 6314 . . . . . . 7
9289, 91pm2.61dan 791 . . . . . 6
9392ad2antrr 725 . . . . 5
949adantl 466 . . . . . . . . . 10
9594notbid 294 . . . . . . . . 9
96 df-xor 1364 . . . . . . . . 9
9795, 96syl6bbr 263 . . . . . . . 8
9897ifbid 3963 . . . . . . 7
9962, 98syl5eqr 2512 . . . . . 6
100 ibar 504 . . . . . . . 8
101100adantl 466 . . . . . . 7
102101ifbid 3963 . . . . . 6
10399, 102oveq12d 6314 . . . . 5
10487, 93, 1033eqtr2rd 2505 . . . 4
105 simplll 759 . . . . . . 7
106 0cnd 9610 . . . . . . 7
107105, 106ifclda 3973 . . . . . 6
108 0cnd 9610 . . . . . 6
109107, 108addcomd 9803 . . . . 5
11063adantl 466 . . . . . . . . 9
111110con1bid 330 . . . . . . . 8
11296, 111syl5bb 257 . . . . . . 7
113112ifbid 3963 . . . . . 6
114 simpr 461 . . . . . . . 8
115114intnanrd 917 . . . . . . 7
116 iffalse 3950 . . . . . . 7
117115, 116syl 16 . . . . . 6
118113, 117oveq12d 6314 . . . . 5
11925adantl 466 . . . . . 6
120119oveq1d 6311 . . . . 5
121109, 118, 1203eqtr4d 2508 . . . 4
122104, 121pm2.61dan 791 . . 3
123 had0 1471 . . . . . . 7
12473, 123syl5bbr 259 . . . . . 6
125124adantl 466 . . . . 5
126125ifbid 3963 . . . 4
127 cad0 1467 . . . . . 6
128127adantl 466 . . . . 5
129128ifbid 3963 . . . 4
130126, 129oveq12d 6314 . . 3
131 iffalse 3950 . . . . 5
132131oveq2d 6312 . . . 4
133 ifcl 3983 . . . . . . 7
1341, 133mpan2 671 . . . . . 6
135134, 3addcld 9636 . . . . 5
136135addid1d 9801 . . . 4
137132, 136sylan9eqr 2520 . . 3
138122, 130, 1373eqtr4d 2508 . 2
13985, 138pm2.61dan 791 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369  \/_wxo 1363  =wceq 1395  haddwhad 1445  caddwcad 1446  e.wcel 1818  ifcif 3941  (class class class)co 6296   cc 9511  0cc0 9513   caddc 9516   cmul 9518  2c2 10610
This theorem is referenced by:  sadadd2lem  14109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-mulcom 9577  ax-addass 9578  ax-mulass 9579  ax-distr 9580  ax-i2m1 9581  ax-1ne0 9582  ax-1rid 9583  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586  ax-pre-lttri 9587  ax-pre-lttrn 9588  ax-pre-ltadd 9589
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-xor 1364  df-tru 1398  df-had 1447  df-cad 1448  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-po 4805  df-so 4806  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6299  df-er 7330  df-en 7537  df-dom 7538  df-sdom 7539  df-pnf 9651  df-mnf 9652  df-ltxr 9654  df-2 10619
  Copyright terms: Public domain W3C validator