Step | Hyp | Ref
| Expression |
1 | | elzn0s 28393 |
. 2
⊢ (𝐴 ∈ ℤs
↔ (𝐴 ∈ No ∧ (𝐴 ∈ ℕ0s ∨ (
-us ‘𝐴)
∈ ℕ0s))) |
2 | | n0scut 28347 |
. . . . 5
⊢ (𝐴 ∈ ℕ0s
→ 𝐴 = ({(𝐴 -s 1s )}
|s ∅)) |
3 | | n0sno 28337 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ0s
→ 𝐴 ∈ No ) |
4 | | 1sno 27881 |
. . . . . . . . 9
⊢
1s ∈ No |
5 | 4 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ0s
→ 1s ∈ No ) |
6 | 3, 5 | subscld 28102 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ0s
→ (𝐴 -s
1s ) ∈ No ) |
7 | | snelpwi 5466 |
. . . . . . 7
⊢ ((𝐴 -s 1s )
∈ No → {(𝐴 -s 1s )} ∈
𝒫 No ) |
8 | | nulssgt 27852 |
. . . . . . 7
⊢ ({(𝐴 -s 1s )}
∈ 𝒫 No → {(𝐴 -s 1s )} <<s
∅) |
9 | 6, 7, 8 | 3syl 18 |
. . . . . 6
⊢ (𝐴 ∈ ℕ0s
→ {(𝐴 -s
1s )} <<s ∅) |
10 | | slerflex 27817 |
. . . . . . . 8
⊢ ((𝐴 -s 1s )
∈ No → (𝐴 -s 1s ) ≤s (𝐴 -s 1s
)) |
11 | 6, 10 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ0s
→ (𝐴 -s
1s ) ≤s (𝐴
-s 1s )) |
12 | | ovex 7478 |
. . . . . . . . 9
⊢ (𝐴 -s 1s )
∈ V |
13 | | breq1 5172 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐴 -s 1s ) → (𝑥 ≤s 𝑦 ↔ (𝐴 -s 1s ) ≤s 𝑦)) |
14 | 13 | rexbidv 3181 |
. . . . . . . . 9
⊢ (𝑥 = (𝐴 -s 1s ) →
(∃𝑦 ∈ {(𝐴 -s 1s
)}𝑥 ≤s 𝑦 ↔ ∃𝑦 ∈ {(𝐴 -s 1s )} (𝐴 -s 1s )
≤s 𝑦)) |
15 | 12, 14 | ralsn 4705 |
. . . . . . . 8
⊢
(∀𝑥 ∈
{(𝐴 -s
1s )}∃𝑦
∈ {(𝐴 -s
1s )}𝑥 ≤s
𝑦 ↔ ∃𝑦 ∈ {(𝐴 -s 1s )} (𝐴 -s 1s )
≤s 𝑦) |
16 | | breq2 5173 |
. . . . . . . . 9
⊢ (𝑦 = (𝐴 -s 1s ) →
((𝐴 -s
1s ) ≤s 𝑦
↔ (𝐴 -s
1s ) ≤s (𝐴
-s 1s ))) |
17 | 12, 16 | rexsn 4706 |
. . . . . . . 8
⊢
(∃𝑦 ∈
{(𝐴 -s
1s )} (𝐴
-s 1s ) ≤s 𝑦 ↔ (𝐴 -s 1s ) ≤s (𝐴 -s 1s
)) |
18 | 15, 17 | bitri 275 |
. . . . . . 7
⊢
(∀𝑥 ∈
{(𝐴 -s
1s )}∃𝑦
∈ {(𝐴 -s
1s )}𝑥 ≤s
𝑦 ↔ (𝐴 -s 1s ) ≤s (𝐴 -s 1s
)) |
19 | 11, 18 | sylibr 234 |
. . . . . 6
⊢ (𝐴 ∈ ℕ0s
→ ∀𝑥 ∈
{(𝐴 -s
1s )}∃𝑦
∈ {(𝐴 -s
1s )}𝑥 ≤s
𝑦) |
20 | | ral0 4532 |
. . . . . . 7
⊢
∀𝑥 ∈
∅ ∃𝑦 ∈
{(𝐴 +s
1s )}𝑦 ≤s
𝑥 |
21 | 20 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℕ0s
→ ∀𝑥 ∈
∅ ∃𝑦 ∈
{(𝐴 +s
1s )}𝑦 ≤s
𝑥) |
22 | 3 | sltm1d 28140 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ0s
→ (𝐴 -s
1s ) <s 𝐴) |
23 | 6, 3, 22 | ssltsn 27846 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ0s
→ {(𝐴 -s
1s )} <<s {𝐴}) |
24 | 2 | sneqd 4660 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ0s
→ {𝐴} = {({(𝐴 -s 1s )}
|s ∅)}) |
25 | 23, 24 | breqtrd 5195 |
. . . . . 6
⊢ (𝐴 ∈ ℕ0s
→ {(𝐴 -s
1s )} <<s {({(𝐴 -s 1s )} |s
∅)}) |
26 | 3, 5 | addscld 28022 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ0s
→ (𝐴 +s
1s ) ∈ No ) |
27 | 3 | sltp1d 28057 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ0s
→ 𝐴 <s (𝐴 +s 1s
)) |
28 | 3, 26, 27 | ssltsn 27846 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ0s
→ {𝐴} <<s
{(𝐴 +s
1s )}) |
29 | 24, 28 | eqbrtrrd 5193 |
. . . . . 6
⊢ (𝐴 ∈ ℕ0s
→ {({(𝐴 -s
1s )} |s ∅)} <<s {(𝐴 +s 1s
)}) |
30 | 9, 19, 21, 25, 29 | cofcut1d 27964 |
. . . . 5
⊢ (𝐴 ∈ ℕ0s
→ ({(𝐴 -s
1s )} |s ∅) = ({(𝐴 -s 1s )} |s {(𝐴 +s 1s
)})) |
31 | 2, 30 | eqtrd 2774 |
. . . 4
⊢ (𝐴 ∈ ℕ0s
→ 𝐴 = ({(𝐴 -s 1s )}
|s {(𝐴 +s
1s )})) |
32 | 31 | adantl 481 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐴 ∈
ℕ0s) → 𝐴 = ({(𝐴 -s 1s )} |s {(𝐴 +s 1s
)})) |
33 | | negsfn 28064 |
. . . . . . . 8
⊢
-us Fn No |
34 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → 𝐴 ∈
No ) |
35 | 4 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) →
1s ∈ No ) |
36 | 34, 35 | addscld 28022 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → (𝐴 +s 1s )
∈ No ) |
37 | | fnsnfv 6999 |
. . . . . . . 8
⊢ ((
-us Fn No ∧ (𝐴 +s 1s ) ∈ No ) → {( -us ‘(𝐴 +s 1s ))} = (
-us “ {(𝐴
+s 1s )})) |
38 | 33, 36, 37 | sylancr 586 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → {(
-us ‘(𝐴
+s 1s ))} = ( -us “ {(𝐴 +s 1s
)})) |
39 | | negsdi 28091 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 1s ∈ No ) →
( -us ‘(𝐴
+s 1s )) = (( -us ‘𝐴) +s ( -us ‘
1s ))) |
40 | 34, 4, 39 | sylancl 585 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → (
-us ‘(𝐴
+s 1s )) = (( -us ‘𝐴) +s ( -us ‘
1s ))) |
41 | | n0sno 28337 |
. . . . . . . . . . 11
⊢ ((
-us ‘𝐴)
∈ ℕ0s → ( -us ‘𝐴) ∈ No
) |
42 | 41 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → (
-us ‘𝐴)
∈ No ) |
43 | 42, 35 | subsvald 28100 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → ((
-us ‘𝐴)
-s 1s ) = (( -us ‘𝐴) +s ( -us ‘
1s ))) |
44 | 40, 43 | eqtr4d 2777 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → (
-us ‘(𝐴
+s 1s )) = (( -us ‘𝐴) -s 1s
)) |
45 | 44 | sneqd 4660 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → {(
-us ‘(𝐴
+s 1s ))} = {(( -us ‘𝐴) -s 1s
)}) |
46 | 38, 45 | eqtr3d 2776 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → (
-us “ {(𝐴
+s 1s )}) = {(( -us ‘𝐴) -s 1s
)}) |
47 | 34, 35 | subscld 28102 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → (𝐴 -s 1s )
∈ No ) |
48 | | fnsnfv 6999 |
. . . . . . . 8
⊢ ((
-us Fn No ∧ (𝐴 -s 1s ) ∈ No ) → {( -us ‘(𝐴 -s 1s ))} = (
-us “ {(𝐴
-s 1s )})) |
49 | 33, 47, 48 | sylancr 586 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → {(
-us ‘(𝐴
-s 1s ))} = ( -us “ {(𝐴 -s 1s
)})) |
50 | 35, 34 | subsvald 28100 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → (
1s -s 𝐴) = ( 1s +s (
-us ‘𝐴))) |
51 | 34, 35 | negsubsdi2d 28119 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → (
-us ‘(𝐴
-s 1s )) = ( 1s -s 𝐴)) |
52 | 42, 35 | addscomd 28009 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → ((
-us ‘𝐴)
+s 1s ) = ( 1s +s ( -us
‘𝐴))) |
53 | 50, 51, 52 | 3eqtr4d 2784 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → (
-us ‘(𝐴
-s 1s )) = (( -us ‘𝐴) +s 1s
)) |
54 | 53 | sneqd 4660 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → {(
-us ‘(𝐴
-s 1s ))} = {(( -us ‘𝐴) +s 1s
)}) |
55 | 49, 54 | eqtr3d 2776 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → (
-us “ {(𝐴
-s 1s )}) = {(( -us ‘𝐴) +s 1s
)}) |
56 | 46, 55 | oveq12d 7463 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → ((
-us “ {(𝐴
+s 1s )}) |s ( -us “ {(𝐴 -s 1s )})) = ({((
-us ‘𝐴)
-s 1s )} |s {(( -us ‘𝐴) +s 1s
)})) |
57 | 34 | sltm1d 28140 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → (𝐴 -s 1s )
<s 𝐴) |
58 | 34 | sltp1d 28057 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → 𝐴 <s (𝐴 +s 1s
)) |
59 | 47, 34, 36, 57, 58 | slttrd 27813 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → (𝐴 -s 1s )
<s (𝐴 +s
1s )) |
60 | 47, 36, 59 | ssltsn 27846 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) →
{(𝐴 -s
1s )} <<s {(𝐴 +s 1s
)}) |
61 | | eqidd 2735 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) →
({(𝐴 -s
1s )} |s {(𝐴
+s 1s )}) = ({(𝐴 -s 1s )} |s {(𝐴 +s 1s
)})) |
62 | 60, 61 | negsunif 28096 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → (
-us ‘({(𝐴
-s 1s )} |s {(𝐴 +s 1s )})) = ((
-us “ {(𝐴
+s 1s )}) |s ( -us “ {(𝐴 -s 1s
)}))) |
63 | | n0scut 28347 |
. . . . . . 7
⊢ ((
-us ‘𝐴)
∈ ℕ0s → ( -us ‘𝐴) = ({(( -us ‘𝐴) -s 1s )}
|s ∅)) |
64 | 4 | a1i 11 |
. . . . . . . . . 10
⊢ ((
-us ‘𝐴)
∈ ℕ0s → 1s ∈
No ) |
65 | 41, 64 | subscld 28102 |
. . . . . . . . 9
⊢ ((
-us ‘𝐴)
∈ ℕ0s → (( -us ‘𝐴) -s 1s ) ∈ No ) |
66 | | snelpwi 5466 |
. . . . . . . . 9
⊢ (((
-us ‘𝐴)
-s 1s ) ∈ No →
{(( -us ‘𝐴) -s 1s )} ∈
𝒫 No ) |
67 | | nulssgt 27852 |
. . . . . . . . 9
⊢ ({((
-us ‘𝐴)
-s 1s )} ∈ 𝒫 No
→ {(( -us ‘𝐴) -s 1s )} <<s
∅) |
68 | 65, 66, 67 | 3syl 18 |
. . . . . . . 8
⊢ ((
-us ‘𝐴)
∈ ℕ0s → {(( -us ‘𝐴) -s 1s )} <<s
∅) |
69 | | slerflex 27817 |
. . . . . . . . . 10
⊢ (((
-us ‘𝐴)
-s 1s ) ∈ No →
(( -us ‘𝐴)
-s 1s ) ≤s (( -us ‘𝐴) -s 1s
)) |
70 | 65, 69 | syl 17 |
. . . . . . . . 9
⊢ ((
-us ‘𝐴)
∈ ℕ0s → (( -us ‘𝐴) -s 1s ) ≤s ((
-us ‘𝐴)
-s 1s )) |
71 | | ovex 7478 |
. . . . . . . . . . 11
⊢ ((
-us ‘𝐴)
-s 1s ) ∈ V |
72 | | breq1 5172 |
. . . . . . . . . . . 12
⊢ (𝑥 = (( -us
‘𝐴) -s
1s ) → (𝑥
≤s 𝑦 ↔ ((
-us ‘𝐴)
-s 1s ) ≤s 𝑦)) |
73 | 72 | rexbidv 3181 |
. . . . . . . . . . 11
⊢ (𝑥 = (( -us
‘𝐴) -s
1s ) → (∃𝑦 ∈ {(( -us ‘𝐴) -s 1s
)}𝑥 ≤s 𝑦 ↔ ∃𝑦 ∈ {(( -us
‘𝐴) -s
1s )} (( -us ‘𝐴) -s 1s ) ≤s 𝑦)) |
74 | 71, 73 | ralsn 4705 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
{(( -us ‘𝐴) -s 1s )}∃𝑦 ∈ {(( -us
‘𝐴) -s
1s )}𝑥 ≤s
𝑦 ↔ ∃𝑦 ∈ {(( -us
‘𝐴) -s
1s )} (( -us ‘𝐴) -s 1s ) ≤s 𝑦) |
75 | | breq2 5173 |
. . . . . . . . . . 11
⊢ (𝑦 = (( -us
‘𝐴) -s
1s ) → ((( -us ‘𝐴) -s 1s ) ≤s 𝑦 ↔ (( -us
‘𝐴) -s
1s ) ≤s (( -us ‘𝐴) -s 1s
))) |
76 | 71, 75 | rexsn 4706 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈ {((
-us ‘𝐴)
-s 1s )} (( -us ‘𝐴) -s 1s ) ≤s 𝑦 ↔ (( -us
‘𝐴) -s
1s ) ≤s (( -us ‘𝐴) -s 1s
)) |
77 | 74, 76 | bitri 275 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
{(( -us ‘𝐴) -s 1s )}∃𝑦 ∈ {(( -us
‘𝐴) -s
1s )}𝑥 ≤s
𝑦 ↔ (( -us
‘𝐴) -s
1s ) ≤s (( -us ‘𝐴) -s 1s
)) |
78 | 70, 77 | sylibr 234 |
. . . . . . . 8
⊢ ((
-us ‘𝐴)
∈ ℕ0s → ∀𝑥 ∈ {(( -us ‘𝐴) -s 1s
)}∃𝑦 ∈ {((
-us ‘𝐴)
-s 1s )}𝑥 ≤s 𝑦) |
79 | | ral0 4532 |
. . . . . . . . 9
⊢
∀𝑥 ∈
∅ ∃𝑦 ∈ {((
-us ‘𝐴)
+s 1s )}𝑦 ≤s 𝑥 |
80 | 79 | a1i 11 |
. . . . . . . 8
⊢ ((
-us ‘𝐴)
∈ ℕ0s → ∀𝑥 ∈ ∅ ∃𝑦 ∈ {(( -us ‘𝐴) +s 1s
)}𝑦 ≤s 𝑥) |
81 | 41 | sltm1d 28140 |
. . . . . . . . . 10
⊢ ((
-us ‘𝐴)
∈ ℕ0s → (( -us ‘𝐴) -s 1s ) <s (
-us ‘𝐴)) |
82 | 65, 41, 81 | ssltsn 27846 |
. . . . . . . . 9
⊢ ((
-us ‘𝐴)
∈ ℕ0s → {(( -us ‘𝐴) -s 1s )} <<s
{( -us ‘𝐴)}) |
83 | 63 | sneqd 4660 |
. . . . . . . . 9
⊢ ((
-us ‘𝐴)
∈ ℕ0s → {( -us ‘𝐴)} = {({(( -us ‘𝐴) -s 1s )}
|s ∅)}) |
84 | 82, 83 | breqtrd 5195 |
. . . . . . . 8
⊢ ((
-us ‘𝐴)
∈ ℕ0s → {(( -us ‘𝐴) -s 1s )} <<s
{({(( -us ‘𝐴) -s 1s )} |s
∅)}) |
85 | 41, 64 | addscld 28022 |
. . . . . . . . . 10
⊢ ((
-us ‘𝐴)
∈ ℕ0s → (( -us ‘𝐴) +s 1s ) ∈ No ) |
86 | 41 | sltp1d 28057 |
. . . . . . . . . 10
⊢ ((
-us ‘𝐴)
∈ ℕ0s → ( -us ‘𝐴) <s (( -us ‘𝐴) +s 1s
)) |
87 | 41, 85, 86 | ssltsn 27846 |
. . . . . . . . 9
⊢ ((
-us ‘𝐴)
∈ ℕ0s → {( -us ‘𝐴)} <<s {(( -us ‘𝐴) +s 1s
)}) |
88 | 83, 87 | eqbrtrrd 5193 |
. . . . . . . 8
⊢ ((
-us ‘𝐴)
∈ ℕ0s → {({(( -us ‘𝐴) -s 1s )}
|s ∅)} <<s {(( -us ‘𝐴) +s 1s
)}) |
89 | 68, 78, 80, 84, 88 | cofcut1d 27964 |
. . . . . . 7
⊢ ((
-us ‘𝐴)
∈ ℕ0s → ({(( -us ‘𝐴) -s 1s )} |s ∅)
= ({(( -us ‘𝐴) -s 1s )} |s {((
-us ‘𝐴)
+s 1s )})) |
90 | 63, 89 | eqtrd 2774 |
. . . . . 6
⊢ ((
-us ‘𝐴)
∈ ℕ0s → ( -us ‘𝐴) = ({(( -us ‘𝐴) -s 1s )}
|s {(( -us ‘𝐴) +s 1s
)})) |
91 | 90 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → (
-us ‘𝐴) =
({(( -us ‘𝐴) -s 1s )} |s {((
-us ‘𝐴)
+s 1s )})) |
92 | 56, 62, 91 | 3eqtr4rd 2785 |
. . . 4
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → (
-us ‘𝐴) =
( -us ‘({(𝐴 -s 1s )} |s {(𝐴 +s 1s
)}))) |
93 | 60 | scutcld 27857 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) →
({(𝐴 -s
1s )} |s {(𝐴
+s 1s )}) ∈ No
) |
94 | | negs11 28090 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ ({(𝐴
-s 1s )} |s {(𝐴 +s 1s )}) ∈
No ) → (( -us ‘𝐴) = ( -us
‘({(𝐴 -s
1s )} |s {(𝐴
+s 1s )})) ↔ 𝐴 = ({(𝐴 -s 1s )} |s {(𝐴 +s 1s
)}))) |
95 | 93, 94 | syldan 590 |
. . . 4
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → ((
-us ‘𝐴) =
( -us ‘({(𝐴 -s 1s )} |s {(𝐴 +s 1s
)})) ↔ 𝐴 = ({(𝐴 -s 1s )}
|s {(𝐴 +s
1s )}))) |
96 | 92, 95 | mpbid 232 |
. . 3
⊢ ((𝐴 ∈
No ∧ ( -us ‘𝐴) ∈ ℕ0s) → 𝐴 = ({(𝐴 -s 1s )} |s {(𝐴 +s 1s
)})) |
97 | 32, 96 | jaodan 958 |
. 2
⊢ ((𝐴 ∈
No ∧ (𝐴 ∈
ℕ0s ∨ ( -us ‘𝐴) ∈ ℕ0s)) → 𝐴 = ({(𝐴 -s 1s )} |s {(𝐴 +s 1s
)})) |
98 | 1, 97 | sylbi 217 |
1
⊢ (𝐴 ∈ ℤs
→ 𝐴 = ({(𝐴 -s 1s )}
|s {(𝐴 +s
1s )})) |