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

Theorem fourierdlem19 45437
Description: If two elements of ๐ท have the same periodic image in (๐ด(,]๐ต) then they are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem19.a (๐œ‘ โ†’ ๐ด โˆˆ โ„)
fourierdlem19.b (๐œ‘ โ†’ ๐ต โˆˆ โ„)
fourierdlem19.altb (๐œ‘ โ†’ ๐ด < ๐ต)
fourierdlem19.x (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„)
fourierdlem19.d ๐ท = {๐‘ฆ โˆˆ ((๐ด + ๐‘‹)(,](๐ต + ๐‘‹)) โˆฃ โˆƒ๐‘˜ โˆˆ โ„ค (๐‘ฆ + (๐‘˜ ยท ๐‘‡)) โˆˆ ๐ถ}
fourierdlem19.t ๐‘‡ = (๐ต โˆ’ ๐ด)
fourierdlem19.e ๐ธ = (๐‘ฅ โˆˆ โ„ โ†ฆ (๐‘ฅ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡)))
fourierdlem19.w (๐œ‘ โ†’ ๐‘Š โˆˆ ๐ท)
fourierdlem19.z (๐œ‘ โ†’ ๐‘ โˆˆ ๐ท)
fourierdlem19.ezew (๐œ‘ โ†’ (๐ธโ€˜๐‘) = (๐ธโ€˜๐‘Š))
Assertion
Ref Expression
fourierdlem19 (๐œ‘ โ†’ ยฌ ๐‘Š < ๐‘)
Distinct variable groups:   ๐‘ฅ,๐ด   ๐‘ฆ,๐ด   ๐‘ฅ,๐ต   ๐‘ฆ,๐ต   ๐‘ฅ,๐‘‡   ๐‘ฅ,๐‘Š   ๐‘ฆ,๐‘‹   ๐‘ฅ,๐‘   ๐œ‘,๐‘ฅ
Allowed substitution hints:   ๐œ‘(๐‘ฆ,๐‘˜)   ๐ด(๐‘˜)   ๐ต(๐‘˜)   ๐ถ(๐‘ฅ,๐‘ฆ,๐‘˜)   ๐ท(๐‘ฅ,๐‘ฆ,๐‘˜)   ๐‘‡(๐‘ฆ,๐‘˜)   ๐ธ(๐‘ฅ,๐‘ฆ,๐‘˜)   ๐‘Š(๐‘ฆ,๐‘˜)   ๐‘‹(๐‘ฅ,๐‘˜)   ๐‘(๐‘ฆ,๐‘˜)

