[STATEMENT]
lemma bij_betw_arith_prog:
  assumes "b > 0"
  shows   "bij_betw (\<lambda>n. a + int b * n) UNIV (arith_prog a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (\<lambda>n. a + int b * n) UNIV (arith_prog a b)
[PROOF STEP]
proof (rule bij_betwI[of _ _ _ "\<lambda>x. (x - a) div int b"], goal_cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. (\<lambda>n. a + int b * n) \<in> UNIV \<rightarrow> arith_prog a b
 2. (\<lambda>x. (x - a) div int b) \<in> arith_prog a b \<rightarrow> UNIV
 3. \<And>x. x \<in> UNIV \<Longrightarrow> (a + int b * x - a) div int b = x
 4. \<And>y. y \<in> arith_prog a b \<Longrightarrow> a + int b * ((y - a) div int b) = y
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. (\<lambda>n. a + int b * n) \<in> UNIV \<rightarrow> arith_prog a b
 2. (\<lambda>x. (x - a) div int b) \<in> arith_prog a b \<rightarrow> UNIV
 3. \<And>x. x \<in> UNIV \<Longrightarrow> (a + int b * x - a) div int b = x
 4. \<And>y. y \<in> arith_prog a b \<Longrightarrow> a + int b * ((y - a) div int b) = y
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. a + int b * n) \<in> UNIV \<rightarrow> arith_prog a b
[PROOF STEP]
by (auto simp: arith_prog_def cong_add_lcancel_0 cong_mult_self_right mult_of_nat_commute)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. a + int b * n) \<in> UNIV \<rightarrow> arith_prog a b

goal (3 subgoals):
 1. (\<lambda>x. (x - a) div int b) \<in> arith_prog a b \<rightarrow> UNIV
 2. \<And>x. x \<in> UNIV \<Longrightarrow> (a + int b * x - a) div int b = x
 3. \<And>y. y \<in> arith_prog a b \<Longrightarrow> a + int b * ((y - a) div int b) = y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (\<lambda>x. (x - a) div int b) \<in> arith_prog a b \<rightarrow> UNIV
 2. \<And>x. x \<in> UNIV \<Longrightarrow> (a + int b * x - a) div int b = x
 3. \<And>y. y \<in> arith_prog a b \<Longrightarrow> a + int b * ((y - a) div int b) = y
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:
y_ \<in> arith_prog a b

goal (3 subgoals):
 1. (\<lambda>x. (x - a) div int b) \<in> arith_prog a b \<rightarrow> UNIV
 2. \<And>x. x \<in> UNIV \<Longrightarrow> (a + int b * x - a) div int b = x
 3. \<And>y. y \<in> arith_prog a b \<Longrightarrow> a + int b * ((y - a) div int b) = y
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
y_ \<in> arith_prog a b

goal (1 subgoal):
 1. a + int b * ((y_ - a) div int b) = y_
[PROOF STEP]
by (auto simp: arith_prog_def cong_iff_lin)
[PROOF STATE]
proof (state)
this:
a + int b * ((y_ - a) div int b) = y_

goal (2 subgoals):
 1. (\<lambda>x. (x - a) div int b) \<in> arith_prog a b \<rightarrow> UNIV
 2. \<And>x. x \<in> UNIV \<Longrightarrow> (a + int b * x - a) div int b = x
[PROOF STEP]
qed (use \<open>b > 0\<close> in \<open>auto simp: arith_prog_def\<close>)


