Step | Hyp | Ref
| Expression |
1 | | cnfld0 20844 |
. . . . . . 7
β’ 0 =
(0gββfld) |
2 | | cnring 20842 |
. . . . . . . 8
β’
βfld β Ring |
3 | | ringabl 20010 |
. . . . . . . 8
β’
(βfld β Ring β βfld β
Abel) |
4 | 2, 3 | mp1i 13 |
. . . . . . 7
β’ (π β βfld
β Abel) |
5 | | jensen.4 |
. . . . . . . 8
β’ (π β π΄ β Fin) |
6 | | jensenlem.2 |
. . . . . . . . 9
β’ (π β (π΅ βͺ {π§}) β π΄) |
7 | 6 | unssad 4151 |
. . . . . . . 8
β’ (π β π΅ β π΄) |
8 | 5, 7 | ssfid 9217 |
. . . . . . 7
β’ (π β π΅ β Fin) |
9 | | resubdrg 21035 |
. . . . . . . . 9
β’ (β
β (SubRingββfld) β§ βfld β
DivRing) |
10 | 9 | simpli 485 |
. . . . . . . 8
β’ β
β (SubRingββfld) |
11 | | subrgsubg 20270 |
. . . . . . . 8
β’ (β
β (SubRingββfld) β β β
(SubGrpββfld)) |
12 | 10, 11 | mp1i 13 |
. . . . . . 7
β’ (π β β β
(SubGrpββfld)) |
13 | | remulcl 11144 |
. . . . . . . . . 10
β’ ((π₯ β β β§ π¦ β β) β (π₯ Β· π¦) β β) |
14 | 13 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β β§ π¦ β β)) β (π₯ Β· π¦) β β) |
15 | | jensen.5 |
. . . . . . . . . 10
β’ (π β π:π΄βΆ(0[,)+β)) |
16 | | rge0ssre 13382 |
. . . . . . . . . 10
β’
(0[,)+β) β β |
17 | | fss 6689 |
. . . . . . . . . 10
β’ ((π:π΄βΆ(0[,)+β) β§ (0[,)+β)
β β) β π:π΄βΆβ) |
18 | 15, 16, 17 | sylancl 587 |
. . . . . . . . 9
β’ (π β π:π΄βΆβ) |
19 | | jensen.6 |
. . . . . . . . . 10
β’ (π β π:π΄βΆπ·) |
20 | | jensen.1 |
. . . . . . . . . 10
β’ (π β π· β β) |
21 | 19, 20 | fssd 6690 |
. . . . . . . . 9
β’ (π β π:π΄βΆβ) |
22 | | inidm 4182 |
. . . . . . . . 9
β’ (π΄ β© π΄) = π΄ |
23 | 14, 18, 21, 5, 5, 22 | off 7639 |
. . . . . . . 8
β’ (π β (π βf Β· π):π΄βΆβ) |
24 | 23, 7 | fssresd 6713 |
. . . . . . 7
β’ (π β ((π βf Β· π) βΎ π΅):π΅βΆβ) |
25 | | c0ex 11157 |
. . . . . . . . 9
β’ 0 β
V |
26 | 25 | a1i 11 |
. . . . . . . 8
β’ (π β 0 β
V) |
27 | 24, 8, 26 | fdmfifsupp 9323 |
. . . . . . 7
β’ (π β ((π βf Β· π) βΎ π΅) finSupp 0) |
28 | 1, 4, 8, 12, 24, 27 | gsumsubgcl 19705 |
. . . . . 6
β’ (π β (βfld
Ξ£g ((π βf Β· π) βΎ π΅)) β β) |
29 | 28 | recnd 11191 |
. . . . 5
β’ (π β (βfld
Ξ£g ((π βf Β· π) βΎ π΅)) β β) |
30 | | ax-resscn 11116 |
. . . . . . . 8
β’ β
β β |
31 | 16, 30 | sstri 3957 |
. . . . . . 7
β’
(0[,)+β) β β |
32 | 6 | unssbd 4152 |
. . . . . . . . 9
β’ (π β {π§} β π΄) |
33 | | vex 3451 |
. . . . . . . . . 10
β’ π§ β V |
34 | 33 | snss 4750 |
. . . . . . . . 9
β’ (π§ β π΄ β {π§} β π΄) |
35 | 32, 34 | sylibr 233 |
. . . . . . . 8
β’ (π β π§ β π΄) |
36 | 15, 35 | ffvelcdmd 7040 |
. . . . . . 7
β’ (π β (πβπ§) β (0[,)+β)) |
37 | 31, 36 | sselid 3946 |
. . . . . 6
β’ (π β (πβπ§) β β) |
38 | 19, 35 | ffvelcdmd 7040 |
. . . . . . . 8
β’ (π β (πβπ§) β π·) |
39 | 20, 38 | sseldd 3949 |
. . . . . . 7
β’ (π β (πβπ§) β β) |
40 | 39 | recnd 11191 |
. . . . . 6
β’ (π β (πβπ§) β β) |
41 | 37, 40 | mulcld 11183 |
. . . . 5
β’ (π β ((πβπ§) Β· (πβπ§)) β β) |
42 | | jensen.2 |
. . . . . . . 8
β’ (π β πΉ:π·βΆβ) |
43 | | jensen.3 |
. . . . . . . 8
β’ ((π β§ (π β π· β§ π β π·)) β (π[,]π) β π·) |
44 | | jensen.7 |
. . . . . . . 8
β’ (π β 0 <
(βfld Ξ£g π)) |
45 | | jensen.8 |
. . . . . . . 8
β’ ((π β§ (π₯ β π· β§ π¦ β π· β§ π‘ β (0[,]1))) β (πΉβ((π‘ Β· π₯) + ((1 β π‘) Β· π¦))) β€ ((π‘ Β· (πΉβπ₯)) + ((1 β π‘) Β· (πΉβπ¦)))) |
46 | | jensenlem.1 |
. . . . . . . 8
β’ (π β Β¬ π§ β π΅) |
47 | | jensenlem.s |
. . . . . . . 8
β’ π = (βfld
Ξ£g (π βΎ π΅)) |
48 | | jensenlem.l |
. . . . . . . 8
β’ πΏ = (βfld
Ξ£g (π βΎ (π΅ βͺ {π§}))) |
49 | 20, 42, 43, 5, 15, 19, 44, 45, 46, 6, 47, 48 | jensenlem1 26359 |
. . . . . . 7
β’ (π β πΏ = (π + (πβπ§))) |
50 | | jensenlem.3 |
. . . . . . . . 9
β’ (π β π β
β+) |
51 | 50 | rpred 12965 |
. . . . . . . 8
β’ (π β π β β) |
52 | | elrege0 13380 |
. . . . . . . . . 10
β’ ((πβπ§) β (0[,)+β) β ((πβπ§) β β β§ 0 β€ (πβπ§))) |
53 | 52 | simplbi 499 |
. . . . . . . . 9
β’ ((πβπ§) β (0[,)+β) β (πβπ§) β β) |
54 | 36, 53 | syl 17 |
. . . . . . . 8
β’ (π β (πβπ§) β β) |
55 | 51, 54 | readdcld 11192 |
. . . . . . 7
β’ (π β (π + (πβπ§)) β β) |
56 | 49, 55 | eqeltrd 2834 |
. . . . . 6
β’ (π β πΏ β β) |
57 | 56 | recnd 11191 |
. . . . 5
β’ (π β πΏ β β) |
58 | | 0red 11166 |
. . . . . . 7
β’ (π β 0 β
β) |
59 | 50 | rpgt0d 12968 |
. . . . . . 7
β’ (π β 0 < π) |
60 | 52 | simprbi 498 |
. . . . . . . . . 10
β’ ((πβπ§) β (0[,)+β) β 0 β€ (πβπ§)) |
61 | 36, 60 | syl 17 |
. . . . . . . . 9
β’ (π β 0 β€ (πβπ§)) |
62 | 51, 54 | addge01d 11751 |
. . . . . . . . 9
β’ (π β (0 β€ (πβπ§) β π β€ (π + (πβπ§)))) |
63 | 61, 62 | mpbid 231 |
. . . . . . . 8
β’ (π β π β€ (π + (πβπ§))) |
64 | 63, 49 | breqtrrd 5137 |
. . . . . . 7
β’ (π β π β€ πΏ) |
65 | 58, 51, 56, 59, 64 | ltletrd 11323 |
. . . . . 6
β’ (π β 0 < πΏ) |
66 | 65 | gt0ne0d 11727 |
. . . . 5
β’ (π β πΏ β 0) |
67 | 29, 41, 57, 66 | divdird 11977 |
. . . 4
β’ (π β (((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) + ((πβπ§) Β· (πβπ§))) / πΏ) = (((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / πΏ) + (((πβπ§) Β· (πβπ§)) / πΏ))) |
68 | | cnfldbas 20823 |
. . . . . . 7
β’ β =
(Baseββfld) |
69 | | cnfldadd 20824 |
. . . . . . 7
β’ + =
(+gββfld) |
70 | | ringcmn 20011 |
. . . . . . . 8
β’
(βfld β Ring β βfld β
CMnd) |
71 | 2, 70 | mp1i 13 |
. . . . . . 7
β’ (π β βfld
β CMnd) |
72 | 7 | sselda 3948 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΅) β π₯ β π΄) |
73 | 15 | ffvelcdmda 7039 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (πβπ₯) β (0[,)+β)) |
74 | 72, 73 | syldan 592 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅) β (πβπ₯) β (0[,)+β)) |
75 | 31, 74 | sselid 3946 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅) β (πβπ₯) β β) |
76 | 20 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΅) β π· β β) |
77 | 19 | ffvelcdmda 7039 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β (πβπ₯) β π·) |
78 | 72, 77 | syldan 592 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΅) β (πβπ₯) β π·) |
79 | 76, 78 | sseldd 3949 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅) β (πβπ₯) β β) |
80 | 79 | recnd 11191 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅) β (πβπ₯) β β) |
81 | 75, 80 | mulcld 11183 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β ((πβπ₯) Β· (πβπ₯)) β β) |
82 | | fveq2 6846 |
. . . . . . . 8
β’ (π₯ = π§ β (πβπ₯) = (πβπ§)) |
83 | | fveq2 6846 |
. . . . . . . 8
β’ (π₯ = π§ β (πβπ₯) = (πβπ§)) |
84 | 82, 83 | oveq12d 7379 |
. . . . . . 7
β’ (π₯ = π§ β ((πβπ₯) Β· (πβπ₯)) = ((πβπ§) Β· (πβπ§))) |
85 | 68, 69, 71, 8, 81, 35, 46, 41, 84 | gsumunsn 19745 |
. . . . . 6
β’ (π β (βfld
Ξ£g (π₯ β (π΅ βͺ {π§}) β¦ ((πβπ₯) Β· (πβπ₯)))) = ((βfld
Ξ£g (π₯ β π΅ β¦ ((πβπ₯) Β· (πβπ₯)))) + ((πβπ§) Β· (πβπ§)))) |
86 | 15 | feqmptd 6914 |
. . . . . . . . . 10
β’ (π β π = (π₯ β π΄ β¦ (πβπ₯))) |
87 | 19 | feqmptd 6914 |
. . . . . . . . . 10
β’ (π β π = (π₯ β π΄ β¦ (πβπ₯))) |
88 | 5, 73, 77, 86, 87 | offval2 7641 |
. . . . . . . . 9
β’ (π β (π βf Β· π) = (π₯ β π΄ β¦ ((πβπ₯) Β· (πβπ₯)))) |
89 | 88 | reseq1d 5940 |
. . . . . . . 8
β’ (π β ((π βf Β· π) βΎ (π΅ βͺ {π§})) = ((π₯ β π΄ β¦ ((πβπ₯) Β· (πβπ₯))) βΎ (π΅ βͺ {π§}))) |
90 | 6 | resmptd 5998 |
. . . . . . . 8
β’ (π β ((π₯ β π΄ β¦ ((πβπ₯) Β· (πβπ₯))) βΎ (π΅ βͺ {π§})) = (π₯ β (π΅ βͺ {π§}) β¦ ((πβπ₯) Β· (πβπ₯)))) |
91 | 89, 90 | eqtrd 2773 |
. . . . . . 7
β’ (π β ((π βf Β· π) βΎ (π΅ βͺ {π§})) = (π₯ β (π΅ βͺ {π§}) β¦ ((πβπ₯) Β· (πβπ₯)))) |
92 | 91 | oveq2d 7377 |
. . . . . 6
β’ (π β (βfld
Ξ£g ((π βf Β· π) βΎ (π΅ βͺ {π§}))) = (βfld
Ξ£g (π₯ β (π΅ βͺ {π§}) β¦ ((πβπ₯) Β· (πβπ₯))))) |
93 | 88 | reseq1d 5940 |
. . . . . . . . 9
β’ (π β ((π βf Β· π) βΎ π΅) = ((π₯ β π΄ β¦ ((πβπ₯) Β· (πβπ₯))) βΎ π΅)) |
94 | 7 | resmptd 5998 |
. . . . . . . . 9
β’ (π β ((π₯ β π΄ β¦ ((πβπ₯) Β· (πβπ₯))) βΎ π΅) = (π₯ β π΅ β¦ ((πβπ₯) Β· (πβπ₯)))) |
95 | 93, 94 | eqtrd 2773 |
. . . . . . . 8
β’ (π β ((π βf Β· π) βΎ π΅) = (π₯ β π΅ β¦ ((πβπ₯) Β· (πβπ₯)))) |
96 | 95 | oveq2d 7377 |
. . . . . . 7
β’ (π β (βfld
Ξ£g ((π βf Β· π) βΎ π΅)) = (βfld
Ξ£g (π₯ β π΅ β¦ ((πβπ₯) Β· (πβπ₯))))) |
97 | 96 | oveq1d 7376 |
. . . . . 6
β’ (π β ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) + ((πβπ§) Β· (πβπ§))) = ((βfld
Ξ£g (π₯ β π΅ β¦ ((πβπ₯) Β· (πβπ₯)))) + ((πβπ§) Β· (πβπ§)))) |
98 | 85, 92, 97 | 3eqtr4d 2783 |
. . . . 5
β’ (π β (βfld
Ξ£g ((π βf Β· π) βΎ (π΅ βͺ {π§}))) = ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) + ((πβπ§) Β· (πβπ§)))) |
99 | 98 | oveq1d 7376 |
. . . 4
β’ (π β ((βfld
Ξ£g ((π βf Β· π) βΎ (π΅ βͺ {π§}))) / πΏ) = (((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) + ((πβπ§) Β· (πβπ§))) / πΏ)) |
100 | 51 | recnd 11191 |
. . . . . 6
β’ (π β π β β) |
101 | 50 | rpne0d 12970 |
. . . . . 6
β’ (π β π β 0) |
102 | 29, 100, 57, 101, 66 | dmdcand 11968 |
. . . . 5
β’ (π β ((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) = ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / πΏ)) |
103 | 57, 100, 57, 66 | divsubdird 11978 |
. . . . . . . 8
β’ (π β ((πΏ β π) / πΏ) = ((πΏ / πΏ) β (π / πΏ))) |
104 | 100, 37, 49 | mvrladdd 11576 |
. . . . . . . . 9
β’ (π β (πΏ β π) = (πβπ§)) |
105 | 104 | oveq1d 7376 |
. . . . . . . 8
β’ (π β ((πΏ β π) / πΏ) = ((πβπ§) / πΏ)) |
106 | 57, 66 | dividd 11937 |
. . . . . . . . 9
β’ (π β (πΏ / πΏ) = 1) |
107 | 106 | oveq1d 7376 |
. . . . . . . 8
β’ (π β ((πΏ / πΏ) β (π / πΏ)) = (1 β (π / πΏ))) |
108 | 103, 105,
107 | 3eqtr3rd 2782 |
. . . . . . 7
β’ (π β (1 β (π / πΏ)) = ((πβπ§) / πΏ)) |
109 | 108 | oveq1d 7376 |
. . . . . 6
β’ (π β ((1 β (π / πΏ)) Β· (πβπ§)) = (((πβπ§) / πΏ) Β· (πβπ§))) |
110 | 37, 40, 57, 66 | div23d 11976 |
. . . . . 6
β’ (π β (((πβπ§) Β· (πβπ§)) / πΏ) = (((πβπ§) / πΏ) Β· (πβπ§))) |
111 | 109, 110 | eqtr4d 2776 |
. . . . 5
β’ (π β ((1 β (π / πΏ)) Β· (πβπ§)) = (((πβπ§) Β· (πβπ§)) / πΏ)) |
112 | 102, 111 | oveq12d 7379 |
. . . 4
β’ (π β (((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β (π / πΏ)) Β· (πβπ§))) = (((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / πΏ) + (((πβπ§) Β· (πβπ§)) / πΏ))) |
113 | 67, 99, 112 | 3eqtr4d 2783 |
. . 3
β’ (π β ((βfld
Ξ£g ((π βf Β· π) βΎ (π΅ βͺ {π§}))) / πΏ) = (((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β (π / πΏ)) Β· (πβπ§)))) |
114 | | jensenlem.4 |
. . . . 5
β’ (π β ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π) β π·) |
115 | 51, 56, 66 | redivcld 11991 |
. . . . . 6
β’ (π β (π / πΏ) β β) |
116 | 50 | rpge0d 12969 |
. . . . . . 7
β’ (π β 0 β€ π) |
117 | | divge0 12032 |
. . . . . . 7
β’ (((π β β β§ 0 β€
π) β§ (πΏ β β β§ 0 < πΏ)) β 0 β€ (π / πΏ)) |
118 | 51, 116, 56, 65, 117 | syl22anc 838 |
. . . . . 6
β’ (π β 0 β€ (π / πΏ)) |
119 | 57 | mulid1d 11180 |
. . . . . . . 8
β’ (π β (πΏ Β· 1) = πΏ) |
120 | 64, 119 | breqtrrd 5137 |
. . . . . . 7
β’ (π β π β€ (πΏ Β· 1)) |
121 | | 1red 11164 |
. . . . . . . 8
β’ (π β 1 β
β) |
122 | | ledivmul 12039 |
. . . . . . . 8
β’ ((π β β β§ 1 β
β β§ (πΏ β
β β§ 0 < πΏ))
β ((π / πΏ) β€ 1 β π β€ (πΏ Β· 1))) |
123 | 51, 121, 56, 65, 122 | syl112anc 1375 |
. . . . . . 7
β’ (π β ((π / πΏ) β€ 1 β π β€ (πΏ Β· 1))) |
124 | 120, 123 | mpbird 257 |
. . . . . 6
β’ (π β (π / πΏ) β€ 1) |
125 | | elicc01 13392 |
. . . . . 6
β’ ((π / πΏ) β (0[,]1) β ((π / πΏ) β β β§ 0 β€ (π / πΏ) β§ (π / πΏ) β€ 1)) |
126 | 115, 118,
124, 125 | syl3anbrc 1344 |
. . . . 5
β’ (π β (π / πΏ) β (0[,]1)) |
127 | 114, 38, 126 | 3jca 1129 |
. . . 4
β’ (π β (((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π) β π· β§ (πβπ§) β π· β§ (π / πΏ) β (0[,]1))) |
128 | 20, 43 | cvxcl 26357 |
. . . 4
β’ ((π β§ (((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π) β π· β§ (πβπ§) β π· β§ (π / πΏ) β (0[,]1))) β (((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β (π / πΏ)) Β· (πβπ§))) β π·) |
129 | 127, 128 | mpdan 686 |
. . 3
β’ (π β (((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β (π / πΏ)) Β· (πβπ§))) β π·) |
130 | 113, 129 | eqeltrd 2834 |
. 2
β’ (π β ((βfld
Ξ£g ((π βf Β· π) βΎ (π΅ βͺ {π§}))) / πΏ) β π·) |
131 | 42, 129 | ffvelcdmd 7040 |
. . . 4
β’ (π β (πΉβ(((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β (π / πΏ)) Β· (πβπ§)))) β β) |
132 | 42, 114 | ffvelcdmd 7040 |
. . . . . 6
β’ (π β (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) β β) |
133 | 115, 132 | remulcld 11193 |
. . . . 5
β’ (π β ((π / πΏ) Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) β β) |
134 | 42, 38 | ffvelcdmd 7040 |
. . . . . . 7
β’ (π β (πΉβ(πβπ§)) β β) |
135 | 54, 134 | remulcld 11193 |
. . . . . 6
β’ (π β ((πβπ§) Β· (πΉβ(πβπ§))) β β) |
136 | 135, 56, 66 | redivcld 11991 |
. . . . 5
β’ (π β (((πβπ§) Β· (πΉβ(πβπ§))) / πΏ) β β) |
137 | 133, 136 | readdcld 11192 |
. . . 4
β’ (π β (((π / πΏ) Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + (((πβπ§) Β· (πΉβ(πβπ§))) / πΏ)) β β) |
138 | | fco 6696 |
. . . . . . . . . . 11
β’ ((πΉ:π·βΆβ β§ π:π΄βΆπ·) β (πΉ β π):π΄βΆβ) |
139 | 42, 19, 138 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (πΉ β π):π΄βΆβ) |
140 | 14, 18, 139, 5, 5, 22 | off 7639 |
. . . . . . . . 9
β’ (π β (π βf Β· (πΉ β π)):π΄βΆβ) |
141 | 140, 7 | fssresd 6713 |
. . . . . . . 8
β’ (π β ((π βf Β· (πΉ β π)) βΎ π΅):π΅βΆβ) |
142 | 141, 8, 26 | fdmfifsupp 9323 |
. . . . . . . 8
β’ (π β ((π βf Β· (πΉ β π)) βΎ π΅) finSupp 0) |
143 | 1, 4, 8, 12, 141, 142 | gsumsubgcl 19705 |
. . . . . . 7
β’ (π β (βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) β β) |
144 | 143, 51, 101 | redivcld 11991 |
. . . . . 6
β’ (π β ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) / π) β β) |
145 | 115, 144 | remulcld 11193 |
. . . . 5
β’ (π β ((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) / π)) β β) |
146 | | 1re 11163 |
. . . . . . 7
β’ 1 β
β |
147 | | resubcl 11473 |
. . . . . . 7
β’ ((1
β β β§ (π /
πΏ) β β) β
(1 β (π / πΏ)) β
β) |
148 | 146, 115,
147 | sylancr 588 |
. . . . . 6
β’ (π β (1 β (π / πΏ)) β β) |
149 | 148, 134 | remulcld 11193 |
. . . . 5
β’ (π β ((1 β (π / πΏ)) Β· (πΉβ(πβπ§))) β β) |
150 | 145, 149 | readdcld 11192 |
. . . 4
β’ (π β (((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) / π)) + ((1 β (π / πΏ)) Β· (πΉβ(πβπ§)))) β β) |
151 | | oveq2 7369 |
. . . . . . . . . . 11
β’ (π₯ = ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π) β (π‘ Β· π₯) = (π‘ Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) |
152 | 151 | fvoveq1d 7383 |
. . . . . . . . . 10
β’ (π₯ = ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π) β (πΉβ((π‘ Β· π₯) + ((1 β π‘) Β· π¦))) = (πΉβ((π‘ Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β π‘) Β· π¦)))) |
153 | | fveq2 6846 |
. . . . . . . . . . . 12
β’ (π₯ = ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π) β (πΉβπ₯) = (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) |
154 | 153 | oveq2d 7377 |
. . . . . . . . . . 11
β’ (π₯ = ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π) β (π‘ Β· (πΉβπ₯)) = (π‘ Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)))) |
155 | 154 | oveq1d 7376 |
. . . . . . . . . 10
β’ (π₯ = ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π) β ((π‘ Β· (πΉβπ₯)) + ((1 β π‘) Β· (πΉβπ¦))) = ((π‘ Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + ((1 β π‘) Β· (πΉβπ¦)))) |
156 | 152, 155 | breq12d 5122 |
. . . . . . . . 9
β’ (π₯ = ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π) β ((πΉβ((π‘ Β· π₯) + ((1 β π‘) Β· π¦))) β€ ((π‘ Β· (πΉβπ₯)) + ((1 β π‘) Β· (πΉβπ¦))) β (πΉβ((π‘ Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β π‘) Β· π¦))) β€ ((π‘ Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + ((1 β π‘) Β· (πΉβπ¦))))) |
157 | 156 | imbi2d 341 |
. . . . . . . 8
β’ (π₯ = ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π) β ((π β (πΉβ((π‘ Β· π₯) + ((1 β π‘) Β· π¦))) β€ ((π‘ Β· (πΉβπ₯)) + ((1 β π‘) Β· (πΉβπ¦)))) β (π β (πΉβ((π‘ Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β π‘) Β· π¦))) β€ ((π‘ Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + ((1 β π‘) Β· (πΉβπ¦)))))) |
158 | | oveq2 7369 |
. . . . . . . . . . . 12
β’ (π¦ = (πβπ§) β ((1 β π‘) Β· π¦) = ((1 β π‘) Β· (πβπ§))) |
159 | 158 | oveq2d 7377 |
. . . . . . . . . . 11
β’ (π¦ = (πβπ§) β ((π‘ Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β π‘) Β· π¦)) = ((π‘ Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β π‘) Β· (πβπ§)))) |
160 | 159 | fveq2d 6850 |
. . . . . . . . . 10
β’ (π¦ = (πβπ§) β (πΉβ((π‘ Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β π‘) Β· π¦))) = (πΉβ((π‘ Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β π‘) Β· (πβπ§))))) |
161 | | fveq2 6846 |
. . . . . . . . . . . 12
β’ (π¦ = (πβπ§) β (πΉβπ¦) = (πΉβ(πβπ§))) |
162 | 161 | oveq2d 7377 |
. . . . . . . . . . 11
β’ (π¦ = (πβπ§) β ((1 β π‘) Β· (πΉβπ¦)) = ((1 β π‘) Β· (πΉβ(πβπ§)))) |
163 | 162 | oveq2d 7377 |
. . . . . . . . . 10
β’ (π¦ = (πβπ§) β ((π‘ Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + ((1 β π‘) Β· (πΉβπ¦))) = ((π‘ Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + ((1 β π‘) Β· (πΉβ(πβπ§))))) |
164 | 160, 163 | breq12d 5122 |
. . . . . . . . 9
β’ (π¦ = (πβπ§) β ((πΉβ((π‘ Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β π‘) Β· π¦))) β€ ((π‘ Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + ((1 β π‘) Β· (πΉβπ¦))) β (πΉβ((π‘ Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β π‘) Β· (πβπ§)))) β€ ((π‘ Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + ((1 β π‘) Β· (πΉβ(πβπ§)))))) |
165 | 164 | imbi2d 341 |
. . . . . . . 8
β’ (π¦ = (πβπ§) β ((π β (πΉβ((π‘ Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β π‘) Β· π¦))) β€ ((π‘ Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + ((1 β π‘) Β· (πΉβπ¦)))) β (π β (πΉβ((π‘ Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β π‘) Β· (πβπ§)))) β€ ((π‘ Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + ((1 β π‘) Β· (πΉβ(πβπ§))))))) |
166 | | oveq1 7368 |
. . . . . . . . . . . 12
β’ (π‘ = (π / πΏ) β (π‘ Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) = ((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) |
167 | | oveq2 7369 |
. . . . . . . . . . . . 13
β’ (π‘ = (π / πΏ) β (1 β π‘) = (1 β (π / πΏ))) |
168 | 167 | oveq1d 7376 |
. . . . . . . . . . . 12
β’ (π‘ = (π / πΏ) β ((1 β π‘) Β· (πβπ§)) = ((1 β (π / πΏ)) Β· (πβπ§))) |
169 | 166, 168 | oveq12d 7379 |
. . . . . . . . . . 11
β’ (π‘ = (π / πΏ) β ((π‘ Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β π‘) Β· (πβπ§))) = (((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β (π / πΏ)) Β· (πβπ§)))) |
170 | 169 | fveq2d 6850 |
. . . . . . . . . 10
β’ (π‘ = (π / πΏ) β (πΉβ((π‘ Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β π‘) Β· (πβπ§)))) = (πΉβ(((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β (π / πΏ)) Β· (πβπ§))))) |
171 | | oveq1 7368 |
. . . . . . . . . . 11
β’ (π‘ = (π / πΏ) β (π‘ Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) = ((π / πΏ) Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)))) |
172 | 167 | oveq1d 7376 |
. . . . . . . . . . 11
β’ (π‘ = (π / πΏ) β ((1 β π‘) Β· (πΉβ(πβπ§))) = ((1 β (π / πΏ)) Β· (πΉβ(πβπ§)))) |
173 | 171, 172 | oveq12d 7379 |
. . . . . . . . . 10
β’ (π‘ = (π / πΏ) β ((π‘ Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + ((1 β π‘) Β· (πΉβ(πβπ§)))) = (((π / πΏ) Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + ((1 β (π / πΏ)) Β· (πΉβ(πβπ§))))) |
174 | 170, 173 | breq12d 5122 |
. . . . . . . . 9
β’ (π‘ = (π / πΏ) β ((πΉβ((π‘ Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β π‘) Β· (πβπ§)))) β€ ((π‘ Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + ((1 β π‘) Β· (πΉβ(πβπ§)))) β (πΉβ(((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β (π / πΏ)) Β· (πβπ§)))) β€ (((π / πΏ) Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + ((1 β (π / πΏ)) Β· (πΉβ(πβπ§)))))) |
175 | 174 | imbi2d 341 |
. . . . . . . 8
β’ (π‘ = (π / πΏ) β ((π β (πΉβ((π‘ Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β π‘) Β· (πβπ§)))) β€ ((π‘ Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + ((1 β π‘) Β· (πΉβ(πβπ§))))) β (π β (πΉβ(((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β (π / πΏ)) Β· (πβπ§)))) β€ (((π / πΏ) Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + ((1 β (π / πΏ)) Β· (πΉβ(πβπ§))))))) |
176 | 45 | expcom 415 |
. . . . . . . 8
β’ ((π₯ β π· β§ π¦ β π· β§ π‘ β (0[,]1)) β (π β (πΉβ((π‘ Β· π₯) + ((1 β π‘) Β· π¦))) β€ ((π‘ Β· (πΉβπ₯)) + ((1 β π‘) Β· (πΉβπ¦))))) |
177 | 157, 165,
175, 176 | vtocl3ga 3540 |
. . . . . . 7
β’
((((βfld Ξ£g ((π βf Β· π) βΎ π΅)) / π) β π· β§ (πβπ§) β π· β§ (π / πΏ) β (0[,]1)) β (π β (πΉβ(((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β (π / πΏ)) Β· (πβπ§)))) β€ (((π / πΏ) Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + ((1 β (π / πΏ)) Β· (πΉβ(πβπ§)))))) |
178 | 114, 38, 126, 177 | syl3anc 1372 |
. . . . . 6
β’ (π β (π β (πΉβ(((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β (π / πΏ)) Β· (πβπ§)))) β€ (((π / πΏ) Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + ((1 β (π / πΏ)) Β· (πΉβ(πβπ§)))))) |
179 | 178 | pm2.43i 52 |
. . . . 5
β’ (π β (πΉβ(((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β (π / πΏ)) Β· (πβπ§)))) β€ (((π / πΏ) Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + ((1 β (π / πΏ)) Β· (πΉβ(πβπ§))))) |
180 | 108 | oveq1d 7376 |
. . . . . . 7
β’ (π β ((1 β (π / πΏ)) Β· (πΉβ(πβπ§))) = (((πβπ§) / πΏ) Β· (πΉβ(πβπ§)))) |
181 | 134 | recnd 11191 |
. . . . . . . 8
β’ (π β (πΉβ(πβπ§)) β β) |
182 | 37, 181, 57, 66 | div23d 11976 |
. . . . . . 7
β’ (π β (((πβπ§) Β· (πΉβ(πβπ§))) / πΏ) = (((πβπ§) / πΏ) Β· (πΉβ(πβπ§)))) |
183 | 180, 182 | eqtr4d 2776 |
. . . . . 6
β’ (π β ((1 β (π / πΏ)) Β· (πΉβ(πβπ§))) = (((πβπ§) Β· (πΉβ(πβπ§))) / πΏ)) |
184 | 183 | oveq2d 7377 |
. . . . 5
β’ (π β (((π / πΏ) Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + ((1 β (π / πΏ)) Β· (πΉβ(πβπ§)))) = (((π / πΏ) Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + (((πβπ§) Β· (πΉβ(πβπ§))) / πΏ))) |
185 | 179, 184 | breqtrd 5135 |
. . . 4
β’ (π β (πΉβ(((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β (π / πΏ)) Β· (πβπ§)))) β€ (((π / πΏ) Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + (((πβπ§) Β· (πΉβ(πβπ§))) / πΏ))) |
186 | 182, 180 | eqtr4d 2776 |
. . . . . 6
β’ (π β (((πβπ§) Β· (πΉβ(πβπ§))) / πΏ) = ((1 β (π / πΏ)) Β· (πΉβ(πβπ§)))) |
187 | 186 | oveq2d 7377 |
. . . . 5
β’ (π β (((π / πΏ) Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + (((πβπ§) Β· (πΉβ(πβπ§))) / πΏ)) = (((π / πΏ) Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + ((1 β (π / πΏ)) Β· (πΉβ(πβπ§))))) |
188 | | jensenlem.5 |
. . . . . . 7
β’ (π β (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) / π)) |
189 | 51, 56, 59, 65 | divgt0d 12098 |
. . . . . . . 8
β’ (π β 0 < (π / πΏ)) |
190 | | lemul2 12016 |
. . . . . . . 8
β’ (((πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) β β β§
((βfld Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) / π) β β β§ ((π / πΏ) β β β§ 0 < (π / πΏ))) β ((πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) / π) β ((π / πΏ) Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) β€ ((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) / π)))) |
191 | 132, 144,
115, 189, 190 | syl112anc 1375 |
. . . . . . 7
β’ (π β ((πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) / π) β ((π / πΏ) Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) β€ ((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) / π)))) |
192 | 188, 191 | mpbid 231 |
. . . . . 6
β’ (π β ((π / πΏ) Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) β€ ((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) / π))) |
193 | 133, 145,
149, 192 | leadd1dd 11777 |
. . . . 5
β’ (π β (((π / πΏ) Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + ((1 β (π / πΏ)) Β· (πΉβ(πβπ§)))) β€ (((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) / π)) + ((1 β (π / πΏ)) Β· (πΉβ(πβπ§))))) |
194 | 187, 193 | eqbrtrd 5131 |
. . . 4
β’ (π β (((π / πΏ) Β· (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π))) + (((πβπ§) Β· (πΉβ(πβπ§))) / πΏ)) β€ (((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) / π)) + ((1 β (π / πΏ)) Β· (πΉβ(πβπ§))))) |
195 | 131, 137,
150, 185, 194 | letrd 11320 |
. . 3
β’ (π β (πΉβ(((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β (π / πΏ)) Β· (πβπ§)))) β€ (((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) / π)) + ((1 β (π / πΏ)) Β· (πΉβ(πβπ§))))) |
196 | 113 | fveq2d 6850 |
. . 3
β’ (π β (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ (π΅ βͺ {π§}))) / πΏ)) = (πΉβ(((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· π) βΎ π΅)) / π)) + ((1 β (π / πΏ)) Β· (πβπ§))))) |
197 | 143 | recnd 11191 |
. . . . 5
β’ (π β (βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) β β) |
198 | 135 | recnd 11191 |
. . . . 5
β’ (π β ((πβπ§) Β· (πΉβ(πβπ§))) β β) |
199 | 197, 198,
57, 66 | divdird 11977 |
. . . 4
β’ (π β (((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) + ((πβπ§) Β· (πΉβ(πβπ§)))) / πΏ) = (((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) / πΏ) + (((πβπ§) Β· (πΉβ(πβπ§))) / πΏ))) |
200 | 16, 73 | sselid 3946 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (πβπ₯) β β) |
201 | 42 | ffvelcdmda 7039 |
. . . . . . . . . . 11
β’ ((π β§ (πβπ₯) β π·) β (πΉβ(πβπ₯)) β β) |
202 | 77, 201 | syldan 592 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (πΉβ(πβπ₯)) β β) |
203 | 200, 202 | remulcld 11193 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β ((πβπ₯) Β· (πΉβ(πβπ₯))) β β) |
204 | 203 | recnd 11191 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β ((πβπ₯) Β· (πΉβ(πβπ₯))) β β) |
205 | 72, 204 | syldan 592 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β ((πβπ₯) Β· (πΉβ(πβπ₯))) β β) |
206 | 83 | fveq2d 6850 |
. . . . . . . 8
β’ (π₯ = π§ β (πΉβ(πβπ₯)) = (πΉβ(πβπ§))) |
207 | 82, 206 | oveq12d 7379 |
. . . . . . 7
β’ (π₯ = π§ β ((πβπ₯) Β· (πΉβ(πβπ₯))) = ((πβπ§) Β· (πΉβ(πβπ§)))) |
208 | 68, 69, 71, 8, 205, 35, 46, 198, 207 | gsumunsn 19745 |
. . . . . 6
β’ (π β (βfld
Ξ£g (π₯ β (π΅ βͺ {π§}) β¦ ((πβπ₯) Β· (πΉβ(πβπ₯))))) = ((βfld
Ξ£g (π₯ β π΅ β¦ ((πβπ₯) Β· (πΉβ(πβπ₯))))) + ((πβπ§) Β· (πΉβ(πβπ§))))) |
209 | 42 | feqmptd 6914 |
. . . . . . . . . . 11
β’ (π β πΉ = (π¦ β π· β¦ (πΉβπ¦))) |
210 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π¦ = (πβπ₯) β (πΉβπ¦) = (πΉβ(πβπ₯))) |
211 | 77, 87, 209, 210 | fmptco 7079 |
. . . . . . . . . 10
β’ (π β (πΉ β π) = (π₯ β π΄ β¦ (πΉβ(πβπ₯)))) |
212 | 5, 73, 202, 86, 211 | offval2 7641 |
. . . . . . . . 9
β’ (π β (π βf Β· (πΉ β π)) = (π₯ β π΄ β¦ ((πβπ₯) Β· (πΉβ(πβπ₯))))) |
213 | 212 | reseq1d 5940 |
. . . . . . . 8
β’ (π β ((π βf Β· (πΉ β π)) βΎ (π΅ βͺ {π§})) = ((π₯ β π΄ β¦ ((πβπ₯) Β· (πΉβ(πβπ₯)))) βΎ (π΅ βͺ {π§}))) |
214 | 6 | resmptd 5998 |
. . . . . . . 8
β’ (π β ((π₯ β π΄ β¦ ((πβπ₯) Β· (πΉβ(πβπ₯)))) βΎ (π΅ βͺ {π§})) = (π₯ β (π΅ βͺ {π§}) β¦ ((πβπ₯) Β· (πΉβ(πβπ₯))))) |
215 | 213, 214 | eqtrd 2773 |
. . . . . . 7
β’ (π β ((π βf Β· (πΉ β π)) βΎ (π΅ βͺ {π§})) = (π₯ β (π΅ βͺ {π§}) β¦ ((πβπ₯) Β· (πΉβ(πβπ₯))))) |
216 | 215 | oveq2d 7377 |
. . . . . 6
β’ (π β (βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π΅ βͺ {π§}))) = (βfld
Ξ£g (π₯ β (π΅ βͺ {π§}) β¦ ((πβπ₯) Β· (πΉβ(πβπ₯)))))) |
217 | 212 | reseq1d 5940 |
. . . . . . . . 9
β’ (π β ((π βf Β· (πΉ β π)) βΎ π΅) = ((π₯ β π΄ β¦ ((πβπ₯) Β· (πΉβ(πβπ₯)))) βΎ π΅)) |
218 | 7 | resmptd 5998 |
. . . . . . . . 9
β’ (π β ((π₯ β π΄ β¦ ((πβπ₯) Β· (πΉβ(πβπ₯)))) βΎ π΅) = (π₯ β π΅ β¦ ((πβπ₯) Β· (πΉβ(πβπ₯))))) |
219 | 217, 218 | eqtrd 2773 |
. . . . . . . 8
β’ (π β ((π βf Β· (πΉ β π)) βΎ π΅) = (π₯ β π΅ β¦ ((πβπ₯) Β· (πΉβ(πβπ₯))))) |
220 | 219 | oveq2d 7377 |
. . . . . . 7
β’ (π β (βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) = (βfld
Ξ£g (π₯ β π΅ β¦ ((πβπ₯) Β· (πΉβ(πβπ₯)))))) |
221 | 220 | oveq1d 7376 |
. . . . . 6
β’ (π β ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) + ((πβπ§) Β· (πΉβ(πβπ§)))) = ((βfld
Ξ£g (π₯ β π΅ β¦ ((πβπ₯) Β· (πΉβ(πβπ₯))))) + ((πβπ§) Β· (πΉβ(πβπ§))))) |
222 | 208, 216,
221 | 3eqtr4d 2783 |
. . . . 5
β’ (π β (βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π΅ βͺ {π§}))) = ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) + ((πβπ§) Β· (πΉβ(πβπ§))))) |
223 | 222 | oveq1d 7376 |
. . . 4
β’ (π β ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π΅ βͺ {π§}))) / πΏ) = (((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) + ((πβπ§) Β· (πΉβ(πβπ§)))) / πΏ)) |
224 | 197, 100,
57, 101, 66 | dmdcand 11968 |
. . . . 5
β’ (π β ((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) / π)) = ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) / πΏ)) |
225 | 224, 183 | oveq12d 7379 |
. . . 4
β’ (π β (((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) / π)) + ((1 β (π / πΏ)) Β· (πΉβ(πβπ§)))) = (((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) / πΏ) + (((πβπ§) Β· (πΉβ(πβπ§))) / πΏ))) |
226 | 199, 223,
225 | 3eqtr4d 2783 |
. . 3
β’ (π β ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π΅ βͺ {π§}))) / πΏ) = (((π / πΏ) Β· ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΅)) / π)) + ((1 β (π / πΏ)) Β· (πΉβ(πβπ§))))) |
227 | 195, 196,
226 | 3brtr4d 5141 |
. 2
β’ (π β (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ (π΅ βͺ {π§}))) / πΏ)) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π΅ βͺ {π§}))) / πΏ)) |
228 | 130, 227 | jca 513 |
1
β’ (π β (((βfld
Ξ£g ((π βf Β· π) βΎ (π΅ βͺ {π§}))) / πΏ) β π· β§ (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ (π΅ βͺ {π§}))) / πΏ)) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π΅ βͺ {π§}))) / πΏ))) |