# Metamath Proof Explorer

## Theorem prod1

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

Ref Expression
Assertion prod1 $⊢ A ⊆ ℤ ≥ M ∨ A ∈ Fin → ∏ k ∈ A 1 = 1$

### Proof

Step Hyp Ref Expression
1 eqid $⊢ ℤ ≥ M = ℤ ≥ M$
2 simpr $⊢ A ⊆ ℤ ≥ M ∧ M ∈ ℤ → M ∈ ℤ$
3 ax-1ne0 $⊢ 1 ≠ 0$
4 3 a1i $⊢ A ⊆ ℤ ≥ M ∧ M ∈ ℤ → 1 ≠ 0$
5 1 prodfclim1 $⊢ M ∈ ℤ → seq M × ℤ ≥ M × 1 ⇝ 1$
6 5 adantl $⊢ A ⊆ ℤ ≥ M ∧ M ∈ ℤ → seq M × ℤ ≥ M × 1 ⇝ 1$
7 simpl $⊢ A ⊆ ℤ ≥ M ∧ M ∈ ℤ → A ⊆ ℤ ≥ M$
8 1ex $⊢ 1 ∈ V$
9 8 fvconst2 $⊢ k ∈ ℤ ≥ M → ℤ ≥ M × 1 ⁡ k = 1$
10 ifid $⊢ if k ∈ A 1 1 = 1$
11 9 10 eqtr4di $⊢ k ∈ ℤ ≥ M → ℤ ≥ M × 1 ⁡ k = if k ∈ A 1 1$
12 11 adantl $⊢ A ⊆ ℤ ≥ M ∧ M ∈ ℤ ∧ k ∈ ℤ ≥ M → ℤ ≥ M × 1 ⁡ k = if k ∈ A 1 1$
13 1cnd $⊢ A ⊆ ℤ ≥ M ∧ M ∈ ℤ ∧ k ∈ A → 1 ∈ ℂ$
14 1 2 4 6 7 12 13 zprodn0 $⊢ A ⊆ ℤ ≥ M ∧ M ∈ ℤ → ∏ k ∈ A 1 = 1$
15 uzf $⊢ ℤ ≥ : ℤ ⟶ 𝒫 ℤ$
16 15 fdmi $⊢ dom ⁡ ℤ ≥ = ℤ$
17 16 eleq2i $⊢ M ∈ dom ⁡ ℤ ≥ ↔ M ∈ ℤ$
18 ndmfv $⊢ ¬ M ∈ dom ⁡ ℤ ≥ → ℤ ≥ M = ∅$
19 17 18 sylnbir $⊢ ¬ M ∈ ℤ → ℤ ≥ M = ∅$
20 19 sseq2d $⊢ ¬ M ∈ ℤ → A ⊆ ℤ ≥ M ↔ A ⊆ ∅$
21 20 biimpac $⊢ A ⊆ ℤ ≥ M ∧ ¬ M ∈ ℤ → A ⊆ ∅$
22 ss0 $⊢ A ⊆ ∅ → A = ∅$
23 prodeq1 $⊢ A = ∅ → ∏ k ∈ A 1 = ∏ k ∈ ∅ 1$
24 prod0 $⊢ ∏ k ∈ ∅ 1 = 1$
25 23 24 eqtrdi $⊢ A = ∅ → ∏ k ∈ A 1 = 1$
26 21 22 25 3syl $⊢ A ⊆ ℤ ≥ M ∧ ¬ M ∈ ℤ → ∏ k ∈ A 1 = 1$
27 14 26 pm2.61dan $⊢ A ⊆ ℤ ≥ M → ∏ k ∈ A 1 = 1$
28 fz1f1o $⊢ A ∈ Fin → A = ∅ ∨ A ∈ ℕ ∧ ∃ f f : 1 … A ⟶ 1-1 onto A$
29 eqidd $⊢ k = f ⁡ j → 1 = 1$
30 simpl $⊢ A ∈ ℕ ∧ f : 1 … A ⟶ 1-1 onto A → A ∈ ℕ$
31 simpr $⊢ A ∈ ℕ ∧ f : 1 … A ⟶ 1-1 onto A → f : 1 … A ⟶ 1-1 onto A$
32 1cnd $⊢ A ∈ ℕ ∧ f : 1 … A ⟶ 1-1 onto A ∧ k ∈ A → 1 ∈ ℂ$
33 elfznn $⊢ j ∈ 1 … A → j ∈ ℕ$
34 8 fvconst2 $⊢ j ∈ ℕ → ℕ × 1 ⁡ j = 1$
35 33 34 syl $⊢ j ∈ 1 … A → ℕ × 1 ⁡ j = 1$
36 35 adantl $⊢ A ∈ ℕ ∧ f : 1 … A ⟶ 1-1 onto A ∧ j ∈ 1 … A → ℕ × 1 ⁡ j = 1$
37 29 30 31 32 36 fprod $⊢ A ∈ ℕ ∧ f : 1 … A ⟶ 1-1 onto A → ∏ k ∈ A 1 = seq 1 × ℕ × 1 ⁡ A$
38 nnuz $⊢ ℕ = ℤ ≥ 1$
39 38 prodf1 $⊢ A ∈ ℕ → seq 1 × ℕ × 1 ⁡ A = 1$
40 39 adantr $⊢ A ∈ ℕ ∧ f : 1 … A ⟶ 1-1 onto A → seq 1 × ℕ × 1 ⁡ A = 1$
41 37 40 eqtrd $⊢ A ∈ ℕ ∧ f : 1 … A ⟶ 1-1 onto A → ∏ k ∈ A 1 = 1$
42 41 ex $⊢ A ∈ ℕ → f : 1 … A ⟶ 1-1 onto A → ∏ k ∈ A 1 = 1$
43 42 exlimdv $⊢ A ∈ ℕ → ∃ f f : 1 … A ⟶ 1-1 onto A → ∏ k ∈ A 1 = 1$
44 43 imp $⊢ A ∈ ℕ ∧ ∃ f f : 1 … A ⟶ 1-1 onto A → ∏ k ∈ A 1 = 1$
45 25 44 jaoi $⊢ A = ∅ ∨ A ∈ ℕ ∧ ∃ f f : 1 … A ⟶ 1-1 onto A → ∏ k ∈ A 1 = 1$
46 28 45 syl $⊢ A ∈ Fin → ∏ k ∈ A 1 = 1$
47 27 46 jaoi $⊢ A ⊆ ℤ ≥ M ∨ A ∈ Fin → ∏ k ∈ A 1 = 1$