IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory IntGroup_ZF imports Group_ZF_2 Int_ZF_1

begin

In the Monoid_ZF_1 theory we consider multiplicities of $n\cdot x$ of monoid elements, i.e. special cases of expressions of the form $x_1\oplus x_2\oplus\dots\oplus x_n$ where $x_i=x$ for $i=1..n$. In the group context where we usually use multiplicative notation this translates to the "power" $x^n$ where $n\in \mathbb{N}$, see also section "Product of a list of group elements" in the Group_ZF theory. In the group setting the notion of raising an element to natural power can be naturally generalized to the notion of raising an element to an integer power.

Properties of natural powers of an element and its inverse

The integer power is defined in terms of natural powers of an element and its inverse. In this section we study properties of expressions $(x^n)\cdot(x^{-1})^k$, where $x$ is a group element and $n,k$ are natural numbers.

The natural power of $x$ multiplied by the same power of $x^{-1}$ cancel out to give the neutral element of the group.

lemma (in group0) nat_pow_inv_cancel:

assumes $ n\in nat $, $ x\in G $

shows $ x^{n}\cdot (x^{-1})^{n} = 1 $proof

from assms(1) have $ n\in nat $ and $ x^{0}\cdot (x^{-1})^{0} = 1 $ using nat_mult_zero, group0_2_L2

moreover

have $ \forall k\in nat.\ x^{k}\cdot (x^{-1})^{k} = 1 \longrightarrow x^{k + 1}\cdot (x^{-1})^{k + 1} = 1 $proof

{

fix $ k $

assume $ k\in nat $ and $ x^{k}\cdot (x^{-1})^{k} = 1 $

from assms(2), $ k\in nat $ have $ x^{k + 1}\cdot (x^{-1})^{k + 1} = x^{k}\cdot x\cdot (x^{-1}\cdot (x^{-1})^{k}) $ using inverse_in_group, nat_pow_add_one

with assms(2), $ k\in nat $, $ x^{k}\cdot (x^{-1})^{k} = 1 $ have $ x^{k + 1}\cdot (x^{-1})^{k + 1} = 1 $ using nat_mult_type, inverse_in_group, rearr4elem_monoid, group0_2_L6(1), group0_2_L2

}

thus $ thesis $

qed

ultimately show $ thesis $ by (rule ind_on_nat1 )

qed

The natural power of $x^{-1}$ multiplied by the same power of $x$ cancel out to give the neutral element of the group. Same as nat_pow_inv_cancel written with $x^{-1}$ instead of $x$.

lemma (in group0) nat_pow_inv_cancel1:

assumes $ n\in nat $, $ x\in G $

shows $ (x^{-1})^{n}\cdot x^{n} = 1 $proof

from assms have $ (x^{-1})^{n}\cdot ((x^{-1})^{-1})^{n} = 1 $ using inverse_in_group, nat_pow_inv_cancel

with assms(2) show $ (x^{-1})^{n}\cdot x^{n} = 1 $ using group_inv_of_inv

qed

If $k\leq n$ are natural numbers and $x$ an element of the group, then $x^n\cdot (x^{-1})^k = x^(k-n)$.

lemma (in group0) nat_pow_cancel_less:

assumes $ n\in nat $, $ k\leq n $, $ x\in G $

shows $ x^{n}\cdot (x^{-1})^{k} = x^{n - k} $proof

from assms have $ k\in nat $, $ n - k \in nat $, $ x^{(n - k)} \in G $, $ x^{k} \in G $, $ (x^{-1})^{k} \in G $ using leq_nat_is_nat, diff_type, nat_mult_type, inverse_in_group

from assms(3), $ k\in nat $, $ n - k \in nat $ have $ x^{(n - k) + k} = x^{(n - k)}\cdot x^{k} $ using nat_mult_add

with assms(1,2), $ x^{(n - k)} \in G $, $ x^{k} \in G $, $ (x^{-1})^{k} \in G $ have $ x^{n}\cdot (x^{-1})^{k} = x^{n - k}\cdot (x^{k}\cdot (x^{-1})^{k}) $ using add_diff_inverse2, group_oper_assoc

with assms(3), $ k\in nat $, $ x^{(n - k)} \in G $ show $ thesis $ using nat_pow_inv_cancel, group0_2_L2

qed

If $k\leq n$ are natural numbers and $x$ an element of the group, then $(x^{-1})^n\cdot x^k = (x^{-1})^(k-n)$.

