add

formal source

  71lemma one (φ : ℝ) : PhiClosed φ (1 : ℝ) :=
  72  (phiSubfield φ).one_mem
  73
  74lemma add (hx : PhiClosed φ x) (hy : PhiClosed φ y) :
  75    PhiClosed φ (x + y) :=
  76  (phiSubfield φ).add_mem hx hy
  77
  78lemma sub (hx : PhiClosed φ x) (hy : PhiClosed φ y) :
  79    PhiClosed φ (x - y) :=
  80  (phiSubfield φ).sub_mem hx hy
  81
  82lemma neg (hx : PhiClosed φ x) : PhiClosed φ (-x) :=
  83  (phiSubfield φ).neg_mem hx
  84
  85lemma mul (hx : PhiClosed φ x) (hy : PhiClosed φ y) :
  86    PhiClosed φ (x * y) :=
  87  (phiSubfield φ).mul_mem hx hy
  88
  89lemma inv (hx : PhiClosed φ x) : PhiClosed φ x⁻¹ :=
  90  (phiSubfield φ).inv_mem hx
  91
  92lemma div (hx : PhiClosed φ x) (hy : PhiClosed φ y) :
  93    PhiClosed φ (x / y) :=
  94  (phiSubfield φ).div_mem hx hy
  95
  96lemma pow (hx : PhiClosed φ x) (n : ℕ) : PhiClosed φ (x ^ n) := by
  97  simpa using (phiSubfield φ).pow_mem hx n
  98
  99lemma pow_self (φ : ℝ) (n : ℕ) : PhiClosed φ (φ ^ n) :=
 100  pow (self φ) n
 101
 102lemma inv_self (φ : ℝ) : PhiClosed φ (φ⁻¹) :=
 103  inv (self φ)
 104