author | hoelzl |
Tue, 05 Jan 2016 13:35:06 +0100 | |
changeset 62055 | 755fda743c49 |
parent 62049 | b0f941e207cf |
child 62072 | bf3d9f113474 |
permissions | -rw-r--r-- |
62055
755fda743c49
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset
|
1 |
(* Title: HOL/Library/Nonpos_Ints.thy |
755fda743c49
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset
|
2 |
Author: Manuel Eberl, TU München |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
3 |
*) |
62055
755fda743c49
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset
|
4 |
|
755fda743c49
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset
|
5 |
section \<open>Non-positive integers\<close> |
755fda743c49
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset
|
6 |
|
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
7 |
theory Nonpos_Ints |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
8 |
imports Complex_Main |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
9 |
begin |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
10 |
|
62055
755fda743c49
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset
|
11 |
text \<open> |
755fda743c49
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset
|
12 |
The set of non-positive integers on a ring. (in analogy to the set of non-negative |
755fda743c49
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset
|
13 |
integers @{term "\<nat>"}) This is useful e.g. for the Gamma function. |
755fda743c49
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset
|
14 |
\<close> |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
15 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
16 |
definition nonpos_Ints ("\<int>\<^sub>\<le>\<^sub>0") where "\<int>\<^sub>\<le>\<^sub>0 = {of_int n |n. n \<le> 0}" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
17 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
18 |
lemma zero_in_nonpos_Ints [simp,intro]: "0 \<in> \<int>\<^sub>\<le>\<^sub>0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
19 |
unfolding nonpos_Ints_def by (auto intro!: exI[of _ "0::int"]) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
20 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
21 |
lemma neg_one_in_nonpos_Ints [simp,intro]: "-1 \<in> \<int>\<^sub>\<le>\<^sub>0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
22 |
unfolding nonpos_Ints_def by (auto intro!: exI[of _ "-1::int"]) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
23 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
24 |
lemma neg_numeral_in_nonpos_Ints [simp,intro]: "-numeral n \<in> \<int>\<^sub>\<le>\<^sub>0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
25 |
unfolding nonpos_Ints_def by (auto intro!: exI[of _ "-numeral n::int"]) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
26 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
27 |
lemma one_notin_nonpos_Ints [simp]: "(1 :: 'a :: ring_char_0) \<notin> \<int>\<^sub>\<le>\<^sub>0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
28 |
by (auto simp: nonpos_Ints_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
29 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
30 |
lemma numeral_notin_nonpos_Ints [simp]: "(numeral n :: 'a :: ring_char_0) \<notin> \<int>\<^sub>\<le>\<^sub>0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
31 |
by (auto simp: nonpos_Ints_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
32 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
33 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
34 |
lemma minus_of_nat_in_nonpos_Ints [simp, intro]: "- of_nat n \<in> \<int>\<^sub>\<le>\<^sub>0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
35 |
proof - |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
36 |
have "- of_nat n = of_int (-int n)" by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
37 |
also have "-int n \<le> 0" by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
38 |
hence "of_int (-int n) \<in> \<int>\<^sub>\<le>\<^sub>0" unfolding nonpos_Ints_def by blast |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
39 |
finally show ?thesis . |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
40 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
41 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
42 |
lemma of_nat_in_nonpos_Ints_iff: "(of_nat n :: 'a :: {ring_1,ring_char_0}) \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n = 0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
43 |
proof |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
44 |
assume "(of_nat n :: 'a) \<in> \<int>\<^sub>\<le>\<^sub>0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
45 |
then obtain m where "of_nat n = (of_int m :: 'a)" "m \<le> 0" by (auto simp: nonpos_Ints_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
46 |
hence "(of_int m :: 'a) = of_nat n" by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
47 |
also have "... = of_int (int n)" by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
48 |
finally have "m = int n" by (subst (asm) of_int_eq_iff) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
49 |
with `m \<le> 0` show "n = 0" by auto |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
50 |
qed simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
51 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
52 |
lemma nonpos_Ints_of_int: "n \<le> 0 \<Longrightarrow> of_int n \<in> \<int>\<^sub>\<le>\<^sub>0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
53 |
unfolding nonpos_Ints_def by blast |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
54 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
55 |
lemma nonpos_IntsI: |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
56 |
"x \<in> \<int> \<Longrightarrow> x \<le> 0 \<Longrightarrow> (x :: 'a :: linordered_idom) \<in> \<int>\<^sub>\<le>\<^sub>0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
57 |
using assms unfolding nonpos_Ints_def Ints_def by auto |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
58 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
59 |
lemma nonpos_Ints_subset_Ints: "\<int>\<^sub>\<le>\<^sub>0 \<subseteq> \<int>" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
60 |
unfolding nonpos_Ints_def Ints_def by blast |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
61 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
62 |
lemma nonpos_Ints_nonpos [dest]: "x \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> x \<le> (0 :: 'a :: linordered_idom)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
63 |
unfolding nonpos_Ints_def by auto |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
64 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
65 |
lemma nonpos_Ints_Int [dest]: "x \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> x \<in> \<int>" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
66 |
unfolding nonpos_Ints_def Ints_def by blast |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
67 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
68 |
lemma nonpos_Ints_cases: |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
69 |
assumes "x \<in> \<int>\<^sub>\<le>\<^sub>0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
70 |
obtains n where "x = of_int n" "n \<le> 0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
71 |
using assms unfolding nonpos_Ints_def by (auto elim!: Ints_cases) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
72 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
73 |
lemma nonpos_Ints_cases': |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
74 |
assumes "x \<in> \<int>\<^sub>\<le>\<^sub>0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
75 |
obtains n where "x = -of_nat n" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
76 |
proof - |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
77 |
from assms obtain m where "x = of_int m" and m: "m \<le> 0" by (auto elim!: nonpos_Ints_cases) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
78 |
hence "x = - of_int (-m)" by auto |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
79 |
also from m have "(of_int (-m) :: 'a) = of_nat (nat (-m))" by simp_all |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
80 |
finally show ?thesis by (rule that) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
81 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
82 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
83 |
lemma of_real_in_nonpos_Ints_iff: "(of_real x :: 'a :: real_algebra_1) \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> x \<in> \<int>\<^sub>\<le>\<^sub>0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
84 |
proof |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
85 |
assume "of_real x \<in> (\<int>\<^sub>\<le>\<^sub>0 :: 'a set)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
86 |
then obtain n where "(of_real x :: 'a) = of_int n" "n \<le> 0" by (erule nonpos_Ints_cases) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
87 |
note `of_real x = of_int n` |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
88 |
also have "of_int n = of_real (of_int n)" by (rule of_real_of_int_eq [symmetric]) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
89 |
finally have "x = of_int n" by (subst (asm) of_real_eq_iff) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
90 |
with `n \<le> 0` show "x \<in> \<int>\<^sub>\<le>\<^sub>0" by (simp add: nonpos_Ints_of_int) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
91 |
qed (auto elim!: nonpos_Ints_cases intro!: nonpos_Ints_of_int) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
92 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
93 |
lemma nonpos_Ints_altdef: "\<int>\<^sub>\<le>\<^sub>0 = {n \<in> \<int>. (n :: 'a :: linordered_idom) \<le> 0}" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
94 |
by (auto intro!: nonpos_IntsI elim!: nonpos_Ints_cases) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
95 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
96 |
lemma uminus_in_Nats_iff: "-x \<in> \<nat> \<longleftrightarrow> x \<in> \<int>\<^sub>\<le>\<^sub>0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
97 |
proof |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
98 |
assume "-x \<in> \<nat>" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
99 |
then obtain n where "n \<ge> 0" "-x = of_int n" by (auto simp: Nats_altdef1) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
100 |
hence "-n \<le> 0" "x = of_int (-n)" by (simp_all add: eq_commute minus_equation_iff[of x]) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
101 |
thus "x \<in> \<int>\<^sub>\<le>\<^sub>0" unfolding nonpos_Ints_def by blast |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
102 |
next |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
103 |
assume "x \<in> \<int>\<^sub>\<le>\<^sub>0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
104 |
then obtain n where "n \<le> 0" "x = of_int n" by (auto simp: nonpos_Ints_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
105 |
hence "-n \<ge> 0" "-x = of_int (-n)" by (simp_all add: eq_commute minus_equation_iff[of x]) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
106 |
thus "-x \<in> \<nat>" unfolding Nats_altdef1 by blast |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
107 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
108 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
109 |
lemma uminus_in_nonpos_Ints_iff: "-x \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> x \<in> \<nat>" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
110 |
using uminus_in_Nats_iff[of "-x"] by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
111 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
112 |
lemma nonpos_Ints_mult: "x \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> y \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> x * y \<in> \<nat>" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
113 |
using Nats_mult[of "-x" "-y"] by (simp add: uminus_in_Nats_iff) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
114 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
115 |
lemma Nats_mult_nonpos_Ints: "x \<in> \<nat> \<Longrightarrow> y \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> x * y \<in> \<int>\<^sub>\<le>\<^sub>0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
116 |
using Nats_mult[of x "-y"] by (simp add: uminus_in_Nats_iff) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
117 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
118 |
lemma nonpos_Ints_mult_Nats: |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
119 |
"x \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> y \<in> \<nat> \<Longrightarrow> x * y \<in> \<int>\<^sub>\<le>\<^sub>0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
120 |
using Nats_mult[of "-x" y] by (simp add: uminus_in_Nats_iff) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
121 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
122 |
lemma nonpos_Ints_add: |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
123 |
"x \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> y \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> x + y \<in> \<int>\<^sub>\<le>\<^sub>0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
124 |
using Nats_add[of "-x" "-y"] uminus_in_Nats_iff[of "y+x", simplified minus_add] |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
125 |
by (simp add: uminus_in_Nats_iff add.commute) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
126 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
127 |
lemma nonpos_Ints_diff_Nats: |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
128 |
"x \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> y \<in> \<nat> \<Longrightarrow> x - y \<in> \<int>\<^sub>\<le>\<^sub>0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
129 |
using Nats_add[of "-x" "y"] uminus_in_Nats_iff[of "x-y", simplified minus_add] |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
130 |
by (simp add: uminus_in_Nats_iff add.commute) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
131 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
132 |
lemma Nats_diff_nonpos_Ints: |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
133 |
"x \<in> \<nat> \<Longrightarrow> y \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> x - y \<in> \<nat>" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
134 |
using Nats_add[of "x" "-y"] by (simp add: uminus_in_Nats_iff add.commute) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
135 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
136 |
lemma plus_of_nat_eq_0_imp: "z + of_nat n = 0 \<Longrightarrow> z \<in> \<int>\<^sub>\<le>\<^sub>0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
137 |
proof - |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
138 |
assume "z + of_nat n = 0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
139 |
hence A: "z = - of_nat n" by (simp add: eq_neg_iff_add_eq_0) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
140 |
show "z \<in> \<int>\<^sub>\<le>\<^sub>0" by (subst A) simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
141 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
142 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
143 |
end |