lemma (in group0) nat_pow_cancel_less1:

assumes $ n\in nat $, $ k\leq n $, $ x\in G $

shows $ (x^{-1})^{n}\cdot x^{k} = (x^{-1})^{n - k} $proof

from assms have $ (x^{-1})^{n}\cdot ((x^{-1})^{-1})^{k} = (x^{-1})^{n - k} $ using inverse_in_group, nat_pow_cancel_less

with assms(3) show $ thesis $ using group_inv_of_inv

qed

If $k\leq n$ are natural numbers and $x$ an element of the group, then $x^k\cdot (x^{-1})^n = (x^{-1})^(k-n)$.

lemma (in group0) nat_pow_cancel_more:

assumes $ n\in nat $, $ k\leq n $, $ x\in G $

shows $ (x^{-1})^{k}\cdot x^{n} = x^{n - k} $proof

from assms have $ k\in nat $, $ n - k \in nat $, $ x^{(n - k)} \in G $, $ x^{k} \in G $, $ (x^{-1})^{k} \in G $ using leq_nat_is_nat, diff_type, nat_mult_type, inverse_in_group

from assms(3), $ k\in nat $, $ n - k \in nat $ have $ x^{k + (n - k)} = x^{k}\cdot x^{(n - k)} $ using nat_mult_add

with assms(1,2), $ x^{(n - k)} \in G $, $ x^{k} \in G $, $ (x^{-1})^{k} \in G $ have $ (x^{-1})^{k}\cdot x^{n} = ((x^{-1})^{k}\cdot x^{k})\cdot x^{n - k} $ using add_diff_inverse, group_oper_assoc

with assms(3), $ k\in nat $, $ x^{(n - k)} \in G $ show $ thesis $ using nat_pow_inv_cancel1, group0_2_L2

qed

If $k\leq n$ are natural numbers and $x$ an element of the group, then $(x^{-1})^k\cdot x^n = x^{(k-n)}$.

lemma (in group0) nat_pow_cancel_more1:

assumes $ n\in nat $, $ k\leq n $, $ x\in G $

shows $ x^{k}\cdot (x^{-1})^{n} = (x^{-1})^{n - k} $proof

from assms have $ ((x^{-1})^{-1})^{k}\cdot (x^{-1})^{n} = (x^{-1})^{n - k} $ using inverse_in_group, nat_pow_cancel_more

with assms(3) show $ thesis $ using group_inv_of_inv

qed

Integer powers

In this section we introduce notation basic properties of integer power in group context. The goal is to show that the power homomorphism property: if $x$ is an element of the group and $n,m$ are integers then $x^{n+m}=x^n\cdot x^m$.

We extend the group0 context with some notation from int0 context. Since we inherit the multiplicative notation from the group0 context the integer "one" is denoted $ 1 _Z $ rather than just $ 1 $ (which is the group's neutral element).

locale group_int0 = group0 +

defines $ \mathbb{Z} \equiv int $

defines $ a + b \equiv IntegerAddition\langle a,b\rangle $

defines $ - a \equiv \text{GroupInv}(\mathbb{Z} ,IntegerAddition)(a) $

defines $ a - b \equiv a + ( - b) $

defines $ 0 \equiv \text{ TheNeutralElement}(\mathbb{Z} ,IntegerAddition) $

defines $ 1 _Z \equiv \text{ TheNeutralElement}(\mathbb{Z} ,IntegerMultiplication) $

defines $ \mathbb{Z} ^+ \equiv \text{Nonnegative}(\mathbb{Z} ,IntegerAddition,IntegerOrder) $

defines $ m \leq n \equiv \langle m,n\rangle \in IntegerOrder $

defines $ a \lt b \equiv a\leq b \wedge a\neq b $

Next define notation for the integer power $ x^{z} $. The difficulty here is that in ZF set theory nonnegative integers and natural numbers are different things. So, we use the notion of zmagnitude defined in the standard Isabelle/ZF Int theory. For an integer number $z$, $ | z|_N $ is like absolute value of $z$ but interpreted as a natural number. Hence, we define the integer power $ x^{z} $ as $x$ raised to the magnitude of $z$ if $z$ is nonnegative or $x^{-1}$ raised to the same natural power otherwise.

definition (in group_int0)

$ x^{z} \equiv (\text{if } 0 \leq z\text{ then }x\text{ else }x^{-1})^{| z|_N } $

An integer power of a group element is in the group.

lemma (in group_int0) powz_type:

assumes $ z\in \mathbb{Z} $, $ x\in G $

shows $ x^{z} \in G $ using assms, zmagnitude_type, nat_mult_type, inverse_in_group unfolding powz_def

A group element raised to (integer) zero'th power is equal to the group's neutral element. An element raised to (integer) power one is the same element.

lemma (in group_int0) int_power_zero_one:

assumes $ x\in G $

shows $ x^{ 0 } = 1 $ and $ x^{1 _Z} = x $ using assms, Int_ZF_1_L8A(1), int_ord_is_refl1, zmag_zero_one, nat_mult_zero, Int_ZF_2_L16A(1), nat_mult_one unfolding powz_def

If $x$ is an element of the group and $z_1,z_2$ are nonnegative integers then $x^{z_1+z_2}=x^{z_1}\cdot x^{z_2}$, i.e. the power homomorphism property holds.

lemma (in group_int0) powz_hom_nneg_nneg:

assumes $ 0 \leq z_1 $, $ 0 \leq z_2 $, $ x\in G $

shows $ x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} $ using assms, add_nonneg_ints(1,2), nat_mult_add unfolding powz_def

