Step | Hyp | Ref
| Expression |
1 | | 1red 9934 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → 1 ∈
ℝ) |
2 | | fprodle.kph |
. . . . . 6
⊢
Ⅎ𝑘𝜑 |
3 | | nfra1 2925 |
. . . . . 6
⊢
Ⅎ𝑘∀𝑘 ∈ 𝐴 𝐵 ≠ 0 |
4 | 2, 3 | nfan 1816 |
. . . . 5
⊢
Ⅎ𝑘(𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) |
5 | | fprodle.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ Fin) |
6 | 5 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → 𝐴 ∈ Fin) |
7 | | fprodle.c |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ) |
8 | 7 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ) |
9 | | fprodle.b |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) |
10 | 9 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) |
11 | | rspa 2914 |
. . . . . . 7
⊢
((∀𝑘 ∈
𝐴 𝐵 ≠ 0 ∧ 𝑘 ∈ 𝐴) → 𝐵 ≠ 0) |
12 | 11 | adantll 746 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 𝐵 ≠ 0) |
13 | 8, 10, 12 | redivcld 10732 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → (𝐶 / 𝐵) ∈ ℝ) |
14 | 4, 6, 13 | fprodreclf 14528 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 (𝐶 / 𝐵) ∈ ℝ) |
15 | 2, 5, 9 | fprodreclf 14528 |
. . . . 5
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ∈ ℝ) |
16 | 15 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 𝐵 ∈ ℝ) |
17 | | fprodle.0l3b |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵) |
18 | 2, 5, 9, 17 | fprodge0 14563 |
. . . . 5
⊢ (𝜑 → 0 ≤ ∏𝑘 ∈ 𝐴 𝐵) |
19 | 18 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → 0 ≤ ∏𝑘 ∈ 𝐴 𝐵) |
20 | | 0red 9920 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 0 ∈ ℝ) |
21 | 17 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵) |
22 | 20, 10, 21, 12 | leneltd 10070 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 0 < 𝐵) |
23 | 10, 22 | elrpd 11745 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈
ℝ+) |
24 | | fprodle.blec |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ≤ 𝐶) |
25 | 24 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 𝐵 ≤ 𝐶) |
26 | | divge1 11774 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ
∧ 𝐵 ≤ 𝐶) → 1 ≤ (𝐶 / 𝐵)) |
27 | 23, 8, 25, 26 | syl3anc 1318 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 1 ≤ (𝐶 / 𝐵)) |
28 | 4, 6, 13, 27 | fprodge1 14565 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → 1 ≤ ∏𝑘 ∈ 𝐴 (𝐶 / 𝐵)) |
29 | 1, 14, 16, 19, 28 | lemul2ad 10843 |
. . 3
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → (∏𝑘 ∈ 𝐴 𝐵 · 1) ≤ (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 (𝐶 / 𝐵))) |
30 | 9 | recnd 9947 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
31 | 2, 5, 30 | fprodclf 14562 |
. . . . . 6
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
32 | 31 | mulid1d 9936 |
. . . . 5
⊢ (𝜑 → (∏𝑘 ∈ 𝐴 𝐵 · 1) = ∏𝑘 ∈ 𝐴 𝐵) |
33 | 32 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → (∏𝑘 ∈ 𝐴 𝐵 · 1) = ∏𝑘 ∈ 𝐴 𝐵) |
34 | 7 | recnd 9947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) |
35 | 34 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) |
36 | 30 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
37 | 4, 6, 35, 36, 12 | fproddivf 14557 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 (𝐶 / 𝐵) = (∏𝑘 ∈ 𝐴 𝐶 / ∏𝑘 ∈ 𝐴 𝐵)) |
38 | 37 | oveq2d 6565 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 (𝐶 / 𝐵)) = (∏𝑘 ∈ 𝐴 𝐵 · (∏𝑘 ∈ 𝐴 𝐶 / ∏𝑘 ∈ 𝐴 𝐵))) |
39 | 2, 5, 34 | fprodclf 14562 |
. . . . . . 7
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 ∈ ℂ) |
40 | 39 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 𝐶 ∈ ℂ) |
41 | 31 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
42 | 4, 6, 36, 12 | fprodn0f 14561 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 𝐵 ≠ 0) |
43 | 40, 41, 42 | divcan2d 10682 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → (∏𝑘 ∈ 𝐴 𝐵 · (∏𝑘 ∈ 𝐴 𝐶 / ∏𝑘 ∈ 𝐴 𝐵)) = ∏𝑘 ∈ 𝐴 𝐶) |
44 | | eqidd 2611 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐴 𝐶) |
45 | 38, 43, 44 | 3eqtrd 2648 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 (𝐶 / 𝐵)) = ∏𝑘 ∈ 𝐴 𝐶) |
46 | 33, 45 | breq12d 4596 |
. . 3
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ((∏𝑘 ∈ 𝐴 𝐵 · 1) ≤ (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 (𝐶 / 𝐵)) ↔ ∏𝑘 ∈ 𝐴 𝐵 ≤ ∏𝑘 ∈ 𝐴 𝐶)) |
47 | 29, 46 | mpbid 221 |
. 2
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 𝐵 ≤ ∏𝑘 ∈ 𝐴 𝐶) |
48 | | simpl 472 |
. . 3
⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → 𝜑) |
49 | | nne 2786 |
. . . . . . 7
⊢ (¬
𝐵 ≠ 0 ↔ 𝐵 = 0) |
50 | 49 | rexbii 3023 |
. . . . . 6
⊢
(∃𝑘 ∈
𝐴 ¬ 𝐵 ≠ 0 ↔ ∃𝑘 ∈ 𝐴 𝐵 = 0) |
51 | | rexnal 2978 |
. . . . . 6
⊢
(∃𝑘 ∈
𝐴 ¬ 𝐵 ≠ 0 ↔ ¬ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) |
52 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑗 𝐵 = 0 |
53 | | nfcsb1v 3515 |
. . . . . . . 8
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 |
54 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑘0 |
55 | 53, 54 | nfeq 2762 |
. . . . . . 7
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 = 0 |
56 | | csbeq1a 3508 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑘⦌𝐵) |
57 | 56 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → (𝐵 = 0 ↔ ⦋𝑗 / 𝑘⦌𝐵 = 0)) |
58 | 52, 55, 57 | cbvrex 3144 |
. . . . . 6
⊢
(∃𝑘 ∈
𝐴 𝐵 = 0 ↔ ∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0) |
59 | 50, 51, 58 | 3bitr3i 289 |
. . . . 5
⊢ (¬
∀𝑘 ∈ 𝐴 𝐵 ≠ 0 ↔ ∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0) |
60 | 59 | biimpi 205 |
. . . 4
⊢ (¬
∀𝑘 ∈ 𝐴 𝐵 ≠ 0 → ∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0) |
61 | 60 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0) |
62 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑗𝜑 |
63 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑗∏𝑘 ∈ 𝐴 𝐵 = 0 |
64 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑘 𝑗 ∈ 𝐴 |
65 | 2, 64, 55 | nf3an 1819 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋𝑗 / 𝑘⦌𝐵 = 0) |
66 | 5 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋𝑗 / 𝑘⦌𝐵 = 0) → 𝐴 ∈ Fin) |
67 | 30 | 3ad2antl1 1216 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋𝑗 / 𝑘⦌𝐵 = 0) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
68 | | simp2 1055 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋𝑗 / 𝑘⦌𝐵 = 0) → 𝑗 ∈ 𝐴) |
69 | 57 | biimparc 503 |
. . . . . . . . 9
⊢
((⦋𝑗 /
𝑘⦌𝐵 = 0 ∧ 𝑘 = 𝑗) → 𝐵 = 0) |
70 | 69 | 3ad2antl3 1218 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋𝑗 / 𝑘⦌𝐵 = 0) ∧ 𝑘 = 𝑗) → 𝐵 = 0) |
71 | 65, 66, 67, 68, 70 | fprodeq0g 14564 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋𝑗 / 𝑘⦌𝐵 = 0) → ∏𝑘 ∈ 𝐴 𝐵 = 0) |
72 | 71 | 3exp 1256 |
. . . . . 6
⊢ (𝜑 → (𝑗 ∈ 𝐴 → (⦋𝑗 / 𝑘⦌𝐵 = 0 → ∏𝑘 ∈ 𝐴 𝐵 = 0))) |
73 | 62, 63, 72 | rexlimd 3008 |
. . . . 5
⊢ (𝜑 → (∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0 → ∏𝑘 ∈ 𝐴 𝐵 = 0)) |
74 | 73 | imp 444 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0) → ∏𝑘 ∈ 𝐴 𝐵 = 0) |
75 | | 0red 9920 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ∈ ℝ) |
76 | 75, 9, 7, 17, 24 | letrd 10073 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐶) |
77 | 2, 5, 7, 76 | fprodge0 14563 |
. . . . 5
⊢ (𝜑 → 0 ≤ ∏𝑘 ∈ 𝐴 𝐶) |
78 | 77 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0) → 0 ≤ ∏𝑘 ∈ 𝐴 𝐶) |
79 | 74, 78 | eqbrtrd 4605 |
. . 3
⊢ ((𝜑 ∧ ∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0) → ∏𝑘 ∈ 𝐴 𝐵 ≤ ∏𝑘 ∈ 𝐴 𝐶) |
80 | 48, 61, 79 | syl2anc 691 |
. 2
⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 𝐵 ≤ ∏𝑘 ∈ 𝐴 𝐶) |
81 | 47, 80 | pm2.61dan 828 |
1
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ≤ ∏𝑘 ∈ 𝐴 𝐶) |