Step | Hyp | Ref
| Expression |
1 | | prodeq1 11516 |
. . 3
⊢ (𝑤 = ∅ → ∏𝑘 ∈ 𝑤 𝐵 = ∏𝑘 ∈ ∅ 𝐵) |
2 | 1 | breq1d 3999 |
. 2
⊢ (𝑤 = ∅ → (∏𝑘 ∈ 𝑤 𝐵 # 0 ↔ ∏𝑘 ∈ ∅ 𝐵 # 0)) |
3 | | prodeq1 11516 |
. . 3
⊢ (𝑤 = 𝑦 → ∏𝑘 ∈ 𝑤 𝐵 = ∏𝑘 ∈ 𝑦 𝐵) |
4 | 3 | breq1d 3999 |
. 2
⊢ (𝑤 = 𝑦 → (∏𝑘 ∈ 𝑤 𝐵 # 0 ↔ ∏𝑘 ∈ 𝑦 𝐵 # 0)) |
5 | | prodeq1 11516 |
. . 3
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ∏𝑘 ∈ 𝑤 𝐵 = ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵) |
6 | 5 | breq1d 3999 |
. 2
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∏𝑘 ∈ 𝑤 𝐵 # 0 ↔ ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 # 0)) |
7 | | prodeq1 11516 |
. . 3
⊢ (𝑤 = 𝐴 → ∏𝑘 ∈ 𝑤 𝐵 = ∏𝑘 ∈ 𝐴 𝐵) |
8 | 7 | breq1d 3999 |
. 2
⊢ (𝑤 = 𝐴 → (∏𝑘 ∈ 𝑤 𝐵 # 0 ↔ ∏𝑘 ∈ 𝐴 𝐵 # 0)) |
9 | | prod0 11548 |
. . . 4
⊢
∏𝑘 ∈
∅ 𝐵 =
1 |
10 | | 1ap0 8509 |
. . . 4
⊢ 1 #
0 |
11 | 9, 10 | eqbrtri 4010 |
. . 3
⊢
∏𝑘 ∈
∅ 𝐵 #
0 |
12 | 11 | a1i 9 |
. 2
⊢ (𝜑 → ∏𝑘 ∈ ∅ 𝐵 # 0) |
13 | | fprodn0f.kph |
. . . . . . . . 9
⊢
Ⅎ𝑘𝜑 |
14 | | nfv 1521 |
. . . . . . . . 9
⊢
Ⅎ𝑘 𝑦 ∈ Fin |
15 | 13, 14 | nfan 1558 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝜑 ∧ 𝑦 ∈ Fin) |
16 | | nfv 1521 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) |
17 | 15, 16 | nfan 1558 |
. . . . . . 7
⊢
Ⅎ𝑘((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) |
18 | | simplr 525 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑦 ∈ Fin) |
19 | | simplll 528 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝜑) |
20 | | simplrl 530 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝑦 ⊆ 𝐴) |
21 | | simpr 109 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝑦) |
22 | 20, 21 | sseldd 3148 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝐴) |
23 | | fprodn0f.b |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
24 | 19, 22, 23 | syl2anc 409 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝐵 ∈ ℂ) |
25 | 17, 18, 24 | fprodclf 11598 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ∏𝑘 ∈ 𝑦 𝐵 ∈ ℂ) |
26 | 25 | adantr 274 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ∏𝑘 ∈ 𝑦 𝐵 # 0) → ∏𝑘 ∈ 𝑦 𝐵 ∈ ℂ) |
27 | | simprr 527 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∈ (𝐴 ∖ 𝑦)) |
28 | 27 | eldifad 3132 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∈ 𝐴) |
29 | 23 | ex 114 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ 𝐴 → 𝐵 ∈ ℂ)) |
30 | 13, 29 | ralrimi 2541 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
31 | 30 | ad2antrr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
32 | | rspcsbela 3108 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℂ) |
33 | 28, 31, 32 | syl2anc 409 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℂ) |
34 | 33 | adantr 274 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ∏𝑘 ∈ 𝑦 𝐵 # 0) → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℂ) |
35 | | simpr 109 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ∏𝑘 ∈ 𝑦 𝐵 # 0) → ∏𝑘 ∈ 𝑦 𝐵 # 0) |
36 | | fprodap0f.bap0 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 # 0) |
37 | 36 | ex 114 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ 𝐴 → 𝐵 # 0)) |
38 | 13, 37 | ralrimi 2541 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 # 0) |
39 | 38 | ad2antrr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ∀𝑘 ∈ 𝐴 𝐵 # 0) |
40 | | nfcsb1v 3082 |
. . . . . . . . 9
⊢
Ⅎ𝑘⦋𝑧 / 𝑘⦌𝐵 |
41 | | nfcv 2312 |
. . . . . . . . 9
⊢
Ⅎ𝑘
# |
42 | | nfcv 2312 |
. . . . . . . . 9
⊢
Ⅎ𝑘0 |
43 | 40, 41, 42 | nfbr 4035 |
. . . . . . . 8
⊢
Ⅎ𝑘⦋𝑧 / 𝑘⦌𝐵 # 0 |
44 | | csbeq1a 3058 |
. . . . . . . . 9
⊢ (𝑘 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑘⦌𝐵) |
45 | 44 | breq1d 3999 |
. . . . . . . 8
⊢ (𝑘 = 𝑧 → (𝐵 # 0 ↔ ⦋𝑧 / 𝑘⦌𝐵 # 0)) |
46 | 43, 45 | rspc 2828 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 # 0 → ⦋𝑧 / 𝑘⦌𝐵 # 0)) |
47 | 28, 39, 46 | sylc 62 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ⦋𝑧 / 𝑘⦌𝐵 # 0) |
48 | 47 | adantr 274 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ∏𝑘 ∈ 𝑦 𝐵 # 0) → ⦋𝑧 / 𝑘⦌𝐵 # 0) |
49 | 26, 34, 35, 48 | mulap0d 8576 |
. . . 4
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ∏𝑘 ∈ 𝑦 𝐵 # 0) → (∏𝑘 ∈ 𝑦 𝐵 · ⦋𝑧 / 𝑘⦌𝐵) # 0) |
50 | 27 | eldifbd 3133 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ¬ 𝑧 ∈ 𝑦) |
51 | 17, 40, 18, 27, 50, 24, 44, 33 | fprodsplitsn 11596 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 = (∏𝑘 ∈ 𝑦 𝐵 · ⦋𝑧 / 𝑘⦌𝐵)) |
52 | 51 | breq1d 3999 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 # 0 ↔ (∏𝑘 ∈ 𝑦 𝐵 · ⦋𝑧 / 𝑘⦌𝐵) # 0)) |
53 | 52 | adantr 274 |
. . . 4
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ∏𝑘 ∈ 𝑦 𝐵 # 0) → (∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 # 0 ↔ (∏𝑘 ∈ 𝑦 𝐵 · ⦋𝑧 / 𝑘⦌𝐵) # 0)) |
54 | 49, 53 | mpbird 166 |
. . 3
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ∏𝑘 ∈ 𝑦 𝐵 # 0) → ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 # 0) |
55 | 54 | ex 114 |
. 2
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (∏𝑘 ∈ 𝑦 𝐵 # 0 → ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 # 0)) |
56 | | fprodn0f.a |
. 2
⊢ (𝜑 → 𝐴 ∈ Fin) |
57 | 2, 4, 6, 8, 12, 55, 56 | findcard2sd 6870 |
1
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 # 0) |