If $x$ is an element of the group and $z_1,z_2$ are negative integers then the power homomorphism property holds.

lemma (in group_int0) powz_hom_neg_neg:

assumes $ z_1 \lt 0 $, $ z_2 \lt 0 $, $ x\in G $

shows $ x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} $ using assms, neg_not_nonneg, add_neg_ints(1,2), inverse_in_group, nat_mult_add unfolding powz_def

When the integers are of different signs we further split into cases depending on which magnitude is greater. If $x$ is an element of the group and $z_1$ is nonnegative, $z_2$ is negative and $|z_2|\leq |z_1|$ then the power homomorphism property holds. The proof of this lemma is presented with more detail than necessary, to show the schema of the proofs of the remaining lemmas that we let Isabelle prove automatically.

lemma (in group_int0) powz_hom_nneg_neg1:

assumes $ 0 \leq z_1 $, $ z_2 \lt 0 $, $ \left| z_2 \right|_N \leq \left| z_1 \right|_N $, $ x\in G $

shows $ x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} $proof

let $ m_1 = \left| z_1 \right|_N $

let $ m_2 = \left| z_2 \right|_N $

from assms(1,2,3) have $ x^{z_1 + z_2} = x^{\left| z_1 + z_2 \right|_N } $ using add_nonneg_neg1(1) unfolding powz_def

also

from assms(1,2,3) have $ .\ .\ .\ = x^{m_1 - m_2} $ using add_nonneg_neg1(2)

also

from assms(3,4) have $ .\ .\ .\ = x^{m_1}\cdot (x^{-1})^{m_2} $ using nat_pow_cancel_less

also

from assms(1,2) have $ .\ .\ .\ = x^{z_1}\cdot x^{z_2} $ using neg_not_nonneg unfolding powz_def

finally show $ thesis $

qed

If $x$ is an element of the group and $z_1$ is nonnegative, $z_2$ is negative and $|z_1|<|z_2|$ then the power homomorphism property holds.

lemma (in group_int0) powz_hom_nneg_neg2:

assumes $ 0 \leq z_1 $, $ z_2 \lt 0 $, $ \left| z_1 \right|_N \lt \left| z_2 \right|_N $, $ x\in G $

shows $ x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} $ using assms, add_nonneg_neg2, neg_not_nonneg, leI, nat_pow_cancel_more1 unfolding powz_def

If $x$ is an element of the group and $z_1$ is negative, $z_2$ is nonnegative and $|z_1|\leq |z_2|$ then the power homomorphism property holds.

lemma (in group_int0) powz_hom_neg_nneg1:

assumes $ z_1 \lt 0 $, $ 0 \leq z_2 $, $ \left| z_1 \right|_N \leq \left| z_2 \right|_N $, $ x\in G $

shows $ x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} $ using assms, add_neg_nonneg1, nat_pow_cancel_more, neg_not_nonneg unfolding powz_def

If $x$ is an element of the group and $z_1$ is negative, $z_2$ is nonnegative and $|z_2| < |z_1|$ then the power homomorphism property holds.

lemma (in group_int0) powz_hom_neg_nneg2:

assumes $ z_1 \lt 0 $, $ 0 \leq z_2 $, $ \left| z_2 \right|_N \lt \left| z_1 \right|_N $, $ x\in G $

