Step | Hyp | Ref
| Expression |
1 | | intlewftc.4 |
. . . . . 6
β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) |
2 | | cncff 24272 |
. . . . . 6
β’ (πΉ β ((π΄[,]π΅)βcnββ) β πΉ:(π΄[,]π΅)βΆβ) |
3 | 1, 2 | syl 17 |
. . . . 5
β’ (π β πΉ:(π΄[,]π΅)βΆβ) |
4 | | intlewftc.2 |
. . . . . . 7
β’ (π β π΅ β β) |
5 | | intlewftc.3 |
. . . . . . 7
β’ (π β π΄ β€ π΅) |
6 | 4 | leidd 11726 |
. . . . . . 7
β’ (π β π΅ β€ π΅) |
7 | 4, 5, 6 | 3jca 1129 |
. . . . . 6
β’ (π β (π΅ β β β§ π΄ β€ π΅ β§ π΅ β€ π΅)) |
8 | | intlewftc.1 |
. . . . . . 7
β’ (π β π΄ β β) |
9 | | elicc2 13335 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β) β (π΅ β (π΄[,]π΅) β (π΅ β β β§ π΄ β€ π΅ β§ π΅ β€ π΅))) |
10 | 8, 4, 9 | syl2anc 585 |
. . . . . 6
β’ (π β (π΅ β (π΄[,]π΅) β (π΅ β β β§ π΄ β€ π΅ β§ π΅ β€ π΅))) |
11 | 7, 10 | mpbird 257 |
. . . . 5
β’ (π β π΅ β (π΄[,]π΅)) |
12 | 3, 11 | ffvelcdmd 7037 |
. . . 4
β’ (π β (πΉβπ΅) β β) |
13 | 8 | leidd 11726 |
. . . . . . 7
β’ (π β π΄ β€ π΄) |
14 | 8, 13, 5 | 3jca 1129 |
. . . . . 6
β’ (π β (π΄ β β β§ π΄ β€ π΄ β§ π΄ β€ π΅)) |
15 | | elicc2 13335 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β) β (π΄ β (π΄[,]π΅) β (π΄ β β β§ π΄ β€ π΄ β§ π΄ β€ π΅))) |
16 | 8, 4, 15 | syl2anc 585 |
. . . . . 6
β’ (π β (π΄ β (π΄[,]π΅) β (π΄ β β β§ π΄ β€ π΄ β§ π΄ β€ π΅))) |
17 | 14, 16 | mpbird 257 |
. . . . 5
β’ (π β π΄ β (π΄[,]π΅)) |
18 | 3, 17 | ffvelcdmd 7037 |
. . . 4
β’ (π β (πΉβπ΄) β β) |
19 | 12, 18 | resubcld 11588 |
. . 3
β’ (π β ((πΉβπ΅) β (πΉβπ΄)) β β) |
20 | | intlewftc.5 |
. . . . . 6
β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) |
21 | | cncff 24272 |
. . . . . 6
β’ (πΊ β ((π΄[,]π΅)βcnββ) β πΊ:(π΄[,]π΅)βΆβ) |
22 | 20, 21 | syl 17 |
. . . . 5
β’ (π β πΊ:(π΄[,]π΅)βΆβ) |
23 | 22, 11 | ffvelcdmd 7037 |
. . . 4
β’ (π β (πΊβπ΅) β β) |
24 | 22, 17 | ffvelcdmd 7037 |
. . . 4
β’ (π β (πΊβπ΄) β β) |
25 | 23, 24 | resubcld 11588 |
. . 3
β’ (π β ((πΊβπ΅) β (πΊβπ΄)) β β) |
26 | | intlewftc.10 |
. . . . . 6
β’ (π β π· β
πΏ1) |
27 | | intlewftc.12 |
. . . . . . 7
β’ (π β π· = (π₯ β (π΄(,)π΅) β¦ π)) |
28 | 27 | eleq1d 2819 |
. . . . . 6
β’ (π β (π· β πΏ1 β (π₯ β (π΄(,)π΅) β¦ π) β
πΏ1)) |
29 | 26, 28 | mpbid 231 |
. . . . 5
β’ (π β (π₯ β (π΄(,)π΅) β¦ π) β
πΏ1) |
30 | | intlewftc.11 |
. . . . . 6
β’ (π β πΈ β
πΏ1) |
31 | | intlewftc.13 |
. . . . . . 7
β’ (π β πΈ = (π₯ β (π΄(,)π΅) β¦ π)) |
32 | 31 | eleq1d 2819 |
. . . . . 6
β’ (π β (πΈ β πΏ1 β (π₯ β (π΄(,)π΅) β¦ π) β
πΏ1)) |
33 | 30, 32 | mpbid 231 |
. . . . 5
β’ (π β (π₯ β (π΄(,)π΅) β¦ π) β
πΏ1) |
34 | | intlewftc.8 |
. . . . . . . 8
β’ (π β π· β ((π΄(,)π΅)βcnββ)) |
35 | | cncff 24272 |
. . . . . . . 8
β’ (π· β ((π΄(,)π΅)βcnββ) β π·:(π΄(,)π΅)βΆβ) |
36 | 34, 35 | syl 17 |
. . . . . . 7
β’ (π β π·:(π΄(,)π΅)βΆβ) |
37 | 27 | feq1d 6654 |
. . . . . . 7
β’ (π β (π·:(π΄(,)π΅)βΆβ β (π₯ β (π΄(,)π΅) β¦ π):(π΄(,)π΅)βΆβ)) |
38 | 36, 37 | mpbid 231 |
. . . . . 6
β’ (π β (π₯ β (π΄(,)π΅) β¦ π):(π΄(,)π΅)βΆβ) |
39 | 38 | fvmptelcdm 7062 |
. . . . 5
β’ ((π β§ π₯ β (π΄(,)π΅)) β π β β) |
40 | | intlewftc.9 |
. . . . . . . 8
β’ (π β πΈ β ((π΄(,)π΅)βcnββ)) |
41 | | cncff 24272 |
. . . . . . . 8
β’ (πΈ β ((π΄(,)π΅)βcnββ) β πΈ:(π΄(,)π΅)βΆβ) |
42 | 40, 41 | syl 17 |
. . . . . . 7
β’ (π β πΈ:(π΄(,)π΅)βΆβ) |
43 | 31 | feq1d 6654 |
. . . . . . 7
β’ (π β (πΈ:(π΄(,)π΅)βΆβ β (π₯ β (π΄(,)π΅) β¦ π):(π΄(,)π΅)βΆβ)) |
44 | 42, 43 | mpbid 231 |
. . . . . 6
β’ (π β (π₯ β (π΄(,)π΅) β¦ π):(π΄(,)π΅)βΆβ) |
45 | 44 | fvmptelcdm 7062 |
. . . . 5
β’ ((π β§ π₯ β (π΄(,)π΅)) β π β β) |
46 | | intlewftc.14 |
. . . . 5
β’ ((π β§ π₯ β (π΄(,)π΅)) β π β€ π) |
47 | 29, 33, 39, 45, 46 | itgle 25190 |
. . . 4
β’ (π β β«(π΄(,)π΅)π dπ₯ β€ β«(π΄(,)π΅)π dπ₯) |
48 | 39 | itgmpt 25163 |
. . . . . 6
β’ (π β β«(π΄(,)π΅)π dπ₯ = β«(π΄(,)π΅)((π₯ β (π΄(,)π΅) β¦ π)βπ‘) dπ‘) |
49 | 27 | fveq1d 6845 |
. . . . . . . . . 10
β’ (π β (π·βπ‘) = ((π₯ β (π΄(,)π΅) β¦ π)βπ‘)) |
50 | 49 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π‘ β (π΄(,)π΅)) β (π·βπ‘) = ((π₯ β (π΄(,)π΅) β¦ π)βπ‘)) |
51 | 50 | eqcomd 2739 |
. . . . . . . 8
β’ ((π β§ π‘ β (π΄(,)π΅)) β ((π₯ β (π΄(,)π΅) β¦ π)βπ‘) = (π·βπ‘)) |
52 | 51 | itgeq2dv 25162 |
. . . . . . 7
β’ (π β β«(π΄(,)π΅)((π₯ β (π΄(,)π΅) β¦ π)βπ‘) dπ‘ = β«(π΄(,)π΅)(π·βπ‘) dπ‘) |
53 | | intlewftc.6 |
. . . . . . . . . . 11
β’ (π β π· = (β D πΉ)) |
54 | 53 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π‘ β (π΄(,)π΅)) β π· = (β D πΉ)) |
55 | 54 | fveq1d 6845 |
. . . . . . . . 9
β’ ((π β§ π‘ β (π΄(,)π΅)) β (π·βπ‘) = ((β D πΉ)βπ‘)) |
56 | 55 | itgeq2dv 25162 |
. . . . . . . 8
β’ (π β β«(π΄(,)π΅)(π·βπ‘) dπ‘ = β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘) |
57 | | ax-resscn 11113 |
. . . . . . . . . . . . 13
β’ β
β β |
58 | 57 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β β
β) |
59 | | fss 6686 |
. . . . . . . . . . . 12
β’ ((π·:(π΄(,)π΅)βΆβ β§ β β
β) β π·:(π΄(,)π΅)βΆβ) |
60 | 36, 58, 59 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β π·:(π΄(,)π΅)βΆβ) |
61 | | ssidd 3968 |
. . . . . . . . . . . 12
β’ (π β β β
β) |
62 | | cncfcdm 24277 |
. . . . . . . . . . . 12
β’ ((β
β β β§ π·
β ((π΄(,)π΅)βcnββ)) β (π· β ((π΄(,)π΅)βcnββ) β π·:(π΄(,)π΅)βΆβ)) |
63 | 61, 34, 62 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (π· β ((π΄(,)π΅)βcnββ) β π·:(π΄(,)π΅)βΆβ)) |
64 | 60, 63 | mpbird 257 |
. . . . . . . . . 10
β’ (π β π· β ((π΄(,)π΅)βcnββ)) |
65 | 53 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π β (π· β ((π΄(,)π΅)βcnββ) β (β D πΉ) β ((π΄(,)π΅)βcnββ))) |
66 | 64, 65 | mpbid 231 |
. . . . . . . . 9
β’ (π β (β D πΉ) β ((π΄(,)π΅)βcnββ)) |
67 | 53, 26 | eqeltrrd 2835 |
. . . . . . . . 9
β’ (π β (β D πΉ) β
πΏ1) |
68 | | fss 6686 |
. . . . . . . . . . 11
β’ ((πΉ:(π΄[,]π΅)βΆβ β§ β β
β) β πΉ:(π΄[,]π΅)βΆβ) |
69 | 3, 58, 68 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β πΉ:(π΄[,]π΅)βΆβ) |
70 | | cncfcdm 24277 |
. . . . . . . . . . 11
β’ ((β
β β β§ πΉ
β ((π΄[,]π΅)βcnββ)) β (πΉ β ((π΄[,]π΅)βcnββ) β πΉ:(π΄[,]π΅)βΆβ)) |
71 | 61, 1, 70 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (πΉ β ((π΄[,]π΅)βcnββ) β πΉ:(π΄[,]π΅)βΆβ)) |
72 | 69, 71 | mpbird 257 |
. . . . . . . . 9
β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) |
73 | 8, 4, 5, 66, 67, 72 | ftc2 25424 |
. . . . . . . 8
β’ (π β β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘ = ((πΉβπ΅) β (πΉβπ΄))) |
74 | 56, 73 | eqtrd 2773 |
. . . . . . 7
β’ (π β β«(π΄(,)π΅)(π·βπ‘) dπ‘ = ((πΉβπ΅) β (πΉβπ΄))) |
75 | 52, 74 | eqtrd 2773 |
. . . . . 6
β’ (π β β«(π΄(,)π΅)((π₯ β (π΄(,)π΅) β¦ π)βπ‘) dπ‘ = ((πΉβπ΅) β (πΉβπ΄))) |
76 | 48, 75 | eqtrd 2773 |
. . . . 5
β’ (π β β«(π΄(,)π΅)π dπ₯ = ((πΉβπ΅) β (πΉβπ΄))) |
77 | 45 | itgmpt 25163 |
. . . . . . 7
β’ (π β β«(π΄(,)π΅)π dπ₯ = β«(π΄(,)π΅)((π₯ β (π΄(,)π΅) β¦ π)βπ‘) dπ‘) |
78 | 31 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π‘ β (π΄(,)π΅)) β πΈ = (π₯ β (π΄(,)π΅) β¦ π)) |
79 | 78 | eqcomd 2739 |
. . . . . . . . 9
β’ ((π β§ π‘ β (π΄(,)π΅)) β (π₯ β (π΄(,)π΅) β¦ π) = πΈ) |
80 | 79 | fveq1d 6845 |
. . . . . . . 8
β’ ((π β§ π‘ β (π΄(,)π΅)) β ((π₯ β (π΄(,)π΅) β¦ π)βπ‘) = (πΈβπ‘)) |
81 | 80 | itgeq2dv 25162 |
. . . . . . 7
β’ (π β β«(π΄(,)π΅)((π₯ β (π΄(,)π΅) β¦ π)βπ‘) dπ‘ = β«(π΄(,)π΅)(πΈβπ‘) dπ‘) |
82 | 77, 81 | eqtrd 2773 |
. . . . . 6
β’ (π β β«(π΄(,)π΅)π dπ₯ = β«(π΄(,)π΅)(πΈβπ‘) dπ‘) |
83 | | intlewftc.7 |
. . . . . . . . . 10
β’ (π β πΈ = (β D πΊ)) |
84 | 83 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π‘ β (π΄(,)π΅)) β πΈ = (β D πΊ)) |
85 | 84 | fveq1d 6845 |
. . . . . . . 8
β’ ((π β§ π‘ β (π΄(,)π΅)) β (πΈβπ‘) = ((β D πΊ)βπ‘)) |
86 | 85 | itgeq2dv 25162 |
. . . . . . 7
β’ (π β β«(π΄(,)π΅)(πΈβπ‘) dπ‘ = β«(π΄(,)π΅)((β D πΊ)βπ‘) dπ‘) |
87 | | fss 6686 |
. . . . . . . . . . . . 13
β’ ((πΈ:(π΄(,)π΅)βΆβ β§ β β
β) β πΈ:(π΄(,)π΅)βΆβ) |
88 | 42, 58, 87 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β πΈ:(π΄(,)π΅)βΆβ) |
89 | | cncfcdm 24277 |
. . . . . . . . . . . . 13
β’ ((β
β β β§ πΈ
β ((π΄(,)π΅)βcnββ)) β (πΈ β ((π΄(,)π΅)βcnββ) β πΈ:(π΄(,)π΅)βΆβ)) |
90 | 61, 40, 89 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (πΈ β ((π΄(,)π΅)βcnββ) β πΈ:(π΄(,)π΅)βΆβ)) |
91 | 88, 90 | mpbird 257 |
. . . . . . . . . . 11
β’ (π β πΈ β ((π΄(,)π΅)βcnββ)) |
92 | 83 | eleq1d 2819 |
. . . . . . . . . . 11
β’ (π β (πΈ β ((π΄(,)π΅)βcnββ) β (β D πΊ) β ((π΄(,)π΅)βcnββ))) |
93 | 91, 92 | mpbid 231 |
. . . . . . . . . 10
β’ (π β (β D πΊ) β ((π΄(,)π΅)βcnββ)) |
94 | 93, 92 | mpbird 257 |
. . . . . . . . 9
β’ (π β πΈ β ((π΄(,)π΅)βcnββ)) |
95 | 94, 92 | mpbid 231 |
. . . . . . . 8
β’ (π β (β D πΊ) β ((π΄(,)π΅)βcnββ)) |
96 | 83, 30 | eqeltrrd 2835 |
. . . . . . . 8
β’ (π β (β D πΊ) β
πΏ1) |
97 | | fss 6686 |
. . . . . . . . . 10
β’ ((πΊ:(π΄[,]π΅)βΆβ β§ β β
β) β πΊ:(π΄[,]π΅)βΆβ) |
98 | 22, 58, 97 | syl2anc 585 |
. . . . . . . . 9
β’ (π β πΊ:(π΄[,]π΅)βΆβ) |
99 | | cncfcdm 24277 |
. . . . . . . . . 10
β’ ((β
β β β§ πΊ
β ((π΄[,]π΅)βcnββ)) β (πΊ β ((π΄[,]π΅)βcnββ) β πΊ:(π΄[,]π΅)βΆβ)) |
100 | 61, 20, 99 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (πΊ β ((π΄[,]π΅)βcnββ) β πΊ:(π΄[,]π΅)βΆβ)) |
101 | 98, 100 | mpbird 257 |
. . . . . . . 8
β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) |
102 | 8, 4, 5, 95, 96, 101 | ftc2 25424 |
. . . . . . 7
β’ (π β β«(π΄(,)π΅)((β D πΊ)βπ‘) dπ‘ = ((πΊβπ΅) β (πΊβπ΄))) |
103 | 86, 102 | eqtrd 2773 |
. . . . . 6
β’ (π β β«(π΄(,)π΅)(πΈβπ‘) dπ‘ = ((πΊβπ΅) β (πΊβπ΄))) |
104 | 82, 103 | eqtrd 2773 |
. . . . 5
β’ (π β β«(π΄(,)π΅)π dπ₯ = ((πΊβπ΅) β (πΊβπ΄))) |
105 | 76, 104 | breq12d 5119 |
. . . 4
β’ (π β (β«(π΄(,)π΅)π dπ₯ β€ β«(π΄(,)π΅)π dπ₯ β ((πΉβπ΅) β (πΉβπ΄)) β€ ((πΊβπ΅) β (πΊβπ΄)))) |
106 | 47, 105 | mpbid 231 |
. . 3
β’ (π β ((πΉβπ΅) β (πΉβπ΄)) β€ ((πΊβπ΅) β (πΊβπ΄))) |
107 | | intlewftc.15 |
. . 3
β’ (π β (πΉβπ΄) β€ (πΊβπ΄)) |
108 | 19, 18, 25, 24, 106, 107 | le2addd 11779 |
. 2
β’ (π β (((πΉβπ΅) β (πΉβπ΄)) + (πΉβπ΄)) β€ (((πΊβπ΅) β (πΊβπ΄)) + (πΊβπ΄))) |
109 | 57, 12 | sselid 3943 |
. . . 4
β’ (π β (πΉβπ΅) β β) |
110 | 57, 18 | sselid 3943 |
. . . 4
β’ (π β (πΉβπ΄) β β) |
111 | 109, 110 | npcand 11521 |
. . 3
β’ (π β (((πΉβπ΅) β (πΉβπ΄)) + (πΉβπ΄)) = (πΉβπ΅)) |
112 | 57, 23 | sselid 3943 |
. . . 4
β’ (π β (πΊβπ΅) β β) |
113 | 57, 24 | sselid 3943 |
. . . 4
β’ (π β (πΊβπ΄) β β) |
114 | 112, 113 | npcand 11521 |
. . 3
β’ (π β (((πΊβπ΅) β (πΊβπ΄)) + (πΊβπ΄)) = (πΊβπ΅)) |
115 | 111, 114 | breq12d 5119 |
. 2
β’ (π β ((((πΉβπ΅) β (πΉβπ΄)) + (πΉβπ΄)) β€ (((πΊβπ΅) β (πΊβπ΄)) + (πΊβπ΄)) β (πΉβπ΅) β€ (πΊβπ΅))) |
116 | 108, 115 | mpbid 231 |
1
β’ (π β (πΉβπ΅) β€ (πΊβπ΅)) |