odlem2

Description: Any positive annihilator of a group element is an upper bound on the (positive) order of the element. (Contributed by Mario Carneiro, 14-Jan-2015) (Revised by Stefan O'Rear, 5-Sep-2015) (Proof shortened by AV, 5-Oct-2020)

	Ref	Expression
Hypotheses	odcl.1	$⊢ X = {Base}_{G}$
	odcl.2	$⊢ O = od (G)$
	odid.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	odid.4	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	odlem2	$⊢ (A \in X \land N \in ℕ \land N \underset{˙}{\cdot} A = \underset{˙}{0}) \to O (A) \in (1 \dots N)$

Proof

Step	Hyp	Ref	Expression
1		odcl.1	$⊢ X = {Base}_{G}$
2		odcl.2	$⊢ O = od (G)$
3		odid.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
4		odid.4	$⊢ \underset{˙}{0} = 0_{G}$
5		oveq1	$⊢ y = N \to y \underset{˙}{\cdot} A = N \underset{˙}{\cdot} A$
6	5	eqeq1d	$⊢ y = N \to (y \underset{˙}{\cdot} A = \underset{˙}{0} \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0})$
7	6	elrab	$⊢ N \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} \leftrightarrow (N \in ℕ \land N \underset{˙}{\cdot} A = \underset{˙}{0})$
8		eqid	$⊢ \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} = \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\}$
9	1 3 4 2 8	odval	$⊢ A \in X \to O (A) = if (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} = \emptyset, 0, inf (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} ℝ <))$
10		n0i	$⊢ N \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} \to \neg \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} = \emptyset$
11	10	iffalsed	$⊢ N \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} \to if (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} = \emptyset, 0, inf (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} ℝ <)) = inf (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} ℝ <)$
12	9 11	sylan9eq	$⊢ (A \in X \land N \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\}) \to O (A) = inf (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} ℝ <)$
13		ssrab2	$⊢ \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} \subseteq ℕ$
14		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
15	13 14	sseqtri	$⊢ \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} \subseteq ℤ_{\geq 1}$
16		ne0i	$⊢ N \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} \to \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} \neq \emptyset$
17	16	adantl	$⊢ (A \in X \land N \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\}) \to \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} \neq \emptyset$
18		infssuzcl	$⊢ (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} \subseteq ℤ_{\geq 1} \land \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} \neq \emptyset) \to inf (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} ℝ <) \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\}$
19	15 17 18	sylancr	$⊢ (A \in X \land N \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\}) \to inf (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} ℝ <) \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\}$
20	13 19	sselid	$⊢ (A \in X \land N \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\}) \to inf (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} ℝ <) \in ℕ$
21		infssuzle	$⊢ (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} \subseteq ℤ_{\geq 1} \land N \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\}) \to inf (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} ℝ <) \leq N$
22	15 21	mpan	$⊢ N \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} \to inf (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} ℝ <) \leq N$
23	22	adantl	$⊢ (A \in X \land N \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\}) \to inf (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} ℝ <) \leq N$
24		elrabi	$⊢ N \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} \to N \in ℕ$
25	24	nnzd	$⊢ N \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} \to N \in ℤ$
26		fznn	$⊢ N \in ℤ \to (inf (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} ℝ <) \in (1 \dots N) \leftrightarrow (inf (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} ℝ <) \in ℕ \land inf (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} ℝ <) \leq N))$
27	25 26	syl	$⊢ N \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} \to (inf (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} ℝ <) \in (1 \dots N) \leftrightarrow (inf (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} ℝ <) \in ℕ \land inf (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} ℝ <) \leq N))$
28	27	adantl	$⊢ (A \in X \land N \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\}) \to (inf (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} ℝ <) \in (1 \dots N) \leftrightarrow (inf (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} ℝ <) \in ℕ \land inf (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} ℝ <) \leq N))$
29	20 23 28	mpbir2and	$⊢ (A \in X \land N \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\}) \to inf (\{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\} ℝ <) \in (1 \dots N)$
30	12 29	eqeltrd	$⊢ (A \in X \land N \in \{y \in ℕ \| y \underset{˙}{\cdot} A = \underset{˙}{0}\}) \to O (A) \in (1 \dots N)$
31	7 30	sylan2br	$⊢ (A \in X \land (N \in ℕ \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to O (A) \in (1 \dots N)$
32	31	3impb	$⊢ (A \in X \land N \in ℕ \land N \underset{˙}{\cdot} A = \underset{˙}{0}) \to O (A) \in (1 \dots N)$

Metamath Proof Explorer

Theorem odlem2

Proof