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

Theorem fourierdlem26 44460
Description: Periodic image of a point ๐‘Œ that's in the period that begins with the point ๐‘‹. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem26.1 (๐œ‘ โ†’ ๐ด โˆˆ โ„)
fourierdlem26.2 (๐œ‘ โ†’ ๐ต โˆˆ โ„)
fourierdlem26.3 (๐œ‘ โ†’ ๐ด < ๐ต)
fourierdlem26.4 ๐‘‡ = (๐ต โˆ’ ๐ด)
fourierdlem26.5 ๐ธ = (๐‘ฅ โˆˆ โ„ โ†ฆ (๐‘ฅ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡)))
fourierdlem26.6 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„)
fourierdlem26.7 (๐œ‘ โ†’ (๐ธโ€˜๐‘‹) = ๐ต)
fourierdlem26.8 (๐œ‘ โ†’ ๐‘Œ โˆˆ (๐‘‹(,](๐‘‹ + ๐‘‡)))
Assertion
Ref Expression
fourierdlem26 (๐œ‘ โ†’ (๐ธโ€˜๐‘Œ) = (๐ด + (๐‘Œ โˆ’ ๐‘‹)))
Distinct variable groups:   ๐‘ฅ,๐ต   ๐‘ฅ,๐‘‡   ๐‘ฅ,๐‘‹   ๐‘ฅ,๐‘Œ   ๐œ‘,๐‘ฅ
Allowed substitution hints:   ๐ด(๐‘ฅ)   ๐ธ(๐‘ฅ)

