| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑘 = 0 → (𝑀↑𝑘) = (𝑀↑0)) | 
| 2 | 1 | fveq2d 6910 | . . . . . 6
⊢ (𝑘 = 0 → (𝐹‘(𝑀↑𝑘)) = (𝐹‘(𝑀↑0))) | 
| 3 |  | oveq2 7439 | . . . . . 6
⊢ (𝑘 = 0 → ((𝐹‘𝑀)↑𝑘) = ((𝐹‘𝑀)↑0)) | 
| 4 | 2, 3 | eqeq12d 2753 | . . . . 5
⊢ (𝑘 = 0 → ((𝐹‘(𝑀↑𝑘)) = ((𝐹‘𝑀)↑𝑘) ↔ (𝐹‘(𝑀↑0)) = ((𝐹‘𝑀)↑0))) | 
| 5 | 4 | imbi2d 340 | . . . 4
⊢ (𝑘 = 0 → (((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘(𝑀↑𝑘)) = ((𝐹‘𝑀)↑𝑘)) ↔ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘(𝑀↑0)) = ((𝐹‘𝑀)↑0)))) | 
| 6 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑘 = 𝑛 → (𝑀↑𝑘) = (𝑀↑𝑛)) | 
| 7 | 6 | fveq2d 6910 | . . . . . 6
⊢ (𝑘 = 𝑛 → (𝐹‘(𝑀↑𝑘)) = (𝐹‘(𝑀↑𝑛))) | 
| 8 |  | oveq2 7439 | . . . . . 6
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑀)↑𝑘) = ((𝐹‘𝑀)↑𝑛)) | 
| 9 | 7, 8 | eqeq12d 2753 | . . . . 5
⊢ (𝑘 = 𝑛 → ((𝐹‘(𝑀↑𝑘)) = ((𝐹‘𝑀)↑𝑘) ↔ (𝐹‘(𝑀↑𝑛)) = ((𝐹‘𝑀)↑𝑛))) | 
| 10 | 9 | imbi2d 340 | . . . 4
⊢ (𝑘 = 𝑛 → (((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘(𝑀↑𝑘)) = ((𝐹‘𝑀)↑𝑘)) ↔ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘(𝑀↑𝑛)) = ((𝐹‘𝑀)↑𝑛)))) | 
| 11 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑘 = (𝑛 + 1) → (𝑀↑𝑘) = (𝑀↑(𝑛 + 1))) | 
| 12 | 11 | fveq2d 6910 | . . . . . 6
⊢ (𝑘 = (𝑛 + 1) → (𝐹‘(𝑀↑𝑘)) = (𝐹‘(𝑀↑(𝑛 + 1)))) | 
| 13 |  | oveq2 7439 | . . . . . 6
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑀)↑𝑘) = ((𝐹‘𝑀)↑(𝑛 + 1))) | 
| 14 | 12, 13 | eqeq12d 2753 | . . . . 5
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘(𝑀↑𝑘)) = ((𝐹‘𝑀)↑𝑘) ↔ (𝐹‘(𝑀↑(𝑛 + 1))) = ((𝐹‘𝑀)↑(𝑛 + 1)))) | 
| 15 | 14 | imbi2d 340 | . . . 4
⊢ (𝑘 = (𝑛 + 1) → (((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘(𝑀↑𝑘)) = ((𝐹‘𝑀)↑𝑘)) ↔ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘(𝑀↑(𝑛 + 1))) = ((𝐹‘𝑀)↑(𝑛 + 1))))) | 
| 16 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑘 = 𝑁 → (𝑀↑𝑘) = (𝑀↑𝑁)) | 
| 17 | 16 | fveq2d 6910 | . . . . . 6
⊢ (𝑘 = 𝑁 → (𝐹‘(𝑀↑𝑘)) = (𝐹‘(𝑀↑𝑁))) | 
| 18 |  | oveq2 7439 | . . . . . 6
⊢ (𝑘 = 𝑁 → ((𝐹‘𝑀)↑𝑘) = ((𝐹‘𝑀)↑𝑁)) | 
| 19 | 17, 18 | eqeq12d 2753 | . . . . 5
⊢ (𝑘 = 𝑁 → ((𝐹‘(𝑀↑𝑘)) = ((𝐹‘𝑀)↑𝑘) ↔ (𝐹‘(𝑀↑𝑁)) = ((𝐹‘𝑀)↑𝑁))) | 
| 20 | 19 | imbi2d 340 | . . . 4
⊢ (𝑘 = 𝑁 → (((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘(𝑀↑𝑘)) = ((𝐹‘𝑀)↑𝑘)) ↔ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘(𝑀↑𝑁)) = ((𝐹‘𝑀)↑𝑁)))) | 
| 21 |  | ax-1ne0 11224 | . . . . . . 7
⊢ 1 ≠
0 | 
| 22 |  | qabsabv.a | . . . . . . . 8
⊢ 𝐴 = (AbsVal‘𝑄) | 
| 23 |  | qrng.q | . . . . . . . . 9
⊢ 𝑄 = (ℂfld
↾s ℚ) | 
| 24 | 23 | qrng1 27666 | . . . . . . . 8
⊢ 1 =
(1r‘𝑄) | 
| 25 | 23 | qrng0 27665 | . . . . . . . 8
⊢ 0 =
(0g‘𝑄) | 
| 26 | 22, 24, 25 | abv1z 20825 | . . . . . . 7
⊢ ((𝐹 ∈ 𝐴 ∧ 1 ≠ 0) → (𝐹‘1) = 1) | 
| 27 | 21, 26 | mpan2 691 | . . . . . 6
⊢ (𝐹 ∈ 𝐴 → (𝐹‘1) = 1) | 
| 28 | 27 | adantr 480 | . . . . 5
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘1) = 1) | 
| 29 |  | qcn 13005 | . . . . . . . 8
⊢ (𝑀 ∈ ℚ → 𝑀 ∈
ℂ) | 
| 30 | 29 | adantl 481 | . . . . . . 7
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → 𝑀 ∈ ℂ) | 
| 31 | 30 | exp0d 14180 | . . . . . 6
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝑀↑0) = 1) | 
| 32 | 31 | fveq2d 6910 | . . . . 5
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘(𝑀↑0)) = (𝐹‘1)) | 
| 33 | 23 | qrngbas 27663 | . . . . . . . 8
⊢ ℚ =
(Base‘𝑄) | 
| 34 | 22, 33 | abvcl 20817 | . . . . . . 7
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘𝑀) ∈ ℝ) | 
| 35 | 34 | recnd 11289 | . . . . . 6
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘𝑀) ∈ ℂ) | 
| 36 | 35 | exp0d 14180 | . . . . 5
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → ((𝐹‘𝑀)↑0) = 1) | 
| 37 | 28, 32, 36 | 3eqtr4d 2787 | . . . 4
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘(𝑀↑0)) = ((𝐹‘𝑀)↑0)) | 
| 38 |  | oveq1 7438 | . . . . . . 7
⊢ ((𝐹‘(𝑀↑𝑛)) = ((𝐹‘𝑀)↑𝑛) → ((𝐹‘(𝑀↑𝑛)) · (𝐹‘𝑀)) = (((𝐹‘𝑀)↑𝑛) · (𝐹‘𝑀))) | 
| 39 |  | expp1 14109 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℂ ∧ 𝑛 ∈ ℕ0)
→ (𝑀↑(𝑛 + 1)) = ((𝑀↑𝑛) · 𝑀)) | 
| 40 | 30, 39 | sylan 580 | . . . . . . . . . 10
⊢ (((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) ∧ 𝑛 ∈ ℕ0) → (𝑀↑(𝑛 + 1)) = ((𝑀↑𝑛) · 𝑀)) | 
| 41 | 40 | fveq2d 6910 | . . . . . . . . 9
⊢ (((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(𝑀↑(𝑛 + 1))) = (𝐹‘((𝑀↑𝑛) · 𝑀))) | 
| 42 |  | simpll 767 | . . . . . . . . . 10
⊢ (((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) ∧ 𝑛 ∈ ℕ0) → 𝐹 ∈ 𝐴) | 
| 43 |  | qexpcl 14118 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℚ ∧ 𝑛 ∈ ℕ0)
→ (𝑀↑𝑛) ∈
ℚ) | 
| 44 | 43 | adantll 714 | . . . . . . . . . 10
⊢ (((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) ∧ 𝑛 ∈ ℕ0) → (𝑀↑𝑛) ∈ ℚ) | 
| 45 |  | simplr 769 | . . . . . . . . . 10
⊢ (((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) ∧ 𝑛 ∈ ℕ0) → 𝑀 ∈
ℚ) | 
| 46 |  | qex 13003 | . . . . . . . . . . . 12
⊢ ℚ
∈ V | 
| 47 |  | cnfldmul 21372 | . . . . . . . . . . . . 13
⊢  ·
= (.r‘ℂfld) | 
| 48 | 23, 47 | ressmulr 17351 | . . . . . . . . . . . 12
⊢ (ℚ
∈ V → · = (.r‘𝑄)) | 
| 49 | 46, 48 | ax-mp 5 | . . . . . . . . . . 11
⊢  ·
= (.r‘𝑄) | 
| 50 | 22, 33, 49 | abvmul 20822 | . . . . . . . . . 10
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑀↑𝑛) ∈ ℚ ∧ 𝑀 ∈ ℚ) → (𝐹‘((𝑀↑𝑛) · 𝑀)) = ((𝐹‘(𝑀↑𝑛)) · (𝐹‘𝑀))) | 
| 51 | 42, 44, 45, 50 | syl3anc 1373 | . . . . . . . . 9
⊢ (((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑀↑𝑛) · 𝑀)) = ((𝐹‘(𝑀↑𝑛)) · (𝐹‘𝑀))) | 
| 52 | 41, 51 | eqtrd 2777 | . . . . . . . 8
⊢ (((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(𝑀↑(𝑛 + 1))) = ((𝐹‘(𝑀↑𝑛)) · (𝐹‘𝑀))) | 
| 53 |  | expp1 14109 | . . . . . . . . 9
⊢ (((𝐹‘𝑀) ∈ ℂ ∧ 𝑛 ∈ ℕ0) → ((𝐹‘𝑀)↑(𝑛 + 1)) = (((𝐹‘𝑀)↑𝑛) · (𝐹‘𝑀))) | 
| 54 | 35, 53 | sylan 580 | . . . . . . . 8
⊢ (((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) ∧ 𝑛 ∈ ℕ0) → ((𝐹‘𝑀)↑(𝑛 + 1)) = (((𝐹‘𝑀)↑𝑛) · (𝐹‘𝑀))) | 
| 55 | 52, 54 | eqeq12d 2753 | . . . . . . 7
⊢ (((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) ∧ 𝑛 ∈ ℕ0) → ((𝐹‘(𝑀↑(𝑛 + 1))) = ((𝐹‘𝑀)↑(𝑛 + 1)) ↔ ((𝐹‘(𝑀↑𝑛)) · (𝐹‘𝑀)) = (((𝐹‘𝑀)↑𝑛) · (𝐹‘𝑀)))) | 
| 56 | 38, 55 | imbitrrid 246 | . . . . . 6
⊢ (((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) ∧ 𝑛 ∈ ℕ0) → ((𝐹‘(𝑀↑𝑛)) = ((𝐹‘𝑀)↑𝑛) → (𝐹‘(𝑀↑(𝑛 + 1))) = ((𝐹‘𝑀)↑(𝑛 + 1)))) | 
| 57 | 56 | expcom 413 | . . . . 5
⊢ (𝑛 ∈ ℕ0
→ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → ((𝐹‘(𝑀↑𝑛)) = ((𝐹‘𝑀)↑𝑛) → (𝐹‘(𝑀↑(𝑛 + 1))) = ((𝐹‘𝑀)↑(𝑛 + 1))))) | 
| 58 | 57 | a2d 29 | . . . 4
⊢ (𝑛 ∈ ℕ0
→ (((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘(𝑀↑𝑛)) = ((𝐹‘𝑀)↑𝑛)) → ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘(𝑀↑(𝑛 + 1))) = ((𝐹‘𝑀)↑(𝑛 + 1))))) | 
| 59 | 5, 10, 15, 20, 37, 58 | nn0ind 12713 | . . 3
⊢ (𝑁 ∈ ℕ0
→ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘(𝑀↑𝑁)) = ((𝐹‘𝑀)↑𝑁))) | 
| 60 | 59 | com12 32 | . 2
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝑁 ∈ ℕ0 → (𝐹‘(𝑀↑𝑁)) = ((𝐹‘𝑀)↑𝑁))) | 
| 61 | 60 | 3impia 1118 | 1
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (𝐹‘(𝑀↑𝑁)) = ((𝐹‘𝑀)↑𝑁)) |