toReal_zero

formal source

 133instance : LE LogicReal := ⟨fun x y => toReal x ≤ toReal y⟩
 134instance : LT LogicReal := ⟨fun x y => toReal x < toReal y⟩
 135
 136@[simp] theorem toReal_zero : toReal (0 : LogicReal) = 0 := toReal_fromReal 0
 137@[simp] theorem toReal_one : toReal (1 : LogicReal) = 1 := toReal_fromReal 1
 138@[simp] theorem toReal_add (x y : LogicReal) : toReal (x + y) = toReal x + toReal y :=
 139  toReal_fromReal _
 140@[simp] theorem toReal_neg (x : LogicReal) : toReal (-x) = -toReal x :=
 141  toReal_fromReal _
 142@[simp] theorem toReal_sub (x y : LogicReal) : toReal (x - y) = toReal x - toReal y :=
 143  toReal_fromReal _
 144@[simp] theorem toReal_mul (x y : LogicReal) : toReal (x * y) = toReal x * toReal y :=
 145  toReal_fromReal _
 146@[simp] theorem toReal_inv (x : LogicReal) : toReal x⁻¹ = (toReal x)⁻¹ :=
 147  toReal_fromReal _
 148@[simp] theorem toReal_div (x y : LogicReal) : toReal (x / y) = toReal x / toReal y :=
 149  toReal_fromReal _
 150
 151theorem le_iff_toReal_le {x y : LogicReal} : x ≤ y ↔ toReal x ≤ toReal y := Iff.rfl
 152theorem lt_iff_toReal_lt {x y : LogicReal} : x < y ↔ toReal x < toReal y := Iff.rfl
 153
 154theorem add_assoc' (x y z : LogicReal) : (x + y) + z = x + (y + z) := by
 155  rw [eq_iff_toReal_eq]
 156  simp
 157  ring
 158
 159theorem add_comm' (x y : LogicReal) : x + y = y + x := by
 160  rw [eq_iff_toReal_eq]
 161  simp
 162  ring
 163
 164theorem zero_add' (x : LogicReal) : (0 : LogicReal) + x = x := by
 165  rw [eq_iff_toReal_eq]
 166  simp