Step | Hyp | Ref
| Expression |
1 | | eqid 2170 |
. . 3
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) |
2 | | simp1 992 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ⊆
(ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) → 𝑀 ∈ ℤ) |
3 | | 1ap0 8509 |
. . . 4
⊢ 1 #
0 |
4 | 3 | a1i 9 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ⊆
(ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) → 1 # 0) |
5 | 1 | prodfclim1 11507 |
. . . 4
⊢ (𝑀 ∈ ℤ → seq𝑀( · ,
((ℤ≥‘𝑀) × {1})) ⇝ 1) |
6 | 2, 5 | syl 14 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ⊆
(ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) → seq𝑀( · ,
((ℤ≥‘𝑀) × {1})) ⇝ 1) |
7 | | simp3 994 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ⊆
(ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) → ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) |
8 | | eleq1w 2231 |
. . . . . 6
⊢ (𝑗 = 𝑎 → (𝑗 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴)) |
9 | 8 | dcbid 833 |
. . . . 5
⊢ (𝑗 = 𝑎 → (DECID 𝑗 ∈ 𝐴 ↔ DECID 𝑎 ∈ 𝐴)) |
10 | 9 | cbvralv 2696 |
. . . 4
⊢
(∀𝑗 ∈
(ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴 ↔ ∀𝑎 ∈ (ℤ≥‘𝑀)DECID 𝑎 ∈ 𝐴) |
11 | 7, 10 | sylib 121 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ⊆
(ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) → ∀𝑎 ∈ (ℤ≥‘𝑀)DECID 𝑎 ∈ 𝐴) |
12 | | simp2 993 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ⊆
(ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) → 𝐴 ⊆ (ℤ≥‘𝑀)) |
13 | | 1ex 7915 |
. . . . . 6
⊢ 1 ∈
V |
14 | 13 | fvconst2 5712 |
. . . . 5
⊢ (𝑘 ∈
(ℤ≥‘𝑀) →
(((ℤ≥‘𝑀) × {1})‘𝑘) = 1) |
15 | 14 | adantl 275 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆
(ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) →
(((ℤ≥‘𝑀) × {1})‘𝑘) = 1) |
16 | | eleq1w 2231 |
. . . . . . 7
⊢ (𝑎 = 𝑘 → (𝑎 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴)) |
17 | 16 | dcbid 833 |
. . . . . 6
⊢ (𝑎 = 𝑘 → (DECID 𝑎 ∈ 𝐴 ↔ DECID 𝑘 ∈ 𝐴)) |
18 | 11 | adantr 274 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆
(ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ∀𝑎 ∈
(ℤ≥‘𝑀)DECID 𝑎 ∈ 𝐴) |
19 | | simpr 109 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆
(ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
20 | 17, 18, 19 | rspcdva 2839 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆
(ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴) |
21 | | ifiddc 3559 |
. . . . 5
⊢
(DECID 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 1, 1) = 1) |
22 | 20, 21 | syl 14 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆
(ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → if(𝑘 ∈ 𝐴, 1, 1) = 1) |
23 | 15, 22 | eqtr4d 2206 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆
(ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) →
(((ℤ≥‘𝑀) × {1})‘𝑘) = if(𝑘 ∈ 𝐴, 1, 1)) |
24 | | 1cnd 7936 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆
(ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐴) → 1 ∈ ℂ) |
25 | 1, 2, 4, 6, 11, 12, 23, 24 | zprodap0 11544 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ⊆
(ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) → ∏𝑘 ∈ 𝐴 1 = 1) |
26 | | fz1f1o 11338 |
. . 3
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨
((♯‘𝐴) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) |
27 | | prodeq1 11516 |
. . . . 5
⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 1 = ∏𝑘 ∈ ∅ 1) |
28 | | prod0 11548 |
. . . . 5
⊢
∏𝑘 ∈
∅ 1 = 1 |
29 | 27, 28 | eqtrdi 2219 |
. . . 4
⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 1 = 1) |
30 | | eqidd 2171 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑓‘𝑗) → 1 = 1) |
31 | | simpl 108 |
. . . . . . . . . 10
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → (♯‘𝐴) ∈
ℕ) |
32 | | simpr 109 |
. . . . . . . . . 10
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) |
33 | | 1cnd 7936 |
. . . . . . . . . 10
⊢
((((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) ∧ 𝑘 ∈ 𝐴) → 1 ∈ ℂ) |
34 | | elfznn 10010 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(1...(♯‘𝐴))
→ 𝑗 ∈
ℕ) |
35 | 13 | fvconst2 5712 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → ((ℕ
× {1})‘𝑗) =
1) |
36 | 34, 35 | syl 14 |
. . . . . . . . . . 11
⊢ (𝑗 ∈
(1...(♯‘𝐴))
→ ((ℕ × {1})‘𝑗) = 1) |
37 | 36 | adantl 275 |
. . . . . . . . . 10
⊢
((((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) ∧ 𝑗 ∈ (1...(♯‘𝐴))) → ((ℕ ×
{1})‘𝑗) =
1) |
38 | 30, 31, 32, 33, 37 | fprodseq 11546 |
. . . . . . . . 9
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → ∏𝑘 ∈ 𝐴 1 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ((ℕ × {1})‘𝑗),
1)))‘(♯‘𝐴))) |
39 | | simpr 109 |
. . . . . . . . . . . . . . . . 17
⊢
((((♯‘𝐴)
∈ ℕ ∧ 𝑗
∈ ℕ) ∧ 𝑗
≤ (♯‘𝐴))
→ 𝑗 ≤
(♯‘𝐴)) |
40 | 39 | iftrued 3533 |
. . . . . . . . . . . . . . . 16
⊢
((((♯‘𝐴)
∈ ℕ ∧ 𝑗
∈ ℕ) ∧ 𝑗
≤ (♯‘𝐴))
→ if(𝑗 ≤
(♯‘𝐴),
((ℕ × {1})‘𝑗), 1) = ((ℕ × {1})‘𝑗)) |
41 | 35 | ad2antlr 486 |
. . . . . . . . . . . . . . . 16
⊢
((((♯‘𝐴)
∈ ℕ ∧ 𝑗
∈ ℕ) ∧ 𝑗
≤ (♯‘𝐴))
→ ((ℕ × {1})‘𝑗) = 1) |
42 | 40, 41 | eqtrd 2203 |
. . . . . . . . . . . . . . 15
⊢
((((♯‘𝐴)
∈ ℕ ∧ 𝑗
∈ ℕ) ∧ 𝑗
≤ (♯‘𝐴))
→ if(𝑗 ≤
(♯‘𝐴),
((ℕ × {1})‘𝑗), 1) = 1) |
43 | | simpr 109 |
. . . . . . . . . . . . . . . 16
⊢
((((♯‘𝐴)
∈ ℕ ∧ 𝑗
∈ ℕ) ∧ ¬ 𝑗 ≤ (♯‘𝐴)) → ¬ 𝑗 ≤ (♯‘𝐴)) |
44 | 43 | iffalsed 3536 |
. . . . . . . . . . . . . . 15
⊢
((((♯‘𝐴)
∈ ℕ ∧ 𝑗
∈ ℕ) ∧ ¬ 𝑗 ≤ (♯‘𝐴)) → if(𝑗 ≤ (♯‘𝐴), ((ℕ × {1})‘𝑗), 1) = 1) |
45 | | nnz 9231 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℤ) |
46 | | nnz 9231 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘𝐴)
∈ ℕ → (♯‘𝐴) ∈ ℤ) |
47 | | zdcle 9288 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ ℤ ∧
(♯‘𝐴) ∈
ℤ) → DECID 𝑗 ≤ (♯‘𝐴)) |
48 | 45, 46, 47 | syl2anr 288 |
. . . . . . . . . . . . . . . 16
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑗
∈ ℕ) → DECID 𝑗 ≤ (♯‘𝐴)) |
49 | | exmiddc 831 |
. . . . . . . . . . . . . . . 16
⊢
(DECID 𝑗 ≤ (♯‘𝐴) → (𝑗 ≤ (♯‘𝐴) ∨ ¬ 𝑗 ≤ (♯‘𝐴))) |
50 | 48, 49 | syl 14 |
. . . . . . . . . . . . . . 15
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑗
∈ ℕ) → (𝑗
≤ (♯‘𝐴) ∨
¬ 𝑗 ≤
(♯‘𝐴))) |
51 | 42, 44, 50 | mpjaodan 793 |
. . . . . . . . . . . . . 14
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑗
∈ ℕ) → if(𝑗
≤ (♯‘𝐴),
((ℕ × {1})‘𝑗), 1) = 1) |
52 | 51 | mpteq2dva 4079 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐴)
∈ ℕ → (𝑗
∈ ℕ ↦ if(𝑗
≤ (♯‘𝐴),
((ℕ × {1})‘𝑗), 1)) = (𝑗 ∈ ℕ ↦ 1)) |
53 | | fconstmpt 4658 |
. . . . . . . . . . . . 13
⊢ (ℕ
× {1}) = (𝑗 ∈
ℕ ↦ 1) |
54 | 52, 53 | eqtr4di 2221 |
. . . . . . . . . . . 12
⊢
((♯‘𝐴)
∈ ℕ → (𝑗
∈ ℕ ↦ if(𝑗
≤ (♯‘𝐴),
((ℕ × {1})‘𝑗), 1)) = (ℕ ×
{1})) |
55 | 54 | seqeq3d 10409 |
. . . . . . . . . . 11
⊢
((♯‘𝐴)
∈ ℕ → seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ((ℕ × {1})‘𝑗), 1))) = seq1( · ,
(ℕ × {1}))) |
56 | 55 | adantr 274 |
. . . . . . . . . 10
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ((ℕ ×
{1})‘𝑗), 1))) = seq1(
· , (ℕ × {1}))) |
57 | 56 | fveq1d 5498 |
. . . . . . . . 9
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → (seq1( · ,
(𝑗 ∈ ℕ ↦
if(𝑗 ≤
(♯‘𝐴),
((ℕ × {1})‘𝑗), 1)))‘(♯‘𝐴)) = (seq1( · , (ℕ
× {1}))‘(♯‘𝐴))) |
58 | 38, 57 | eqtrd 2203 |
. . . . . . . 8
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → ∏𝑘 ∈ 𝐴 1 = (seq1( · , (ℕ ×
{1}))‘(♯‘𝐴))) |
59 | | nnuz 9522 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
60 | 59 | prodf1 11505 |
. . . . . . . . 9
⊢
((♯‘𝐴)
∈ ℕ → (seq1( · , (ℕ ×
{1}))‘(♯‘𝐴)) = 1) |
61 | 60 | adantr 274 |
. . . . . . . 8
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → (seq1( · ,
(ℕ × {1}))‘(♯‘𝐴)) = 1) |
62 | 58, 61 | eqtrd 2203 |
. . . . . . 7
⊢
(((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → ∏𝑘 ∈ 𝐴 1 = 1) |
63 | 62 | ex 114 |
. . . . . 6
⊢
((♯‘𝐴)
∈ ℕ → (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → ∏𝑘 ∈ 𝐴 1 = 1)) |
64 | 63 | exlimdv 1812 |
. . . . 5
⊢
((♯‘𝐴)
∈ ℕ → (∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → ∏𝑘 ∈ 𝐴 1 = 1)) |
65 | 64 | imp 123 |
. . . 4
⊢
(((♯‘𝐴)
∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → ∏𝑘 ∈ 𝐴 1 = 1) |
66 | 29, 65 | jaoi 711 |
. . 3
⊢ ((𝐴 = ∅ ∨
((♯‘𝐴) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ∏𝑘 ∈ 𝐴 1 = 1) |
67 | 26, 66 | syl 14 |
. 2
⊢ (𝐴 ∈ Fin → ∏𝑘 ∈ 𝐴 1 = 1) |
68 | 25, 67 | jaoi 711 |
1
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆
(ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) ∨ 𝐴 ∈ Fin) → ∏𝑘 ∈ 𝐴 1 = 1) |