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 = ℂ_{fld} ↾_{𝑠} ℚ$
	qabsabv.a	$⊢ A = AbsVal (Q)$
Assertion	qabvexp	$⊢ (F \in A \land M \in ℚ \land N \in ℕ_{0}) \to F (M^{N}) = {F (M)}^{N}$

Proof

Step	Hyp	Ref	Expression
1		qrng.q	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
2		qabsabv.a	$⊢ A = AbsVal (Q)$
3		oveq2	$⊢ k = 0 \to M^{k} = M^{0}$
4	3	fveq2d	$⊢ k = 0 \to F (M^{k}) = F (M^{0})$
5		oveq2	$⊢ k = 0 \to {F (M)}^{k} = {F (M)}^{0}$
6	4 5	eqeq12d	$⊢ k = 0 \to (F (M^{k}) = {F (M)}^{k} \leftrightarrow F (M^{0}) = {F (M)}^{0})$
7	6	imbi2d	$⊢ k = 0 \to (((F \in A \land M \in ℚ) \to F (M^{k}) = {F (M)}^{k}) \leftrightarrow ((F \in A \land M \in ℚ) \to F (M^{0}) = {F (M)}^{0}))$
8		oveq2	$⊢ k = n \to M^{k} = M^{n}$
9	8	fveq2d	$⊢ k = n \to F (M^{k}) = F (M^{n})$
10		oveq2	$⊢ k = n \to {F (M)}^{k} = {F (M)}^{n}$
11	9 10	eqeq12d	$⊢ k = n \to (F (M^{k}) = {F (M)}^{k} \leftrightarrow F (M^{n}) = {F (M)}^{n})$
12	11	imbi2d	$⊢ k = n \to (((F \in A \land M \in ℚ) \to F (M^{k}) = {F (M)}^{k}) \leftrightarrow ((F \in A \land M \in ℚ) \to F (M^{n}) = {F (M)}^{n}))$
13		oveq2	$⊢ k = n + 1 \to M^{k} = M^{n + 1}$
14	13	fveq2d	$⊢ k = n + 1 \to F (M^{k}) = F (M^{n + 1})$
15		oveq2	$⊢ k = n + 1 \to {F (M)}^{k} = {F (M)}^{n + 1}$
16	14 15	eqeq12d	$⊢ k = n + 1 \to (F (M^{k}) = {F (M)}^{k} \leftrightarrow F (M^{n + 1}) = {F (M)}^{n + 1})$
17	16	imbi2d	$⊢ k = n + 1 \to (((F \in A \land M \in ℚ) \to F (M^{k}) = {F (M)}^{k}) \leftrightarrow ((F \in A \land M \in ℚ) \to F (M^{n + 1}) = {F (M)}^{n + 1}))$
18		oveq2	$⊢ k = N \to M^{k} = M^{N}$
19	18	fveq2d	$⊢ k = N \to F (M^{k}) = F (M^{N})$
20		oveq2	$⊢ k = N \to {F (M)}^{k} = {F (M)}^{N}$
21	19 20	eqeq12d	$⊢ k = N \to (F (M^{k}) = {F (M)}^{k} \leftrightarrow F (M^{N}) = {F (M)}^{N})$
22	21	imbi2d	$⊢ k = N \to (((F \in A \land M \in ℚ) \to F (M^{k}) = {F (M)}^{k}) \leftrightarrow ((F \in A \land M \in ℚ) \to F (M^{N}) = {F (M)}^{N}))$
23		ax-1ne0	$⊢ 1 \neq 0$
24	1	qrng1	$⊢ 1 = 1_{Q}$
25	1	qrng0	$⊢ 0 = 0_{Q}$
26	2 24 25	abv1z	$⊢ (F \in A \land 1 \neq 0) \to F (1) = 1$
27	23 26	mpan2	$⊢ F \in A \to F (1) = 1$
28	27	adantr	$⊢ (F \in A \land M \in ℚ) \to F (1) = 1$
29		qcn	$⊢ M \in ℚ \to M \in ℂ$
30	29	adantl	$⊢ (F \in A \land M \in ℚ) \to M \in ℂ$
31	30	exp0d	$⊢ (F \in A \land M \in ℚ) \to M^{0} = 1$
32	31	fveq2d	$⊢ (F \in A \land M \in ℚ) \to F (M^{0}) = F (1)$
33	1	qrngbas	$⊢ ℚ = {Base}_{Q}$
34	2 33	abvcl	$⊢ (F \in A \land M \in ℚ) \to F (M) \in ℝ$
35	34	recnd	$⊢ (F \in A \land M \in ℚ) \to F (M) \in ℂ$
36	35	exp0d	$⊢ (F \in A \land M \in ℚ) \to {F (M)}^{0} = 1$
37	28 32 36	3eqtr4d	$⊢ (F \in A \land M \in ℚ) \to F (M^{0}) = {F (M)}^{0}$
38		oveq1	$⊢ F (M^{n}) = {F (M)}^{n} \to F (M^{n}) F (M) = {F (M)}^{n} F (M)$
39		expp1	$⊢ (M \in ℂ \land n \in ℕ_{0}) \to M^{n + 1} = M^{n} \cdot M$
40	30 39	sylan	$⊢ ((F \in A \land M \in ℚ) \land n \in ℕ_{0}) \to M^{n + 1} = M^{n} \cdot M$
41	40	fveq2d	$⊢ ((F \in A \land M \in ℚ) \land n \in ℕ_{0}) \to F (M^{n + 1}) = F (M^{n} \cdot M)$
42		simpll	$⊢ ((F \in A \land M \in ℚ) \land n \in ℕ_{0}) \to F \in A$
43		qexpcl	$⊢ (M \in ℚ \land n \in ℕ_{0}) \to M^{n} \in ℚ$
44	43	adantll	$⊢ ((F \in A \land M \in ℚ) \land n \in ℕ_{0}) \to M^{n} \in ℚ$
45		simplr	$⊢ ((F \in A \land M \in ℚ) \land n \in ℕ_{0}) \to M \in ℚ$
46		qex	$⊢ ℚ \in V$
47		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
48	1 47	ressmulr	$⊢ ℚ \in V \to \times = \cdot_{Q}$
49	46 48	ax-mp	$⊢ \times = \cdot_{Q}$
50	2 33 49	abvmul	$⊢ (F \in A \land M^{n} \in ℚ \land M \in ℚ) \to F (M^{n} \cdot M) = F (M^{n}) F (M)$
51	42 44 45 50	syl3anc	$⊢ ((F \in A \land M \in ℚ) \land n \in ℕ_{0}) \to F (M^{n} \cdot M) = F (M^{n}) F (M)$
52	41 51	eqtrd	$⊢ ((F \in A \land M \in ℚ) \land n \in ℕ_{0}) \to F (M^{n + 1}) = F (M^{n}) F (M)$
53		expp1	$⊢ (F (M) \in ℂ \land n \in ℕ_{0}) \to {F (M)}^{n + 1} = {F (M)}^{n} F (M)$
54	35 53	sylan	$⊢ ((F \in A \land M \in ℚ) \land n \in ℕ_{0}) \to {F (M)}^{n + 1} = {F (M)}^{n} F (M)$
55	52 54	eqeq12d	$⊢ ((F \in A \land M \in ℚ) \land n \in ℕ_{0}) \to (F (M^{n + 1}) = {F (M)}^{n + 1} \leftrightarrow F (M^{n}) F (M) = {F (M)}^{n} F (M))$
56	38 55	imbitrrid	$⊢ ((F \in A \land M \in ℚ) \land n \in ℕ_{0}) \to (F (M^{n}) = {F (M)}^{n} \to F (M^{n + 1}) = {F (M)}^{n + 1})$
57	56	expcom	$⊢ n \in ℕ_{0} \to ((F \in A \land M \in ℚ) \to (F (M^{n}) = {F (M)}^{n} \to F (M^{n + 1}) = {F (M)}^{n + 1}))$
58	57	a2d	$⊢ n \in ℕ_{0} \to (((F \in A \land M \in ℚ) \to F (M^{n}) = {F (M)}^{n}) \to ((F \in A \land M \in ℚ) \to F (M^{n + 1}) = {F (M)}^{n + 1}))$
59	7 12 17 22 37 58	nn0ind	$⊢ N \in ℕ_{0} \to ((F \in A \land M \in ℚ) \to F (M^{N}) = {F (M)}^{N})$
60	59	com12	$⊢ (F \in A \land M \in ℚ) \to (N \in ℕ_{0} \to F (M^{N}) = {F (M)}^{N})$
61	60	3impia	$⊢ (F \in A \land M \in ℚ \land N \in ℕ_{0}) \to F (M^{N}) = {F (M)}^{N}$

Metamath Proof Explorer

Theorem qabvexp

Proof