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

Theorem fourierdlem49 47301
Description: The given periodic function 𝐹 has a left limit at every point in the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem49.a (𝜑 → 𝐴 ∈ ℝ)
fourierdlem49.b (𝜑 → 𝐵 ∈ ℝ)
fourierdlem49.altb (𝜑 → 𝐴 < 𝐵)
fourierdlem49.p 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem49.t 𝑇 = (𝐵 − 𝐴)
fourierdlem49.m (𝜑 → 𝑀 ∈ ℕ)
fourierdlem49.q (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
fourierdlem49.d (𝜑 → 𝐷 ⊆ ℝ)
fourierdlem49.f (𝜑 → 𝐹:𝐷⟶ℝ)
fourierdlem49.dper ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)
fourierdlem49.per ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥))
fourierdlem49.cn ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
fourierdlem49.l ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))))
fourierdlem49.x (𝜑 → 𝑋 ∈ ℝ)
fourierdlem49.z 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
fourierdlem49.e 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥)))
Assertion
Ref Expression
fourierdlem49 (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) ≠ ∅)
Distinct variable groups:   𝐴,𝑖,𝑚,𝑝   𝑥,𝐴,𝑖   𝐵,𝑖,𝑘   𝐵,𝑚,𝑝   𝑥,𝐵,𝑘   𝐷,𝑘,𝑥   𝑖,𝐸,𝑘,𝑥   𝑖,𝐹,𝑘,𝑥   𝑖,𝑀,𝑘   𝑚,𝑀,𝑝   𝑥,𝑀   𝑄,𝑖,𝑘   𝑄,𝑝   𝑥,𝑄   𝑇,𝑘,𝑥   𝑖,𝑋,𝑘,𝑥   𝑘,𝑍,𝑥   𝜑,𝑖,𝑘,𝑥
Allowed substitution hints:   𝜑(𝑚, 𝑝)   𝐴(𝑘)   𝐷(𝑖, 𝑚, 𝑝)   𝑃(𝑥, 𝑖, 𝑘, 𝑚, 𝑝)   𝑄(𝑚)   𝑇(𝑖, 𝑚, 𝑝)   𝐸(𝑚, 𝑝)   𝐹(𝑚, 𝑝)   𝐿(𝑥, 𝑖, 𝑘, 𝑚, 𝑝)   𝑋(𝑚, 𝑝)   𝑍(𝑖, 𝑚, 𝑝)

