Step | Hyp | Ref
| Expression |
1 | | dvfsum.s |
. . . 4
β’ π = (π(,)+β) |
2 | | ioossre 13334 |
. . . 4
β’ (π(,)+β) β
β |
3 | 1, 2 | eqsstri 3982 |
. . 3
β’ π β
β |
4 | | dvfsumlem1.2 |
. . 3
β’ (π β π β π) |
5 | 3, 4 | sselid 3946 |
. 2
β’ (π β π β β) |
6 | | dvfsumlem1.1 |
. . . 4
β’ (π β π β π) |
7 | 3, 6 | sselid 3946 |
. . 3
β’ (π β π β β) |
8 | | reflcl 13710 |
. . 3
β’ (π β β β
(ββπ) β
β) |
9 | | peano2re 11336 |
. . 3
β’
((ββπ)
β β β ((ββπ) + 1) β β) |
10 | 7, 8, 9 | 3syl 18 |
. 2
β’ (π β ((ββπ) + 1) β
β) |
11 | | dvfsum.z |
. . 3
β’ π =
(β€β₯βπ) |
12 | | dvfsum.m |
. . . 4
β’ (π β π β β€) |
13 | 12 | adantr 482 |
. . 3
β’ ((π β§ π β€ ((ββπ) + 1)) β π β β€) |
14 | | dvfsum.d |
. . . 4
β’ (π β π· β β) |
15 | 14 | adantr 482 |
. . 3
β’ ((π β§ π β€ ((ββπ) + 1)) β π· β β) |
16 | | dvfsum.md |
. . . 4
β’ (π β π β€ (π· + 1)) |
17 | 16 | adantr 482 |
. . 3
β’ ((π β§ π β€ ((ββπ) + 1)) β π β€ (π· + 1)) |
18 | | dvfsum.t |
. . . 4
β’ (π β π β β) |
19 | 18 | adantr 482 |
. . 3
β’ ((π β§ π β€ ((ββπ) + 1)) β π β β) |
20 | | dvfsum.a |
. . . 4
β’ ((π β§ π₯ β π) β π΄ β β) |
21 | 20 | adantlr 714 |
. . 3
β’ (((π β§ π β€ ((ββπ) + 1)) β§ π₯ β π) β π΄ β β) |
22 | | dvfsum.b1 |
. . . 4
β’ ((π β§ π₯ β π) β π΅ β π) |
23 | 22 | adantlr 714 |
. . 3
β’ (((π β§ π β€ ((ββπ) + 1)) β§ π₯ β π) β π΅ β π) |
24 | | dvfsum.b2 |
. . . 4
β’ ((π β§ π₯ β π) β π΅ β β) |
25 | 24 | adantlr 714 |
. . 3
β’ (((π β§ π β€ ((ββπ) + 1)) β§ π₯ β π) β π΅ β β) |
26 | | dvfsum.b3 |
. . . 4
β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) |
27 | 26 | adantr 482 |
. . 3
β’ ((π β§ π β€ ((ββπ) + 1)) β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) |
28 | | dvfsum.c |
. . 3
β’ (π₯ = π β π΅ = πΆ) |
29 | | dvfsum.u |
. . . 4
β’ (π β π β
β*) |
30 | 29 | adantr 482 |
. . 3
β’ ((π β§ π β€ ((ββπ) + 1)) β π β
β*) |
31 | | dvfsum.l |
. . . 4
β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ π)) β πΆ β€ π΅) |
32 | 31 | 3adant1r 1178 |
. . 3
β’ (((π β§ π β€ ((ββπ) + 1)) β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ π)) β πΆ β€ π΅) |
33 | | dvfsum.h |
. . 3
β’ π» = (π₯ β π β¦ (((π₯ β (ββπ₯)) Β· π΅) + (Ξ£π β (π...(ββπ₯))πΆ β π΄))) |
34 | 6 | adantr 482 |
. . 3
β’ ((π β§ π β€ ((ββπ) + 1)) β π β π) |
35 | 4 | adantr 482 |
. . 3
β’ ((π β§ π β€ ((ββπ) + 1)) β π β π) |
36 | | dvfsumlem1.3 |
. . . 4
β’ (π β π· β€ π) |
37 | 36 | adantr 482 |
. . 3
β’ ((π β§ π β€ ((ββπ) + 1)) β π· β€ π) |
38 | | dvfsumlem1.4 |
. . . 4
β’ (π β π β€ π) |
39 | 38 | adantr 482 |
. . 3
β’ ((π β§ π β€ ((ββπ) + 1)) β π β€ π) |
40 | | dvfsumlem1.5 |
. . . 4
β’ (π β π β€ π) |
41 | 40 | adantr 482 |
. . 3
β’ ((π β§ π β€ ((ββπ) + 1)) β π β€ π) |
42 | | simpr 486 |
. . 3
β’ ((π β§ π β€ ((ββπ) + 1)) β π β€ ((ββπ) + 1)) |
43 | 1, 11, 13, 15, 17, 19, 21, 23, 25, 27, 28, 30, 32, 33, 34, 35, 37, 39, 41, 42 | dvfsumlem2 25414 |
. 2
β’ ((π β§ π β€ ((ββπ) + 1)) β ((π»βπ) β€ (π»βπ) β§ ((π»βπ) β β¦π / π₯β¦π΅) β€ ((π»βπ) β β¦π / π₯β¦π΅))) |
44 | 3 | a1i 11 |
. . . . . . . . . . 11
β’ (π β π β β) |
45 | 44 | sselda 3948 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β π₯ β β) |
46 | | reflcl 13710 |
. . . . . . . . . . 11
β’ (π₯ β β β
(ββπ₯) β
β) |
47 | 45, 46 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β (ββπ₯) β β) |
48 | 45, 47 | resubcld 11591 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β (π₯ β (ββπ₯)) β β) |
49 | 44, 20, 22, 26 | dvmptrecl 25411 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β π΅ β β) |
50 | 48, 49 | remulcld 11193 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β ((π₯ β (ββπ₯)) Β· π΅) β β) |
51 | | fzfid 13887 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β (π...(ββπ₯)) β Fin) |
52 | 24 | ralrimiva 3140 |
. . . . . . . . . . . 12
β’ (π β βπ₯ β π π΅ β β) |
53 | 52 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β βπ₯ β π π΅ β β) |
54 | | elfzuz 13446 |
. . . . . . . . . . . 12
β’ (π β (π...(ββπ₯)) β π β (β€β₯βπ)) |
55 | 54, 11 | eleqtrrdi 2845 |
. . . . . . . . . . 11
β’ (π β (π...(ββπ₯)) β π β π) |
56 | 28 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π΅ β β β πΆ β β)) |
57 | 56 | rspccva 3582 |
. . . . . . . . . . 11
β’
((βπ₯ β
π π΅ β β β§ π β π) β πΆ β β) |
58 | 53, 55, 57 | syl2an 597 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π β (π...(ββπ₯))) β πΆ β β) |
59 | 51, 58 | fsumrecl 15627 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β Ξ£π β (π...(ββπ₯))πΆ β β) |
60 | 59, 20 | resubcld 11591 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (Ξ£π β (π...(ββπ₯))πΆ β π΄) β β) |
61 | 50, 60 | readdcld 11192 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (((π₯ β (ββπ₯)) Β· π΅) + (Ξ£π β (π...(ββπ₯))πΆ β π΄)) β β) |
62 | 61, 33 | fmptd 7066 |
. . . . . 6
β’ (π β π»:πβΆβ) |
63 | 62 | adantr 482 |
. . . . 5
β’ ((π β§ ((ββπ) + 1) β€ π) β π»:πβΆβ) |
64 | 4 | adantr 482 |
. . . . 5
β’ ((π β§ ((ββπ) + 1) β€ π) β π β π) |
65 | 63, 64 | ffvelcdmd 7040 |
. . . 4
β’ ((π β§ ((ββπ) + 1) β€ π) β (π»βπ) β β) |
66 | 5 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((ββπ) + 1) β€ π) β π β β) |
67 | | reflcl 13710 |
. . . . . . . 8
β’ (π β β β
(ββπ) β
β) |
68 | 66, 67 | syl 17 |
. . . . . . 7
β’ ((π β§ ((ββπ) + 1) β€ π) β (ββπ) β β) |
69 | 18 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((ββπ) + 1) β€ π) β π β β) |
70 | 7 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ ((ββπ) + 1) β€ π) β π β β) |
71 | 70, 8, 9 | 3syl 18 |
. . . . . . . 8
β’ ((π β§ ((ββπ) + 1) β€ π) β ((ββπ) + 1) β β) |
72 | 6, 1 | eleqtrdi 2844 |
. . . . . . . . . . . 12
β’ (π β π β (π(,)+β)) |
73 | 18 | rexrd 11213 |
. . . . . . . . . . . . 13
β’ (π β π β
β*) |
74 | | elioopnf 13369 |
. . . . . . . . . . . . 13
β’ (π β β*
β (π β (π(,)+β) β (π β β β§ π < π))) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π β (π(,)+β) β (π β β β§ π < π))) |
76 | 72, 75 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β (π β β β§ π < π)) |
77 | 76 | simprd 497 |
. . . . . . . . . 10
β’ (π β π < π) |
78 | | fllep1 13715 |
. . . . . . . . . . 11
β’ (π β β β π β€ ((ββπ) + 1)) |
79 | 7, 78 | syl 17 |
. . . . . . . . . 10
β’ (π β π β€ ((ββπ) + 1)) |
80 | 18, 7, 10, 77, 79 | ltletrd 11323 |
. . . . . . . . 9
β’ (π β π < ((ββπ) + 1)) |
81 | 80 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((ββπ) + 1) β€ π) β π < ((ββπ) + 1)) |
82 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ ((ββπ) + 1) β€ π) β ((ββπ) + 1) β€ π) |
83 | 70 | flcld 13712 |
. . . . . . . . . . 11
β’ ((π β§ ((ββπ) + 1) β€ π) β (ββπ) β β€) |
84 | 83 | peano2zd 12618 |
. . . . . . . . . 10
β’ ((π β§ ((ββπ) + 1) β€ π) β ((ββπ) + 1) β β€) |
85 | | flge 13719 |
. . . . . . . . . 10
β’ ((π β β β§
((ββπ) + 1)
β β€) β (((ββπ) + 1) β€ π β ((ββπ) + 1) β€ (ββπ))) |
86 | 66, 84, 85 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ ((ββπ) + 1) β€ π) β (((ββπ) + 1) β€ π β ((ββπ) + 1) β€ (ββπ))) |
87 | 82, 86 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ ((ββπ) + 1) β€ π) β ((ββπ) + 1) β€ (ββπ)) |
88 | 69, 71, 68, 81, 87 | ltletrd 11323 |
. . . . . . 7
β’ ((π β§ ((ββπ) + 1) β€ π) β π < (ββπ)) |
89 | 73 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((ββπ) + 1) β€ π) β π β
β*) |
90 | | elioopnf 13369 |
. . . . . . . 8
β’ (π β β*
β ((ββπ)
β (π(,)+β)
β ((ββπ)
β β β§ π <
(ββπ)))) |
91 | 89, 90 | syl 17 |
. . . . . . 7
β’ ((π β§ ((ββπ) + 1) β€ π) β ((ββπ) β (π(,)+β) β ((ββπ) β β β§ π < (ββπ)))) |
92 | 68, 88, 91 | mpbir2and 712 |
. . . . . 6
β’ ((π β§ ((ββπ) + 1) β€ π) β (ββπ) β (π(,)+β)) |
93 | 92, 1 | eleqtrrdi 2845 |
. . . . 5
β’ ((π β§ ((ββπ) + 1) β€ π) β (ββπ) β π) |
94 | 63, 93 | ffvelcdmd 7040 |
. . . 4
β’ ((π β§ ((ββπ) + 1) β€ π) β (π»β(ββπ)) β β) |
95 | 6 | adantr 482 |
. . . . 5
β’ ((π β§ ((ββπ) + 1) β€ π) β π β π) |
96 | 63, 95 | ffvelcdmd 7040 |
. . . 4
β’ ((π β§ ((ββπ) + 1) β€ π) β (π»βπ) β β) |
97 | 12 | adantr 482 |
. . . . . 6
β’ ((π β§ ((ββπ) + 1) β€ π) β π β β€) |
98 | 14 | adantr 482 |
. . . . . 6
β’ ((π β§ ((ββπ) + 1) β€ π) β π· β β) |
99 | 16 | adantr 482 |
. . . . . 6
β’ ((π β§ ((ββπ) + 1) β€ π) β π β€ (π· + 1)) |
100 | 20 | adantlr 714 |
. . . . . 6
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π₯ β π) β π΄ β β) |
101 | 22 | adantlr 714 |
. . . . . 6
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π₯ β π) β π΅ β π) |
102 | 24 | adantlr 714 |
. . . . . 6
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π₯ β π) β π΅ β β) |
103 | 26 | adantr 482 |
. . . . . 6
β’ ((π β§ ((ββπ) + 1) β€ π) β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) |
104 | 29 | adantr 482 |
. . . . . 6
β’ ((π β§ ((ββπ) + 1) β€ π) β π β
β*) |
105 | 31 | 3adant1r 1178 |
. . . . . 6
β’ (((π β§ ((ββπ) + 1) β€ π) β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ π)) β πΆ β€ π΅) |
106 | 36 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((ββπ) + 1) β€ π) β π· β€ π) |
107 | 70, 78 | syl 17 |
. . . . . . . 8
β’ ((π β§ ((ββπ) + 1) β€ π) β π β€ ((ββπ) + 1)) |
108 | 98, 70, 71, 106, 107 | letrd 11320 |
. . . . . . 7
β’ ((π β§ ((ββπ) + 1) β€ π) β π· β€ ((ββπ) + 1)) |
109 | 98, 71, 68, 108, 87 | letrd 11320 |
. . . . . 6
β’ ((π β§ ((ββπ) + 1) β€ π) β π· β€ (ββπ)) |
110 | | flle 13713 |
. . . . . . 7
β’ (π β β β
(ββπ) β€
π) |
111 | 66, 110 | syl 17 |
. . . . . 6
β’ ((π β§ ((ββπ) + 1) β€ π) β (ββπ) β€ π) |
112 | 40 | adantr 482 |
. . . . . 6
β’ ((π β§ ((ββπ) + 1) β€ π) β π β€ π) |
113 | | fllep1 13715 |
. . . . . . . 8
β’ (π β β β π β€ ((ββπ) + 1)) |
114 | 66, 113 | syl 17 |
. . . . . . 7
β’ ((π β§ ((ββπ) + 1) β€ π) β π β€ ((ββπ) + 1)) |
115 | | flidm 13723 |
. . . . . . . . 9
β’ (π β β β
(ββ(ββπ)) = (ββπ)) |
116 | 66, 115 | syl 17 |
. . . . . . . 8
β’ ((π β§ ((ββπ) + 1) β€ π) β (ββ(ββπ)) = (ββπ)) |
117 | 116 | oveq1d 7376 |
. . . . . . 7
β’ ((π β§ ((ββπ) + 1) β€ π) β
((ββ(ββπ)) + 1) = ((ββπ) + 1)) |
118 | 114, 117 | breqtrrd 5137 |
. . . . . 6
β’ ((π β§ ((ββπ) + 1) β€ π) β π β€ ((ββ(ββπ)) + 1)) |
119 | 1, 11, 97, 98, 99, 69, 100, 101, 102, 103, 28, 104, 105, 33, 93, 64, 109, 111, 112, 118 | dvfsumlem2 25414 |
. . . . 5
β’ ((π β§ ((ββπ) + 1) β€ π) β ((π»βπ) β€ (π»β(ββπ)) β§ ((π»β(ββπ)) β
β¦(ββπ) / π₯β¦π΅) β€ ((π»βπ) β β¦π / π₯β¦π΅))) |
120 | 119 | simpld 496 |
. . . 4
β’ ((π β§ ((ββπ) + 1) β€ π) β (π»βπ) β€ (π»β(ββπ))) |
121 | | elioopnf 13369 |
. . . . . . . . . 10
β’ (π β β*
β (((ββπ)
+ 1) β (π(,)+β)
β (((ββπ)
+ 1) β β β§ π
< ((ββπ) +
1)))) |
122 | 73, 121 | syl 17 |
. . . . . . . . 9
β’ (π β (((ββπ) + 1) β (π(,)+β) β (((ββπ) + 1) β β β§
π <
((ββπ) +
1)))) |
123 | 10, 80, 122 | mpbir2and 712 |
. . . . . . . 8
β’ (π β ((ββπ) + 1) β (π(,)+β)) |
124 | 123, 1 | eleqtrrdi 2845 |
. . . . . . 7
β’ (π β ((ββπ) + 1) β π) |
125 | 124 | adantr 482 |
. . . . . 6
β’ ((π β§ ((ββπ) + 1) β€ π) β ((ββπ) + 1) β π) |
126 | 63, 125 | ffvelcdmd 7040 |
. . . . 5
β’ ((π β§ ((ββπ) + 1) β€ π) β (π»β((ββπ) + 1)) β β) |
127 | 66 | flcld 13712 |
. . . . . . 7
β’ ((π β§ ((ββπ) + 1) β€ π) β (ββπ) β β€) |
128 | | eluz2 12777 |
. . . . . . 7
β’
((ββπ)
β (β€β₯β((ββπ) + 1)) β (((ββπ) + 1) β β€ β§
(ββπ) β
β€ β§ ((ββπ) + 1) β€ (ββπ))) |
129 | 84, 127, 87, 128 | syl3anbrc 1344 |
. . . . . 6
β’ ((π β§ ((ββπ) + 1) β€ π) β (ββπ) β
(β€β₯β((ββπ) + 1))) |
130 | 63 | adantr 482 |
. . . . . . 7
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...(ββπ))) β π»:πβΆβ) |
131 | | elfzelz 13450 |
. . . . . . . . . . 11
β’ (π β (((ββπ) + 1)...(ββπ)) β π β β€) |
132 | 131 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...(ββπ))) β π β β€) |
133 | 132 | zred 12615 |
. . . . . . . . 9
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...(ββπ))) β π β β) |
134 | 69 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...(ββπ))) β π β β) |
135 | 71 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...(ββπ))) β ((ββπ) + 1) β β) |
136 | 80 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...(ββπ))) β π < ((ββπ) + 1)) |
137 | | elfzle1 13453 |
. . . . . . . . . . 11
β’ (π β (((ββπ) + 1)...(ββπ)) β ((ββπ) + 1) β€ π) |
138 | 137 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...(ββπ))) β ((ββπ) + 1) β€ π) |
139 | 134, 135,
133, 136, 138 | ltletrd 11323 |
. . . . . . . . 9
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...(ββπ))) β π < π) |
140 | 73 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...(ββπ))) β π β
β*) |
141 | | elioopnf 13369 |
. . . . . . . . . 10
β’ (π β β*
β (π β (π(,)+β) β (π β β β§ π < π))) |
142 | 140, 141 | syl 17 |
. . . . . . . . 9
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...(ββπ))) β (π β (π(,)+β) β (π β β β§ π < π))) |
143 | 133, 139,
142 | mpbir2and 712 |
. . . . . . . 8
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...(ββπ))) β π β (π(,)+β)) |
144 | 143, 1 | eleqtrrdi 2845 |
. . . . . . 7
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...(ββπ))) β π β π) |
145 | 130, 144 | ffvelcdmd 7040 |
. . . . . 6
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...(ββπ))) β (π»βπ) β β) |
146 | 97 | adantr 482 |
. . . . . . . 8
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β π β β€) |
147 | 98 | adantr 482 |
. . . . . . . 8
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β π· β β) |
148 | 16 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β π β€ (π· + 1)) |
149 | 69 | adantr 482 |
. . . . . . . 8
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β π β β) |
150 | 100 | adantlr 714 |
. . . . . . . 8
β’ ((((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β§ π₯ β π) β π΄ β β) |
151 | 101 | adantlr 714 |
. . . . . . . 8
β’ ((((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β§ π₯ β π) β π΅ β π) |
152 | 102 | adantlr 714 |
. . . . . . . 8
β’ ((((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β§ π₯ β π) β π΅ β β) |
153 | 103 | adantr 482 |
. . . . . . . 8
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) |
154 | 104 | adantr 482 |
. . . . . . . 8
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β π β
β*) |
155 | 105 | 3adant1r 1178 |
. . . . . . . 8
β’ ((((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ π)) β πΆ β€ π΅) |
156 | | elfzelz 13450 |
. . . . . . . . . . . 12
β’ (π β (((ββπ) + 1)...((ββπ) β 1)) β π β
β€) |
157 | 156 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β π β β€) |
158 | 157 | zred 12615 |
. . . . . . . . . 10
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β π β β) |
159 | 71 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β ((ββπ) + 1) β
β) |
160 | 80 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β π < ((ββπ) + 1)) |
161 | | elfzle1 13453 |
. . . . . . . . . . . 12
β’ (π β (((ββπ) + 1)...((ββπ) β 1)) β
((ββπ) + 1)
β€ π) |
162 | 161 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β ((ββπ) + 1) β€ π) |
163 | 149, 159,
158, 160, 162 | ltletrd 11323 |
. . . . . . . . . 10
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β π < π) |
164 | 149 | rexrd 11213 |
. . . . . . . . . . 11
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β π β
β*) |
165 | 164, 141 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β (π β (π(,)+β) β (π β β β§ π < π))) |
166 | 158, 163,
165 | mpbir2and 712 |
. . . . . . . . 9
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β π β (π(,)+β)) |
167 | 166, 1 | eleqtrrdi 2845 |
. . . . . . . 8
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β π β π) |
168 | | peano2re 11336 |
. . . . . . . . . . 11
β’ (π β β β (π + 1) β
β) |
169 | 158, 168 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β (π + 1) β β) |
170 | 158 | lep1d 12094 |
. . . . . . . . . . 11
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β π β€ (π + 1)) |
171 | 149, 158,
169, 163, 170 | ltletrd 11323 |
. . . . . . . . . 10
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β π < (π + 1)) |
172 | | elioopnf 13369 |
. . . . . . . . . . 11
β’ (π β β*
β ((π + 1) β
(π(,)+β) β
((π + 1) β β
β§ π < (π + 1)))) |
173 | 164, 172 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β ((π + 1) β (π(,)+β) β ((π + 1) β β β§ π < (π + 1)))) |
174 | 169, 171,
173 | mpbir2and 712 |
. . . . . . . . 9
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β (π + 1) β (π(,)+β)) |
175 | 174, 1 | eleqtrrdi 2845 |
. . . . . . . 8
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β (π + 1) β π) |
176 | 108 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β π· β€ ((ββπ) + 1)) |
177 | 147, 159,
158, 176, 162 | letrd 11320 |
. . . . . . . 8
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β π· β€ π) |
178 | 169 | rexrd 11213 |
. . . . . . . . 9
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β (π + 1) β
β*) |
179 | 68 | rexrd 11213 |
. . . . . . . . . 10
β’ ((π β§ ((ββπ) + 1) β€ π) β (ββπ) β
β*) |
180 | 179 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β (ββπ) β
β*) |
181 | | elfzle2 13454 |
. . . . . . . . . . 11
β’ (π β (((ββπ) + 1)...((ββπ) β 1)) β π β€ ((ββπ) β 1)) |
182 | 181 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β π β€ ((ββπ) β 1)) |
183 | | 1red 11164 |
. . . . . . . . . . 11
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β 1 β
β) |
184 | 66 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β π β β) |
185 | 184, 67 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β (ββπ) β
β) |
186 | | leaddsub 11639 |
. . . . . . . . . . 11
β’ ((π β β β§ 1 β
β β§ (ββπ) β β) β ((π + 1) β€ (ββπ) β π β€ ((ββπ) β 1))) |
187 | 158, 183,
185, 186 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β ((π + 1) β€ (ββπ) β π β€ ((ββπ) β 1))) |
188 | 182, 187 | mpbird 257 |
. . . . . . . . 9
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β (π + 1) β€ (ββπ)) |
189 | 66 | rexrd 11213 |
. . . . . . . . . . 11
β’ ((π β§ ((ββπ) + 1) β€ π) β π β
β*) |
190 | 179, 189,
104, 111, 112 | xrletrd 13090 |
. . . . . . . . . 10
β’ ((π β§ ((ββπ) + 1) β€ π) β (ββπ) β€ π) |
191 | 190 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β (ββπ) β€ π) |
192 | 178, 180,
154, 188, 191 | xrletrd 13090 |
. . . . . . . 8
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β (π + 1) β€ π) |
193 | | flid 13722 |
. . . . . . . . . . . 12
β’ (π β β€ β
(ββπ) = π) |
194 | 157, 193 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β (ββπ) = π) |
195 | 194 | eqcomd 2739 |
. . . . . . . . . 10
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β π = (ββπ)) |
196 | 195 | oveq1d 7376 |
. . . . . . . . 9
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β (π + 1) = ((ββπ) + 1)) |
197 | 169, 196 | eqled 11266 |
. . . . . . . 8
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β (π + 1) β€ ((ββπ) + 1)) |
198 | 1, 11, 146, 147, 148, 149, 150, 151, 152, 153, 28, 154, 155, 33, 167, 175, 177, 170, 192, 197 | dvfsumlem2 25414 |
. . . . . . 7
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β ((π»β(π + 1)) β€ (π»βπ) β§ ((π»βπ) β β¦π / π₯β¦π΅) β€ ((π»β(π + 1)) β β¦(π + 1) / π₯β¦π΅))) |
199 | 198 | simpld 496 |
. . . . . 6
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β (π»β(π + 1)) β€ (π»βπ)) |
200 | 129, 145,
199 | monoord2 13948 |
. . . . 5
β’ ((π β§ ((ββπ) + 1) β€ π) β (π»β(ββπ)) β€ (π»β((ββπ) + 1))) |
201 | 71 | rexrd 11213 |
. . . . . . . 8
β’ ((π β§ ((ββπ) + 1) β€ π) β ((ββπ) + 1) β
β*) |
202 | 201, 179,
104, 87, 190 | xrletrd 13090 |
. . . . . . 7
β’ ((π β§ ((ββπ) + 1) β€ π) β ((ββπ) + 1) β€ π) |
203 | 71 | leidd 11729 |
. . . . . . 7
β’ ((π β§ ((ββπ) + 1) β€ π) β ((ββπ) + 1) β€ ((ββπ) + 1)) |
204 | 1, 11, 97, 98, 99, 69, 100, 101, 102, 103, 28, 104, 105, 33, 95, 125, 106, 107, 202, 203 | dvfsumlem2 25414 |
. . . . . 6
β’ ((π β§ ((ββπ) + 1) β€ π) β ((π»β((ββπ) + 1)) β€ (π»βπ) β§ ((π»βπ) β β¦π / π₯β¦π΅) β€ ((π»β((ββπ) + 1)) β
β¦((ββπ) + 1) / π₯β¦π΅))) |
205 | 204 | simpld 496 |
. . . . 5
β’ ((π β§ ((ββπ) + 1) β€ π) β (π»β((ββπ) + 1)) β€ (π»βπ)) |
206 | 94, 126, 96, 200, 205 | letrd 11320 |
. . . 4
β’ ((π β§ ((ββπ) + 1) β€ π) β (π»β(ββπ)) β€ (π»βπ)) |
207 | 65, 94, 96, 120, 206 | letrd 11320 |
. . 3
β’ ((π β§ ((ββπ) + 1) β€ π) β (π»βπ) β€ (π»βπ)) |
208 | | csbeq1 3862 |
. . . . . . 7
β’ (π = π β β¦π / π₯β¦π΅ = β¦π / π₯β¦π΅) |
209 | 208 | eleq1d 2819 |
. . . . . 6
β’ (π = π β (β¦π / π₯β¦π΅ β β β β¦π / π₯β¦π΅ β β)) |
210 | 49 | ralrimiva 3140 |
. . . . . . . . 9
β’ (π β βπ₯ β π π΅ β β) |
211 | 210 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((ββπ) + 1) β€ π) β βπ₯ β π π΅ β β) |
212 | | nfcsb1v 3884 |
. . . . . . . . . 10
β’
β²π₯β¦π / π₯β¦π΅ |
213 | 212 | nfel1 2920 |
. . . . . . . . 9
β’
β²π₯β¦π / π₯β¦π΅ β β |
214 | | csbeq1a 3873 |
. . . . . . . . . 10
β’ (π₯ = π β π΅ = β¦π / π₯β¦π΅) |
215 | 214 | eleq1d 2819 |
. . . . . . . . 9
β’ (π₯ = π β (π΅ β β β β¦π / π₯β¦π΅ β β)) |
216 | 213, 215 | rspc 3571 |
. . . . . . . 8
β’ (π β π β (βπ₯ β π π΅ β β β β¦π / π₯β¦π΅ β β)) |
217 | 211, 216 | mpan9 508 |
. . . . . . 7
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β π) β β¦π / π₯β¦π΅ β β) |
218 | 217 | ralrimiva 3140 |
. . . . . 6
β’ ((π β§ ((ββπ) + 1) β€ π) β βπ β π β¦π / π₯β¦π΅ β β) |
219 | 209, 218,
95 | rspcdva 3584 |
. . . . 5
β’ ((π β§ ((ββπ) + 1) β€ π) β β¦π / π₯β¦π΅ β β) |
220 | 96, 219 | resubcld 11591 |
. . . 4
β’ ((π β§ ((ββπ) + 1) β€ π) β ((π»βπ) β β¦π / π₯β¦π΅) β β) |
221 | | csbeq1 3862 |
. . . . . . 7
β’ (π = (ββπ) β β¦π / π₯β¦π΅ = β¦(ββπ) / π₯β¦π΅) |
222 | 221 | eleq1d 2819 |
. . . . . 6
β’ (π = (ββπ) β (β¦π / π₯β¦π΅ β β β
β¦(ββπ) / π₯β¦π΅ β β)) |
223 | 222, 218,
93 | rspcdva 3584 |
. . . . 5
β’ ((π β§ ((ββπ) + 1) β€ π) β β¦(ββπ) / π₯β¦π΅ β β) |
224 | 94, 223 | resubcld 11591 |
. . . 4
β’ ((π β§ ((ββπ) + 1) β€ π) β ((π»β(ββπ)) β
β¦(ββπ) / π₯β¦π΅) β β) |
225 | | csbeq1 3862 |
. . . . . . 7
β’ (π = π β β¦π / π₯β¦π΅ = β¦π / π₯β¦π΅) |
226 | 225 | eleq1d 2819 |
. . . . . 6
β’ (π = π β (β¦π / π₯β¦π΅ β β β β¦π / π₯β¦π΅ β β)) |
227 | 226, 218,
64 | rspcdva 3584 |
. . . . 5
β’ ((π β§ ((ββπ) + 1) β€ π) β β¦π / π₯β¦π΅ β β) |
228 | 65, 227 | resubcld 11591 |
. . . 4
β’ ((π β§ ((ββπ) + 1) β€ π) β ((π»βπ) β β¦π / π₯β¦π΅) β β) |
229 | | csbeq1 3862 |
. . . . . . . 8
β’ (π = ((ββπ) + 1) β
β¦π / π₯β¦π΅ = β¦((ββπ) + 1) / π₯β¦π΅) |
230 | 229 | eleq1d 2819 |
. . . . . . 7
β’ (π = ((ββπ) + 1) β
(β¦π / π₯β¦π΅ β β β
β¦((ββπ) + 1) / π₯β¦π΅ β β)) |
231 | 230, 218,
125 | rspcdva 3584 |
. . . . . 6
β’ ((π β§ ((ββπ) + 1) β€ π) β
β¦((ββπ) + 1) / π₯β¦π΅ β β) |
232 | 126, 231 | resubcld 11591 |
. . . . 5
β’ ((π β§ ((ββπ) + 1) β€ π) β ((π»β((ββπ) + 1)) β
β¦((ββπ) + 1) / π₯β¦π΅) β β) |
233 | 204 | simprd 497 |
. . . . 5
β’ ((π β§ ((ββπ) + 1) β€ π) β ((π»βπ) β β¦π / π₯β¦π΅) β€ ((π»β((ββπ) + 1)) β
β¦((ββπ) + 1) / π₯β¦π΅)) |
234 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π¦ = π β (π»βπ¦) = (π»βπ)) |
235 | | csbeq1 3862 |
. . . . . . . . . . 11
β’ (π¦ = π β β¦π¦ / π₯β¦π΅ = β¦π / π₯β¦π΅) |
236 | 234, 235 | oveq12d 7379 |
. . . . . . . . . 10
β’ (π¦ = π β ((π»βπ¦) β β¦π¦ / π₯β¦π΅) = ((π»βπ) β β¦π / π₯β¦π΅)) |
237 | | eqid 2733 |
. . . . . . . . . 10
β’ (π¦ β V β¦ ((π»βπ¦) β β¦π¦ / π₯β¦π΅)) = (π¦ β V β¦ ((π»βπ¦) β β¦π¦ / π₯β¦π΅)) |
238 | | ovex 7394 |
. . . . . . . . . 10
β’ ((π»βπ¦) β β¦π¦ / π₯β¦π΅) β V |
239 | 236, 237,
238 | fvmpt3i 6957 |
. . . . . . . . 9
β’ (π β V β ((π¦ β V β¦ ((π»βπ¦) β β¦π¦ / π₯β¦π΅))βπ) = ((π»βπ) β β¦π / π₯β¦π΅)) |
240 | 239 | elv 3453 |
. . . . . . . 8
β’ ((π¦ β V β¦ ((π»βπ¦) β β¦π¦ / π₯β¦π΅))βπ) = ((π»βπ) β β¦π / π₯β¦π΅) |
241 | 144, 217 | syldan 592 |
. . . . . . . . 9
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...(ββπ))) β β¦π / π₯β¦π΅ β β) |
242 | 145, 241 | resubcld 11591 |
. . . . . . . 8
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...(ββπ))) β ((π»βπ) β β¦π / π₯β¦π΅) β β) |
243 | 240, 242 | eqeltrid 2838 |
. . . . . . 7
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...(ββπ))) β ((π¦ β V β¦ ((π»βπ¦) β β¦π¦ / π₯β¦π΅))βπ) β β) |
244 | 198 | simprd 497 |
. . . . . . . 8
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β ((π»βπ) β β¦π / π₯β¦π΅) β€ ((π»β(π + 1)) β β¦(π + 1) / π₯β¦π΅)) |
245 | | ovex 7394 |
. . . . . . . . 9
β’ (π + 1) β V |
246 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π¦ = (π + 1) β (π»βπ¦) = (π»β(π + 1))) |
247 | | csbeq1 3862 |
. . . . . . . . . . 11
β’ (π¦ = (π + 1) β β¦π¦ / π₯β¦π΅ = β¦(π + 1) / π₯β¦π΅) |
248 | 246, 247 | oveq12d 7379 |
. . . . . . . . . 10
β’ (π¦ = (π + 1) β ((π»βπ¦) β β¦π¦ / π₯β¦π΅) = ((π»β(π + 1)) β β¦(π + 1) / π₯β¦π΅)) |
249 | 248, 237,
238 | fvmpt3i 6957 |
. . . . . . . . 9
β’ ((π + 1) β V β ((π¦ β V β¦ ((π»βπ¦) β β¦π¦ / π₯β¦π΅))β(π + 1)) = ((π»β(π + 1)) β β¦(π + 1) / π₯β¦π΅)) |
250 | 245, 249 | ax-mp 5 |
. . . . . . . 8
β’ ((π¦ β V β¦ ((π»βπ¦) β β¦π¦ / π₯β¦π΅))β(π + 1)) = ((π»β(π + 1)) β β¦(π + 1) / π₯β¦π΅) |
251 | 244, 240,
250 | 3brtr4g 5143 |
. . . . . . 7
β’ (((π β§ ((ββπ) + 1) β€ π) β§ π β (((ββπ) + 1)...((ββπ) β 1))) β ((π¦ β V β¦ ((π»βπ¦) β β¦π¦ / π₯β¦π΅))βπ) β€ ((π¦ β V β¦ ((π»βπ¦) β β¦π¦ / π₯β¦π΅))β(π + 1))) |
252 | 129, 243,
251 | monoord 13947 |
. . . . . 6
β’ ((π β§ ((ββπ) + 1) β€ π) β ((π¦ β V β¦ ((π»βπ¦) β β¦π¦ / π₯β¦π΅))β((ββπ) + 1)) β€ ((π¦ β V β¦ ((π»βπ¦) β β¦π¦ / π₯β¦π΅))β(ββπ))) |
253 | | ovex 7394 |
. . . . . . 7
β’
((ββπ) +
1) β V |
254 | | fveq2 6846 |
. . . . . . . . 9
β’ (π¦ = ((ββπ) + 1) β (π»βπ¦) = (π»β((ββπ) + 1))) |
255 | | csbeq1 3862 |
. . . . . . . . 9
β’ (π¦ = ((ββπ) + 1) β
β¦π¦ / π₯β¦π΅ = β¦((ββπ) + 1) / π₯β¦π΅) |
256 | 254, 255 | oveq12d 7379 |
. . . . . . . 8
β’ (π¦ = ((ββπ) + 1) β ((π»βπ¦) β β¦π¦ / π₯β¦π΅) = ((π»β((ββπ) + 1)) β
β¦((ββπ) + 1) / π₯β¦π΅)) |
257 | 256, 237,
238 | fvmpt3i 6957 |
. . . . . . 7
β’
(((ββπ)
+ 1) β V β ((π¦
β V β¦ ((π»βπ¦) β β¦π¦ / π₯β¦π΅))β((ββπ) + 1)) = ((π»β((ββπ) + 1)) β
β¦((ββπ) + 1) / π₯β¦π΅)) |
258 | 253, 257 | ax-mp 5 |
. . . . . 6
β’ ((π¦ β V β¦ ((π»βπ¦) β β¦π¦ / π₯β¦π΅))β((ββπ) + 1)) = ((π»β((ββπ) + 1)) β
β¦((ββπ) + 1) / π₯β¦π΅) |
259 | | fvex 6859 |
. . . . . . 7
β’
(ββπ)
β V |
260 | | fveq2 6846 |
. . . . . . . . 9
β’ (π¦ = (ββπ) β (π»βπ¦) = (π»β(ββπ))) |
261 | | csbeq1 3862 |
. . . . . . . . 9
β’ (π¦ = (ββπ) β β¦π¦ / π₯β¦π΅ = β¦(ββπ) / π₯β¦π΅) |
262 | 260, 261 | oveq12d 7379 |
. . . . . . . 8
β’ (π¦ = (ββπ) β ((π»βπ¦) β β¦π¦ / π₯β¦π΅) = ((π»β(ββπ)) β
β¦(ββπ) / π₯β¦π΅)) |
263 | 262, 237,
238 | fvmpt3i 6957 |
. . . . . . 7
β’
((ββπ)
β V β ((π¦ β
V β¦ ((π»βπ¦) β β¦π¦ / π₯β¦π΅))β(ββπ)) = ((π»β(ββπ)) β
β¦(ββπ) / π₯β¦π΅)) |
264 | 259, 263 | ax-mp 5 |
. . . . . 6
β’ ((π¦ β V β¦ ((π»βπ¦) β β¦π¦ / π₯β¦π΅))β(ββπ)) = ((π»β(ββπ)) β
β¦(ββπ) / π₯β¦π΅) |
265 | 252, 258,
264 | 3brtr3g 5142 |
. . . . 5
β’ ((π β§ ((ββπ) + 1) β€ π) β ((π»β((ββπ) + 1)) β
β¦((ββπ) + 1) / π₯β¦π΅) β€ ((π»β(ββπ)) β
β¦(ββπ) / π₯β¦π΅)) |
266 | 220, 232,
224, 233, 265 | letrd 11320 |
. . . 4
β’ ((π β§ ((ββπ) + 1) β€ π) β ((π»βπ) β β¦π / π₯β¦π΅) β€ ((π»β(ββπ)) β
β¦(ββπ) / π₯β¦π΅)) |
267 | 119 | simprd 497 |
. . . 4
β’ ((π β§ ((ββπ) + 1) β€ π) β ((π»β(ββπ)) β
β¦(ββπ) / π₯β¦π΅) β€ ((π»βπ) β β¦π / π₯β¦π΅)) |
268 | 220, 224,
228, 266, 267 | letrd 11320 |
. . 3
β’ ((π β§ ((ββπ) + 1) β€ π) β ((π»βπ) β β¦π / π₯β¦π΅) β€ ((π»βπ) β β¦π / π₯β¦π΅)) |
269 | 207, 268 | jca 513 |
. 2
β’ ((π β§ ((ββπ) + 1) β€ π) β ((π»βπ) β€ (π»βπ) β§ ((π»βπ) β β¦π / π₯β¦π΅) β€ ((π»βπ) β β¦π / π₯β¦π΅))) |
270 | 5, 10, 43, 269 | lecasei 11269 |
1
β’ (π β ((π»βπ) β€ (π»βπ) β§ ((π»βπ) β β¦π / π₯β¦π΅) β€ ((π»βπ) β β¦π / π₯β¦π΅))) |