Proof of Theorem fourierdlem19
StepHypRef Expression
1 fourierdlem19.a . . . . . 6 (๐œ‘ โ†’ ๐ด โˆˆ โ„)
2 fourierdlem19.x . . . . . 6 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„)
31, 2readdcld 11265 . . . . 5 (๐œ‘ โ†’ (๐ด + ๐‘‹) โˆˆ โ„)
43rexrd 11286 . . . 4 (๐œ‘ โ†’ (๐ด + ๐‘‹) โˆˆ โ„*)
5 fourierdlem19.b . . . . . 6 (๐œ‘ โ†’ ๐ต โˆˆ โ„)
65, 2readdcld 11265 . . . . 5 (๐œ‘ โ†’ (๐ต + ๐‘‹) โˆˆ โ„)
76rexrd 11286 . . . 4 (๐œ‘ โ†’ (๐ต + ๐‘‹) โˆˆ โ„*)
8 fourierdlem19.d . . . . . 6 ๐ท = {๐‘ฆ โˆˆ ((๐ด + ๐‘‹)(,](๐ต + ๐‘‹)) โˆฃ โˆƒ๐‘˜ โˆˆ โ„ค (๐‘ฆ + (๐‘˜ ยท ๐‘‡)) โˆˆ ๐ถ}
9 ssrab2 4073 . . . . . 6 {๐‘ฆ โˆˆ ((๐ด + ๐‘‹)(,](๐ต + ๐‘‹)) โˆฃ โˆƒ๐‘˜ โˆˆ โ„ค (๐‘ฆ + (๐‘˜ ยท ๐‘‡)) โˆˆ ๐ถ} โІ ((๐ด + ๐‘‹)(,](๐ต + ๐‘‹))
108, 9eqsstri 4012 . . . . 5 ๐ท โІ ((๐ด + ๐‘‹)(,](๐ต + ๐‘‹))
11 fourierdlem19.z . . . . 5 (๐œ‘ โ†’ ๐‘ โˆˆ ๐ท)
1210, 11sselid 3976 . . . 4 (๐œ‘ โ†’ ๐‘ โˆˆ ((๐ด + ๐‘‹)(,](๐ต + ๐‘‹)))
13 iocleub 44811 . . . 4 (((๐ด + ๐‘‹) โˆˆ โ„* โˆง (๐ต + ๐‘‹) โˆˆ โ„* โˆง ๐‘ โˆˆ ((๐ด + ๐‘‹)(,](๐ต + ๐‘‹))) โ†’ ๐‘ โ‰ค (๐ต + ๐‘‹))
144, 7, 12, 13syl3anc 1369 . . 3 (๐œ‘ โ†’ ๐‘ โ‰ค (๐ต + ๐‘‹))
1514adantr 480 . 2 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ๐‘ โ‰ค (๐ต + ๐‘‹))
166adantr 480 . . . 4 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (๐ต + ๐‘‹) โˆˆ โ„)
17 iocssre 13428 . . . . . . . 8 (((๐ด + ๐‘‹) โˆˆ โ„* โˆง (๐ต + ๐‘‹) โˆˆ โ„) โ†’ ((๐ด + ๐‘‹)(,](๐ต + ๐‘‹)) โІ โ„)
184, 6, 17syl2anc 583 . . . . . . 7 (๐œ‘ โ†’ ((๐ด + ๐‘‹)(,](๐ต + ๐‘‹)) โІ โ„)
19 fourierdlem19.w . . . . . . . 8 (๐œ‘ โ†’ ๐‘Š โˆˆ ๐ท)
2010, 19sselid 3976 . . . . . . 7 (๐œ‘ โ†’ ๐‘Š โˆˆ ((๐ด + ๐‘‹)(,](๐ต + ๐‘‹)))
2118, 20sseldd 3979 . . . . . 6 (๐œ‘ โ†’ ๐‘Š โˆˆ โ„)
22 fourierdlem19.t . . . . . . 7 ๐‘‡ = (๐ต โˆ’ ๐ด)
235, 1resubcld 11664 . . . . . . 7 (๐œ‘ โ†’ (๐ต โˆ’ ๐ด) โˆˆ โ„)
2422, 23eqeltrid 2832 . . . . . 6 (๐œ‘ โ†’ ๐‘‡ โˆˆ โ„)
2521, 24readdcld 11265 . . . . 5 (๐œ‘ โ†’ (๐‘Š + ๐‘‡) โˆˆ โ„)
2625adantr 480 . . . 4 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (๐‘Š + ๐‘‡) โˆˆ โ„)
2718, 12sseldd 3979 . . . . 5 (๐œ‘ โ†’ ๐‘ โˆˆ โ„)
2827adantr 480 . . . 4 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ๐‘ โˆˆ โ„)
2922eqcomi 2736 . . . . . . . . . . 11 (๐ต โˆ’ ๐ด) = ๐‘‡
3029a1i 11 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ต โˆ’ ๐ด) = ๐‘‡)
315recnd 11264 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
321recnd 11264 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
3324recnd 11264 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘‡ โˆˆ โ„‚)
3431, 32, 33subaddd 11611 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ต โˆ’ ๐ด) = ๐‘‡ โ†” (๐ด + ๐‘‡) = ๐ต))
3530, 34mpbid 231 . . . . . . . . 9 (๐œ‘ โ†’ (๐ด + ๐‘‡) = ๐ต)
3635eqcomd 2733 . . . . . . . 8 (๐œ‘ โ†’ ๐ต = (๐ด + ๐‘‡))
3736oveq1d 7429 . . . . . . 7 (๐œ‘ โ†’ (๐ต + ๐‘‹) = ((๐ด + ๐‘‡) + ๐‘‹))
382recnd 11264 . . . . . . . 8 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„‚)
3932, 33, 38add32d 11463 . . . . . . 7 (๐œ‘ โ†’ ((๐ด + ๐‘‡) + ๐‘‹) = ((๐ด + ๐‘‹) + ๐‘‡))
4037, 39eqtrd 2767 . . . . . 6 (๐œ‘ โ†’ (๐ต + ๐‘‹) = ((๐ด + ๐‘‹) + ๐‘‡))
41 iocgtlb 44810 . . . . . . . 8 (((๐ด + ๐‘‹) โˆˆ โ„* โˆง (๐ต + ๐‘‹) โˆˆ โ„* โˆง ๐‘Š โˆˆ ((๐ด + ๐‘‹)(,](๐ต + ๐‘‹))) โ†’ (๐ด + ๐‘‹) < ๐‘Š)
424, 7, 20, 41syl3anc 1369 . . . . . . 7 (๐œ‘ โ†’ (๐ด + ๐‘‹) < ๐‘Š)
433, 21, 24, 42ltadd1dd 11847 . . . . . 6 (๐œ‘ โ†’ ((๐ด + ๐‘‹) + ๐‘‡) < (๐‘Š + ๐‘‡))
4440, 43eqbrtrd 5164 . . . . 5 (๐œ‘ โ†’ (๐ต + ๐‘‹) < (๐‘Š + ๐‘‡))
4544adantr 480 . . . 4 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (๐ต + ๐‘‹) < (๐‘Š + ๐‘‡))
46 fourierdlem19.e . . . . . . . . . . . . 13 ๐ธ = (๐‘ฅ โˆˆ โ„ โ†ฆ (๐‘ฅ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡)))
4746a1i 11 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ธ = (๐‘ฅ โˆˆ โ„ โ†ฆ (๐‘ฅ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡))))
48 id 22 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘Š โ†’ ๐‘ฅ = ๐‘Š)
49 oveq2 7422 . . . . . . . . . . . . . . . . 17 (๐‘ฅ = ๐‘Š โ†’ (๐ต โˆ’ ๐‘ฅ) = (๐ต โˆ’ ๐‘Š))
5049oveq1d 7429 . . . . . . . . . . . . . . . 16 (๐‘ฅ = ๐‘Š โ†’ ((๐ต โˆ’ ๐‘ฅ) / ๐‘‡) = ((๐ต โˆ’ ๐‘Š) / ๐‘‡))
5150fveq2d 6895 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘Š โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) = (โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)))
5251oveq1d 7429 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘Š โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡) = ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡))
5348, 52oveq12d 7432 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘Š โ†’ (๐‘ฅ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡)) = (๐‘Š + ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡)))
5453adantl 481 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ = ๐‘Š) โ†’ (๐‘ฅ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡)) = (๐‘Š + ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡)))
555, 21resubcld 11664 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐ต โˆ’ ๐‘Š) โˆˆ โ„)
56 fourierdlem19.altb . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ๐ด < ๐ต)
571, 5posdifd 11823 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐ด < ๐ต โ†” 0 < (๐ต โˆ’ ๐ด)))
5856, 57mpbid 231 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ 0 < (๐ต โˆ’ ๐ด))
5958, 22breqtrrdi 5184 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 0 < ๐‘‡)
6059gt0ne0d 11800 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ๐‘‡ โ‰  0)
6155, 24, 60redivcld 12064 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐ต โˆ’ ๐‘Š) / ๐‘‡) โˆˆ โ„)
6261flcld 13787 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) โˆˆ โ„ค)
6362zred 12688 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) โˆˆ โ„)
6463, 24remulcld 11266 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡) โˆˆ โ„)
6521, 64readdcld 11265 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘Š + ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡)) โˆˆ โ„)
6647, 54, 21, 65fvmptd 7006 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ธโ€˜๐‘Š) = (๐‘Š + ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡)))
6766, 65eqeltrd 2828 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ธโ€˜๐‘Š) โˆˆ โ„)
6867recnd 11264 . . . . . . . . 9 (๐œ‘ โ†’ (๐ธโ€˜๐‘Š) โˆˆ โ„‚)
6968adantr 480 . . . . . . . 8 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (๐ธโ€˜๐‘Š) โˆˆ โ„‚)
7064recnd 11264 . . . . . . . . 9 (๐œ‘ โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡) โˆˆ โ„‚)
7170adantr 480 . . . . . . . 8 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡) โˆˆ โ„‚)
7233adantr 480 . . . . . . . 8 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ๐‘‡ โˆˆ โ„‚)
7369, 71, 72subsubd 11621 . . . . . . 7 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ((๐ธโ€˜๐‘Š) โˆ’ (((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡) โˆ’ ๐‘‡)) = (((๐ธโ€˜๐‘Š) โˆ’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡)) + ๐‘‡))
7473eqcomd 2733 . . . . . 6 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (((๐ธโ€˜๐‘Š) โˆ’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡)) + ๐‘‡) = ((๐ธโ€˜๐‘Š) โˆ’ (((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡) โˆ’ ๐‘‡)))
755, 27resubcld 11664 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐ต โˆ’ ๐‘) โˆˆ โ„)
7675, 24, 60redivcld 12064 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐ต โˆ’ ๐‘) / ๐‘‡) โˆˆ โ„)
7776flcld 13787 . . . . . . . . . 10 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) โˆˆ โ„ค)
7877zred 12688 . . . . . . . . 9 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) โˆˆ โ„)
7978adantr 480 . . . . . . . 8 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) โˆˆ โ„)
8024adantr 480 . . . . . . . 8 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ๐‘‡ โˆˆ โ„)
8179, 80remulcld 11266 . . . . . . 7 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡) โˆˆ โ„)
8263adantr 480 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) โˆˆ โ„)
8382, 80remulcld 11266 . . . . . . . 8 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡) โˆˆ โ„)
8483, 80resubcld 11664 . . . . . . 7 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡) โˆ’ ๐‘‡) โˆˆ โ„)
8567adantr 480 . . . . . . 7 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (๐ธโ€˜๐‘Š) โˆˆ โ„)
8678, 24remulcld 11266 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡) โˆˆ โ„)
8786recnd 11264 . . . . . . . . . . 11 (๐œ‘ โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡) โˆˆ โ„‚)
8887, 33pncand 11594 . . . . . . . . . 10 (๐œ‘ โ†’ ((((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡) + ๐‘‡) โˆ’ ๐‘‡) = ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡))
8988eqcomd 2733 . . . . . . . . 9 (๐œ‘ โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡) = ((((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡) + ๐‘‡) โˆ’ ๐‘‡))
9089adantr 480 . . . . . . . 8 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡) = ((((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡) + ๐‘‡) โˆ’ ๐‘‡))
9181, 80readdcld 11265 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡) + ๐‘‡) โˆˆ โ„)
9278recnd 11264 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) โˆˆ โ„‚)
9392, 33adddirp1d 11262 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) + 1) ยท ๐‘‡) = (((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡) + ๐‘‡))
9493eqcomd 2733 . . . . . . . . . . 11 (๐œ‘ โ†’ (((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡) + ๐‘‡) = (((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) + 1) ยท ๐‘‡))
9594adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡) + ๐‘‡) = (((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) + 1) ยท ๐‘‡))
96 1red 11237 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ 1 โˆˆ โ„)
9779, 96readdcld 11265 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) + 1) โˆˆ โ„)
98 0red 11239 . . . . . . . . . . . . 13 (๐œ‘ โ†’ 0 โˆˆ โ„)
9998, 24, 59ltled 11384 . . . . . . . . . . . 12 (๐œ‘ โ†’ 0 โ‰ค ๐‘‡)
10099adantr 480 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ 0 โ‰ค ๐‘‡)
10185, 28resubcld 11664 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ((๐ธโ€˜๐‘Š) โˆ’ ๐‘) โˆˆ โ„)
10221adantr 480 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ๐‘Š โˆˆ โ„)
10385, 102resubcld 11664 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ((๐ธโ€˜๐‘Š) โˆ’ ๐‘Š) โˆˆ โ„)
10424, 59elrpd 13037 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐‘‡ โˆˆ โ„+)
105104adantr 480 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ๐‘‡ โˆˆ โ„+)
106 simpr 484 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ๐‘Š < ๐‘)
107102, 28, 85, 106ltsub2dd 11849 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ((๐ธโ€˜๐‘Š) โˆ’ ๐‘) < ((๐ธโ€˜๐‘Š) โˆ’ ๐‘Š))
108101, 103, 105, 107ltdiv1dd 13097 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (((๐ธโ€˜๐‘Š) โˆ’ ๐‘) / ๐‘‡) < (((๐ธโ€˜๐‘Š) โˆ’ ๐‘Š) / ๐‘‡))
109 fourierdlem19.ezew . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐ธโ€˜๐‘) = (๐ธโ€˜๐‘Š))
110 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ = ๐‘ โ†’ ๐‘ฅ = ๐‘)
111 oveq2 7422 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฅ = ๐‘ โ†’ (๐ต โˆ’ ๐‘ฅ) = (๐ต โˆ’ ๐‘))
112111oveq1d 7429 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฅ = ๐‘ โ†’ ((๐ต โˆ’ ๐‘ฅ) / ๐‘‡) = ((๐ต โˆ’ ๐‘) / ๐‘‡))
113112fveq2d 6895 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฅ = ๐‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) = (โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)))
114113oveq1d 7429 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ = ๐‘ โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡) = ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡))
115110, 114oveq12d 7432 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฅ = ๐‘ โ†’ (๐‘ฅ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡)) = (๐‘ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡)))
116115adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง ๐‘ฅ = ๐‘) โ†’ (๐‘ฅ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡)) = (๐‘ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡)))
11727, 86readdcld 11265 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐‘ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡)) โˆˆ โ„)
11847, 116, 27, 117fvmptd 7006 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐ธโ€˜๐‘) = (๐‘ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡)))
119109, 118eqtr3d 2769 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐ธโ€˜๐‘Š) = (๐‘ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡)))
120119oveq1d 7429 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐ธโ€˜๐‘Š) โˆ’ ๐‘) = ((๐‘ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡)) โˆ’ ๐‘))
12127recnd 11264 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐‘ โˆˆ โ„‚)
122121, 87pncan2d 11595 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐‘ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡)) โˆ’ ๐‘) = ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡))
123120, 122eqtrd 2767 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐ธโ€˜๐‘Š) โˆ’ ๐‘) = ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡))
124123oveq1d 7429 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((๐ธโ€˜๐‘Š) โˆ’ ๐‘) / ๐‘‡) = (((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡) / ๐‘‡))
12592, 33, 60divcan4d 12018 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡) / ๐‘‡) = (โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)))
126124, 125eqtr2d 2768 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) = (((๐ธโ€˜๐‘Š) โˆ’ ๐‘) / ๐‘‡))
127126adantr 480 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) = (((๐ธโ€˜๐‘Š) โˆ’ ๐‘) / ๐‘‡))
12866oveq1d 7429 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐ธโ€˜๐‘Š) โˆ’ ๐‘Š) = ((๐‘Š + ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡)) โˆ’ ๐‘Š))
129128oveq1d 7429 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((๐ธโ€˜๐‘Š) โˆ’ ๐‘Š) / ๐‘‡) = (((๐‘Š + ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡)) โˆ’ ๐‘Š) / ๐‘‡))
13021recnd 11264 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ๐‘Š โˆˆ โ„‚)
131130, 70pncan2d 11595 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐‘Š + ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡)) โˆ’ ๐‘Š) = ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡))
132131oveq1d 7429 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((๐‘Š + ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡)) โˆ’ ๐‘Š) / ๐‘‡) = (((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡) / ๐‘‡))
13363recnd 11264 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) โˆˆ โ„‚)
134133, 33, 60divcan4d 12018 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡) / ๐‘‡) = (โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)))
135129, 132, 1343eqtrrd 2772 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) = (((๐ธโ€˜๐‘Š) โˆ’ ๐‘Š) / ๐‘‡))
136135adantr 480 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) = (((๐ธโ€˜๐‘Š) โˆ’ ๐‘Š) / ๐‘‡))
137108, 127, 1363brtr4d 5174 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) < (โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)))
13877adantr 480 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) โˆˆ โ„ค)
13962adantr 480 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) โˆˆ โ„ค)
140 zltp1le 12634 . . . . . . . . . . . . 13 (((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) โˆˆ โ„ค โˆง (โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) โˆˆ โ„ค) โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) < (โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) โ†” ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) + 1) โ‰ค (โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡))))
141138, 139, 140syl2anc 583 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) < (โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) โ†” ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) + 1) โ‰ค (โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡))))
142137, 141mpbid 231 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) + 1) โ‰ค (โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)))
14397, 82, 80, 100, 142lemul1ad 12175 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) + 1) ยท ๐‘‡) โ‰ค ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡))
14495, 143eqbrtrd 5164 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡) + ๐‘‡) โ‰ค ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡))
14591, 83, 80, 144lesub1dd 11852 . . . . . . . 8 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ((((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡) + ๐‘‡) โˆ’ ๐‘‡) โ‰ค (((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡) โˆ’ ๐‘‡))
14690, 145eqbrtrd 5164 . . . . . . 7 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡) โ‰ค (((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡) โˆ’ ๐‘‡))
14781, 84, 85, 146lesub2dd 11853 . . . . . 6 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ((๐ธโ€˜๐‘Š) โˆ’ (((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡) โˆ’ ๐‘‡)) โ‰ค ((๐ธโ€˜๐‘Š) โˆ’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡)))
14874, 147eqbrtrd 5164 . . . . 5 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (((๐ธโ€˜๐‘Š) โˆ’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡)) + ๐‘‡) โ‰ค ((๐ธโ€˜๐‘Š) โˆ’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡)))
14966eqcomd 2733 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘Š + ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡)) = (๐ธโ€˜๐‘Š))
15068, 70, 130subadd2d 11612 . . . . . . . . 9 (๐œ‘ โ†’ (((๐ธโ€˜๐‘Š) โˆ’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡)) = ๐‘Š โ†” (๐‘Š + ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡)) = (๐ธโ€˜๐‘Š)))
151149, 150mpbird 257 . . . . . . . 8 (๐œ‘ โ†’ ((๐ธโ€˜๐‘Š) โˆ’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡)) = ๐‘Š)
152151eqcomd 2733 . . . . . . 7 (๐œ‘ โ†’ ๐‘Š = ((๐ธโ€˜๐‘Š) โˆ’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡)))
153152oveq1d 7429 . . . . . 6 (๐œ‘ โ†’ (๐‘Š + ๐‘‡) = (((๐ธโ€˜๐‘Š) โˆ’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡)) + ๐‘‡))
154153adantr 480 . . . . 5 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (๐‘Š + ๐‘‡) = (((๐ธโ€˜๐‘Š) โˆ’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘Š) / ๐‘‡)) ยท ๐‘‡)) + ๐‘‡))
155118eqcomd 2733 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡)) = (๐ธโ€˜๐‘))
1561rexrd 11286 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ด โˆˆ โ„*)
157 iocssre 13428 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„* โˆง ๐ต โˆˆ โ„) โ†’ (๐ด(,]๐ต) โІ โ„)
158156, 5, 157syl2anc 583 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ด(,]๐ต) โІ โ„)
1591, 5, 56, 22, 46fourierdlem4 45422 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ธ:โ„โŸถ(๐ด(,]๐ต))
160159, 27ffvelcdmd 7089 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ธโ€˜๐‘) โˆˆ (๐ด(,]๐ต))
161158, 160sseldd 3979 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ธโ€˜๐‘) โˆˆ โ„)
162161recnd 11264 . . . . . . . . 9 (๐œ‘ โ†’ (๐ธโ€˜๐‘) โˆˆ โ„‚)
163162, 87, 121subadd2d 11612 . . . . . . . 8 (๐œ‘ โ†’ (((๐ธโ€˜๐‘) โˆ’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡)) = ๐‘ โ†” (๐‘ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡)) = (๐ธโ€˜๐‘)))
164155, 163mpbird 257 . . . . . . 7 (๐œ‘ โ†’ ((๐ธโ€˜๐‘) โˆ’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡)) = ๐‘)
165109oveq1d 7429 . . . . . . 7 (๐œ‘ โ†’ ((๐ธโ€˜๐‘) โˆ’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡)) = ((๐ธโ€˜๐‘Š) โˆ’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡)))
166164, 165eqtr3d 2769 . . . . . 6 (๐œ‘ โ†’ ๐‘ = ((๐ธโ€˜๐‘Š) โˆ’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡)))
167166adantr 480 . . . . 5 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ๐‘ = ((๐ธโ€˜๐‘Š) โˆ’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘) / ๐‘‡)) ยท ๐‘‡)))
168148, 154, 1673brtr4d 5174 . . . 4 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (๐‘Š + ๐‘‡) โ‰ค ๐‘)
16916, 26, 28, 45, 168ltletrd 11396 . . 3 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ (๐ต + ๐‘‹) < ๐‘)
17016, 28ltnled 11383 . . 3 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ((๐ต + ๐‘‹) < ๐‘ โ†” ยฌ ๐‘ โ‰ค (๐ต + ๐‘‹)))
171169, 170mpbid 231 . 2 ((๐œ‘ โˆง ๐‘Š < ๐‘) โ†’ ยฌ ๐‘ โ‰ค (๐ต + ๐‘‹))
17215, 171pm2.65da 816 1 (๐œ‘ โ†’ ยฌ ๐‘Š < ๐‘)
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 395   = wceq 1534   โˆˆ wcel 2099  โˆƒwrex 3065  {crab 3427   โІ wss 3944   class class class wbr 5142   โ†ฆ cmpt 5225  โ€˜cfv 6542  (class class class)co 7414  โ„‚cc 11128  โ„cr 11129  0cc0 11130  1c1 11131   + caddc 11133   ยท cmul 11135  โ„*cxr 11269   < clt 11270   โ‰ค cle 11271   โˆ’ cmin 11466   / cdiv 11893  โ„คcz 12580  โ„+crp 12998  (,]cioc 13349  โŒŠcfl 13779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-er 8718  df-en 8956  df-dom 8957  df-sdom 8958  df-sup 9457  df-inf 9458  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-n0 12495  df-z 12581  df-uz 12845  df-rp 12999  df-ioc 13353  df-fl 13781
This theorem is referenced by:  fourierdlem51  45468
  Copyright terms: Public domain W3C validator