prod1

Description: Any product of one over a valid set is one. (Contributed by Scott Fenton, 7-Dec-2017)

		Ref	Expression
	Assertion	prod1	$⊢ (A \subseteq ℤ_{\geq M} \lor A \in Fin) \to \prod_{k \in A} 1 = 1$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ℤ_{\geq M} = ℤ_{\geq M}$
2		simpr	$⊢ (A \subseteq ℤ_{\geq M} \land M \in ℤ) \to M \in ℤ$
3		ax-1ne0	$⊢ 1 \neq 0$
4	3	a1i	$⊢ (A \subseteq ℤ_{\geq M} \land M \in ℤ) \to 1 \neq 0$
5	1	prodfclim1	$⊢ M \in ℤ \to seq M (\times (ℤ_{\geq M} \times \{1\})) ⇝ 1$
6	5	adantl	$⊢ (A \subseteq ℤ_{\geq M} \land M \in ℤ) \to seq M (\times (ℤ_{\geq M} \times \{1\})) ⇝ 1$
7		simpl	$⊢ (A \subseteq ℤ_{\geq M} \land M \in ℤ) \to A \subseteq ℤ_{\geq M}$
8		1ex	$⊢ 1 \in V$
9	8	fvconst2	$⊢ k \in ℤ_{\geq M} \to (ℤ_{\geq M} \times \{1\}) (k) = 1$
10		ifid	$⊢ if (k \in A, 1, 1) = 1$
11	9 10	eqtr4di	$⊢ k \in ℤ_{\geq M} \to (ℤ_{\geq M} \times \{1\}) (k) = if (k \in A, 1, 1)$
12	11	adantl	$⊢ ((A \subseteq ℤ_{\geq M} \land M \in ℤ) \land k \in ℤ_{\geq M}) \to (ℤ_{\geq M} \times \{1\}) (k) = if (k \in A, 1, 1)$
13		1cnd	$⊢ ((A \subseteq ℤ_{\geq M} \land M \in ℤ) \land k \in A) \to 1 \in ℂ$
14	1 2 4 6 7 12 13	zprodn0	$⊢ (A \subseteq ℤ_{\geq M} \land M \in ℤ) \to \prod_{k \in A} 1 = 1$
15		uzf	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ$
16	15	fdmi	$⊢ dom ℤ_{\geq} = ℤ$
17	16	eleq2i	$⊢ M \in dom ℤ_{\geq} \leftrightarrow M \in ℤ$
18		ndmfv	$⊢ \neg M \in dom ℤ_{\geq} \to ℤ_{\geq M} = \emptyset$
19	17 18	sylnbir	$⊢ \neg M \in ℤ \to ℤ_{\geq M} = \emptyset$
20	19	sseq2d	$⊢ \neg M \in ℤ \to (A \subseteq ℤ_{\geq M} \leftrightarrow A \subseteq \emptyset)$
21	20	biimpac	$⊢ (A \subseteq ℤ_{\geq M} \land \neg M \in ℤ) \to A \subseteq \emptyset$
22		ss0	$⊢ A \subseteq \emptyset \to A = \emptyset$
23		prodeq1	$⊢ A = \emptyset \to \prod_{k \in A} 1 = \prod_{k \in \emptyset} 1$
24		prod0	$⊢ \prod_{k \in \emptyset} 1 = 1$
25	23 24	eqtrdi	$⊢ A = \emptyset \to \prod_{k \in A} 1 = 1$
26	21 22 25	3syl	$⊢ (A \subseteq ℤ_{\geq M} \land \neg M \in ℤ) \to \prod_{k \in A} 1 = 1$
27	14 26	pm2.61dan	$⊢ A \subseteq ℤ_{\geq M} \to \prod_{k \in A} 1 = 1$
28		fz1f1o	$⊢ A \in Fin \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
29		eqidd	$⊢ k = f (j) \to 1 = 1$
30		simpl	$⊢ (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to \|A\| \in ℕ$
31		simpr	$⊢ (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
32		1cnd	$⊢ ((\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land k \in A) \to 1 \in ℂ$
33		elfznn	$⊢ j \in (1 \dots \|A\|) \to j \in ℕ$
34	8	fvconst2	$⊢ j \in ℕ \to (ℕ \times \{1\}) (j) = 1$
35	33 34	syl	$⊢ j \in (1 \dots \|A\|) \to (ℕ \times \{1\}) (j) = 1$
36	35	adantl	$⊢ ((\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land j \in (1 \dots \|A\|)) \to (ℕ \times \{1\}) (j) = 1$
37	29 30 31 32 36	fprod	$⊢ (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to \prod_{k \in A} 1 = seq 1 (\times (ℕ \times \{1\})) (\|A\|)$
38		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
39	38	prodf1	$⊢ \|A\| \in ℕ \to seq 1 (\times (ℕ \times \{1\})) (\|A\|) = 1$
40	39	adantr	$⊢ (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to seq 1 (\times (ℕ \times \{1\})) (\|A\|) = 1$
41	37 40	eqtrd	$⊢ (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to \prod_{k \in A} 1 = 1$
42	41	ex	$⊢ \|A\| \in ℕ \to (f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \prod_{k \in A} 1 = 1)$
43	42	exlimdv	$⊢ \|A\| \in ℕ \to (\exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \prod_{k \in A} 1 = 1)$
44	43	imp	$⊢ (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to \prod_{k \in A} 1 = 1$
45	25 44	jaoi	$⊢ (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \prod_{k \in A} 1 = 1$
46	28 45	syl	$⊢ A \in Fin \to \prod_{k \in A} 1 = 1$
47	27 46	jaoi	$⊢ (A \subseteq ℤ_{\geq M} \lor A \in Fin) \to \prod_{k \in A} 1 = 1$

Metamath Proof Explorer

Theorem prod1

Proof