API tools faq
paste
Advertisement
Guest User

Area of a box in R2 METAMATH

a guest
Mar 18th, 2019
126
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 12.28 KB | None | 0 0
raw download clone embed print report
  1. $( <MM> <PROOF_ASST> THEOREM=areabox LOC_AFTER=?
  2.  
  3. h50::areabox.1 |- S = ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) )
  4.  
  5. 51::1re |- 1 e. RR
  6. 52::ax1cn |- 1 e. CC
  7. 53:51:a1i |- ( x e. ( 0 [,] 1 ) -> 1 e. RR )
  8. 54::0re |- 0 e. RR
  9. 55::0cn |- 0 e. CC
  10. 56::0le1 |- 0 <_ 1
  11. 57::iccssre |- ( ( 0 e. RR /\ 1 e. RR ) -> ( 0 [,] 1 ) C_ RR )
  12. 58:54,51,57:mp2an |- ( 0 [,] 1 ) C_ RR
  13. 59::axresscn |- RR C_ CC
  14. 60:58,59:sstri |- ( 0 [,] 1 ) C_ CC
  15. 61::cncfmptc |- ( ( 1 e. CC /\ ( 0 [,] 1 ) C_ CC /\ CC C_ CC )
  16. -> ( x e. ( 0 [,] 1 ) |-> 1 ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
  17. 62::ssid |- CC C_ CC
  18. 63:52,60,62,61:mp3an |- ( x e. ( 0 [,] 1 ) |-> 1 ) e. ( ( 0 [,] 1 ) -cn-> CC )
  19. 64:62:a1i |- ( ph -> CC C_ CC )
  20.  
  21. 65::cniccibl |- ( ( 0 e. RR /\ 1 e. RR /\ ( x e. ( 0 [,] 1 ) |-> 1 ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
  22. -> ( x e. ( 0 [,] 1 ) |-> 1 ) e. L^1 )
  23. 66:54,51,63,65:mp3an |- ( x e. ( 0 [,] 1 ) |-> 1 ) e. L^1
  24.  
  25. *define area
  26. 67::areaval |- ( S e. dom area -> ( area ` S ) = S. RR ( vol ` ( S " { x } ) ) _d x )
  27. 68:50:imaeq1i |- ( S " { x } ) = ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } )
  28. 69::xpimasn |- ( x e. ( 0 [,] 1 ) -> ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) = ( 0 [,] 1 ) )
  29. 70::xpima1 |- ( ( ( 0 [,] 1 ) i^i { x } ) = (/) -> ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) = (/) )
  30. 71::disjsn |- ( ( ( 0 [,] 1 ) i^i { x } ) = (/) <-> -. x e. ( 0 [,] 1 ) )
  31. 72:71,70:sylbir |- ( -. x e. ( 0 [,] 1 ) -> ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) = (/) )
  32. 73::iftrue |- ( x e. ( 0 [,] 1 ) -> if ( x e. ( 0 [,] 1 ) , ( 0 [,] 1 ) , (/) ) = ( 0 [,] 1 ) )
  33. 74::iffalse |- ( -. x e. ( 0 [,] 1 ) -> if ( x e. ( 0 [,] 1 ) , ( 0 [,] 1 ) , (/) ) = (/) )
  34. 75:73,69:eqtr4d |- ( x e. ( 0 [,] 1 ) -> if ( x e. ( 0 [,] 1 ) , ( 0 [,] 1 ) , (/) ) = ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) )
  35. 76:74,72:eqtr4d |- ( -. x e. ( 0 [,] 1 ) -> if ( x e. ( 0 [,] 1 ) , ( 0 [,] 1 ) , (/) ) = ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) )
  36. 77:75,76:pm2.61i |- if ( x e. ( 0 [,] 1 ) , ( 0 [,] 1 ) , (/) ) = ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } )
  37. 78:68,77:eqtr4i |- ( S " { x } ) = if ( x e. ( 0 [,] 1 ) , ( 0 [,] 1 ) , (/) )
  38. 79:78:fveq2i |- ( vol ` ( S " { x } ) ) = ( vol ` if ( x e. ( 0 [,] 1 ) , ( 0 [,] 1 ) , (/) ) )
  39. 80:79:a1i |- ( x e. ( 0 [,] 1 ) -> ( vol ` ( S " { x } ) ) = ( vol ` if ( x e. ( 0 [,] 1 ) , ( 0 [,] 1 ) , (/) ) ) )
  40. 81:79:a1i |- ( -. x e. ( 0 [,] 1 ) -> ( vol ` ( S " { x } ) ) = ( vol ` if ( x e. ( 0 [,] 1 ) , ( 0 [,] 1 ) , (/) ) ) )
  41. 82:73:fveq2d |- ( x e. ( 0 [,] 1 )
  42. -> ( vol ` if ( x e. ( 0 [,] 1 ) , ( 0 [,] 1 ) , (/) ) ) = ( vol ` ( 0 [,] 1 ) ) )
  43. 83:74:fveq2d |- ( -. x e. ( 0 [,] 1 )
  44. -> ( vol ` if ( x e. ( 0 [,] 1 ) , ( 0 [,] 1 ) , (/) ) ) = ( vol ` (/) ) )
  45. 84:80,82:eqtrd |- ( x e. ( 0 [,] 1 ) -> ( vol ` ( S " { x } ) ) = ( vol ` ( 0 [,] 1 ) ) )
  46. 85:81,83:eqtrd |- ( -. x e. ( 0 [,] 1 ) -> ( vol ` ( S " { x } ) ) = ( vol ` (/) ) )
  47. *show S e. dom area
  48. 86::dmarea |- ( S e. dom area <-> ( S C_ ( RR X. RR )
  49. /\ A. x e. RR ( S " { x } ) e. ( `' vol " RR )
  50. /\ ( x e. RR |-> ( vol ` ( S " { x } ) ) ) e. L^1 ) )
  51.  
  52. *1. S C_ RR X. RR
  53. 87::xpss12 |- ( ( ( 0 [,] 1 ) C_ RR /\ ( 0 [,] 1 ) C_ RR ) -> ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) C_ ( RR X. RR ) )
  54. 88:58,58:pm3.2i |- ( ( 0 [,] 1 ) C_ RR /\ ( 0 [,] 1 ) C_ RR )
  55. 89:88,87:ax-mp |- ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) C_ ( RR X. RR )
  56. 90:50,89:eqsstri |- S C_ ( RR X. RR )
  57.  
  58. *2 S " {x} e. `' vol " RR
  59. 91::iccmbl |- ( ( 0 e. RR /\ 1 e. RR ) -> ( 0 [,] 1 ) e. dom vol )
  60. 92:54,51,91:mp2an |- ( 0 [,] 1 ) e. dom vol
  61. 93::0mbl |- (/) e. dom vol
  62. 94::ifcl |- ( ( ( 0 [,] 1 ) e. dom vol /\ (/) e. dom vol )
  63. -> if ( x e. ( 0 [,] 1 ) , ( 0 [,] 1 ) , (/) ) e. dom vol )
  64. 95:92,93,94:mp2an |- if ( x e. ( 0 [,] 1 ) , ( 0 [,] 1 ) , (/) ) e. dom vol
  65. 96:78,95:eqeltri |- ( S " { x } ) e. dom vol
  66. *63::cnvimass |- ( `' vol " RR ) C_ dom vol
  67. *64:: |- A. x e. RR ( S " { x } ) e. ( `' vol " RR )
  68. 97::fvimacnv |- ( ( Fun vol /\ ( S " { x } ) e. dom vol ) -> ( ( vol ` ( S " { x } ) ) e. RR <-> ( S " { x } ) e. ( `' vol " RR ) ) )
  69. 98::volf |- vol : dom vol --> ( 0 [,] +oo )
  70. 99::ffun |- ( vol : dom vol --> ( 0 [,] +oo ) -> Fun vol )
  71. 100:98,99:ax-mp |- Fun vol
  72. 101:100,96,97:mp2an |- ( ( vol ` ( S " { x } ) ) e. RR <-> ( S " { x } ) e. ( `' vol " RR ) )
  73. 102::ifcl |- ( ( 1 e. RR /\ 0 e. RR ) -> if ( x e. ( 0 [,] 1 ) , 1 , 0 ) e. RR )
  74. 103:51,54,102:mp2an |- if ( x e. ( 0 [,] 1 ) , 1 , 0 ) e. RR
  75. 104::itgconst |- ( ( ( 0 [,] 1 ) e. dom vol /\ ( vol ` ( 0 [,] 1 ) ) e. RR /\ 1 e. CC )
  76. -> S. ( 0 [,] 1 ) 1 _d x = ( 1 x. ( vol ` ( 0 [,] 1 ) ) ) )
  77.  
  78. *find the value of area
  79. 105::itgss2 |- ( ( 0 [,] 1 ) C_ RR -> S. ( 0 [,] 1 ) 1 _d x
  80. = S. RR if ( x e. ( 0 [,] 1 ) , 1 , 0 ) _d x )
  81. 106::unitssre |- ( 0 [,] 1 ) C_ RR
  82. 107:106,105:ax-mp |- S. ( 0 [,] 1 ) 1 _d x = S. RR if ( x e. ( 0 [,] 1 ) , 1 , 0 ) _d x
  83. 108::ovolicc |- ( ( 0 e. RR /\ 1 e. RR /\ 0 <_ 1 ) -> ( vol* ` ( 0 [,] 1 ) ) = ( 1 - 0 ) )
  84. 109:54,51,56,108:mp3an |- ( vol* ` ( 0 [,] 1 ) ) = ( 1 - 0 )
  85. 110::mblvol |- ( ( 0 [,] 1 ) e. dom vol -> ( vol ` ( 0 [,] 1 ) ) = ( vol* ` ( 0 [,] 1 ) ) )
  86. 111:92,110:ax-mp |- ( vol ` ( 0 [,] 1 ) ) = ( vol* ` ( 0 [,] 1 ) )
  87. 112:111,109:eqtri |- ( vol ` ( 0 [,] 1 ) ) = ( 1 - 0 )
  88. 113::1m0e1 |- ( 1 - 0 ) = 1
  89. 114:112,113:eqtri |- ( vol ` ( 0 [,] 1 ) ) = 1
  90. 115:84,114:syl6eq |- ( x e. ( 0 [,] 1 ) -> ( vol ` ( S " { x } ) ) = 1 )
  91. 116:115,53:eqeltrd |- ( x e. ( 0 [,] 1 ) -> ( vol ` ( S " { x } ) ) e. RR )
  92. 117:114:oveq2i |- ( 1 x. ( vol ` ( 0 [,] 1 ) ) ) = ( 1 x. 1 )
  93. 118:114,51:eqeltri |- ( vol ` ( 0 [,] 1 ) ) e. RR
  94. 119:92,118,52,104:mp3an |- S. ( 0 [,] 1 ) 1 _d x = ( 1 x. ( vol ` ( 0 [,] 1 ) ) )
  95. 120:119,117:eqtri |- S. ( 0 [,] 1 ) 1 _d x = ( 1 x. 1 )
  96. 121::1t1e1 |- ( 1 x. 1 ) = 1
  97. 122:120,121:eqtri |- S. ( 0 [,] 1 ) 1 _d x = 1
  98. 123:122,107:eqtr3i |- 1 = S. RR if ( x e. ( 0 [,] 1 ) , 1 , 0 ) _d x
  99. 124:123:eqcomi |- S. RR if ( x e. ( 0 [,] 1 ) , 1 , 0 ) _d x = 1
  100.  
  101. *show this area is the same as S
  102. 125::xpimasn |- ( x e. ( 0 [,] 1 ) -> ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) = ( 0 [,] 1 ) )
  103. 126::xpima1 |- ( ( ( 0 [,] 1 ) i^i { x } ) = (/) -> ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) = (/) )
  104. 127::disjsn |- ( ( ( 0 [,] 1 ) i^i { x } ) = (/) <-> -. x e. ( 0 [,] 1 ) )
  105. 128:127,126:sylbir |- ( -. x e. ( 0 [,] 1 ) -> ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) = (/) )
  106. 129::ovol0 |- ( vol* ` (/) ) = 0
  107. 130::mblvol |- ( (/) e. dom vol -> ( vol ` (/) ) = ( vol* ` (/) ) )
  108. 131::0mbl |- (/) e. dom vol
  109. 132:131,130:ax-mp |- ( vol ` (/) ) = ( vol* ` (/) )
  110. 133:132,129:eqtri |- ( vol ` (/) ) = 0
  111. 134:133:a1i |- ( -. x e. ( 0 [,] 1 ) -> ( vol ` (/) ) = 0 )
  112. 135:85,134:eqtrd |- ( -. x e. ( 0 [,] 1 ) -> ( vol ` ( S " { x } ) ) = 0 )
  113. 136:125:fveq2d |- ( x e. ( 0 [,] 1 ) -> ( vol ` ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) ) = ( vol ` ( 0 [,] 1 ) ) )
  114. 137:136:idi |- ( x e. ( 0 [,] 1 ) -> ( vol ` ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) ) = ( vol ` ( 0 [,] 1 ) ) )
  115. 138:128:fveq2d |- ( -. x e. ( 0 [,] 1 ) -> ( vol ` ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) ) = ( vol ` (/) ) )
  116. 139:137,114:syl6req |- ( x e. ( 0 [,] 1 ) -> 1 = ( vol ` ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) ) )
  117. 140:138,133:syl6req |- ( -. x e. ( 0 [,] 1 ) -> 0 = ( vol ` ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) ) )
  118. 141:139:adantl |- ( ( x e. RR /\ x e. ( 0 [,] 1 ) ) -> 1 = ( vol ` ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) ) )
  119. 142:140:adantl |- ( ( x e. RR /\ -. x e. ( 0 [,] 1 ) ) -> 0 = ( vol ` ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) ) )
  120. 143:141,142:ifeqda |- ( x e. RR -> if ( x e. ( 0 [,] 1 ) , 1 , 0 ) = ( vol ` ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) ) )
  121.  
  122. 144:68:fveq2i |- ( vol ` ( S " { x } ) ) = ( vol ` ( ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) " { x } ) )
  123. 145:143,144:syl6reqr |- ( x e. RR -> ( vol ` ( S " { x } ) ) = if ( x e. ( 0 [,] 1 ) , 1 , 0 ) )
  124. 146:145,103:syl6eqel |- ( x e. RR -> ( vol ` ( S " { x } ) ) e. RR )
  125. 147:146,101:sylib |- ( x e. RR -> ( S " { x } ) e. ( `' vol " RR ) )
  126. 148:147:rgen |- A. x e. RR ( S " { x } ) e. ( `' vol " RR )
  127.  
  128.  
  129. 149:145:rgen |- A. x e. RR ( vol ` ( S " { x } ) ) = if ( x e. ( 0 [,] 1 ) , 1 , 0 )
  130. 150::itgeq2 |- ( A. x e. RR ( vol ` ( S " { x } ) ) = if ( x e. ( 0 [,] 1 ) , 1 , 0 )
  131. -> S. RR ( vol ` ( S " { x } ) ) _d x = S. RR if ( x e. ( 0 [,] 1 ) , 1 , 0 ) _d x )
  132. 151:149,150:ax-mp |- S. RR ( vol ` ( S " { x } ) ) _d x = S. RR if ( x e. ( 0 [,] 1 ) , 1 , 0 ) _d x
  133.  
  134. 152::iblconst |- ( ( ( 0 [,] 1 ) e. dom vol
  135. /\ ( vol ` ( 0 [,] 1 ) ) e. RR
  136. /\ 1 e. CC )
  137. -> ( ( 0 [,] 1 ) X. { 1 } ) e. L^1 )
  138. 153::rembl |- RR e. dom vol
  139. 154::eldifn |- ( x e. ( RR \ ( 0 [,] 1 ) ) -> -. x e. ( 0 [,] 1 ) )
  140. 155:154,135:syl |- ( x e. ( RR \ ( 0 [,] 1 ) ) -> ( vol ` ( S " { x } ) ) = 0 )
  141. 156:115:mpteq2ia |- ( x e. ( 0 [,] 1 ) |-> ( vol ` ( S " { x } ) ) ) = ( x e. ( 0 [,] 1 ) |-> 1 )
  142. 157:156,66:eqeltri |- ( x e. ( 0 [,] 1 ) |-> ( vol ` ( S " { x } ) ) ) e. L^1
  143. *800:20a,d24,405d,d22,d26:iblss2
  144. |- ( x e. RR |-> ( vol ` ( S " { x } ) ) ) e. L^1
  145.  
  146. 158:58:a1i |- ( 0 e. RR -> ( 0 [,] 1 ) C_ RR )
  147. 159:153:a1i |- ( 0 e. RR -> RR e. dom vol )
  148. 160:116:adantl |- ( ( 0 e. RR /\ x e. ( 0 [,] 1 ) ) -> ( vol ` ( S " { x } ) ) e. RR )
  149. 161:155:adantl |- ( ( 0 e. RR /\ x e. ( RR \ ( 0 [,] 1 ) ) ) -> ( vol ` ( S " { x } ) ) = 0 )
  150. 162:157:a1i |- ( 0 e. RR -> ( x e. ( 0 [,] 1 ) |-> ( vol ` ( S " { x } ) ) ) e. L^1 )
  151. 163:158,159,160,161,162:iblss2
  152. |- ( 0 e. RR -> ( x e. RR |-> ( vol ` ( S " { x } ) ) ) e. L^1 )
  153. 164:54,163:ax-mp |- ( x e. RR |-> ( vol ` ( S " { x } ) ) ) e. L^1
  154.  
  155. 165:90,148,164:3pm3.2i |- ( S C_ ( RR X. RR )
  156. /\ A. x e. RR ( S " { x } ) e. ( `' vol " RR )
  157. /\ ( x e. RR |-> ( vol ` ( S " { x } ) ) ) e. L^1 )
  158. 166:165,86:mpbir |- S e. dom area
  159. 167:166,67:ax-mp |- ( area ` S ) = S. RR ( vol ` ( S " { x } ) ) _d x
  160.  
  161. 168:151,124:eqtri |- S. RR ( vol ` ( S " { x } ) ) _d x = 1
  162.  
  163. qed:167,168:eqtri |- ( area ` S ) = 1
  164.  
  165. $d S x
  166. $= ( vx cfv cr cvol c1 wcel wss cc0 co 0re 1re mp2an ax-mp eqtri c0
  167. wceq a1i cc carea csn cima citg cdm cxp ccnv wral cmpt cibl cicc
  168. cv w3a iccssre pm3.2i xpss12 eqsstri cif xpimasn fveq2d idi cmin
  169. wa covol iccmbl mblvol cle wbr 0le1 ovolicc mp3an syl6req adantl
  170. wi 1m0e1 wn cin disjsn xpima1 sylbir ovol0 ifeqda imaeq1i fveq2i
  171. 0mbl syl6reqr ifcl syl6eqel wfun wb cpnf volf ffun iftrue eqtr4d
  172. iffalse pm2.61i eqtr4i eqeltri fvimacnv sylib rembl eqtrd syl6eq
  173. rgen eqeltrd cdif eldifn syl mpteq2ia ccncf ax1cn axresscn sstri
  174. ssid cncfmptc cniccibl iblss2 3pm3.2i dmarea areaval itgeq2 cmul
  175. wf mpbir itgconst oveq2i 1t1e1 unitssre itgss2 eqtr3i eqcomi ) A
  176. UADZCEACULZUBZUCZFDZUDZGAUAUEHZYMYRRYSAEEUFZIZYPFUGEUCHZCEUHZCEY
  177. QUIUJHZUMUUAUUCUUDAJGUKKZUUEUFZYTBUUEEIZUUGVCUUFYTIUUGUUGJEHZGEH
  178. ZUUGLMJGUNNZUUJUOUUEEUUEEUPOUQUUBCEYNEHZYQEHZUUBUUKYQYNUUEHZGJUR
  179. ZEUUKUUNUUFYOUCZFDZYQUUKUUMGJUUPUUMGUUPRUUKUUMUUPUUEFDZGUUMUUPUU
  180. QRVNUUMUUOUUEFUUEUUEYNUSZUTVAUUQGJVBKZGUUQUUEVDDZUUSUUEFUEZHZUUQ
  181. UUTRUUHUUIUVBLMJGVENZUUEVFOUUHUUIJGVGVHUUTUUSRLMVIJGVJVKPVOPZVLV
  182. MUUMVPZJUUPRUUKUVEUUPQFDZJUVEUUOQFUVEUUEYOVQQRUUOQRUUEYNVRUUEUUE
  183. YOVSVTZUTUVFQVDDZJQUVAHZUVFUVHRWEQVFOWAPZVLVMWBYPUUOFAUUFYOBWCZW
  184. DWFZUUIUUHUUNEHMLUUMGJEWGNWHFWIZYPUVAHUULUUBWJUVAJWKUKKZFYDUVMWL
  185. UVAUVNFWMOYPUUMUUEQURZUVAYPUUOUVOUVKUUMUVOUUORUUMUVOUUEUUOUUMUUE
  186. QWNZUURWOUVEUVOQUUOUUMUUEQWPZUVGWOWQWRZUVBUVIUVOUVAHUVCWEUUMUUEQ
  187. UVAWGNWSYPEFWTNXAXEUUHUUDLUUHCUUEEYQEUUGUUHUUJSEUVAHUUHXBSUUMUUL
  188. UUHUUMYQGEUUMYQUUQGUUMYQUVOFDZUUQYQUVSRZUUMYPUVOFUVRWDZSUUMUVOUU
  189. EFUVPUTXCUVDXDZUUIUUMMSXFVMYNEUUEXGHZYQJRZUUHUWCUVEUWDYNEUUEXHUV
  190. EYQUVFJUVEYQUVSUVFUVTUVEUWASUVEUVOQFUVQUTXCUVFJRUVEUVJSXCXIVMCUU
  191. EYQUIZUJHUUHUWECUUEGUIZUJCUUEYQGUWBXJUUHUUIUWFUUETXKKHZUWFUJHLMG
  192. THZUUETITTIUWGXLUUEETUUJXMXNTXOCGUUETXPVKJGUWFXQVKWSSXROXSCAXTYE
  193. CAYAOYRCEUUNUDZGYQUUNRZCEUHYRUWIRUWJCEUVLXECEYQUUNYBOGUWICUUEGUD
  194. ZGUWIUWKGGYCKZGUWKGUUQYCKZUWLUVBUUQEHUWHUWKUWMRUVCUUQGEUVDMWSXLC
  195. UUEGYFVKUUQGGYCUVDYGPYHPUUGUWKUWIRYICUUEEGYJOYKYLPP $.
  196. $)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!