Metamath Proof Explorer


Theorem expval

Description: Value of exponentiation to integer powers. (Contributed by NM, 20-May-2004) (Revised by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion expval ANAN=ifN=01if0<Nseq1××AN1seq1××AN

Proof

Step Hyp Ref Expression
1 simpr x=Ay=Ny=N
2 1 eqeq1d x=Ay=Ny=0N=0
3 1 breq2d x=Ay=N0<y0<N
4 simpl x=Ay=Nx=A
5 4 sneqd x=Ay=Nx=A
6 5 xpeq2d x=Ay=N×x=×A
7 6 seqeq3d x=Ay=Nseq1××x=seq1××A
8 7 1 fveq12d x=Ay=Nseq1××xy=seq1××AN
9 1 negeqd x=Ay=Ny=N
10 7 9 fveq12d x=Ay=Nseq1××xy=seq1××AN
11 10 oveq2d x=Ay=N1seq1××xy=1seq1××AN
12 3 8 11 ifbieq12d x=Ay=Nif0<yseq1××xy1seq1××xy=if0<Nseq1××AN1seq1××AN
13 2 12 ifbieq2d x=Ay=Nify=01if0<yseq1××xy1seq1××xy=ifN=01if0<Nseq1××AN1seq1××AN
14 df-exp ^=x,yify=01if0<yseq1××xy1seq1××xy
15 1ex 1V
16 fvex seq1××ANV
17 ovex 1seq1××ANV
18 16 17 ifex if0<Nseq1××AN1seq1××ANV
19 15 18 ifex ifN=01if0<Nseq1××AN1seq1××ANV
20 13 14 19 ovmpoa ANAN=ifN=01if0<Nseq1××AN1seq1××AN