shows $ x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} $ using assms, add_neg_nonneg2, neg_not_nonneg, leI, nat_pow_cancel_less1 unfolding powz_def

The next theorem collects the results from the above lemmas to show the power homomorphism property holds for any pair of integer numbers and any group element.

theorem (in group_int0) powz_hom_prop:

assumes $ z_1\in \mathbb{Z} $, $ z_2\in \mathbb{Z} $, $ x\in G $

shows $ x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} $proof

with assms(3) show $ thesis $ using powz_hom_nneg_nneg, powz_hom_neg_neg, powz_hom_nneg_neg1, powz_hom_nneg_neg2, powz_hom_neg_nneg1, powz_hom_neg_nneg2

qed

A group element raised to power $-1$ is the inverse of that group element.

lemma (in group_int0) inpt_power_neg_one:

assumes $ x\in G $

shows $ x^{ - 1 _Z} = x^{-1} $ using assms, neg_not_nonneg, neg_one_less_zero, zmag_opposite_same(2), Int_ZF_1_L8A(2), zmag_zero_one(2), inverse_in_group, nat_mult_one unfolding powz_def

Increasing the (integer) power by one is the same as multiplying by the group element.

lemma (in group_int0) int_power_add_one:

assumes $ z\in \mathbb{Z} $, $ x\in G $

shows $ x^{z + 1 _Z} = x^{z}\cdot x $ using assms, Int_ZF_1_L8A(2), powz_hom_prop, int_power_zero_one(2)

For integer power taking a negative of the exponent is the same as taking inverse of the group element.

lemma (in group_int0) minus_exp_inv_base:

assumes $ z\in \mathbb{Z} $, $ x\in G $

shows $ x^{ - z} = (x^{-1})^{z} $proof

from assms(1) have $ 0 \lt z \vee z= 0 \vee z \lt 0 $ using int_neg_zero_pos

moreover

from assms(1) have $ 0 \lt z \longrightarrow x^{ - z} = (x^{-1})^{z} $ using neg_pos_int_neg, neg_not_nonneg, zmag_opposite_same(2) unfolding powz_def

moreover

from assms(2) have $ z= 0 \longrightarrow x^{ - z} = (x^{-1})^{z} $ using Int_ZF_1_L11, int_power_zero_one(1), inverse_in_group

moreover

from assms have $ z \lt 0 \longrightarrow x^{ - z} = (x^{-1})^{z} $ using neg_not_nonneg, neg_neg_int_pos, group_inv_of_inv, zmag_opposite_same(2) unfolding powz_def

ultimately show $ x^{ - z} = (x^{-1})^{z} $

qed

Integer power of a group element is the same as the inverse of the element raised to negative of the exponent.

lemma (in group_int0) minus_exp_inv_base1:

assumes $ z\in \mathbb{Z} $, $ x\in G $

shows $ x^{z} = (x^{-1})^{ - z} $proof

from assms(1) have $ ( - z)\in \mathbb{Z} $ using int_neg_type

with assms show $ thesis $ using minus_exp_inv_base, neg_neg_noop

qed

The next context is like group_int0 but adds the assumption that the group operation is commutative (i.e. the group is abelian).

locale abgroup_int0 = group_int0 +

assumes isAbelian: $ P \text{ is commutative on } G $

In abelian groups taking a nonnegative integer power commutes with the group operation. Unfortunately we have to drop to raw set theory notation in the proof to be able to use int0.Induction_on_int from the abgroup_int0 context.

lemma (in abgroup_int0) powz_groupop_commute0:

assumes $ 0 \leq k $, $ x\in G $, $ y\in G $

shows $ (x\cdot y)^{k} = x^{k}\cdot y^{k} $proof

let $ A_Z = IntegerAddition $

let $ M_Z = IntegerMultiplication $

let $ O_Z = IntegerOrder $

from assms have $ \langle 0 ,k\rangle \in O_Z $ and $ (x\cdot y)^{ 0 } = x^{ 0 }\cdot y^{ 0 } $ using group_op_closed, int_power_zero_one(1), group0_2_L2

moreover {

fix $ m $

assume $ 0 \leq m $ and I: $ (x\cdot y)^{m} = x^{m}\cdot y^{m} $

from assms(2,3), $ 0 \leq m $ have $ m\in \mathbb{Z} $ and $ x\cdot y \in G $ using Int_ZF_2_L1A(3), group_op_closed

with isAbelian, assms(2,3), I have $ (x\cdot y)^{m + 1 _Z} = x^{m + 1 _Z}\cdot y^{m + 1 _Z} $ using int_power_add_one, group0_4_L8(3), powz_type

}

