| Step |
Hyp |
Ref |
Expression |
| 1 |
|
psgnfzto1st.d |
⊢ 𝐷 = ( 1 ... 𝑁 ) |
| 2 |
|
psgnfzto1st.p |
⊢ 𝑃 = ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐼 , if ( 𝑖 ≤ 𝐼 , ( 𝑖 − 1 ) , 𝑖 ) ) ) |
| 3 |
|
psgnfzto1st.g |
⊢ 𝐺 = ( SymGrp ‘ 𝐷 ) |
| 4 |
|
psgnfzto1st.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
| 5 |
|
psgnfzto1st.s |
⊢ 𝑆 = ( pmSgn ‘ 𝐷 ) |
| 6 |
|
elfz1b |
⊢ ( 𝐼 ∈ ( 1 ... 𝑁 ) ↔ ( 𝐼 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐼 ≤ 𝑁 ) ) |
| 7 |
6
|
biimpi |
⊢ ( 𝐼 ∈ ( 1 ... 𝑁 ) → ( 𝐼 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐼 ≤ 𝑁 ) ) |
| 8 |
7 1
|
eleq2s |
⊢ ( 𝐼 ∈ 𝐷 → ( 𝐼 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐼 ≤ 𝑁 ) ) |
| 9 |
|
3ancoma |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℕ ∧ 𝐼 ≤ 𝑁 ) ↔ ( 𝐼 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐼 ≤ 𝑁 ) ) |
| 10 |
8 9
|
sylibr |
⊢ ( 𝐼 ∈ 𝐷 → ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℕ ∧ 𝐼 ≤ 𝑁 ) ) |
| 11 |
|
df-3an |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℕ ∧ 𝐼 ≤ 𝑁 ) ↔ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℕ ) ∧ 𝐼 ≤ 𝑁 ) ) |
| 12 |
|
breq1 |
⊢ ( 𝑚 = 1 → ( 𝑚 ≤ 𝑁 ↔ 1 ≤ 𝑁 ) ) |
| 13 |
|
id |
⊢ ( 𝑚 = 1 → 𝑚 = 1 ) |
| 14 |
|
breq2 |
⊢ ( 𝑚 = 1 → ( 𝑖 ≤ 𝑚 ↔ 𝑖 ≤ 1 ) ) |
| 15 |
14
|
ifbid |
⊢ ( 𝑚 = 1 → if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) = if ( 𝑖 ≤ 1 , ( 𝑖 − 1 ) , 𝑖 ) ) |
| 16 |
13 15
|
ifeq12d |
⊢ ( 𝑚 = 1 → if ( 𝑖 = 1 , 𝑚 , if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) ) = if ( 𝑖 = 1 , 1 , if ( 𝑖 ≤ 1 , ( 𝑖 − 1 ) , 𝑖 ) ) ) |
| 17 |
16
|
mpteq2dv |
⊢ ( 𝑚 = 1 → ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑚 , if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) ) ) = ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 1 , if ( 𝑖 ≤ 1 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) |
| 18 |
17
|
fveq2d |
⊢ ( 𝑚 = 1 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑚 , if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 1 , if ( 𝑖 ≤ 1 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) ) |
| 19 |
|
oveq1 |
⊢ ( 𝑚 = 1 → ( 𝑚 + 1 ) = ( 1 + 1 ) ) |
| 20 |
19
|
oveq2d |
⊢ ( 𝑚 = 1 → ( - 1 ↑ ( 𝑚 + 1 ) ) = ( - 1 ↑ ( 1 + 1 ) ) ) |
| 21 |
18 20
|
eqeq12d |
⊢ ( 𝑚 = 1 → ( ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑚 , if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑚 + 1 ) ) ↔ ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 1 , if ( 𝑖 ≤ 1 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 1 + 1 ) ) ) ) |
| 22 |
12 21
|
imbi12d |
⊢ ( 𝑚 = 1 → ( ( 𝑚 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑚 , if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑚 + 1 ) ) ) ↔ ( 1 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 1 , if ( 𝑖 ≤ 1 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 1 + 1 ) ) ) ) ) |
| 23 |
|
breq1 |
⊢ ( 𝑚 = 𝑛 → ( 𝑚 ≤ 𝑁 ↔ 𝑛 ≤ 𝑁 ) ) |
| 24 |
|
id |
⊢ ( 𝑚 = 𝑛 → 𝑚 = 𝑛 ) |
| 25 |
|
breq2 |
⊢ ( 𝑚 = 𝑛 → ( 𝑖 ≤ 𝑚 ↔ 𝑖 ≤ 𝑛 ) ) |
| 26 |
25
|
ifbid |
⊢ ( 𝑚 = 𝑛 → if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) = if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) |
| 27 |
24 26
|
ifeq12d |
⊢ ( 𝑚 = 𝑛 → if ( 𝑖 = 1 , 𝑚 , if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) ) = if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) |
| 28 |
27
|
mpteq2dv |
⊢ ( 𝑚 = 𝑛 → ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑚 , if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) ) ) = ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) |
| 29 |
28
|
fveq2d |
⊢ ( 𝑚 = 𝑛 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑚 , if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) ) |
| 30 |
|
oveq1 |
⊢ ( 𝑚 = 𝑛 → ( 𝑚 + 1 ) = ( 𝑛 + 1 ) ) |
| 31 |
30
|
oveq2d |
⊢ ( 𝑚 = 𝑛 → ( - 1 ↑ ( 𝑚 + 1 ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) |
| 32 |
29 31
|
eqeq12d |
⊢ ( 𝑚 = 𝑛 → ( ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑚 , if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑚 + 1 ) ) ↔ ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) |
| 33 |
23 32
|
imbi12d |
⊢ ( 𝑚 = 𝑛 → ( ( 𝑚 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑚 , if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑚 + 1 ) ) ) ↔ ( 𝑛 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) ) |
| 34 |
|
breq1 |
⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑚 ≤ 𝑁 ↔ ( 𝑛 + 1 ) ≤ 𝑁 ) ) |
| 35 |
|
id |
⊢ ( 𝑚 = ( 𝑛 + 1 ) → 𝑚 = ( 𝑛 + 1 ) ) |
| 36 |
|
breq2 |
⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑖 ≤ 𝑚 ↔ 𝑖 ≤ ( 𝑛 + 1 ) ) ) |
| 37 |
36
|
ifbid |
⊢ ( 𝑚 = ( 𝑛 + 1 ) → if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) = if ( 𝑖 ≤ ( 𝑛 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) |
| 38 |
35 37
|
ifeq12d |
⊢ ( 𝑚 = ( 𝑛 + 1 ) → if ( 𝑖 = 1 , 𝑚 , if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) ) = if ( 𝑖 = 1 , ( 𝑛 + 1 ) , if ( 𝑖 ≤ ( 𝑛 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) ) |
| 39 |
38
|
mpteq2dv |
⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑚 , if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) ) ) = ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , ( 𝑛 + 1 ) , if ( 𝑖 ≤ ( 𝑛 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) |
| 40 |
39
|
fveq2d |
⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑚 , if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , ( 𝑛 + 1 ) , if ( 𝑖 ≤ ( 𝑛 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) ) |
| 41 |
|
oveq1 |
⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑚 + 1 ) = ( ( 𝑛 + 1 ) + 1 ) ) |
| 42 |
41
|
oveq2d |
⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( - 1 ↑ ( 𝑚 + 1 ) ) = ( - 1 ↑ ( ( 𝑛 + 1 ) + 1 ) ) ) |
| 43 |
40 42
|
eqeq12d |
⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑚 , if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑚 + 1 ) ) ↔ ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , ( 𝑛 + 1 ) , if ( 𝑖 ≤ ( 𝑛 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( ( 𝑛 + 1 ) + 1 ) ) ) ) |
| 44 |
34 43
|
imbi12d |
⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ( 𝑚 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑚 , if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑚 + 1 ) ) ) ↔ ( ( 𝑛 + 1 ) ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , ( 𝑛 + 1 ) , if ( 𝑖 ≤ ( 𝑛 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( ( 𝑛 + 1 ) + 1 ) ) ) ) ) |
| 45 |
|
breq1 |
⊢ ( 𝑚 = 𝐼 → ( 𝑚 ≤ 𝑁 ↔ 𝐼 ≤ 𝑁 ) ) |
| 46 |
|
id |
⊢ ( 𝑚 = 𝐼 → 𝑚 = 𝐼 ) |
| 47 |
|
breq2 |
⊢ ( 𝑚 = 𝐼 → ( 𝑖 ≤ 𝑚 ↔ 𝑖 ≤ 𝐼 ) ) |
| 48 |
47
|
ifbid |
⊢ ( 𝑚 = 𝐼 → if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) = if ( 𝑖 ≤ 𝐼 , ( 𝑖 − 1 ) , 𝑖 ) ) |
| 49 |
46 48
|
ifeq12d |
⊢ ( 𝑚 = 𝐼 → if ( 𝑖 = 1 , 𝑚 , if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) ) = if ( 𝑖 = 1 , 𝐼 , if ( 𝑖 ≤ 𝐼 , ( 𝑖 − 1 ) , 𝑖 ) ) ) |
| 50 |
49
|
mpteq2dv |
⊢ ( 𝑚 = 𝐼 → ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑚 , if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) ) ) = ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐼 , if ( 𝑖 ≤ 𝐼 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) |
| 51 |
50 2
|
eqtr4di |
⊢ ( 𝑚 = 𝐼 → ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑚 , if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) ) ) = 𝑃 ) |
| 52 |
51
|
fveq2d |
⊢ ( 𝑚 = 𝐼 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑚 , if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( 𝑆 ‘ 𝑃 ) ) |
| 53 |
|
oveq1 |
⊢ ( 𝑚 = 𝐼 → ( 𝑚 + 1 ) = ( 𝐼 + 1 ) ) |
| 54 |
53
|
oveq2d |
⊢ ( 𝑚 = 𝐼 → ( - 1 ↑ ( 𝑚 + 1 ) ) = ( - 1 ↑ ( 𝐼 + 1 ) ) ) |
| 55 |
52 54
|
eqeq12d |
⊢ ( 𝑚 = 𝐼 → ( ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑚 , if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑚 + 1 ) ) ↔ ( 𝑆 ‘ 𝑃 ) = ( - 1 ↑ ( 𝐼 + 1 ) ) ) ) |
| 56 |
45 55
|
imbi12d |
⊢ ( 𝑚 = 𝐼 → ( ( 𝑚 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑚 , if ( 𝑖 ≤ 𝑚 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑚 + 1 ) ) ) ↔ ( 𝐼 ≤ 𝑁 → ( 𝑆 ‘ 𝑃 ) = ( - 1 ↑ ( 𝐼 + 1 ) ) ) ) ) |
| 57 |
|
fzfi |
⊢ ( 1 ... 𝑁 ) ∈ Fin |
| 58 |
1 57
|
eqeltri |
⊢ 𝐷 ∈ Fin |
| 59 |
5
|
psgnid |
⊢ ( 𝐷 ∈ Fin → ( 𝑆 ‘ ( I ↾ 𝐷 ) ) = 1 ) |
| 60 |
58 59
|
ax-mp |
⊢ ( 𝑆 ‘ ( I ↾ 𝐷 ) ) = 1 |
| 61 |
|
eqid |
⊢ 1 = 1 |
| 62 |
|
eqid |
⊢ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 1 , if ( 𝑖 ≤ 1 , ( 𝑖 − 1 ) , 𝑖 ) ) ) = ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 1 , if ( 𝑖 ≤ 1 , ( 𝑖 − 1 ) , 𝑖 ) ) ) |
| 63 |
1 62
|
fzto1st1 |
⊢ ( 1 = 1 → ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 1 , if ( 𝑖 ≤ 1 , ( 𝑖 − 1 ) , 𝑖 ) ) ) = ( I ↾ 𝐷 ) ) |
| 64 |
61 63
|
ax-mp |
⊢ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 1 , if ( 𝑖 ≤ 1 , ( 𝑖 − 1 ) , 𝑖 ) ) ) = ( I ↾ 𝐷 ) |
| 65 |
64
|
fveq2i |
⊢ ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 1 , if ( 𝑖 ≤ 1 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( 𝑆 ‘ ( I ↾ 𝐷 ) ) |
| 66 |
|
1p1e2 |
⊢ ( 1 + 1 ) = 2 |
| 67 |
66
|
oveq2i |
⊢ ( - 1 ↑ ( 1 + 1 ) ) = ( - 1 ↑ 2 ) |
| 68 |
|
neg1sqe1 |
⊢ ( - 1 ↑ 2 ) = 1 |
| 69 |
67 68
|
eqtri |
⊢ ( - 1 ↑ ( 1 + 1 ) ) = 1 |
| 70 |
60 65 69
|
3eqtr4i |
⊢ ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 1 , if ( 𝑖 ≤ 1 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 1 + 1 ) ) |
| 71 |
70
|
2a1i |
⊢ ( 𝑁 ∈ ℕ → ( 1 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 1 , if ( 𝑖 ≤ 1 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 1 + 1 ) ) ) ) |
| 72 |
|
simplr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → 𝑛 ∈ ℕ ) |
| 73 |
72
|
peano2nnd |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( 𝑛 + 1 ) ∈ ℕ ) |
| 74 |
|
simpll |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → 𝑁 ∈ ℕ ) |
| 75 |
|
simpr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( 𝑛 + 1 ) ≤ 𝑁 ) |
| 76 |
73 74 75
|
3jca |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( ( 𝑛 + 1 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) ) |
| 77 |
|
elfz1b |
⊢ ( ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝑛 + 1 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) ) |
| 78 |
76 77
|
sylibr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) ) |
| 79 |
78 1
|
eleqtrrdi |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( 𝑛 + 1 ) ∈ 𝐷 ) |
| 80 |
1
|
psgnfzto1stlem |
⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑛 + 1 ) ∈ 𝐷 ) → ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , ( 𝑛 + 1 ) , if ( 𝑖 ≤ ( 𝑛 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑛 , ( 𝑛 + 1 ) } ) ∘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) ) |
| 81 |
72 79 80
|
syl2anc |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , ( 𝑛 + 1 ) , if ( 𝑖 ≤ ( 𝑛 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑛 , ( 𝑛 + 1 ) } ) ∘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) ) |
| 82 |
81
|
adantlr |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , ( 𝑛 + 1 ) , if ( 𝑖 ≤ ( 𝑛 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑛 , ( 𝑛 + 1 ) } ) ∘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) ) |
| 83 |
82
|
fveq2d |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , ( 𝑛 + 1 ) , if ( 𝑖 ≤ ( 𝑛 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( 𝑆 ‘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑛 , ( 𝑛 + 1 ) } ) ∘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) ) ) |
| 84 |
58
|
a1i |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → 𝐷 ∈ Fin ) |
| 85 |
|
eqid |
⊢ ran ( pmTrsp ‘ 𝐷 ) = ran ( pmTrsp ‘ 𝐷 ) |
| 86 |
85 3 4
|
symgtrf |
⊢ ran ( pmTrsp ‘ 𝐷 ) ⊆ 𝐵 |
| 87 |
|
eqid |
⊢ ( pmTrsp ‘ 𝐷 ) = ( pmTrsp ‘ 𝐷 ) |
| 88 |
1 87
|
pmtrto1cl |
⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑛 + 1 ) ∈ 𝐷 ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑛 , ( 𝑛 + 1 ) } ) ∈ ran ( pmTrsp ‘ 𝐷 ) ) |
| 89 |
72 79 88
|
syl2anc |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑛 , ( 𝑛 + 1 ) } ) ∈ ran ( pmTrsp ‘ 𝐷 ) ) |
| 90 |
89
|
adantlr |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑛 , ( 𝑛 + 1 ) } ) ∈ ran ( pmTrsp ‘ 𝐷 ) ) |
| 91 |
86 90
|
sselid |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑛 , ( 𝑛 + 1 ) } ) ∈ 𝐵 ) |
| 92 |
72
|
nnred |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → 𝑛 ∈ ℝ ) |
| 93 |
|
1red |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → 1 ∈ ℝ ) |
| 94 |
92 93
|
readdcld |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( 𝑛 + 1 ) ∈ ℝ ) |
| 95 |
74
|
nnred |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → 𝑁 ∈ ℝ ) |
| 96 |
92
|
lep1d |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → 𝑛 ≤ ( 𝑛 + 1 ) ) |
| 97 |
92 94 95 96 75
|
letrd |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → 𝑛 ≤ 𝑁 ) |
| 98 |
72 74 97
|
3jca |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( 𝑛 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑛 ≤ 𝑁 ) ) |
| 99 |
|
elfz1b |
⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑛 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑛 ≤ 𝑁 ) ) |
| 100 |
98 99
|
sylibr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → 𝑛 ∈ ( 1 ... 𝑁 ) ) |
| 101 |
100 1
|
eleqtrrdi |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → 𝑛 ∈ 𝐷 ) |
| 102 |
101
|
adantlr |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → 𝑛 ∈ 𝐷 ) |
| 103 |
|
eqid |
⊢ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) = ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) |
| 104 |
1 103 3 4
|
fzto1st |
⊢ ( 𝑛 ∈ 𝐷 → ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ∈ 𝐵 ) |
| 105 |
102 104
|
syl |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ∈ 𝐵 ) |
| 106 |
3 5 4
|
psgnco |
⊢ ( ( 𝐷 ∈ Fin ∧ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑛 , ( 𝑛 + 1 ) } ) ∈ 𝐵 ∧ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ∈ 𝐵 ) → ( 𝑆 ‘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑛 , ( 𝑛 + 1 ) } ) ∘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) ) = ( ( 𝑆 ‘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑛 , ( 𝑛 + 1 ) } ) ) · ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) ) ) |
| 107 |
84 91 105 106
|
syl3anc |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( 𝑆 ‘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑛 , ( 𝑛 + 1 ) } ) ∘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) ) = ( ( 𝑆 ‘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑛 , ( 𝑛 + 1 ) } ) ) · ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) ) ) |
| 108 |
3 85 5
|
psgnpmtr |
⊢ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑛 , ( 𝑛 + 1 ) } ) ∈ ran ( pmTrsp ‘ 𝐷 ) → ( 𝑆 ‘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑛 , ( 𝑛 + 1 ) } ) ) = - 1 ) |
| 109 |
89 108
|
syl |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( 𝑆 ‘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑛 , ( 𝑛 + 1 ) } ) ) = - 1 ) |
| 110 |
109
|
adantlr |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( 𝑆 ‘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑛 , ( 𝑛 + 1 ) } ) ) = - 1 ) |
| 111 |
97
|
adantlr |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → 𝑛 ≤ 𝑁 ) |
| 112 |
|
simplr |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( 𝑛 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) |
| 113 |
111 112
|
mpd |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) |
| 114 |
110 113
|
oveq12d |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( ( 𝑆 ‘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑛 , ( 𝑛 + 1 ) } ) ) · ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) ) = ( - 1 · ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) |
| 115 |
|
neg1cn |
⊢ - 1 ∈ ℂ |
| 116 |
|
peano2nn |
⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ℕ ) |
| 117 |
116
|
nnnn0d |
⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ℕ0 ) |
| 118 |
|
expp1 |
⊢ ( ( - 1 ∈ ℂ ∧ ( 𝑛 + 1 ) ∈ ℕ0 ) → ( - 1 ↑ ( ( 𝑛 + 1 ) + 1 ) ) = ( ( - 1 ↑ ( 𝑛 + 1 ) ) · - 1 ) ) |
| 119 |
115 117 118
|
sylancr |
⊢ ( 𝑛 ∈ ℕ → ( - 1 ↑ ( ( 𝑛 + 1 ) + 1 ) ) = ( ( - 1 ↑ ( 𝑛 + 1 ) ) · - 1 ) ) |
| 120 |
115
|
a1i |
⊢ ( 𝑛 ∈ ℕ → - 1 ∈ ℂ ) |
| 121 |
120 117
|
expcld |
⊢ ( 𝑛 ∈ ℕ → ( - 1 ↑ ( 𝑛 + 1 ) ) ∈ ℂ ) |
| 122 |
121 120
|
mulcomd |
⊢ ( 𝑛 ∈ ℕ → ( ( - 1 ↑ ( 𝑛 + 1 ) ) · - 1 ) = ( - 1 · ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) |
| 123 |
119 122
|
eqtr2d |
⊢ ( 𝑛 ∈ ℕ → ( - 1 · ( - 1 ↑ ( 𝑛 + 1 ) ) ) = ( - 1 ↑ ( ( 𝑛 + 1 ) + 1 ) ) ) |
| 124 |
123
|
ad3antlr |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( - 1 · ( - 1 ↑ ( 𝑛 + 1 ) ) ) = ( - 1 ↑ ( ( 𝑛 + 1 ) + 1 ) ) ) |
| 125 |
114 124
|
eqtrd |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( ( 𝑆 ‘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑛 , ( 𝑛 + 1 ) } ) ) · ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) ) = ( - 1 ↑ ( ( 𝑛 + 1 ) + 1 ) ) ) |
| 126 |
83 107 125
|
3eqtrd |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) ∧ ( 𝑛 + 1 ) ≤ 𝑁 ) → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , ( 𝑛 + 1 ) , if ( 𝑖 ≤ ( 𝑛 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( ( 𝑛 + 1 ) + 1 ) ) ) |
| 127 |
126
|
ex |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝑛 , if ( 𝑖 ≤ 𝑛 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( 𝑛 + 1 ) ) ) ) → ( ( 𝑛 + 1 ) ≤ 𝑁 → ( 𝑆 ‘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , ( 𝑛 + 1 ) , if ( 𝑖 ≤ ( 𝑛 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) = ( - 1 ↑ ( ( 𝑛 + 1 ) + 1 ) ) ) ) |
| 128 |
22 33 44 56 71 127
|
nnindd |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℕ ) → ( 𝐼 ≤ 𝑁 → ( 𝑆 ‘ 𝑃 ) = ( - 1 ↑ ( 𝐼 + 1 ) ) ) ) |
| 129 |
128
|
imp |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℕ ) ∧ 𝐼 ≤ 𝑁 ) → ( 𝑆 ‘ 𝑃 ) = ( - 1 ↑ ( 𝐼 + 1 ) ) ) |
| 130 |
11 129
|
sylbi |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℕ ∧ 𝐼 ≤ 𝑁 ) → ( 𝑆 ‘ 𝑃 ) = ( - 1 ↑ ( 𝐼 + 1 ) ) ) |
| 131 |
10 130
|
syl |
⊢ ( 𝐼 ∈ 𝐷 → ( 𝑆 ‘ 𝑃 ) = ( - 1 ↑ ( 𝐼 + 1 ) ) ) |