This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) ∨ 𝐴 ∈ Fin ) → ∏ 𝑘 ∈ 𝐴 1 = 1 )

Proof

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