This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fourierdlem26

Description: Periodic image of a point Y that's in the period that begins with the point X . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem26.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem26.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem26.3 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
fourierdlem26.4 ⊢ 𝑇 = ( 𝐵 − 𝐴 )
fourierdlem26.5 ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
fourierdlem26.6 ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem26.7 ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) = 𝐵 )
fourierdlem26.8 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 (,] ( 𝑋 + 𝑇 ) ) )
Assertion fourierdlem26 ( 𝜑 → ( 𝐸 ‘ 𝑌 ) = ( 𝐴 + ( 𝑌 − 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem26.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 fourierdlem26.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 fourierdlem26.3 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
4 fourierdlem26.4 ⊢ 𝑇 = ( 𝐵 − 𝐴 )
5 fourierdlem26.5 ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
6 fourierdlem26.6 ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
7 fourierdlem26.7 ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) = 𝐵 )
8 fourierdlem26.8 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 (,] ( 𝑋 + 𝑇 ) ) )
9 5 a1i ⊢ ( 𝜑 → 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → 𝑥 = 𝑌 )
11 10 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ( 𝐵 − 𝑥 ) = ( 𝐵 − 𝑌 ) )
12 11 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ( ( 𝐵 − 𝑥 ) / 𝑇 ) = ( ( 𝐵 − 𝑌 ) / 𝑇 ) )
13 12 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) )
14 13 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) )
15 10 14 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑌 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ) )
16 6 rexrd ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
17 2 1 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
18 4 17 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
19 6 18 readdcld ⊢ ( 𝜑 → ( 𝑋 + 𝑇 ) ∈ ℝ )
20 elioc2 ⊢ ( ( 𝑋 ∈ ℝ* ∧ ( 𝑋 + 𝑇 ) ∈ ℝ ) → ( 𝑌 ∈ ( 𝑋 (,] ( 𝑋 + 𝑇 ) ) ↔ ( 𝑌 ∈ ℝ ∧ 𝑋 < 𝑌 ∧ 𝑌 ≤ ( 𝑋 + 𝑇 ) ) ) )
21 16 19 20 syl2anc ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑋 (,] ( 𝑋 + 𝑇 ) ) ↔ ( 𝑌 ∈ ℝ ∧ 𝑋 < 𝑌 ∧ 𝑌 ≤ ( 𝑋 + 𝑇 ) ) ) )
22 8 21 mpbid ⊢ ( 𝜑 → ( 𝑌 ∈ ℝ ∧ 𝑋 < 𝑌 ∧ 𝑌 ≤ ( 𝑋 + 𝑇 ) ) )
23 22 simp1d ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
24 2 23 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝑌 ) ∈ ℝ )
25 1 2 posdifd ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
26 3 25 mpbid ⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
27 26 4 breqtrrdi ⊢ ( 𝜑 → 0 < 𝑇 )
28 27 gt0ne0d ⊢ ( 𝜑 → 𝑇 ≠ 0 )
29 24 18 28 redivcld ⊢ ( 𝜑 → ( ( 𝐵 − 𝑌 ) / 𝑇 ) ∈ ℝ )
30 29 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) ∈ ℤ )
31 30 zred ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) ∈ ℝ )
32 31 18 remulcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
33 23 32 readdcld ⊢ ( 𝜑 → ( 𝑌 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
34 9 15 23 33 fvmptd ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑌 ) = ( 𝑌 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ) )
35 6 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
36 23 recnd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
37 35 36 pncan3d ⊢ ( 𝜑 → ( 𝑋 + ( 𝑌 − 𝑋 ) ) = 𝑌 )
38 37 eqcomd ⊢ ( 𝜑 → 𝑌 = ( 𝑋 + ( 𝑌 − 𝑋 ) ) )
39 38 oveq2d ⊢ ( 𝜑 → ( 𝐵 − 𝑌 ) = ( 𝐵 − ( 𝑋 + ( 𝑌 − 𝑋 ) ) ) )
40 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
41 36 35 subcld ⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) ∈ ℂ )
42 40 35 41 subsub4d ⊢ ( 𝜑 → ( ( 𝐵 − 𝑋 ) − ( 𝑌 − 𝑋 ) ) = ( 𝐵 − ( 𝑋 + ( 𝑌 − 𝑋 ) ) ) )
43 39 42 eqtr4d ⊢ ( 𝜑 → ( 𝐵 − 𝑌 ) = ( ( 𝐵 − 𝑋 ) − ( 𝑌 − 𝑋 ) ) )
44 43 oveq1d ⊢ ( 𝜑 → ( ( 𝐵 − 𝑌 ) / 𝑇 ) = ( ( ( 𝐵 − 𝑋 ) − ( 𝑌 − 𝑋 ) ) / 𝑇 ) )
45 2 6 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) ∈ ℝ )
46 45 recnd ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) ∈ ℂ )
47 18 recnd ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
48 46 41 47 28 divsubdird ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑋 ) − ( 𝑌 − 𝑋 ) ) / 𝑇 ) = ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − ( ( 𝑌 − 𝑋 ) / 𝑇 ) ) )
49 41 47 28 divnegd ⊢ ( 𝜑 → - ( ( 𝑌 − 𝑋 ) / 𝑇 ) = ( - ( 𝑌 − 𝑋 ) / 𝑇 ) )
50 36 35 negsubdi2d ⊢ ( 𝜑 → - ( 𝑌 − 𝑋 ) = ( 𝑋 − 𝑌 ) )
51 50 oveq1d ⊢ ( 𝜑 → ( - ( 𝑌 − 𝑋 ) / 𝑇 ) = ( ( 𝑋 − 𝑌 ) / 𝑇 ) )
52 49 51 eqtrd ⊢ ( 𝜑 → - ( ( 𝑌 − 𝑋 ) / 𝑇 ) = ( ( 𝑋 − 𝑌 ) / 𝑇 ) )
53 52 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) + - ( ( 𝑌 − 𝑋 ) / 𝑇 ) ) = ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) )
54 45 18 28 redivcld ⊢ ( 𝜑 → ( ( 𝐵 − 𝑋 ) / 𝑇 ) ∈ ℝ )
55 54 recnd ⊢ ( 𝜑 → ( ( 𝐵 − 𝑋 ) / 𝑇 ) ∈ ℂ )
56 41 47 28 divcld ⊢ ( 𝜑 → ( ( 𝑌 − 𝑋 ) / 𝑇 ) ∈ ℂ )
57 55 56 negsubd ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) + - ( ( 𝑌 − 𝑋 ) / 𝑇 ) ) = ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − ( ( 𝑌 − 𝑋 ) / 𝑇 ) ) )
58 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
59 55 58 npcand ⊢ ( 𝜑 → ( ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − 1 ) + 1 ) = ( ( 𝐵 − 𝑋 ) / 𝑇 ) )
60 59 eqcomd ⊢ ( 𝜑 → ( ( 𝐵 − 𝑋 ) / 𝑇 ) = ( ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − 1 ) + 1 ) )
61 60 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) = ( ( ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − 1 ) + 1 ) + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) )
62 55 58 subcld ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − 1 ) ∈ ℂ )
63 35 36 subcld ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) ∈ ℂ )
64 63 47 28 divcld ⊢ ( 𝜑 → ( ( 𝑋 − 𝑌 ) / 𝑇 ) ∈ ℂ )
65 62 58 64 addassd ⊢ ( 𝜑 → ( ( ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − 1 ) + 1 ) + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) = ( ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − 1 ) + ( 1 + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) ) )
66 61 65 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) = ( ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − 1 ) + ( 1 + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) ) )
67 53 57 66 3eqtr3d ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − ( ( 𝑌 − 𝑋 ) / 𝑇 ) ) = ( ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − 1 ) + ( 1 + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) ) )
68 44 48 67 3eqtrd ⊢ ( 𝜑 → ( ( 𝐵 − 𝑌 ) / 𝑇 ) = ( ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − 1 ) + ( 1 + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) ) )
69 68 fveq2d ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − 1 ) + ( 1 + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) ) ) )
70 6 23 resubcld ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) ∈ ℝ )
71 18 70 readdcld ⊢ ( 𝜑 → ( 𝑇 + ( 𝑋 − 𝑌 ) ) ∈ ℝ )
72 18 27 elrpd ⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
73 35 47 addcomd ⊢ ( 𝜑 → ( 𝑋 + 𝑇 ) = ( 𝑇 + 𝑋 ) )
74 73 oveq2d ⊢ ( 𝜑 → ( 𝑋 (,] ( 𝑋 + 𝑇 ) ) = ( 𝑋 (,] ( 𝑇 + 𝑋 ) ) )
75 8 74 eleqtrd ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 (,] ( 𝑇 + 𝑋 ) ) )
76 18 6 readdcld ⊢ ( 𝜑 → ( 𝑇 + 𝑋 ) ∈ ℝ )
77 elioc2 ⊢ ( ( 𝑋 ∈ ℝ* ∧ ( 𝑇 + 𝑋 ) ∈ ℝ ) → ( 𝑌 ∈ ( 𝑋 (,] ( 𝑇 + 𝑋 ) ) ↔ ( 𝑌 ∈ ℝ ∧ 𝑋 < 𝑌 ∧ 𝑌 ≤ ( 𝑇 + 𝑋 ) ) ) )
78 16 76 77 syl2anc ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑋 (,] ( 𝑇 + 𝑋 ) ) ↔ ( 𝑌 ∈ ℝ ∧ 𝑋 < 𝑌 ∧ 𝑌 ≤ ( 𝑇 + 𝑋 ) ) ) )
79 75 78 mpbid ⊢ ( 𝜑 → ( 𝑌 ∈ ℝ ∧ 𝑋 < 𝑌 ∧ 𝑌 ≤ ( 𝑇 + 𝑋 ) ) )
80 79 simp3d ⊢ ( 𝜑 → 𝑌 ≤ ( 𝑇 + 𝑋 ) )
81 23 6 18 lesubaddd ⊢ ( 𝜑 → ( ( 𝑌 − 𝑋 ) ≤ 𝑇 ↔ 𝑌 ≤ ( 𝑇 + 𝑋 ) ) )
82 80 81 mpbird ⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) ≤ 𝑇 )
83 23 6 resubcld ⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) ∈ ℝ )
84 18 83 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( 𝑇 − ( 𝑌 − 𝑋 ) ) ↔ ( 𝑌 − 𝑋 ) ≤ 𝑇 ) )
85 82 84 mpbird ⊢ ( 𝜑 → 0 ≤ ( 𝑇 − ( 𝑌 − 𝑋 ) ) )
86 47 36 35 subsub2d ⊢ ( 𝜑 → ( 𝑇 − ( 𝑌 − 𝑋 ) ) = ( 𝑇 + ( 𝑋 − 𝑌 ) ) )
87 85 86 breqtrd ⊢ ( 𝜑 → 0 ≤ ( 𝑇 + ( 𝑋 − 𝑌 ) ) )
88 71 72 87 divge0d ⊢ ( 𝜑 → 0 ≤ ( ( 𝑇 + ( 𝑋 − 𝑌 ) ) / 𝑇 ) )
89 47 63 47 28 divdird ⊢ ( 𝜑 → ( ( 𝑇 + ( 𝑋 − 𝑌 ) ) / 𝑇 ) = ( ( 𝑇 / 𝑇 ) + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) )
90 47 28 dividd ⊢ ( 𝜑 → ( 𝑇 / 𝑇 ) = 1 )
91 90 eqcomd ⊢ ( 𝜑 → 1 = ( 𝑇 / 𝑇 ) )
92 91 oveq1d ⊢ ( 𝜑 → ( 1 + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) = ( ( 𝑇 / 𝑇 ) + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) )
93 89 92 eqtr4d ⊢ ( 𝜑 → ( ( 𝑇 + ( 𝑋 − 𝑌 ) ) / 𝑇 ) = ( 1 + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) )
94 88 93 breqtrd ⊢ ( 𝜑 → 0 ≤ ( 1 + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) )
95 22 simp2d ⊢ ( 𝜑 → 𝑋 < 𝑌 )
96 6 23 sublt0d ⊢ ( 𝜑 → ( ( 𝑋 − 𝑌 ) < 0 ↔ 𝑋 < 𝑌 ) )
97 95 96 mpbird ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) < 0 )
98 70 72 97 divlt0gt0d ⊢ ( 𝜑 → ( ( 𝑋 − 𝑌 ) / 𝑇 ) < 0 )
99 70 18 28 redivcld ⊢ ( 𝜑 → ( ( 𝑋 − 𝑌 ) / 𝑇 ) ∈ ℝ )
100 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
101 ltaddneg ⊢ ( ( ( ( 𝑋 − 𝑌 ) / 𝑇 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( ( 𝑋 − 𝑌 ) / 𝑇 ) < 0 ↔ ( 1 + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) < 1 ) )
102 99 100 101 syl2anc ⊢ ( 𝜑 → ( ( ( 𝑋 − 𝑌 ) / 𝑇 ) < 0 ↔ ( 1 + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) < 1 ) )
103 98 102 mpbid ⊢ ( 𝜑 → ( 1 + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) < 1 )
104 54 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) ∈ ℤ )
105 104 zcnd ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) ∈ ℂ )
106 105 47 mulcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ∈ ℂ )
107 35 106 pncan2d ⊢ ( 𝜑 → ( ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑋 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) )
108 107 eqcomd ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) = ( ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑋 ) )
109 108 oveq1d ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) / 𝑇 ) = ( ( ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑋 ) / 𝑇 ) )
110 105 47 28 divcan4d ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) / 𝑇 ) = ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) )
111 id ⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
112 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐵 − 𝑥 ) = ( 𝐵 − 𝑋 ) )
113 112 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐵 − 𝑥 ) / 𝑇 ) = ( ( 𝐵 − 𝑋 ) / 𝑇 ) )
114 113 fveq2d ⊢ ( 𝑥 = 𝑋 → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) )
115 114 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) )
116 111 115 oveq12d ⊢ ( 𝑥 = 𝑋 → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
117 116 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
118 reflcl ⊢ ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) ∈ ℝ → ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) ∈ ℝ )
119 54 118 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) ∈ ℝ )
120 119 18 remulcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
121 6 120 readdcld ⊢ ( 𝜑 → ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
122 9 117 6 121 fvmptd ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) = ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
123 122 eqcomd ⊢ ( 𝜑 → ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝐸 ‘ 𝑋 ) )
124 123 oveq1d ⊢ ( 𝜑 → ( ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑋 ) = ( ( 𝐸 ‘ 𝑋 ) − 𝑋 ) )
125 124 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑋 ) / 𝑇 ) = ( ( ( 𝐸 ‘ 𝑋 ) − 𝑋 ) / 𝑇 ) )
126 7 oveq1d ⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑋 ) − 𝑋 ) = ( 𝐵 − 𝑋 ) )
127 126 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ 𝑋 ) − 𝑋 ) / 𝑇 ) = ( ( 𝐵 − 𝑋 ) / 𝑇 ) )
128 125 127 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑋 ) / 𝑇 ) = ( ( 𝐵 − 𝑋 ) / 𝑇 ) )
129 109 110 128 3eqtr3d ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) = ( ( 𝐵 − 𝑋 ) / 𝑇 ) )
130 129 104 eqeltrrd ⊢ ( 𝜑 → ( ( 𝐵 − 𝑋 ) / 𝑇 ) ∈ ℤ )
131 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
132 130 131 zsubcld ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − 1 ) ∈ ℤ )
133 100 99 readdcld ⊢ ( 𝜑 → ( 1 + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) ∈ ℝ )
134 flbi2 ⊢ ( ( ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − 1 ) ∈ ℤ ∧ ( 1 + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) ∈ ℝ ) → ( ( ⌊ ‘ ( ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − 1 ) + ( 1 + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) ) ) = ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − 1 ) ↔ ( 0 ≤ ( 1 + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) ∧ ( 1 + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) < 1 ) ) )
135 132 133 134 syl2anc ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − 1 ) + ( 1 + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) ) ) = ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − 1 ) ↔ ( 0 ≤ ( 1 + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) ∧ ( 1 + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) < 1 ) ) )
136 94 103 135 mpbir2and ⊢ ( 𝜑 → ( ⌊ ‘ ( ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − 1 ) + ( 1 + ( ( 𝑋 − 𝑌 ) / 𝑇 ) ) ) ) = ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − 1 ) )
137 129 eqcomd ⊢ ( 𝜑 → ( ( 𝐵 − 𝑋 ) / 𝑇 ) = ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) )
138 137 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐵 − 𝑋 ) / 𝑇 ) − 1 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) − 1 ) )
139 69 136 138 3eqtrd ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) − 1 ) )
140 139 oveq1d ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) = ( ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) − 1 ) · 𝑇 ) )
141 140 oveq2d ⊢ ( 𝜑 → ( 𝑌 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑌 + ( ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) − 1 ) · 𝑇 ) ) )
142 38 oveq1d ⊢ ( 𝜑 → ( 𝑌 + ( ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) − 1 ) · 𝑇 ) ) = ( ( 𝑋 + ( 𝑌 − 𝑋 ) ) + ( ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) − 1 ) · 𝑇 ) ) )
143 105 58 47 subdird ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) − 1 ) · 𝑇 ) = ( ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) − ( 1 · 𝑇 ) ) )
144 143 oveq2d ⊢ ( 𝜑 → ( ( 𝑋 + ( 𝑌 − 𝑋 ) ) + ( ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) − 1 ) · 𝑇 ) ) = ( ( 𝑋 + ( 𝑌 − 𝑋 ) ) + ( ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) − ( 1 · 𝑇 ) ) ) )
145 35 41 addcld ⊢ ( 𝜑 → ( 𝑋 + ( 𝑌 − 𝑋 ) ) ∈ ℂ )
146 58 47 mulcld ⊢ ( 𝜑 → ( 1 · 𝑇 ) ∈ ℂ )
147 145 106 146 addsubassd ⊢ ( 𝜑 → ( ( ( 𝑋 + ( 𝑌 − 𝑋 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) − ( 1 · 𝑇 ) ) = ( ( 𝑋 + ( 𝑌 − 𝑋 ) ) + ( ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) − ( 1 · 𝑇 ) ) ) )
148 147 eqcomd ⊢ ( 𝜑 → ( ( 𝑋 + ( 𝑌 − 𝑋 ) ) + ( ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) − ( 1 · 𝑇 ) ) ) = ( ( ( 𝑋 + ( 𝑌 − 𝑋 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) − ( 1 · 𝑇 ) ) )
149 35 41 106 add32d ⊢ ( 𝜑 → ( ( 𝑋 + ( 𝑌 − 𝑋 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) + ( 𝑌 − 𝑋 ) ) )
150 149 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑋 + ( 𝑌 − 𝑋 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) − ( 1 · 𝑇 ) ) = ( ( ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) + ( 𝑌 − 𝑋 ) ) − ( 1 · 𝑇 ) ) )
151 123 oveq1d ⊢ ( 𝜑 → ( ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) + ( 𝑌 − 𝑋 ) ) = ( ( 𝐸 ‘ 𝑋 ) + ( 𝑌 − 𝑋 ) ) )
152 47 mullidd ⊢ ( 𝜑 → ( 1 · 𝑇 ) = 𝑇 )
153 151 152 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) + ( 𝑌 − 𝑋 ) ) − ( 1 · 𝑇 ) ) = ( ( ( 𝐸 ‘ 𝑋 ) + ( 𝑌 − 𝑋 ) ) − 𝑇 ) )
154 7 2 eqeltrd ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) ∈ ℝ )
155 154 recnd ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) ∈ ℂ )
156 155 41 47 addsubd ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ 𝑋 ) + ( 𝑌 − 𝑋 ) ) − 𝑇 ) = ( ( ( 𝐸 ‘ 𝑋 ) − 𝑇 ) + ( 𝑌 − 𝑋 ) ) )
157 7 oveq1d ⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑋 ) − 𝑇 ) = ( 𝐵 − 𝑇 ) )
158 4 a1i ⊢ ( 𝜑 → 𝑇 = ( 𝐵 − 𝐴 ) )
159 158 oveq2d ⊢ ( 𝜑 → ( 𝐵 − 𝑇 ) = ( 𝐵 − ( 𝐵 − 𝐴 ) ) )
160 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
161 40 160 nncand ⊢ ( 𝜑 → ( 𝐵 − ( 𝐵 − 𝐴 ) ) = 𝐴 )
162 157 159 161 3eqtrd ⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑋 ) − 𝑇 ) = 𝐴 )
163 162 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ 𝑋 ) − 𝑇 ) + ( 𝑌 − 𝑋 ) ) = ( 𝐴 + ( 𝑌 − 𝑋 ) ) )
164 156 163 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ 𝑋 ) + ( 𝑌 − 𝑋 ) ) − 𝑇 ) = ( 𝐴 + ( 𝑌 − 𝑋 ) ) )
165 150 153 164 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝑋 + ( 𝑌 − 𝑋 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) − ( 1 · 𝑇 ) ) = ( 𝐴 + ( 𝑌 − 𝑋 ) ) )
166 144 148 165 3eqtrd ⊢ ( 𝜑 → ( ( 𝑋 + ( 𝑌 − 𝑋 ) ) + ( ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) − 1 ) · 𝑇 ) ) = ( 𝐴 + ( 𝑌 − 𝑋 ) ) )
167 142 166 eqtrd ⊢ ( 𝜑 → ( 𝑌 + ( ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) − 1 ) · 𝑇 ) ) = ( 𝐴 + ( 𝑌 − 𝑋 ) ) )
168 34 141 167 3eqtrd ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑌 ) = ( 𝐴 + ( 𝑌 − 𝑋 ) ) )