fprodabs

Description: The absolute value of a finite product. (Contributed by Scott Fenton, 25-Dec-2017)

	Ref	Expression
Hypotheses	fprodabs.1	$⊢ Z = ℤ_{\geq M}$
	fprodabs.2	$⊢ φ \to N \in Z$
	fprodabs.3	$⊢ (φ \land k \in Z) \to A \in ℂ$
Assertion	fprodabs	$⊢ φ \to \|\prod_{k = M}^{N} A\| = \prod_{k = M}^{N} \|A\|$

Proof

Step	Hyp	Ref	Expression
1		fprodabs.1	$⊢ Z = ℤ_{\geq M}$
2		fprodabs.2	$⊢ φ \to N \in Z$
3		fprodabs.3	$⊢ (φ \land k \in Z) \to A \in ℂ$
4	2 1	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq M}$
5		oveq2	$⊢ a = M \to (M \dots a) = (M \dots M)$
6	5	prodeq1d	$⊢ a = M \to \prod_{k = M}^{a} A = \prod_{k = M}^{M} A$
7	6	fveq2d	$⊢ a = M \to \|\prod_{k = M}^{a} A\| = \|\prod_{k = M}^{M} A\|$
8	5	prodeq1d	$⊢ a = M \to \prod_{k = M}^{a} \|A\| = \prod_{k = M}^{M} \|A\|$
9	7 8	eqeq12d	$⊢ a = M \to (\|\prod_{k = M}^{a} A\| = \prod_{k = M}^{a} \|A\| \leftrightarrow \|\prod_{k = M}^{M} A\| = \prod_{k = M}^{M} \|A\|)$
10	9	imbi2d	$⊢ a = M \to ((φ \to \|\prod_{k = M}^{a} A\| = \prod_{k = M}^{a} \|A\|) \leftrightarrow (φ \to \|\prod_{k = M}^{M} A\| = \prod_{k = M}^{M} \|A\|))$
11		oveq2	$⊢ a = n \to (M \dots a) = (M \dots n)$
12	11	prodeq1d	$⊢ a = n \to \prod_{k = M}^{a} A = \prod_{k = M}^{n} A$
13	12	fveq2d	$⊢ a = n \to \|\prod_{k = M}^{a} A\| = \|\prod_{k = M}^{n} A\|$
14	11	prodeq1d	$⊢ a = n \to \prod_{k = M}^{a} \|A\| = \prod_{k = M}^{n} \|A\|$
15	13 14	eqeq12d	$⊢ a = n \to (\|\prod_{k = M}^{a} A\| = \prod_{k = M}^{a} \|A\| \leftrightarrow \|\prod_{k = M}^{n} A\| = \prod_{k = M}^{n} \|A\|)$
16	15	imbi2d	$⊢ a = n \to ((φ \to \|\prod_{k = M}^{a} A\| = \prod_{k = M}^{a} \|A\|) \leftrightarrow (φ \to \|\prod_{k = M}^{n} A\| = \prod_{k = M}^{n} \|A\|))$
17		oveq2	$⊢ a = n + 1 \to (M \dots a) = (M \dots n + 1)$
18	17	prodeq1d	$⊢ a = n + 1 \to \prod_{k = M}^{a} A = \prod_{k = M}^{n + 1} A$
19	18	fveq2d	$⊢ a = n + 1 \to \|\prod_{k = M}^{a} A\| = \|\prod_{k = M}^{n + 1} A\|$
20	17	prodeq1d	$⊢ a = n + 1 \to \prod_{k = M}^{a} \|A\| = \prod_{k = M}^{n + 1} \|A\|$
21	19 20	eqeq12d	$⊢ a = n + 1 \to (\|\prod_{k = M}^{a} A\| = \prod_{k = M}^{a} \|A\| \leftrightarrow \|\prod_{k = M}^{n + 1} A\| = \prod_{k = M}^{n + 1} \|A\|)$
22	21	imbi2d	$⊢ a = n + 1 \to ((φ \to \|\prod_{k = M}^{a} A\| = \prod_{k = M}^{a} \|A\|) \leftrightarrow (φ \to \|\prod_{k = M}^{n + 1} A\| = \prod_{k = M}^{n + 1} \|A\|))$
23		oveq2	$⊢ a = N \to (M \dots a) = (M \dots N)$
24	23	prodeq1d	$⊢ a = N \to \prod_{k = M}^{a} A = \prod_{k = M}^{N} A$
25	24	fveq2d	$⊢ a = N \to \|\prod_{k = M}^{a} A\| = \|\prod_{k = M}^{N} A\|$
26	23	prodeq1d	$⊢ a = N \to \prod_{k = M}^{a} \|A\| = \prod_{k = M}^{N} \|A\|$
27	25 26	eqeq12d	$⊢ a = N \to (\|\prod_{k = M}^{a} A\| = \prod_{k = M}^{a} \|A\| \leftrightarrow \|\prod_{k = M}^{N} A\| = \prod_{k = M}^{N} \|A\|)$
28	27	imbi2d	$⊢ a = N \to ((φ \to \|\prod_{k = M}^{a} A\| = \prod_{k = M}^{a} \|A\|) \leftrightarrow (φ \to \|\prod_{k = M}^{N} A\| = \prod_{k = M}^{N} \|A\|))$
29		csbfv2g	$⊢ M \in ℤ \to ⦋ M / k ⦌ \|A\| = \|⦋ M / k ⦌ A\|$
30	29	adantl	$⊢ (φ \land M \in ℤ) \to ⦋ M / k ⦌ \|A\| = \|⦋ M / k ⦌ A\|$
31		fzsn	$⊢ M \in ℤ \to (M \dots M) = \{M\}$
32	31	adantl	$⊢ (φ \land M \in ℤ) \to (M \dots M) = \{M\}$
33	32	prodeq1d	$⊢ (φ \land M \in ℤ) \to \prod_{k = M}^{M} \|A\| = \prod_{k \in \{M\}} \|A\|$
34		simpr	$⊢ (φ \land M \in ℤ) \to M \in ℤ$
35		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
36	35 1	eleqtrrdi	$⊢ M \in ℤ \to M \in Z$
37	3	ralrimiva	$⊢ φ \to \forall k \in Z A \in ℂ$
38		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ M / k ⦌ A$
39	38	nfel1	$⊢ Ⅎ k ⦋ M / k ⦌ A \in ℂ$
40		csbeq1a	$⊢ k = M \to A = ⦋ M / k ⦌ A$
41	40	eleq1d	$⊢ k = M \to (A \in ℂ \leftrightarrow ⦋ M / k ⦌ A \in ℂ)$
42	39 41	rspc	$⊢ M \in Z \to (\forall k \in Z A \in ℂ \to ⦋ M / k ⦌ A \in ℂ)$
43	37 42	mpan9	$⊢ (φ \land M \in Z) \to ⦋ M / k ⦌ A \in ℂ$
44	36 43	sylan2	$⊢ (φ \land M \in ℤ) \to ⦋ M / k ⦌ A \in ℂ$
45	44	abscld	$⊢ (φ \land M \in ℤ) \to \|⦋ M / k ⦌ A\| \in ℝ$
46	45	recnd	$⊢ (φ \land M \in ℤ) \to \|⦋ M / k ⦌ A\| \in ℂ$
47	30 46	eqeltrd	$⊢ (φ \land M \in ℤ) \to ⦋ M / k ⦌ \|A\| \in ℂ$
48		prodsns	$⊢ (M \in ℤ \land ⦋ M / k ⦌ \|A\| \in ℂ) \to \prod_{k \in \{M\}} \|A\| = ⦋ M / k ⦌ \|A\|$
49	34 47 48	syl2anc	$⊢ (φ \land M \in ℤ) \to \prod_{k \in \{M\}} \|A\| = ⦋ M / k ⦌ \|A\|$
50	33 49	eqtrd	$⊢ (φ \land M \in ℤ) \to \prod_{k = M}^{M} \|A\| = ⦋ M / k ⦌ \|A\|$
51	31	prodeq1d	$⊢ M \in ℤ \to \prod_{k = M}^{M} A = \prod_{k \in \{M\}} A$
52	51	adantl	$⊢ (φ \land M \in ℤ) \to \prod_{k = M}^{M} A = \prod_{k \in \{M\}} A$
53		prodsns	$⊢ (M \in ℤ \land ⦋ M / k ⦌ A \in ℂ) \to \prod_{k \in \{M\}} A = ⦋ M / k ⦌ A$
54	34 44 53	syl2anc	$⊢ (φ \land M \in ℤ) \to \prod_{k \in \{M\}} A = ⦋ M / k ⦌ A$
55	52 54	eqtrd	$⊢ (φ \land M \in ℤ) \to \prod_{k = M}^{M} A = ⦋ M / k ⦌ A$
56	55	fveq2d	$⊢ (φ \land M \in ℤ) \to \|\prod_{k = M}^{M} A\| = \|⦋ M / k ⦌ A\|$
57	30 50 56	3eqtr4rd	$⊢ (φ \land M \in ℤ) \to \|\prod_{k = M}^{M} A\| = \prod_{k = M}^{M} \|A\|$
58	57	expcom	$⊢ M \in ℤ \to (φ \to \|\prod_{k = M}^{M} A\| = \prod_{k = M}^{M} \|A\|)$
59		simp3	$⊢ (φ \land n \in ℤ_{\geq M} \land \|\prod_{k = M}^{n} A\| = \prod_{k = M}^{n} \|A\|) \to \|\prod_{k = M}^{n} A\| = \prod_{k = M}^{n} \|A\|$
60		ovex	$⊢ n + 1 \in V$
61		csbfv2g	$⊢ n + 1 \in V \to ⦋ (n + 1) / k ⦌ \|A\| = \|⦋ (n + 1) / k ⦌ A\|$
62	60 61	ax-mp	$⊢ ⦋ (n + 1) / k ⦌ \|A\| = \|⦋ (n + 1) / k ⦌ A\|$
63	62	eqcomi	$⊢ \|⦋ (n + 1) / k ⦌ A\| = ⦋ (n + 1) / k ⦌ \|A\|$
64	63	a1i	$⊢ (φ \land n \in ℤ_{\geq M} \land \|\prod_{k = M}^{n} A\| = \prod_{k = M}^{n} \|A\|) \to \|⦋ (n + 1) / k ⦌ A\| = ⦋ (n + 1) / k ⦌ \|A\|$
65	59 64	oveq12d	$⊢ (φ \land n \in ℤ_{\geq M} \land \|\prod_{k = M}^{n} A\| = \prod_{k = M}^{n} \|A\|) \to \|\prod_{k = M}^{n} A\| \|⦋ (n + 1) / k ⦌ A\| = \prod_{k = M}^{n} \|A\| ⦋ (n + 1) / k ⦌ \|A\|$
66		simpr	$⊢ (φ \land n \in ℤ_{\geq M}) \to n \in ℤ_{\geq M}$
67		elfzuz	$⊢ k \in (M \dots n + 1) \to k \in ℤ_{\geq M}$
68	67 1	eleqtrrdi	$⊢ k \in (M \dots n + 1) \to k \in Z$
69	68 3	sylan2	$⊢ (φ \land k \in (M \dots n + 1)) \to A \in ℂ$
70	69	adantlr	$⊢ ((φ \land n \in ℤ_{\geq M}) \land k \in (M \dots n + 1)) \to A \in ℂ$
71	66 70	fprodp1s	$⊢ (φ \land n \in ℤ_{\geq M}) \to \prod_{k = M}^{n + 1} A = \prod_{k = M}^{n} A ⦋ (n + 1) / k ⦌ A$
72	71	fveq2d	$⊢ (φ \land n \in ℤ_{\geq M}) \to \|\prod_{k = M}^{n + 1} A\| = \|\prod_{k = M}^{n} A ⦋ (n + 1) / k ⦌ A\|$
73		fzfid	$⊢ (φ \land n \in ℤ_{\geq M}) \to (M \dots n) \in Fin$
74		elfzuz	$⊢ k \in (M \dots n) \to k \in ℤ_{\geq M}$
75	74 1	eleqtrrdi	$⊢ k \in (M \dots n) \to k \in Z$
76	75 3	sylan2	$⊢ (φ \land k \in (M \dots n)) \to A \in ℂ$
77	76	adantlr	$⊢ ((φ \land n \in ℤ_{\geq M}) \land k \in (M \dots n)) \to A \in ℂ$
78	73 77	fprodcl	$⊢ (φ \land n \in ℤ_{\geq M}) \to \prod_{k = M}^{n} A \in ℂ$
79		peano2uz	$⊢ n \in ℤ_{\geq M} \to n + 1 \in ℤ_{\geq M}$
80	79 1	eleqtrrdi	$⊢ n \in ℤ_{\geq M} \to n + 1 \in Z$
81		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ (n + 1) / k ⦌ A$
82	81	nfel1	$⊢ Ⅎ k ⦋ (n + 1) / k ⦌ A \in ℂ$
83		csbeq1a	$⊢ k = n + 1 \to A = ⦋ (n + 1) / k ⦌ A$
84	83	eleq1d	$⊢ k = n + 1 \to (A \in ℂ \leftrightarrow ⦋ (n + 1) / k ⦌ A \in ℂ)$
85	82 84	rspc	$⊢ n + 1 \in Z \to (\forall k \in Z A \in ℂ \to ⦋ (n + 1) / k ⦌ A \in ℂ)$
86	37 85	mpan9	$⊢ (φ \land n + 1 \in Z) \to ⦋ (n + 1) / k ⦌ A \in ℂ$
87	80 86	sylan2	$⊢ (φ \land n \in ℤ_{\geq M}) \to ⦋ (n + 1) / k ⦌ A \in ℂ$
88	78 87	absmuld	$⊢ (φ \land n \in ℤ_{\geq M}) \to \|\prod_{k = M}^{n} A ⦋ (n + 1) / k ⦌ A\| = \|\prod_{k = M}^{n} A\| \|⦋ (n + 1) / k ⦌ A\|$
89	72 88	eqtrd	$⊢ (φ \land n \in ℤ_{\geq M}) \to \|\prod_{k = M}^{n + 1} A\| = \|\prod_{k = M}^{n} A\| \|⦋ (n + 1) / k ⦌ A\|$
90	89	3adant3	$⊢ (φ \land n \in ℤ_{\geq M} \land \|\prod_{k = M}^{n} A\| = \prod_{k = M}^{n} \|A\|) \to \|\prod_{k = M}^{n + 1} A\| = \|\prod_{k = M}^{n} A\| \|⦋ (n + 1) / k ⦌ A\|$
91	70	abscld	$⊢ ((φ \land n \in ℤ_{\geq M}) \land k \in (M \dots n + 1)) \to \|A\| \in ℝ$
92	91	recnd	$⊢ ((φ \land n \in ℤ_{\geq M}) \land k \in (M \dots n + 1)) \to \|A\| \in ℂ$
93	66 92	fprodp1s	$⊢ (φ \land n \in ℤ_{\geq M}) \to \prod_{k = M}^{n + 1} \|A\| = \prod_{k = M}^{n} \|A\| ⦋ (n + 1) / k ⦌ \|A\|$
94	93	3adant3	$⊢ (φ \land n \in ℤ_{\geq M} \land \|\prod_{k = M}^{n} A\| = \prod_{k = M}^{n} \|A\|) \to \prod_{k = M}^{n + 1} \|A\| = \prod_{k = M}^{n} \|A\| ⦋ (n + 1) / k ⦌ \|A\|$
95	65 90 94	3eqtr4d	$⊢ (φ \land n \in ℤ_{\geq M} \land \|\prod_{k = M}^{n} A\| = \prod_{k = M}^{n} \|A\|) \to \|\prod_{k = M}^{n + 1} A\| = \prod_{k = M}^{n + 1} \|A\|$
96	95	3exp	$⊢ φ \to (n \in ℤ_{\geq M} \to (\|\prod_{k = M}^{n} A\| = \prod_{k = M}^{n} \|A\| \to \|\prod_{k = M}^{n + 1} A\| = \prod_{k = M}^{n + 1} \|A\|))$
97	96	com12	$⊢ n \in ℤ_{\geq M} \to (φ \to (\|\prod_{k = M}^{n} A\| = \prod_{k = M}^{n} \|A\| \to \|\prod_{k = M}^{n + 1} A\| = \prod_{k = M}^{n + 1} \|A\|))$
98	97	a2d	$⊢ n \in ℤ_{\geq M} \to ((φ \to \|\prod_{k = M}^{n} A\| = \prod_{k = M}^{n} \|A\|) \to (φ \to \|\prod_{k = M}^{n + 1} A\| = \prod_{k = M}^{n + 1} \|A\|))$
99	10 16 22 28 58 98	uzind4	$⊢ N \in ℤ_{\geq M} \to (φ \to \|\prod_{k = M}^{N} A\| = \prod_{k = M}^{N} \|A\|)$
100	4 99	mpcom	$⊢ φ \to \|\prod_{k = M}^{N} A\| = \prod_{k = M}^{N} \|A\|$

Metamath Proof Explorer

Theorem fprodabs

Proof