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

Metamath Proof Explorer

Theorem fourierdlem65

Description: The distance of two adjacent points in the moved partition is preserved in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem65.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem65.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
fourierdlem65.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem65.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
fourierdlem65.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
fourierdlem65.d ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 (,) +∞ ) )
fourierdlem65.o ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem65.n ⊢ 𝑁 = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) − 1 )
fourierdlem65.s ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
fourierdlem65.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
fourierdlem65.l ⊢ 𝐿 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
fourierdlem65.z ⊢ 𝑍 = ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
Assertion fourierdlem65 ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem65.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
2 fourierdlem65.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
3 fourierdlem65.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4 fourierdlem65.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
5 fourierdlem65.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
6 fourierdlem65.d ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 (,) +∞ ) )
7 fourierdlem65.o ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
8 fourierdlem65.n ⊢ 𝑁 = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) − 1 )
9 fourierdlem65.s ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
10 fourierdlem65.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
11 fourierdlem65.l ⊢ 𝐿 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
12 fourierdlem65.z ⊢ 𝑍 = ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
13 11 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐿 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) ) )
14 simpr ⊢ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
15 simpl ⊢ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 )
16 14 15 eqtrd ⊢ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → 𝑦 = 𝐵 )
17 16 iftrued ⊢ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) = 𝐴 )
18 17 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) = 𝐴 )
19 1 3 4 fourierdlem11 ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) )
20 19 simp1d ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
21 19 simp2d ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
22 19 simp3d ⊢ ( 𝜑 → 𝐴 < 𝐵 )
23 20 21 22 2 10 fourierdlem4 ⊢ ( 𝜑 → 𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )
25 ioossre ⊢ ( 𝐶 (,) +∞ ) ⊆ ℝ
26 25 6 sselid ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
27 5 rexrd ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
28 pnfxr ⊢ +∞ ∈ ℝ*
29 28 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
30 ioogtlb ⊢ ( ( 𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐷 ∈ ( 𝐶 (,) +∞ ) ) → 𝐶 < 𝐷 )
31 27 29 6 30 syl3anc ⊢ ( 𝜑 → 𝐶 < 𝐷 )
32 id ⊢ ( 𝑦 = 𝑥 → 𝑦 = 𝑥 )
33 2 eqcomi ⊢ ( 𝐵 − 𝐴 ) = 𝑇
34 33 oveq2i ⊢ ( 𝑘 · ( 𝐵 − 𝐴 ) ) = ( 𝑘 · 𝑇 )
35 34 a1i ⊢ ( 𝑦 = 𝑥 → ( 𝑘 · ( 𝐵 − 𝐴 ) ) = ( 𝑘 · 𝑇 ) )
36 32 35 oveq12d ⊢ ( 𝑦 = 𝑥 → ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
37 36 eleq1d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
38 37 rexbidv ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
39 38 cbvrabv ⊢ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } = { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 }
40 39 uneq2i ⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
41 2 1 3 4 5 26 31 7 40 8 9 fourierdlem54 ⊢ ( 𝜑 → ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) ∧ 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) ) )
42 41 simpld ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) )
43 42 simprd ⊢ ( 𝜑 → 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) )
44 42 simpld ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
45 7 fourierdlem2 ⊢ ( 𝑁 ∈ ℕ → ( 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ↔ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
46 44 45 syl ⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ↔ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
47 43 46 mpbid ⊢ ( 𝜑 → ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) )
48 47 simpld ⊢ ( 𝜑 → 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) )
49 elmapi ⊢ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
50 48 49 syl ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
51 50 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
52 elfzofz ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
53 52 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
54 51 53 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
55 24 54 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
56 55 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
57 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐴 ∈ ℝ )
58 13 18 56 57 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = 𝐴 )
59 58 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − 𝐴 ) )
60 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐵 ∈ ℝ )
61 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐴 < 𝐵 )
62 54 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
63 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 )
64 fzofzp1 ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) )
65 64 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) )
66 51 65 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
67 66 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
68 elfzoelz ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → 𝑗 ∈ ℤ )
69 68 zred ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → 𝑗 ∈ ℝ )
70 69 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 ∈ ℝ )
71 70 ltp1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 < ( 𝑗 + 1 ) )
72 41 simprd ⊢ ( 𝜑 → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
73 72 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
74 isorel ⊢ ( ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) ∧ ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑗 < ( 𝑗 + 1 ) ↔ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
75 73 53 65 74 syl12anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑗 < ( 𝑗 + 1 ) ↔ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
76 71 75 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
77 76 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
78 isof1o ⊢ ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) → 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
79 f1ofo ⊢ ( 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) → 𝑆 : ( 0 ... 𝑁 ) –onto→ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
80 72 78 79 3syl ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) –onto→ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
81 80 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → 𝑆 : ( 0 ... 𝑁 ) –onto→ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
82 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → 𝐶 ∈ ℝ )
83 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → 𝐷 ∈ ℝ )
84 21 20 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
85 2 84 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
86 85 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑇 ∈ ℝ )
87 54 86 readdcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ℝ )
88 87 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ℝ )
89 5 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐶 ∈ ℝ )
90 7 44 43 fourierdlem15 ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ( 𝐶 [,] 𝐷 ) )
91 90 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑆 : ( 0 ... 𝑁 ) ⟶ ( 𝐶 [,] 𝐷 ) )
92 91 53 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐶 [,] 𝐷 ) )
93 26 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐷 ∈ ℝ )
94 elicc2 ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑆 ‘ 𝑗 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ 𝑗 ) ∧ ( 𝑆 ‘ 𝑗 ) ≤ 𝐷 ) ) )
95 89 93 94 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑆 ‘ 𝑗 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ 𝑗 ) ∧ ( 𝑆 ‘ 𝑗 ) ≤ 𝐷 ) ) )
96 92 95 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ 𝑗 ) ∧ ( 𝑆 ‘ 𝑗 ) ≤ 𝐷 ) )
97 96 simp2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐶 ≤ ( 𝑆 ‘ 𝑗 ) )
98 20 21 posdifd ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
99 22 98 mpbid ⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
100 99 2 breqtrrdi ⊢ ( 𝜑 → 0 < 𝑇 )
101 85 100 elrpd ⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
102 101 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑇 ∈ ℝ+ )
103 54 102 ltaddrpd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) < ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
104 89 54 87 97 103 lelttrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐶 < ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
105 89 87 104 ltled ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐶 ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
106 105 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → 𝐶 ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
107 66 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
108 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
109 88 107 ltnled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ↔ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) )
110 108 109 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
111 91 65 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( 𝐶 [,] 𝐷 ) )
112 elicc2 ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ 𝐷 ) ) )
113 89 93 112 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ 𝐷 ) ) )
114 111 113 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ 𝐷 ) )
115 114 simp3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ 𝐷 )
116 115 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ 𝐷 )
117 88 107 83 110 116 ltletrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) < 𝐷 )
118 88 83 117 ltled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ≤ 𝐷 )
119 82 83 88 106 118 eliccd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ( 𝐶 [,] 𝐷 ) )
120 119 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ( 𝐶 [,] 𝐷 ) )
121 10 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) )
122 id ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → 𝑥 = ( 𝑆 ‘ 𝑗 ) )
123 oveq2 ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → ( 𝐵 − 𝑥 ) = ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) )
124 123 oveq1d ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → ( ( 𝐵 − 𝑥 ) / 𝑇 ) = ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
125 124 fveq2d ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) )
126 125 oveq1d ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) )
127 122 126 oveq12d ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) )
128 127 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 = ( 𝑆 ‘ 𝑗 ) ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) )
129 21 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐵 ∈ ℝ )
130 129 54 resubcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ )
131 130 102 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∈ ℝ )
132 131 flcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) ∈ ℤ )
133 132 zred ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) ∈ ℝ )
134 133 86 remulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
135 54 134 readdcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
136 121 128 54 135 fvmptd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) )
137 136 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) = ( ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
138 137 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) = ( ( ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
139 54 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ℂ )
140 134 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ∈ ℂ )
141 139 140 pncan2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) − ( 𝑆 ‘ 𝑗 ) ) = ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) )
142 141 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) = ( ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) / 𝑇 ) )
143 133 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) ∈ ℂ )
144 86 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑇 ∈ ℂ )
145 102 rpne0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑇 ≠ 0 )
146 143 144 145 divcan4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) / 𝑇 ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) )
147 138 142 146 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) )
148 147 132 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∈ ℤ )
149 peano2zm ⊢ ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∈ ℤ → ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) ∈ ℤ )
150 148 149 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) ∈ ℤ )
151 150 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) ∈ ℤ )
152 33 oveq2i ⊢ ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · ( 𝐵 − 𝐴 ) ) = ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · 𝑇 )
153 152 oveq2i ⊢ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · ( 𝐵 − 𝐴 ) ) ) = ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · 𝑇 ) )
154 153 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · ( 𝐵 − 𝐴 ) ) ) = ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · 𝑇 ) ) )
155 136 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) )
156 oveq1 ⊢ ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 → ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) = ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) )
157 156 eqcomd ⊢ ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 → ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) = ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
158 157 oveq1d ⊢ ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 → ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) = ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
159 158 fveq2d ⊢ ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) = ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) )
160 159 oveq1d ⊢ ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) )
161 160 oveq2d ⊢ ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 → ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) )
162 161 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) )
163 147 143 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∈ ℂ )
164 1cnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 1 ∈ ℂ )
165 163 164 144 subdird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · 𝑇 ) = ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) − ( 1 · 𝑇 ) ) )
166 85 recnd ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
167 166 mullidd ⊢ ( 𝜑 → ( 1 · 𝑇 ) = 𝑇 )
168 167 oveq2d ⊢ ( 𝜑 → ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) − ( 1 · 𝑇 ) ) = ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) − 𝑇 ) )
169 168 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) − ( 1 · 𝑇 ) ) = ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) − 𝑇 ) )
170 165 169 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · 𝑇 ) = ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) − 𝑇 ) )
171 170 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · 𝑇 ) ) = ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) − 𝑇 ) ) )
172 163 144 mulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) ∈ ℂ )
173 139 144 172 ppncand ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) − 𝑇 ) ) = ( ( 𝑆 ‘ 𝑗 ) + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) ) )
174 flid ⊢ ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∈ ℤ → ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) = ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
175 148 174 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) = ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
176 175 eqcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) = ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) )
177 176 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) = ( ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) )
178 177 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) ) = ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) )
179 171 173 178 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) = ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · 𝑇 ) ) )
180 179 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) = ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · 𝑇 ) ) )
181 155 162 180 3eqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · 𝑇 ) ) = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
182 154 181 63 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · ( 𝐵 − 𝐴 ) ) ) = 𝐵 )
183 1 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
184 3 183 syl ⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
185 4 184 mpbid ⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
186 185 simprd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
187 186 simpld ⊢ ( 𝜑 → ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) )
188 187 simprd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = 𝐵 )
189 188 eqcomd ⊢ ( 𝜑 → 𝐵 = ( 𝑄 ‘ 𝑀 ) )
190 1 3 4 fourierdlem15 ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) )
191 ffn ⊢ ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) → 𝑄 Fn ( 0 ... 𝑀 ) )
192 190 191 syl ⊢ ( 𝜑 → 𝑄 Fn ( 0 ... 𝑀 ) )
193 3 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
194 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
195 193 194 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
196 eluzfz2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → 𝑀 ∈ ( 0 ... 𝑀 ) )
197 195 196 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑀 ) )
198 fnfvelrn ⊢ ( ( 𝑄 Fn ( 0 ... 𝑀 ) ∧ 𝑀 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑀 ) ∈ ran 𝑄 )
199 192 197 198 syl2anc ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ∈ ran 𝑄 )
200 189 199 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ ran 𝑄 )
201 200 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐵 ∈ ran 𝑄 )
202 182 201 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
203 202 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
204 oveq1 ⊢ ( 𝑘 = ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) → ( 𝑘 · ( 𝐵 − 𝐴 ) ) = ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · ( 𝐵 − 𝐴 ) ) )
205 204 oveq2d ⊢ ( 𝑘 = ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) → ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) = ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · ( 𝐵 − 𝐴 ) ) ) )
206 205 eleq1d ⊢ ( 𝑘 = ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) → ( ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) )
207 206 rspcev ⊢ ( ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) ∈ ℤ ∧ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) → ∃ 𝑘 ∈ ℤ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
208 151 203 207 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ∃ 𝑘 ∈ ℤ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
209 oveq1 ⊢ ( 𝑦 = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) → ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) = ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) )
210 209 eleq1d ⊢ ( 𝑦 = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) → ( ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) )
211 210 rexbidv ⊢ ( 𝑦 = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) → ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) )
212 211 elrab ⊢ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ↔ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ( 𝐶 [,] 𝐷 ) ∧ ∃ 𝑘 ∈ ℤ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) )
213 120 208 212 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } )
214 elun2 ⊢ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
215 213 214 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
216 foelrn ⊢ ( ( 𝑆 : ( 0 ... 𝑁 ) –onto→ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ∧ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) → ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) = ( 𝑆 ‘ 𝑖 ) )
217 81 215 216 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) = ( 𝑆 ‘ 𝑖 ) )
218 eqcom ⊢ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) = ( 𝑆 ‘ 𝑖 ) ↔ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
219 218 rexbii ⊢ ( ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) = ( 𝑆 ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
220 217 219 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
221 103 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( 𝑆 ‘ 𝑗 ) < ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
222 218 bilanri ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) = ( 𝑆 ‘ 𝑖 ) )
223 221 222 breqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) )
224 110 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
225 222 224 eqbrtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
226 223 225 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
227 226 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
228 simplll ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) )
229 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
230 elfzelz ⊢ ( 𝑖 ∈ ( 0 ... 𝑁 ) → 𝑖 ∈ ℤ )
231 230 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑖 ∈ ℤ )
232 68 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑗 ∈ ℤ )
233 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) )
234 73 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ) → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
235 53 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
236 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
237 isorel ⊢ ( ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) ∧ ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑗 < 𝑖 ↔ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ) )
238 234 235 236 237 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ) → ( 𝑗 < 𝑖 ↔ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ) )
239 233 238 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ) → 𝑗 < 𝑖 )
240 239 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑗 < 𝑖 )
241 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
242 73 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
243 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
244 65 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) )
245 isorel ⊢ ( ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) ∧ ( 𝑖 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑖 < ( 𝑗 + 1 ) ↔ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
246 242 243 244 245 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑖 < ( 𝑗 + 1 ) ↔ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
247 241 246 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → 𝑖 < ( 𝑗 + 1 ) )
248 247 adantrl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑖 < ( 𝑗 + 1 ) )
249 btwnnz ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑗 < 𝑖 ∧ 𝑖 < ( 𝑗 + 1 ) ) → ¬ 𝑖 ∈ ℤ )
250 232 240 248 249 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ¬ 𝑖 ∈ ℤ )
251 231 250 pm2.65da ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ¬ ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
252 228 229 251 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ¬ ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
253 227 252 pm2.65da ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ¬ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
254 253 nrexdv ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ¬ ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
255 254 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ¬ ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
256 220 255 condan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
257 62 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ* )
258 85 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝑇 ∈ ℝ )
259 62 258 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ℝ )
260 elioc2 ⊢ ( ( ( 𝑆 ‘ 𝑗 ) ∈ ℝ* ∧ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ℝ ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( ( 𝑆 ‘ 𝑗 ) (,] ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ↔ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ) )
261 257 259 260 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( ( 𝑆 ‘ 𝑗 ) (,] ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ↔ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ) )
262 67 77 256 261 mpbir3and ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( ( 𝑆 ‘ 𝑗 ) (,] ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) )
263 57 60 61 2 10 62 63 262 fourierdlem26 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( 𝐴 + ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) )
264 263 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − 𝐴 ) = ( ( 𝐴 + ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) − 𝐴 ) )
265 57 recnd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐴 ∈ ℂ )
266 66 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℂ )
267 266 139 subcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ∈ ℂ )
268 267 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ∈ ℂ )
269 265 268 pncan2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝐴 + ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) − 𝐴 ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
270 59 264 269 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
271 11 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐿 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) ) )
272 eqcom ⊢ ( 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ↔ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝑦 )
273 272 bilani ⊢ ( ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝑦 )
274 neqne ⊢ ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≠ 𝐵 )
275 274 adantr ⊢ ( ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≠ 𝐵 )
276 273 275 eqnetrrd ⊢ ( ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → 𝑦 ≠ 𝐵 )
277 276 neneqd ⊢ ( ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → ¬ 𝑦 = 𝐵 )
278 277 iffalsed ⊢ ( ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) = 𝑦 )
279 simpr ⊢ ( ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
280 278 279 eqtrd ⊢ ( ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
281 280 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
282 55 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
283 271 281 282 282 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
284 283 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
285 id ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) → 𝑥 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
286 oveq2 ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) → ( 𝐵 − 𝑥 ) = ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
287 286 oveq1d ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) → ( ( 𝐵 − 𝑥 ) / 𝑇 ) = ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) )
288 287 fveq2d ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) )
289 288 oveq1d ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) )
290 285 289 oveq12d ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) )
291 290 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) )
292 129 66 resubcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ )
293 292 102 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ∈ ℝ )
294 293 flcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ∈ ℤ )
295 294 zred ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ∈ ℝ )
296 295 86 remulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
297 66 296 readdcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
298 121 291 66 297 fvmptd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) )
299 298 136 oveq12d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) − ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) ) )
300 299 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) − ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) ) )
301 flle ⊢ ( ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ∈ ℝ → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ≤ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) )
302 293 301 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ≤ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) )
303 54 66 76 ltled ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ≤ ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
304 54 66 129 303 lesub2dd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ≤ ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) )
305 292 130 102 304 lediv1dd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
306 295 293 131 302 305 letrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
307 306 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
308 295 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ∈ ℝ )
309 1red ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) → 1 ∈ ℝ )
310 308 309 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ∈ ℝ )
311 131 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) → ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∈ ℝ )
312 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) → ¬ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) )
313 310 311 312 nltled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
314 313 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
315 80 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝑆 : ( 0 ... 𝑁 ) –onto→ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
316 89 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝐶 ∈ ℝ )
317 93 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝐷 ∈ ℝ )
318 136 135 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ )
319 129 318 resubcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℝ )
320 54 319 readdcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) ∈ ℝ )
321 12 320 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑍 ∈ ℝ )
322 321 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝑍 ∈ ℝ )
323 20 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
324 323 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 ∈ ℝ* )
325 elioc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 𝐴 (,] 𝐵 ) ↔ ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ ∧ 𝐴 < ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝐵 ) ) )
326 324 129 325 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 𝐴 (,] 𝐵 ) ↔ ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ ∧ 𝐴 < ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝐵 ) ) )
327 55 326 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ ∧ 𝐴 < ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝐵 ) )
328 327 simp3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝐵 )
329 129 318 subge0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 0 ≤ ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ↔ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝐵 ) )
330 328 329 mpbird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 0 ≤ ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
331 54 319 addge01d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 0 ≤ ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ↔ ( 𝑆 ‘ 𝑗 ) ≤ ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) ) )
332 330 331 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ≤ ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) )
333 89 54 320 97 332 letrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐶 ≤ ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) )
334 333 12 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐶 ≤ 𝑍 )
335 334 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝐶 ≤ 𝑍 )
336 66 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
337 293 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ∈ ℝ )
338 reflcl ⊢ ( ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ∈ ℝ → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ∈ ℝ )
339 peano2re ⊢ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ∈ ℝ → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ∈ ℝ )
340 337 338 339 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ∈ ℝ )
341 129 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝐵 ∈ ℝ )
342 341 322 resubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( 𝐵 − 𝑍 ) ∈ ℝ )
343 102 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝑇 ∈ ℝ+ )
344 342 343 rerpdivcld ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( 𝐵 − 𝑍 ) / 𝑇 ) ∈ ℝ )
345 flltp1 ⊢ ( ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ∈ ℝ → ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) )
346 293 345 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) )
347 346 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) )
348 294 peano2zd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ∈ ℤ )
349 348 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ∈ ℤ )
350 131 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∈ ℝ )
351 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
352 319 102 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) ∈ ℝ )
353 352 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) ∈ ℝ )
354 20 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 ∈ ℝ )
355 327 simp2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 < ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
356 354 318 129 355 ltsub2dd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) < ( 𝐵 − 𝐴 ) )
357 356 2 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) < 𝑇 )
358 319 86 102 357 ltdiv1dd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) < ( 𝑇 / 𝑇 ) )
359 144 145 dividd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑇 / 𝑇 ) = 1 )
360 358 359 breqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) < 1 )
361 360 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) < 1 )
362 130 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) ∈ ℂ )
363 319 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℂ )
364 362 363 144 145 divsubdird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) − ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) / 𝑇 ) = ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) ) )
365 364 eqcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) ) = ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) − ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) / 𝑇 ) )
366 129 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐵 ∈ ℂ )
367 318 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ℂ )
368 366 139 367 nnncan1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) − ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
369 368 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) − ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) / 𝑇 ) = ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
370 365 369 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) ) = ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
371 370 148 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) ) ∈ ℤ )
372 371 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) ) ∈ ℤ )
373 349 350 351 353 361 372 zltlesub ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) ) )
374 12 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑍 = ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) )
375 374 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − 𝑍 ) = ( 𝐵 − ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) ) )
376 139 366 367 addsub12d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( 𝐵 + ( ( 𝑆 ‘ 𝑗 ) − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) )
377 366 367 139 subsub2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝐵 + ( ( 𝑆 ‘ 𝑗 ) − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) )
378 376 377 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( 𝐵 − ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) )
379 378 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) ) = ( 𝐵 − ( 𝐵 − ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) ) )
380 367 139 subcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) ∈ ℂ )
381 366 380 nncand ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( 𝐵 − ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
382 375 379 381 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − 𝑍 ) = ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
383 382 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 − 𝑍 ) / 𝑇 ) = ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
384 369 365 383 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) ) = ( ( 𝐵 − 𝑍 ) / 𝑇 ) )
385 384 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) ) = ( ( 𝐵 − 𝑍 ) / 𝑇 ) )
386 373 385 breqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − 𝑍 ) / 𝑇 ) )
387 337 340 344 347 386 ltletrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) < ( ( 𝐵 − 𝑍 ) / 𝑇 ) )
388 292 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ )
389 388 342 343 ltdiv1d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) < ( 𝐵 − 𝑍 ) ↔ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) < ( ( 𝐵 − 𝑍 ) / 𝑇 ) ) )
390 387 389 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) < ( 𝐵 − 𝑍 ) )
391 322 336 341 ltsub2d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( 𝑍 < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ↔ ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) < ( 𝐵 − 𝑍 ) ) )
392 390 391 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝑍 < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
393 115 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ 𝐷 )
394 322 336 317 392 393 ltletrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝑍 < 𝐷 )
395 322 317 394 ltled ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝑍 ≤ 𝐷 )
396 316 317 322 335 395 eliccd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝑍 ∈ ( 𝐶 [,] 𝐷 ) )
397 33 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − 𝐴 ) = 𝑇 )
398 397 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · ( 𝐵 − 𝐴 ) ) = ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) )
399 380 144 145 divcan1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) = ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
400 398 399 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · ( 𝐵 − 𝐴 ) ) = ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
401 374 400 oveq12d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑍 + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · ( 𝐵 − 𝐴 ) ) ) = ( ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) + ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) )
402 139 363 addcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) + ( 𝑆 ‘ 𝑗 ) ) )
403 402 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) + ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) + ( 𝑆 ‘ 𝑗 ) ) + ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) )
404 363 139 367 ppncand ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) + ( 𝑆 ‘ 𝑗 ) ) + ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) = ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) + ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
405 366 367 npcand ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) + ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = 𝐵 )
406 404 405 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) + ( 𝑆 ‘ 𝑗 ) ) + ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) = 𝐵 )
407 401 403 406 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑍 + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · ( 𝐵 − 𝐴 ) ) ) = 𝐵 )
408 200 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐵 ∈ ran 𝑄 )
409 407 408 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑍 + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
410 oveq1 ⊢ ( 𝑘 = ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) → ( 𝑘 · ( 𝐵 − 𝐴 ) ) = ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · ( 𝐵 − 𝐴 ) ) )
411 410 oveq2d ⊢ ( 𝑘 = ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) → ( 𝑍 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) = ( 𝑍 + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · ( 𝐵 − 𝐴 ) ) ) )
412 411 eleq1d ⊢ ( 𝑘 = ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) → ( ( 𝑍 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ( 𝑍 + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) )
413 412 rspcev ⊢ ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∈ ℤ ∧ ( 𝑍 + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) → ∃ 𝑘 ∈ ℤ ( 𝑍 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
414 148 409 413 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ∃ 𝑘 ∈ ℤ ( 𝑍 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
415 414 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ∃ 𝑘 ∈ ℤ ( 𝑍 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
416 oveq1 ⊢ ( 𝑦 = 𝑍 → ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) = ( 𝑍 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) )
417 416 eleq1d ⊢ ( 𝑦 = 𝑍 → ( ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ( 𝑍 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) )
418 417 rexbidv ⊢ ( 𝑦 = 𝑍 → ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑍 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) )
419 418 elrab ⊢ ( 𝑍 ∈ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ↔ ( 𝑍 ∈ ( 𝐶 [,] 𝐷 ) ∧ ∃ 𝑘 ∈ ℤ ( 𝑍 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) )
420 396 415 419 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝑍 ∈ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } )
421 elun2 ⊢ ( 𝑍 ∈ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } → 𝑍 ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
422 420 421 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝑍 ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
423 foelrn ⊢ ( ( 𝑆 : ( 0 ... 𝑁 ) –onto→ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ∧ 𝑍 ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) → ∃ 𝑖 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑆 ‘ 𝑖 ) )
424 315 422 423 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ∃ 𝑖 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑆 ‘ 𝑖 ) )
425 54 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
426 319 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℝ )
427 318 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ )
428 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐵 ∈ ℝ )
429 328 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝐵 )
430 274 necomd ⊢ ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 → 𝐵 ≠ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
431 430 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐵 ≠ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
432 427 428 429 431 leneltd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) < 𝐵 )
433 427 428 posdifd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) < 𝐵 ↔ 0 < ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) )
434 432 433 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 0 < ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
435 426 434 elrpd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℝ+ )
436 425 435 ltaddrpd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ 𝑗 ) < ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) )
437 436 12 breqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ 𝑗 ) < 𝑍 )
438 437 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) ∧ 𝑍 = ( 𝑆 ‘ 𝑖 ) ) → ( 𝑆 ‘ 𝑗 ) < 𝑍 )
439 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) ∧ 𝑍 = ( 𝑆 ‘ 𝑖 ) ) → 𝑍 = ( 𝑆 ‘ 𝑖 ) )
440 438 439 breqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) ∧ 𝑍 = ( 𝑆 ‘ 𝑖 ) ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) )
441 392 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) ∧ 𝑍 = ( 𝑆 ‘ 𝑖 ) ) → 𝑍 < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
442 439 441 eqbrtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) ∧ 𝑍 = ( 𝑆 ‘ 𝑖 ) ) → ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
443 440 442 jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) ∧ 𝑍 = ( 𝑆 ‘ 𝑖 ) ) → ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
444 443 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( 𝑍 = ( 𝑆 ‘ 𝑖 ) → ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
445 444 reximdv ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ∃ 𝑖 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑆 ‘ 𝑖 ) → ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
446 424 445 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
447 314 446 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) → ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
448 251 nrexdv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ¬ ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
449 448 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) → ¬ ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
450 447 449 condan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) )
451 307 450 jca ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∧ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) )
452 131 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∈ ℝ )
453 294 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ∈ ℤ )
454 flbi ⊢ ( ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∈ ℝ ∧ ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ∈ ℤ ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ↔ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∧ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) ) )
455 452 453 454 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ↔ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∧ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) ) )
456 451 455 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) )
457 456 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) )
458 457 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) )
459 458 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) )
460 459 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) − ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) ) = ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) − ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) ) )
461 266 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℂ )
462 139 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ 𝑗 ) ∈ ℂ )
463 140 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ∈ ℂ )
464 461 462 463 pnpcan2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) − ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
465 460 464 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) − ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
466 284 300 465 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
467 270 466 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) )