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 9343 . . . . . 6
213anidm13 1242 . . . . 5
3 2times 10099 . . . . . 6
43adantr 452 . . . . 5
52, 4eqtr4d 2471 . . . 4
65oveq1d 6096 . . 3
7 addcl 9072 . . . 4
8 subcl 9305 . . . 4
9 2cn 10070 . . . . . 6
10 2ne0 10083 . . . . . 6
119, 10pm3.2i 442 . . . . 5
12 divdir 9701 . . . . 5
1311, 12mp3an3 1268 . . . 4
147, 8, 13syl2anc 643 . . 3
15 divcan3 9702 . . . . 5
169, 10, 15mp3an23 1271 . . . 4
186, 14, 173eqtr3d 2476 . 2
19 pnncan 9342 . . . . . 6
20193anidm23 1243 . . . . 5
21 2times 10099 . . . . . 6
2221adantl 453 . . . . 5
2320, 22eqtr4d 2471 . . . 4
2423oveq1d 6096 . . 3
25 divsubdir 9710 . . . . 5
2611, 25mp3an3 1268 . . . 4
277, 8, 26syl2anc 643 . . 3
28 divcan3 9702 . . . . 5
299, 10, 28mp3an23 1271 . . . 4