Metamath Proof Explorer

Theorem qabvexp

Description: Induct the product rule abvmul to find the absolute value of a power. (Contributed by Mario Carneiro, 10-Sep-2014)

Ref Expression
Hypotheses qrng.q 
|- Q = ( CCfld |`s QQ )
qabsabv.a 
|- A = ( AbsVal ` Q )
Assertion qabvexp 
|- ( ( F e. A /\ M e. QQ /\ N e. NN0 ) -> ( F ` ( M ^ N ) ) = ( ( F ` M ) ^ N ) )

Proof

Step Hyp Ref Expression
1 qrng.q 
 |-  Q = ( CCfld |`s QQ )
2 qabsabv.a 
 |-  A = ( AbsVal ` Q )
3 oveq2 
 |-  ( k = 0 -> ( M ^ k ) = ( M ^ 0 ) )
4 3 fveq2d 
 |-  ( k = 0 -> ( F ` ( M ^ k ) ) = ( F ` ( M ^ 0 ) ) )
5 oveq2 
 |-  ( k = 0 -> ( ( F ` M ) ^ k ) = ( ( F ` M ) ^ 0 ) )
6 4 5 eqeq12d 
 |-  ( k = 0 -> ( ( F ` ( M ^ k ) ) = ( ( F ` M ) ^ k ) <-> ( F ` ( M ^ 0 ) ) = ( ( F ` M ) ^ 0 ) ) )
7 6 imbi2d 
 |-  ( k = 0 -> ( ( ( F e. A /\ M e. QQ ) -> ( F ` ( M ^ k ) ) = ( ( F ` M ) ^ k ) ) <-> ( ( F e. A /\ M e. QQ ) -> ( F ` ( M ^ 0 ) ) = ( ( F ` M ) ^ 0 ) ) ) )
8 oveq2 
 |-  ( k = n -> ( M ^ k ) = ( M ^ n ) )
9 8 fveq2d 
 |-  ( k = n -> ( F ` ( M ^ k ) ) = ( F ` ( M ^ n ) ) )
10 oveq2 
 |-  ( k = n -> ( ( F ` M ) ^ k ) = ( ( F ` M ) ^ n ) )
11 9 10 eqeq12d 
 |-  ( k = n -> ( ( F ` ( M ^ k ) ) = ( ( F ` M ) ^ k ) <-> ( F ` ( M ^ n ) ) = ( ( F ` M ) ^ n ) ) )
12 11 imbi2d 
 |-  ( k = n -> ( ( ( F e. A /\ M e. QQ ) -> ( F ` ( M ^ k ) ) = ( ( F ` M ) ^ k ) ) <-> ( ( F e. A /\ M e. QQ ) -> ( F ` ( M ^ n ) ) = ( ( F ` M ) ^ n ) ) ) )
13 oveq2 
 |-  ( k = ( n + 1 ) -> ( M ^ k ) = ( M ^ ( n + 1 ) ) )
14 13 fveq2d 
 |-  ( k = ( n + 1 ) -> ( F ` ( M ^ k ) ) = ( F ` ( M ^ ( n + 1 ) ) ) )
15 oveq2 
 |-  ( k = ( n + 1 ) -> ( ( F ` M ) ^ k ) = ( ( F ` M ) ^ ( n + 1 ) ) )
16 14 15 eqeq12d 
 |-  ( k = ( n + 1 ) -> ( ( F ` ( M ^ k ) ) = ( ( F ` M ) ^ k ) <-> ( F ` ( M ^ ( n + 1 ) ) ) = ( ( F ` M ) ^ ( n + 1 ) ) ) )
17 16 imbi2d 
 |-  ( k = ( n + 1 ) -> ( ( ( F e. A /\ M e. QQ ) -> ( F ` ( M ^ k ) ) = ( ( F ` M ) ^ k ) ) <-> ( ( F e. A /\ M e. QQ ) -> ( F ` ( M ^ ( n + 1 ) ) ) = ( ( F ` M ) ^ ( n + 1 ) ) ) ) )
