Step | Hyp | Ref
| Expression |
1 | | dvfsum.s |
. . . . . . . . 9
β’ π = (π(,)+β) |
2 | | ioossre 13334 |
. . . . . . . . 9
β’ (π(,)+β) β
β |
3 | 1, 2 | eqsstri 3982 |
. . . . . . . 8
β’ π β
β |
4 | | dvfsumlem1.2 |
. . . . . . . 8
β’ (π β π β π) |
5 | 3, 4 | sselid 3946 |
. . . . . . 7
β’ (π β π β β) |
6 | | dvfsumlem1.1 |
. . . . . . . . . . 11
β’ (π β π β π) |
7 | 6, 1 | eleqtrdi 2844 |
. . . . . . . . . 10
β’ (π β π β (π(,)+β)) |
8 | | dvfsum.t |
. . . . . . . . . . . 12
β’ (π β π β β) |
9 | 8 | rexrd 11213 |
. . . . . . . . . . 11
β’ (π β π β
β*) |
10 | | elioopnf 13369 |
. . . . . . . . . . 11
β’ (π β β*
β (π β (π(,)+β) β (π β β β§ π < π))) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
β’ (π β (π β (π(,)+β) β (π β β β§ π < π))) |
12 | 7, 11 | mpbid 231 |
. . . . . . . . 9
β’ (π β (π β β β§ π < π)) |
13 | 12 | simpld 496 |
. . . . . . . 8
β’ (π β π β β) |
14 | | reflcl 13710 |
. . . . . . . 8
β’ (π β β β
(ββπ) β
β) |
15 | 13, 14 | syl 17 |
. . . . . . 7
β’ (π β (ββπ) β
β) |
16 | 5, 15 | resubcld 11591 |
. . . . . 6
β’ (π β (π β (ββπ)) β β) |
17 | | csbeq1 3862 |
. . . . . . . 8
β’ (π¦ = π β β¦π¦ / π₯β¦π΅ = β¦π / π₯β¦π΅) |
18 | 17 | eleq1d 2819 |
. . . . . . 7
β’ (π¦ = π β (β¦π¦ / π₯β¦π΅ β β β β¦π / π₯β¦π΅ β β)) |
19 | 3 | a1i 11 |
. . . . . . . . . 10
β’ (π β π β β) |
20 | | dvfsum.a |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β π΄ β β) |
21 | | dvfsum.b1 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β π΅ β π) |
22 | | dvfsum.b3 |
. . . . . . . . . 10
β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) |
23 | 19, 20, 21, 22 | dvmptrecl 25411 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β π΅ β β) |
24 | 23 | fmpttd 7067 |
. . . . . . . 8
β’ (π β (π₯ β π β¦ π΅):πβΆβ) |
25 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π¦π΅ |
26 | | nfcsb1v 3884 |
. . . . . . . . . 10
β’
β²π₯β¦π¦ / π₯β¦π΅ |
27 | | csbeq1a 3873 |
. . . . . . . . . 10
β’ (π₯ = π¦ β π΅ = β¦π¦ / π₯β¦π΅) |
28 | 25, 26, 27 | cbvmpt 5220 |
. . . . . . . . 9
β’ (π₯ β π β¦ π΅) = (π¦ β π β¦ β¦π¦ / π₯β¦π΅) |
29 | 28 | fmpt 7062 |
. . . . . . . 8
β’
(βπ¦ β
π β¦π¦ / π₯β¦π΅ β β β (π₯ β π β¦ π΅):πβΆβ) |
30 | 24, 29 | sylibr 233 |
. . . . . . 7
β’ (π β βπ¦ β π β¦π¦ / π₯β¦π΅ β β) |
31 | 18, 30, 4 | rspcdva 3584 |
. . . . . 6
β’ (π β β¦π / π₯β¦π΅ β β) |
32 | 16, 31 | remulcld 11193 |
. . . . 5
β’ (π β ((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β) |
33 | | csbeq1 3862 |
. . . . . . 7
β’ (π¦ = π β β¦π¦ / π₯β¦π΄ = β¦π / π₯β¦π΄) |
34 | 33 | eleq1d 2819 |
. . . . . 6
β’ (π¦ = π β (β¦π¦ / π₯β¦π΄ β β β β¦π / π₯β¦π΄ β β)) |
35 | 20 | fmpttd 7067 |
. . . . . . 7
β’ (π β (π₯ β π β¦ π΄):πβΆβ) |
36 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π¦π΄ |
37 | | nfcsb1v 3884 |
. . . . . . . . 9
β’
β²π₯β¦π¦ / π₯β¦π΄ |
38 | | csbeq1a 3873 |
. . . . . . . . 9
β’ (π₯ = π¦ β π΄ = β¦π¦ / π₯β¦π΄) |
39 | 36, 37, 38 | cbvmpt 5220 |
. . . . . . . 8
β’ (π₯ β π β¦ π΄) = (π¦ β π β¦ β¦π¦ / π₯β¦π΄) |
40 | 39 | fmpt 7062 |
. . . . . . 7
β’
(βπ¦ β
π β¦π¦ / π₯β¦π΄ β β β (π₯ β π β¦ π΄):πβΆβ) |
41 | 35, 40 | sylibr 233 |
. . . . . 6
β’ (π β βπ¦ β π β¦π¦ / π₯β¦π΄ β β) |
42 | 34, 41, 4 | rspcdva 3584 |
. . . . 5
β’ (π β β¦π / π₯β¦π΄ β β) |
43 | 32, 42 | resubcld 11591 |
. . . 4
β’ (π β (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β β) |
44 | 13, 15 | resubcld 11591 |
. . . . . 6
β’ (π β (π β (ββπ)) β β) |
45 | | csbeq1 3862 |
. . . . . . . 8
β’ (π¦ = π β β¦π¦ / π₯β¦π΅ = β¦π / π₯β¦π΅) |
46 | 45 | eleq1d 2819 |
. . . . . . 7
β’ (π¦ = π β (β¦π¦ / π₯β¦π΅ β β β β¦π / π₯β¦π΅ β β)) |
47 | 46, 30, 6 | rspcdva 3584 |
. . . . . 6
β’ (π β β¦π / π₯β¦π΅ β β) |
48 | 44, 47 | remulcld 11193 |
. . . . 5
β’ (π β ((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β) |
49 | | csbeq1 3862 |
. . . . . . 7
β’ (π¦ = π β β¦π¦ / π₯β¦π΄ = β¦π / π₯β¦π΄) |
50 | 49 | eleq1d 2819 |
. . . . . 6
β’ (π¦ = π β (β¦π¦ / π₯β¦π΄ β β β β¦π / π₯β¦π΄ β β)) |
51 | 50, 41, 6 | rspcdva 3584 |
. . . . 5
β’ (π β β¦π / π₯β¦π΄ β β) |
52 | 48, 51 | resubcld 11591 |
. . . 4
β’ (π β (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β β) |
53 | | fzfid 13887 |
. . . . 5
β’ (π β (π...(ββπ)) β Fin) |
54 | | dvfsum.b2 |
. . . . . . 7
β’ ((π β§ π₯ β π) β π΅ β β) |
55 | 54 | ralrimiva 3140 |
. . . . . 6
β’ (π β βπ₯ β π π΅ β β) |
56 | | elfzuz 13446 |
. . . . . . 7
β’ (π β (π...(ββπ)) β π β (β€β₯βπ)) |
57 | | dvfsum.z |
. . . . . . 7
β’ π =
(β€β₯βπ) |
58 | 56, 57 | eleqtrrdi 2845 |
. . . . . 6
β’ (π β (π...(ββπ)) β π β π) |
59 | | dvfsum.c |
. . . . . . . 8
β’ (π₯ = π β π΅ = πΆ) |
60 | 59 | eleq1d 2819 |
. . . . . . 7
β’ (π₯ = π β (π΅ β β β πΆ β β)) |
61 | 60 | rspccva 3582 |
. . . . . 6
β’
((βπ₯ β
π π΅ β β β§ π β π) β πΆ β β) |
62 | 55, 58, 61 | syl2an 597 |
. . . . 5
β’ ((π β§ π β (π...(ββπ))) β πΆ β β) |
63 | 53, 62 | fsumrecl 15627 |
. . . 4
β’ (π β Ξ£π β (π...(ββπ))πΆ β β) |
64 | 44, 31 | remulcld 11193 |
. . . . . 6
β’ (π β ((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β) |
65 | 64, 51 | resubcld 11591 |
. . . . 5
β’ (π β (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β β) |
66 | 5, 13 | resubcld 11591 |
. . . . . . . . 9
β’ (π β (π β π) β β) |
67 | 31, 66 | remulcld 11193 |
. . . . . . . 8
β’ (π β (β¦π / π₯β¦π΅ Β· (π β π)) β β) |
68 | 31 | recnd 11191 |
. . . . . . . . . 10
β’ (π β β¦π / π₯β¦π΅ β β) |
69 | 5 | recnd 11191 |
. . . . . . . . . 10
β’ (π β π β β) |
70 | 13 | recnd 11191 |
. . . . . . . . . 10
β’ (π β π β β) |
71 | 68, 69, 70 | subdid 11619 |
. . . . . . . . 9
β’ (π β (β¦π / π₯β¦π΅ Β· (π β π)) = ((β¦π / π₯β¦π΅ Β· π) β (β¦π / π₯β¦π΅ Β· π))) |
72 | | eqid 2733 |
. . . . . . . . . . 11
β’
(TopOpenββfld) =
(TopOpenββfld) |
73 | 72 | mulcn 24253 |
. . . . . . . . . . 11
β’ Β·
β (((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld)) |
74 | | pnfxr 11217 |
. . . . . . . . . . . . . . . 16
β’ +β
β β* |
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β +β β
β*) |
76 | 12 | simprd 497 |
. . . . . . . . . . . . . . 15
β’ (π β π < π) |
77 | 5 | ltpnfd 13050 |
. . . . . . . . . . . . . . 15
β’ (π β π < +β) |
78 | | iccssioo 13342 |
. . . . . . . . . . . . . . 15
β’ (((π β β*
β§ +β β β*) β§ (π < π β§ π < +β)) β (π[,]π) β (π(,)+β)) |
79 | 9, 75, 76, 77, 78 | syl22anc 838 |
. . . . . . . . . . . . . 14
β’ (π β (π[,]π) β (π(,)+β)) |
80 | 79, 2 | sstrdi 3960 |
. . . . . . . . . . . . 13
β’ (π β (π[,]π) β β) |
81 | | ax-resscn 11116 |
. . . . . . . . . . . . 13
β’ β
β β |
82 | 80, 81 | sstrdi 3960 |
. . . . . . . . . . . 12
β’ (π β (π[,]π) β β) |
83 | 81 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β β
β) |
84 | | cncfmptc 24298 |
. . . . . . . . . . . 12
β’
((β¦π /
π₯β¦π΅ β β β§ (π[,]π) β β β§ β β
β) β (π¦ β
(π[,]π) β¦ β¦π / π₯β¦π΅) β ((π[,]π)βcnββ)) |
85 | 31, 82, 83, 84 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β (π¦ β (π[,]π) β¦ β¦π / π₯β¦π΅) β ((π[,]π)βcnββ)) |
86 | | cncfmptid 24299 |
. . . . . . . . . . . 12
β’ (((π[,]π) β β β§ β β
β) β (π¦ β
(π[,]π) β¦ π¦) β ((π[,]π)βcnββ)) |
87 | 80, 81, 86 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β (π¦ β (π[,]π) β¦ π¦) β ((π[,]π)βcnββ)) |
88 | | remulcl 11144 |
. . . . . . . . . . 11
β’
((β¦π /
π₯β¦π΅ β β β§ π¦ β β) β
(β¦π / π₯β¦π΅ Β· π¦) β β) |
89 | 72, 73, 85, 87, 81, 88 | cncfmpt2ss 24302 |
. . . . . . . . . 10
β’ (π β (π¦ β (π[,]π) β¦ (β¦π / π₯β¦π΅ Β· π¦)) β ((π[,]π)βcnββ)) |
90 | | reelprrecn 11151 |
. . . . . . . . . . . . 13
β’ β
β {β, β} |
91 | 90 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β β {β,
β}) |
92 | | ioossicc 13359 |
. . . . . . . . . . . . . . 15
β’ (π(,)π) β (π[,]π) |
93 | 92, 80 | sstrid 3959 |
. . . . . . . . . . . . . 14
β’ (π β (π(,)π) β β) |
94 | 93 | sselda 3948 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (π(,)π)) β π¦ β β) |
95 | 94 | recnd 11191 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π(,)π)) β π¦ β β) |
96 | | 1cnd 11158 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π(,)π)) β 1 β β) |
97 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β β) β π¦ β β) |
98 | 97 | recnd 11191 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β β) β π¦ β β) |
99 | | 1cnd 11158 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β β) β 1 β
β) |
100 | 91 | dvmptid 25344 |
. . . . . . . . . . . . 13
β’ (π β (β D (π¦ β β β¦ π¦)) = (π¦ β β β¦ 1)) |
101 | 72 | tgioo2 24189 |
. . . . . . . . . . . . 13
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
102 | | iooretop 24152 |
. . . . . . . . . . . . . 14
β’ (π(,)π) β (topGenβran
(,)) |
103 | 102 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β (π(,)π) β (topGenβran
(,))) |
104 | 91, 98, 99, 100, 93, 101, 72, 103 | dvmptres 25350 |
. . . . . . . . . . . 12
β’ (π β (β D (π¦ β (π(,)π) β¦ π¦)) = (π¦ β (π(,)π) β¦ 1)) |
105 | 91, 95, 96, 104, 68 | dvmptcmul 25351 |
. . . . . . . . . . 11
β’ (π β (β D (π¦ β (π(,)π) β¦ (β¦π / π₯β¦π΅ Β· π¦))) = (π¦ β (π(,)π) β¦ (β¦π / π₯β¦π΅ Β· 1))) |
106 | 68 | mulridd 11180 |
. . . . . . . . . . . 12
β’ (π β (β¦π / π₯β¦π΅ Β· 1) = β¦π / π₯β¦π΅) |
107 | 106 | mpteq2dv 5211 |
. . . . . . . . . . 11
β’ (π β (π¦ β (π(,)π) β¦ (β¦π / π₯β¦π΅ Β· 1)) = (π¦ β (π(,)π) β¦ β¦π / π₯β¦π΅)) |
108 | 105, 107 | eqtrd 2773 |
. . . . . . . . . 10
β’ (π β (β D (π¦ β (π(,)π) β¦ (β¦π / π₯β¦π΅ Β· π¦))) = (π¦ β (π(,)π) β¦ β¦π / π₯β¦π΅)) |
109 | 79, 1 | sseqtrrdi 3999 |
. . . . . . . . . . . 12
β’ (π β (π[,]π) β π) |
110 | 109 | resmptd 5998 |
. . . . . . . . . . 11
β’ (π β ((π¦ β π β¦ β¦π¦ / π₯β¦π΄) βΎ (π[,]π)) = (π¦ β (π[,]π) β¦ β¦π¦ / π₯β¦π΄)) |
111 | 20 | recnd 11191 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β π) β π΄ β β) |
112 | 111 | fmpttd 7067 |
. . . . . . . . . . . . . . . 16
β’ (π β (π₯ β π β¦ π΄):πβΆβ) |
113 | 22 | dmeqd 5865 |
. . . . . . . . . . . . . . . . 17
β’ (π β dom (β D (π₯ β π β¦ π΄)) = dom (π₯ β π β¦ π΅)) |
114 | 21 | ralrimiva 3140 |
. . . . . . . . . . . . . . . . . 18
β’ (π β βπ₯ β π π΅ β π) |
115 | | dmmptg 6198 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ₯ β
π π΅ β π β dom (π₯ β π β¦ π΅) = π) |
116 | 114, 115 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β dom (π₯ β π β¦ π΅) = π) |
117 | 113, 116 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
β’ (π β dom (β D (π₯ β π β¦ π΄)) = π) |
118 | | dvcn 25308 |
. . . . . . . . . . . . . . . 16
β’
(((β β β β§ (π₯ β π β¦ π΄):πβΆβ β§ π β β) β§ dom (β D
(π₯ β π β¦ π΄)) = π) β (π₯ β π β¦ π΄) β (πβcnββ)) |
119 | 83, 112, 19, 117, 118 | syl31anc 1374 |
. . . . . . . . . . . . . . 15
β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) |
120 | | cncfcdm 24284 |
. . . . . . . . . . . . . . 15
β’ ((β
β β β§ (π₯
β π β¦ π΄) β (πβcnββ)) β ((π₯ β π β¦ π΄) β (πβcnββ) β (π₯ β π β¦ π΄):πβΆβ)) |
121 | 81, 119, 120 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ (π β ((π₯ β π β¦ π΄) β (πβcnββ) β (π₯ β π β¦ π΄):πβΆβ)) |
122 | 35, 121 | mpbird 257 |
. . . . . . . . . . . . 13
β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) |
123 | 39, 122 | eqeltrrid 2839 |
. . . . . . . . . . . 12
β’ (π β (π¦ β π β¦ β¦π¦ / π₯β¦π΄) β (πβcnββ)) |
124 | | rescncf 24283 |
. . . . . . . . . . . 12
β’ ((π[,]π) β π β ((π¦ β π β¦ β¦π¦ / π₯β¦π΄) β (πβcnββ) β ((π¦ β π β¦ β¦π¦ / π₯β¦π΄) βΎ (π[,]π)) β ((π[,]π)βcnββ))) |
125 | 109, 123,
124 | sylc 65 |
. . . . . . . . . . 11
β’ (π β ((π¦ β π β¦ β¦π¦ / π₯β¦π΄) βΎ (π[,]π)) β ((π[,]π)βcnββ)) |
126 | 110, 125 | eqeltrrd 2835 |
. . . . . . . . . 10
β’ (π β (π¦ β (π[,]π) β¦ β¦π¦ / π₯β¦π΄) β ((π[,]π)βcnββ)) |
127 | 41 | r19.21bi 3233 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β π) β β¦π¦ / π₯β¦π΄ β β) |
128 | 127 | recnd 11191 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π) β β¦π¦ / π₯β¦π΄ β β) |
129 | 30 | r19.21bi 3233 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π) β β¦π¦ / π₯β¦π΅ β β) |
130 | 39 | oveq2i 7372 |
. . . . . . . . . . . 12
β’ (β
D (π₯ β π β¦ π΄)) = (β D (π¦ β π β¦ β¦π¦ / π₯β¦π΄)) |
131 | 22, 130, 28 | 3eqtr3g 2796 |
. . . . . . . . . . 11
β’ (π β (β D (π¦ β π β¦ β¦π¦ / π₯β¦π΄)) = (π¦ β π β¦ β¦π¦ / π₯β¦π΅)) |
132 | 92, 109 | sstrid 3959 |
. . . . . . . . . . 11
β’ (π β (π(,)π) β π) |
133 | 91, 128, 129, 131, 132, 101, 72, 103 | dvmptres 25350 |
. . . . . . . . . 10
β’ (π β (β D (π¦ β (π(,)π) β¦ β¦π¦ / π₯β¦π΄)) = (π¦ β (π(,)π) β¦ β¦π¦ / π₯β¦π΅)) |
134 | 92 | sseli 3944 |
. . . . . . . . . . 11
β’ (π¦ β (π(,)π) β π¦ β (π[,]π)) |
135 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π[,]π)) β π) |
136 | 109 | sselda 3948 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π[,]π)) β π¦ β π) |
137 | 4 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π[,]π)) β π β π) |
138 | | dvfsum.d |
. . . . . . . . . . . . . 14
β’ (π β π· β β) |
139 | 138 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (π[,]π)) β π· β β) |
140 | 13 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (π[,]π)) β π β β) |
141 | | elicc2 13338 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β) β (π¦ β (π[,]π) β (π¦ β β β§ π β€ π¦ β§ π¦ β€ π))) |
142 | 13, 5, 141 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (π¦ β (π[,]π) β (π¦ β β β§ π β€ π¦ β§ π¦ β€ π))) |
143 | 142 | biimpa 478 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (π[,]π)) β (π¦ β β β§ π β€ π¦ β§ π¦ β€ π)) |
144 | 143 | simp1d 1143 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (π[,]π)) β π¦ β β) |
145 | | dvfsumlem1.3 |
. . . . . . . . . . . . . 14
β’ (π β π· β€ π) |
146 | 145 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (π[,]π)) β π· β€ π) |
147 | 143 | simp2d 1144 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (π[,]π)) β π β€ π¦) |
148 | 139, 140,
144, 146, 147 | letrd 11320 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π[,]π)) β π· β€ π¦) |
149 | 143 | simp3d 1145 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π[,]π)) β π¦ β€ π) |
150 | | dvfsumlem1.5 |
. . . . . . . . . . . . 13
β’ (π β π β€ π) |
151 | 150 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π[,]π)) β π β€ π) |
152 | | simp2r 1201 |
. . . . . . . . . . . . 13
β’ ((π β§ (π¦ β π β§ π β π) β§ (π· β€ π¦ β§ π¦ β€ π β§ π β€ π)) β π β π) |
153 | | eleq1 2822 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π β π β π β π)) |
154 | 153 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π¦ β π β§ π β π) β (π¦ β π β§ π β π))) |
155 | | breq2 5113 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π¦ β€ π β π¦ β€ π)) |
156 | | breq1 5112 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π β€ π β π β€ π)) |
157 | 155, 156 | 3anbi23d 1440 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π· β€ π¦ β§ π¦ β€ π β§ π β€ π) β (π· β€ π¦ β§ π¦ β€ π β§ π β€ π))) |
158 | 154, 157 | 3anbi23d 1440 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π β§ (π¦ β π β§ π β π) β§ (π· β€ π¦ β§ π¦ β€ π β§ π β€ π)) β (π β§ (π¦ β π β§ π β π) β§ (π· β€ π¦ β§ π¦ β€ π β§ π β€ π)))) |
159 | | vex 3451 |
. . . . . . . . . . . . . . . . . 18
β’ π β V |
160 | 159, 59 | csbie 3895 |
. . . . . . . . . . . . . . . . 17
β’
β¦π /
π₯β¦π΅ = πΆ |
161 | | csbeq1 3862 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β β¦π / π₯β¦π΅ = β¦π / π₯β¦π΅) |
162 | 160, 161 | eqtr3id 2787 |
. . . . . . . . . . . . . . . 16
β’ (π = π β πΆ = β¦π / π₯β¦π΅) |
163 | 162 | breq1d 5119 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πΆ β€ β¦π¦ / π₯β¦π΅ β β¦π / π₯β¦π΅ β€ β¦π¦ / π₯β¦π΅)) |
164 | 158, 163 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π = π β (((π β§ (π¦ β π β§ π β π) β§ (π· β€ π¦ β§ π¦ β€ π β§ π β€ π)) β πΆ β€ β¦π¦ / π₯β¦π΅) β ((π β§ (π¦ β π β§ π β π) β§ (π· β€ π¦ β§ π¦ β€ π β§ π β€ π)) β β¦π / π₯β¦π΅ β€ β¦π¦ / π₯β¦π΅))) |
165 | | nfv 1918 |
. . . . . . . . . . . . . . . 16
β’
β²π₯(π β§ (π¦ β π β§ π β π) β§ (π· β€ π¦ β§ π¦ β€ π β§ π β€ π)) |
166 | | nfcv 2904 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯πΆ |
167 | | nfcv 2904 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯
β€ |
168 | 166, 167,
26 | nfbr 5156 |
. . . . . . . . . . . . . . . 16
β’
β²π₯ πΆ β€ β¦π¦ / π₯β¦π΅ |
169 | 165, 168 | nfim 1900 |
. . . . . . . . . . . . . . 15
β’
β²π₯((π β§ (π¦ β π β§ π β π) β§ (π· β€ π¦ β§ π¦ β€ π β§ π β€ π)) β πΆ β€ β¦π¦ / π₯β¦π΅) |
170 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π¦ β (π₯ β π β π¦ β π)) |
171 | 170 | anbi1d 631 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π¦ β ((π₯ β π β§ π β π) β (π¦ β π β§ π β π))) |
172 | | breq2 5113 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π¦ β (π· β€ π₯ β π· β€ π¦)) |
173 | | breq1 5112 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π¦ β (π₯ β€ π β π¦ β€ π)) |
174 | 172, 173 | 3anbi12d 1438 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π¦ β ((π· β€ π₯ β§ π₯ β€ π β§ π β€ π) β (π· β€ π¦ β§ π¦ β€ π β§ π β€ π))) |
175 | 171, 174 | 3anbi23d 1440 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π¦ β ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ π)) β (π β§ (π¦ β π β§ π β π) β§ (π· β€ π¦ β§ π¦ β€ π β§ π β€ π)))) |
176 | 27 | breq2d 5121 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π¦ β (πΆ β€ π΅ β πΆ β€ β¦π¦ / π₯β¦π΅)) |
177 | 175, 176 | imbi12d 345 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π¦ β (((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ π)) β πΆ β€ π΅) β ((π β§ (π¦ β π β§ π β π) β§ (π· β€ π¦ β§ π¦ β€ π β§ π β€ π)) β πΆ β€ β¦π¦ / π₯β¦π΅))) |
178 | | dvfsum.l |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ π)) β πΆ β€ π΅) |
179 | 169, 177,
178 | chvarfv 2234 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π¦ β π β§ π β π) β§ (π· β€ π¦ β§ π¦ β€ π β§ π β€ π)) β πΆ β€ β¦π¦ / π₯β¦π΅) |
180 | 164, 179 | vtoclg 3527 |
. . . . . . . . . . . . 13
β’ (π β π β ((π β§ (π¦ β π β§ π β π) β§ (π· β€ π¦ β§ π¦ β€ π β§ π β€ π)) β β¦π / π₯β¦π΅ β€ β¦π¦ / π₯β¦π΅)) |
181 | 152, 180 | mpcom 38 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β π β§ π β π) β§ (π· β€ π¦ β§ π¦ β€ π β§ π β€ π)) β β¦π / π₯β¦π΅ β€ β¦π¦ / π₯β¦π΅) |
182 | 135, 136,
137, 148, 149, 151, 181 | syl123anc 1388 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (π[,]π)) β β¦π / π₯β¦π΅ β€ β¦π¦ / π₯β¦π΅) |
183 | 134, 182 | sylan2 594 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π(,)π)) β β¦π / π₯β¦π΅ β€ β¦π¦ / π₯β¦π΅) |
184 | 13 | rexrd 11213 |
. . . . . . . . . . 11
β’ (π β π β
β*) |
185 | 5 | rexrd 11213 |
. . . . . . . . . . 11
β’ (π β π β
β*) |
186 | | dvfsumlem1.4 |
. . . . . . . . . . 11
β’ (π β π β€ π) |
187 | | lbicc2 13390 |
. . . . . . . . . . 11
β’ ((π β β*
β§ π β
β* β§ π
β€ π) β π β (π[,]π)) |
188 | 184, 185,
186, 187 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β π β (π[,]π)) |
189 | | ubicc2 13391 |
. . . . . . . . . . 11
β’ ((π β β*
β§ π β
β* β§ π
β€ π) β π β (π[,]π)) |
190 | 184, 185,
186, 189 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β π β (π[,]π)) |
191 | | oveq2 7369 |
. . . . . . . . . 10
β’ (π¦ = π β (β¦π / π₯β¦π΅ Β· π¦) = (β¦π / π₯β¦π΅ Β· π)) |
192 | | oveq2 7369 |
. . . . . . . . . 10
β’ (π¦ = π β (β¦π / π₯β¦π΅ Β· π¦) = (β¦π / π₯β¦π΅ Β· π)) |
193 | 13, 5, 89, 108, 126, 133, 183, 188, 190, 186, 191, 49, 192, 33 | dvle 25394 |
. . . . . . . . 9
β’ (π β ((β¦π / π₯β¦π΅ Β· π) β (β¦π / π₯β¦π΅ Β· π)) β€ (β¦π / π₯β¦π΄ β β¦π / π₯β¦π΄)) |
194 | 71, 193 | eqbrtrd 5131 |
. . . . . . . 8
β’ (π β (β¦π / π₯β¦π΅ Β· (π β π)) β€ (β¦π / π₯β¦π΄ β β¦π / π₯β¦π΄)) |
195 | 67, 42, 51, 194 | lesubd 11767 |
. . . . . . 7
β’ (π β β¦π / π₯β¦π΄ β€ (β¦π / π₯β¦π΄ β (β¦π / π₯β¦π΅ Β· (π β π)))) |
196 | 64 | recnd 11191 |
. . . . . . . . 9
β’ (π β ((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β) |
197 | 32 | recnd 11191 |
. . . . . . . . 9
β’ (π β ((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β) |
198 | 42 | recnd 11191 |
. . . . . . . . 9
β’ (π β β¦π / π₯β¦π΄ β β) |
199 | 196, 197,
198 | subsubd 11548 |
. . . . . . . 8
β’ (π β (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄)) = ((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β ((π β (ββπ)) Β· β¦π / π₯β¦π΅)) + β¦π / π₯β¦π΄)) |
200 | 197, 196 | negsubdi2d 11536 |
. . . . . . . . . . 11
β’ (π β -(((π β (ββπ)) Β· β¦π / π₯β¦π΅) β ((π β (ββπ)) Β· β¦π / π₯β¦π΅)) = (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β ((π β (ββπ)) Β· β¦π / π₯β¦π΅))) |
201 | 15 | recnd 11191 |
. . . . . . . . . . . . . . 15
β’ (π β (ββπ) β
β) |
202 | 69, 70, 201 | nnncan2d 11555 |
. . . . . . . . . . . . . 14
β’ (π β ((π β (ββπ)) β (π β (ββπ))) = (π β π)) |
203 | 202 | oveq1d 7376 |
. . . . . . . . . . . . 13
β’ (π β (((π β (ββπ)) β (π β (ββπ))) Β· β¦π / π₯β¦π΅) = ((π β π) Β· β¦π / π₯β¦π΅)) |
204 | 16 | recnd 11191 |
. . . . . . . . . . . . . 14
β’ (π β (π β (ββπ)) β β) |
205 | 44 | recnd 11191 |
. . . . . . . . . . . . . 14
β’ (π β (π β (ββπ)) β β) |
206 | 204, 205,
68 | subdird 11620 |
. . . . . . . . . . . . 13
β’ (π β (((π β (ββπ)) β (π β (ββπ))) Β· β¦π / π₯β¦π΅) = (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β ((π β (ββπ)) Β· β¦π / π₯β¦π΅))) |
207 | 66 | recnd 11191 |
. . . . . . . . . . . . . 14
β’ (π β (π β π) β β) |
208 | 207, 68 | mulcomd 11184 |
. . . . . . . . . . . . 13
β’ (π β ((π β π) Β· β¦π / π₯β¦π΅) = (β¦π / π₯β¦π΅ Β· (π β π))) |
209 | 203, 206,
208 | 3eqtr3d 2781 |
. . . . . . . . . . . 12
β’ (π β (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β ((π β (ββπ)) Β· β¦π / π₯β¦π΅)) = (β¦π / π₯β¦π΅ Β· (π β π))) |
210 | 209 | negeqd 11403 |
. . . . . . . . . . 11
β’ (π β -(((π β (ββπ)) Β· β¦π / π₯β¦π΅) β ((π β (ββπ)) Β· β¦π / π₯β¦π΅)) = -(β¦π / π₯β¦π΅ Β· (π β π))) |
211 | 200, 210 | eqtr3d 2775 |
. . . . . . . . . 10
β’ (π β (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β ((π β (ββπ)) Β· β¦π / π₯β¦π΅)) = -(β¦π / π₯β¦π΅ Β· (π β π))) |
212 | 211 | oveq1d 7376 |
. . . . . . . . 9
β’ (π β ((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β ((π β (ββπ)) Β· β¦π / π₯β¦π΅)) + β¦π / π₯β¦π΄) = (-(β¦π / π₯β¦π΅ Β· (π β π)) + β¦π / π₯β¦π΄)) |
213 | 67 | recnd 11191 |
. . . . . . . . . 10
β’ (π β (β¦π / π₯β¦π΅ Β· (π β π)) β β) |
214 | 213, 198 | negsubdid 11535 |
. . . . . . . . 9
β’ (π β -((β¦π / π₯β¦π΅ Β· (π β π)) β β¦π / π₯β¦π΄) = (-(β¦π / π₯β¦π΅ Β· (π β π)) + β¦π / π₯β¦π΄)) |
215 | 212, 214 | eqtr4d 2776 |
. . . . . . . 8
β’ (π β ((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β ((π β (ββπ)) Β· β¦π / π₯β¦π΅)) + β¦π / π₯β¦π΄) = -((β¦π / π₯β¦π΅ Β· (π β π)) β β¦π / π₯β¦π΄)) |
216 | 213, 198 | negsubdi2d 11536 |
. . . . . . . 8
β’ (π β -((β¦π / π₯β¦π΅ Β· (π β π)) β β¦π / π₯β¦π΄) = (β¦π / π₯β¦π΄ β (β¦π / π₯β¦π΅ Β· (π β π)))) |
217 | 199, 215,
216 | 3eqtrd 2777 |
. . . . . . 7
β’ (π β (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄)) = (β¦π / π₯β¦π΄ β (β¦π / π₯β¦π΅ Β· (π β π)))) |
218 | 195, 217 | breqtrrd 5137 |
. . . . . 6
β’ (π β β¦π / π₯β¦π΄ β€ (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄))) |
219 | 51, 64, 43, 218 | lesubd 11767 |
. . . . 5
β’ (π β (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β€ (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄)) |
220 | | flle 13713 |
. . . . . . . . 9
β’ (π β β β
(ββπ) β€
π) |
221 | 13, 220 | syl 17 |
. . . . . . . 8
β’ (π β (ββπ) β€ π) |
222 | 13, 15 | subge0d 11753 |
. . . . . . . 8
β’ (π β (0 β€ (π β (ββπ)) β (ββπ) β€ π)) |
223 | 221, 222 | mpbird 257 |
. . . . . . 7
β’ (π β 0 β€ (π β (ββπ))) |
224 | 45 | breq2d 5121 |
. . . . . . . 8
β’ (π¦ = π β (β¦π / π₯β¦π΅ β€ β¦π¦ / π₯β¦π΅ β β¦π / π₯β¦π΅ β€ β¦π / π₯β¦π΅)) |
225 | 182 | ralrimiva 3140 |
. . . . . . . 8
β’ (π β βπ¦ β (π[,]π)β¦π / π₯β¦π΅ β€ β¦π¦ / π₯β¦π΅) |
226 | 224, 225,
188 | rspcdva 3584 |
. . . . . . 7
β’ (π β β¦π / π₯β¦π΅ β€ β¦π / π₯β¦π΅) |
227 | 31, 47, 44, 223, 226 | lemul2ad 12103 |
. . . . . 6
β’ (π β ((π β (ββπ)) Β· β¦π / π₯β¦π΅) β€ ((π β (ββπ)) Β· β¦π / π₯β¦π΅)) |
228 | 64, 48, 51, 227 | lesub1dd 11779 |
. . . . 5
β’ (π β (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β€ (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄)) |
229 | 43, 65, 52, 219, 228 | letrd 11320 |
. . . 4
β’ (π β (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β€ (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄)) |
230 | 43, 52, 63, 229 | leadd1dd 11777 |
. . 3
β’ (π β ((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) + Ξ£π β (π...(ββπ))πΆ) β€ ((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) + Ξ£π β (π...(ββπ))πΆ)) |
231 | | dvfsum.m |
. . . 4
β’ (π β π β β€) |
232 | | dvfsum.md |
. . . 4
β’ (π β π β€ (π· + 1)) |
233 | | dvfsum.u |
. . . 4
β’ (π β π β
β*) |
234 | | dvfsum.h |
. . . 4
β’ π» = (π₯ β π β¦ (((π₯ β (ββπ₯)) Β· π΅) + (Ξ£π β (π...(ββπ₯))πΆ β π΄))) |
235 | | dvfsumlem1.6 |
. . . 4
β’ (π β π β€ ((ββπ) + 1)) |
236 | 1, 57, 231, 138, 232, 8, 20, 21, 54, 22, 59, 233, 178, 234, 6, 4, 145, 186, 150, 235 | dvfsumlem1 25413 |
. . 3
β’ (π β (π»βπ) = ((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) + Ξ£π β (π...(ββπ))πΆ)) |
237 | 13 | leidd 11729 |
. . . 4
β’ (π β π β€ π) |
238 | 184, 185,
233, 186, 150 | xrletrd 13090 |
. . . 4
β’ (π β π β€ π) |
239 | | fllep1 13715 |
. . . . 5
β’ (π β β β π β€ ((ββπ) + 1)) |
240 | 13, 239 | syl 17 |
. . . 4
β’ (π β π β€ ((ββπ) + 1)) |
241 | 1, 57, 231, 138, 232, 8, 20, 21, 54, 22, 59, 233, 178, 234, 6, 6, 145, 237, 238, 240 | dvfsumlem1 25413 |
. . 3
β’ (π β (π»βπ) = ((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) + Ξ£π β (π...(ββπ))πΆ)) |
242 | 230, 236,
241 | 3brtr4d 5141 |
. 2
β’ (π β (π»βπ) β€ (π»βπ)) |
243 | 52, 47 | resubcld 11591 |
. . . . 5
β’ (π β ((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β β¦π / π₯β¦π΅) β β) |
244 | 43, 31 | resubcld 11591 |
. . . . 5
β’ (π β ((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β β¦π / π₯β¦π΅) β β) |
245 | | peano2rem 11476 |
. . . . . . . . . . 11
β’ ((π β (ββπ)) β β β ((π β (ββπ)) β 1) β
β) |
246 | 44, 245 | syl 17 |
. . . . . . . . . 10
β’ (π β ((π β (ββπ)) β 1) β
β) |
247 | 246, 47 | remulcld 11193 |
. . . . . . . . 9
β’ (π β (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β β) |
248 | 247, 51 | resubcld 11591 |
. . . . . . . 8
β’ (π β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β β) |
249 | | peano2rem 11476 |
. . . . . . . . . . 11
β’ ((π β (ββπ)) β β β ((π β (ββπ)) β 1) β
β) |
250 | 16, 249 | syl 17 |
. . . . . . . . . 10
β’ (π β ((π β (ββπ)) β 1) β
β) |
251 | 250, 47 | remulcld 11193 |
. . . . . . . . 9
β’ (π β (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β β) |
252 | 251, 42 | resubcld 11591 |
. . . . . . . 8
β’ (π β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β β) |
253 | 250, 31 | remulcld 11193 |
. . . . . . . . 9
β’ (π β (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β β) |
254 | 253, 42 | resubcld 11591 |
. . . . . . . 8
β’ (π β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β β) |
255 | 247 | recnd 11191 |
. . . . . . . . . . . . . 14
β’ (π β (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β β) |
256 | 251 | recnd 11191 |
. . . . . . . . . . . . . 14
β’ (π β (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β β) |
257 | 255, 256 | subcld 11520 |
. . . . . . . . . . . . 13
β’ (π β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅)) β β) |
258 | 257, 198 | addcomd 11365 |
. . . . . . . . . . . 12
β’ (π β (((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅)) + β¦π / π₯β¦π΄) = (β¦π / π₯β¦π΄ + ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅)))) |
259 | 255, 256,
198 | subsubd 11548 |
. . . . . . . . . . . 12
β’ (π β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄)) = (((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅)) + β¦π / π₯β¦π΄)) |
260 | 198, 256,
255 | subsub2d 11549 |
. . . . . . . . . . . 12
β’ (π β (β¦π / π₯β¦π΄ β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅))) = (β¦π / π₯β¦π΄ + ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅)))) |
261 | 258, 259,
260 | 3eqtr4d 2783 |
. . . . . . . . . . 11
β’ (π β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄)) = (β¦π / π₯β¦π΄ β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅)))) |
262 | | 1cnd 11158 |
. . . . . . . . . . . . . . . 16
β’ (π β 1 β
β) |
263 | 204, 205,
262 | nnncan2d 11555 |
. . . . . . . . . . . . . . 15
β’ (π β (((π β (ββπ)) β 1) β ((π β (ββπ)) β 1)) = ((π β (ββπ)) β (π β (ββπ)))) |
264 | 263, 202 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ (π β (((π β (ββπ)) β 1) β ((π β (ββπ)) β 1)) = (π β π)) |
265 | 264 | oveq1d 7376 |
. . . . . . . . . . . . 13
β’ (π β ((((π β (ββπ)) β 1) β ((π β (ββπ)) β 1)) Β· β¦π / π₯β¦π΅) = ((π β π) Β· β¦π / π₯β¦π΅)) |
266 | 250 | recnd 11191 |
. . . . . . . . . . . . . 14
β’ (π β ((π β (ββπ)) β 1) β
β) |
267 | 246 | recnd 11191 |
. . . . . . . . . . . . . 14
β’ (π β ((π β (ββπ)) β 1) β
β) |
268 | 47 | recnd 11191 |
. . . . . . . . . . . . . 14
β’ (π β β¦π / π₯β¦π΅ β β) |
269 | 266, 267,
268 | subdird 11620 |
. . . . . . . . . . . . 13
β’ (π β ((((π β (ββπ)) β 1) β ((π β (ββπ)) β 1)) Β· β¦π / π₯β¦π΅) = ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅))) |
270 | 207, 268 | mulcomd 11184 |
. . . . . . . . . . . . 13
β’ (π β ((π β π) Β· β¦π / π₯β¦π΅) = (β¦π / π₯β¦π΅ Β· (π β π))) |
271 | 265, 269,
270 | 3eqtr3d 2781 |
. . . . . . . . . . . 12
β’ (π β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅)) = (β¦π / π₯β¦π΅ Β· (π β π))) |
272 | 271 | oveq2d 7377 |
. . . . . . . . . . 11
β’ (π β (β¦π / π₯β¦π΄ β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅))) = (β¦π / π₯β¦π΄ β (β¦π / π₯β¦π΅ Β· (π β π)))) |
273 | 261, 272 | eqtrd 2773 |
. . . . . . . . . 10
β’ (π β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄)) = (β¦π / π₯β¦π΄ β (β¦π / π₯β¦π΅ Β· (π β π)))) |
274 | 47, 66 | remulcld 11193 |
. . . . . . . . . . 11
β’ (π β (β¦π / π₯β¦π΅ Β· (π β π)) β β) |
275 | | cncfmptc 24298 |
. . . . . . . . . . . . . . 15
β’
((β¦π /
π₯β¦π΅ β β β§ (π[,]π) β β β§ β β
β) β (π¦ β
(π[,]π) β¦ β¦π / π₯β¦π΅) β ((π[,]π)βcnββ)) |
276 | 47, 82, 83, 275 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (π β (π¦ β (π[,]π) β¦ β¦π / π₯β¦π΅) β ((π[,]π)βcnββ)) |
277 | | remulcl 11144 |
. . . . . . . . . . . . . 14
β’
((β¦π /
π₯β¦π΅ β β β§ π¦ β β) β
(β¦π / π₯β¦π΅ Β· π¦) β β) |
278 | 72, 73, 276, 87, 81, 277 | cncfmpt2ss 24302 |
. . . . . . . . . . . . 13
β’ (π β (π¦ β (π[,]π) β¦ (β¦π / π₯β¦π΅ Β· π¦)) β ((π[,]π)βcnββ)) |
279 | 91, 95, 96, 104, 268 | dvmptcmul 25351 |
. . . . . . . . . . . . . 14
β’ (π β (β D (π¦ β (π(,)π) β¦ (β¦π / π₯β¦π΅ Β· π¦))) = (π¦ β (π(,)π) β¦ (β¦π / π₯β¦π΅ Β· 1))) |
280 | 268 | mulridd 11180 |
. . . . . . . . . . . . . . 15
β’ (π β (β¦π / π₯β¦π΅ Β· 1) = β¦π / π₯β¦π΅) |
281 | 280 | mpteq2dv 5211 |
. . . . . . . . . . . . . 14
β’ (π β (π¦ β (π(,)π) β¦ (β¦π / π₯β¦π΅ Β· 1)) = (π¦ β (π(,)π) β¦ β¦π / π₯β¦π΅)) |
282 | 279, 281 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (π β (β D (π¦ β (π(,)π) β¦ (β¦π / π₯β¦π΅ Β· π¦))) = (π¦ β (π(,)π) β¦ β¦π / π₯β¦π΅)) |
283 | 6 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (π[,]π)) β π β π) |
284 | 144 | rexrd 11213 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (π[,]π)) β π¦ β β*) |
285 | 185 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (π[,]π)) β π β
β*) |
286 | 233 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (π[,]π)) β π β
β*) |
287 | 284, 285,
286, 149, 151 | xrletrd 13090 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (π[,]π)) β π¦ β€ π) |
288 | | vex 3451 |
. . . . . . . . . . . . . . . 16
β’ π¦ β V |
289 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π¦ β (π β π β π¦ β π)) |
290 | 289 | anbi2d 630 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π¦ β ((π β π β§ π β π) β (π β π β§ π¦ β π))) |
291 | | breq2 5113 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π¦ β (π β€ π β π β€ π¦)) |
292 | | breq1 5112 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π¦ β (π β€ π β π¦ β€ π)) |
293 | 291, 292 | 3anbi23d 1440 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π¦ β ((π· β€ π β§ π β€ π β§ π β€ π) β (π· β€ π β§ π β€ π¦ β§ π¦ β€ π))) |
294 | 290, 293 | 3anbi23d 1440 |
. . . . . . . . . . . . . . . . 17
β’ (π = π¦ β ((π β§ (π β π β§ π β π) β§ (π· β€ π β§ π β€ π β§ π β€ π)) β (π β§ (π β π β§ π¦ β π) β§ (π· β€ π β§ π β€ π¦ β§ π¦ β€ π)))) |
295 | | csbeq1 3862 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π¦ β β¦π / π₯β¦π΅ = β¦π¦ / π₯β¦π΅) |
296 | 160, 295 | eqtr3id 2787 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π¦ β πΆ = β¦π¦ / π₯β¦π΅) |
297 | 296 | breq1d 5119 |
. . . . . . . . . . . . . . . . 17
β’ (π = π¦ β (πΆ β€ β¦π / π₯β¦π΅ β β¦π¦ / π₯β¦π΅ β€ β¦π / π₯β¦π΅)) |
298 | 294, 297 | imbi12d 345 |
. . . . . . . . . . . . . . . 16
β’ (π = π¦ β (((π β§ (π β π β§ π β π) β§ (π· β€ π β§ π β€ π β§ π β€ π)) β πΆ β€ β¦π / π₯β¦π΅) β ((π β§ (π β π β§ π¦ β π) β§ (π· β€ π β§ π β€ π¦ β§ π¦ β€ π)) β β¦π¦ / π₯β¦π΅ β€ β¦π / π₯β¦π΅))) |
299 | | simp2l 1200 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β π β§ π β π) β§ (π· β€ π β§ π β€ π β§ π β€ π)) β π β π) |
300 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π₯(π β§ (π β π β§ π β π) β§ (π· β€ π β§ π β€ π β§ π β€ π)) |
301 | | nfcsb1v 3884 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π₯β¦π / π₯β¦π΅ |
302 | 166, 167,
301 | nfbr 5156 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π₯ πΆ β€ β¦π / π₯β¦π΅ |
303 | 300, 302 | nfim 1900 |
. . . . . . . . . . . . . . . . . 18
β’
β²π₯((π β§ (π β π β§ π β π) β§ (π· β€ π β§ π β€ π β§ π β€ π)) β πΆ β€ β¦π / π₯β¦π΅) |
304 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π β (π₯ β π β π β π)) |
305 | 304 | anbi1d 631 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π β ((π₯ β π β§ π β π) β (π β π β§ π β π))) |
306 | | breq2 5113 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π β (π· β€ π₯ β π· β€ π)) |
307 | | breq1 5112 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π β (π₯ β€ π β π β€ π)) |
308 | 306, 307 | 3anbi12d 1438 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π β ((π· β€ π₯ β§ π₯ β€ π β§ π β€ π) β (π· β€ π β§ π β€ π β§ π β€ π))) |
309 | 305, 308 | 3anbi23d 1440 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π β ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ π)) β (π β§ (π β π β§ π β π) β§ (π· β€ π β§ π β€ π β§ π β€ π)))) |
310 | | csbeq1a 3873 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π β π΅ = β¦π / π₯β¦π΅) |
311 | 310 | breq2d 5121 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π β (πΆ β€ π΅ β πΆ β€ β¦π / π₯β¦π΅)) |
312 | 309, 311 | imbi12d 345 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π β (((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ π)) β πΆ β€ π΅) β ((π β§ (π β π β§ π β π) β§ (π· β€ π β§ π β€ π β§ π β€ π)) β πΆ β€ β¦π / π₯β¦π΅))) |
313 | 303, 312,
178 | vtoclg1f 3526 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β ((π β§ (π β π β§ π β π) β§ (π· β€ π β§ π β€ π β§ π β€ π)) β πΆ β€ β¦π / π₯β¦π΅)) |
314 | 299, 313 | mpcom 38 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π β§ π β π) β§ (π· β€ π β§ π β€ π β§ π β€ π)) β πΆ β€ β¦π / π₯β¦π΅) |
315 | 288, 298,
314 | vtocl 3520 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π β§ π¦ β π) β§ (π· β€ π β§ π β€ π¦ β§ π¦ β€ π)) β β¦π¦ / π₯β¦π΅ β€ β¦π / π₯β¦π΅) |
316 | 135, 283,
136, 146, 147, 287, 315 | syl123anc 1388 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (π[,]π)) β β¦π¦ / π₯β¦π΅ β€ β¦π / π₯β¦π΅) |
317 | 134, 316 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (π(,)π)) β β¦π¦ / π₯β¦π΅ β€ β¦π / π₯β¦π΅) |
318 | | oveq2 7369 |
. . . . . . . . . . . . 13
β’ (π¦ = π β (β¦π / π₯β¦π΅ Β· π¦) = (β¦π / π₯β¦π΅ Β· π)) |
319 | | oveq2 7369 |
. . . . . . . . . . . . 13
β’ (π¦ = π β (β¦π / π₯β¦π΅ Β· π¦) = (β¦π / π₯β¦π΅ Β· π)) |
320 | 13, 5, 126, 133, 278, 282, 317, 188, 190, 186, 49, 318, 33, 319 | dvle 25394 |
. . . . . . . . . . . 12
β’ (π β (β¦π / π₯β¦π΄ β β¦π / π₯β¦π΄) β€ ((β¦π / π₯β¦π΅ Β· π) β (β¦π / π₯β¦π΅ Β· π))) |
321 | 268, 69, 70 | subdid 11619 |
. . . . . . . . . . . 12
β’ (π β (β¦π / π₯β¦π΅ Β· (π β π)) = ((β¦π / π₯β¦π΅ Β· π) β (β¦π / π₯β¦π΅ Β· π))) |
322 | 320, 321 | breqtrrd 5137 |
. . . . . . . . . . 11
β’ (π β (β¦π / π₯β¦π΄ β β¦π / π₯β¦π΄) β€ (β¦π / π₯β¦π΅ Β· (π β π))) |
323 | 42, 51, 274, 322 | subled 11766 |
. . . . . . . . . 10
β’ (π β (β¦π / π₯β¦π΄ β (β¦π / π₯β¦π΅ Β· (π β π))) β€ β¦π / π₯β¦π΄) |
324 | 273, 323 | eqbrtrd 5131 |
. . . . . . . . 9
β’ (π β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄)) β€ β¦π / π₯β¦π΄) |
325 | 247, 252,
51, 324 | subled 11766 |
. . . . . . . 8
β’ (π β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β€ ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄)) |
326 | 250 | renegcld 11590 |
. . . . . . . . . . . 12
β’ (π β -((π β (ββπ)) β 1) β
β) |
327 | | 1red 11164 |
. . . . . . . . . . . . . . . 16
β’ (π β 1 β
β) |
328 | 5, 15, 327 | lesubadd2d 11762 |
. . . . . . . . . . . . . . 15
β’ (π β ((π β (ββπ)) β€ 1 β π β€ ((ββπ) + 1))) |
329 | 235, 328 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ (π β (π β (ββπ)) β€ 1) |
330 | 16, 327 | suble0d 11754 |
. . . . . . . . . . . . . 14
β’ (π β (((π β (ββπ)) β 1) β€ 0 β (π β (ββπ)) β€ 1)) |
331 | 329, 330 | mpbird 257 |
. . . . . . . . . . . . 13
β’ (π β ((π β (ββπ)) β 1) β€ 0) |
332 | 250 | le0neg1d 11734 |
. . . . . . . . . . . . 13
β’ (π β (((π β (ββπ)) β 1) β€ 0 β 0 β€ -((π β (ββπ)) β 1))) |
333 | 331, 332 | mpbid 231 |
. . . . . . . . . . . 12
β’ (π β 0 β€ -((π β (ββπ)) β 1)) |
334 | 31, 47, 326, 333, 226 | lemul2ad 12103 |
. . . . . . . . . . 11
β’ (π β (-((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β€ (-((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅)) |
335 | 266, 68 | mulneg1d 11616 |
. . . . . . . . . . 11
β’ (π β (-((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) = -(((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅)) |
336 | 266, 268 | mulneg1d 11616 |
. . . . . . . . . . 11
β’ (π β (-((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) = -(((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅)) |
337 | 334, 335,
336 | 3brtr3d 5140 |
. . . . . . . . . 10
β’ (π β -(((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β€ -(((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅)) |
338 | 251, 253 | lenegd 11742 |
. . . . . . . . . 10
β’ (π β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β€ (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β -(((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β€ -(((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅))) |
339 | 337, 338 | mpbird 257 |
. . . . . . . . 9
β’ (π β (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β€ (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅)) |
340 | 251, 253,
42, 339 | lesub1dd 11779 |
. . . . . . . 8
β’ (π β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β€ ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄)) |
341 | 248, 252,
254, 325, 340 | letrd 11320 |
. . . . . . 7
β’ (π β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β€ ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄)) |
342 | 205, 262,
268 | subdird 11620 |
. . . . . . . . 9
β’ (π β (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) = (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β (1 Β· β¦π / π₯β¦π΅))) |
343 | 268 | mullidd 11181 |
. . . . . . . . . 10
β’ (π β (1 Β·
β¦π / π₯β¦π΅) = β¦π / π₯β¦π΅) |
344 | 343 | oveq2d 7377 |
. . . . . . . . 9
β’ (π β (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β (1 Β· β¦π / π₯β¦π΅)) = (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΅)) |
345 | 342, 344 | eqtrd 2773 |
. . . . . . . 8
β’ (π β (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) = (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΅)) |
346 | 345 | oveq1d 7376 |
. . . . . . 7
β’ (π β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) = ((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄)) |
347 | 204, 262,
68 | subdird 11620 |
. . . . . . . . 9
β’ (π β (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) = (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β (1 Β· β¦π / π₯β¦π΅))) |
348 | 68 | mullidd 11181 |
. . . . . . . . . 10
β’ (π β (1 Β·
β¦π / π₯β¦π΅) = β¦π / π₯β¦π΅) |
349 | 348 | oveq2d 7377 |
. . . . . . . . 9
β’ (π β (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β (1 Β· β¦π / π₯β¦π΅)) = (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΅)) |
350 | 347, 349 | eqtrd 2773 |
. . . . . . . 8
β’ (π β (((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) = (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΅)) |
351 | 350 | oveq1d 7376 |
. . . . . . 7
β’ (π β ((((π β (ββπ)) β 1) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) = ((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄)) |
352 | 341, 346,
351 | 3brtr3d 5140 |
. . . . . 6
β’ (π β ((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β€ ((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄)) |
353 | 48 | recnd 11191 |
. . . . . . 7
β’ (π β ((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β) |
354 | 51 | recnd 11191 |
. . . . . . 7
β’ (π β β¦π / π₯β¦π΄ β β) |
355 | 353, 354,
268 | sub32d 11552 |
. . . . . 6
β’ (π β ((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β β¦π / π₯β¦π΅) = ((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄)) |
356 | 197, 198,
68 | sub32d 11552 |
. . . . . 6
β’ (π β ((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β β¦π / π₯β¦π΅) = ((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄)) |
357 | 352, 355,
356 | 3brtr4d 5141 |
. . . . 5
β’ (π β ((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β β¦π / π₯β¦π΅) β€ ((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β β¦π / π₯β¦π΅)) |
358 | 243, 244,
63, 357 | leadd1dd 11777 |
. . . 4
β’ (π β (((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β β¦π / π₯β¦π΅) + Ξ£π β (π...(ββπ))πΆ) β€ (((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β β¦π / π₯β¦π΅) + Ξ£π β (π...(ββπ))πΆ)) |
359 | 52 | recnd 11191 |
. . . . 5
β’ (π β (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β β) |
360 | 63 | recnd 11191 |
. . . . 5
β’ (π β Ξ£π β (π...(ββπ))πΆ β β) |
361 | 359, 360,
268 | addsubd 11541 |
. . . 4
β’ (π β (((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) + Ξ£π β (π...(ββπ))πΆ) β β¦π / π₯β¦π΅) = (((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β β¦π / π₯β¦π΅) + Ξ£π β (π...(ββπ))πΆ)) |
362 | 43 | recnd 11191 |
. . . . 5
β’ (π β (((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β β) |
363 | 362, 360,
68 | addsubd 11541 |
. . . 4
β’ (π β (((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) + Ξ£π β (π...(ββπ))πΆ) β β¦π / π₯β¦π΅) = (((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) β β¦π / π₯β¦π΅) + Ξ£π β (π...(ββπ))πΆ)) |
364 | 358, 361,
363 | 3brtr4d 5141 |
. . 3
β’ (π β (((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) + Ξ£π β (π...(ββπ))πΆ) β β¦π / π₯β¦π΅) β€ (((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) + Ξ£π β (π...(ββπ))πΆ) β β¦π / π₯β¦π΅)) |
365 | 241 | oveq1d 7376 |
. . 3
β’ (π β ((π»βπ) β β¦π / π₯β¦π΅) = (((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) + Ξ£π β (π...(ββπ))πΆ) β β¦π / π₯β¦π΅)) |
366 | 236 | oveq1d 7376 |
. . 3
β’ (π β ((π»βπ) β β¦π / π₯β¦π΅) = (((((π β (ββπ)) Β· β¦π / π₯β¦π΅) β β¦π / π₯β¦π΄) + Ξ£π β (π...(ββπ))πΆ) β β¦π / π₯β¦π΅)) |
367 | 364, 365,
366 | 3brtr4d 5141 |
. 2
β’ (π β ((π»βπ) β β¦π / π₯β¦π΅) β€ ((π»βπ) β β¦π / π₯β¦π΅)) |
368 | 242, 367 | jca 513 |
1
β’ (π β ((π»βπ) β€ (π»βπ) β§ ((π»βπ) β β¦π / π₯β¦π΅) β€ ((π»βπ) β β¦π / π₯β¦π΅))) |