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 44849
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 7425 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ = ๐‘Œ) โ†’ (๐ต โˆ’ ๐‘ฅ) = (๐ต โˆ’ ๐‘Œ))
54oveq1d 7424 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ = ๐‘Œ) โ†’ ((๐ต โˆ’ ๐‘ฅ) / ๐‘‡) = ((๐ต โˆ’ ๐‘Œ) / ๐‘‡))
65fveq2d 6896 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ = ๐‘Œ) โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) = (โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)))
76oveq1d 7424 . . . 4 ((๐œ‘ โˆง ๐‘ฅ = ๐‘Œ) โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡) = ((โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) ยท ๐‘‡))
83, 7oveq12d 7427 . . 3 ((๐œ‘ โˆง ๐‘ฅ = ๐‘Œ) โ†’ (๐‘ฅ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡)) = (๐‘Œ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) ยท ๐‘‡)))
9 fourierdlem26.8 . . . . 5 (๐œ‘ โ†’ ๐‘Œ โˆˆ (๐‘‹(,](๐‘‹ + ๐‘‡)))
10 fourierdlem26.6 . . . . . . 7 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„)
1110rexrd 11264 . . . . . 6 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„*)
12 fourierdlem26.4 . . . . . . . 8 ๐‘‡ = (๐ต โˆ’ ๐ด)
13 fourierdlem26.2 . . . . . . . . 9 (๐œ‘ โ†’ ๐ต โˆˆ โ„)
14 fourierdlem26.1 . . . . . . . . 9 (๐œ‘ โ†’ ๐ด โˆˆ โ„)
1513, 14resubcld 11642 . . . . . . . 8 (๐œ‘ โ†’ (๐ต โˆ’ ๐ด) โˆˆ โ„)
1612, 15eqeltrid 2838 . . . . . . 7 (๐œ‘ โ†’ ๐‘‡ โˆˆ โ„)
1710, 16readdcld 11243 . . . . . 6 (๐œ‘ โ†’ (๐‘‹ + ๐‘‡) โˆˆ โ„)
18 elioc2 13387 . . . . . 6 ((๐‘‹ โˆˆ โ„* โˆง (๐‘‹ + ๐‘‡) โˆˆ โ„) โ†’ (๐‘Œ โˆˆ (๐‘‹(,](๐‘‹ + ๐‘‡)) โ†” (๐‘Œ โˆˆ โ„ โˆง ๐‘‹ < ๐‘Œ โˆง ๐‘Œ โ‰ค (๐‘‹ + ๐‘‡))))
1911, 17, 18syl2anc 585 . . . . 5 (๐œ‘ โ†’ (๐‘Œ โˆˆ (๐‘‹(,](๐‘‹ + ๐‘‡)) โ†” (๐‘Œ โˆˆ โ„ โˆง ๐‘‹ < ๐‘Œ โˆง ๐‘Œ โ‰ค (๐‘‹ + ๐‘‡))))
209, 19mpbid 231 . . . 4 (๐œ‘ โ†’ (๐‘Œ โˆˆ โ„ โˆง ๐‘‹ < ๐‘Œ โˆง ๐‘Œ โ‰ค (๐‘‹ + ๐‘‡)))
2120simp1d 1143 . . 3 (๐œ‘ โ†’ ๐‘Œ โˆˆ โ„)
2213, 21resubcld 11642 . . . . . . . 8 (๐œ‘ โ†’ (๐ต โˆ’ ๐‘Œ) โˆˆ โ„)
23 fourierdlem26.3 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ด < ๐ต)
2414, 13posdifd 11801 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ด < ๐ต โ†” 0 < (๐ต โˆ’ ๐ด)))
2523, 24mpbid 231 . . . . . . . . . 10 (๐œ‘ โ†’ 0 < (๐ต โˆ’ ๐ด))
2625, 12breqtrrdi 5191 . . . . . . . . 9 (๐œ‘ โ†’ 0 < ๐‘‡)
2726gt0ne0d 11778 . . . . . . . 8 (๐œ‘ โ†’ ๐‘‡ โ‰  0)
2822, 16, 27redivcld 12042 . . . . . . 7 (๐œ‘ โ†’ ((๐ต โˆ’ ๐‘Œ) / ๐‘‡) โˆˆ โ„)
2928flcld 13763 . . . . . 6 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) โˆˆ โ„ค)
3029zred 12666 . . . . 5 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) โˆˆ โ„)
3130, 16remulcld 11244 . . . 4 (๐œ‘ โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) ยท ๐‘‡) โˆˆ โ„)
3221, 31readdcld 11243 . . 3 (๐œ‘ โ†’ (๐‘Œ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) ยท ๐‘‡)) โˆˆ โ„)
332, 8, 21, 32fvmptd 7006 . 2 (๐œ‘ โ†’ (๐ธโ€˜๐‘Œ) = (๐‘Œ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) ยท ๐‘‡)))
3410recnd 11242 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘‹ โˆˆ โ„‚)
3521recnd 11242 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘Œ โˆˆ โ„‚)
3634, 35pncan3d 11574 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) = ๐‘Œ)
3736eqcomd 2739 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘Œ = (๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)))
3837oveq2d 7425 . . . . . . . . 9 (๐œ‘ โ†’ (๐ต โˆ’ ๐‘Œ) = (๐ต โˆ’ (๐‘‹ + (๐‘Œ โˆ’ ๐‘‹))))
3913recnd 11242 . . . . . . . . . 10 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
4035, 34subcld 11571 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘Œ โˆ’ ๐‘‹) โˆˆ โ„‚)
4139, 34, 40subsub4d 11602 . . . . . . . . 9 (๐œ‘ โ†’ ((๐ต โˆ’ ๐‘‹) โˆ’ (๐‘Œ โˆ’ ๐‘‹)) = (๐ต โˆ’ (๐‘‹ + (๐‘Œ โˆ’ ๐‘‹))))
4238, 41eqtr4d 2776 . . . . . . . 8 (๐œ‘ โ†’ (๐ต โˆ’ ๐‘Œ) = ((๐ต โˆ’ ๐‘‹) โˆ’ (๐‘Œ โˆ’ ๐‘‹)))
4342oveq1d 7424 . . . . . . 7 (๐œ‘ โ†’ ((๐ต โˆ’ ๐‘Œ) / ๐‘‡) = (((๐ต โˆ’ ๐‘‹) โˆ’ (๐‘Œ โˆ’ ๐‘‹)) / ๐‘‡))
4413, 10resubcld 11642 . . . . . . . . 9 (๐œ‘ โ†’ (๐ต โˆ’ ๐‘‹) โˆˆ โ„)
4544recnd 11242 . . . . . . . 8 (๐œ‘ โ†’ (๐ต โˆ’ ๐‘‹) โˆˆ โ„‚)
4616recnd 11242 . . . . . . . 8 (๐œ‘ โ†’ ๐‘‡ โˆˆ โ„‚)
4745, 40, 46, 27divsubdird 12029 . . . . . . 7 (๐œ‘ โ†’ (((๐ต โˆ’ ๐‘‹) โˆ’ (๐‘Œ โˆ’ ๐‘‹)) / ๐‘‡) = (((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ ((๐‘Œ โˆ’ ๐‘‹) / ๐‘‡)))
4840, 46, 27divnegd 12003 . . . . . . . . . 10 (๐œ‘ โ†’ -((๐‘Œ โˆ’ ๐‘‹) / ๐‘‡) = (-(๐‘Œ โˆ’ ๐‘‹) / ๐‘‡))
4935, 34negsubdi2d 11587 . . . . . . . . . . 11 (๐œ‘ โ†’ -(๐‘Œ โˆ’ ๐‘‹) = (๐‘‹ โˆ’ ๐‘Œ))
5049oveq1d 7424 . . . . . . . . . 10 (๐œ‘ โ†’ (-(๐‘Œ โˆ’ ๐‘‹) / ๐‘‡) = ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡))
5148, 50eqtrd 2773 . . . . . . . . 9 (๐œ‘ โ†’ -((๐‘Œ โˆ’ ๐‘‹) / ๐‘‡) = ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡))
5251oveq2d 7425 . . . . . . . 8 (๐œ‘ โ†’ (((๐ต โˆ’ ๐‘‹) / ๐‘‡) + -((๐‘Œ โˆ’ ๐‘‹) / ๐‘‡)) = (((๐ต โˆ’ ๐‘‹) / ๐‘‡) + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)))
5344, 16, 27redivcld 12042 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆˆ โ„)
5453recnd 11242 . . . . . . . . 9 (๐œ‘ โ†’ ((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆˆ โ„‚)
5540, 46, 27divcld 11990 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘Œ โˆ’ ๐‘‹) / ๐‘‡) โˆˆ โ„‚)
5654, 55negsubd 11577 . . . . . . . 8 (๐œ‘ โ†’ (((๐ต โˆ’ ๐‘‹) / ๐‘‡) + -((๐‘Œ โˆ’ ๐‘‹) / ๐‘‡)) = (((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ ((๐‘Œ โˆ’ ๐‘‹) / ๐‘‡)))
57 1cnd 11209 . . . . . . . . . . . 12 (๐œ‘ โ†’ 1 โˆˆ โ„‚)
5854, 57npcand 11575 . . . . . . . . . . 11 (๐œ‘ โ†’ ((((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) + 1) = ((๐ต โˆ’ ๐‘‹) / ๐‘‡))
5958eqcomd 2739 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ต โˆ’ ๐‘‹) / ๐‘‡) = ((((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) + 1))
6059oveq1d 7424 . . . . . . . . 9 (๐œ‘ โ†’ (((๐ต โˆ’ ๐‘‹) / ๐‘‡) + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)) = (((((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) + 1) + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)))
6154, 57subcld 11571 . . . . . . . . . 10 (๐œ‘ โ†’ (((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) โˆˆ โ„‚)
6234, 35subcld 11571 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‹ โˆ’ ๐‘Œ) โˆˆ โ„‚)
6362, 46, 27divcld 11990 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡) โˆˆ โ„‚)
6461, 57, 63addassd 11236 . . . . . . . . 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 6896 . . . . 5 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) = (โŒŠโ€˜((((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) + (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)))))
6910, 21resubcld 11642 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘‹ โˆ’ ๐‘Œ) โˆˆ โ„)
7016, 69readdcld 11243 . . . . . . . 8 (๐œ‘ โ†’ (๐‘‡ + (๐‘‹ โˆ’ ๐‘Œ)) โˆˆ โ„)
7116, 26elrpd 13013 . . . . . . . 8 (๐œ‘ โ†’ ๐‘‡ โˆˆ โ„+)
7234, 46addcomd 11416 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐‘‹ + ๐‘‡) = (๐‘‡ + ๐‘‹))
7372oveq2d 7425 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘‹(,](๐‘‹ + ๐‘‡)) = (๐‘‹(,](๐‘‡ + ๐‘‹)))
749, 73eleqtrd 2836 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘Œ โˆˆ (๐‘‹(,](๐‘‡ + ๐‘‹)))
7516, 10readdcld 11243 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘‡ + ๐‘‹) โˆˆ โ„)
76 elioc2 13387 . . . . . . . . . . . . . 14 ((๐‘‹ โˆˆ โ„* โˆง (๐‘‡ + ๐‘‹) โˆˆ โ„) โ†’ (๐‘Œ โˆˆ (๐‘‹(,](๐‘‡ + ๐‘‹)) โ†” (๐‘Œ โˆˆ โ„ โˆง ๐‘‹ < ๐‘Œ โˆง ๐‘Œ โ‰ค (๐‘‡ + ๐‘‹))))
7711, 75, 76syl2anc 585 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘Œ โˆˆ (๐‘‹(,](๐‘‡ + ๐‘‹)) โ†” (๐‘Œ โˆˆ โ„ โˆง ๐‘‹ < ๐‘Œ โˆง ๐‘Œ โ‰ค (๐‘‡ + ๐‘‹))))
7874, 77mpbid 231 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘Œ โˆˆ โ„ โˆง ๐‘‹ < ๐‘Œ โˆง ๐‘Œ โ‰ค (๐‘‡ + ๐‘‹)))
7978simp3d 1145 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘Œ โ‰ค (๐‘‡ + ๐‘‹))
8021, 10, 16lesubaddd 11811 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐‘Œ โˆ’ ๐‘‹) โ‰ค ๐‘‡ โ†” ๐‘Œ โ‰ค (๐‘‡ + ๐‘‹)))
8179, 80mpbird 257 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘Œ โˆ’ ๐‘‹) โ‰ค ๐‘‡)
8221, 10resubcld 11642 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘Œ โˆ’ ๐‘‹) โˆˆ โ„)
8316, 82subge0d 11804 . . . . . . . . . 10 (๐œ‘ โ†’ (0 โ‰ค (๐‘‡ โˆ’ (๐‘Œ โˆ’ ๐‘‹)) โ†” (๐‘Œ โˆ’ ๐‘‹) โ‰ค ๐‘‡))
8481, 83mpbird 257 . . . . . . . . 9 (๐œ‘ โ†’ 0 โ‰ค (๐‘‡ โˆ’ (๐‘Œ โˆ’ ๐‘‹)))
8546, 35, 34subsub2d 11600 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘‡ โˆ’ (๐‘Œ โˆ’ ๐‘‹)) = (๐‘‡ + (๐‘‹ โˆ’ ๐‘Œ)))
8684, 85breqtrd 5175 . . . . . . . 8 (๐œ‘ โ†’ 0 โ‰ค (๐‘‡ + (๐‘‹ โˆ’ ๐‘Œ)))
8770, 71, 86divge0d 13056 . . . . . . 7 (๐œ‘ โ†’ 0 โ‰ค ((๐‘‡ + (๐‘‹ โˆ’ ๐‘Œ)) / ๐‘‡))
8846, 62, 46, 27divdird 12028 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘‡ + (๐‘‹ โˆ’ ๐‘Œ)) / ๐‘‡) = ((๐‘‡ / ๐‘‡) + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)))
8946, 27dividd 11988 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘‡ / ๐‘‡) = 1)
9089eqcomd 2739 . . . . . . . . 9 (๐œ‘ โ†’ 1 = (๐‘‡ / ๐‘‡))
9190oveq1d 7424 . . . . . . . 8 (๐œ‘ โ†’ (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)) = ((๐‘‡ / ๐‘‡) + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)))
9288, 91eqtr4d 2776 . . . . . . 7 (๐œ‘ โ†’ ((๐‘‡ + (๐‘‹ โˆ’ ๐‘Œ)) / ๐‘‡) = (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)))
9387, 92breqtrd 5175 . . . . . 6 (๐œ‘ โ†’ 0 โ‰ค (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)))
9420simp2d 1144 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘‹ < ๐‘Œ)
9510, 21sublt0d 11840 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘‹ โˆ’ ๐‘Œ) < 0 โ†” ๐‘‹ < ๐‘Œ))
9694, 95mpbird 257 . . . . . . . 8 (๐œ‘ โ†’ (๐‘‹ โˆ’ ๐‘Œ) < 0)
9769, 71, 96divlt0gt0d 43996 . . . . . . 7 (๐œ‘ โ†’ ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡) < 0)
9869, 16, 27redivcld 12042 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡) โˆˆ โ„)
99 1red 11215 . . . . . . . 8 (๐œ‘ โ†’ 1 โˆˆ โ„)
100 ltaddneg 11429 . . . . . . . 8 ((((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡) โˆˆ โ„ โˆง 1 โˆˆ โ„) โ†’ (((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡) < 0 โ†” (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)) < 1))
10198, 99, 100syl2anc 585 . . . . . . 7 (๐œ‘ โ†’ (((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡) < 0 โ†” (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)) < 1))
10297, 101mpbid 231 . . . . . 6 (๐œ‘ โ†’ (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)) < 1)
10353flcld 13763 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆˆ โ„ค)
104103zcnd 12667 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆˆ โ„‚)
105104, 46mulcld 11234 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡) โˆˆ โ„‚)
10634, 105pncan2d 11573 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) โˆ’ ๐‘‹) = ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡))
107106eqcomd 2739 . . . . . . . . . . 11 (๐œ‘ โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡) = ((๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) โˆ’ ๐‘‹))
108107oveq1d 7424 . . . . . . . . . 10 (๐œ‘ โ†’ (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡) / ๐‘‡) = (((๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) โˆ’ ๐‘‹) / ๐‘‡))
109104, 46, 27divcan4d 11996 . . . . . . . . . 10 (๐œ‘ โ†’ (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡) / ๐‘‡) = (โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)))
110 id 22 . . . . . . . . . . . . . . . . 17 (๐‘ฅ = ๐‘‹ โ†’ ๐‘ฅ = ๐‘‹)
111 oveq2 7417 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ = ๐‘‹ โ†’ (๐ต โˆ’ ๐‘ฅ) = (๐ต โˆ’ ๐‘‹))
112111oveq1d 7424 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ = ๐‘‹ โ†’ ((๐ต โˆ’ ๐‘ฅ) / ๐‘‡) = ((๐ต โˆ’ ๐‘‹) / ๐‘‡))
113112fveq2d 6896 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ = ๐‘‹ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) = (โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)))
114113oveq1d 7424 . . . . . . . . . . . . . . . . 17 (๐‘ฅ = ๐‘‹ โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡) = ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡))
115110, 114oveq12d 7427 . . . . . . . . . . . . . . . 16 (๐‘ฅ = ๐‘‹ โ†’ (๐‘ฅ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡)) = (๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)))
116115adantl 483 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ฅ = ๐‘‹) โ†’ (๐‘ฅ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘ฅ) / ๐‘‡)) ยท ๐‘‡)) = (๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)))
117 reflcl 13761 . . . . . . . . . . . . . . . . . 18 (((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆˆ โ„ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆˆ โ„)
11853, 117syl 17 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆˆ โ„)
119118, 16remulcld 11244 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡) โˆˆ โ„)
12010, 119readdcld 11243 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) โˆˆ โ„)
1212, 116, 10, 120fvmptd 7006 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ธโ€˜๐‘‹) = (๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)))
122121eqcomd 2739 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) = (๐ธโ€˜๐‘‹))
123122oveq1d 7424 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) โˆ’ ๐‘‹) = ((๐ธโ€˜๐‘‹) โˆ’ ๐‘‹))
124123oveq1d 7424 . . . . . . . . . . 11 (๐œ‘ โ†’ (((๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) โˆ’ ๐‘‹) / ๐‘‡) = (((๐ธโ€˜๐‘‹) โˆ’ ๐‘‹) / ๐‘‡))
125 fourierdlem26.7 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐ธโ€˜๐‘‹) = ๐ต)
126125oveq1d 7424 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ธโ€˜๐‘‹) โˆ’ ๐‘‹) = (๐ต โˆ’ ๐‘‹))
127126oveq1d 7424 . . . . . . . . . . 11 (๐œ‘ โ†’ (((๐ธโ€˜๐‘‹) โˆ’ ๐‘‹) / ๐‘‡) = ((๐ต โˆ’ ๐‘‹) / ๐‘‡))
128124, 127eqtrd 2773 . . . . . . . . . 10 (๐œ‘ โ†’ (((๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) โˆ’ ๐‘‹) / ๐‘‡) = ((๐ต โˆ’ ๐‘‹) / ๐‘‡))
129108, 109, 1283eqtr3d 2781 . . . . . . . . 9 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) = ((๐ต โˆ’ ๐‘‹) / ๐‘‡))
130129, 103eqeltrrd 2835 . . . . . . . 8 (๐œ‘ โ†’ ((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆˆ โ„ค)
131 1zzd 12593 . . . . . . . 8 (๐œ‘ โ†’ 1 โˆˆ โ„ค)
132130, 131zsubcld 12671 . . . . . . 7 (๐œ‘ โ†’ (((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) โˆˆ โ„ค)
13399, 98readdcld 11243 . . . . . . 7 (๐œ‘ โ†’ (1 + ((๐‘‹ โˆ’ ๐‘Œ) / ๐‘‡)) โˆˆ โ„)
134 flbi2 13782 . . . . . . 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 7424 . . . . 5 (๐œ‘ โ†’ (((๐ต โˆ’ ๐‘‹) / ๐‘‡) โˆ’ 1) = ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆ’ 1))
13968, 136, 1383eqtrd 2777 . . . 4 (๐œ‘ โ†’ (โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) = ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆ’ 1))
140139oveq1d 7424 . . 3 (๐œ‘ โ†’ ((โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) ยท ๐‘‡) = (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆ’ 1) ยท ๐‘‡))
141140oveq2d 7425 . 2 (๐œ‘ โ†’ (๐‘Œ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘Œ) / ๐‘‡)) ยท ๐‘‡)) = (๐‘Œ + (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆ’ 1) ยท ๐‘‡)))
14237oveq1d 7424 . . 3 (๐œ‘ โ†’ (๐‘Œ + (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆ’ 1) ยท ๐‘‡)) = ((๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) + (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆ’ 1) ยท ๐‘‡)))
143104, 57, 46subdird 11671 . . . . 5 (๐œ‘ โ†’ (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆ’ 1) ยท ๐‘‡) = (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡) โˆ’ (1 ยท ๐‘‡)))
144143oveq2d 7425 . . . 4 (๐œ‘ โ†’ ((๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) + (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) โˆ’ 1) ยท ๐‘‡)) = ((๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) + (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡) โˆ’ (1 ยท ๐‘‡))))
14534, 40addcld 11233 . . . . . 6 (๐œ‘ โ†’ (๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) โˆˆ โ„‚)
14657, 46mulcld 11234 . . . . . 6 (๐œ‘ โ†’ (1 ยท ๐‘‡) โˆˆ โ„‚)
147145, 105, 146addsubassd 11591 . . . . 5 (๐œ‘ โ†’ (((๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) โˆ’ (1 ยท ๐‘‡)) = ((๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) + (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡) โˆ’ (1 ยท ๐‘‡))))
148147eqcomd 2739 . . . 4 (๐œ‘ โ†’ ((๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) + (((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡) โˆ’ (1 ยท ๐‘‡))) = (((๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) โˆ’ (1 ยท ๐‘‡)))
14934, 40, 105add32d 11441 . . . . . 6 (๐œ‘ โ†’ ((๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) = ((๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) + (๐‘Œ โˆ’ ๐‘‹)))
150149oveq1d 7424 . . . . 5 (๐œ‘ โ†’ (((๐‘‹ + (๐‘Œ โˆ’ ๐‘‹)) + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) โˆ’ (1 ยท ๐‘‡)) = (((๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) + (๐‘Œ โˆ’ ๐‘‹)) โˆ’ (1 ยท ๐‘‡)))
151122oveq1d 7424 . . . . . 6 (๐œ‘ โ†’ ((๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) + (๐‘Œ โˆ’ ๐‘‹)) = ((๐ธโ€˜๐‘‹) + (๐‘Œ โˆ’ ๐‘‹)))
15246mullidd 11232 . . . . . 6 (๐œ‘ โ†’ (1 ยท ๐‘‡) = ๐‘‡)
153151, 152oveq12d 7427 . . . . 5 (๐œ‘ โ†’ (((๐‘‹ + ((โŒŠโ€˜((๐ต โˆ’ ๐‘‹) / ๐‘‡)) ยท ๐‘‡)) + (๐‘Œ โˆ’ ๐‘‹)) โˆ’ (1 ยท ๐‘‡)) = (((๐ธโ€˜๐‘‹) + (๐‘Œ โˆ’ ๐‘‹)) โˆ’ ๐‘‡))
154125, 13eqeltrd 2834 . . . . . . . 8 (๐œ‘ โ†’ (๐ธโ€˜๐‘‹) โˆˆ โ„)
155154recnd 11242 . . . . . . 7 (๐œ‘ โ†’ (๐ธโ€˜๐‘‹) โˆˆ โ„‚)
156155, 40, 46addsubd 11592 . . . . . 6 (๐œ‘ โ†’ (((๐ธโ€˜๐‘‹) + (๐‘Œ โˆ’ ๐‘‹)) โˆ’ ๐‘‡) = (((๐ธโ€˜๐‘‹) โˆ’ ๐‘‡) + (๐‘Œ โˆ’ ๐‘‹)))
157125oveq1d 7424 . . . . . . . 8 (๐œ‘ โ†’ ((๐ธโ€˜๐‘‹) โˆ’ ๐‘‡) = (๐ต โˆ’ ๐‘‡))
15812a1i 11 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘‡ = (๐ต โˆ’ ๐ด))
159158oveq2d 7425 . . . . . . . 8 (๐œ‘ โ†’ (๐ต โˆ’ ๐‘‡) = (๐ต โˆ’ (๐ต โˆ’ ๐ด)))
16014recnd 11242 . . . . . . . . 9 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
16139, 160nncand 11576 . . . . . . . 8 (๐œ‘ โ†’ (๐ต โˆ’ (๐ต โˆ’ ๐ด)) = ๐ด)
162157, 159, 1613eqtrd 2777 . . . . . . 7 (๐œ‘ โ†’ ((๐ธโ€˜๐‘‹) โˆ’ ๐‘‡) = ๐ด)
163162oveq1d 7424 . . . . . 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 5149   โ†ฆ cmpt 5232  โ€˜cfv 6544  (class class class)co 7409  โ„cr 11109  0cc0 11110  1c1 11111   + caddc 11113   ยท cmul 11115  โ„*cxr 11247   < clt 11248   โ‰ค cle 11249   โˆ’ cmin 11444  -cneg 11445   / cdiv 11871  โ„คcz 12558  (,]cioc 13325  โŒŠcfl 13755
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 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188
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 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-sup 9437  df-inf 9438  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-n0 12473  df-z 12559  df-uz 12823  df-rp 12975  df-ioc 13329  df-fl 13757
This theorem is referenced by:  fourierdlem65  44887  fourierdlem79  44901
  Copyright terms: Public domain W3C validator