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 syl6eqr 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 syl6eq 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