| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . . 4
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) | 
| 2 |  | simpr 484 | . . . 4
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∧ 𝑀 ∈ ℤ) → 𝑀 ∈ ℤ) | 
| 3 |  | ax-1ne0 11225 | . . . . 5
⊢ 1 ≠
0 | 
| 4 | 3 | a1i 11 | . . . 4
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∧ 𝑀 ∈ ℤ) → 1 ≠
0) | 
| 5 | 1 | prodfclim1 15930 | . . . . 5
⊢ (𝑀 ∈ ℤ → seq𝑀( · ,
((ℤ≥‘𝑀) × {1})) ⇝ 1) | 
| 6 | 5 | adantl 481 | . . . 4
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∧ 𝑀 ∈ ℤ) → seq𝑀( · ,
((ℤ≥‘𝑀) × {1})) ⇝ 1) | 
| 7 |  | simpl 482 | . . . 4
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∧ 𝑀 ∈ ℤ) → 𝐴 ⊆ (ℤ≥‘𝑀)) | 
| 8 |  | 1ex 11258 | . . . . . . 7
⊢ 1 ∈
V | 
| 9 | 8 | fvconst2 7225 | . . . . . 6
⊢ (𝑘 ∈
(ℤ≥‘𝑀) →
(((ℤ≥‘𝑀) × {1})‘𝑘) = 1) | 
| 10 |  | ifid 4565 | . . . . . 6
⊢ if(𝑘 ∈ 𝐴, 1, 1) = 1 | 
| 11 | 9, 10 | eqtr4di 2794 | . . . . 5
⊢ (𝑘 ∈
(ℤ≥‘𝑀) →
(((ℤ≥‘𝑀) × {1})‘𝑘) = if(𝑘 ∈ 𝐴, 1, 1)) | 
| 12 | 11 | adantl 481 | . . . 4
⊢ (((𝐴 ⊆
(ℤ≥‘𝑀) ∧ 𝑀 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) →
(((ℤ≥‘𝑀) × {1})‘𝑘) = if(𝑘 ∈ 𝐴, 1, 1)) | 
| 13 |  | 1cnd 11257 | . . . 4
⊢ (((𝐴 ⊆
(ℤ≥‘𝑀) ∧ 𝑀 ∈ ℤ) ∧ 𝑘 ∈ 𝐴) → 1 ∈ ℂ) | 
| 14 | 1, 2, 4, 6, 7, 12,
13 | zprodn0 15976 | . . 3
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∧ 𝑀 ∈ ℤ) → ∏𝑘 ∈ 𝐴 1 = 1) | 
| 15 |  | uzf 12882 | . . . . . . . . 9
⊢
ℤ≥:ℤ⟶𝒫 ℤ | 
| 16 | 15 | fdmi 6746 | . . . . . . . 8
⊢ dom
ℤ≥ = ℤ | 
| 17 | 16 | eleq2i 2832 | . . . . . . 7
⊢ (𝑀 ∈ dom
ℤ≥ ↔ 𝑀 ∈ ℤ) | 
| 18 |  | ndmfv 6940 | . . . . . . 7
⊢ (¬
𝑀 ∈ dom
ℤ≥ → (ℤ≥‘𝑀) = ∅) | 
| 19 | 17, 18 | sylnbir 331 | . . . . . 6
⊢ (¬
𝑀 ∈ ℤ →
(ℤ≥‘𝑀) = ∅) | 
| 20 | 19 | sseq2d 4015 | . . . . 5
⊢ (¬
𝑀 ∈ ℤ →
(𝐴 ⊆
(ℤ≥‘𝑀) ↔ 𝐴 ⊆ ∅)) | 
| 21 | 20 | biimpac 478 | . . . 4
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∧ ¬ 𝑀 ∈ ℤ) → 𝐴 ⊆ ∅) | 
| 22 |  | ss0 4401 | . . . 4
⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) | 
| 23 |  | prodeq1 15944 | . . . . 5
⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 1 = ∏𝑘 ∈ ∅ 1) | 
| 24 |  | prod0 15980 | . . . . 5
⊢
∏𝑘 ∈
∅ 1 = 1 | 
| 25 | 23, 24 | eqtrdi 2792 | . . . 4
⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 1 = 1) | 
| 26 | 21, 22, 25 | 3syl 18 | . . 3
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∧ ¬ 𝑀 ∈ ℤ) → ∏𝑘 ∈ 𝐴 1 = 1) | 
| 27 | 14, 26 | pm2.61dan 812 | . 2
⊢ (𝐴 ⊆
(ℤ≥‘𝑀) → ∏𝑘 ∈ 𝐴 1 = 1) | 
| 28 |  | fz1f1o 15747 | . . 3
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨
((♯‘𝐴) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) | 
| 29 |  | eqidd 2737 | . . . . . . . . 9
⊢ (𝑘 = (𝑓‘𝑗) → 1 = 1) | 
| 30 |  | simpl 482 | . . . . . . . . 9
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → (♯‘𝐴) ∈
ℕ) | 
| 31 |  | simpr 484 | . . . . . . . . 9
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) | 
| 32 |  | 1cnd 11257 | . . . . . . . . 9
⊢
((((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) ∧ 𝑘 ∈ 𝐴) → 1 ∈ ℂ) | 
| 33 |  | elfznn 13594 | . . . . . . . . . . 11
⊢ (𝑗 ∈
(1...(♯‘𝐴))
→ 𝑗 ∈
ℕ) | 
| 34 | 8 | fvconst2 7225 | . . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → ((ℕ
× {1})‘𝑗) =
1) | 
| 35 | 33, 34 | syl 17 | . . . . . . . . . 10
⊢ (𝑗 ∈
(1...(♯‘𝐴))
→ ((ℕ × {1})‘𝑗) = 1) | 
| 36 | 35 | adantl 481 | . . . . . . . . 9
⊢
((((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) ∧ 𝑗 ∈ (1...(♯‘𝐴))) → ((ℕ ×
{1})‘𝑗) =
1) | 
| 37 | 29, 30, 31, 32, 36 | fprod 15978 | . . . . . . . 8
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → ∏𝑘 ∈ 𝐴 1 = (seq1( · , (ℕ ×
{1}))‘(♯‘𝐴))) | 
| 38 |  | nnuz 12922 | . . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) | 
| 39 | 38 | prodf1 15928 | . . . . . . . . 9
⊢
((♯‘𝐴)
∈ ℕ → (seq1( · , (ℕ ×
{1}))‘(♯‘𝐴)) = 1) | 
| 40 | 39 | adantr 480 | . . . . . . . 8
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → (seq1( · ,
(ℕ × {1}))‘(♯‘𝐴)) = 1) | 
| 41 | 37, 40 | eqtrd 2776 | . . . . . . 7
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → ∏𝑘 ∈ 𝐴 1 = 1) | 
| 42 | 41 | ex 412 | . . . . . 6
⊢
((♯‘𝐴)
∈ ℕ → (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → ∏𝑘 ∈ 𝐴 1 = 1)) | 
| 43 | 42 | exlimdv 1932 | . . . . 5
⊢
((♯‘𝐴)
∈ ℕ → (∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → ∏𝑘 ∈ 𝐴 1 = 1)) | 
| 44 | 43 | imp 406 | . . . 4
⊢
(((♯‘𝐴)
∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → ∏𝑘 ∈ 𝐴 1 = 1) | 
| 45 | 25, 44 | jaoi 857 | . . 3
⊢ ((𝐴 = ∅ ∨
((♯‘𝐴) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ∏𝑘 ∈ 𝐴 1 = 1) | 
| 46 | 28, 45 | syl 17 | . 2
⊢ (𝐴 ∈ Fin → ∏𝑘 ∈ 𝐴 1 = 1) | 
| 47 | 27, 46 | jaoi 857 | 1
⊢ ((𝐴 ⊆
(ℤ≥‘𝑀) ∨ 𝐴 ∈ Fin) → ∏𝑘 ∈ 𝐴 1 = 1) |