Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem65 Structured version   Visualization version   GIF version

Theorem fourierdlem65 39721
 Description: The distance of two adjacent points in the moved partition is preserved in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem65.p 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem65.t 𝑇 = (𝐵𝐴)
fourierdlem65.m (𝜑𝑀 ∈ ℕ)
fourierdlem65.q (𝜑𝑄 ∈ (𝑃𝑀))
fourierdlem65.c (𝜑𝐶 ∈ ℝ)
fourierdlem65.d (𝜑𝐷 ∈ (𝐶(,)+∞))
fourierdlem65.o 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem65.n 𝑁 = ((#‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})) − 1)
fourierdlem65.s 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})))
fourierdlem65.e 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
fourierdlem65.l 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))
fourierdlem65.z 𝑍 = ((𝑆𝑗) + (𝐵 − (𝐸‘(𝑆𝑗))))
Assertion
Ref Expression
fourierdlem65 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐿‘(𝐸‘(𝑆𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)))
Distinct variable groups:   𝐴,𝑓,𝑘,𝑦   𝐴,𝑖,𝑥,𝑘,𝑦   𝐴,𝑚,𝑝,𝑖   𝐵,𝑓,𝑘,𝑦   𝐵,𝑖,𝑥   𝐵,𝑚,𝑝   𝐶,𝑓,𝑦   𝐶,𝑖,𝑚,𝑝   𝑥,𝐶   𝐷,𝑓,𝑦   𝐷,𝑖,𝑚,𝑝   𝑥,𝐷   𝑖,𝐸,𝑘,𝑥,𝑦   𝑖,𝑀,𝑚,𝑝   𝑓,𝑁,𝑦   𝑖,𝑁,𝑚,𝑝   𝑥,𝑁   𝑄,𝑓,𝑘,𝑦   𝑄,𝑖,𝑥   𝑄,𝑝   𝑆,𝑓,𝑘,𝑦   𝑆,𝑖,𝑥   𝑆,𝑝   𝑇,𝑖,𝑘,𝑥,𝑦   𝑖,𝑍,𝑘,𝑦   𝜑,𝑓,𝑘,𝑦   𝑖,𝑗,𝑘,𝑥,𝑦   𝜑,𝑖,𝑥
Allowed substitution hints:   𝜑(𝑗,𝑚,𝑝)   𝐴(𝑗)   𝐵(𝑗)   𝐶(𝑗,𝑘)   𝐷(𝑗,𝑘)   𝑃(𝑥,𝑦,𝑓,𝑖,𝑗,𝑘,𝑚,𝑝)   𝑄(𝑗,𝑚)   𝑆(𝑗,𝑚)   𝑇(𝑓,𝑗,𝑚,𝑝)   𝐸(𝑓,𝑗,𝑚,𝑝)   𝐿(𝑥,𝑦,𝑓,𝑖,𝑗,𝑘,𝑚,𝑝)   𝑀(𝑥,𝑦,𝑓,𝑗,𝑘)   𝑁(𝑗,𝑘)   𝑂(𝑥,𝑦,𝑓,𝑖,𝑗,𝑘,𝑚,𝑝)   𝑍(𝑥,𝑓,𝑗,𝑚,𝑝)

