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 ⊢ 𝑄 = ( ℂfld ↾s ℚ )
qabsabv.a ⊢ 𝐴 = ( AbsVal ‘ 𝑄 )
Assertion qabvexp ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑀 ↑ 𝑁 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 qrng.q ⊢ 𝑄 = ( ℂfld ↾s ℚ )
2 qabsabv.a ⊢ 𝐴 = ( AbsVal ‘ 𝑄 )
3 oveq2 ⊢ ( 𝑘 = 0 → ( 𝑀 ↑ 𝑘 ) = ( 𝑀 ↑ 0 ) )
4 3 fveq2d ⊢ ( 𝑘 = 0 → ( 𝐹 ‘ ( 𝑀 ↑ 𝑘 ) ) = ( 𝐹 ‘ ( 𝑀 ↑ 0 ) ) )
5 oveq2 ⊢ ( 𝑘 = 0 → ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑘 ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 0 ) )
6 4 5 eqeq12d ⊢ ( 𝑘 = 0 → ( ( 𝐹 ‘ ( 𝑀 ↑ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑘 ) ↔ ( 𝐹 ‘ ( 𝑀 ↑ 0 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 0 ) ) )
7 6 imbi2d ⊢ ( 𝑘 = 0 → ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( 𝐹 ‘ ( 𝑀 ↑ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑘 ) ) ↔ ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( 𝐹 ‘ ( 𝑀 ↑ 0 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 0 ) ) ) )
8 oveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝑀 ↑ 𝑘 ) = ( 𝑀 ↑ 𝑛 ) )
9 8 fveq2d ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ ( 𝑀 ↑ 𝑘 ) ) = ( 𝐹 ‘ ( 𝑀 ↑ 𝑛 ) ) )
10 oveq2 ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑘 ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) )
11 9 10 eqeq12d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ ( 𝑀 ↑ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑘 ) ↔ ( 𝐹 ‘ ( 𝑀 ↑ 𝑛 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) ) )
12 11 imbi2d ⊢ ( 𝑘 = 𝑛 → ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( 𝐹 ‘ ( 𝑀 ↑ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑘 ) ) ↔ ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( 𝐹 ‘ ( 𝑀 ↑ 𝑛 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) ) ) )
13 oveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝑀 ↑ 𝑘 ) = ( 𝑀 ↑ ( 𝑛 + 1 ) ) )
14 13 fveq2d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐹 ‘ ( 𝑀 ↑ 𝑘 ) ) = ( 𝐹 ‘ ( 𝑀 ↑ ( 𝑛 + 1 ) ) ) )
15 oveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑘 ) = ( ( 𝐹 ‘ 𝑀 ) ↑ ( 𝑛 + 1 ) ) )
16 14 15 eqeq12d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ ( 𝑀 ↑ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑘 ) ↔ ( 𝐹 ‘ ( 𝑀 ↑ ( 𝑛 + 1 ) ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ ( 𝑛 + 1 ) ) ) )
17 16 imbi2d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( 𝐹 ‘ ( 𝑀 ↑ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑘 ) ) ↔ ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( 𝐹 ‘ ( 𝑀 ↑ ( 𝑛 + 1 ) ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ ( 𝑛 + 1 ) ) ) ) )
18 oveq2 ⊢ ( 𝑘 = 𝑁 → ( 𝑀 ↑ 𝑘 ) = ( 𝑀 ↑ 𝑁 ) )
19 18 fveq2d ⊢ ( 𝑘 = 𝑁 → ( 𝐹 ‘ ( 𝑀 ↑ 𝑘 ) ) = ( 𝐹 ‘ ( 𝑀 ↑ 𝑁 ) ) )
20 oveq2 ⊢ ( 𝑘 = 𝑁 → ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑘 ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑁 ) )
21 19 20 eqeq12d ⊢ ( 𝑘 = 𝑁 → ( ( 𝐹 ‘ ( 𝑀 ↑ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑘 ) ↔ ( 𝐹 ‘ ( 𝑀 ↑ 𝑁 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑁 ) ) )
22 21 imbi2d ⊢ ( 𝑘 = 𝑁 → ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( 𝐹 ‘ ( 𝑀 ↑ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑘 ) ) ↔ ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( 𝐹 ‘ ( 𝑀 ↑ 𝑁 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑁 ) ) ) )
23 ax-1ne0 ⊢ 1 ≠ 0
24 1 qrng1 ⊢ 1 = ( 1r ‘ 𝑄 )
25 1 qrng0 ⊢ 0 = ( 0g ‘ 𝑄 )
26 2 24 25 abv1z ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → ( 𝐹 ‘ 1 ) = 1 )
27 23 26 mpan2 ⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ 1 ) = 1 )
28 27 adantr ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( 𝐹 ‘ 1 ) = 1 )
29 qcn ⊢ ( 𝑀 ∈ ℚ → 𝑀 ∈ ℂ )
30 29 adantl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → 𝑀 ∈ ℂ )
31 30 exp0d ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( 𝑀 ↑ 0 ) = 1 )
32 31 fveq2d ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( 𝐹 ‘ ( 𝑀 ↑ 0 ) ) = ( 𝐹 ‘ 1 ) )
33 1 qrngbas ⊢ ℚ = ( Base ‘ 𝑄 )
34 2 33 abvcl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( 𝐹 ‘ 𝑀 ) ∈ ℝ )
35 34 recnd ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( 𝐹 ‘ 𝑀 ) ∈ ℂ )
36 35 exp0d ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( ( 𝐹 ‘ 𝑀 ) ↑ 0 ) = 1 )
37 28 32 36 3eqtr4d ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( 𝐹 ‘ ( 𝑀 ↑ 0 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 0 ) )
38 oveq1 ⊢ ( ( 𝐹 ‘ ( 𝑀 ↑ 𝑛 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) → ( ( 𝐹 ‘ ( 𝑀 ↑ 𝑛 ) ) · ( 𝐹 ‘ 𝑀 ) ) = ( ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) · ( 𝐹 ‘ 𝑀 ) ) )
39 expp1 ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑀 ↑ ( 𝑛 + 1 ) ) = ( ( 𝑀 ↑ 𝑛 ) · 𝑀 ) )
40 30 39 sylan ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑀 ↑ ( 𝑛 + 1 ) ) = ( ( 𝑀 ↑ 𝑛 ) · 𝑀 ) )
41 40 fveq2d ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑀 ↑ ( 𝑛 + 1 ) ) ) = ( 𝐹 ‘ ( ( 𝑀 ↑ 𝑛 ) · 𝑀 ) ) )
42 simpll ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) ∧ 𝑛 ∈ ℕ0 ) → 𝐹 ∈ 𝐴 )
43 qexpcl ⊢ ( ( 𝑀 ∈ ℚ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑀 ↑ 𝑛 ) ∈ ℚ )
44 43 adantll ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑀 ↑ 𝑛 ) ∈ ℚ )
45 simplr ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) ∧ 𝑛 ∈ ℕ0 ) → 𝑀 ∈ ℚ )
46 qex ⊢ ℚ ∈ V
47 cnfldmul ⊢ · = ( .r ‘ ℂfld )
48 1 47 ressmulr ⊢ ( ℚ ∈ V → · = ( .r ‘ 𝑄 ) )
49 46 48 ax-mp ⊢ · = ( .r ‘ 𝑄 )
50 2 33 49 abvmul ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑀 ↑ 𝑛 ) ∈ ℚ ∧ 𝑀 ∈ ℚ ) → ( 𝐹 ‘ ( ( 𝑀 ↑ 𝑛 ) · 𝑀 ) ) = ( ( 𝐹 ‘ ( 𝑀 ↑ 𝑛 ) ) · ( 𝐹 ‘ 𝑀 ) ) )
51 42 44 45 50 syl3anc ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐹 ‘ ( ( 𝑀 ↑ 𝑛 ) · 𝑀 ) ) = ( ( 𝐹 ‘ ( 𝑀 ↑ 𝑛 ) ) · ( 𝐹 ‘ 𝑀 ) ) )
52 41 51 eqtrd ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑀 ↑ ( 𝑛 + 1 ) ) ) = ( ( 𝐹 ‘ ( 𝑀 ↑ 𝑛 ) ) · ( 𝐹 ‘ 𝑀 ) ) )
53 expp1 ⊢ ( ( ( 𝐹 ‘ 𝑀 ) ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑀 ) ↑ ( 𝑛 + 1 ) ) = ( ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) · ( 𝐹 ‘ 𝑀 ) ) )
54 35 53 sylan ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑀 ) ↑ ( 𝑛 + 1 ) ) = ( ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) · ( 𝐹 ‘ 𝑀 ) ) )
55 52 54 eqeq12d ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐹 ‘ ( 𝑀 ↑ ( 𝑛 + 1 ) ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ ( 𝑛 + 1 ) ) ↔ ( ( 𝐹 ‘ ( 𝑀 ↑ 𝑛 ) ) · ( 𝐹 ‘ 𝑀 ) ) = ( ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) · ( 𝐹 ‘ 𝑀 ) ) ) )
56 38 55 syl5ibr ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐹 ‘ ( 𝑀 ↑ 𝑛 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) → ( 𝐹 ‘ ( 𝑀 ↑ ( 𝑛 + 1 ) ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ ( 𝑛 + 1 ) ) ) )
57 56 expcom ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( ( 𝐹 ‘ ( 𝑀 ↑ 𝑛 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) → ( 𝐹 ‘ ( 𝑀 ↑ ( 𝑛 + 1 ) ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ ( 𝑛 + 1 ) ) ) ) )
58 57 a2d ⊢ ( 𝑛 ∈ ℕ0 → ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( 𝐹 ‘ ( 𝑀 ↑ 𝑛 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑛 ) ) → ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( 𝐹 ‘ ( 𝑀 ↑ ( 𝑛 + 1 ) ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ ( 𝑛 + 1 ) ) ) ) )
59 7 12 17 22 37 58 nn0ind ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( 𝐹 ‘ ( 𝑀 ↑ 𝑁 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑁 ) ) )
60 59 com12 ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( 𝑁 ∈ ℕ0 → ( 𝐹 ‘ ( 𝑀 ↑ 𝑁 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑁 ) ) )
61 60 3impia ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑀 ↑ 𝑁 ) ) = ( ( 𝐹 ‘ 𝑀 ) ↑ 𝑁 ) )