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 )