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 )