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

Proof of Theorem fourierdlem49
Dummy variables 𝑗 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem49.a . . . . . 6 (𝜑𝐴 ∈ ℝ)
2 fourierdlem49.b . . . . . 6 (𝜑𝐵 ∈ ℝ)
3 fourierdlem49.altb . . . . . 6 (𝜑𝐴 < 𝐵)
4 fourierdlem49.t . . . . . 6 𝑇 = (𝐵𝐴)
5 fourierdlem49.e . . . . . . 7 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥)))
6 ovex 7438 . . . . . . . . . 10 ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ V
7 fourierdlem49.z . . . . . . . . . . 11 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
87fvmpt2 6997 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ V) → (𝑍𝑥) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
96, 8mpan2 691 . . . . . . . . 9 (𝑥 ∈ ℝ → (𝑍𝑥) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
109oveq2d 7421 . . . . . . . 8 (𝑥 ∈ ℝ → (𝑥 + (𝑍𝑥)) = (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
1110mpteq2ia 5216 . . . . . . 7 (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
125, 11eqtri 2758 . . . . . 6 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
131, 2, 3, 4, 12fourierdlem4 46140 . . . . 5 (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))
14 fourierdlem49.x . . . . 5 (𝜑𝑋 ∈ ℝ)
1513, 14ffvelcdmd 7075 . . . 4 (𝜑 → (𝐸𝑋) ∈ (𝐴(,]𝐵))
16 simpr 484 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → (𝐸𝑋) ∈ ran 𝑄)
17 fourierdlem49.q . . . . . . . . . . . . 13 (𝜑𝑄 ∈ (𝑃𝑀))
18 fourierdlem49.m . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℕ)
19 fourierdlem49.p . . . . . . . . . . . . . . 15 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
2019fourierdlem2 46138 . . . . . . . . . . . . . 14 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
2118, 20syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
2217, 21mpbid 232 . . . . . . . . . . . 12 (𝜑 → (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
2322simpld 494 . . . . . . . . . . 11 (𝜑𝑄 ∈ (ℝ ↑m (0...𝑀)))
24 elmapi 8863 . . . . . . . . . . 11 (𝑄 ∈ (ℝ ↑m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
2523, 24syl 17 . . . . . . . . . 10 (𝜑𝑄:(0...𝑀)⟶ℝ)
26 ffn 6706 . . . . . . . . . 10 (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
2725, 26syl 17 . . . . . . . . 9 (𝜑𝑄 Fn (0...𝑀))
2827ad2antrr 726 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → 𝑄 Fn (0...𝑀))
29 fvelrnb 6939 . . . . . . . 8 (𝑄 Fn (0...𝑀) → ((𝐸𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋)))
3028, 29syl 17 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → ((𝐸𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋)))
3116, 30mpbid 232 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋))
32 1zzd 12623 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 1 ∈ ℤ)
33 elfzelz 13541 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
3433ad2antlr 727 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℤ)
35 1e0p1 12750 . . . . . . . . . . . . . . . . 17 1 = (0 + 1)
3635a1i 11 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 1 = (0 + 1))
3734zred 12697 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℝ)
38 elfzle1 13544 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
3938ad2antlr 727 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ≤ 𝑗)
40 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑄𝑗) = (𝐸𝑋) → (𝑄𝑗) = (𝐸𝑋))
4140eqcomd 2741 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑄𝑗) = (𝐸𝑋) → (𝐸𝑋) = (𝑄𝑗))
4241ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝐸𝑋) = (𝑄𝑗))
43 fveq2 6876 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = 0 → (𝑄𝑗) = (𝑄‘0))
4443adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝑄𝑗) = (𝑄‘0))
4522simprld 771 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵))
4645simpld 494 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑄‘0) = 𝐴)
4746ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝑄‘0) = 𝐴)
4842, 44, 473eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝐸𝑋) = 𝐴)
4948adantllr 719 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝐸𝑋) = 𝐴)
5049adantllr 719 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝐸𝑋) = 𝐴)
511adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 ∈ ℝ)
521rexrd 11285 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐴 ∈ ℝ*)
5352adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 ∈ ℝ*)
542rexrd 11285 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐵 ∈ ℝ*)
5554adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐵 ∈ ℝ*)
56 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ∈ (𝐴(,]𝐵))
57 iocgtlb 45531 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸𝑋))
5853, 55, 56, 57syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸𝑋))
5951, 58gtned 11370 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ≠ 𝐴)
6059neneqd 2937 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → ¬ (𝐸𝑋) = 𝐴)
6160ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → ¬ (𝐸𝑋) = 𝐴)
6250, 61pm2.65da 816 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → ¬ 𝑗 = 0)
6362neqned 2939 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ≠ 0)
6437, 39, 63ne0gt0d 11372 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 < 𝑗)
65 0zd 12600 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ∈ ℤ)
66 zltp1le 12642 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
6765, 34, 66syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
6864, 67mpbid 232 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 + 1) ≤ 𝑗)
6936, 68eqbrtrd 5141 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 1 ≤ 𝑗)
70 eluz2 12858 . . . . . . . . . . . . . . 15 (𝑗 ∈ (ℤ‘1) ↔ (1 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗))
7132, 34, 69, 70syl3anbrc 1344 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ (ℤ‘1))
72 nnuz 12895 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
7371, 72eleqtrrdi 2845 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℕ)
74 nnm1nn0 12542 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ → (𝑗 − 1) ∈ ℕ0)
7573, 74syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ ℕ0)
76 nn0uz 12894 . . . . . . . . . . . . 13 0 = (ℤ‘0)
7776a1i 11 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → ℕ0 = (ℤ‘0))
7875, 77eleqtrd 2836 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (ℤ‘0))
7918nnzd 12615 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℤ)
8079ad3antrrr 730 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑀 ∈ ℤ)
81 peano2zm 12635 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℤ → (𝑗 − 1) ∈ ℤ)
8233, 81syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℤ)
8382zred 12697 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
8433zred 12697 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
85 elfzel2 13539 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
8685zred 12697 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
8784ltm1d 12174 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑗)
88 elfzle2 13545 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗𝑀)
8983, 84, 86, 87, 88ltletrd 11395 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
9089ad2antlr 727 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) < 𝑀)
91 elfzo2 13679 . . . . . . . . . . 11 ((𝑗 − 1) ∈ (0..^𝑀) ↔ ((𝑗 − 1) ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) < 𝑀))
9278, 80, 90, 91syl3anbrc 1344 . . . . . . . . . 10 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (0..^𝑀))
9325ad3antrrr 730 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑄:(0...𝑀)⟶ℝ)
9434, 81syl 17 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ ℤ)
9575nn0ge0d 12565 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ≤ (𝑗 − 1))
9683, 86, 89ltled 11383 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ≤ 𝑀)
9796ad2antlr 727 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ≤ 𝑀)
9865, 80, 94, 95, 97elfzd 13532 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (0...𝑀))
9993, 98ffvelcdmd 7075 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ)
10099rexrd 11285 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ*)
10125ffvelcdmda 7074 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ)
102101rexrd 11285 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ*)
103102adantlr 715 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ*)
104103adantr 480 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ∈ ℝ*)
105 iocssre 13444 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
10652, 2, 105syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
107106sselda 3958 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ∈ ℝ)
108107rexrd 11285 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ∈ ℝ*)
109108ad2antrr 726 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ*)
110 simplll 774 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝜑)
111 ovex 7438 . . . . . . . . . . . . . . . 16 (𝑗 − 1) ∈ V
112 eleq1 2822 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 − 1) → (𝑖 ∈ (0..^𝑀) ↔ (𝑗 − 1) ∈ (0..^𝑀)))
113112anbi2d 630 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 − 1) → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀))))
114 fveq2 6876 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 − 1) → (𝑄𝑖) = (𝑄‘(𝑗 − 1)))
115 oveq1 7412 . . . . . . . . . . . . . . . . . . 19 (𝑖 = (𝑗 − 1) → (𝑖 + 1) = ((𝑗 − 1) + 1))
116115fveq2d 6880 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 − 1) → (𝑄‘(𝑖 + 1)) = (𝑄‘((𝑗 − 1) + 1)))
117114, 116breq12d 5132 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 − 1) → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1))))
118113, 117imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 − 1) → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))))
11922simprrd 773 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))
120119r19.21bi 3234 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
121111, 118, 120vtocl 3537 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
122110, 92, 121syl2anc 584 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
12333zcnd 12698 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
124 1cnd 11230 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 1 ∈ ℂ)
125123, 124npcand 11598 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → ((𝑗 − 1) + 1) = 𝑗)
126125eqcomd 2741 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → 𝑗 = ((𝑗 − 1) + 1))
127126fveq2d 6880 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → (𝑄𝑗) = (𝑄‘((𝑗 − 1) + 1)))
128127eqcomd 2741 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
129128ad2antlr 727 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
130122, 129breqtrd 5145 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄𝑗))
131 simpr 484 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) = (𝐸𝑋))
132130, 131breqtrd 5145 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝐸𝑋))
133106, 15sseldd 3959 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸𝑋) ∈ ℝ)
134133leidd 11803 . . . . . . . . . . . . . . 15 (𝜑 → (𝐸𝑋) ≤ (𝐸𝑋))
135134ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝐸𝑋))
13641adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) = (𝑄𝑗))
137135, 136breqtrd 5145 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄𝑗))
138137adantllr 719 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄𝑗))
139100, 104, 109, 132, 138eliocd 45536 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄𝑗)))
140127oveq2d 7421 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → ((𝑄‘(𝑗 − 1))(,](𝑄𝑗)) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
141140ad2antlr 727 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → ((𝑄‘(𝑗 − 1))(,](𝑄𝑗)) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
142139, 141eleqtrd 2836 . . . . . . . . . 10 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
143114, 116oveq12d 7423 . . . . . . . . . . . 12 (𝑖 = (𝑗 − 1) → ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
144143eleq2d 2820 . . . . . . . . . . 11 (𝑖 = (𝑗 − 1) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) ↔ (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))))
145144rspcev 3601 . . . . . . . . . 10 (((𝑗 − 1) ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
14692, 142, 145syl2anc 584 . . . . . . . . 9 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
147146ex 412 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
148147adantlr 715 . . . . . . 7 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
149148rexlimdva 3141 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
15031, 149mpd 15 . . . . 5 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
15118ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → 𝑀 ∈ ℕ)
15225ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ)
153 iocssicc 13454 . . . . . . . . . 10 (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵)
15446eqcomd 2741 . . . . . . . . . . 11 (𝜑𝐴 = (𝑄‘0))
15545simprd 495 . . . . . . . . . . . 12 (𝜑 → (𝑄𝑀) = 𝐵)
156155eqcomd 2741 . . . . . . . . . . 11 (𝜑𝐵 = (𝑄𝑀))
157154, 156oveq12d 7423 . . . . . . . . . 10 (𝜑 → (𝐴[,]𝐵) = ((𝑄‘0)[,](𝑄𝑀)))
158153, 157sseqtrid 4001 . . . . . . . . 9 (𝜑 → (𝐴(,]𝐵) ⊆ ((𝑄‘0)[,](𝑄𝑀)))
159158sselda 3958 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ∈ ((𝑄‘0)[,](𝑄𝑀)))
160159adantr 480 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (𝐸𝑋) ∈ ((𝑄‘0)[,](𝑄𝑀)))
161 simpr 484 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ¬ (𝐸𝑋) ∈ ran 𝑄)
162 fveq2 6876 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝑄𝑘) = (𝑄𝑗))
163162breq1d 5129 . . . . . . . . 9 (𝑘 = 𝑗 → ((𝑄𝑘) < (𝐸𝑋) ↔ (𝑄𝑗) < (𝐸𝑋)))
164163cbvrabv 3426 . . . . . . . 8 {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < (𝐸𝑋)} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < (𝐸𝑋)}
165164supeq1i 9459 . . . . . . 7 sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < (𝐸𝑋)}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < (𝐸𝑋)}, ℝ, < )
166151, 152, 160, 161, 165fourierdlem25 46161 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
167 ioossioc 45521 . . . . . . . . 9 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))
168167sseli 3954 . . . . . . . 8 ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
169168a1i 11 . . . . . . 7 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
170169reximdva 3153 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
171166, 170mpd 15 . . . . 5 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
172150, 171pm2.61dan 812 . . . 4 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
17315, 172mpdan 687 . . 3 (𝜑 → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
174 fourierdlem49.f . . . . . . . . . . 11 (𝜑𝐹:𝐷⟶ℝ)
175 frel 6711 . . . . . . . . . . 11 (𝐹:𝐷⟶ℝ → Rel 𝐹)
176174, 175syl 17 . . . . . . . . . 10 (𝜑 → Rel 𝐹)
177 resindm 6017 . . . . . . . . . . 11 (Rel 𝐹 → (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹)) = (𝐹 ↾ (-∞(,)(𝐸𝑋))))
178177eqcomd 2741 . . . . . . . . . 10 (Rel 𝐹 → (𝐹 ↾ (-∞(,)(𝐸𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹)))
179176, 178syl 17 . . . . . . . . 9 (𝜑 → (𝐹 ↾ (-∞(,)(𝐸𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹)))
180 fdm 6715 . . . . . . . . . . . 12 (𝐹:𝐷⟶ℝ → dom 𝐹 = 𝐷)
181174, 180syl 17 . . . . . . . . . . 11 (𝜑 → dom 𝐹 = 𝐷)
182181ineq2d 4195 . . . . . . . . . 10 (𝜑 → ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹) = ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
183182reseq2d 5966 . . . . . . . . 9 (𝜑 → (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹)) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)))
184179, 183eqtrd 2770 . . . . . . . 8 (𝜑 → (𝐹 ↾ (-∞(,)(𝐸𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)))
1851843ad2ant1 1133 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ (-∞(,)(𝐸𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)))
186185oveq1d 7420 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) lim (𝐸𝑋)))
187 ax-resscn 11186 . . . . . . . . . . 11 ℝ ⊆ ℂ
188187a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ⊆ ℂ)
189174, 188fssd 6723 . . . . . . . . 9 (𝜑𝐹:𝐷⟶ℂ)
1901893ad2ant1 1133 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐹:𝐷⟶ℂ)
191 inss2 4213 . . . . . . . . 9 ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ 𝐷
192191a1i 11 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ 𝐷)
193190, 192fssresd 6745 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)):((-∞(,)(𝐸𝑋)) ∩ 𝐷)⟶ℂ)
194 mnfxr 11292 . . . . . . . . . 10 -∞ ∈ ℝ*
195194a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ∈ ℝ*)
19625adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
197 elfzofz 13692 . . . . . . . . . . . . . 14 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
198197adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
199196, 198ffvelcdmd 7075 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
200199rexrd 11285 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ*)
201199mnfltd 13140 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ < (𝑄𝑖))
202195, 200, 201xrltled 13166 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ≤ (𝑄𝑖))
203 iooss1 13397 . . . . . . . . . 10 ((-∞ ∈ ℝ* ∧ -∞ ≤ (𝑄𝑖)) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ (-∞(,)(𝐸𝑋)))
204194, 202, 203sylancr 587 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ (-∞(,)(𝐸𝑋)))
2052043adant3 1132 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ (-∞(,)(𝐸𝑋)))
206 fzofzp1 13780 . . . . . . . . . . . . . 14 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
207206adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
208196, 207ffvelcdmd 7075 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
2092083adant3 1132 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
210209rexrd 11285 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
2111993adant3 1132 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
212211rexrd 11285 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ*)
213 simp3 1138 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
214 iocleub 45532 . . . . . . . . . . 11 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
215212, 210, 213, 214syl3anc 1373 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
216 iooss2 13398 . . . . . . . . . 10 (((𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
217210, 215, 216syl2anc 584 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
218 fourierdlem49.cn . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
219 cncff 24837 . . . . . . . . . . . . 13 ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
220 fdm 6715 . . . . . . . . . . . . 13 ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ → dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
221218, 219, 2203syl 18 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
222 ssdmres 6000 . . . . . . . . . . . 12 (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹 ↔ dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
223221, 222sylibr 234 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹)
224181adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → dom 𝐹 = 𝐷)
225223, 224sseqtrd 3995 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
2262253adant3 1132 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
227217, 226sstrd 3969 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ 𝐷)
228205, 227ssind 4216 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
229 fourierdlem49.d . . . . . . . . . 10 (𝜑𝐷 ⊆ ℝ)
230229, 188sstrd 3969 . . . . . . . . 9 (𝜑𝐷 ⊆ ℂ)
2312303ad2ant1 1133 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐷 ⊆ ℂ)
232191, 231sstrid 3970 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ ℂ)
233 eqid 2735 . . . . . . 7 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
234 eqid 2735 . . . . . . 7 ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) = ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
2351333ad2ant1 1133 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ℝ)
236235rexrd 11285 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ℝ*)
237 iocgtlb 45531 . . . . . . . . . 10 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝐸𝑋))
238212, 210, 213, 237syl3anc 1373 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝐸𝑋))
239235leidd 11803 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝐸𝑋))
240212, 236, 236, 238, 239eliocd 45536 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝐸𝑋)))
241 ioounsn 13494 . . . . . . . . . . 11 (((𝑄𝑖) ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ* ∧ (𝑄𝑖) < (𝐸𝑋)) → (((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)}) = ((𝑄𝑖)(,](𝐸𝑋)))
242212, 236, 238, 241syl3anc 1373 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)}) = ((𝑄𝑖)(,](𝐸𝑋)))
243242fveq2d 6880 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘(((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)})) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘((𝑄𝑖)(,](𝐸𝑋))))
244233cnfldtop 24722 . . . . . . . . . . 11 (TopOpen‘ℂfld) ∈ Top
245 ovex 7438 . . . . . . . . . . . . 13 (-∞(,)(𝐸𝑋)) ∈ V
246245inex1 5287 . . . . . . . . . . . 12 ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∈ V
247 snex 5406 . . . . . . . . . . . 12 {(𝐸𝑋)} ∈ V
248246, 247unex 7738 . . . . . . . . . . 11 (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∈ V
249 resttop 23098 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ∈ Top ∧ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∈ V) → ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ Top)
250244, 248, 249mp2an 692 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ Top
251 retop 24700 . . . . . . . . . . . . 13 (topGen‘ran (,)) ∈ Top
252251a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (topGen‘ran (,)) ∈ Top)
253248a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∈ V)
254 iooretop 24704 . . . . . . . . . . . . 13 ((𝑄𝑖)(,)+∞) ∈ (topGen‘ran (,))
255254a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)+∞) ∈ (topGen‘ran (,)))
256 elrestr 17442 . . . . . . . . . . . 12 (((topGen‘ran (,)) ∈ Top ∧ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∈ V ∧ ((𝑄𝑖)(,)+∞) ∈ (topGen‘ran (,))) → (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
257252, 253, 255, 256syl3anc 1373 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
258 simpr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 = (𝐸𝑋)) → 𝑥 = (𝐸𝑋))
259 pnfxr 11289 . . . . . . . . . . . . . . . . . . . 20 +∞ ∈ ℝ*
260259a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → +∞ ∈ ℝ*)
261235ltpnfd 13137 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) < +∞)
262212, 260, 235, 238, 261eliood 45527 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,)+∞))
263 snidg 4636 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸𝑋) ∈ ℝ → (𝐸𝑋) ∈ {(𝐸𝑋)})
264 elun2 4158 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸𝑋) ∈ {(𝐸𝑋)} → (𝐸𝑋) ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
265263, 264syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝐸𝑋) ∈ ℝ → (𝐸𝑋) ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
266133, 265syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐸𝑋) ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
2672663ad2ant1 1133 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
268262, 267elind 4175 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
269268adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
270258, 269eqeltrd 2834 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
271270adantlr 715 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
272212adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝑄𝑖) ∈ ℝ*)
273259a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → +∞ ∈ ℝ*)
274200adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝑄𝑖) ∈ ℝ*)
275133adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐸𝑋) ∈ ℝ)
276275adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝐸𝑋) ∈ ℝ)
277 iocssre 13444 . . . . . . . . . . . . . . . . . . . 20 (((𝑄𝑖) ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ) → ((𝑄𝑖)(,](𝐸𝑋)) ⊆ ℝ)
278274, 276, 277syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → ((𝑄𝑖)(,](𝐸𝑋)) ⊆ ℝ)
279 simpr 484 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋)))
280278, 279sseldd 3959 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ ℝ)
2812803adantl3 1169 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ ℝ)
282276rexrd 11285 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝐸𝑋) ∈ ℝ*)
283 iocgtlb 45531 . . . . . . . . . . . . . . . . . . 19 (((𝑄𝑖) ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ*𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝑄𝑖) < 𝑥)
284274, 282, 279, 283syl3anc 1373 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝑄𝑖) < 𝑥)
2852843adantl3 1169 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝑄𝑖) < 𝑥)
286281ltpnfd 13137 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 < +∞)
287272, 273, 281, 285, 286eliood 45527 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ ((𝑄𝑖)(,)+∞))
288287adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ((𝑄𝑖)(,)+∞))
289194a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → -∞ ∈ ℝ*)
290282adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ*)
291280adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ℝ)
292291mnfltd 13140 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → -∞ < 𝑥)
293133ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ)
294 iocleub 45532 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑄𝑖) ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ*𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ≤ (𝐸𝑋))
295274, 282, 279, 294syl3anc 1373 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ≤ (𝐸𝑋))
296295adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ≤ (𝐸𝑋))
297 neqne 2940 . . . . . . . . . . . . . . . . . . . . . 22 𝑥 = (𝐸𝑋) → 𝑥 ≠ (𝐸𝑋))
298297necomd 2987 . . . . . . . . . . . . . . . . . . . . 21 𝑥 = (𝐸𝑋) → (𝐸𝑋) ≠ 𝑥)
299298adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ≠ 𝑥)
300291, 293, 296, 299leneltd 11389 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 < (𝐸𝑋))
301289, 290, 291, 292, 300eliood 45527 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (-∞(,)(𝐸𝑋)))
3023013adantll3 45066 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (-∞(,)(𝐸𝑋)))
303226ad2antrr 726 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
304272adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝑄𝑖) ∈ ℝ*)
305210ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
306281adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ℝ)
307285adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝑄𝑖) < 𝑥)
308235ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ)
309209ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
3103003adantll3 45066 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 < (𝐸𝑋))
311215ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
312306, 308, 309, 310, 311ltletrd 11395 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 < (𝑄‘(𝑖 + 1)))
313304, 305, 306, 307, 312eliood 45527 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
314303, 313sseldd 3959 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥𝐷)
315302, 314elind 4175 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
316 elun1 4157 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷) → 𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
317315, 316syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
318288, 317elind 4175 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
319271, 318pm2.61dan 812 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
320212adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝑄𝑖) ∈ ℝ*)
321236adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝐸𝑋) ∈ ℝ*)
322 elinel1 4176 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ∈ ((𝑄𝑖)(,)+∞))
323 elioore 13392 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((𝑄𝑖)(,)+∞) → 𝑥 ∈ ℝ)
324323rexrd 11285 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((𝑄𝑖)(,)+∞) → 𝑥 ∈ ℝ*)
325322, 324syl 17 . . . . . . . . . . . . . . 15 (𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ∈ ℝ*)
326325adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ∈ ℝ*)
327200adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝑄𝑖) ∈ ℝ*)
328259a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → +∞ ∈ ℝ*)
329322adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ∈ ((𝑄𝑖)(,)+∞))
330 ioogtlb 45524 . . . . . . . . . . . . . . . 16 (((𝑄𝑖) ∈ ℝ* ∧ +∞ ∈ ℝ*𝑥 ∈ ((𝑄𝑖)(,)+∞)) → (𝑄𝑖) < 𝑥)
331327, 328, 329, 330syl3anc 1373 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝑄𝑖) < 𝑥)
3323313adantl3 1169 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝑄𝑖) < 𝑥)
333 elinel2 4177 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
334 elsni 4618 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {(𝐸𝑋)} → 𝑥 = (𝐸𝑋))
335334adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ {(𝐸𝑋)}) → 𝑥 = (𝐸𝑋))
336134adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ {(𝐸𝑋)}) → (𝐸𝑋) ≤ (𝐸𝑋))
337335, 336eqbrtrd 5141 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ≤ (𝐸𝑋))
338337adantlr 715 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∧ 𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ≤ (𝐸𝑋))
339 simpll 766 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∧ ¬ 𝑥 ∈ {(𝐸𝑋)}) → 𝜑)
340 elunnel2 4130 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∧ ¬ 𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
341340adantll 714 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∧ ¬ 𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
342 elinel1 4176 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷) → 𝑥 ∈ (-∞(,)(𝐸𝑋)))
343 elioore 13392 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (-∞(,)(𝐸𝑋)) → 𝑥 ∈ ℝ)
344343adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 ∈ ℝ)
345133adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → (𝐸𝑋) ∈ ℝ)
346194a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → -∞ ∈ ℝ*)
347345rexrd 11285 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → (𝐸𝑋) ∈ ℝ*)
348 simpr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 ∈ (-∞(,)(𝐸𝑋)))
349 iooltub 45539 . . . . . . . . . . . . . . . . . . . . . 22 ((-∞ ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ*𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 < (𝐸𝑋))
350346, 347, 348, 349syl3anc 1373 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 < (𝐸𝑋))
351344, 345, 350ltled 11383 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 ≤ (𝐸𝑋))
352342, 351sylan2 593 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) → 𝑥 ≤ (𝐸𝑋))
353339, 341, 352syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∧ ¬ 𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ≤ (𝐸𝑋))
354338, 353pm2.61dan 812 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ≤ (𝐸𝑋))
355354adantlr 715 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ≤ (𝐸𝑋))
356333, 355sylan2 593 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ≤ (𝐸𝑋))
3573563adantl3 1169 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ≤ (𝐸𝑋))
358320, 321, 326, 332, 357eliocd 45536 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋)))
359319, 358impbida 800 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋)) ↔ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))))
360359eqrdv 2733 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,](𝐸𝑋)) = (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
361 ioossre 13424 . . . . . . . . . . . . . 14 (-∞(,)(𝐸𝑋)) ⊆ ℝ
362 ssinss1 4221 . . . . . . . . . . . . . 14 ((-∞(,)(𝐸𝑋)) ⊆ ℝ → ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ ℝ)
363361, 362mp1i 13 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ ℝ)
364235snssd 4785 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {(𝐸𝑋)} ⊆ ℝ)
365363, 364unssd 4167 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ⊆ ℝ)
366 eqid 2735 . . . . . . . . . . . . 13 (topGen‘ran (,)) = (topGen‘ran (,))
367233, 366rerest 24743 . . . . . . . . . . . 12 ((((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) = ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
368365, 367syl 17 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) = ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
369257, 360, 3683eltr4d 2849 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,](𝐸𝑋)) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
370 isopn3i 23020 . . . . . . . . . 10 ((((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ Top ∧ ((𝑄𝑖)(,](𝐸𝑋)) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘((𝑄𝑖)(,](𝐸𝑋))) = ((𝑄𝑖)(,](𝐸𝑋)))
371250, 369, 370sylancr 587 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘((𝑄𝑖)(,](𝐸𝑋))) = ((𝑄𝑖)(,](𝐸𝑋)))
372243, 371eqtr2d 2771 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,](𝐸𝑋)) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘(((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)})))
373240, 372eleqtrd 2836 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘(((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)})))
374193, 228, 232, 233, 234, 373limcres 25839 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) lim (𝐸𝑋)))
375228resabs1d 5995 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) = (𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))))
376375oveq1d 7420 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
377186, 374, 3763eqtr2d 2776 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
378181feq2d 6692 . . . . . . . . . . . 12 (𝜑 → (𝐹:dom 𝐹⟶ℂ ↔ 𝐹:𝐷⟶ℂ))
379189, 378mpbird 257 . . . . . . . . . . 11 (𝜑𝐹:dom 𝐹⟶ℂ)
380379adantr 480 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝐹:dom 𝐹⟶ℂ)
3813803ad2antl1 1186 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝐹:dom 𝐹⟶ℂ)
382 ioosscn 13425 . . . . . . . . . 10 ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ℂ
383382a1i 11 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ℂ)
384181eqcomd 2741 . . . . . . . . . . . 12 (𝜑𝐷 = dom 𝐹)
3853843ad2ant1 1133 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐷 = dom 𝐹)
386227, 385sseqtrd 3995 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ dom 𝐹)
387386adantr 480 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ dom 𝐹)
3887a1i 11 . . . . . . . . . . . . . . 15 (𝜑𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
389 oveq2 7413 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋 → (𝐵𝑥) = (𝐵𝑋))
390389oveq1d 7420 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋 → ((𝐵𝑥) / 𝑇) = ((𝐵𝑋) / 𝑇))
391390fveq2d 6880 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋 → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵𝑋) / 𝑇)))
392391oveq1d 7420 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
393392adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑥 = 𝑋) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
3942, 14resubcld 11665 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵𝑋) ∈ ℝ)
3952, 1resubcld 11665 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐵𝐴) ∈ ℝ)
3964, 395eqeltrid 2838 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑇 ∈ ℝ)
3971, 2posdifd 11824 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
3983, 397mpbid 232 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 < (𝐵𝐴))
3994eqcomi 2744 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵𝐴) = 𝑇
400399a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵𝐴) = 𝑇)
401398, 400breqtrd 5145 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 < 𝑇)
402401gt0ne0d 11801 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑇 ≠ 0)
403394, 396, 402redivcld 12069 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵𝑋) / 𝑇) ∈ ℝ)
404403flcld 13815 . . . . . . . . . . . . . . . . 17 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
405404zred 12697 . . . . . . . . . . . . . . . 16 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℝ)
406405, 396remulcld 11265 . . . . . . . . . . . . . . 15 (𝜑 → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
407388, 393, 14, 406fvmptd 6993 . . . . . . . . . . . . . 14 (𝜑 → (𝑍𝑋) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
408407, 406eqeltrd 2834 . . . . . . . . . . . . 13 (𝜑 → (𝑍𝑋) ∈ ℝ)
409408recnd 11263 . . . . . . . . . . . 12 (𝜑 → (𝑍𝑋) ∈ ℂ)
410409adantr 480 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → (𝑍𝑋) ∈ ℂ)
4114103ad2antl1 1186 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → (𝑍𝑋) ∈ ℂ)
412411negcld 11581 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → -(𝑍𝑋) ∈ ℂ)
413 eqid 2735 . . . . . . . . 9 {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}
414 ioosscn 13425 . . . . . . . . . . . . . . . . . . 19 (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ ℂ
415414sseli 3954 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) → 𝑦 ∈ ℂ)
416415adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℂ)
417409adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℂ)
418416, 417pncand 11595 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = 𝑦)
419418eqcomd 2741 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)))
4204193ad2antl1 1186 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)))
421407oveq2d 7421 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = ((𝑦 + (𝑍𝑋)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
422421adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = ((𝑦 + (𝑍𝑋)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
423416, 417addcld 11254 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℂ)
424406recnd 11263 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
425424adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
426423, 425negsubd 11600 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + (𝑍𝑋)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
427404zcnd 12698 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℂ)
428396recnd 11263 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑇 ∈ ℂ)
429427, 428mulneg1d 11690 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
430429eqcomd 2741 . . . . . . . . . . . . . . . . . . 19 (𝜑 → -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
431430oveq2d 7421 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑦 + (𝑍𝑋)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
432431adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
433422, 426, 4323eqtr2d 2776 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
4344333ad2antl1 1186 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
435404znegcld 12699 . . . . . . . . . . . . . . . . . 18 (𝜑 → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
436435adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
4374363ad2antl1 1186 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
438 simpl1 1192 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝜑)
439227adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ 𝐷)
440200adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) ∈ ℝ*)
441133rexrd 11285 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐸𝑋) ∈ ℝ*)
442441ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐸𝑋) ∈ ℝ*)
443 elioore 13392 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) → 𝑦 ∈ ℝ)
444443adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
445408adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℝ)
446444, 445readdcld 11264 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
447446adantlr 715 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
448408adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑍𝑋) ∈ ℝ)
449199, 448resubcld 11665 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ)
450449rexrd 11285 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
451450adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
45214rexrd 11285 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑋 ∈ ℝ*)
453452ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑋 ∈ ℝ*)
454 simpr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
455 ioogtlb 45524 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑦)
456451, 453, 454, 455syl3anc 1373 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑦)
457199adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) ∈ ℝ)
458448adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℝ)
459443adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
460457, 458, 459ltsubaddd 11833 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (((𝑄𝑖) − (𝑍𝑋)) < 𝑦 ↔ (𝑄𝑖) < (𝑦 + (𝑍𝑋))))
461456, 460mpbid 232 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) < (𝑦 + (𝑍𝑋)))
46214ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑋 ∈ ℝ)
463 iooltub 45539 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 < 𝑋)
464451, 453, 454, 463syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 < 𝑋)
465459, 462, 458, 464ltadd1dd 11848 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝑋 + (𝑍𝑋)))
4665a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥))))
467 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑋𝑥 = 𝑋)
468 fveq2 6876 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑋 → (𝑍𝑥) = (𝑍𝑋))
469467, 468oveq12d 7423 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑋 → (𝑥 + (𝑍𝑥)) = (𝑋 + (𝑍𝑋)))
470469adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 = 𝑋) → (𝑥 + (𝑍𝑥)) = (𝑋 + (𝑍𝑋)))
47114, 408readdcld 11264 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑋 + (𝑍𝑋)) ∈ ℝ)
472466, 470, 14, 471fvmptd 6993 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
473472eqcomd 2741 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
474473ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
475465, 474breqtrd 5145 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝐸𝑋))
476440, 442, 447, 461, 475eliood 45527 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ((𝑄𝑖)(,)(𝐸𝑋)))
4774763adantl3 1169 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ((𝑄𝑖)(,)(𝐸𝑋)))
478439, 477sseldd 3959 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ 𝐷)
479438, 478, 4373jca 1128 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
480 eleq1 2822 . . . . . . . . . . . . . . . . . . 19 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
4814803anbi3d 1444 . . . . . . . . . . . . . . . . . 18 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)))
482 oveq1 7412 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 · 𝑇) = (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
483482oveq2d 7421 . . . . . . . . . . . . . . . . . . 19 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
484483eleq1d 2819 . . . . . . . . . . . . . . . . . 18 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
485481, 484imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)))
486 ovex 7438 . . . . . . . . . . . . . . . . . 18 (𝑦 + (𝑍𝑋)) ∈ V
487 eleq1 2822 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑦 + (𝑍𝑋)) → (𝑥𝐷 ↔ (𝑦 + (𝑍𝑋)) ∈ 𝐷))
4884873anbi2d 1443 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑦 + (𝑍𝑋)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ)))
489 oveq1 7412 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑦 + (𝑍𝑋)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)))
490489eleq1d 2819 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑦 + (𝑍𝑋)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷))
491488, 490imbi12d 344 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑦 + (𝑍𝑋)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)))
492 fourierdlem49.dper . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)
493486, 491, 492vtocl 3537 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)
494485, 493vtoclg 3533 . . . . . . . . . . . . . . . 16 (-(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ → ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
495437, 479, 494sylc 65 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
496434, 495eqeltrd 2834 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) ∈ 𝐷)
497420, 496eqeltrd 2834 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦𝐷)
498497ralrimiva 3132 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑦𝐷)
499 dfss3 3947 . . . . . . . . . . . 12 ((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷 ↔ ∀𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑦𝐷)
500498, 499sylibr 234 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷)
501199recnd 11263 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℂ)
502409adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑍𝑋) ∈ ℂ)
503501, 502negsubd 11600 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + -(𝑍𝑋)) = ((𝑄𝑖) − (𝑍𝑋)))
504503eqcomd 2741 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) = ((𝑄𝑖) + -(𝑍𝑋)))
505472oveq1d 7420 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸𝑋) + -(𝑍𝑋)) = ((𝑋 + (𝑍𝑋)) + -(𝑍𝑋)))
506471recnd 11263 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑋 + (𝑍𝑋)) ∈ ℂ)
507506, 409negsubd 11600 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑋 + (𝑍𝑋)) + -(𝑍𝑋)) = ((𝑋 + (𝑍𝑋)) − (𝑍𝑋)))
50814recnd 11263 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 ∈ ℂ)
509508, 409pncand 11595 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑋 + (𝑍𝑋)) − (𝑍𝑋)) = 𝑋)
510505, 507, 5093eqtrrd 2775 . . . . . . . . . . . . . . 15 (𝜑𝑋 = ((𝐸𝑋) + -(𝑍𝑋)))
511510adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 = ((𝐸𝑋) + -(𝑍𝑋)))
512504, 511oveq12d 7423 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) = (((𝑄𝑖) + -(𝑍𝑋))(,)((𝐸𝑋) + -(𝑍𝑋))))
513448renegcld 11664 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → -(𝑍𝑋) ∈ ℝ)
514199, 275, 513iooshift 45551 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) + -(𝑍𝑋))(,)((𝐸𝑋) + -(𝑍𝑋))) = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))})
515512, 514eqtr2d 2771 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} = (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
5165153adant3 1132 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} = (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
5171813ad2ant1 1133 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → dom 𝐹 = 𝐷)
518500, 516, 5173sstr4d 4014 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} ⊆ dom 𝐹)
519518adantr 480 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} ⊆ dom 𝐹)
520407negeqd 11476 . . . . . . . . . . . . . . . 16 (𝜑 → -(𝑍𝑋) = -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
521520, 430eqtrd 2770 . . . . . . . . . . . . . . 15 (𝜑 → -(𝑍𝑋) = (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
522521oveq2d 7421 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 + -(𝑍𝑋)) = (𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
523522fveq2d 6880 . . . . . . . . . . . . 13 (𝜑 → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
524523adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
5255243ad2antl1 1186 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
526435adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
5275263ad2antl1 1186 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
528 simpl1 1192 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → 𝜑)
529227sselda 3958 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → 𝑥𝐷)
530528, 529, 5273jca 1128 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝜑𝑥𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
5314803anbi3d 1444 . . . . . . . . . . . . . 14 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑𝑥𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)))
532482oveq2d 7421 . . . . . . . . . . . . . . . 16 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = (𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
533532fveq2d 6880 . . . . . . . . . . . . . . 15 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
534533eqeq1d 2737 . . . . . . . . . . . . . 14 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥) ↔ (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
535531, 534imbi12d 344 . . . . . . . . . . . . 13 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥)) ↔ ((𝜑𝑥𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥))))
536 fourierdlem49.per . . . . . . . . . . . . 13 ((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥))
537535, 536vtoclg 3533 . . . . . . . . . . . 12 (-(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ → ((𝜑𝑥𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
538527, 530, 537sylc 65 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥))
539525, 538eqtrd 2770 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹𝑥))
540539adantlr 715 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹𝑥))
541 simpr 484 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
542381, 383, 387, 412, 413, 519, 540, 541limcperiod 45657 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝑦 ∈ ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) lim ((𝐸𝑋) + -(𝑍𝑋))))
543515reseq2d 5966 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) = (𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)))
544511eqcomd 2741 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) + -(𝑍𝑋)) = 𝑋)
545543, 544oveq12d 7423 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) lim ((𝐸𝑋) + -(𝑍𝑋))) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
5465453adant3 1132 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) lim ((𝐸𝑋) + -(𝑍𝑋))) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
547546adantr 480 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) lim ((𝐸𝑋) + -(𝑍𝑋))) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
548542, 547eleqtrd 2836 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
549379adantr 480 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → 𝐹:dom 𝐹⟶ℂ)
5505493ad2antl1 1186 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → 𝐹:dom 𝐹⟶ℂ)
551414a1i 11 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ ℂ)
552500, 517sseqtrrd 3996 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ dom 𝐹)
553552adantr 480 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ dom 𝐹)
554409adantr 480 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → (𝑍𝑋) ∈ ℂ)
5555543ad2antl1 1186 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → (𝑍𝑋) ∈ ℂ)
556 eqid 2735 . . . . . . . . 9 {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}
557501, 502npcand 11598 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) − (𝑍𝑋)) + (𝑍𝑋)) = (𝑄𝑖))
558557eqcomd 2741 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) = (((𝑄𝑖) − (𝑍𝑋)) + (𝑍𝑋)))
559472adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
560558, 559oveq12d 7423 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝐸𝑋)) = ((((𝑄𝑖) − (𝑍𝑋)) + (𝑍𝑋))(,)(𝑋 + (𝑍𝑋))))
56114adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
562449, 561, 448iooshift 45551 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((((𝑄𝑖) − (𝑍𝑋)) + (𝑍𝑋))(,)(𝑋 + (𝑍𝑋))) = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))})
563560, 562eqtr2d 2771 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} = ((𝑄𝑖)(,)(𝐸𝑋)))
5645633adant3 1132 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} = ((𝑄𝑖)(,)(𝐸𝑋)))
565227, 564, 5173sstr4d 4014 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} ⊆ dom 𝐹)
566565adantr 480 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} ⊆ dom 𝐹)
567407oveq2d 7421 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 + (𝑍𝑋)) = (𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
568567fveq2d 6880 . . . . . . . . . . . . 13 (𝜑 → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
569568adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
5705693ad2antl1 1186 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
571404adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
5725713ad2antl1 1186 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
573 simpl1 1192 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝜑)
574500sselda 3958 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑥𝐷)
575573, 574, 5723jca 1128 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝜑𝑥𝐷 ∧ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
576 eleq1 2822 . . . . . . . . . . . . . . 15 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
5775763anbi3d 1444 . . . . . . . . . . . . . 14 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑𝑥𝐷 ∧ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)))
578 oveq1 7412 . . . . . . . . . . . . . . . . 17 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
579578oveq2d 7421 . . . . . . . . . . . . . . . 16 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = (𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
580579fveq2d 6880 . . . . . . . . . . . . . . 15 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
581580eqeq1d 2737 . . . . . . . . . . . . . 14 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → ((𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥) ↔ (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
582577, 581imbi12d 344 . . . . . . . . . . . . 13 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥)) ↔ ((𝜑𝑥𝐷 ∧ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥))))
583582, 536vtoclg 3533 . . . . . . . . . . . 12 ((⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ → ((𝜑𝑥𝐷 ∧ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
584572, 575, 583sylc 65 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥))
585570, 584eqtrd 2770 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹𝑥))
586585adantlr 715 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹𝑥))
587 simpr 484 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
588550, 551, 553, 555, 556, 566, 586, 587limcperiod 45657 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → 𝑦 ∈ ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) lim (𝑋 + (𝑍𝑋))))
589563reseq2d 5966 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) = (𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))))
590473adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
591589, 590oveq12d 7423 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) lim (𝑋 + (𝑍𝑋))) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
5925913adant3 1132 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) lim (𝑋 + (𝑍𝑋))) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
593592adantr 480 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) lim (𝑋 + (𝑍𝑋))) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
594588, 593eleqtrd 2836 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
595548, 594impbida 800 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) ↔ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)))
596595eqrdv 2733 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
597 resindm 6017 . . . . . . . . . . 11 (Rel 𝐹 → (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)) = (𝐹 ↾ (-∞(,)𝑋)))
598597eqcomd 2741 . . . . . . . . . 10 (Rel 𝐹 → (𝐹 ↾ (-∞(,)𝑋)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)))
599176, 598syl 17 . . . . . . . . 9 (𝜑 → (𝐹 ↾ (-∞(,)𝑋)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)))
600181ineq2d 4195 . . . . . . . . . 10 (𝜑 → ((-∞(,)𝑋) ∩ dom 𝐹) = ((-∞(,)𝑋) ∩ 𝐷))
601600reseq2d 5966 . . . . . . . . 9 (𝜑 → (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)))
602599, 601eqtrd 2770 . . . . . . . 8 (𝜑 → (𝐹 ↾ (-∞(,)𝑋)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)))
603602oveq1d 7420 . . . . . . 7 (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) lim 𝑋))
6046033ad2ant1 1133 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) lim 𝑋))
605 inss2 4213 . . . . . . . . . 10 ((-∞(,)𝑋) ∩ 𝐷) ⊆ 𝐷
606605a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)𝑋) ∩ 𝐷) ⊆ 𝐷)
607190, 606fssresd 6745 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)):((-∞(,)𝑋) ∩ 𝐷)⟶ℂ)
608449mnfltd 13140 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ < ((𝑄𝑖) − (𝑍𝑋)))
609195, 450, 608xrltled 13166 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ≤ ((𝑄𝑖) − (𝑍𝑋)))
610 iooss1 13397 . . . . . . . . . . 11 ((-∞ ∈ ℝ* ∧ -∞ ≤ ((𝑄𝑖) − (𝑍𝑋))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ (-∞(,)𝑋))
611194, 609, 610sylancr 587 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ (-∞(,)𝑋))
6126113adant3 1132 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ (-∞(,)𝑋))
613612, 500ssind 4216 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ ((-∞(,)𝑋) ∩ 𝐷))
614605, 231sstrid 3970 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)𝑋) ∩ 𝐷) ⊆ ℂ)
615 eqid 2735 . . . . . . . 8 ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) = ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
6164503adant3 1132 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
6174523ad2ant1 1133 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ*)
6184723ad2ant1 1133 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
619238, 618breqtrd 5145 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝑋 + (𝑍𝑋)))
6204083ad2ant1 1133 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑍𝑋) ∈ ℝ)
621143ad2ant1 1133 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
622211, 620, 621ltsubaddd 11833 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋)) < 𝑋 ↔ (𝑄𝑖) < (𝑋 + (𝑍𝑋))))
623619, 622mpbird 257 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑋)
62414leidd 11803 . . . . . . . . . . 11 (𝜑𝑋𝑋)
6256243ad2ant1 1133 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋𝑋)
626616, 617, 617, 623, 625eliocd 45536 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
627 ioounsn 13494 . . . . . . . . . . . 12 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ* ∧ ((𝑄𝑖) − (𝑍𝑋)) < 𝑋) → ((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋}) = (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
628616, 617, 623, 627syl3anc 1373 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋}) = (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
629628fveq2d 6880 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋})) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘(((𝑄𝑖) − (𝑍𝑋))(,]𝑋)))
630 ovex 7438 . . . . . . . . . . . . . 14 (-∞(,)𝑋) ∈ V
631630inex1 5287 . . . . . . . . . . . . 13 ((-∞(,)𝑋) ∩ 𝐷) ∈ V
632 snex 5406 . . . . . . . . . . . . 13 {𝑋} ∈ V
633631, 632unex 7738 . . . . . . . . . . . 12 (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V
634 resttop 23098 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ∈ Top ∧ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V) → ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ Top)
635244, 633, 634mp2an 692 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ Top
636633a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V)
637 iooretop 24704 . . . . . . . . . . . . . 14 (((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∈ (topGen‘ran (,))
638637a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∈ (topGen‘ran (,)))
639 elrestr 17442 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ∈ Top ∧ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V ∧ (((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∈ (topGen‘ran (,))) → ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
640252, 636, 638, 639syl3anc 1373 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
641450adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
642259a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → +∞ ∈ ℝ*)
64314ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑋 ∈ ℝ)
644 iocssre 13444 . . . . . . . . . . . . . . . . . . 19 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ⊆ ℝ)
645641, 643, 644syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ⊆ ℝ)
646 simpr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
647645, 646sseldd 3959 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ ℝ)
648452ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑋 ∈ ℝ*)
649 iocgtlb 45531 . . . . . . . . . . . . . . . . . 18 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
650641, 648, 646, 649syl3anc 1373 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
651647ltpnfd 13137 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 < +∞)
652641, 642, 647, 650, 651eliood 45527 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞))
6536523adantl3 1169 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞))
654 eqvisset 3479 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑋𝑋 ∈ V)
655 snidg 4636 . . . . . . . . . . . . . . . . . . . 20 (𝑋 ∈ V → 𝑋 ∈ {𝑋})
656654, 655syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋𝑋 ∈ {𝑋})
657467, 656eqeltrd 2834 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋𝑥 ∈ {𝑋})
658 elun2 4158 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ {𝑋} → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
659657, 658syl 17 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
660659adantl 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ 𝑥 = 𝑋) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
661 simpll 766 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → (𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
662641adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
663452ad3antrrr 730 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑋 ∈ ℝ*)
664647adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ ℝ)
665650adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
66614ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑋 ∈ ℝ)
667 iocleub 45532 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥𝑋)
668641, 648, 646, 667syl3anc 1373 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥𝑋)
669668adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥𝑋)
670467eqcoms 2743 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 = 𝑥𝑥 = 𝑋)
671670necon3bi 2958 . . . . . . . . . . . . . . . . . . . . 21 𝑥 = 𝑋𝑋𝑥)
672671adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑋𝑥)
673664, 666, 669, 672leneltd 11389 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 < 𝑋)
674662, 663, 664, 665, 673eliood 45527 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
6756743adantll3 45066 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
676613sselda 3958 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷))
677 elun1 4157 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
678676, 677syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
679661, 675, 678syl2anc 584 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
680660, 679pm2.61dan 812 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
681653, 680elind 4175 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
682616adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
683617adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑋 ∈ ℝ*)
684 elinel1 4176 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞))
685 elioore 13392 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞) → 𝑥 ∈ ℝ)
686684, 685syl 17 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ ℝ)
687686rexrd 11285 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ ℝ*)
688687adantl 481 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ∈ ℝ*)
689450adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
690259a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → +∞ ∈ ℝ*)
691684adantl 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞))
692 ioogtlb 45524 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ* ∧ +∞ ∈ ℝ*𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
693689, 690, 691, 692syl3anc 1373 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
6946933adantl3 1169 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
695 elinel2 4177 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
696 elsni 4618 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {𝑋} → 𝑥 = 𝑋)
697696adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ {𝑋}) → 𝑥 = 𝑋)
698624adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ {𝑋}) → 𝑋𝑋)
699697, 698eqbrtrd 5141 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ {𝑋}) → 𝑥𝑋)
700699adantlr 715 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ 𝑥 ∈ {𝑋}) → 𝑥𝑋)
701 simpll 766 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝜑)
702 elunnel2 4130 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷))
703702adantll 714 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷))
704 elinel1 4176 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷) → 𝑥 ∈ (-∞(,)𝑋))
705703, 704syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ∈ (-∞(,)𝑋))
706 elioore 13392 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (-∞(,)𝑋) → 𝑥 ∈ ℝ)
707706adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑥 ∈ ℝ)
70814adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑋 ∈ ℝ)
709194a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → -∞ ∈ ℝ*)
710452adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑋 ∈ ℝ*)
711 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑥 ∈ (-∞(,)𝑋))
712 iooltub 45539 . . . . . . . . . . . . . . . . . . . . 21 ((-∞ ∈ ℝ*𝑋 ∈ ℝ*𝑥 ∈ (-∞(,)𝑋)) → 𝑥 < 𝑋)
713709, 710, 711, 712syl3anc 1373 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑥 < 𝑋)
714707, 708, 713ltled 11383 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑥𝑋)
715701, 705, 714syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥𝑋)
716700, 715pm2.61dan 812 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥𝑋)
717695, 716sylan2 593 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥𝑋)
7187173ad2antl1 1186 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥𝑋)
719682, 683, 688, 694, 718eliocd 45536 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
720681, 719impbida 800 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ↔ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))))
721720eqrdv 2733 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) = ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
722605, 229sstrid 3970 . . . . . . . . . . . . . . 15 (𝜑 → ((-∞(,)𝑋) ∩ 𝐷) ⊆ ℝ)
72314snssd 4785 . . . . . . . . . . . . . . 15 (𝜑 → {𝑋} ⊆ ℝ)
724722, 723unssd 4167 . . . . . . . . . . . . . 14 (𝜑 → (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ⊆ ℝ)
7257243ad2ant1 1133 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ⊆ ℝ)
726233, 366rerest 24743 . . . . . . . . . . . . 13 ((((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) = ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
727725, 726syl 17 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) = ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
728640, 721, 7273eltr4d 2849 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
729 isopn3i 23020 . . . . . . . . . . 11 ((((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ Top ∧ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘(((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) = (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
730635, 728, 729sylancr 587 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘(((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) = (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
731629, 730eqtr2d 2771 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋})))
732626, 731eleqtrd 2836 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋})))
733607, 613, 614, 233, 615, 732limcres 25839 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋) = ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) lim 𝑋))
734733eqcomd 2741 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) lim 𝑋) = (((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
735613resabs1d 5995 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) = (𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)))
736735oveq1d 7420 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
737604, 734, 7363eqtrrd 2775 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋))
738377, 596, 7373eqtrrd 2775 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)))
739738rexlimdv3a 3145 . . 3 (𝜑 → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋))))
740173, 739mpd 15 . 2 (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)))
7411203adant3 1132 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
7422183adant3 1132 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
743 fourierdlem49.l . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
7447433adant3 1132 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
745 eqid 2735 . . . . . . . 8 if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋))) = if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋)))
746 eqid 2735 . . . . . . . 8 ((TopOpen‘ℂfld) ↾t (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))})) = ((TopOpen‘ℂfld) ↾t (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))}))
747211, 209, 741, 742, 744, 211, 235, 238, 217, 745, 746fourierdlem33 46169 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋))) ∈ (((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
748217resabs1d 5995 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) = (𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))))
749748oveq1d 7420 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
750747, 749eleqtrd 2836 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋))) ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
751 ne0i 4316 . . . . . 6 (if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋))) ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅)
752750, 751syl 17 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅)
753377, 752eqnetrd 2999 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅)
754753rexlimdv3a 3145 . . 3 (𝜑 → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅))
755173, 754mpd 15 . 2 (𝜑 → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅)
756740, 755eqnetrd 2999 1 (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1540  wcel 2108  wne 2932  wral 3051  wrex 3060  {crab 3415  Vcvv 3459  cun 3924  cin 3925  wss 3926  c0 4308  ifcif 4500  {csn 4601   class class class wbr 5119  cmpt 5201  dom cdm 5654  ran crn 5655  cres 5656  Rel wrel 5659   Fn wfn 6526  wf 6527  cfv 6531  (class class class)co 7405  m cmap 8840  supcsup 9452  cc 11127  cr 11128  0cc0 11129  1c1 11130   + caddc 11132   · cmul 11134  +∞cpnf 11266  -∞cmnf 11267  *cxr 11268   < clt 11269  cle 11270  cmin 11466  -cneg 11467   / cdiv 11894  cn 12240  0cn0 12501  cz 12588  cuz 12852  (,)cioo 13362  (,]cioc 13363  [,]cicc 13365  ...cfz 13524  ..^cfzo 13671  cfl 13807  t crest 17434  TopOpenctopn 17435  topGenctg 17451  fldccnfld 21315  Topctop 22831  intcnt 22955  cnccncf 24820   lim climc 25815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-cnex 11185  ax-resscn 11186  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-mulcom 11193  ax-addass 11194  ax-mulass 11195  ax-distr 11196  ax-i2m1 11197  ax-1ne0 11198  ax-1rid 11199  ax-rnegex 11200  ax-rrecex 11201  ax-cnre 11202  ax-pre-lttri 11203  ax-pre-lttrn 11204  ax-pre-ltadd 11205  ax-pre-mulgt0 11206  ax-pre-sup 11207
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-tp 4606  df-op 4608  df-uni 4884  df-int 4923  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7362  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7862  df-1st 7988  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-er 8719  df-map 8842  df-pm 8843  df-en 8960  df-dom 8961  df-sdom 8962  df-fin 8963  df-fi 9423  df-sup 9454  df-inf 9455  df-pnf 11271  df-mnf 11272  df-xr 11273  df-ltxr 11274  df-le 11275  df-sub 11468  df-neg 11469  df-div 11895  df-nn 12241  df-2 12303  df-3 12304  df-4 12305  df-5 12306  df-6 12307  df-7 12308  df-8 12309  df-9 12310  df-n0 12502  df-z 12589  df-dec 12709  df-uz 12853  df-q 12965  df-rp 13009  df-xneg 13128  df-xadd 13129  df-xmul 13130  df-ioo 13366  df-ioc 13367  df-icc 13369  df-fz 13525  df-fzo 13672  df-fl 13809  df-seq 14020  df-exp 14080  df-cj 15118  df-re 15119  df-im 15120  df-sqrt 15254  df-abs 15255  df-struct 17166  df-slot 17201  df-ndx 17213  df-base 17229  df-plusg 17284  df-mulr 17285  df-starv 17286  df-tset 17290  df-ple 17291  df-ds 17293  df-unif 17294  df-rest 17436  df-topn 17437  df-topgen 17457  df-psmet 21307  df-xmet 21308  df-met 21309  df-bl 21310  df-mopn 21311  df-cnfld 21316  df-top 22832  df-topon 22849  df-topsp 22871  df-bases 22884  df-ntr 22958  df-cn 23165  df-cnp 23166  df-xms 24259  df-ms 24260  df-cncf 24822  df-limc 25819
This theorem is referenced by:  fourierdlem94  46229  fourierdlem113  46248
  Copyright terms: Public domain W3C validator