hence $ \forall m.\ 0 \leq m \wedge (x\cdot y)^{m} = x^{m}\cdot y^{m} \longrightarrow $ $ (x\cdot y)^{m + 1 _Z} = x^{m + 1 _Z}\cdot y^{m + 1 _Z} $

hence $ \forall m.\ \langle 0 , m\rangle \in O_Z \wedge (x\cdot y)^{m} = x^{m}\cdot y^{m} \longrightarrow $ $ (x\cdot y)^{A_Z(\langle m,\text{ TheNeutralElement}(int,M_Z)\rangle )} = $ $ x^{A_Z(\langle m,\text{ TheNeutralElement}(int,M_Z)\rangle )}\cdot y^{A_Z(\langle m,\text{ TheNeutralElement}(int,M_Z)\rangle )} $

ultimately show $ (x\cdot y)^{k} = x^{k}\cdot y^{k} $ by (rule Induction_on_int )

qed

In abelian groups taking a nonpositive integer power commutes with the group operation. We could use backwards induction in the proof but it is shorter to use the nonnegative case from powz_groupop_commute0.

lemma (in abgroup_int0) powz_groupop_commute1:

assumes $ k\leq 0 $, $ x\in G $, $ y\in G $

shows $ (x\cdot y)^{k} = x^{k}\cdot y^{k} $proof

from isAbelian, assms have $ (x\cdot y)^{k} = (x^{-1}\cdot y^{-1})^{ - k} $ using Int_ZF_2_L1A(2), group_op_closed, minus_exp_inv_base1, group_inv_of_two unfolding IsCommutative_def

with assms show $ thesis $ using Int_ZF_2_L10A, inverse_in_group, powz_groupop_commute0, Int_ZF_2_L1A(2), minus_exp_inv_base1

qed

In abelian groups taking an integer power commutes with the group operation.

theorem (in abgroup_int0) powz_groupop_commute:

assumes $ z\in \mathbb{Z} $, $ x\in G $, $ y\in G $

shows $ (x\cdot y)^{z} = x^{z}\cdot y^{z} $proof

from assms(1) have $ 0 \leq z \vee z\leq 0 $ using int_nonneg_or_nonpos

with assms(2,3) show $ thesis $ using powz_groupop_commute0, powz_groupop_commute1

qed

For any integer $n$ the mapping $x\mapsto x^n$ maps $G$ into $G$ and is a homomorphism hence an endomorphism of $(G,P)$.

theorem (in abgroup_int0) powz_end:

assumes $ n\in \mathbb{Z} $

defines $ h \equiv \{\langle x,x^{n}\rangle .\ x\in G\} $

shows $ h:G\rightarrow G $, $ \text{Homomor}(h,G,P,G,P) $, $ h \in \text{End}(G,P) $proof

from assms show $ h:G\rightarrow G $ using powz_type, ZF_fun_from_total

with assms have $ \text{IsMorphism}(G,P,P,h) $ using ZF_fun_from_tot_val(1), group_op_closed, powz_groupop_commute unfolding IsMorphism_def

with $ h:G\rightarrow G $ show $ \text{Homomor}(h,G,P,G,P) $ and $ h \in \text{End}(G,P) $ unfolding Homomor_def, End_def

qed

The mapping $\mathbb{Z}\ni n\mapsto (x\mapsto x^n\in G)$ maps integers to endomorphisms of $(G,P)$.

theorem (in abgroup_int0) powz_maps_int_End:

shows $ \{\langle n,\{\langle x,x^{n}\rangle .\ x\in G\}\rangle .\ n\in \mathbb{Z} \} : \mathbb{Z} \rightarrow \text{End}(G,P) $ using powz_end(3), ZF_fun_from_total

end

lemma (in monoid1) nat_mult_zero: shows $ 0\cdot x = 0 $

lemma (in group0) group0_2_L2: shows $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g)) $

lemma (in group0) inverse_in_group:

assumes $ x\in G $

shows $ x^{-1}\in G $

lemma (in group0) nat_pow_add_one:

assumes $ n\in nat $, $ x\in G $

shows $ x^{n + 1} = x^{n}\cdot x $ and $ x^{n + 1} = x\cdot x^{n} $

