Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . 4
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) |
2 | | simpr 477 |
. . . 4
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∧ 𝑀 ∈ ℤ) → 𝑀 ∈ ℤ) |
3 | | ax-1ne0 10005 |
. . . . 5
⊢ 1 ≠
0 |
4 | 3 | a1i 11 |
. . . 4
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∧ 𝑀 ∈ ℤ) → 1 ≠
0) |
5 | 1 | prodfclim1 14625 |
. . . . 5
⊢ (𝑀 ∈ ℤ → seq𝑀( · ,
((ℤ≥‘𝑀) × {1})) ⇝ 1) |
6 | 5 | adantl 482 |
. . . 4
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∧ 𝑀 ∈ ℤ) → seq𝑀( · ,
((ℤ≥‘𝑀) × {1})) ⇝ 1) |
7 | | simpl 473 |
. . . 4
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∧ 𝑀 ∈ ℤ) → 𝐴 ⊆ (ℤ≥‘𝑀)) |
8 | | 1ex 10035 |
. . . . . . 7
⊢ 1 ∈
V |
9 | 8 | fvconst2 6469 |
. . . . . 6
⊢ (𝑘 ∈
(ℤ≥‘𝑀) →
(((ℤ≥‘𝑀) × {1})‘𝑘) = 1) |
10 | | ifid 4125 |
. . . . . 6
⊢ if(𝑘 ∈ 𝐴, 1, 1) = 1 |
11 | 9, 10 | syl6eqr 2674 |
. . . . 5
⊢ (𝑘 ∈
(ℤ≥‘𝑀) →
(((ℤ≥‘𝑀) × {1})‘𝑘) = if(𝑘 ∈ 𝐴, 1, 1)) |
12 | 11 | adantl 482 |
. . . 4
⊢ (((𝐴 ⊆
(ℤ≥‘𝑀) ∧ 𝑀 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) →
(((ℤ≥‘𝑀) × {1})‘𝑘) = if(𝑘 ∈ 𝐴, 1, 1)) |
13 | | 1cnd 10056 |
. . . 4
⊢ (((𝐴 ⊆
(ℤ≥‘𝑀) ∧ 𝑀 ∈ ℤ) ∧ 𝑘 ∈ 𝐴) → 1 ∈ ℂ) |
14 | 1, 2, 4, 6, 7, 12,
13 | zprodn0 14669 |
. . 3
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∧ 𝑀 ∈ ℤ) → ∏𝑘 ∈ 𝐴 1 = 1) |
15 | | uzf 11690 |
. . . . . . . . 9
⊢
ℤ≥:ℤ⟶𝒫 ℤ |
16 | 15 | fdmi 6052 |
. . . . . . . 8
⊢ dom
ℤ≥ = ℤ |
17 | 16 | eleq2i 2693 |
. . . . . . 7
⊢ (𝑀 ∈ dom
ℤ≥ ↔ 𝑀 ∈ ℤ) |
18 | | ndmfv 6218 |
. . . . . . 7
⊢ (¬
𝑀 ∈ dom
ℤ≥ → (ℤ≥‘𝑀) = ∅) |
19 | 17, 18 | sylnbir 321 |
. . . . . 6
⊢ (¬
𝑀 ∈ ℤ →
(ℤ≥‘𝑀) = ∅) |
20 | 19 | sseq2d 3633 |
. . . . 5
⊢ (¬
𝑀 ∈ ℤ →
(𝐴 ⊆
(ℤ≥‘𝑀) ↔ 𝐴 ⊆ ∅)) |
21 | 20 | biimpac 503 |
. . . 4
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∧ ¬ 𝑀 ∈ ℤ) → 𝐴 ⊆ ∅) |
22 | | ss0 3974 |
. . . 4
⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) |
23 | | prodeq1 14639 |
. . . . 5
⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 1 = ∏𝑘 ∈ ∅ 1) |
24 | | prod0 14673 |
. . . . 5
⊢
∏𝑘 ∈
∅ 1 = 1 |
25 | 23, 24 | syl6eq 2672 |
. . . 4
⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 1 = 1) |
26 | 21, 22, 25 | 3syl 18 |
. . 3
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∧ ¬ 𝑀 ∈ ℤ) → ∏𝑘 ∈ 𝐴 1 = 1) |
27 | 14, 26 | pm2.61dan 832 |
. 2
⊢ (𝐴 ⊆
(ℤ≥‘𝑀) → ∏𝑘 ∈ 𝐴 1 = 1) |
28 | | fz1f1o 14441 |
. . 3
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨ ((#‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴))) |
29 | | eqidd 2623 |
. . . . . . . . 9
⊢ (𝑘 = (𝑓‘𝑗) → 1 = 1) |
30 | | simpl 473 |
. . . . . . . . 9
⊢
(((#‘𝐴) ∈
ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) → (#‘𝐴) ∈
ℕ) |
31 | | simpr 477 |
. . . . . . . . 9
⊢
(((#‘𝐴) ∈
ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) → 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) |
32 | | 1cnd 10056 |
. . . . . . . . 9
⊢
((((#‘𝐴)
∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) ∧ 𝑘 ∈ 𝐴) → 1 ∈ ℂ) |
33 | | elfznn 12370 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (1...(#‘𝐴)) → 𝑗 ∈ ℕ) |
34 | 8 | fvconst2 6469 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → ((ℕ
× {1})‘𝑗) =
1) |
35 | 33, 34 | syl 17 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (1...(#‘𝐴)) → ((ℕ ×
{1})‘𝑗) =
1) |
36 | 35 | adantl 482 |
. . . . . . . . 9
⊢
((((#‘𝐴)
∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) ∧ 𝑗 ∈ (1...(#‘𝐴))) → ((ℕ ×
{1})‘𝑗) =
1) |
37 | 29, 30, 31, 32, 36 | fprod 14671 |
. . . . . . . 8
⊢
(((#‘𝐴) ∈
ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) → ∏𝑘 ∈ 𝐴 1 = (seq1( · , (ℕ ×
{1}))‘(#‘𝐴))) |
38 | | nnuz 11723 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
39 | 38 | prodf1 14623 |
. . . . . . . . 9
⊢
((#‘𝐴) ∈
ℕ → (seq1( · , (ℕ × {1}))‘(#‘𝐴)) = 1) |
40 | 39 | adantr 481 |
. . . . . . . 8
⊢
(((#‘𝐴) ∈
ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) → (seq1( · ,
(ℕ × {1}))‘(#‘𝐴)) = 1) |
41 | 37, 40 | eqtrd 2656 |
. . . . . . 7
⊢
(((#‘𝐴) ∈
ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) → ∏𝑘 ∈ 𝐴 1 = 1) |
42 | 41 | ex 450 |
. . . . . 6
⊢
((#‘𝐴) ∈
ℕ → (𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → ∏𝑘 ∈ 𝐴 1 = 1)) |
43 | 42 | exlimdv 1861 |
. . . . 5
⊢
((#‘𝐴) ∈
ℕ → (∃𝑓
𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → ∏𝑘 ∈ 𝐴 1 = 1)) |
44 | 43 | imp 445 |
. . . 4
⊢
(((#‘𝐴) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) → ∏𝑘 ∈ 𝐴 1 = 1) |
45 | 25, 44 | jaoi 394 |
. . 3
⊢ ((𝐴 = ∅ ∨ ((#‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ∏𝑘 ∈ 𝐴 1 = 1) |
46 | 28, 45 | syl 17 |
. 2
⊢ (𝐴 ∈ Fin → ∏𝑘 ∈ 𝐴 1 = 1) |
47 | 27, 46 | jaoi 394 |
1
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∨ 𝐴 ∈ Fin) → ∏𝑘 ∈ 𝐴 1 = 1) |