18 oveq2 
 |-  ( k = N -> ( M ^ k ) = ( M ^ N ) )
19 18 fveq2d 
 |-  ( k = N -> ( F ` ( M ^ k ) ) = ( F ` ( M ^ N ) ) )
20 oveq2 
 |-  ( k = N -> ( ( F ` M ) ^ k ) = ( ( F ` M ) ^ N ) )
21 19 20 eqeq12d 
 |-  ( k = N -> ( ( F ` ( M ^ k ) ) = ( ( F ` M ) ^ k ) <-> ( F ` ( M ^ N ) ) = ( ( F ` M ) ^ N ) ) )
22 21 imbi2d 
 |-  ( k = N -> ( ( ( F e. A /\ M e. QQ ) -> ( F ` ( M ^ k ) ) = ( ( F ` M ) ^ k ) ) <-> ( ( F e. A /\ M e. QQ ) -> ( F ` ( M ^ N ) ) = ( ( F ` M ) ^ N ) ) ) )
23 ax-1ne0 
 |-  1 =/= 0
24 1 qrng1 
 |-  1 = ( 1r ` Q )
25 1 qrng0 
 |-  0 = ( 0g ` Q )
26 2 24 25 abv1z 
 |-  ( ( F e. A /\ 1 =/= 0 ) -> ( F ` 1 ) = 1 )
27 23 26 mpan2 
 |-  ( F e. A -> ( F ` 1 ) = 1 )
