let b, i be Nat; :: thesis: ( b >= 1 implies (powerfact b) . i <= ((1 / b) GeoSeq) . i )
assume A1: b >= 1 ; :: thesis: (powerfact b) . i <= ((1 / b) GeoSeq) . i
A3: (powerfact b) . i = 1 / (b to_power (i !)) by DefPower;
A2: ((1 / b) GeoSeq) . i = (1 / b) |^ i by PREPOWER:def 1
.= 1 / (b to_power i) by PREPOWER:7 ;
1 * (b to_power i) <= 1 * (b to_power (i !)) by A1, PRE_FF:8, NEWTON:38;
hence (powerfact b) . i <= ((1 / b) GeoSeq) . i by A2, A3, A1, XREAL_1:102; :: thesis: verum