Proof of Theorem fprodex01
| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑙 ∈ 𝐴 𝐶 = 1) → ∀𝑙 ∈ 𝐴 𝐶 = 1) |
| 2 | | fprodex01.1 |
. . . . . . . 8
⊢ (𝑘 = 𝑙 → 𝐵 = 𝐶) |
| 3 | 2 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑘 = 𝑙 → (𝐵 = 1 ↔ 𝐶 = 1)) |
| 4 | 3 | cbvralvw 3237 |
. . . . . 6
⊢
(∀𝑘 ∈
𝐴 𝐵 = 1 ↔ ∀𝑙 ∈ 𝐴 𝐶 = 1) |
| 5 | 1, 4 | sylibr 234 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑙 ∈ 𝐴 𝐶 = 1) → ∀𝑘 ∈ 𝐴 𝐵 = 1) |
| 6 | 5 | prodeq2d 15957 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑙 ∈ 𝐴 𝐶 = 1) → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 1) |
| 7 | | fprodex01.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ Fin) |
| 8 | | prod1 15980 |
. . . . . . 7
⊢ ((𝐴 ⊆
(ℤ≥‘0) ∨ 𝐴 ∈ Fin) → ∏𝑘 ∈ 𝐴 1 = 1) |
| 9 | 8 | olcs 877 |
. . . . . 6
⊢ (𝐴 ∈ Fin → ∏𝑘 ∈ 𝐴 1 = 1) |
| 10 | 7, 9 | syl 17 |
. . . . 5
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 1 = 1) |
| 11 | 10 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑙 ∈ 𝐴 𝐶 = 1) → ∏𝑘 ∈ 𝐴 1 = 1) |
| 12 | 6, 11 | eqtr2d 2778 |
. . 3
⊢ ((𝜑 ∧ ∀𝑙 ∈ 𝐴 𝐶 = 1) → 1 = ∏𝑘 ∈ 𝐴 𝐵) |
| 13 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑙𝜑 |
| 14 | | nfra1 3284 |
. . . . . . 7
⊢
Ⅎ𝑙∀𝑙 ∈ 𝐴 𝐶 = 1 |
| 15 | 14 | nfn 1857 |
. . . . . 6
⊢
Ⅎ𝑙 ¬
∀𝑙 ∈ 𝐴 𝐶 = 1 |
| 16 | 13, 15 | nfan 1899 |
. . . . 5
⊢
Ⅎ𝑙(𝜑 ∧ ¬ ∀𝑙 ∈ 𝐴 𝐶 = 1) |
| 17 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑙∏𝑘 ∈ 𝐴 𝐵 = 0 |
| 18 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ ∀𝑙 ∈ 𝐴 𝐶 = 1) → 𝐴 ∈ Fin) |
| 19 | 18 | ad2antrr 726 |
. . . . . 6
⊢ ((((𝜑 ∧ ¬ ∀𝑙 ∈ 𝐴 𝐶 = 1) ∧ 𝑙 ∈ 𝐴) ∧ 𝐶 = 0) → 𝐴 ∈ Fin) |
| 20 | | pr01ssre 32826 |
. . . . . . . . . . 11
⊢ {0, 1}
⊆ ℝ |
| 21 | | ax-resscn 11212 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
| 22 | 20, 21 | sstri 3993 |
. . . . . . . . . 10
⊢ {0, 1}
⊆ ℂ |
| 23 | | fprodex01.b |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ {0, 1}) |
| 24 | 22, 23 | sselid 3981 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
| 25 | 24 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ ∀𝑙 ∈ 𝐴 𝐶 = 1) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
| 26 | 25 | adantlr 715 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ ∀𝑙 ∈ 𝐴 𝐶 = 1) ∧ 𝑙 ∈ 𝐴) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
| 27 | 26 | adantlr 715 |
. . . . . 6
⊢
(((((𝜑 ∧ ¬
∀𝑙 ∈ 𝐴 𝐶 = 1) ∧ 𝑙 ∈ 𝐴) ∧ 𝐶 = 0) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
| 28 | | simplr 769 |
. . . . . 6
⊢ ((((𝜑 ∧ ¬ ∀𝑙 ∈ 𝐴 𝐶 = 1) ∧ 𝑙 ∈ 𝐴) ∧ 𝐶 = 0) → 𝑙 ∈ 𝐴) |
| 29 | | simpr 484 |
. . . . . 6
⊢ ((((𝜑 ∧ ¬ ∀𝑙 ∈ 𝐴 𝐶 = 1) ∧ 𝑙 ∈ 𝐴) ∧ 𝐶 = 0) → 𝐶 = 0) |
| 30 | 2, 19, 27, 28, 29 | fprodeq02 32825 |
. . . . 5
⊢ ((((𝜑 ∧ ¬ ∀𝑙 ∈ 𝐴 𝐶 = 1) ∧ 𝑙 ∈ 𝐴) ∧ 𝐶 = 0) → ∏𝑘 ∈ 𝐴 𝐵 = 0) |
| 31 | | rexnal 3100 |
. . . . . . . 8
⊢
(∃𝑙 ∈
𝐴 ¬ 𝐶 = 1 ↔ ¬ ∀𝑙 ∈ 𝐴 𝐶 = 1) |
| 32 | 31 | biimpri 228 |
. . . . . . 7
⊢ (¬
∀𝑙 ∈ 𝐴 𝐶 = 1 → ∃𝑙 ∈ 𝐴 ¬ 𝐶 = 1) |
| 33 | 32 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ ∀𝑙 ∈ 𝐴 𝐶 = 1) → ∃𝑙 ∈ 𝐴 ¬ 𝐶 = 1) |
| 34 | 23 | ralrimiva 3146 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ {0, 1}) |
| 35 | 2 | eleq1d 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑙 → (𝐵 ∈ {0, 1} ↔ 𝐶 ∈ {0, 1})) |
| 36 | 35 | cbvralvw 3237 |
. . . . . . . . . . . . 13
⊢
(∀𝑘 ∈
𝐴 𝐵 ∈ {0, 1} ↔ ∀𝑙 ∈ 𝐴 𝐶 ∈ {0, 1}) |
| 37 | 34, 36 | sylib 218 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑙 ∈ 𝐴 𝐶 ∈ {0, 1}) |
| 38 | 37 | r19.21bi 3251 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑙 ∈ 𝐴) → 𝐶 ∈ {0, 1}) |
| 39 | | c0ex 11255 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
| 40 | | 1ex 11257 |
. . . . . . . . . . . 12
⊢ 1 ∈
V |
| 41 | 39, 40 | elpr2 4652 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ {0, 1} ↔ (𝐶 = 0 ∨ 𝐶 = 1)) |
| 42 | 38, 41 | sylib 218 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑙 ∈ 𝐴) → (𝐶 = 0 ∨ 𝐶 = 1)) |
| 43 | 42 | orcomd 872 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑙 ∈ 𝐴) → (𝐶 = 1 ∨ 𝐶 = 0)) |
| 44 | 43 | ord 865 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑙 ∈ 𝐴) → (¬ 𝐶 = 1 → 𝐶 = 0)) |
| 45 | 44 | reximdva 3168 |
. . . . . . 7
⊢ (𝜑 → (∃𝑙 ∈ 𝐴 ¬ 𝐶 = 1 → ∃𝑙 ∈ 𝐴 𝐶 = 0)) |
| 46 | 45 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ ∀𝑙 ∈ 𝐴 𝐶 = 1) → (∃𝑙 ∈ 𝐴 ¬ 𝐶 = 1 → ∃𝑙 ∈ 𝐴 𝐶 = 0)) |
| 47 | 33, 46 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ ¬ ∀𝑙 ∈ 𝐴 𝐶 = 1) → ∃𝑙 ∈ 𝐴 𝐶 = 0) |
| 48 | 16, 17, 30, 47 | r19.29af2 3267 |
. . . 4
⊢ ((𝜑 ∧ ¬ ∀𝑙 ∈ 𝐴 𝐶 = 1) → ∏𝑘 ∈ 𝐴 𝐵 = 0) |
| 49 | 48 | eqcomd 2743 |
. . 3
⊢ ((𝜑 ∧ ¬ ∀𝑙 ∈ 𝐴 𝐶 = 1) → 0 = ∏𝑘 ∈ 𝐴 𝐵) |
| 50 | 12, 49 | ifeqda 4562 |
. 2
⊢ (𝜑 → if(∀𝑙 ∈ 𝐴 𝐶 = 1, 1, 0) = ∏𝑘 ∈ 𝐴 𝐵) |
| 51 | 50 | eqcomd 2743 |
1
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = if(∀𝑙 ∈ 𝐴 𝐶 = 1, 1, 0)) |