Theorem gexlem2

Description: Any positive annihilator of all the group elements is an upper bound on the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016) (Proof shortened by AV, 26-Sep-2020)

	Ref	Expression
Hypotheses	gexcl.1	$$⊢X={\mathrm{Base}}_G$$
	gexcl.2	$$⊢E=\mathrm{gEx}\left(G\right)$$
	gexid.3	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	gexid.4	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	gexlem2	$$⊢\left(G\in V\wedge N\in \mathbb{N}\wedge \forall x\in XN\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right)\to E\in \left(1\dots N\right)$$

Proof

Step	Hyp	Ref	Expression
1		gexcl.1	$$⊢X={\mathrm{Base}}_G$$
2		gexcl.2	$$⊢E=\mathrm{gEx}\left(G\right)$$
3		gexid.3	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
4		gexid.4	$$⊢\underset{\dot{}}{0}=0_G$$
5		oveq1	$$⊢y=N\to y\underset{\dot{}}{·}x=N\underset{\dot{}}{·}x$$
6	5	eqeq1d	$$⊢y=N\to \left(y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\leftrightarrow N\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right)$$
7	6	ralbidv	$$⊢y=N\to \left(\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\leftrightarrow \forall x\in XN\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right)$$
8	7	elrab	$$⊢N\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\leftrightarrow \left(N\in \mathbb{N}\wedge \forall x\in XN\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right)$$
9		eqid	$$⊢\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}=\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}$$
10	1 3 4 2 9	gexval	$$⊢G\in V\to E=if\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}=\varnothing ,0,inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\right)$$
11		ne0i	$$⊢N\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\to \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\ne \varnothing$$
12		ifnefalse	$$⊢\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\ne \varnothing \to if\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}=\varnothing ,0,inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\right)=inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)$$
13	11 12	syl	$$⊢N\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\to if\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}=\varnothing ,0,inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\right)=inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)$$
14	10 13	sylan9eq	$$⊢\left(G\in V\wedge N\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\right)\to E=inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)$$
15		ssrab2	$$⊢\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\subseteq \mathbb{N}$$
16		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
17	15 16	sseqtri	$$⊢\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\subseteq {\mathbb{Z}}_{\ge 1}$$
18	11	adantl	$$⊢\left(G\in V\wedge N\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\right)\to \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\ne \varnothing$$
19		infssuzcl	$$⊢\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\subseteq {\mathbb{Z}}_{\ge 1}\wedge \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\ne \varnothing \right)\to inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}$$
20	17 18 19	sylancr	$$⊢\left(G\in V\wedge N\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\right)\to inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}$$
21	15 20	sselid	$$⊢\left(G\in V\wedge N\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\right)\to inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\in \mathbb{N}$$
22		infssuzle	$$⊢\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\subseteq {\mathbb{Z}}_{\ge 1}\wedge N\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\right)\to inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\le N$$
23	17 22	mpan	$$⊢N\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\to inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\le N$$
24	23	adantl	$$⊢\left(G\in V\wedge N\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\right)\to inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\le N$$
25		elrabi	$$⊢N\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\to N\in \mathbb{N}$$
26	25	nnzd	$$⊢N\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\to N\in \mathbb{Z}$$
27		fznn	$$⊢N\in \mathbb{Z}\to \left(inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\in \left(1\dots N\right)\leftrightarrow \left(inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\in \mathbb{N}\wedge inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\le N\right)\right)$$
28	26 27	syl	$$⊢N\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\to \left(inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\in \left(1\dots N\right)\leftrightarrow \left(inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\in \mathbb{N}\wedge inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\le N\right)\right)$$
29	28	adantl	$$⊢\left(G\in V\wedge N\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\right)\to \left(inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\in \left(1\dots N\right)\leftrightarrow \left(inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\in \mathbb{N}\wedge inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\le N\right)\right)$$
30	21 24 29	mpbir2and	$$⊢\left(G\in V\wedge N\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\right)\to inf\left(\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\in \left(1\dots N\right)$$
31	14 30	eqeltrd	$$⊢\left(G\in V\wedge N\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\right)\to E\in \left(1\dots N\right)$$
32	8 31	sylan2br	$$⊢\left(G\in V\wedge \left(N\in \mathbb{N}\wedge \forall x\in XN\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right)\right)\to E\in \left(1\dots N\right)$$
33	32	3impb	$$⊢\left(G\in V\wedge N\in \mathbb{N}\wedge \forall x\in XN\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right)\to E\in \left(1\dots N\right)$$