Proof of Theorem lgsfval
| Step | Hyp | Ref
| Expression |
| 1 | | eleq1 2829 |
. . 3
⊢ (𝑛 = 𝑀 → (𝑛 ∈ ℙ ↔ 𝑀 ∈ ℙ)) |
| 2 | | eqeq1 2741 |
. . . . 5
⊢ (𝑛 = 𝑀 → (𝑛 = 2 ↔ 𝑀 = 2)) |
| 3 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑀 → (𝑛 − 1) = (𝑀 − 1)) |
| 4 | 3 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑛 = 𝑀 → ((𝑛 − 1) / 2) = ((𝑀 − 1) / 2)) |
| 5 | 4 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑛 = 𝑀 → (𝐴↑((𝑛 − 1) / 2)) = (𝐴↑((𝑀 − 1) / 2))) |
| 6 | 5 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑛 = 𝑀 → ((𝐴↑((𝑛 − 1) / 2)) + 1) = ((𝐴↑((𝑀 − 1) / 2)) + 1)) |
| 7 | | id 22 |
. . . . . . 7
⊢ (𝑛 = 𝑀 → 𝑛 = 𝑀) |
| 8 | 6, 7 | oveq12d 7449 |
. . . . . 6
⊢ (𝑛 = 𝑀 → (((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) = (((𝐴↑((𝑀 − 1) / 2)) + 1) mod 𝑀)) |
| 9 | 8 | oveq1d 7446 |
. . . . 5
⊢ (𝑛 = 𝑀 → ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1) = ((((𝐴↑((𝑀 − 1) / 2)) + 1) mod 𝑀) − 1)) |
| 10 | 2, 9 | ifbieq2d 4552 |
. . . 4
⊢ (𝑛 = 𝑀 → 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))) |
| 11 | | oveq1 7438 |
. . . 4
⊢ (𝑛 = 𝑀 → (𝑛 pCnt 𝑁) = (𝑀 pCnt 𝑁)) |
| 12 | 10, 11 | oveq12d 7449 |
. . 3
⊢ (𝑛 = 𝑀 → (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 𝑁))) |
| 13 | 1, 12 | ifbieq1d 4550 |
. 2
⊢ (𝑛 = 𝑀 → 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)) |
| 14 | | lgsval.1 |
. 2
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1)) |
| 15 | | ovex 7464 |
. . 3
⊢ (if(𝑀 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑀 − 1) / 2)) + 1) mod 𝑀) − 1))↑(𝑀 pCnt 𝑁)) ∈ V |
| 16 | | 1ex 11257 |
. . 3
⊢ 1 ∈
V |
| 17 | 15, 16 | ifex 4576 |
. 2
⊢ if(𝑀 ∈ ℙ, (if(𝑀 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑀 − 1) / 2)) + 1) mod 𝑀) − 1))↑(𝑀 pCnt 𝑁)), 1) ∈ V |
| 18 | 13, 14, 17 | fvmpt 7016 |
1
⊢ (𝑀 ∈ ℕ → (𝐹‘𝑀) = if(𝑀 ∈ ℙ, (if(𝑀 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑀 − 1) / 2)) + 1) mod 𝑀) − 1))↑(𝑀 pCnt 𝑁)), 1)) |