28 27 adantr 
 |-  ( ( F e. A /\ M e. QQ ) -> ( F ` 1 ) = 1 )
29 qcn 
 |-  ( M e. QQ -> M e. CC )
30 29 adantl 
 |-  ( ( F e. A /\ M e. QQ ) -> M e. CC )
31 30 exp0d 
 |-  ( ( F e. A /\ M e. QQ ) -> ( M ^ 0 ) = 1 )
32 31 fveq2d 
 |-  ( ( F e. A /\ M e. QQ ) -> ( F ` ( M ^ 0 ) ) = ( F ` 1 ) )
33 1 qrngbas 
 |-  QQ = ( Base ` Q )
34 2 33 abvcl 
 |-  ( ( F e. A /\ M e. QQ ) -> ( F ` M ) e. RR )
35 34 recnd 
 |-  ( ( F e. A /\ M e. QQ ) -> ( F ` M ) e. CC )
36 35 exp0d 
 |-  ( ( F e. A /\ M e. QQ ) -> ( ( F ` M ) ^ 0 ) = 1 )
37 28 32 36 3eqtr4d 
 |-  ( ( F e. A /\ M e. QQ ) -> ( F ` ( M ^ 0 ) ) = ( ( F ` M ) ^ 0 ) )
38 oveq1 
 |-  ( ( F ` ( M ^ n ) ) = ( ( F ` M ) ^ n ) -> ( ( F ` ( M ^ n ) ) x. ( F ` M ) ) = ( ( ( F ` M ) ^ n ) x. ( F ` M ) ) )
39 expp1 
 |-  ( ( M e. CC /\ n e. NN0 ) -> ( M ^ ( n + 1 ) ) = ( ( M ^ n ) x. M ) )
40 30 39 sylan 
 |-  ( ( ( F e. A /\ M e. QQ ) /\ n e. NN0 ) -> ( M ^ ( n + 1 ) ) = ( ( M ^ n ) x. M ) )
41 40 fveq2d 
 |-  ( ( ( F e. A /\ M e. QQ ) /\ n e. NN0 ) -> ( F ` ( M ^ ( n + 1 ) ) ) = ( F ` ( ( M ^ n ) x. M ) ) )
42 simpll 
 |-  ( ( ( F e. A /\ M e. QQ ) /\ n e. NN0 ) -> F e. A )
43 qexpcl 
 |-  ( ( M e. QQ /\ n e. NN0 ) -> ( M ^ n ) e. QQ )
44 43 adantll 
 |-  ( ( ( F e. A /\ M e. QQ ) /\ n e. NN0 ) -> ( M ^ n ) e. QQ )
45 simplr 
 |-  ( ( ( F e. A /\ M e. QQ ) /\ n e. NN0 ) -> M e. QQ )
46 qex 
 |-  QQ e. _V
47 cnfldmul 
 |-  x. = ( .r ` CCfld )
48 1 47 ressmulr 
 |-  ( QQ e. _V -> x. = ( .r ` Q ) )
49 46 48 ax-mp 
 |-  x. = ( .r ` Q )
50 2 33 49 abvmul 
 |-  ( ( F e. A /\ ( M ^ n ) e. QQ /\ M e. QQ ) -> ( F ` ( ( M ^ n ) x. M ) ) = ( ( F ` ( M ^ n ) ) x. ( F ` M ) ) )
51 42 44 45 50 syl3anc 
 |-  ( ( ( F e. A /\ M e. QQ ) /\ n e. NN0 ) -> ( F ` ( ( M ^ n ) x. M ) ) = ( ( F ` ( M ^ n ) ) x. ( F ` M ) ) )
52 41 51 eqtrd 
 |-  ( ( ( F e. A /\ M e. QQ ) /\ n e. NN0 ) -> ( F ` ( M ^ ( n + 1 ) ) ) = ( ( F ` ( M ^ n ) ) x. ( F ` M ) ) )
53 expp1 
 |-  ( ( ( F ` M ) e. CC /\ n e. NN0 ) -> ( ( F ` M ) ^ ( n + 1 ) ) = ( ( ( F ` M ) ^ n ) x. ( F ` M ) ) )
54 35 53 sylan 
 |-  ( ( ( F e. A /\ M e. QQ ) /\ n e. NN0 ) -> ( ( F ` M ) ^ ( n + 1 ) ) = ( ( ( F ` M ) ^ n ) x. ( F ` M ) ) )
55 52 54 eqeq12d 
 |-  ( ( ( F e. A /\ M e. QQ ) /\ n e. NN0 ) -> ( ( F ` ( M ^ ( n + 1 ) ) ) = ( ( F ` M ) ^ ( n + 1 ) ) <-> ( ( F ` ( M ^ n ) ) x. ( F ` M ) ) = ( ( ( F ` M ) ^ n ) x. ( F ` M ) ) ) )
56 38 55 syl5ibr 
 |-  ( ( ( F e. A /\ M e. QQ ) /\ n e. NN0 ) -> ( ( F ` ( M ^ n ) ) = ( ( F ` M ) ^ n ) -> ( F ` ( M ^ ( n + 1 ) ) ) = ( ( F ` M ) ^ ( n + 1 ) ) ) )
57 56 expcom 
 |-  ( n e. NN0 -> ( ( F e. A /\ M e. QQ ) -> ( ( F ` ( M ^ n ) ) = ( ( F ` M ) ^ n ) -> ( F ` ( M ^ ( n + 1 ) ) ) = ( ( F ` M ) ^ ( n + 1 ) ) ) ) )
58 57 a2d 
 |-  ( n e. NN0 -> ( ( ( F e. A /\ M e. QQ ) -> ( F ` ( M ^ n ) ) = ( ( F ` M ) ^ n ) ) -> ( ( F e. A /\ M e. QQ ) -> ( F ` ( M ^ ( n + 1 ) ) ) = ( ( F ` M ) ^ ( n + 1 ) ) ) ) )
59 7 12 17 22 37 58 nn0ind 
 |-  ( N e. NN0 -> ( ( F e. A /\ M e. QQ ) -> ( F ` ( M ^ N ) ) = ( ( F ` M ) ^ N ) ) )
60 59 com12 
 |-  ( ( F e. A /\ M e. QQ ) -> ( N e. NN0 -> ( F ` ( M ^ N ) ) = ( ( F ` M ) ^ N ) ) )
61 60 3impia 
 |-  ( ( F e. A /\ M e. QQ /\ N e. NN0 ) -> ( F ` ( M ^ N ) ) = ( ( F ` M ) ^ N ) )