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