| Step |
Hyp |
Ref |
Expression |
| 1 |
|
finxpeq2 |
|- ( n = (/) -> ( (/) ^^ n ) = ( (/) ^^ (/) ) ) |
| 2 |
1
|
eqeq1d |
|- ( n = (/) -> ( ( (/) ^^ n ) = (/) <-> ( (/) ^^ (/) ) = (/) ) ) |
| 3 |
|
finxpeq2 |
|- ( n = m -> ( (/) ^^ n ) = ( (/) ^^ m ) ) |
| 4 |
3
|
eqeq1d |
|- ( n = m -> ( ( (/) ^^ n ) = (/) <-> ( (/) ^^ m ) = (/) ) ) |
| 5 |
|
finxpeq2 |
|- ( n = suc m -> ( (/) ^^ n ) = ( (/) ^^ suc m ) ) |
| 6 |
5
|
eqeq1d |
|- ( n = suc m -> ( ( (/) ^^ n ) = (/) <-> ( (/) ^^ suc m ) = (/) ) ) |
| 7 |
|
finxpeq2 |
|- ( n = N -> ( (/) ^^ n ) = ( (/) ^^ N ) ) |
| 8 |
7
|
eqeq1d |
|- ( n = N -> ( ( (/) ^^ n ) = (/) <-> ( (/) ^^ N ) = (/) ) ) |
| 9 |
|
finxp0 |
|- ( (/) ^^ (/) ) = (/) |
| 10 |
|
suceq |
|- ( m = (/) -> suc m = suc (/) ) |
| 11 |
|
df-1o |
|- 1o = suc (/) |
| 12 |
10 11
|
eqtr4di |
|- ( m = (/) -> suc m = 1o ) |
| 13 |
|
finxpeq2 |
|- ( suc m = 1o -> ( (/) ^^ suc m ) = ( (/) ^^ 1o ) ) |
| 14 |
12 13
|
syl |
|- ( m = (/) -> ( (/) ^^ suc m ) = ( (/) ^^ 1o ) ) |
| 15 |
|
finxp1o |
|- ( (/) ^^ 1o ) = (/) |
| 16 |
14 15
|
eqtrdi |
|- ( m = (/) -> ( (/) ^^ suc m ) = (/) ) |
| 17 |
16
|
adantl |
|- ( ( m e. _om /\ m = (/) ) -> ( (/) ^^ suc m ) = (/) ) |
| 18 |
|
finxpsuc |
|- ( ( m e. _om /\ m =/= (/) ) -> ( (/) ^^ suc m ) = ( ( (/) ^^ m ) X. (/) ) ) |
| 19 |
|
xp0 |
|- ( ( (/) ^^ m ) X. (/) ) = (/) |
| 20 |
18 19
|
eqtrdi |
|- ( ( m e. _om /\ m =/= (/) ) -> ( (/) ^^ suc m ) = (/) ) |
| 21 |
17 20
|
pm2.61dane |
|- ( m e. _om -> ( (/) ^^ suc m ) = (/) ) |
| 22 |
21
|
a1d |
|- ( m e. _om -> ( ( (/) ^^ m ) = (/) -> ( (/) ^^ suc m ) = (/) ) ) |
| 23 |
2 4 6 8 9 22
|
finds |
|- ( N e. _om -> ( (/) ^^ N ) = (/) ) |
| 24 |
|
finxpnom |
|- ( -. N e. _om -> ( (/) ^^ N ) = (/) ) |
| 25 |
23 24
|
pm2.61i |
|- ( (/) ^^ N ) = (/) |