author  wenzelm 
Tue, 05 Jan 2016 21:57:21 +0100  
changeset 62072  bf3d9f113474 
parent 62055  755fda743c49 
child 62131  1baed43f453e 
permissions  rwrr 
62055
755fda743c49
MultivariateAnalysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset

1 
(* Title: HOL/Library/Nonpos_Ints.thy 
755fda743c49
MultivariateAnalysis: 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
MultivariateAnalysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset

4 

755fda743c49
MultivariateAnalysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset

5 
section \<open>Nonpositive integers\<close> 
755fda743c49
MultivariateAnalysis: 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
MultivariateAnalysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset

11 
text \<open> 
755fda743c49
MultivariateAnalysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset

12 
The set of nonpositive integers on a ring. (in analogy to the set of nonnegative 
755fda743c49
MultivariateAnalysis: 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
MultivariateAnalysis: 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) 
62072  49 
with \<open>m \<le> 0\<close> show "n = 0" by auto 
62049
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) 
62072  87 
note \<open>of_real x = of_int n\<close> 
62049
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) 
62072  90 
with \<open>n \<le> 0\<close> show "x \<in> \<int>\<^sub>\<le>\<^sub>0" by (simp add: nonpos_Ints_of_int) 
62049
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 "xy", 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 