Proof of Theorem fourierdlem26
StepHypRef Expression
1 fourierdlem26.5 . . . 4 ๐ธ = (๐‘ฅ โˆˆ โ„ โ†ฆ (๐‘ฅ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡)))
21a1i 11 . . 3 (๐œ‘ โ†’ ๐ธ = (๐‘ฅ โˆˆ โ„ โ†ฆ (๐‘ฅ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡))))
3 simpr 486 . . . 4 ((๐œ‘ โˆง ๐‘ฅ = ๐‘Œ) โ†’ ๐‘ฅ = ๐‘Œ)
43oveq2d 7374 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ = ๐‘Œ) โ†’ (๐ต โˆ’ ๐‘ฅ) = (๐ต โˆ’ ๐‘Œ))
54oveq1d 7373 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ = ๐‘Œ) โ†’ ((๐ต โˆ’ ๐‘ฅ) / ๐‘‡) = ((๐ต โˆ’ ๐‘Œ) / ๐‘‡))
65fveq2d 6847 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ = ๐‘Œ) โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) = (โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)))
76oveq1d 7373 . . . 4 ((๐œ‘ โˆง ๐‘ฅ = ๐‘Œ) โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡) = ((โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) ยท ๐‘‡))
83, 7oveq12d 7376 . . 3 ((๐œ‘ โˆง ๐‘ฅ = ๐‘Œ) โ†’ (๐‘ฅ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡)) = (๐‘Œ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) ยท ๐‘‡)))
9 fourierdlem26.8 . . . . 5 (๐œ‘ โ†’ ๐‘Œ โˆˆ (๐‘‹(,](๐‘‹ + ๐‘‡)))
10 fourierdlem26.6 . . . . . . 7 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„)
1110rexrd 11210 . . . . . 6 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„*)
12 fourierdlem26.4 . . . . . . . 8 ๐‘‡ = (๐ต โˆ’ ๐ด)
13 fourierdlem26.2 . . . . . . . . 9 (๐œ‘ โ†’ ๐ต โˆˆ โ„)
14 fourierdlem26.1 . . . . . . . . 9 (๐œ‘ โ†’ ๐ด โˆˆ โ„)
1513, 14resubcld 11588 . . . . . . . 8 (๐œ‘ โ†’ (๐ต โˆ’ ๐ด) โˆˆ โ„)
1612, 15eqeltrid 2838 . . . . . . 7 (๐œ‘ โ†’ ๐‘‡ โˆˆ โ„)
1710, 16readdcld 11189 . . . . . 6 (๐œ‘ โ†’ (๐‘‹ + ๐‘‡) โˆˆ โ„)
18 elioc2 13333 . . . . . 6 ((๐‘‹ โˆˆ โ„* โˆง (๐‘‹ + ๐‘‡) โˆˆ โ„) โ†’ (๐‘Œ โˆˆ (๐‘‹(,](๐‘‹ + ๐‘‡)) โ†” (๐‘Œ โˆˆ โ„ โˆง ๐‘‹ < ๐‘Œ โˆง ๐‘Œ โ‰ค (๐‘‹ + ๐‘‡))))
1911, 17, 18syl2anc 585 . . . . 5 (๐œ‘ โ†’ (๐‘Œ โˆˆ (๐‘‹(,](๐‘‹ + ๐‘‡)) โ†” (๐‘Œ โˆˆ โ„ โˆง ๐‘‹ < ๐‘Œ โˆง ๐‘Œ โ‰ค (๐‘‹ + ๐‘‡))))
209, 19mpbid 231 . . . 4 (๐œ‘ โ†’ (๐‘Œ โˆˆ โ„ โˆง ๐‘‹ < ๐‘Œ โˆง ๐‘Œ โ‰ค (๐‘‹ + ๐‘‡)))
2120simp1d 1143 . . 3 (๐œ‘ โ†’ ๐‘Œ โˆˆ โ„)
2213, 21resubcld 11588 . . . . . . . 8 (๐œ‘ โ†’ (๐ต โˆ’ ๐‘Œ) โˆˆ โ„)
23 fourierdlem26.3 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ด < ๐ต)
2414, 13posdifd 11747 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ด < ๐ต โ†” 0 < (๐ต โˆ’ ๐ด)))
2523, 24mpbid 231 . . . . . . . . . 10 (๐œ‘ โ†’ 0 < (๐ต โˆ’ ๐ด))
2625, 12breqtrrdi 5148 . . . . . . . . 9 (๐œ‘ โ†’ 0 < ๐‘‡)
2726gt0ne0d 11724 . . . . . . . 8 (๐œ‘ โ†’ ๐‘‡ โ‰  0)
2822, 16, 27redivcld 11988 . . . . . . 7 (๐œ‘ โ†’ ((๐ต โˆ’ ๐‘Œ) / ๐‘‡) โˆˆ โ„)
2928flcld 13709 . . . . . 6 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) โˆˆ โ„ค)
3029zred 12612 . . . . 5 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) โˆˆ โ„)
3130, 16remulcld 11190 . . . 4 (๐œ‘ โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) ยท ๐‘‡) โˆˆ โ„)
3221, 31readdcld 11189 . . 3 (๐œ‘ โ†’ (๐‘Œ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) ยท ๐‘‡)) โˆˆ โ„)
332, 8, 21, 32fvmptd 6956 . 2 (๐œ‘ โ†’ (๐ธโ€˜๐‘Œ) = (๐‘Œ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) ยท ๐‘‡)))
3410recnd 11188 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„‚)
3521recnd 11188 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘Œ โˆˆ โ„‚)
3634, 35pncan3d 11520 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) = ๐‘Œ)
3736eqcomd 2739 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘Œ = (๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)))
3837oveq2d 7374 . . . . . . . . 9 (๐œ‘ โ†’ (๐ต โˆ’ ๐‘Œ) = (๐ต โˆ’ (๐‘‹ + (๐‘Œ โˆ’ ๐‘‹))))
3913recnd 11188 . . . . . . . . . 10 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
4035, 34subcld 11517 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘Œ โˆ’ ๐‘‹) โˆˆ โ„‚)
4139, 34, 40subsub4d 11548 . . . . . . . . 9 (๐œ‘ โ†’ ((๐ต โˆ’ ๐‘‹) โˆ’ (๐‘Œ โˆ’ ๐‘‹)) = (๐ต โˆ’ (๐‘‹ + (๐‘Œ โˆ’ ๐‘‹))))
4238, 41eqtr4d 2776 . . . . . . . 8 (๐œ‘ โ†’ (๐ต โˆ’ ๐‘Œ) = ((๐ต โˆ’ ๐‘‹) โˆ’ (๐‘Œ โˆ’ ๐‘‹)))
4342oveq1d 7373 . . . . . . 7 (๐œ‘ โ†’ ((๐ต โˆ’ ๐‘Œ) / ๐‘‡) = (((๐ต โˆ’ ๐‘‹) โˆ’ (๐‘Œ โˆ’ ๐‘‹)) / ๐‘‡))
4413, 10resubcld 11588 . . . . . . . . 9 (๐œ‘ โ†’ (๐ต โˆ’ ๐‘‹) โˆˆ โ„)
4544recnd 11188 . . . . . . . 8 (๐œ‘ โ†’ (๐ต โˆ’ ๐‘‹) โˆˆ โ„‚)
4616recnd 11188 . . . . . . . 8 (๐œ‘ โ†’ ๐‘‡ โˆˆ โ„‚)
4745, 40, 46, 27divsubdird 11975 . . . . . . 7 (๐œ‘ โ†’ (((๐ต โˆ’ ๐‘‹) โˆ’ (๐‘Œ โˆ’ ๐‘‹)) / ๐‘‡) = (((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ ((๐‘Œ โˆ’ ๐‘‹) / ๐‘‡)))
4840, 46, 27divnegd 11949 . . . . . . . . . 10 (๐œ‘ โ†’ -((๐‘Œ โˆ’ ๐‘‹) / ๐‘‡) = (-(๐‘Œ โˆ’ ๐‘‹) / ๐‘‡))
4935, 34negsubdi2d 11533 . . . . . . . . . . 11 (๐œ‘ โ†’ -(๐‘Œ โˆ’ ๐‘‹) = (๐‘‹ โˆ’ ๐‘Œ))
5049oveq1d 7373 . . . . . . . . . 10 (๐œ‘ โ†’ (-(๐‘Œ โˆ’ ๐‘‹) / ๐‘‡) = ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡))
5148, 50eqtrd 2773 . . . . . . . . 9 (๐œ‘ โ†’ -((๐‘Œ โˆ’ ๐‘‹) / ๐‘‡) = ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡))
5251oveq2d 7374 . . . . . . . 8 (๐œ‘ โ†’ (((๐ต โˆ’ ๐‘‹) / ๐‘‡) + -((๐‘Œ โˆ’ ๐‘‹) / ๐‘‡)) = (((๐ต โˆ’ ๐‘‹) / ๐‘‡) + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)))
5344, 16, 27redivcld 11988 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆˆ โ„)
5453recnd 11188 . . . . . . . . 9 (๐œ‘ โ†’ ((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆˆ โ„‚)
5540, 46, 27divcld 11936 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘Œ โˆ’ ๐‘‹) / ๐‘‡) โˆˆ โ„‚)
5654, 55negsubd 11523 . . . . . . . 8 (๐œ‘ โ†’ (((๐ต โˆ’ ๐‘‹) / ๐‘‡) + -((๐‘Œ โˆ’ ๐‘‹) / ๐‘‡)) = (((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ ((๐‘Œ โˆ’ ๐‘‹) / ๐‘‡)))
57 1cnd 11155 . . . . . . . . . . . 12 (๐œ‘ โ†’ 1 โˆˆ โ„‚)
5854, 57npcand 11521 . . . . . . . . . . 11 (๐œ‘ โ†’ ((((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) + 1) = ((๐ต โˆ’ ๐‘‹) / ๐‘‡))
5958eqcomd 2739 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ต โˆ’ ๐‘‹) / ๐‘‡) = ((((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) + 1))
6059oveq1d 7373 . . . . . . . . 9 (๐œ‘ โ†’ (((๐ต โˆ’ ๐‘‹) / ๐‘‡) + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)) = (((((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) + 1) + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)))
6154, 57subcld 11517 . . . . . . . . . 10 (๐œ‘ โ†’ (((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) โˆˆ โ„‚)
6234, 35subcld 11517 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‹ โˆ’ ๐‘Œ) โˆˆ โ„‚)
6362, 46, 27divcld 11936 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡) โˆˆ โ„‚)
6461, 57, 63addassd 11182 . . . . . . . . 9 (๐œ‘ โ†’ (((((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) + 1) + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)) = ((((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) + (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡))))
6560, 64eqtrd 2773 . . . . . . . 8 (๐œ‘ โ†’ (((๐ต โˆ’ ๐‘‹) / ๐‘‡) + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)) = ((((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) + (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡))))
6652, 56, 653eqtr3d 2781 . . . . . . 7 (๐œ‘ โ†’ (((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ ((๐‘Œ โˆ’ ๐‘‹) / ๐‘‡)) = ((((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) + (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡))))
6743, 47, 663eqtrd 2777 . . . . . 6 (๐œ‘ โ†’ ((๐ต โˆ’ ๐‘Œ) / ๐‘‡) = ((((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) + (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡))))
6867fveq2d 6847 . . . . 5 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) = (โŒŠโ€˜((((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) + (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)))))
6910, 21resubcld 11588 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘‹ โˆ’ ๐‘Œ) โˆˆ โ„)
7016, 69readdcld 11189 . . . . . . . 8 (๐œ‘ โ†’ (๐‘‡ + (๐‘‹ โˆ’ ๐‘Œ)) โˆˆ โ„)
7116, 26elrpd 12959 . . . . . . . 8 (๐œ‘ โ†’ ๐‘‡ โˆˆ โ„+)
7234, 46addcomd 11362 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐‘‹ + ๐‘‡) = (๐‘‡ + ๐‘‹))
7372oveq2d 7374 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘‹(,](๐‘‹ + ๐‘‡)) = (๐‘‹(,](๐‘‡ + ๐‘‹)))
749, 73eleqtrd 2836 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘Œ โˆˆ (๐‘‹(,](๐‘‡ + ๐‘‹)))
7516, 10readdcld 11189 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘‡ + ๐‘‹) โˆˆ โ„)
76 elioc2 13333 . . . . . . . . . . . . . 14 ((๐‘‹ โˆˆ โ„* โˆง (๐‘‡ + ๐‘‹) โˆˆ โ„) โ†’ (๐‘Œ โˆˆ (๐‘‹(,](๐‘‡ + ๐‘‹)) โ†” (๐‘Œ โˆˆ โ„ โˆง ๐‘‹ < ๐‘Œ โˆง ๐‘Œ โ‰ค (๐‘‡ + ๐‘‹))))
7711, 75, 76syl2anc 585 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘Œ โˆˆ (๐‘‹(,](๐‘‡ + ๐‘‹)) โ†” (๐‘Œ โˆˆ โ„ โˆง ๐‘‹ < ๐‘Œ โˆง ๐‘Œ โ‰ค (๐‘‡ + ๐‘‹))))
7874, 77mpbid 231 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘Œ โˆˆ โ„ โˆง ๐‘‹ < ๐‘Œ โˆง ๐‘Œ โ‰ค (๐‘‡ + ๐‘‹)))
7978simp3d 1145 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘Œ โ‰ค (๐‘‡ + ๐‘‹))
8021, 10, 16lesubaddd 11757 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐‘Œ โˆ’ ๐‘‹) โ‰ค ๐‘‡ โ†” ๐‘Œ โ‰ค (๐‘‡ + ๐‘‹)))
8179, 80mpbird 257 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘Œ โˆ’ ๐‘‹) โ‰ค ๐‘‡)
8221, 10resubcld 11588 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘Œ โˆ’ ๐‘‹) โˆˆ โ„)
8316, 82subge0d 11750 . . . . . . . . . 10 (๐œ‘ โ†’ (0 โ‰ค (๐‘‡ โˆ’ (๐‘Œ โˆ’ ๐‘‹)) โ†” (๐‘Œ โˆ’ ๐‘‹) โ‰ค ๐‘‡))
8481, 83mpbird 257 . . . . . . . . 9 (๐œ‘ โ†’ 0 โ‰ค (๐‘‡ โˆ’ (๐‘Œ โˆ’ ๐‘‹)))
8546, 35, 34subsub2d 11546 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘‡ โˆ’ (๐‘Œ โˆ’ ๐‘‹)) = (๐‘‡ + (๐‘‹ โˆ’ ๐‘Œ)))
8684, 85breqtrd 5132 . . . . . . . 8 (๐œ‘ โ†’ 0 โ‰ค (๐‘‡ + (๐‘‹ โˆ’ ๐‘Œ)))
8770, 71, 86divge0d 13002 . . . . . . 7 (๐œ‘ โ†’ 0 โ‰ค ((๐‘‡ + (๐‘‹ โˆ’ ๐‘Œ)) / ๐‘‡))
8846, 62, 46, 27divdird 11974 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘‡ + (๐‘‹ โˆ’ ๐‘Œ)) / ๐‘‡) = ((๐‘‡ / ๐‘‡) + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)))
8946, 27dividd 11934 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘‡ / ๐‘‡) = 1)
9089eqcomd 2739 . . . . . . . . 9 (๐œ‘ โ†’ 1 = (๐‘‡ / ๐‘‡))
9190oveq1d 7373 . . . . . . . 8 (๐œ‘ โ†’ (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)) = ((๐‘‡ / ๐‘‡) + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)))
9288, 91eqtr4d 2776 . . . . . . 7 (๐œ‘ โ†’ ((๐‘‡ + (๐‘‹ โˆ’ ๐‘Œ)) / ๐‘‡) = (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)))
9387, 92breqtrd 5132 . . . . . 6 (๐œ‘ โ†’ 0 โ‰ค (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)))
9420simp2d 1144 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘‹ < ๐‘Œ)
9510, 21sublt0d 11786 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘‹ โˆ’ ๐‘Œ) < 0 โ†” ๐‘‹ < ๐‘Œ))
9694, 95mpbird 257 . . . . . . . 8 (๐œ‘ โ†’ (๐‘‹ โˆ’ ๐‘Œ) < 0)
9769, 71, 96divlt0gt0d 43607 . . . . . . 7 (๐œ‘ โ†’ ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡) < 0)
9869, 16, 27redivcld 11988 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡) โˆˆ โ„)
99 1red 11161 . . . . . . . 8 (๐œ‘ โ†’ 1 โˆˆ โ„)
100 ltaddneg 11375 . . . . . . . 8 ((((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡) โˆˆ โ„ โˆง 1 โˆˆ โ„) โ†’ (((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡) < 0 โ†” (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)) < 1))
10198, 99, 100syl2anc 585 . . . . . . 7 (๐œ‘ โ†’ (((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡) < 0 โ†” (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)) < 1))
10297, 101mpbid 231 . . . . . 6 (๐œ‘ โ†’ (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)) < 1)
10353flcld 13709 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆˆ โ„ค)
104103zcnd 12613 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆˆ โ„‚)
105104, 46mulcld 11180 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡) โˆˆ โ„‚)
10634, 105pncan2d 11519 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) โˆ’ ๐‘‹) = ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡))
107106eqcomd 2739 . . . . . . . . . . 11 (๐œ‘ โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡) = ((๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) โˆ’ ๐‘‹))
108107oveq1d 7373 . . . . . . . . . 10 (๐œ‘ โ†’ (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡) / ๐‘‡) = (((๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) โˆ’ ๐‘‹) / ๐‘‡))
109104, 46, 27divcan4d 11942 . . . . . . . . . 10 (๐œ‘ โ†’ (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡) / ๐‘‡) = (โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)))
110 id 22 . . . . . . . . . . . . . . . . 17 (๐‘ฅ = ๐‘‹ โ†’ ๐‘ฅ = ๐‘‹)
111 oveq2 7366 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ = ๐‘‹ โ†’ (๐ต โˆ’ ๐‘ฅ) = (๐ต โˆ’ ๐‘‹))
112111oveq1d 7373 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ = ๐‘‹ โ†’ ((๐ต โˆ’ ๐‘ฅ) / ๐‘‡) = ((๐ต โˆ’ ๐‘‹) / ๐‘‡))
113112fveq2d 6847 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ = ๐‘‹ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) = (โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)))
114113oveq1d 7373 . . . . . . . . . . . . . . . . 17 (๐‘ฅ = ๐‘‹ โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡) = ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡))
115110, 114oveq12d 7376 . . . . . . . . . . . . . . . 16 (๐‘ฅ = ๐‘‹ โ†’ (๐‘ฅ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡)) = (๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)))
116115adantl 483 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โ†’ (๐‘ฅ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡)) = (๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)))
117 reflcl 13707 . . . . . . . . . . . . . . . . . 18 (((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆˆ โ„ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆˆ โ„)
11853, 117syl 17 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆˆ โ„)
119118, 16remulcld 11190 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡) โˆˆ โ„)
12010, 119readdcld 11189 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) โˆˆ โ„)
1212, 116, 10, 120fvmptd 6956 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ธโ€˜๐‘‹) = (๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)))
122121eqcomd 2739 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) = (๐ธโ€˜๐‘‹))
123122oveq1d 7373 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) โˆ’ ๐‘‹) = ((๐ธโ€˜๐‘‹) โˆ’ ๐‘‹))
124123oveq1d 7373 . . . . . . . . . . 11 (๐œ‘ โ†’ (((๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) โˆ’ ๐‘‹) / ๐‘‡) = (((๐ธโ€˜๐‘‹) โˆ’ ๐‘‹) / ๐‘‡))
125 fourierdlem26.7 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐ธโ€˜๐‘‹) = ๐ต)
126125oveq1d 7373 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ธโ€˜๐‘‹) โˆ’ ๐‘‹) = (๐ต โˆ’ ๐‘‹))
127126oveq1d 7373 . . . . . . . . . . 11 (๐œ‘ โ†’ (((๐ธโ€˜๐‘‹) โˆ’ ๐‘‹) / ๐‘‡) = ((๐ต โˆ’ ๐‘‹) / ๐‘‡))
128124, 127eqtrd 2773 . . . . . . . . . 10 (๐œ‘ โ†’ (((๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) โˆ’ ๐‘‹) / ๐‘‡) = ((๐ต โˆ’ ๐‘‹) / ๐‘‡))
129108, 109, 1283eqtr3d 2781 . . . . . . . . 9 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) = ((๐ต โˆ’ ๐‘‹) / ๐‘‡))
130129, 103eqeltrrd 2835 . . . . . . . 8 (๐œ‘ โ†’ ((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆˆ โ„ค)
131 1zzd 12539 . . . . . . . 8 (๐œ‘ โ†’ 1 โˆˆ โ„ค)
132130, 131zsubcld 12617 . . . . . . 7 (๐œ‘ โ†’ (((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) โˆˆ โ„ค)
13399, 98readdcld 11189 . . . . . . 7 (๐œ‘ โ†’ (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)) โˆˆ โ„)
134 flbi2 13728 . . . . . . 7 (((((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) โˆˆ โ„ค โˆง (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)) โˆˆ โ„) โ†’ ((โŒŠโ€˜((((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) + (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)))) = (((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) โ†” (0 โ‰ค (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)) โˆง (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)) < 1)))
135132, 133, 134syl2anc 585 . . . . . 6 (๐œ‘ โ†’ ((โŒŠโ€˜((((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) + (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)))) = (((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) โ†” (0 โ‰ค (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)) โˆง (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)) < 1)))
13693, 102, 135mpbir2and 712 . . . . 5 (๐œ‘ โ†’ (โŒŠโ€˜((((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) + (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)))) = (((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1))
137129eqcomd 2739 . . . . . 6 (๐œ‘ โ†’ ((๐ต โˆ’ ๐‘‹) / ๐‘‡) = (โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)))
138137oveq1d 7373 . . . . 5 (๐œ‘ โ†’ (((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) = ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆ’ 1))
13968, 136, 1383eqtrd 2777 . . . 4 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) = ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆ’ 1))
140139oveq1d 7373 . . 3 (๐œ‘ โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) ยท ๐‘‡) = (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆ’ 1) ยท ๐‘‡))
141140oveq2d 7374 . 2 (๐œ‘ โ†’ (๐‘Œ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) ยท ๐‘‡)) = (๐‘Œ + (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆ’ 1) ยท ๐‘‡)))
14237oveq1d 7373 . . 3 (๐œ‘ โ†’ (๐‘Œ + (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆ’ 1) ยท ๐‘‡)) = ((๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) + (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆ’ 1) ยท ๐‘‡)))
143104, 57, 46subdird 11617 . . . . 5 (๐œ‘ โ†’ (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆ’ 1) ยท ๐‘‡) = (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡) โˆ’ (1 ยท ๐‘‡)))
144143oveq2d 7374 . . . 4 (๐œ‘ โ†’ ((๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) + (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆ’ 1) ยท ๐‘‡)) = ((๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) + (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡) โˆ’ (1 ยท ๐‘‡))))
14534, 40addcld 11179 . . . . . 6 (๐œ‘ โ†’ (๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) โˆˆ โ„‚)
14657, 46mulcld 11180 . . . . . 6 (๐œ‘ โ†’ (1 ยท ๐‘‡) โˆˆ โ„‚)
147145, 105, 146addsubassd 11537 . . . . 5 (๐œ‘ โ†’ (((๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) โˆ’ (1 ยท ๐‘‡)) = ((๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) + (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡) โˆ’ (1 ยท ๐‘‡))))
148147eqcomd 2739 . . . 4 (๐œ‘ โ†’ ((๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) + (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡) โˆ’ (1 ยท ๐‘‡))) = (((๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) โˆ’ (1 ยท ๐‘‡)))
14934, 40, 105add32d 11387 . . . . . 6 (๐œ‘ โ†’ ((๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) = ((๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) + (๐‘Œ โˆ’ ๐‘‹)))
150149oveq1d 7373 . . . . 5 (๐œ‘ โ†’ (((๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) โˆ’ (1 ยท ๐‘‡)) = (((๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) + (๐‘Œ โˆ’ ๐‘‹)) โˆ’ (1 ยท ๐‘‡)))
151122oveq1d 7373 . . . . . 6 (๐œ‘ โ†’ ((๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) + (๐‘Œ โˆ’ ๐‘‹)) = ((๐ธโ€˜๐‘‹) + (๐‘Œ โˆ’ ๐‘‹)))
15246mulid2d 11178 . . . . . 6 (๐œ‘ โ†’ (1 ยท ๐‘‡) = ๐‘‡)
153151, 152oveq12d 7376 . . . . 5 (๐œ‘ โ†’ (((๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) + (๐‘Œ โˆ’ ๐‘‹)) โˆ’ (1 ยท ๐‘‡)) = (((๐ธโ€˜๐‘‹) + (๐‘Œ โˆ’ ๐‘‹)) โˆ’ ๐‘‡))
154125, 13eqeltrd 2834 . . . . . . . 8 (๐œ‘ โ†’ (๐ธโ€˜๐‘‹) โˆˆ โ„)
155154recnd 11188 . . . . . . 7 (๐œ‘ โ†’ (๐ธโ€˜๐‘‹) โˆˆ โ„‚)
156155, 40, 46addsubd 11538 . . . . . 6 (๐œ‘ โ†’ (((๐ธโ€˜๐‘‹) + (๐‘Œ โˆ’ ๐‘‹)) โˆ’ ๐‘‡) = (((๐ธโ€˜๐‘‹) โˆ’ ๐‘‡) + (๐‘Œ โˆ’ ๐‘‹)))
157125oveq1d 7373 . . . . . . . 8 (๐œ‘ โ†’ ((๐ธโ€˜๐‘‹) โˆ’ ๐‘‡) = (๐ต โˆ’ ๐‘‡))
15812a1i 11 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘‡ = (๐ต โˆ’ ๐ด))
159158oveq2d 7374 . . . . . . . 8 (๐œ‘ โ†’ (๐ต โˆ’ ๐‘‡) = (๐ต โˆ’ (๐ต โˆ’ ๐ด)))
16014recnd 11188 . . . . . . . . 9 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
16139, 160nncand 11522 . . . . . . . 8 (๐œ‘ โ†’ (๐ต โˆ’ (๐ต โˆ’ ๐ด)) = ๐ด)
162157, 159, 1613eqtrd 2777 . . . . . . 7 (๐œ‘ โ†’ ((๐ธโ€˜๐‘‹) โˆ’ ๐‘‡) = ๐ด)
163162oveq1d 7373 . . . . . 6 (๐œ‘ โ†’ (((๐ธโ€˜๐‘‹) โˆ’ ๐‘‡) + (๐‘Œ โˆ’ ๐‘‹)) = (๐ด + (๐‘Œ โˆ’ ๐‘‹)))
164156, 163eqtrd 2773 . . . . 5 (๐œ‘ โ†’ (((๐ธโ€˜๐‘‹) + (๐‘Œ โˆ’ ๐‘‹)) โˆ’ ๐‘‡) = (๐ด + (๐‘Œ โˆ’ ๐‘‹)))
165150, 153, 1643eqtrd 2777 . . . 4 (๐œ‘ โ†’ (((๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) โˆ’ (1 ยท ๐‘‡)) = (๐ด + (๐‘Œ โˆ’ ๐‘‹)))
166144, 148, 1653eqtrd 2777 . . 3 (๐œ‘ โ†’ ((๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) + (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆ’ 1) ยท ๐‘‡)) = (๐ด + (๐‘Œ โˆ’ ๐‘‹)))
167142, 166eqtrd 2773 . 2 (๐œ‘ โ†’ (๐‘Œ + (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆ’ 1) ยท ๐‘‡)) = (๐ด + (๐‘Œ โˆ’ ๐‘‹)))
16833, 141, 1673eqtrd 2777 1 (๐œ‘ โ†’ (๐ธโ€˜๐‘Œ) = (๐ด + (๐‘Œ โˆ’ ๐‘‹)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   class class class wbr 5106   โ†ฆ cmpt 5189  โ€˜cfv 6497  (class class class)co 7358  โ„cr 11055  0cc0 11056  1c1 11057   + caddc 11059   ยท cmul 11061  โ„*cxr 11193   < clt 11194   โ‰ค cle 11195   โˆ’ cmin 11390  -cneg 11391   / cdiv 11817  โ„คcz 12504  (,]cioc 13271  โŒŠcfl 13701
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-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  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
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-op 4594  df-uni 4867  df-iun 4957  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-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-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-er 8651  df-en 8887  df-dom 8888  df-sdom 8889  df-sup 9383  df-inf 9384  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-n0 12419  df-z 12505  df-uz 12769  df-rp 12921  df-ioc 13275  df-fl 13703
This theorem is referenced by:  fourierdlem65  44498  fourierdlem79  44512
  Copyright terms: Public domain W3C validator