Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem41 Structured version   Visualization version   GIF version

Theorem fourierdlem41 42310
Description: Lemma used to prove that every real is a limit point for the domain of the derivative of the periodic function to be approximated. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem41.a (𝜑𝐴 ∈ ℝ)
fourierdlem41.b (𝜑𝐵 ∈ ℝ)
fourierdlem41.altb (𝜑𝐴 < 𝐵)
fourierdlem41.t 𝑇 = (𝐵𝐴)
fourierdlem41.dper ((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)
fourierdlem41.x (𝜑𝑋 ∈ ℝ)
fourierdlem41.z 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
fourierdlem41.e 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥)))
fourierdlem41.p 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem41.m (𝜑𝑀 ∈ ℕ)
fourierdlem41.q (𝜑𝑄 ∈ (𝑃𝑀))
fourierdlem41.qssd ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
Assertion
Ref Expression
fourierdlem41 (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ∧ ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))
Distinct variable groups:   𝐴,𝑚,𝑝   𝑥,𝐴   𝐵,𝑖,𝑘   𝐵,𝑚,𝑝,𝑖   𝑥,𝐵,𝑦,𝑘   𝐷,𝑖,𝑘,𝑦   𝑥,𝐷   𝑖,𝐸,𝑘,𝑦   𝑖,𝑀,𝑘   𝑚,𝑀,𝑝   𝑦,𝑀   𝑄,𝑖,𝑘   𝑄,𝑝   𝑦,𝑄   𝑇,𝑘,𝑥,𝑦   𝑖,𝑋,𝑘   𝑥,𝑋,𝑦   𝑘,𝑍,𝑥,𝑦   𝜑,𝑖,𝑘   𝜑,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑚,𝑝)   𝐴(𝑦,𝑖,𝑘)   𝐷(𝑚,𝑝)   𝑃(𝑥,𝑦,𝑖,𝑘,𝑚,𝑝)   𝑄(𝑥,𝑚)   𝑇(𝑖,𝑚,𝑝)   𝐸(𝑥,𝑚,𝑝)   𝑀(𝑥)   𝑋(𝑚,𝑝)   𝑍(𝑖,𝑚,𝑝)