Proof of Theorem fourierdlem65
StepHypRef Expression
1 fourierdlem65.l . . . . . 6 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))
21a1i 11 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
3 simpr 477 . . . . . . . 8 (((𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → 𝑦 = (𝐸‘(𝑆𝑗)))
4 simpl 473 . . . . . . . 8 (((𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → (𝐸‘(𝑆𝑗)) = 𝐵)
53, 4eqtrd 2655 . . . . . . 7 (((𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → 𝑦 = 𝐵)
65iftrued 4071 . . . . . 6 (((𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝐴)
76adantll 749 . . . . 5 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ 𝑦 = (𝐸‘(𝑆𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝐴)
8 fourierdlem65.p . . . . . . . . . . 11 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
9 fourierdlem65.m . . . . . . . . . . 11 (𝜑𝑀 ∈ ℕ)
10 fourierdlem65.q . . . . . . . . . . 11 (𝜑𝑄 ∈ (𝑃𝑀))
118, 9, 10fourierdlem11 39668 . . . . . . . . . 10 (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
1211simp1d 1071 . . . . . . . . 9 (𝜑𝐴 ∈ ℝ)
1311simp2d 1072 . . . . . . . . 9 (𝜑𝐵 ∈ ℝ)
1411simp3d 1073 . . . . . . . . 9 (𝜑𝐴 < 𝐵)
15 fourierdlem65.t . . . . . . . . 9 𝑇 = (𝐵𝐴)
16 fourierdlem65.e . . . . . . . . 9 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
1712, 13, 14, 15, 16fourierdlem4 39661 . . . . . . . 8 (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))
1817adantr 481 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐸:ℝ⟶(𝐴(,]𝐵))
19 fourierdlem65.c . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ ℝ)
20 ioossre 12185 . . . . . . . . . . . . . . . 16 (𝐶(,)+∞) ⊆ ℝ
21 fourierdlem65.d . . . . . . . . . . . . . . . 16 (𝜑𝐷 ∈ (𝐶(,)+∞))
2220, 21sseldi 3585 . . . . . . . . . . . . . . 15 (𝜑𝐷 ∈ ℝ)
2319rexrd 10041 . . . . . . . . . . . . . . . 16 (𝜑𝐶 ∈ ℝ*)
24 pnfxr 10044 . . . . . . . . . . . . . . . . 17 +∞ ∈ ℝ*
2524a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → +∞ ∈ ℝ*)
26 ioogtlb 39159 . . . . . . . . . . . . . . . 16 ((𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ*𝐷 ∈ (𝐶(,)+∞)) → 𝐶 < 𝐷)
2723, 25, 21, 26syl3anc 1323 . . . . . . . . . . . . . . 15 (𝜑𝐶 < 𝐷)
28 fourierdlem65.o . . . . . . . . . . . . . . 15 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
29 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥𝑦 = 𝑥)
3015eqcomi 2630 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵𝐴) = 𝑇
3130oveq2i 6621 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 · (𝐵𝐴)) = (𝑘 · 𝑇)
3231a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → (𝑘 · (𝐵𝐴)) = (𝑘 · 𝑇))
3329, 32oveq12d 6628 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑥 → (𝑦 + (𝑘 · (𝐵𝐴))) = (𝑥 + (𝑘 · 𝑇)))
3433eleq1d 2683 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑥 → ((𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄 ↔ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄))
3534rexbidv 3046 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑥 → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄))
3635cbvrabv 3188 . . . . . . . . . . . . . . . 16 {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄} = {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}
3736uneq2i 3747 . . . . . . . . . . . . . . 15 ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
38 fourierdlem65.n . . . . . . . . . . . . . . 15 𝑁 = ((#‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})) − 1)
39 fourierdlem65.s . . . . . . . . . . . . . . 15 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})))
4015, 8, 9, 10, 19, 22, 27, 28, 37, 38, 39fourierdlem54 39710 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄}))))
4140simpld 475 . . . . . . . . . . . . 13 (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)))
4241simprd 479 . . . . . . . . . . . 12 (𝜑𝑆 ∈ (𝑂𝑁))
4341simpld 475 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℕ)
4428fourierdlem2 39659 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂𝑁) ↔ (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
4543, 44syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑆 ∈ (𝑂𝑁) ↔ (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
4642, 45mpbid 222 . . . . . . . . . . 11 (𝜑 → (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1)))))
4746simpld 475 . . . . . . . . . 10 (𝜑𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)))
48 elmapi 7831 . . . . . . . . . 10 (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
4947, 48syl 17 . . . . . . . . 9 (𝜑𝑆:(0...𝑁)⟶ℝ)
5049adantr 481 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
51 elfzofz 12434 . . . . . . . . 9 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
5251adantl 482 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0...𝑁))
5350, 52ffvelrnd 6321 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ∈ ℝ)
5418, 53ffvelrnd 6321 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆𝑗)) ∈ (𝐴(,]𝐵))
5554adantr 481 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) ∈ (𝐴(,]𝐵))
5612ad2antrr 761 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐴 ∈ ℝ)
572, 7, 55, 56fvmptd 6250 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆𝑗))) = 𝐴)
5857oveq2d 6626 . . 3 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐿‘(𝐸‘(𝑆𝑗)))) = ((𝐸‘(𝑆‘(𝑗 + 1))) − 𝐴))
5913ad2antrr 761 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐵 ∈ ℝ)
6014ad2antrr 761 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐴 < 𝐵)
6153adantr 481 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝑆𝑗) ∈ ℝ)
62 simpr 477 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) = 𝐵)
63 fzofzp1 12514 . . . . . . . . 9 (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
6463adantl 482 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ (0...𝑁))
6550, 64ffvelrnd 6321 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
6665adantr 481 . . . . . 6 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
67 elfzoelz 12419 . . . . . . . . . . 11 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℤ)
6867zred 11434 . . . . . . . . . 10 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℝ)
6968adantl 482 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℝ)
7069ltp1d 10906 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑗 < (𝑗 + 1))
7140simprd 479 . . . . . . . . . 10 (𝜑𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})))
7271adantr 481 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})))
73 isorel 6536 . . . . . . . . 9 ((𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑗 < (𝑗 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝑗 + 1))))
7472, 52, 64, 73syl12anc 1321 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑗 < (𝑗 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝑗 + 1))))
7570, 74mpbid 222 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) < (𝑆‘(𝑗 + 1)))
7675adantr 481 . . . . . 6 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝑆𝑗) < (𝑆‘(𝑗 + 1)))
77 isof1o 6533 . . . . . . . . . . 11 (𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})) → 𝑆:(0...𝑁)–1-1-onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄}))
78 f1ofo 6106 . . . . . . . . . . 11 (𝑆:(0...𝑁)–1-1-onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄}) → 𝑆:(0...𝑁)–onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄}))
7971, 77, 783syl 18 . . . . . . . . . 10 (𝜑𝑆:(0...𝑁)–onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄}))
8079ad3antrrr 765 . . . . . . . . 9 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → 𝑆:(0...𝑁)–onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄}))
8119ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → 𝐶 ∈ ℝ)
8222ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → 𝐷 ∈ ℝ)
8313, 12resubcld 10410 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝐴) ∈ ℝ)
8415, 83syl5eqel 2702 . . . . . . . . . . . . . . . 16 (𝜑𝑇 ∈ ℝ)
8584adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑇 ∈ ℝ)
8653, 85readdcld 10021 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + 𝑇) ∈ ℝ)
8786adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → ((𝑆𝑗) + 𝑇) ∈ ℝ)
8819adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐶 ∈ ℝ)
8928, 43, 42fourierdlem15 39672 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
9089adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
9190, 52ffvelrnd 6321 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ∈ (𝐶[,]𝐷))
9222adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐷 ∈ ℝ)
93 elicc2 12188 . . . . . . . . . . . . . . . . . . 19 ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆𝑗) ∈ (𝐶[,]𝐷) ↔ ((𝑆𝑗) ∈ ℝ ∧ 𝐶 ≤ (𝑆𝑗) ∧ (𝑆𝑗) ≤ 𝐷)))
9488, 92, 93syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) ∈ (𝐶[,]𝐷) ↔ ((𝑆𝑗) ∈ ℝ ∧ 𝐶 ≤ (𝑆𝑗) ∧ (𝑆𝑗) ≤ 𝐷)))
9591, 94mpbid 222 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) ∈ ℝ ∧ 𝐶 ≤ (𝑆𝑗) ∧ (𝑆𝑗) ≤ 𝐷))
9695simp2d 1072 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐶 ≤ (𝑆𝑗))
9712, 13posdifd 10566 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
9814, 97mpbid 222 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 < (𝐵𝐴))
9998, 15syl6breqr 4660 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 < 𝑇)
10084, 99elrpd 11821 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ∈ ℝ+)
101100adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑇 ∈ ℝ+)
10253, 101ltaddrpd 11857 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) < ((𝑆𝑗) + 𝑇))
10388, 53, 86, 96, 102lelttrd 10147 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐶 < ((𝑆𝑗) + 𝑇))
10488, 86, 103ltled 10137 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐶 ≤ ((𝑆𝑗) + 𝑇))
105104adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → 𝐶 ≤ ((𝑆𝑗) + 𝑇))
10665adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
107 simpr 477 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇))
10887, 106ltnled 10136 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → (((𝑆𝑗) + 𝑇) < (𝑆‘(𝑗 + 1)) ↔ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)))
109107, 108mpbird 247 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → ((𝑆𝑗) + 𝑇) < (𝑆‘(𝑗 + 1)))
11090, 64ffvelrnd 6321 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ (𝐶[,]𝐷))
111 elicc2 12188 . . . . . . . . . . . . . . . . . . 19 ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘(𝑗 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝑗 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝑗 + 1)) ∧ (𝑆‘(𝑗 + 1)) ≤ 𝐷)))
11288, 92, 111syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆‘(𝑗 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝑗 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝑗 + 1)) ∧ (𝑆‘(𝑗 + 1)) ≤ 𝐷)))
113110, 112mpbid 222 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆‘(𝑗 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝑗 + 1)) ∧ (𝑆‘(𝑗 + 1)) ≤ 𝐷))
114113simp3d 1073 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ≤ 𝐷)
115114adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → (𝑆‘(𝑗 + 1)) ≤ 𝐷)
11687, 106, 82, 109, 115ltletrd 10149 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → ((𝑆𝑗) + 𝑇) < 𝐷)
11787, 82, 116ltled 10137 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → ((𝑆𝑗) + 𝑇) ≤ 𝐷)
11881, 82, 87, 105, 117eliccd 39168 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → ((𝑆𝑗) + 𝑇) ∈ (𝐶[,]𝐷))
119118adantlr 750 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → ((𝑆𝑗) + 𝑇) ∈ (𝐶[,]𝐷))
12016a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))))
121 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = (𝑆𝑗) → 𝑥 = (𝑆𝑗))
122 oveq2 6618 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = (𝑆𝑗) → (𝐵𝑥) = (𝐵 − (𝑆𝑗)))
123122oveq1d 6625 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑆𝑗) → ((𝐵𝑥) / 𝑇) = ((𝐵 − (𝑆𝑗)) / 𝑇))
124123fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (𝑆𝑗) → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)))
125124oveq1d 6625 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = (𝑆𝑗) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇))
126121, 125oveq12d 6628 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑆𝑗) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) = ((𝑆𝑗) + ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇)))
127126adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑥 = (𝑆𝑗)) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) = ((𝑆𝑗) + ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇)))
12813adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐵 ∈ ℝ)
129128, 53resubcld 10410 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝑆𝑗)) ∈ ℝ)
130129, 101rerpdivcld 11855 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝑆𝑗)) / 𝑇) ∈ ℝ)
131130flcld 12547 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0..^𝑁)) → (⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) ∈ ℤ)
132131zred 11434 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0..^𝑁)) → (⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) ∈ ℝ)
133132, 85remulcld 10022 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇) ∈ ℝ)
13453, 133readdcld 10021 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇)) ∈ ℝ)
135120, 127, 53, 134fvmptd 6250 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆𝑗)) = ((𝑆𝑗) + ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇)))
136135oveq1d 6625 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) = (((𝑆𝑗) + ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇)) − (𝑆𝑗)))
137136oveq1d 6625 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) = ((((𝑆𝑗) + ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇)) − (𝑆𝑗)) / 𝑇))
13853recnd 10020 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ∈ ℂ)
139133recnd 10020 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑁)) → ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇) ∈ ℂ)
140138, 139pncan2d 10346 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆𝑗) + ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇)) − (𝑆𝑗)) = ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇))
141140oveq1d 6625 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → ((((𝑆𝑗) + ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇)) − (𝑆𝑗)) / 𝑇) = (((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇) / 𝑇))
142132recnd 10020 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → (⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) ∈ ℂ)
14385recnd 10020 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑇 ∈ ℂ)
144101rpne0d 11829 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑇 ≠ 0)
145142, 143, 144divcan4d 10759 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → (((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)))
146137, 141, 1453eqtrd 2659 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) = (⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)))
147146, 131eqeltrd 2698 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) ∈ ℤ)
148 peano2zm 11372 . . . . . . . . . . . . . 14 ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) ∈ ℤ → ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) ∈ ℤ)
149147, 148syl 17 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) ∈ ℤ)
150149ad2antrr 761 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) ∈ ℤ)
15130oveq2i 6621 . . . . . . . . . . . . . . . . 17 (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) · (𝐵𝐴)) = (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) · 𝑇)
152151oveq2i 6621 . . . . . . . . . . . . . . . 16 (((𝑆𝑗) + 𝑇) + (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) · (𝐵𝐴))) = (((𝑆𝑗) + 𝑇) + (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) · 𝑇))
153152a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (((𝑆𝑗) + 𝑇) + (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) · (𝐵𝐴))) = (((𝑆𝑗) + 𝑇) + (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) · 𝑇)))
154135adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) = ((𝑆𝑗) + ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇)))
155 oveq1 6617 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐸‘(𝑆𝑗)) = 𝐵 → ((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) = (𝐵 − (𝑆𝑗)))
156155eqcomd 2627 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸‘(𝑆𝑗)) = 𝐵 → (𝐵 − (𝑆𝑗)) = ((𝐸‘(𝑆𝑗)) − (𝑆𝑗)))
157156oveq1d 6625 . . . . . . . . . . . . . . . . . . . 20 ((𝐸‘(𝑆𝑗)) = 𝐵 → ((𝐵 − (𝑆𝑗)) / 𝑇) = (((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇))
158157fveq2d 6157 . . . . . . . . . . . . . . . . . . 19 ((𝐸‘(𝑆𝑗)) = 𝐵 → (⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) = (⌊‘(((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇)))
159158oveq1d 6625 . . . . . . . . . . . . . . . . . 18 ((𝐸‘(𝑆𝑗)) = 𝐵 → ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇) = ((⌊‘(((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇)) · 𝑇))
160159oveq2d 6626 . . . . . . . . . . . . . . . . 17 ((𝐸‘(𝑆𝑗)) = 𝐵 → ((𝑆𝑗) + ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇)) = ((𝑆𝑗) + ((⌊‘(((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇)) · 𝑇)))
161160adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝑆𝑗) + ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇)) = ((𝑆𝑗) + ((⌊‘(((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇)) · 𝑇)))
162146, 142eqeltrd 2698 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) ∈ ℂ)
163 1cnd 10008 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0..^𝑁)) → 1 ∈ ℂ)
164162, 163, 143subdird 10439 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) · 𝑇) = (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · 𝑇) − (1 · 𝑇)))
16584recnd 10020 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑇 ∈ ℂ)
166165mulid2d 10010 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1 · 𝑇) = 𝑇)
167166oveq2d 6626 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · 𝑇) − (1 · 𝑇)) = (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · 𝑇) − 𝑇))
168167adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · 𝑇) − (1 · 𝑇)) = (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · 𝑇) − 𝑇))
169164, 168eqtrd 2655 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) · 𝑇) = (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · 𝑇) − 𝑇))
170169oveq2d 6626 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆𝑗) + 𝑇) + (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) · 𝑇)) = (((𝑆𝑗) + 𝑇) + (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · 𝑇) − 𝑇)))
171162, 143mulcld 10012 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · 𝑇) ∈ ℂ)
172138, 143, 171ppncand 10384 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆𝑗) + 𝑇) + (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · 𝑇) − 𝑇)) = ((𝑆𝑗) + ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · 𝑇)))
173 flid 12557 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) ∈ ℤ → (⌊‘(((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇)) = (((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇))
174147, 173syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0..^𝑁)) → (⌊‘(((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇)) = (((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇))
175174eqcomd 2627 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) = (⌊‘(((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇)))
176175oveq1d 6625 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · 𝑇) = ((⌊‘(((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇)) · 𝑇))
177176oveq2d 6626 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · 𝑇)) = ((𝑆𝑗) + ((⌊‘(((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇)) · 𝑇)))
178170, 172, 1773eqtrrd 2660 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + ((⌊‘(((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇)) · 𝑇)) = (((𝑆𝑗) + 𝑇) + (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) · 𝑇)))
179178adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝑆𝑗) + ((⌊‘(((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇)) · 𝑇)) = (((𝑆𝑗) + 𝑇) + (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) · 𝑇)))
180154, 161, 1793eqtrrd 2660 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (((𝑆𝑗) + 𝑇) + (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) · 𝑇)) = (𝐸‘(𝑆𝑗)))
181153, 180, 623eqtrd 2659 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (((𝑆𝑗) + 𝑇) + (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) · (𝐵𝐴))) = 𝐵)
1828fourierdlem2 39659 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
1839, 182syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
18410, 183mpbid 222 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
185184simprd 479 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))
186185simpld 475 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵))
187186simprd 479 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑄𝑀) = 𝐵)
188187eqcomd 2627 . . . . . . . . . . . . . . . 16 (𝜑𝐵 = (𝑄𝑀))
1898, 9, 10fourierdlem15 39672 . . . . . . . . . . . . . . . . . 18 (𝜑𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
190 ffn 6007 . . . . . . . . . . . . . . . . . 18 (𝑄:(0...𝑀)⟶(𝐴[,]𝐵) → 𝑄 Fn (0...𝑀))
191189, 190syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑄 Fn (0...𝑀))
1929nnnn0d 11303 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ ℕ0)
193 nn0uz 11674 . . . . . . . . . . . . . . . . . . 19 0 = (ℤ‘0)
194192, 193syl6eleq 2708 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 ∈ (ℤ‘0))
195 eluzfz2 12299 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ (ℤ‘0) → 𝑀 ∈ (0...𝑀))
196194, 195syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ (0...𝑀))
197 fnfvelrn 6317 . . . . . . . . . . . . . . . . 17 ((𝑄 Fn (0...𝑀) ∧ 𝑀 ∈ (0...𝑀)) → (𝑄𝑀) ∈ ran 𝑄)
198191, 196, 197syl2anc 692 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄𝑀) ∈ ran 𝑄)
199188, 198eqeltrd 2698 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ ran 𝑄)
200199ad2antrr 761 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐵 ∈ ran 𝑄)
201181, 200eqeltrd 2698 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (((𝑆𝑗) + 𝑇) + (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) · (𝐵𝐴))) ∈ ran 𝑄)
202201adantr 481 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → (((𝑆𝑗) + 𝑇) + (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) · (𝐵𝐴))) ∈ ran 𝑄)
203 oveq1 6617 . . . . . . . . . . . . . . 15 (𝑘 = ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) → (𝑘 · (𝐵𝐴)) = (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) · (𝐵𝐴)))
204203oveq2d 6626 . . . . . . . . . . . . . 14 (𝑘 = ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) → (((𝑆𝑗) + 𝑇) + (𝑘 · (𝐵𝐴))) = (((𝑆𝑗) + 𝑇) + (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) · (𝐵𝐴))))
205204eleq1d 2683 . . . . . . . . . . . . 13 (𝑘 = ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) → ((((𝑆𝑗) + 𝑇) + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄 ↔ (((𝑆𝑗) + 𝑇) + (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) · (𝐵𝐴))) ∈ ran 𝑄))
206205rspcev 3298 . . . . . . . . . . . 12 ((((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) ∈ ℤ ∧ (((𝑆𝑗) + 𝑇) + (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) − 1) · (𝐵𝐴))) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (((𝑆𝑗) + 𝑇) + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄)
207150, 202, 206syl2anc 692 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → ∃𝑘 ∈ ℤ (((𝑆𝑗) + 𝑇) + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄)
208 oveq1 6617 . . . . . . . . . . . . . 14 (𝑦 = ((𝑆𝑗) + 𝑇) → (𝑦 + (𝑘 · (𝐵𝐴))) = (((𝑆𝑗) + 𝑇) + (𝑘 · (𝐵𝐴))))
209208eleq1d 2683 . . . . . . . . . . . . 13 (𝑦 = ((𝑆𝑗) + 𝑇) → ((𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄 ↔ (((𝑆𝑗) + 𝑇) + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄))
210209rexbidv 3046 . . . . . . . . . . . 12 (𝑦 = ((𝑆𝑗) + 𝑇) → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (((𝑆𝑗) + 𝑇) + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄))
211210elrab 3350 . . . . . . . . . . 11 (((𝑆𝑗) + 𝑇) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄} ↔ (((𝑆𝑗) + 𝑇) ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (((𝑆𝑗) + 𝑇) + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄))
212119, 207, 211sylanbrc 697 . . . . . . . . . 10 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → ((𝑆𝑗) + 𝑇) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})
213 elun2 3764 . . . . . . . . . 10 (((𝑆𝑗) + 𝑇) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄} → ((𝑆𝑗) + 𝑇) ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄}))
214212, 213syl 17 . . . . . . . . 9 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → ((𝑆𝑗) + 𝑇) ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄}))
215 foelrn 6339 . . . . . . . . 9 ((𝑆:(0...𝑁)–onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄}) ∧ ((𝑆𝑗) + 𝑇) ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})) → ∃𝑖 ∈ (0...𝑁)((𝑆𝑗) + 𝑇) = (𝑆𝑖))
21680, 214, 215syl2anc 692 . . . . . . . 8 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → ∃𝑖 ∈ (0...𝑁)((𝑆𝑗) + 𝑇) = (𝑆𝑖))
217 eqcom 2628 . . . . . . . . 9 (((𝑆𝑗) + 𝑇) = (𝑆𝑖) ↔ (𝑆𝑖) = ((𝑆𝑗) + 𝑇))
218217rexbii 3035 . . . . . . . 8 (∃𝑖 ∈ (0...𝑁)((𝑆𝑗) + 𝑇) = (𝑆𝑖) ↔ ∃𝑖 ∈ (0...𝑁)(𝑆𝑖) = ((𝑆𝑗) + 𝑇))
219216, 218sylib 208 . . . . . . 7 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → ∃𝑖 ∈ (0...𝑁)(𝑆𝑖) = ((𝑆𝑗) + 𝑇))
220102ad2antrr 761 . . . . . . . . . . . . 13 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) ∧ (𝑆𝑖) = ((𝑆𝑗) + 𝑇)) → (𝑆𝑗) < ((𝑆𝑗) + 𝑇))
221217biimpri 218 . . . . . . . . . . . . . 14 ((𝑆𝑖) = ((𝑆𝑗) + 𝑇) → ((𝑆𝑗) + 𝑇) = (𝑆𝑖))
222221adantl 482 . . . . . . . . . . . . 13 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) ∧ (𝑆𝑖) = ((𝑆𝑗) + 𝑇)) → ((𝑆𝑗) + 𝑇) = (𝑆𝑖))
223220, 222breqtrd 4644 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) ∧ (𝑆𝑖) = ((𝑆𝑗) + 𝑇)) → (𝑆𝑗) < (𝑆𝑖))
224109adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) ∧ (𝑆𝑖) = ((𝑆𝑗) + 𝑇)) → ((𝑆𝑗) + 𝑇) < (𝑆‘(𝑗 + 1)))
225222, 224eqbrtrrd 4642 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) ∧ (𝑆𝑖) = ((𝑆𝑗) + 𝑇)) → (𝑆𝑖) < (𝑆‘(𝑗 + 1)))
226223, 225jca 554 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) ∧ (𝑆𝑖) = ((𝑆𝑗) + 𝑇)) → ((𝑆𝑗) < (𝑆𝑖) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1))))
227226adantlr 750 . . . . . . . . . 10 (((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆𝑖) = ((𝑆𝑗) + 𝑇)) → ((𝑆𝑗) < (𝑆𝑖) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1))))
228 simplll 797 . . . . . . . . . . 11 (((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆𝑖) = ((𝑆𝑗) + 𝑇)) → (𝜑𝑗 ∈ (0..^𝑁)))
229 simplr 791 . . . . . . . . . . 11 (((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆𝑖) = ((𝑆𝑗) + 𝑇)) → 𝑖 ∈ (0...𝑁))
230 elfzelz 12292 . . . . . . . . . . . . 13 (𝑖 ∈ (0...𝑁) → 𝑖 ∈ ℤ)
231230ad2antlr 762 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ ((𝑆𝑗) < (𝑆𝑖) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1)))) → 𝑖 ∈ ℤ)
23267ad3antlr 766 . . . . . . . . . . . . 13 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ ((𝑆𝑗) < (𝑆𝑖) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1)))) → 𝑗 ∈ ℤ)
233 simpr 477 . . . . . . . . . . . . . . 15 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆𝑖)) → (𝑆𝑗) < (𝑆𝑖))
23472ad2antrr 761 . . . . . . . . . . . . . . . 16 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆𝑖)) → 𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})))
23552ad2antrr 761 . . . . . . . . . . . . . . . 16 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆𝑖)) → 𝑗 ∈ (0...𝑁))
236 simplr 791 . . . . . . . . . . . . . . . 16 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆𝑖)) → 𝑖 ∈ (0...𝑁))
237 isorel 6536 . . . . . . . . . . . . . . . 16 ((𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})) ∧ (𝑗 ∈ (0...𝑁) ∧ 𝑖 ∈ (0...𝑁))) → (𝑗 < 𝑖 ↔ (𝑆𝑗) < (𝑆𝑖)))
238234, 235, 236, 237syl12anc 1321 . . . . . . . . . . . . . . 15 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆𝑖)) → (𝑗 < 𝑖 ↔ (𝑆𝑗) < (𝑆𝑖)))
239233, 238mpbird 247 . . . . . . . . . . . . . 14 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆𝑖)) → 𝑗 < 𝑖)
240239adantrr 752 . . . . . . . . . . . . 13 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ ((𝑆𝑗) < (𝑆𝑖) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1)))) → 𝑗 < 𝑖)
241 simpr 477 . . . . . . . . . . . . . . 15 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1))) → (𝑆𝑖) < (𝑆‘(𝑗 + 1)))
24272ad2antrr 761 . . . . . . . . . . . . . . . 16 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1))) → 𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})))
243 simplr 791 . . . . . . . . . . . . . . . 16 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1))) → 𝑖 ∈ (0...𝑁))
24464ad2antrr 761 . . . . . . . . . . . . . . . 16 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1))) → (𝑗 + 1) ∈ (0...𝑁))
245 isorel 6536 . . . . . . . . . . . . . . . 16 ((𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})) ∧ (𝑖 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑖 < (𝑗 + 1) ↔ (𝑆𝑖) < (𝑆‘(𝑗 + 1))))
246242, 243, 244, 245syl12anc 1321 . . . . . . . . . . . . . . 15 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1))) → (𝑖 < (𝑗 + 1) ↔ (𝑆𝑖) < (𝑆‘(𝑗 + 1))))
247241, 246mpbird 247 . . . . . . . . . . . . . 14 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1))) → 𝑖 < (𝑗 + 1))
248247adantrl 751 . . . . . . . . . . . . 13 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ ((𝑆𝑗) < (𝑆𝑖) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1)))) → 𝑖 < (𝑗 + 1))
249 btwnnz 11405 . . . . . . . . . . . . 13 ((𝑗 ∈ ℤ ∧ 𝑗 < 𝑖𝑖 < (𝑗 + 1)) → ¬ 𝑖 ∈ ℤ)
250232, 240, 248, 249syl3anc 1323 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ ((𝑆𝑗) < (𝑆𝑖) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1)))) → ¬ 𝑖 ∈ ℤ)
251231, 250pm2.65da 599 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) → ¬ ((𝑆𝑗) < (𝑆𝑖) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1))))
252228, 229, 251syl2anc 692 . . . . . . . . . 10 (((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆𝑖) = ((𝑆𝑗) + 𝑇)) → ¬ ((𝑆𝑗) < (𝑆𝑖) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1))))
253227, 252pm2.65da 599 . . . . . . . . 9 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) ∧ 𝑖 ∈ (0...𝑁)) → ¬ (𝑆𝑖) = ((𝑆𝑗) + 𝑇))
254253nrexdv 2996 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → ¬ ∃𝑖 ∈ (0...𝑁)(𝑆𝑖) = ((𝑆𝑗) + 𝑇))
255254adantlr 750 . . . . . . 7 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇)) → ¬ ∃𝑖 ∈ (0...𝑁)(𝑆𝑖) = ((𝑆𝑗) + 𝑇))
256219, 255condan 834 . . . . . 6 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇))
25761rexrd 10041 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝑆𝑗) ∈ ℝ*)
25884ad2antrr 761 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝑇 ∈ ℝ)
25961, 258readdcld 10021 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝑆𝑗) + 𝑇) ∈ ℝ)
260 elioc2 12186 . . . . . . 7 (((𝑆𝑗) ∈ ℝ* ∧ ((𝑆𝑗) + 𝑇) ∈ ℝ) → ((𝑆‘(𝑗 + 1)) ∈ ((𝑆𝑗)(,]((𝑆𝑗) + 𝑇)) ↔ ((𝑆‘(𝑗 + 1)) ∈ ℝ ∧ (𝑆𝑗) < (𝑆‘(𝑗 + 1)) ∧ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇))))
261257, 259, 260syl2anc 692 . . . . . 6 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝑆‘(𝑗 + 1)) ∈ ((𝑆𝑗)(,]((𝑆𝑗) + 𝑇)) ↔ ((𝑆‘(𝑗 + 1)) ∈ ℝ ∧ (𝑆𝑗) < (𝑆‘(𝑗 + 1)) ∧ (𝑆‘(𝑗 + 1)) ≤ ((𝑆𝑗) + 𝑇))))
26266, 76, 256, 261mpbir3and 1243 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝑆‘(𝑗 + 1)) ∈ ((𝑆𝑗)(,]((𝑆𝑗) + 𝑇)))
26356, 59, 60, 15, 16, 61, 62, 262fourierdlem26 39683 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) = (𝐴 + ((𝑆‘(𝑗 + 1)) − (𝑆𝑗))))
264263oveq1d 6625 . . 3 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝐸‘(𝑆‘(𝑗 + 1))) − 𝐴) = ((𝐴 + ((𝑆‘(𝑗 + 1)) − (𝑆𝑗))) − 𝐴))
26556recnd 10020 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐴 ∈ ℂ)
26665recnd 10020 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℂ)
267266, 138subcld 10344 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) ∈ ℂ)
268267adantr 481 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) ∈ ℂ)
269265, 268pncan2d 10346 . . 3 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝐴 + ((𝑆‘(𝑗 + 1)) − (𝑆𝑗))) − 𝐴) = ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)))
27058, 264, 2693eqtrd 2659 . 2 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐿‘(𝐸‘(𝑆𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)))
2711a1i 11 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
272 eqcom 2628 . . . . . . . . . . . 12 (𝑦 = (𝐸‘(𝑆𝑗)) ↔ (𝐸‘(𝑆𝑗)) = 𝑦)
273272biimpi 206 . . . . . . . . . . 11 (𝑦 = (𝐸‘(𝑆𝑗)) → (𝐸‘(𝑆𝑗)) = 𝑦)
274273adantl 482 . . . . . . . . . 10 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → (𝐸‘(𝑆𝑗)) = 𝑦)
275 neqne 2798 . . . . . . . . . . 11 (¬ (𝐸‘(𝑆𝑗)) = 𝐵 → (𝐸‘(𝑆𝑗)) ≠ 𝐵)
276275adantr 481 . . . . . . . . . 10 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → (𝐸‘(𝑆𝑗)) ≠ 𝐵)
277274, 276eqnetrrd 2858 . . . . . . . . 9 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → 𝑦𝐵)
278277neneqd 2795 . . . . . . . 8 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → ¬ 𝑦 = 𝐵)
279278iffalsed 4074 . . . . . . 7 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝑦)
280 simpr 477 . . . . . . 7 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → 𝑦 = (𝐸‘(𝑆𝑗)))
281279, 280eqtrd 2655 . . . . . 6 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = (𝐸‘(𝑆𝑗)))
282281adantll 749 . . . . 5 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ 𝑦 = (𝐸‘(𝑆𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = (𝐸‘(𝑆𝑗)))
28354adantr 481 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) ∈ (𝐴(,]𝐵))
284271, 282, 283, 283fvmptd 6250 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆𝑗))) = (𝐸‘(𝑆𝑗)))
285284oveq2d 6626 . . 3 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐿‘(𝐸‘(𝑆𝑗)))) = ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐸‘(𝑆𝑗))))
286 id 22 . . . . . . . 8 (𝑥 = (𝑆‘(𝑗 + 1)) → 𝑥 = (𝑆‘(𝑗 + 1)))
287 oveq2 6618 . . . . . . . . . . 11 (𝑥 = (𝑆‘(𝑗 + 1)) → (𝐵𝑥) = (𝐵 − (𝑆‘(𝑗 + 1))))
288287oveq1d 6625 . . . . . . . . . 10 (𝑥 = (𝑆‘(𝑗 + 1)) → ((𝐵𝑥) / 𝑇) = ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇))
289288fveq2d 6157 . . . . . . . . 9 (𝑥 = (𝑆‘(𝑗 + 1)) → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)))
290289oveq1d 6625 . . . . . . . 8 (𝑥 = (𝑆‘(𝑗 + 1)) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇))
291286, 290oveq12d 6628 . . . . . . 7 (𝑥 = (𝑆‘(𝑗 + 1)) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)))
292291adantl 482 . . . . . 6 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑥 = (𝑆‘(𝑗 + 1))) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)))
293128, 65resubcld 10410 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝑆‘(𝑗 + 1))) ∈ ℝ)
294293, 101rerpdivcld 11855 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) ∈ ℝ)
295294flcld 12547 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ∈ ℤ)
296295zred 11434 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ∈ ℝ)
297296, 85remulcld 10022 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇) ∈ ℝ)
29865, 297readdcld 10021 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)) ∈ ℝ)
299120, 292, 65, 298fvmptd 6250 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘(𝑗 + 1))) = ((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)))
300299, 135oveq12d 6628 . . . 4 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐸‘(𝑆𝑗))) = (((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)) − ((𝑆𝑗) + ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇))))
301300adantr 481 . . 3 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐸‘(𝑆𝑗))) = (((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)) − ((𝑆𝑗) + ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇))))
302 flle 12548 . . . . . . . . . . . . 13 (((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) ∈ ℝ → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ≤ ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇))
303294, 302syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ≤ ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇))
30453, 65, 75ltled 10137 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ≤ (𝑆‘(𝑗 + 1)))
30553, 65, 128, 304lesub2dd 10596 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝑆‘(𝑗 + 1))) ≤ (𝐵 − (𝑆𝑗)))
306293, 129, 101, 305lediv1dd 11882 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇))
307296, 294, 130, 303, 306letrd 10146 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇))
308307adantr 481 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇))
309296adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝐵 − (𝑆𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ∈ ℝ)
310 1red 10007 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝐵 − (𝑆𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → 1 ∈ ℝ)
311309, 310readdcld 10021 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝐵 − (𝑆𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ∈ ℝ)
312130adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝐵 − (𝑆𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → ((𝐵 − (𝑆𝑗)) / 𝑇) ∈ ℝ)
313 simpr 477 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝐵 − (𝑆𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → ¬ ((𝐵 − (𝑆𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1))
314311, 312, 313nltled 10139 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝐵 − (𝑆𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇))
315314adantlr 750 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ ((𝐵 − (𝑆𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇))
31679ad3antrrr 765 . . . . . . . . . . . . . 14 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → 𝑆:(0...𝑁)–onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄}))
31788ad2antrr 761 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → 𝐶 ∈ ℝ)
31892ad2antrr 761 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → 𝐷 ∈ ℝ)
319 fourierdlem65.z . . . . . . . . . . . . . . . . . . 19 𝑍 = ((𝑆𝑗) + (𝐵 − (𝐸‘(𝑆𝑗))))
320135, 134eqeltrd 2698 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆𝑗)) ∈ ℝ)
321128, 320resubcld 10410 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝐸‘(𝑆𝑗))) ∈ ℝ)
32253, 321readdcld 10021 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + (𝐵 − (𝐸‘(𝑆𝑗)))) ∈ ℝ)
323319, 322syl5eqel 2702 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ℝ)
324323ad2antrr 761 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → 𝑍 ∈ ℝ)
32512rexrd 10041 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐴 ∈ ℝ*)
326325adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ*)
327 elioc2 12186 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → ((𝐸‘(𝑆𝑗)) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘(𝑆𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆𝑗)) ∧ (𝐸‘(𝑆𝑗)) ≤ 𝐵)))
328326, 128, 327syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆𝑗)) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘(𝑆𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆𝑗)) ∧ (𝐸‘(𝑆𝑗)) ≤ 𝐵)))
32954, 328mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆𝑗)) ∧ (𝐸‘(𝑆𝑗)) ≤ 𝐵))
330329simp3d 1073 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆𝑗)) ≤ 𝐵)
331128, 320subge0d 10569 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0..^𝑁)) → (0 ≤ (𝐵 − (𝐸‘(𝑆𝑗))) ↔ (𝐸‘(𝑆𝑗)) ≤ 𝐵))
332330, 331mpbird 247 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 ≤ (𝐵 − (𝐸‘(𝑆𝑗))))
33353, 321addge01d 10567 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0..^𝑁)) → (0 ≤ (𝐵 − (𝐸‘(𝑆𝑗))) ↔ (𝑆𝑗) ≤ ((𝑆𝑗) + (𝐵 − (𝐸‘(𝑆𝑗))))))
334332, 333mpbid 222 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ≤ ((𝑆𝑗) + (𝐵 − (𝐸‘(𝑆𝑗)))))
33588, 53, 322, 96, 334letrd 10146 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐶 ≤ ((𝑆𝑗) + (𝐵 − (𝐸‘(𝑆𝑗)))))
336335, 319syl6breqr 4660 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐶𝑍)
337336ad2antrr 761 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → 𝐶𝑍)
33865ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
339294ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) ∈ ℝ)
340 reflcl 12545 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) ∈ ℝ → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ∈ ℝ)
341 peano2re 10161 . . . . . . . . . . . . . . . . . . . . . . 23 ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ∈ ℝ → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ∈ ℝ)
342339, 340, 3413syl 18 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ∈ ℝ)
343128ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → 𝐵 ∈ ℝ)
344343, 324resubcld 10410 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → (𝐵𝑍) ∈ ℝ)
345101ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → 𝑇 ∈ ℝ+)
346344, 345rerpdivcld 11855 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → ((𝐵𝑍) / 𝑇) ∈ ℝ)
347 flltp1 12549 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) ∈ ℝ → ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1))
348294, 347syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1))
349348ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1))
350295peano2zd 11437 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0..^𝑁)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ∈ ℤ)
351350ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ∈ ℤ)
352130ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → ((𝐵 − (𝑆𝑗)) / 𝑇) ∈ ℝ)
353 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇))
354321, 101rerpdivcld 11855 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝐸‘(𝑆𝑗))) / 𝑇) ∈ ℝ)
355354ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → ((𝐵 − (𝐸‘(𝑆𝑗))) / 𝑇) ∈ ℝ)
35612adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ)
357329simp2d 1072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐴 < (𝐸‘(𝑆𝑗)))
358356, 320, 128, 357ltsub2dd 10592 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝐸‘(𝑆𝑗))) < (𝐵𝐴))
359358, 15syl6breqr 4660 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝐸‘(𝑆𝑗))) < 𝑇)
360321, 85, 101, 359ltdiv1dd 11881 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝐸‘(𝑆𝑗))) / 𝑇) < (𝑇 / 𝑇))
361143, 144dividd 10751 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑇 / 𝑇) = 1)
362360, 361breqtrd 4644 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝐸‘(𝑆𝑗))) / 𝑇) < 1)
363362ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → ((𝐵 − (𝐸‘(𝑆𝑗))) / 𝑇) < 1)
364129recnd 10020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝑆𝑗)) ∈ ℂ)
365321recnd 10020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝐸‘(𝑆𝑗))) ∈ ℂ)
366364, 365, 143, 144divsubdird 10792 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝑆𝑗)) − (𝐵 − (𝐸‘(𝑆𝑗)))) / 𝑇) = (((𝐵 − (𝑆𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆𝑗))) / 𝑇)))
367366eqcomd 2627 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝑆𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆𝑗))) / 𝑇)) = (((𝐵 − (𝑆𝑗)) − (𝐵 − (𝐸‘(𝑆𝑗)))) / 𝑇))
368128recnd 10020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐵 ∈ ℂ)
369320recnd 10020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆𝑗)) ∈ ℂ)
370368, 138, 369nnncan1d 10378 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝑆𝑗)) − (𝐵 − (𝐸‘(𝑆𝑗)))) = ((𝐸‘(𝑆𝑗)) − (𝑆𝑗)))
371370oveq1d 6625 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝑆𝑗)) − (𝐵 − (𝐸‘(𝑆𝑗)))) / 𝑇) = (((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇))
372367, 371eqtrd 2655 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝑆𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆𝑗))) / 𝑇)) = (((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇))
373372, 147eqeltrd 2698 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝑆𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆𝑗))) / 𝑇)) ∈ ℤ)
374373ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → (((𝐵 − (𝑆𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆𝑗))) / 𝑇)) ∈ ℤ)
375351, 352, 353, 355, 363, 374zltlesub 38992 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ (((𝐵 − (𝑆𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆𝑗))) / 𝑇)))
376319a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑍 = ((𝑆𝑗) + (𝐵 − (𝐸‘(𝑆𝑗)))))
377376oveq2d 6626 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐵𝑍) = (𝐵 − ((𝑆𝑗) + (𝐵 − (𝐸‘(𝑆𝑗))))))
378138, 368, 369addsub12d 10367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + (𝐵 − (𝐸‘(𝑆𝑗)))) = (𝐵 + ((𝑆𝑗) − (𝐸‘(𝑆𝑗)))))
379368, 369, 138subsub2d 10373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐵 − ((𝐸‘(𝑆𝑗)) − (𝑆𝑗))) = (𝐵 + ((𝑆𝑗) − (𝐸‘(𝑆𝑗)))))
380378, 379eqtr4d 2658 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + (𝐵 − (𝐸‘(𝑆𝑗)))) = (𝐵 − ((𝐸‘(𝑆𝑗)) − (𝑆𝑗))))
381380oveq2d 6626 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐵 − ((𝑆𝑗) + (𝐵 − (𝐸‘(𝑆𝑗))))) = (𝐵 − (𝐵 − ((𝐸‘(𝑆𝑗)) − (𝑆𝑗)))))
382369, 138subcld 10344 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) ∈ ℂ)
383368, 382nncand 10349 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝐵 − ((𝐸‘(𝑆𝑗)) − (𝑆𝑗)))) = ((𝐸‘(𝑆𝑗)) − (𝑆𝑗)))
384377, 381, 3833eqtrd 2659 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐵𝑍) = ((𝐸‘(𝑆𝑗)) − (𝑆𝑗)))
385384oveq1d 6625 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐵𝑍) / 𝑇) = (((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇))
386371, 367, 3853eqtr4d 2665 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝑆𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆𝑗))) / 𝑇)) = ((𝐵𝑍) / 𝑇))
387386ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → (((𝐵 − (𝑆𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆𝑗))) / 𝑇)) = ((𝐵𝑍) / 𝑇))
388375, 387breqtrd 4644 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵𝑍) / 𝑇))
389339, 342, 346, 349, 388ltletrd 10149 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) < ((𝐵𝑍) / 𝑇))
390293ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → (𝐵 − (𝑆‘(𝑗 + 1))) ∈ ℝ)
391390, 344, 345ltdiv1d 11869 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → ((𝐵 − (𝑆‘(𝑗 + 1))) < (𝐵𝑍) ↔ ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) < ((𝐵𝑍) / 𝑇)))
392389, 391mpbird 247 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → (𝐵 − (𝑆‘(𝑗 + 1))) < (𝐵𝑍))
393324, 338, 343ltsub2d 10589 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → (𝑍 < (𝑆‘(𝑗 + 1)) ↔ (𝐵 − (𝑆‘(𝑗 + 1))) < (𝐵𝑍)))
394392, 393mpbird 247 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → 𝑍 < (𝑆‘(𝑗 + 1)))
395114ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → (𝑆‘(𝑗 + 1)) ≤ 𝐷)
396324, 338, 318, 394, 395ltletrd 10149 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → 𝑍 < 𝐷)
397324, 318, 396ltled 10137 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → 𝑍𝐷)
398317, 318, 324, 337, 397eliccd 39168 . . . . . . . . . . . . . . . 16 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → 𝑍 ∈ (𝐶[,]𝐷))
39930a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐵𝐴) = 𝑇)
400399oveq2d 6626 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0..^𝑁)) → ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · (𝐵𝐴)) = ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · 𝑇))
401382, 143, 144divcan1d 10754 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0..^𝑁)) → ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · 𝑇) = ((𝐸‘(𝑆𝑗)) − (𝑆𝑗)))
402400, 401eqtrd 2655 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0..^𝑁)) → ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · (𝐵𝐴)) = ((𝐸‘(𝑆𝑗)) − (𝑆𝑗)))
403376, 402oveq12d 6628 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑍 + ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · (𝐵𝐴))) = (((𝑆𝑗) + (𝐵 − (𝐸‘(𝑆𝑗)))) + ((𝐸‘(𝑆𝑗)) − (𝑆𝑗))))
404138, 365addcomd 10190 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + (𝐵 − (𝐸‘(𝑆𝑗)))) = ((𝐵 − (𝐸‘(𝑆𝑗))) + (𝑆𝑗)))
405404oveq1d 6625 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆𝑗) + (𝐵 − (𝐸‘(𝑆𝑗)))) + ((𝐸‘(𝑆𝑗)) − (𝑆𝑗))) = (((𝐵 − (𝐸‘(𝑆𝑗))) + (𝑆𝑗)) + ((𝐸‘(𝑆𝑗)) − (𝑆𝑗))))
406365, 138, 369ppncand 10384 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝐸‘(𝑆𝑗))) + (𝑆𝑗)) + ((𝐸‘(𝑆𝑗)) − (𝑆𝑗))) = ((𝐵 − (𝐸‘(𝑆𝑗))) + (𝐸‘(𝑆𝑗))))
407368, 369npcand 10348 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝐸‘(𝑆𝑗))) + (𝐸‘(𝑆𝑗))) = 𝐵)
408406, 407eqtrd 2655 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝐸‘(𝑆𝑗))) + (𝑆𝑗)) + ((𝐸‘(𝑆𝑗)) − (𝑆𝑗))) = 𝐵)
409403, 405, 4083eqtrd 2659 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑍 + ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · (𝐵𝐴))) = 𝐵)
410199adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐵 ∈ ran 𝑄)
411409, 410eqeltrd 2698 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑍 + ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · (𝐵𝐴))) ∈ ran 𝑄)
412 oveq1 6617 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = (((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) → (𝑘 · (𝐵𝐴)) = ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · (𝐵𝐴)))
413412oveq2d 6626 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = (((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) → (𝑍 + (𝑘 · (𝐵𝐴))) = (𝑍 + ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · (𝐵𝐴))))
414413eleq1d 2683 . . . . . . . . . . . . . . . . . . 19 (𝑘 = (((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) → ((𝑍 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄 ↔ (𝑍 + ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · (𝐵𝐴))) ∈ ran 𝑄))
415414rspcev 3298 . . . . . . . . . . . . . . . . . 18 (((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) ∈ ℤ ∧ (𝑍 + ((((𝐸‘(𝑆𝑗)) − (𝑆𝑗)) / 𝑇) · (𝐵𝐴))) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (𝑍 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄)
416147, 411, 415syl2anc 692 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → ∃𝑘 ∈ ℤ (𝑍 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄)
417416ad2antrr 761 . . . . . . . . . . . . . . . 16 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → ∃𝑘 ∈ ℤ (𝑍 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄)
418 oveq1 6617 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑍 → (𝑦 + (𝑘 · (𝐵𝐴))) = (𝑍 + (𝑘 · (𝐵𝐴))))
419418eleq1d 2683 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑍 → ((𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄 ↔ (𝑍 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄))
420419rexbidv 3046 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑍 → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑍 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄))
421420elrab 3350 . . . . . . . . . . . . . . . 16 (𝑍 ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄} ↔ (𝑍 ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (𝑍 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄))
422398, 417, 421sylanbrc 697 . . . . . . . . . . . . . . 15 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → 𝑍 ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})
423 elun2 3764 . . . . . . . . . . . . . . 15 (𝑍 ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄} → 𝑍 ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄}))
424422, 423syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → 𝑍 ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄}))
425 foelrn 6339 . . . . . . . . . . . . . 14 ((𝑆:(0...𝑁)–onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄}) ∧ 𝑍 ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})) → ∃𝑖 ∈ (0...𝑁)𝑍 = (𝑆𝑖))
426316, 424, 425syl2anc 692 . . . . . . . . . . . . 13 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → ∃𝑖 ∈ (0...𝑁)𝑍 = (𝑆𝑖))
42753adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝑆𝑗) ∈ ℝ)
428321adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐵 − (𝐸‘(𝑆𝑗))) ∈ ℝ)
429320adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) ∈ ℝ)
43013ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐵 ∈ ℝ)
431330adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) ≤ 𝐵)
432275necomd 2845 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ (𝐸‘(𝑆𝑗)) = 𝐵𝐵 ≠ (𝐸‘(𝑆𝑗)))
433432adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐵 ≠ (𝐸‘(𝑆𝑗)))
434429, 430, 431, 433leneltd 10143 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) < 𝐵)
435429, 430posdifd 10566 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝐸‘(𝑆𝑗)) < 𝐵 ↔ 0 < (𝐵 − (𝐸‘(𝑆𝑗)))))
436434, 435mpbid 222 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → 0 < (𝐵 − (𝐸‘(𝑆𝑗))))
437428, 436elrpd 11821 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐵 − (𝐸‘(𝑆𝑗))) ∈ ℝ+)
438427, 437ltaddrpd 11857 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝑆𝑗) < ((𝑆𝑗) + (𝐵 − (𝐸‘(𝑆𝑗)))))
439438, 319syl6breqr 4660 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝑆𝑗) < 𝑍)
440439ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) ∧ 𝑍 = (𝑆𝑖)) → (𝑆𝑗) < 𝑍)
441 simpr 477 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) ∧ 𝑍 = (𝑆𝑖)) → 𝑍 = (𝑆𝑖))
442440, 441breqtrd 4644 . . . . . . . . . . . . . . . 16 (((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) ∧ 𝑍 = (𝑆𝑖)) → (𝑆𝑗) < (𝑆𝑖))
443394adantr 481 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) ∧ 𝑍 = (𝑆𝑖)) → 𝑍 < (𝑆‘(𝑗 + 1)))
444441, 443eqbrtrrd 4642 . . . . . . . . . . . . . . . 16 (((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) ∧ 𝑍 = (𝑆𝑖)) → (𝑆𝑖) < (𝑆‘(𝑗 + 1)))
445442, 444jca 554 . . . . . . . . . . . . . . 15 (((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) ∧ 𝑍 = (𝑆𝑖)) → ((𝑆𝑗) < (𝑆𝑖) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1))))
446445ex 450 . . . . . . . . . . . . . 14 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → (𝑍 = (𝑆𝑖) → ((𝑆𝑗) < (𝑆𝑖) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1)))))
447446reximdv 3011 . . . . . . . . . . . . 13 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → (∃𝑖 ∈ (0...𝑁)𝑍 = (𝑆𝑖) → ∃𝑖 ∈ (0...𝑁)((𝑆𝑗) < (𝑆𝑖) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1)))))
448426, 447mpd 15 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇)) → ∃𝑖 ∈ (0...𝑁)((𝑆𝑗) < (𝑆𝑖) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1))))
449315, 448syldan 487 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ ((𝐵 − (𝑆𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → ∃𝑖 ∈ (0...𝑁)((𝑆𝑗) < (𝑆𝑖) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1))))
450251nrexdv 2996 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → ¬ ∃𝑖 ∈ (0...𝑁)((𝑆𝑗) < (𝑆𝑖) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1))))
451450ad2antrr 761 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ ((𝐵 − (𝑆𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → ¬ ∃𝑖 ∈ (0...𝑁)((𝑆𝑗) < (𝑆𝑖) ∧ (𝑆𝑖) < (𝑆‘(𝑗 + 1))))
452449, 451condan 834 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝐵 − (𝑆𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1))
453308, 452jca 554 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇) ∧ ((𝐵 − (𝑆𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)))
454130adantr 481 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝐵 − (𝑆𝑗)) / 𝑇) ∈ ℝ)
455295adantr 481 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ∈ ℤ)
456 flbi 12565 . . . . . . . . . 10 ((((𝐵 − (𝑆𝑗)) / 𝑇) ∈ ℝ ∧ (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ∈ ℤ) → ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ↔ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇) ∧ ((𝐵 − (𝑆𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1))))
457454, 455, 456syl2anc 692 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ↔ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ≤ ((𝐵 − (𝑆𝑗)) / 𝑇) ∧ ((𝐵 − (𝑆𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1))))
458453, 457mpbird 247 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)))
459458eqcomd 2627 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) = (⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)))
460459oveq1d 6625 . . . . . 6 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇))
461460oveq2d 6626 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)) = ((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇)))
462461oveq1d 6625 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)) − ((𝑆𝑗) + ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇))) = (((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇)) − ((𝑆𝑗) + ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇))))
463266adantr 481 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝑆‘(𝑗 + 1)) ∈ ℂ)
464138adantr 481 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝑆𝑗) ∈ ℂ)
465139adantr 481 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇) ∈ ℂ)
466463, 464, 465pnpcan2d 10382 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇)) − ((𝑆𝑗) + ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇))) = ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)))
467462, 466eqtrd 2655 . . 3 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)) − ((𝑆𝑗) + ((⌊‘((𝐵 − (𝑆𝑗)) / 𝑇)) · 𝑇))) = ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)))
468285, 301, 4673eqtrd 2659 . 2 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐿‘(𝐸‘(𝑆𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)))
469270, 468pm2.61dan 831 1 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐿‘(𝐸‘(𝑆𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987   ≠ wne 2790  ∀wral 2907  ∃wrex 2908  {crab 2911   ∪ cun 3557  ifcif 4063  {cpr 4155   class class class wbr 4618   ↦ cmpt 4678  ran crn 5080  ℩cio 5813   Fn wfn 5847  ⟶wf 5848  –onto→wfo 5850  –1-1-onto→wf1o 5851  ‘cfv 5852   Isom wiso 5853  (class class class)co 6610   ↑𝑚 cmap 7809  ℂcc 9886  ℝcr 9887  0cc0 9888  1c1 9889   + caddc 9891   · cmul 9893  +∞cpnf 10023  ℝ*cxr 10025   < clt 10026   ≤ cle 10027   − cmin 10218   / cdiv 10636  ℕcn 10972  ℕ0cn0 11244  ℤcz 11329  ℤ≥cuz 11639  ℝ+crp 11784  (,)cioo 12125  (,]cioc 12126  [,]cicc 12128  ...cfz 12276  ..^cfzo 12414  ⌊cfl 12539  #chash 13065 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8490  ax-cnex 9944  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-mulcom 9952  ax-addass 9953  ax-mulass 9954  ax-distr 9955  ax-i2m1 9956  ax-1ne0 9957  ax-1rid 9958  ax-rnegex 9959  ax-rrecex 9960  ax-cnre 9961  ax-pre-lttri 9962  ax-pre-lttrn 9963  ax-pre-ltadd 9964  ax-pre-mulgt0 9965  ax-pre-sup 9966 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-er 7694  df-map 7811  df-en 7908  df-dom 7909  df-sdom 7910  df-fin 7911  df-fi 8269  df-sup 8300  df-inf 8301  df-oi 8367  df-card 8717  df-cda 8942  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-sub 10220  df-neg 10221  df-div 10637  df-nn 10973  df-2 11031  df-3 11032  df-n0 11245  df-xnn0 11316  df-z 11330  df-uz 11640  df-q 11741  df-rp 11785  df-xneg 11898  df-xadd 11899  df-xmul 11900  df-ioo 12129  df-ioc 12130  df-icc 12132  df-fz 12277  df-fzo 12415  df-fl 12541  df-seq 12750  df-exp 12809  df-hash 13066  df-cj 13781  df-re 13782  df-im 13783  df-sqrt 13917  df-abs 13918  df-rest 16015  df-topgen 16036  df-psmet 19670  df-xmet 19671  df-met 19672  df-bl 19673  df-mopn 19674  df-top 20631  df-topon 20648  df-bases 20674  df-cld 20746  df-ntr 20747  df-cls 20748  df-nei 20825  df-lp 20863  df-cmp 21113 This theorem is referenced by:  fourierdlem89  39745  fourierdlem90  39746  fourierdlem91  39747
 Copyright terms: Public domain W3C validator