Step | Hyp | Ref
| Expression |
1 | | dvfsumlem4.2 |
. . . . 5
โข (๐ โ ๐ โ ๐) |
2 | | fzfid 13887 |
. . . . . . 7
โข (๐ โ (๐...(โโ๐)) โ Fin) |
3 | | dvfsum.b2 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐) โ ๐ต โ โ) |
4 | 3 | ralrimiva 3140 |
. . . . . . . 8
โข (๐ โ โ๐ฅ โ ๐ ๐ต โ โ) |
5 | | elfzuz 13446 |
. . . . . . . . 9
โข (๐ โ (๐...(โโ๐)) โ ๐ โ (โคโฅโ๐)) |
6 | | dvfsum.z |
. . . . . . . . 9
โข ๐ =
(โคโฅโ๐) |
7 | 5, 6 | eleqtrrdi 2845 |
. . . . . . . 8
โข (๐ โ (๐...(โโ๐)) โ ๐ โ ๐) |
8 | | dvfsum.c |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ ๐ต = ๐ถ) |
9 | 8 | eleq1d 2819 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ (๐ต โ โ โ ๐ถ โ โ)) |
10 | 9 | rspccva 3582 |
. . . . . . . 8
โข
((โ๐ฅ โ
๐ ๐ต โ โ โง ๐ โ ๐) โ ๐ถ โ โ) |
11 | 4, 7, 10 | syl2an 597 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐...(โโ๐))) โ ๐ถ โ โ) |
12 | 2, 11 | fsumrecl 15627 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โ) |
13 | | dvfsum.a |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐) โ ๐ด โ โ) |
14 | 13 | ralrimiva 3140 |
. . . . . . 7
โข (๐ โ โ๐ฅ โ ๐ ๐ด โ โ) |
15 | | nfcsb1v 3884 |
. . . . . . . . 9
โข
โฒ๐ฅโฆ๐ / ๐ฅโฆ๐ด |
16 | 15 | nfel1 2920 |
. . . . . . . 8
โข
โฒ๐ฅโฆ๐ / ๐ฅโฆ๐ด โ โ |
17 | | csbeq1a 3873 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ ๐ด = โฆ๐ / ๐ฅโฆ๐ด) |
18 | 17 | eleq1d 2819 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (๐ด โ โ โ โฆ๐ / ๐ฅโฆ๐ด โ โ)) |
19 | 16, 18 | rspc 3571 |
. . . . . . 7
โข (๐ โ ๐ โ (โ๐ฅ โ ๐ ๐ด โ โ โ โฆ๐ / ๐ฅโฆ๐ด โ โ)) |
20 | 1, 14, 19 | sylc 65 |
. . . . . 6
โข (๐ โ โฆ๐ / ๐ฅโฆ๐ด โ โ) |
21 | 12, 20 | resubcld 11591 |
. . . . 5
โข (๐ โ (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โ โ) |
22 | | nfcv 2904 |
. . . . . 6
โข
โฒ๐ฅ๐ |
23 | | nfcv 2904 |
. . . . . . 7
โข
โฒ๐ฅฮฃ๐ โ (๐...(โโ๐))๐ถ |
24 | | nfcv 2904 |
. . . . . . 7
โข
โฒ๐ฅ
โ |
25 | 23, 24, 15 | nfov 7391 |
. . . . . 6
โข
โฒ๐ฅ(ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) |
26 | | fveq2 6846 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ (โโ๐ฅ) = (โโ๐)) |
27 | 26 | oveq2d 7377 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (๐...(โโ๐ฅ)) = (๐...(โโ๐))) |
28 | 27 | sumeq1d 15594 |
. . . . . . 7
โข (๐ฅ = ๐ โ ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ = ฮฃ๐ โ (๐...(โโ๐))๐ถ) |
29 | 28, 17 | oveq12d 7379 |
. . . . . 6
โข (๐ฅ = ๐ โ (ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ โ ๐ด) = (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) |
30 | | dvfsumlem4.g |
. . . . . 6
โข ๐บ = (๐ฅ โ ๐ โฆ (ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ โ ๐ด)) |
31 | 22, 25, 29, 30 | fvmptf 6973 |
. . . . 5
โข ((๐ โ ๐ โง (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โ โ) โ (๐บโ๐) = (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) |
32 | 1, 21, 31 | syl2anc 585 |
. . . 4
โข (๐ โ (๐บโ๐) = (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) |
33 | | dvfsumlem4.1 |
. . . . 5
โข (๐ โ ๐ โ ๐) |
34 | | fzfid 13887 |
. . . . . . 7
โข (๐ โ (๐...(โโ๐)) โ Fin) |
35 | | elfzuz 13446 |
. . . . . . . . 9
โข (๐ โ (๐...(โโ๐)) โ ๐ โ (โคโฅโ๐)) |
36 | 35, 6 | eleqtrrdi 2845 |
. . . . . . . 8
โข (๐ โ (๐...(โโ๐)) โ ๐ โ ๐) |
37 | 4, 36, 10 | syl2an 597 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐...(โโ๐))) โ ๐ถ โ โ) |
38 | 34, 37 | fsumrecl 15627 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โ) |
39 | | nfcsb1v 3884 |
. . . . . . . . 9
โข
โฒ๐ฅโฆ๐ / ๐ฅโฆ๐ด |
40 | 39 | nfel1 2920 |
. . . . . . . 8
โข
โฒ๐ฅโฆ๐ / ๐ฅโฆ๐ด โ โ |
41 | | csbeq1a 3873 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ ๐ด = โฆ๐ / ๐ฅโฆ๐ด) |
42 | 41 | eleq1d 2819 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (๐ด โ โ โ โฆ๐ / ๐ฅโฆ๐ด โ โ)) |
43 | 40, 42 | rspc 3571 |
. . . . . . 7
โข (๐ โ ๐ โ (โ๐ฅ โ ๐ ๐ด โ โ โ โฆ๐ / ๐ฅโฆ๐ด โ โ)) |
44 | 33, 14, 43 | sylc 65 |
. . . . . 6
โข (๐ โ โฆ๐ / ๐ฅโฆ๐ด โ โ) |
45 | 38, 44 | resubcld 11591 |
. . . . 5
โข (๐ โ (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โ โ) |
46 | | nfcv 2904 |
. . . . . 6
โข
โฒ๐ฅ๐ |
47 | | nfcv 2904 |
. . . . . . 7
โข
โฒ๐ฅฮฃ๐ โ (๐...(โโ๐))๐ถ |
48 | 47, 24, 39 | nfov 7391 |
. . . . . 6
โข
โฒ๐ฅ(ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) |
49 | | fveq2 6846 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ (โโ๐ฅ) = (โโ๐)) |
50 | 49 | oveq2d 7377 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (๐...(โโ๐ฅ)) = (๐...(โโ๐))) |
51 | 50 | sumeq1d 15594 |
. . . . . . 7
โข (๐ฅ = ๐ โ ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ = ฮฃ๐ โ (๐...(โโ๐))๐ถ) |
52 | 51, 41 | oveq12d 7379 |
. . . . . 6
โข (๐ฅ = ๐ โ (ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ โ ๐ด) = (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) |
53 | 46, 48, 52, 30 | fvmptf 6973 |
. . . . 5
โข ((๐ โ ๐ โง (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โ โ) โ (๐บโ๐) = (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) |
54 | 33, 45, 53 | syl2anc 585 |
. . . 4
โข (๐ โ (๐บโ๐) = (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) |
55 | 32, 54 | oveq12d 7379 |
. . 3
โข (๐ โ ((๐บโ๐) โ (๐บโ๐)) = ((ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โ (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด))) |
56 | 55 | fveq2d 6850 |
. 2
โข (๐ โ (absโ((๐บโ๐) โ (๐บโ๐))) = (absโ((ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โ (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)))) |
57 | | dvfsum.s |
. . . . . . . . . . 11
โข ๐ = (๐(,)+โ) |
58 | | ioossre 13334 |
. . . . . . . . . . 11
โข (๐(,)+โ) โ
โ |
59 | 57, 58 | eqsstri 3982 |
. . . . . . . . . 10
โข ๐ โ
โ |
60 | 59 | a1i 11 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
61 | | dvfsum.b1 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐) โ ๐ต โ ๐) |
62 | | dvfsum.b3 |
. . . . . . . . 9
โข (๐ โ (โ D (๐ฅ โ ๐ โฆ ๐ด)) = (๐ฅ โ ๐ โฆ ๐ต)) |
63 | 60, 13, 61, 62 | dvmptrecl 25411 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐) โ ๐ต โ โ) |
64 | 63 | ralrimiva 3140 |
. . . . . . 7
โข (๐ โ โ๐ฅ โ ๐ ๐ต โ โ) |
65 | | nfv 1918 |
. . . . . . . 8
โข
โฒ๐ ๐ต โ โ |
66 | | nfcsb1v 3884 |
. . . . . . . . 9
โข
โฒ๐ฅโฆ๐ / ๐ฅโฆ๐ต |
67 | 66 | nfel1 2920 |
. . . . . . . 8
โข
โฒ๐ฅโฆ๐ / ๐ฅโฆ๐ต โ โ |
68 | | csbeq1a 3873 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ ๐ต = โฆ๐ / ๐ฅโฆ๐ต) |
69 | 68 | eleq1d 2819 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (๐ต โ โ โ โฆ๐ / ๐ฅโฆ๐ต โ โ)) |
70 | 65, 67, 69 | cbvralw 3288 |
. . . . . . 7
โข
(โ๐ฅ โ
๐ ๐ต โ โ โ โ๐ โ ๐ โฆ๐ / ๐ฅโฆ๐ต โ โ) |
71 | 64, 70 | sylib 217 |
. . . . . 6
โข (๐ โ โ๐ โ ๐ โฆ๐ / ๐ฅโฆ๐ต โ โ) |
72 | | csbeq1 3862 |
. . . . . . . 8
โข (๐ = ๐ โ โฆ๐ / ๐ฅโฆ๐ต = โฆ๐ / ๐ฅโฆ๐ต) |
73 | 72 | eleq1d 2819 |
. . . . . . 7
โข (๐ = ๐ โ (โฆ๐ / ๐ฅโฆ๐ต โ โ โ โฆ๐ / ๐ฅโฆ๐ต โ โ)) |
74 | 73 | rspcv 3579 |
. . . . . 6
โข (๐ โ ๐ โ (โ๐ โ ๐ โฆ๐ / ๐ฅโฆ๐ต โ โ โ โฆ๐ / ๐ฅโฆ๐ต โ โ)) |
75 | 33, 71, 74 | sylc 65 |
. . . . 5
โข (๐ โ โฆ๐ / ๐ฅโฆ๐ต โ โ) |
76 | 45, 75 | resubcld 11591 |
. . . 4
โข (๐ โ ((ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โ โฆ๐ / ๐ฅโฆ๐ต) โ โ) |
77 | 59, 33 | sselid 3946 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
78 | | reflcl 13710 |
. . . . . . . . 9
โข (๐ โ โ โ
(โโ๐) โ
โ) |
79 | 77, 78 | syl 17 |
. . . . . . . 8
โข (๐ โ (โโ๐) โ
โ) |
80 | 77, 79 | resubcld 11591 |
. . . . . . 7
โข (๐ โ (๐ โ (โโ๐)) โ โ) |
81 | 80, 75 | remulcld 11193 |
. . . . . 6
โข (๐ โ ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) โ โ) |
82 | 81, 45 | readdcld 11192 |
. . . . 5
โข (๐ โ (((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) โ โ) |
83 | 82, 75 | resubcld 11591 |
. . . 4
โข (๐ โ ((((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) โ โฆ๐ / ๐ฅโฆ๐ต) โ โ) |
84 | | fracge0 13718 |
. . . . . . . 8
โข (๐ โ โ โ 0 โค
(๐ โ
(โโ๐))) |
85 | 77, 84 | syl 17 |
. . . . . . 7
โข (๐ โ 0 โค (๐ โ (โโ๐))) |
86 | | dvfsumlem4.3 |
. . . . . . . . 9
โข (๐ โ ๐ท โค ๐) |
87 | 77 | rexrd 11213 |
. . . . . . . . . 10
โข (๐ โ ๐ โ
โ*) |
88 | 59, 1 | sselid 3946 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
89 | 88 | rexrd 11213 |
. . . . . . . . . 10
โข (๐ โ ๐ โ
โ*) |
90 | | dvfsum.u |
. . . . . . . . . 10
โข (๐ โ ๐ โ
โ*) |
91 | | dvfsumlem4.4 |
. . . . . . . . . 10
โข (๐ โ ๐ โค ๐) |
92 | | dvfsumlem4.5 |
. . . . . . . . . 10
โข (๐ โ ๐ โค ๐) |
93 | 87, 89, 90, 91, 92 | xrletrd 13090 |
. . . . . . . . 9
โข (๐ โ ๐ โค ๐) |
94 | 33, 86, 93 | 3jca 1129 |
. . . . . . . 8
โข (๐ โ (๐ โ ๐ โง ๐ท โค ๐ โง ๐ โค ๐)) |
95 | | simpr1 1195 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐ โง ๐ท โค ๐ โง ๐ โค ๐)) โ ๐ โ ๐) |
96 | | nfv 1918 |
. . . . . . . . . . 11
โข
โฒ๐ฅ(๐ โง (๐ โ ๐ โง ๐ท โค ๐ โง ๐ โค ๐)) |
97 | | nfcv 2904 |
. . . . . . . . . . . 12
โข
โฒ๐ฅ0 |
98 | | nfcv 2904 |
. . . . . . . . . . . 12
โข
โฒ๐ฅ
โค |
99 | | nfcsb1v 3884 |
. . . . . . . . . . . 12
โข
โฒ๐ฅโฆ๐ / ๐ฅโฆ๐ต |
100 | 97, 98, 99 | nfbr 5156 |
. . . . . . . . . . 11
โข
โฒ๐ฅ0 โค
โฆ๐ / ๐ฅโฆ๐ต |
101 | 96, 100 | nfim 1900 |
. . . . . . . . . 10
โข
โฒ๐ฅ((๐ โง (๐ โ ๐ โง ๐ท โค ๐ โง ๐ โค ๐)) โ 0 โค โฆ๐ / ๐ฅโฆ๐ต) |
102 | | eleq1 2822 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ โ (๐ฅ โ ๐ โ ๐ โ ๐)) |
103 | | breq2 5113 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ โ (๐ท โค ๐ฅ โ ๐ท โค ๐)) |
104 | | breq1 5112 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ โ (๐ฅ โค ๐ โ ๐ โค ๐)) |
105 | 102, 103,
104 | 3anbi123d 1437 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ โ ((๐ฅ โ ๐ โง ๐ท โค ๐ฅ โง ๐ฅ โค ๐) โ (๐ โ ๐ โง ๐ท โค ๐ โง ๐ โค ๐))) |
106 | 105 | anbi2d 630 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ โ ((๐ โง (๐ฅ โ ๐ โง ๐ท โค ๐ฅ โง ๐ฅ โค ๐)) โ (๐ โง (๐ โ ๐ โง ๐ท โค ๐ โง ๐ โค ๐)))) |
107 | | csbeq1a 3873 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ โ ๐ต = โฆ๐ / ๐ฅโฆ๐ต) |
108 | 107 | breq2d 5121 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ โ (0 โค ๐ต โ 0 โค โฆ๐ / ๐ฅโฆ๐ต)) |
109 | 106, 108 | imbi12d 345 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ (((๐ โง (๐ฅ โ ๐ โง ๐ท โค ๐ฅ โง ๐ฅ โค ๐)) โ 0 โค ๐ต) โ ((๐ โง (๐ โ ๐ โง ๐ท โค ๐ โง ๐ โค ๐)) โ 0 โค โฆ๐ / ๐ฅโฆ๐ต))) |
110 | | dvfsumlem4.0 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ ๐ โง ๐ท โค ๐ฅ โง ๐ฅ โค ๐)) โ 0 โค ๐ต) |
111 | 101, 109,
110 | vtoclg1f 3526 |
. . . . . . . . 9
โข (๐ โ ๐ โ ((๐ โง (๐ โ ๐ โง ๐ท โค ๐ โง ๐ โค ๐)) โ 0 โค โฆ๐ / ๐ฅโฆ๐ต)) |
112 | 95, 111 | mpcom 38 |
. . . . . . . 8
โข ((๐ โง (๐ โ ๐ โง ๐ท โค ๐ โง ๐ โค ๐)) โ 0 โค โฆ๐ / ๐ฅโฆ๐ต) |
113 | 94, 112 | mpdan 686 |
. . . . . . 7
โข (๐ โ 0 โค
โฆ๐ / ๐ฅโฆ๐ต) |
114 | 80, 75, 85, 113 | mulge0d 11740 |
. . . . . 6
โข (๐ โ 0 โค ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต)) |
115 | 45, 81 | addge02d 11752 |
. . . . . 6
โข (๐ โ (0 โค ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) โ (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โค (((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)))) |
116 | 114, 115 | mpbid 231 |
. . . . 5
โข (๐ โ (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โค (((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด))) |
117 | 45, 82, 75, 116 | lesub1dd 11779 |
. . . 4
โข (๐ โ ((ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โ โฆ๐ / ๐ฅโฆ๐ต) โค ((((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) โ โฆ๐ / ๐ฅโฆ๐ต)) |
118 | | reflcl 13710 |
. . . . . . . . . 10
โข (๐ โ โ โ
(โโ๐) โ
โ) |
119 | 88, 118 | syl 17 |
. . . . . . . . 9
โข (๐ โ (โโ๐) โ
โ) |
120 | 88, 119 | resubcld 11591 |
. . . . . . . 8
โข (๐ โ (๐ โ (โโ๐)) โ โ) |
121 | | csbeq1 3862 |
. . . . . . . . . . 11
โข (๐ = ๐ โ โฆ๐ / ๐ฅโฆ๐ต = โฆ๐ / ๐ฅโฆ๐ต) |
122 | 121 | eleq1d 2819 |
. . . . . . . . . 10
โข (๐ = ๐ โ (โฆ๐ / ๐ฅโฆ๐ต โ โ โ โฆ๐ / ๐ฅโฆ๐ต โ โ)) |
123 | 122 | rspcv 3579 |
. . . . . . . . 9
โข (๐ โ ๐ โ (โ๐ โ ๐ โฆ๐ / ๐ฅโฆ๐ต โ โ โ โฆ๐ / ๐ฅโฆ๐ต โ โ)) |
124 | 1, 71, 123 | sylc 65 |
. . . . . . . 8
โข (๐ โ โฆ๐ / ๐ฅโฆ๐ต โ โ) |
125 | 120, 124 | remulcld 11193 |
. . . . . . 7
โข (๐ โ ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) โ โ) |
126 | 125, 21 | readdcld 11192 |
. . . . . 6
โข (๐ โ (((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) โ โ) |
127 | 126, 124 | resubcld 11591 |
. . . . 5
โข (๐ โ ((((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) โ โฆ๐ / ๐ฅโฆ๐ต) โ โ) |
128 | | dvfsum.m |
. . . . . . . 8
โข (๐ โ ๐ โ โค) |
129 | | dvfsum.d |
. . . . . . . 8
โข (๐ โ ๐ท โ โ) |
130 | | dvfsum.md |
. . . . . . . 8
โข (๐ โ ๐ โค (๐ท + 1)) |
131 | | dvfsum.t |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
132 | | dvfsum.l |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ ๐ โง ๐ โ ๐) โง (๐ท โค ๐ฅ โง ๐ฅ โค ๐ โง ๐ โค ๐)) โ ๐ถ โค ๐ต) |
133 | | eqid 2733 |
. . . . . . . 8
โข (๐ฅ โ ๐ โฆ (((๐ฅ โ (โโ๐ฅ)) ยท ๐ต) + (ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ โ ๐ด))) = (๐ฅ โ ๐ โฆ (((๐ฅ โ (โโ๐ฅ)) ยท ๐ต) + (ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ โ ๐ด))) |
134 | 57, 6, 128, 129, 130, 131, 13, 61, 3, 62, 8, 90, 132, 133, 33, 1, 86, 91, 92 | dvfsumlem3 25415 |
. . . . . . 7
โข (๐ โ (((๐ฅ โ ๐ โฆ (((๐ฅ โ (โโ๐ฅ)) ยท ๐ต) + (ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ โ ๐ด)))โ๐) โค ((๐ฅ โ ๐ โฆ (((๐ฅ โ (โโ๐ฅ)) ยท ๐ต) + (ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ โ ๐ด)))โ๐) โง (((๐ฅ โ ๐ โฆ (((๐ฅ โ (โโ๐ฅ)) ยท ๐ต) + (ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ โ ๐ด)))โ๐) โ โฆ๐ / ๐ฅโฆ๐ต) โค (((๐ฅ โ ๐ โฆ (((๐ฅ โ (โโ๐ฅ)) ยท ๐ต) + (ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ โ ๐ด)))โ๐) โ โฆ๐ / ๐ฅโฆ๐ต))) |
135 | 134 | simprd 497 |
. . . . . 6
โข (๐ โ (((๐ฅ โ ๐ โฆ (((๐ฅ โ (โโ๐ฅ)) ยท ๐ต) + (ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ โ ๐ด)))โ๐) โ โฆ๐ / ๐ฅโฆ๐ต) โค (((๐ฅ โ ๐ โฆ (((๐ฅ โ (โโ๐ฅ)) ยท ๐ต) + (ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ โ ๐ด)))โ๐) โ โฆ๐ / ๐ฅโฆ๐ต)) |
136 | | nfcv 2904 |
. . . . . . . . . . 11
โข
โฒ๐ฅ(๐ โ (โโ๐)) |
137 | | nfcv 2904 |
. . . . . . . . . . 11
โข
โฒ๐ฅ
ยท |
138 | 136, 137,
99 | nfov 7391 |
. . . . . . . . . 10
โข
โฒ๐ฅ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) |
139 | | nfcv 2904 |
. . . . . . . . . 10
โข
โฒ๐ฅ
+ |
140 | 138, 139,
48 | nfov 7391 |
. . . . . . . . 9
โข
โฒ๐ฅ(((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) |
141 | | id 22 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ โ ๐ฅ = ๐) |
142 | 141, 49 | oveq12d 7379 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ โ (๐ฅ โ (โโ๐ฅ)) = (๐ โ (โโ๐))) |
143 | 142, 107 | oveq12d 7379 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ ((๐ฅ โ (โโ๐ฅ)) ยท ๐ต) = ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต)) |
144 | 143, 52 | oveq12d 7379 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ (((๐ฅ โ (โโ๐ฅ)) ยท ๐ต) + (ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ โ ๐ด)) = (((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด))) |
145 | 46, 140, 144, 133 | fvmptf 6973 |
. . . . . . . 8
โข ((๐ โ ๐ โง (((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) โ โ) โ ((๐ฅ โ ๐ โฆ (((๐ฅ โ (โโ๐ฅ)) ยท ๐ต) + (ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ โ ๐ด)))โ๐) = (((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด))) |
146 | 33, 82, 145 | syl2anc 585 |
. . . . . . 7
โข (๐ โ ((๐ฅ โ ๐ โฆ (((๐ฅ โ (โโ๐ฅ)) ยท ๐ต) + (ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ โ ๐ด)))โ๐) = (((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด))) |
147 | 146 | oveq1d 7376 |
. . . . . 6
โข (๐ โ (((๐ฅ โ ๐ โฆ (((๐ฅ โ (โโ๐ฅ)) ยท ๐ต) + (ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ โ ๐ด)))โ๐) โ โฆ๐ / ๐ฅโฆ๐ต) = ((((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) โ โฆ๐ / ๐ฅโฆ๐ต)) |
148 | | nfcv 2904 |
. . . . . . . . . . 11
โข
โฒ๐ฅ(๐ โ (โโ๐)) |
149 | | nfcsb1v 3884 |
. . . . . . . . . . 11
โข
โฒ๐ฅโฆ๐ / ๐ฅโฆ๐ต |
150 | 148, 137,
149 | nfov 7391 |
. . . . . . . . . 10
โข
โฒ๐ฅ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) |
151 | 150, 139,
25 | nfov 7391 |
. . . . . . . . 9
โข
โฒ๐ฅ(((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) |
152 | | id 22 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ โ ๐ฅ = ๐) |
153 | 152, 26 | oveq12d 7379 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ โ (๐ฅ โ (โโ๐ฅ)) = (๐ โ (โโ๐))) |
154 | | csbeq1a 3873 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ โ ๐ต = โฆ๐ / ๐ฅโฆ๐ต) |
155 | 153, 154 | oveq12d 7379 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ ((๐ฅ โ (โโ๐ฅ)) ยท ๐ต) = ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต)) |
156 | 155, 29 | oveq12d 7379 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ (((๐ฅ โ (โโ๐ฅ)) ยท ๐ต) + (ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ โ ๐ด)) = (((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด))) |
157 | 22, 151, 156, 133 | fvmptf 6973 |
. . . . . . . 8
โข ((๐ โ ๐ โง (((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) โ โ) โ ((๐ฅ โ ๐ โฆ (((๐ฅ โ (โโ๐ฅ)) ยท ๐ต) + (ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ โ ๐ด)))โ๐) = (((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด))) |
158 | 1, 126, 157 | syl2anc 585 |
. . . . . . 7
โข (๐ โ ((๐ฅ โ ๐ โฆ (((๐ฅ โ (โโ๐ฅ)) ยท ๐ต) + (ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ โ ๐ด)))โ๐) = (((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด))) |
159 | 158 | oveq1d 7376 |
. . . . . 6
โข (๐ โ (((๐ฅ โ ๐ โฆ (((๐ฅ โ (โโ๐ฅ)) ยท ๐ต) + (ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ โ ๐ด)))โ๐) โ โฆ๐ / ๐ฅโฆ๐ต) = ((((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) โ โฆ๐ / ๐ฅโฆ๐ต)) |
160 | 135, 147,
159 | 3brtr3d 5140 |
. . . . 5
โข (๐ โ ((((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) โ โฆ๐ / ๐ฅโฆ๐ต) โค ((((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) โ โฆ๐ / ๐ฅโฆ๐ต)) |
161 | 21 | recnd 11191 |
. . . . . . . 8
โข (๐ โ (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โ โ) |
162 | 124 | recnd 11191 |
. . . . . . . 8
โข (๐ โ โฆ๐ / ๐ฅโฆ๐ต โ โ) |
163 | 125 | recnd 11191 |
. . . . . . . 8
โข (๐ โ ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) โ โ) |
164 | 161, 162,
163 | subsub3d 11550 |
. . . . . . 7
โข (๐ โ ((ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โ (โฆ๐ / ๐ฅโฆ๐ต โ ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต))) = (((ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) + ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต)) โ โฆ๐ / ๐ฅโฆ๐ต)) |
165 | 161, 163 | addcomd 11365 |
. . . . . . . 8
โข (๐ โ ((ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) + ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต)) = (((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด))) |
166 | 165 | oveq1d 7376 |
. . . . . . 7
โข (๐ โ (((ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) + ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต)) โ โฆ๐ / ๐ฅโฆ๐ต) = ((((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) โ โฆ๐ / ๐ฅโฆ๐ต)) |
167 | 164, 166 | eqtrd 2773 |
. . . . . 6
โข (๐ โ ((ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โ (โฆ๐ / ๐ฅโฆ๐ต โ ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต))) = ((((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) โ โฆ๐ / ๐ฅโฆ๐ต)) |
168 | | 1red 11164 |
. . . . . . . . . 10
โข (๐ โ 1 โ
โ) |
169 | 129, 77, 88, 86, 91 | letrd 11320 |
. . . . . . . . . . . 12
โข (๐ โ ๐ท โค ๐) |
170 | 1, 169, 92 | 3jca 1129 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ ๐ โง ๐ท โค ๐ โง ๐ โค ๐)) |
171 | | simpr1 1195 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐ โง ๐ท โค ๐ โง ๐ โค ๐)) โ ๐ โ ๐) |
172 | | nfv 1918 |
. . . . . . . . . . . . . 14
โข
โฒ๐ฅ(๐ โง (๐ โ ๐ โง ๐ท โค ๐ โง ๐ โค ๐)) |
173 | 97, 98, 149 | nfbr 5156 |
. . . . . . . . . . . . . 14
โข
โฒ๐ฅ0 โค
โฆ๐ / ๐ฅโฆ๐ต |
174 | 172, 173 | nfim 1900 |
. . . . . . . . . . . . 13
โข
โฒ๐ฅ((๐ โง (๐ โ ๐ โง ๐ท โค ๐ โง ๐ โค ๐)) โ 0 โค โฆ๐ / ๐ฅโฆ๐ต) |
175 | | eleq1 2822 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = ๐ โ (๐ฅ โ ๐ โ ๐ โ ๐)) |
176 | | breq2 5113 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = ๐ โ (๐ท โค ๐ฅ โ ๐ท โค ๐)) |
177 | | breq1 5112 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = ๐ โ (๐ฅ โค ๐ โ ๐ โค ๐)) |
178 | 175, 176,
177 | 3anbi123d 1437 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ โ ((๐ฅ โ ๐ โง ๐ท โค ๐ฅ โง ๐ฅ โค ๐) โ (๐ โ ๐ โง ๐ท โค ๐ โง ๐ โค ๐))) |
179 | 178 | anbi2d 630 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ โ ((๐ โง (๐ฅ โ ๐ โง ๐ท โค ๐ฅ โง ๐ฅ โค ๐)) โ (๐ โง (๐ โ ๐ โง ๐ท โค ๐ โง ๐ โค ๐)))) |
180 | 154 | breq2d 5121 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ โ (0 โค ๐ต โ 0 โค โฆ๐ / ๐ฅโฆ๐ต)) |
181 | 179, 180 | imbi12d 345 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ โ (((๐ โง (๐ฅ โ ๐ โง ๐ท โค ๐ฅ โง ๐ฅ โค ๐)) โ 0 โค ๐ต) โ ((๐ โง (๐ โ ๐ โง ๐ท โค ๐ โง ๐ โค ๐)) โ 0 โค โฆ๐ / ๐ฅโฆ๐ต))) |
182 | 174, 181,
110 | vtoclg1f 3526 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ ((๐ โง (๐ โ ๐ โง ๐ท โค ๐ โง ๐ โค ๐)) โ 0 โค โฆ๐ / ๐ฅโฆ๐ต)) |
183 | 171, 182 | mpcom 38 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐ โง ๐ท โค ๐ โง ๐ โค ๐)) โ 0 โค โฆ๐ / ๐ฅโฆ๐ต) |
184 | 170, 183 | mpdan 686 |
. . . . . . . . . 10
โข (๐ โ 0 โค
โฆ๐ / ๐ฅโฆ๐ต) |
185 | | fracle1 13717 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ โ (โโ๐)) โค 1) |
186 | 88, 185 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (๐ โ (โโ๐)) โค 1) |
187 | 120, 168,
124, 184, 186 | lemul1ad 12102 |
. . . . . . . . 9
โข (๐ โ ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) โค (1 ยท โฆ๐ / ๐ฅโฆ๐ต)) |
188 | 162 | mullidd 11181 |
. . . . . . . . 9
โข (๐ โ (1 ยท
โฆ๐ / ๐ฅโฆ๐ต) = โฆ๐ / ๐ฅโฆ๐ต) |
189 | 187, 188 | breqtrd 5135 |
. . . . . . . 8
โข (๐ โ ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) โค โฆ๐ / ๐ฅโฆ๐ต) |
190 | 124, 125 | subge0d 11753 |
. . . . . . . 8
โข (๐ โ (0 โค
(โฆ๐ / ๐ฅโฆ๐ต โ ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต)) โ ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) โค โฆ๐ / ๐ฅโฆ๐ต)) |
191 | 189, 190 | mpbird 257 |
. . . . . . 7
โข (๐ โ 0 โค
(โฆ๐ / ๐ฅโฆ๐ต โ ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต))) |
192 | 124, 125 | resubcld 11591 |
. . . . . . . 8
โข (๐ โ (โฆ๐ / ๐ฅโฆ๐ต โ ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต)) โ โ) |
193 | 21, 192 | subge02d 11755 |
. . . . . . 7
โข (๐ โ (0 โค
(โฆ๐ / ๐ฅโฆ๐ต โ ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต)) โ ((ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โ (โฆ๐ / ๐ฅโฆ๐ต โ ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต))) โค (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด))) |
194 | 191, 193 | mpbid 231 |
. . . . . 6
โข (๐ โ ((ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โ (โฆ๐ / ๐ฅโฆ๐ต โ ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต))) โค (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) |
195 | 167, 194 | eqbrtrrd 5133 |
. . . . 5
โข (๐ โ ((((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) โ โฆ๐ / ๐ฅโฆ๐ต) โค (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) |
196 | 83, 127, 21, 160, 195 | letrd 11320 |
. . . 4
โข (๐ โ ((((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) โ โฆ๐ / ๐ฅโฆ๐ต) โค (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) |
197 | 76, 83, 21, 117, 196 | letrd 11320 |
. . 3
โข (๐ โ ((ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โ โฆ๐ / ๐ฅโฆ๐ต) โค (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) |
198 | 75, 45 | readdcld 11192 |
. . . . 5
โข (๐ โ (โฆ๐ / ๐ฅโฆ๐ต + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) โ โ) |
199 | | fracge0 13718 |
. . . . . . . . 9
โข (๐ โ โ โ 0 โค
(๐ โ
(โโ๐))) |
200 | 88, 199 | syl 17 |
. . . . . . . 8
โข (๐ โ 0 โค (๐ โ (โโ๐))) |
201 | 120, 124,
200, 184 | mulge0d 11740 |
. . . . . . 7
โข (๐ โ 0 โค ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต)) |
202 | 21, 125 | addge02d 11752 |
. . . . . . 7
โข (๐ โ (0 โค ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) โ (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โค (((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)))) |
203 | 201, 202 | mpbid 231 |
. . . . . 6
โข (๐ โ (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โค (((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด))) |
204 | 134 | simpld 496 |
. . . . . . 7
โข (๐ โ ((๐ฅ โ ๐ โฆ (((๐ฅ โ (โโ๐ฅ)) ยท ๐ต) + (ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ โ ๐ด)))โ๐) โค ((๐ฅ โ ๐ โฆ (((๐ฅ โ (โโ๐ฅ)) ยท ๐ต) + (ฮฃ๐ โ (๐...(โโ๐ฅ))๐ถ โ ๐ด)))โ๐)) |
205 | 204, 158,
146 | 3brtr3d 5140 |
. . . . . 6
โข (๐ โ (((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) โค (((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด))) |
206 | 21, 126, 82, 203, 205 | letrd 11320 |
. . . . 5
โข (๐ โ (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โค (((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด))) |
207 | | fracle1 13717 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ โ (โโ๐)) โค 1) |
208 | 77, 207 | syl 17 |
. . . . . . . 8
โข (๐ โ (๐ โ (โโ๐)) โค 1) |
209 | 80, 168, 75, 113, 208 | lemul1ad 12102 |
. . . . . . 7
โข (๐ โ ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) โค (1 ยท โฆ๐ / ๐ฅโฆ๐ต)) |
210 | 75 | recnd 11191 |
. . . . . . . 8
โข (๐ โ โฆ๐ / ๐ฅโฆ๐ต โ โ) |
211 | 210 | mullidd 11181 |
. . . . . . 7
โข (๐ โ (1 ยท
โฆ๐ / ๐ฅโฆ๐ต) = โฆ๐ / ๐ฅโฆ๐ต) |
212 | 209, 211 | breqtrd 5135 |
. . . . . 6
โข (๐ โ ((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) โค โฆ๐ / ๐ฅโฆ๐ต) |
213 | 81, 75, 45, 212 | leadd1dd 11777 |
. . . . 5
โข (๐ โ (((๐ โ (โโ๐)) ยท โฆ๐ / ๐ฅโฆ๐ต) + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) โค (โฆ๐ / ๐ฅโฆ๐ต + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด))) |
214 | 21, 82, 198, 206, 213 | letrd 11320 |
. . . 4
โข (๐ โ (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โค (โฆ๐ / ๐ฅโฆ๐ต + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด))) |
215 | 45 | recnd 11191 |
. . . . 5
โข (๐ โ (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โ โ) |
216 | 210, 215 | addcomd 11365 |
. . . 4
โข (๐ โ (โฆ๐ / ๐ฅโฆ๐ต + (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด)) = ((ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) + โฆ๐ / ๐ฅโฆ๐ต)) |
217 | 214, 216 | breqtrd 5135 |
. . 3
โข (๐ โ (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โค ((ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) + โฆ๐ / ๐ฅโฆ๐ต)) |
218 | 21, 45, 75 | absdifled 15328 |
. . 3
โข (๐ โ ((absโ((ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โ (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด))) โค โฆ๐ / ๐ฅโฆ๐ต โ (((ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โ โฆ๐ / ๐ฅโฆ๐ต) โค (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โง (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โค ((ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) + โฆ๐ / ๐ฅโฆ๐ต)))) |
219 | 197, 217,
218 | mpbir2and 712 |
. 2
โข (๐ โ (absโ((ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด) โ (ฮฃ๐ โ (๐...(โโ๐))๐ถ โ โฆ๐ / ๐ฅโฆ๐ด))) โค โฆ๐ / ๐ฅโฆ๐ต) |
220 | 56, 219 | eqbrtrd 5131 |
1
โข (๐ โ (absโ((๐บโ๐) โ (๐บโ๐))) โค โฆ๐ / ๐ฅโฆ๐ต) |