Proof of Theorem fourierdlem41
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 simpr 485 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → (𝐸𝑋) ∈ ran 𝑄)
2 fourierdlem41.q . . . . . . . . . . 11 (𝜑𝑄 ∈ (𝑃𝑀))
3 fourierdlem41.m . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℕ)
4 fourierdlem41.p . . . . . . . . . . . . 13 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
54fourierdlem2 42271 . . . . . . . . . . . 12 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
63, 5syl 17 . . . . . . . . . . 11 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
72, 6mpbid 233 . . . . . . . . . 10 (𝜑 → (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
87simpld 495 . . . . . . . . 9 (𝜑𝑄 ∈ (ℝ ↑m (0...𝑀)))
9 elmapi 8417 . . . . . . . . 9 (𝑄 ∈ (ℝ ↑m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
10 ffn 6507 . . . . . . . . 9 (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
118, 9, 103syl 18 . . . . . . . 8 (𝜑𝑄 Fn (0...𝑀))
1211adantr 481 . . . . . . 7 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → 𝑄 Fn (0...𝑀))
13 fvelrnb 6719 . . . . . . 7 (𝑄 Fn (0...𝑀) → ((𝐸𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋)))
1412, 13syl 17 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → ((𝐸𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋)))
151, 14mpbid 233 . . . . 5 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋))
16 0zd 11981 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ∈ ℤ)
17 elfzelz 12896 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
18173ad2ant2 1126 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℤ)
19 1zzd 12001 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 1 ∈ ℤ)
2018, 19zsubcld 12080 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ ℤ)
21 simpll 763 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → 𝜑)
22 elfzle1 12898 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
2322anim1i 614 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → (0 ≤ 𝑗 ∧ ¬ 0 < 𝑗))
24 0red 10632 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 0 ∈ ℝ)
2517zred 12075 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
2625adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 𝑗 ∈ ℝ)
2724, 26eqleltd 10772 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → (0 = 𝑗 ↔ (0 ≤ 𝑗 ∧ ¬ 0 < 𝑗)))
2823, 27mpbird 258 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 0 = 𝑗)
2928eqcomd 2824 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 𝑗 = 0)
3029adantll 710 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → 𝑗 = 0)
31 fveq2 6663 . . . . . . . . . . . . . . . 16 (𝑗 = 0 → (𝑄𝑗) = (𝑄‘0))
327simprld 768 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵))
3332simpld 495 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘0) = 𝐴)
3431, 33sylan9eqr 2875 . . . . . . . . . . . . . . 15 ((𝜑𝑗 = 0) → (𝑄𝑗) = 𝐴)
3521, 30, 34syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → (𝑄𝑗) = 𝐴)
36353adantl3 1160 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄𝑗) = 𝐴)
37 simpr 485 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) = (𝐸𝑋))
38 fourierdlem41.a . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℝ)
3938rexrd 10679 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℝ*)
40 fourierdlem41.b . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 ∈ ℝ)
4140rexrd 10679 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ ℝ*)
42 fourierdlem41.altb . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐴 < 𝐵)
43 fourierdlem41.t . . . . . . . . . . . . . . . . . . . . . . 23 𝑇 = (𝐵𝐴)
44 eqid 2818 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
4538, 40, 42, 43, 44fourierdlem4 42273 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))):ℝ⟶(𝐴(,]𝐵))
46 fourierdlem41.e . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥)))
4746a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥))))
48 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
4940adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
5049, 48resubcld 11056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑥 ∈ ℝ) → (𝐵𝑥) ∈ ℝ)
5140, 38resubcld 11056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (𝐵𝐴) ∈ ℝ)
5243, 51eqeltrid 2914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝑇 ∈ ℝ)
5352adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
54 0red 10632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → 0 ∈ ℝ)
5538, 40posdifd 11215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
5642, 55mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → 0 < (𝐵𝐴))
5743eqcomi 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝐵𝐴) = 𝑇
5857a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → (𝐵𝐴) = 𝑇)
5956, 58breqtrd 5083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → 0 < 𝑇)
6054, 59gtned 10763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝑇 ≠ 0)
6160adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑥 ∈ ℝ) → 𝑇 ≠ 0)
6250, 53, 61redivcld 11456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑥 ∈ ℝ) → ((𝐵𝑥) / 𝑇) ∈ ℝ)
6362flcld 13156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑥 ∈ ℝ) → (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℤ)
6463zred 12075 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑥 ∈ ℝ) → (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℝ)
6564, 53remulcld 10659 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥 ∈ ℝ) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
66 fourierdlem41.z . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
6766fvmpt2 6771 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℝ ∧ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ ℝ) → (𝑍𝑥) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
6848, 65, 67syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑥 ∈ ℝ) → (𝑍𝑥) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
6968oveq2d 7161 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥 ∈ ℝ) → (𝑥 + (𝑍𝑥)) = (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
7069mpteq2dva 5152 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))))
7147, 70eqtrd 2853 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))))
7271feq1d 6492 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐸:ℝ⟶(𝐴(,]𝐵) ↔ (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))):ℝ⟶(𝐴(,]𝐵)))
7345, 72mpbird 258 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))
74 fourierdlem41.x . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑋 ∈ ℝ)
7573, 74ffvelrnd 6844 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐸𝑋) ∈ (𝐴(,]𝐵))
76 iocgtlb 41653 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸𝑋))
7739, 41, 75, 76syl3anc 1363 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 < (𝐸𝑋))
7838, 77gtned 10763 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐸𝑋) ≠ 𝐴)
7978adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≠ 𝐴)
8037, 79eqnetrd 3080 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ≠ 𝐴)
8180adantr 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄𝑗) ≠ 𝐴)
82813adantl2 1159 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄𝑗) ≠ 𝐴)
8382neneqd 3018 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ ¬ 0 < 𝑗) → ¬ (𝑄𝑗) = 𝐴)
8436, 83condan 814 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 < 𝑗)
85 zltlem1 12023 . . . . . . . . . . . . 13 ((0 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (0 < 𝑗 ↔ 0 ≤ (𝑗 − 1)))
8616, 18, 85syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 < 𝑗 ↔ 0 ≤ (𝑗 − 1)))
8784, 86mpbid 233 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ≤ (𝑗 − 1))
88 eluz2 12237 . . . . . . . . . . 11 ((𝑗 − 1) ∈ (ℤ‘0) ↔ (0 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ ∧ 0 ≤ (𝑗 − 1)))
8916, 20, 87, 88syl3anbrc 1335 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (ℤ‘0))
90 elfzel2 12894 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
91903ad2ant2 1126 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑀 ∈ ℤ)
92 1red 10630 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 1 ∈ ℝ)
9325, 92resubcld 11056 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
9490zred 12075 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
9525ltm1d 11560 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑗)
96 elfzle2 12899 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → 𝑗𝑀)
9793, 25, 94, 95, 96ltletrd 10788 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
98973ad2ant2 1126 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) < 𝑀)
99 elfzo2 13029 . . . . . . . . . 10 ((𝑗 − 1) ∈ (0..^𝑀) ↔ ((𝑗 − 1) ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) < 𝑀))
10089, 91, 98, 99syl3anbrc 1335 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (0..^𝑀))
1018, 9syl 17 . . . . . . . . . . . . 13 (𝜑𝑄:(0...𝑀)⟶ℝ)
1021013ad2ant1 1125 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑄:(0...𝑀)⟶ℝ)
10316, 91, 203jca 1120 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ))
10493, 94, 97ltled 10776 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ≤ 𝑀)
1051043ad2ant2 1126 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ≤ 𝑀)
106103, 87, 105jca32 516 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ) ∧ (0 ≤ (𝑗 − 1) ∧ (𝑗 − 1) ≤ 𝑀)))
107 elfz2 12887 . . . . . . . . . . . . 13 ((𝑗 − 1) ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ) ∧ (0 ≤ (𝑗 − 1) ∧ (𝑗 − 1) ≤ 𝑀)))
108106, 107sylibr 235 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (0...𝑀))
109102, 108ffvelrnd 6844 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ)
110109rexrd 10679 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ*)
11125recnd 10657 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
112 1cnd 10624 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 1 ∈ ℂ)
113111, 112npcand 10989 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → ((𝑗 − 1) + 1) = 𝑗)
114113fveq2d 6667 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
115114adantl 482 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
116101ffvelrnda 6843 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ)
117116rexrd 10679 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ*)
118115, 117eqeltrd 2910 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄‘((𝑗 − 1) + 1)) ∈ ℝ*)
1191183adant3 1124 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘((𝑗 − 1) + 1)) ∈ ℝ*)
120 id 22 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋𝑥 = 𝑋)
121 fveq2 6663 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (𝑍𝑥) = (𝑍𝑋))
122120, 121oveq12d 7163 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → (𝑥 + (𝑍𝑥)) = (𝑋 + (𝑍𝑋)))
123122adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑥 = 𝑋) → (𝑥 + (𝑍𝑥)) = (𝑋 + (𝑍𝑋)))
12466a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
125 oveq2 7153 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑋 → (𝐵𝑥) = (𝐵𝑋))
126125oveq1d 7160 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑋 → ((𝐵𝑥) / 𝑇) = ((𝐵𝑋) / 𝑇))
127126fveq2d 6667 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋 → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵𝑋) / 𝑇)))
128127oveq1d 7160 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋 → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
129128adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 = 𝑋) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
13040, 74resubcld 11056 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵𝑋) ∈ ℝ)
131130, 52, 60redivcld 11456 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐵𝑋) / 𝑇) ∈ ℝ)
132131flcld 13156 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
133132zred 12075 . . . . . . . . . . . . . . . . . 18 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℝ)
134133, 52remulcld 10659 . . . . . . . . . . . . . . . . 17 (𝜑 → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
135124, 129, 74, 134fvmptd 6767 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑍𝑋) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
136135, 134eqeltrd 2910 . . . . . . . . . . . . . . 15 (𝜑 → (𝑍𝑋) ∈ ℝ)
13774, 136readdcld 10658 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 + (𝑍𝑋)) ∈ ℝ)
13847, 123, 74, 137fvmptd 6767 . . . . . . . . . . . . 13 (𝜑 → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
139138, 137eqeltrd 2910 . . . . . . . . . . . 12 (𝜑 → (𝐸𝑋) ∈ ℝ)
140139rexrd 10679 . . . . . . . . . . 11 (𝜑 → (𝐸𝑋) ∈ ℝ*)
1411403ad2ant1 1125 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ*)
142 simp1 1128 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝜑)
143 ovex 7178 . . . . . . . . . . . . . 14 (𝑗 − 1) ∈ V
144 eleq1 2897 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 − 1) → (𝑖 ∈ (0..^𝑀) ↔ (𝑗 − 1) ∈ (0..^𝑀)))
145144anbi2d 628 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗 − 1) → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀))))
146 fveq2 6663 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 − 1) → (𝑄𝑖) = (𝑄‘(𝑗 − 1)))
147 oveq1 7152 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 − 1) → (𝑖 + 1) = ((𝑗 − 1) + 1))
148147fveq2d 6667 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 − 1) → (𝑄‘(𝑖 + 1)) = (𝑄‘((𝑗 − 1) + 1)))
149146, 148breq12d 5070 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗 − 1) → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1))))
150145, 149imbi12d 346 . . . . . . . . . . . . . 14 (𝑖 = (𝑗 − 1) → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))))
1517simprrd 770 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))
152151r19.21bi 3205 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
153143, 150, 152vtocl 3557 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
154142, 100, 153syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
1551143ad2ant2 1126 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
156154, 155breqtrd 5083 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄𝑗))
157 simp3 1130 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) = (𝐸𝑋))
158156, 157breqtrd 5083 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝐸𝑋))
159139leidd 11194 . . . . . . . . . . . . . 14 (𝜑 → (𝐸𝑋) ≤ (𝐸𝑋))
160159adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝐸𝑋))
16137eqcomd 2824 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) = (𝑄𝑗))
162160, 161breqtrd 5083 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄𝑗))
1631623adant2 1123 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄𝑗))
164113eqcomd 2824 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗 = ((𝑗 − 1) + 1))
165164fveq2d 6667 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑄𝑗) = (𝑄‘((𝑗 − 1) + 1)))
1661653ad2ant2 1126 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) = (𝑄‘((𝑗 − 1) + 1)))
167163, 166breqtrd 5083 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄‘((𝑗 − 1) + 1)))
168110, 119, 141, 158, 167eliocd 41659 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
169146, 148oveq12d 7163 . . . . . . . . . . 11 (𝑖 = (𝑗 − 1) → ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
170169eleq2d 2895 . . . . . . . . . 10 (𝑖 = (𝑗 − 1) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) ↔ (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))))
171170rspcev 3620 . . . . . . . . 9 (((𝑗 − 1) ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
172100, 168, 171syl2anc 584 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
1731723exp 1111 . . . . . . 7 (𝜑 → (𝑗 ∈ (0...𝑀) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))))
174173adantr 481 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → (𝑗 ∈ (0...𝑀) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))))
175174rexlimdv 3280 . . . . 5 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
17615, 175mpd 15 . . . 4 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
1773adantr 481 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → 𝑀 ∈ ℕ)
178101adantr 481 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ)
179 iocssicc 12813 . . . . . . . 8 ((𝑄‘0)(,](𝑄𝑀)) ⊆ ((𝑄‘0)[,](𝑄𝑀))
18032simprd 496 . . . . . . . . . 10 (𝜑 → (𝑄𝑀) = 𝐵)
18133, 180oveq12d 7163 . . . . . . . . 9 (𝜑 → ((𝑄‘0)(,](𝑄𝑀)) = (𝐴(,]𝐵))
18275, 181eleqtrrd 2913 . . . . . . . 8 (𝜑 → (𝐸𝑋) ∈ ((𝑄‘0)(,](𝑄𝑀)))
183179, 182sseldi 3962 . . . . . . 7 (𝜑 → (𝐸𝑋) ∈ ((𝑄‘0)[,](𝑄𝑀)))
184183adantr 481 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (𝐸𝑋) ∈ ((𝑄‘0)[,](𝑄𝑀)))
185 simpr 485 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ¬ (𝐸𝑋) ∈ ran 𝑄)
186 fveq2 6663 . . . . . . . . 9 (𝑘 = 𝑗 → (𝑄𝑘) = (𝑄𝑗))
187186breq1d 5067 . . . . . . . 8 (𝑘 = 𝑗 → ((𝑄𝑘) < (𝐸𝑋) ↔ (𝑄𝑗) < (𝐸𝑋)))
188187cbvrabv 3489 . . . . . . 7 {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < (𝐸𝑋)} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < (𝐸𝑋)}
189188supeq1i 8899 . . . . . 6 sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < (𝐸𝑋)}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < (𝐸𝑋)}, ℝ, < )
190177, 178, 184, 185, 189fourierdlem25 42294 . . . . 5 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
191 ioossioc 41642 . . . . . . . 8 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))
192191a1i 11 . . . . . . 7 (((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
193192sseld 3963 . . . . . 6 (((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
194193reximdva 3271 . . . . 5 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
195190, 194mpd 15 . . . 4 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
196176, 195pm2.61dan 809 . . 3 (𝜑 → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
197101adantr 481 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
198 elfzofz 13041 . . . . . . . . . 10 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
199198adantl 482 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
200197, 199ffvelrnd 6844 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
2012003adant3 1124 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
2021363ad2ant1 1125 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑍𝑋) ∈ ℝ)
203201, 202resubcld 11056 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ)
2041393ad2ant1 1125 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ℝ)
205201rexrd 10679 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ*)
206 fzofzp1 13122 . . . . . . . . . . . . 13 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
207206adantl 482 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
208197, 207ffvelrnd 6844 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
209208rexrd 10679 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
2102093adant3 1124 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
211 simp3 1130 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
212 iocgtlb 41653 . . . . . . . . 9 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝐸𝑋))
213205, 210, 211, 212syl3anc 1363 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝐸𝑋))
214201, 204, 202, 213ltsub1dd 11240 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) < ((𝐸𝑋) − (𝑍𝑋)))
215138oveq1d 7160 . . . . . . . . 9 (𝜑 → ((𝐸𝑋) − (𝑍𝑋)) = ((𝑋 + (𝑍𝑋)) − (𝑍𝑋)))
21674recnd 10657 . . . . . . . . . 10 (𝜑𝑋 ∈ ℂ)
217136recnd 10657 . . . . . . . . . 10 (𝜑 → (𝑍𝑋) ∈ ℂ)
218216, 217pncand 10986 . . . . . . . . 9 (𝜑 → ((𝑋 + (𝑍𝑋)) − (𝑍𝑋)) = 𝑋)
219215, 218eqtrd 2853 . . . . . . . 8 (𝜑 → ((𝐸𝑋) − (𝑍𝑋)) = 𝑋)
2202193ad2ant1 1125 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐸𝑋) − (𝑍𝑋)) = 𝑋)
221214, 220breqtrd 5083 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑋)
222 elioore 12756 . . . . . . . . . . 11 (𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) → 𝑦 ∈ ℝ)
223135oveq2d 7161 . . . . . . . . . . . . . 14 (𝜑 → (𝑦 + (𝑍𝑋)) = (𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
224133recnd 10657 . . . . . . . . . . . . . . 15 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℂ)
22552recnd 10657 . . . . . . . . . . . . . . 15 (𝜑𝑇 ∈ ℂ)
226224, 225mulneg1d 11081 . . . . . . . . . . . . . 14 (𝜑 → (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
227223, 226oveq12d 7163 . . . . . . . . . . . . 13 (𝜑 → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
228227adantr 481 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
229 simpr 485 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
230134adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
231229, 230readdcld 10658 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → (𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ ℝ)
232231recnd 10657 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → (𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ ℂ)
233230recnd 10657 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
234232, 233negsubd 10991 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
235229recnd 10657 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
236235, 233pncand 10986 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = 𝑦)
237228, 234, 2363eqtrrd 2858 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
238222, 237sylan2 592 . . . . . . . . . 10 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
2392383ad2antl1 1177 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
240 simpl1 1183 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝜑)
241 fourierdlem41.qssd . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
2422413adant3 1124 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
243242adantr 481 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
244205adantr 481 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) ∈ ℝ*)
245210adantr 481 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
246222adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
247136adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℝ)
248246, 247readdcld 10658 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
2492483ad2antl1 1177 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
250136adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑍𝑋) ∈ ℝ)
251200, 250resubcld 11056 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ)
252251rexrd 10679 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
253252adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
25474rexrd 10679 . . . . . . . . . . . . . . . 16 (𝜑𝑋 ∈ ℝ*)
255254ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑋 ∈ ℝ*)
256 simpr 485 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
257 ioogtlb 41646 . . . . . . . . . . . . . . 15 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑦)
258253, 255, 256, 257syl3anc 1363 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑦)
259200adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) ∈ ℝ)
260136ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℝ)
261222adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
262259, 260, 261ltsubaddd 11224 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (((𝑄𝑖) − (𝑍𝑋)) < 𝑦 ↔ (𝑄𝑖) < (𝑦 + (𝑍𝑋))))
263258, 262mpbid 233 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) < (𝑦 + (𝑍𝑋)))
2642633adantl3 1160 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) < (𝑦 + (𝑍𝑋)))
265240, 139syl 17 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐸𝑋) ∈ ℝ)
266208adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
2672663adantl3 1160 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
26874ad2antrr 722 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑋 ∈ ℝ)
269 iooltub 41662 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 < 𝑋)
270253, 255, 256, 269syl3anc 1363 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 < 𝑋)
271261, 268, 260, 270ltadd1dd 11239 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝑋 + (𝑍𝑋)))
272138eqcomd 2824 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
273272ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
274271, 273breqtrd 5083 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝐸𝑋))
2752743adantl3 1160 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝐸𝑋))
276 iocleub 41654 . . . . . . . . . . . . . . 15 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
277205, 210, 211, 276syl3anc 1363 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
278277adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
279249, 265, 267, 275, 278ltletrd 10788 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝑄‘(𝑖 + 1)))
280244, 245, 249, 264, 279eliood 41649 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
281243, 280sseldd 3965 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ 𝐷)
282240, 131syl 17 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝐵𝑋) / 𝑇) ∈ ℝ)
283282flcld 13156 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
284283znegcld 12077 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
285 negex 10872 . . . . . . . . . . 11 -(⌊‘((𝐵𝑋) / 𝑇)) ∈ V
286 eleq1 2897 . . . . . . . . . . . . 13 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
2872863anbi3d 1433 . . . . . . . . . . . 12 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)))
288 oveq1 7152 . . . . . . . . . . . . . 14 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 · 𝑇) = (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
289288oveq2d 7161 . . . . . . . . . . . . 13 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
290289eleq1d 2894 . . . . . . . . . . . 12 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
291287, 290imbi12d 346 . . . . . . . . . . 11 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)))
292 ovex 7178 . . . . . . . . . . . 12 (𝑦 + (𝑍𝑋)) ∈ V
293 eleq1 2897 . . . . . . . . . . . . . 14 (𝑥 = (𝑦 + (𝑍𝑋)) → (𝑥𝐷 ↔ (𝑦 + (𝑍𝑋)) ∈ 𝐷))
2942933anbi2d 1432 . . . . . . . . . . . . 13 (𝑥 = (𝑦 + (𝑍𝑋)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ)))
295 oveq1 7152 . . . . . . . . . . . . . 14 (𝑥 = (𝑦 + (𝑍𝑋)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)))
296295eleq1d 2894 . . . . . . . . . . . . 13 (𝑥 = (𝑦 + (𝑍𝑋)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷))
297294, 296imbi12d 346 . . . . . . . . . . . 12 (𝑥 = (𝑦 + (𝑍𝑋)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)))
298 fourierdlem41.dper . . . . . . . . . . . 12 ((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)
299292, 297, 298vtocl 3557 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)
300285, 291, 299vtocl 3557 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
301240, 281, 284, 300syl3anc 1363 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
302239, 301eqeltrd 2910 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦𝐷)
303302ralrimiva 3179 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑦𝐷)
304 dfss3 3953 . . . . . . 7 ((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷 ↔ ∀𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑦𝐷)
305303, 304sylibr 235 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷)
306 breq1 5060 . . . . . . . 8 (𝑦 = ((𝑄𝑖) − (𝑍𝑋)) → (𝑦 < 𝑋 ↔ ((𝑄𝑖) − (𝑍𝑋)) < 𝑋))
307 oveq1 7152 . . . . . . . . 9 (𝑦 = ((𝑄𝑖) − (𝑍𝑋)) → (𝑦(,)𝑋) = (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
308307sseq1d 3995 . . . . . . . 8 (𝑦 = ((𝑄𝑖) − (𝑍𝑋)) → ((𝑦(,)𝑋) ⊆ 𝐷 ↔ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷))
309306, 308anbi12d 630 . . . . . . 7 (𝑦 = ((𝑄𝑖) − (𝑍𝑋)) → ((𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ↔ (((𝑄𝑖) − (𝑍𝑋)) < 𝑋 ∧ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷)))
310309rspcev 3620 . . . . . 6 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ ∧ (((𝑄𝑖) − (𝑍𝑋)) < 𝑋 ∧ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
311203, 221, 305, 310syl12anc 832 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
3123113exp 1111 . . . 4 (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))))
313312rexlimdv 3280 . . 3 (𝜑 → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷)))
314196, 313mpd 15 . 2 (𝜑 → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
315 0zd 11981 . . . . . . . . . 10 (𝜑 → 0 ∈ ℤ)
3163nnzd 12074 . . . . . . . . . 10 (𝜑𝑀 ∈ ℤ)
317 1zzd 12001 . . . . . . . . . 10 (𝜑 → 1 ∈ ℤ)
318315, 316, 3173jca 1120 . . . . . . . . 9 (𝜑 → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 1 ∈ ℤ))
319 0le1 11151 . . . . . . . . . 10 0 ≤ 1
320319a1i 11 . . . . . . . . 9 (𝜑 → 0 ≤ 1)
3213nnge1d 11673 . . . . . . . . 9 (𝜑 → 1 ≤ 𝑀)
322318, 320, 321jca32 516 . . . . . . . 8 (𝜑 → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 1 ∈ ℤ) ∧ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
323 elfz2 12887 . . . . . . . 8 (1 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 1 ∈ ℤ) ∧ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
324322, 323sylibr 235 . . . . . . 7 (𝜑 → 1 ∈ (0...𝑀))
325101, 324ffvelrnd 6844 . . . . . 6 (𝜑 → (𝑄‘1) ∈ ℝ)
326136, 52resubcld 11056 . . . . . 6 (𝜑 → ((𝑍𝑋) − 𝑇) ∈ ℝ)
327325, 326resubcld 11056 . . . . 5 (𝜑 → ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ)
328327adantr 481 . . . 4 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ)
32938recnd 10657 . . . . . . . . . 10 (𝜑𝐴 ∈ ℂ)
330329, 225pncand 10986 . . . . . . . . 9 (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
331330adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
33243oveq2i 7156 . . . . . . . . . . 11 (𝐴 + 𝑇) = (𝐴 + (𝐵𝐴))
333332a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝐴 + 𝑇) = (𝐴 + (𝐵𝐴)))
33440recnd 10657 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℂ)
335329, 334pncan3d 10988 . . . . . . . . . . 11 (𝜑 → (𝐴 + (𝐵𝐴)) = 𝐵)
336335adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝐴 + (𝐵𝐴)) = 𝐵)
337 id 22 . . . . . . . . . . . 12 ((𝐸𝑋) = 𝐵 → (𝐸𝑋) = 𝐵)
338337eqcomd 2824 . . . . . . . . . . 11 ((𝐸𝑋) = 𝐵𝐵 = (𝐸𝑋))
339338adantl 482 . . . . . . . . . 10 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → 𝐵 = (𝐸𝑋))
340333, 336, 3393eqtrrd 2858 . . . . . . . . 9 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝐸𝑋) = (𝐴 + 𝑇))
341340oveq1d 7160 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝐸𝑋) − 𝑇) = ((𝐴 + 𝑇) − 𝑇))
34233adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑄‘0) = 𝐴)
343331, 341, 3423eqtr4rd 2864 . . . . . . 7 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑄‘0) = ((𝐸𝑋) − 𝑇))
344343oveq1d 7160 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑄‘0) − ((𝑍𝑋) − 𝑇)) = (((𝐸𝑋) − 𝑇) − ((𝑍𝑋) − 𝑇)))
345139recnd 10657 . . . . . . . 8 (𝜑 → (𝐸𝑋) ∈ ℂ)
346345, 217, 225nnncan2d 11020 . . . . . . 7 (𝜑 → (((𝐸𝑋) − 𝑇) − ((𝑍𝑋) − 𝑇)) = ((𝐸𝑋) − (𝑍𝑋)))
347346adantr 481 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (((𝐸𝑋) − 𝑇) − ((𝑍𝑋) − 𝑇)) = ((𝐸𝑋) − (𝑍𝑋)))
348219adantr 481 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝐸𝑋) − (𝑍𝑋)) = 𝑋)
349344, 347, 3483eqtrrd 2858 . . . . 5 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → 𝑋 = ((𝑄‘0) − ((𝑍𝑋) − 𝑇)))
35033, 38eqeltrd 2910 . . . . . . 7 (𝜑 → (𝑄‘0) ∈ ℝ)
3513nngt0d 11674 . . . . . . . . . 10 (𝜑 → 0 < 𝑀)
352 fzolb 13032 . . . . . . . . . 10 (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
353315, 316, 351, 352syl3anbrc 1335 . . . . . . . . 9 (𝜑 → 0 ∈ (0..^𝑀))
354 0re 10631 . . . . . . . . . 10 0 ∈ ℝ
355 eleq1 2897 . . . . . . . . . . . . 13 (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀)))
356355anbi2d 628 . . . . . . . . . . . 12 (𝑖 = 0 → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀))))
357 fveq2 6663 . . . . . . . . . . . . 13 (𝑖 = 0 → (𝑄𝑖) = (𝑄‘0))
358 oveq1 7152 . . . . . . . . . . . . . 14 (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
359358fveq2d 6667 . . . . . . . . . . . . 13 (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1)))
360357, 359breq12d 5070 . . . . . . . . . . . 12 (𝑖 = 0 → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1))))
361356, 360imbi12d 346 . . . . . . . . . . 11 (𝑖 = 0 → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))))
362361, 152vtoclg 3565 . . . . . . . . . 10 (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))
363354, 362ax-mp 5 . . . . . . . . 9 ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))
364353, 363mpdan 683 . . . . . . . 8 (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1)))
365 0p1e1 11747 . . . . . . . . . 10 (0 + 1) = 1
366365fveq2i 6666 . . . . . . . . 9 (𝑄‘(0 + 1)) = (𝑄‘1)
367366a1i 11 . . . . . . . 8 (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1))
368364, 367breqtrd 5083 . . . . . . 7 (𝜑 → (𝑄‘0) < (𝑄‘1))
369350, 325, 326, 368ltsub1dd 11240 . . . . . 6 (𝜑 → ((𝑄‘0) − ((𝑍𝑋) − 𝑇)) < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
370369adantr 481 . . . . 5 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑄‘0) − ((𝑍𝑋) − 𝑇)) < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
371349, 370eqbrtrd 5079 . . . 4 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → 𝑋 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
372 elioore 12756 . . . . . . . . 9 (𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) → 𝑦 ∈ ℝ)
373135eqcomd 2824 . . . . . . . . . . . . . . . 16 (𝜑 → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = (𝑍𝑋))
374373negeqd 10868 . . . . . . . . . . . . . . 15 (𝜑 → -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = -(𝑍𝑋))
375226, 374eqtrd 2853 . . . . . . . . . . . . . 14 (𝜑 → (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = -(𝑍𝑋))
376225mulid2d 10647 . . . . . . . . . . . . . 14 (𝜑 → (1 · 𝑇) = 𝑇)
377375, 376oveq12d 7163 . . . . . . . . . . . . 13 (𝜑 → ((-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) + (1 · 𝑇)) = (-(𝑍𝑋) + 𝑇))
378224negcld 10972 . . . . . . . . . . . . . 14 (𝜑 → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℂ)
379 1cnd 10624 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℂ)
380378, 379, 225adddird 10654 . . . . . . . . . . . . 13 (𝜑 → ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇) = ((-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) + (1 · 𝑇)))
381217, 225negsubdid 11000 . . . . . . . . . . . . 13 (𝜑 → -((𝑍𝑋) − 𝑇) = (-(𝑍𝑋) + 𝑇))
382377, 380, 3813eqtr4d 2863 . . . . . . . . . . . 12 (𝜑 → ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇) = -((𝑍𝑋) − 𝑇))
383382oveq2d 7161 . . . . . . . . . . 11 (𝜑 → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) + -((𝑍𝑋) − 𝑇)))
384383adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) + -((𝑍𝑋) − 𝑇)))
385326adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → ((𝑍𝑋) − 𝑇) ∈ ℝ)
386229, 385readdcld 10658 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ℝ)
387386recnd 10657 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ℂ)
388385recnd 10657 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → ((𝑍𝑋) − 𝑇) ∈ ℂ)
389387, 388negsubd 10991 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + -((𝑍𝑋) − 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) − ((𝑍𝑋) − 𝑇)))
390235, 388pncand 10986 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) − ((𝑍𝑋) − 𝑇)) = 𝑦)
391384, 389, 3903eqtrrd 2858 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → 𝑦 = ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)))
392372, 391sylan2 592 . . . . . . . 8 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 = ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)))
393392adantlr 711 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 = ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)))
394 simpll 763 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝜑)
395367eqcomd 2824 . . . . . . . . . . . 12 (𝜑 → (𝑄‘1) = (𝑄‘(0 + 1)))
396395oveq2d 7161 . . . . . . . . . . 11 (𝜑 → ((𝑄‘0)(,)(𝑄‘1)) = ((𝑄‘0)(,)(𝑄‘(0 + 1))))
397357, 359oveq12d 7163 . . . . . . . . . . . . . . . 16 (𝑖 = 0 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘0)(,)(𝑄‘(0 + 1))))
398397sseq1d 3995 . . . . . . . . . . . . . . 15 (𝑖 = 0 → (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷 ↔ ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷))
399356, 398imbi12d 346 . . . . . . . . . . . . . 14 (𝑖 = 0 → (((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)))
400399, 241vtoclg 3565 . . . . . . . . . . . . 13 (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷))
401354, 400ax-mp 5 . . . . . . . . . . . 12 ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)
402353, 401mpdan 683 . . . . . . . . . . 11 (𝜑 → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)
403396, 402eqsstrd 4002 . . . . . . . . . 10 (𝜑 → ((𝑄‘0)(,)(𝑄‘1)) ⊆ 𝐷)
404403ad2antrr 722 . . . . . . . . 9 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑄‘0)(,)(𝑄‘1)) ⊆ 𝐷)
40533, 39eqeltrd 2910 . . . . . . . . . . 11 (𝜑 → (𝑄‘0) ∈ ℝ*)
406405ad2antrr 722 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘0) ∈ ℝ*)
407325rexrd 10679 . . . . . . . . . . 11 (𝜑 → (𝑄‘1) ∈ ℝ*)
408407ad2antrr 722 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘1) ∈ ℝ*)
409372, 386sylan2 592 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ℝ)
410409adantlr 711 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ℝ)
411345, 216, 217subaddd 11003 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐸𝑋) − 𝑋) = (𝑍𝑋) ↔ (𝑋 + (𝑍𝑋)) = (𝐸𝑋)))
412272, 411mpbird 258 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸𝑋) − 𝑋) = (𝑍𝑋))
413 oveq1 7152 . . . . . . . . . . . . . . . 16 ((𝐸𝑋) = 𝐵 → ((𝐸𝑋) − 𝑋) = (𝐵𝑋))
414412, 413sylan9req 2874 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑍𝑋) = (𝐵𝑋))
415414oveq1d 7160 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑍𝑋) − 𝑇) = ((𝐵𝑋) − 𝑇))
416415oveq2d 7161 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑋 + ((𝑍𝑋) − 𝑇)) = (𝑋 + ((𝐵𝑋) − 𝑇)))
417130recnd 10657 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵𝑋) ∈ ℂ)
418216, 417, 225addsubassd 11005 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑋 + (𝐵𝑋)) − 𝑇) = (𝑋 + ((𝐵𝑋) − 𝑇)))
419418eqcomd 2824 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 + ((𝐵𝑋) − 𝑇)) = ((𝑋 + (𝐵𝑋)) − 𝑇))
420419adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑋 + ((𝐵𝑋) − 𝑇)) = ((𝑋 + (𝐵𝑋)) − 𝑇))
421334, 225, 329subsub23d 41429 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵𝑇) = 𝐴 ↔ (𝐵𝐴) = 𝑇))
42258, 421mpbird 258 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵𝑇) = 𝐴)
423216, 334pncan3d 10988 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋 + (𝐵𝑋)) = 𝐵)
424423oveq1d 7160 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑋 + (𝐵𝑋)) − 𝑇) = (𝐵𝑇))
425422, 424, 333eqtr4d 2863 . . . . . . . . . . . . . 14 (𝜑 → ((𝑋 + (𝐵𝑋)) − 𝑇) = (𝑄‘0))
426425adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑋 + (𝐵𝑋)) − 𝑇) = (𝑄‘0))
427416, 420, 4263eqtrrd 2858 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑄‘0) = (𝑋 + ((𝑍𝑋) − 𝑇)))
428427adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘0) = (𝑋 + ((𝑍𝑋) − 𝑇)))
42974adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑋 ∈ ℝ)
430372adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 ∈ ℝ)
431326adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑍𝑋) − 𝑇) ∈ ℝ)
432254adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑋 ∈ ℝ*)
433327rexrd 10679 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ*)
434433adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ*)
435 simpr 485 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))))
436 ioogtlb 41646 . . . . . . . . . . . . . 14 ((𝑋 ∈ ℝ* ∧ ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ*𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑋 < 𝑦)
437432, 434, 435, 436syl3anc 1363 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑋 < 𝑦)
438429, 430, 431, 437ltadd1dd 11239 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑋 + ((𝑍𝑋) − 𝑇)) < (𝑦 + ((𝑍𝑋) − 𝑇)))
439438adantlr 711 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑋 + ((𝑍𝑋) − 𝑇)) < (𝑦 + ((𝑍𝑋) − 𝑇)))
440428, 439eqbrtrd 5079 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘0) < (𝑦 + ((𝑍𝑋) − 𝑇)))
441 iooltub 41662 . . . . . . . . . . . . 13 ((𝑋 ∈ ℝ* ∧ ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ*𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
442432, 434, 435, 441syl3anc 1363 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
443325adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘1) ∈ ℝ)
444430, 431, 443ltaddsubd 11228 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑦 + ((𝑍𝑋) − 𝑇)) < (𝑄‘1) ↔ 𝑦 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇))))
445442, 444mpbird 258 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) < (𝑄‘1))
446445adantlr 711 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) < (𝑄‘1))
447406, 408, 410, 440, 446eliood 41649 . . . . . . . . 9 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ((𝑄‘0)(,)(𝑄‘1)))
448404, 447sseldd 3965 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷)
449132znegcld 12077 . . . . . . . . . 10 (𝜑 → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
450449peano2zd 12078 . . . . . . . . 9 (𝜑 → (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ)
451450ad2antrr 722 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ)
452 ovex 7178 . . . . . . . . 9 (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ V
453 eleq1 2897 . . . . . . . . . . 11 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → (𝑘 ∈ ℤ ↔ (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ))
4544533anbi3d 1433 . . . . . . . . . 10 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ)))
455 oveq1 7152 . . . . . . . . . . . 12 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → (𝑘 · 𝑇) = ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇))
456455oveq2d 7161 . . . . . . . . . . 11 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)))
457456eleq1d 2894 . . . . . . . . . 10 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → (((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷))
458454, 457imbi12d 346 . . . . . . . . 9 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → (((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)))
459 ovex 7178 . . . . . . . . . 10 (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ V
460 eleq1 2897 . . . . . . . . . . . 12 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → (𝑥𝐷 ↔ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷))
4614603anbi2d 1432 . . . . . . . . . . 11 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ)))
462 oveq1 7152 . . . . . . . . . . . 12 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)))
463462eleq1d 2894 . . . . . . . . . . 11 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷))
464461, 463imbi12d 346 . . . . . . . . . 10 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷)))
465459, 464, 298vtocl 3557 . . . . . . . . 9 ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷)
466452, 458, 465vtocl 3557 . . . . . . . 8 ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)
467394, 448, 451, 466syl3anc 1363 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)
468393, 467eqeltrd 2910 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦𝐷)
469468ralrimiva 3179 . . . . 5 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ∀𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))𝑦𝐷)
470 dfss3 3953 . . . . 5 ((𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷 ↔ ∀𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))𝑦𝐷)
471469, 470sylibr 235 . . . 4 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷)
472 breq2 5061 . . . . . 6 (𝑦 = ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) → (𝑋 < 𝑦𝑋 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇))))
473 oveq2 7153 . . . . . . 7 (𝑦 = ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) → (𝑋(,)𝑦) = (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))))
474473sseq1d 3995 . . . . . 6 (𝑦 = ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) → ((𝑋(,)𝑦) ⊆ 𝐷 ↔ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷))
475472, 474anbi12d 630 . . . . 5 (𝑦 = ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) → ((𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷) ↔ (𝑋 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∧ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷)))
476475rspcev 3620 . . . 4 ((((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ ∧ (𝑋 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∧ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
477328, 371, 471, 476syl12anc 832 . . 3 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
47815adantlr 711 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋))
479 simp2 1129 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ (0...𝑀))
480253ad2ant2 1126 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℝ)
481943ad2ant2 1126 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑀 ∈ ℝ)
482963ad2ant2 1126 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗𝑀)
483 id 22 . . . . . . . . . . . . . . . . . 18 ((𝑄𝑗) = (𝐸𝑋) → (𝑄𝑗) = (𝐸𝑋))
484483eqcomd 2824 . . . . . . . . . . . . . . . . 17 ((𝑄𝑗) = (𝐸𝑋) → (𝐸𝑋) = (𝑄𝑗))
485484adantr 481 . . . . . . . . . . . . . . . 16 (((𝑄𝑗) = (𝐸𝑋) ∧ 𝑀 = 𝑗) → (𝐸𝑋) = (𝑄𝑗))
4864853ad2antl3 1179 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → (𝐸𝑋) = (𝑄𝑗))
487 fveq2 6663 . . . . . . . . . . . . . . . . 17 (𝑀 = 𝑗 → (𝑄𝑀) = (𝑄𝑗))
488487eqcomd 2824 . . . . . . . . . . . . . . . 16 (𝑀 = 𝑗 → (𝑄𝑗) = (𝑄𝑀))
489488adantl 482 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → (𝑄𝑗) = (𝑄𝑀))
490180ad2antrr 722 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑀 = 𝑗) → (𝑄𝑀) = 𝐵)
4914903ad2antl1 1177 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → (𝑄𝑀) = 𝐵)
492486, 489, 4913eqtrd 2857 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → (𝐸𝑋) = 𝐵)
493 neneq 3019 . . . . . . . . . . . . . . . 16 ((𝐸𝑋) ≠ 𝐵 → ¬ (𝐸𝑋) = 𝐵)
494493ad2antlr 723 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑀 = 𝑗) → ¬ (𝐸𝑋) = 𝐵)
4954943ad2antl1 1177 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → ¬ (𝐸𝑋) = 𝐵)
496492, 495pm2.65da 813 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → ¬ 𝑀 = 𝑗)
497496neqned 3020 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑀𝑗)
498480, 481, 482, 497leneltd 10782 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 < 𝑀)
499 elfzfzo 41418 . . . . . . . . . . 11 (𝑗 ∈ (0..^𝑀) ↔ (𝑗 ∈ (0...𝑀) ∧ 𝑗 < 𝑀))
500479, 498, 499sylanbrc 583 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ (0..^𝑀))
501117adantlr 711 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ*)
5025013adant3 1124 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ∈ ℝ*)
503 simp1l 1189 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝜑)
504101adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
505 fzofzp1 13122 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0..^𝑀) → (𝑗 + 1) ∈ (0...𝑀))
506505adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑗 + 1) ∈ (0...𝑀))
507504, 506ffvelrnd 6844 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ)
508507rexrd 10679 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ*)
509503, 500, 508syl2anc 584 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 + 1)) ∈ ℝ*)
5101413adant1r 1169 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ*)
51137, 160eqbrtrd 5079 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ≤ (𝐸𝑋))
512511adantlr 711 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ≤ (𝐸𝑋))
5135123adant2 1123 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ≤ (𝐸𝑋))
5144843ad2ant3 1127 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) = (𝑄𝑗))
515 eleq1 2897 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 → (𝑖 ∈ (0..^𝑀) ↔ 𝑗 ∈ (0..^𝑀)))
516515anbi2d 628 . . . . . . . . . . . . . . 15 (𝑖 = 𝑗 → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑𝑗 ∈ (0..^𝑀))))
517 fveq2 6663 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 → (𝑄𝑖) = (𝑄𝑗))
518 oveq1 7152 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
519518fveq2d 6667 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑗 + 1)))
520517, 519breq12d 5070 . . . . . . . . . . . . . . 15 (𝑖 = 𝑗 → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄𝑗) < (𝑄‘(𝑗 + 1))))
521516, 520imbi12d 346 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄𝑗) < (𝑄‘(𝑗 + 1)))))
522521, 152chvarvv 1996 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄𝑗) < (𝑄‘(𝑗 + 1)))
523503, 500, 522syl2anc 584 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) < (𝑄‘(𝑗 + 1)))
524514, 523eqbrtrd 5079 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) < (𝑄‘(𝑗 + 1)))
525502, 509, 510, 513, 524elicod 12775 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ((𝑄𝑗)[,)(𝑄‘(𝑗 + 1))))
526517, 519oveq12d 7163 . . . . . . . . . . . 12 (𝑖 = 𝑗 → ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑗)[,)(𝑄‘(𝑗 + 1))))
527526eleq2d 2895 . . . . . . . . . . 11 (𝑖 = 𝑗 → ((𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) ↔ (𝐸𝑋) ∈ ((𝑄𝑗)[,)(𝑄‘(𝑗 + 1)))))
528527rspcev 3620 . . . . . . . . . 10 ((𝑗 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑗)[,)(𝑄‘(𝑗 + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
529500, 525, 528syl2anc 584 . . . . . . . . 9 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
5305293exp 1111 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → (𝑗 ∈ (0...𝑀) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))))
531530adantr 481 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝐸𝑋) ∈ ran 𝑄) → (𝑗 ∈ (0...𝑀) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))))
532531rexlimdv 3280 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))))
533478, 532mpd 15 . . . . 5 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
534 ioossico 12814 . . . . . . . . . . 11 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))
535 simpr 485 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
536534, 535sseldi 3962 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
537536ex 413 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))))
538537adantlr 711 . . . . . . . 8 (((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))))
539538reximdva 3271 . . . . . . 7 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))))
540190, 539mpd 15 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
541540adantlr 711 . . . . 5 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
542533, 541pm2.61dan 809 . . . 4 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
543208, 250resubcld 11056 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ)
5445433adant3 1124 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ)
545219eqcomd 2824 . . . . . . . . . 10 (𝜑𝑋 = ((𝐸𝑋) − (𝑍𝑋)))
5465453ad2ant1 1125 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → 𝑋 = ((𝐸𝑋) − (𝑍𝑋)))
5471393ad2ant1 1125 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ℝ)
5482083adant3 1124 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
5491363ad2ant1 1125 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑍𝑋) ∈ ℝ)
550200rexrd 10679 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ*)
5515503adant3 1124 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ*)
5522093adant3 1124 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
553 simp3 1130 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
554 icoltub 41660 . . . . . . . . . . 11 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) < (𝑄‘(𝑖 + 1)))
555551, 552, 553, 554syl3anc 1363 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) < (𝑄‘(𝑖 + 1)))
556547, 548, 549, 555ltsub1dd 11240 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝐸𝑋) − (𝑍𝑋)) < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))
557546, 556eqbrtrd 5079 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → 𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))
558 elioore 12756 . . . . . . . . . . . . 13 (𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) → 𝑦 ∈ ℝ)
559558, 237sylan2 592 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
5605593ad2antl1 1177 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
561 simpl1 1183 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝜑)
5622413adant3 1124 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
563562adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
564551adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄𝑖) ∈ ℝ*)
565552adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
566558adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 ∈ ℝ)
567136adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑍𝑋) ∈ ℝ)
568566, 567readdcld 10658 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
5695683ad2antl1 1177 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
5702003adant3 1124 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
571570adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄𝑖) ∈ ℝ)
572561, 139syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝐸𝑋) ∈ ℝ)
573 icogelb 12776 . . . . . . . . . . . . . . . . 17 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ≤ (𝐸𝑋))
574551, 552, 553, 573syl3anc 1363 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ≤ (𝐸𝑋))
575574adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄𝑖) ≤ (𝐸𝑋))
576138ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
57774ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑋 ∈ ℝ)
578558adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 ∈ ℝ)
579136ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑍𝑋) ∈ ℝ)
580254ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑋 ∈ ℝ*)
581543rexrd 10679 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ*)
582581adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ*)
583 simpr 485 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))))
584 ioogtlb 41646 . . . . . . . . . . . . . . . . . . 19 ((𝑋 ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ*𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑋 < 𝑦)
585580, 582, 583, 584syl3anc 1363 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑋 < 𝑦)
586577, 578, 579, 585ltadd1dd 11239 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑋 + (𝑍𝑋)) < (𝑦 + (𝑍𝑋)))
587576, 586eqbrtrd 5079 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝐸𝑋) < (𝑦 + (𝑍𝑋)))
5885873adantl3 1160 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝐸𝑋) < (𝑦 + (𝑍𝑋)))
589571, 572, 569, 575, 588lelttrd 10786 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄𝑖) < (𝑦 + (𝑍𝑋)))
590543adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ)
591 iooltub 41662 . . . . . . . . . . . . . . . . . 18 ((𝑋 ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ*𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))
592580, 582, 583, 591syl3anc 1363 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))
593578, 590, 579, 592ltadd1dd 11239 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) < (((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) + (𝑍𝑋)))
594208recnd 10657 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
595217adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑍𝑋) ∈ ℂ)
596594, 595npcand 10989 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) + (𝑍𝑋)) = (𝑄‘(𝑖 + 1)))
597596adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) + (𝑍𝑋)) = (𝑄‘(𝑖 + 1)))
598593, 597breqtrd 5083 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) < (𝑄‘(𝑖 + 1)))
5995983adantl3 1160 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) < (𝑄‘(𝑖 + 1)))
600564, 565, 569, 589, 599eliood 41649 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
601563, 600sseldd 3965 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) ∈ 𝐷)
602561, 449syl 17 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
603561, 601, 602, 300syl3anc 1363 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
604560, 603eqeltrd 2910 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦𝐷)
605604ralrimiva 3179 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))𝑦𝐷)
606 dfss3 3953 . . . . . . . . 9 ((𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷 ↔ ∀𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))𝑦𝐷)
607605, 606sylibr 235 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷)
608 breq2 5061 . . . . . . . . . 10 (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) → (𝑋 < 𝑦𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋))))
609 oveq2 7153 . . . . . . . . . . 11 (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) → (𝑋(,)𝑦) = (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))))
610609sseq1d 3995 . . . . . . . . . 10 (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) → ((𝑋(,)𝑦) ⊆ 𝐷 ↔ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷))
611608, 610anbi12d 630 . . . . . . . . 9 (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) → ((𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷) ↔ (𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∧ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷)))
612611rspcev 3620 . . . . . . . 8 ((((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ ∧ (𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∧ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
613544, 557, 607, 612syl12anc 832 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
6146133exp 1111 . . . . . 6 (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))))
615614adantr 481 . . . . 5 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → (𝑖 ∈ (0..^𝑀) → ((𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))))
616615rexlimdv 3280 . . . 4 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))
617542, 616mpd 15 . . 3 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
618477, 617pm2.61dane 3101 . 2 (𝜑 → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
619314, 618jca 512 1 (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ∧ ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wcel 2105  wne 3013  wral 3135  wrex 3136  {crab 3139  wss 3933   class class class wbr 5057  cmpt 5137  ran crn 5549   Fn wfn 6343  wf 6344  cfv 6348  (class class class)co 7145  m cmap 8395  supcsup 8892  cc 10523  cr 10524  0cc0 10525  1c1 10526   + caddc 10528   · cmul 10530  *cxr 10662   < clt 10663  cle 10664  cmin 10858  -cneg 10859   / cdiv 11285  cn 11626  cz 11969  cuz 12231  (,)cioo 12726  (,]cioc 12727  [,)cico 12728  [,]cicc 12729  ...cfz 12880  ..^cfzo 13021  cfl 13148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-er 8278  df-map 8397  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-sup 8894  df-inf 8895  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-n0 11886  df-z 11970  df-uz 12232  df-rp 12378  df-ioo 12730  df-ioc 12731  df-ico 12732  df-icc 12733  df-fz 12881  df-fzo 13022  df-fl 13150
This theorem is referenced by:  fourierdlem113  42381
  Copyright terms: Public domain W3C validator