Theorem 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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	odcl.2	⊢ 𝑂 = ( od ‘ 𝐺 )
	odid.3	⊢ · = ( .g ‘ 𝐺 )
	odid.4	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	odlem2	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ ∧ ( 𝑁 · 𝐴 ) = 0 ) → ( 𝑂 ‘ 𝐴 ) ∈ ( 1 ... 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		odcl.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		odcl.2	⊢ 𝑂 = ( od ‘ 𝐺 )
3		odid.3	⊢ · = ( .g ‘ 𝐺 )
4		odid.4	⊢ 0 = ( 0g ‘ 𝐺 )
5		oveq1	⊢ ( 𝑦 = 𝑁 → ( 𝑦 · 𝐴 ) = ( 𝑁 · 𝐴 ) )
6	5	eqeq1d	⊢ ( 𝑦 = 𝑁 → ( ( 𝑦 · 𝐴 ) = 0 ↔ ( 𝑁 · 𝐴 ) = 0 ) )
7	6	elrab	⊢ ( 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ↔ ( 𝑁 ∈ ℕ ∧ ( 𝑁 · 𝐴 ) = 0 ) )
8		eqid	⊢ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } = { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 }
9	1 3 4 2 8	odval	⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) = if ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } = ∅ , 0 , inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } , ℝ , < ) ) )
10		n0i	⊢ ( 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } → ¬ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } = ∅ )
11	10	iffalsed	⊢ ( 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } → if ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } = ∅ , 0 , inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } , ℝ , < ) ) = inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } , ℝ , < ) )
12	9 11	sylan9eq	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ) → ( 𝑂 ‘ 𝐴 ) = inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } , ℝ , < ) )
13		ssrab2	⊢ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ⊆ ℕ
14		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
15	13 14	sseqtri	⊢ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ⊆ ( ℤ≥ ‘ 1 )
16		ne0i	⊢ ( 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } → { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ≠ ∅ )
17	16	adantl	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ) → { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ≠ ∅ )
18		infssuzcl	⊢ ( ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ⊆ ( ℤ≥ ‘ 1 ) ∧ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ≠ ∅ ) → inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } , ℝ , < ) ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } )
19	15 17 18	sylancr	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ) → inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } , ℝ , < ) ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } )
20	13 19	sselid	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ) → inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } , ℝ , < ) ∈ ℕ )
21		infssuzle	⊢ ( ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ) → inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } , ℝ , < ) ≤ 𝑁 )
22	15 21	mpan	⊢ ( 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } → inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } , ℝ , < ) ≤ 𝑁 )
23	22	adantl	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ) → inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } , ℝ , < ) ≤ 𝑁 )
24		elrabi	⊢ ( 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } → 𝑁 ∈ ℕ )
25	24	nnzd	⊢ ( 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } → 𝑁 ∈ ℤ )
26		fznn	⊢ ( 𝑁 ∈ ℤ → ( inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } , ℝ , < ) ∈ ( 1 ... 𝑁 ) ↔ ( inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } , ℝ , < ) ∈ ℕ ∧ inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } , ℝ , < ) ≤ 𝑁 ) ) )
27	25 26	syl	⊢ ( 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } → ( inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } , ℝ , < ) ∈ ( 1 ... 𝑁 ) ↔ ( inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } , ℝ , < ) ∈ ℕ ∧ inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } , ℝ , < ) ≤ 𝑁 ) ) )
28	27	adantl	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ) → ( inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } , ℝ , < ) ∈ ( 1 ... 𝑁 ) ↔ ( inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } , ℝ , < ) ∈ ℕ ∧ inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } , ℝ , < ) ≤ 𝑁 ) ) )
29	20 23 28	mpbir2and	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ) → inf ( { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } , ℝ , < ) ∈ ( 1 ... 𝑁 ) )
30	12 29	eqeltrd	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ) → ( 𝑂 ‘ 𝐴 ) ∈ ( 1 ... 𝑁 ) )
31	7 30	sylan2br	⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝑁 · 𝐴 ) = 0 ) ) → ( 𝑂 ‘ 𝐴 ) ∈ ( 1 ... 𝑁 ) )
32	31	3impb	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ ∧ ( 𝑁 · 𝐴 ) = 0 ) → ( 𝑂 ‘ 𝐴 ) ∈ ( 1 ... 𝑁 ) )