Proof of Theorem fourierdlem49
Dummy variables 𝑗 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem49.a . . . . . 6 (𝜑 → 𝐴 ∈ ℝ)
2 fourierdlem49.b . . . . . 6 (𝜑 → 𝐵 ∈ ℝ)
3 fourierdlem49.altb . . . . . 6 (𝜑 → 𝐴 < 𝐵)
4 fourierdlem49.t . . . . . 6 𝑇 = (𝐵 − 𝐴)
5 fourierdlem49.e . . . . . . 7 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥)))
6 ovex 7457 . . . . . . . . . 10 ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ V
7 fourierdlem49.z . . . . . . . . . . 11 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
87fvmpt2 7010 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ V) → (𝑍‘𝑥) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
96, 8mpan2 704 . . . . . . . . 9 (𝑥 ∈ ℝ → (𝑍‘𝑥) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
109oveq2d 7440 . . . . . . . 8 (𝑥 ∈ ℝ → (𝑥 + (𝑍‘𝑥)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
1110mpteq2ia 5199 . . . . . . 7 (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
125, 11eqtri 2783 . . . . . 6 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
131, 2, 3, 4, 12fourierdlem4 47257 . . . . 5 (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
14 fourierdlem49.x . . . . 5 (𝜑 → 𝑋 ∈ ℝ)
1513, 14ffvelcdmd 7090 . . . 4 (𝜑 → (𝐸‘𝑋) ∈ (𝐴(,]𝐵))
16 simpr 490 . . . . . . 7 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (𝐸‘𝑋) ∈ ran 𝑄)
17 fourierdlem49.q . . . . . . . . . . . . 13 (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
18 fourierdlem49.m . . . . . . . . . . . . . 14 (𝜑 → 𝑀 ∈ ℕ)
19 fourierdlem49.p . . . . . . . . . . . . . . 15 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
2019fourierdlem2 47255 . . . . . . . . . . . . . 14 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
2118, 20syl 18 . . . . . . . . . . . . 13 (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
2217, 21mpbid 235 . . . . . . . . . . . 12 (𝜑 → (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
2322simpld 500 . . . . . . . . . . 11 (𝜑 → 𝑄 ∈ (ℝ ↑m (0...𝑀)))
24 elmapi 8877 . . . . . . . . . . 11 (𝑄 ∈ (ℝ ↑m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
2523, 24syl 18 . . . . . . . . . 10 (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
2625ffnd 6715 . . . . . . . . 9 (𝜑 → 𝑄 Fn (0...𝑀))
2726ad2antrr 739 . . . . . . . 8 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → 𝑄 Fn (0...𝑀))
28 fvelrnb 6950 . . . . . . . 8 (𝑄 Fn (0...𝑀) → ((𝐸‘𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋)))
2927, 28syl 18 . . . . . . 7 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ((𝐸‘𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋)))
3016, 29mpbid 235 . . . . . 6 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋))
31 fveq2 6890 . . . . . . . . . . . 12 (𝑖 = (𝑗 − 1) → (𝑄‘𝑖) = (𝑄‘(𝑗 − 1)))
32 fvoveq1 7447 . . . . . . . . . . . 12 (𝑖 = (𝑗 − 1) → (𝑄‘(𝑖 + 1)) = (𝑄‘((𝑗 − 1) + 1)))
3331, 32oveq12d 7442 . . . . . . . . . . 11 (𝑖 = (𝑗 − 1) → ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
3433eleq2d 2846 . . . . . . . . . 10 (𝑖 = (𝑗 − 1) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) ↔ (𝐸‘𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))))
35 nnuz 13011 . . . . . . . . . . . . . 14 ℕ = (ℤ≥‘1)
36 1zzd 12734 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 1 ∈ ℤ)
37 elfzelz 13663 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
3837ad2antlr 740 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ ℤ)
39 1e0p1 12868 . . . . . . . . . . . . . . 15 1 = (0 + 1)
4038zred 12810 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ ℝ)
41 elfzle1 13667 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
4241ad2antlr 740 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 ≤ 𝑗)
43 id 23 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑄‘𝑗) = (𝐸‘𝑋) → (𝑄‘𝑗) = (𝐸‘𝑋))
4443eqcomd 2766 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑄‘𝑗) = (𝐸‘𝑋) → (𝐸‘𝑋) = (𝑄‘𝑗))
4544ad2antlr 740 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑗 = 0) → (𝐸‘𝑋) = (𝑄‘𝑗))
46 fveq2 6890 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 0 → (𝑄‘𝑗) = (𝑄‘0))
4746adantl 487 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑗 = 0) → (𝑄‘𝑗) = (𝑄‘0))
4822simprld 784 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
4948simpld 500 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑄‘0) = 𝐴)
5049ad2antrr 739 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑗 = 0) → (𝑄‘0) = 𝐴)
5145, 47, 503eqtrd 2799 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑗 = 0) → (𝐸‘𝑋) = 𝐴)
5251adantllr 732 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑗 = 0) → (𝐸‘𝑋) = 𝐴)
5352adantllr 732 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑗 = 0) → (𝐸‘𝑋) = 𝐴)
541adantr 486 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 ∈ ℝ)
551rexrd 11366 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 𝐴 ∈ ℝ*)
5655adantr 486 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 ∈ ℝ*)
572rexrd 11366 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 𝐵 ∈ ℝ*)
5857adantr 486 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → 𝐵 ∈ ℝ*)
59 simpr 490 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → (𝐸‘𝑋) ∈ (𝐴(,]𝐵))
6056, 58, 59iocgtlbd 46717 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸‘𝑋))
6154, 60gtned 11452 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → (𝐸‘𝑋) ≠ 𝐴)
6261neneqd 2960 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → ¬ (𝐸‘𝑋) = 𝐴)
6362ad3antrrr 743 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑗 = 0) → ¬ (𝐸‘𝑋) = 𝐴)
6453, 63pm2.65da 829 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → ¬ 𝑗 = 0)
6564neqned 2962 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ≠ 0)
6640, 42, 65ne0gt0d 11454 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 < 𝑗)
67 0zd 12712 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 ∈ ℤ)
6867, 38zltp1led 12758 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
6966, 68mpbid 235 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (0 + 1) ≤ 𝑗)
7039, 69eqbrtrid 5139 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 1 ≤ 𝑗)
7135, 36, 38, 70eluzd 46555 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ ℕ)
72 nnm1nn0 12654 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ → (𝑗 − 1) ∈ ℕ0)
7371, 72syl 18 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ ℕ0)
74 nn0uz 13010 . . . . . . . . . . . 12 ℕ0 = (ℤ≥‘0)
7573, 74eleqtrdi 2870 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ (ℤ≥‘0))
7618nnzd 12726 . . . . . . . . . . . 12 (𝜑 → 𝑀 ∈ ℤ)
7776ad3antrrr 743 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑀 ∈ ℤ)
78 peano2zm 12746 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℤ → (𝑗 − 1) ∈ ℤ)
7937, 78syl 18 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℤ)
8079zred 12810 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
8137zred 12810 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
82 elfzel2 13661 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
8382zred 12810 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
8481ltm1d 12256 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑗)
85 elfzle2 13668 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀)
8680, 81, 83, 84, 85ltletrd 11477 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
8786ad2antlr 740 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) < 𝑀)
8875, 77, 87elfzod 13804 . . . . . . . . . 10 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ (0..^𝑀))
8925ad3antrrr 743 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑄:(0...𝑀)⟶ℝ)
9038, 78syl 18 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ ℤ)
9173nn0ge0d 12677 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 ≤ (𝑗 − 1))
9280, 83, 86ltled 11465 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ≤ 𝑀)
9392ad2antlr 740 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ≤ 𝑀)
9467, 77, 90, 91, 93elfzd 13654 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ (0...𝑀))
9589, 94ffvelcdmd 7090 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ)
9695rexrd 11366 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ*)
9725ffvelcdmda 7089 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ)
9897rexrd 11366 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ*)
9998adantlr 728 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ*)
10099adantr 486 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ∈ ℝ*)
101 iocssre 13565 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
10255, 2, 101syl2anc 596 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
103102sselda 3909 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → (𝐸‘𝑋) ∈ ℝ)
104103rexrd 11366 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → (𝐸‘𝑋) ∈ ℝ*)
105104ad2antrr 739 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ℝ*)
106 simplll 787 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝜑)
107 ovex 7457 . . . . . . . . . . . . . . . 16 (𝑗 − 1) ∈ V
108 eleq1 2848 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 − 1) → (𝑖 ∈ (0..^𝑀) ↔ (𝑗 − 1) ∈ (0..^𝑀)))
109108anbi2d 642 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 − 1) → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀))))
11031, 32breq12d 5115 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 − 1) → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1))))
111109, 110imbi12d 347 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 − 1) → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))))
11222simprrd 786 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
113112r19.21bi 3254 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
114107, 111, 113vtocl 3520 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
115106, 88, 114syl2anc 596 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
11637zcnd 12811 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
117 1cnd 11309 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 1 ∈ ℂ)
118116, 117npcand 11680 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → ((𝑗 − 1) + 1) = 𝑗)
119118eqcomd 2766 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → 𝑗 = ((𝑗 − 1) + 1))
120119fveq2d 6894 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → (𝑄‘𝑗) = (𝑄‘((𝑗 − 1) + 1)))
121120eqcomd 2766 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄‘𝑗))
122121ad2antlr 740 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄‘𝑗))
123115, 122breqtrd 5130 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘𝑗))
124 simpr 490 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) = (𝐸‘𝑋))
125123, 124breqtrd 5130 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) < (𝐸‘𝑋))
126102, 15sseldd 3910 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸‘𝑋) ∈ ℝ)
127126leidd 11889 . . . . . . . . . . . . . . 15 (𝜑 → (𝐸‘𝑋) ≤ (𝐸‘𝑋))
128127ad2antrr 739 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝐸‘𝑋))
12944adantl 487 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) = (𝑄‘𝑗))
130128, 129breqtrd 5130 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘𝑗))
131130adantllr 732 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘𝑗))
13296, 100, 105, 125, 131eliocd 46655 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘𝑗)))
133120oveq2d 7440 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → ((𝑄‘(𝑗 − 1))(,](𝑄‘𝑗)) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
134133ad2antlr 740 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → ((𝑄‘(𝑗 − 1))(,](𝑄‘𝑗)) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
135132, 134eleqtrd 2862 . . . . . . . . . 10 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
13634, 88, 135rspcedvdw 3579 . . . . . . . . 9 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
137136ex 418 . . . . . . . 8 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
138137adantlr 728 . . . . . . 7 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸‘𝑋) ∈ ran 𝑄) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
139138rexlimdva 3163 . . . . . 6 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
14030, 139mpd 16 . . . . 5 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
14118ad2antrr 739 . . . . . . 7 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → 𝑀 ∈ ℕ)
14225ad2antrr 739 . . . . . . 7 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ)
143 iocssicc 13575 . . . . . . . . . 10 (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵)
14449eqcomd 2766 . . . . . . . . . . 11 (𝜑 → 𝐴 = (𝑄‘0))
14548simprd 501 . . . . . . . . . . . 12 (𝜑 → (𝑄‘𝑀) = 𝐵)
146145eqcomd 2766 . . . . . . . . . . 11 (𝜑 → 𝐵 = (𝑄‘𝑀))
147144, 146oveq12d 7442 . . . . . . . . . 10 (𝜑 → (𝐴[,]𝐵) = ((𝑄‘0)[,](𝑄‘𝑀)))
148143, 147sseqtrid 3951 . . . . . . . . 9 (𝜑 → (𝐴(,]𝐵) ⊆ ((𝑄‘0)[,](𝑄‘𝑀)))
149148sselda 3909 . . . . . . . 8 ((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → (𝐸‘𝑋) ∈ ((𝑄‘0)[,](𝑄‘𝑀)))
150149adantr 486 . . . . . . 7 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → (𝐸‘𝑋) ∈ ((𝑄‘0)[,](𝑄‘𝑀)))
151 simpr 490 . . . . . . 7 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ¬ (𝐸‘𝑋) ∈ ran 𝑄)
152 fveq2 6890 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝑄‘𝑘) = (𝑄‘𝑗))
153152breq1d 5112 . . . . . . . . 9 (𝑘 = 𝑗 → ((𝑄‘𝑘) < (𝐸‘𝑋) ↔ (𝑄‘𝑗) < (𝐸‘𝑋)))
154153cbvrabv 3422 . . . . . . . 8 {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < (𝐸‘𝑋)} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < (𝐸‘𝑋)}
155154supeq1i 9446 . . . . . . 7 sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < (𝐸‘𝑋)}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < (𝐸‘𝑋)}, ℝ, < )
156141, 142, 150, 151, 155fourierdlem25 47278 . . . . . 6 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
157 ioossioc 46640 . . . . . . . . 9 ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))
158157sseli 3905 . . . . . . . 8 ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
159158a1i 11 . . . . . . 7 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
160159reximdva 3175 . . . . . 6 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
161156, 160mpd 16 . . . . 5 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
162140, 161pm2.61dan 825 . . . 4 ((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
16315, 162mpdan 700 . . 3 (𝜑 → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
164 resindm 6021 . . . . . . . . 9 (𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ dom 𝐹)) = (𝐹 ↾ (-∞(,)(𝐸‘𝑋)))
165 fourierdlem49.f . . . . . . . . . . . 12 (𝜑 → 𝐹:𝐷⟶ℝ)
166165fdmd 6725 . . . . . . . . . . 11 (𝜑 → dom 𝐹 = 𝐷)
167166ineq2d 4116 . . . . . . . . . 10 (𝜑 → ((-∞(,)(𝐸‘𝑋)) ∩ dom 𝐹) = ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷))
168167reseq2d 5971 . . . . . . . . 9 (𝜑 → (𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ dom 𝐹)) = (𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷)))
169164, 168eqtr3id 2809 . . . . . . . 8 (𝜑 → (𝐹 ↾ (-∞(,)(𝐸‘𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷)))
1701693ad2ant1 1151 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ (-∞(,)(𝐸‘𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷)))
171170oveq1d 7439 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) = ((𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷)) limℂ (𝐸‘𝑋)))
172 ax-resscn 11264 . . . . . . . . . . 11 ℝ ⊆ ℂ
173172a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ⊆ ℂ)
174165, 173fssd 6732 . . . . . . . . 9 (𝜑 → 𝐹:𝐷⟶ℂ)
1751743ad2ant1 1151 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐹:𝐷⟶ℂ)
176 inss2 4133 . . . . . . . . 9 ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ⊆ 𝐷
177176a1i 11 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ⊆ 𝐷)
178175, 177fssresd 6754 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷)):((-∞(,)(𝐸‘𝑋)) ∩ 𝐷)⟶ℂ)
179 mnfxr 11373 . . . . . . . . . 10 -∞ ∈ ℝ*
18025adantr 486 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
181 elfzofz 13817 . . . . . . . . . . . . . 14 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
182181adantl 487 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
183180, 182ffvelcdmd 7090 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
184183rexrd 11366 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ*)
185184mnfled 13272 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -∞ ≤ (𝑄‘𝑖))
186 iooss1 13518 . . . . . . . . . 10 ((-∞ ∈ ℝ* ∧ -∞ ≤ (𝑄‘𝑖)) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ (-∞(,)(𝐸‘𝑋)))
187179, 185, 186sylancr 599 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ (-∞(,)(𝐸‘𝑋)))
1881873adant3 1150 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ (-∞(,)(𝐸‘𝑋)))
189 fzofzp1 13906 . . . . . . . . . . . . . 14 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
190189adantl 487 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
191180, 190ffvelcdmd 7090 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
1921913adant3 1150 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
193192rexrd 11366 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
1941833adant3 1150 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
195194rexrd 11366 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ*)
196 simp3 1156 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
197195, 193, 196iocleubd 46706 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ≤ (𝑄‘(𝑖 + 1)))
198 iooss2 13519 . . . . . . . . . 10 (((𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸‘𝑋) ≤ (𝑄‘(𝑖 + 1))) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
199193, 197, 198syl2anc 596 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
200 fourierdlem49.cn . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
201 cncff 25223 . . . . . . . . . . . . 13 ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
202 fdm 6724 . . . . . . . . . . . . 13 ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
203200, 201, 2023syl 19 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
204 ssdmres 6006 . . . . . . . . . . . 12 (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹 ↔ dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
205203, 204sylibr 237 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹)
206166adantr 486 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom 𝐹 = 𝐷)
207205, 206sseqtrd 3945 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
2082073adant3 1150 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
209199, 208sstrd 3919 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ 𝐷)
210188, 209ssind 4136 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷))
211 fourierdlem49.d . . . . . . . . . 10 (𝜑 → 𝐷 ⊆ ℝ)
212211, 173sstrd 3919 . . . . . . . . 9 (𝜑 → 𝐷 ⊆ ℂ)
2132123ad2ant1 1151 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐷 ⊆ ℂ)
214213ssinss2d 46213 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ⊆ ℂ)
215 eqid 2760 . . . . . . 7 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
216 eqid 2760 . . . . . . 7 ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) = ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))
2171263ad2ant1 1151 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ℝ)
218217rexrd 11366 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ℝ*)
219195, 193, 196iocgtlbd 46717 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝐸‘𝑋))
220217leidd 11889 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ≤ (𝐸‘𝑋))
221195, 218, 218, 219, 220eliocd 46655 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋)))
222 ioounsn 13615 . . . . . . . . . . 11 (((𝑄‘𝑖) ∈ ℝ* ∧ (𝐸‘𝑋) ∈ ℝ* ∧ (𝑄‘𝑖) < (𝐸‘𝑋)) → (((𝑄‘𝑖)(,)(𝐸‘𝑋)) ∪ {(𝐸‘𝑋)}) = ((𝑄‘𝑖)(,](𝐸‘𝑋)))
223195, 218, 219, 222syl3anc 1398 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖)(,)(𝐸‘𝑋)) ∪ {(𝐸‘𝑋)}) = ((𝑄‘𝑖)(,](𝐸‘𝑋)))
224223fveq2d 6894 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))‘(((𝑄‘𝑖)(,)(𝐸‘𝑋)) ∪ {(𝐸‘𝑋)})) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))‘((𝑄‘𝑖)(,](𝐸‘𝑋))))
225215cnfldtop 25111 . . . . . . . . . . 11 (TopOpen‘ℂfld) ∈ Top
226 ovex 7457 . . . . . . . . . . . . 13 (-∞(,)(𝐸‘𝑋)) ∈ V
227226inex1 5277 . . . . . . . . . . . 12 ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∈ V
228 snex 5397 . . . . . . . . . . . 12 {(𝐸‘𝑋)} ∈ V
229227, 228unex 7765 . . . . . . . . . . 11 (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}) ∈ V
230 resttop 23487 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ∈ Top ∧ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}) ∈ V) → ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) ∈ Top)
231225, 229, 230mp2an 705 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) ∈ Top
232 retop 25089 . . . . . . . . . . . 12 (topGen‘ran (,)) ∈ Top
233 iooretop 25093 . . . . . . . . . . . . 13 ((𝑄‘𝑖)(,)+∞) ∈ (topGen‘ran (,))
234233a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)+∞) ∈ (topGen‘ran (,)))
235 elrestr 17608 . . . . . . . . . . . 12 (((topGen‘ran (,)) ∈ Top ∧ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}) ∈ V ∧ ((𝑄‘𝑖)(,)+∞) ∈ (topGen‘ran (,))) → (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
236232, 229, 234, 235mp3an12i 1494 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
237 simpr 490 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 = (𝐸‘𝑋)) → 𝑥 = (𝐸‘𝑋))
238 pnfxr 11370 . . . . . . . . . . . . . . . . . . . 20 +∞ ∈ ℝ*
239238a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → +∞ ∈ ℝ*)
240217ltpnfd 13257 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) < +∞)
241195, 239, 217, 219, 240eliood 46646 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)+∞))
242 snidg 4617 . . . . . . . . . . . . . . . . . . . 20 ((𝐸‘𝑋) ∈ ℝ → (𝐸‘𝑋) ∈ {(𝐸‘𝑋)})
243 elun2 4180 . . . . . . . . . . . . . . . . . . . 20 ((𝐸‘𝑋) ∈ {(𝐸‘𝑋)} → (𝐸‘𝑋) ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))
244126, 242, 2433syl 19 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐸‘𝑋) ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))
2452443ad2ant1 1151 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))
246241, 245elind 4096 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
247246adantr 486 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
248237, 247eqeltrd 2860 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 = (𝐸‘𝑋)) → 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
249248adantlr 728 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ 𝑥 = (𝐸‘𝑋)) → 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
250195adantr 486 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → (𝑄‘𝑖) ∈ ℝ*)
251238a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → +∞ ∈ ℝ*)
252184adantr 486 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → (𝑄‘𝑖) ∈ ℝ*)
253126ad2antrr 739 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → (𝐸‘𝑋) ∈ ℝ)
254 iocssre 13565 . . . . . . . . . . . . . . . . . . . 20 (((𝑄‘𝑖) ∈ ℝ* ∧ (𝐸‘𝑋) ∈ ℝ) → ((𝑄‘𝑖)(,](𝐸‘𝑋)) ⊆ ℝ)
255252, 253, 254syl2anc 596 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → ((𝑄‘𝑖)(,](𝐸‘𝑋)) ⊆ ℝ)
256 simpr 490 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋)))
257255, 256sseldd 3910 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → 𝑥 ∈ ℝ)
2582573adantl3 1187 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → 𝑥 ∈ ℝ)
259253rexrd 11366 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → (𝐸‘𝑋) ∈ ℝ*)
260252, 259, 256iocgtlbd 46717 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → (𝑄‘𝑖) < 𝑥)
2612603adantl3 1187 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → (𝑄‘𝑖) < 𝑥)
262258ltpnfd 13257 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → 𝑥 < +∞)
263250, 251, 258, 261, 262eliood 46646 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → 𝑥 ∈ ((𝑄‘𝑖)(,)+∞))
264263adantr 486 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 ∈ ((𝑄‘𝑖)(,)+∞))
265179a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → -∞ ∈ ℝ*)
266259adantr 486 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ℝ*)
267257adantr 486 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 ∈ ℝ)
268267mnfltd 13260 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → -∞ < 𝑥)
269126ad3antrrr 743 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ℝ)
270252, 259, 256iocleubd 46706 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → 𝑥 ≤ (𝐸‘𝑋))
271270adantr 486 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 ≤ (𝐸‘𝑋))
272 neqne 2963 . . . . . . . . . . . . . . . . . . . . . 22 (¬ 𝑥 = (𝐸‘𝑋) → 𝑥 ≠ (𝐸‘𝑋))
273272necomd 3010 . . . . . . . . . . . . . . . . . . . . 21 (¬ 𝑥 = (𝐸‘𝑋) → (𝐸‘𝑋) ≠ 𝑥)
274273adantl 487 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → (𝐸‘𝑋) ≠ 𝑥)
275267, 269, 271, 274leneltd 11471 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 < (𝐸‘𝑋))
276265, 266, 267, 268, 275eliood 46646 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 ∈ (-∞(,)(𝐸‘𝑋)))
2772763adantll3 46195 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 ∈ (-∞(,)(𝐸‘𝑋)))
278208ad2antrr 739 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
279195ad2antrr 739 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → (𝑄‘𝑖) ∈ ℝ*)
280193ad2antrr 739 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
281258adantr 486 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 ∈ ℝ)
282261adantr 486 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → (𝑄‘𝑖) < 𝑥)
283217ad2antrr 739 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ℝ)
284192ad2antrr 739 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
2852753adantll3 46195 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 < (𝐸‘𝑋))
286197ad2antrr 739 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘(𝑖 + 1)))
287281, 283, 284, 285, 286ltletrd 11477 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 < (𝑄‘(𝑖 + 1)))
288279, 280, 281, 282, 287eliood 46646 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
289278, 288sseldd 3910 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 ∈ 𝐷)
290277, 289elind 4096 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 ∈ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷))
291 elun1 4179 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) → 𝑥 ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))
292290, 291syl 18 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))
293264, 292elind 4096 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
294249, 293pm2.61dan 825 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
295195adantr 486 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))) → (𝑄‘𝑖) ∈ ℝ*)
296218adantr 486 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))) → (𝐸‘𝑋) ∈ ℝ*)
297 elinel1 4097 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) → 𝑥 ∈ ((𝑄‘𝑖)(,)+∞))
298 elioore 13513 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((𝑄‘𝑖)(,)+∞) → 𝑥 ∈ ℝ)
299298rexrd 11366 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((𝑄‘𝑖)(,)+∞) → 𝑥 ∈ ℝ*)
300297, 299syl 18 . . . . . . . . . . . . . . 15 (𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) → 𝑥 ∈ ℝ*)
301300adantl 487 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))) → 𝑥 ∈ ℝ*)
302184adantr 486 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))) → (𝑄‘𝑖) ∈ ℝ*)
303238a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))) → +∞ ∈ ℝ*)
304297adantl 487 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))) → 𝑥 ∈ ((𝑄‘𝑖)(,)+∞))
305302, 303, 304ioogtlbd 46698 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))) → (𝑄‘𝑖) < 𝑥)
3063053adantl3 1187 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))) → (𝑄‘𝑖) < 𝑥)
307 elinel2 4098 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) → 𝑥 ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))
308 elsni 4597 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {(𝐸‘𝑋)} → 𝑥 = (𝐸‘𝑋))
309308adantl 487 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑥 ∈ {(𝐸‘𝑋)}) → 𝑥 = (𝐸‘𝑋))
310127adantr 486 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑥 ∈ {(𝐸‘𝑋)}) → (𝐸‘𝑋) ≤ (𝐸‘𝑋))
311309, 310eqbrtrd 5126 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑥 ∈ {(𝐸‘𝑋)}) → 𝑥 ≤ (𝐸‘𝑋))
312311adantlr 728 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑥 ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) ∧ 𝑥 ∈ {(𝐸‘𝑋)}) → 𝑥 ≤ (𝐸‘𝑋))
313 simpll 779 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑥 ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) ∧ ¬ 𝑥 ∈ {(𝐸‘𝑋)}) → 𝜑)
314 elunnel2 4153 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}) ∧ ¬ 𝑥 ∈ {(𝐸‘𝑋)}) → 𝑥 ∈ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷))
315314adantll 727 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑥 ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) ∧ ¬ 𝑥 ∈ {(𝐸‘𝑋)}) → 𝑥 ∈ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷))
316 elinel1 4097 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) → 𝑥 ∈ (-∞(,)(𝐸‘𝑋)))
317 elioore 13513 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (-∞(,)(𝐸‘𝑋)) → 𝑥 ∈ ℝ)
318317adantl 487 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑥 ∈ (-∞(,)(𝐸‘𝑋))) → 𝑥 ∈ ℝ)
319126adantr 486 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑥 ∈ (-∞(,)(𝐸‘𝑋))) → (𝐸‘𝑋) ∈ ℝ)
320179a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑥 ∈ (-∞(,)(𝐸‘𝑋))) → -∞ ∈ ℝ*)
321319rexrd 11366 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑥 ∈ (-∞(,)(𝐸‘𝑋))) → (𝐸‘𝑋) ∈ ℝ*)
322 simpr 490 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑥 ∈ (-∞(,)(𝐸‘𝑋))) → 𝑥 ∈ (-∞(,)(𝐸‘𝑋)))
323320, 321, 322iooltubd 46692 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑥 ∈ (-∞(,)(𝐸‘𝑋))) → 𝑥 < (𝐸‘𝑋))
324318, 319, 323ltled 11465 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑥 ∈ (-∞(,)(𝐸‘𝑋))) → 𝑥 ≤ (𝐸‘𝑋))
325316, 324sylan2 605 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑥 ∈ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷)) → 𝑥 ≤ (𝐸‘𝑋))
326313, 315, 325syl2anc 596 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑥 ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) ∧ ¬ 𝑥 ∈ {(𝐸‘𝑋)}) → 𝑥 ≤ (𝐸‘𝑋))
327312, 326pm2.61dan 825 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑥 ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) → 𝑥 ≤ (𝐸‘𝑋))
328327adantlr 728 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) → 𝑥 ≤ (𝐸‘𝑋))
329307, 328sylan2 605 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))) → 𝑥 ≤ (𝐸‘𝑋))
3303293adantl3 1187 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))) → 𝑥 ≤ (𝐸‘𝑋))
331295, 296, 301, 306, 330eliocd 46655 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))) → 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋)))
332294, 331impbida 813 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋)) ↔ 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))))
333332eqrdv 2758 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,](𝐸‘𝑋)) = (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
334 ioossre 13545 . . . . . . . . . . . . . 14 (-∞(,)(𝐸‘𝑋)) ⊆ ℝ
335 ssinss1 4141 . . . . . . . . . . . . . 14 ((-∞(,)(𝐸‘𝑋)) ⊆ ℝ → ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ⊆ ℝ)
336334, 335mp1i 14 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ⊆ ℝ)
337217snssd 4743 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → {(𝐸‘𝑋)} ⊆ ℝ)
338336, 337unssd 4189 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}) ⊆ ℝ)
339 eqid 2760 . . . . . . . . . . . . 13 (topGen‘ran (,)) = (topGen‘ran (,))
340215, 339rerest 25132 . . . . . . . . . . . 12 ((((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) = ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
341338, 340syl 18 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) = ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
342236, 333, 3413eltr4d 2875 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,](𝐸‘𝑋)) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
343 isopn3i 23409 . . . . . . . . . 10 ((((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) ∈ Top ∧ ((𝑄‘𝑖)(,](𝐸‘𝑋)) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))‘((𝑄‘𝑖)(,](𝐸‘𝑋))) = ((𝑄‘𝑖)(,](𝐸‘𝑋)))
344231, 342, 343sylancr 599 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))‘((𝑄‘𝑖)(,](𝐸‘𝑋))) = ((𝑄‘𝑖)(,](𝐸‘𝑋)))
345224, 344eqtr2d 2796 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,](𝐸‘𝑋)) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))‘(((𝑄‘𝑖)(,)(𝐸‘𝑋)) ∪ {(𝐸‘𝑋)})))
346221, 345eleqtrd 2862 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))‘(((𝑄‘𝑖)(,)(𝐸‘𝑋)) ∪ {(𝐸‘𝑋)})))
347178, 210, 214, 215, 216, 346limcres 26215 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷)) ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) = ((𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷)) limℂ (𝐸‘𝑋)))
348210resabs1d 6001 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷)) ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))))
349348oveq1d 7439 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷)) ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
350171, 347, 3493eqtr2d 2801 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
351174ffdmd 6745 . . . . . . . . . . 11 (𝜑 → 𝐹:dom 𝐹⟶ℂ)
352351adantr 486 . . . . . . . . . 10 ((𝜑 ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → 𝐹:dom 𝐹⟶ℂ)
3533523ad2antl1 1204 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → 𝐹:dom 𝐹⟶ℂ)
354 ioosscn 13546 . . . . . . . . . 10 ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ ℂ
355354a1i 11 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ ℂ)
356166eqcomd 2766 . . . . . . . . . . . 12 (𝜑 → 𝐷 = dom 𝐹)
3573563ad2ant1 1151 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐷 = dom 𝐹)
358209, 357sseqtrd 3945 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ dom 𝐹)
359358adantr 486 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ dom 𝐹)
360 oveq2 7432 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋 → (𝐵 − 𝑥) = (𝐵 − 𝑋))
361360fvoveq1d 7446 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑋) / 𝑇)))
362361oveq1d 7439 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
3632, 14resubcld 11751 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵 − 𝑋) ∈ ℝ)
3642, 1resubcld 11751 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
3654, 364eqeltrid 2864 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 𝑇 ∈ ℝ)
3661, 2posdifd 11910 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
3673, 366mpbid 235 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 < (𝐵 − 𝐴))
368367, 4breqtrrdi 5146 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 < 𝑇)
369368gt0ne0d 11887 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 𝑇 ≠ 0)
370363, 365, 369redivcld 12152 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 − 𝑋) / 𝑇) ∈ ℝ)
371370flcld 13945 . . . . . . . . . . . . . . . . 17 (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
372371zred 12810 . . . . . . . . . . . . . . . 16 (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℝ)
373372, 365remulcld 11346 . . . . . . . . . . . . . . 15 (𝜑 → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
3747, 362, 14, 373fvmptd3 7022 . . . . . . . . . . . . . 14 (𝜑 → (𝑍‘𝑋) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
375374, 373eqeltrd 2860 . . . . . . . . . . . . 13 (𝜑 → (𝑍‘𝑋) ∈ ℝ)
376375recnd 11344 . . . . . . . . . . . 12 (𝜑 → (𝑍‘𝑋) ∈ ℂ)
377376adantr 486 . . . . . . . . . . 11 ((𝜑 ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → (𝑍‘𝑋) ∈ ℂ)
3783773ad2antl1 1204 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → (𝑍‘𝑋) ∈ ℂ)
379378negcld 11663 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → -(𝑍‘𝑋) ∈ ℂ)
380 eqid 2760 . . . . . . . . 9 {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))} = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))}
381 ioosscn 13546 . . . . . . . . . . . . . . . . . 18 (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ ℂ
382381sseli 3905 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) → 𝑦 ∈ ℂ)
383382adantl 487 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ ℂ)
384376adantr 486 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑍‘𝑋) ∈ ℂ)
385383, 384pncand 11677 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑦 + (𝑍‘𝑋)) − (𝑍‘𝑋)) = 𝑦)
386385eqcomd 2766 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) − (𝑍‘𝑋)))
3873863ad2antl1 1204 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) − (𝑍‘𝑋)))
388374oveq2d 7440 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑦 + (𝑍‘𝑋)) − (𝑍‘𝑋)) = ((𝑦 + (𝑍‘𝑋)) − ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
389388adantr 486 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑦 + (𝑍‘𝑋)) − (𝑍‘𝑋)) = ((𝑦 + (𝑍‘𝑋)) − ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
390383, 384addcld 11335 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ℂ)
391373recnd 11344 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
392391adantr 486 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
393390, 392negsubd 11682 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑦 + (𝑍‘𝑋)) + -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + (𝑍‘𝑋)) − ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
394371zcnd 12811 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℂ)
395365recnd 11344 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 𝑇 ∈ ℂ)
396394, 395mulneg1d 11776 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
397396eqcomd 2766 . . . . . . . . . . . . . . . . . 18 (𝜑 → -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
398397oveq2d 7440 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑦 + (𝑍‘𝑋)) + -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
399398adantr 486 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑦 + (𝑍‘𝑋)) + -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
400389, 393, 3993eqtr2d 2801 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑦 + (𝑍‘𝑋)) − (𝑍‘𝑋)) = ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
4014003ad2antl1 1204 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑦 + (𝑍‘𝑋)) − (𝑍‘𝑋)) = ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
402371znegcld 12812 . . . . . . . . . . . . . . . . 17 (𝜑 → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
403402adantr 486 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
4044033ad2antl1 1204 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
405 simpl1 1210 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝜑)
406209adantr 486 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ 𝐷)
407184adantr 486 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) ∈ ℝ*)
408126rexrd 11366 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐸‘𝑋) ∈ ℝ*)
409408ad2antrr 739 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝐸‘𝑋) ∈ ℝ*)
410 elioore 13513 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) → 𝑦 ∈ ℝ)
411410adantl 487 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
412375adantr 486 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑍‘𝑋) ∈ ℝ)
413411, 412readdcld 11345 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
414413adantlr 728 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
415375adantr 486 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑍‘𝑋) ∈ ℝ)
416183, 415resubcld 11751 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ)
417416rexrd 11366 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ*)
418417adantr 486 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ*)
41914rexrd 11366 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 𝑋 ∈ ℝ*)
420419ad2antrr 739 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑋 ∈ ℝ*)
421 simpr 490 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋))
422418, 420, 421ioogtlbd 46698 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑦)
423183adantr 486 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) ∈ ℝ)
424375ad2antrr 739 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑍‘𝑋) ∈ ℝ)
425410adantl 487 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
426423, 424, 425ltsubaddd 11919 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑦 ↔ (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋))))
427422, 426mpbid 235 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋)))
42814ad2antrr 739 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑋 ∈ ℝ)
429418, 420, 421iooltubd 46692 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 < 𝑋)
430425, 428, 424, 429ltadd1dd 11934 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝑋 + (𝑍‘𝑋)))
431 id 23 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑋 → 𝑥 = 𝑋)
432 fveq2 6890 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑋 → (𝑍‘𝑥) = (𝑍‘𝑋))
433431, 432oveq12d 7442 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑋 → (𝑥 + (𝑍‘𝑥)) = (𝑋 + (𝑍‘𝑋)))
43414, 375readdcld 11345 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑋 + (𝑍‘𝑋)) ∈ ℝ)
4355, 433, 14, 434fvmptd3 7022 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐸‘𝑋) = (𝑋 + (𝑍‘𝑋)))
436435eqcomd 2766 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑋 + (𝑍‘𝑋)) = (𝐸‘𝑋))
437436ad2antrr 739 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑋 + (𝑍‘𝑋)) = (𝐸‘𝑋))
438430, 437breqtrd 5130 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝐸‘𝑋))
439407, 409, 414, 427, 438eliood 46646 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋)))
4404393adantl3 1187 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋)))
441406, 440sseldd 3910 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ 𝐷)
442405, 441, 4043jca 1146 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ))
443 eleq1 2848 . . . . . . . . . . . . . . . . . 18 (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ))
4444433anbi3d 1470 . . . . . . . . . . . . . . . . 17 (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)))
445 oveq1 7431 . . . . . . . . . . . . . . . . . . 19 (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑘 · 𝑇) = ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
446445oveq2d 7440 . . . . . . . . . . . . . . . . . 18 (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) = ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
447446eleq1d 2845 . . . . . . . . . . . . . . . . 17 (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
448444, 447imbi12d 347 . . . . . . . . . . . . . . . 16 (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)))
449 ovex 7457 . . . . . . . . . . . . . . . . 17 (𝑦 + (𝑍‘𝑋)) ∈ V
450 eleq1 2848 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑦 + (𝑍‘𝑋)) → (𝑥 ∈ 𝐷 ↔ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷))
4514503anbi2d 1469 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑦 + (𝑍‘𝑋)) → ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ)))
452 oveq1 7431 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑦 + (𝑍‘𝑋)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)))
453452eleq1d 2845 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑦 + (𝑍‘𝑋)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷))
454451, 453imbi12d 347 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑦 + (𝑍‘𝑋)) → (((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)))
455 fourierdlem49.dper . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)
456449, 454, 455vtocl 3520 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)
457448, 456vtoclg 3517 . . . . . . . . . . . . . . 15 ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ → ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
458404, 442, 457sylc 66 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
459401, 458eqeltrd 2860 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑦 + (𝑍‘𝑋)) − (𝑍‘𝑋)) ∈ 𝐷)
460387, 459eqeltrd 2860 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ 𝐷)
461460ssd 46233 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷)
462183recnd 11344 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℂ)
463376adantr 486 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑍‘𝑋) ∈ ℂ)
464462, 463negsubd 11682 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) + -(𝑍‘𝑋)) = ((𝑄‘𝑖) − (𝑍‘𝑋)))
465464eqcomd 2766 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) = ((𝑄‘𝑖) + -(𝑍‘𝑋)))
466435oveq1d 7439 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸‘𝑋) + -(𝑍‘𝑋)) = ((𝑋 + (𝑍‘𝑋)) + -(𝑍‘𝑋)))
467434recnd 11344 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑋 + (𝑍‘𝑋)) ∈ ℂ)
468467, 376negsubd 11682 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑋 + (𝑍‘𝑋)) + -(𝑍‘𝑋)) = ((𝑋 + (𝑍‘𝑋)) − (𝑍‘𝑋)))
46914recnd 11344 . . . . . . . . . . . . . . . . 17 (𝜑 → 𝑋 ∈ ℂ)
470469, 376pncand 11677 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑋 + (𝑍‘𝑋)) − (𝑍‘𝑋)) = 𝑋)
471466, 468, 4703eqtrrd 2800 . . . . . . . . . . . . . . 15 (𝜑 → 𝑋 = ((𝐸‘𝑋) + -(𝑍‘𝑋)))
472471adantr 486 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 = ((𝐸‘𝑋) + -(𝑍‘𝑋)))
473465, 472oveq12d 7442 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) = (((𝑄‘𝑖) + -(𝑍‘𝑋))(,)((𝐸‘𝑋) + -(𝑍‘𝑋))))
474126adantr 486 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐸‘𝑋) ∈ ℝ)
475415renegcld 11750 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -(𝑍‘𝑋) ∈ ℝ)
476183, 474, 475iooshift 46670 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘𝑖) + -(𝑍‘𝑋))(,)((𝐸‘𝑋) + -(𝑍‘𝑋))) = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))})
477473, 476eqtr2d 2796 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))} = (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋))
4784773adant3 1150 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))} = (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋))
4791663ad2ant1 1151 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → dom 𝐹 = 𝐷)
480461, 478, 4793sstr4d 3964 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))} ⊆ dom 𝐹)
481480adantr 486 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))} ⊆ dom 𝐹)
482374negeqd 11558 . . . . . . . . . . . . . . . 16 (𝜑 → -(𝑍‘𝑋) = -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
483482, 397eqtrd 2795 . . . . . . . . . . . . . . 15 (𝜑 → -(𝑍‘𝑋) = ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
484483oveq2d 7440 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 + -(𝑍‘𝑋)) = (𝑥 + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
485484fveq2d 6894 . . . . . . . . . . . . 13 (𝜑 → (𝐹‘(𝑥 + -(𝑍‘𝑋))) = (𝐹‘(𝑥 + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))))
486485adantr 486 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) → (𝐹‘(𝑥 + -(𝑍‘𝑋))) = (𝐹‘(𝑥 + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))))
4874863ad2antl1 1204 . . . . . . . . . . 11 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) → (𝐹‘(𝑥 + -(𝑍‘𝑋))) = (𝐹‘(𝑥 + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))))
488402adantr 486 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
4894883ad2antl1 1204 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
490 simpl1 1210 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) → 𝜑)
491209sselda 3909 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) → 𝑥 ∈ 𝐷)
492490, 491, 4893jca 1146 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) → (𝜑 ∧ 𝑥 ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ))
4934433anbi3d 1470 . . . . . . . . . . . . . 14 (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ 𝑥 ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)))
494445oveq2d 7440 . . . . . . . . . . . . . . 15 (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = (𝑥 + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
495494fveqeq2d 6898 . . . . . . . . . . . . . 14 (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥) ↔ (𝐹‘(𝑥 + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))) = (𝐹‘𝑥)))
496493, 495imbi12d 347 . . . . . . . . . . . . 13 (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))) = (𝐹‘𝑥))))
497 fourierdlem49.per . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥))
498496, 497vtoclg 3517 . . . . . . . . . . . 12 ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ → ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))) = (𝐹‘𝑥)))
499489, 492, 498sylc 66 . . . . . . . . . . 11 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) → (𝐹‘(𝑥 + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))) = (𝐹‘𝑥))
500487, 499eqtrd 2795 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) → (𝐹‘(𝑥 + -(𝑍‘𝑋))) = (𝐹‘𝑥))
501500adantlr 728 . . . . . . . . 9 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) → (𝐹‘(𝑥 + -(𝑍‘𝑋))) = (𝐹‘𝑥))
502 simpr 490 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
503353, 355, 359, 379, 380, 481, 501, 502limcperiod 46776 . . . . . . . 8 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → 𝑦 ∈ ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))}) limℂ ((𝐸‘𝑋) + -(𝑍‘𝑋))))
504477reseq2d 5971 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))}) = (𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)))
505472eqcomd 2766 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸‘𝑋) + -(𝑍‘𝑋)) = 𝑋)
506504, 505oveq12d 7442 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))}) limℂ ((𝐸‘𝑋) + -(𝑍‘𝑋))) = ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋))
5075063adant3 1150 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))}) limℂ ((𝐸‘𝑋) + -(𝑍‘𝑋))) = ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋))
508507adantr 486 . . . . . . . 8 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))}) limℂ ((𝐸‘𝑋) + -(𝑍‘𝑋))) = ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋))
509503, 508eleqtrd 2862 . . . . . . 7 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋))
510351adantr 486 . . . . . . . . . 10 ((𝜑 ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋)) → 𝐹:dom 𝐹⟶ℂ)
5115103ad2antl1 1204 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋)) → 𝐹:dom 𝐹⟶ℂ)
512381a1i 11 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋)) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ ℂ)
513461, 479sseqtrrd 3946 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ dom 𝐹)
514513adantr 486 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋)) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ dom 𝐹)
515376adantr 486 . . . . . . . . . 10 ((𝜑 ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋)) → (𝑍‘𝑋) ∈ ℂ)
5165153ad2antl1 1204 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋)) → (𝑍‘𝑋) ∈ ℂ)
517 eqid 2760 . . . . . . . . 9 {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))} = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))}
518462, 463npcand 11680 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘𝑖) − (𝑍‘𝑋)) + (𝑍‘𝑋)) = (𝑄‘𝑖))
519518eqcomd 2766 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = (((𝑄‘𝑖) − (𝑍‘𝑋)) + (𝑍‘𝑋)))
520435adantr 486 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐸‘𝑋) = (𝑋 + (𝑍‘𝑋)))
521519, 520oveq12d 7442 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) = ((((𝑄‘𝑖) − (𝑍‘𝑋)) + (𝑍‘𝑋))(,)(𝑋 + (𝑍‘𝑋))))
52214adantr 486 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
523416, 522, 415iooshift 46670 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((((𝑄‘𝑖) − (𝑍‘𝑋)) + (𝑍‘𝑋))(,)(𝑋 + (𝑍‘𝑋))) = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))})
524521, 523eqtr2d 2796 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))} = ((𝑄‘𝑖)(,)(𝐸‘𝑋)))
5255243adant3 1150 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))} = ((𝑄‘𝑖)(,)(𝐸‘𝑋)))
526209, 525, 4793sstr4d 3964 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))} ⊆ dom 𝐹)
527526adantr 486 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋)) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))} ⊆ dom 𝐹)
528374oveq2d 7440 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 + (𝑍‘𝑋)) = (𝑥 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
529528fveq2d 6894 . . . . . . . . . . . . 13 (𝜑 → (𝐹‘(𝑥 + (𝑍‘𝑋))) = (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))))
530529adantr 486 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍‘𝑋))) = (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))))
5315303ad2antl1 1204 . . . . . . . . . . 11 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍‘𝑋))) = (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))))
532371adantr 486 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
5335323ad2antl1 1204 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
534 simpl1 1210 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝜑)
535461sselda 3909 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑥 ∈ 𝐷)
536534, 535, 5333jca 1146 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝜑 ∧ 𝑥 ∈ 𝐷 ∧ (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ))
537 eleq1 2848 . . . . . . . . . . . . . . 15 (𝑘 = (⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ))
5385373anbi3d 1470 . . . . . . . . . . . . . 14 (𝑘 = (⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ 𝑥 ∈ 𝐷 ∧ (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)))
539 oveq1 7431 . . . . . . . . . . . . . . . 16 (𝑘 = (⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑘 · 𝑇) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
540539oveq2d 7440 . . . . . . . . . . . . . . 15 (𝑘 = (⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = (𝑥 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
541540fveqeq2d 6898 . . . . . . . . . . . . . 14 (𝑘 = (⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥) ↔ (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))) = (𝐹‘𝑥)))
542538, 541imbi12d 347 . . . . . . . . . . . . 13 (𝑘 = (⌊‘((𝐵 − 𝑋) / 𝑇)) → (((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))) = (𝐹‘𝑥))))
543542, 497vtoclg 3517 . . . . . . . . . . . 12 ((⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ → ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))) = (𝐹‘𝑥)))
544533, 536, 543sylc 66 . . . . . . . . . . 11 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))) = (𝐹‘𝑥))
545531, 544eqtrd 2795 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍‘𝑋))) = (𝐹‘𝑥))
546545adantlr 728 . . . . . . . . 9 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍‘𝑋))) = (𝐹‘𝑥))
547 simpr 490 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋)) → 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋))
548511, 512, 514, 516, 517, 527, 546, 547limcperiod 46776 . . . . . . . 8 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋)) → 𝑦 ∈ ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))}) limℂ (𝑋 + (𝑍‘𝑋))))
549524reseq2d 5971 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))}) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))))
550436adantr 486 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑍‘𝑋)) = (𝐸‘𝑋))
551549, 550oveq12d 7442 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))}) limℂ (𝑋 + (𝑍‘𝑋))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
5525513adant3 1150 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))}) limℂ (𝑋 + (𝑍‘𝑋))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
553552adantr 486 . . . . . . . 8 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋)) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))}) limℂ (𝑋 + (𝑍‘𝑋))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
554548, 553eleqtrd 2862 . . . . . . 7 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋)) → 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
555509, 554impbida 813 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) ↔ 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋)))
556555eqrdv 2758 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) = ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋))
557 resindm 6021 . . . . . . . . 9 (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)) = (𝐹 ↾ (-∞(,)𝑋))
558166ineq2d 4116 . . . . . . . . . 10 (𝜑 → ((-∞(,)𝑋) ∩ dom 𝐹) = ((-∞(,)𝑋) ∩ 𝐷))
559558reseq2d 5971 . . . . . . . . 9 (𝜑 → (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)))
560557, 559eqtr3id 2809 . . . . . . . 8 (𝜑 → (𝐹 ↾ (-∞(,)𝑋)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)))
561560oveq1d 7439 . . . . . . 7 (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) = ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) limℂ 𝑋))
5625613ad2ant1 1151 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) = ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) limℂ 𝑋))
563 inss2 4133 . . . . . . . . 9 ((-∞(,)𝑋) ∩ 𝐷) ⊆ 𝐷
564563a1i 11 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)𝑋) ∩ 𝐷) ⊆ 𝐷)
565175, 564fssresd 6754 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)):((-∞(,)𝑋) ∩ 𝐷)⟶ℂ)
566417mnfled 13272 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -∞ ≤ ((𝑄‘𝑖) − (𝑍‘𝑋)))
567 iooss1 13518 . . . . . . . . . 10 ((-∞ ∈ ℝ* ∧ -∞ ≤ ((𝑄‘𝑖) − (𝑍‘𝑋))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ (-∞(,)𝑋))
568179, 566, 567sylancr 599 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ (-∞(,)𝑋))
5695683adant3 1150 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ (-∞(,)𝑋))
570569, 461ssind 4136 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ ((-∞(,)𝑋) ∩ 𝐷))
571213ssinss2d 46213 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)𝑋) ∩ 𝐷) ⊆ ℂ)
572 eqid 2760 . . . . . . 7 ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) = ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
5734173adant3 1150 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ*)
5744193ad2ant1 1151 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ*)
5754353ad2ant1 1151 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) = (𝑋 + (𝑍‘𝑋)))
576219, 575breqtrd 5130 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝑋 + (𝑍‘𝑋)))
5773753ad2ant1 1151 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑍‘𝑋) ∈ ℝ)
578143ad2ant1 1151 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
579194, 577, 578ltsubaddd 11919 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋 ↔ (𝑄‘𝑖) < (𝑋 + (𝑍‘𝑋))))
580576, 579mpbird 260 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋)
58114leidd 11889 . . . . . . . . . 10 (𝜑 → 𝑋 ≤ 𝑋)
5825813ad2ant1 1151 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ≤ 𝑋)
583573, 574, 574, 580, 582eliocd 46655 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋))
584 ioounsn 13615 . . . . . . . . . . 11 ((((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ∧ ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋) → ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ∪ {𝑋}) = (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋))
585573, 574, 580, 584syl3anc 1398 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ∪ {𝑋}) = (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋))
586585fveq2d 6894 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘((((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ∪ {𝑋})) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘(((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)))
587 ovex 7457 . . . . . . . . . . . . 13 (-∞(,)𝑋) ∈ V
588587inex1 5277 . . . . . . . . . . . 12 ((-∞(,)𝑋) ∩ 𝐷) ∈ V
589 snex 5397 . . . . . . . . . . . 12 {𝑋} ∈ V
590588, 589unex 7765 . . . . . . . . . . 11 (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V
591 resttop 23487 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ∈ Top ∧ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V) → ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ Top)
592225, 590, 591mp2an 705 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ Top
593 iooretop 25093 . . . . . . . . . . . . 13 (((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∈ (topGen‘ran (,))
594593a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∈ (topGen‘ran (,)))
595 elrestr 17608 . . . . . . . . . . . 12 (((topGen‘ran (,)) ∈ Top ∧ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V ∧ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∈ (topGen‘ran (,))) → ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
596232, 590, 594, 595mp3an12i 1494 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
597417adantr 486 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ*)
598238a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → +∞ ∈ ℝ*)
59914ad2antrr 739 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → 𝑋 ∈ ℝ)
600 iocssre 13565 . . . . . . . . . . . . . . . . . 18 ((((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ* ∧ 𝑋 ∈ ℝ) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋) ⊆ ℝ)
601597, 599, 600syl2anc 596 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋) ⊆ ℝ)
602 simpr 490 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋))
603601, 602sseldd 3910 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → 𝑥 ∈ ℝ)
604419ad2antrr 739 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → 𝑋 ∈ ℝ*)
605597, 604, 602iocgtlbd 46717 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑥)
606603ltpnfd 13257 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → 𝑥 < +∞)
607597, 598, 603, 605, 606eliood 46646 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞))
6086073adantl3 1187 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞))
609 eqvisset 3470 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋 → 𝑋 ∈ V)
610 snidg 4617 . . . . . . . . . . . . . . . . . . 19 (𝑋 ∈ V → 𝑋 ∈ {𝑋})
611609, 610syl 18 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋 → 𝑋 ∈ {𝑋})
612431, 611eqeltrd 2860 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋 → 𝑥 ∈ {𝑋})
613 elun2 4180 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑋} → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
614612, 613syl 18 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
615614adantl 487 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) ∧ 𝑥 = 𝑋) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
616 simpll 779 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → (𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
617417ad2antrr 739 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ*)
618419ad3antrrr 743 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑋 ∈ ℝ*)
619603adantr 486 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ ℝ)
620605adantr 486 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑥)
62114ad3antrrr 743 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑋 ∈ ℝ)
622597, 604, 602iocleubd 46706 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → 𝑥 ≤ 𝑋)
623622adantr 486 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ≤ 𝑋)
624431eqcoms 2768 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 = 𝑥 → 𝑥 = 𝑋)
625624necon3bi 2981 . . . . . . . . . . . . . . . . . . . 20 (¬ 𝑥 = 𝑋 → 𝑋 ≠ 𝑥)
626625adantl 487 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑋 ≠ 𝑥)
627619, 621, 623, 626leneltd 11471 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 < 𝑋)
628617, 618, 619, 620, 627eliood 46646 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋))
6296283adantll3 46195 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋))
630570sselda 3909 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷))
631 elun1 4179 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
632630, 631syl 18 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
633616, 629, 632syl2anc 596 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
634615, 633pm2.61dan 825 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
635608, 634elind 4096 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
636573adantr 486 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ*)
637574adantr 486 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑋 ∈ ℝ*)
638 elinel1 4097 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞))
639 elioore 13513 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) → 𝑥 ∈ ℝ)
640638, 639syl 18 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ ℝ)
641640rexrd 11366 . . . . . . . . . . . . . . 15 (𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ ℝ*)
642641adantl 487 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ∈ ℝ*)
643417adantr 486 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ*)
644238a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → +∞ ∈ ℝ*)
645638adantl 487 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞))
646643, 644, 645ioogtlbd 46698 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑥)
6476463adantl3 1187 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑥)
648 elinel2 4098 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
649 elsni 4597 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ {𝑋} → 𝑥 = 𝑋)
650649adantl 487 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑥 ∈ {𝑋}) → 𝑥 = 𝑋)
651581adantr 486 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑥 ∈ {𝑋}) → 𝑋 ≤ 𝑋)
652650, 651eqbrtrd 5126 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑥 ∈ {𝑋}) → 𝑥 ≤ 𝑋)
653652adantlr 728 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ 𝑥 ∈ {𝑋}) → 𝑥 ≤ 𝑋)
654 simpll 779 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝜑)
655 elunnel2 4153 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷))
656655adantll 727 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷))
657656elin1d 4100 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ∈ (-∞(,)𝑋))
658 elioore 13513 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (-∞(,)𝑋) → 𝑥 ∈ ℝ)
659658adantl 487 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑥 ∈ (-∞(,)𝑋)) → 𝑥 ∈ ℝ)
66014adantr 486 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑥 ∈ (-∞(,)𝑋)) → 𝑋 ∈ ℝ)
661179a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑥 ∈ (-∞(,)𝑋)) → -∞ ∈ ℝ*)
662419adantr 486 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑥 ∈ (-∞(,)𝑋)) → 𝑋 ∈ ℝ*)
663 simpr 490 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑥 ∈ (-∞(,)𝑋)) → 𝑥 ∈ (-∞(,)𝑋))
664661, 662, 663iooltubd 46692 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑥 ∈ (-∞(,)𝑋)) → 𝑥 < 𝑋)
665659, 660, 664ltled 11465 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑥 ∈ (-∞(,)𝑋)) → 𝑥 ≤ 𝑋)
666654, 657, 665syl2anc 596 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ≤ 𝑋)
667653, 666pm2.61dan 825 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ≤ 𝑋)
668648, 667sylan2 605 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ≤ 𝑋)
6696683ad2antl1 1204 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ≤ 𝑋)
670636, 637, 642, 647, 669eliocd 46655 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋))
671635, 670impbida 813 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋) ↔ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))))
672671eqrdv 2758 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋) = ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
673211ssinss2d 46213 . . . . . . . . . . . . . 14 (𝜑 → ((-∞(,)𝑋) ∩ 𝐷) ⊆ ℝ)
67414snssd 4743 . . . . . . . . . . . . . 14 (𝜑 → {𝑋} ⊆ ℝ)
675673, 674unssd 4189 . . . . . . . . . . . . 13 (𝜑 → (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ⊆ ℝ)
6766753ad2ant1 1151 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ⊆ ℝ)
677215, 339rerest 25132 . . . . . . . . . . . 12 ((((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) = ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
678676, 677syl 18 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) = ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
679596, 672, 6783eltr4d 2875 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
680 isopn3i 23409 . . . . . . . . . 10 ((((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ Top ∧ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘(((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) = (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋))
681592, 679, 680sylancr 599 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘(((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) = (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋))
682586, 681eqtr2d 2796 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘((((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ∪ {𝑋})))
683583, 682eleqtrd 2862 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘((((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ∪ {𝑋})))
684565, 570, 571, 215, 572, 683limcres 26215 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋) = ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) limℂ 𝑋))
685570resabs1d 6001 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) = (𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)))
686685oveq1d 7439 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋) = ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋))
687562, 684, 6863eqtr2rd 2802 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋) = ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋))
688350, 556, 6873eqtrrd 2800 . . . 4 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) = ((𝐹 ↾ (-∞(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
689688rexlimdv3a 3167 . . 3 (𝜑 → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) = ((𝐹 ↾ (-∞(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))))
690163, 689mpd 16 . 2 (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) = ((𝐹 ↾ (-∞(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
6911133adant3 1150 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
6922003adant3 1150 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
693 fourierdlem49.l . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))))
6946933adant3 1150 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))))
695 eqid 2760 . . . . . . . 8 if((𝐸‘𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸‘𝑋))) = if((𝐸‘𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸‘𝑋)))
696 eqid 2760 . . . . . . . 8 ((TopOpen‘ℂfld) ↾t (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))})) = ((TopOpen‘ℂfld) ↾t (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))}))
697194, 192, 691, 692, 694, 194, 217, 219, 199, 695, 696fourierdlem33 47286 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → if((𝐸‘𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸‘𝑋))) ∈ (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
698199resabs1d 6001 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))))
699698oveq1d 7439 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
700697, 699eleqtrd 2862 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → if((𝐸‘𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸‘𝑋))) ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
701700ne0d 4287 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) ≠ ∅)
702350, 701eqnetrd 3022 . . . 4 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) ≠ ∅)
703702rexlimdv3a 3167 . . 3 (𝜑 → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ (-∞(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) ≠ ∅))
704163, 703mpd 16 . 2 (𝜑 → ((𝐹 ↾ (-∞(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) ≠ ∅)
705690, 704eqnetrd 3022 1 (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) ≠ ∅)
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  ∀wral 3076  ∃wrex 3086  {crab 3412  Vcvv 3450   ⊆ wss 3896   ∩ cin 4088   ∪ cun 4148  ∅c0 4277  ifcif 4481  {csn 4584   class class class wbr 5102   ↦ cmpt 5185  dom cdm 5651  ran crn 5652   ↾ cres 5653   Fn wfn 6538  ⟶wf 6539  ‘cfv 6543  (class class class)co 7424   ↑m cmap 8855  supcsup 9439  ℂcc 11205  ℝcr 11206  0cc0 11207  1c1 11208   + caddc 11210   · cmul 11212  +∞cpnf 11347  -∞cmnf 11348  ℝ*cxr 11349   < clt 11350   ≤ cle 11351   − cmin 11548   -cneg 11549   / cdiv 11980  ℕcn 12342  ℕ0cn0 12613  ℤcz 12700  ℤ≥cuz 12972  (,)cioo 13483  (,]cioc 13484  [,]cicc 13486  ...cfz 13646  ..^cfzo 13795  ⌊cfl 13937   ↾t crest 17600  TopOpenctopn 17601  topGenctg 17617  ℂfldccnfld 21687  Topctop 23220  intcnt 23344  –cn→ccncf 25206   limℂ climc 26191
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755  ax-cnex 11263  ax-resscn 11264  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-addrcl 11268  ax-mulcl 11269  ax-mulrcl 11270  ax-mulcom 11271  ax-addass 11272  ax-mulass 11273  ax-distr 11274  ax-i2m1 11275  ax-1ne0 11276  ax-1rid 11277  ax-rnegex 11278  ax-rrecex 11279  ax-cnre 11280  ax-pre-lttri 11281  ax-pre-lttrn 11282  ax-pre-ltadd 11283  ax-pre-mulgt0 11284  ax-pre-sup 11285
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6307  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7381  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7882  df-1st 8005  df-2nd 8006  df-frecs 8307  df-wrecs 8338  df-recs 8387  df-rdg 8426  df-1o 8484  df-er 8725  df-map 8857  df-pm 8858  df-en 8982  df-dom 8983  df-sdom 8984  df-fin 8985  df-fi 9410  df-sup 9441  df-inf 9442  df-pnf 11352  df-mnf 11353  df-xr 11354  df-ltxr 11355  df-le 11356  df-sub 11550  df-neg 11551  df-div 11981  df-nn 12343  df-2 12412  df-3 12413  df-4 12414  df-5 12415  df-6 12416  df-7 12417  df-8 12418  df-9 12419  df-n0 12614  df-z 12701  df-dec 12822  df-uz 12973  df-q 13083  df-rp 13128  df-xneg 13248  df-xadd 13249  df-xmul 13250  df-ioo 13487  df-ioc 13488  df-icc 13490  df-fz 13647  df-fzo 13796  df-fl 13939  df-seq 14152  df-exp 14212  df-cj 15275  df-re 15276  df-im 15277  df-sqrt 15411  df-abs 15412  df-struct 17334  df-slot 17369  df-ndx 17381  df-base 17397  df-plusg 17450  df-mulr 17451  df-starv 17452  df-tset 17456  df-ple 17457  df-ds 17459  df-unif 17460  df-rest 17602  df-topn 17603  df-topgen 17623  df-psmet 21679  df-xmet 21680  df-met 21681  df-bl 21682  df-mopn 21683  df-cnfld 21688  df-top 23221  df-topon 23238  df-topsp 23260  df-bases 23273  df-ntr 23347  df-cn 23554  df-cnp 23555  df-xms 24648  df-ms 24649  df-cncf 25208  df-limc 26195
This theorem is used by:  fourierdlem94  47346  fourierdlem113  47365
  Copyright terms: Public domain W3C validator