Step * of Lemma mon_ident_q

No Annotations
[a:ℚ]. (((a 0) a ∈ ℚ) ∧ ((0 a) a ∈ ℚ))
BY
(ProveSpecializedLemmaWReduce mon_ident) [⌜parm{i}⌝; ⌜<ℚ+>⌝]⋅ }


Latex:


Latex:
No  Annotations
\mforall{}[a:\mBbbQ{}].  (((a  +  0)  =  a)  \mwedge{}  ((0  +  a)  =  a))


By


Latex:
(ProveSpecializedLemmaWReduce  mon\_ident)  0  [\mkleeneopen{}parm\{i\}\mkleeneclose{};  \mkleeneopen{}<\mBbbQ{}+>\mkleeneclose{}]\mcdot{}




Home Index