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 46583
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 7400 . . . . . . . . . 10 ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ V
7 fourierdlem49.z . . . . . . . . . . 11 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
87fvmpt2 6959 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ V) → (𝑍𝑥) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
96, 8mpan2 692 . . . . . . . . 9 (𝑥 ∈ ℝ → (𝑍𝑥) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
109oveq2d 7383 . . . . . . . 8 (𝑥 ∈ ℝ → (𝑥 + (𝑍𝑥)) = (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
1110mpteq2ia 5180 . . . . . . 7 (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
125, 11eqtri 2759 . . . . . 6 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
131, 2, 3, 4, 12fourierdlem4 46539 . . . . 5 (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))
14 fourierdlem49.x . . . . 5 (𝜑𝑋 ∈ ℝ)
1513, 14ffvelcdmd 7037 . . . 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 46537 . . . . . . . . . . . . . 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 8796 . . . . . . . . . . 11 (𝑄 ∈ (ℝ ↑m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
2523, 24syl 17 . . . . . . . . . 10 (𝜑𝑄:(0...𝑀)⟶ℝ)
26 ffn 6668 . . . . . . . . . 10 (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
2725, 26syl 17 . . . . . . . . 9 (𝜑𝑄 Fn (0...𝑀))
2827ad2antrr 727 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → 𝑄 Fn (0...𝑀))
29 fvelrnb 6900 . . . . . . . 8 (𝑄 Fn (0...𝑀) → ((𝐸𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋)))
3028, 29syl 17 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → ((𝐸𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋)))
3116, 30mpbid 232 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋))
32 1zzd 12558 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 1 ∈ ℤ)
33 elfzelz 13478 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
3433ad2antlr 728 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℤ)
35 1e0p1 12686 . . . . . . . . . . . . . . . . 17 1 = (0 + 1)
3635a1i 11 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 1 = (0 + 1))
3734zred 12633 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℝ)
38 elfzle1 13481 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
3938ad2antlr 728 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ≤ 𝑗)
40 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑄𝑗) = (𝐸𝑋) → (𝑄𝑗) = (𝐸𝑋))
4140eqcomd 2742 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑄𝑗) = (𝐸𝑋) → (𝐸𝑋) = (𝑄𝑗))
4241ad2antlr 728 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝐸𝑋) = (𝑄𝑗))
43 fveq2 6840 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = 0 → (𝑄𝑗) = (𝑄‘0))
4443adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝑄𝑗) = (𝑄‘0))
4522simprld 772 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵))
4645simpld 494 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑄‘0) = 𝐴)
4746ad2antrr 727 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝑄‘0) = 𝐴)
4842, 44, 473eqtrd 2775 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝐸𝑋) = 𝐴)
4948adantllr 720 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝐸𝑋) = 𝐴)
5049adantllr 720 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → (𝐸𝑋) = 𝐴)
511adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 ∈ ℝ)
521rexrd 11195 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐴 ∈ ℝ*)
5352adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 ∈ ℝ*)
542rexrd 11195 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐵 ∈ ℝ*)
5554adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐵 ∈ ℝ*)
56 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ∈ (𝐴(,]𝐵))
57 iocgtlb 45932 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸𝑋))
5853, 55, 56, 57syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸𝑋))
5951, 58gtned 11281 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ≠ 𝐴)
6059neneqd 2937 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → ¬ (𝐸𝑋) = 𝐴)
6160ad3antrrr 731 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑗 = 0) → ¬ (𝐸𝑋) = 𝐴)
6250, 61pm2.65da 817 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → ¬ 𝑗 = 0)
6362neqned 2939 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ≠ 0)
6437, 39, 63ne0gt0d 11283 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 < 𝑗)
65 0zd 12536 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ∈ ℤ)
66 zltp1le 12577 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
6765, 34, 66syl2anc 585 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
6864, 67mpbid 232 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 + 1) ≤ 𝑗)
6936, 68eqbrtrd 5107 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 1 ≤ 𝑗)
70 eluz2 12794 . . . . . . . . . . . . . . 15 (𝑗 ∈ (ℤ‘1) ↔ (1 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗))
7132, 34, 69, 70syl3anbrc 1345 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ (ℤ‘1))
72 nnuz 12827 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
7371, 72eleqtrrdi 2847 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℕ)
74 nnm1nn0 12478 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ → (𝑗 − 1) ∈ ℕ0)
7573, 74syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ ℕ0)
76 nn0uz 12826 . . . . . . . . . . . . 13 0 = (ℤ‘0)
7776a1i 11 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → ℕ0 = (ℤ‘0))
7875, 77eleqtrd 2838 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (ℤ‘0))
7918nnzd 12550 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℤ)
8079ad3antrrr 731 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑀 ∈ ℤ)
81 peano2zm 12570 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℤ → (𝑗 − 1) ∈ ℤ)
8233, 81syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℤ)
8382zred 12633 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
8433zred 12633 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
85 elfzel2 13476 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
8685zred 12633 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
8784ltm1d 12088 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑗)
88 elfzle2 13482 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗𝑀)
8983, 84, 86, 87, 88ltletrd 11306 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
9089ad2antlr 728 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) < 𝑀)
91 elfzo2 13616 . . . . . . . . . . 11 ((𝑗 − 1) ∈ (0..^𝑀) ↔ ((𝑗 − 1) ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) < 𝑀))
9278, 80, 90, 91syl3anbrc 1345 . . . . . . . . . 10 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (0..^𝑀))
9325ad3antrrr 731 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑄:(0...𝑀)⟶ℝ)
9434, 81syl 17 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ ℤ)
9575nn0ge0d 12501 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ≤ (𝑗 − 1))
9683, 86, 89ltled 11294 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ≤ 𝑀)
9796ad2antlr 728 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ≤ 𝑀)
9865, 80, 94, 95, 97elfzd 13469 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (0...𝑀))
9993, 98ffvelcdmd 7037 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ)
10099rexrd 11195 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ*)
10125ffvelcdmda 7036 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ)
102101rexrd 11195 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ*)
103102adantlr 716 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ*)
104103adantr 480 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ∈ ℝ*)
105 iocssre 13380 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
10652, 2, 105syl2anc 585 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
107106sselda 3921 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ∈ ℝ)
108107rexrd 11195 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ∈ ℝ*)
109108ad2antrr 727 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ*)
110 simplll 775 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝜑)
111 ovex 7400 . . . . . . . . . . . . . . . 16 (𝑗 − 1) ∈ V
112 eleq1 2824 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 − 1) → (𝑖 ∈ (0..^𝑀) ↔ (𝑗 − 1) ∈ (0..^𝑀)))
113112anbi2d 631 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 − 1) → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀))))
114 fveq2 6840 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 − 1) → (𝑄𝑖) = (𝑄‘(𝑗 − 1)))
115 oveq1 7374 . . . . . . . . . . . . . . . . . . 19 (𝑖 = (𝑗 − 1) → (𝑖 + 1) = ((𝑗 − 1) + 1))
116115fveq2d 6844 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 − 1) → (𝑄‘(𝑖 + 1)) = (𝑄‘((𝑗 − 1) + 1)))
117114, 116breq12d 5098 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 − 1) → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1))))
118113, 117imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 − 1) → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))))
11922simprrd 774 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))
120119r19.21bi 3229 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
121111, 118, 120vtocl 3503 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
122110, 92, 121syl2anc 585 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
12333zcnd 12634 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
124 1cnd 11139 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 1 ∈ ℂ)
125123, 124npcand 11509 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → ((𝑗 − 1) + 1) = 𝑗)
126125eqcomd 2742 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → 𝑗 = ((𝑗 − 1) + 1))
127126fveq2d 6844 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → (𝑄𝑗) = (𝑄‘((𝑗 − 1) + 1)))
128127eqcomd 2742 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
129128ad2antlr 728 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
130122, 129breqtrd 5111 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄𝑗))
131 simpr 484 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) = (𝐸𝑋))
132130, 131breqtrd 5111 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝐸𝑋))
133106, 15sseldd 3922 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸𝑋) ∈ ℝ)
134133leidd 11716 . . . . . . . . . . . . . . 15 (𝜑 → (𝐸𝑋) ≤ (𝐸𝑋))
135134ad2antrr 727 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝐸𝑋))
13641adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) = (𝑄𝑗))
137135, 136breqtrd 5111 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄𝑗))
138137adantllr 720 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄𝑗))
139100, 104, 109, 132, 138eliocd 45937 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄𝑗)))
140127oveq2d 7383 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → ((𝑄‘(𝑗 − 1))(,](𝑄𝑗)) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
141140ad2antlr 728 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → ((𝑄‘(𝑗 − 1))(,](𝑄𝑗)) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
142139, 141eleqtrd 2838 . . . . . . . . . 10 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
143114, 116oveq12d 7385 . . . . . . . . . . . 12 (𝑖 = (𝑗 − 1) → ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
144143eleq2d 2822 . . . . . . . . . . 11 (𝑖 = (𝑗 − 1) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) ↔ (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))))
145144rspcev 3564 . . . . . . . . . 10 (((𝑗 − 1) ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
14692, 142, 145syl2anc 585 . . . . . . . . 9 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄𝑗) = (𝐸𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
147146ex 412 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
148147adantlr 716 . . . . . . 7 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
149148rexlimdva 3138 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
15031, 149mpd 15 . . . . 5 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
15118ad2antrr 727 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → 𝑀 ∈ ℕ)
15225ad2antrr 727 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ)
153 iocssicc 13390 . . . . . . . . . 10 (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵)
15446eqcomd 2742 . . . . . . . . . . 11 (𝜑𝐴 = (𝑄‘0))
15545simprd 495 . . . . . . . . . . . 12 (𝜑 → (𝑄𝑀) = 𝐵)
156155eqcomd 2742 . . . . . . . . . . 11 (𝜑𝐵 = (𝑄𝑀))
157154, 156oveq12d 7385 . . . . . . . . . 10 (𝜑 → (𝐴[,]𝐵) = ((𝑄‘0)[,](𝑄𝑀)))
158153, 157sseqtrid 3964 . . . . . . . . 9 (𝜑 → (𝐴(,]𝐵) ⊆ ((𝑄‘0)[,](𝑄𝑀)))
159158sselda 3921 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → (𝐸𝑋) ∈ ((𝑄‘0)[,](𝑄𝑀)))
160159adantr 480 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (𝐸𝑋) ∈ ((𝑄‘0)[,](𝑄𝑀)))
161 simpr 484 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ¬ (𝐸𝑋) ∈ ran 𝑄)
162 fveq2 6840 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝑄𝑘) = (𝑄𝑗))
163162breq1d 5095 . . . . . . . . 9 (𝑘 = 𝑗 → ((𝑄𝑘) < (𝐸𝑋) ↔ (𝑄𝑗) < (𝐸𝑋)))
164163cbvrabv 3399 . . . . . . . 8 {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < (𝐸𝑋)} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < (𝐸𝑋)}
165164supeq1i 9360 . . . . . . 7 sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < (𝐸𝑋)}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < (𝐸𝑋)}, ℝ, < )
166151, 152, 160, 161, 165fourierdlem25 46560 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
167 ioossioc 45922 . . . . . . . . 9 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))
168167sseli 3917 . . . . . . . 8 ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
169168a1i 11 . . . . . . 7 ((((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
170169reximdva 3150 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
171166, 170mpd 15 . . . . 5 (((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
172150, 171pm2.61dan 813 . . . 4 ((𝜑 ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
17315, 172mpdan 688 . . 3 (𝜑 → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
174 fourierdlem49.f . . . . . . . . . . 11 (𝜑𝐹:𝐷⟶ℝ)
175 frel 6673 . . . . . . . . . . 11 (𝐹:𝐷⟶ℝ → Rel 𝐹)
176174, 175syl 17 . . . . . . . . . 10 (𝜑 → Rel 𝐹)
177 resindm 5995 . . . . . . . . . . 11 (Rel 𝐹 → (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹)) = (𝐹 ↾ (-∞(,)(𝐸𝑋))))
178177eqcomd 2742 . . . . . . . . . 10 (Rel 𝐹 → (𝐹 ↾ (-∞(,)(𝐸𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹)))
179176, 178syl 17 . . . . . . . . 9 (𝜑 → (𝐹 ↾ (-∞(,)(𝐸𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹)))
180 fdm 6677 . . . . . . . . . . . 12 (𝐹:𝐷⟶ℝ → dom 𝐹 = 𝐷)
181174, 180syl 17 . . . . . . . . . . 11 (𝜑 → dom 𝐹 = 𝐷)
182181ineq2d 4160 . . . . . . . . . 10 (𝜑 → ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹) = ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
183182reseq2d 5944 . . . . . . . . 9 (𝜑 → (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ dom 𝐹)) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)))
184179, 183eqtrd 2771 . . . . . . . 8 (𝜑 → (𝐹 ↾ (-∞(,)(𝐸𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)))
1851843ad2ant1 1134 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ (-∞(,)(𝐸𝑋))) = (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)))
186185oveq1d 7382 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) lim (𝐸𝑋)))
187 ax-resscn 11095 . . . . . . . . . . 11 ℝ ⊆ ℂ
188187a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ⊆ ℂ)
189174, 188fssd 6685 . . . . . . . . 9 (𝜑𝐹:𝐷⟶ℂ)
1901893ad2ant1 1134 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐹:𝐷⟶ℂ)
191 inss2 4178 . . . . . . . . 9 ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ 𝐷
192191a1i 11 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ 𝐷)
193190, 192fssresd 6707 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)):((-∞(,)(𝐸𝑋)) ∩ 𝐷)⟶ℂ)
194 mnfxr 11202 . . . . . . . . . 10 -∞ ∈ ℝ*
195194a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ∈ ℝ*)
19625adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
197 elfzofz 13630 . . . . . . . . . . . . . 14 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
198197adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
199196, 198ffvelcdmd 7037 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
200199rexrd 11195 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ*)
201199mnfltd 13075 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ < (𝑄𝑖))
202195, 200, 201xrltled 13101 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ≤ (𝑄𝑖))
203 iooss1 13333 . . . . . . . . . 10 ((-∞ ∈ ℝ* ∧ -∞ ≤ (𝑄𝑖)) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ (-∞(,)(𝐸𝑋)))
204194, 202, 203sylancr 588 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ (-∞(,)(𝐸𝑋)))
2052043adant3 1133 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ (-∞(,)(𝐸𝑋)))
206 fzofzp1 13719 . . . . . . . . . . . . . 14 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
207206adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
208196, 207ffvelcdmd 7037 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
2092083adant3 1133 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
210209rexrd 11195 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
2111993adant3 1133 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
212211rexrd 11195 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ*)
213 simp3 1139 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
214 iocleub 45933 . . . . . . . . . . 11 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
215212, 210, 213, 214syl3anc 1374 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
216 iooss2 13334 . . . . . . . . . 10 (((𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
217210, 215, 216syl2anc 585 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
218 fourierdlem49.cn . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
219 cncff 24860 . . . . . . . . . . . . 13 ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
220 fdm 6677 . . . . . . . . . . . . 13 ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ → dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
221218, 219, 2203syl 18 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
222 ssdmres 5978 . . . . . . . . . . . 12 (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹 ↔ dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
223221, 222sylibr 234 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹)
224181adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → dom 𝐹 = 𝐷)
225223, 224sseqtrd 3958 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
2262253adant3 1133 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
227217, 226sstrd 3932 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ 𝐷)
228205, 227ssind 4181 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
229 fourierdlem49.d . . . . . . . . . 10 (𝜑𝐷 ⊆ ℝ)
230229, 188sstrd 3932 . . . . . . . . 9 (𝜑𝐷 ⊆ ℂ)
2312303ad2ant1 1134 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐷 ⊆ ℂ)
232191, 231sstrid 3933 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ ℂ)
233 eqid 2736 . . . . . . 7 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
234 eqid 2736 . . . . . . 7 ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) = ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
2351333ad2ant1 1134 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ℝ)
236235rexrd 11195 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ℝ*)
237 iocgtlb 45932 . . . . . . . . . 10 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝐸𝑋))
238212, 210, 213, 237syl3anc 1374 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝐸𝑋))
239235leidd 11716 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝐸𝑋))
240212, 236, 236, 238, 239eliocd 45937 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝐸𝑋)))
241 ioounsn 13430 . . . . . . . . . . 11 (((𝑄𝑖) ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ* ∧ (𝑄𝑖) < (𝐸𝑋)) → (((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)}) = ((𝑄𝑖)(,](𝐸𝑋)))
242212, 236, 238, 241syl3anc 1374 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)}) = ((𝑄𝑖)(,](𝐸𝑋)))
243242fveq2d 6844 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘(((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)})) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘((𝑄𝑖)(,](𝐸𝑋))))
244233cnfldtop 24748 . . . . . . . . . . 11 (TopOpen‘ℂfld) ∈ Top
245 ovex 7400 . . . . . . . . . . . . 13 (-∞(,)(𝐸𝑋)) ∈ V
246245inex1 5258 . . . . . . . . . . . 12 ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∈ V
247 snex 5381 . . . . . . . . . . . 12 {(𝐸𝑋)} ∈ V
248246, 247unex 7698 . . . . . . . . . . 11 (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∈ V
249 resttop 23125 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ∈ Top ∧ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∈ V) → ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ Top)
250244, 248, 249mp2an 693 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ Top
251 retop 24726 . . . . . . . . . . . . 13 (topGen‘ran (,)) ∈ Top
252251a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (topGen‘ran (,)) ∈ Top)
253248a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∈ V)
254 iooretop 24730 . . . . . . . . . . . . 13 ((𝑄𝑖)(,)+∞) ∈ (topGen‘ran (,))
255254a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)+∞) ∈ (topGen‘ran (,)))
256 elrestr 17391 . . . . . . . . . . . 12 (((topGen‘ran (,)) ∈ Top ∧ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∈ V ∧ ((𝑄𝑖)(,)+∞) ∈ (topGen‘ran (,))) → (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
257252, 253, 255, 256syl3anc 1374 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
258 simpr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 = (𝐸𝑋)) → 𝑥 = (𝐸𝑋))
259 pnfxr 11199 . . . . . . . . . . . . . . . . . . . 20 +∞ ∈ ℝ*
260259a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → +∞ ∈ ℝ*)
261235ltpnfd 13072 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) < +∞)
262212, 260, 235, 238, 261eliood 45928 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,)+∞))
263 snidg 4604 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸𝑋) ∈ ℝ → (𝐸𝑋) ∈ {(𝐸𝑋)})
264 elun2 4123 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸𝑋) ∈ {(𝐸𝑋)} → (𝐸𝑋) ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
265263, 264syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝐸𝑋) ∈ ℝ → (𝐸𝑋) ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
266133, 265syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐸𝑋) ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
2672663ad2ant1 1134 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
268262, 267elind 4140 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
269268adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
270258, 269eqeltrd 2836 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
271270adantlr 716 . . . . . . . . . . . . . 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 13380 . . . . . . . . . . . . . . . . . . . 20 (((𝑄𝑖) ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ) → ((𝑄𝑖)(,](𝐸𝑋)) ⊆ ℝ)
278274, 276, 277syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → ((𝑄𝑖)(,](𝐸𝑋)) ⊆ ℝ)
279 simpr 484 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋)))
280278, 279sseldd 3922 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ ℝ)
2812803adantl3 1170 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ ℝ)
282276rexrd 11195 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝐸𝑋) ∈ ℝ*)
283 iocgtlb 45932 . . . . . . . . . . . . . . . . . . 19 (((𝑄𝑖) ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ*𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝑄𝑖) < 𝑥)
284274, 282, 279, 283syl3anc 1374 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝑄𝑖) < 𝑥)
2852843adantl3 1170 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → (𝑄𝑖) < 𝑥)
286281ltpnfd 13072 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 < +∞)
287272, 273, 281, 285, 286eliood 45928 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ ((𝑄𝑖)(,)+∞))
288287adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ((𝑄𝑖)(,)+∞))
289194a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → -∞ ∈ ℝ*)
290282adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ*)
291280adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ℝ)
292291mnfltd 13075 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → -∞ < 𝑥)
293133ad3antrrr 731 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ)
294 iocleub 45933 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑄𝑖) ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ*𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ≤ (𝐸𝑋))
295274, 282, 279, 294syl3anc 1374 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ≤ (𝐸𝑋))
296295adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ≤ (𝐸𝑋))
297 neqne 2940 . . . . . . . . . . . . . . . . . . . . . 22 𝑥 = (𝐸𝑋) → 𝑥 ≠ (𝐸𝑋))
298297necomd 2987 . . . . . . . . . . . . . . . . . . . . 21 𝑥 = (𝐸𝑋) → (𝐸𝑋) ≠ 𝑥)
299298adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ≠ 𝑥)
300291, 293, 296, 299leneltd 11300 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 < (𝐸𝑋))
301289, 290, 291, 292, 300eliood 45928 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (-∞(,)(𝐸𝑋)))
3023013adantll3 45473 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (-∞(,)(𝐸𝑋)))
303226ad2antrr 727 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
304272adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝑄𝑖) ∈ ℝ*)
305210ad2antrr 727 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
306281adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ℝ)
307285adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝑄𝑖) < 𝑥)
308235ad2antrr 727 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ)
309209ad2antrr 727 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
3103003adantll3 45473 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 < (𝐸𝑋))
311215ad2antrr 727 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
312306, 308, 309, 310, 311ltletrd 11306 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 < (𝑄‘(𝑖 + 1)))
313304, 305, 306, 307, 312eliood 45928 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
314303, 313sseldd 3922 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥𝐷)
315302, 314elind 4140 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
316 elun1 4122 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷) → 𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
317315, 316syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
318288, 317elind 4140 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) ∧ ¬ 𝑥 = (𝐸𝑋)) → 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
319271, 318pm2.61dan 813 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋))) → 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
320212adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝑄𝑖) ∈ ℝ*)
321236adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝐸𝑋) ∈ ℝ*)
322 elinel1 4141 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ∈ ((𝑄𝑖)(,)+∞))
323 elioore 13328 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((𝑄𝑖)(,)+∞) → 𝑥 ∈ ℝ)
324323rexrd 11195 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((𝑄𝑖)(,)+∞) → 𝑥 ∈ ℝ*)
325322, 324syl 17 . . . . . . . . . . . . . . 15 (𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ∈ ℝ*)
326325adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ∈ ℝ*)
327200adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝑄𝑖) ∈ ℝ*)
328259a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → +∞ ∈ ℝ*)
329322adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ∈ ((𝑄𝑖)(,)+∞))
330 ioogtlb 45925 . . . . . . . . . . . . . . . 16 (((𝑄𝑖) ∈ ℝ* ∧ +∞ ∈ ℝ*𝑥 ∈ ((𝑄𝑖)(,)+∞)) → (𝑄𝑖) < 𝑥)
331327, 328, 329, 330syl3anc 1374 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝑄𝑖) < 𝑥)
3323313adantl3 1170 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → (𝑄𝑖) < 𝑥)
333 elinel2 4142 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))
334 elsni 4584 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {(𝐸𝑋)} → 𝑥 = (𝐸𝑋))
335334adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ {(𝐸𝑋)}) → 𝑥 = (𝐸𝑋))
336134adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ {(𝐸𝑋)}) → (𝐸𝑋) ≤ (𝐸𝑋))
337335, 336eqbrtrd 5107 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ≤ (𝐸𝑋))
338337adantlr 716 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∧ 𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ≤ (𝐸𝑋))
339 simpll 767 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∧ ¬ 𝑥 ∈ {(𝐸𝑋)}) → 𝜑)
340 elunnel2 4095 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ∧ ¬ 𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
341340adantll 715 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∧ ¬ 𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷))
342 elinel1 4141 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷) → 𝑥 ∈ (-∞(,)(𝐸𝑋)))
343 elioore 13328 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (-∞(,)(𝐸𝑋)) → 𝑥 ∈ ℝ)
344343adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 ∈ ℝ)
345133adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → (𝐸𝑋) ∈ ℝ)
346194a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → -∞ ∈ ℝ*)
347345rexrd 11195 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → (𝐸𝑋) ∈ ℝ*)
348 simpr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 ∈ (-∞(,)(𝐸𝑋)))
349 iooltub 45940 . . . . . . . . . . . . . . . . . . . . . 22 ((-∞ ∈ ℝ* ∧ (𝐸𝑋) ∈ ℝ*𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 < (𝐸𝑋))
350346, 347, 348, 349syl3anc 1374 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 < (𝐸𝑋))
351344, 345, 350ltled 11294 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (-∞(,)(𝐸𝑋))) → 𝑥 ≤ (𝐸𝑋))
352342, 351sylan2 594 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) → 𝑥 ≤ (𝐸𝑋))
353339, 341, 352syl2anc 585 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∧ ¬ 𝑥 ∈ {(𝐸𝑋)}) → 𝑥 ≤ (𝐸𝑋))
354338, 353pm2.61dan 813 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ≤ (𝐸𝑋))
355354adantlr 716 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) → 𝑥 ≤ (𝐸𝑋))
356333, 355sylan2 594 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ≤ (𝐸𝑋))
3573563adantl3 1170 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ≤ (𝐸𝑋))
358320, 321, 326, 332, 357eliocd 45937 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → 𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋)))
359319, 358impbida 801 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑥 ∈ ((𝑄𝑖)(,](𝐸𝑋)) ↔ 𝑥 ∈ (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))))
360359eqrdv 2734 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,](𝐸𝑋)) = (((𝑄𝑖)(,)+∞) ∩ (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
361 ioossre 13360 . . . . . . . . . . . . . 14 (-∞(,)(𝐸𝑋)) ⊆ ℝ
362 ssinss1 4186 . . . . . . . . . . . . . 14 ((-∞(,)(𝐸𝑋)) ⊆ ℝ → ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ ℝ)
363361, 362mp1i 13 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)(𝐸𝑋)) ∩ 𝐷) ⊆ ℝ)
364235snssd 4730 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {(𝐸𝑋)} ⊆ ℝ)
365363, 364unssd 4132 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ⊆ ℝ)
366 eqid 2736 . . . . . . . . . . . . 13 (topGen‘ran (,)) = (topGen‘ran (,))
367233, 366rerest 24769 . . . . . . . . . . . 12 ((((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) = ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
368365, 367syl 17 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) = ((topGen‘ran (,)) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
369257, 360, 3683eltr4d 2851 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,](𝐸𝑋)) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))
370 isopn3i 23047 . . . . . . . . . 10 ((((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})) ∈ Top ∧ ((𝑄𝑖)(,](𝐸𝑋)) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)}))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘((𝑄𝑖)(,](𝐸𝑋))) = ((𝑄𝑖)(,](𝐸𝑋)))
371250, 369, 370sylancr 588 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘((𝑄𝑖)(,](𝐸𝑋))) = ((𝑄𝑖)(,](𝐸𝑋)))
372243, 371eqtr2d 2772 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,](𝐸𝑋)) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘(((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)})))
373240, 372eleqtrd 2838 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)(𝐸𝑋)) ∩ 𝐷) ∪ {(𝐸𝑋)})))‘(((𝑄𝑖)(,)(𝐸𝑋)) ∪ {(𝐸𝑋)})))
374193, 228, 232, 233, 234, 373limcres 25853 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) lim (𝐸𝑋)))
375228resabs1d 5973 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) = (𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))))
376375oveq1d 7382 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)(𝐸𝑋)) ∩ 𝐷)) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
377186, 374, 3763eqtr2d 2777 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
378181feq2d 6652 . . . . . . . . . . . 12 (𝜑 → (𝐹:dom 𝐹⟶ℂ ↔ 𝐹:𝐷⟶ℂ))
379189, 378mpbird 257 . . . . . . . . . . 11 (𝜑𝐹:dom 𝐹⟶ℂ)
380379adantr 480 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝐹:dom 𝐹⟶ℂ)
3813803ad2antl1 1187 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝐹:dom 𝐹⟶ℂ)
382 ioosscn 13361 . . . . . . . . . 10 ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ℂ
383382a1i 11 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ ℂ)
384181eqcomd 2742 . . . . . . . . . . . 12 (𝜑𝐷 = dom 𝐹)
3853843ad2ant1 1134 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐷 = dom 𝐹)
386227, 385sseqtrd 3958 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ dom 𝐹)
387386adantr 480 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ dom 𝐹)
3887a1i 11 . . . . . . . . . . . . . . 15 (𝜑𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
389 oveq2 7375 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋 → (𝐵𝑥) = (𝐵𝑋))
390389oveq1d 7382 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋 → ((𝐵𝑥) / 𝑇) = ((𝐵𝑋) / 𝑇))
391390fveq2d 6844 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋 → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵𝑋) / 𝑇)))
392391oveq1d 7382 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
393392adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑥 = 𝑋) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
3942, 14resubcld 11578 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵𝑋) ∈ ℝ)
3952, 1resubcld 11578 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐵𝐴) ∈ ℝ)
3964, 395eqeltrid 2840 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑇 ∈ ℝ)
3971, 2posdifd 11737 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
3983, 397mpbid 232 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 < (𝐵𝐴))
3994eqcomi 2745 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵𝐴) = 𝑇
400399a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵𝐴) = 𝑇)
401398, 400breqtrd 5111 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 < 𝑇)
402401gt0ne0d 11714 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑇 ≠ 0)
403394, 396, 402redivcld 11983 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵𝑋) / 𝑇) ∈ ℝ)
404403flcld 13757 . . . . . . . . . . . . . . . . 17 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
405404zred 12633 . . . . . . . . . . . . . . . 16 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℝ)
406405, 396remulcld 11175 . . . . . . . . . . . . . . 15 (𝜑 → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
407388, 393, 14, 406fvmptd 6955 . . . . . . . . . . . . . 14 (𝜑 → (𝑍𝑋) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
408407, 406eqeltrd 2836 . . . . . . . . . . . . 13 (𝜑 → (𝑍𝑋) ∈ ℝ)
409408recnd 11173 . . . . . . . . . . . 12 (𝜑 → (𝑍𝑋) ∈ ℂ)
410409adantr 480 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → (𝑍𝑋) ∈ ℂ)
4114103ad2antl1 1187 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → (𝑍𝑋) ∈ ℂ)
412411negcld 11492 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → -(𝑍𝑋) ∈ ℂ)
413 eqid 2736 . . . . . . . . 9 {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}
414 ioosscn 13361 . . . . . . . . . . . . . . . . . . 19 (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ ℂ
415414sseli 3917 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) → 𝑦 ∈ ℂ)
416415adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℂ)
417409adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℂ)
418416, 417pncand 11506 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = 𝑦)
419418eqcomd 2742 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)))
4204193ad2antl1 1187 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)))
421407oveq2d 7383 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = ((𝑦 + (𝑍𝑋)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
422421adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = ((𝑦 + (𝑍𝑋)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
423416, 417addcld 11164 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℂ)
424406recnd 11173 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
425424adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
426423, 425negsubd 11511 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + (𝑍𝑋)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
427404zcnd 12634 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℂ)
428396recnd 11173 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑇 ∈ ℂ)
429427, 428mulneg1d 11603 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
430429eqcomd 2742 . . . . . . . . . . . . . . . . . . 19 (𝜑 → -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
431430oveq2d 7383 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑦 + (𝑍𝑋)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
432431adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
433422, 426, 4323eqtr2d 2777 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
4344333ad2antl1 1187 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
435404znegcld 12635 . . . . . . . . . . . . . . . . . 18 (𝜑 → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
436435adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
4374363ad2antl1 1187 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
438 simpl1 1193 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝜑)
439227adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖)(,)(𝐸𝑋)) ⊆ 𝐷)
440200adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) ∈ ℝ*)
441133rexrd 11195 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐸𝑋) ∈ ℝ*)
442441ad2antrr 727 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐸𝑋) ∈ ℝ*)
443 elioore 13328 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) → 𝑦 ∈ ℝ)
444443adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
445408adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℝ)
446444, 445readdcld 11174 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
447446adantlr 716 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
448408adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑍𝑋) ∈ ℝ)
449199, 448resubcld 11578 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ)
450449rexrd 11195 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
451450adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
45214rexrd 11195 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑋 ∈ ℝ*)
453452ad2antrr 727 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑋 ∈ ℝ*)
454 simpr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
455 ioogtlb 45925 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑦)
456451, 453, 454, 455syl3anc 1374 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑦)
457199adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) ∈ ℝ)
458448adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℝ)
459443adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
460457, 458, 459ltsubaddd 11746 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (((𝑄𝑖) − (𝑍𝑋)) < 𝑦 ↔ (𝑄𝑖) < (𝑦 + (𝑍𝑋))))
461456, 460mpbid 232 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) < (𝑦 + (𝑍𝑋)))
46214ad2antrr 727 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑋 ∈ ℝ)
463 iooltub 45940 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 < 𝑋)
464451, 453, 454, 463syl3anc 1374 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 < 𝑋)
465459, 462, 458, 464ltadd1dd 11761 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝑋 + (𝑍𝑋)))
4665a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥))))
467 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑋𝑥 = 𝑋)
468 fveq2 6840 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑋 → (𝑍𝑥) = (𝑍𝑋))
469467, 468oveq12d 7385 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑋 → (𝑥 + (𝑍𝑥)) = (𝑋 + (𝑍𝑋)))
470469adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 = 𝑋) → (𝑥 + (𝑍𝑥)) = (𝑋 + (𝑍𝑋)))
47114, 408readdcld 11174 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑋 + (𝑍𝑋)) ∈ ℝ)
472466, 470, 14, 471fvmptd 6955 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
473472eqcomd 2742 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
474473ad2antrr 727 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
475465, 474breqtrd 5111 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝐸𝑋))
476440, 442, 447, 461, 475eliood 45928 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ((𝑄𝑖)(,)(𝐸𝑋)))
4774763adantl3 1170 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ((𝑄𝑖)(,)(𝐸𝑋)))
478439, 477sseldd 3922 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ 𝐷)
479438, 478, 4373jca 1129 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
480 eleq1 2824 . . . . . . . . . . . . . . . . . . 19 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
4814803anbi3d 1445 . . . . . . . . . . . . . . . . . 18 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)))
482 oveq1 7374 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 · 𝑇) = (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
483482oveq2d 7383 . . . . . . . . . . . . . . . . . . 19 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
484483eleq1d 2821 . . . . . . . . . . . . . . . . . 18 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
485481, 484imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)))
486 ovex 7400 . . . . . . . . . . . . . . . . . 18 (𝑦 + (𝑍𝑋)) ∈ V
487 eleq1 2824 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑦 + (𝑍𝑋)) → (𝑥𝐷 ↔ (𝑦 + (𝑍𝑋)) ∈ 𝐷))
4884873anbi2d 1444 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑦 + (𝑍𝑋)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ)))
489 oveq1 7374 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑦 + (𝑍𝑋)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)))
490489eleq1d 2821 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑦 + (𝑍𝑋)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷))
491488, 490imbi12d 344 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑦 + (𝑍𝑋)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)))
492 fourierdlem49.dper . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)
493486, 491, 492vtocl 3503 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)
494485, 493vtoclg 3499 . . . . . . . . . . . . . . . 16 (-(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ → ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
495437, 479, 494sylc 65 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
496434, 495eqeltrd 2836 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) − (𝑍𝑋)) ∈ 𝐷)
497420, 496eqeltrd 2836 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦𝐷)
498497ralrimiva 3129 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑦𝐷)
499 dfss3 3910 . . . . . . . . . . . 12 ((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷 ↔ ∀𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑦𝐷)
500498, 499sylibr 234 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷)
501199recnd 11173 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℂ)
502409adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑍𝑋) ∈ ℂ)
503501, 502negsubd 11511 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + -(𝑍𝑋)) = ((𝑄𝑖) − (𝑍𝑋)))
504503eqcomd 2742 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) = ((𝑄𝑖) + -(𝑍𝑋)))
505472oveq1d 7382 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸𝑋) + -(𝑍𝑋)) = ((𝑋 + (𝑍𝑋)) + -(𝑍𝑋)))
506471recnd 11173 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑋 + (𝑍𝑋)) ∈ ℂ)
507506, 409negsubd 11511 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑋 + (𝑍𝑋)) + -(𝑍𝑋)) = ((𝑋 + (𝑍𝑋)) − (𝑍𝑋)))
50814recnd 11173 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 ∈ ℂ)
509508, 409pncand 11506 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑋 + (𝑍𝑋)) − (𝑍𝑋)) = 𝑋)
510505, 507, 5093eqtrrd 2776 . . . . . . . . . . . . . . 15 (𝜑𝑋 = ((𝐸𝑋) + -(𝑍𝑋)))
511510adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 = ((𝐸𝑋) + -(𝑍𝑋)))
512504, 511oveq12d 7385 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) = (((𝑄𝑖) + -(𝑍𝑋))(,)((𝐸𝑋) + -(𝑍𝑋))))
513448renegcld 11577 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → -(𝑍𝑋) ∈ ℝ)
514199, 275, 513iooshift 45952 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) + -(𝑍𝑋))(,)((𝐸𝑋) + -(𝑍𝑋))) = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))})
515512, 514eqtr2d 2772 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} = (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
5165153adant3 1133 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} = (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
5171813ad2ant1 1134 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → dom 𝐹 = 𝐷)
518500, 516, 5173sstr4d 3977 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} ⊆ dom 𝐹)
519518adantr 480 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))} ⊆ dom 𝐹)
520407negeqd 11387 . . . . . . . . . . . . . . . 16 (𝜑 → -(𝑍𝑋) = -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
521520, 430eqtrd 2771 . . . . . . . . . . . . . . 15 (𝜑 → -(𝑍𝑋) = (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
522521oveq2d 7383 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 + -(𝑍𝑋)) = (𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
523522fveq2d 6844 . . . . . . . . . . . . 13 (𝜑 → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
524523adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
5255243ad2antl1 1187 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
526435adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
5275263ad2antl1 1187 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
528 simpl1 1193 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → 𝜑)
529227sselda 3921 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → 𝑥𝐷)
530528, 529, 5273jca 1129 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝜑𝑥𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
5314803anbi3d 1445 . . . . . . . . . . . . . 14 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑𝑥𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)))
532482oveq2d 7383 . . . . . . . . . . . . . . . 16 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = (𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
533532fveq2d 6844 . . . . . . . . . . . . . . 15 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
534533eqeq1d 2738 . . . . . . . . . . . . . 14 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥) ↔ (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
535531, 534imbi12d 344 . . . . . . . . . . . . 13 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥)) ↔ ((𝜑𝑥𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥))))
536 fourierdlem49.per . . . . . . . . . . . . 13 ((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥))
537535, 536vtoclg 3499 . . . . . . . . . . . 12 (-(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ → ((𝜑𝑥𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
538527, 530, 537sylc 65 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥))
539525, 538eqtrd 2771 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹𝑥))
540539adantlr 716 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))) → (𝐹‘(𝑥 + -(𝑍𝑋))) = (𝐹𝑥))
541 simpr 484 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
542381, 383, 387, 412, 413, 519, 540, 541limcperiod 46058 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝑦 ∈ ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) lim ((𝐸𝑋) + -(𝑍𝑋))))
543515reseq2d 5944 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) = (𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)))
544511eqcomd 2742 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) + -(𝑍𝑋)) = 𝑋)
545543, 544oveq12d 7385 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) lim ((𝐸𝑋) + -(𝑍𝑋))) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
5465453adant3 1133 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) lim ((𝐸𝑋) + -(𝑍𝑋))) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
547546adantr 480 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ ((𝑄𝑖)(,)(𝐸𝑋))𝑧 = (𝑥 + -(𝑍𝑋))}) lim ((𝐸𝑋) + -(𝑍𝑋))) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
548542, 547eleqtrd 2838 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋))) → 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
549379adantr 480 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → 𝐹:dom 𝐹⟶ℂ)
5505493ad2antl1 1187 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → 𝐹:dom 𝐹⟶ℂ)
551414a1i 11 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ ℂ)
552500, 517sseqtrrd 3959 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ dom 𝐹)
553552adantr 480 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ dom 𝐹)
554409adantr 480 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → (𝑍𝑋) ∈ ℂ)
5555543ad2antl1 1187 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → (𝑍𝑋) ∈ ℂ)
556 eqid 2736 . . . . . . . . 9 {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}
557501, 502npcand 11509 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) − (𝑍𝑋)) + (𝑍𝑋)) = (𝑄𝑖))
558557eqcomd 2742 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) = (((𝑄𝑖) − (𝑍𝑋)) + (𝑍𝑋)))
559472adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
560558, 559oveq12d 7385 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝐸𝑋)) = ((((𝑄𝑖) − (𝑍𝑋)) + (𝑍𝑋))(,)(𝑋 + (𝑍𝑋))))
56114adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
562449, 561, 448iooshift 45952 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((((𝑄𝑖) − (𝑍𝑋)) + (𝑍𝑋))(,)(𝑋 + (𝑍𝑋))) = {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))})
563560, 562eqtr2d 2772 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} = ((𝑄𝑖)(,)(𝐸𝑋)))
5645633adant3 1133 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} = ((𝑄𝑖)(,)(𝐸𝑋)))
565227, 564, 5173sstr4d 3977 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} ⊆ dom 𝐹)
566565adantr 480 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))} ⊆ dom 𝐹)
567407oveq2d 7383 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 + (𝑍𝑋)) = (𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
568567fveq2d 6844 . . . . . . . . . . . . 13 (𝜑 → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
569568adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
5705693ad2antl1 1187 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
571404adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
5725713ad2antl1 1187 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
573 simpl1 1193 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝜑)
574500sselda 3921 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑥𝐷)
575573, 574, 5723jca 1129 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝜑𝑥𝐷 ∧ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
576 eleq1 2824 . . . . . . . . . . . . . . 15 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
5775763anbi3d 1445 . . . . . . . . . . . . . 14 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑𝑥𝐷 ∧ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)))
578 oveq1 7374 . . . . . . . . . . . . . . . . 17 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
579578oveq2d 7383 . . . . . . . . . . . . . . . 16 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = (𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
580579fveq2d 6844 . . . . . . . . . . . . . . 15 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))))
581580eqeq1d 2738 . . . . . . . . . . . . . 14 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → ((𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥) ↔ (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
582577, 581imbi12d 344 . . . . . . . . . . . . 13 (𝑘 = (⌊‘((𝐵𝑋) / 𝑇)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥)) ↔ ((𝜑𝑥𝐷 ∧ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥))))
583582, 536vtoclg 3499 . . . . . . . . . . . 12 ((⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ → ((𝜑𝑥𝐷 ∧ (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
584572, 575, 583sylc 65 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))) = (𝐹𝑥))
585570, 584eqtrd 2771 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹𝑥))
586585adantlr 716 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐹‘(𝑥 + (𝑍𝑋))) = (𝐹𝑥))
587 simpr 484 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
588550, 551, 553, 555, 556, 566, 586, 587limcperiod 46058 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → 𝑦 ∈ ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) lim (𝑋 + (𝑍𝑋))))
589563reseq2d 5944 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) = (𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))))
590473adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
591589, 590oveq12d 7385 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) lim (𝑋 + (𝑍𝑋))) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
5925913adant3 1133 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) lim (𝑋 + (𝑍𝑋))) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
593592adantr 480 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → ((𝐹 ↾ {𝑧 ∈ ℂ ∣ ∃𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑧 = (𝑥 + (𝑍𝑋))}) lim (𝑋 + (𝑍𝑋))) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
594588, 593eleqtrd 2838 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)) → 𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
595548, 594impbida 801 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) ↔ 𝑦 ∈ ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋)))
596595eqrdv 2734 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
597 resindm 5995 . . . . . . . . . . 11 (Rel 𝐹 → (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)) = (𝐹 ↾ (-∞(,)𝑋)))
598597eqcomd 2742 . . . . . . . . . 10 (Rel 𝐹 → (𝐹 ↾ (-∞(,)𝑋)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)))
599176, 598syl 17 . . . . . . . . 9 (𝜑 → (𝐹 ↾ (-∞(,)𝑋)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)))
600181ineq2d 4160 . . . . . . . . . 10 (𝜑 → ((-∞(,)𝑋) ∩ dom 𝐹) = ((-∞(,)𝑋) ∩ 𝐷))
601600reseq2d 5944 . . . . . . . . 9 (𝜑 → (𝐹 ↾ ((-∞(,)𝑋) ∩ dom 𝐹)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)))
602599, 601eqtrd 2771 . . . . . . . 8 (𝜑 → (𝐹 ↾ (-∞(,)𝑋)) = (𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)))
603602oveq1d 7382 . . . . . . 7 (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) lim 𝑋))
6046033ad2ant1 1134 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) lim 𝑋))
605 inss2 4178 . . . . . . . . . 10 ((-∞(,)𝑋) ∩ 𝐷) ⊆ 𝐷
606605a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)𝑋) ∩ 𝐷) ⊆ 𝐷)
607190, 606fssresd 6707 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)):((-∞(,)𝑋) ∩ 𝐷)⟶ℂ)
608449mnfltd 13075 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ < ((𝑄𝑖) − (𝑍𝑋)))
609195, 450, 608xrltled 13101 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ≤ ((𝑄𝑖) − (𝑍𝑋)))
610 iooss1 13333 . . . . . . . . . . 11 ((-∞ ∈ ℝ* ∧ -∞ ≤ ((𝑄𝑖) − (𝑍𝑋))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ (-∞(,)𝑋))
611194, 609, 610sylancr 588 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ (-∞(,)𝑋))
6126113adant3 1133 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ (-∞(,)𝑋))
613612, 500ssind 4181 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ ((-∞(,)𝑋) ∩ 𝐷))
614605, 231sstrid 3933 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((-∞(,)𝑋) ∩ 𝐷) ⊆ ℂ)
615 eqid 2736 . . . . . . . 8 ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) = ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
6164503adant3 1133 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
6174523ad2ant1 1134 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ*)
6184723ad2ant1 1134 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
619238, 618breqtrd 5111 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝑋 + (𝑍𝑋)))
6204083ad2ant1 1134 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑍𝑋) ∈ ℝ)
621143ad2ant1 1134 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
622211, 620, 621ltsubaddd 11746 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋)) < 𝑋 ↔ (𝑄𝑖) < (𝑋 + (𝑍𝑋))))
623619, 622mpbird 257 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑋)
62414leidd 11716 . . . . . . . . . . 11 (𝜑𝑋𝑋)
6256243ad2ant1 1134 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋𝑋)
626616, 617, 617, 623, 625eliocd 45937 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
627 ioounsn 13430 . . . . . . . . . . . 12 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ* ∧ ((𝑄𝑖) − (𝑍𝑋)) < 𝑋) → ((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋}) = (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
628616, 617, 623, 627syl3anc 1374 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋}) = (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
629628fveq2d 6844 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋})) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘(((𝑄𝑖) − (𝑍𝑋))(,]𝑋)))
630 ovex 7400 . . . . . . . . . . . . . 14 (-∞(,)𝑋) ∈ V
631630inex1 5258 . . . . . . . . . . . . 13 ((-∞(,)𝑋) ∩ 𝐷) ∈ V
632 snex 5381 . . . . . . . . . . . . 13 {𝑋} ∈ V
633631, 632unex 7698 . . . . . . . . . . . 12 (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V
634 resttop 23125 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ∈ Top ∧ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V) → ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ Top)
635244, 633, 634mp2an 693 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ Top
636633a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V)
637 iooretop 24730 . . . . . . . . . . . . . 14 (((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∈ (topGen‘ran (,))
638637a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∈ (topGen‘ran (,)))
639 elrestr 17391 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ∈ Top ∧ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∈ V ∧ (((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∈ (topGen‘ran (,))) → ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
640252, 636, 638, 639syl3anc 1374 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
641450adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
642259a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → +∞ ∈ ℝ*)
64314ad2antrr 727 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑋 ∈ ℝ)
644 iocssre 13380 . . . . . . . . . . . . . . . . . . 19 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ⊆ ℝ)
645641, 643, 644syl2anc 585 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ⊆ ℝ)
646 simpr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
647645, 646sseldd 3922 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ ℝ)
648452ad2antrr 727 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑋 ∈ ℝ*)
649 iocgtlb 45932 . . . . . . . . . . . . . . . . . 18 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
650641, 648, 646, 649syl3anc 1374 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
651647ltpnfd 13072 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 < +∞)
652641, 642, 647, 650, 651eliood 45928 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞))
6536523adantl3 1170 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞))
654 eqvisset 3449 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑋𝑋 ∈ V)
655 snidg 4604 . . . . . . . . . . . . . . . . . . . 20 (𝑋 ∈ V → 𝑋 ∈ {𝑋})
656654, 655syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋𝑋 ∈ {𝑋})
657467, 656eqeltrd 2836 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋𝑥 ∈ {𝑋})
658 elun2 4123 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ {𝑋} → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
659657, 658syl 17 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
660659adantl 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ 𝑥 = 𝑋) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
661 simpll 767 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → (𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
662641adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
663452ad3antrrr 731 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑋 ∈ ℝ*)
664647adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ ℝ)
665650adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
66614ad3antrrr 731 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑋 ∈ ℝ)
667 iocleub 45933 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥𝑋)
668641, 648, 646, 667syl3anc 1374 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥𝑋)
669668adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥𝑋)
670467eqcoms 2744 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 = 𝑥𝑥 = 𝑋)
671670necon3bi 2958 . . . . . . . . . . . . . . . . . . . . 21 𝑥 = 𝑋𝑋𝑥)
672671adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑋𝑥)
673664, 666, 669, 672leneltd 11300 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 < 𝑋)
674662, 663, 664, 665, 673eliood 45928 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
6756743adantll3 45473 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
676613sselda 3921 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷))
677 elun1 4122 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
678676, 677syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
679661, 675, 678syl2anc 585 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) ∧ ¬ 𝑥 = 𝑋) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
680660, 679pm2.61dan 813 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
681653, 680elind 4140 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) → 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
682616adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
683617adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑋 ∈ ℝ*)
684 elinel1 4141 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞))
685 elioore 13328 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞) → 𝑥 ∈ ℝ)
686684, 685syl 17 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ ℝ)
687686rexrd 11195 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ ℝ*)
688687adantl 481 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ∈ ℝ*)
689450adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
690259a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → +∞ ∈ ℝ*)
691684adantl 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞))
692 ioogtlb 45925 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ* ∧ +∞ ∈ ℝ*𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)+∞)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
693689, 690, 691, 692syl3anc 1374 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
6946933adantl3 1170 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑥)
695 elinel2 4142 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))
696 elsni 4584 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {𝑋} → 𝑥 = 𝑋)
697696adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ {𝑋}) → 𝑥 = 𝑋)
698624adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ {𝑋}) → 𝑋𝑋)
699697, 698eqbrtrd 5107 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ {𝑋}) → 𝑥𝑋)
700699adantlr 716 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ 𝑥 ∈ {𝑋}) → 𝑥𝑋)
701 simpll 767 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝜑)
702 elunnel2 4095 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷))
703702adantll 715 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷))
704 elinel1 4141 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ((-∞(,)𝑋) ∩ 𝐷) → 𝑥 ∈ (-∞(,)𝑋))
705703, 704syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥 ∈ (-∞(,)𝑋))
706 elioore 13328 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (-∞(,)𝑋) → 𝑥 ∈ ℝ)
707706adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑥 ∈ ℝ)
70814adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑋 ∈ ℝ)
709194a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → -∞ ∈ ℝ*)
710452adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑋 ∈ ℝ*)
711 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑥 ∈ (-∞(,)𝑋))
712 iooltub 45940 . . . . . . . . . . . . . . . . . . . . 21 ((-∞ ∈ ℝ*𝑋 ∈ ℝ*𝑥 ∈ (-∞(,)𝑋)) → 𝑥 < 𝑋)
713709, 710, 711, 712syl3anc 1374 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑥 < 𝑋)
714707, 708, 713ltled 11294 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (-∞(,)𝑋)) → 𝑥𝑋)
715701, 705, 714syl2anc 585 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∧ ¬ 𝑥 ∈ {𝑋}) → 𝑥𝑋)
716700, 715pm2.61dan 813 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) → 𝑥𝑋)
717695, 716sylan2 594 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥𝑋)
7187173ad2antl1 1187 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥𝑋)
719682, 683, 688, 694, 718eliocd 45937 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → 𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
720681, 719impbida 801 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑥 ∈ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ↔ 𝑥 ∈ ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))))
721720eqrdv 2734 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) = ((((𝑄𝑖) − (𝑍𝑋))(,)+∞) ∩ (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
722605, 229sstrid 3933 . . . . . . . . . . . . . . 15 (𝜑 → ((-∞(,)𝑋) ∩ 𝐷) ⊆ ℝ)
72314snssd 4730 . . . . . . . . . . . . . . 15 (𝜑 → {𝑋} ⊆ ℝ)
724722, 723unssd 4132 . . . . . . . . . . . . . 14 (𝜑 → (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ⊆ ℝ)
7257243ad2ant1 1134 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ⊆ ℝ)
726233, 366rerest 24769 . . . . . . . . . . . . 13 ((((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) = ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
727725, 726syl 17 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) = ((topGen‘ran (,)) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
728640, 721, 7273eltr4d 2851 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))
729 isopn3i 23047 . . . . . . . . . . 11 ((((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})) ∈ Top ∧ (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) ∈ ((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋}))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘(((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) = (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
730635, 728, 729sylancr 588 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘(((𝑄𝑖) − (𝑍𝑋))(,]𝑋)) = (((𝑄𝑖) − (𝑍𝑋))(,]𝑋))
731629, 730eqtr2d 2772 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,]𝑋) = ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋})))
732626, 731eleqtrd 2838 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ((int‘((TopOpen‘ℂfld) ↾t (((-∞(,)𝑋) ∩ 𝐷) ∪ {𝑋})))‘((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ∪ {𝑋})))
733607, 613, 614, 233, 615, 732limcres 25853 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋) = ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) lim 𝑋))
734733eqcomd 2742 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) lim 𝑋) = (((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
735613resabs1d 5973 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) = (𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)))
736735oveq1d 7382 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((-∞(,)𝑋) ∩ 𝐷)) ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋))
737604, 734, 7363eqtrrd 2776 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋))
738377, 596, 7373eqtrrd 2776 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)))
739738rexlimdv3a 3142 . . 3 (𝜑 → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋))))
740173, 739mpd 15 . 2 (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) = ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)))
7411203adant3 1133 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
7422183adant3 1133 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
743 fourierdlem49.l . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
7447433adant3 1133 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
745 eqid 2736 . . . . . . . 8 if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋))) = if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋)))
746 eqid 2736 . . . . . . . 8 ((TopOpen‘ℂfld) ↾t (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))})) = ((TopOpen‘ℂfld) ↾t (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))}))
747211, 209, 741, 742, 744, 211, 235, 238, 217, 745, 746fourierdlem33 46568 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋))) ∈ (((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
748217resabs1d 5973 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) = (𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))))
749748oveq1d 7382 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
750747, 749eleqtrd 2838 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋))) ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)))
751 ne0i 4281 . . . . . 6 (if((𝐸𝑋) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝐸𝑋))) ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅)
752750, 751syl 17 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅)
753377, 752eqnetrd 2999 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (-∞(,)(𝐸𝑋))) lim (𝐸𝑋)) ≠ ∅)
754753rexlimdv3a 3142 . . 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 1087   = wceq 1542  wcel 2114  wne 2932  wral 3051  wrex 3061  {crab 3389  Vcvv 3429  cun 3887  cin 3888  wss 3889  c0 4273  ifcif 4466  {csn 4567   class class class wbr 5085  cmpt 5166  dom cdm 5631  ran crn 5632  cres 5633  Rel wrel 5636   Fn wfn 6493  wf 6494  cfv 6498  (class class class)co 7367  m cmap 8773  supcsup 9353  cc 11036  cr 11037  0cc0 11038  1c1 11039   + caddc 11041   · cmul 11043  +∞cpnf 11176  -∞cmnf 11177  *cxr 11178   < clt 11179  cle 11180  cmin 11377  -cneg 11378   / cdiv 11807  cn 12174  0cn0 12437  cz 12524  cuz 12788  (,)cioo 13298  (,]cioc 13299  [,]cicc 13301  ...cfz 13461  ..^cfzo 13608  cfl 13749  t crest 17383  TopOpenctopn 17384  topGenctg 17400  fldccnfld 21352  Topctop 22858  intcnt 22982  cnccncf 24843   lim climc 25829
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4851  df-int 4890  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-1st 7942  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-1o 8405  df-er 8643  df-map 8775  df-pm 8776  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-fi 9324  df-sup 9355  df-inf 9356  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-div 11808  df-nn 12175  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248  df-7 12249  df-8 12250  df-9 12251  df-n0 12438  df-z 12525  df-dec 12645  df-uz 12789  df-q 12899  df-rp 12943  df-xneg 13063  df-xadd 13064  df-xmul 13065  df-ioo 13302  df-ioc 13303  df-icc 13305  df-fz 13462  df-fzo 13609  df-fl 13751  df-seq 13964  df-exp 14024  df-cj 15061  df-re 15062  df-im 15063  df-sqrt 15197  df-abs 15198  df-struct 17117  df-slot 17152  df-ndx 17164  df-base 17180  df-plusg 17233  df-mulr 17234  df-starv 17235  df-tset 17239  df-ple 17240  df-ds 17242  df-unif 17243  df-rest 17385  df-topn 17386  df-topgen 17406  df-psmet 21344  df-xmet 21345  df-met 21346  df-bl 21347  df-mopn 21348  df-cnfld 21353  df-top 22859  df-topon 22876  df-topsp 22898  df-bases 22911  df-ntr 22985  df-cn 23192  df-cnp 23193  df-xms 24285  df-ms 24286  df-cncf 24845  df-limc 25833
This theorem is referenced by:  fourierdlem94  46628  fourierdlem113  46647
  Copyright terms: Public domain W3C validator