[STATEMENT]
lemma arith_prog_altdef: "arith_prog a b = range (\<lambda>n. a + int b * n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog a b = range (\<lambda>n. a + int b * n)
[PROOF STEP]
proof (cases "b = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b = 0 \<Longrightarrow> arith_prog a b = range (\<lambda>n. a + int b * n)
 2. b \<noteq> 0 \<Longrightarrow> arith_prog a b = range (\<lambda>n. a + int b * n)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
b \<noteq> 0

goal (2 subgoals):
 1. b = 0 \<Longrightarrow> arith_prog a b = range (\<lambda>n. a + int b * n)
 2. b \<noteq> 0 \<Longrightarrow> arith_prog a b = range (\<lambda>n. a + int b * n)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<noteq> 0

goal (1 subgoal):
 1. arith_prog a b = range (\<lambda>n. a + int b * n)
[PROOF STEP]
using bij_betw_arith_prog[of b]
[PROOF STATE]
proof (prove)
using this:
b \<noteq> 0
0 < b \<Longrightarrow> bij_betw (\<lambda>n. ?a + int b * n) UNIV (arith_prog ?a b)

goal (1 subgoal):
 1. arith_prog a b = range (\<lambda>n. a + int b * n)
[PROOF STEP]
by (auto simp: bij_betw_def)
[PROOF STATE]
proof (state)
this:
arith_prog a b = range (\<lambda>n. a + int b * n)

goal (1 subgoal):
 1. b = 0 \<Longrightarrow> arith_prog a b = range (\<lambda>n. a + int b * n)
[PROOF STEP]
qed auto


[STATEMENT]
lemma infinite_arith_prog: "b > 0 \<Longrightarrow> infinite (arith_prog a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < b \<Longrightarrow> infinite (arith_prog a b)
[PROOF STEP]
using bij_betw_finite[OF bij_betw_arith_prog[of b]]
[PROOF STATE]
proof (prove)
using this:
0 < b \<Longrightarrow> finite UNIV = finite (arith_prog ?a1 b)

goal (1 subgoal):
 1. 0 < b \<Longrightarrow> infinite (arith_prog a b)
[PROOF STEP]
by simp


[STATEMENT]
lemma open_fbint_imp_infinite:
  fixes U :: "fbint set"
  assumes "open U" and "U \<noteq> {}"
  shows   "infinite U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite U
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
open U
U \<noteq> {}

goal (1 subgoal):
 1. infinite U
[PROOF STEP]
proof transfer
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>U. \<lbrakk>\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U; U \<noteq> {}\<rbrakk> \<Longrightarrow> infinite U
[PROOF STEP]
fix U :: "int set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>U. \<lbrakk>\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U; U \<noteq> {}\<rbrakk> \<Longrightarrow> infinite U
[PROOF STEP]
assume *: "\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U" and "U \<noteq> {}"
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U
U \<noteq> {}

goal (1 subgoal):
 1. \<And>U. \<lbrakk>\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U; U \<noteq> {}\<rbrakk> \<Longrightarrow> infinite U
[PROOF STEP]
from \<open>U \<noteq> {}\<close>
[PROOF STATE]
proof (chain)
picking this:
U \<noteq> {}
[PROOF STEP]
obtain x where "x \<in> U"
[PROOF STATE]
proof (prove)
using this:
U \<noteq> {}

goal (1 subgoal):
 1. (\<And>x. x \<in> U \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> U

goal (1 subgoal):
 1. \<And>U. \<lbrakk>\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U; U \<noteq> {}\<rbrakk> \<Longrightarrow> infinite U
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U
x \<in> U
[PROOF STEP]
obtain b where b: "b > 0" "arith_prog x b \<subseteq> U"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U
x \<in> U

goal (1 subgoal):
 1. (\<And>b. \<lbrakk>0 < b; arith_prog x b \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < b
arith_prog x b \<subseteq> U

goal (1 subgoal):
 1. \<And>U. \<lbrakk>\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U; U \<noteq> {}\<rbrakk> \<Longrightarrow> infinite U
[PROOF STEP]
from b
[PROOF STATE]
proof (chain)
picking this:
0 < b
arith_prog x b \<subseteq> U
[PROOF STEP]
have "infinite (arith_prog x b)"
[PROOF STATE]
proof (prove)
using this:
0 < b
arith_prog x b \<subseteq> U

goal (1 subgoal):
 1. infinite (arith_prog x b)
[PROOF STEP]
using infinite_arith_prog
[PROOF STATE]
proof (prove)
using this:
0 < b
arith_prog x b \<subseteq> U
0 < ?b \<Longrightarrow> infinite (arith_prog ?a ?b)

goal (1 subgoal):
 1. infinite (arith_prog x b)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
infinite (arith_prog x b)

goal (1 subgoal):
 1. \<And>U. \<lbrakk>\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U; U \<noteq> {}\<rbrakk> \<Longrightarrow> infinite U
[PROOF STEP]
with b
[PROOF STATE]
proof (chain)
picking this:
0 < b
arith_prog x b \<subseteq> U
infinite (arith_prog x b)
[PROOF STEP]
show "infinite U"
[PROOF STATE]
proof (prove)
using this:
0 < b
arith_prog x b \<subseteq> U
infinite (arith_prog x b)

goal (1 subgoal):
 1. infinite U
[PROOF STEP]
using finite_subset
[PROOF STATE]
proof (prove)
using this:
0 < b
arith_prog x b \<subseteq> U
infinite (arith_prog x b)
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. infinite U
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
infinite U

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_open_finite_fbint [simp]:
  assumes "finite (U :: fbint set)" "U \<noteq> {}"
  shows   "\<not>open U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> open U
[PROOF STEP]
using open_fbint_imp_infinite assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>open ?U; ?U \<noteq> {}\<rbrakk> \<Longrightarrow> infinite ?U
finite U
U \<noteq> {}

goal (1 subgoal):
 1. \<not> open U
[PROOF STEP]
by blast


[STATEMENT]
lemma open_arith_prog_fb [intro]:
  assumes "b > 0"
  shows   "open (arith_prog_fb a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (arith_prog_fb a b)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < b

goal (1 subgoal):
 1. open (arith_prog_fb a b)
[PROOF STEP]
proof transfer
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b a. 0 < b \<Longrightarrow> \<forall>x\<in>arith_prog a b. \<exists>ba>0. arith_prog x ba \<subseteq> arith_prog a b
[PROOF STEP]
fix a :: int and b :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b a. 0 < b \<Longrightarrow> \<forall>x\<in>arith_prog a b. \<exists>ba>0. arith_prog x ba \<subseteq> arith_prog a b
[PROOF STEP]
assume "b > 0"
[PROOF STATE]
proof (state)
this:
0 < b

goal (1 subgoal):
 1. \<And>b a. 0 < b \<Longrightarrow> \<forall>x\<in>arith_prog a b. \<exists>ba>0. arith_prog x ba \<subseteq> arith_prog a b
[PROOF STEP]
show "\<forall>x\<in>arith_prog a b. \<exists>b'>0. arith_prog x b' \<subseteq> arith_prog a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>arith_prog a b. \<exists>b'>0. arith_prog x b' \<subseteq> arith_prog a b
[PROOF STEP]
proof (intro ballI exI[of _ b] conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> arith_prog a b \<Longrightarrow> 0 < b
 2. \<And>x. x \<in> arith_prog a b \<Longrightarrow> arith_prog x b \<subseteq> arith_prog a b
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> arith_prog a b \<Longrightarrow> 0 < b
 2. \<And>x. x \<in> arith_prog a b \<Longrightarrow> arith_prog x b \<subseteq> arith_prog a b
[PROOF STEP]
assume "x \<in> arith_prog a b"
[PROOF STATE]
proof (state)
this:
x \<in> arith_prog a b

goal (2 subgoals):
 1. \<And>x. x \<in> arith_prog a b \<Longrightarrow> 0 < b
 2. \<And>x. x \<in> arith_prog a b \<Longrightarrow> arith_prog x b \<subseteq> arith_prog a b
[PROOF STEP]
thus "arith_prog x b \<subseteq> arith_prog a b"
[PROOF STATE]
proof (prove)
using this:
x \<in> arith_prog a b

goal (1 subgoal):
 1. arith_prog x b \<subseteq> arith_prog a b
[PROOF STEP]
using cong_trans
[PROOF STATE]
proof (prove)
using this:
x \<in> arith_prog a b
\<lbrakk>[?b = ?c] (mod ?a); [?c = ?d] (mod ?a)\<rbrakk> \<Longrightarrow> [?b = ?d] (mod ?a)

goal (1 subgoal):
 1. arith_prog x b \<subseteq> arith_prog a b
[PROOF STEP]
by (auto simp: arith_prog_def )
[PROOF STATE]
proof (state)
this:
arith_prog x b \<subseteq> arith_prog a b

goal (1 subgoal):
 1. \<And>x. x \<in> arith_prog a b \<Longrightarrow> 0 < b
[PROOF STEP]
qed (use \<open>b > 0\<close> in auto)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>arith_prog a b. \<exists>b'>0. arith_prog x b' \<subseteq> arith_prog a b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma closed_arith_prog_fb [intro]:
  assumes "b > 0"
  shows   "closed (arith_prog_fb a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (arith_prog_fb a b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. closed (arith_prog_fb a b)
[PROOF STEP]
have "open (-arith_prog_fb a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (- arith_prog_fb a b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. open (- arith_prog_fb a b)
[PROOF STEP]
have "-arith_prog_fb a b = (\<Union>i\<in>{1..<b}. arith_prog_fb (a+i) b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - arith_prog_fb a b = (\<Union>i\<in>{1..<b}. arith_prog_fb (a + int i) b)
[PROOF STEP]
proof (transfer fixing: b)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. - arith_prog a b = (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)
[PROOF STEP]
fix a :: int
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. - arith_prog a b = (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)
[PROOF STEP]
have disjoint: "x \<notin> arith_prog a b" if "x \<in> arith_prog (a + int i) b" "i \<in> {1..<b}" for x i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> arith_prog a b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> arith_prog a b
[PROOF STEP]
have "[a \<noteq> a + int i] (mod int b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a \<noteq> a + int i] (mod int b)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [a = a + int i] (mod int b) \<Longrightarrow> False
[PROOF STEP]
assume "[a = a + int i] (mod int b)"
[PROOF STATE]
proof (state)
this:
[a = a + int i] (mod int b)

goal (1 subgoal):
 1. [a = a + int i] (mod int b) \<Longrightarrow> False
[PROOF STEP]
hence "[a + 0 = a + int i] (mod int b)"
[PROOF STATE]
proof (prove)
using this:
[a = a + int i] (mod int b)

goal (1 subgoal):
 1. [a + 0 = a + int i] (mod int b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[a + 0 = a + int i] (mod int b)

goal (1 subgoal):
 1. [a = a + int i] (mod int b) \<Longrightarrow> False
[PROOF STEP]
hence "[0 = int i] (mod int b)"
[PROOF STATE]
proof (prove)
using this:
[a + 0 = a + int i] (mod int b)

goal (1 subgoal):
 1. [0 = int i] (mod int b)
[PROOF STEP]
by (subst (asm) cong_add_lcancel) auto
[PROOF STATE]
proof (state)
this:
[0 = int i] (mod int b)

goal (1 subgoal):
 1. [a = a + int i] (mod int b) \<Longrightarrow> False
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
x \<in> arith_prog (a + int i) b
i \<in> {1..<b}
[0 = int i] (mod int b)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
x \<in> arith_prog (a + int i) b
i \<in> {1..<b}
[0 = int i] (mod int b)

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto simp: cong_def)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[a \<noteq> a + int i] (mod int b)

goal (1 subgoal):
 1. x \<notin> arith_prog a b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[a \<noteq> a + int i] (mod int b)

goal (1 subgoal):
 1. x \<notin> arith_prog a b
[PROOF STEP]
using arith_prog_disjoint[of a "a + int i" b] \<open>b > 0\<close> that
[PROOF STATE]
proof (prove)
using this:
[a \<noteq> a + int i] (mod int b)
\<lbrakk>[a \<noteq> a + int i] (mod int b); 0 < b\<rbrakk> \<Longrightarrow> arith_prog a b \<inter> arith_prog (a + int i) b = {}
0 < b
x \<in> arith_prog (a + int i) b
i \<in> {1..<b}

goal (1 subgoal):
 1. x \<notin> arith_prog a b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<notin> arith_prog a b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> arith_prog (a + int ?i) b; ?i \<in> {1..<b}\<rbrakk> \<Longrightarrow> ?x \<notin> arith_prog a b

goal (1 subgoal):
 1. \<And>a. - arith_prog a b = (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)
[PROOF STEP]
have covering: "x \<in> arith_prog a b \<or> x \<in> (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> arith_prog a b \<or> x \<in> (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> arith_prog a b \<or> x \<in> (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)
[PROOF STEP]
define i where "i = nat ((x - a) mod (int b))"
[PROOF STATE]
proof (state)
this:
i = nat ((x - a) mod int b)

goal (1 subgoal):
 1. x \<in> arith_prog a b \<or> x \<in> (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)
[PROOF STEP]
have "[a + int i = a + (x - a) mod int b] (mod int b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a + int i = a + (x - a) mod int b] (mod int b)
[PROOF STEP]
unfolding i_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a + int (nat ((x - a) mod int b)) = a + (x - a) mod int b] (mod int b)
[PROOF STEP]
using \<open>b > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < b

goal (1 subgoal):
 1. [a + int (nat ((x - a) mod int b)) = a + (x - a) mod int b] (mod int b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[a + int i = a + (x - a) mod int b] (mod int b)

goal (1 subgoal):
 1. x \<in> arith_prog a b \<or> x \<in> (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[a + int i = a + (x - a) mod int b] (mod int b)

goal (1 subgoal):
 1. x \<in> arith_prog a b \<or> x \<in> (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)
[PROOF STEP]
have "[a + (x - a) mod int b = a + (x - a)] (mod int b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a + (x - a) mod int b = a + (x - a)] (mod int b)
[PROOF STEP]
by (intro cong_add) auto
[PROOF STATE]
proof (state)
this:
[a + (x - a) mod int b = a + (x - a)] (mod int b)

goal (1 subgoal):
 1. x \<in> arith_prog a b \<or> x \<in> (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
[a + int i = a + (x - a)] (mod int b)
[PROOF STEP]
have "[x = a + int i] (mod int b)"
[PROOF STATE]
proof (prove)
using this:
[a + int i = a + (x - a)] (mod int b)

goal (1 subgoal):
 1. [x = a + int i] (mod int b)
[PROOF STEP]
by (simp add: cong_sym_eq)
[PROOF STATE]
proof (state)
this:
[x = a + int i] (mod int b)

goal (1 subgoal):
 1. x \<in> arith_prog a b \<or> x \<in> (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)
[PROOF STEP]
hence "x \<in> arith_prog (a + int i) b"
[PROOF STATE]
proof (prove)
using this:
[x = a + int i] (mod int b)

goal (1 subgoal):
 1. x \<in> arith_prog (a + int i) b
[PROOF STEP]
using \<open>b > 0\<close>
[PROOF STATE]
proof (prove)
using this:
[x = a + int i] (mod int b)
0 < b

goal (1 subgoal):
 1. x \<in> arith_prog (a + int i) b
[PROOF STEP]
by (auto simp: arith_prog_def)
[PROOF STATE]
proof (state)
this:
x \<in> arith_prog (a + int i) b

goal (1 subgoal):
 1. x \<in> arith_prog a b \<or> x \<in> (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> arith_prog (a + int i) b

goal (1 subgoal):
 1. x \<in> arith_prog a b \<or> x \<in> (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)
[PROOF STEP]
have "i < b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < b
[PROOF STEP]
using \<open>b > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < b

goal (1 subgoal):
 1. i < b
[PROOF STEP]
by (auto simp: i_def nat_less_iff)
[PROOF STATE]
proof (state)
this:
i < b

goal (1 subgoal):
 1. x \<in> arith_prog a b \<or> x \<in> (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> arith_prog (a + int i) b
i < b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> arith_prog (a + int i) b
i < b

goal (1 subgoal):
 1. x \<in> arith_prog a b \<or> x \<in> (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)
[PROOF STEP]
using \<open>b > 0\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> arith_prog (a + int i) b
i < b
0 < b

goal (1 subgoal):
 1. x \<in> arith_prog a b \<or> x \<in> (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)
[PROOF STEP]
by (cases "i = 0") auto
[PROOF STATE]
proof (state)
this:
x \<in> arith_prog a b \<or> x \<in> (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in> arith_prog a b \<or> ?x \<in> (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)

goal (1 subgoal):
 1. \<And>a. - arith_prog a b = (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)
[PROOF STEP]
from disjoint and covering
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x \<in> arith_prog (a + int ?i) b; ?i \<in> {1..<b}\<rbrakk> \<Longrightarrow> ?x \<notin> arith_prog a b
?x \<in> arith_prog a b \<or> ?x \<in> (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)
[PROOF STEP]
show "- arith_prog a b = (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> arith_prog (a + int ?i) b; ?i \<in> {1..<b}\<rbrakk> \<Longrightarrow> ?x \<notin> arith_prog a b
?x \<in> arith_prog a b \<or> ?x \<in> (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)

goal (1 subgoal):
 1. - arith_prog a b = (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
- arith_prog a b = (\<Union>i\<in>{1..<b}. arith_prog (a + int i) b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
- arith_prog_fb a b = (\<Union>i\<in>{1..<b}. arith_prog_fb (a + int i) b)

goal (1 subgoal):
 1. open (- arith_prog_fb a b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- arith_prog_fb a b = (\<Union>i\<in>{1..<b}. arith_prog_fb (a + int i) b)

goal (1 subgoal):
 1. open (- arith_prog_fb a b)
[PROOF STEP]
from \<open>b > 0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < b
[PROOF STEP]
have "open \<dots>"
[PROOF STATE]
proof (prove)
using this:
0 < b

goal (1 subgoal):
 1. open (\<Union>i\<in>{1..<b}. arith_prog_fb (a + int i) b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
open (\<Union>i\<in>{1..<b}. arith_prog_fb (a + int i) b)

goal (1 subgoal):
 1. open (- arith_prog_fb a b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
open (- arith_prog_fb a b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
open (- arith_prog_fb a b)

goal (1 subgoal):
 1. open (- arith_prog_fb a b)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
open (- arith_prog_fb a b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
open (- arith_prog_fb a b)

goal (1 subgoal):
 1. closed (arith_prog_fb a b)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
open (- arith_prog_fb a b)

goal (1 subgoal):
 1. closed (arith_prog_fb a b)
[PROOF STEP]
by (simp add: closed_def)
[PROOF STATE]
proof (state)
this:
closed (arith_prog_fb a b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem "infinite {p::nat. prime p}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {p. prime p}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {p. prime p} \<Longrightarrow> False
[PROOF STEP]
assume fin: "finite {p::nat. prime p}"
[PROOF STATE]
proof (state)
this:
finite {p. prime p}

goal (1 subgoal):
 1. finite {p. prime p} \<Longrightarrow> False
[PROOF STEP]
define A where "A = (\<Union>p\<in>{p::nat. prime p}. arith_prog_fb 0 p)"
[PROOF STATE]
proof (state)
this:
A = \<Union> (arith_prog_fb 0 ` {p. prime p})

goal (1 subgoal):
 1. finite {p. prime p} \<Longrightarrow> False
[PROOF STEP]
have "closed A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed A
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (\<Union> (arith_prog_fb 0 ` Collect prime))
[PROOF STEP]
using fin
[PROOF STATE]
proof (prove)
using this:
finite {p. prime p}

goal (1 subgoal):
 1. closed (\<Union> (arith_prog_fb 0 ` Collect prime))
[PROOF STEP]
by (intro closed_Union) (auto simp: prime_gt_0_nat)
[PROOF STATE]
proof (state)
this:
closed A

goal (1 subgoal):
 1. finite {p. prime p} \<Longrightarrow> False
[PROOF STEP]
hence "open (-A)"
[PROOF STATE]
proof (prove)
using this:
closed A

goal (1 subgoal):
 1. open (- A)
[PROOF STEP]
by (simp add: closed_def)
[PROOF STATE]
proof (state)
this:
open (- A)

goal (1 subgoal):
 1. finite {p. prime p} \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
open (- A)

goal (1 subgoal):
 1. finite {p. prime p} \<Longrightarrow> False
[PROOF STEP]
have "A = -{fbint 1, fbint (-1)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = - {fbint 1, fbint (- 1)}
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (arith_prog_fb 0 ` Collect prime) = - {fbint 1, fbint (- 1)}
[PROOF STEP]
proof transfer
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> (arith_prog 0 ` Collect prime) = - {1, - 1}
[PROOF STEP]
show "(\<Union>p\<in>{p::nat. prime p}. arith_prog 0 p) = - {1, - 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (arith_prog 0 ` {p. prime p}) = - {1, - 1}
[PROOF STEP]
proof (intro equalityI subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> \<Union> (arith_prog 0 ` {p. prime p}) \<Longrightarrow> x \<in> - {1, - 1}
 2. \<And>x. x \<in> - {1, - 1} \<Longrightarrow> x \<in> \<Union> (arith_prog 0 ` {p. prime p})
[PROOF STEP]
fix x :: int
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> \<Union> (arith_prog 0 ` {p. prime p}) \<Longrightarrow> x \<in> - {1, - 1}
 2. \<And>x. x \<in> - {1, - 1} \<Longrightarrow> x \<in> \<Union> (arith_prog 0 ` {p. prime p})
[PROOF STEP]
assume x: "x \<in> -{1, -1}"
[PROOF STATE]
proof (state)
this:
x \<in> - {1, - 1}

goal (2 subgoals):
 1. \<And>x. x \<in> \<Union> (arith_prog 0 ` {p. prime p}) \<Longrightarrow> x \<in> - {1, - 1}
 2. \<And>x. x \<in> - {1, - 1} \<Longrightarrow> x \<in> \<Union> (arith_prog 0 ` {p. prime p})
[PROOF STEP]
hence "\<bar>x\<bar> \<noteq> 1"
[PROOF STATE]
proof (prove)
using this:
x \<in> - {1, - 1}

goal (1 subgoal):
 1. \<bar>x\<bar> \<noteq> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>x\<bar> \<noteq> 1

goal (2 subgoals):
 1. \<And>x. x \<in> \<Union> (arith_prog 0 ` {p. prime p}) \<Longrightarrow> x \<in> - {1, - 1}
 2. \<And>x. x \<in> - {1, - 1} \<Longrightarrow> x \<in> \<Union> (arith_prog 0 ` {p. prime p})
[PROOF STEP]
show "x \<in> (\<Union>p\<in>{p::nat. prime p}. arith_prog 0 p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> \<Union> (arith_prog 0 ` {p. prime p})
[PROOF STEP]
proof (cases "x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = 0 \<Longrightarrow> x \<in> \<Union> (arith_prog 0 ` {p. prime p})
 2. x \<noteq> 0 \<Longrightarrow> x \<in> \<Union> (arith_prog 0 ` {p. prime p})
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = 0

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> x \<in> \<Union> (arith_prog 0 ` {p. prime p})
 2. x \<noteq> 0 \<Longrightarrow> x \<in> \<Union> (arith_prog 0 ` {p. prime p})
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 0

goal (1 subgoal):
 1. x \<in> \<Union> (arith_prog 0 ` {p. prime p})
[PROOF STEP]
by (auto simp: A_def intro!: exI[of _ 2])
[PROOF STATE]
proof (state)
this:
x \<in> \<Union> (arith_prog 0 ` {p. prime p})

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> x \<in> \<Union> (arith_prog 0 ` {p. prime p})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> x \<in> \<Union> (arith_prog 0 ` {p. prime p})
[PROOF STEP]
case [simp]: False
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> x \<in> \<Union> (arith_prog 0 ` {p. prime p})
[PROOF STEP]
obtain p where p: "prime p" "p dvd x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. \<lbrakk>prime p; p dvd x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prime_divisor_exists[of x] and \<open>\<bar>x\<bar> \<noteq> 1\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x \<noteq> 0; \<not> is_unit x\<rbrakk> \<Longrightarrow> \<exists>b. b dvd x \<and> prime b
\<bar>x\<bar> \<noteq> 1

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>prime p; p dvd x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prime p
p dvd x

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> x \<in> \<Union> (arith_prog 0 ` {p. prime p})
[PROOF STEP]
hence "x \<in> arith_prog 0 (nat p)"
[PROOF STATE]
proof (prove)
using this:
prime p
p dvd x

goal (1 subgoal):
 1. x \<in> arith_prog 0 (nat p)
[PROOF STEP]
using prime_gt_0_int[of p]
[PROOF STATE]
proof (prove)
using this:
prime p
p dvd x
prime p \<Longrightarrow> 0 < p

goal (1 subgoal):
 1. x \<in> arith_prog 0 (nat p)
[PROOF STEP]
by (auto simp: arith_prog_def cong_0_iff)
[PROOF STATE]
proof (state)
this:
x \<in> arith_prog 0 (nat p)

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> x \<in> \<Union> (arith_prog 0 ` {p. prime p})
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> arith_prog 0 (nat p)

goal (1 subgoal):
 1. x \<in> \<Union> (arith_prog 0 ` {p. prime p})
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
x \<in> arith_prog 0 (nat p)
prime p
p dvd x

goal (1 subgoal):
 1. x \<in> \<Union> (arith_prog 0 ` {p. prime p})
[PROOF STEP]
by (auto simp: A_def intro!: exI[of _ "nat p"])
[PROOF STATE]
proof (state)
this:
x \<in> \<Union> (arith_prog 0 ` {p. prime p})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> \<Union> (arith_prog 0 ` {p. prime p})

goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> (arith_prog 0 ` {p. prime p}) \<Longrightarrow> x \<in> - {1, - 1}
[PROOF STEP]
qed (auto simp: A_def arith_prog_def cong_0_iff)
[PROOF STATE]
proof (state)
this:
\<Union> (arith_prog 0 ` {p. prime p}) = - {1, - 1}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A = - {fbint 1, fbint (- 1)}

goal (1 subgoal):
 1. finite {p. prime p} \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A = - {fbint 1, fbint (- 1)}

goal (1 subgoal):
 1. finite {p. prime p} \<Longrightarrow> False
[PROOF STEP]
have "-(-{fbint 1, fbint (-1)}) = {fbint 1, fbint (-1)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (- {fbint 1, fbint (- 1)}) = {fbint 1, fbint (- 1)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- (- {fbint 1, fbint (- 1)}) = {fbint 1, fbint (- 1)}

goal (1 subgoal):
 1. finite {p. prime p} \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
open {fbint 1, fbint (- 1)}
[PROOF STEP]
have "open {fbint 1, fbint (-1)}"
[PROOF STATE]
proof (prove)
using this:
open {fbint 1, fbint (- 1)}

goal (1 subgoal):
 1. open {fbint 1, fbint (- 1)}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
open {fbint 1, fbint (- 1)}

goal (1 subgoal):
 1. finite {p. prime p} \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
open {fbint 1, fbint (- 1)}

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma open_fbint_altdef: "open = generate_topology {arith_prog_fb a b |a b. b > 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open = generate_topology {arith_prog_fb a b |a b. 0 < b}
[PROOF STEP]
using topological_basis_imp_subbasis[OF topological_basis_fbint]
[PROOF STATE]
proof (prove)
using this:
open = generate_topology {arith_prog_fb a b |a b. 0 < b}

goal (1 subgoal):
 1. open = generate_topology {arith_prog_fb a b |a b. 0 < b}
[PROOF STEP]
.


[STATEMENT]
lemma t2_space_t3_spaceI:
  assumes "\<And>(x :: 'a :: t2_space) U. x \<in> U \<Longrightarrow> open U \<Longrightarrow>
             \<exists>V. x \<in> V \<and> open V \<and> closure V \<subseteq> U"
  shows   "OFCLASS('a, t3_space_class)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OFCLASS('a, t3_space_class)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S y. \<lbrakk>closed S; y \<notin> S\<rbrakk> \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> y \<in> U \<and> S \<subseteq> V \<and> U \<inter> V = {}
[PROOF STEP]
fix X :: "'a set" and z :: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S y. \<lbrakk>closed S; y \<notin> S\<rbrakk> \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> y \<in> U \<and> S \<subseteq> V \<and> U \<inter> V = {}
[PROOF STEP]
assume X: "closed X" "z \<notin> X"
[PROOF STATE]
proof (state)
this:
closed X
z \<notin> X

goal (1 subgoal):
 1. \<And>S y. \<lbrakk>closed S; y \<notin> S\<rbrakk> \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> y \<in> U \<and> S \<subseteq> V \<and> U \<inter> V = {}
[PROOF STEP]
with assms[of z "-X"]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>z \<in> - X; open (- X)\<rbrakk> \<Longrightarrow> \<exists>V. z \<in> V \<and> open V \<and> closure V \<subseteq> - X
closed X
z \<notin> X
[PROOF STEP]
obtain V where V: "z \<in> V" "open V" "closure V \<subseteq> -X"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>z \<in> - X; open (- X)\<rbrakk> \<Longrightarrow> \<exists>V. z \<in> V \<and> open V \<and> closure V \<subseteq> - X
closed X
z \<notin> X

goal (1 subgoal):
 1. (\<And>V. \<lbrakk>z \<in> V; open V; closure V \<subseteq> - X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> V
open V
closure V \<subseteq> - X

goal (1 subgoal):
 1. \<And>S y. \<lbrakk>closed S; y \<notin> S\<rbrakk> \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> y \<in> U \<and> S \<subseteq> V \<and> U \<inter> V = {}
[PROOF STEP]
show "\<exists>U V. open U \<and> open V \<and> z \<in> U \<and> X \<subseteq> V \<and> U \<inter> V = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>U V. open U \<and> open V \<and> z \<in> U \<and> X \<subseteq> V \<and> U \<inter> V = {}
[PROOF STEP]
by (rule exI[of _ V], rule exI[of _ "-closure V"])
       (use X V closure_subset[of V] in auto)
[PROOF STATE]
proof (state)
this:
\<exists>U V. open U \<and> open V \<and> z \<in> U \<and> X \<subseteq> V \<and> U \<inter> V = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma N_summable: "summable (\<lambda>k. if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>k. if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k)
[PROOF STEP]
by (rule summable_comparison_test[OF _ summable_geometric[of "1/q"]])
     (use q_gt_1 in \<open>auto intro!: exI[of _ 0] simp: power_divide\<close>)


[STATEMENT]
lemma N_sums: "(\<lambda>k. if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k) sums N n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>k. if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k) sums N n
[PROOF STEP]
using N_summable
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>k. if k = 0 \<or> int k dvd ?n then 0 else 1 / q ^ k)

goal (1 subgoal):
 1. (\<lambda>k. if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k) sums N n
[PROOF STEP]
unfolding N_def
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>k. if k = 0 \<or> int k dvd ?n then 0 else 1 / q ^ k)

goal (1 subgoal):
 1. (\<lambda>k. if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k) sums (\<Sum>k. if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k)
[PROOF STEP]
by (rule summable_sums)


[STATEMENT]
lemma N_nonneg: "N n \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> N n
[PROOF STEP]
by (rule sums_le[OF _ sums_zero N_sums]) (use q_gt_1 in auto)


[STATEMENT]
lemma N_uminus [simp]: "N (-n) = N n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N (- n) = N n
[PROOF STEP]
by (simp add: N_def)


[STATEMENT]
lemma N_minus_commute: "N (x - y) = N (y - x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N (x - y) = N (y - x)
[PROOF STEP]
using N_uminus[of "x - y"]
[PROOF STATE]
proof (prove)
using this:
N (- (x - y)) = N (x - y)

goal (1 subgoal):
 1. N (x - y) = N (y - x)
[PROOF STEP]
by (simp del: N_uminus)


[STATEMENT]
lemma N_zero [simp]: "N 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N 0 = 0
[PROOF STEP]
by (simp add: N_def)


[STATEMENT]
lemma not_dvd_imp_N_ge:
  assumes "\<not>n dvd a" "n > 0"
  shows   "N a \<ge> 1 / q ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / q ^ n \<le> N a
[PROOF STEP]
by (rule sums_le[OF _ sums_single[of n] N_sums]) (use q_gt_1 assms in auto)


[STATEMENT]
lemma N_lt_imp_dvd:
  assumes "N a < 1 / q ^ n" and "n > 0"
  shows   "n dvd a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int n dvd a
[PROOF STEP]
using not_dvd_imp_N_ge[of n a] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> int n dvd a; 0 < n\<rbrakk> \<Longrightarrow> 1 / q ^ n \<le> N a
N a < 1 / q ^ n
0 < n

goal (1 subgoal):
 1. int n dvd a
[PROOF STEP]
by auto


[STATEMENT]
lemma N_pos:
  assumes "n \<noteq> 0"
  shows   "N n > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < N n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < N n
[PROOF STEP]
have "0 < 1 / q ^ (nat \<bar>n\<bar>+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 / q ^ (nat \<bar>n\<bar> + 1)
[PROOF STEP]
using q_gt_1
[PROOF STATE]
proof (prove)
using this:
1 < q

goal (1 subgoal):
 1. 0 < 1 / q ^ (nat \<bar>n\<bar> + 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < 1 / q ^ (nat \<bar>n\<bar> + 1)

goal (1 subgoal):
 1. 0 < N n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 < 1 / q ^ (nat \<bar>n\<bar> + 1)

goal (1 subgoal):
 1. 0 < N n
[PROOF STEP]
have "\<not>1 + \<bar>n\<bar> dvd \<bar>n\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 1 + \<bar>n\<bar> dvd \<bar>n\<bar>
[PROOF STEP]
using zdvd_imp_le[of "1 + \<bar>n\<bar>" "\<bar>n\<bar>"] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>1 + \<bar>n\<bar> dvd \<bar>n\<bar>; 0 < \<bar>n\<bar>\<rbrakk> \<Longrightarrow> 1 + \<bar>n\<bar> \<le> \<bar>n\<bar>
n \<noteq> 0

goal (1 subgoal):
 1. \<not> 1 + \<bar>n\<bar> dvd \<bar>n\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> 1 + \<bar>n\<bar> dvd \<bar>n\<bar>

goal (1 subgoal):
 1. 0 < N n
[PROOF STEP]
hence "1 / q ^ (nat \<bar>n\<bar>+1) \<le> N n"
[PROOF STATE]
proof (prove)
using this:
\<not> 1 + \<bar>n\<bar> dvd \<bar>n\<bar>

goal (1 subgoal):
 1. 1 / q ^ (nat \<bar>n\<bar> + 1) \<le> N n
[PROOF STEP]
by (intro not_dvd_imp_N_ge) (use assms in auto)
[PROOF STATE]
proof (state)
this:
1 / q ^ (nat \<bar>n\<bar> + 1) \<le> N n

goal (1 subgoal):
 1. 0 < N n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 < N n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < N n

goal (1 subgoal):
 1. 0 < N n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
0 < N n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma N_zero_iff [simp]: "N n = 0 \<longleftrightarrow> n = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (N n = 0) = (n = 0)
[PROOF STEP]
using N_pos[of n]
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0 \<Longrightarrow> 0 < N n

goal (1 subgoal):
 1. (N n = 0) = (n = 0)
[PROOF STEP]
by (cases "n = 0") auto


[STATEMENT]
lemma N_triangle_ineq: "N (n + m) \<le> N n + N m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N (n + m) \<le> N n + N m
[PROOF STEP]
proof (rule sums_le)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n. ?f n \<le> ?g n
 2. ?f sums N (n + m)
 3. ?g sums (N n + N m)
[PROOF STEP]
let ?I = "\<lambda>n k. if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n. ?f n \<le> ?g n
 2. ?f sums N (n + m)
 3. ?g sums (N n + N m)
[PROOF STEP]
show "?I (n + m) sums N (n + m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>k. if k = 0 \<or> int k dvd n + m then 0 else 1 / q ^ k) sums N (n + m)
[PROOF STEP]
by (rule N_sums)
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k = 0 \<or> int k dvd n + m then 0 else 1 / q ^ k) sums N (n + m)

goal (2 subgoals):
 1. \<And>na. (if na = 0 \<or> int na dvd n + m then 0 else 1 / q ^ na) \<le> ?g na
 2. ?g sums (N n + N m)
[PROOF STEP]
show "(\<lambda>k. ?I n k + ?I m k) sums (N n + N m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>k. (if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k) + (if k = 0 \<or> int k dvd m then 0 else 1 / q ^ k)) sums (N n + N m)
[PROOF STEP]
by (intro sums_add N_sums)
[PROOF STATE]
proof (state)
this:
(\<lambda>k. (if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k) + (if k = 0 \<or> int k dvd m then 0 else 1 / q ^ k)) sums (N n + N m)

goal (1 subgoal):
 1. \<And>na. (if na = 0 \<or> int na dvd n + m then 0 else 1 / q ^ na) \<le> (if na = 0 \<or> int na dvd n then 0 else 1 / q ^ na) + (if na = 0 \<or> int na dvd m then 0 else 1 / q ^ na)
[PROOF STEP]
qed (use q_gt_1 in auto)


[STATEMENT]
lemma N_1: "N 1 = 1 / (q * (q - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N 1 = 1 / (q * (q - 1))
[PROOF STEP]
proof (rule sums_unique2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?f sums N 1
 2. ?f sums (1 / (q * (q - 1)))
[PROOF STEP]
have "(\<lambda>k. if k = 0 \<or> int k dvd 1 then 0 else 1 / q ^ k) sums N 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>k. if k = 0 \<or> is_unit (int k) then 0 else 1 / q ^ k) sums N 1
[PROOF STEP]
by (rule N_sums)
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k = 0 \<or> is_unit (int k) then 0 else 1 / q ^ k) sums N 1

goal (2 subgoals):
 1. ?f sums N 1
 2. ?f sums (1 / (q * (q - 1)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k = 0 \<or> is_unit (int k) then 0 else 1 / q ^ k) sums N 1

goal (2 subgoals):
 1. ?f sums N 1
 2. ?f sums (1 / (q * (q - 1)))
[PROOF STEP]
have "(\<lambda>k. if k = 0 \<or> int k dvd 1 then 0 else 1 / q ^ k) =
               (\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>k. if k = 0 \<or> is_unit (int k) then 0 else 1 / q ^ k) = (\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k)
[PROOF STEP]
by (simp add: power_divide cong: if_cong)
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k = 0 \<or> is_unit (int k) then 0 else 1 / q ^ k) = (\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k)

goal (2 subgoals):
 1. ?f sums N 1
 2. ?f sums (1 / (q * (q - 1)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k) sums N 1
[PROOF STEP]
show "(\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k) sums N 1"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k) sums N 1

goal (1 subgoal):
 1. (\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k) sums N 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k) sums N 1

goal (1 subgoal):
 1. (\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k) sums (1 / (q * (q - 1)))
[PROOF STEP]
have "(\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k) sums
                 (1 / (1 - 1 / q) + (- (1 / q) - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k) sums (1 / (1 - 1 / q) + (- (1 / q) - 1))
[PROOF STEP]
by (rule sums_If_finite_set'[OF geometric_sums]) (use q_gt_1 in auto)
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k) sums (1 / (1 - 1 / q) + (- (1 / q) - 1))

goal (1 subgoal):
 1. (\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k) sums (1 / (q * (q - 1)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k) sums (1 / (1 - 1 / q) + (- (1 / q) - 1))

goal (1 subgoal):
 1. (\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k) sums (1 / (q * (q - 1)))
[PROOF STEP]
have "\<dots> = 1 / (q * (q - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / (1 - 1 / q) + (- (1 / q) - 1) = 1 / (q * (q - 1))
[PROOF STEP]
using q_gt_1
[PROOF STATE]
proof (prove)
using this:
1 < q

goal (1 subgoal):
 1. 1 / (1 - 1 / q) + (- (1 / q) - 1) = 1 / (q * (q - 1))
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
1 / (1 - 1 / q) + (- (1 / q) - 1) = 1 / (q * (q - 1))

goal (1 subgoal):
 1. (\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k) sums (1 / (q * (q - 1)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k) sums (1 / (q * (q - 1)))
[PROOF STEP]
show "(\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k) sums \<dots>"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k) sums (1 / (q * (q - 1)))

goal (1 subgoal):
 1. (\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k) sums (1 / (q * (q - 1)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k \<in> {0, 1} then 0 else (1 / q) ^ k) sums (1 / (q * (q - 1)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma N_dvd_mono:
  assumes "m dvd n"
  shows   "N n \<le> N m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N n \<le> N m
[PROOF STEP]
proof (rule sums_le[OF _ N_sums N_sums])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na. (if na = 0 \<or> int na dvd n then 0 else 1 / q ^ na) \<le> (if na = 0 \<or> int na dvd m then 0 else 1 / q ^ na)
[PROOF STEP]
fix k :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na. (if na = 0 \<or> int na dvd n then 0 else 1 / q ^ na) \<le> (if na = 0 \<or> int na dvd m then 0 else 1 / q ^ na)
[PROOF STEP]
show "(if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k) \<le>
        (if k = 0 \<or> int k dvd m then 0 else 1 / q ^ k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k) \<le> (if k = 0 \<or> int k dvd m then 0 else 1 / q ^ k)
[PROOF STEP]
using q_gt_1 assms
[PROOF STATE]
proof (prove)
using this:
1 < q
m dvd n

goal (1 subgoal):
 1. (if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k) \<le> (if k = 0 \<or> int k dvd m then 0 else 1 / q ^ k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k) \<le> (if k = 0 \<or> int k dvd m then 0 else 1 / q ^ k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma N_le_N_1: "N n \<le> N 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N n \<le> N 1
[PROOF STEP]
by (rule N_dvd_mono) auto


[STATEMENT]
lemma N_prime:
  assumes "prime p"
  shows   "N p = N 1 - 1 / q ^ nat p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N p = N 1 - 1 / q ^ nat p
[PROOF STEP]
proof (rule sums_unique2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?f sums N p
 2. ?f sums (N 1 - 1 / q ^ nat p)
[PROOF STEP]
define p' where "p' = nat p"
[PROOF STATE]
proof (state)
this:
p' = nat p

goal (2 subgoals):
 1. ?f sums N p
 2. ?f sums (N 1 - 1 / q ^ nat p)
[PROOF STEP]
have p: "p = int p'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = int p'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prime p

goal (1 subgoal):
 1. p = int p'
[PROOF STEP]
by (auto simp: p'_def prime_ge_0_int)
[PROOF STATE]
proof (state)
this:
p = int p'

goal (2 subgoals):
 1. ?f sums N p
 2. ?f sums (N 1 - 1 / q ^ nat p)
[PROOF STEP]
have "prime p'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime p'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prime p

goal (1 subgoal):
 1. prime p'
[PROOF STEP]
by (simp add: p)
[PROOF STATE]
proof (state)
this:
prime p'

goal (2 subgoals):
 1. ?f sums N p
 2. ?f sums (N 1 - 1 / q ^ nat p)
[PROOF STEP]
have "(\<lambda>k. if k = 0 \<or> int k dvd p then 0 else 1 / q ^ k) sums N p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>k. if k = 0 \<or> int k dvd p then 0 else 1 / q ^ k) sums N p
[PROOF STEP]
by (rule N_sums)
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k = 0 \<or> int k dvd p then 0 else 1 / q ^ k) sums N p

goal (2 subgoals):
 1. ?f sums N p
 2. ?f sums (N 1 - 1 / q ^ nat p)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k = 0 \<or> int k dvd p then 0 else 1 / q ^ k) sums N p

goal (2 subgoals):
 1. ?f sums N p
 2. ?f sums (N 1 - 1 / q ^ nat p)
[PROOF STEP]
have "int k dvd p \<longleftrightarrow> k \<in> {1, p'}" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (int k dvd p) = (k \<in> {1, p'})
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prime p

goal (1 subgoal):
 1. (int k dvd p) = (k \<in> {1, p'})
[PROOF STEP]
by (auto simp: p prime_nat_iff)
[PROOF STATE]
proof (state)
this:
(int ?k dvd p) = (?k \<in> {1, p'})

goal (2 subgoals):
 1. ?f sums N p
 2. ?f sums (N 1 - 1 / q ^ nat p)
[PROOF STEP]
hence "(\<lambda>k. if k = 0 \<or> int k dvd p then 0 else 1 / q ^ k) =
         (\<lambda>k. if k \<in> {0, 1, p'} then 0 else (1 / q) ^ k)"
[PROOF STATE]
proof (prove)
using this:
(int ?k dvd p) = (?k \<in> {1, p'})

goal (1 subgoal):
 1. (\<lambda>k. if k = 0 \<or> int k dvd p then 0 else 1 / q ^ k) = (\<lambda>k. if k \<in> {0, 1, p'} then 0 else (1 / q) ^ k)
[PROOF STEP]
using assms q_gt_1
[PROOF STATE]
proof (prove)
using this:
(int ?k dvd p) = (?k \<in> {1, p'})
prime p
1 < q

goal (1 subgoal):
 1. (\<lambda>k. if k = 0 \<or> int k dvd p then 0 else 1 / q ^ k) = (\<lambda>k. if k \<in> {0, 1, p'} then 0 else (1 / q) ^ k)
[PROOF STEP]
by (simp add: power_divide cong: if_cong)
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k = 0 \<or> int k dvd p then 0 else 1 / q ^ k) = (\<lambda>k. if k \<in> {0, 1, p'} then 0 else (1 / q) ^ k)

goal (2 subgoals):
 1. ?f sums N p
 2. ?f sums (N 1 - 1 / q ^ nat p)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>k. if k \<in> {0, 1, p'} then 0 else (1 / q) ^ k) sums N p
[PROOF STEP]
show "\<dots> sums N p"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>k. if k \<in> {0, 1, p'} then 0 else (1 / q) ^ k) sums N p

goal (1 subgoal):
 1. (\<lambda>k. if k \<in> {0, 1, p'} then 0 else (1 / q) ^ k) sums N p
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k \<in> {0, 1, p'} then 0 else (1 / q) ^ k) sums N p

goal (1 subgoal):
 1. (\<lambda>k. if k \<in> {0, 1, nat p} then 0 else (1 / q) ^ k) sums (N 1 - 1 / q ^ nat p)
[PROOF STEP]
have "(\<lambda>k. if k \<in> {0, 1, p'} then 0 else (1 / q) ^ k) sums
                 (1 / (1 - 1 / q) + (- (1 / q) - (1 / q) ^ p' - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>k. if k \<in> {0, 1, p'} then 0 else (1 / q) ^ k) sums (1 / (1 - 1 / q) + (- (1 / q) - (1 / q) ^ p' - 1))
[PROOF STEP]
by (rule sums_If_finite_set'[OF geometric_sums])
       (use \<open>prime p'\<close> q_gt_1 prime_gt_Suc_0_nat[of p'] in \<open>auto simp: \<close>)
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k \<in> {0, 1, p'} then 0 else (1 / q) ^ k) sums (1 / (1 - 1 / q) + (- (1 / q) - (1 / q) ^ p' - 1))

goal (1 subgoal):
 1. (\<lambda>k. if k \<in> {0, 1, nat p} then 0 else (1 / q) ^ k) sums (N 1 - 1 / q ^ nat p)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k \<in> {0, 1, p'} then 0 else (1 / q) ^ k) sums (1 / (1 - 1 / q) + (- (1 / q) - (1 / q) ^ p' - 1))

goal (1 subgoal):
 1. (\<lambda>k. if k \<in> {0, 1, nat p} then 0 else (1 / q) ^ k) sums (N 1 - 1 / q ^ nat p)
[PROOF STEP]
have "\<dots> = N 1 - 1 / q ^ p'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / (1 - 1 / q) + (- (1 / q) - (1 / q) ^ p' - 1) = N 1 - 1 / q ^ p'
[PROOF STEP]
using q_gt_1
[PROOF STATE]
proof (prove)
using this:
1 < q

goal (1 subgoal):
 1. 1 / (1 - 1 / q) + (- (1 / q) - (1 / q) ^ p' - 1) = N 1 - 1 / q ^ p'
[PROOF STEP]
by (simp add: field_simps N_1)
[PROOF STATE]
proof (state)
this:
1 / (1 - 1 / q) + (- (1 / q) - (1 / q) ^ p' - 1) = N 1 - 1 / q ^ p'

goal (1 subgoal):
 1. (\<lambda>k. if k \<in> {0, 1, nat p} then 0 else (1 / q) ^ k) sums (N 1 - 1 / q ^ nat p)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>k. if k \<in> {0, 1, p'} then 0 else (1 / q) ^ k) sums (N 1 - 1 / q ^ p')
[PROOF STEP]
show "(\<lambda>k. if k \<in> {0, 1, p'} then 0 else (1 / q) ^ k) sums \<dots>"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>k. if k \<in> {0, 1, p'} then 0 else (1 / q) ^ k) sums (N 1 - 1 / q ^ p')

goal (1 subgoal):
 1. (\<lambda>k. if k \<in> {0, 1, p'} then 0 else (1 / q) ^ k) sums (N 1 - 1 / q ^ p')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k \<in> {0, 1, p'} then 0 else (1 / q) ^ k) sums (N 1 - 1 / q ^ p')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma N_2: "N 2 = 1 / (q ^ 2 * (q - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N 2 = 1 / (q\<^sup>2 * (q - 1))
[PROOF STEP]
using q_gt_1
[PROOF STATE]
proof (prove)
using this:
1 < q

goal (1 subgoal):
 1. N 2 = 1 / (q\<^sup>2 * (q - 1))
[PROOF STEP]
by (auto simp: N_prime N_1 field_simps power2_eq_square)


[STATEMENT]
lemma N_less_N_1:
  assumes "n \<noteq> 1" "n \<noteq> -1"
  shows   "N n < N 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N n < N 1
[PROOF STEP]
proof (cases "n = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> N n < N 1
 2. n \<noteq> 0 \<Longrightarrow> N n < N 1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> N n < N 1
 2. n \<noteq> 0 \<Longrightarrow> N n < N 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> 0
[PROOF STEP]
obtain p where p: "prime p" "p dvd n"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>prime p; p dvd n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prime_divisor_exists[of n] assms
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0
\<lbrakk>n \<noteq> 0; \<not> is_unit n\<rbrakk> \<Longrightarrow> \<exists>b. b dvd n \<and> prime b
n \<noteq> 1
n \<noteq> - 1

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>prime p; p dvd n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
prime p
p dvd n

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> N n < N 1
 2. n \<noteq> 0 \<Longrightarrow> N n < N 1
[PROOF STEP]
hence "N n \<le> N p"
[PROOF STATE]
proof (prove)
using this:
prime p
p dvd n

goal (1 subgoal):
 1. N n \<le> N p
[PROOF STEP]
by (intro N_dvd_mono)
[PROOF STATE]
proof (state)
this:
N n \<le> N p

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> N n < N 1
 2. n \<noteq> 0 \<Longrightarrow> N n < N 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
N n \<le> N p

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> N n < N 1
 2. n \<noteq> 0 \<Longrightarrow> N n < N 1
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
prime p
p dvd n
[PROOF STEP]
have "N p < N 1"
[PROOF STATE]
proof (prove)
using this:
prime p
p dvd n

goal (1 subgoal):
 1. N p < N 1
[PROOF STEP]
using q_gt_1
[PROOF STATE]
proof (prove)
using this:
prime p
p dvd n
1 < q

goal (1 subgoal):
 1. N p < N 1
[PROOF STEP]
by (simp add: N_prime)
[PROOF STATE]
proof (state)
this:
N p < N 1

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> N n < N 1
 2. n \<noteq> 0 \<Longrightarrow> N n < N 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
N n < N 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
N n < N 1

goal (1 subgoal):
 1. N n < N 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
N n < N 1

goal (1 subgoal):
 1. n = 0 \<Longrightarrow> N n < N 1
[PROOF STEP]
qed (use q_gt_1 in \<open>auto simp: N_1\<close>)


[STATEMENT]
lemma nonprime_imp_N_lt:
  assumes "\<not>prime_elem n" "\<bar>n\<bar> \<noteq> 1" "n \<noteq> 0"
  shows   "N n < N 1 - 1 / q ^ nat \<bar>n\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N n < N 1 - 1 / q ^ nat \<bar>n\<bar>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. N n < N 1 - 1 / q ^ nat \<bar>n\<bar>
[PROOF STEP]
obtain p where p: "prime p" "p dvd n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. \<lbrakk>prime p; p dvd n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prime_divisor_exists[of n] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n \<noteq> 0; \<not> is_unit n\<rbrakk> \<Longrightarrow> \<exists>b. b dvd n \<and> prime b
\<not> prime_elem n
\<bar>n\<bar> \<noteq> 1
n \<noteq> 0

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>prime p; p dvd n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prime p
p dvd n

goal (1 subgoal):
 1. N n < N 1 - 1 / q ^ nat \<bar>n\<bar>
[PROOF STEP]
define p' where "p' = nat p"
[PROOF STATE]
proof (state)
this:
p' = nat p

goal (1 subgoal):
 1. N n < N 1 - 1 / q ^ nat \<bar>n\<bar>
[PROOF STEP]
have p': "p = int p'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = int p'
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
prime p
p dvd n

goal (1 subgoal):
 1. p = int p'
[PROOF STEP]
by (auto simp: p'_def prime_ge_0_int)
[PROOF STATE]
proof (state)
this:
p = int p'

goal (1 subgoal):
 1. N n < N 1 - 1 / q ^ nat \<bar>n\<bar>
[PROOF STEP]
have "prime p'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime p'
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
prime p
p dvd n

goal (1 subgoal):
 1. prime p'
[PROOF STEP]
by (simp add: p')
[PROOF STATE]
proof (state)
this:
prime p'

goal (1 subgoal):
 1. N n < N 1 - 1 / q ^ nat \<bar>n\<bar>
[PROOF STEP]
define n' where "n' = nat \<bar>n\<bar>"
[PROOF STATE]
proof (state)
this:
n' = nat \<bar>n\<bar>

goal (1 subgoal):
 1. N n < N 1 - 1 / q ^ nat \<bar>n\<bar>
[PROOF STEP]
have "n' > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < n'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> prime_elem n
\<bar>n\<bar> \<noteq> 1
n \<noteq> 0

goal (1 subgoal):
 1. 1 < n'
[PROOF STEP]
by (auto simp: n'_def)
[PROOF STATE]
proof (state)
this:
1 < n'

goal (1 subgoal):
 1. N n < N 1 - 1 / q ^ nat \<bar>n\<bar>
[PROOF STEP]
have "N n \<le> 1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N n \<le> 1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n'
[PROOF STEP]
proof (rule sums_le)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n. ?f n \<le> ?g n
 2. ?f sums N n
 3. ?g sums (1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n')
[PROOF STEP]
show "(\<lambda>k. if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k) sums N n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>k. if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k) sums N n
[PROOF STEP]
by (rule N_sums)
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k) sums N n

goal (2 subgoals):
 1. \<And>na. (if na = 0 \<or> int na dvd n then 0 else 1 / q ^ na) \<le> ?g na
 2. ?g sums (1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>na. (if na = 0 \<or> int na dvd n then 0 else 1 / q ^ na) \<le> ?g na
 2. ?g sums (1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n')
[PROOF STEP]
from assms p
[PROOF STATE]
proof (chain)
picking this:
\<not> prime_elem n
\<bar>n\<bar> \<noteq> 1
n \<noteq> 0
prime p
p dvd n
[PROOF STEP]
have "n' \<noteq> p'"
[PROOF STATE]
proof (prove)
using this:
\<not> prime_elem n
\<bar>n\<bar> \<noteq> 1
n \<noteq> 0
prime p
p dvd n

goal (1 subgoal):
 1. n' \<noteq> p'
[PROOF STEP]
by (auto simp: n'_def p'_def nat_eq_iff)
[PROOF STATE]
proof (state)
this:
n' \<noteq> p'

goal (2 subgoals):
 1. \<And>na. (if na = 0 \<or> int na dvd n then 0 else 1 / q ^ na) \<le> ?g na
 2. ?g sums (1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n')
[PROOF STEP]
hence "(\<lambda>k. if k \<in> {0, 1, p', n'} then 0 else (1 / q) ^ k) sums
                   (1 / (1 - 1 / q) + (- (1 / q) - (1 / q) ^ p' - (1 / q) ^ n' - 1))"
[PROOF STATE]
proof (prove)
using this:
n' \<noteq> p'

goal (1 subgoal):
 1. (\<lambda>k. if k \<in> {0, 1, p', n'} then 0 else (1 / q) ^ k) sums (1 / (1 - 1 / q) + (- (1 / q) - (1 / q) ^ p' - (1 / q) ^ n' - 1))
[PROOF STEP]
by (intro sums_If_finite_set'[OF geometric_sums])
         (use \<open>prime p'\<close> q_gt_1 prime_gt_Suc_0_nat[of p'] \<open>n' > 1\<close> in \<open>auto simp: \<close>)
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k \<in> {0, 1, p', n'} then 0 else (1 / q) ^ k) sums (1 / (1 - 1 / q) + (- (1 / q) - (1 / q) ^ p' - (1 / q) ^ n' - 1))

goal (2 subgoals):
 1. \<And>na. (if na = 0 \<or> int na dvd n then 0 else 1 / q ^ na) \<le> ?g na
 2. ?g sums (1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k \<in> {0, 1, p', n'} then 0 else (1 / q) ^ k) sums (1 / (1 - 1 / q) + (- (1 / q) - (1 / q) ^ p' - (1 / q) ^ n' - 1))

goal (2 subgoals):
 1. \<And>na. (if na = 0 \<or> int na dvd n then 0 else 1 / q ^ na) \<le> ?g na
 2. ?g sums (1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n')
[PROOF STEP]
have "\<dots> = 1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / (1 - 1 / q) + (- (1 / q) - (1 / q) ^ p' - (1 / q) ^ n' - 1) = 1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n'
[PROOF STEP]
using q_gt_1
[PROOF STATE]
proof (prove)
using this:
1 < q

goal (1 subgoal):
 1. 1 / (1 - 1 / q) + (- (1 / q) - (1 / q) ^ p' - (1 / q) ^ n' - 1) = 1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n'
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
1 / (1 - 1 / q) + (- (1 / q) - (1 / q) ^ p' - (1 / q) ^ n' - 1) = 1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n'

goal (2 subgoals):
 1. \<And>na. (if na = 0 \<or> int na dvd n then 0 else 1 / q ^ na) \<le> ?g na
 2. ?g sums (1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>k. if k \<in> {0, 1, p', n'} then 0 else (1 / q) ^ k) sums (1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n')
[PROOF STEP]
show "(\<lambda>k. if k \<in> {0, 1, p', n'} then 0 else (1 / q) ^ k) sums \<dots>"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>k. if k \<in> {0, 1, p', n'} then 0 else (1 / q) ^ k) sums (1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n')

goal (1 subgoal):
 1. (\<lambda>k. if k \<in> {0, 1, p', n'} then 0 else (1 / q) ^ k) sums (1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k \<in> {0, 1, p', n'} then 0 else (1 / q) ^ k) sums (1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n')

goal (1 subgoal):
 1. \<And>na. (if na = 0 \<or> int na dvd n then 0 else 1 / q ^ na) \<le> (if na \<in> {0, 1, p', n'} then 0 else (1 / q) ^ na)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na. (if na = 0 \<or> int na dvd n then 0 else 1 / q ^ na) \<le> (if na \<in> {0, 1, p', n'} then 0 else (1 / q) ^ na)
[PROOF STEP]
show "\<And>k. (if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k)
         \<le> (if k \<in> {0, 1, p', n'} then 0 else (1 / q) ^ k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. (if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k) \<le> (if k \<in> {0, 1, p', n'} then 0 else (1 / q) ^ k)
[PROOF STEP]
using q_gt_1 p
[PROOF STATE]
proof (prove)
using this:
1 < q
prime p
p dvd n

goal (1 subgoal):
 1. \<And>k. (if k = 0 \<or> int k dvd n then 0 else 1 / q ^ k) \<le> (if k \<in> {0, 1, p', n'} then 0 else (1 / q) ^ k)
[PROOF STEP]
by (auto simp: p'_def n'_def power_divide)
[PROOF STATE]
proof (state)
this:
(if ?k = 0 \<or> int ?k dvd n then 0 else 1 / q ^ ?k) \<le> (if ?k \<in> {0, 1, p', n'} then 0 else (1 / q) ^ ?k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
N n \<le> 1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n'

goal (1 subgoal):
 1. N n < N 1 - 1 / q ^ nat \<bar>n\<bar>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
N n \<le> 1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n'

goal (1 subgoal):
 1. N n < N 1 - 1 / q ^ nat \<bar>n\<bar>
[PROOF STEP]
have "\<dots> < 1 / (q * (q - 1)) - 1 / q ^ n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n' < 1 / (q * (q - 1)) - 1 / q ^ n'
[PROOF STEP]
using q_gt_1
[PROOF STATE]
proof (prove)
using this:
1 < q

goal (1 subgoal):
 1. 1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n' < 1 / (q * (q - 1)) - 1 / q ^ n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 / (q * (q - 1)) - 1 / q ^ p' - 1 / q ^ n' < 1 / (q * (q - 1)) - 1 / q ^ n'

goal (1 subgoal):
 1. N n < N 1 - 1 / q ^ nat \<bar>n\<bar>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
N n < 1 / (q * (q - 1)) - 1 / q ^ n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
N n < 1 / (q * (q - 1)) - 1 / q ^ n'

goal (1 subgoal):
 1. N n < N 1 - 1 / q ^ nat \<bar>n\<bar>
[PROOF STEP]
by (simp add: n'_def N_1)
[PROOF STATE]
proof (state)
this:
N n < N 1 - 1 / q ^ nat \<bar>n\<bar>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prime_iff_N_eq:
  assumes "n \<noteq> 0"
  shows   "prime_elem n \<longleftrightarrow> N n = N 1 - 1 / q ^ nat \<bar>n\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
have *: "prime_elem n \<longleftrightarrow> N n = N 1 - 1 / q ^ nat \<bar>n\<bar>" if "n > 0" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
consider "n = 1" | "prime n" | "\<not>prime n" "n > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = 1 \<Longrightarrow> thesis; prime n \<Longrightarrow> thesis; \<lbrakk>\<not> prime n; 1 < n\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using \<open>n > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. \<lbrakk>n = 1 \<Longrightarrow> thesis; prime n \<Longrightarrow> thesis; \<lbrakk>\<not> prime n; 1 < n\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>n = 1 \<Longrightarrow> ?thesis; prime n \<Longrightarrow> ?thesis; \<lbrakk>\<not> prime n; 1 < n\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n = 1 \<Longrightarrow> ?thesis; prime n \<Longrightarrow> ?thesis; \<lbrakk>\<not> prime n; 1 < n\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. n = 1 \<Longrightarrow> prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
 2. prime n \<Longrightarrow> prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
 3. \<lbrakk>\<not> prime n; 1 < n\<rbrakk> \<Longrightarrow> prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
assume "n = 1"
[PROOF STATE]
proof (state)
this:
n = 1

goal (3 subgoals):
 1. n = 1 \<Longrightarrow> prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
 2. prime n \<Longrightarrow> prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
 3. \<lbrakk>\<not> prime n; 1 < n\<rbrakk> \<Longrightarrow> prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 1

goal (1 subgoal):
 1. prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
using q_gt_1
[PROOF STATE]
proof (prove)
using this:
n = 1
1 < q

goal (1 subgoal):
 1. prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
by (auto simp: N_1)
[PROOF STATE]
proof (state)
this:
prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)

goal (2 subgoals):
 1. prime n \<Longrightarrow> prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
 2. \<lbrakk>\<not> prime n; 1 < n\<rbrakk> \<Longrightarrow> prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. prime n \<Longrightarrow> prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
 2. \<lbrakk>\<not> prime n; 1 < n\<rbrakk> \<Longrightarrow> prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
assume n: "\<not>prime n" "n > 1"
[PROOF STATE]
proof (state)
this:
\<not> prime n
1 < n

goal (2 subgoals):
 1. prime n \<Longrightarrow> prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
 2. \<lbrakk>\<not> prime n; 1 < n\<rbrakk> \<Longrightarrow> prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
with nonprime_imp_N_lt[of n]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> prime_elem n; \<bar>n\<bar> \<noteq> 1; n \<noteq> 0\<rbrakk> \<Longrightarrow> N n < N 1 - 1 / q ^ nat \<bar>n\<bar>
\<not> prime n
1 < n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> prime_elem n; \<bar>n\<bar> \<noteq> 1; n \<noteq> 0\<rbrakk> \<Longrightarrow> N n < N 1 - 1 / q ^ nat \<bar>n\<bar>
\<not> prime n
1 < n

goal (1 subgoal):
 1. prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)

goal (1 subgoal):
 1. prime n \<Longrightarrow> prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
qed (auto simp: N_prime prime_ge_0_int)
[PROOF STATE]
proof (state)
this:
prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < ?n \<Longrightarrow> prime_elem ?n = (N ?n = N 1 - 1 / q ^ nat \<bar>?n\<bar>)

goal (1 subgoal):
 1. prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
proof (cases "n > 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < n \<Longrightarrow> prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
 2. \<not> 0 < n \<Longrightarrow> prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 < n

goal (2 subgoals):
 1. 0 < n \<Longrightarrow> prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
 2. \<not> 0 < n \<Longrightarrow> prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
0 < ?n \<Longrightarrow> prime_elem ?n = (N ?n = N 1 - 1 / q ^ nat \<bar>?n\<bar>)
0 < n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < ?n \<Longrightarrow> prime_elem ?n = (N ?n = N 1 - 1 / q ^ nat \<bar>?n\<bar>)
0 < n

goal (1 subgoal):
 1. prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)

goal (1 subgoal):
 1. \<not> 0 < n \<Longrightarrow> prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 < n \<Longrightarrow> prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 < n

goal (1 subgoal):
 1. \<not> 0 < n \<Longrightarrow> prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
with *[of "-n"] assms
[PROOF STATE]
proof (chain)
picking this:
0 < - n \<Longrightarrow> prime_elem (- n) = (N (- n) = N 1 - 1 / q ^ nat \<bar>- n\<bar>)
n \<noteq> 0
\<not> 0 < n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < - n \<Longrightarrow> prime_elem (- n) = (N (- n) = N 1 - 1 / q ^ nat \<bar>- n\<bar>)
n \<noteq> 0
\<not> 0 < n

goal (1 subgoal):
 1. prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
prime_elem n = (N n = N 1 - 1 / q ^ nat \<bar>n\<bar>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma N_fact_le: "N (fact m) \<le> 1 / (q - 1) * 1 / q ^ m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N (fact m) \<le> 1 / (q - 1) * 1 / q ^ m
[PROOF STEP]
proof (rule sums_le[OF _ N_sums])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. (if n = 0 \<or> int n dvd fact m then 0 else 1 / q ^ n) \<le> ?g n
 2. ?g sums (1 / (q - 1) * 1 / q ^ m)
[PROOF STEP]
have "(\<lambda>k. 1 / q ^ k / q ^ Suc m) sums (q / (q - 1) / q ^ Suc m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>k. 1 / q ^ k / q ^ Suc m) sums (q / (q - 1) / q ^ Suc m)
[PROOF STEP]
using geometric_sums[of "1 / q"] q_gt_1
[PROOF STATE]
proof (prove)
using this:
norm (1 / q) < 1 \<Longrightarrow> (^) (1 / q) sums (1 / (1 - 1 / q))
1 < q

goal (1 subgoal):
 1. (\<lambda>k. 1 / q ^ k / q ^ Suc m) sums (q / (q - 1) / q ^ Suc m)
[PROOF STEP]
by (intro sums_divide) (auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
(\<lambda>k. 1 / q ^ k / q ^ Suc m) sums (q / (q - 1) / q ^ Suc m)

goal (2 subgoals):
 1. \<And>n. (if n = 0 \<or> int n dvd fact m then 0 else 1 / q ^ n) \<le> ?g n
 2. ?g sums (1 / (q - 1) * 1 / q ^ m)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>k. 1 / q ^ k / q ^ Suc m) sums (q / (q - 1) / q ^ Suc m)

goal (2 subgoals):
 1. \<And>n. (if n = 0 \<or> int n dvd fact m then 0 else 1 / q ^ n) \<le> ?g n
 2. ?g sums (1 / (q - 1) * 1 / q ^ m)
[PROOF STEP]
have "(q / (q - 1) / q ^ Suc m) = 1 / (q - 1) * 1 / q ^ m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q / (q - 1) / q ^ Suc m = 1 / (q - 1) * 1 / q ^ m
[PROOF STEP]
using q_gt_1
[PROOF STATE]
proof (prove)
using this:
1 < q

goal (1 subgoal):
 1. q / (q - 1) / q ^ Suc m = 1 / (q - 1) * 1 / q ^ m
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
q / (q - 1) / q ^ Suc m = 1 / (q - 1) * 1 / q ^ m

goal (2 subgoals):
 1. \<And>n. (if n = 0 \<or> int n dvd fact m then 0 else 1 / q ^ n) \<le> ?g n
 2. ?g sums (1 / (q - 1) * 1 / q ^ m)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
q / (q - 1) / q ^ Suc m = 1 / (q - 1) * 1 / q ^ m

goal (2 subgoals):
 1. \<And>n. (if n = 0 \<or> int n dvd fact m then 0 else 1 / q ^ n) \<le> ?g n
 2. ?g sums (1 / (q - 1) * 1 / q ^ m)
[PROOF STEP]
have "(\<lambda>k. 1 / q ^ k / q ^ Suc m) = (\<lambda>k. 1 / q ^ (k + Suc m))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>k. 1 / q ^ k / q ^ Suc m) = (\<lambda>k. 1 / q ^ (k + Suc m))
[PROOF STEP]
using q_gt_1
[PROOF STATE]
proof (prove)
using this:
1 < q

goal (1 subgoal):
 1. (\<lambda>k. 1 / q ^ k / q ^ Suc m) = (\<lambda>k. 1 / q ^ (k + Suc m))
[PROOF STEP]
by (simp add: field_simps power_add)
[PROOF STATE]
proof (state)
this:
(\<lambda>k. 1 / q ^ k / q ^ Suc m) = (\<lambda>k. 1 / q ^ (k + Suc m))

goal (2 subgoals):
 1. \<And>n. (if n = 0 \<or> int n dvd fact m then 0 else 1 / q ^ n) \<le> ?g n
 2. ?g sums (1 / (q - 1) * 1 / q ^ m)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>k. 1 / q ^ k / q ^ Suc m) = (\<lambda>k. 1 / q ^ (k + Suc m))

goal (2 subgoals):
 1. \<And>n. (if n = 0 \<or> int n dvd fact m then 0 else 1 / q ^ n) \<le> ?g n
 2. ?g sums (1 / (q - 1) * 1 / q ^ m)
[PROOF STEP]
have "\<dots> = (\<lambda>k. if k + Suc m \<le> m then 0 else 1 / q ^ (k + Suc m))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>k. 1 / q ^ (k + Suc m)) = (\<lambda>k. if k + Suc m \<le> m then 0 else 1 / q ^ (k + Suc m))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>k. 1 / q ^ (k + Suc m)) = (\<lambda>k. if k + Suc m \<le> m then 0 else 1 / q ^ (k + Suc m))

goal (2 subgoals):
 1. \<And>n. (if n = 0 \<or> int n dvd fact m then 0 else 1 / q ^ n) \<le> ?g n
 2. ?g sums (1 / (q - 1) * 1 / q ^ m)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>k. if k + Suc m \<le> m then 0 else 1 / q ^ (k + Suc m)) sums (1 / (q - 1) * 1 / q ^ m)
[PROOF STEP]
have "\<dots> sums (1 / (q - 1) * 1 / q ^ m)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>k. if k + Suc m \<le> m then 0 else 1 / q ^ (k + Suc m)) sums (1 / (q - 1) * 1 / q ^ m)

goal (1 subgoal):
 1. (\<lambda>k. if k + Suc m \<le> m then 0 else 1 / q ^ (k + Suc m)) sums (1 / (q - 1) * 1 / q ^ m)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k + Suc m \<le> m then 0 else 1 / q ^ (k + Suc m)) sums (1 / (q - 1) * 1 / q ^ m)

goal (2 subgoals):
 1. \<And>n. (if n = 0 \<or> int n dvd fact m then 0 else 1 / q ^ n) \<le> ?g n
 2. ?g sums (1 / (q - 1) * 1 / q ^ m)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k + Suc m \<le> m then 0 else 1 / q ^ (k + Suc m)) sums (1 / (q - 1) * 1 / q ^ m)

goal (2 subgoals):
 1. \<And>n. (if n = 0 \<or> int n dvd fact m then 0 else 1 / q ^ n) \<le> ?g n
 2. ?g sums (1 / (q - 1) * 1 / q ^ m)
[PROOF STEP]
have "?this \<longleftrightarrow> (\<lambda>k. if k \<le> m then 0 else 1 / q ^ k) sums (1 / (q - 1) * 1 / q ^ m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>k. if k + Suc m \<le> m then 0 else 1 / q ^ (k + Suc m)) sums (1 / (q - 1) * 1 / q ^ m) = (\<lambda>k. if k \<le> m then 0 else 1 / q ^ k) sums (1 / (q - 1) * 1 / q ^ m)
[PROOF STEP]
by (rule sums_zero_iff_shift) auto
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k + Suc m \<le> m then 0 else 1 / q ^ (k + Suc m)) sums (1 / (q - 1) * 1 / q ^ m) = (\<lambda>k. if k \<le> m then 0 else 1 / q ^ k) sums (1 / (q - 1) * 1 / q ^ m)

goal (2 subgoals):
 1. \<And>n. (if n = 0 \<or> int n dvd fact m then 0 else 1 / q ^ n) \<le> ?g n
 2. ?g sums (1 / (q - 1) * 1 / q ^ m)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>k. if k \<le> m then 0 else 1 / q ^ k) sums (1 / (q - 1) * 1 / q ^ m)
[PROOF STEP]
show \<dots>
[PROOF STATE]
proof (prove)
using this:
(\<lambda>k. if k \<le> m then 0 else 1 / q ^ k) sums (1 / (q - 1) * 1 / q ^ m)

goal (1 subgoal):
 1. (\<lambda>k. if k \<le> m then 0 else 1 / q ^ k) sums (1 / (q - 1) * 1 / q ^ m)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>k. if k \<le> m then 0 else 1 / q ^ k) sums (1 / (q - 1) * 1 / q ^ m)

goal (1 subgoal):
 1. \<And>n. (if n = 0 \<or> int n dvd fact m then 0 else 1 / q ^ n) \<le> (if n \<le> m then 0 else 1 / q ^ n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. (if n = 0 \<or> int n dvd fact m then 0 else 1 / q ^ n) \<le> (if n \<le> m then 0 else 1 / q ^ n)
[PROOF STEP]
fix k :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. (if n = 0 \<or> int n dvd fact m then 0 else 1 / q ^ n) \<le> (if n \<le> m then 0 else 1 / q ^ n)
[PROOF STEP]
have "int k dvd fact m" if "k > 0" "k \<le> m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int k dvd fact m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. int k dvd fact m
[PROOF STEP]
have "int k dvd int (fact m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int k dvd int (fact m)
[PROOF STEP]
unfolding int_dvd_int_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k dvd fact m
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
0 < k
k \<le> m

goal (1 subgoal):
 1. k dvd fact m
[PROOF STEP]
by (simp add: dvd_fact)
[PROOF STATE]
proof (state)
this:
int k dvd int (fact m)

goal (1 subgoal):
 1. int k dvd fact m
[PROOF STEP]
thus "int k dvd fact m"
[PROOF STATE]
proof (prove)
using this:
int k dvd int (fact m)

goal (1 subgoal):
 1. int k dvd fact m
[PROOF STEP]
unfolding of_nat_fact
[PROOF STATE]
proof (prove)
using this:
int k dvd fact m

goal (1 subgoal):
 1. int k dvd fact m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
int k dvd fact m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> int k dvd fact m

goal (1 subgoal):
 1. \<And>n. (if n = 0 \<or> int n dvd fact m then 0 else 1 / q ^ n) \<le> (if n \<le> m then 0 else 1 / q ^ n)
[PROOF STEP]
thus "(if k = 0 \<or> int k dvd fact m then 0 else 1 / q ^ k) \<le>
        (if k \<le> m then 0 else 1 / q ^ k)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> int k dvd fact m

goal (1 subgoal):
 1. (if k = 0 \<or> int k dvd fact m then 0 else 1 / q ^ k) \<le> (if k \<le> m then 0 else 1 / q ^ k)
[PROOF STEP]
using q_gt_1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < k; k \<le> m\<rbrakk> \<Longrightarrow> int k dvd fact m
1 < q

goal (1 subgoal):
 1. (if k = 0 \<or> int k dvd fact m then 0 else 1 / q ^ k) \<le> (if k \<le> m then 0 else 1 / q ^ k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(if k = 0 \<or> int k dvd fact m then 0 else 1 / q ^ k) \<le> (if k \<le> m then 0 else 1 / q ^ k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma N_prime_mono:
  assumes "prime p" "prime p'" "p \<le> p'"
  shows   "N p \<le> N p'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N p \<le> N p'
[PROOF STEP]
using assms q_gt_1
[PROOF STATE]
proof (prove)
using this:
prime p
prime p'
p \<le> p'
1 < q

goal (1 subgoal):
 1. N p \<le> N p'
[PROOF STEP]
by (auto simp add: N_prime field_simps nat_le_iff prime_ge_0_int)


[STATEMENT]
lemma N_prime_ge:
  assumes "prime p"
  shows   "N p \<ge> 1 / (q\<^sup>2 * (q - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / (q\<^sup>2 * (q - 1)) \<le> N p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 / (q\<^sup>2 * (q - 1)) \<le> N p
[PROOF STEP]
have "1 / (q ^ 2 * (q - 1)) = N 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / (q\<^sup>2 * (q - 1)) = N 2
[PROOF STEP]
using q_gt_1
[PROOF STATE]
proof (prove)
using this:
1 < q

goal (1 subgoal):
 1. 1 / (q\<^sup>2 * (q - 1)) = N 2
[PROOF STEP]
by (auto simp: N_prime N_1 field_simps power2_eq_square)
[PROOF STATE]
proof (state)
this:
1 / (q\<^sup>2 * (q - 1)) = N 2

goal (1 subgoal):
 1. 1 / (q\<^sup>2 * (q - 1)) \<le> N p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 / (q\<^sup>2 * (q - 1)) = N 2

goal (1 subgoal):
 1. 1 / (q\<^sup>2 * (q - 1)) \<le> N p
[PROOF STEP]
have "\<dots> \<le> N p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N 2 \<le> N p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prime p

goal (1 subgoal):
 1. N 2 \<le> N p
[PROOF STEP]
by (intro N_prime_mono) (auto simp: prime_ge_2_int)
[PROOF STATE]
proof (state)
this:
N 2 \<le> N p

goal (1 subgoal):
 1. 1 / (q\<^sup>2 * (q - 1)) \<le> N p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
1 / (q\<^sup>2 * (q - 1)) \<le> N p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 / (q\<^sup>2 * (q - 1)) \<le> N p

goal (1 subgoal):
 1. 1 / (q\<^sup>2 * (q - 1)) \<le> N p
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
1 / (q\<^sup>2 * (q - 1)) \<le> N p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma N_prime_elem_ge:
  assumes "prime_elem p"
  shows   "N p \<ge> 1 / (q\<^sup>2 * (q - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / (q\<^sup>2 * (q - 1)) \<le> N p
[PROOF STEP]
proof (cases "p \<ge> 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> p \<Longrightarrow> 1 / (q\<^sup>2 * (q - 1)) \<le> N p
 2. \<not> 0 \<le> p \<Longrightarrow> 1 / (q\<^sup>2 * (q - 1)) \<le> N p
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 \<le> p

goal (2 subgoals):
 1. 0 \<le> p \<Longrightarrow> 1 / (q\<^sup>2 * (q - 1)) \<le> N p
 2. \<not> 0 \<le> p \<Longrightarrow> 1 / (q\<^sup>2 * (q - 1)) \<le> N p
[PROOF STEP]
with assms N_prime_ge
[PROOF STATE]
proof (chain)
picking this:
prime_elem p
prime ?p \<Longrightarrow> 1 / (q\<^sup>2 * (q - 1)) \<le> N ?p
0 \<le> p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prime_elem p
prime ?p \<Longrightarrow> 1 / (q\<^sup>2 * (q - 1)) \<le> N ?p
0 \<le> p

goal (1 subgoal):
 1. 1 / (q\<^sup>2 * (q - 1)) \<le> N p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 / (q\<^sup>2 * (q - 1)) \<le> N p

goal (1 subgoal):
 1. \<not> 0 \<le> p \<Longrightarrow> 1 / (q\<^sup>2 * (q - 1)) \<le> N p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 \<le> p \<Longrightarrow> 1 / (q\<^sup>2 * (q - 1)) \<le> N p
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 \<le> p

goal (1 subgoal):
 1. \<not> 0 \<le> p \<Longrightarrow> 1 / (q\<^sup>2 * (q - 1)) \<le> N p
[PROOF STEP]
with assms N_prime_ge[of "-p"]
[PROOF STATE]
proof (chain)
picking this:
prime_elem p
prime (- p) \<Longrightarrow> 1 / (q\<^sup>2 * (q - 1)) \<le> N (- p)
\<not> 0 \<le> p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prime_elem p
prime (- p) \<Longrightarrow> 1 / (q\<^sup>2 * (q - 1)) \<le> N (- p)
\<not> 0 \<le> p

goal (1 subgoal):
 1. 1 / (q\<^sup>2 * (q - 1)) \<le> N p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 / (q\<^sup>2 * (q - 1)) \<le> N p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dist_self [simp]: "dist x x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.dist x x = 0
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma dist_sym [simp]: "dist x y = dist y x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.dist x y = local.dist y x
[PROOF STEP]
by transfer (simp add: N_minus_commute)


[STATEMENT]
lemma dist_pos: "x \<noteq> y \<Longrightarrow> dist x y > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> 0 < local.dist x y
[PROOF STEP]
by transfer (use N_pos in simp)


[STATEMENT]
lemma dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (local.dist x y = 0) = (x = y)
[PROOF STEP]
using dist_pos[of x y]
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y \<Longrightarrow> 0 < local.dist x y

goal (1 subgoal):
 1. (local.dist x y = 0) = (x = y)
[PROOF STEP]
by (cases "x = y") auto


[STATEMENT]
lemma dist_triangle_ineq: "dist x z \<le> dist x y + dist y z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.dist x z \<le> local.dist x y + local.dist y z
[PROOF STEP]
proof transfer
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x z y. N (x - z) \<le> N (x - y) + N (y - z)
[PROOF STEP]
fix x y z :: int
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x z y. N (x - z) \<le> N (x - y) + N (y - z)
[PROOF STEP]
show "N (x - z) \<le> N (x - y) + N (y - z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N (x - z) \<le> N (x - y) + N (y - z)
[PROOF STEP]
using N_triangle_ineq[of "x - y" "y - z"]
[PROOF STATE]
proof (prove)
using this:
N (x - y + (y - z)) \<le> N (x - y) + N (y - z)

goal (1 subgoal):
 1. N (x - z) \<le> N (x - y) + N (y - z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
N (x - z) \<le> N (x - y) + N (y - z)

goal:
No subgoals!
[PROOF STEP]
qed