Step | Hyp | Ref
| Expression |
1 | | prodeq1 14639 |
. . . . 5
⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ ∅ 𝐵) |
2 | | prod0 14673 |
. . . . 5
⊢
∏𝑘 ∈
∅ 𝐵 =
1 |
3 | 1, 2 | syl6eq 2672 |
. . . 4
⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 𝐵 = 1) |
4 | | ax-1ne0 10005 |
. . . . 5
⊢ 1 ≠
0 |
5 | 4 | a1i 11 |
. . . 4
⊢ (𝐴 = ∅ → 1 ≠
0) |
6 | 3, 5 | eqnetrd 2861 |
. . 3
⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 𝐵 ≠ 0) |
7 | 6 | a1i 11 |
. 2
⊢ (𝜑 → (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 𝐵 ≠ 0)) |
8 | | prodfc 14675 |
. . . . . . 7
⊢
∏𝑚 ∈
𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ∏𝑘 ∈ 𝐴 𝐵 |
9 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
10 | | simprl 794 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (#‘𝐴) ∈
ℕ) |
11 | | simprr 796 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) |
12 | | fprodn0.2 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
13 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵) |
14 | 12, 13 | fmptd 6385 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
15 | 14 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
16 | 15 | ffvelrnda 6359 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) ∈ ℂ) |
17 | | f1of 6137 |
. . . . . . . . . 10
⊢ (𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → 𝑓:(1...(#‘𝐴))⟶𝐴) |
18 | 11, 17 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(#‘𝐴))⟶𝐴) |
19 | | fvco3 6275 |
. . . . . . . . 9
⊢ ((𝑓:(1...(#‘𝐴))⟶𝐴 ∧ 𝑛 ∈ (1...(#‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
20 | 18, 19 | sylan 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(#‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
21 | 9, 10, 11, 16, 20 | fprod 14671 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = (seq1( · , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓))‘(#‘𝐴))) |
22 | 8, 21 | syl5eqr 2670 |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ∏𝑘 ∈ 𝐴 𝐵 = (seq1( · , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓))‘(#‘𝐴))) |
23 | | nnuz 11723 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
24 | 10, 23 | syl6eleq 2711 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (#‘𝐴) ∈
(ℤ≥‘1)) |
25 | | fco 6058 |
. . . . . . . . 9
⊢ (((𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ ∧ 𝑓:(1...(#‘𝐴))⟶𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(#‘𝐴))⟶ℂ) |
26 | 15, 18, 25 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(#‘𝐴))⟶ℂ) |
27 | 26 | ffvelrnda 6359 |
. . . . . . 7
⊢ (((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ (1...(#‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑚) ∈ ℂ) |
28 | | fvco3 6275 |
. . . . . . . . 9
⊢ ((𝑓:(1...(#‘𝐴))⟶𝐴 ∧ 𝑚 ∈ (1...(#‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑚))) |
29 | 18, 28 | sylan 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ (1...(#‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑚))) |
30 | 17 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢ ((𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 ∧ 𝑚 ∈ (1...(#‘𝐴))) → (𝑓‘𝑚) ∈ 𝐴) |
31 | 30 | adantll 750 |
. . . . . . . . . 10
⊢
((((#‘𝐴)
∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) ∧ 𝑚 ∈ (1...(#‘𝐴))) → (𝑓‘𝑚) ∈ 𝐴) |
32 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓‘𝑚) ∈ 𝐴) → (𝑓‘𝑚) ∈ 𝐴) |
33 | | nfcv 2764 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘(𝑓‘𝑚) |
34 | | nfv 1843 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘𝜑 |
35 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 |
36 | 35 | nfel1 2779 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ |
37 | 34, 36 | nfim 1825 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘(𝜑 → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ) |
38 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑓‘𝑚) → 𝐵 = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
39 | 38 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑓‘𝑚) → (𝐵 ∈ ℂ ↔ ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) |
40 | 39 | imbi2d 330 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑓‘𝑚) → ((𝜑 → 𝐵 ∈ ℂ) ↔ (𝜑 → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ))) |
41 | 12 | expcom 451 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ 𝐴 → (𝜑 → 𝐵 ∈ ℂ)) |
42 | 33, 37, 40, 41 | vtoclgaf 3271 |
. . . . . . . . . . . . 13
⊢ ((𝑓‘𝑚) ∈ 𝐴 → (𝜑 → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) |
43 | 42 | impcom 446 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓‘𝑚) ∈ 𝐴) → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ) |
44 | 13 | fvmpts 6285 |
. . . . . . . . . . . 12
⊢ (((𝑓‘𝑚) ∈ 𝐴 ∧ ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑚)) = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
45 | 32, 43, 44 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓‘𝑚) ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑚)) = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
46 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘0 |
47 | 35, 46 | nfne 2894 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ≠ 0 |
48 | 34, 47 | nfim 1825 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘(𝜑 → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ≠ 0) |
49 | 38 | neeq1d 2853 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑓‘𝑚) → (𝐵 ≠ 0 ↔ ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ≠ 0)) |
50 | 49 | imbi2d 330 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑓‘𝑚) → ((𝜑 → 𝐵 ≠ 0) ↔ (𝜑 → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ≠ 0))) |
51 | | fprodn0.3 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ≠ 0) |
52 | 51 | expcom 451 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝐴 → (𝜑 → 𝐵 ≠ 0)) |
53 | 33, 48, 50, 52 | vtoclgaf 3271 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑚) ∈ 𝐴 → (𝜑 → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ≠ 0)) |
54 | 53 | impcom 446 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓‘𝑚) ∈ 𝐴) → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ≠ 0) |
55 | 45, 54 | eqnetrd 2861 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓‘𝑚) ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑚)) ≠ 0) |
56 | 31, 55 | sylan2 491 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) ∧ 𝑚 ∈ (1...(#‘𝐴)))) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑚)) ≠ 0) |
57 | 56 | anassrs 680 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ (1...(#‘𝐴))) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑚)) ≠ 0) |
58 | 29, 57 | eqnetrd 2861 |
. . . . . . 7
⊢ (((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ (1...(#‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑚) ≠ 0) |
59 | 24, 27, 58 | prodfn0 14626 |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (seq1( · ,
((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓))‘(#‘𝐴)) ≠ 0) |
60 | 22, 59 | eqnetrd 2861 |
. . . . 5
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ∏𝑘 ∈ 𝐴 𝐵 ≠ 0) |
61 | 60 | expr 643 |
. . . 4
⊢ ((𝜑 ∧ (#‘𝐴) ∈ ℕ) → (𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → ∏𝑘 ∈ 𝐴 𝐵 ≠ 0)) |
62 | 61 | exlimdv 1861 |
. . 3
⊢ ((𝜑 ∧ (#‘𝐴) ∈ ℕ) → (∃𝑓 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → ∏𝑘 ∈ 𝐴 𝐵 ≠ 0)) |
63 | 62 | expimpd 629 |
. 2
⊢ (𝜑 → (((#‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) → ∏𝑘 ∈ 𝐴 𝐵 ≠ 0)) |
64 | | fprodn0.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
65 | | fz1f1o 14441 |
. . 3
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨ ((#‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴))) |
66 | 64, 65 | syl 17 |
. 2
⊢ (𝜑 → (𝐴 = ∅ ∨ ((#‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴))) |
67 | 7, 63, 66 | mpjaod 396 |
1
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ≠ 0) |