proposition: Lemma binomial : forall (x y:R) (n:nat), (x + y) ^ n = sum_f_R0 (fun i:nat => C n i * x ^ i * y ^ (n - i)) n.
proof: Proof. intros; induction n as [| n Hrecn]. - unfold C; simpl; unfold Rdiv; repeat rewrite Rmult_1_r; rewrite Rinv_1; ring. - pattern (S n) at 1; replace (S n) with (n + 1)%nat; [ idtac | ring ]. rewrite pow_add; rewrite Hrecn. replace ((x + y) ^ 1) with (x + y); [ idtac | simpl; ring ]. rewrite tech5. cut (forall p:nat, C p p = 1). 1:cut (forall p:nat, C p 0 = 1). + intros; rewrite H0; rewrite Nat.sub_diag; rewrite Rmult_1_l. replace (y ^ 0) with 1; [ rewrite Rmult_1_r | simpl; reflexivity ]. induction n as [| n Hrecn0]. * simpl; do 2 rewrite H; ring. * set (N := S n). rewrite Rmult_plus_distr_l. replace (sum_f_R0 (fun i:nat => C N i * x ^ i * y ^ (N - i)) N * x) with (sum_f_R0 (fun i:nat => C N i * x ^ S i * y ^ (N - i)) N). 1: replace (sum_f_R0 (fun i:nat => C N i * x ^ i * y ^ (N - i)) N * y) with (sum_f_R0 (fun i:nat => C N i * x ^ i * y ^ (S N - i)) N). -- rewrite (decomp_sum (fun i:nat => C (S N) i * x ^ i * y ^ (S N - i)) N). ++ rewrite H; replace (x ^ 0) with 1; [ idtac | reflexivity ]. do 2 rewrite Rmult_1_l. replace (S N - 0)%nat with (S N); [ idtac | reflexivity ]. set (An := fun i:nat => C N i * x ^ S i * y ^ (N - i)). set (Bn := fun i:nat => C N (S i) * x ^ S i * y ^ (N - i)). replace (pred N) with n. 1:replace (sum_f_R0 (fun i:nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) n) with (sum_f_R0 (fun i:nat => An i + Bn i) n). ** rewrite plus_sum. replace (x ^ S N) with (An (S n)). { rewrite (Rplus_comm (sum_f_R0 An n)). repeat rewrite Rplus_assoc. rewrite <- tech5. fold N. set (Cn := fun i:nat => C N i * x ^ i * y ^ (S N - i)). cut (forall i:nat, (i < N)%nat -> Cn (S i) = Bn i). - intro; replace (sum_f_R0 Bn n) with (sum_f_R0 (fun i:nat => Cn (S i)) n). + replace (y ^ S N) with (Cn 0%nat). * rewrite <- Rplus_assoc; rewrite (decomp_sum Cn N). -- replace (pred N) with n. ++ ring. ++ unfold N; simpl; reflexivity. -- unfold N; apply Nat.lt_0_succ. * unfold Cn; rewrite H; simpl; ring. + apply sum_eq. intros; apply H1. unfold N; apply Nat.le_lt_trans with n; [ assumption | apply Nat.lt_succ_diag_r ]. - reflexivity. } unfold An; fold N; rewrite Nat.sub_diag; rewrite H0; simpl; ring. ** apply sum_eq. intros; unfold An, Bn. change (S N - S i)%nat with (N - i)%nat. rewrite <- pascal; [ ring | apply Nat.le_lt_trans with n; [ assumption | unfold N; apply Nat.lt_succ_diag_r ] ]. ** unfold N; reflexivity. ++ unfold N; apply Nat.lt_0_succ. -- rewrite <- (Rmult_comm y); rewrite scal_sum; apply sum_eq. intros; replace (S N - i)%nat with (S (N - i)). ++ replace (S (N - i)) with (N - i + 1)%nat; [ idtac | ring ]. rewrite pow_add; replace (y ^ 1) with y; [ idtac | simpl; ring ]; ring. ++ symmetry; apply Nat.sub_succ_l; assumption. -- rewrite <- (Rmult_comm x); rewrite scal_sum; apply sum_eq. intros; replace (S i) with (i + 1)%nat; [ idtac | ring ]; rewrite pow_add; replace (x ^ 1) with x; [ idtac | simpl; ring ]; ring. + intro; unfold C. replace (INR (fact 0)) with 1; [ idtac | reflexivity ]. replace (p - 0)%nat with p; [ idtac | symmetry; apply Nat.sub_0_r ]. rewrite Rmult_1_l; unfold Rdiv; rewrite Rinv_r; [ reflexivity | apply INR_fact_neq_0 ]. + intro; unfold C. replace (p - p)%nat with 0%nat; [ idtac | symmetry; apply Nat.sub_diag ]. replace (INR (fact 0)) with 1; [ idtac | reflexivity ]. rewrite Rmult_1_r; unfold Rdiv; rewrite Rinv_r; [ reflexivity | apply INR_fact_neq_0 ]. Qed.
imports: Rbase Rfunctions PartSum