Step | Hyp | Ref
| Expression |
1 | | amgm.1 |
. . . . . . . . 9
⊢ 𝑀 =
(mulGrp‘ℂfld) |
2 | | cnfldbas 19750 |
. . . . . . . . 9
⊢ ℂ =
(Base‘ℂfld) |
3 | 1, 2 | mgpbas 18495 |
. . . . . . . 8
⊢ ℂ =
(Base‘𝑀) |
4 | | cnfld1 19771 |
. . . . . . . . 9
⊢ 1 =
(1r‘ℂfld) |
5 | 1, 4 | ringidval 18503 |
. . . . . . . 8
⊢ 1 =
(0g‘𝑀) |
6 | | cnfldmul 19752 |
. . . . . . . . 9
⊢ ·
= (.r‘ℂfld) |
7 | 1, 6 | mgpplusg 18493 |
. . . . . . . 8
⊢ ·
= (+g‘𝑀) |
8 | | cncrng 19767 |
. . . . . . . . 9
⊢
ℂfld ∈ CRing |
9 | 1 | crngmgp 18555 |
. . . . . . . . 9
⊢
(ℂfld ∈ CRing → 𝑀 ∈ CMnd) |
10 | 8, 9 | mp1i 13 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 𝑀 ∈ CMnd) |
11 | | simpl1 1064 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 𝐴 ∈ Fin) |
12 | | simpl3 1066 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 𝐹:𝐴⟶(0[,)+∞)) |
13 | | rge0ssre 12280 |
. . . . . . . . . 10
⊢
(0[,)+∞) ⊆ ℝ |
14 | | ax-resscn 9993 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
15 | 13, 14 | sstri 3612 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℂ |
16 | | fss 6056 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶(0[,)+∞) ∧ (0[,)+∞)
⊆ ℂ) → 𝐹:𝐴⟶ℂ) |
17 | 12, 15, 16 | sylancl 694 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 𝐹:𝐴⟶ℂ) |
18 | | 1ex 10035 |
. . . . . . . . . 10
⊢ 1 ∈
V |
19 | 18 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 1 ∈ V) |
20 | 17, 11, 19 | fdmfifsupp 8285 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 𝐹 finSupp 1) |
21 | | disjdif 4040 |
. . . . . . . . 9
⊢ ({𝑥} ∩ (𝐴 ∖ {𝑥})) = ∅ |
22 | 21 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → ({𝑥} ∩ (𝐴 ∖ {𝑥})) = ∅) |
23 | | undif2 4044 |
. . . . . . . . 9
⊢ ({𝑥} ∪ (𝐴 ∖ {𝑥})) = ({𝑥} ∪ 𝐴) |
24 | | simprl 794 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 𝑥 ∈ 𝐴) |
25 | 24 | snssd 4340 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → {𝑥} ⊆ 𝐴) |
26 | | ssequn1 3783 |
. . . . . . . . . 10
⊢ ({𝑥} ⊆ 𝐴 ↔ ({𝑥} ∪ 𝐴) = 𝐴) |
27 | 25, 26 | sylib 208 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → ({𝑥} ∪ 𝐴) = 𝐴) |
28 | 23, 27 | syl5req 2669 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 𝐴 = ({𝑥} ∪ (𝐴 ∖ {𝑥}))) |
29 | 3, 5, 7, 10, 11, 17, 20, 22, 28 | gsumsplit 18328 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝑀 Σg 𝐹) = ((𝑀 Σg (𝐹 ↾ {𝑥})) · (𝑀 Σg (𝐹 ↾ (𝐴 ∖ {𝑥}))))) |
30 | 12, 25 | feqresmpt 6250 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝐹 ↾ {𝑥}) = (𝑦 ∈ {𝑥} ↦ (𝐹‘𝑦))) |
31 | 30 | oveq2d 6666 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝑀 Σg (𝐹 ↾ {𝑥})) = (𝑀 Σg (𝑦 ∈ {𝑥} ↦ (𝐹‘𝑦)))) |
32 | | cnring 19768 |
. . . . . . . . . . 11
⊢
ℂfld ∈ Ring |
33 | 1 | ringmgp 18553 |
. . . . . . . . . . 11
⊢
(ℂfld ∈ Ring → 𝑀 ∈ Mnd) |
34 | 32, 33 | mp1i 13 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 𝑀 ∈ Mnd) |
35 | 17, 24 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝐹‘𝑥) ∈ ℂ) |
36 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥)) |
37 | 3, 36 | gsumsn 18354 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ Mnd ∧ 𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ ℂ) → (𝑀 Σg (𝑦 ∈ {𝑥} ↦ (𝐹‘𝑦))) = (𝐹‘𝑥)) |
38 | 34, 24, 35, 37 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝑀 Σg (𝑦 ∈ {𝑥} ↦ (𝐹‘𝑦))) = (𝐹‘𝑥)) |
39 | | simprr 796 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝐹‘𝑥) = 0) |
40 | 31, 38, 39 | 3eqtrd 2660 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝑀 Σg (𝐹 ↾ {𝑥})) = 0) |
41 | 40 | oveq1d 6665 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → ((𝑀 Σg (𝐹 ↾ {𝑥})) · (𝑀 Σg (𝐹 ↾ (𝐴 ∖ {𝑥})))) = (0 · (𝑀 Σg (𝐹 ↾ (𝐴 ∖ {𝑥}))))) |
42 | | diffi 8192 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin → (𝐴 ∖ {𝑥}) ∈ Fin) |
43 | 11, 42 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝐴 ∖ {𝑥}) ∈ Fin) |
44 | | difss 3737 |
. . . . . . . . . 10
⊢ (𝐴 ∖ {𝑥}) ⊆ 𝐴 |
45 | | fssres 6070 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ (𝐴 ∖ {𝑥}) ⊆ 𝐴) → (𝐹 ↾ (𝐴 ∖ {𝑥})):(𝐴 ∖ {𝑥})⟶ℂ) |
46 | 17, 44, 45 | sylancl 694 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝐹 ↾ (𝐴 ∖ {𝑥})):(𝐴 ∖ {𝑥})⟶ℂ) |
47 | 46, 43, 19 | fdmfifsupp 8285 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝐹 ↾ (𝐴 ∖ {𝑥})) finSupp 1) |
48 | 3, 5, 10, 43, 46, 47 | gsumcl 18316 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝑀 Σg (𝐹 ↾ (𝐴 ∖ {𝑥}))) ∈ ℂ) |
49 | 48 | mul02d 10234 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (0 · (𝑀 Σg (𝐹 ↾ (𝐴 ∖ {𝑥})))) = 0) |
50 | 29, 41, 49 | 3eqtrd 2660 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (𝑀 Σg 𝐹) = 0) |
51 | 50 | oveq1d 6665 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → ((𝑀 Σg 𝐹)↑𝑐(1 /
(#‘𝐴))) =
(0↑𝑐(1 / (#‘𝐴)))) |
52 | | simpl2 1065 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 𝐴 ≠ ∅) |
53 | | hashnncl 13157 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin →
((#‘𝐴) ∈ ℕ
↔ 𝐴 ≠
∅)) |
54 | 11, 53 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) |
55 | 52, 54 | mpbird 247 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (#‘𝐴) ∈ ℕ) |
56 | 55 | nncnd 11036 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (#‘𝐴) ∈ ℂ) |
57 | 55 | nnne0d 11065 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (#‘𝐴) ≠ 0) |
58 | 56, 57 | reccld 10794 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (1 / (#‘𝐴)) ∈
ℂ) |
59 | 56, 57 | recne0d 10795 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (1 / (#‘𝐴)) ≠ 0) |
60 | 58, 59 | 0cxpd 24456 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (0↑𝑐(1
/ (#‘𝐴))) =
0) |
61 | 51, 60 | eqtrd 2656 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → ((𝑀 Σg 𝐹)↑𝑐(1 /
(#‘𝐴))) =
0) |
62 | | cnfld0 19770 |
. . . . . . 7
⊢ 0 =
(0g‘ℂfld) |
63 | | ringcmn 18581 |
. . . . . . . 8
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) |
64 | 32, 63 | mp1i 13 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → ℂfld ∈
CMnd) |
65 | | rege0subm 19802 |
. . . . . . . 8
⊢
(0[,)+∞) ∈
(SubMnd‘ℂfld) |
66 | 65 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (0[,)+∞) ∈
(SubMnd‘ℂfld)) |
67 | | c0ex 10034 |
. . . . . . . . 9
⊢ 0 ∈
V |
68 | 67 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 0 ∈ V) |
69 | 12, 11, 68 | fdmfifsupp 8285 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 𝐹 finSupp 0) |
70 | 62, 64, 11, 66, 12, 69 | gsumsubmcl 18319 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (ℂfld
Σg 𝐹) ∈ (0[,)+∞)) |
71 | | elrege0 12278 |
. . . . . 6
⊢
((ℂfld Σg 𝐹) ∈ (0[,)+∞) ↔
((ℂfld Σg 𝐹) ∈ ℝ ∧ 0 ≤
(ℂfld Σg 𝐹))) |
72 | 70, 71 | sylib 208 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → ((ℂfld
Σg 𝐹) ∈ ℝ ∧ 0 ≤
(ℂfld Σg 𝐹))) |
73 | 55 | nnred 11035 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → (#‘𝐴) ∈ ℝ) |
74 | 55 | nngt0d 11064 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 0 < (#‘𝐴)) |
75 | | divge0 10892 |
. . . . 5
⊢
((((ℂfld Σg 𝐹) ∈ ℝ ∧ 0 ≤
(ℂfld Σg 𝐹)) ∧ ((#‘𝐴) ∈ ℝ ∧ 0 < (#‘𝐴))) → 0 ≤
((ℂfld Σg 𝐹) / (#‘𝐴))) |
76 | 72, 73, 74, 75 | syl12anc 1324 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → 0 ≤ ((ℂfld
Σg 𝐹) / (#‘𝐴))) |
77 | 61, 76 | eqbrtrd 4675 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 0)) → ((𝑀 Σg 𝐹)↑𝑐(1 /
(#‘𝐴))) ≤
((ℂfld Σg 𝐹) / (#‘𝐴))) |
78 | 77 | rexlimdvaa 3032 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 0 → ((𝑀 Σg 𝐹)↑𝑐(1 /
(#‘𝐴))) ≤
((ℂfld Σg 𝐹) / (#‘𝐴)))) |
79 | | ralnex 2992 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ¬ (𝐹‘𝑥) = 0 ↔ ¬ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 0) |
80 | | simpl1 1064 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ ∀𝑥 ∈ 𝐴 ¬ (𝐹‘𝑥) = 0) → 𝐴 ∈ Fin) |
81 | | simpl2 1065 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ ∀𝑥 ∈ 𝐴 ¬ (𝐹‘𝑥) = 0) → 𝐴 ≠ ∅) |
82 | | simpl3 1066 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ ∀𝑥 ∈ 𝐴 ¬ (𝐹‘𝑥) = 0) → 𝐹:𝐴⟶(0[,)+∞)) |
83 | | ffn 6045 |
. . . . . . 7
⊢ (𝐹:𝐴⟶(0[,)+∞) → 𝐹 Fn 𝐴) |
84 | 82, 83 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ ∀𝑥 ∈ 𝐴 ¬ (𝐹‘𝑥) = 0) → 𝐹 Fn 𝐴) |
85 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝐴⟶(0[,)+∞) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
86 | 85 | 3ad2antl3 1225 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
87 | | elrege0 12278 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
88 | 86, 87 | sylib 208 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
89 | 88 | simprd 479 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → 0 ≤ (𝐹‘𝑥)) |
90 | | 0re 10040 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
91 | 88 | simpld 475 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℝ) |
92 | | leloe 10124 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ) → (0 ≤ (𝐹‘𝑥) ↔ (0 < (𝐹‘𝑥) ∨ 0 = (𝐹‘𝑥)))) |
93 | 90, 91, 92 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → (0 ≤ (𝐹‘𝑥) ↔ (0 < (𝐹‘𝑥) ∨ 0 = (𝐹‘𝑥)))) |
94 | 89, 93 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → (0 < (𝐹‘𝑥) ∨ 0 = (𝐹‘𝑥))) |
95 | 94 | ord 392 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → (¬ 0 < (𝐹‘𝑥) → 0 = (𝐹‘𝑥))) |
96 | | eqcom 2629 |
. . . . . . . . . . 11
⊢ (0 =
(𝐹‘𝑥) ↔ (𝐹‘𝑥) = 0) |
97 | 95, 96 | syl6ib 241 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → (¬ 0 < (𝐹‘𝑥) → (𝐹‘𝑥) = 0)) |
98 | 97 | con1d 139 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → (¬ (𝐹‘𝑥) = 0 → 0 < (𝐹‘𝑥))) |
99 | | elrp 11834 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑥) ∈ ℝ+ ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 < (𝐹‘𝑥))) |
100 | 99 | baib 944 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ ℝ → ((𝐹‘𝑥) ∈ ℝ+ ↔ 0 <
(𝐹‘𝑥))) |
101 | 91, 100 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) ∈ ℝ+ ↔ 0 <
(𝐹‘𝑥))) |
102 | 98, 101 | sylibrd 249 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ 𝑥 ∈ 𝐴) → (¬ (𝐹‘𝑥) = 0 → (𝐹‘𝑥) ∈
ℝ+)) |
103 | 102 | ralimdva 2962 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(∀𝑥 ∈ 𝐴 ¬ (𝐹‘𝑥) = 0 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈
ℝ+)) |
104 | 103 | imp 445 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ ∀𝑥 ∈ 𝐴 ¬ (𝐹‘𝑥) = 0) → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈
ℝ+) |
105 | | ffnfv 6388 |
. . . . . 6
⊢ (𝐹:𝐴⟶ℝ+ ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈
ℝ+)) |
106 | 84, 104, 105 | sylanbrc 698 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ ∀𝑥 ∈ 𝐴 ¬ (𝐹‘𝑥) = 0) → 𝐹:𝐴⟶ℝ+) |
107 | 1, 80, 81, 106 | amgmlem 24716 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) ∧ ∀𝑥 ∈ 𝐴 ¬ (𝐹‘𝑥) = 0) → ((𝑀 Σg 𝐹)↑𝑐(1 /
(#‘𝐴))) ≤
((ℂfld Σg 𝐹) / (#‘𝐴))) |
108 | 107 | ex 450 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) →
(∀𝑥 ∈ 𝐴 ¬ (𝐹‘𝑥) = 0 → ((𝑀 Σg 𝐹)↑𝑐(1 /
(#‘𝐴))) ≤
((ℂfld Σg 𝐹) / (#‘𝐴)))) |
109 | 79, 108 | syl5bir 233 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) → (¬
∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 0 → ((𝑀 Σg 𝐹)↑𝑐(1 /
(#‘𝐴))) ≤
((ℂfld Σg 𝐹) / (#‘𝐴)))) |
110 | 78, 109 | pm2.61d 170 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) → ((𝑀 Σg
𝐹)↑𝑐(1 /
(#‘𝐴))) ≤
((ℂfld Σg 𝐹) / (#‘𝐴))) |