let nn, nn9, A, B, N be Nat; :: thesis: ( nn = (2 * nn9) + 1 & Fusc N = (A * (Fusc nn)) + (B * (Fusc (nn + 1))) implies Fusc N = (A * (Fusc nn9)) + ((B + A) * (Fusc (nn9 + 1))) )
assume that
A1: nn = (2 * nn9) + 1 and
A2: Fusc N = (A * (Fusc nn)) + (B * (Fusc (nn + 1))) ; :: thesis: Fusc N = (A * (Fusc nn9)) + ((B + A) * (Fusc (nn9 + 1)))
( nn + 1 = 2 * (nn9 + 1) & Fusc nn = (Fusc nn9) + (Fusc (nn9 + 1)) ) by A1, Th17;
hence Fusc N = ((A * (Fusc nn9)) + (A * (Fusc (nn9 + 1)))) + (B * (Fusc (nn9 + 1))) by A2, Th17
.= (A * (Fusc nn9)) + ((B + A) * (Fusc (nn9 + 1))) ;
:: thesis: verum