Step | Hyp | Ref
| Expression |
1 | | 1re 9918 |
. . . 4
⊢ 1 ∈
ℝ |
2 | 1 | rexri 9976 |
. . 3
⊢ 1 ∈
ℝ* |
3 | 2 | a1i 11 |
. 2
⊢ (𝜑 → 1 ∈
ℝ*) |
4 | | pnfxr 9971 |
. . 3
⊢ +∞
∈ ℝ* |
5 | 4 | a1i 11 |
. 2
⊢ (𝜑 → +∞ ∈
ℝ*) |
6 | | fprodge1.ph |
. . 3
⊢
Ⅎ𝑘𝜑 |
7 | | icossre 12125 |
. . . . . 6
⊢ ((1
∈ ℝ ∧ +∞ ∈ ℝ*) → (1[,)+∞)
⊆ ℝ) |
8 | 1, 4, 7 | mp2an 704 |
. . . . 5
⊢
(1[,)+∞) ⊆ ℝ |
9 | | ax-resscn 9872 |
. . . . 5
⊢ ℝ
⊆ ℂ |
10 | 8, 9 | sstri 3577 |
. . . 4
⊢
(1[,)+∞) ⊆ ℂ |
11 | 10 | a1i 11 |
. . 3
⊢ (𝜑 → (1[,)+∞) ⊆
ℂ) |
12 | 2 | a1i 11 |
. . . . 5
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑦 ∈ (1[,)+∞))
→ 1 ∈ ℝ*) |
13 | 4 | a1i 11 |
. . . . 5
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑦 ∈ (1[,)+∞))
→ +∞ ∈ ℝ*) |
14 | 8 | sseli 3564 |
. . . . . . . 8
⊢ (𝑥 ∈ (1[,)+∞) →
𝑥 ∈
ℝ) |
15 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑦 ∈ (1[,)+∞))
→ 𝑥 ∈
ℝ) |
16 | 8 | sseli 3564 |
. . . . . . . 8
⊢ (𝑦 ∈ (1[,)+∞) →
𝑦 ∈
ℝ) |
17 | 16 | adantl 481 |
. . . . . . 7
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑦 ∈ (1[,)+∞))
→ 𝑦 ∈
ℝ) |
18 | 15, 17 | remulcld 9949 |
. . . . . 6
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑦 ∈ (1[,)+∞))
→ (𝑥 · 𝑦) ∈
ℝ) |
19 | 18 | rexrd 9968 |
. . . . 5
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑦 ∈ (1[,)+∞))
→ (𝑥 · 𝑦) ∈
ℝ*) |
20 | | 1t1e1 11052 |
. . . . . . . 8
⊢ (1
· 1) = 1 |
21 | 20 | eqcomi 2619 |
. . . . . . 7
⊢ 1 = (1
· 1) |
22 | 21 | a1i 11 |
. . . . . 6
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑦 ∈ (1[,)+∞))
→ 1 = (1 · 1)) |
23 | 1 | a1i 11 |
. . . . . . 7
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑦 ∈ (1[,)+∞))
→ 1 ∈ ℝ) |
24 | | 0le1 10430 |
. . . . . . . 8
⊢ 0 ≤
1 |
25 | 24 | a1i 11 |
. . . . . . 7
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑦 ∈ (1[,)+∞))
→ 0 ≤ 1) |
26 | 2 | a1i 11 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1[,)+∞) → 1
∈ ℝ*) |
27 | 4 | a1i 11 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1[,)+∞) →
+∞ ∈ ℝ*) |
28 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1[,)+∞) →
𝑥 ∈
(1[,)+∞)) |
29 | | icogelb 12096 |
. . . . . . . . 9
⊢ ((1
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
𝑥 ∈ (1[,)+∞))
→ 1 ≤ 𝑥) |
30 | 26, 27, 28, 29 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝑥 ∈ (1[,)+∞) → 1
≤ 𝑥) |
31 | 30 | adantr 480 |
. . . . . . 7
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑦 ∈ (1[,)+∞))
→ 1 ≤ 𝑥) |
32 | 2 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 ∈ (1[,)+∞) → 1
∈ ℝ*) |
33 | 4 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 ∈ (1[,)+∞) →
+∞ ∈ ℝ*) |
34 | | id 22 |
. . . . . . . . 9
⊢ (𝑦 ∈ (1[,)+∞) →
𝑦 ∈
(1[,)+∞)) |
35 | | icogelb 12096 |
. . . . . . . . 9
⊢ ((1
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
𝑦 ∈ (1[,)+∞))
→ 1 ≤ 𝑦) |
36 | 32, 33, 34, 35 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝑦 ∈ (1[,)+∞) → 1
≤ 𝑦) |
37 | 36 | adantl 481 |
. . . . . . 7
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑦 ∈ (1[,)+∞))
→ 1 ≤ 𝑦) |
38 | 23, 15, 23, 17, 25, 25, 31, 37 | lemul12ad 10845 |
. . . . . 6
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑦 ∈ (1[,)+∞))
→ (1 · 1) ≤ (𝑥 · 𝑦)) |
39 | 22, 38 | eqbrtrd 4605 |
. . . . 5
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑦 ∈ (1[,)+∞))
→ 1 ≤ (𝑥 ·
𝑦)) |
40 | 18 | ltpnfd 11831 |
. . . . 5
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑦 ∈ (1[,)+∞))
→ (𝑥 · 𝑦) <
+∞) |
41 | 12, 13, 19, 39, 40 | elicod 12095 |
. . . 4
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑦 ∈ (1[,)+∞))
→ (𝑥 · 𝑦) ∈
(1[,)+∞)) |
42 | 41 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (1[,)+∞) ∧ 𝑦 ∈ (1[,)+∞))) →
(𝑥 · 𝑦) ∈
(1[,)+∞)) |
43 | | fprodge1.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
44 | 2 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ∈
ℝ*) |
45 | 4 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → +∞ ∈
ℝ*) |
46 | | fprodge1.b |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) |
47 | 46 | rexrd 9968 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈
ℝ*) |
48 | | fprodge1.ge |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ≤ 𝐵) |
49 | 46 | ltpnfd 11831 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 < +∞) |
50 | 44, 45, 47, 48, 49 | elicod 12095 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (1[,)+∞)) |
51 | | 1le1 10534 |
. . . . . 6
⊢ 1 ≤
1 |
52 | | ltpnf 11830 |
. . . . . . 7
⊢ (1 ∈
ℝ → 1 < +∞) |
53 | 1, 52 | ax-mp 5 |
. . . . . 6
⊢ 1 <
+∞ |
54 | 1, 51, 53 | 3pm3.2i 1232 |
. . . . 5
⊢ (1 ∈
ℝ ∧ 1 ≤ 1 ∧ 1 < +∞) |
55 | | elico2 12108 |
. . . . . 6
⊢ ((1
∈ ℝ ∧ +∞ ∈ ℝ*) → (1 ∈
(1[,)+∞) ↔ (1 ∈ ℝ ∧ 1 ≤ 1 ∧ 1 <
+∞))) |
56 | 1, 4, 55 | mp2an 704 |
. . . . 5
⊢ (1 ∈
(1[,)+∞) ↔ (1 ∈ ℝ ∧ 1 ≤ 1 ∧ 1 <
+∞)) |
57 | 54, 56 | mpbir 220 |
. . . 4
⊢ 1 ∈
(1[,)+∞) |
58 | 57 | a1i 11 |
. . 3
⊢ (𝜑 → 1 ∈
(1[,)+∞)) |
59 | 6, 11, 42, 43, 50, 58 | fprodcllemf 14527 |
. 2
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ∈ (1[,)+∞)) |
60 | | icogelb 12096 |
. 2
⊢ ((1
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
∏𝑘 ∈ 𝐴 𝐵 ∈ (1[,)+∞)) → 1 ≤
∏𝑘 ∈ 𝐴 𝐵) |
61 | 3, 5, 59, 60 | syl3anc 1318 |
1
⊢ (𝜑 → 1 ≤ ∏𝑘 ∈ 𝐴 𝐵) |