Metamath Proof Explorer

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 sseldi ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 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 ... 𝑁 ) )