关于Java BigDecimal中精确十进制除法最大小数位数计算公式的推导问询

大家好，我最近在琢磨一个问题：精确做十进制除法的时候，最多需要多少位小数才能得到准确结果？研究Java的BigDecimal实现时，发现它的注释和代码里有个相关的计算公式，但我搞不懂它是怎么来的，想请教下各位大佬。

先跟大家说下背景：BigDecimal里提到，如果被除数除以除数的商是有限小数，那这个小数的位数不会超过 (a.precision() + ceil(10*b.precision/3))（注：原源码注释里有个括号写错了，正确的应该是这样，代码里的实现是对的）。

这里得先明确下precision的定义：按照浮点数表示的标准（比如IEEE 754-2008），它指的是把一个有限小数写成十进制科学计数法 s * 10^e 时，有效数字（significand/coefficient/mantissa）s的位数——而且这个s是经过归一化的，去掉了所有前导和后导零。

给大家看下相关的源码片段：

/*
* If the quotient this/divisor has a terminating decimal
* expansion, the expansion can have no more than
* (a.precision() + ceil(10*b.precision)/3) digits.
* Therefore, create a MathContext object with this
* precision and do a divide with the UNNECESSARY rounding
* mode.
*/
MathContext mc = new MathContext( (int)Math.min(this.precision() +
(long)Math.ceil(10.0*divisor.precision()/3.0),
Integer.MAX_VALUE),
RoundingMode.UNNECESSARY);
BigDecimal quotient;
try {
quotient = this.divide(divisor, mc);
} catch (ArithmeticException e) {
throw new ArithmeticException("Non-terminating decimal expansion; " +
"no exact representable decimal result.");
}

我之前在相关问题的回答里看到有人提到过这个BigDecimal的公式，但完全没解释它的推导过程。所以想问问大家：这个计算精确十进制除法最大小数位数的公式，到底是怎么推导出来的？

备注：内容来源于stack exchange，提问作者MTH