Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem30 Structured version   Visualization version   GIF version

Theorem fourierdlem30 44464
Description: Sum of three small pieces is less than ฮต. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem30.ibl (๐œ‘ โ†’ (๐‘ฅ โˆˆ ๐ผ โ†ฆ (๐น ยท -๐บ)) โˆˆ ๐ฟ1)
fourierlemreimleblemlte22.f ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โ†’ ๐น โˆˆ โ„‚)
fourierdlem30.g ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โ†’ ๐บ โˆˆ โ„‚)
fourierdlem30.a (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
fourierdlem30.x ๐‘‹ = (absโ€˜๐ด)
fourierdlem30.c (๐œ‘ โ†’ ๐ถ โˆˆ โ„‚)
fourierdlem30.y ๐‘Œ = (absโ€˜๐ถ)
fourierdlem30.z ๐‘ = (absโ€˜โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)
fourierdlem30.e (๐œ‘ โ†’ ๐ธ โˆˆ โ„+)
fourierdlem30.r (๐œ‘ โ†’ ๐‘… โˆˆ โ„)
fourierdlem30.ler (๐œ‘ โ†’ ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1) โ‰ค ๐‘…)
fourierdlem30.b (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
fourierdlem30.12 (๐œ‘ โ†’ (absโ€˜๐ต) โ‰ค 1)
fourierdlem30.d (๐œ‘ โ†’ ๐ท โˆˆ โ„‚)
fourierdlem30.14 (๐œ‘ โ†’ (absโ€˜๐ท) โ‰ค 1)
Assertion
Ref Expression
fourierdlem30 (๐œ‘ โ†’ (absโ€˜(((๐ด ยท -(๐ต / ๐‘…)) โˆ’ (๐ถ ยท -(๐ท / ๐‘…))) โˆ’ โˆซ๐ผ(๐น ยท -(๐บ / ๐‘…)) d๐‘ฅ)) < ๐ธ)
Distinct variable groups:   ๐‘ฅ,๐ผ   ๐‘ฅ,๐‘…   ๐œ‘,๐‘ฅ
Allowed substitution hints:   ๐ด(๐‘ฅ)   ๐ต(๐‘ฅ)   ๐ถ(๐‘ฅ)   ๐ท(๐‘ฅ)   ๐ธ(๐‘ฅ)   ๐น(๐‘ฅ)   ๐บ(๐‘ฅ)   ๐‘‹(๐‘ฅ)   ๐‘Œ(๐‘ฅ)   ๐‘(๐‘ฅ)

Proof of Theorem fourierdlem30
StepHypRef Expression
1 fourierdlem30.b . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
2 fourierdlem30.r . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘… โˆˆ โ„)
32recnd 11188 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘… โˆˆ โ„‚)
4 0red 11163 . . . . . . . . . . . . 13 (๐œ‘ โ†’ 0 โˆˆ โ„)
5 1red 11161 . . . . . . . . . . . . 13 (๐œ‘ โ†’ 1 โˆˆ โ„)
6 0lt1 11682 . . . . . . . . . . . . . 14 0 < 1
76a1i 11 . . . . . . . . . . . . 13 (๐œ‘ โ†’ 0 < 1)
8 fourierdlem30.x . . . . . . . . . . . . . . . . . . 19 ๐‘‹ = (absโ€˜๐ด)
9 fourierdlem30.a . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
109abscld 15327 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (absโ€˜๐ด) โˆˆ โ„)
118, 10eqeltrid 2838 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„)
12 fourierdlem30.y . . . . . . . . . . . . . . . . . . 19 ๐‘Œ = (absโ€˜๐ถ)
13 fourierdlem30.c . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ๐ถ โˆˆ โ„‚)
1413abscld 15327 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (absโ€˜๐ถ) โˆˆ โ„)
1512, 14eqeltrid 2838 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐‘Œ โˆˆ โ„)
1611, 15readdcld 11189 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐‘‹ + ๐‘Œ) โˆˆ โ„)
17 fourierdlem30.z . . . . . . . . . . . . . . . . . 18 ๐‘ = (absโ€˜โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)
18 fourierlemreimleblemlte22.f . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โ†’ ๐น โˆˆ โ„‚)
19 fourierdlem30.g . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โ†’ ๐บ โˆˆ โ„‚)
2019negcld 11504 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โ†’ -๐บ โˆˆ โ„‚)
2118, 20mulcld 11180 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โ†’ (๐น ยท -๐บ) โˆˆ โ„‚)
22 fourierdlem30.ibl . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐‘ฅ โˆˆ ๐ผ โ†ฆ (๐น ยท -๐บ)) โˆˆ ๐ฟ1)
2321, 22itgcl 25164 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ โˆˆ โ„‚)
2423abscld 15327 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (absโ€˜โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ) โˆˆ โ„)
2517, 24eqeltrid 2838 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ๐‘ โˆˆ โ„)
2616, 25readdcld 11189 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐‘‹ + ๐‘Œ) + ๐‘) โˆˆ โ„)
27 fourierdlem30.e . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ๐ธ โˆˆ โ„+)
2827rpred 12962 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ธ โˆˆ โ„)
2927rpne0d 12967 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ธ โ‰  0)
3026, 28, 29redivcld 11988 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) โˆˆ โ„)
3130, 5readdcld 11189 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1) โˆˆ โ„)
329absge0d 15335 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ 0 โ‰ค (absโ€˜๐ด))
3332, 8breqtrrdi 5148 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 0 โ‰ค ๐‘‹)
3413absge0d 15335 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ 0 โ‰ค (absโ€˜๐ถ))
3534, 12breqtrrdi 5148 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 0 โ‰ค ๐‘Œ)
3611, 15, 33, 35addge0d 11736 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 0 โ‰ค (๐‘‹ + ๐‘Œ))
3723absge0d 15335 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 0 โ‰ค (absโ€˜โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ))
3837, 17breqtrrdi 5148 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 0 โ‰ค ๐‘)
3916, 25, 36, 38addge0d 11736 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 0 โ‰ค ((๐‘‹ + ๐‘Œ) + ๐‘))
4026, 27, 39divge0d 13002 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 0 โ‰ค (((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ))
415, 30addge02d 11749 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (0 โ‰ค (((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) โ†” 1 โ‰ค ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1)))
4240, 41mpbid 231 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 1 โ‰ค ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1))
43 fourierdlem30.ler . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1) โ‰ค ๐‘…)
445, 31, 2, 42, 43letrd 11317 . . . . . . . . . . . . 13 (๐œ‘ โ†’ 1 โ‰ค ๐‘…)
454, 5, 2, 7, 44ltletrd 11320 . . . . . . . . . . . 12 (๐œ‘ โ†’ 0 < ๐‘…)
4645gt0ne0d 11724 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘… โ‰  0)
471, 3, 46divnegd 11949 . . . . . . . . . 10 (๐œ‘ โ†’ -(๐ต / ๐‘…) = (-๐ต / ๐‘…))
4847oveq2d 7374 . . . . . . . . 9 (๐œ‘ โ†’ (๐ด ยท -(๐ต / ๐‘…)) = (๐ด ยท (-๐ต / ๐‘…)))
491negcld 11504 . . . . . . . . . 10 (๐œ‘ โ†’ -๐ต โˆˆ โ„‚)
509, 49, 3, 46divassd 11971 . . . . . . . . 9 (๐œ‘ โ†’ ((๐ด ยท -๐ต) / ๐‘…) = (๐ด ยท (-๐ต / ๐‘…)))
5148, 50eqtr4d 2776 . . . . . . . 8 (๐œ‘ โ†’ (๐ด ยท -(๐ต / ๐‘…)) = ((๐ด ยท -๐ต) / ๐‘…))
52 fourierdlem30.d . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ท โˆˆ โ„‚)
5352, 3, 46divnegd 11949 . . . . . . . . . 10 (๐œ‘ โ†’ -(๐ท / ๐‘…) = (-๐ท / ๐‘…))
5453oveq2d 7374 . . . . . . . . 9 (๐œ‘ โ†’ (๐ถ ยท -(๐ท / ๐‘…)) = (๐ถ ยท (-๐ท / ๐‘…)))
5552negcld 11504 . . . . . . . . . 10 (๐œ‘ โ†’ -๐ท โˆˆ โ„‚)
5613, 55, 3, 46divassd 11971 . . . . . . . . 9 (๐œ‘ โ†’ ((๐ถ ยท -๐ท) / ๐‘…) = (๐ถ ยท (-๐ท / ๐‘…)))
5754, 56eqtr4d 2776 . . . . . . . 8 (๐œ‘ โ†’ (๐ถ ยท -(๐ท / ๐‘…)) = ((๐ถ ยท -๐ท) / ๐‘…))
5851, 57oveq12d 7376 . . . . . . 7 (๐œ‘ โ†’ ((๐ด ยท -(๐ต / ๐‘…)) โˆ’ (๐ถ ยท -(๐ท / ๐‘…))) = (((๐ด ยท -๐ต) / ๐‘…) โˆ’ ((๐ถ ยท -๐ท) / ๐‘…)))
599, 49mulcld 11180 . . . . . . . 8 (๐œ‘ โ†’ (๐ด ยท -๐ต) โˆˆ โ„‚)
6013, 55mulcld 11180 . . . . . . . 8 (๐œ‘ โ†’ (๐ถ ยท -๐ท) โˆˆ โ„‚)
6159, 60, 3, 46divsubdird 11975 . . . . . . 7 (๐œ‘ โ†’ (((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท)) / ๐‘…) = (((๐ด ยท -๐ต) / ๐‘…) โˆ’ ((๐ถ ยท -๐ท) / ๐‘…)))
6258, 61eqtr4d 2776 . . . . . 6 (๐œ‘ โ†’ ((๐ด ยท -(๐ต / ๐‘…)) โˆ’ (๐ถ ยท -(๐ท / ๐‘…))) = (((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท)) / ๐‘…))
633, 46reccld 11929 . . . . . . . 8 (๐œ‘ โ†’ (1 / ๐‘…) โˆˆ โ„‚)
6463, 21, 22itgmulc2 25214 . . . . . . 7 (๐œ‘ โ†’ ((1 / ๐‘…) ยท โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ) = โˆซ๐ผ((1 / ๐‘…) ยท (๐น ยท -๐บ)) d๐‘ฅ)
6523, 3, 46divrec2d 11940 . . . . . . 7 (๐œ‘ โ†’ (โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ / ๐‘…) = ((1 / ๐‘…) ยท โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ))
663adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โ†’ ๐‘… โˆˆ โ„‚)
6746adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โ†’ ๐‘… โ‰  0)
6819, 66, 67divnegd 11949 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โ†’ -(๐บ / ๐‘…) = (-๐บ / ๐‘…))
6968oveq2d 7374 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โ†’ (๐น ยท -(๐บ / ๐‘…)) = (๐น ยท (-๐บ / ๐‘…)))
7018, 20, 66, 67divassd 11971 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โ†’ ((๐น ยท -๐บ) / ๐‘…) = (๐น ยท (-๐บ / ๐‘…)))
7121, 66, 67divrec2d 11940 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โ†’ ((๐น ยท -๐บ) / ๐‘…) = ((1 / ๐‘…) ยท (๐น ยท -๐บ)))
7269, 70, 713eqtr2d 2779 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ผ) โ†’ (๐น ยท -(๐บ / ๐‘…)) = ((1 / ๐‘…) ยท (๐น ยท -๐บ)))
7372itgeq2dv 25162 . . . . . . 7 (๐œ‘ โ†’ โˆซ๐ผ(๐น ยท -(๐บ / ๐‘…)) d๐‘ฅ = โˆซ๐ผ((1 / ๐‘…) ยท (๐น ยท -๐บ)) d๐‘ฅ)
7464, 65, 733eqtr4rd 2784 . . . . . 6 (๐œ‘ โ†’ โˆซ๐ผ(๐น ยท -(๐บ / ๐‘…)) d๐‘ฅ = (โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ / ๐‘…))
7562, 74oveq12d 7376 . . . . 5 (๐œ‘ โ†’ (((๐ด ยท -(๐ต / ๐‘…)) โˆ’ (๐ถ ยท -(๐ท / ๐‘…))) โˆ’ โˆซ๐ผ(๐น ยท -(๐บ / ๐‘…)) d๐‘ฅ) = ((((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท)) / ๐‘…) โˆ’ (โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ / ๐‘…)))
7659, 60subcld 11517 . . . . . 6 (๐œ‘ โ†’ ((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท)) โˆˆ โ„‚)
7776, 23, 3, 46divsubdird 11975 . . . . 5 (๐œ‘ โ†’ ((((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท)) โˆ’ โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ) / ๐‘…) = ((((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท)) / ๐‘…) โˆ’ (โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ / ๐‘…)))
7875, 77eqtr4d 2776 . . . 4 (๐œ‘ โ†’ (((๐ด ยท -(๐ต / ๐‘…)) โˆ’ (๐ถ ยท -(๐ท / ๐‘…))) โˆ’ โˆซ๐ผ(๐น ยท -(๐บ / ๐‘…)) d๐‘ฅ) = ((((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท)) โˆ’ โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ) / ๐‘…))
7978fveq2d 6847 . . 3 (๐œ‘ โ†’ (absโ€˜(((๐ด ยท -(๐ต / ๐‘…)) โˆ’ (๐ถ ยท -(๐ท / ๐‘…))) โˆ’ โˆซ๐ผ(๐น ยท -(๐บ / ๐‘…)) d๐‘ฅ)) = (absโ€˜((((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท)) โˆ’ โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ) / ๐‘…)))
8076, 23subcld 11517 . . . 4 (๐œ‘ โ†’ (((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท)) โˆ’ โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ) โˆˆ โ„‚)
8180, 3, 46absdivd 15346 . . 3 (๐œ‘ โ†’ (absโ€˜((((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท)) โˆ’ โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ) / ๐‘…)) = ((absโ€˜(((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท)) โˆ’ โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) / (absโ€˜๐‘…)))
824, 2, 45ltled 11308 . . . . 5 (๐œ‘ โ†’ 0 โ‰ค ๐‘…)
832, 82absidd 15313 . . . 4 (๐œ‘ โ†’ (absโ€˜๐‘…) = ๐‘…)
8483oveq2d 7374 . . 3 (๐œ‘ โ†’ ((absโ€˜(((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท)) โˆ’ โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) / (absโ€˜๐‘…)) = ((absโ€˜(((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท)) โˆ’ โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) / ๐‘…))
8579, 81, 843eqtrd 2777 . 2 (๐œ‘ โ†’ (absโ€˜(((๐ด ยท -(๐ต / ๐‘…)) โˆ’ (๐ถ ยท -(๐ท / ๐‘…))) โˆ’ โˆซ๐ผ(๐น ยท -(๐บ / ๐‘…)) d๐‘ฅ)) = ((absโ€˜(((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท)) โˆ’ โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) / ๐‘…))
8680abscld 15327 . . . 4 (๐œ‘ โ†’ (absโ€˜(((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท)) โˆ’ โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) โˆˆ โ„)
8786, 2, 46redivcld 11988 . . 3 (๐œ‘ โ†’ ((absโ€˜(((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท)) โˆ’ โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) / ๐‘…) โˆˆ โ„)
8810, 14readdcld 11189 . . . . 5 (๐œ‘ โ†’ ((absโ€˜๐ด) + (absโ€˜๐ถ)) โˆˆ โ„)
8988, 24readdcld 11189 . . . 4 (๐œ‘ โ†’ (((absโ€˜๐ด) + (absโ€˜๐ถ)) + (absโ€˜โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) โˆˆ โ„)
9089, 2, 46redivcld 11988 . . 3 (๐œ‘ โ†’ ((((absโ€˜๐ด) + (absโ€˜๐ถ)) + (absโ€˜โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) / ๐‘…) โˆˆ โ„)
912, 45elrpd 12959 . . . 4 (๐œ‘ โ†’ ๐‘… โˆˆ โ„+)
9276abscld 15327 . . . . . 6 (๐œ‘ โ†’ (absโ€˜((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท))) โˆˆ โ„)
9392, 24readdcld 11189 . . . . 5 (๐œ‘ โ†’ ((absโ€˜((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท))) + (absโ€˜โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) โˆˆ โ„)
9476, 23abs2dif2d 15349 . . . . 5 (๐œ‘ โ†’ (absโ€˜(((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท)) โˆ’ โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) โ‰ค ((absโ€˜((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท))) + (absโ€˜โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)))
9559abscld 15327 . . . . . . . 8 (๐œ‘ โ†’ (absโ€˜(๐ด ยท -๐ต)) โˆˆ โ„)
9660abscld 15327 . . . . . . . 8 (๐œ‘ โ†’ (absโ€˜(๐ถ ยท -๐ท)) โˆˆ โ„)
9795, 96readdcld 11189 . . . . . . 7 (๐œ‘ โ†’ ((absโ€˜(๐ด ยท -๐ต)) + (absโ€˜(๐ถ ยท -๐ท))) โˆˆ โ„)
9859, 60abs2dif2d 15349 . . . . . . 7 (๐œ‘ โ†’ (absโ€˜((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท))) โ‰ค ((absโ€˜(๐ด ยท -๐ต)) + (absโ€˜(๐ถ ยท -๐ท))))
999, 49absmuld 15345 . . . . . . . . 9 (๐œ‘ โ†’ (absโ€˜(๐ด ยท -๐ต)) = ((absโ€˜๐ด) ยท (absโ€˜-๐ต)))
10049abscld 15327 . . . . . . . . . . 11 (๐œ‘ โ†’ (absโ€˜-๐ต) โˆˆ โ„)
1011absnegd 15340 . . . . . . . . . . . 12 (๐œ‘ โ†’ (absโ€˜-๐ต) = (absโ€˜๐ต))
102 fourierdlem30.12 . . . . . . . . . . . 12 (๐œ‘ โ†’ (absโ€˜๐ต) โ‰ค 1)
103101, 102eqbrtrd 5128 . . . . . . . . . . 11 (๐œ‘ โ†’ (absโ€˜-๐ต) โ‰ค 1)
104100, 5, 10, 32, 103lemul2ad 12100 . . . . . . . . . 10 (๐œ‘ โ†’ ((absโ€˜๐ด) ยท (absโ€˜-๐ต)) โ‰ค ((absโ€˜๐ด) ยท 1))
10510recnd 11188 . . . . . . . . . . 11 (๐œ‘ โ†’ (absโ€˜๐ด) โˆˆ โ„‚)
106105mulid1d 11177 . . . . . . . . . 10 (๐œ‘ โ†’ ((absโ€˜๐ด) ยท 1) = (absโ€˜๐ด))
107104, 106breqtrd 5132 . . . . . . . . 9 (๐œ‘ โ†’ ((absโ€˜๐ด) ยท (absโ€˜-๐ต)) โ‰ค (absโ€˜๐ด))
10899, 107eqbrtrd 5128 . . . . . . . 8 (๐œ‘ โ†’ (absโ€˜(๐ด ยท -๐ต)) โ‰ค (absโ€˜๐ด))
10913, 55absmuld 15345 . . . . . . . . 9 (๐œ‘ โ†’ (absโ€˜(๐ถ ยท -๐ท)) = ((absโ€˜๐ถ) ยท (absโ€˜-๐ท)))
11055abscld 15327 . . . . . . . . . . 11 (๐œ‘ โ†’ (absโ€˜-๐ท) โˆˆ โ„)
11152absnegd 15340 . . . . . . . . . . . 12 (๐œ‘ โ†’ (absโ€˜-๐ท) = (absโ€˜๐ท))
112 fourierdlem30.14 . . . . . . . . . . . 12 (๐œ‘ โ†’ (absโ€˜๐ท) โ‰ค 1)
113111, 112eqbrtrd 5128 . . . . . . . . . . 11 (๐œ‘ โ†’ (absโ€˜-๐ท) โ‰ค 1)
114110, 5, 14, 34, 113lemul2ad 12100 . . . . . . . . . 10 (๐œ‘ โ†’ ((absโ€˜๐ถ) ยท (absโ€˜-๐ท)) โ‰ค ((absโ€˜๐ถ) ยท 1))
11514recnd 11188 . . . . . . . . . . 11 (๐œ‘ โ†’ (absโ€˜๐ถ) โˆˆ โ„‚)
116115mulid1d 11177 . . . . . . . . . 10 (๐œ‘ โ†’ ((absโ€˜๐ถ) ยท 1) = (absโ€˜๐ถ))
117114, 116breqtrd 5132 . . . . . . . . 9 (๐œ‘ โ†’ ((absโ€˜๐ถ) ยท (absโ€˜-๐ท)) โ‰ค (absโ€˜๐ถ))
118109, 117eqbrtrd 5128 . . . . . . . 8 (๐œ‘ โ†’ (absโ€˜(๐ถ ยท -๐ท)) โ‰ค (absโ€˜๐ถ))
11995, 96, 10, 14, 108, 118le2addd 11779 . . . . . . 7 (๐œ‘ โ†’ ((absโ€˜(๐ด ยท -๐ต)) + (absโ€˜(๐ถ ยท -๐ท))) โ‰ค ((absโ€˜๐ด) + (absโ€˜๐ถ)))
12092, 97, 88, 98, 119letrd 11317 . . . . . 6 (๐œ‘ โ†’ (absโ€˜((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท))) โ‰ค ((absโ€˜๐ด) + (absโ€˜๐ถ)))
12192, 88, 24, 120leadd1dd 11774 . . . . 5 (๐œ‘ โ†’ ((absโ€˜((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท))) + (absโ€˜โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) โ‰ค (((absโ€˜๐ด) + (absโ€˜๐ถ)) + (absโ€˜โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)))
12286, 93, 89, 94, 121letrd 11317 . . . 4 (๐œ‘ โ†’ (absโ€˜(((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท)) โˆ’ โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) โ‰ค (((absโ€˜๐ด) + (absโ€˜๐ถ)) + (absโ€˜โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)))
12386, 89, 91, 122lediv1dd 13020 . . 3 (๐œ‘ โ†’ ((absโ€˜(((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท)) โˆ’ โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) / ๐‘…) โ‰ค ((((absโ€˜๐ด) + (absโ€˜๐ถ)) + (absโ€˜โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) / ๐‘…))
12430ltp1d 12090 . . . . . . 7 (๐œ‘ โ†’ (((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) < ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1))
1254, 30, 31, 40, 124lelttrd 11318 . . . . . 6 (๐œ‘ โ†’ 0 < ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1))
126125gt0ne0d 11724 . . . . 5 (๐œ‘ โ†’ ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1) โ‰  0)
12789, 31, 126redivcld 11988 . . . 4 (๐œ‘ โ†’ ((((absโ€˜๐ด) + (absโ€˜๐ถ)) + (absโ€˜โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) / ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1)) โˆˆ โ„)
12830, 40ge0p1rpd 12992 . . . . 5 (๐œ‘ โ†’ ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1) โˆˆ โ„+)
1298eqcomi 2742 . . . . . . . 8 (absโ€˜๐ด) = ๐‘‹
13012eqcomi 2742 . . . . . . . 8 (absโ€˜๐ถ) = ๐‘Œ
131129, 130oveq12i 7370 . . . . . . 7 ((absโ€˜๐ด) + (absโ€˜๐ถ)) = (๐‘‹ + ๐‘Œ)
13217eqcomi 2742 . . . . . . 7 (absโ€˜โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ) = ๐‘
133131, 132oveq12i 7370 . . . . . 6 (((absโ€˜๐ด) + (absโ€˜๐ถ)) + (absโ€˜โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) = ((๐‘‹ + ๐‘Œ) + ๐‘)
13439, 133breqtrrdi 5148 . . . . 5 (๐œ‘ โ†’ 0 โ‰ค (((absโ€˜๐ด) + (absโ€˜๐ถ)) + (absโ€˜โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)))
135128, 91, 89, 134, 43lediv2ad 12984 . . . 4 (๐œ‘ โ†’ ((((absโ€˜๐ด) + (absโ€˜๐ถ)) + (absโ€˜โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) / ๐‘…) โ‰ค ((((absโ€˜๐ด) + (absโ€˜๐ถ)) + (absโ€˜โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) / ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1)))
136133oveq1i 7368 . . . . 5 ((((absโ€˜๐ด) + (absโ€˜๐ถ)) + (absโ€˜โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) / ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1)) = (((๐‘‹ + ๐‘Œ) + ๐‘) / ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1))
137 oveq1 7365 . . . . . . . . 9 (((๐‘‹ + ๐‘Œ) + ๐‘) = 0 โ†’ (((๐‘‹ + ๐‘Œ) + ๐‘) / ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1)) = (0 / ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1)))
138137adantl 483 . . . . . . . 8 ((๐œ‘ โˆง ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ (((๐‘‹ + ๐‘Œ) + ๐‘) / ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1)) = (0 / ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1)))
13930recnd 11188 . . . . . . . . . . 11 (๐œ‘ โ†’ (((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) โˆˆ โ„‚)
1405recnd 11188 . . . . . . . . . . 11 (๐œ‘ โ†’ 1 โˆˆ โ„‚)
141139, 140addcld 11179 . . . . . . . . . 10 (๐œ‘ โ†’ ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1) โˆˆ โ„‚)
142141adantr 482 . . . . . . . . 9 ((๐œ‘ โˆง ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1) โˆˆ โ„‚)
143 oveq1 7365 . . . . . . . . . . . . . 14 (((๐‘‹ + ๐‘Œ) + ๐‘) = 0 โ†’ (((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) = (0 / ๐ธ))
144143adantl 483 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ (((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) = (0 / ๐ธ))
14527rpcnd 12964 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ธ โˆˆ โ„‚)
146145adantr 482 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ ๐ธ โˆˆ โ„‚)
14729adantr 482 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ ๐ธ โ‰  0)
148146, 147div0d 11935 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ (0 / ๐ธ) = 0)
149144, 148eqtrd 2773 . . . . . . . . . . . 12 ((๐œ‘ โˆง ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ (((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) = 0)
150149oveq1d 7373 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1) = (0 + 1))
151 0p1e1 12280 . . . . . . . . . . 11 (0 + 1) = 1
152150, 151eqtrdi 2789 . . . . . . . . . 10 ((๐œ‘ โˆง ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1) = 1)
153 ax-1ne0 11125 . . . . . . . . . . 11 1 โ‰  0
154153a1i 11 . . . . . . . . . 10 ((๐œ‘ โˆง ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ 1 โ‰  0)
155152, 154eqnetrd 3008 . . . . . . . . 9 ((๐œ‘ โˆง ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1) โ‰  0)
156142, 155div0d 11935 . . . . . . . 8 ((๐œ‘ โˆง ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ (0 / ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1)) = 0)
157138, 156eqtrd 2773 . . . . . . 7 ((๐œ‘ โˆง ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ (((๐‘‹ + ๐‘Œ) + ๐‘) / ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1)) = 0)
15827rpgt0d 12965 . . . . . . . 8 (๐œ‘ โ†’ 0 < ๐ธ)
159158adantr 482 . . . . . . 7 ((๐œ‘ โˆง ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ 0 < ๐ธ)
160157, 159eqbrtrd 5128 . . . . . 6 ((๐œ‘ โˆง ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ (((๐‘‹ + ๐‘Œ) + ๐‘) / ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1)) < ๐ธ)
16126adantr 482 . . . . . . 7 ((๐œ‘ โˆง ยฌ ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ ((๐‘‹ + ๐‘Œ) + ๐‘) โˆˆ โ„)
16227adantr 482 . . . . . . 7 ((๐œ‘ โˆง ยฌ ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ ๐ธ โˆˆ โ„+)
16339adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ยฌ ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ 0 โ‰ค ((๐‘‹ + ๐‘Œ) + ๐‘))
164 neqne 2948 . . . . . . . . . . . 12 (ยฌ ((๐‘‹ + ๐‘Œ) + ๐‘) = 0 โ†’ ((๐‘‹ + ๐‘Œ) + ๐‘) โ‰  0)
165164adantl 483 . . . . . . . . . . 11 ((๐œ‘ โˆง ยฌ ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ ((๐‘‹ + ๐‘Œ) + ๐‘) โ‰  0)
166161, 163, 165ne0gt0d 11297 . . . . . . . . . 10 ((๐œ‘ โˆง ยฌ ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ 0 < ((๐‘‹ + ๐‘Œ) + ๐‘))
167161, 166elrpd 12959 . . . . . . . . 9 ((๐œ‘ โˆง ยฌ ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ ((๐‘‹ + ๐‘Œ) + ๐‘) โˆˆ โ„+)
168167, 162rpdivcld 12979 . . . . . . . 8 ((๐œ‘ โˆง ยฌ ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ (((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) โˆˆ โ„+)
169 1rp 12924 . . . . . . . . 9 1 โˆˆ โ„+
170169a1i 11 . . . . . . . 8 ((๐œ‘ โˆง ยฌ ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ 1 โˆˆ โ„+)
171168, 170rpaddcld 12977 . . . . . . 7 ((๐œ‘ โˆง ยฌ ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1) โˆˆ โ„+)
172124adantr 482 . . . . . . 7 ((๐œ‘ โˆง ยฌ ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ (((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) < ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1))
173161, 162, 171, 172ltdiv23d 13029 . . . . . 6 ((๐œ‘ โˆง ยฌ ((๐‘‹ + ๐‘Œ) + ๐‘) = 0) โ†’ (((๐‘‹ + ๐‘Œ) + ๐‘) / ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1)) < ๐ธ)
174160, 173pm2.61dan 812 . . . . 5 (๐œ‘ โ†’ (((๐‘‹ + ๐‘Œ) + ๐‘) / ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1)) < ๐ธ)
175136, 174eqbrtrid 5141 . . . 4 (๐œ‘ โ†’ ((((absโ€˜๐ด) + (absโ€˜๐ถ)) + (absโ€˜โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) / ((((๐‘‹ + ๐‘Œ) + ๐‘) / ๐ธ) + 1)) < ๐ธ)
17690, 127, 28, 135, 175lelttrd 11318 . . 3 (๐œ‘ โ†’ ((((absโ€˜๐ด) + (absโ€˜๐ถ)) + (absโ€˜โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) / ๐‘…) < ๐ธ)
17787, 90, 28, 123, 176lelttrd 11318 . 2 (๐œ‘ โ†’ ((absโ€˜(((๐ด ยท -๐ต) โˆ’ (๐ถ ยท -๐ท)) โˆ’ โˆซ๐ผ(๐น ยท -๐บ) d๐‘ฅ)) / ๐‘…) < ๐ธ)
17885, 177eqbrtrd 5128 1 (๐œ‘ โ†’ (absโ€˜(((๐ด ยท -(๐ต / ๐‘…)) โˆ’ (๐ถ ยท -(๐ท / ๐‘…))) โˆ’ โˆซ๐ผ(๐น ยท -(๐บ / ๐‘…)) d๐‘ฅ)) < ๐ธ)
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2940   class class class wbr 5106   โ†ฆ cmpt 5189  โ€˜cfv 6497  (class class class)co 7358  โ„‚cc 11054  โ„cr 11055  0cc0 11056  1c1 11057   + caddc 11059   ยท cmul 11061   < clt 11194   โ‰ค cle 11195   โˆ’ cmin 11390  -cneg 11391   / cdiv 11817  โ„+crp 12920  abscabs 15125  ๐ฟ1cibl 24997  โˆซcitg 24998
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9582  ax-cc 10376  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133  ax-pre-sup 11134  ax-addf 11135  ax-mulf 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-iin 4958  df-disj 5072  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7618  df-ofr 7619  df-om 7804  df-1st 7922  df-2nd 7923  df-supp 8094  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-oadd 8417  df-omul 8418  df-er 8651  df-map 8770  df-pm 8771  df-ixp 8839  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9309  df-fi 9352  df-sup 9383  df-inf 9384  df-oi 9451  df-dju 9842  df-card 9880  df-acn 9883  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-div 11818  df-nn 12159  df-2 12221  df-3 12222  df-4 12223  df-5 12224  df-6 12225  df-7 12226  df-8 12227  df-9 12228  df-n0 12419  df-z 12505  df-dec 12624  df-uz 12769  df-q 12879  df-rp 12921  df-xneg 13038  df-xadd 13039  df-xmul 13040  df-ioo 13274  df-ioc 13275  df-ico 13276  df-icc 13277  df-fz 13431  df-fzo 13574  df-fl 13703  df-mod 13781  df-seq 13913  df-exp 13974  df-hash 14237  df-cj 14990  df-re 14991  df-im 14992  df-sqrt 15126  df-abs 15127  df-clim 15376  df-rlim 15377  df-sum 15577  df-struct 17024  df-sets 17041  df-slot 17059  df-ndx 17071  df-base 17089  df-ress 17118  df-plusg 17151  df-mulr 17152  df-starv 17153  df-sca 17154  df-vsca 17155  df-ip 17156  df-tset 17157  df-ple 17158  df-ds 17160  df-unif 17161  df-hom 17162  df-cco 17163  df-rest 17309  df-topn 17310  df-0g 17328  df-gsum 17329  df-topgen 17330  df-pt 17331  df-prds 17334  df-xrs 17389  df-qtop 17394  df-imas 17395  df-xps 17397  df-mre 17471  df-mrc 17472  df-acs 17474  df-mgm 18502  df-sgrp 18551  df-mnd 18562  df-submnd 18607  df-mulg 18878  df-cntz 19102  df-cmn 19569  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cn 22594  df-cnp 22595  df-cmp 22754  df-tx 22929  df-hmeo 23122  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-ovol 24844  df-vol 24845  df-mbf 24999  df-itg1 25000  df-itg2 25001  df-ibl 25002  df-itg 25003  df-0p 25050
This theorem is referenced by:  fourierdlem47  44480
  Copyright terms: Public domain W3C validator