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 sselid ⊢ ( 𝜑 → 𝑍 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) )
18 iocleub ⊢ ( ( ( 𝐴 + 𝑋 ) ∈ ℝ* ∧ ( 𝐵 + 𝑋 ) ∈ ℝ* ∧ 𝑍 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ) → 𝑍 ≤ ( 𝐵 + 𝑋 ) )
19 12 14 17 18 syl3anc ⊢ ( 𝜑 → 𝑍 ≤ ( 𝐵 + 𝑋 ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑊 < 𝑍 ) → 𝑍 ≤ ( 𝐵 + 𝑋 ) )
21 13 adantr ⊢ ( ( 𝜑 ∧ 𝑊 < 𝑍 ) → ( 𝐵 + 𝑋 ) ∈ ℝ )
22 iocssre ⊢ ( ( ( 𝐴 + 𝑋 ) ∈ ℝ* ∧ ( 𝐵 + 𝑋 ) ∈ ℝ ) → ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ⊆ ℝ )
23 12 13 22 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) ⊆ ℝ )
24 16 8 sselid ⊢ ( 𝜑 → 𝑊 ∈ ( ( 𝐴 + 𝑋 ) (,] ( 𝐵 + 𝑋 ) ) )
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 ⊢ ( 𝜑 → ¬ 𝑊 < 𝑍 )