helm/software/matita/contribs/procedural/CoRN/transc/InvTrigonom.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "CoRN.ma".
  18
  19 (* $Id: InvTrigonom.v,v 1.9 2004/04/23 10:01:07 lcf Exp $ *)
  20
  21 include "transc/RealPowers.ma".
  22
  23 include "transc/TrigMon.ma".
  24
  25 include "ftc/StrongIVT.ma".
  26
  27 (*#* printing ArcSin %\ensuremath{\arcsin}% *)
  28
  29 (*#* printing ArcCos %\ensuremath{\arccos}% *)
  30
  31 (*#* printing ArcTan %\ensuremath{\arctan}% *)
  32
  33 (*#* *Inverse Trigonometric Functions
  34
  35 **Definitions
  36
  37 We will now define arcsine, arccosine and arctangent as indefinite
  38 integrals and prove their main properties.  We begin by proving that
  39 the appropriate indefinite integrals can be defined, then prove the
  40 main properties of the function.
  41
  42 Arccosine is defined in terms of arcsine by the relation
  43 [ArcCos(x)=Pi[/]Two-ArcSin(x)].
  44
  45 ***Arcsine
  46 *)
  47
  48 (* UNEXPORTED
  49 Opaque Sine Cosine Expon Logarithm.
  50 *)
  51
  52 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcSin_def_lemma.con" as lemma.
  53
  54 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcSin_def_zero.con" as lemma.
  55
  56 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcSin.con" as definition.
  57
  58 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcSin_domain.con" as lemma.
  59
  60 inline procedural "cic:/CoRN/transc/InvTrigonom/Continuous_ArcSin.con" as lemma.
  61
  62 inline procedural "cic:/CoRN/transc/InvTrigonom/Derivative_ArcSin.con" as lemma.
  63
  64 (* UNEXPORTED
  65 Hint Resolve Derivative_ArcSin: derivate.
  66 *)
  67
  68 (* UNEXPORTED
  69 Hint Resolve Continuous_ArcSin: continuous.
  70 *)
  71
  72 (*#* ***Arccosine
  73 *)
  74
  75 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcCos.con" as definition.
  76
  77 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcCos_domain.con" as lemma.
  78
  79 inline procedural "cic:/CoRN/transc/InvTrigonom/Continuous_ArcCos.con" as lemma.
  80
  81 inline procedural "cic:/CoRN/transc/InvTrigonom/Derivative_ArcCos.con" as lemma.
  82
  83 (*#* ***Arctangent
  84 *)
  85
  86 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcTan_def_lemma.con" as lemma.
  87
  88 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcTang.con" as definition.
  89
  90 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcTan_domain.con" as lemma.
  91
  92 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcTan.con" as definition.
  93
  94 inline procedural "cic:/CoRN/transc/InvTrigonom/Continuous_ArcTan.con" as lemma.
  95
  96 inline procedural "cic:/CoRN/transc/InvTrigonom/Derivative_ArcTan.con" as lemma.
  97
  98 (* UNEXPORTED
  99 Hint Resolve Derivative_ArcCos Derivative_ArcTan: derivate.
 100 *)
 101
 102 (* UNEXPORTED
 103 Hint Resolve Continuous_ArcCos Continuous_ArcTan: continuous.
 104 *)
 105
 106 (* UNEXPORTED
 107 Section Inverses
 108 *)
 109
 110 (*#* **Composition properties
 111
 112 We now prove that this functions are in fact inverses to the corresponding trigonometric functions.
 113
 114 ***Sine and Arcsine
 115 *)
 116
 117 inline procedural "cic:/CoRN/transc/InvTrigonom/maps_Sin.con" as lemma.
 118
 119 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcSin_Sin_inv.con" as lemma.
 120
 121 (* UNEXPORTED
 122 Opaque ArcSin.
 123 *)
 124
 125 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcSin_Sin.con" as lemma.
 126
 127 (* UNEXPORTED
 128 Transparent ArcSin.
 129 *)
 130
 131 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcSin_range.con" as lemma.
 132
 133 (* UNEXPORTED
 134 Transparent ArcSin.
 135 *)
 136
 137 inline procedural "cic:/CoRN/transc/InvTrigonom/Sin_ArcSin.con" as lemma.
 138
 139 inline procedural "cic:/CoRN/transc/InvTrigonom/Sin_ArcSin_inv.con" as lemma.
 140
 141 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcSin_resp_leEq.con" as lemma.
 142
 143 (*#* ***Cosine and Arcosine
 144 *)
 145
 146 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcCos_Cos.con" as lemma.
 147
 148 inline procedural "cic:/CoRN/transc/InvTrigonom/Cos_ArcCos.con" as lemma.
 149
 150 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcCos_Cos_inv.con" as lemma.
 151
 152 inline procedural "cic:/CoRN/transc/InvTrigonom/Cos_ArcCos_inv.con" as lemma.
 153
 154 (* UNEXPORTED
 155 Opaque ArcSin.
 156 *)
 157
 158 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcCos_resp_leEq.con" as lemma.
 159
 160 (*#* ***Tangent and Arctangent
 161 *)
 162
 163 inline procedural "cic:/CoRN/transc/InvTrigonom/maps_Tan.con" as lemma.
 164
 165 (* UNEXPORTED
 166 Opaque Tang.
 167 *)
 168
 169 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcTan_Tan_inv.con" as lemma.
 170
 171 (* UNEXPORTED
 172 Transparent Tang.
 173 *)
 174
 175 (* UNEXPORTED
 176 Opaque ArcTang.
 177 *)
 178
 179 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcTan_Tan.con" as lemma.
 180
 181 (* UNEXPORTED
 182 Opaque iprop.
 183 *)
 184
 185 (* UNEXPORTED
 186 Transparent iprop.
 187 *)
 188
 189 (* UNEXPORTED
 190 Opaque Cos.
 191 *)
 192
 193 inline procedural "cic:/CoRN/transc/InvTrigonom/Tan_ilim.con" as lemma.
 194
 195 (* UNEXPORTED
 196 Opaque Min.
 197 *)
 198
 199 (* UNEXPORTED
 200 Transparent Cos.
 201 *)
 202
 203 (* UNEXPORTED
 204 Section ArcTan_Range
 205 *)
 206
 207 (* UNEXPORTED
 208 cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/x.var
 209 *)
 210
 211 (* begin hide *)
 212
 213 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min.con" "Inverses__ArcTan_Range__" as definition.
 214
 215 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max.con" "Inverses__ArcTan_Range__" as definition.
 216
 217 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min1.con" "Inverses__ArcTan_Range__" as definition.
 218
 219 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min2.con" "Inverses__ArcTan_Range__" as definition.
 220
 221 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min3.con" "Inverses__ArcTan_Range__" as definition.
 222
 223 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min4.con" "Inverses__ArcTan_Range__" as definition.
 224
 225 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max1.con" "Inverses__ArcTan_Range__" as definition.
 226
 227 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max2.con" "Inverses__ArcTan_Range__" as definition.
 228
 229 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max3.con" "Inverses__ArcTan_Range__" as definition.
 230
 231 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max4.con" "Inverses__ArcTan_Range__" as definition.
 232
 233 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min5.con" "Inverses__ArcTan_Range__" as definition.
 234
 235 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/min6.con" "Inverses__ArcTan_Range__" as definition.
 236
 237 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max5.con" "Inverses__ArcTan_Range__" as definition.
 238
 239 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/max6.con" "Inverses__ArcTan_Range__" as definition.
 240
 241 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a.con" "Inverses__ArcTan_Range__" as definition.
 242
 243 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a1.con" "Inverses__ArcTan_Range__" as definition.
 244
 245 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a2.con" "Inverses__ArcTan_Range__" as definition.
 246
 247 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a3.con" "Inverses__ArcTan_Range__" as definition.
 248
 249 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a4.con" "Inverses__ArcTan_Range__" as definition.
 250
 251 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/a5.con" "Inverses__ArcTan_Range__" as definition.
 252
 253 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b.con" "Inverses__ArcTan_Range__" as definition.
 254
 255 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b1.con" "Inverses__ArcTan_Range__" as definition.
 256
 257 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b2.con" "Inverses__ArcTan_Range__" as definition.
 258
 259 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b3.con" "Inverses__ArcTan_Range__" as definition.
 260
 261 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b4.con" "Inverses__ArcTan_Range__" as definition.
 262
 263 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/b5.con" "Inverses__ArcTan_Range__" as definition.
 264
 265 inline procedural "cic:/CoRN/transc/InvTrigonom/Inverses/ArcTan_Range/ab.con" "Inverses__ArcTan_Range__" as definition.
 266
 267 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcTan_range_lemma.con" as lemma.
 268
 269 (* end hide *)
 270
 271 (* UNEXPORTED
 272 Transparent ArcTang.
 273 *)
 274
 275 inline procedural "cic:/CoRN/transc/InvTrigonom/ArcTan_range.con" as lemma.
 276
 277 (* UNEXPORTED
 278 End ArcTan_Range
 279 *)
 280
 281 (* UNEXPORTED
 282 Transparent ArcTang.
 283 *)
 284
 285 inline procedural "cic:/CoRN/transc/InvTrigonom/Tan_ArcTan.con" as lemma.
 286
 287 (* UNEXPORTED
 288 Opaque ArcTang.
 289 *)
 290
 291 inline procedural "cic:/CoRN/transc/InvTrigonom/Tan_ArcTan_inv.con" as lemma.
 292
 293 (* UNEXPORTED
 294 End Inverses
 295 *)
 296