equal
deleted
inserted
replaced
73 text {* \medskip @{term funprod} and @{term funsum} *} |
73 text {* \medskip @{term funprod} and @{term funsum} *} |
74 |
74 |
75 lemma funprod_pos: "(\<forall>i. i \<le> n --> 0 < mf i) ==> 0 < funprod mf 0 n" |
75 lemma funprod_pos: "(\<forall>i. i \<le> n --> 0 < mf i) ==> 0 < funprod mf 0 n" |
76 apply (induct n) |
76 apply (induct n) |
77 apply auto |
77 apply auto |
78 apply (simp add: int_0_less_mult_iff) |
78 apply (simp add: zero_less_mult_iff) |
79 done |
79 done |
80 |
80 |
81 lemma funprod_zgcd [rule_format (no_asm)]: |
81 lemma funprod_zgcd [rule_format (no_asm)]: |
82 "(\<forall>i. k \<le> i \<and> i \<le> k + l --> zgcd (mf i, mf m) = 1) --> |
82 "(\<forall>i. k \<le> i \<and> i \<le> k + l --> zgcd (mf i, mf m) = 1) --> |
83 zgcd (funprod mf k l, mf m) = 1" |
83 zgcd (funprod mf k l, mf m) = 1" |