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 40372
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 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (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 6678 . . . . . . . . . 10 ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ V
7 fourierdlem49.z . . . . . . . . . . 11 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
87fvmpt2 6291 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ V) → (𝑍𝑥) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
96, 8mpan2 707 . . . . . . . . 9 (𝑥 ∈ ℝ → (𝑍𝑥) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
109oveq2d 6666 . . . . . . . 8 (𝑥 ∈ ℝ → (𝑥 + (𝑍𝑥)) = (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
1110mpteq2ia 4740 . . . . . . 7 (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
125, 11eqtri 2644 . . . . . 6 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
131, 2, 3, 4, 12fourierdlem4 40328 . . . . 5 (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))
14 fourierdlem49.x . . . . 5 (𝜑𝑋 ∈ ℝ)
1513, 14ffvelrnd 6360 . . . 4 (𝜑 → (𝐸𝑋) ∈ (𝐴(,]𝐵))
16 simpr 477 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → (𝐸𝑋) ∈ ran 𝑄)
17 fourierdlem49.q . . . . . . . . . . . . 13 (𝜑𝑄 ∈ (𝑃𝑀))
18 fourierdlem49.m . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℕ)
19 fourierdlem49.p . . . . . . . . . . . . . . 15 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
2019fourierdlem2 40326 . . . . . . . . . . . . . 14 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
2118, 20syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
2217, 21mpbid 222 . . . . . . . . . . . 12 (𝜑 → (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
2322simpld 475 . . . . . . . . . . 11 (𝜑𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)))
24 elmapi 7879 . . . . . . . . . . 11 (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
2523, 24syl 17 . . . . . . . . . 10 (𝜑𝑄:(0...𝑀)⟶ℝ)
26 ffn 6045 . . . . . . . . . 10 (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
2725, 26syl 17 . . . . . . . . 9 (𝜑𝑄 Fn (0...𝑀))
2827ad2antrr 762 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → 𝑄 Fn (0...𝑀))
29 fvelrnb 6243 . . . . . . . 8 (𝑄 Fn (0...𝑀) → ((𝐸𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋)))
3028, 29syl 17 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → ((𝐸𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋)))
3116, 30mpbid 222 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋))
32 1zzd 11408 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 1 ∈ ℤ)
33 elfzelz 12342 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
3433ad2antlr 763 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℤ)
35 1e0p1 11552 . . . . . . . . . . . . . . . . 17 1 = (0 + 1)
3635a1i 11 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 1 = (0 + 1))
3734zred 11482 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℝ)
38 elfzle1 12344 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
3938ad2antlr 763 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ≤ 𝑗)
40 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑄𝑗) = (𝐸𝑋) → (𝑄𝑗) = (𝐸𝑋))
4140eqcomd 2628 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑄𝑗) = (𝐸𝑋) → (𝐸𝑋) = (𝑄𝑗))
4241ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝐸𝑋) = (𝑄𝑗))
43 fveq2 6191 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = 0 → (𝑄𝑗) = (𝑄‘0))
4443adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝑄𝑗) = (𝑄‘0))
4522simprld 795 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵))
4645simpld 475 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑄‘0) = 𝐴)
4746ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝑄‘0) = 𝐴)
4842, 44, 473eqtrd 2660 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝐸𝑋) = 𝐴)
4948adantllr 755 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝐸𝑋) = 𝐴)
5049adantllr 755 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝐸𝑋) = 𝐴)
511adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 ∈ ℝ)
521rexrd 10089 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐴 ∈ ℝ*)
5352adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 ∈ ℝ*)
542rexrd 10089 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐵 ∈ ℝ*)
5554adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐵 ∈ ℝ*)
56 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ∈ (𝐴(,]𝐵))
57 iocgtlb 39724 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸𝑋))
5853, 55, 56, 57syl3anc 1326 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸𝑋))
5951, 58gtned 10172 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ≠ 𝐴)
6059neneqd 2799 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → ¬ (𝐸𝑋) = 𝐴)
6160ad3antrrr 766 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → ¬ (𝐸𝑋) = 𝐴)
6250, 61pm2.65da 600 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → ¬ 𝑗 = 0)
6362neqned 2801 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ≠ 0)
6437, 39, 63ne0gt0d 10174 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 < 𝑗)
65 0zd 11389 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ∈ ℤ)
66 zltp1le 11427 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
6765, 34, 66syl2anc 693 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
6864, 67mpbid 222 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 + 1) ≤ 𝑗)
6936, 68eqbrtrd 4675 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 1 ≤ 𝑗)
70 eluz2 11693 . . . . . . . . . . . . . . 15 (𝑗 ∈ (ℤ‘1) ↔ (1 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗))
7132, 34, 69, 70syl3anbrc 1246 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ (ℤ‘1))
72 nnuz 11723 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
7371, 72syl6eleqr 2712 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℕ)
74 nnm1nn0 11334 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ → (𝑗 − 1) ∈ ℕ0)
7573, 74syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ ℕ0)
76 nn0uz 11722 . . . . . . . . . . . . 13 0 = (ℤ‘0)
7776a1i 11 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → ℕ0 = (ℤ‘0))
7875, 77eleqtrd 2703 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (ℤ‘0))
7918nnzd 11481 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℤ)
8079ad3antrrr 766 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑀 ∈ ℤ)
81 peano2zm 11420 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℤ → (𝑗 − 1) ∈ ℤ)
8233, 81syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℤ)
8382zred 11482 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
8433zred 11482 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
85 elfzel2 12340 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
8685zred 11482 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
8784ltm1d 10956 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑗)
88 elfzle2 12345 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗𝑀)
8983, 84, 86, 87, 88ltletrd 10197 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
9089ad2antlr 763 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) < 𝑀)
91 elfzo2 12473 . . . . . . . . . . 11 ((𝑗 − 1) ∈ (0..^𝑀) ↔ ((𝑗 − 1) ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) < 𝑀))
9278, 80, 90, 91syl3anbrc 1246 . . . . . . . . . 10 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (0..^𝑀))
9325ad3antrrr 766 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑄:(0...𝑀)⟶ℝ)
9434, 81syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ ℤ)
9565, 80, 943jca 1242 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ))
9675nn0ge0d 11354 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ≤ (𝑗 − 1))
9783, 86, 89ltled 10185 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ≤ 𝑀)
9897ad2antlr 763 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ≤ 𝑀)
9995, 96, 98jca32 558 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ) ∧ (0 ≤ (𝑗 − 1) ∧ (𝑗 − 1) ≤ 𝑀)))
100 elfz2 12333 . . . . . . . . . . . . . . 15 ((𝑗 − 1) ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ) ∧ (0 ≤ (𝑗 − 1) ∧ (𝑗 − 1) ≤ 𝑀)))
10199, 100sylibr 224 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (0...𝑀))
10293, 101ffvelrnd 6360 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ)
103102rexrd 10089 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ*)
10425ffvelrnda 6359 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ)
105104rexrd 10089 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ*)
106105adantlr 751 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ*)
107106adantr 481 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ∈ ℝ*)
108 iocssre 12253 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
10952, 2, 108syl2anc 693 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
110109sselda 3603 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ∈ ℝ)
111110rexrd 10089 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ∈ ℝ*)
112111ad2antrr 762 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ*)
113 simplll 798 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝜑)
114 ovex 6678 . . . . . . . . . . . . . . . 16 (𝑗 − 1) ∈ V
115 eleq1 2689 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 − 1) → (𝑖 ∈ (0..^𝑀) ↔ (𝑗 − 1) ∈ (0..^𝑀)))
116115anbi2d 740 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 − 1) → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀))))
117 fveq2 6191 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 − 1) → (𝑄𝑖) = (𝑄‘(𝑗 − 1)))
118 oveq1 6657 . . . . . . . . . . . . . . . . . . 19 (𝑖 = (𝑗 − 1) → (𝑖 + 1) = ((𝑗 − 1) + 1))
119118fveq2d 6195 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 − 1) → (𝑄‘(𝑖 + 1)) = (𝑄‘((𝑗 − 1) + 1)))
120117, 119breq12d 4666 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 − 1) → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1))))
121116, 120imbi12d 334 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 − 1) → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))))
12222simprrd 797 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))
123122r19.21bi 2932 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
124114, 121, 123vtocl 3259 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
125113, 92, 124syl2anc 693 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
12633zcnd 11483 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
127 1cnd 10056 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 1 ∈ ℂ)
128126, 127npcand 10396 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → ((𝑗 − 1) + 1) = 𝑗)
129128eqcomd 2628 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → 𝑗 = ((𝑗 − 1) + 1))
130129fveq2d 6195 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → (𝑄𝑗) = (𝑄‘((𝑗 − 1) + 1)))
131130eqcomd 2628 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
132131ad2antlr 763 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
133125, 132breqtrd 4679 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄𝑗))
134 simpr 477 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) = (𝐸𝑋))
135133, 134breqtrd 4679 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝐸𝑋))
136109, 15sseldd 3604 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸𝑋) ∈ ℝ)
137136leidd 10594 . . . . . . . . . . . . . . 15 (𝜑 → (𝐸𝑋) ≤ (𝐸𝑋))
138137ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝐸𝑋))
13941adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) = (𝑄𝑗))
140138, 139breqtrd 4679 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄𝑗))
141140adantllr 755 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄𝑗))
142103, 107, 112, 135, 141eliocd 39730 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄𝑗)))
143130oveq2d 6666 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → ((𝑄‘(𝑗 − 1))(,](𝑄𝑗)) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
144143ad2antlr 763 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → ((𝑄‘(𝑗 − 1))(,](𝑄𝑗)) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
145142, 144eleqtrd 2703 . . . . . . . . . 10 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
146117, 119oveq12d 6668 . . . . . . . . . . . 12 (𝑖 = (𝑗 − 1) → ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
147146eleq2d 2687 . . . . . . . . . . 11 (𝑖 = (𝑗 − 1) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) ↔ (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))))
148147rspcev 3309 . . . . . . . . . 10 (((𝑗 − 1) ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
14992, 145, 148syl2anc 693 . . . . . . . . 9 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
150149ex 450 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
151150adantlr 751 . . . . . . 7 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
152151rexlimdva 3031 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
15331, 152mpd 15 . . . . 5 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
15418ad2antrr 762 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → 𝑀 ∈ ℕ)
15525ad2antrr 762 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ)
156 iocssicc 12261 . . . . . . . . . 10 (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵)
15746eqcomd 2628 . . . . . . . . . . 11 (𝜑𝐴 = (𝑄‘0))
15845simprd 479 . . . . . . . . . . . 12 (𝜑 → (𝑄𝑀) = 𝐵)
159158eqcomd 2628 . . . . . . . . . . 11 (𝜑𝐵 = (𝑄𝑀))
160157, 159oveq12d 6668 . . . . . . . . . 10 (𝜑 → (𝐴[,]𝐵) = ((𝑄‘0)[,](𝑄𝑀)))
161156, 160syl5sseq 3653 . . . . . . . . 9 (𝜑 → (𝐴(,]𝐵) ⊆ ((𝑄‘0)[,](𝑄𝑀)))
162161sselda 3603 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ∈ ((𝑄‘0)[,](𝑄𝑀)))
163162adantr 481 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (𝐸𝑋) ∈ ((𝑄‘0)[,](𝑄𝑀)))
164 simpr 477 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ¬ (𝐸𝑋) ∈ ran 𝑄)
165 fveq2 6191 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝑄𝑘) = (𝑄𝑗))
166165breq1d 4663 . . . . . . . . 9 (𝑘 = 𝑗 → ((𝑄𝑘) < (𝐸𝑋) ↔ (𝑄𝑗) < (𝐸𝑋)))
167166cbvrabv 3199 . . . . . . . 8 {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < (𝐸𝑋)} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < (𝐸𝑋)}
168167supeq1i 8353 . . . . . . 7 sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < (𝐸𝑋)}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < (𝐸𝑋)}, ℝ, < )
169154, 155, 163, 164, 168fourierdlem25 40349 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
170 ioossioc 39713 . . . . . . . . 9 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))
171170sseli 3599 . . . . . . . 8 ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
172171a1i 11 . . . . . . 7 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
173172reximdva 3017 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
174169, 173mpd 15 . . . . 5 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
175153, 174pm2.61dan 832 . . . 4 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
17615, 175mpdan 702 . . 3 (𝜑 → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
177 fourierdlem49.f . . . . . . . . . . 11 (𝜑𝐹:𝐷⟶ℝ)
178 frel 6050 . . . . . . . . . . 11 (𝐹:𝐷⟶ℝ → Rel 𝐹)
179177, 178syl 17 . . . . . . . . . 10 (𝜑 → Rel 𝐹)
180 resindm 5444 . . . . . . . . . . 11 (Rel 𝐹 → (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹)) = (𝐹 ↾ (-∞(,)(𝐸𝑋))))
181180eqcomd 2628 . . . . . . . . . 10 (Rel 𝐹 → (𝐹 ↾ (-∞(,)(𝐸𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹)))
182179, 181syl 17 . . . . . . . . 9 (𝜑 → (𝐹 ↾ (-∞(,)(𝐸𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹)))
183 fdm 6051 . . . . . . . . . . . 12 (𝐹:𝐷⟶ℝ → dom 𝐹 = 𝐷)
184177, 183syl 17 . . . . . . . . . . 11 (𝜑 → dom 𝐹 = 𝐷)
185184ineq2d 3814 . . . . . . . . . 10 (𝜑 → ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹) = ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
186185reseq2d 5396 . . . . . . . . 9 (𝜑 → (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹)) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)))
187182, 186eqtrd 2656 . . . . . . . 8 (𝜑 → (𝐹 ↾ (-∞(,)(𝐸𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)))
1881873ad2ant1 1082 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ (-∞(,)(𝐸𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)))
189188oveq1d 6665 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) lim (𝐸𝑋)))
190 ax-resscn 9993 . . . . . . . . . . 11 ℝ ⊆ ℂ
191190a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ⊆ ℂ)
192177, 191fssd 6057 . . . . . . . . 9 (𝜑𝐹:𝐷⟶ℂ)
1931923ad2ant1 1082 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐹:𝐷⟶ℂ)
194 inss2 3834 . . . . . . . . 9 ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ 𝐷
195194a1i 11 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ 𝐷)
196193, 195fssresd 6071 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)):((-∞(,)(𝐸𝑋)) ∩ 𝐷)⟶ℂ)
197 mnfxr 10096 . . . . . . . . . 10 -∞ ∈ ℝ*
198197a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ∈ ℝ*)
19925adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
200 elfzofz 12485 . . . . . . . . . . . . . 14 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
201200adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
202199, 201ffvelrnd 6360 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
203202rexrd 10089 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ*)
204202mnfltd 11958 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ < (𝑄𝑖))
205198, 203, 204xrltled 39486 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ≤ (𝑄𝑖))
206 iooss1 12210 . . . . . . . . . 10 ((-∞ ∈ ℝ* ∧ -∞ ≤ (𝑄𝑖)) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ (-∞(,)(𝐸𝑋)))
207197, 205, 206sylancr 695 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ (-∞(,)(𝐸𝑋)))
2082073adant3 1081 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ (-∞(,)(𝐸𝑋)))
209 fzofzp1 12565 . . . . . . . . . . . . . 14 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
210209adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
211199, 210ffvelrnd 6360 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
2122113adant3 1081 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
213212rexrd 10089 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
2142023adant3 1081 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
215214rexrd 10089 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ*)
216 simp3 1063 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
217 iocleub 39725 . . . . . . . . . . 11 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
218215, 213, 216, 217syl3anc 1326 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
219 iooss2 12211 . . . . . . . . . 10 (((𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
220213, 218, 219syl2anc 693 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
221 fourierdlem49.cn . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
222 cncff 22696 . . . . . . . . . . . . 13 ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
223 fdm 6051 . . . . . . . . . . . . 13 ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ → dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
224221, 222, 2233syl 18 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
225 ssdmres 5420 . . . . . . . . . . . 12 (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹 ↔ dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
226224, 225sylibr 224 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹)
227184adantr 481 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → dom 𝐹 = 𝐷)
228226, 227sseqtrd 3641 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
2292283adant3 1081 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
230220, 229sstrd 3613 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ 𝐷)
231208, 230ssind 3837 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
232 fourierdlem49.d . . . . . . . . . 10 (𝜑𝐷 ⊆ ℝ)
233232, 191sstrd 3613 . . . . . . . . 9 (𝜑𝐷 ⊆ ℂ)
2342333ad2ant1 1082 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐷 ⊆ ℂ)
235194, 234syl5ss 3614 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ ℂ)
236 eqid 2622 . . . . . . 7 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
237 eqid 2622 . . . . . . 7 ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) = ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
2381363ad2ant1 1082 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ℝ)
239238rexrd 10089 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ℝ*)
240 iocgtlb 39724 . . . . . . . . . 10 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝐸𝑋))
241215, 213, 216, 240syl3anc 1326 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝐸𝑋))
242238leidd 10594 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝐸𝑋))
243215, 239, 239, 241, 242eliocd 39730 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝐸𝑋)))
244 snunioo2 39731 . . . . . . . . . . 11 (((𝑄𝑖) ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ* ∧ (𝑄𝑖) < (𝐸𝑋)) → (((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)}) = ((𝑄𝑖)(,](𝐸𝑋)))
245215, 239, 241, 244syl3anc 1326 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)}) = ((𝑄𝑖)(,](𝐸𝑋)))
246245fveq2d 6195 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘(((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)})) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘((𝑄𝑖)(,](𝐸𝑋))))
247236cnfldtop 22587 . . . . . . . . . . 11 (TopOpen‘ℂfld) ∈ Top
248 ovex 6678 . . . . . . . . . . . . 13 (-∞(,)(𝐸𝑋)) ∈ V
249248inex1 4799 . . . . . . . . . . . 12 ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∈ V
250 snex 4908 . . . . . . . . . . . 12 {(𝐸𝑋)} ∈ V
251249, 250unex 6956 . . . . . . . . . . 11 (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∈ V
252 resttop 20964 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ∈ Top ∧ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∈ V) → ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ Top)
253247, 251, 252mp2an 708 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ Top
254 retop 22565 . . . . . . . . . . . . 13 (topGen‘ran (,)) ∈ Top
255254a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (topGen‘ran (,)) ∈ Top)
256251a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∈ V)
257 iooretop 22569 . . . . . . . . . . . . 13 ((𝑄𝑖)(,)+∞) ∈ (topGen‘ran (,))
258257a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)+∞) ∈ (topGen‘ran (,)))
259 elrestr 16089 . . . . . . . . . . . 12 (((topGen‘ran (,)) ∈ Top ∧ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∈ V ∧ ((𝑄𝑖)(,)+∞) ∈ (topGen‘ran (,))) → (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
260255, 256, 258, 259syl3anc 1326 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
261 simpr 477 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 = (𝐸𝑋)) → 𝑥 = (𝐸𝑋))
262 pnfxr 10092 . . . . . . . . . . . . . . . . . . . 20 +∞ ∈ ℝ*
263262a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → +∞ ∈ ℝ*)
264238ltpnfd 11955 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) < +∞)
265215, 263, 238, 241, 264eliood 39720 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,)+∞))
266 snidg 4206 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸𝑋) ∈ ℝ → (𝐸𝑋) ∈ {(𝐸𝑋)})
267 elun2 3781 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸𝑋) ∈ {(𝐸𝑋)} → (𝐸𝑋) ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
268266, 267syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝐸𝑋) ∈ ℝ → (𝐸𝑋) ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
269136, 268syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐸𝑋) ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
2702693ad2ant1 1082 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
271265, 270elind 3798 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
272271adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
273261, 272eqeltrd 2701 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
274273adantlr 751 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
275215adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝑄𝑖) ∈ ℝ*)
276262a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → +∞ ∈ ℝ*)
277203adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝑄𝑖) ∈ ℝ*)
278136adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐸𝑋) ∈ ℝ)
279278adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝐸𝑋) ∈ ℝ)
280 iocssre 12253 . . . . . . . . . . . . . . . . . . . 20 (((𝑄𝑖) ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ) → ((𝑄𝑖)(,](𝐸𝑋)) ⊆ ℝ)
281277, 279, 280syl2anc 693 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → ((𝑄𝑖)(,](𝐸𝑋)) ⊆ ℝ)
282 simpr 477 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋)))
283281, 282sseldd 3604 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ ℝ)
2842833adantl3 1219 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ ℝ)
285279rexrd 10089 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝐸𝑋) ∈ ℝ*)
286 iocgtlb 39724 . . . . . . . . . . . . . . . . . . 19 (((𝑄𝑖) ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ*𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝑄𝑖) < 𝑥)
287277, 285, 282, 286syl3anc 1326 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝑄𝑖) < 𝑥)
2882873adantl3 1219 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝑄𝑖) < 𝑥)
289284ltpnfd 11955 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 < +∞)
290275, 276, 284, 288, 289eliood 39720 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ ((𝑄𝑖)(,)+∞))
291290adantr 481 . . . . . . . . . . . . . . 15 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ((𝑄𝑖)(,)+∞))
292197a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → -∞ ∈ ℝ*)
293285adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ*)
294283adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ℝ)
295294mnfltd 11958 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → -∞ < 𝑥)
296136ad3antrrr 766 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ)
297 iocleub 39725 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑄𝑖) ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ*𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ≤ (𝐸𝑋))
298277, 285, 282, 297syl3anc 1326 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ≤ (𝐸𝑋))
299298adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ≤ (𝐸𝑋))
300 neqne 2802 . . . . . . . . . . . . . . . . . . . . . 22 𝑥 = (𝐸𝑋) → 𝑥 ≠ (𝐸𝑋))
301300necomd 2849 . . . . . . . . . . . . . . . . . . . . 21 𝑥 = (𝐸𝑋) → (𝐸𝑋) ≠ 𝑥)
302301adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ≠ 𝑥)
303294, 296, 299, 302leneltd 10191 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 < (𝐸𝑋))
304292, 293, 294, 295, 303eliood 39720 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (-∞(,)(𝐸𝑋)))
3053043adantll3 39203 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (-∞(,)(𝐸𝑋)))
306229ad2antrr 762 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
307275adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝑄𝑖) ∈ ℝ*)
308213ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
309284adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ℝ)
310288adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝑄𝑖) < 𝑥)
311238ad2antrr 762 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ)
312212ad2antrr 762 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
3133033adantll3 39203 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 < (𝐸𝑋))
314218ad2antrr 762 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
315309, 311, 312, 313, 314ltletrd 10197 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 < (𝑄‘(𝑖 + 1)))
316307, 308, 309, 310, 315eliood 39720 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
317306, 316sseldd 3604 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥𝐷)
318305, 317elind 3798 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
319 elun1 3780 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷) → 𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
320318, 319syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
321291, 320elind 3798 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
322274, 321pm2.61dan 832 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
323215adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝑄𝑖) ∈ ℝ*)
324239adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝐸𝑋) ∈ ℝ*)
325 elinel1 3799 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ∈ ((𝑄𝑖)(,)+∞))
326 elioore 12205 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((𝑄𝑖)(,)+∞) → 𝑥 ∈ ℝ)
327326rexrd 10089 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((𝑄𝑖)(,)+∞) → 𝑥 ∈ ℝ*)
328325, 327syl 17 . . . . . . . . . . . . . . 15 (𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ∈ ℝ*)
329328adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ∈ ℝ*)
330203adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝑄𝑖) ∈ ℝ*)
331262a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → +∞ ∈ ℝ*)
332325adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ∈ ((𝑄𝑖)(,)+∞))
333 ioogtlb 39717 . . . . . . . . . . . . . . . 16 (((𝑄𝑖) ∈ ℝ* ∧ +∞ ∈ ℝ*𝑥 ∈ ((𝑄𝑖)(,)+∞)) → (𝑄𝑖) < 𝑥)
334330, 331, 332, 333syl3anc 1326 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝑄𝑖) < 𝑥)
3353343adantl3 1219 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝑄𝑖) < 𝑥)
336 elinel2 3800 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
337 elsni 4194 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {(𝐸𝑋)} → 𝑥 = (𝐸𝑋))
338337adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ {(𝐸𝑋)}) → 𝑥 = (𝐸𝑋))
339137adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ {(𝐸𝑋)}) → (𝐸𝑋) ≤ (𝐸𝑋))
340338, 339eqbrtrd 4675 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ≤ (𝐸𝑋))
341340adantlr 751 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∧ 𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ≤ (𝐸𝑋))
342 simpll 790 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∧ ¬ 𝑥 ∈ {(𝐸𝑋)}) → 𝜑)
343 elunnel2 39198 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∧ ¬ 𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
344343adantll 750 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∧ ¬ 𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
345 elinel1 3799 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷) → 𝑥 ∈ (-∞(,)(𝐸𝑋)))
346 elioore 12205 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (-∞(,)(𝐸𝑋)) → 𝑥 ∈ ℝ)
347346adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 ∈ ℝ)
348136adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → (𝐸𝑋) ∈ ℝ)
349197a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → -∞ ∈ ℝ*)
350348rexrd 10089 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → (𝐸𝑋) ∈ ℝ*)
351 simpr 477 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 ∈ (-∞(,)(𝐸𝑋)))
352 iooltub 39735 . . . . . . . . . . . . . . . . . . . . . 22 ((-∞ ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ*𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 < (𝐸𝑋))
353349, 350, 351, 352syl3anc 1326 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 < (𝐸𝑋))
354347, 348, 353ltled 10185 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 ≤ (𝐸𝑋))
355345, 354sylan2 491 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) → 𝑥 ≤ (𝐸𝑋))
356342, 344, 355syl2anc 693 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∧ ¬ 𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ≤ (𝐸𝑋))
357341, 356pm2.61dan 832 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ≤ (𝐸𝑋))
358357adantlr 751 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ≤ (𝐸𝑋))
359336, 358sylan2 491 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ≤ (𝐸𝑋))
3603593adantl3 1219 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ≤ (𝐸𝑋))
361323, 324, 329, 335, 360eliocd 39730 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋)))
362322, 361impbida 877 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋)) ↔ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))))
363362eqrdv 2620 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,](𝐸𝑋)) = (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
364 ioossre 12235 . . . . . . . . . . . . . 14 (-∞(,)(𝐸𝑋)) ⊆ ℝ
365 ssinss1 3841 . . . . . . . . . . . . . 14 ((-∞(,)(𝐸𝑋)) ⊆ ℝ → ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ ℝ)
366364, 365mp1i 13 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ ℝ)
367238snssd 4340 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {(𝐸𝑋)} ⊆ ℝ)
368366, 367unssd 3789 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ⊆ ℝ)
369 eqid 2622 . . . . . . . . . . . . 13 (topGen‘ran (,)) = (topGen‘ran (,))
370236, 369tgiooss 39733 . . . . . . . . . . . 12 ((((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) = ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
371368, 370syl 17 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) = ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
372260, 363, 3713eltr4d 2716 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,](𝐸𝑋)) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
373 isopn3i 20886 . . . . . . . . . 10 ((((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ Top ∧ ((𝑄𝑖)(,](𝐸𝑋)) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘((𝑄𝑖)(,](𝐸𝑋))) = ((𝑄𝑖)(,](𝐸𝑋)))
374253, 372, 373sylancr 695 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘((𝑄𝑖)(,](𝐸𝑋))) = ((𝑄𝑖)(,](𝐸𝑋)))
375246, 374eqtr2d 2657 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,](𝐸𝑋)) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘(((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)})))
376243, 375eleqtrd 2703 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘(((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)})))
377196, 231, 235, 236, 237, 376limcres 23650 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) lim (𝐸𝑋)))
378231resabs1d 5428 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) = (𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))))
379378oveq1d 6665 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
380189, 377, 3793eqtr2d 2662 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
381184feq2d 6031 . . . . . . . . . . . 12 (𝜑 → (𝐹:dom 𝐹⟶ℂ ↔ 𝐹:𝐷⟶ℂ))
382192, 381mpbird 247 . . . . . . . . . . 11 (𝜑𝐹:dom 𝐹⟶ℂ)
383382adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝐹:dom 𝐹⟶ℂ)
3843833ad2antl1 1223 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝐹:dom 𝐹⟶ℂ)
385 ioosscn 39716 . . . . . . . . . 10 ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ℂ
386385a1i 11 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ℂ)
387184eqcomd 2628 . . . . . . . . . . . 12 (𝜑𝐷 = dom 𝐹)
3883873ad2ant1 1082 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐷 = dom 𝐹)
389230, 388sseqtrd 3641 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ dom 𝐹)
390389adantr 481 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ dom 𝐹)
3917a1i 11 . . . . . . . . . . . . . . 15 (𝜑𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
392 oveq2 6658 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋 → (𝐵𝑥) = (𝐵𝑋))
393392oveq1d 6665 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋 → ((𝐵𝑥) / 𝑇) = ((𝐵𝑋) / 𝑇))
394393fveq2d 6195 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋 → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵𝑋) / 𝑇)))
395394oveq1d 6665 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
396395adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑥 = 𝑋) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
3972, 14resubcld 10458 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵𝑋) ∈ ℝ)
3982, 1resubcld 10458 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐵𝐴) ∈ ℝ)
3994, 398syl5eqel 2705 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑇 ∈ ℝ)
4001, 2posdifd 10614 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
4013, 400mpbid 222 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 < (𝐵𝐴))
4024eqcomi 2631 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵𝐴) = 𝑇
403402a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵𝐴) = 𝑇)
404401, 403breqtrd 4679 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 < 𝑇)
405404gt0ne0d 10592 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑇 ≠ 0)
406397, 399, 405redivcld 10853 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵𝑋) / 𝑇) ∈ ℝ)
407406flcld 12599 . . . . . . . . . . . . . . . . 17 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
408407zred 11482 . . . . . . . . . . . . . . . 16 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℝ)
409408, 399remulcld 10070 . . . . . . . . . . . . . . 15 (𝜑 → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
410391, 396, 14, 409fvmptd 6288 . . . . . . . . . . . . . 14 (𝜑 → (𝑍𝑋) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
411410, 409eqeltrd 2701 . . . . . . . . . . . . 13 (𝜑 → (𝑍𝑋) ∈ ℝ)
412411recnd 10068 . . . . . . . . . . . 12 (𝜑 → (𝑍𝑋) ∈ ℂ)
413412adantr 481 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → (𝑍𝑋) ∈ ℂ)
4144133ad2antl1 1223 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → (𝑍𝑋) ∈ ℂ)
415414negcld 10379 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → -(𝑍𝑋) ∈ ℂ)
416 eqid 2622 . . . . . . . . 9 {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}
417 ioosscn 39716 . . . . . . . . . . . . . . . . . . 19 (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ ℂ
418417sseli 3599 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) → 𝑦 ∈ ℂ)
419418adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℂ)
420412adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℂ)
421419, 420pncand 10393 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = 𝑦)
422421eqcomd 2628 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)))
4234223ad2antl1 1223 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)))
424410oveq2d 6666 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = ((𝑦 + (𝑍𝑋)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
425424adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = ((𝑦 + (𝑍𝑋)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
426419, 420addcld 10059 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℂ)
427409recnd 10068 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
428427adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
429426, 428negsubd 10398 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + (𝑍𝑋)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
430407zcnd 11483 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℂ)
431399recnd 10068 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑇 ∈ ℂ)
432430, 431mulneg1d 10483 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
433432eqcomd 2628 . . . . . . . . . . . . . . . . . . 19 (𝜑 → -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
434433oveq2d 6666 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑦 + (𝑍𝑋)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
435434adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
436425, 429, 4353eqtr2d 2662 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
4374363ad2antl1 1223 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
438407znegcld 11484 . . . . . . . . . . . . . . . . . 18 (𝜑 → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
439438adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
4404393ad2antl1 1223 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
441 simpl1 1064 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝜑)
442230adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ 𝐷)
443203adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) ∈ ℝ*)
444136rexrd 10089 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐸𝑋) ∈ ℝ*)
445444ad2antrr 762 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐸𝑋) ∈ ℝ*)
446 elioore 12205 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) → 𝑦 ∈ ℝ)
447446adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
448411adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℝ)
449447, 448readdcld 10069 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
450449adantlr 751 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
451411adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑍𝑋) ∈ ℝ)
452202, 451resubcld 10458 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ)
453452rexrd 10089 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
454453adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
45514rexrd 10089 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑋 ∈ ℝ*)
456455ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑋 ∈ ℝ*)
457 simpr 477 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
458 ioogtlb 39717 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑦)
459454, 456, 457, 458syl3anc 1326 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑦)
460202adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) ∈ ℝ)
461451adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℝ)
462446adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
463460, 461, 462ltsubaddd 10623 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (((𝑄𝑖) − (𝑍𝑋)) < 𝑦 ↔ (𝑄𝑖) < (𝑦 + (𝑍𝑋))))
464459, 463mpbid 222 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) < (𝑦 + (𝑍𝑋)))
46514ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑋 ∈ ℝ)
466 iooltub 39735 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 < 𝑋)
467454, 456, 457, 466syl3anc 1326 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 < 𝑋)
468462, 465, 461, 467ltadd1dd 10638 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝑋 + (𝑍𝑋)))
4695a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥))))
470 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑋𝑥 = 𝑋)
471 fveq2 6191 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑋 → (𝑍𝑥) = (𝑍𝑋))
472470, 471oveq12d 6668 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑋 → (𝑥 + (𝑍𝑥)) = (𝑋 + (𝑍𝑋)))
473472adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 = 𝑋) → (𝑥 + (𝑍𝑥)) = (𝑋 + (𝑍𝑋)))
47414, 411readdcld 10069 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑋 + (𝑍𝑋)) ∈ ℝ)
475469, 473, 14, 474fvmptd 6288 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
476475eqcomd 2628 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
477476ad2antrr 762 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
478468, 477breqtrd 4679 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝐸𝑋))
479443, 445, 450, 464, 478eliood 39720 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ((𝑄𝑖)(,)(𝐸𝑋)))
4804793adantl3 1219 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ((𝑄𝑖)(,)(𝐸𝑋)))
481442, 480sseldd 3604 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ 𝐷)
482441, 481, 4403jca 1242 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
483 eleq1 2689 . . . . . . . . . . . . . . . . . . 19 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
4844833anbi3d 1405 . . . . . . . . . . . . . . . . . 18 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)))
485 oveq1 6657 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 · 𝑇) = (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
486485oveq2d 6666 . . . . . . . . . . . . . . . . . . 19 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
487486eleq1d 2686 . . . . . . . . . . . . . . . . . 18 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
488484, 487imbi12d 334 . . . . . . . . . . . . . . . . 17 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)))
489 ovex 6678 . . . . . . . . . . . . . . . . . 18 (𝑦 + (𝑍𝑋)) ∈ V
490 eleq1 2689 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑦 + (𝑍𝑋)) → (𝑥𝐷 ↔ (𝑦 + (𝑍𝑋)) ∈ 𝐷))
4914903anbi2d 1404 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑦 + (𝑍𝑋)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ)))
492 oveq1 6657 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑦 + (𝑍𝑋)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)))
493492eleq1d 2686 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑦 + (𝑍𝑋)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷))
494491, 493imbi12d 334 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑦 + (𝑍𝑋)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)))
495 fourierdlem49.dper . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)
496489, 494, 495vtocl 3259 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)
497488, 496vtoclg 3266 . . . . . . . . . . . . . . . 16 (-(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ → ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
498440, 482, 497sylc 65 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
499437, 498eqeltrd 2701 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) ∈ 𝐷)
500423, 499eqeltrd 2701 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦𝐷)
501500ralrimiva 2966 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑦𝐷)
502 dfss3 3592 . . . . . . . . . . . 12 ((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷 ↔ ∀𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑦𝐷)
503501, 502sylibr 224 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷)
504202recnd 10068 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℂ)
505412adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑍𝑋) ∈ ℂ)
506504, 505negsubd 10398 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + -(𝑍𝑋)) = ((𝑄𝑖) − (𝑍𝑋)))
507506eqcomd 2628 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) = ((𝑄𝑖) + -(𝑍𝑋)))
508475oveq1d 6665 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸𝑋) + -(𝑍𝑋)) = ((𝑋 + (𝑍𝑋)) + -(𝑍𝑋)))
509474recnd 10068 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑋 + (𝑍𝑋)) ∈ ℂ)
510509, 412negsubd 10398 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑋 + (𝑍𝑋)) + -(𝑍𝑋)) = ((𝑋 + (𝑍𝑋)) − (𝑍𝑋)))
51114recnd 10068 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 ∈ ℂ)
512511, 412pncand 10393 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑋 + (𝑍𝑋)) − (𝑍𝑋)) = 𝑋)
513508, 510, 5123eqtrrd 2661 . . . . . . . . . . . . . . 15 (𝜑𝑋 = ((𝐸𝑋) + -(𝑍𝑋)))
514513adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 = ((𝐸𝑋) + -(𝑍𝑋)))
515507, 514oveq12d 6668 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) = (((𝑄𝑖) + -(𝑍𝑋))(,)((𝐸𝑋) + -(𝑍𝑋))))
516451renegcld 10457 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → -(𝑍𝑋) ∈ ℝ)
517202, 278, 516iooshift 39748 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) + -(𝑍𝑋))(,)((𝐸𝑋) + -(𝑍𝑋))) = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))})
518515, 517eqtr2d 2657 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} = (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
5195183adant3 1081 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} = (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
5201843ad2ant1 1082 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → dom 𝐹 = 𝐷)
521503, 519, 5203sstr4d 3648 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} ⊆ dom 𝐹)
522521adantr 481 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} ⊆ dom 𝐹)
523410negeqd 10275 . . . . . . . . . . . . . . . 16 (𝜑 → -(𝑍𝑋) = -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
524523, 433eqtrd 2656 . . . . . . . . . . . . . . 15 (𝜑 → -(𝑍𝑋) = (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
525524oveq2d 6666 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 + -(𝑍𝑋)) = (𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
526525fveq2d 6195 . . . . . . . . . . . . 13 (𝜑 → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
527526adantr 481 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
5285273ad2antl1 1223 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
529438adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
5305293ad2antl1 1223 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
531 simpl1 1064 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → 𝜑)
532230sselda 3603 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → 𝑥𝐷)
533531, 532, 5303jca 1242 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝜑𝑥𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
5344833anbi3d 1405 . . . . . . . . . . . . . 14 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑𝑥𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)))
535485oveq2d 6666 . . . . . . . . . . . . . . . 16 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = (𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
536535fveq2d 6195 . . . . . . . . . . . . . . 15 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
537536eqeq1d 2624 . . . . . . . . . . . . . 14 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥) ↔ (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
538534, 537imbi12d 334 . . . . . . . . . . . . 13 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥)) ↔ ((𝜑𝑥𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥))))
539 fourierdlem49.per . . . . . . . . . . . . 13 ((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥))
540538, 539vtoclg 3266 . . . . . . . . . . . 12 (-(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ → ((𝜑𝑥𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
541530, 533, 540sylc 65 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥))
542528, 541eqtrd 2656 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹𝑥))
543542adantlr 751 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹𝑥))
544 simpr 477 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
545384, 386, 390, 415, 416, 522, 543, 544limcperiod 39860 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝑦 ∈ ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) lim ((𝐸𝑋) + -(𝑍𝑋))))
546518reseq2d 5396 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) = (𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)))
547514eqcomd 2628 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) + -(𝑍𝑋)) = 𝑋)
548546, 547oveq12d 6668 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) lim ((𝐸𝑋) + -(𝑍𝑋))) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
5495483adant3 1081 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) lim ((𝐸𝑋) + -(𝑍𝑋))) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
550549adantr 481 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) lim ((𝐸𝑋) + -(𝑍𝑋))) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
551545, 550eleqtrd 2703 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
552382adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → 𝐹:dom 𝐹⟶ℂ)
5535523ad2antl1 1223 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → 𝐹:dom 𝐹⟶ℂ)
554417a1i 11 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ ℂ)
555503, 520sseqtr4d 3642 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ dom 𝐹)
556555adantr 481 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ dom 𝐹)
557412adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → (𝑍𝑋) ∈ ℂ)
5585573ad2antl1 1223 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → (𝑍𝑋) ∈ ℂ)
559 eqid 2622 . . . . . . . . 9 {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}
560504, 505npcand 10396 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) − (𝑍𝑋)) + (𝑍𝑋)) = (𝑄𝑖))
561560eqcomd 2628 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) = (((𝑄𝑖) − (𝑍𝑋)) + (𝑍𝑋)))
562475adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
563561, 562oveq12d 6668 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝐸𝑋)) = ((((𝑄𝑖) − (𝑍𝑋)) + (𝑍𝑋))(,)(𝑋 + (𝑍𝑋))))
56414adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
565452, 564, 451iooshift 39748 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((((𝑄𝑖) − (𝑍𝑋)) + (𝑍𝑋))(,)(𝑋 + (𝑍𝑋))) = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))})
566563, 565eqtr2d 2657 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} = ((𝑄𝑖)(,)(𝐸𝑋)))
5675663adant3 1081 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} = ((𝑄𝑖)(,)(𝐸𝑋)))
568230, 567, 5203sstr4d 3648 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} ⊆ dom 𝐹)
569568adantr 481 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} ⊆ dom 𝐹)
570410oveq2d 6666 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 + (𝑍𝑋)) = (𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
571570fveq2d 6195 . . . . . . . . . . . . 13 (𝜑 → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
572571adantr 481 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
5735723ad2antl1 1223 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
574407adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
5755743ad2antl1 1223 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
576 simpl1 1064 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝜑)
577503sselda 3603 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑥𝐷)
578576, 577, 5753jca 1242 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝜑𝑥𝐷 ∧ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
579 eleq1 2689 . . . . . . . . . . . . . . 15 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
5805793anbi3d 1405 . . . . . . . . . . . . . 14 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑𝑥𝐷 ∧ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)))
581 oveq1 6657 . . . . . . . . . . . . . . . . 17 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
582581oveq2d 6666 . . . . . . . . . . . . . . . 16 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = (𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
583582fveq2d 6195 . . . . . . . . . . . . . . 15 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
584583eqeq1d 2624 . . . . . . . . . . . . . 14 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → ((𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥) ↔ (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
585580, 584imbi12d 334 . . . . . . . . . . . . 13 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥)) ↔ ((𝜑𝑥𝐷 ∧ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥))))
586585, 539vtoclg 3266 . . . . . . . . . . . 12 ((⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ → ((𝜑𝑥𝐷 ∧ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
587575, 578, 586sylc 65 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥))
588573, 587eqtrd 2656 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹𝑥))
589588adantlr 751 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹𝑥))
590 simpr 477 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
591553, 554, 556, 558, 559, 569, 589, 590limcperiod 39860 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → 𝑦 ∈ ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) lim (𝑋 + (𝑍𝑋))))
592566reseq2d 5396 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) = (𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))))
593476adantr 481 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
594592, 593oveq12d 6668 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) lim (𝑋 + (𝑍𝑋))) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
5955943adant3 1081 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) lim (𝑋 + (𝑍𝑋))) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
596595adantr 481 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) lim (𝑋 + (𝑍𝑋))) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
597591, 596eleqtrd 2703 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
598551, 597impbida 877 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) ↔ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)))
599598eqrdv 2620 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
600 resindm 5444 . . . . . . . . . . 11 (Rel 𝐹 → (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)) = (𝐹 ↾ (-∞(,)𝑋)))
601600eqcomd 2628 . . . . . . . . . 10 (Rel 𝐹 → (𝐹 ↾ (-∞(,)𝑋)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)))
602179, 601syl 17 . . . . . . . . 9 (𝜑 → (𝐹 ↾ (-∞(,)𝑋)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)))
603184ineq2d 3814 . . . . . . . . . 10 (𝜑 → ((-∞(,)𝑋) ∩ dom 𝐹) = ((-∞(,)𝑋) ∩ 𝐷))
604603reseq2d 5396 . . . . . . . . 9 (𝜑 → (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)))
605602, 604eqtrd 2656 . . . . . . . 8 (𝜑 → (𝐹 ↾ (-∞(,)𝑋)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)))
606605oveq1d 6665 . . . . . . 7 (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) lim 𝑋))
6076063ad2ant1 1082 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) lim 𝑋))
608 inss2 3834 . . . . . . . . . 10 ((-∞(,)𝑋) ∩ 𝐷) ⊆ 𝐷
609608a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)𝑋) ∩ 𝐷) ⊆ 𝐷)
610193, 609fssresd 6071 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)):((-∞(,)𝑋) ∩ 𝐷)⟶ℂ)
611452mnfltd 11958 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ < ((𝑄𝑖) − (𝑍𝑋)))
612198, 453, 611xrltled 39486 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ≤ ((𝑄𝑖) − (𝑍𝑋)))
613 iooss1 12210 . . . . . . . . . . 11 ((-∞ ∈ ℝ* ∧ -∞ ≤ ((𝑄𝑖) − (𝑍𝑋))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ (-∞(,)𝑋))
614197, 612, 613sylancr 695 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ (-∞(,)𝑋))
6156143adant3 1081 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ (-∞(,)𝑋))
616615, 503ssind 3837 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ ((-∞(,)𝑋) ∩ 𝐷))
617608, 234syl5ss 3614 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)𝑋) ∩ 𝐷) ⊆ ℂ)
618 eqid 2622 . . . . . . . 8 ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) = ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
6194533adant3 1081 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
6204553ad2ant1 1082 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ*)
6214753ad2ant1 1082 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
622241, 621breqtrd 4679 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝑋 + (𝑍𝑋)))
6234113ad2ant1 1082 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑍𝑋) ∈ ℝ)
624143ad2ant1 1082 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
625214, 623, 624ltsubaddd 10623 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋)) < 𝑋 ↔ (𝑄𝑖) < (𝑋 + (𝑍𝑋))))
626622, 625mpbird 247 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑋)
62714leidd 10594 . . . . . . . . . . 11 (𝜑𝑋𝑋)
6286273ad2ant1 1082 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋𝑋)
629619, 620, 620, 626, 628eliocd 39730 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
630 snunioo2 39731 . . . . . . . . . . . 12 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ* ∧ ((𝑄𝑖) − (𝑍𝑋)) < 𝑋) → ((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋}) = (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
631619, 620, 626, 630syl3anc 1326 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋}) = (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
632631fveq2d 6195 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋})) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘(((𝑄𝑖) − (𝑍𝑋))(,]𝑋)))
633 ovex 6678 . . . . . . . . . . . . . 14 (-∞(,)𝑋) ∈ V
634633inex1 4799 . . . . . . . . . . . . 13 ((-∞(,)𝑋) ∩ 𝐷) ∈ V
635 snex 4908 . . . . . . . . . . . . 13 {𝑋} ∈ V
636634, 635unex 6956 . . . . . . . . . . . 12 (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V
637 resttop 20964 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ∈ Top ∧ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V) → ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ Top)
638247, 636, 637mp2an 708 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ Top
639636a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V)
640 iooretop 22569 . . . . . . . . . . . . . 14 (((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∈ (topGen‘ran (,))
641640a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∈ (topGen‘ran (,)))
642 elrestr 16089 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ∈ Top ∧ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V ∧ (((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∈ (topGen‘ran (,))) → ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
643255, 639, 641, 642syl3anc 1326 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
644453adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
645262a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → +∞ ∈ ℝ*)
64614ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑋 ∈ ℝ)
647 iocssre 12253 . . . . . . . . . . . . . . . . . . 19 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ⊆ ℝ)
648644, 646, 647syl2anc 693 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ⊆ ℝ)
649 simpr 477 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
650648, 649sseldd 3604 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ ℝ)
651455ad2antrr 762 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑋 ∈ ℝ*)
652 iocgtlb 39724 . . . . . . . . . . . . . . . . . 18 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
653644, 651, 649, 652syl3anc 1326 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
654650ltpnfd 11955 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 < +∞)
655644, 645, 650, 653, 654eliood 39720 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞))
6566553adantl3 1219 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞))
657 eqvisset 3211 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑋𝑋 ∈ V)
658 snidg 4206 . . . . . . . . . . . . . . . . . . . 20 (𝑋 ∈ V → 𝑋 ∈ {𝑋})
659657, 658syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋𝑋 ∈ {𝑋})
660470, 659eqeltrd 2701 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋𝑥 ∈ {𝑋})
661 elun2 3781 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ {𝑋} → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
662660, 661syl 17 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
663662adantl 482 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ 𝑥 = 𝑋) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
664 simpll 790 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → (𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
665644adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
666455ad3antrrr 766 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑋 ∈ ℝ*)
667650adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ ℝ)
668653adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
66914ad3antrrr 766 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑋 ∈ ℝ)
670 iocleub 39725 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥𝑋)
671644, 651, 649, 670syl3anc 1326 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥𝑋)
672671adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥𝑋)
673470eqcoms 2630 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 = 𝑥𝑥 = 𝑋)
674673necon3bi 2820 . . . . . . . . . . . . . . . . . . . . 21 𝑥 = 𝑋𝑋𝑥)
675674adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑋𝑥)
676667, 669, 672, 675leneltd 10191 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 < 𝑋)
677665, 666, 667, 668, 676eliood 39720 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
6786773adantll3 39203 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
679616sselda 3603 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷))
680 elun1 3780 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
681679, 680syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
682664, 678, 681syl2anc 693 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
683663, 682pm2.61dan 832 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
684656, 683elind 3798 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
685619adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
686620adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑋 ∈ ℝ*)
687 elinel1 3799 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞))
688 elioore 12205 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞) → 𝑥 ∈ ℝ)
689687, 688syl 17 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ ℝ)
690689rexrd 10089 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ ℝ*)
691690adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ∈ ℝ*)
692453adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
693262a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → +∞ ∈ ℝ*)
694687adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞))
695 ioogtlb 39717 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ* ∧ +∞ ∈ ℝ*𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
696692, 693, 694, 695syl3anc 1326 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
6976963adantl3 1219 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
698 elinel2 3800 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
699 elsni 4194 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {𝑋} → 𝑥 = 𝑋)
700699adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ {𝑋}) → 𝑥 = 𝑋)
701627adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ {𝑋}) → 𝑋𝑋)
702700, 701eqbrtrd 4675 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ {𝑋}) → 𝑥𝑋)
703702adantlr 751 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ 𝑥 ∈ {𝑋}) → 𝑥𝑋)
704 simpll 790 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝜑)
705 elunnel2 39198 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷))
706705adantll 750 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷))
707 elinel1 3799 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷) → 𝑥 ∈ (-∞(,)𝑋))
708706, 707syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ∈ (-∞(,)𝑋))
709 elioore 12205 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (-∞(,)𝑋) → 𝑥 ∈ ℝ)
710709adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑥 ∈ ℝ)
71114adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑋 ∈ ℝ)
712197a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → -∞ ∈ ℝ*)
713455adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑋 ∈ ℝ*)
714 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑥 ∈ (-∞(,)𝑋))
715 iooltub 39735 . . . . . . . . . . . . . . . . . . . . 21 ((-∞ ∈ ℝ*𝑋 ∈ ℝ*𝑥 ∈ (-∞(,)𝑋)) → 𝑥 < 𝑋)
716712, 713, 714, 715syl3anc 1326 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑥 < 𝑋)
717710, 711, 716ltled 10185 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑥𝑋)
718704, 708, 717syl2anc 693 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥𝑋)
719703, 718pm2.61dan 832 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥𝑋)
720698, 719sylan2 491 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥𝑋)
7217203ad2antl1 1223 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥𝑋)
722685, 686, 691, 697, 721eliocd 39730 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
723684, 722impbida 877 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ↔ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))))
724723eqrdv 2620 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) = ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
725608, 232syl5ss 3614 . . . . . . . . . . . . . . 15 (𝜑 → ((-∞(,)𝑋) ∩ 𝐷) ⊆ ℝ)
72614snssd 4340 . . . . . . . . . . . . . . 15 (𝜑 → {𝑋} ⊆ ℝ)
727725, 726unssd 3789 . . . . . . . . . . . . . 14 (𝜑 → (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ⊆ ℝ)
7287273ad2ant1 1082 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ⊆ ℝ)
729236, 369tgiooss 39733 . . . . . . . . . . . . 13 ((((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) = ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
730728, 729syl 17 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) = ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
731643, 724, 7303eltr4d 2716 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
732 isopn3i 20886 . . . . . . . . . . 11 ((((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ Top ∧ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘(((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) = (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
733638, 731, 732sylancr 695 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘(((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) = (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
734632, 733eqtr2d 2657 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋})))
735629, 734eleqtrd 2703 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋})))
736610, 616, 617, 236, 618, 735limcres 23650 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋) = ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) lim 𝑋))
737736eqcomd 2628 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) lim 𝑋) = (((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
738616resabs1d 5428 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) = (𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)))
739738oveq1d 6665 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
740607, 737, 7393eqtrrd 2661 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋))
741380, 599, 7403eqtrrd 2661 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)))
742741rexlimdv3a 3033 . . 3 (𝜑 → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋))))
743176, 742mpd 15 . 2 (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)))
7441233adant3 1081 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
7452213adant3 1081 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
746 fourierdlem49.l . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
7477463adant3 1081 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
748 eqid 2622 . . . . . . . 8 if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋))) = if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋)))
749 eqid 2622 . . . . . . . 8 ((TopOpen‘ℂfld) ↾t (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))})) = ((TopOpen‘ℂfld) ↾t (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))}))
750214, 212, 744, 745, 747, 214, 238, 241, 220, 748, 749fourierdlem33 40357 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋))) ∈ (((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
751220resabs1d 5428 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) = (𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))))
752751oveq1d 6665 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
753750, 752eleqtrd 2703 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋))) ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
754 ne0i 3921 . . . . . 6 (if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋))) ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅)
755753, 754syl 17 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅)
756380, 755eqnetrd 2861 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅)
757756rexlimdv3a 3033 . . 3 (𝜑 → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅))
758176, 757mpd 15 . 2 (𝜑 → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅)
759743, 758eqnetrd 2861 1 (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1037   = wceq 1483  wcel 1990  wne 2794  wral 2912  wrex 2913  {crab 2916  Vcvv 3200  cun 3572  cin 3573  wss 3574  c0 3915  ifcif 4086  {csn 4177   class class class wbr 4653  cmpt 4729  dom cdm 5114  ran crn 5115  cres 5116  Rel wrel 5119   Fn wfn 5883  wf 5884  cfv 5888  (class class class)co 6650  𝑚 cmap 7857  supcsup 8346  cc 9934  cr 9935  0cc0 9936  1c1 9937   + caddc 9939   · cmul 9941  +∞cpnf 10071  -∞cmnf 10072  *cxr 10073   < clt 10074  cle 10075  cmin 10266  -cneg 10267   / cdiv 10684  cn 11020  0cn0 11292  cz 11377  cuz 11687  (,)cioo 12175  (,]cioc 12176  [,]cicc 12178  ...cfz 12326  ..^cfzo 12465  cfl 12591  t crest 16081  TopOpenctopn 16082  topGenctg 16098  fldccnfld 19746  Topctop 20698  intcnt 20821  cnccncf 22679   lim climc 23626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fi 8317  df-sup 8348  df-inf 8349  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-ioc 12180  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593  df-seq 12802  df-exp 12861  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-plusg 15954  df-mulr 15955  df-starv 15956  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-rest 16083  df-topn 16084  df-topgen 16104  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-cnfld 19747  df-top 20699  df-topon 20716  df-topsp 20737  df-bases 20750  df-ntr 20824  df-cn 21031  df-cnp 21032  df-xms 22125  df-ms 22126  df-cncf 22681  df-limc 23630
This theorem is referenced by:  fourierdlem94  40417  fourierdlem113  40436
  Copyright terms: Public domain W3C validator