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

 Description: Sum and difference of half-sum and half-difference. (Contributed by Paul Chapman, 12-Oct-2007.)
Assertion
Ref Expression

StepHypRef Expression
1 ppncan 9880 . . . . . 6
213anidm13 1286 . . . . 5
3 2times 10675 . . . . . 6
43adantr 465 . . . . 5
52, 4eqtr4d 2501 . . . 4
65oveq1d 6311 . . 3
7 addcl 9591 . . . 4
8 subcl 9838 . . . 4
9 2cnne0 10771 . . . . 5
10 divdir 10251 . . . . 5
119, 10mp3an3 1313 . . . 4
127, 8, 11syl2anc 661 . . 3
13 2cn 10627 . . . . 5
14 2ne0 10649 . . . . 5
15 divcan3 10252 . . . . 5
1613, 14, 15mp3an23 1316 . . . 4
186, 12, 173eqtr3d 2506 . 2
19 pnncan 9879 . . . . . 6
20193anidm23 1287 . . . . 5
21 2times 10675 . . . . . 6
2221adantl 466 . . . . 5
2320, 22eqtr4d 2501 . . . 4
2423oveq1d 6311 . . 3
25 divsubdir 10261 . . . . 5
269, 25mp3an3 1313 . . . 4
277, 8, 26syl2anc 661 . . 3
28 divcan3 10252 . . . . 5
2913, 14, 28mp3an23 1316 . . . 4