Step | Hyp | Ref
| Expression |
1 | | eqid 2798 |
. . . 4
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) |
2 | | simpr 488 |
. . . 4
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∧ 𝑀 ∈ ℤ) → 𝑀 ∈ ℤ) |
3 | | ax-1ne0 10595 |
. . . . 5
⊢ 1 ≠
0 |
4 | 3 | a1i 11 |
. . . 4
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∧ 𝑀 ∈ ℤ) → 1 ≠
0) |
5 | 1 | prodfclim1 15241 |
. . . . 5
⊢ (𝑀 ∈ ℤ → seq𝑀( · ,
((ℤ≥‘𝑀) × {1})) ⇝ 1) |
6 | 5 | adantl 485 |
. . . 4
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∧ 𝑀 ∈ ℤ) → seq𝑀( · ,
((ℤ≥‘𝑀) × {1})) ⇝ 1) |
7 | | simpl 486 |
. . . 4
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∧ 𝑀 ∈ ℤ) → 𝐴 ⊆ (ℤ≥‘𝑀)) |
8 | | 1ex 10626 |
. . . . . . 7
⊢ 1 ∈
V |
9 | 8 | fvconst2 6943 |
. . . . . 6
⊢ (𝑘 ∈
(ℤ≥‘𝑀) →
(((ℤ≥‘𝑀) × {1})‘𝑘) = 1) |
10 | | ifid 4464 |
. . . . . 6
⊢ if(𝑘 ∈ 𝐴, 1, 1) = 1 |
11 | 9, 10 | eqtr4di 2851 |
. . . . 5
⊢ (𝑘 ∈
(ℤ≥‘𝑀) →
(((ℤ≥‘𝑀) × {1})‘𝑘) = if(𝑘 ∈ 𝐴, 1, 1)) |
12 | 11 | adantl 485 |
. . . 4
⊢ (((𝐴 ⊆
(ℤ≥‘𝑀) ∧ 𝑀 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) →
(((ℤ≥‘𝑀) × {1})‘𝑘) = if(𝑘 ∈ 𝐴, 1, 1)) |
13 | | 1cnd 10625 |
. . . 4
⊢ (((𝐴 ⊆
(ℤ≥‘𝑀) ∧ 𝑀 ∈ ℤ) ∧ 𝑘 ∈ 𝐴) → 1 ∈ ℂ) |
14 | 1, 2, 4, 6, 7, 12,
13 | zprodn0 15285 |
. . 3
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∧ 𝑀 ∈ ℤ) → ∏𝑘 ∈ 𝐴 1 = 1) |
15 | | uzf 12234 |
. . . . . . . . 9
⊢
ℤ≥:ℤ⟶𝒫 ℤ |
16 | 15 | fdmi 6498 |
. . . . . . . 8
⊢ dom
ℤ≥ = ℤ |
17 | 16 | eleq2i 2881 |
. . . . . . 7
⊢ (𝑀 ∈ dom
ℤ≥ ↔ 𝑀 ∈ ℤ) |
18 | | ndmfv 6675 |
. . . . . . 7
⊢ (¬
𝑀 ∈ dom
ℤ≥ → (ℤ≥‘𝑀) = ∅) |
19 | 17, 18 | sylnbir 334 |
. . . . . 6
⊢ (¬
𝑀 ∈ ℤ →
(ℤ≥‘𝑀) = ∅) |
20 | 19 | sseq2d 3947 |
. . . . 5
⊢ (¬
𝑀 ∈ ℤ →
(𝐴 ⊆
(ℤ≥‘𝑀) ↔ 𝐴 ⊆ ∅)) |
21 | 20 | biimpac 482 |
. . . 4
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∧ ¬ 𝑀 ∈ ℤ) → 𝐴 ⊆ ∅) |
22 | | ss0 4306 |
. . . 4
⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) |
23 | | prodeq1 15255 |
. . . . 5
⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 1 = ∏𝑘 ∈ ∅ 1) |
24 | | prod0 15289 |
. . . . 5
⊢
∏𝑘 ∈
∅ 1 = 1 |
25 | 23, 24 | eqtrdi 2849 |
. . . 4
⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 1 = 1) |
26 | 21, 22, 25 | 3syl 18 |
. . 3
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∧ ¬ 𝑀 ∈ ℤ) → ∏𝑘 ∈ 𝐴 1 = 1) |
27 | 14, 26 | pm2.61dan 812 |
. 2
⊢ (𝐴 ⊆
(ℤ≥‘𝑀) → ∏𝑘 ∈ 𝐴 1 = 1) |
28 | | fz1f1o 15059 |
. . 3
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨
((♯‘𝐴) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) |
29 | | eqidd 2799 |
. . . . . . . . 9
⊢ (𝑘 = (𝑓‘𝑗) → 1 = 1) |
30 | | simpl 486 |
. . . . . . . . 9
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → (♯‘𝐴) ∈
ℕ) |
31 | | simpr 488 |
. . . . . . . . 9
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) |
32 | | 1cnd 10625 |
. . . . . . . . 9
⊢
((((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) ∧ 𝑘 ∈ 𝐴) → 1 ∈ ℂ) |
33 | | elfznn 12931 |
. . . . . . . . . . 11
⊢ (𝑗 ∈
(1...(♯‘𝐴))
→ 𝑗 ∈
ℕ) |
34 | 8 | fvconst2 6943 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → ((ℕ
× {1})‘𝑗) =
1) |
35 | 33, 34 | syl 17 |
. . . . . . . . . 10
⊢ (𝑗 ∈
(1...(♯‘𝐴))
→ ((ℕ × {1})‘𝑗) = 1) |
36 | 35 | adantl 485 |
. . . . . . . . 9
⊢
((((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) ∧ 𝑗 ∈ (1...(♯‘𝐴))) → ((ℕ ×
{1})‘𝑗) =
1) |
37 | 29, 30, 31, 32, 36 | fprod 15287 |
. . . . . . . 8
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → ∏𝑘 ∈ 𝐴 1 = (seq1( · , (ℕ ×
{1}))‘(♯‘𝐴))) |
38 | | nnuz 12269 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
39 | 38 | prodf1 15239 |
. . . . . . . . 9
⊢
((♯‘𝐴)
∈ ℕ → (seq1( · , (ℕ ×
{1}))‘(♯‘𝐴)) = 1) |
40 | 39 | adantr 484 |
. . . . . . . 8
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → (seq1( · ,
(ℕ × {1}))‘(♯‘𝐴)) = 1) |
41 | 37, 40 | eqtrd 2833 |
. . . . . . 7
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → ∏𝑘 ∈ 𝐴 1 = 1) |
42 | 41 | ex 416 |
. . . . . 6
⊢
((♯‘𝐴)
∈ ℕ → (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → ∏𝑘 ∈ 𝐴 1 = 1)) |
43 | 42 | exlimdv 1934 |
. . . . 5
⊢
((♯‘𝐴)
∈ ℕ → (∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → ∏𝑘 ∈ 𝐴 1 = 1)) |
44 | 43 | imp 410 |
. . . 4
⊢
(((♯‘𝐴)
∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → ∏𝑘 ∈ 𝐴 1 = 1) |
45 | 25, 44 | jaoi 854 |
. . 3
⊢ ((𝐴 = ∅ ∨
((♯‘𝐴) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ∏𝑘 ∈ 𝐴 1 = 1) |
46 | 28, 45 | syl 17 |
. 2
⊢ (𝐴 ∈ Fin → ∏𝑘 ∈ 𝐴 1 = 1) |
47 | 27, 46 | jaoi 854 |
1
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∨ 𝐴 ∈ Fin) → ∏𝑘 ∈ 𝐴 1 = 1) |