Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  halfaddsub 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 7469 . . . . . 6
213anidm13 1228 . . . . 5
3 2times 8279 . . . . . 6
43adantr 270 . . . . 5
52, 4eqtr4d 2118 . . . 4
65oveq1d 5578 . . 3
7 addcl 7212 . . . 4
8 subcl 7426 . . . 4
9 2cn 8229 . . . . . 6
10 2ap0 8251 . . . . . 6 #
119, 10pm3.2i 266 . . . . 5 #
12 divdirap 7904 . . . . 5 #
1311, 12mp3an3 1258 . . . 4
147, 8, 13syl2anc 403 . . 3
15 divcanap3 7905 . . . . 5 #
169, 10, 15mp3an23 1261 . . . 4
186, 14, 173eqtr3d 2123 . 2
19 pnncan 7468 . . . . . 6
20193anidm23 1229 . . . . 5
21 2times 8279 . . . . . 6
2221adantl 271 . . . . 5
2320, 22eqtr4d 2118 . . . 4
2423oveq1d 5578 . . 3
25 divsubdirap 7915 . . . . 5 #
2611, 25mp3an3 1258 . . . 4
277, 8, 26syl2anc 403 . . 3
28 divcanap3 7905 . . . . 5 #
299, 10, 28mp3an23 1261 . . . 4