This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-odz

Description: Define the order function on the class of integers modulo N. (Contributed by Mario Carneiro, 23-Feb-2014) (Revised by AV, 26-Sep-2020)

Ref Expression
Assertion df-odz odℤ = ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ { 𝑥 ∈ ℤ ∣ ( 𝑥 gcd 𝑛 ) = 1 } ↦ inf ( { 𝑚 ∈ ℕ ∣ 𝑛 ∥ ( ( 𝑥 ↑ 𝑚 ) − 1 ) } , ℝ , < ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 codz ⊢ odℤ
1 vn ⊢ 𝑛
2 cn ⊢ ℕ
3 vx ⊢ 𝑥
4 cz ⊢ ℤ
5 3 cv ⊢ 𝑥
6 cgcd ⊢ gcd
7 1 cv ⊢ 𝑛
8 5 7 6 co ⊢ ( 𝑥 gcd 𝑛 )
9 c1 ⊢ 1
10 8 9 wceq ⊢ ( 𝑥 gcd 𝑛 ) = 1
11 10 3 4 crab ⊢ { 𝑥 ∈ ℤ ∣ ( 𝑥 gcd 𝑛 ) = 1 }
12 vm ⊢ 𝑚
13 cdvds ⊢ ∥
14 cexp ⊢ ↑
15 12 cv ⊢ 𝑚
16 5 15 14 co ⊢ ( 𝑥 ↑ 𝑚 )
17 cmin ⊢ −
18 16 9 17 co ⊢ ( ( 𝑥 ↑ 𝑚 ) − 1 )
19 7 18 13 wbr ⊢ 𝑛 ∥ ( ( 𝑥 ↑ 𝑚 ) − 1 )
20 19 12 2 crab ⊢ { 𝑚 ∈ ℕ ∣ 𝑛 ∥ ( ( 𝑥 ↑ 𝑚 ) − 1 ) }
21 cr ⊢ ℝ
22 clt ⊢ <
23 20 21 22 cinf ⊢ inf ( { 𝑚 ∈ ℕ ∣ 𝑛 ∥ ( ( 𝑥 ↑ 𝑚 ) − 1 ) } , ℝ , < )
24 3 11 23 cmpt ⊢ ( 𝑥 ∈ { 𝑥 ∈ ℤ ∣ ( 𝑥 gcd 𝑛 ) = 1 } ↦ inf ( { 𝑚 ∈ ℕ ∣ 𝑛 ∥ ( ( 𝑥 ↑ 𝑚 ) − 1 ) } , ℝ , < ) )
25 1 2 24 cmpt ⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ { 𝑥 ∈ ℤ ∣ ( 𝑥 gcd 𝑛 ) = 1 } ↦ inf ( { 𝑚 ∈ ℕ ∣ 𝑛 ∥ ( ( 𝑥 ↑ 𝑚 ) − 1 ) } , ℝ , < ) ) )
26 0 25 wceq ⊢ odℤ = ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ { 𝑥 ∈ ℤ ∣ ( 𝑥 gcd 𝑛 ) = 1 } ↦ inf ( { 𝑚 ∈ ℕ ∣ 𝑛 ∥ ( ( 𝑥 ↑ 𝑚 ) − 1 ) } , ℝ , < ) ) )