| Step | Hyp | Ref
| Expression |
| 1 | | sge0le.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
| 2 | | sge0le.F |
. . . . . 6
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) |
| 3 | 1, 2 | sge0xrcl 46400 |
. . . . 5
⊢ (𝜑 →
(Σ^‘𝐹) ∈
ℝ*) |
| 4 | | pnfge 13172 |
. . . . 5
⊢
((Σ^‘𝐹) ∈ ℝ* →
(Σ^‘𝐹) ≤ +∞) |
| 5 | 3, 4 | syl 17 |
. . . 4
⊢ (𝜑 →
(Σ^‘𝐹) ≤ +∞) |
| 6 | 5 | adantr 480 |
. . 3
⊢ ((𝜑 ∧
(Σ^‘𝐺) = +∞) →
(Σ^‘𝐹) ≤ +∞) |
| 7 | | id 22 |
. . . . 5
⊢
((Σ^‘𝐺) = +∞ →
(Σ^‘𝐺) = +∞) |
| 8 | 7 | eqcomd 2743 |
. . . 4
⊢
((Σ^‘𝐺) = +∞ → +∞ =
(Σ^‘𝐺)) |
| 9 | 8 | adantl 481 |
. . 3
⊢ ((𝜑 ∧
(Σ^‘𝐺) = +∞) → +∞ =
(Σ^‘𝐺)) |
| 10 | 6, 9 | breqtrd 5169 |
. 2
⊢ ((𝜑 ∧
(Σ^‘𝐺) = +∞) →
(Σ^‘𝐹) ≤
(Σ^‘𝐺)) |
| 11 | | elinel2 4202 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝒫 𝑋 ∩ Fin) → 𝑦 ∈ Fin) |
| 12 | 11 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑦 ∈ Fin) |
| 13 | 2 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) → 𝐹:𝑋⟶(0[,]+∞)) |
| 14 | 1 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝑋 ∈ 𝑉) |
| 15 | | sge0le.g |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:𝑋⟶(0[,]+∞)) |
| 16 | 15 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝐺:𝑋⟶(0[,]+∞)) |
| 17 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → +∞ ∈ ran
𝐹) |
| 18 | 2 | ffnd 6737 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 Fn 𝑋) |
| 19 | | fvelrnb 6969 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 Fn 𝑋 → (+∞ ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = +∞)) |
| 20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (+∞ ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = +∞)) |
| 21 | 20 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → (+∞ ∈ ran
𝐹 ↔ ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = +∞)) |
| 22 | 17, 21 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = +∞) |
| 23 | | iccssxr 13470 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(0[,]+∞) ⊆ ℝ* |
| 24 | 15 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺‘𝑥) ∈ (0[,]+∞)) |
| 25 | 23, 24 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺‘𝑥) ∈
ℝ*) |
| 26 | 25 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = +∞) → (𝐺‘𝑥) ∈
ℝ*) |
| 27 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹‘𝑥) = +∞ → (𝐹‘𝑥) = +∞) |
| 28 | 27 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘𝑥) = +∞ → +∞ = (𝐹‘𝑥)) |
| 29 | 28 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = +∞) → +∞ = (𝐹‘𝑥)) |
| 30 | | sge0le.le |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ≤ (𝐺‘𝑥)) |
| 31 | 30 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = +∞) → (𝐹‘𝑥) ≤ (𝐺‘𝑥)) |
| 32 | 29, 31 | eqbrtrd 5165 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = +∞) → +∞ ≤ (𝐺‘𝑥)) |
| 33 | 26, 32 | xrgepnfd 45342 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = +∞) → (𝐺‘𝑥) = +∞) |
| 34 | 33 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = +∞) → +∞ = (𝐺‘𝑥)) |
| 35 | 15 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐺 Fn 𝑋) |
| 36 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐺 Fn 𝑋) |
| 37 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
| 38 | | fnfvelrn 7100 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 Fn 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝐺‘𝑥) ∈ ran 𝐺) |
| 39 | 36, 37, 38 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺‘𝑥) ∈ ran 𝐺) |
| 40 | 39 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = +∞) → (𝐺‘𝑥) ∈ ran 𝐺) |
| 41 | 34, 40 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = +∞) → +∞ ∈ ran
𝐺) |
| 42 | 41 | ex 412 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥) = +∞ → +∞ ∈ ran 𝐺)) |
| 43 | 42 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥) = +∞ → +∞ ∈ ran 𝐺)) |
| 44 | 43 | rexlimdva 3155 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → (∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = +∞ → +∞ ∈ ran 𝐺)) |
| 45 | 22, 44 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → +∞ ∈ ran
𝐺) |
| 46 | 14, 16, 45 | sge0pnfval 46388 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) →
(Σ^‘𝐺) = +∞) |
| 47 | 46 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ +∞ ∈ ran
𝐹) →
(Σ^‘𝐺) = +∞) |
| 48 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ +∞ ∈ ran
𝐹) → ¬
(Σ^‘𝐺) = +∞) |
| 49 | 47, 48 | pm2.65da 817 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) → ¬ +∞ ∈
ran 𝐹) |
| 50 | 13, 49 | fge0iccico 46385 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) → 𝐹:𝑋⟶(0[,)+∞)) |
| 51 | 50 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) → 𝐹:𝑋⟶(0[,)+∞)) |
| 52 | | elpwinss 45054 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝒫 𝑋 ∩ Fin) → 𝑦 ⊆ 𝑋) |
| 53 | 52 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑦 ⊆ 𝑋) |
| 54 | 51, 53 | fssresd 6775 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑦):𝑦⟶(0[,)+∞)) |
| 55 | 12, 54 | sge0fsum 46402 |
. . . . . 6
⊢ (((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝑦)) = Σ𝑥 ∈ 𝑦 ((𝐹 ↾ 𝑦)‘𝑥)) |
| 56 | | rge0ssre 13496 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ ℝ |
| 57 | 54 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → ((𝐹 ↾ 𝑦)‘𝑥) ∈ (0[,)+∞)) |
| 58 | 56, 57 | sselid 3981 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → ((𝐹 ↾ 𝑦)‘𝑥) ∈ ℝ) |
| 59 | 12, 58 | fsumrecl 15770 |
. . . . . 6
⊢ (((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑥 ∈ 𝑦 ((𝐹 ↾ 𝑦)‘𝑥) ∈ ℝ) |
| 60 | 55, 59 | eqeltrd 2841 |
. . . . 5
⊢ (((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝑦)) ∈ ℝ) |
| 61 | 15 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) → 𝐺:𝑋⟶(0[,]+∞)) |
| 62 | 1 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) → 𝑋 ∈ 𝑉) |
| 63 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) → ¬
(Σ^‘𝐺) = +∞) |
| 64 | 62, 61 | sge0repnf 46401 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) →
((Σ^‘𝐺) ∈ ℝ ↔ ¬
(Σ^‘𝐺) = +∞)) |
| 65 | 63, 64 | mpbird 257 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) →
(Σ^‘𝐺) ∈ ℝ) |
| 66 | 62, 61, 65 | sge0rern 46403 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) → ¬ +∞ ∈
ran 𝐺) |
| 67 | 61, 66 | fge0iccico 46385 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) → 𝐺:𝑋⟶(0[,)+∞)) |
| 68 | 67 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) → 𝐺:𝑋⟶(0[,)+∞)) |
| 69 | 68, 53 | fssresd 6775 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐺 ↾ 𝑦):𝑦⟶(0[,)+∞)) |
| 70 | 12, 69 | sge0fsum 46402 |
. . . . . 6
⊢ (((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐺 ↾ 𝑦)) = Σ𝑥 ∈ 𝑦 ((𝐺 ↾ 𝑦)‘𝑥)) |
| 71 | 69 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → ((𝐺 ↾ 𝑦)‘𝑥) ∈ (0[,)+∞)) |
| 72 | 56, 71 | sselid 3981 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → ((𝐺 ↾ 𝑦)‘𝑥) ∈ ℝ) |
| 73 | 12, 72 | fsumrecl 15770 |
. . . . . 6
⊢ (((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑥 ∈ 𝑦 ((𝐺 ↾ 𝑦)‘𝑥) ∈ ℝ) |
| 74 | 70, 73 | eqeltrd 2841 |
. . . . 5
⊢ (((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐺 ↾ 𝑦)) ∈ ℝ) |
| 75 | 65 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘𝐺) ∈ ℝ) |
| 76 | | simplll 775 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 𝜑) |
| 77 | 53 | sselda 3983 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝑋) |
| 78 | 76, 77, 30 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (𝐹‘𝑥) ≤ (𝐺‘𝑥)) |
| 79 | | fvres 6925 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑦 → ((𝐹 ↾ 𝑦)‘𝑥) = (𝐹‘𝑥)) |
| 80 | 79 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → ((𝐹 ↾ 𝑦)‘𝑥) = (𝐹‘𝑥)) |
| 81 | | fvres 6925 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑦 → ((𝐺 ↾ 𝑦)‘𝑥) = (𝐺‘𝑥)) |
| 82 | 81 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → ((𝐺 ↾ 𝑦)‘𝑥) = (𝐺‘𝑥)) |
| 83 | 80, 82 | breq12d 5156 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (((𝐹 ↾ 𝑦)‘𝑥) ≤ ((𝐺 ↾ 𝑦)‘𝑥) ↔ (𝐹‘𝑥) ≤ (𝐺‘𝑥))) |
| 84 | 78, 83 | mpbird 257 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → ((𝐹 ↾ 𝑦)‘𝑥) ≤ ((𝐺 ↾ 𝑦)‘𝑥)) |
| 85 | 12, 58, 72, 84 | fsumle 15835 |
. . . . . 6
⊢ (((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑥 ∈ 𝑦 ((𝐹 ↾ 𝑦)‘𝑥) ≤ Σ𝑥 ∈ 𝑦 ((𝐺 ↾ 𝑦)‘𝑥)) |
| 86 | 55, 70 | breq12d 5156 |
. . . . . 6
⊢ (((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) →
((Σ^‘(𝐹 ↾ 𝑦)) ≤
(Σ^‘(𝐺 ↾ 𝑦)) ↔ Σ𝑥 ∈ 𝑦 ((𝐹 ↾ 𝑦)‘𝑥) ≤ Σ𝑥 ∈ 𝑦 ((𝐺 ↾ 𝑦)‘𝑥))) |
| 87 | 85, 86 | mpbird 257 |
. . . . 5
⊢ (((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝑦)) ≤
(Σ^‘(𝐺 ↾ 𝑦))) |
| 88 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑋 ∈ 𝑉) |
| 89 | 15 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) → 𝐺:𝑋⟶(0[,]+∞)) |
| 90 | 88, 89 | sge0less 46407 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐺 ↾ 𝑦)) ≤
(Σ^‘𝐺)) |
| 91 | 90 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐺 ↾ 𝑦)) ≤
(Σ^‘𝐺)) |
| 92 | 60, 74, 75, 87, 91 | letrd 11418 |
. . . 4
⊢ (((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝑦)) ≤
(Σ^‘𝐺)) |
| 93 | 92 | ralrimiva 3146 |
. . 3
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) → ∀𝑦 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑦)) ≤
(Σ^‘𝐺)) |
| 94 | 62, 61 | sge0xrcl 46400 |
. . . 4
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) →
(Σ^‘𝐺) ∈
ℝ*) |
| 95 | 62, 13, 94 | sge0lefi 46413 |
. . 3
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) →
((Σ^‘𝐹) ≤
(Σ^‘𝐺) ↔ ∀𝑦 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑦)) ≤
(Σ^‘𝐺))) |
| 96 | 93, 95 | mpbird 257 |
. 2
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐺) = +∞) →
(Σ^‘𝐹) ≤
(Σ^‘𝐺)) |
| 97 | 10, 96 | pm2.61dan 813 |
1
⊢ (𝜑 →
(Σ^‘𝐹) ≤
(Σ^‘𝐺)) |