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 46341
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 7389 . . . . . . . . . 10 ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ V
7 fourierdlem49.z . . . . . . . . . . 11 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
87fvmpt2 6950 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ V) → (𝑍𝑥) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
96, 8mpan2 691 . . . . . . . . 9 (𝑥 ∈ ℝ → (𝑍𝑥) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
109oveq2d 7372 . . . . . . . 8 (𝑥 ∈ ℝ → (𝑥 + (𝑍𝑥)) = (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
1110mpteq2ia 5191 . . . . . . 7 (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
125, 11eqtri 2757 . . . . . 6 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
131, 2, 3, 4, 12fourierdlem4 46297 . . . . 5 (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))
14 fourierdlem49.x . . . . 5 (𝜑𝑋 ∈ ℝ)
1513, 14ffvelcdmd 7028 . . . 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 46295 . . . . . . . . . . . . . 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 8784 . . . . . . . . . . 11 (𝑄 ∈ (ℝ ↑m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
2523, 24syl 17 . . . . . . . . . 10 (𝜑𝑄:(0...𝑀)⟶ℝ)
26 ffn 6660 . . . . . . . . . 10 (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
2725, 26syl 17 . . . . . . . . 9 (𝜑𝑄 Fn (0...𝑀))
2827ad2antrr 726 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → 𝑄 Fn (0...𝑀))
29 fvelrnb 6892 . . . . . . . 8 (𝑄 Fn (0...𝑀) → ((𝐸𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋)))
3028, 29syl 17 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → ((𝐸𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋)))
3116, 30mpbid 232 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋))
32 1zzd 12520 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 1 ∈ ℤ)
33 elfzelz 13438 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
3433ad2antlr 727 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℤ)
35 1e0p1 12647 . . . . . . . . . . . . . . . . 17 1 = (0 + 1)
3635a1i 11 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 1 = (0 + 1))
3734zred 12594 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℝ)
38 elfzle1 13441 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
3938ad2antlr 727 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ≤ 𝑗)
40 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑄𝑗) = (𝐸𝑋) → (𝑄𝑗) = (𝐸𝑋))
4140eqcomd 2740 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑄𝑗) = (𝐸𝑋) → (𝐸𝑋) = (𝑄𝑗))
4241ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝐸𝑋) = (𝑄𝑗))
43 fveq2 6832 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = 0 → (𝑄𝑗) = (𝑄‘0))
4443adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝑄𝑗) = (𝑄‘0))
4522simprld 771 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵))
4645simpld 494 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑄‘0) = 𝐴)
4746ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝑄‘0) = 𝐴)
4842, 44, 473eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝐸𝑋) = 𝐴)
4948adantllr 719 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝐸𝑋) = 𝐴)
5049adantllr 719 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝐸𝑋) = 𝐴)
511adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 ∈ ℝ)
521rexrd 11180 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐴 ∈ ℝ*)
5352adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 ∈ ℝ*)
542rexrd 11180 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐵 ∈ ℝ*)
5554adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐵 ∈ ℝ*)
56 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ∈ (𝐴(,]𝐵))
57 iocgtlb 45690 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸𝑋))
5853, 55, 56, 57syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸𝑋))
5951, 58gtned 11266 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ≠ 𝐴)
6059neneqd 2935 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → ¬ (𝐸𝑋) = 𝐴)
6160ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → ¬ (𝐸𝑋) = 𝐴)
6250, 61pm2.65da 816 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → ¬ 𝑗 = 0)
6362neqned 2937 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ≠ 0)
6437, 39, 63ne0gt0d 11268 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 < 𝑗)
65 0zd 12498 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ∈ ℤ)
66 zltp1le 12539 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
6765, 34, 66syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
6864, 67mpbid 232 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 + 1) ≤ 𝑗)
6936, 68eqbrtrd 5118 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 1 ≤ 𝑗)
70 eluz2 12755 . . . . . . . . . . . . . . 15 (𝑗 ∈ (ℤ‘1) ↔ (1 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗))
7132, 34, 69, 70syl3anbrc 1344 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ (ℤ‘1))
72 nnuz 12788 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
7371, 72eleqtrrdi 2845 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℕ)
74 nnm1nn0 12440 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ → (𝑗 − 1) ∈ ℕ0)
7573, 74syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ ℕ0)
76 nn0uz 12787 . . . . . . . . . . . . 13 0 = (ℤ‘0)
7776a1i 11 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → ℕ0 = (ℤ‘0))
7875, 77eleqtrd 2836 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (ℤ‘0))
7918nnzd 12512 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℤ)
8079ad3antrrr 730 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑀 ∈ ℤ)
81 peano2zm 12532 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℤ → (𝑗 − 1) ∈ ℤ)
8233, 81syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℤ)
8382zred 12594 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
8433zred 12594 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
85 elfzel2 13436 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
8685zred 12594 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
8784ltm1d 12072 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑗)
88 elfzle2 13442 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗𝑀)
8983, 84, 86, 87, 88ltletrd 11291 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
9089ad2antlr 727 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) < 𝑀)
91 elfzo2 13576 . . . . . . . . . . 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 12463 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ≤ (𝑗 − 1))
9683, 86, 89ltled 11279 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ≤ 𝑀)
9796ad2antlr 727 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ≤ 𝑀)
9865, 80, 94, 95, 97elfzd 13429 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (0...𝑀))
9993, 98ffvelcdmd 7028 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ)
10099rexrd 11180 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ*)
10125ffvelcdmda 7027 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ)
102101rexrd 11180 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ*)
103102adantlr 715 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ*)
104103adantr 480 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ∈ ℝ*)
105 iocssre 13341 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
10652, 2, 105syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
107106sselda 3931 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ∈ ℝ)
108107rexrd 11180 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ∈ ℝ*)
109108ad2antrr 726 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ*)
110 simplll 774 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝜑)
111 ovex 7389 . . . . . . . . . . . . . . . 16 (𝑗 − 1) ∈ V
112 eleq1 2822 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 − 1) → (𝑖 ∈ (0..^𝑀) ↔ (𝑗 − 1) ∈ (0..^𝑀)))
113112anbi2d 630 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 − 1) → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀))))
114 fveq2 6832 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 − 1) → (𝑄𝑖) = (𝑄‘(𝑗 − 1)))
115 oveq1 7363 . . . . . . . . . . . . . . . . . . 19 (𝑖 = (𝑗 − 1) → (𝑖 + 1) = ((𝑗 − 1) + 1))
116115fveq2d 6836 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 − 1) → (𝑄‘(𝑖 + 1)) = (𝑄‘((𝑗 − 1) + 1)))
117114, 116breq12d 5109 . . . . . . . . . . . . . . . . 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 3226 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
121111, 118, 120vtocl 3513 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
122110, 92, 121syl2anc 584 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
12333zcnd 12595 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
124 1cnd 11125 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 1 ∈ ℂ)
125123, 124npcand 11494 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → ((𝑗 − 1) + 1) = 𝑗)
126125eqcomd 2740 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → 𝑗 = ((𝑗 − 1) + 1))
127126fveq2d 6836 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → (𝑄𝑗) = (𝑄‘((𝑗 − 1) + 1)))
128127eqcomd 2740 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
129128ad2antlr 727 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
130122, 129breqtrd 5122 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄𝑗))
131 simpr 484 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) = (𝐸𝑋))
132130, 131breqtrd 5122 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝐸𝑋))
133106, 15sseldd 3932 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸𝑋) ∈ ℝ)
134133leidd 11701 . . . . . . . . . . . . . . 15 (𝜑 → (𝐸𝑋) ≤ (𝐸𝑋))
135134ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝐸𝑋))
13641adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) = (𝑄𝑗))
137135, 136breqtrd 5122 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄𝑗))
138137adantllr 719 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄𝑗))
139100, 104, 109, 132, 138eliocd 45695 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄𝑗)))
140127oveq2d 7372 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → ((𝑄‘(𝑗 − 1))(,](𝑄𝑗)) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
141140ad2antlr 727 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → ((𝑄‘(𝑗 − 1))(,](𝑄𝑗)) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
142139, 141eleqtrd 2836 . . . . . . . . . 10 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
143114, 116oveq12d 7374 . . . . . . . . . . . 12 (𝑖 = (𝑗 − 1) → ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
144143eleq2d 2820 . . . . . . . . . . 11 (𝑖 = (𝑗 − 1) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) ↔ (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))))
145144rspcev 3574 . . . . . . . . . 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 3135 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
15031, 149mpd 15 . . . . 5 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
15118ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → 𝑀 ∈ ℕ)
15225ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ)
153 iocssicc 13351 . . . . . . . . . 10 (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵)
15446eqcomd 2740 . . . . . . . . . . 11 (𝜑𝐴 = (𝑄‘0))
15545simprd 495 . . . . . . . . . . . 12 (𝜑 → (𝑄𝑀) = 𝐵)
156155eqcomd 2740 . . . . . . . . . . 11 (𝜑𝐵 = (𝑄𝑀))
157154, 156oveq12d 7374 . . . . . . . . . 10 (𝜑 → (𝐴[,]𝐵) = ((𝑄‘0)[,](𝑄𝑀)))
158153, 157sseqtrid 3974 . . . . . . . . 9 (𝜑 → (𝐴(,]𝐵) ⊆ ((𝑄‘0)[,](𝑄𝑀)))
159158sselda 3931 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ∈ ((𝑄‘0)[,](𝑄𝑀)))
160159adantr 480 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (𝐸𝑋) ∈ ((𝑄‘0)[,](𝑄𝑀)))
161 simpr 484 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ¬ (𝐸𝑋) ∈ ran 𝑄)
162 fveq2 6832 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝑄𝑘) = (𝑄𝑗))
163162breq1d 5106 . . . . . . . . 9 (𝑘 = 𝑗 → ((𝑄𝑘) < (𝐸𝑋) ↔ (𝑄𝑗) < (𝐸𝑋)))
164163cbvrabv 3407 . . . . . . . 8 {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < (𝐸𝑋)} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < (𝐸𝑋)}
165164supeq1i 9348 . . . . . . 7 sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < (𝐸𝑋)}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < (𝐸𝑋)}, ℝ, < )
166151, 152, 160, 161, 165fourierdlem25 46318 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
167 ioossioc 45680 . . . . . . . . 9 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))
168167sseli 3927 . . . . . . . 8 ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
169168a1i 11 . . . . . . 7 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
170169reximdva 3147 . . . . . 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 6665 . . . . . . . . . . 11 (𝐹:𝐷⟶ℝ → Rel 𝐹)
176174, 175syl 17 . . . . . . . . . 10 (𝜑 → Rel 𝐹)
177 resindm 5987 . . . . . . . . . . 11 (Rel 𝐹 → (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹)) = (𝐹 ↾ (-∞(,)(𝐸𝑋))))
178177eqcomd 2740 . . . . . . . . . 10 (Rel 𝐹 → (𝐹 ↾ (-∞(,)(𝐸𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹)))
179176, 178syl 17 . . . . . . . . 9 (𝜑 → (𝐹 ↾ (-∞(,)(𝐸𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹)))
180 fdm 6669 . . . . . . . . . . . 12 (𝐹:𝐷⟶ℝ → dom 𝐹 = 𝐷)
181174, 180syl 17 . . . . . . . . . . 11 (𝜑 → dom 𝐹 = 𝐷)
182181ineq2d 4170 . . . . . . . . . 10 (𝜑 → ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹) = ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
183182reseq2d 5936 . . . . . . . . 9 (𝜑 → (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹)) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)))
184179, 183eqtrd 2769 . . . . . . . 8 (𝜑 → (𝐹 ↾ (-∞(,)(𝐸𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)))
1851843ad2ant1 1133 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ (-∞(,)(𝐸𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)))
186185oveq1d 7371 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) lim (𝐸𝑋)))
187 ax-resscn 11081 . . . . . . . . . . 11 ℝ ⊆ ℂ
188187a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ⊆ ℂ)
189174, 188fssd 6677 . . . . . . . . 9 (𝜑𝐹:𝐷⟶ℂ)
1901893ad2ant1 1133 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐹:𝐷⟶ℂ)
191 inss2 4188 . . . . . . . . 9 ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ 𝐷
192191a1i 11 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ 𝐷)
193190, 192fssresd 6699 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)):((-∞(,)(𝐸𝑋)) ∩ 𝐷)⟶ℂ)
194 mnfxr 11187 . . . . . . . . . 10 -∞ ∈ ℝ*
195194a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ∈ ℝ*)
19625adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
197 elfzofz 13589 . . . . . . . . . . . . . 14 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
198197adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
199196, 198ffvelcdmd 7028 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
200199rexrd 11180 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ*)
201199mnfltd 13036 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ < (𝑄𝑖))
202195, 200, 201xrltled 13062 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ≤ (𝑄𝑖))
203 iooss1 13294 . . . . . . . . . 10 ((-∞ ∈ ℝ* ∧ -∞ ≤ (𝑄𝑖)) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ (-∞(,)(𝐸𝑋)))
204194, 202, 203sylancr 587 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ (-∞(,)(𝐸𝑋)))
2052043adant3 1132 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ (-∞(,)(𝐸𝑋)))
206 fzofzp1 13678 . . . . . . . . . . . . . 14 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
207206adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
208196, 207ffvelcdmd 7028 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
2092083adant3 1132 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
210209rexrd 11180 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
2111993adant3 1132 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
212211rexrd 11180 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ*)
213 simp3 1138 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
214 iocleub 45691 . . . . . . . . . . 11 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
215212, 210, 213, 214syl3anc 1373 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
216 iooss2 13295 . . . . . . . . . 10 (((𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
217210, 215, 216syl2anc 584 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
218 fourierdlem49.cn . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
219 cncff 24840 . . . . . . . . . . . . 13 ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
220 fdm 6669 . . . . . . . . . . . . 13 ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ → dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
221218, 219, 2203syl 18 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
222 ssdmres 5970 . . . . . . . . . . . 12 (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹 ↔ dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
223221, 222sylibr 234 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹)
224181adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → dom 𝐹 = 𝐷)
225223, 224sseqtrd 3968 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
2262253adant3 1132 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
227217, 226sstrd 3942 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ 𝐷)
228205, 227ssind 4191 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
229 fourierdlem49.d . . . . . . . . . 10 (𝜑𝐷 ⊆ ℝ)
230229, 188sstrd 3942 . . . . . . . . 9 (𝜑𝐷 ⊆ ℂ)
2312303ad2ant1 1133 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐷 ⊆ ℂ)
232191, 231sstrid 3943 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ ℂ)
233 eqid 2734 . . . . . . 7 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
234 eqid 2734 . . . . . . 7 ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) = ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
2351333ad2ant1 1133 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ℝ)
236235rexrd 11180 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ℝ*)
237 iocgtlb 45690 . . . . . . . . . 10 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝐸𝑋))
238212, 210, 213, 237syl3anc 1373 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝐸𝑋))
239235leidd 11701 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝐸𝑋))
240212, 236, 236, 238, 239eliocd 45695 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝐸𝑋)))
241 ioounsn 13391 . . . . . . . . . . 11 (((𝑄𝑖) ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ* ∧ (𝑄𝑖) < (𝐸𝑋)) → (((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)}) = ((𝑄𝑖)(,](𝐸𝑋)))
242212, 236, 238, 241syl3anc 1373 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)}) = ((𝑄𝑖)(,](𝐸𝑋)))
243242fveq2d 6836 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘(((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)})) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘((𝑄𝑖)(,](𝐸𝑋))))
244233cnfldtop 24725 . . . . . . . . . . 11 (TopOpen‘ℂfld) ∈ Top
245 ovex 7389 . . . . . . . . . . . . 13 (-∞(,)(𝐸𝑋)) ∈ V
246245inex1 5260 . . . . . . . . . . . 12 ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∈ V
247 snex 5379 . . . . . . . . . . . 12 {(𝐸𝑋)} ∈ V
248246, 247unex 7687 . . . . . . . . . . 11 (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∈ V
249 resttop 23102 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ∈ Top ∧ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∈ V) → ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ Top)
250244, 248, 249mp2an 692 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ Top
251 retop 24703 . . . . . . . . . . . . 13 (topGen‘ran (,)) ∈ Top
252251a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (topGen‘ran (,)) ∈ Top)
253248a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∈ V)
254 iooretop 24707 . . . . . . . . . . . . 13 ((𝑄𝑖)(,)+∞) ∈ (topGen‘ran (,))
255254a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)+∞) ∈ (topGen‘ran (,)))
256 elrestr 17346 . . . . . . . . . . . 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 11184 . . . . . . . . . . . . . . . . . . . 20 +∞ ∈ ℝ*
260259a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → +∞ ∈ ℝ*)
261235ltpnfd 13033 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) < +∞)
262212, 260, 235, 238, 261eliood 45686 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,)+∞))
263 snidg 4615 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸𝑋) ∈ ℝ → (𝐸𝑋) ∈ {(𝐸𝑋)})
264 elun2 4133 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸𝑋) ∈ {(𝐸𝑋)} → (𝐸𝑋) ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
265263, 264syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝐸𝑋) ∈ ℝ → (𝐸𝑋) ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
266133, 265syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐸𝑋) ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
2672663ad2ant1 1133 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
268262, 267elind 4150 . . . . . . . . . . . . . . . . 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 13341 . . . . . . . . . . . . . . . . . . . 20 (((𝑄𝑖) ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ) → ((𝑄𝑖)(,](𝐸𝑋)) ⊆ ℝ)
278274, 276, 277syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → ((𝑄𝑖)(,](𝐸𝑋)) ⊆ ℝ)
279 simpr 484 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋)))
280278, 279sseldd 3932 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ ℝ)
2812803adantl3 1169 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ ℝ)
282276rexrd 11180 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝐸𝑋) ∈ ℝ*)
283 iocgtlb 45690 . . . . . . . . . . . . . . . . . . 19 (((𝑄𝑖) ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ*𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝑄𝑖) < 𝑥)
284274, 282, 279, 283syl3anc 1373 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝑄𝑖) < 𝑥)
2852843adantl3 1169 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝑄𝑖) < 𝑥)
286281ltpnfd 13033 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 < +∞)
287272, 273, 281, 285, 286eliood 45686 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ ((𝑄𝑖)(,)+∞))
288287adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ((𝑄𝑖)(,)+∞))
289194a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → -∞ ∈ ℝ*)
290282adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ*)
291280adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ℝ)
292291mnfltd 13036 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → -∞ < 𝑥)
293133ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ)
294 iocleub 45691 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑄𝑖) ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ*𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ≤ (𝐸𝑋))
295274, 282, 279, 294syl3anc 1373 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ≤ (𝐸𝑋))
296295adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ≤ (𝐸𝑋))
297 neqne 2938 . . . . . . . . . . . . . . . . . . . . . 22 𝑥 = (𝐸𝑋) → 𝑥 ≠ (𝐸𝑋))
298297necomd 2985 . . . . . . . . . . . . . . . . . . . . 21 𝑥 = (𝐸𝑋) → (𝐸𝑋) ≠ 𝑥)
299298adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ≠ 𝑥)
300291, 293, 296, 299leneltd 11285 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 < (𝐸𝑋))
301289, 290, 291, 292, 300eliood 45686 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (-∞(,)(𝐸𝑋)))
3023013adantll3 45229 . . . . . . . . . . . . . . . . 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 45229 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 < (𝐸𝑋))
311215ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
312306, 308, 309, 310, 311ltletrd 11291 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 < (𝑄‘(𝑖 + 1)))
313304, 305, 306, 307, 312eliood 45686 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
314303, 313sseldd 3932 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥𝐷)
315302, 314elind 4150 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
316 elun1 4132 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷) → 𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
317315, 316syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
318288, 317elind 4150 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
319271, 318pm2.61dan 812 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
320212adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝑄𝑖) ∈ ℝ*)
321236adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝐸𝑋) ∈ ℝ*)
322 elinel1 4151 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ∈ ((𝑄𝑖)(,)+∞))
323 elioore 13289 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((𝑄𝑖)(,)+∞) → 𝑥 ∈ ℝ)
324323rexrd 11180 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((𝑄𝑖)(,)+∞) → 𝑥 ∈ ℝ*)
325322, 324syl 17 . . . . . . . . . . . . . . 15 (𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ∈ ℝ*)
326325adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ∈ ℝ*)
327200adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝑄𝑖) ∈ ℝ*)
328259a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → +∞ ∈ ℝ*)
329322adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ∈ ((𝑄𝑖)(,)+∞))
330 ioogtlb 45683 . . . . . . . . . . . . . . . 16 (((𝑄𝑖) ∈ ℝ* ∧ +∞ ∈ ℝ*𝑥 ∈ ((𝑄𝑖)(,)+∞)) → (𝑄𝑖) < 𝑥)
331327, 328, 329, 330syl3anc 1373 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝑄𝑖) < 𝑥)
3323313adantl3 1169 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝑄𝑖) < 𝑥)
333 elinel2 4152 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
334 elsni 4595 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {(𝐸𝑋)} → 𝑥 = (𝐸𝑋))
335334adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ {(𝐸𝑋)}) → 𝑥 = (𝐸𝑋))
336134adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ {(𝐸𝑋)}) → (𝐸𝑋) ≤ (𝐸𝑋))
337335, 336eqbrtrd 5118 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ≤ (𝐸𝑋))
338337adantlr 715 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∧ 𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ≤ (𝐸𝑋))
339 simpll 766 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∧ ¬ 𝑥 ∈ {(𝐸𝑋)}) → 𝜑)
340 elunnel2 4105 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∧ ¬ 𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
341340adantll 714 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∧ ¬ 𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
342 elinel1 4151 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷) → 𝑥 ∈ (-∞(,)(𝐸𝑋)))
343 elioore 13289 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (-∞(,)(𝐸𝑋)) → 𝑥 ∈ ℝ)
344343adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 ∈ ℝ)
345133adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → (𝐸𝑋) ∈ ℝ)
346194a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → -∞ ∈ ℝ*)
347345rexrd 11180 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → (𝐸𝑋) ∈ ℝ*)
348 simpr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 ∈ (-∞(,)(𝐸𝑋)))
349 iooltub 45698 . . . . . . . . . . . . . . . . . . . . . 22 ((-∞ ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ*𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 < (𝐸𝑋))
350346, 347, 348, 349syl3anc 1373 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 < (𝐸𝑋))
351344, 345, 350ltled 11279 . . . . . . . . . . . . . . . . . . . 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 45695 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋)))
359319, 358impbida 800 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋)) ↔ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))))
360359eqrdv 2732 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,](𝐸𝑋)) = (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
361 ioossre 13321 . . . . . . . . . . . . . 14 (-∞(,)(𝐸𝑋)) ⊆ ℝ
362 ssinss1 4196 . . . . . . . . . . . . . 14 ((-∞(,)(𝐸𝑋)) ⊆ ℝ → ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ ℝ)
363361, 362mp1i 13 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ ℝ)
364235snssd 4763 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {(𝐸𝑋)} ⊆ ℝ)
365363, 364unssd 4142 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ⊆ ℝ)
366 eqid 2734 . . . . . . . . . . . . 13 (topGen‘ran (,)) = (topGen‘ran (,))
367233, 366rerest 24746 . . . . . . . . . . . 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 23024 . . . . . . . . . 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 2770 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,](𝐸𝑋)) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘(((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)})))
373240, 372eleqtrd 2836 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘(((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)})))
374193, 228, 232, 233, 234, 373limcres 25841 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) lim (𝐸𝑋)))
375228resabs1d 5965 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) = (𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))))
376375oveq1d 7371 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
377186, 374, 3763eqtr2d 2775 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
378181feq2d 6644 . . . . . . . . . . . 12 (𝜑 → (𝐹:dom 𝐹⟶ℂ ↔ 𝐹:𝐷⟶ℂ))
379189, 378mpbird 257 . . . . . . . . . . 11 (𝜑𝐹:dom 𝐹⟶ℂ)
380379adantr 480 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝐹:dom 𝐹⟶ℂ)
3813803ad2antl1 1186 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝐹:dom 𝐹⟶ℂ)
382 ioosscn 13322 . . . . . . . . . 10 ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ℂ
383382a1i 11 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ℂ)
384181eqcomd 2740 . . . . . . . . . . . 12 (𝜑𝐷 = dom 𝐹)
3853843ad2ant1 1133 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐷 = dom 𝐹)
386227, 385sseqtrd 3968 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ dom 𝐹)
387386adantr 480 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ dom 𝐹)
3887a1i 11 . . . . . . . . . . . . . . 15 (𝜑𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
389 oveq2 7364 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋 → (𝐵𝑥) = (𝐵𝑋))
390389oveq1d 7371 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋 → ((𝐵𝑥) / 𝑇) = ((𝐵𝑋) / 𝑇))
391390fveq2d 6836 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋 → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵𝑋) / 𝑇)))
392391oveq1d 7371 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
393392adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑥 = 𝑋) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
3942, 14resubcld 11563 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵𝑋) ∈ ℝ)
3952, 1resubcld 11563 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐵𝐴) ∈ ℝ)
3964, 395eqeltrid 2838 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑇 ∈ ℝ)
3971, 2posdifd 11722 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
3983, 397mpbid 232 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 < (𝐵𝐴))
3994eqcomi 2743 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵𝐴) = 𝑇
400399a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵𝐴) = 𝑇)
401398, 400breqtrd 5122 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 < 𝑇)
402401gt0ne0d 11699 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑇 ≠ 0)
403394, 396, 402redivcld 11967 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵𝑋) / 𝑇) ∈ ℝ)
404403flcld 13716 . . . . . . . . . . . . . . . . 17 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
405404zred 12594 . . . . . . . . . . . . . . . 16 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℝ)
406405, 396remulcld 11160 . . . . . . . . . . . . . . 15 (𝜑 → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
407388, 393, 14, 406fvmptd 6946 . . . . . . . . . . . . . 14 (𝜑 → (𝑍𝑋) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
408407, 406eqeltrd 2834 . . . . . . . . . . . . 13 (𝜑 → (𝑍𝑋) ∈ ℝ)
409408recnd 11158 . . . . . . . . . . . 12 (𝜑 → (𝑍𝑋) ∈ ℂ)
410409adantr 480 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → (𝑍𝑋) ∈ ℂ)
4114103ad2antl1 1186 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → (𝑍𝑋) ∈ ℂ)
412411negcld 11477 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → -(𝑍𝑋) ∈ ℂ)
413 eqid 2734 . . . . . . . . 9 {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}
414 ioosscn 13322 . . . . . . . . . . . . . . . . . . 19 (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ ℂ
415414sseli 3927 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) → 𝑦 ∈ ℂ)
416415adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℂ)
417409adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℂ)
418416, 417pncand 11491 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = 𝑦)
419418eqcomd 2740 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)))
4204193ad2antl1 1186 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)))
421407oveq2d 7372 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = ((𝑦 + (𝑍𝑋)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
422421adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = ((𝑦 + (𝑍𝑋)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
423416, 417addcld 11149 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℂ)
424406recnd 11158 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
425424adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
426423, 425negsubd 11496 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + (𝑍𝑋)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
427404zcnd 12595 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℂ)
428396recnd 11158 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑇 ∈ ℂ)
429427, 428mulneg1d 11588 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
430429eqcomd 2740 . . . . . . . . . . . . . . . . . . 19 (𝜑 → -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
431430oveq2d 7372 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑦 + (𝑍𝑋)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
432431adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
433422, 426, 4323eqtr2d 2775 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
4344333ad2antl1 1186 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
435404znegcld 12596 . . . . . . . . . . . . . . . . . 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 11180 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐸𝑋) ∈ ℝ*)
442441ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐸𝑋) ∈ ℝ*)
443 elioore 13289 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) → 𝑦 ∈ ℝ)
444443adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
445408adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℝ)
446444, 445readdcld 11159 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
447446adantlr 715 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
448408adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑍𝑋) ∈ ℝ)
449199, 448resubcld 11563 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ)
450449rexrd 11180 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
451450adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
45214rexrd 11180 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑋 ∈ ℝ*)
453452ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑋 ∈ ℝ*)
454 simpr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
455 ioogtlb 45683 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑦)
456451, 453, 454, 455syl3anc 1373 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑦)
457199adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) ∈ ℝ)
458448adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℝ)
459443adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
460457, 458, 459ltsubaddd 11731 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (((𝑄𝑖) − (𝑍𝑋)) < 𝑦 ↔ (𝑄𝑖) < (𝑦 + (𝑍𝑋))))
461456, 460mpbid 232 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) < (𝑦 + (𝑍𝑋)))
46214ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑋 ∈ ℝ)
463 iooltub 45698 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 < 𝑋)
464451, 453, 454, 463syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 < 𝑋)
465459, 462, 458, 464ltadd1dd 11746 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝑋 + (𝑍𝑋)))
4665a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥))))
467 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑋𝑥 = 𝑋)
468 fveq2 6832 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑋 → (𝑍𝑥) = (𝑍𝑋))
469467, 468oveq12d 7374 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑋 → (𝑥 + (𝑍𝑥)) = (𝑋 + (𝑍𝑋)))
470469adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 = 𝑋) → (𝑥 + (𝑍𝑥)) = (𝑋 + (𝑍𝑋)))
47114, 408readdcld 11159 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑋 + (𝑍𝑋)) ∈ ℝ)
472466, 470, 14, 471fvmptd 6946 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
473472eqcomd 2740 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
474473ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
475465, 474breqtrd 5122 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝐸𝑋))
476440, 442, 447, 461, 475eliood 45686 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ((𝑄𝑖)(,)(𝐸𝑋)))
4774763adantl3 1169 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ((𝑄𝑖)(,)(𝐸𝑋)))
478439, 477sseldd 3932 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ 𝐷)
479438, 478, 4373jca 1128 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
480 eleq1 2822 . . . . . . . . . . . . . . . . . . 19 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
4814803anbi3d 1444 . . . . . . . . . . . . . . . . . 18 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)))
482 oveq1 7363 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 · 𝑇) = (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
483482oveq2d 7372 . . . . . . . . . . . . . . . . . . 19 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
484483eleq1d 2819 . . . . . . . . . . . . . . . . . 18 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
485481, 484imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)))
486 ovex 7389 . . . . . . . . . . . . . . . . . 18 (𝑦 + (𝑍𝑋)) ∈ V
487 eleq1 2822 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑦 + (𝑍𝑋)) → (𝑥𝐷 ↔ (𝑦 + (𝑍𝑋)) ∈ 𝐷))
4884873anbi2d 1443 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑦 + (𝑍𝑋)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ)))
489 oveq1 7363 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑦 + (𝑍𝑋)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)))
490489eleq1d 2819 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑦 + (𝑍𝑋)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷))
491488, 490imbi12d 344 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑦 + (𝑍𝑋)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)))
492 fourierdlem49.dper . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)
493486, 491, 492vtocl 3513 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)
494485, 493vtoclg 3509 . . . . . . . . . . . . . . . 16 (-(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ → ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
495437, 479, 494sylc 65 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
496434, 495eqeltrd 2834 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) ∈ 𝐷)
497420, 496eqeltrd 2834 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦𝐷)
498497ralrimiva 3126 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑦𝐷)
499 dfss3 3920 . . . . . . . . . . . 12 ((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷 ↔ ∀𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑦𝐷)
500498, 499sylibr 234 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷)
501199recnd 11158 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℂ)
502409adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑍𝑋) ∈ ℂ)
503501, 502negsubd 11496 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + -(𝑍𝑋)) = ((𝑄𝑖) − (𝑍𝑋)))
504503eqcomd 2740 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) = ((𝑄𝑖) + -(𝑍𝑋)))
505472oveq1d 7371 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸𝑋) + -(𝑍𝑋)) = ((𝑋 + (𝑍𝑋)) + -(𝑍𝑋)))
506471recnd 11158 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑋 + (𝑍𝑋)) ∈ ℂ)
507506, 409negsubd 11496 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑋 + (𝑍𝑋)) + -(𝑍𝑋)) = ((𝑋 + (𝑍𝑋)) − (𝑍𝑋)))
50814recnd 11158 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 ∈ ℂ)
509508, 409pncand 11491 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑋 + (𝑍𝑋)) − (𝑍𝑋)) = 𝑋)
510505, 507, 5093eqtrrd 2774 . . . . . . . . . . . . . . 15 (𝜑𝑋 = ((𝐸𝑋) + -(𝑍𝑋)))
511510adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 = ((𝐸𝑋) + -(𝑍𝑋)))
512504, 511oveq12d 7374 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) = (((𝑄𝑖) + -(𝑍𝑋))(,)((𝐸𝑋) + -(𝑍𝑋))))
513448renegcld 11562 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → -(𝑍𝑋) ∈ ℝ)
514199, 275, 513iooshift 45710 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) + -(𝑍𝑋))(,)((𝐸𝑋) + -(𝑍𝑋))) = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))})
515512, 514eqtr2d 2770 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} = (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
5165153adant3 1132 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} = (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
5171813ad2ant1 1133 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → dom 𝐹 = 𝐷)
518500, 516, 5173sstr4d 3987 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} ⊆ dom 𝐹)
519518adantr 480 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} ⊆ dom 𝐹)
520407negeqd 11372 . . . . . . . . . . . . . . . 16 (𝜑 → -(𝑍𝑋) = -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
521520, 430eqtrd 2769 . . . . . . . . . . . . . . 15 (𝜑 → -(𝑍𝑋) = (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
522521oveq2d 7372 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 + -(𝑍𝑋)) = (𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
523522fveq2d 6836 . . . . . . . . . . . . 13 (𝜑 → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
524523adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
5255243ad2antl1 1186 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
526435adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
5275263ad2antl1 1186 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
528 simpl1 1192 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → 𝜑)
529227sselda 3931 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → 𝑥𝐷)
530528, 529, 5273jca 1128 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝜑𝑥𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
5314803anbi3d 1444 . . . . . . . . . . . . . 14 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑𝑥𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)))
532482oveq2d 7372 . . . . . . . . . . . . . . . 16 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = (𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
533532fveq2d 6836 . . . . . . . . . . . . . . 15 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
534533eqeq1d 2736 . . . . . . . . . . . . . 14 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥) ↔ (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
535531, 534imbi12d 344 . . . . . . . . . . . . 13 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥)) ↔ ((𝜑𝑥𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥))))
536 fourierdlem49.per . . . . . . . . . . . . 13 ((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥))
537535, 536vtoclg 3509 . . . . . . . . . . . 12 (-(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ → ((𝜑𝑥𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
538527, 530, 537sylc 65 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥))
539525, 538eqtrd 2769 . . . . . . . . . 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 45816 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝑦 ∈ ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) lim ((𝐸𝑋) + -(𝑍𝑋))))
543515reseq2d 5936 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) = (𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)))
544511eqcomd 2740 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) + -(𝑍𝑋)) = 𝑋)
545543, 544oveq12d 7374 . . . . . . . . . 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 3969 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ dom 𝐹)
553552adantr 480 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ dom 𝐹)
554409adantr 480 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → (𝑍𝑋) ∈ ℂ)
5555543ad2antl1 1186 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → (𝑍𝑋) ∈ ℂ)
556 eqid 2734 . . . . . . . . 9 {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}
557501, 502npcand 11494 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) − (𝑍𝑋)) + (𝑍𝑋)) = (𝑄𝑖))
558557eqcomd 2740 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) = (((𝑄𝑖) − (𝑍𝑋)) + (𝑍𝑋)))
559472adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
560558, 559oveq12d 7374 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝐸𝑋)) = ((((𝑄𝑖) − (𝑍𝑋)) + (𝑍𝑋))(,)(𝑋 + (𝑍𝑋))))
56114adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
562449, 561, 448iooshift 45710 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((((𝑄𝑖) − (𝑍𝑋)) + (𝑍𝑋))(,)(𝑋 + (𝑍𝑋))) = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))})
563560, 562eqtr2d 2770 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} = ((𝑄𝑖)(,)(𝐸𝑋)))
5645633adant3 1132 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} = ((𝑄𝑖)(,)(𝐸𝑋)))
565227, 564, 5173sstr4d 3987 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} ⊆ dom 𝐹)
566565adantr 480 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} ⊆ dom 𝐹)
567407oveq2d 7372 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 + (𝑍𝑋)) = (𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
568567fveq2d 6836 . . . . . . . . . . . . 13 (𝜑 → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
569568adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
5705693ad2antl1 1186 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
571404adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
5725713ad2antl1 1186 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
573 simpl1 1192 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝜑)
574500sselda 3931 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑥𝐷)
575573, 574, 5723jca 1128 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝜑𝑥𝐷 ∧ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
576 eleq1 2822 . . . . . . . . . . . . . . 15 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
5775763anbi3d 1444 . . . . . . . . . . . . . 14 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑𝑥𝐷 ∧ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)))
578 oveq1 7363 . . . . . . . . . . . . . . . . 17 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
579578oveq2d 7372 . . . . . . . . . . . . . . . 16 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = (𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
580579fveq2d 6836 . . . . . . . . . . . . . . 15 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
581580eqeq1d 2736 . . . . . . . . . . . . . 14 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → ((𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥) ↔ (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
582577, 581imbi12d 344 . . . . . . . . . . . . 13 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥)) ↔ ((𝜑𝑥𝐷 ∧ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥))))
583582, 536vtoclg 3509 . . . . . . . . . . . 12 ((⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ → ((𝜑𝑥𝐷 ∧ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
584572, 575, 583sylc 65 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥))
585570, 584eqtrd 2769 . . . . . . . . . 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 45816 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → 𝑦 ∈ ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) lim (𝑋 + (𝑍𝑋))))
589563reseq2d 5936 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) = (𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))))
590473adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
591589, 590oveq12d 7374 . . . . . . . . . 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 2732 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
597 resindm 5987 . . . . . . . . . . 11 (Rel 𝐹 → (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)) = (𝐹 ↾ (-∞(,)𝑋)))
598597eqcomd 2740 . . . . . . . . . 10 (Rel 𝐹 → (𝐹 ↾ (-∞(,)𝑋)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)))
599176, 598syl 17 . . . . . . . . 9 (𝜑 → (𝐹 ↾ (-∞(,)𝑋)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)))
600181ineq2d 4170 . . . . . . . . . 10 (𝜑 → ((-∞(,)𝑋) ∩ dom 𝐹) = ((-∞(,)𝑋) ∩ 𝐷))
601600reseq2d 5936 . . . . . . . . 9 (𝜑 → (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)))
602599, 601eqtrd 2769 . . . . . . . 8 (𝜑 → (𝐹 ↾ (-∞(,)𝑋)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)))
603602oveq1d 7371 . . . . . . 7 (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) lim 𝑋))
6046033ad2ant1 1133 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) lim 𝑋))
605 inss2 4188 . . . . . . . . . 10 ((-∞(,)𝑋) ∩ 𝐷) ⊆ 𝐷
606605a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)𝑋) ∩ 𝐷) ⊆ 𝐷)
607190, 606fssresd 6699 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)):((-∞(,)𝑋) ∩ 𝐷)⟶ℂ)
608449mnfltd 13036 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ < ((𝑄𝑖) − (𝑍𝑋)))
609195, 450, 608xrltled 13062 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ≤ ((𝑄𝑖) − (𝑍𝑋)))
610 iooss1 13294 . . . . . . . . . . 11 ((-∞ ∈ ℝ* ∧ -∞ ≤ ((𝑄𝑖) − (𝑍𝑋))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ (-∞(,)𝑋))
611194, 609, 610sylancr 587 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ (-∞(,)𝑋))
6126113adant3 1132 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ (-∞(,)𝑋))
613612, 500ssind 4191 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ ((-∞(,)𝑋) ∩ 𝐷))
614605, 231sstrid 3943 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)𝑋) ∩ 𝐷) ⊆ ℂ)
615 eqid 2734 . . . . . . . 8 ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) = ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
6164503adant3 1132 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
6174523ad2ant1 1133 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ*)
6184723ad2ant1 1133 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
619238, 618breqtrd 5122 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝑋 + (𝑍𝑋)))
6204083ad2ant1 1133 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑍𝑋) ∈ ℝ)
621143ad2ant1 1133 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
622211, 620, 621ltsubaddd 11731 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋)) < 𝑋 ↔ (𝑄𝑖) < (𝑋 + (𝑍𝑋))))
623619, 622mpbird 257 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑋)
62414leidd 11701 . . . . . . . . . . 11 (𝜑𝑋𝑋)
6256243ad2ant1 1133 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋𝑋)
626616, 617, 617, 623, 625eliocd 45695 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
627 ioounsn 13391 . . . . . . . . . . . 12 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ* ∧ ((𝑄𝑖) − (𝑍𝑋)) < 𝑋) → ((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋}) = (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
628616, 617, 623, 627syl3anc 1373 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋}) = (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
629628fveq2d 6836 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋})) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘(((𝑄𝑖) − (𝑍𝑋))(,]𝑋)))
630 ovex 7389 . . . . . . . . . . . . . 14 (-∞(,)𝑋) ∈ V
631630inex1 5260 . . . . . . . . . . . . 13 ((-∞(,)𝑋) ∩ 𝐷) ∈ V
632 snex 5379 . . . . . . . . . . . . 13 {𝑋} ∈ V
633631, 632unex 7687 . . . . . . . . . . . 12 (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V
634 resttop 23102 . . . . . . . . . . . 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 24707 . . . . . . . . . . . . . 14 (((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∈ (topGen‘ran (,))
638637a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∈ (topGen‘ran (,)))
639 elrestr 17346 . . . . . . . . . . . . 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 13341 . . . . . . . . . . . . . . . . . . 19 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ⊆ ℝ)
645641, 643, 644syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ⊆ ℝ)
646 simpr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
647645, 646sseldd 3932 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ ℝ)
648452ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑋 ∈ ℝ*)
649 iocgtlb 45690 . . . . . . . . . . . . . . . . . 18 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
650641, 648, 646, 649syl3anc 1373 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
651647ltpnfd 13033 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 < +∞)
652641, 642, 647, 650, 651eliood 45686 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞))
6536523adantl3 1169 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞))
654 eqvisset 3458 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑋𝑋 ∈ V)
655 snidg 4615 . . . . . . . . . . . . . . . . . . . 20 (𝑋 ∈ V → 𝑋 ∈ {𝑋})
656654, 655syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋𝑋 ∈ {𝑋})
657467, 656eqeltrd 2834 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋𝑥 ∈ {𝑋})
658 elun2 4133 . . . . . . . . . . . . . . . . . 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 45691 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥𝑋)
668641, 648, 646, 667syl3anc 1373 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥𝑋)
669668adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥𝑋)
670467eqcoms 2742 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 = 𝑥𝑥 = 𝑋)
671670necon3bi 2956 . . . . . . . . . . . . . . . . . . . . 21 𝑥 = 𝑋𝑋𝑥)
672671adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑋𝑥)
673664, 666, 669, 672leneltd 11285 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 < 𝑋)
674662, 663, 664, 665, 673eliood 45686 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
6756743adantll3 45229 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
676613sselda 3931 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷))
677 elun1 4132 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
678676, 677syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
679661, 675, 678syl2anc 584 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
680660, 679pm2.61dan 812 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
681653, 680elind 4150 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
682616adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
683617adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑋 ∈ ℝ*)
684 elinel1 4151 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞))
685 elioore 13289 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞) → 𝑥 ∈ ℝ)
686684, 685syl 17 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ ℝ)
687686rexrd 11180 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ ℝ*)
688687adantl 481 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ∈ ℝ*)
689450adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
690259a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → +∞ ∈ ℝ*)
691684adantl 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞))
692 ioogtlb 45683 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ* ∧ +∞ ∈ ℝ*𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
693689, 690, 691, 692syl3anc 1373 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
6946933adantl3 1169 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
695 elinel2 4152 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
696 elsni 4595 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {𝑋} → 𝑥 = 𝑋)
697696adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ {𝑋}) → 𝑥 = 𝑋)
698624adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ {𝑋}) → 𝑋𝑋)
699697, 698eqbrtrd 5118 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ {𝑋}) → 𝑥𝑋)
700699adantlr 715 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ 𝑥 ∈ {𝑋}) → 𝑥𝑋)
701 simpll 766 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝜑)
702 elunnel2 4105 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷))
703702adantll 714 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷))
704 elinel1 4151 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷) → 𝑥 ∈ (-∞(,)𝑋))
705703, 704syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ∈ (-∞(,)𝑋))
706 elioore 13289 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (-∞(,)𝑋) → 𝑥 ∈ ℝ)
707706adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑥 ∈ ℝ)
70814adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑋 ∈ ℝ)
709194a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → -∞ ∈ ℝ*)
710452adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑋 ∈ ℝ*)
711 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑥 ∈ (-∞(,)𝑋))
712 iooltub 45698 . . . . . . . . . . . . . . . . . . . . 21 ((-∞ ∈ ℝ*𝑋 ∈ ℝ*𝑥 ∈ (-∞(,)𝑋)) → 𝑥 < 𝑋)
713709, 710, 711, 712syl3anc 1373 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑥 < 𝑋)
714707, 708, 713ltled 11279 . . . . . . . . . . . . . . . . . . 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 45695 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
720681, 719impbida 800 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ↔ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))))
721720eqrdv 2732 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) = ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
722605, 229sstrid 3943 . . . . . . . . . . . . . . 15 (𝜑 → ((-∞(,)𝑋) ∩ 𝐷) ⊆ ℝ)
72314snssd 4763 . . . . . . . . . . . . . . 15 (𝜑 → {𝑋} ⊆ ℝ)
724722, 723unssd 4142 . . . . . . . . . . . . . 14 (𝜑 → (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ⊆ ℝ)
7257243ad2ant1 1133 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ⊆ ℝ)
726233, 366rerest 24746 . . . . . . . . . . . . 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 23024 . . . . . . . . . . 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 2770 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋})))
732626, 731eleqtrd 2836 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋})))
733607, 613, 614, 233, 615, 732limcres 25841 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋) = ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) lim 𝑋))
734733eqcomd 2740 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) lim 𝑋) = (((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
735613resabs1d 5965 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) = (𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)))
736735oveq1d 7371 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
737604, 734, 7363eqtrrd 2774 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋))
738377, 596, 7373eqtrrd 2774 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)))
739738rexlimdv3a 3139 . . 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 2734 . . . . . . . 8 if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋))) = if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋)))
746 eqid 2734 . . . . . . . 8 ((TopOpen‘ℂfld) ↾t (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))})) = ((TopOpen‘ℂfld) ↾t (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))}))
747211, 209, 741, 742, 744, 211, 235, 238, 217, 745, 746fourierdlem33 46326 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋))) ∈ (((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
748217resabs1d 5965 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) = (𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))))
749748oveq1d 7371 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
750747, 749eleqtrd 2836 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋))) ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
751 ne0i 4291 . . . . . 6 (if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋))) ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅)
752750, 751syl 17 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅)
753377, 752eqnetrd 2997 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅)
754753rexlimdv3a 3139 . . 3 (𝜑 → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅))
755173, 754mpd 15 . 2 (𝜑 → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅)
756740, 755eqnetrd 2997 1 (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1541  wcel 2113  wne 2930  wral 3049  wrex 3058  {crab 3397  Vcvv 3438  cun 3897  cin 3898  wss 3899  c0 4283  ifcif 4477  {csn 4578   class class class wbr 5096  cmpt 5177  dom cdm 5622  ran crn 5623  cres 5624  Rel wrel 5627   Fn wfn 6485  wf 6486  cfv 6490  (class class class)co 7356  m cmap 8761  supcsup 9341  cc 11022  cr 11023  0cc0 11024  1c1 11025   + caddc 11027   · cmul 11029  +∞cpnf 11161  -∞cmnf 11162  *cxr 11163   < clt 11164  cle 11165  cmin 11362  -cneg 11363   / cdiv 11792  cn 12143  0cn0 12399  cz 12486  cuz 12749  (,)cioo 13259  (,]cioc 13260  [,]cicc 13262  ...cfz 13421  ..^cfzo 13568  cfl 13708  t crest 17338  TopOpenctopn 17339  topGenctg 17355  fldccnfld 21307  Topctop 22835  intcnt 22959  cnccncf 24823   lim climc 25817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-rep 5222  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-cnex 11080  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-i2m1 11092  ax-1ne0 11093  ax-1rid 11094  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097  ax-pre-lttri 11098  ax-pre-lttrn 11099  ax-pre-ltadd 11100  ax-pre-mulgt0 11101  ax-pre-sup 11102
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-tp 4583  df-op 4585  df-uni 4862  df-int 4901  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-1st 7931  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-er 8633  df-map 8763  df-pm 8764  df-en 8882  df-dom 8883  df-sdom 8884  df-fin 8885  df-fi 9312  df-sup 9343  df-inf 9344  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170  df-sub 11364  df-neg 11365  df-div 11793  df-nn 12144  df-2 12206  df-3 12207  df-4 12208  df-5 12209  df-6 12210  df-7 12211  df-8 12212  df-9 12213  df-n0 12400  df-z 12487  df-dec 12606  df-uz 12750  df-q 12860  df-rp 12904  df-xneg 13024  df-xadd 13025  df-xmul 13026  df-ioo 13263  df-ioc 13264  df-icc 13266  df-fz 13422  df-fzo 13569  df-fl 13710  df-seq 13923  df-exp 13983  df-cj 15020  df-re 15021  df-im 15022  df-sqrt 15156  df-abs 15157  df-struct 17072  df-slot 17107  df-ndx 17119  df-base 17135  df-plusg 17188  df-mulr 17189  df-starv 17190  df-tset 17194  df-ple 17195  df-ds 17197  df-unif 17198  df-rest 17340  df-topn 17341  df-topgen 17361  df-psmet 21299  df-xmet 21300  df-met 21301  df-bl 21302  df-mopn 21303  df-cnfld 21308  df-top 22836  df-topon 22853  df-topsp 22875  df-bases 22888  df-ntr 22962  df-cn 23169  df-cnp 23170  df-xms 24262  df-ms 24263  df-cncf 24825  df-limc 25821
This theorem is referenced by:  fourierdlem94  46386  fourierdlem113  46405
  Copyright terms: Public domain W3C validator