>>679
乗法に関する逆元なんだから定義より当たり前だろ
それとも別の公理系を考えるのか？

>>680
あ、そこ証明必要だったか

まず、指数関数を対数関数の逆関数と定義する。
ちなみに対数関数は t^(-1) の [1,x] の不定積分として定義。

指数関数
y = e^x
を考えると、
x = log(y)
ここで、s = e^u, t = e^v として対数関数の加法定理より
u + v = log(s) + log(t) = log(st)
よって、e^(u + v) = st = (e^u)*(e^v).
次に、対数関数の加法定理の証明。
f(x) = log(xy) - log(x)
っていう関数を考える。任意なy>0を固定してxで微分すると
f'(x) = y/xy - 1/x = 0.
よってf(x)は定数で
f(x) = f(1) = log(y).
故に log(y) + log(x) = log(xy).

微分積分の定義されている前提なら、こんな感じかな
ただ、実数の連続性とかからやろうとするとだるい