---

Step * of Lemma rcos-rabs

∀x:ℝ. (rcos(|x|) = rcos(x))
BY
{ (Auto THEN (StableCases ⌜x < r0⌝⋅ THENA Auto)) }

1
1. x : ℝ
2. x < r0
⊢ rcos(|x|) = rcos(x)

2
1. x : ℝ
2. ¬(x < r0)
⊢ rcos(|x|) = rcos(x)

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  (rcos(|x|)  =  rcos(x))


By

---

Latex:
(Auto  THEN  (StableCases  \mkleeneopen{}x  <  r0\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index