Step
*
of Lemma
rpositive-rmax
∀x,y:ℝ.  (rpositive(rmax(x;y)) 
⇐⇒ rpositive(x) ∨ rpositive(y))
BY
{ Auto }
1
1. x : ℝ@i
2. y : ℝ@i
3. rpositive(rmax(x;y))@i
⊢ rpositive(x) ∨ rpositive(y)
2
1. x : ℝ@i
2. y : ℝ@i
3. rpositive(x) ∨ rpositive(y)@i
⊢ rpositive(rmax(x;y))
Latex:
Latex:
\mforall{}x,y:\mBbbR{}.    (rpositive(rmax(x;y))  \mLeftarrow{}{}\mRightarrow{}  rpositive(x)  \mvee{}  rpositive(y))
By
Latex:
Auto
Home
Index