| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1red 11262 | . . . 4
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → 1 ∈
ℝ) | 
| 2 |  | fprodle.kph | . . . . . 6
⊢
Ⅎ𝑘𝜑 | 
| 3 |  | nfra1 3284 | . . . . . 6
⊢
Ⅎ𝑘∀𝑘 ∈ 𝐴 𝐵 ≠ 0 | 
| 4 | 2, 3 | nfan 1899 | . . . . 5
⊢
Ⅎ𝑘(𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) | 
| 5 |  | fprodle.a | . . . . . 6
⊢ (𝜑 → 𝐴 ∈ Fin) | 
| 6 | 5 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → 𝐴 ∈ Fin) | 
| 7 |  | fprodle.c | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ) | 
| 8 | 7 | adantlr 715 | . . . . . 6
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ) | 
| 9 |  | fprodle.b | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) | 
| 10 | 9 | adantlr 715 | . . . . . 6
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) | 
| 11 |  | rspa 3248 | . . . . . . 7
⊢
((∀𝑘 ∈
𝐴 𝐵 ≠ 0 ∧ 𝑘 ∈ 𝐴) → 𝐵 ≠ 0) | 
| 12 | 11 | adantll 714 | . . . . . 6
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 𝐵 ≠ 0) | 
| 13 | 8, 10, 12 | redivcld 12095 | . . . . 5
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → (𝐶 / 𝐵) ∈ ℝ) | 
| 14 | 4, 6, 13 | fprodreclf 15995 | . . . 4
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 (𝐶 / 𝐵) ∈ ℝ) | 
| 15 | 2, 5, 9 | fprodreclf 15995 | . . . . 5
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ∈ ℝ) | 
| 16 | 15 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 𝐵 ∈ ℝ) | 
| 17 |  | fprodle.0l3b | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵) | 
| 18 | 2, 5, 9, 17 | fprodge0 16029 | . . . . 5
⊢ (𝜑 → 0 ≤ ∏𝑘 ∈ 𝐴 𝐵) | 
| 19 | 18 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → 0 ≤ ∏𝑘 ∈ 𝐴 𝐵) | 
| 20 | 17 | adantlr 715 | . . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵) | 
| 21 | 10, 20, 12 | ne0gt0d 11398 | . . . . . . 7
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 0 < 𝐵) | 
| 22 | 10, 21 | elrpd 13074 | . . . . . 6
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈
ℝ+) | 
| 23 |  | fprodle.blec | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ≤ 𝐶) | 
| 24 | 23 | adantlr 715 | . . . . . 6
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 𝐵 ≤ 𝐶) | 
| 25 |  | divge1 13103 | . . . . . 6
⊢ ((𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ
∧ 𝐵 ≤ 𝐶) → 1 ≤ (𝐶 / 𝐵)) | 
| 26 | 22, 8, 24, 25 | syl3anc 1373 | . . . . 5
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 1 ≤ (𝐶 / 𝐵)) | 
| 27 | 4, 6, 13, 26 | fprodge1 16031 | . . . 4
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → 1 ≤ ∏𝑘 ∈ 𝐴 (𝐶 / 𝐵)) | 
| 28 | 1, 14, 16, 19, 27 | lemul2ad 12208 | . . 3
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → (∏𝑘 ∈ 𝐴 𝐵 · 1) ≤ (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 (𝐶 / 𝐵))) | 
| 29 | 9 | recnd 11289 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) | 
| 30 | 2, 5, 29 | fprodclf 16028 | . . . . 5
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ∈ ℂ) | 
| 31 | 30 | mulridd 11278 | . . . 4
⊢ (𝜑 → (∏𝑘 ∈ 𝐴 𝐵 · 1) = ∏𝑘 ∈ 𝐴 𝐵) | 
| 32 | 31 | adantr 480 | . . 3
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → (∏𝑘 ∈ 𝐴 𝐵 · 1) = ∏𝑘 ∈ 𝐴 𝐵) | 
| 33 | 7 | recnd 11289 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) | 
| 34 | 33 | adantlr 715 | . . . . . 6
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) | 
| 35 | 29 | adantlr 715 | . . . . . 6
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) | 
| 36 | 4, 6, 34, 35, 12 | fproddivf 16023 | . . . . 5
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 (𝐶 / 𝐵) = (∏𝑘 ∈ 𝐴 𝐶 / ∏𝑘 ∈ 𝐴 𝐵)) | 
| 37 | 36 | oveq2d 7447 | . . . 4
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 (𝐶 / 𝐵)) = (∏𝑘 ∈ 𝐴 𝐵 · (∏𝑘 ∈ 𝐴 𝐶 / ∏𝑘 ∈ 𝐴 𝐵))) | 
| 38 | 2, 5, 33 | fprodclf 16028 | . . . . . 6
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 ∈ ℂ) | 
| 39 | 38 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 𝐶 ∈ ℂ) | 
| 40 | 30 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 𝐵 ∈ ℂ) | 
| 41 | 4, 6, 35, 12 | fprodn0f 16027 | . . . . 5
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 𝐵 ≠ 0) | 
| 42 | 39, 40, 41 | divcan2d 12045 | . . . 4
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → (∏𝑘 ∈ 𝐴 𝐵 · (∏𝑘 ∈ 𝐴 𝐶 / ∏𝑘 ∈ 𝐴 𝐵)) = ∏𝑘 ∈ 𝐴 𝐶) | 
| 43 | 37, 42 | eqtrd 2777 | . . 3
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 (𝐶 / 𝐵)) = ∏𝑘 ∈ 𝐴 𝐶) | 
| 44 | 28, 32, 43 | 3brtr3d 5174 | . 2
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 𝐵 ≤ ∏𝑘 ∈ 𝐴 𝐶) | 
| 45 |  | nne 2944 | . . . . 5
⊢ (¬
𝐵 ≠ 0 ↔ 𝐵 = 0) | 
| 46 | 45 | rexbii 3094 | . . . 4
⊢
(∃𝑘 ∈
𝐴 ¬ 𝐵 ≠ 0 ↔ ∃𝑘 ∈ 𝐴 𝐵 = 0) | 
| 47 |  | rexnal 3100 | . . . 4
⊢
(∃𝑘 ∈
𝐴 ¬ 𝐵 ≠ 0 ↔ ¬ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) | 
| 48 |  | nfv 1914 | . . . . 5
⊢
Ⅎ𝑗 𝐵 = 0 | 
| 49 |  | nfcsb1v 3923 | . . . . . 6
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 | 
| 50 | 49 | nfeq1 2921 | . . . . 5
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 = 0 | 
| 51 |  | csbeq1a 3913 | . . . . . 6
⊢ (𝑘 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑘⦌𝐵) | 
| 52 | 51 | eqeq1d 2739 | . . . . 5
⊢ (𝑘 = 𝑗 → (𝐵 = 0 ↔ ⦋𝑗 / 𝑘⦌𝐵 = 0)) | 
| 53 | 48, 50, 52 | cbvrexw 3307 | . . . 4
⊢
(∃𝑘 ∈
𝐴 𝐵 = 0 ↔ ∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0) | 
| 54 | 46, 47, 53 | 3bitr3i 301 | . . 3
⊢ (¬
∀𝑘 ∈ 𝐴 𝐵 ≠ 0 ↔ ∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0) | 
| 55 |  | nfv 1914 | . . . . . . . 8
⊢
Ⅎ𝑘 𝑗 ∈ 𝐴 | 
| 56 | 2, 55, 50 | nf3an 1901 | . . . . . . 7
⊢
Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋𝑗 / 𝑘⦌𝐵 = 0) | 
| 57 | 5 | 3ad2ant1 1134 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋𝑗 / 𝑘⦌𝐵 = 0) → 𝐴 ∈ Fin) | 
| 58 | 29 | 3ad2antl1 1186 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋𝑗 / 𝑘⦌𝐵 = 0) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) | 
| 59 |  | simp2 1138 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋𝑗 / 𝑘⦌𝐵 = 0) → 𝑗 ∈ 𝐴) | 
| 60 | 52 | biimparc 479 | . . . . . . . 8
⊢
((⦋𝑗 /
𝑘⦌𝐵 = 0 ∧ 𝑘 = 𝑗) → 𝐵 = 0) | 
| 61 | 60 | 3ad2antl3 1188 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋𝑗 / 𝑘⦌𝐵 = 0) ∧ 𝑘 = 𝑗) → 𝐵 = 0) | 
| 62 | 56, 57, 58, 59, 61 | fprodeq0g 16030 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋𝑗 / 𝑘⦌𝐵 = 0) → ∏𝑘 ∈ 𝐴 𝐵 = 0) | 
| 63 | 62 | rexlimdv3a 3159 | . . . . 5
⊢ (𝜑 → (∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0 → ∏𝑘 ∈ 𝐴 𝐵 = 0)) | 
| 64 | 63 | imp 406 | . . . 4
⊢ ((𝜑 ∧ ∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0) → ∏𝑘 ∈ 𝐴 𝐵 = 0) | 
| 65 |  | 0red 11264 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ∈ ℝ) | 
| 66 | 65, 9, 7, 17, 23 | letrd 11418 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐶) | 
| 67 | 2, 5, 7, 66 | fprodge0 16029 | . . . . 5
⊢ (𝜑 → 0 ≤ ∏𝑘 ∈ 𝐴 𝐶) | 
| 68 | 67 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ ∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0) → 0 ≤ ∏𝑘 ∈ 𝐴 𝐶) | 
| 69 | 64, 68 | eqbrtrd 5165 | . . 3
⊢ ((𝜑 ∧ ∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0) → ∏𝑘 ∈ 𝐴 𝐵 ≤ ∏𝑘 ∈ 𝐴 𝐶) | 
| 70 | 54, 69 | sylan2b 594 | . 2
⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 𝐵 ≤ ∏𝑘 ∈ 𝐴 𝐶) | 
| 71 | 44, 70 | pm2.61dan 813 | 1
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ≤ ∏𝑘 ∈ 𝐴 𝐶) |