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