lemma (in monoid1) nat_mult_type:

assumes $ n\in nat $, $ x\in G $

shows $ n\cdot x \in G $

lemma (in monoid0) rearr4elem_monoid:

assumes $ a\in G $, $ b\in G $, $ c\in G $, $ d\in G $

shows $ a\oplus b\oplus (c\oplus d) = a\oplus (b\oplus c)\oplus d $

lemma (in group0) group0_2_L6:

assumes $ x\in G $

shows $ x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 $

lemma ind_on_nat1:

assumes $ n\in nat $ and $ P(0) $ and $ \forall k\in nat.\ P(k)\longrightarrow P(k + 1) $

shows $ P(n) $

lemma (in group0) nat_pow_inv_cancel:

assumes $ n\in nat $, $ x\in G $

shows $ x^{n}\cdot (x^{-1})^{n} = 1 $

lemma (in group0) group_inv_of_inv:

assumes $ a\in G $

shows $ a = (a^{-1})^{-1} $

lemma leq_nat_is_nat:

assumes $ n\in nat $, $ k\leq n $

shows $ k\in nat $

lemma (in monoid1) nat_mult_add:

assumes $ n\in nat $, $ m\in nat $, $ x\in G $

shows $ (n + m)\cdot x = n\cdot x \oplus m\cdot x $

lemma (in group0) group_oper_assoc:

assumes $ a\in G $, $ b\in G $, $ c\in G $

shows $ a\cdot (b\cdot c) = a\cdot b\cdot c $

lemma (in group0) nat_pow_cancel_less:

assumes $ n\in nat $, $ k\leq n $, $ x\in G $

shows $ x^{n}\cdot (x^{-1})^{k} = x^{n - k} $

lemma (in group0) nat_pow_inv_cancel1:

assumes $ n\in nat $, $ x\in G $

shows $ (x^{-1})^{n}\cdot x^{n} = 1 $

lemma (in group0) nat_pow_cancel_more:

assumes $ n\in nat $, $ k\leq n $, $ x\in G $

shows $ (x^{-1})^{k}\cdot x^{n} = x^{n - k} $

Definition of powz: $ x^{z} \equiv (\text{if } 0 \leq z\text{ then }x\text{ else }x^{-1})^{| z|_N } $

lemma (in int0) Int_ZF_1_L8A: shows $ 0 \in \mathbb{Z} $, $ 1 \in \mathbb{Z} $

lemma (in int0) int_ord_is_refl1:

assumes $ z\in \mathbb{Z} $

shows $ z\leq z $

lemma (in int0) zmag_zero_one: shows $ \left| 0 \right|_N = 0 $ and $ \left| 1 \right|_N = 1 $

lemma (in int0) Int_ZF_2_L16A: shows $ 0 \leq 1 $, $ 0 \lt 1 $, $ abs(1 ) = 1 $

lemma (in monoid1) nat_mult_one:

assumes $ x\in G $

shows $ 1\cdot x = x $

lemma (in int0) add_nonneg_ints:

assumes $ 0 \leq z_1 $, $ 0 \leq z_2 $

corollary (in int0) neg_not_nonneg:

assumes $ m \lt 0 $

shows $ \neg ( 0 \leq m) $

lemma (in int0) add_neg_ints:

assumes $ z_1 \lt 0 $, $ z_2 \lt 0 $

lemma (in int0) add_nonneg_neg1:

assumes $ 0 \leq z_1 $, $ z_2 \lt 0 $, $ \left| z_2 \right|_N \leq \left| z_1 \right|_N $

lemma (in int0) add_nonneg_neg1:

assumes $ 0 \leq z_1 $, $ z_2 \lt 0 $, $ \left| z_2 \right|_N \leq \left| z_1 \right|_N $

lemma (in int0) add_nonneg_neg2:

assumes $ 0 \leq z_1 $, $ z_2 \lt 0 $, $ \left| z_1 \right|_N \lt \left| z_2 \right|_N $

lemma (in group0) nat_pow_cancel_more1:

assumes $ n\in nat $, $ k\leq n $, $ x\in G $

shows $ x^{k}\cdot (x^{-1})^{n} = (x^{-1})^{n - k} $

lemma (in int0) add_neg_nonneg1:

assumes $ z_1 \lt 0 $, $ 0 \leq z_2 $, $ \left| z_1 \right|_N \leq \left| z_2 \right|_N $

