Step |
Hyp |
Ref |
Expression |
1 |
|
lgsval.1 |
⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) |
2 |
|
eleq1 |
⊢ ( 𝑛 = 𝑀 → ( 𝑛 ∈ ℙ ↔ 𝑀 ∈ ℙ ) ) |
3 |
|
eqeq1 |
⊢ ( 𝑛 = 𝑀 → ( 𝑛 = 2 ↔ 𝑀 = 2 ) ) |
4 |
|
oveq1 |
⊢ ( 𝑛 = 𝑀 → ( 𝑛 − 1 ) = ( 𝑀 − 1 ) ) |
5 |
4
|
oveq1d |
⊢ ( 𝑛 = 𝑀 → ( ( 𝑛 − 1 ) / 2 ) = ( ( 𝑀 − 1 ) / 2 ) ) |
6 |
5
|
oveq2d |
⊢ ( 𝑛 = 𝑀 → ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) = ( 𝐴 ↑ ( ( 𝑀 − 1 ) / 2 ) ) ) |
7 |
6
|
oveq1d |
⊢ ( 𝑛 = 𝑀 → ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) = ( ( 𝐴 ↑ ( ( 𝑀 − 1 ) / 2 ) ) + 1 ) ) |
8 |
|
id |
⊢ ( 𝑛 = 𝑀 → 𝑛 = 𝑀 ) |
9 |
7 8
|
oveq12d |
⊢ ( 𝑛 = 𝑀 → ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) = ( ( ( 𝐴 ↑ ( ( 𝑀 − 1 ) / 2 ) ) + 1 ) mod 𝑀 ) ) |
10 |
9
|
oveq1d |
⊢ ( 𝑛 = 𝑀 → ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) = ( ( ( ( 𝐴 ↑ ( ( 𝑀 − 1 ) / 2 ) ) + 1 ) mod 𝑀 ) − 1 ) ) |
11 |
3 10
|
ifbieq2d |
⊢ ( 𝑛 = 𝑀 → if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) = if ( 𝑀 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑀 − 1 ) / 2 ) ) + 1 ) mod 𝑀 ) − 1 ) ) ) |
12 |
|
oveq1 |
⊢ ( 𝑛 = 𝑀 → ( 𝑛 pCnt 𝑁 ) = ( 𝑀 pCnt 𝑁 ) ) |
13 |
11 12
|
oveq12d |
⊢ ( 𝑛 = 𝑀 → ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) = ( if ( 𝑀 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑀 − 1 ) / 2 ) ) + 1 ) mod 𝑀 ) − 1 ) ) ↑ ( 𝑀 pCnt 𝑁 ) ) ) |
14 |
2 13
|
ifbieq1d |
⊢ ( 𝑛 = 𝑀 → if ( 𝑛 ∈ ℙ , ( if ( 𝑛 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) = if ( 𝑀 ∈ ℙ , ( if ( 𝑀 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑀 − 1 ) / 2 ) ) + 1 ) mod 𝑀 ) − 1 ) ) ↑ ( 𝑀 pCnt 𝑁 ) ) , 1 ) ) |
15 |
|
ovex |
⊢ ( if ( 𝑀 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑀 − 1 ) / 2 ) ) + 1 ) mod 𝑀 ) − 1 ) ) ↑ ( 𝑀 pCnt 𝑁 ) ) ∈ V |
16 |
|
1ex |
⊢ 1 ∈ V |
17 |
15 16
|
ifex |
⊢ if ( 𝑀 ∈ ℙ , ( if ( 𝑀 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑀 − 1 ) / 2 ) ) + 1 ) mod 𝑀 ) − 1 ) ) ↑ ( 𝑀 pCnt 𝑁 ) ) , 1 ) ∈ V |
18 |
14 1 17
|
fvmpt |
⊢ ( 𝑀 ∈ ℕ → ( 𝐹 ‘ 𝑀 ) = if ( 𝑀 ∈ ℙ , ( if ( 𝑀 = 2 , if ( 2 ∥ 𝐴 , 0 , if ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } , 1 , - 1 ) ) , ( ( ( ( 𝐴 ↑ ( ( 𝑀 − 1 ) / 2 ) ) + 1 ) mod 𝑀 ) − 1 ) ) ↑ ( 𝑀 pCnt 𝑁 ) ) , 1 ) ) |