Detailed syntax breakdown of Definition df-lgs
| Step | Hyp | Ref
| Expression |
| 1 | | clgs 27338 |
. 2
class
/L |
| 2 | | va |
. . 3
setvar 𝑎 |
| 3 | | vn |
. . 3
setvar 𝑛 |
| 4 | | cz 12613 |
. . 3
class
ℤ |
| 5 | 3 | cv 1539 |
. . . . 5
class 𝑛 |
| 6 | | cc0 11155 |
. . . . 5
class
0 |
| 7 | 5, 6 | wceq 1540 |
. . . 4
wff 𝑛 = 0 |
| 8 | 2 | cv 1539 |
. . . . . . 7
class 𝑎 |
| 9 | | c2 12321 |
. . . . . . 7
class
2 |
| 10 | | cexp 14102 |
. . . . . . 7
class
↑ |
| 11 | 8, 9, 10 | co 7431 |
. . . . . 6
class (𝑎↑2) |
| 12 | | c1 11156 |
. . . . . 6
class
1 |
| 13 | 11, 12 | wceq 1540 |
. . . . 5
wff (𝑎↑2) = 1 |
| 14 | 13, 12, 6 | cif 4525 |
. . . 4
class if((𝑎↑2) = 1, 1,
0) |
| 15 | | clt 11295 |
. . . . . . . 8
class
< |
| 16 | 5, 6, 15 | wbr 5143 |
. . . . . . 7
wff 𝑛 < 0 |
| 17 | 8, 6, 15 | wbr 5143 |
. . . . . . 7
wff 𝑎 < 0 |
| 18 | 16, 17 | wa 395 |
. . . . . 6
wff (𝑛 < 0 ∧ 𝑎 < 0) |
| 19 | 12 | cneg 11493 |
. . . . . 6
class
-1 |
| 20 | 18, 19, 12 | cif 4525 |
. . . . 5
class if((𝑛 < 0 ∧ 𝑎 < 0), -1, 1) |
| 21 | | cabs 15273 |
. . . . . . 7
class
abs |
| 22 | 5, 21 | cfv 6561 |
. . . . . 6
class
(abs‘𝑛) |
| 23 | | cmul 11160 |
. . . . . . 7
class
· |
| 24 | | vm |
. . . . . . . 8
setvar 𝑚 |
| 25 | | cn 12266 |
. . . . . . . 8
class
ℕ |
| 26 | 24 | cv 1539 |
. . . . . . . . . 10
class 𝑚 |
| 27 | | cprime 16708 |
. . . . . . . . . 10
class
ℙ |
| 28 | 26, 27 | wcel 2108 |
. . . . . . . . 9
wff 𝑚 ∈ ℙ |
| 29 | 26, 9 | wceq 1540 |
. . . . . . . . . . 11
wff 𝑚 = 2 |
| 30 | | cdvds 16290 |
. . . . . . . . . . . . 13
class
∥ |
| 31 | 9, 8, 30 | wbr 5143 |
. . . . . . . . . . . 12
wff 2 ∥
𝑎 |
| 32 | | c8 12327 |
. . . . . . . . . . . . . . 15
class
8 |
| 33 | | cmo 13909 |
. . . . . . . . . . . . . . 15
class
mod |
| 34 | 8, 32, 33 | co 7431 |
. . . . . . . . . . . . . 14
class (𝑎 mod 8) |
| 35 | | c7 12326 |
. . . . . . . . . . . . . . 15
class
7 |
| 36 | 12, 35 | cpr 4628 |
. . . . . . . . . . . . . 14
class {1,
7} |
| 37 | 34, 36 | wcel 2108 |
. . . . . . . . . . . . 13
wff (𝑎 mod 8) ∈ {1,
7} |
| 38 | 37, 12, 19 | cif 4525 |
. . . . . . . . . . . 12
class if((𝑎 mod 8) ∈ {1, 7}, 1,
-1) |
| 39 | 31, 6, 38 | cif 4525 |
. . . . . . . . . . 11
class if(2
∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1,
-1)) |
| 40 | | cmin 11492 |
. . . . . . . . . . . . . . . . 17
class
− |
| 41 | 26, 12, 40 | co 7431 |
. . . . . . . . . . . . . . . 16
class (𝑚 − 1) |
| 42 | | cdiv 11920 |
. . . . . . . . . . . . . . . 16
class
/ |
| 43 | 41, 9, 42 | co 7431 |
. . . . . . . . . . . . . . 15
class ((𝑚 − 1) /
2) |
| 44 | 8, 43, 10 | co 7431 |
. . . . . . . . . . . . . 14
class (𝑎↑((𝑚 − 1) / 2)) |
| 45 | | caddc 11158 |
. . . . . . . . . . . . . 14
class
+ |
| 46 | 44, 12, 45 | co 7431 |
. . . . . . . . . . . . 13
class ((𝑎↑((𝑚 − 1) / 2)) + 1) |
| 47 | 46, 26, 33 | co 7431 |
. . . . . . . . . . . 12
class (((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) |
| 48 | 47, 12, 40 | co 7431 |
. . . . . . . . . . 11
class ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1) |
| 49 | 29, 39, 48 | cif 4525 |
. . . . . . . . . 10
class if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1)) |
| 50 | | cpc 16874 |
. . . . . . . . . . 11
class
pCnt |
| 51 | 26, 5, 50 | co 7431 |
. . . . . . . . . 10
class (𝑚 pCnt 𝑛) |
| 52 | 49, 51, 10 | co 7431 |
. . . . . . . . 9
class (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)) |
| 53 | 28, 52, 12 | cif 4525 |
. . . . . . . 8
class if(𝑚 ∈ ℙ, (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)), 1) |
| 54 | 24, 25, 53 | cmpt 5225 |
. . . . . . 7
class (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)), 1)) |
| 55 | 23, 54, 12 | cseq 14042 |
. . . . . 6
class seq1(
· , (𝑚 ∈
ℕ ↦ if(𝑚 ∈
ℙ, (if(𝑚 = 2, if(2
∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)),
((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)), 1))) |
| 56 | 22, 55 | cfv 6561 |
. . . . 5
class (seq1(
· , (𝑚 ∈
ℕ ↦ if(𝑚 ∈
ℙ, (if(𝑚 = 2, if(2
∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)),
((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)), 1)))‘(abs‘𝑛)) |
| 57 | 20, 56, 23 | co 7431 |
. . . 4
class
(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‘𝑛))) |
| 58 | 7, 14, 57 | cif 4525 |
. . 3
class 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‘𝑛)))) |
| 59 | 2, 3, 4, 4, 58 | cmpo 7433 |
. 2
class (𝑎 ∈ ℤ, 𝑛 ∈ ℤ ↦ 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‘𝑛))))) |
| 60 | 1, 59 | wceq 1540 |
1
wff
/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‘𝑛))))) |