lemma (in int0) add_neg_nonneg2:

assumes $ z_1 \lt 0 $, $ 0 \leq z_2 $, $ \left| z_2 \right|_N \lt \left| z_1 \right|_N $

lemma (in group0) nat_pow_cancel_less1:

assumes $ n\in nat $, $ k\leq n $, $ x\in G $

shows $ (x^{-1})^{n}\cdot x^{k} = (x^{-1})^{n - k} $

lemma (in int0) int_pair_6cases:

assumes $ z_1\in \mathbb{Z} $, $ z_2\in \mathbb{Z} $

lemma (in group_int0) powz_hom_nneg_nneg:

assumes $ 0 \leq z_1 $, $ 0 \leq z_2 $, $ x\in G $

shows $ x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} $

lemma (in group_int0) powz_hom_neg_neg:

assumes $ z_1 \lt 0 $, $ z_2 \lt 0 $, $ x\in G $

shows $ x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} $

lemma (in group_int0) powz_hom_nneg_neg1:

assumes $ 0 \leq z_1 $, $ z_2 \lt 0 $, $ \left| z_2 \right|_N \leq \left| z_1 \right|_N $, $ x\in G $

shows $ x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} $

lemma (in group_int0) powz_hom_nneg_neg2:

assumes $ 0 \leq z_1 $, $ z_2 \lt 0 $, $ \left| z_1 \right|_N \lt \left| z_2 \right|_N $, $ x\in G $

shows $ x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} $

lemma (in group_int0) powz_hom_neg_nneg1:

assumes $ z_1 \lt 0 $, $ 0 \leq z_2 $, $ \left| z_1 \right|_N \leq \left| z_2 \right|_N $, $ x\in G $

shows $ x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} $

lemma (in group_int0) powz_hom_neg_nneg2:

assumes $ z_1 \lt 0 $, $ 0 \leq z_2 $, $ \left| z_2 \right|_N \lt \left| z_1 \right|_N $, $ x\in G $

shows $ x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} $

lemma (in int0) neg_one_less_zero: shows $ ( - 1 ) \lt 0 $

lemma (in int0) zmag_opposite_same:

assumes $ z\in \mathbb{Z} $

shows $ | z|_N = \left| \ \$\!-\!z \right|_N $, $ | z|_N = \left| - z \right|_N $

lemma (in int0) Int_ZF_1_L8A: shows $ 0 \in \mathbb{Z} $, $ 1 \in \mathbb{Z} $

lemma (in int0) zmag_zero_one: shows $ \left| 0 \right|_N = 0 $ and $ \left| 1 \right|_N = 1 $

theorem (in group_int0) powz_hom_prop:

assumes $ z_1\in \mathbb{Z} $, $ z_2\in \mathbb{Z} $, $ x\in G $

shows $ x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} $

lemma (in group_int0) int_power_zero_one:

assumes $ x\in G $

shows $ x^{ 0 } = 1 $ and $ x^{1 _Z} = x $

lemma (in int0) int_neg_zero_pos:

assumes $ z\in \mathbb{Z} $

shows $ 0 \lt z \vee z= 0 \vee z \lt 0 $

lemma (in int0) neg_pos_int_neg:

assumes $ 0 \lt z $

shows $ ( - z) \lt 0 $

lemma (in int0) Int_ZF_1_L11: shows $ ( - 0 ) = 0 $

lemma (in group_int0) int_power_zero_one:

assumes $ x\in G $

shows $ x^{ 0 } = 1 $ and $ x^{1 _Z} = x $

lemma (in int0) neg_neg_int_pos:

assumes $ z \lt 0 $

shows $ 0 \lt ( - z) $

lemma (in int0) int_neg_type:

assumes $ m\in \mathbb{Z} $

shows $ ( - m) \in \mathbb{Z} $

lemma (in group_int0) minus_exp_inv_base:

assumes $ z\in \mathbb{Z} $, $ x\in G $

shows $ x^{ - z} = (x^{-1})^{z} $

lemma (in int0) neg_neg_noop:

assumes $ m\in \mathbb{Z} $

shows $ ( - ( - m)) = m $

lemma (in group0) group_op_closed:

assumes $ a\in G $, $ b\in G $

shows $ a\cdot b \in G $

lemma (in int0) Int_ZF_2_L1A:

assumes $ m \leq n $

shows $ m \ \$\!\leq\ n $, $ m\in \mathbb{Z} $, $ n\in \mathbb{Z} $

