Step | Hyp | Ref
| Expression |
1 | | prodeq1 15617 |
. . . . 5
⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ ∅ 𝐵) |
2 | | prod0 15651 |
. . . . 5
⊢
∏𝑘 ∈
∅ 𝐵 =
1 |
3 | 1, 2 | eqtrdi 2796 |
. . . 4
⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 𝐵 = 1) |
4 | | ax-1ne0 10941 |
. . . . 5
⊢ 1 ≠
0 |
5 | 4 | a1i 11 |
. . . 4
⊢ (𝐴 = ∅ → 1 ≠
0) |
6 | 3, 5 | eqnetrd 3013 |
. . 3
⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 𝐵 ≠ 0) |
7 | 6 | a1i 11 |
. 2
⊢ (𝜑 → (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 𝐵 ≠ 0)) |
8 | | prodfc 15653 |
. . . . . . 7
⊢
∏𝑚 ∈
𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ∏𝑘 ∈ 𝐴 𝐵 |
9 | | fveq2 6771 |
. . . . . . . 8
⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
10 | | simprl 768 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (♯‘𝐴) ∈
ℕ) |
11 | | simprr 770 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) |
12 | | fprodn0.2 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
13 | 12 | fmpttd 6986 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
14 | 13 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
15 | 14 | ffvelrnda 6958 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) ∈ ℂ) |
16 | | f1of 6714 |
. . . . . . . . . 10
⊢ (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝑓:(1...(♯‘𝐴))⟶𝐴) |
17 | 11, 16 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))⟶𝐴) |
18 | | fvco3 6864 |
. . . . . . . . 9
⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
19 | 17, 18 | sylan 580 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
20 | 9, 10, 11, 15, 19 | fprod 15649 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = (seq1( · , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓))‘(♯‘𝐴))) |
21 | 8, 20 | eqtr3id 2794 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ∏𝑘 ∈ 𝐴 𝐵 = (seq1( · , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓))‘(♯‘𝐴))) |
22 | | nnuz 12620 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
23 | 10, 22 | eleqtrdi 2851 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (♯‘𝐴) ∈
(ℤ≥‘1)) |
24 | | fco 6622 |
. . . . . . . . 9
⊢ (((𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ ∧ 𝑓:(1...(♯‘𝐴))⟶𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ) |
25 | 14, 17, 24 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ) |
26 | 25 | ffvelrnda 6958 |
. . . . . . 7
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑚) ∈ ℂ) |
27 | | fvco3 6864 |
. . . . . . . . 9
⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑚 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑚))) |
28 | 17, 27 | sylan 580 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑚))) |
29 | 16 | ffvelrnda 6958 |
. . . . . . . . . . 11
⊢ ((𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 ∧ 𝑚 ∈ (1...(♯‘𝐴))) → (𝑓‘𝑚) ∈ 𝐴) |
30 | 29 | adantll 711 |
. . . . . . . . . 10
⊢
((((♯‘𝐴)
∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) ∧ 𝑚 ∈ (1...(♯‘𝐴))) → (𝑓‘𝑚) ∈ 𝐴) |
31 | | simpr 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓‘𝑚) ∈ 𝐴) → (𝑓‘𝑚) ∈ 𝐴) |
32 | | nfcv 2909 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘(𝑓‘𝑚) |
33 | | nfv 1921 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘𝜑 |
34 | | nfcsb1v 3862 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 |
35 | 34 | nfel1 2925 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ |
36 | 33, 35 | nfim 1903 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘(𝜑 → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ) |
37 | | csbeq1a 3851 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑓‘𝑚) → 𝐵 = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
38 | 37 | eleq1d 2825 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑓‘𝑚) → (𝐵 ∈ ℂ ↔ ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) |
39 | 38 | imbi2d 341 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑓‘𝑚) → ((𝜑 → 𝐵 ∈ ℂ) ↔ (𝜑 → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ))) |
40 | 12 | expcom 414 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ 𝐴 → (𝜑 → 𝐵 ∈ ℂ)) |
41 | 32, 36, 39, 40 | vtoclgaf 3511 |
. . . . . . . . . . . . 13
⊢ ((𝑓‘𝑚) ∈ 𝐴 → (𝜑 → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) |
42 | 41 | impcom 408 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓‘𝑚) ∈ 𝐴) → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ) |
43 | | eqid 2740 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵) |
44 | 43 | fvmpts 6875 |
. . . . . . . . . . . 12
⊢ (((𝑓‘𝑚) ∈ 𝐴 ∧ ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑚)) = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
45 | 31, 42, 44 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓‘𝑚) ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑚)) = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
46 | | nfcv 2909 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘0 |
47 | 34, 46 | nfne 3047 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ≠ 0 |
48 | 33, 47 | nfim 1903 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘(𝜑 → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ≠ 0) |
49 | 37 | neeq1d 3005 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑓‘𝑚) → (𝐵 ≠ 0 ↔ ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ≠ 0)) |
50 | 49 | imbi2d 341 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑓‘𝑚) → ((𝜑 → 𝐵 ≠ 0) ↔ (𝜑 → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ≠ 0))) |
51 | | fprodn0.3 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ≠ 0) |
52 | 51 | expcom 414 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝐴 → (𝜑 → 𝐵 ≠ 0)) |
53 | 32, 48, 50, 52 | vtoclgaf 3511 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑚) ∈ 𝐴 → (𝜑 → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ≠ 0)) |
54 | 53 | impcom 408 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓‘𝑚) ∈ 𝐴) → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ≠ 0) |
55 | 45, 54 | eqnetrd 3013 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓‘𝑚) ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑚)) ≠ 0) |
56 | 30, 55 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) ∧ 𝑚 ∈ (1...(♯‘𝐴)))) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑚)) ≠ 0) |
57 | 56 | anassrs 468 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ (1...(♯‘𝐴))) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑚)) ≠ 0) |
58 | 28, 57 | eqnetrd 3013 |
. . . . . . 7
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑚) ≠ 0) |
59 | 23, 26, 58 | prodfn0 15604 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (seq1( · ,
((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓))‘(♯‘𝐴)) ≠ 0) |
60 | 21, 59 | eqnetrd 3013 |
. . . . 5
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ∏𝑘 ∈ 𝐴 𝐵 ≠ 0) |
61 | 60 | expr 457 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) → (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → ∏𝑘 ∈ 𝐴 𝐵 ≠ 0)) |
62 | 61 | exlimdv 1940 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) →
(∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → ∏𝑘 ∈ 𝐴 𝐵 ≠ 0)) |
63 | 62 | expimpd 454 |
. 2
⊢ (𝜑 → (((♯‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → ∏𝑘 ∈ 𝐴 𝐵 ≠ 0)) |
64 | | fprodn0.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
65 | | fz1f1o 15420 |
. . 3
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨
((♯‘𝐴) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) |
66 | 64, 65 | syl 17 |
. 2
⊢ (𝜑 → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) |
67 | 7, 63, 66 | mpjaod 857 |
1
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ≠ 0) |