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 47438
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 7484 . . . . . . . . . 10 ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ V
7 fourierdlem49.z . . . . . . . . . . 11 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
87fvmpt2 7036 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ V) → (𝑍‘𝑥) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
96, 8mpan2 704 . . . . . . . . 9 (𝑥 ∈ ℝ → (𝑍‘𝑥) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
109oveq2d 7467 . . . . . . . 8 (𝑥 ∈ ℝ → (𝑥 + (𝑍‘𝑥)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
1110mpteq2ia 5206 . . . . . . 7 (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
125, 11eqtri 2786 . . . . . 6 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
131, 2, 3, 4, 12fourierdlem4 47394 . . . . 5 (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
14 fourierdlem49.x . . . . 5 (𝜑 → 𝑋 ∈ ℝ)
1513, 14ffvelcdmd 7117 . . . 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 47392 . . . . . . . . . . . . . 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 8907 . . . . . . . . . . 11 (𝑄 ∈ (ℝ ↑m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
2523, 24syl 18 . . . . . . . . . 10 (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
2625ffnd 6740 . . . . . . . . 9 (𝜑 → 𝑄 Fn (0...𝑀))
2726ad2antrr 739 . . . . . . . 8 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → 𝑄 Fn (0...𝑀))
28 fvelrnb 6976 . . . . . . . 8 (𝑄 Fn (0...𝑀) → ((𝐸‘𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋)))
2927, 28syl 18 . . . . . . 7 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ((𝐸‘𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋)))
3016, 29mpbid 235 . . . . . 6 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋))
31 fveq2 6916 . . . . . . . . . . . 12 (𝑖 = (𝑗 − 1) → (𝑄‘𝑖) = (𝑄‘(𝑗 − 1)))
32 fvoveq1 7474 . . . . . . . . . . . 12 (𝑖 = (𝑗 − 1) → (𝑄‘(𝑖 + 1)) = (𝑄‘((𝑗 − 1) + 1)))
3331, 32oveq12d 7469 . . . . . . . . . . 11 (𝑖 = (𝑗 − 1) → ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
3433eleq2d 2850 . . . . . . . . . 10 (𝑖 = (𝑗 − 1) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) ↔ (𝐸‘𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))))
35 nnuz 13044 . . . . . . . . . . . . . 14 ℕ = (ℤ≥‘1)
36 1zzd 12767 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 1 ∈ ℤ)
37 elfzelz 13696 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
3837ad2antlr 740 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ ℤ)
39 1e0p1 12901 . . . . . . . . . . . . . . 15 1 = (0 + 1)
4038zred 12843 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ ℝ)
41 elfzle1 13700 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
4241ad2antlr 740 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 ≤ 𝑗)
43 id 23 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑄‘𝑗) = (𝐸‘𝑋) → (𝑄‘𝑗) = (𝐸‘𝑋))
4443eqcomd 2769 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑄‘𝑗) = (𝐸‘𝑋) → (𝐸‘𝑋) = (𝑄‘𝑗))
4544ad2antlr 740 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑗 = 0) → (𝐸‘𝑋) = (𝑄‘𝑗))
46 fveq2 6916 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 0 → (𝑄‘𝑗) = (𝑄‘0))
4746adantl 487 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑗 = 0) → (𝑄‘𝑗) = (𝑄‘0))
4822simprld 784 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
4948simpld 500 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑄‘0) = 𝐴)
5049ad2antrr 739 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑗 = 0) → (𝑄‘0) = 𝐴)
5145, 47, 503eqtrd 2802 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑗 = 0) → (𝐸‘𝑋) = 𝐴)
5251adantllr 732 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑗 = 0) → (𝐸‘𝑋) = 𝐴)
5352adantllr 732 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑗 = 0) → (𝐸‘𝑋) = 𝐴)
541adantr 486 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 ∈ ℝ)
551rexrd 11398 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 𝐴 ∈ ℝ*)
5655adantr 486 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 ∈ ℝ*)
572rexrd 11398 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 𝐵 ∈ ℝ*)
5857adantr 486 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → 𝐵 ∈ ℝ*)
59 simpr 490 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → (𝐸‘𝑋) ∈ (𝐴(,]𝐵))
6056, 58, 59iocgtlbd 46854 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸‘𝑋))
6154, 60gtned 11484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → (𝐸‘𝑋) ≠ 𝐴)
6261neneqd 2964 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → ¬ (𝐸‘𝑋) = 𝐴)
6362ad3antrrr 743 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑗 = 0) → ¬ (𝐸‘𝑋) = 𝐴)
6453, 63pm2.65da 829 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → ¬ 𝑗 = 0)
6564neqned 2966 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ≠ 0)
6640, 42, 65ne0gt0d 11486 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 < 𝑗)
67 0zd 12745 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 ∈ ℤ)
6867, 38zltp1led 12791 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
6966, 68mpbid 235 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (0 + 1) ≤ 𝑗)
7039, 69eqbrtrid 5146 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 1 ≤ 𝑗)
7135, 36, 38, 70eluzd 46692 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ ℕ)
72 nnm1nn0 12687 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ → (𝑗 − 1) ∈ ℕ0)
7371, 72syl 18 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ ℕ0)
74 nn0uz 13043 . . . . . . . . . . . 12 ℕ0 = (ℤ≥‘0)
7573, 74eleqtrdi 2874 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ (ℤ≥‘0))
7618nnzd 12759 . . . . . . . . . . . 12 (𝜑 → 𝑀 ∈ ℤ)
7776ad3antrrr 743 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑀 ∈ ℤ)
78 peano2zm 12779 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℤ → (𝑗 − 1) ∈ ℤ)
7937, 78syl 18 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℤ)
8079zred 12843 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
8137zred 12843 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
82 elfzel2 13694 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
8382zred 12843 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
8481ltm1d 12289 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑗)
85 elfzle2 13701 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀)
8680, 81, 83, 84, 85ltletrd 11509 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
8786ad2antlr 740 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) < 𝑀)
8875, 77, 87elfzod 13837 . . . . . . . . . 10 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ (0..^𝑀))
8925ad3antrrr 743 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑄:(0...𝑀)⟶ℝ)
9038, 78syl 18 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ ℤ)
9173nn0ge0d 12710 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 ≤ (𝑗 − 1))
9280, 83, 86ltled 11497 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ≤ 𝑀)
9392ad2antlr 740 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ≤ 𝑀)
9467, 77, 90, 91, 93elfzd 13687 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ (0...𝑀))
9589, 94ffvelcdmd 7117 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ)
9695rexrd 11398 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ*)
9725ffvelcdmda 7116 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ)
9897rexrd 11398 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ*)
9998adantlr 728 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ*)
10099adantr 486 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ∈ ℝ*)
101 iocssre 13598 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
10255, 2, 101syl2anc 596 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
103102sselda 3913 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → (𝐸‘𝑋) ∈ ℝ)
104103rexrd 11398 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → (𝐸‘𝑋) ∈ ℝ*)
105104ad2antrr 739 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ℝ*)
106 simplll 787 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝜑)
107 ovex 7484 . . . . . . . . . . . . . . . 16 (𝑗 − 1) ∈ V
108 eleq1 2852 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 − 1) → (𝑖 ∈ (0..^𝑀) ↔ (𝑗 − 1) ∈ (0..^𝑀)))
109108anbi2d 642 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 − 1) → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀))))
11031, 32breq12d 5121 . . . . . . . . . . . . . . . . 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 3258 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
114107, 111, 113vtocl 3524 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
115106, 88, 114syl2anc 596 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
11637zcnd 12844 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
117 1cnd 11341 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 1 ∈ ℂ)
118116, 117npcand 11712 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → ((𝑗 − 1) + 1) = 𝑗)
119118eqcomd 2769 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → 𝑗 = ((𝑗 − 1) + 1))
120119fveq2d 6920 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → (𝑄‘𝑗) = (𝑄‘((𝑗 − 1) + 1)))
121120eqcomd 2769 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄‘𝑗))
122121ad2antlr 740 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄‘𝑗))
123115, 122breqtrd 5137 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘𝑗))
124 simpr 490 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) = (𝐸‘𝑋))
125123, 124breqtrd 5137 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) < (𝐸‘𝑋))
126102, 15sseldd 3914 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸‘𝑋) ∈ ℝ)
127126leidd 11922 . . . . . . . . . . . . . . 15 (𝜑 → (𝐸‘𝑋) ≤ (𝐸‘𝑋))
128127ad2antrr 739 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝐸‘𝑋))
12944adantl 487 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) = (𝑄‘𝑗))
130128, 129breqtrd 5137 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘𝑗))
131130adantllr 732 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘𝑗))
13296, 100, 105, 125, 131eliocd 46792 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘𝑗)))
133120oveq2d 7467 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → ((𝑄‘(𝑗 − 1))(,](𝑄‘𝑗)) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
134133ad2antlr 740 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → ((𝑄‘(𝑗 − 1))(,](𝑄‘𝑗)) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
135132, 134eleqtrd 2866 . . . . . . . . . 10 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
13634, 88, 135rspcedvdw 3583 . . . . . . . . 9 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
137136ex 418 . . . . . . . 8 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
138137adantlr 728 . . . . . . 7 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸‘𝑋) ∈ ran 𝑄) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
139138rexlimdva 3167 . . . . . 6 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
14030, 139mpd 16 . . . . 5 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
14118ad2antrr 739 . . . . . . 7 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → 𝑀 ∈ ℕ)
14225ad2antrr 739 . . . . . . 7 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ)
143 iocssicc 13608 . . . . . . . . . 10 (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵)
14449eqcomd 2769 . . . . . . . . . . 11 (𝜑 → 𝐴 = (𝑄‘0))
14548simprd 501 . . . . . . . . . . . 12 (𝜑 → (𝑄‘𝑀) = 𝐵)
146145eqcomd 2769 . . . . . . . . . . 11 (𝜑 → 𝐵 = (𝑄‘𝑀))
147144, 146oveq12d 7469 . . . . . . . . . 10 (𝜑 → (𝐴[,]𝐵) = ((𝑄‘0)[,](𝑄‘𝑀)))
148143, 147sseqtrid 3955 . . . . . . . . 9 (𝜑 → (𝐴(,]𝐵) ⊆ ((𝑄‘0)[,](𝑄‘𝑀)))
149148sselda 3913 . . . . . . . 8 ((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → (𝐸‘𝑋) ∈ ((𝑄‘0)[,](𝑄‘𝑀)))
150149adantr 486 . . . . . . 7 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → (𝐸‘𝑋) ∈ ((𝑄‘0)[,](𝑄‘𝑀)))
151 simpr 490 . . . . . . 7 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ¬ (𝐸‘𝑋) ∈ ran 𝑄)
152 fveq2 6916 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝑄‘𝑘) = (𝑄‘𝑗))
153152breq1d 5118 . . . . . . . . 9 (𝑘 = 𝑗 → ((𝑄‘𝑘) < (𝐸‘𝑋) ↔ (𝑄‘𝑗) < (𝐸‘𝑋)))
154153cbvrabv 3426 . . . . . . . 8 {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < (𝐸‘𝑋)} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < (𝐸‘𝑋)}
155154supeq1i 9476 . . . . . . 7 sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < (𝐸‘𝑋)}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < (𝐸‘𝑋)}, ℝ, < )
156141, 142, 150, 151, 155fourierdlem25 47415 . . . . . 6 (((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
157 ioossioc 46777 . . . . . . . . 9 ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))
158157sseli 3909 . . . . . . . 8 ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
159158a1i 11 . . . . . . 7 ((((𝜑 ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
160159reximdva 3179 . . . . . 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 6037 . . . . . . . . 9 (𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ dom 𝐹)) = (𝐹 ↾ (-∞(,)(𝐸‘𝑋)))
165 fourierdlem49.f . . . . . . . . . . . 12 (𝜑 → 𝐹:𝐷⟶ℝ)
166165fdmd 6750 . . . . . . . . . . 11 (𝜑 → dom 𝐹 = 𝐷)
167166ineq2d 4120 . . . . . . . . . 10 (𝜑 → ((-∞(,)(𝐸‘𝑋)) ∩ dom 𝐹) = ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷))
168167reseq2d 5986 . . . . . . . . 9 (𝜑 → (𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ dom 𝐹)) = (𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷)))
169164, 168eqtr3id 2812 . . . . . . . 8 (𝜑 → (𝐹 ↾ (-∞(,)(𝐸‘𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷)))
1701693ad2ant1 1151 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ (-∞(,)(𝐸‘𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷)))
171170oveq1d 7466 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) = ((𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷)) limℂ (𝐸‘𝑋)))
172 ax-resscn 11296 . . . . . . . . . . 11 ℝ ⊆ ℂ
173172a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ⊆ ℂ)
174165, 173fssd 6757 . . . . . . . . 9 (𝜑 → 𝐹:𝐷⟶ℂ)
1751743ad2ant1 1151 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐹:𝐷⟶ℂ)
176 inss2 4137 . . . . . . . . 9 ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ⊆ 𝐷
177176a1i 11 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ⊆ 𝐷)
178175, 177fssresd 6779 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷)):((-∞(,)(𝐸‘𝑋)) ∩ 𝐷)⟶ℂ)
179 mnfxr 11405 . . . . . . . . . 10 -∞ ∈ ℝ*
18025adantr 486 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
181 elfzofz 13850 . . . . . . . . . . . . . 14 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
182181adantl 487 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
183180, 182ffvelcdmd 7117 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
184183rexrd 11398 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ*)
185184mnfled 13305 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -∞ ≤ (𝑄‘𝑖))
186 iooss1 13551 . . . . . . . . . 10 ((-∞ ∈ ℝ* ∧ -∞ ≤ (𝑄‘𝑖)) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ (-∞(,)(𝐸‘𝑋)))
187179, 185, 186sylancr 599 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ (-∞(,)(𝐸‘𝑋)))
1881873adant3 1150 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ (-∞(,)(𝐸‘𝑋)))
189 fzofzp1 13939 . . . . . . . . . . . . . 14 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
190189adantl 487 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
191180, 190ffvelcdmd 7117 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
1921913adant3 1150 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
193192rexrd 11398 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
1941833adant3 1150 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
195194rexrd 11398 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ*)
196 simp3 1156 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
197195, 193, 196iocleubd 46843 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ≤ (𝑄‘(𝑖 + 1)))
198 iooss2 13552 . . . . . . . . . 10 (((𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸‘𝑋) ≤ (𝑄‘(𝑖 + 1))) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
199193, 197, 198syl2anc 596 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
200 fourierdlem49.cn . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
201 cncff 25269 . . . . . . . . . . . . 13 ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
202 fdm 6749 . . . . . . . . . . . . 13 ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
203200, 201, 2023syl 19 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
204 ssdmres 6021 . . . . . . . . . . . 12 (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹 ↔ dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
205203, 204sylibr 237 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹)
206166adantr 486 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom 𝐹 = 𝐷)
207205, 206sseqtrd 3949 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
2082073adant3 1150 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
209199, 208sstrd 3923 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ 𝐷)
210188, 209ssind 4140 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷))
211 fourierdlem49.d . . . . . . . . . 10 (𝜑 → 𝐷 ⊆ ℝ)
212211, 173sstrd 3923 . . . . . . . . 9 (𝜑 → 𝐷 ⊆ ℂ)
2132123ad2ant1 1151 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐷 ⊆ ℂ)
214213ssinss2d 46351 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ⊆ ℂ)
215 eqid 2763 . . . . . . 7 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
216 eqid 2763 . . . . . . 7 ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) = ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))
2171263ad2ant1 1151 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ℝ)
218217rexrd 11398 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ℝ*)
219195, 193, 196iocgtlbd 46854 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝐸‘𝑋))
220217leidd 11922 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ≤ (𝐸‘𝑋))
221195, 218, 218, 219, 220eliocd 46792 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋)))
222 ioounsn 13648 . . . . . . . . . . 11 (((𝑄‘𝑖) ∈ ℝ* ∧ (𝐸‘𝑋) ∈ ℝ* ∧ (𝑄‘𝑖) < (𝐸‘𝑋)) → (((𝑄‘𝑖)(,)(𝐸‘𝑋)) ∪ {(𝐸‘𝑋)}) = ((𝑄‘𝑖)(,](𝐸‘𝑋)))
223195, 218, 219, 222syl3anc 1399 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖)(,)(𝐸‘𝑋)) ∪ {(𝐸‘𝑋)}) = ((𝑄‘𝑖)(,](𝐸‘𝑋)))
224223fveq2d 6920 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))‘(((𝑄‘𝑖)(,)(𝐸‘𝑋)) ∪ {(𝐸‘𝑋)})) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))‘((𝑄‘𝑖)(,](𝐸‘𝑋))))
225215cnfldtop 25157 . . . . . . . . . . 11 (TopOpen‘ℂfld) ∈ Top
226 ovex 7484 . . . . . . . . . . . . 13 (-∞(,)(𝐸‘𝑋)) ∈ V
227226inex1 5284 . . . . . . . . . . . 12 ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∈ V
228 snex 5404 . . . . . . . . . . . 12 {(𝐸‘𝑋)} ∈ V
229227, 228unex 7793 . . . . . . . . . . 11 (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}) ∈ V
230 resttop 23533 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ∈ Top ∧ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}) ∈ V) → ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) ∈ Top)
231225, 229, 230mp2an 705 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) ∈ Top
232 retop 25135 . . . . . . . . . . . 12 (topGen‘ran (,)) ∈ Top
233 iooretop 25139 . . . . . . . . . . . . 13 ((𝑄‘𝑖)(,)+∞) ∈ (topGen‘ran (,))
234233a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)+∞) ∈ (topGen‘ran (,)))
235 elrestr 17649 . . . . . . . . . . . 12 (((topGen‘ran (,)) ∈ Top ∧ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}) ∈ V ∧ ((𝑄‘𝑖)(,)+∞) ∈ (topGen‘ran (,))) → (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
236232, 229, 234, 235mp3an12i 1495 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
237 simpr 490 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 = (𝐸‘𝑋)) → 𝑥 = (𝐸‘𝑋))
238 pnfxr 11402 . . . . . . . . . . . . . . . . . . . 20 +∞ ∈ ℝ*
239238a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → +∞ ∈ ℝ*)
240217ltpnfd 13290 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) < +∞)
241195, 239, 217, 219, 240eliood 46783 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)+∞))
242 snidg 4622 . . . . . . . . . . . . . . . . . . . 20 ((𝐸‘𝑋) ∈ ℝ → (𝐸‘𝑋) ∈ {(𝐸‘𝑋)})
243 elun2 4184 . . . . . . . . . . . . . . . . . . . 20 ((𝐸‘𝑋) ∈ {(𝐸‘𝑋)} → (𝐸‘𝑋) ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))
244126, 242, 2433syl 19 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐸‘𝑋) ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))
2452443ad2ant1 1151 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))
246241, 245elind 4100 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
247246adantr 486 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
248237, 247eqeltrd 2864 . . . . . . . . . . . . . . 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 13598 . . . . . . . . . . . . . . . . . . . 20 (((𝑄‘𝑖) ∈ ℝ* ∧ (𝐸‘𝑋) ∈ ℝ) → ((𝑄‘𝑖)(,](𝐸‘𝑋)) ⊆ ℝ)
255252, 253, 254syl2anc 596 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → ((𝑄‘𝑖)(,](𝐸‘𝑋)) ⊆ ℝ)
256 simpr 490 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋)))
257255, 256sseldd 3914 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → 𝑥 ∈ ℝ)
2582573adantl3 1187 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → 𝑥 ∈ ℝ)
259253rexrd 11398 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → (𝐸‘𝑋) ∈ ℝ*)
260252, 259, 256iocgtlbd 46854 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → (𝑄‘𝑖) < 𝑥)
2612603adantl3 1187 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → (𝑄‘𝑖) < 𝑥)
262258ltpnfd 13290 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → 𝑥 < +∞)
263250, 251, 258, 261, 262eliood 46783 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → 𝑥 ∈ ((𝑄‘𝑖)(,)+∞))
264263adantr 486 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 ∈ ((𝑄‘𝑖)(,)+∞))
265179a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → -∞ ∈ ℝ*)
266259adantr 486 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ℝ*)
267257adantr 486 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 ∈ ℝ)
268267mnfltd 13293 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → -∞ < 𝑥)
269126ad3antrrr 743 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ℝ)
270252, 259, 256iocleubd 46843 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → 𝑥 ≤ (𝐸‘𝑋))
271270adantr 486 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 ≤ (𝐸‘𝑋))
272 neqne 2967 . . . . . . . . . . . . . . . . . . . . . 22 (¬ 𝑥 = (𝐸‘𝑋) → 𝑥 ≠ (𝐸‘𝑋))
273272necomd 3014 . . . . . . . . . . . . . . . . . . . . 21 (¬ 𝑥 = (𝐸‘𝑋) → (𝐸‘𝑋) ≠ 𝑥)
274273adantl 487 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → (𝐸‘𝑋) ≠ 𝑥)
275267, 269, 271, 274leneltd 11503 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 < (𝐸‘𝑋))
276265, 266, 267, 268, 275eliood 46783 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 ∈ (-∞(,)(𝐸‘𝑋)))
2772763adantll3 46333 . . . . . . . . . . . . . . . . 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 46333 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 < (𝐸‘𝑋))
286197ad2antrr 739 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘(𝑖 + 1)))
287281, 283, 284, 285, 286ltletrd 11509 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 < (𝑄‘(𝑖 + 1)))
288279, 280, 281, 282, 287eliood 46783 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
289278, 288sseldd 3914 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 ∈ 𝐷)
290277, 289elind 4100 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 ∈ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷))
291 elun1 4183 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) → 𝑥 ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))
292290, 291syl 18 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))
293264, 292elind 4100 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) ∧ ¬ 𝑥 = (𝐸‘𝑋)) → 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
294249, 293pm2.61dan 825 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋))) → 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
295195adantr 486 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))) → (𝑄‘𝑖) ∈ ℝ*)
296218adantr 486 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))) → (𝐸‘𝑋) ∈ ℝ*)
297 elinel1 4101 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) → 𝑥 ∈ ((𝑄‘𝑖)(,)+∞))
298 elioore 13546 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((𝑄‘𝑖)(,)+∞) → 𝑥 ∈ ℝ)
299298rexrd 11398 . . . . . . . . . . . . . . . 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 46835 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))) → (𝑄‘𝑖) < 𝑥)
3063053adantl3 1187 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))) → (𝑄‘𝑖) < 𝑥)
307 elinel2 4102 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) → 𝑥 ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))
308 elsni 4601 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {(𝐸‘𝑋)} → 𝑥 = (𝐸‘𝑋))
309308adantl 487 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑥 ∈ {(𝐸‘𝑋)}) → 𝑥 = (𝐸‘𝑋))
310127adantr 486 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑥 ∈ {(𝐸‘𝑋)}) → (𝐸‘𝑋) ≤ (𝐸‘𝑋))
311309, 310eqbrtrd 5133 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑥 ∈ {(𝐸‘𝑋)}) → 𝑥 ≤ (𝐸‘𝑋))
312311adantlr 728 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑥 ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) ∧ 𝑥 ∈ {(𝐸‘𝑋)}) → 𝑥 ≤ (𝐸‘𝑋))
313 simpll 779 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑥 ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) ∧ ¬ 𝑥 ∈ {(𝐸‘𝑋)}) → 𝜑)
314 elunnel2 4157 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}) ∧ ¬ 𝑥 ∈ {(𝐸‘𝑋)}) → 𝑥 ∈ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷))
315314adantll 727 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑥 ∈ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) ∧ ¬ 𝑥 ∈ {(𝐸‘𝑋)}) → 𝑥 ∈ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷))
316 elinel1 4101 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) → 𝑥 ∈ (-∞(,)(𝐸‘𝑋)))
317 elioore 13546 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (-∞(,)(𝐸‘𝑋)) → 𝑥 ∈ ℝ)
318317adantl 487 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑥 ∈ (-∞(,)(𝐸‘𝑋))) → 𝑥 ∈ ℝ)
319126adantr 486 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑥 ∈ (-∞(,)(𝐸‘𝑋))) → (𝐸‘𝑋) ∈ ℝ)
320179a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑥 ∈ (-∞(,)(𝐸‘𝑋))) → -∞ ∈ ℝ*)
321319rexrd 11398 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑥 ∈ (-∞(,)(𝐸‘𝑋))) → (𝐸‘𝑋) ∈ ℝ*)
322 simpr 490 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑥 ∈ (-∞(,)(𝐸‘𝑋))) → 𝑥 ∈ (-∞(,)(𝐸‘𝑋)))
323320, 321, 322iooltubd 46829 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑥 ∈ (-∞(,)(𝐸‘𝑋))) → 𝑥 < (𝐸‘𝑋))
324318, 319, 323ltled 11497 . . . . . . . . . . . . . . . . . . . 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 46792 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))) → 𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋)))
332294, 331impbida 813 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑥 ∈ ((𝑄‘𝑖)(,](𝐸‘𝑋)) ↔ 𝑥 ∈ (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}))))
333332eqrdv 2761 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,](𝐸‘𝑋)) = (((𝑄‘𝑖)(,)+∞) ∩ (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
334 ioossre 13578 . . . . . . . . . . . . . 14 (-∞(,)(𝐸‘𝑋)) ⊆ ℝ
335 ssinss1 4145 . . . . . . . . . . . . . 14 ((-∞(,)(𝐸‘𝑋)) ⊆ ℝ → ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ⊆ ℝ)
336334, 335mp1i 14 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ⊆ ℝ)
337217snssd 4749 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → {(𝐸‘𝑋)} ⊆ ℝ)
338336, 337unssd 4193 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}) ⊆ ℝ)
339 eqid 2763 . . . . . . . . . . . . 13 (topGen‘ran (,)) = (topGen‘ran (,))
340215, 339rerest 25178 . . . . . . . . . . . 12 ((((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)}) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) = ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
341338, 340syl 18 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})) = ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
342236, 333, 3413eltr4d 2879 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,](𝐸‘𝑋)) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))
343 isopn3i 23455 . . . . . . . . . 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 2799 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,](𝐸‘𝑋)) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))‘(((𝑄‘𝑖)(,)(𝐸‘𝑋)) ∪ {(𝐸‘𝑋)})))
346221, 345eleqtrd 2866 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸‘𝑋)) ∩ 𝐷) ∪ {(𝐸‘𝑋)})))‘(((𝑄‘𝑖)(,)(𝐸‘𝑋)) ∪ {(𝐸‘𝑋)})))
347178, 210, 214, 215, 216, 346limcres 26261 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷)) ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) = ((𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷)) limℂ (𝐸‘𝑋)))
348210resabs1d 6016 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷)) ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))))
349348oveq1d 7466 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)(𝐸‘𝑋)) ∩ 𝐷)) ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
350171, 347, 3493eqtr2d 2804 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
351174ffdmd 6770 . . . . . . . . . . 11 (𝜑 → 𝐹:dom 𝐹⟶ℂ)
352351adantr 486 . . . . . . . . . 10 ((𝜑 ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → 𝐹:dom 𝐹⟶ℂ)
3533523ad2antl1 1204 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → 𝐹:dom 𝐹⟶ℂ)
354 ioosscn 13579 . . . . . . . . . 10 ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ ℂ
355354a1i 11 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ ℂ)
356166eqcomd 2769 . . . . . . . . . . . 12 (𝜑 → 𝐷 = dom 𝐹)
3573563ad2ant1 1151 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐷 = dom 𝐹)
358209, 357sseqtrd 3949 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ dom 𝐹)
359358adantr 486 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) ⊆ dom 𝐹)
360 oveq2 7459 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋 → (𝐵 − 𝑥) = (𝐵 − 𝑋))
361360fvoveq1d 7473 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑋) / 𝑇)))
362361oveq1d 7466 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
3632, 14resubcld 11783 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵 − 𝑋) ∈ ℝ)
3642, 1resubcld 11783 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
3654, 364eqeltrid 2868 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 𝑇 ∈ ℝ)
3661, 2posdifd 11943 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
3673, 366mpbid 235 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 < (𝐵 − 𝐴))
368367, 4breqtrrdi 5153 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 < 𝑇)
369368gt0ne0d 11920 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 𝑇 ≠ 0)
370363, 365, 369redivcld 12185 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 − 𝑋) / 𝑇) ∈ ℝ)
371370flcld 13978 . . . . . . . . . . . . . . . . 17 (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
372371zred 12843 . . . . . . . . . . . . . . . 16 (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℝ)
373372, 365remulcld 11378 . . . . . . . . . . . . . . 15 (𝜑 → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
3747, 362, 14, 373fvmptd3 7048 . . . . . . . . . . . . . 14 (𝜑 → (𝑍‘𝑋) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
375374, 373eqeltrd 2864 . . . . . . . . . . . . 13 (𝜑 → (𝑍‘𝑋) ∈ ℝ)
376375recnd 11376 . . . . . . . . . . . 12 (𝜑 → (𝑍‘𝑋) ∈ ℂ)
377376adantr 486 . . . . . . . . . . 11 ((𝜑 ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → (𝑍‘𝑋) ∈ ℂ)
3783773ad2antl1 1204 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → (𝑍‘𝑋) ∈ ℂ)
379378negcld 11695 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → -(𝑍‘𝑋) ∈ ℂ)
380 eqid 2763 . . . . . . . . 9 {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))} = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))}
381 ioosscn 13579 . . . . . . . . . . . . . . . . . 18 (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ ℂ
382381sseli 3909 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) → 𝑦 ∈ ℂ)
383382adantl 487 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ ℂ)
384376adantr 486 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑍‘𝑋) ∈ ℂ)
385383, 384pncand 11709 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑦 + (𝑍‘𝑋)) − (𝑍‘𝑋)) = 𝑦)
386385eqcomd 2769 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) − (𝑍‘𝑋)))
3873863ad2antl1 1204 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) − (𝑍‘𝑋)))
388374oveq2d 7467 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑦 + (𝑍‘𝑋)) − (𝑍‘𝑋)) = ((𝑦 + (𝑍‘𝑋)) − ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
389388adantr 486 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑦 + (𝑍‘𝑋)) − (𝑍‘𝑋)) = ((𝑦 + (𝑍‘𝑋)) − ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
390383, 384addcld 11367 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ℂ)
391373recnd 11376 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
392391adantr 486 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
393390, 392negsubd 11714 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑦 + (𝑍‘𝑋)) + -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + (𝑍‘𝑋)) − ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
394371zcnd 12844 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℂ)
395365recnd 11376 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 𝑇 ∈ ℂ)
396394, 395mulneg1d 11808 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
397396eqcomd 2769 . . . . . . . . . . . . . . . . . 18 (𝜑 → -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
398397oveq2d 7467 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑦 + (𝑍‘𝑋)) + -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
399398adantr 486 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑦 + (𝑍‘𝑋)) + -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
400389, 393, 3993eqtr2d 2804 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑦 + (𝑍‘𝑋)) − (𝑍‘𝑋)) = ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
4014003ad2antl1 1204 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑦 + (𝑍‘𝑋)) − (𝑍‘𝑋)) = ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
402371znegcld 12845 . . . . . . . . . . . . . . . . 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 11398 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐸‘𝑋) ∈ ℝ*)
409408ad2antrr 739 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝐸‘𝑋) ∈ ℝ*)
410 elioore 13546 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) → 𝑦 ∈ ℝ)
411410adantl 487 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
412375adantr 486 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑍‘𝑋) ∈ ℝ)
413411, 412readdcld 11377 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
414413adantlr 728 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
415375adantr 486 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑍‘𝑋) ∈ ℝ)
416183, 415resubcld 11783 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ)
417416rexrd 11398 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ*)
418417adantr 486 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ*)
41914rexrd 11398 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 𝑋 ∈ ℝ*)
420419ad2antrr 739 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑋 ∈ ℝ*)
421 simpr 490 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋))
422418, 420, 421ioogtlbd 46835 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑦)
423183adantr 486 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) ∈ ℝ)
424375ad2antrr 739 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑍‘𝑋) ∈ ℝ)
425410adantl 487 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
426423, 424, 425ltsubaddd 11952 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑦 ↔ (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋))))
427422, 426mpbid 235 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋)))
42814ad2antrr 739 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑋 ∈ ℝ)
429418, 420, 421iooltubd 46829 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 < 𝑋)
430425, 428, 424, 429ltadd1dd 11967 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝑋 + (𝑍‘𝑋)))
431 id 23 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑋 → 𝑥 = 𝑋)
432 fveq2 6916 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑋 → (𝑍‘𝑥) = (𝑍‘𝑋))
433431, 432oveq12d 7469 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑋 → (𝑥 + (𝑍‘𝑥)) = (𝑋 + (𝑍‘𝑋)))
43414, 375readdcld 11377 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑋 + (𝑍‘𝑋)) ∈ ℝ)
4355, 433, 14, 434fvmptd3 7048 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐸‘𝑋) = (𝑋 + (𝑍‘𝑋)))
436435eqcomd 2769 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑋 + (𝑍‘𝑋)) = (𝐸‘𝑋))
437436ad2antrr 739 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑋 + (𝑍‘𝑋)) = (𝐸‘𝑋))
438430, 437breqtrd 5137 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝐸‘𝑋))
439407, 409, 414, 427, 438eliood 46783 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋)))
4404393adantl3 1187 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋)))
441406, 440sseldd 3914 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ 𝐷)
442405, 441, 4043jca 1146 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ))
443 eleq1 2852 . . . . . . . . . . . . . . . . . 18 (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ))
4444433anbi3d 1471 . . . . . . . . . . . . . . . . 17 (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)))
445 oveq1 7458 . . . . . . . . . . . . . . . . . . 19 (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑘 · 𝑇) = ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
446445oveq2d 7467 . . . . . . . . . . . . . . . . . 18 (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) = ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
447446eleq1d 2849 . . . . . . . . . . . . . . . . 17 (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
448444, 447imbi12d 347 . . . . . . . . . . . . . . . 16 (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)))
449 ovex 7484 . . . . . . . . . . . . . . . . 17 (𝑦 + (𝑍‘𝑋)) ∈ V
450 eleq1 2852 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑦 + (𝑍‘𝑋)) → (𝑥 ∈ 𝐷 ↔ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷))
4514503anbi2d 1470 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑦 + (𝑍‘𝑋)) → ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ)))
452 oveq1 7458 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑦 + (𝑍‘𝑋)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)))
453452eleq1d 2849 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑦 + (𝑍‘𝑋)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷))
454451, 453imbi12d 347 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑦 + (𝑍‘𝑋)) → (((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)))
455 fourierdlem49.dper . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)
456449, 454, 455vtocl 3524 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)
457448, 456vtoclg 3521 . . . . . . . . . . . . . . 15 ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ → ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
458404, 442, 457sylc 66 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑦 + (𝑍‘𝑋)) + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
459401, 458eqeltrd 2864 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑦 + (𝑍‘𝑋)) − (𝑍‘𝑋)) ∈ 𝐷)
460387, 459eqeltrd 2864 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ 𝐷)
461460ssd 46370 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷)
462183recnd 11376 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℂ)
463376adantr 486 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑍‘𝑋) ∈ ℂ)
464462, 463negsubd 11714 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) + -(𝑍‘𝑋)) = ((𝑄‘𝑖) − (𝑍‘𝑋)))
465464eqcomd 2769 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) = ((𝑄‘𝑖) + -(𝑍‘𝑋)))
466435oveq1d 7466 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸‘𝑋) + -(𝑍‘𝑋)) = ((𝑋 + (𝑍‘𝑋)) + -(𝑍‘𝑋)))
467434recnd 11376 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑋 + (𝑍‘𝑋)) ∈ ℂ)
468467, 376negsubd 11714 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑋 + (𝑍‘𝑋)) + -(𝑍‘𝑋)) = ((𝑋 + (𝑍‘𝑋)) − (𝑍‘𝑋)))
46914recnd 11376 . . . . . . . . . . . . . . . . 17 (𝜑 → 𝑋 ∈ ℂ)
470469, 376pncand 11709 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑋 + (𝑍‘𝑋)) − (𝑍‘𝑋)) = 𝑋)
471466, 468, 4703eqtrrd 2803 . . . . . . . . . . . . . . 15 (𝜑 → 𝑋 = ((𝐸‘𝑋) + -(𝑍‘𝑋)))
472471adantr 486 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 = ((𝐸‘𝑋) + -(𝑍‘𝑋)))
473465, 472oveq12d 7469 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) = (((𝑄‘𝑖) + -(𝑍‘𝑋))(,)((𝐸‘𝑋) + -(𝑍‘𝑋))))
474126adantr 486 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐸‘𝑋) ∈ ℝ)
475415renegcld 11782 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -(𝑍‘𝑋) ∈ ℝ)
476183, 474, 475iooshift 46807 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘𝑖) + -(𝑍‘𝑋))(,)((𝐸‘𝑋) + -(𝑍‘𝑋))) = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))})
477473, 476eqtr2d 2799 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))} = (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋))
4784773adant3 1150 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))} = (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋))
4791663ad2ant1 1151 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → dom 𝐹 = 𝐷)
480461, 478, 4793sstr4d 3968 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))} ⊆ dom 𝐹)
481480adantr 486 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))} ⊆ dom 𝐹)
482374negeqd 11590 . . . . . . . . . . . . . . . 16 (𝜑 → -(𝑍‘𝑋) = -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
483482, 397eqtrd 2798 . . . . . . . . . . . . . . 15 (𝜑 → -(𝑍‘𝑋) = ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
484483oveq2d 7467 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 + -(𝑍‘𝑋)) = (𝑥 + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
485484fveq2d 6920 . . . . . . . . . . . . 13 (𝜑 → (𝐹‘(𝑥 + -(𝑍‘𝑋))) = (𝐹‘(𝑥 + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))))
486485adantr 486 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) → (𝐹‘(𝑥 + -(𝑍‘𝑋))) = (𝐹‘(𝑥 + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))))
4874863ad2antl1 1204 . . . . . . . . . . 11 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) → (𝐹‘(𝑥 + -(𝑍‘𝑋))) = (𝐹‘(𝑥 + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))))
488402adantr 486 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
4894883ad2antl1 1204 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
490 simpl1 1210 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) → 𝜑)
491209sselda 3913 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) → 𝑥 ∈ 𝐷)
492490, 491, 4893jca 1146 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) → (𝜑 ∧ 𝑥 ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ))
4934433anbi3d 1471 . . . . . . . . . . . . . 14 (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ 𝑥 ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)))
494445oveq2d 7467 . . . . . . . . . . . . . . 15 (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = (𝑥 + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
495494fveqeq2d 6924 . . . . . . . . . . . . . 14 (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥) ↔ (𝐹‘(𝑥 + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))) = (𝐹‘𝑥)))
496493, 495imbi12d 347 . . . . . . . . . . . . 13 (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))) = (𝐹‘𝑥))))
497 fourierdlem49.per . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥))
498496, 497vtoclg 3521 . . . . . . . . . . . 12 ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ → ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))) = (𝐹‘𝑥)))
499489, 492, 498sylc 66 . . . . . . . . . . 11 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) → (𝐹‘(𝑥 + ( -(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))) = (𝐹‘𝑥))
500487, 499eqtrd 2798 . . . . . . . . . 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 46913 . . . . . . . 8 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → 𝑦 ∈ ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))}) limℂ ((𝐸‘𝑋) + -(𝑍‘𝑋))))
504477reseq2d 5986 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))}) = (𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)))
505472eqcomd 2769 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸‘𝑋) + -(𝑍‘𝑋)) = 𝑋)
506504, 505oveq12d 7469 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))}) limℂ ((𝐸‘𝑋) + -(𝑍‘𝑋))) = ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋))
5075063adant3 1150 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))}) limℂ ((𝐸‘𝑋) + -(𝑍‘𝑋))) = ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋))
508507adantr 486 . . . . . . . 8 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋))) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄‘𝑖)(,)(𝐸‘𝑋))𝑧 = (𝑥 + -(𝑍‘𝑋))}) limℂ ((𝐸‘𝑋) + -(𝑍‘𝑋))) = ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋))
509503, 508eleqtrd 2866 . . . . . . 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 3950 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ dom 𝐹)
514513adantr 486 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋)) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ dom 𝐹)
515376adantr 486 . . . . . . . . . 10 ((𝜑 ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋)) → (𝑍‘𝑋) ∈ ℂ)
5165153ad2antl1 1204 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋)) → (𝑍‘𝑋) ∈ ℂ)
517 eqid 2763 . . . . . . . . 9 {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))} = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))}
518462, 463npcand 11712 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘𝑖) − (𝑍‘𝑋)) + (𝑍‘𝑋)) = (𝑄‘𝑖))
519518eqcomd 2769 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = (((𝑄‘𝑖) − (𝑍‘𝑋)) + (𝑍‘𝑋)))
520435adantr 486 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐸‘𝑋) = (𝑋 + (𝑍‘𝑋)))
521519, 520oveq12d 7469 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝐸‘𝑋)) = ((((𝑄‘𝑖) − (𝑍‘𝑋)) + (𝑍‘𝑋))(,)(𝑋 + (𝑍‘𝑋))))
52214adantr 486 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
523416, 522, 415iooshift 46807 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((((𝑄‘𝑖) − (𝑍‘𝑋)) + (𝑍‘𝑋))(,)(𝑋 + (𝑍‘𝑋))) = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))})
524521, 523eqtr2d 2799 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))} = ((𝑄‘𝑖)(,)(𝐸‘𝑋)))
5255243adant3 1150 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))} = ((𝑄‘𝑖)(,)(𝐸‘𝑋)))
526209, 525, 4793sstr4d 3968 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))} ⊆ dom 𝐹)
527526adantr 486 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋)) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))} ⊆ dom 𝐹)
528374oveq2d 7467 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 + (𝑍‘𝑋)) = (𝑥 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
529528fveq2d 6920 . . . . . . . . . . . . 13 (𝜑 → (𝐹‘(𝑥 + (𝑍‘𝑋))) = (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))))
530529adantr 486 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍‘𝑋))) = (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))))
5315303ad2antl1 1204 . . . . . . . . . . 11 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍‘𝑋))) = (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))))
532371adantr 486 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
5335323ad2antl1 1204 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
534 simpl1 1210 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝜑)
535461sselda 3913 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑥 ∈ 𝐷)
536534, 535, 5333jca 1146 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝜑 ∧ 𝑥 ∈ 𝐷 ∧ (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ))
537 eleq1 2852 . . . . . . . . . . . . . . 15 (𝑘 = (⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ))
5385373anbi3d 1471 . . . . . . . . . . . . . 14 (𝑘 = (⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ 𝑥 ∈ 𝐷 ∧ (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)))
539 oveq1 7458 . . . . . . . . . . . . . . . 16 (𝑘 = (⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑘 · 𝑇) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
540539oveq2d 7467 . . . . . . . . . . . . . . 15 (𝑘 = (⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = (𝑥 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
541540fveqeq2d 6924 . . . . . . . . . . . . . 14 (𝑘 = (⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥) ↔ (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))) = (𝐹‘𝑥)))
542538, 541imbi12d 347 . . . . . . . . . . . . 13 (𝑘 = (⌊‘((𝐵 − 𝑋) / 𝑇)) → (((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))) = (𝐹‘𝑥))))
543542, 497vtoclg 3521 . . . . . . . . . . . 12 ((⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ → ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))) = (𝐹‘𝑥)))
544533, 536, 543sylc 66 . . . . . . . . . . 11 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))) = (𝐹‘𝑥))
545531, 544eqtrd 2798 . . . . . . . . . 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 46913 . . . . . . . 8 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋)) → 𝑦 ∈ ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))}) limℂ (𝑋 + (𝑍‘𝑋))))
549524reseq2d 5986 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))}) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))))
550436adantr 486 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑍‘𝑋)) = (𝐸‘𝑋))
551549, 550oveq12d 7469 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))}) limℂ (𝑋 + (𝑍‘𝑋))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
5525513adant3 1150 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))}) limℂ (𝑋 + (𝑍‘𝑋))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
553552adantr 486 . . . . . . . 8 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋)) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍‘𝑋))}) limℂ (𝑋 + (𝑍‘𝑋))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
554548, 553eleqtrd 2866 . . . . . . 7 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋)) → 𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
555509, 554impbida 813 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) ↔ 𝑦 ∈ ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋)))
556555eqrdv 2761 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) = ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋))
557 resindm 6037 . . . . . . . . 9 (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)) = (𝐹 ↾ (-∞(,)𝑋))
558166ineq2d 4120 . . . . . . . . . 10 (𝜑 → ((-∞(,)𝑋) ∩ dom 𝐹) = ((-∞(,)𝑋) ∩ 𝐷))
559558reseq2d 5986 . . . . . . . . 9 (𝜑 → (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)))
560557, 559eqtr3id 2812 . . . . . . . 8 (𝜑 → (𝐹 ↾ (-∞(,)𝑋)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)))
561560oveq1d 7466 . . . . . . 7 (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) = ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) limℂ 𝑋))
5625613ad2ant1 1151 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) = ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) limℂ 𝑋))
563 inss2 4137 . . . . . . . . 9 ((-∞(,)𝑋) ∩ 𝐷) ⊆ 𝐷
564563a1i 11 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)𝑋) ∩ 𝐷) ⊆ 𝐷)
565175, 564fssresd 6779 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)):((-∞(,)𝑋) ∩ 𝐷)⟶ℂ)
566417mnfled 13305 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -∞ ≤ ((𝑄‘𝑖) − (𝑍‘𝑋)))
567 iooss1 13551 . . . . . . . . . 10 ((-∞ ∈ ℝ* ∧ -∞ ≤ ((𝑄‘𝑖) − (𝑍‘𝑋))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ (-∞(,)𝑋))
568179, 566, 567sylancr 599 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ (-∞(,)𝑋))
5695683adant3 1150 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ (-∞(,)𝑋))
570569, 461ssind 4140 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ ((-∞(,)𝑋) ∩ 𝐷))
571213ssinss2d 46351 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)𝑋) ∩ 𝐷) ⊆ ℂ)
572 eqid 2763 . . . . . . 7 ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) = ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
5734173adant3 1150 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ*)
5744193ad2ant1 1151 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ*)
5754353ad2ant1 1151 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) = (𝑋 + (𝑍‘𝑋)))
576219, 575breqtrd 5137 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝑋 + (𝑍‘𝑋)))
5773753ad2ant1 1151 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑍‘𝑋) ∈ ℝ)
578143ad2ant1 1151 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
579194, 577, 578ltsubaddd 11952 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋 ↔ (𝑄‘𝑖) < (𝑋 + (𝑍‘𝑋))))
580576, 579mpbird 260 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋)
58114leidd 11922 . . . . . . . . . 10 (𝜑 → 𝑋 ≤ 𝑋)
5825813ad2ant1 1151 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ≤ 𝑋)
583573, 574, 574, 580, 582eliocd 46792 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋))
584 ioounsn 13648 . . . . . . . . . . 11 ((((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ∧ ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋) → ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ∪ {𝑋}) = (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋))
585573, 574, 580, 584syl3anc 1399 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ∪ {𝑋}) = (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋))
586585fveq2d 6920 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘((((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ∪ {𝑋})) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘(((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)))
587 ovex 7484 . . . . . . . . . . . . 13 (-∞(,)𝑋) ∈ V
588587inex1 5284 . . . . . . . . . . . 12 ((-∞(,)𝑋) ∩ 𝐷) ∈ V
589 snex 5404 . . . . . . . . . . . 12 {𝑋} ∈ V
590588, 589unex 7793 . . . . . . . . . . 11 (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V
591 resttop 23533 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ∈ Top ∧ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V) → ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ Top)
592225, 590, 591mp2an 705 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ Top
593 iooretop 25139 . . . . . . . . . . . . 13 (((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∈ (topGen‘ran (,))
594593a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∈ (topGen‘ran (,)))
595 elrestr 17649 . . . . . . . . . . . 12 (((topGen‘ran (,)) ∈ Top ∧ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V ∧ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∈ (topGen‘ran (,))) → ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
596232, 590, 594, 595mp3an12i 1495 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
597417adantr 486 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ*)
598238a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → +∞ ∈ ℝ*)
59914ad2antrr 739 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → 𝑋 ∈ ℝ)
600 iocssre 13598 . . . . . . . . . . . . . . . . . 18 ((((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ* ∧ 𝑋 ∈ ℝ) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋) ⊆ ℝ)
601597, 599, 600syl2anc 596 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋) ⊆ ℝ)
602 simpr 490 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋))
603601, 602sseldd 3914 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → 𝑥 ∈ ℝ)
604419ad2antrr 739 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → 𝑋 ∈ ℝ*)
605597, 604, 602iocgtlbd 46854 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑥)
606603ltpnfd 13290 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → 𝑥 < +∞)
607597, 598, 603, 605, 606eliood 46783 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞))
6086073adantl3 1187 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞))
609 eqvisset 3474 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋 → 𝑋 ∈ V)
610 snidg 4622 . . . . . . . . . . . . . . . . . . 19 (𝑋 ∈ V → 𝑋 ∈ {𝑋})
611609, 610syl 18 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋 → 𝑋 ∈ {𝑋})
612431, 611eqeltrd 2864 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋 → 𝑥 ∈ {𝑋})
613 elun2 4184 . . . . . . . . . . . . . . . . 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 46843 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → 𝑥 ≤ 𝑋)
623622adantr 486 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ≤ 𝑋)
624431eqcoms 2771 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 = 𝑥 → 𝑥 = 𝑋)
625624necon3bi 2985 . . . . . . . . . . . . . . . . . . . 20 (¬ 𝑥 = 𝑋 → 𝑋 ≠ 𝑥)
626625adantl 487 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑋 ≠ 𝑥)
627619, 621, 623, 626leneltd 11503 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 < 𝑋)
628617, 618, 619, 620, 627eliood 46783 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋))
6296283adantll3 46333 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋))
630570sselda 3913 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷))
631 elun1 4183 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
632630, 631syl 18 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
633616, 629, 632syl2anc 596 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
634615, 633pm2.61dan 825 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
635608, 634elind 4100 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋)) → 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
636573adantr 486 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ*)
637574adantr 486 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑋 ∈ ℝ*)
638 elinel1 4101 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞))
639 elioore 13546 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) → 𝑥 ∈ ℝ)
640638, 639syl 18 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ ℝ)
641640rexrd 11398 . . . . . . . . . . . . . . 15 (𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ ℝ*)
642641adantl 487 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ∈ ℝ*)
643417adantr 486 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ*)
644238a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → +∞ ∈ ℝ*)
645638adantl 487 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞))
646643, 644, 645ioogtlbd 46835 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑥)
6476463adantl3 1187 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑥)
648 elinel2 4102 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
649 elsni 4601 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ {𝑋} → 𝑥 = 𝑋)
650649adantl 487 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑥 ∈ {𝑋}) → 𝑥 = 𝑋)
651581adantr 486 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑥 ∈ {𝑋}) → 𝑋 ≤ 𝑋)
652650, 651eqbrtrd 5133 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑥 ∈ {𝑋}) → 𝑥 ≤ 𝑋)
653652adantlr 728 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ 𝑥 ∈ {𝑋}) → 𝑥 ≤ 𝑋)
654 simpll 779 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝜑)
655 elunnel2 4157 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷))
656655adantll 727 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷))
657656elin1d 4104 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ∈ (-∞(,)𝑋))
658 elioore 13546 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (-∞(,)𝑋) → 𝑥 ∈ ℝ)
659658adantl 487 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑥 ∈ (-∞(,)𝑋)) → 𝑥 ∈ ℝ)
66014adantr 486 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑥 ∈ (-∞(,)𝑋)) → 𝑋 ∈ ℝ)
661179a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑥 ∈ (-∞(,)𝑋)) → -∞ ∈ ℝ*)
662419adantr 486 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑥 ∈ (-∞(,)𝑋)) → 𝑋 ∈ ℝ*)
663 simpr 490 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑥 ∈ (-∞(,)𝑋)) → 𝑥 ∈ (-∞(,)𝑋))
664661, 662, 663iooltubd 46829 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑥 ∈ (-∞(,)𝑋)) → 𝑥 < 𝑋)
665659, 660, 664ltled 11497 . . . . . . . . . . . . . . . . . 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 46792 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋))
671635, 670impbida 813 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑥 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋) ↔ 𝑥 ∈ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))))
672671eqrdv 2761 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋) = ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
673211ssinss2d 46351 . . . . . . . . . . . . . 14 (𝜑 → ((-∞(,)𝑋) ∩ 𝐷) ⊆ ℝ)
67414snssd 4749 . . . . . . . . . . . . . 14 (𝜑 → {𝑋} ⊆ ℝ)
675673, 674unssd 4193 . . . . . . . . . . . . 13 (𝜑 → (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ⊆ ℝ)
6766753ad2ant1 1151 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ⊆ ℝ)
677215, 339rerest 25178 . . . . . . . . . . . 12 ((((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) = ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
678676, 677syl 18 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) = ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
679596, 672, 6783eltr4d 2879 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
680 isopn3i 23455 . . . . . . . . . 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 2799 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,]𝑋) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘((((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ∪ {𝑋})))
683583, 682eleqtrd 2866 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘((((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ∪ {𝑋})))
684565, 570, 571, 215, 572, 683limcres 26261 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋) = ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) limℂ 𝑋))
685570resabs1d 6016 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) = (𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)))
686685oveq1d 7466 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋) = ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋))
687562, 684, 6863eqtr2rd 2805 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) limℂ 𝑋) = ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋))
688350, 556, 6873eqtrrd 2803 . . . 4 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) = ((𝐹 ↾ (-∞(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
689688rexlimdv3a 3171 . . 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 2763 . . . . . . . 8 if((𝐸‘𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸‘𝑋))) = if((𝐸‘𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸‘𝑋)))
696 eqid 2763 . . . . . . . 8 ((TopOpen‘ℂfld) ↾t (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))})) = ((TopOpen‘ℂfld) ↾t (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))}))
697194, 192, 691, 692, 694, 194, 217, 219, 199, 695, 696fourierdlem33 47423 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → if((𝐸‘𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸‘𝑋))) ∈ (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
698199resabs1d 6016 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))))
699698oveq1d 7466 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
700697, 699eleqtrd 2866 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → if((𝐸‘𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸‘𝑋))) ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)))
701700ne0d 4291 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) ≠ ∅)
702350, 701eqnetrd 3026 . . . 4 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) ≠ ∅)
703702rexlimdv3a 3171 . . 3 (𝜑 → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ (-∞(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) ≠ ∅))
704163, 703mpd 16 . 2 (𝜑 → ((𝐹 ↾ (-∞(,)(𝐸‘𝑋))) limℂ (𝐸‘𝑋)) ≠ ∅)
705690, 704eqnetrd 3026 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 1570   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  ∃wrex 3090  {crab 3416  Vcvv 3454   ⊆ wss 3900   ∩ cin 4092   ∪ cun 4152  ∅c0 4281  ifcif 4485  {csn 4588   class class class wbr 5108   ↦ cmpt 5192  dom cdm 5658  ran crn 5659   ↾ cres 5660   Fn wfn 6561  ⟶wf 6562  ‘cfv 6566  (class class class)co 7451   ↑m cmap 8885  supcsup 9469  ℂcc 11237  ℝcr 11238  0cc0 11239  1c1 11240   + caddc 11242   · cmul 11244  +∞cpnf 11379  -∞cmnf 11380  ℝ*cxr 11381   < clt 11382   ≤ cle 11383   − cmin 11580   -cneg 11581   / cdiv 12013  ℕcn 12375  ℕ0cn0 12646  ℤcz 12733  ℤ≥cuz 13005  (,)cioo 13516  (,]cioc 13517  [,]cicc 13519  ...cfz 13679  ..^cfzo 13828  ⌊cfl 13970   ↾t crest 17641  TopOpenctopn 17642  topGenctg 17658  ℂfldccnfld 21729  Topctop 23266  intcnt 23390  –cn→ccncf 25252   limℂ climc 26237
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5238  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-cnex 11295  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1ne0 11308  ax-1rid 11309  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314  ax-pre-ltadd 11315  ax-pre-mulgt0 11316  ax-pre-sup 11317
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4841  df-uni 4873  df-int 4913  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-riota 7408  df-ov 7454  df-oprab 7455  df-mpo 7456  df-om 7912  df-1st 8035  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-1o 8514  df-er 8755  df-map 8887  df-pm 8888  df-en 9012  df-dom 9013  df-sdom 9014  df-fin 9015  df-fi 9440  df-sup 9471  df-inf 9472  df-pnf 11384  df-mnf 11385  df-xr 11386  df-ltxr 11387  df-le 11388  df-sub 11582  df-neg 11583  df-div 12014  df-nn 12376  df-2 12445  df-3 12446  df-4 12447  df-5 12448  df-6 12449  df-7 12450  df-8 12451  df-9 12452  df-n0 12647  df-z 12734  df-dec 12855  df-uz 13006  df-q 13116  df-rp 13161  df-xneg 13281  df-xadd 13282  df-xmul 13283  df-ioo 13520  df-ioc 13521  df-icc 13523  df-fz 13680  df-fzo 13829  df-fl 13972  df-seq 14185  df-exp 14245  df-cj 15309  df-re 15310  df-im 15311  df-sqrt 15445  df-abs 15446  df-struct 17369  df-slot 17404  df-ndx 17416  df-base 17432  df-plusg 17486  df-mulr 17487  df-starv 17488  df-tset 17492  df-ple 17493  df-ds 17495  df-unif 17496  df-euf 17499  df-rest 17643  df-topn 17644  df-topgen 17664  df-psmet 21721  df-xmet 21722  df-met 21723  df-bl 21724  df-mopn 21725  df-cnfld 21730  df-top 23267  df-topon 23284  df-topsp 23306  df-bases 23319  df-ntr 23393  df-cn 23600  df-cnp 23601  df-xms 24694  df-ms 24695  df-cncf 25254  df-limc 26241
This theorem is used by:  fourierdlem94  47483  fourierdlem113  47502
  Copyright terms: Public domain W3C validator