Step | Hyp | Ref
| Expression |
1 | | fourierdlem30.b |
. . . . . . . . . . 11
โข (๐ โ ๐ต โ โ) |
2 | | fourierdlem30.r |
. . . . . . . . . . . 12
โข (๐ โ ๐
โ โ) |
3 | 2 | recnd 11188 |
. . . . . . . . . . 11
โข (๐ โ ๐
โ โ) |
4 | | 0red 11163 |
. . . . . . . . . . . . 13
โข (๐ โ 0 โ
โ) |
5 | | 1red 11161 |
. . . . . . . . . . . . 13
โข (๐ โ 1 โ
โ) |
6 | | 0lt1 11682 |
. . . . . . . . . . . . . 14
โข 0 <
1 |
7 | 6 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ 0 < 1) |
8 | | fourierdlem30.x |
. . . . . . . . . . . . . . . . . . 19
โข ๐ = (absโ๐ด) |
9 | | fourierdlem30.a |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐ด โ โ) |
10 | 9 | abscld 15327 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (absโ๐ด) โ
โ) |
11 | 8, 10 | eqeltrid 2838 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐ โ โ) |
12 | | fourierdlem30.y |
. . . . . . . . . . . . . . . . . . 19
โข ๐ = (absโ๐ถ) |
13 | | fourierdlem30.c |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐ถ โ โ) |
14 | 13 | abscld 15327 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (absโ๐ถ) โ
โ) |
15 | 12, 14 | eqeltrid 2838 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐ โ โ) |
16 | 11, 15 | readdcld 11189 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ + ๐) โ โ) |
17 | | fourierdlem30.z |
. . . . . . . . . . . . . . . . . 18
โข ๐ = (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ) |
18 | | fourierlemreimleblemlte22.f |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ฅ โ ๐ผ) โ ๐น โ โ) |
19 | | fourierdlem30.g |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ฅ โ ๐ผ) โ ๐บ โ โ) |
20 | 19 | negcld 11504 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ฅ โ ๐ผ) โ -๐บ โ โ) |
21 | 18, 20 | mulcld 11180 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ฅ โ ๐ผ) โ (๐น ยท -๐บ) โ โ) |
22 | | fourierdlem30.ibl |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐ฅ โ ๐ผ โฆ (๐น ยท -๐บ)) โ
๐ฟ1) |
23 | 21, 22 | itgcl 25164 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โซ๐ผ(๐น ยท -๐บ) d๐ฅ โ โ) |
24 | 23 | abscld 15327 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ) โ โ) |
25 | 17, 24 | eqeltrid 2838 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ โ โ) |
26 | 16, 25 | readdcld 11189 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ + ๐) + ๐) โ โ) |
27 | | fourierdlem30.e |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ธ โ
โ+) |
28 | 27 | rpred 12962 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ธ โ โ) |
29 | 27 | rpne0d 12967 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ธ โ 0) |
30 | 26, 28, 29 | redivcld 11988 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((๐ + ๐) + ๐) / ๐ธ) โ โ) |
31 | 30, 5 | readdcld 11189 |
. . . . . . . . . . . . . 14
โข (๐ โ ((((๐ + ๐) + ๐) / ๐ธ) + 1) โ โ) |
32 | 9 | absge0d 15335 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ 0 โค (absโ๐ด)) |
33 | 32, 8 | breqtrrdi 5148 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 0 โค ๐) |
34 | 13 | absge0d 15335 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ 0 โค (absโ๐ถ)) |
35 | 34, 12 | breqtrrdi 5148 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 0 โค ๐) |
36 | 11, 15, 33, 35 | addge0d 11736 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 0 โค (๐ + ๐)) |
37 | 23 | absge0d 15335 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 0 โค
(absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) |
38 | 37, 17 | breqtrrdi 5148 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 0 โค ๐) |
39 | 16, 25, 36, 38 | addge0d 11736 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 0 โค ((๐ + ๐) + ๐)) |
40 | 26, 27, 39 | divge0d 13002 |
. . . . . . . . . . . . . . 15
โข (๐ โ 0 โค (((๐ + ๐) + ๐) / ๐ธ)) |
41 | 5, 30 | addge02d 11749 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0 โค (((๐ + ๐) + ๐) / ๐ธ) โ 1 โค ((((๐ + ๐) + ๐) / ๐ธ) + 1))) |
42 | 40, 41 | mpbid 231 |
. . . . . . . . . . . . . 14
โข (๐ โ 1 โค ((((๐ + ๐) + ๐) / ๐ธ) + 1)) |
43 | | fourierdlem30.ler |
. . . . . . . . . . . . . 14
โข (๐ โ ((((๐ + ๐) + ๐) / ๐ธ) + 1) โค ๐
) |
44 | 5, 31, 2, 42, 43 | letrd 11317 |
. . . . . . . . . . . . 13
โข (๐ โ 1 โค ๐
) |
45 | 4, 5, 2, 7, 44 | ltletrd 11320 |
. . . . . . . . . . . 12
โข (๐ โ 0 < ๐
) |
46 | 45 | gt0ne0d 11724 |
. . . . . . . . . . 11
โข (๐ โ ๐
โ 0) |
47 | 1, 3, 46 | divnegd 11949 |
. . . . . . . . . 10
โข (๐ โ -(๐ต / ๐
) = (-๐ต / ๐
)) |
48 | 47 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ โ (๐ด ยท -(๐ต / ๐
)) = (๐ด ยท (-๐ต / ๐
))) |
49 | 1 | negcld 11504 |
. . . . . . . . . 10
โข (๐ โ -๐ต โ โ) |
50 | 9, 49, 3, 46 | divassd 11971 |
. . . . . . . . 9
โข (๐ โ ((๐ด ยท -๐ต) / ๐
) = (๐ด ยท (-๐ต / ๐
))) |
51 | 48, 50 | eqtr4d 2776 |
. . . . . . . 8
โข (๐ โ (๐ด ยท -(๐ต / ๐
)) = ((๐ด ยท -๐ต) / ๐
)) |
52 | | fourierdlem30.d |
. . . . . . . . . . 11
โข (๐ โ ๐ท โ โ) |
53 | 52, 3, 46 | divnegd 11949 |
. . . . . . . . . 10
โข (๐ โ -(๐ท / ๐
) = (-๐ท / ๐
)) |
54 | 53 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ โ (๐ถ ยท -(๐ท / ๐
)) = (๐ถ ยท (-๐ท / ๐
))) |
55 | 52 | negcld 11504 |
. . . . . . . . . 10
โข (๐ โ -๐ท โ โ) |
56 | 13, 55, 3, 46 | divassd 11971 |
. . . . . . . . 9
โข (๐ โ ((๐ถ ยท -๐ท) / ๐
) = (๐ถ ยท (-๐ท / ๐
))) |
57 | 54, 56 | eqtr4d 2776 |
. . . . . . . 8
โข (๐ โ (๐ถ ยท -(๐ท / ๐
)) = ((๐ถ ยท -๐ท) / ๐
)) |
58 | 51, 57 | oveq12d 7376 |
. . . . . . 7
โข (๐ โ ((๐ด ยท -(๐ต / ๐
)) โ (๐ถ ยท -(๐ท / ๐
))) = (((๐ด ยท -๐ต) / ๐
) โ ((๐ถ ยท -๐ท) / ๐
))) |
59 | 9, 49 | mulcld 11180 |
. . . . . . . 8
โข (๐ โ (๐ด ยท -๐ต) โ โ) |
60 | 13, 55 | mulcld 11180 |
. . . . . . . 8
โข (๐ โ (๐ถ ยท -๐ท) โ โ) |
61 | 59, 60, 3, 46 | divsubdird 11975 |
. . . . . . 7
โข (๐ โ (((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท)) / ๐
) = (((๐ด ยท -๐ต) / ๐
) โ ((๐ถ ยท -๐ท) / ๐
))) |
62 | 58, 61 | eqtr4d 2776 |
. . . . . 6
โข (๐ โ ((๐ด ยท -(๐ต / ๐
)) โ (๐ถ ยท -(๐ท / ๐
))) = (((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท)) / ๐
)) |
63 | 3, 46 | reccld 11929 |
. . . . . . . 8
โข (๐ โ (1 / ๐
) โ โ) |
64 | 63, 21, 22 | itgmulc2 25214 |
. . . . . . 7
โข (๐ โ ((1 / ๐
) ยท โซ๐ผ(๐น ยท -๐บ) d๐ฅ) = โซ๐ผ((1 / ๐
) ยท (๐น ยท -๐บ)) d๐ฅ) |
65 | 23, 3, 46 | divrec2d 11940 |
. . . . . . 7
โข (๐ โ (โซ๐ผ(๐น ยท -๐บ) d๐ฅ / ๐
) = ((1 / ๐
) ยท โซ๐ผ(๐น ยท -๐บ) d๐ฅ)) |
66 | 3 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ผ) โ ๐
โ โ) |
67 | 46 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ผ) โ ๐
โ 0) |
68 | 19, 66, 67 | divnegd 11949 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ผ) โ -(๐บ / ๐
) = (-๐บ / ๐
)) |
69 | 68 | oveq2d 7374 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ผ) โ (๐น ยท -(๐บ / ๐
)) = (๐น ยท (-๐บ / ๐
))) |
70 | 18, 20, 66, 67 | divassd 11971 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ผ) โ ((๐น ยท -๐บ) / ๐
) = (๐น ยท (-๐บ / ๐
))) |
71 | 21, 66, 67 | divrec2d 11940 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ผ) โ ((๐น ยท -๐บ) / ๐
) = ((1 / ๐
) ยท (๐น ยท -๐บ))) |
72 | 69, 70, 71 | 3eqtr2d 2779 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ผ) โ (๐น ยท -(๐บ / ๐
)) = ((1 / ๐
) ยท (๐น ยท -๐บ))) |
73 | 72 | itgeq2dv 25162 |
. . . . . . 7
โข (๐ โ โซ๐ผ(๐น ยท -(๐บ / ๐
)) d๐ฅ = โซ๐ผ((1 / ๐
) ยท (๐น ยท -๐บ)) d๐ฅ) |
74 | 64, 65, 73 | 3eqtr4rd 2784 |
. . . . . 6
โข (๐ โ โซ๐ผ(๐น ยท -(๐บ / ๐
)) d๐ฅ = (โซ๐ผ(๐น ยท -๐บ) d๐ฅ / ๐
)) |
75 | 62, 74 | oveq12d 7376 |
. . . . 5
โข (๐ โ (((๐ด ยท -(๐ต / ๐
)) โ (๐ถ ยท -(๐ท / ๐
))) โ โซ๐ผ(๐น ยท -(๐บ / ๐
)) d๐ฅ) = ((((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท)) / ๐
) โ (โซ๐ผ(๐น ยท -๐บ) d๐ฅ / ๐
))) |
76 | 59, 60 | subcld 11517 |
. . . . . 6
โข (๐ โ ((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท)) โ โ) |
77 | 76, 23, 3, 46 | divsubdird 11975 |
. . . . 5
โข (๐ โ ((((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท)) โ โซ๐ผ(๐น ยท -๐บ) d๐ฅ) / ๐
) = ((((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท)) / ๐
) โ (โซ๐ผ(๐น ยท -๐บ) d๐ฅ / ๐
))) |
78 | 75, 77 | eqtr4d 2776 |
. . . 4
โข (๐ โ (((๐ด ยท -(๐ต / ๐
)) โ (๐ถ ยท -(๐ท / ๐
))) โ โซ๐ผ(๐น ยท -(๐บ / ๐
)) d๐ฅ) = ((((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท)) โ โซ๐ผ(๐น ยท -๐บ) d๐ฅ) / ๐
)) |
79 | 78 | fveq2d 6847 |
. . 3
โข (๐ โ (absโ(((๐ด ยท -(๐ต / ๐
)) โ (๐ถ ยท -(๐ท / ๐
))) โ โซ๐ผ(๐น ยท -(๐บ / ๐
)) d๐ฅ)) = (absโ((((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท)) โ โซ๐ผ(๐น ยท -๐บ) d๐ฅ) / ๐
))) |
80 | 76, 23 | subcld 11517 |
. . . 4
โข (๐ โ (((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท)) โ โซ๐ผ(๐น ยท -๐บ) d๐ฅ) โ โ) |
81 | 80, 3, 46 | absdivd 15346 |
. . 3
โข (๐ โ (absโ((((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท)) โ โซ๐ผ(๐น ยท -๐บ) d๐ฅ) / ๐
)) = ((absโ(((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท)) โ โซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / (absโ๐
))) |
82 | 4, 2, 45 | ltled 11308 |
. . . . 5
โข (๐ โ 0 โค ๐
) |
83 | 2, 82 | absidd 15313 |
. . . 4
โข (๐ โ (absโ๐
) = ๐
) |
84 | 83 | oveq2d 7374 |
. . 3
โข (๐ โ ((absโ(((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท)) โ โซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / (absโ๐
)) = ((absโ(((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท)) โ โซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / ๐
)) |
85 | 79, 81, 84 | 3eqtrd 2777 |
. 2
โข (๐ โ (absโ(((๐ด ยท -(๐ต / ๐
)) โ (๐ถ ยท -(๐ท / ๐
))) โ โซ๐ผ(๐น ยท -(๐บ / ๐
)) d๐ฅ)) = ((absโ(((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท)) โ โซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / ๐
)) |
86 | 80 | abscld 15327 |
. . . 4
โข (๐ โ (absโ(((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท)) โ โซ๐ผ(๐น ยท -๐บ) d๐ฅ)) โ โ) |
87 | 86, 2, 46 | redivcld 11988 |
. . 3
โข (๐ โ ((absโ(((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท)) โ โซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / ๐
) โ โ) |
88 | 10, 14 | readdcld 11189 |
. . . . 5
โข (๐ โ ((absโ๐ด) + (absโ๐ถ)) โ โ) |
89 | 88, 24 | readdcld 11189 |
. . . 4
โข (๐ โ (((absโ๐ด) + (absโ๐ถ)) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) โ โ) |
90 | 89, 2, 46 | redivcld 11988 |
. . 3
โข (๐ โ ((((absโ๐ด) + (absโ๐ถ)) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / ๐
) โ โ) |
91 | 2, 45 | elrpd 12959 |
. . . 4
โข (๐ โ ๐
โ
โ+) |
92 | 76 | abscld 15327 |
. . . . . 6
โข (๐ โ (absโ((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท))) โ โ) |
93 | 92, 24 | readdcld 11189 |
. . . . 5
โข (๐ โ ((absโ((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท))) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) โ โ) |
94 | 76, 23 | abs2dif2d 15349 |
. . . . 5
โข (๐ โ (absโ(((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท)) โ โซ๐ผ(๐น ยท -๐บ) d๐ฅ)) โค ((absโ((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท))) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ))) |
95 | 59 | abscld 15327 |
. . . . . . . 8
โข (๐ โ (absโ(๐ด ยท -๐ต)) โ โ) |
96 | 60 | abscld 15327 |
. . . . . . . 8
โข (๐ โ (absโ(๐ถ ยท -๐ท)) โ โ) |
97 | 95, 96 | readdcld 11189 |
. . . . . . 7
โข (๐ โ ((absโ(๐ด ยท -๐ต)) + (absโ(๐ถ ยท -๐ท))) โ โ) |
98 | 59, 60 | abs2dif2d 15349 |
. . . . . . 7
โข (๐ โ (absโ((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท))) โค ((absโ(๐ด ยท -๐ต)) + (absโ(๐ถ ยท -๐ท)))) |
99 | 9, 49 | absmuld 15345 |
. . . . . . . . 9
โข (๐ โ (absโ(๐ด ยท -๐ต)) = ((absโ๐ด) ยท (absโ-๐ต))) |
100 | 49 | abscld 15327 |
. . . . . . . . . . 11
โข (๐ โ (absโ-๐ต) โ
โ) |
101 | 1 | absnegd 15340 |
. . . . . . . . . . . 12
โข (๐ โ (absโ-๐ต) = (absโ๐ต)) |
102 | | fourierdlem30.12 |
. . . . . . . . . . . 12
โข (๐ โ (absโ๐ต) โค 1) |
103 | 101, 102 | eqbrtrd 5128 |
. . . . . . . . . . 11
โข (๐ โ (absโ-๐ต) โค 1) |
104 | 100, 5, 10, 32, 103 | lemul2ad 12100 |
. . . . . . . . . 10
โข (๐ โ ((absโ๐ด) ยท (absโ-๐ต)) โค ((absโ๐ด) ยท 1)) |
105 | 10 | recnd 11188 |
. . . . . . . . . . 11
โข (๐ โ (absโ๐ด) โ
โ) |
106 | 105 | mulid1d 11177 |
. . . . . . . . . 10
โข (๐ โ ((absโ๐ด) ยท 1) = (absโ๐ด)) |
107 | 104, 106 | breqtrd 5132 |
. . . . . . . . 9
โข (๐ โ ((absโ๐ด) ยท (absโ-๐ต)) โค (absโ๐ด)) |
108 | 99, 107 | eqbrtrd 5128 |
. . . . . . . 8
โข (๐ โ (absโ(๐ด ยท -๐ต)) โค (absโ๐ด)) |
109 | 13, 55 | absmuld 15345 |
. . . . . . . . 9
โข (๐ โ (absโ(๐ถ ยท -๐ท)) = ((absโ๐ถ) ยท (absโ-๐ท))) |
110 | 55 | abscld 15327 |
. . . . . . . . . . 11
โข (๐ โ (absโ-๐ท) โ
โ) |
111 | 52 | absnegd 15340 |
. . . . . . . . . . . 12
โข (๐ โ (absโ-๐ท) = (absโ๐ท)) |
112 | | fourierdlem30.14 |
. . . . . . . . . . . 12
โข (๐ โ (absโ๐ท) โค 1) |
113 | 111, 112 | eqbrtrd 5128 |
. . . . . . . . . . 11
โข (๐ โ (absโ-๐ท) โค 1) |
114 | 110, 5, 14, 34, 113 | lemul2ad 12100 |
. . . . . . . . . 10
โข (๐ โ ((absโ๐ถ) ยท (absโ-๐ท)) โค ((absโ๐ถ) ยท 1)) |
115 | 14 | recnd 11188 |
. . . . . . . . . . 11
โข (๐ โ (absโ๐ถ) โ
โ) |
116 | 115 | mulid1d 11177 |
. . . . . . . . . 10
โข (๐ โ ((absโ๐ถ) ยท 1) = (absโ๐ถ)) |
117 | 114, 116 | breqtrd 5132 |
. . . . . . . . 9
โข (๐ โ ((absโ๐ถ) ยท (absโ-๐ท)) โค (absโ๐ถ)) |
118 | 109, 117 | eqbrtrd 5128 |
. . . . . . . 8
โข (๐ โ (absโ(๐ถ ยท -๐ท)) โค (absโ๐ถ)) |
119 | 95, 96, 10, 14, 108, 118 | le2addd 11779 |
. . . . . . 7
โข (๐ โ ((absโ(๐ด ยท -๐ต)) + (absโ(๐ถ ยท -๐ท))) โค ((absโ๐ด) + (absโ๐ถ))) |
120 | 92, 97, 88, 98, 119 | letrd 11317 |
. . . . . 6
โข (๐ โ (absโ((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท))) โค ((absโ๐ด) + (absโ๐ถ))) |
121 | 92, 88, 24, 120 | leadd1dd 11774 |
. . . . 5
โข (๐ โ ((absโ((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท))) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) โค (((absโ๐ด) + (absโ๐ถ)) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ))) |
122 | 86, 93, 89, 94, 121 | letrd 11317 |
. . . 4
โข (๐ โ (absโ(((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท)) โ โซ๐ผ(๐น ยท -๐บ) d๐ฅ)) โค (((absโ๐ด) + (absโ๐ถ)) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ))) |
123 | 86, 89, 91, 122 | lediv1dd 13020 |
. . 3
โข (๐ โ ((absโ(((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท)) โ โซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / ๐
) โค ((((absโ๐ด) + (absโ๐ถ)) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / ๐
)) |
124 | 30 | ltp1d 12090 |
. . . . . . 7
โข (๐ โ (((๐ + ๐) + ๐) / ๐ธ) < ((((๐ + ๐) + ๐) / ๐ธ) + 1)) |
125 | 4, 30, 31, 40, 124 | lelttrd 11318 |
. . . . . 6
โข (๐ โ 0 < ((((๐ + ๐) + ๐) / ๐ธ) + 1)) |
126 | 125 | gt0ne0d 11724 |
. . . . 5
โข (๐ โ ((((๐ + ๐) + ๐) / ๐ธ) + 1) โ 0) |
127 | 89, 31, 126 | redivcld 11988 |
. . . 4
โข (๐ โ ((((absโ๐ด) + (absโ๐ถ)) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / ((((๐ + ๐) + ๐) / ๐ธ) + 1)) โ โ) |
128 | 30, 40 | ge0p1rpd 12992 |
. . . . 5
โข (๐ โ ((((๐ + ๐) + ๐) / ๐ธ) + 1) โ
โ+) |
129 | 8 | eqcomi 2742 |
. . . . . . . 8
โข
(absโ๐ด) =
๐ |
130 | 12 | eqcomi 2742 |
. . . . . . . 8
โข
(absโ๐ถ) =
๐ |
131 | 129, 130 | oveq12i 7370 |
. . . . . . 7
โข
((absโ๐ด) +
(absโ๐ถ)) = (๐ + ๐) |
132 | 17 | eqcomi 2742 |
. . . . . . 7
โข
(absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ) = ๐ |
133 | 131, 132 | oveq12i 7370 |
. . . . . 6
โข
(((absโ๐ด) +
(absโ๐ถ)) +
(absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) = ((๐ + ๐) + ๐) |
134 | 39, 133 | breqtrrdi 5148 |
. . . . 5
โข (๐ โ 0 โค (((absโ๐ด) + (absโ๐ถ)) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ))) |
135 | 128, 91, 89, 134, 43 | lediv2ad 12984 |
. . . 4
โข (๐ โ ((((absโ๐ด) + (absโ๐ถ)) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / ๐
) โค ((((absโ๐ด) + (absโ๐ถ)) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / ((((๐ + ๐) + ๐) / ๐ธ) + 1))) |
136 | 133 | oveq1i 7368 |
. . . . 5
โข
((((absโ๐ด) +
(absโ๐ถ)) +
(absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / ((((๐ + ๐) + ๐) / ๐ธ) + 1)) = (((๐ + ๐) + ๐) / ((((๐ + ๐) + ๐) / ๐ธ) + 1)) |
137 | | oveq1 7365 |
. . . . . . . . 9
โข (((๐ + ๐) + ๐) = 0 โ (((๐ + ๐) + ๐) / ((((๐ + ๐) + ๐) / ๐ธ) + 1)) = (0 / ((((๐ + ๐) + ๐) / ๐ธ) + 1))) |
138 | 137 | adantl 483 |
. . . . . . . 8
โข ((๐ โง ((๐ + ๐) + ๐) = 0) โ (((๐ + ๐) + ๐) / ((((๐ + ๐) + ๐) / ๐ธ) + 1)) = (0 / ((((๐ + ๐) + ๐) / ๐ธ) + 1))) |
139 | 30 | recnd 11188 |
. . . . . . . . . . 11
โข (๐ โ (((๐ + ๐) + ๐) / ๐ธ) โ โ) |
140 | 5 | recnd 11188 |
. . . . . . . . . . 11
โข (๐ โ 1 โ
โ) |
141 | 139, 140 | addcld 11179 |
. . . . . . . . . 10
โข (๐ โ ((((๐ + ๐) + ๐) / ๐ธ) + 1) โ โ) |
142 | 141 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ((๐ + ๐) + ๐) = 0) โ ((((๐ + ๐) + ๐) / ๐ธ) + 1) โ โ) |
143 | | oveq1 7365 |
. . . . . . . . . . . . . 14
โข (((๐ + ๐) + ๐) = 0 โ (((๐ + ๐) + ๐) / ๐ธ) = (0 / ๐ธ)) |
144 | 143 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ + ๐) + ๐) = 0) โ (((๐ + ๐) + ๐) / ๐ธ) = (0 / ๐ธ)) |
145 | 27 | rpcnd 12964 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ธ โ โ) |
146 | 145 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ + ๐) + ๐) = 0) โ ๐ธ โ โ) |
147 | 29 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ + ๐) + ๐) = 0) โ ๐ธ โ 0) |
148 | 146, 147 | div0d 11935 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ + ๐) + ๐) = 0) โ (0 / ๐ธ) = 0) |
149 | 144, 148 | eqtrd 2773 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ + ๐) + ๐) = 0) โ (((๐ + ๐) + ๐) / ๐ธ) = 0) |
150 | 149 | oveq1d 7373 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ + ๐) + ๐) = 0) โ ((((๐ + ๐) + ๐) / ๐ธ) + 1) = (0 + 1)) |
151 | | 0p1e1 12280 |
. . . . . . . . . . 11
โข (0 + 1) =
1 |
152 | 150, 151 | eqtrdi 2789 |
. . . . . . . . . 10
โข ((๐ โง ((๐ + ๐) + ๐) = 0) โ ((((๐ + ๐) + ๐) / ๐ธ) + 1) = 1) |
153 | | ax-1ne0 11125 |
. . . . . . . . . . 11
โข 1 โ
0 |
154 | 153 | a1i 11 |
. . . . . . . . . 10
โข ((๐ โง ((๐ + ๐) + ๐) = 0) โ 1 โ 0) |
155 | 152, 154 | eqnetrd 3008 |
. . . . . . . . 9
โข ((๐ โง ((๐ + ๐) + ๐) = 0) โ ((((๐ + ๐) + ๐) / ๐ธ) + 1) โ 0) |
156 | 142, 155 | div0d 11935 |
. . . . . . . 8
โข ((๐ โง ((๐ + ๐) + ๐) = 0) โ (0 / ((((๐ + ๐) + ๐) / ๐ธ) + 1)) = 0) |
157 | 138, 156 | eqtrd 2773 |
. . . . . . 7
โข ((๐ โง ((๐ + ๐) + ๐) = 0) โ (((๐ + ๐) + ๐) / ((((๐ + ๐) + ๐) / ๐ธ) + 1)) = 0) |
158 | 27 | rpgt0d 12965 |
. . . . . . . 8
โข (๐ โ 0 < ๐ธ) |
159 | 158 | adantr 482 |
. . . . . . 7
โข ((๐ โง ((๐ + ๐) + ๐) = 0) โ 0 < ๐ธ) |
160 | 157, 159 | eqbrtrd 5128 |
. . . . . 6
โข ((๐ โง ((๐ + ๐) + ๐) = 0) โ (((๐ + ๐) + ๐) / ((((๐ + ๐) + ๐) / ๐ธ) + 1)) < ๐ธ) |
161 | 26 | adantr 482 |
. . . . . . 7
โข ((๐ โง ยฌ ((๐ + ๐) + ๐) = 0) โ ((๐ + ๐) + ๐) โ โ) |
162 | 27 | adantr 482 |
. . . . . . 7
โข ((๐ โง ยฌ ((๐ + ๐) + ๐) = 0) โ ๐ธ โ
โ+) |
163 | 39 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ยฌ ((๐ + ๐) + ๐) = 0) โ 0 โค ((๐ + ๐) + ๐)) |
164 | | neqne 2948 |
. . . . . . . . . . . 12
โข (ยฌ
((๐ + ๐) + ๐) = 0 โ ((๐ + ๐) + ๐) โ 0) |
165 | 164 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โง ยฌ ((๐ + ๐) + ๐) = 0) โ ((๐ + ๐) + ๐) โ 0) |
166 | 161, 163,
165 | ne0gt0d 11297 |
. . . . . . . . . 10
โข ((๐ โง ยฌ ((๐ + ๐) + ๐) = 0) โ 0 < ((๐ + ๐) + ๐)) |
167 | 161, 166 | elrpd 12959 |
. . . . . . . . 9
โข ((๐ โง ยฌ ((๐ + ๐) + ๐) = 0) โ ((๐ + ๐) + ๐) โ
โ+) |
168 | 167, 162 | rpdivcld 12979 |
. . . . . . . 8
โข ((๐ โง ยฌ ((๐ + ๐) + ๐) = 0) โ (((๐ + ๐) + ๐) / ๐ธ) โ
โ+) |
169 | | 1rp 12924 |
. . . . . . . . 9
โข 1 โ
โ+ |
170 | 169 | a1i 11 |
. . . . . . . 8
โข ((๐ โง ยฌ ((๐ + ๐) + ๐) = 0) โ 1 โ
โ+) |
171 | 168, 170 | rpaddcld 12977 |
. . . . . . 7
โข ((๐ โง ยฌ ((๐ + ๐) + ๐) = 0) โ ((((๐ + ๐) + ๐) / ๐ธ) + 1) โ
โ+) |
172 | 124 | adantr 482 |
. . . . . . 7
โข ((๐ โง ยฌ ((๐ + ๐) + ๐) = 0) โ (((๐ + ๐) + ๐) / ๐ธ) < ((((๐ + ๐) + ๐) / ๐ธ) + 1)) |
173 | 161, 162,
171, 172 | ltdiv23d 13029 |
. . . . . 6
โข ((๐ โง ยฌ ((๐ + ๐) + ๐) = 0) โ (((๐ + ๐) + ๐) / ((((๐ + ๐) + ๐) / ๐ธ) + 1)) < ๐ธ) |
174 | 160, 173 | pm2.61dan 812 |
. . . . 5
โข (๐ โ (((๐ + ๐) + ๐) / ((((๐ + ๐) + ๐) / ๐ธ) + 1)) < ๐ธ) |
175 | 136, 174 | eqbrtrid 5141 |
. . . 4
โข (๐ โ ((((absโ๐ด) + (absโ๐ถ)) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / ((((๐ + ๐) + ๐) / ๐ธ) + 1)) < ๐ธ) |
176 | 90, 127, 28, 135, 175 | lelttrd 11318 |
. . 3
โข (๐ โ ((((absโ๐ด) + (absโ๐ถ)) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / ๐
) < ๐ธ) |
177 | 87, 90, 28, 123, 176 | lelttrd 11318 |
. 2
โข (๐ โ ((absโ(((๐ด ยท -๐ต) โ (๐ถ ยท -๐ท)) โ โซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / ๐
) < ๐ธ) |
178 | 85, 177 | eqbrtrd 5128 |
1
โข (๐ โ (absโ(((๐ด ยท -(๐ต / ๐
)) โ (๐ถ ยท -(๐ท / ๐
))) โ โซ๐ผ(๐น ยท -(๐บ / ๐
)) d๐ฅ)) < ๐ธ) |