lemma (in group_int0) int_power_add_one:

assumes $ z\in \mathbb{Z} $, $ x\in G $

shows $ x^{z + 1 _Z} = x^{z}\cdot x $

lemma (in group0) group0_4_L8:

assumes $ P \text{ is commutative on } G $ and $ a\in G $, $ b\in G $, $ c\in G $, $ d\in G $

shows $ a\cdot (b\cdot c)^{-1} = (a\cdot d^{-1}\cdot c^{-1})\cdot (d\cdot b^{-1}) $, $ a\cdot b\cdot (c\cdot d) = c\cdot a\cdot (b\cdot d) $, $ a\cdot b\cdot (c\cdot d) = a\cdot c\cdot (b\cdot d) $, $ a\cdot (b\cdot c^{-1})\cdot d = a\cdot b\cdot d\cdot c^{-1} $, $ (a\cdot b)\cdot (c\cdot d)^{-1}\cdot (b\cdot d^{-1})^{-1} = a\cdot c^{-1} $

lemma (in group_int0) powz_type:

assumes $ z\in \mathbb{Z} $, $ x\in G $

shows $ x^{z} \in G $

theorem (in int0) Induction_on_int:

assumes $ i\leq k $ and $ Q(i) $ and $ \forall m.\ i\leq m \wedge Q(m) \longrightarrow Q(m + 1 ) $

shows $ Q(k) $

lemma (in int0) Int_ZF_2_L1A:

assumes $ m \leq n $

shows $ m \ \$\!\leq\ n $, $ m\in \mathbb{Z} $, $ n\in \mathbb{Z} $

lemma (in group_int0) minus_exp_inv_base1:

assumes $ z\in \mathbb{Z} $, $ x\in G $

shows $ x^{z} = (x^{-1})^{ - z} $

lemma (in group0) group_inv_of_two:

assumes $ a\in G $ and $ b\in G $

shows $ b^{-1}\cdot a^{-1} = (a\cdot b)^{-1} $

Definition of IsCommutative: $ f \text{ is commutative on } G \equiv \forall x\in G.\ \forall y\in G.\ f\langle x,y\rangle = f\langle y,x\rangle $

lemma (in int0) Int_ZF_2_L10A:

assumes $ k \leq 0 $

shows $ 0 \leq ( - k) $

lemma (in abgroup_int0) powz_groupop_commute0:

assumes $ 0 \leq k $, $ x\in G $, $ y\in G $

shows $ (x\cdot y)^{k} = x^{k}\cdot y^{k} $

corollary (in int0) int_nonneg_or_nonpos:

assumes $ z\in \mathbb{Z} $

shows $ 0 \leq z \vee z\leq 0 $

lemma (in abgroup_int0) powz_groupop_commute1:

assumes $ k\leq 0 $, $ x\in G $, $ y\in G $

shows $ (x\cdot y)^{k} = x^{k}\cdot y^{k} $

lemma ZF_fun_from_total:

assumes $ \forall x\in X.\ b(x) \in Y $

shows $ \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y $

lemma ZF_fun_from_tot_val:

assumes $ f:X\rightarrow Y $, $ x\in X $ and $ f = \{\langle x,b(x)\rangle .\ x\in X\} $

shows $ f(x) = b(x) $ and $ b(x)\in Y $

theorem (in abgroup_int0) powz_groupop_commute:

assumes $ z\in \mathbb{Z} $, $ x\in G $, $ y\in G $

shows $ (x\cdot y)^{z} = x^{z}\cdot y^{z} $

Definition of IsMorphism: $ \text{IsMorphism}(G,P,F,f) \equiv \forall g_1\in G.\ \forall g_2\in G.\ f(P\langle g_1,g_2\rangle ) = F\langle f(g_1),f(g_2)\rangle $

Definition of Homomor: $ \text{Homomor}(f,G,P,H,F) \equiv f:G\rightarrow H \wedge \text{IsMorphism}(G,P,F,f) $

Definition of End: $ \text{End}(G,P) \equiv \{f\in G\rightarrow G.\ \text{Homomor}(f,G,P,G,P)\} $

theorem (in abgroup_int0) powz_end:

assumes $ n\in \mathbb{Z} $

defines $ h \equiv \{\langle x,x^{n}\rangle .\ x\in G\} $

shows $ h:G\rightarrow G $, $ \text{Homomor}(h,G,P,G,P) $, $ h \in \text{End}(G,P) $