Metamath Proof Explorer


Theorem fourierdlem19

Description: If two elements of D have the same periodic image in ( A (,] B ) then they are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem19.a ( 𝜑𝐴 ∈ ℝ )
fourierdlem19.b ( 𝜑𝐵 ∈ ℝ )
fourierdlem19.altb ( 𝜑𝐴 < 𝐵 )
fourierdlem19.x ( 𝜑𝑋 ∈ ℝ )
fourierdlem19.d 𝐷 = { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 }
fourierdlem19.t 𝑇 = ( 𝐵𝐴 )
fourierdlem19.e 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
fourierdlem19.w ( 𝜑𝑊𝐷 )
fourierdlem19.z ( 𝜑𝑍𝐷 )
fourierdlem19.ezew ( 𝜑 → ( 𝐸𝑍 ) = ( 𝐸𝑊 ) )
Assertion fourierdlem19 ( 𝜑 → ¬ 𝑊 < 𝑍 )

Proof

Step Hyp Ref Expression
1 fourierdlem19.a ( 𝜑𝐴 ∈ ℝ )
2 fourierdlem19.b ( 𝜑𝐵 ∈ ℝ )
3 fourierdlem19.altb ( 𝜑𝐴 < 𝐵 )
4 fourierdlem19.x ( 𝜑𝑋 ∈ ℝ )
5 fourierdlem19.d 𝐷 = { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 }
6 fourierdlem19.t 𝑇 = ( 𝐵𝐴 )
7 fourierdlem19.e 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
8 fourierdlem19.w ( 𝜑𝑊𝐷 )
9 fourierdlem19.z ( 𝜑𝑍𝐷 )
10 fourierdlem19.ezew ( 𝜑 → ( 𝐸𝑍 ) = ( 𝐸𝑊 ) )
11 1 4 readdcld ( 𝜑 → ( 𝐴 + 𝑋 ) ∈ ℝ )
12 11 rexrd ( 𝜑 → ( 𝐴 + 𝑋 ) ∈ ℝ* )
13 2 4 readdcld ( 𝜑 → ( 𝐵 + 𝑋 ) ∈ ℝ )
14 13 rexrd ( 𝜑 → ( 𝐵 + 𝑋 ) ∈ ℝ* )
15 ssrab2 { 𝑦 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ 𝐶 } ⊆ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) )
16 5 15 eqsstri 𝐷 ⊆ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) )
17 16 9 sseldi ( 𝜑𝑍 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) )
18 iocleub ( ( ( 𝐴 + 𝑋 ) ∈ ℝ* ∧ ( 𝐵 + 𝑋 ) ∈ ℝ*𝑍 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ) → 𝑍 ≤ ( 𝐵 + 𝑋 ) )
19 12 14 17 18 syl3anc ( 𝜑𝑍 ≤ ( 𝐵 + 𝑋 ) )
20 19 adantr ( ( 𝜑𝑊 < 𝑍 ) → 𝑍 ≤ ( 𝐵 + 𝑋 ) )
21 13 adantr ( ( 𝜑𝑊 < 𝑍 ) → ( 𝐵 + 𝑋 ) ∈ ℝ )
22 iocssre ( ( ( 𝐴 + 𝑋 ) ∈ ℝ* ∧ ( 𝐵 + 𝑋 ) ∈ ℝ ) → ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ⊆ ℝ )
23 12 13 22 syl2anc ( 𝜑 → ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ⊆ ℝ )
24 16 8 sseldi ( 𝜑𝑊 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) )
25 23 24 sseldd ( 𝜑𝑊 ∈ ℝ )
26 2 1 resubcld ( 𝜑 → ( 𝐵𝐴 ) ∈ ℝ )
27 6 26 eqeltrid ( 𝜑𝑇 ∈ ℝ )
28 25 27 readdcld ( 𝜑 → ( 𝑊 + 𝑇 ) ∈ ℝ )
29 28 adantr ( ( 𝜑𝑊 < 𝑍 ) → ( 𝑊 + 𝑇 ) ∈ ℝ )
30 23 17 sseldd ( 𝜑𝑍 ∈ ℝ )
31 30 adantr ( ( 𝜑𝑊 < 𝑍 ) → 𝑍 ∈ ℝ )
32 6 eqcomi ( 𝐵𝐴 ) = 𝑇
33 32 a1i ( 𝜑 → ( 𝐵𝐴 ) = 𝑇 )
34 2 recnd ( 𝜑𝐵 ∈ ℂ )
35 1 recnd ( 𝜑𝐴 ∈ ℂ )
36 27 recnd ( 𝜑𝑇 ∈ ℂ )
37 34 35 36 subaddd ( 𝜑 → ( ( 𝐵𝐴 ) = 𝑇 ↔ ( 𝐴 + 𝑇 ) = 𝐵 ) )
38 33 37 mpbid ( 𝜑 → ( 𝐴 + 𝑇 ) = 𝐵 )
39 38 eqcomd ( 𝜑𝐵 = ( 𝐴 + 𝑇 ) )
40 39 oveq1d ( 𝜑 → ( 𝐵 + 𝑋 ) = ( ( 𝐴 + 𝑇 ) + 𝑋 ) )
41 4 recnd ( 𝜑𝑋 ∈ ℂ )
42 35 36 41 add32d ( 𝜑 → ( ( 𝐴 + 𝑇 ) + 𝑋 ) = ( ( 𝐴 + 𝑋 ) + 𝑇 ) )
43 40 42 eqtrd ( 𝜑 → ( 𝐵 + 𝑋 ) = ( ( 𝐴 + 𝑋 ) + 𝑇 ) )
44 iocgtlb ( ( ( 𝐴 + 𝑋 ) ∈ ℝ* ∧ ( 𝐵 + 𝑋 ) ∈ ℝ*𝑊 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ) → ( 𝐴 + 𝑋 ) < 𝑊 )
45 12 14 24 44 syl3anc ( 𝜑 → ( 𝐴 + 𝑋 ) < 𝑊 )
46 11 25 27 45 ltadd1dd ( 𝜑 → ( ( 𝐴 + 𝑋 ) + 𝑇 ) < ( 𝑊 + 𝑇 ) )
47 43 46 eqbrtrd ( 𝜑 → ( 𝐵 + 𝑋 ) < ( 𝑊 + 𝑇 ) )
48 47 adantr ( ( 𝜑𝑊 < 𝑍 ) → ( 𝐵 + 𝑋 ) < ( 𝑊 + 𝑇 ) )
49 7 a1i ( 𝜑𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) )
50 id ( 𝑥 = 𝑊𝑥 = 𝑊 )
51 oveq2 ( 𝑥 = 𝑊 → ( 𝐵𝑥 ) = ( 𝐵𝑊 ) )
52 51 oveq1d ( 𝑥 = 𝑊 → ( ( 𝐵𝑥 ) / 𝑇 ) = ( ( 𝐵𝑊 ) / 𝑇 ) )
53 52 fveq2d ( 𝑥 = 𝑊 → ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) )
54 53 oveq1d ( 𝑥 = 𝑊 → ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) )
55 50 54 oveq12d ( 𝑥 = 𝑊 → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑊 + ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ) )
56 55 adantl ( ( 𝜑𝑥 = 𝑊 ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑊 + ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ) )
57 2 25 resubcld ( 𝜑 → ( 𝐵𝑊 ) ∈ ℝ )
58 1 2 posdifd ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵𝐴 ) ) )
59 3 58 mpbid ( 𝜑 → 0 < ( 𝐵𝐴 ) )
60 59 6 breqtrrdi ( 𝜑 → 0 < 𝑇 )
61 60 gt0ne0d ( 𝜑𝑇 ≠ 0 )
62 57 27 61 redivcld ( 𝜑 → ( ( 𝐵𝑊 ) / 𝑇 ) ∈ ℝ )
63 62 flcld ( 𝜑 → ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) ∈ ℤ )
64 63 zred ( 𝜑 → ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) ∈ ℝ )
65 64 27 remulcld ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
66 25 65 readdcld ( 𝜑 → ( 𝑊 + ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
67 49 56 25 66 fvmptd ( 𝜑 → ( 𝐸𝑊 ) = ( 𝑊 + ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ) )
68 67 66 eqeltrd ( 𝜑 → ( 𝐸𝑊 ) ∈ ℝ )
69 68 recnd ( 𝜑 → ( 𝐸𝑊 ) ∈ ℂ )
70 69 adantr ( ( 𝜑𝑊 < 𝑍 ) → ( 𝐸𝑊 ) ∈ ℂ )
71 65 recnd ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ∈ ℂ )
72 71 adantr ( ( 𝜑𝑊 < 𝑍 ) → ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ∈ ℂ )
73 36 adantr ( ( 𝜑𝑊 < 𝑍 ) → 𝑇 ∈ ℂ )
74 70 72 73 subsubd ( ( 𝜑𝑊 < 𝑍 ) → ( ( 𝐸𝑊 ) − ( ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) − 𝑇 ) ) = ( ( ( 𝐸𝑊 ) − ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ) + 𝑇 ) )
75 74 eqcomd ( ( 𝜑𝑊 < 𝑍 ) → ( ( ( 𝐸𝑊 ) − ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ) + 𝑇 ) = ( ( 𝐸𝑊 ) − ( ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) − 𝑇 ) ) )
76 2 30 resubcld ( 𝜑 → ( 𝐵𝑍 ) ∈ ℝ )
77 76 27 61 redivcld ( 𝜑 → ( ( 𝐵𝑍 ) / 𝑇 ) ∈ ℝ )
78 77 flcld ( 𝜑 → ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) ∈ ℤ )
79 78 zred ( 𝜑 → ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) ∈ ℝ )
80 79 adantr ( ( 𝜑𝑊 < 𝑍 ) → ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) ∈ ℝ )
81 27 adantr ( ( 𝜑𝑊 < 𝑍 ) → 𝑇 ∈ ℝ )
82 80 81 remulcld ( ( 𝜑𝑊 < 𝑍 ) → ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
83 64 adantr ( ( 𝜑𝑊 < 𝑍 ) → ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) ∈ ℝ )
84 83 81 remulcld ( ( 𝜑𝑊 < 𝑍 ) → ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
85 84 81 resubcld ( ( 𝜑𝑊 < 𝑍 ) → ( ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) − 𝑇 ) ∈ ℝ )
86 68 adantr ( ( 𝜑𝑊 < 𝑍 ) → ( 𝐸𝑊 ) ∈ ℝ )
87 79 27 remulcld ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
88 87 recnd ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) ∈ ℂ )
89 88 36 pncand ( 𝜑 → ( ( ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) + 𝑇 ) − 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) )
90 89 eqcomd ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) = ( ( ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) + 𝑇 ) − 𝑇 ) )
91 90 adantr ( ( 𝜑𝑊 < 𝑍 ) → ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) = ( ( ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) + 𝑇 ) − 𝑇 ) )
92 82 81 readdcld ( ( 𝜑𝑊 < 𝑍 ) → ( ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) + 𝑇 ) ∈ ℝ )
93 79 recnd ( 𝜑 → ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) ∈ ℂ )
94 93 36 adddirp1d ( 𝜑 → ( ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) + 1 ) · 𝑇 ) = ( ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) + 𝑇 ) )
95 94 eqcomd ( 𝜑 → ( ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) + 𝑇 ) = ( ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) + 1 ) · 𝑇 ) )
96 95 adantr ( ( 𝜑𝑊 < 𝑍 ) → ( ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) + 𝑇 ) = ( ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) + 1 ) · 𝑇 ) )
97 1red ( ( 𝜑𝑊 < 𝑍 ) → 1 ∈ ℝ )
98 80 97 readdcld ( ( 𝜑𝑊 < 𝑍 ) → ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) + 1 ) ∈ ℝ )
99 0red ( 𝜑 → 0 ∈ ℝ )
100 99 27 60 ltled ( 𝜑 → 0 ≤ 𝑇 )
101 100 adantr ( ( 𝜑𝑊 < 𝑍 ) → 0 ≤ 𝑇 )
102 86 31 resubcld ( ( 𝜑𝑊 < 𝑍 ) → ( ( 𝐸𝑊 ) − 𝑍 ) ∈ ℝ )
103 25 adantr ( ( 𝜑𝑊 < 𝑍 ) → 𝑊 ∈ ℝ )
104 86 103 resubcld ( ( 𝜑𝑊 < 𝑍 ) → ( ( 𝐸𝑊 ) − 𝑊 ) ∈ ℝ )
105 27 60 elrpd ( 𝜑𝑇 ∈ ℝ+ )
106 105 adantr ( ( 𝜑𝑊 < 𝑍 ) → 𝑇 ∈ ℝ+ )
107 simpr ( ( 𝜑𝑊 < 𝑍 ) → 𝑊 < 𝑍 )
108 103 31 86 107 ltsub2dd ( ( 𝜑𝑊 < 𝑍 ) → ( ( 𝐸𝑊 ) − 𝑍 ) < ( ( 𝐸𝑊 ) − 𝑊 ) )
109 102 104 106 108 ltdiv1dd ( ( 𝜑𝑊 < 𝑍 ) → ( ( ( 𝐸𝑊 ) − 𝑍 ) / 𝑇 ) < ( ( ( 𝐸𝑊 ) − 𝑊 ) / 𝑇 ) )
110 id ( 𝑥 = 𝑍𝑥 = 𝑍 )
111 oveq2 ( 𝑥 = 𝑍 → ( 𝐵𝑥 ) = ( 𝐵𝑍 ) )
112 111 oveq1d ( 𝑥 = 𝑍 → ( ( 𝐵𝑥 ) / 𝑇 ) = ( ( 𝐵𝑍 ) / 𝑇 ) )
113 112 fveq2d ( 𝑥 = 𝑍 → ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) )
114 113 oveq1d ( 𝑥 = 𝑍 → ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) )
115 110 114 oveq12d ( 𝑥 = 𝑍 → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑍 + ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) ) )
116 115 adantl ( ( 𝜑𝑥 = 𝑍 ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑍 + ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) ) )
117 30 87 readdcld ( 𝜑 → ( 𝑍 + ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
118 49 116 30 117 fvmptd ( 𝜑 → ( 𝐸𝑍 ) = ( 𝑍 + ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) ) )
119 10 118 eqtr3d ( 𝜑 → ( 𝐸𝑊 ) = ( 𝑍 + ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) ) )
120 119 oveq1d ( 𝜑 → ( ( 𝐸𝑊 ) − 𝑍 ) = ( ( 𝑍 + ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑍 ) )
121 30 recnd ( 𝜑𝑍 ∈ ℂ )
122 121 88 pncan2d ( 𝜑 → ( ( 𝑍 + ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑍 ) = ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) )
123 120 122 eqtrd ( 𝜑 → ( ( 𝐸𝑊 ) − 𝑍 ) = ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) )
124 123 oveq1d ( 𝜑 → ( ( ( 𝐸𝑊 ) − 𝑍 ) / 𝑇 ) = ( ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) / 𝑇 ) )
125 93 36 61 divcan4d ( 𝜑 → ( ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) / 𝑇 ) = ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) )
126 124 125 eqtr2d ( 𝜑 → ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) = ( ( ( 𝐸𝑊 ) − 𝑍 ) / 𝑇 ) )
127 126 adantr ( ( 𝜑𝑊 < 𝑍 ) → ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) = ( ( ( 𝐸𝑊 ) − 𝑍 ) / 𝑇 ) )
128 67 oveq1d ( 𝜑 → ( ( 𝐸𝑊 ) − 𝑊 ) = ( ( 𝑊 + ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑊 ) )
129 128 oveq1d ( 𝜑 → ( ( ( 𝐸𝑊 ) − 𝑊 ) / 𝑇 ) = ( ( ( 𝑊 + ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑊 ) / 𝑇 ) )
130 25 recnd ( 𝜑𝑊 ∈ ℂ )
131 130 71 pncan2d ( 𝜑 → ( ( 𝑊 + ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑊 ) = ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) )
132 131 oveq1d ( 𝜑 → ( ( ( 𝑊 + ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑊 ) / 𝑇 ) = ( ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) / 𝑇 ) )
133 64 recnd ( 𝜑 → ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) ∈ ℂ )
134 133 36 61 divcan4d ( 𝜑 → ( ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) / 𝑇 ) = ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) )
135 129 132 134 3eqtrrd ( 𝜑 → ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) = ( ( ( 𝐸𝑊 ) − 𝑊 ) / 𝑇 ) )
136 135 adantr ( ( 𝜑𝑊 < 𝑍 ) → ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) = ( ( ( 𝐸𝑊 ) − 𝑊 ) / 𝑇 ) )
137 109 127 136 3brtr4d ( ( 𝜑𝑊 < 𝑍 ) → ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) < ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) )
138 78 adantr ( ( 𝜑𝑊 < 𝑍 ) → ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) ∈ ℤ )
139 63 adantr ( ( 𝜑𝑊 < 𝑍 ) → ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) ∈ ℤ )
140 zltp1le ( ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) ∈ ℤ ∧ ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) ∈ ℤ ) → ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) < ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) ↔ ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) + 1 ) ≤ ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) ) )
141 138 139 140 syl2anc ( ( 𝜑𝑊 < 𝑍 ) → ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) < ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) ↔ ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) + 1 ) ≤ ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) ) )
142 137 141 mpbid ( ( 𝜑𝑊 < 𝑍 ) → ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) + 1 ) ≤ ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) )
143 98 83 81 101 142 lemul1ad ( ( 𝜑𝑊 < 𝑍 ) → ( ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) + 1 ) · 𝑇 ) ≤ ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) )
144 96 143 eqbrtrd ( ( 𝜑𝑊 < 𝑍 ) → ( ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) + 𝑇 ) ≤ ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) )
145 92 84 81 144 lesub1dd ( ( 𝜑𝑊 < 𝑍 ) → ( ( ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) + 𝑇 ) − 𝑇 ) ≤ ( ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) − 𝑇 ) )
146 91 145 eqbrtrd ( ( 𝜑𝑊 < 𝑍 ) → ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) ≤ ( ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) − 𝑇 ) )
147 82 85 86 146 lesub2dd ( ( 𝜑𝑊 < 𝑍 ) → ( ( 𝐸𝑊 ) − ( ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) − 𝑇 ) ) ≤ ( ( 𝐸𝑊 ) − ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) ) )
148 75 147 eqbrtrd ( ( 𝜑𝑊 < 𝑍 ) → ( ( ( 𝐸𝑊 ) − ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ) + 𝑇 ) ≤ ( ( 𝐸𝑊 ) − ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) ) )
149 67 eqcomd ( 𝜑 → ( 𝑊 + ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝐸𝑊 ) )
150 69 71 130 subadd2d ( 𝜑 → ( ( ( 𝐸𝑊 ) − ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ) = 𝑊 ↔ ( 𝑊 + ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝐸𝑊 ) ) )
151 149 150 mpbird ( 𝜑 → ( ( 𝐸𝑊 ) − ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ) = 𝑊 )
152 151 eqcomd ( 𝜑𝑊 = ( ( 𝐸𝑊 ) − ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ) )
153 152 oveq1d ( 𝜑 → ( 𝑊 + 𝑇 ) = ( ( ( 𝐸𝑊 ) − ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ) + 𝑇 ) )
154 153 adantr ( ( 𝜑𝑊 < 𝑍 ) → ( 𝑊 + 𝑇 ) = ( ( ( 𝐸𝑊 ) − ( ( ⌊ ‘ ( ( 𝐵𝑊 ) / 𝑇 ) ) · 𝑇 ) ) + 𝑇 ) )
155 118 eqcomd ( 𝜑 → ( 𝑍 + ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝐸𝑍 ) )
156 1 rexrd ( 𝜑𝐴 ∈ ℝ* )
157 iocssre ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ) → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
158 156 2 157 syl2anc ( 𝜑 → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
159 1 2 3 6 7 fourierdlem4 ( 𝜑𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )
160 159 30 ffvelrnd ( 𝜑 → ( 𝐸𝑍 ) ∈ ( 𝐴 (,] 𝐵 ) )
161 158 160 sseldd ( 𝜑 → ( 𝐸𝑍 ) ∈ ℝ )
162 161 recnd ( 𝜑 → ( 𝐸𝑍 ) ∈ ℂ )
163 162 88 121 subadd2d ( 𝜑 → ( ( ( 𝐸𝑍 ) − ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) ) = 𝑍 ↔ ( 𝑍 + ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝐸𝑍 ) ) )
164 155 163 mpbird ( 𝜑 → ( ( 𝐸𝑍 ) − ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) ) = 𝑍 )
165 10 oveq1d ( 𝜑 → ( ( 𝐸𝑍 ) − ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝐸𝑊 ) − ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) ) )
166 164 165 eqtr3d ( 𝜑𝑍 = ( ( 𝐸𝑊 ) − ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) ) )
167 166 adantr ( ( 𝜑𝑊 < 𝑍 ) → 𝑍 = ( ( 𝐸𝑊 ) − ( ( ⌊ ‘ ( ( 𝐵𝑍 ) / 𝑇 ) ) · 𝑇 ) ) )
168 148 154 167 3brtr4d ( ( 𝜑𝑊 < 𝑍 ) → ( 𝑊 + 𝑇 ) ≤ 𝑍 )
169 21 29 31 48 168 ltletrd ( ( 𝜑𝑊 < 𝑍 ) → ( 𝐵 + 𝑋 ) < 𝑍 )
170 21 31 ltnled ( ( 𝜑𝑊 < 𝑍 ) → ( ( 𝐵 + 𝑋 ) < 𝑍 ↔ ¬ 𝑍 ≤ ( 𝐵 + 𝑋 ) ) )
171 169 170 mpbid ( ( 𝜑𝑊 < 𝑍 ) → ¬ 𝑍 ≤ ( 𝐵 + 𝑋 ) )
172 20 171 pm2.65da ( 𝜑 → ¬ 𝑊 < 𝑍 )