Step | Hyp | Ref
| Expression |
1 | | 1red 10055 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → 1 ∈
ℝ) |
2 | | fprodle.kph |
. . . . . 6
⊢
Ⅎ𝑘𝜑 |
3 | | nfra1 2941 |
. . . . . 6
⊢
Ⅎ𝑘∀𝑘 ∈ 𝐴 𝐵 ≠ 0 |
4 | 2, 3 | nfan 1828 |
. . . . 5
⊢
Ⅎ𝑘(𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) |
5 | | fprodle.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ Fin) |
6 | 5 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → 𝐴 ∈ Fin) |
7 | | fprodle.c |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ) |
8 | 7 | adantlr 751 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ) |
9 | | fprodle.b |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) |
10 | 9 | adantlr 751 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) |
11 | | rspa 2930 |
. . . . . . 7
⊢
((∀𝑘 ∈
𝐴 𝐵 ≠ 0 ∧ 𝑘 ∈ 𝐴) → 𝐵 ≠ 0) |
12 | 11 | adantll 750 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 𝐵 ≠ 0) |
13 | 8, 10, 12 | redivcld 10853 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → (𝐶 / 𝐵) ∈ ℝ) |
14 | 4, 6, 13 | fprodreclf 14689 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 (𝐶 / 𝐵) ∈ ℝ) |
15 | 2, 5, 9 | fprodreclf 14689 |
. . . . 5
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ∈ ℝ) |
16 | 15 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 𝐵 ∈ ℝ) |
17 | | fprodle.0l3b |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵) |
18 | 2, 5, 9, 17 | fprodge0 14724 |
. . . . 5
⊢ (𝜑 → 0 ≤ ∏𝑘 ∈ 𝐴 𝐵) |
19 | 18 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → 0 ≤ ∏𝑘 ∈ 𝐴 𝐵) |
20 | | 0red 10041 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 0 ∈ ℝ) |
21 | 17 | adantlr 751 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵) |
22 | 20, 10, 21, 12 | leneltd 10191 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 0 < 𝐵) |
23 | 10, 22 | elrpd 11869 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈
ℝ+) |
24 | | fprodle.blec |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ≤ 𝐶) |
25 | 24 | adantlr 751 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 𝐵 ≤ 𝐶) |
26 | | divge1 11898 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ
∧ 𝐵 ≤ 𝐶) → 1 ≤ (𝐶 / 𝐵)) |
27 | 23, 8, 25, 26 | syl3anc 1326 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 1 ≤ (𝐶 / 𝐵)) |
28 | 4, 6, 13, 27 | fprodge1 14726 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → 1 ≤ ∏𝑘 ∈ 𝐴 (𝐶 / 𝐵)) |
29 | 1, 14, 16, 19, 28 | lemul2ad 10964 |
. . 3
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → (∏𝑘 ∈ 𝐴 𝐵 · 1) ≤ (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 (𝐶 / 𝐵))) |
30 | 9 | recnd 10068 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
31 | 2, 5, 30 | fprodclf 14723 |
. . . . . 6
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
32 | 31 | mulid1d 10057 |
. . . . 5
⊢ (𝜑 → (∏𝑘 ∈ 𝐴 𝐵 · 1) = ∏𝑘 ∈ 𝐴 𝐵) |
33 | 32 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → (∏𝑘 ∈ 𝐴 𝐵 · 1) = ∏𝑘 ∈ 𝐴 𝐵) |
34 | 7 | recnd 10068 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) |
35 | 34 | adantlr 751 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) |
36 | 30 | adantlr 751 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
37 | 4, 6, 35, 36, 12 | fproddivf 14718 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 (𝐶 / 𝐵) = (∏𝑘 ∈ 𝐴 𝐶 / ∏𝑘 ∈ 𝐴 𝐵)) |
38 | 37 | oveq2d 6666 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 (𝐶 / 𝐵)) = (∏𝑘 ∈ 𝐴 𝐵 · (∏𝑘 ∈ 𝐴 𝐶 / ∏𝑘 ∈ 𝐴 𝐵))) |
39 | 2, 5, 34 | fprodclf 14723 |
. . . . . . 7
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 ∈ ℂ) |
40 | 39 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 𝐶 ∈ ℂ) |
41 | 31 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
42 | 4, 6, 36, 12 | fprodn0f 14722 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 𝐵 ≠ 0) |
43 | 40, 41, 42 | divcan2d 10803 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → (∏𝑘 ∈ 𝐴 𝐵 · (∏𝑘 ∈ 𝐴 𝐶 / ∏𝑘 ∈ 𝐴 𝐵)) = ∏𝑘 ∈ 𝐴 𝐶) |
44 | | eqidd 2623 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐴 𝐶) |
45 | 38, 43, 44 | 3eqtrd 2660 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 (𝐶 / 𝐵)) = ∏𝑘 ∈ 𝐴 𝐶) |
46 | 33, 45 | breq12d 4666 |
. . 3
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ((∏𝑘 ∈ 𝐴 𝐵 · 1) ≤ (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 (𝐶 / 𝐵)) ↔ ∏𝑘 ∈ 𝐴 𝐵 ≤ ∏𝑘 ∈ 𝐴 𝐶)) |
47 | 29, 46 | mpbid 222 |
. 2
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 𝐵 ≤ ∏𝑘 ∈ 𝐴 𝐶) |
48 | | simpl 473 |
. . 3
⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → 𝜑) |
49 | | nne 2798 |
. . . . . . 7
⊢ (¬
𝐵 ≠ 0 ↔ 𝐵 = 0) |
50 | 49 | rexbii 3041 |
. . . . . 6
⊢
(∃𝑘 ∈
𝐴 ¬ 𝐵 ≠ 0 ↔ ∃𝑘 ∈ 𝐴 𝐵 = 0) |
51 | | rexnal 2995 |
. . . . . 6
⊢
(∃𝑘 ∈
𝐴 ¬ 𝐵 ≠ 0 ↔ ¬ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) |
52 | | nfv 1843 |
. . . . . . 7
⊢
Ⅎ𝑗 𝐵 = 0 |
53 | | nfcsb1v 3549 |
. . . . . . . 8
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 |
54 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑘0 |
55 | 53, 54 | nfeq 2776 |
. . . . . . 7
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 = 0 |
56 | | csbeq1a 3542 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑘⦌𝐵) |
57 | 56 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → (𝐵 = 0 ↔ ⦋𝑗 / 𝑘⦌𝐵 = 0)) |
58 | 52, 55, 57 | cbvrex 3168 |
. . . . . 6
⊢
(∃𝑘 ∈
𝐴 𝐵 = 0 ↔ ∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0) |
59 | 50, 51, 58 | 3bitr3i 290 |
. . . . 5
⊢ (¬
∀𝑘 ∈ 𝐴 𝐵 ≠ 0 ↔ ∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0) |
60 | 59 | biimpi 206 |
. . . 4
⊢ (¬
∀𝑘 ∈ 𝐴 𝐵 ≠ 0 → ∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0) |
61 | 60 | adantl 482 |
. . 3
⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0) |
62 | | nfv 1843 |
. . . . . 6
⊢
Ⅎ𝑗𝜑 |
63 | | nfv 1843 |
. . . . . 6
⊢
Ⅎ𝑗∏𝑘 ∈ 𝐴 𝐵 = 0 |
64 | | nfv 1843 |
. . . . . . . . 9
⊢
Ⅎ𝑘 𝑗 ∈ 𝐴 |
65 | 2, 64, 55 | nf3an 1831 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋𝑗 / 𝑘⦌𝐵 = 0) |
66 | 5 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋𝑗 / 𝑘⦌𝐵 = 0) → 𝐴 ∈ Fin) |
67 | 30 | 3ad2antl1 1223 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋𝑗 / 𝑘⦌𝐵 = 0) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
68 | | simp2 1062 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋𝑗 / 𝑘⦌𝐵 = 0) → 𝑗 ∈ 𝐴) |
69 | 57 | biimparc 504 |
. . . . . . . . 9
⊢
((⦋𝑗 /
𝑘⦌𝐵 = 0 ∧ 𝑘 = 𝑗) → 𝐵 = 0) |
70 | 69 | 3ad2antl3 1225 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋𝑗 / 𝑘⦌𝐵 = 0) ∧ 𝑘 = 𝑗) → 𝐵 = 0) |
71 | 65, 66, 67, 68, 70 | fprodeq0g 14725 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋𝑗 / 𝑘⦌𝐵 = 0) → ∏𝑘 ∈ 𝐴 𝐵 = 0) |
72 | 71 | 3exp 1264 |
. . . . . 6
⊢ (𝜑 → (𝑗 ∈ 𝐴 → (⦋𝑗 / 𝑘⦌𝐵 = 0 → ∏𝑘 ∈ 𝐴 𝐵 = 0))) |
73 | 62, 63, 72 | rexlimd 3026 |
. . . . 5
⊢ (𝜑 → (∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0 → ∏𝑘 ∈ 𝐴 𝐵 = 0)) |
74 | 73 | imp 445 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0) → ∏𝑘 ∈ 𝐴 𝐵 = 0) |
75 | | 0red 10041 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ∈ ℝ) |
76 | 75, 9, 7, 17, 24 | letrd 10194 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐶) |
77 | 2, 5, 7, 76 | fprodge0 14724 |
. . . . 5
⊢ (𝜑 → 0 ≤ ∏𝑘 ∈ 𝐴 𝐶) |
78 | 77 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0) → 0 ≤ ∏𝑘 ∈ 𝐴 𝐶) |
79 | 74, 78 | eqbrtrd 4675 |
. . 3
⊢ ((𝜑 ∧ ∃𝑗 ∈ 𝐴 ⦋𝑗 / 𝑘⦌𝐵 = 0) → ∏𝑘 ∈ 𝐴 𝐵 ≤ ∏𝑘 ∈ 𝐴 𝐶) |
80 | 48, 61, 79 | syl2anc 693 |
. 2
⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝐴 𝐵 ≠ 0) → ∏𝑘 ∈ 𝐴 𝐵 ≤ ∏𝑘 ∈ 𝐴 𝐶) |
81 | 47, 80 | pm2.61dan 832 |
1
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ≤ ∏𝑘 ∈ 𝐴 𝐶) |