Step | Hyp | Ref
| Expression |
1 | | simpr 488 |
. . . 4
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → 𝑚 = 𝑁) |
2 | 1 | eqeq1d 2741 |
. . 3
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑚 = 0 ↔ 𝑁 = 0)) |
3 | | simpl 486 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → 𝑎 = 𝐴) |
4 | 3 | oveq1d 7197 |
. . . . 5
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑎↑2) = (𝐴↑2)) |
5 | 4 | eqeq1d 2741 |
. . . 4
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((𝑎↑2) = 1 ↔ (𝐴↑2) = 1)) |
6 | 5 | ifbid 4447 |
. . 3
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if((𝑎↑2) = 1, 1, 0) = if((𝐴↑2) = 1, 1, 0)) |
7 | 1 | breq1d 5050 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑚 < 0 ↔ 𝑁 < 0)) |
8 | 3 | breq1d 5050 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑎 < 0 ↔ 𝐴 < 0)) |
9 | 7, 8 | anbi12d 634 |
. . . . 5
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((𝑚 < 0 ∧ 𝑎 < 0) ↔ (𝑁 < 0 ∧ 𝐴 < 0))) |
10 | 9 | ifbid 4447 |
. . . 4
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if((𝑚 < 0 ∧ 𝑎 < 0), -1, 1) = if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) |
11 | 3 | breq2d 5052 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (2 ∥ 𝑎 ↔ 2 ∥ 𝐴)) |
12 | 3 | oveq1d 7197 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑎 mod 8) = (𝐴 mod 8)) |
13 | 12 | eleq1d 2818 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((𝑎 mod 8) ∈ {1, 7} ↔ (𝐴 mod 8) ∈ {1,
7})) |
14 | 13 | ifbid 4447 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if((𝑎 mod 8) ∈ {1, 7}, 1, -1) = if((𝐴 mod 8) ∈ {1, 7}, 1,
-1)) |
15 | 11, 14 | ifbieq2d 4450 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)) = if(2 ∥
𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1,
-1))) |
16 | 3 | oveq1d 7197 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑎↑((𝑛 − 1) / 2)) = (𝐴↑((𝑛 − 1) / 2))) |
17 | 16 | oveq1d 7197 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((𝑎↑((𝑛 − 1) / 2)) + 1) = ((𝐴↑((𝑛 − 1) / 2)) + 1)) |
18 | 17 | oveq1d 7197 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) = (((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛)) |
19 | 18 | oveq1d 7197 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1) = ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1)) |
20 | 15, 19 | ifeq12d 4445 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → 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))) |
21 | 1 | oveq2d 7198 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑛 pCnt 𝑚) = (𝑛 pCnt 𝑁)) |
22 | 20, 21 | oveq12d 7200 |
. . . . . . . . 9
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (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 𝑁))) |
23 | 22 | ifeq1d 4443 |
. . . . . . . 8
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → 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)) |
24 | 23 | mpteq2dv 5136 |
. . . . . . 7
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑛 ∈ ℕ ↦ 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))) |
25 | | lgsval.1 |
. . . . . . 7
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1)) |
26 | 24, 25 | eqtr4di 2792 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)) = 𝐹) |
27 | 26 | seqeq3d 13480 |
. . . . 5
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1))) = seq1( · , 𝐹)) |
28 | 1 | fveq2d 6690 |
. . . . 5
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (abs‘𝑚) = (abs‘𝑁)) |
29 | 27, 28 | fveq12d 6693 |
. . . 4
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)))‘(abs‘𝑚)) = (seq1( · , 𝐹)‘(abs‘𝑁))) |
30 | 10, 29 | oveq12d 7200 |
. . 3
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (if((𝑚 < 0 ∧ 𝑎 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
(if(𝑛 = 2, if(2 ∥
𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)),
((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)))‘(abs‘𝑚))) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
𝐹)‘(abs‘𝑁)))) |
31 | 2, 6, 30 | ifbieq12d 4452 |
. 2
⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if(𝑚 = 0, if((𝑎↑2) = 1, 1, 0), (if((𝑚 < 0 ∧ 𝑎 < 0), -1, 1) · (seq1( · ,
(𝑛 ∈ ℕ ↦
if(𝑛 ∈ ℙ,
(if(𝑛 = 2, if(2 ∥
𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)),
((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)))‘(abs‘𝑚)))) = if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
𝐹)‘(abs‘𝑁))))) |
32 | | df-lgs 26043 |
. 2
⊢
/L = (𝑎
∈ ℤ, 𝑚 ∈
ℤ ↦ if(𝑚 = 0,
if((𝑎↑2) = 1, 1, 0),
(if((𝑚 < 0 ∧ 𝑎 < 0), -1, 1) · (seq1(
· , (𝑛 ∈
ℕ ↦ if(𝑛 ∈
ℙ, (if(𝑛 = 2, if(2
∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)),
((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)))‘(abs‘𝑚))))) |
33 | | 1nn0 12004 |
. . . . 5
⊢ 1 ∈
ℕ0 |
34 | | 0nn0 12003 |
. . . . 5
⊢ 0 ∈
ℕ0 |
35 | 33, 34 | ifcli 4471 |
. . . 4
⊢ if((𝐴↑2) = 1, 1, 0) ∈
ℕ0 |
36 | 35 | elexi 3419 |
. . 3
⊢ if((𝐴↑2) = 1, 1, 0) ∈
V |
37 | | ovex 7215 |
. . 3
⊢
(if((𝑁 < 0 ∧
𝐴 < 0), -1, 1) ·
(seq1( · , 𝐹)‘(abs‘𝑁))) ∈ V |
38 | 36, 37 | ifex 4474 |
. 2
⊢ if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
𝐹)‘(abs‘𝑁)))) ∈ V |
39 | 31, 32, 38 | ovmpoa 7332 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) = if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · ,
𝐹)‘(abs‘𝑁))))) |