metamath/valid/mathd-algebra-96.mm

$(
  @{
    mathd-algebra-96.0 @e |- ( ph -> X e. RR+ ) $@
    mathd-algebra-96.1 @e |- ( ph -> Y e. RR+ ) $@
    mathd-algebra-96.2 @e |- ( ph -> Z e. RR+ ) $@
    mathd-algebra-96.3 @e |- ( ph -> A e. RR+ ) $@
    mathd-algebra-96.4 @e |- ( ph -> ( ( log ` X ) - ( log ` Y ) ) = A ) $@
    mathd-algebra-96.5 @e |- ( ph -> ( ( log ` Y ) - ( log ` Z ) ) = ; 1 5 ) $@
    mathd-algebra-96.6 @e |- ( ph -> ( ( log ` Z ) - ( log ` X ) ) = -u 7 ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-96 @p |- ( ph -> A = -u 8 ) @=
      ? @.
  @}
$)