| Step | Hyp | Ref
| Expression |
| 1 | | amgm.1 |
. . . . . . . . 9
⊢ 𝑀 =
(mulGrp‘ℂfld) |
| 2 | | cnfldbas 21368 |
. . . . . . . . 9
⊢ ℂ =
(Base‘ℂfld) |
| 3 | 1, 2 | mgpbas 20142 |
. . . . . . . 8
⊢ ℂ =
(Base‘𝑀) |
| 4 | | cnfld1 21406 |
. . . . . . . . 9
⊢ 1 =
(1r‘ℂfld) |
| 5 | 1, 4 | ringidval 20180 |
. . . . . . . 8
⊢ 1 =
(0g‘𝑀) |
| 6 | | cnfldmul 21372 |
. . . . . . . . 9
⊢ ·
= (.r‘ℂfld) |
| 7 | 1, 6 | mgpplusg 20141 |
. . . . . . . 8
⊢ ·
= (+g‘𝑀) |
| 8 | | cncrng 21401 |
. . . . . . . . 9
⊢
ℂfld ∈ CRing |
| 9 | 1 | crngmgp 20238 |
. . . . . . . . 9
⊢
(ℂfld ∈ CRing → 𝑀 ∈ CMnd) |
| 10 | 8, 9 | mp1i 13 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 𝑀 ∈ CMnd) |
| 11 | | simpl1 1192 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 𝐴 ∈ Fin) |
| 12 | | simpl3 1194 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 𝐹:𝐴⟶(0[,)+∞)) |
| 13 | | rge0ssre 13496 |
. . . . . . . . . 10
⊢
(0[,)+∞) ⊆ ℝ |
| 14 | | ax-resscn 11212 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
| 15 | 13, 14 | sstri 3993 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℂ |
| 16 | | fss 6752 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶(0[,)+∞) ∧ (0[,)+∞)
⊆ ℂ) → 𝐹:𝐴⟶ℂ) |
| 17 | 12, 15, 16 | sylancl 586 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 𝐹:𝐴⟶ℂ) |
| 18 | | 1ex 11257 |
. . . . . . . . . 10
⊢ 1 ∈
V |
| 19 | 18 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 1 ∈ V) |
| 20 | 17, 11, 19 | fdmfifsupp 9415 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 𝐹 finSupp 1) |
| 21 | | disjdif 4472 |
. . . . . . . . 9
⊢ ({𝑥} ∩ (𝐴 ∖ {𝑥})) = ∅ |
| 22 | 21 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → ({𝑥} ∩ (𝐴 ∖ {𝑥})) = ∅) |
| 23 | | undif2 4477 |
. . . . . . . . 9
⊢ ({𝑥} ∪ (𝐴 ∖ {𝑥})) = ({𝑥} ∪ 𝐴) |
| 24 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 𝑥 ∈ 𝐴) |
| 25 | 24 | snssd 4809 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → {𝑥} ⊆ 𝐴) |
| 26 | | ssequn1 4186 |
. . . . . . . . . 10
⊢ ({𝑥} ⊆ 𝐴 ↔ ({𝑥} ∪ 𝐴) = 𝐴) |
| 27 | 25, 26 | sylib 218 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → ({𝑥} ∪ 𝐴) = 𝐴) |
| 28 | 23, 27 | eqtr2id 2790 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 𝐴 = ({𝑥} ∪ (𝐴 ∖ {𝑥}))) |
| 29 | 3, 5, 7, 10, 11, 17, 20, 22, 28 | gsumsplit 19946 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝑀 Σg 𝐹) = ((𝑀 Σg (𝐹 ↾ {𝑥})) · (𝑀 Σg (𝐹 ↾ (𝐴 ∖ {𝑥}))))) |
| 30 | 12, 25 | feqresmpt 6978 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝐹 ↾ {𝑥}) = (𝑦 ∈ {𝑥} ↦ (𝐹‘𝑦))) |
| 31 | 30 | oveq2d 7447 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝑀 Σg (𝐹 ↾ {𝑥})) = (𝑀 Σg (𝑦 ∈ {𝑥} ↦ (𝐹‘𝑦)))) |
| 32 | | cnring 21403 |
. . . . . . . . . . 11
⊢
ℂfld ∈ Ring |
| 33 | 1 | ringmgp 20236 |
. . . . . . . . . . 11
⊢
(ℂfld ∈ Ring → 𝑀 ∈ Mnd) |
| 34 | 32, 33 | mp1i 13 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 𝑀 ∈ Mnd) |
| 35 | 17, 24 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝐹‘𝑥) ∈ ℂ) |
| 36 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥)) |
| 37 | 3, 36 | gsumsn 19972 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ Mnd ∧ 𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ ℂ) → (𝑀 Σg (𝑦 ∈ {𝑥} ↦ (𝐹‘𝑦))) = (𝐹‘𝑥)) |
| 38 | 34, 24, 35, 37 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝑀 Σg (𝑦 ∈ {𝑥} ↦ (𝐹‘𝑦))) = (𝐹‘𝑥)) |
| 39 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝐹‘𝑥) = 0) |
| 40 | 31, 38, 39 | 3eqtrd 2781 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝑀 Σg (𝐹 ↾ {𝑥})) = 0) |
| 41 | 40 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → ((𝑀 Σg (𝐹 ↾ {𝑥})) · (𝑀 Σg (𝐹 ↾ (𝐴 ∖ {𝑥})))) = (0 · (𝑀 Σg (𝐹 ↾ (𝐴 ∖ {𝑥}))))) |
| 42 | | diffi 9215 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin → (𝐴 ∖ {𝑥}) ∈ Fin) |
| 43 | 11, 42 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝐴 ∖ {𝑥}) ∈ Fin) |
| 44 | | difss 4136 |
. . . . . . . . . 10
⊢ (𝐴 ∖ {𝑥}) ⊆ 𝐴 |
| 45 | | fssres 6774 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ (𝐴 ∖ {𝑥}) ⊆ 𝐴) → (𝐹 ↾ (𝐴 ∖ {𝑥})):(𝐴 ∖ {𝑥})⟶ℂ) |
| 46 | 17, 44, 45 | sylancl 586 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝐹 ↾ (𝐴 ∖ {𝑥})):(𝐴 ∖ {𝑥})⟶ℂ) |
| 47 | 46, 43, 19 | fdmfifsupp 9415 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝐹 ↾ (𝐴 ∖ {𝑥})) finSupp 1) |
| 48 | 3, 5, 10, 43, 46, 47 | gsumcl 19933 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝑀 Σg (𝐹 ↾ (𝐴 ∖ {𝑥}))) ∈ ℂ) |
| 49 | 48 | mul02d 11459 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (0 · (𝑀 Σg (𝐹 ↾ (𝐴 ∖ {𝑥})))) = 0) |
| 50 | 29, 41, 49 | 3eqtrd 2781 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝑀 Σg 𝐹) = 0) |
| 51 | 50 | oveq1d 7446 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → ((𝑀 Σg 𝐹)↑𝑐(1 /
(♯‘𝐴))) =
(0↑𝑐(1 / (♯‘𝐴)))) |
| 52 | | simpl2 1193 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 𝐴 ≠ ∅) |
| 53 | | hashnncl 14405 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin →
((♯‘𝐴) ∈
ℕ ↔ 𝐴 ≠
∅)) |
| 54 | 11, 53 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) |
| 55 | 52, 54 | mpbird 257 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (♯‘𝐴) ∈
ℕ) |
| 56 | 55 | nncnd 12282 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (♯‘𝐴) ∈
ℂ) |
| 57 | 55 | nnne0d 12316 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (♯‘𝐴) ≠ 0) |
| 58 | 56, 57 | reccld 12036 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (1 / (♯‘𝐴)) ∈
ℂ) |
| 59 | 56, 57 | recne0d 12037 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (1 / (♯‘𝐴)) ≠ 0) |
| 60 | 58, 59 | 0cxpd 26752 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (0↑𝑐(1
/ (♯‘𝐴))) =
0) |
| 61 | 51, 60 | eqtrd 2777 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → ((𝑀 Σg 𝐹)↑𝑐(1 /
(♯‘𝐴))) =
0) |
| 62 | | cnfld0 21405 |
. . . . . . 7
⊢ 0 =
(0g‘ℂfld) |
| 63 | | ringcmn 20279 |
. . . . . . . 8
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) |
| 64 | 32, 63 | mp1i 13 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → ℂfld ∈
CMnd) |
| 65 | | rege0subm 21441 |
. . . . . . . 8
⊢
(0[,)+∞) ∈
(SubMnd‘ℂfld) |
| 66 | 65 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (0[,)+∞) ∈
(SubMnd‘ℂfld)) |
| 67 | | c0ex 11255 |
. . . . . . . . 9
⊢ 0 ∈
V |
| 68 | 67 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 0 ∈ V) |
| 69 | 12, 11, 68 | fdmfifsupp 9415 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 𝐹 finSupp 0) |
| 70 | 62, 64, 11, 66, 12, 69 | gsumsubmcl 19937 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (ℂfld
Σg 𝐹) ∈ (0[,)+∞)) |
| 71 | | elrege0 13494 |
. . . . . 6
⊢
((ℂfld Σg 𝐹) ∈ (0[,)+∞) ↔
((ℂfld Σg 𝐹) ∈ ℝ ∧ 0 ≤
(ℂfld Σg 𝐹))) |
| 72 | 70, 71 | sylib 218 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → ((ℂfld
Σg 𝐹) ∈ ℝ ∧ 0 ≤
(ℂfld Σg 𝐹))) |
| 73 | 55 | nnred 12281 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (♯‘𝐴) ∈
ℝ) |
| 74 | 55 | nngt0d 12315 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 0 < (♯‘𝐴)) |
| 75 | | divge0 12137 |
. . . . 5
⊢
((((ℂfld Σg 𝐹) ∈ ℝ ∧ 0 ≤
(ℂfld Σg 𝐹)) ∧ ((♯‘𝐴) ∈ ℝ ∧ 0 <
(♯‘𝐴))) →
0 ≤ ((ℂfld Σg 𝐹) / (♯‘𝐴))) |
| 76 | 72, 73, 74, 75 | syl12anc 837 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 0 ≤ ((ℂfld
Σg 𝐹) / (♯‘𝐴))) |
| 77 | 61, 76 | eqbrtrd 5165 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → ((𝑀 Σg 𝐹)↑𝑐(1 /
(♯‘𝐴))) ≤
((ℂfld Σg 𝐹) / (♯‘𝐴))) |
| 78 | 77 | rexlimdvaa 3156 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 0 → ((𝑀 Σg 𝐹)↑𝑐(1 /
(♯‘𝐴))) ≤
((ℂfld Σg 𝐹) / (♯‘𝐴)))) |
| 79 | | ralnex 3072 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ¬ (𝐹‘𝑥) = 0 ↔ ¬ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 0) |
| 80 | | simpl1 1192 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ ∀𝑥 ∈ 𝐴 ¬ (𝐹‘𝑥) = 0) → 𝐴 ∈ Fin) |
| 81 | | simpl2 1193 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ ∀𝑥 ∈ 𝐴 ¬ (𝐹‘𝑥) = 0) → 𝐴 ≠ ∅) |
| 82 | | simpl3 1194 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ ∀𝑥 ∈ 𝐴 ¬ (𝐹‘𝑥) = 0) → 𝐹:𝐴⟶(0[,)+∞)) |
| 83 | 82 | ffnd 6737 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ ∀𝑥 ∈ 𝐴 ¬ (𝐹‘𝑥) = 0) → 𝐹 Fn 𝐴) |
| 84 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝐴⟶(0[,)+∞) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
| 85 | 84 | 3ad2antl3 1188 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
| 86 | | elrege0 13494 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
| 87 | 85, 86 | sylib 218 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
| 88 | 87 | simprd 495 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → 0 ≤ (𝐹‘𝑥)) |
| 89 | | 0re 11263 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
| 90 | 87 | simpld 494 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℝ) |
| 91 | | leloe 11347 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ) → (0 ≤ (𝐹‘𝑥) ↔ (0 < (𝐹‘𝑥) ∨ 0 = (𝐹‘𝑥)))) |
| 92 | 89, 90, 91 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → (0 ≤ (𝐹‘𝑥) ↔ (0 < (𝐹‘𝑥) ∨ 0 = (𝐹‘𝑥)))) |
| 93 | 88, 92 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → (0 < (𝐹‘𝑥) ∨ 0 = (𝐹‘𝑥))) |
| 94 | 93 | ord 865 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → (¬ 0 < (𝐹‘𝑥) → 0 = (𝐹‘𝑥))) |
| 95 | | eqcom 2744 |
. . . . . . . . . . 11
⊢ (0 =
(𝐹‘𝑥) ↔ (𝐹‘𝑥) = 0) |
| 96 | 94, 95 | imbitrdi 251 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → (¬ 0 < (𝐹‘𝑥) → (𝐹‘𝑥) = 0)) |
| 97 | 96 | con1d 145 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → (¬ (𝐹‘𝑥) = 0 → 0 < (𝐹‘𝑥))) |
| 98 | | elrp 13036 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑥) ∈ ℝ+ ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 < (𝐹‘𝑥))) |
| 99 | 98 | baib 535 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ ℝ → ((𝐹‘𝑥) ∈ ℝ+ ↔ 0 <
(𝐹‘𝑥))) |
| 100 | 90, 99 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) ∈ ℝ+ ↔ 0 <
(𝐹‘𝑥))) |
| 101 | 97, 100 | sylibrd 259 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → (¬ (𝐹‘𝑥) = 0 → (𝐹‘𝑥) ∈
ℝ+)) |
| 102 | 101 | ralimdva 3167 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(∀𝑥 ∈ 𝐴 ¬ (𝐹‘𝑥) = 0 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈
ℝ+)) |
| 103 | 102 | imp 406 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ ∀𝑥 ∈ 𝐴 ¬ (𝐹‘𝑥) = 0) → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈
ℝ+) |
| 104 | | ffnfv 7139 |
. . . . . 6
⊢ (𝐹:𝐴⟶ℝ+ ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈
ℝ+)) |
| 105 | 83, 103, 104 | sylanbrc 583 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ ∀𝑥 ∈ 𝐴 ¬ (𝐹‘𝑥) = 0) → 𝐹:𝐴⟶ℝ+) |
| 106 | 1, 80, 81, 105 | amgmlem 27033 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ ∀𝑥 ∈ 𝐴 ¬ (𝐹‘𝑥) = 0) → ((𝑀 Σg 𝐹)↑𝑐(1 /
(♯‘𝐴))) ≤
((ℂfld Σg 𝐹) / (♯‘𝐴))) |
| 107 | 106 | ex 412 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(∀𝑥 ∈ 𝐴 ¬ (𝐹‘𝑥) = 0 → ((𝑀 Σg 𝐹)↑𝑐(1 /
(♯‘𝐴))) ≤
((ℂfld Σg 𝐹) / (♯‘𝐴)))) |
| 108 | 79, 107 | biimtrrid 243 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) → (¬
∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 0 → ((𝑀 Σg 𝐹)↑𝑐(1 /
(♯‘𝐴))) ≤
((ℂfld Σg 𝐹) / (♯‘𝐴)))) |
| 109 | 78, 108 | pm2.61d 179 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) → ((𝑀 Σg
𝐹)↑𝑐(1 /
(♯‘𝐴))) ≤
((ℂfld Σg 𝐹) / (♯‘𝐴))) |