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

Theorem fourierdlem41 42729
 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 488 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → (𝐸𝑋) ∈ ran 𝑄)
2 fourierdlem41.q . . . . . . . . . . 11 (𝜑𝑄 ∈ (𝑃𝑀))
3 fourierdlem41.m . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℕ)
4 fourierdlem41.p . . . . . . . . . . . . 13 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
54fourierdlem2 42690 . . . . . . . . . . . 12 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
63, 5syl 17 . . . . . . . . . . 11 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
72, 6mpbid 235 . . . . . . . . . 10 (𝜑 → (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
87simpld 498 . . . . . . . . 9 (𝜑𝑄 ∈ (ℝ ↑m (0...𝑀)))
9 elmapi 8415 . . . . . . . . 9 (𝑄 ∈ (ℝ ↑m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
10 ffn 6494 . . . . . . . . 9 (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
118, 9, 103syl 18 . . . . . . . 8 (𝜑𝑄 Fn (0...𝑀))
1211adantr 484 . . . . . . 7 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → 𝑄 Fn (0...𝑀))
13 fvelrnb 6708 . . . . . . 7 (𝑄 Fn (0...𝑀) → ((𝐸𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋)))
1412, 13syl 17 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → ((𝐸𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋)))
151, 14mpbid 235 . . . . 5 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋))
16 0zd 11981 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ∈ ℤ)
17 elfzelz 12902 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
18173ad2ant2 1131 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℤ)
19 1zzd 12001 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 1 ∈ ℤ)
2018, 19zsubcld 12080 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ ℤ)
21 simpll 766 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → 𝜑)
22 elfzle1 12905 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
2322anim1i 617 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → (0 ≤ 𝑗 ∧ ¬ 0 < 𝑗))
24 0red 10633 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 0 ∈ ℝ)
2517zred 12075 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
2625adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 𝑗 ∈ ℝ)
2724, 26eqleltd 10773 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → (0 = 𝑗 ↔ (0 ≤ 𝑗 ∧ ¬ 0 < 𝑗)))
2823, 27mpbird 260 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 0 = 𝑗)
2928eqcomd 2828 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 𝑗 = 0)
3029adantll 713 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → 𝑗 = 0)
31 fveq2 6652 . . . . . . . . . . . . . . . 16 (𝑗 = 0 → (𝑄𝑗) = (𝑄‘0))
327simprld 771 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵))
3332simpld 498 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘0) = 𝐴)
3431, 33sylan9eqr 2879 . . . . . . . . . . . . . . 15 ((𝜑𝑗 = 0) → (𝑄𝑗) = 𝐴)
3521, 30, 34syl2anc 587 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → (𝑄𝑗) = 𝐴)
36353adantl3 1165 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄𝑗) = 𝐴)
37 simpr 488 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) = (𝐸𝑋))
38 fourierdlem41.a . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℝ)
3938rexrd 10680 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℝ*)
40 fourierdlem41.b . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 ∈ ℝ)
4140rexrd 10680 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ ℝ*)
42 fourierdlem41.altb . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐴 < 𝐵)
43 fourierdlem41.t . . . . . . . . . . . . . . . . . . . . . . 23 𝑇 = (𝐵𝐴)
44 eqid 2822 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
4538, 40, 42, 43, 44fourierdlem4 42692 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))):ℝ⟶(𝐴(,]𝐵))
46 fourierdlem41.e . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥)))
4746a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥))))
48 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
4940adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
5049, 48resubcld 11057 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑥 ∈ ℝ) → (𝐵𝑥) ∈ ℝ)
5140, 38resubcld 11057 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (𝐵𝐴) ∈ ℝ)
5243, 51eqeltrid 2918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝑇 ∈ ℝ)
5352adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
54 0red 10633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → 0 ∈ ℝ)
5538, 40posdifd 11216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
5642, 55mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → 0 < (𝐵𝐴))
5743eqcomi 2831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝐵𝐴) = 𝑇
5857a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → (𝐵𝐴) = 𝑇)
5956, 58breqtrd 5068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → 0 < 𝑇)
6054, 59gtned 10764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑𝑇 ≠ 0)
6160adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑥 ∈ ℝ) → 𝑇 ≠ 0)
6250, 53, 61redivcld 11457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑥 ∈ ℝ) → ((𝐵𝑥) / 𝑇) ∈ ℝ)
6362flcld 13163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑥 ∈ ℝ) → (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℤ)
6463zred 12075 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑥 ∈ ℝ) → (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℝ)
6564, 53remulcld 10660 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥 ∈ ℝ) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
66 fourierdlem41.z . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
6766fvmpt2 6761 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℝ ∧ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ ℝ) → (𝑍𝑥) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
6848, 65, 67syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑥 ∈ ℝ) → (𝑍𝑥) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
6968oveq2d 7156 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥 ∈ ℝ) → (𝑥 + (𝑍𝑥)) = (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
7069mpteq2dva 5137 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))))
7147, 70eqtrd 2857 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))))
7271feq1d 6479 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐸:ℝ⟶(𝐴(,]𝐵) ↔ (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))):ℝ⟶(𝐴(,]𝐵)))
7345, 72mpbird 260 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))
74 fourierdlem41.x . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑋 ∈ ℝ)
7573, 74ffvelrnd 6834 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐸𝑋) ∈ (𝐴(,]𝐵))
76 iocgtlb 42078 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝐸𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸𝑋))
7739, 41, 75, 76syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 < (𝐸𝑋))
7838, 77gtned 10764 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐸𝑋) ≠ 𝐴)
7978adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≠ 𝐴)
8037, 79eqnetrd 3078 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ≠ 𝐴)
8180adantr 484 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄𝑗) ≠ 𝐴)
82813adantl2 1164 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄𝑗) ≠ 𝐴)
8382neneqd 3016 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ ¬ 0 < 𝑗) → ¬ (𝑄𝑗) = 𝐴)
8436, 83condan 817 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 < 𝑗)
85 zltlem1 12023 . . . . . . . . . . . . 13 ((0 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (0 < 𝑗 ↔ 0 ≤ (𝑗 − 1)))
8616, 18, 85syl2anc 587 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 < 𝑗 ↔ 0 ≤ (𝑗 − 1)))
8784, 86mpbid 235 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 0 ≤ (𝑗 − 1))
88 eluz2 12237 . . . . . . . . . . 11 ((𝑗 − 1) ∈ (ℤ‘0) ↔ (0 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ ∧ 0 ≤ (𝑗 − 1)))
8916, 20, 87, 88syl3anbrc 1340 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (ℤ‘0))
90 elfzel2 12900 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
91903ad2ant2 1131 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑀 ∈ ℤ)
92 1red 10631 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 1 ∈ ℝ)
9325, 92resubcld 11057 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
9490zred 12075 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
9525ltm1d 11561 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑗)
96 elfzle2 12906 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → 𝑗𝑀)
9793, 25, 94, 95, 96ltletrd 10789 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
98973ad2ant2 1131 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) < 𝑀)
99 elfzo2 13036 . . . . . . . . . 10 ((𝑗 − 1) ∈ (0..^𝑀) ↔ ((𝑗 − 1) ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) < 𝑀))
10089, 91, 98, 99syl3anbrc 1340 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (0..^𝑀))
1018, 9syl 17 . . . . . . . . . . . . 13 (𝜑𝑄:(0...𝑀)⟶ℝ)
1021013ad2ant1 1130 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑄:(0...𝑀)⟶ℝ)
10316, 91, 203jca 1125 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ))
10493, 94, 97ltled 10777 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ≤ 𝑀)
1051043ad2ant2 1131 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ≤ 𝑀)
106103, 87, 105jca32 519 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ) ∧ (0 ≤ (𝑗 − 1) ∧ (𝑗 − 1) ≤ 𝑀)))
107 elfz2 12892 . . . . . . . . . . . . 13 ((𝑗 − 1) ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ) ∧ (0 ≤ (𝑗 − 1) ∧ (𝑗 − 1) ≤ 𝑀)))
108106, 107sylibr 237 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑗 − 1) ∈ (0...𝑀))
109102, 108ffvelrnd 6834 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ)
110109rexrd 10680 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ*)
11125recnd 10658 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
112 1cnd 10625 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 1 ∈ ℂ)
113111, 112npcand 10990 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → ((𝑗 − 1) + 1) = 𝑗)
114113fveq2d 6656 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
115114adantl 485 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
116101ffvelrnda 6833 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ)
117116rexrd 10680 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ*)
118115, 117eqeltrd 2914 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄‘((𝑗 − 1) + 1)) ∈ ℝ*)
1191183adant3 1129 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘((𝑗 − 1) + 1)) ∈ ℝ*)
120 id 22 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋𝑥 = 𝑋)
121 fveq2 6652 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (𝑍𝑥) = (𝑍𝑋))
122120, 121oveq12d 7158 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → (𝑥 + (𝑍𝑥)) = (𝑋 + (𝑍𝑋)))
123122adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑥 = 𝑋) → (𝑥 + (𝑍𝑥)) = (𝑋 + (𝑍𝑋)))
12466a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
125 oveq2 7148 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑋 → (𝐵𝑥) = (𝐵𝑋))
126125oveq1d 7155 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑋 → ((𝐵𝑥) / 𝑇) = ((𝐵𝑋) / 𝑇))
127126fveq2d 6656 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋 → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵𝑋) / 𝑇)))
128127oveq1d 7155 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋 → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
129128adantl 485 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 = 𝑋) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
13040, 74resubcld 11057 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵𝑋) ∈ ℝ)
131130, 52, 60redivcld 11457 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐵𝑋) / 𝑇) ∈ ℝ)
132131flcld 13163 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
133132zred 12075 . . . . . . . . . . . . . . . . . 18 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℝ)
134133, 52remulcld 10660 . . . . . . . . . . . . . . . . 17 (𝜑 → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
135124, 129, 74, 134fvmptd 6757 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑍𝑋) = ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
136135, 134eqeltrd 2914 . . . . . . . . . . . . . . 15 (𝜑 → (𝑍𝑋) ∈ ℝ)
13774, 136readdcld 10659 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 + (𝑍𝑋)) ∈ ℝ)
13847, 123, 74, 137fvmptd 6757 . . . . . . . . . . . . 13 (𝜑 → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
139138, 137eqeltrd 2914 . . . . . . . . . . . 12 (𝜑 → (𝐸𝑋) ∈ ℝ)
140139rexrd 10680 . . . . . . . . . . 11 (𝜑 → (𝐸𝑋) ∈ ℝ*)
1411403ad2ant1 1130 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ*)
142 simp1 1133 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝜑)
143 ovex 7173 . . . . . . . . . . . . . 14 (𝑗 − 1) ∈ V
144 eleq1 2901 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 − 1) → (𝑖 ∈ (0..^𝑀) ↔ (𝑗 − 1) ∈ (0..^𝑀)))
145144anbi2d 631 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗 − 1) → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀))))
146 fveq2 6652 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 − 1) → (𝑄𝑖) = (𝑄‘(𝑗 − 1)))
147 oveq1 7147 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 − 1) → (𝑖 + 1) = ((𝑗 − 1) + 1))
148147fveq2d 6656 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 − 1) → (𝑄‘(𝑖 + 1)) = (𝑄‘((𝑗 − 1) + 1)))
149146, 148breq12d 5055 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗 − 1) → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1))))
150145, 149imbi12d 348 . . . . . . . . . . . . . 14 (𝑖 = (𝑗 − 1) → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))))
1517simprrd 773 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))
152151r19.21bi 3198 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
153143, 150, 152vtocl 3534 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
154142, 100, 153syl2anc 587 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
1551143ad2ant2 1131 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄𝑗))
156154, 155breqtrd 5068 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄𝑗))
157 simp3 1135 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) = (𝐸𝑋))
158156, 157breqtrd 5068 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 − 1)) < (𝐸𝑋))
159139leidd 11195 . . . . . . . . . . . . . 14 (𝜑 → (𝐸𝑋) ≤ (𝐸𝑋))
160159adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝐸𝑋))
16137eqcomd 2828 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) = (𝑄𝑗))
162160, 161breqtrd 5068 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄𝑗))
1631623adant2 1128 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄𝑗))
164113eqcomd 2828 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 𝑗 = ((𝑗 − 1) + 1))
165164fveq2d 6656 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (𝑄𝑗) = (𝑄‘((𝑗 − 1) + 1)))
1661653ad2ant2 1131 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) = (𝑄‘((𝑗 − 1) + 1)))
167163, 166breqtrd 5068 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ≤ (𝑄‘((𝑗 − 1) + 1)))
168110, 119, 141, 158, 167eliocd 42083 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
169146, 148oveq12d 7158 . . . . . . . . . . 11 (𝑖 = (𝑗 − 1) → ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
170169eleq2d 2899 . . . . . . . . . 10 (𝑖 = (𝑗 − 1) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) ↔ (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))))
171170rspcev 3598 . . . . . . . . 9 (((𝑗 − 1) ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
172100, 168, 171syl2anc 587 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
1731723exp 1116 . . . . . . 7 (𝜑 → (𝑗 ∈ (0...𝑀) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))))
174173adantr 484 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → (𝑗 ∈ (0...𝑀) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))))
175174rexlimdv 3269 . . . . 5 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
17615, 175mpd 15 . . . 4 ((𝜑 ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
1773adantr 484 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → 𝑀 ∈ ℕ)
178101adantr 484 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ)
179 iocssicc 12815 . . . . . . . 8 ((𝑄‘0)(,](𝑄𝑀)) ⊆ ((𝑄‘0)[,](𝑄𝑀))
18032simprd 499 . . . . . . . . . 10 (𝜑 → (𝑄𝑀) = 𝐵)
18133, 180oveq12d 7158 . . . . . . . . 9 (𝜑 → ((𝑄‘0)(,](𝑄𝑀)) = (𝐴(,]𝐵))
18275, 181eleqtrrd 2917 . . . . . . . 8 (𝜑 → (𝐸𝑋) ∈ ((𝑄‘0)(,](𝑄𝑀)))
183179, 182sseldi 3940 . . . . . . 7 (𝜑 → (𝐸𝑋) ∈ ((𝑄‘0)[,](𝑄𝑀)))
184183adantr 484 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (𝐸𝑋) ∈ ((𝑄‘0)[,](𝑄𝑀)))
185 simpr 488 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ¬ (𝐸𝑋) ∈ ran 𝑄)
186 fveq2 6652 . . . . . . . . 9 (𝑘 = 𝑗 → (𝑄𝑘) = (𝑄𝑗))
187186breq1d 5052 . . . . . . . 8 (𝑘 = 𝑗 → ((𝑄𝑘) < (𝐸𝑋) ↔ (𝑄𝑗) < (𝐸𝑋)))
188187cbvrabv 3467 . . . . . . 7 {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < (𝐸𝑋)} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < (𝐸𝑋)}
189188supeq1i 8899 . . . . . 6 sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < (𝐸𝑋)}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < (𝐸𝑋)}, ℝ, < )
190177, 178, 184, 185, 189fourierdlem25 42713 . . . . 5 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
191 ioossioc 42068 . . . . . . . 8 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))
192191a1i 11 . . . . . . 7 (((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
193192sseld 3941 . . . . . 6 (((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
194193reximdva 3260 . . . . 5 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))))
195190, 194mpd 15 . . . 4 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
196176, 195pm2.61dan 812 . . 3 (𝜑 → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
197101adantr 484 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
198 elfzofz 13048 . . . . . . . . . 10 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
199198adantl 485 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
200197, 199ffvelrnd 6834 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
2012003adant3 1129 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
2021363ad2ant1 1130 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑍𝑋) ∈ ℝ)
203201, 202resubcld 11057 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ)
2041393ad2ant1 1130 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ℝ)
205201rexrd 10680 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ*)
206 fzofzp1 13129 . . . . . . . . . . . . 13 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
207206adantl 485 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
208197, 207ffvelrnd 6834 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
209208rexrd 10680 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
2102093adant3 1129 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
211 simp3 1135 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))))
212 iocgtlb 42078 . . . . . . . . 9 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝐸𝑋))
213205, 210, 211, 212syl3anc 1368 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < (𝐸𝑋))
214201, 204, 202, 213ltsub1dd 11241 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) < ((𝐸𝑋) − (𝑍𝑋)))
215138oveq1d 7155 . . . . . . . . 9 (𝜑 → ((𝐸𝑋) − (𝑍𝑋)) = ((𝑋 + (𝑍𝑋)) − (𝑍𝑋)))
21674recnd 10658 . . . . . . . . . 10 (𝜑𝑋 ∈ ℂ)
217136recnd 10658 . . . . . . . . . 10 (𝜑 → (𝑍𝑋) ∈ ℂ)
218216, 217pncand 10987 . . . . . . . . 9 (𝜑 → ((𝑋 + (𝑍𝑋)) − (𝑍𝑋)) = 𝑋)
219215, 218eqtrd 2857 . . . . . . . 8 (𝜑 → ((𝐸𝑋) − (𝑍𝑋)) = 𝑋)
2202193ad2ant1 1130 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐸𝑋) − (𝑍𝑋)) = 𝑋)
221214, 220breqtrd 5068 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑋)
222 elioore 12756 . . . . . . . . . . 11 (𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) → 𝑦 ∈ ℝ)
223135oveq2d 7156 . . . . . . . . . . . . . 14 (𝜑 → (𝑦 + (𝑍𝑋)) = (𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
224133recnd 10658 . . . . . . . . . . . . . . 15 (𝜑 → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℂ)
22552recnd 10658 . . . . . . . . . . . . . . 15 (𝜑𝑇 ∈ ℂ)
226224, 225mulneg1d 11082 . . . . . . . . . . . . . 14 (𝜑 → (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
227223, 226oveq12d 7158 . . . . . . . . . . . . 13 (𝜑 → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
228227adantr 484 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
229 simpr 488 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
230134adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
231229, 230readdcld 10659 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → (𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ ℝ)
232231recnd 10658 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → (𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ ℂ)
233230recnd 10658 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
234232, 233negsubd 10992 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
235229recnd 10658 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
236235, 233pncand 10987 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) − ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) = 𝑦)
237228, 234, 2363eqtrrd 2862 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
238222, 237sylan2 595 . . . . . . . . . 10 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
2392383ad2antl1 1182 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
240 simpl1 1188 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝜑)
241 fourierdlem41.qssd . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
2422413adant3 1129 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
243242adantr 484 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
244205adantr 484 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) ∈ ℝ*)
245210adantr 484 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
246222adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
247136adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℝ)
248246, 247readdcld 10659 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
2492483ad2antl1 1182 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
250136adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑍𝑋) ∈ ℝ)
251200, 250resubcld 11057 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ)
252251rexrd 10680 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
253252adantr 484 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*)
25474rexrd 10680 . . . . . . . . . . . . . . . 16 (𝜑𝑋 ∈ ℝ*)
255254ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑋 ∈ ℝ*)
256 simpr 488 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
257 ioogtlb 42071 . . . . . . . . . . . . . . 15 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑦)
258253, 255, 256, 257syl3anc 1368 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑄𝑖) − (𝑍𝑋)) < 𝑦)
259200adantr 484 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) ∈ ℝ)
260136ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑍𝑋) ∈ ℝ)
261222adantl 485 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
262259, 260, 261ltsubaddd 11225 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (((𝑄𝑖) − (𝑍𝑋)) < 𝑦 ↔ (𝑄𝑖) < (𝑦 + (𝑍𝑋))))
263258, 262mpbid 235 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) < (𝑦 + (𝑍𝑋)))
2642633adantl3 1165 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄𝑖) < (𝑦 + (𝑍𝑋)))
265240, 139syl 17 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐸𝑋) ∈ ℝ)
266208adantr 484 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
2672663adantl3 1165 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
26874ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑋 ∈ ℝ)
269 iooltub 42086 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ*𝑋 ∈ ℝ*𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 < 𝑋)
270253, 255, 256, 269syl3anc 1368 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦 < 𝑋)
271261, 268, 260, 270ltadd1dd 11240 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝑋 + (𝑍𝑋)))
272138eqcomd 2828 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
273272ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑋 + (𝑍𝑋)) = (𝐸𝑋))
274271, 273breqtrd 5068 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝐸𝑋))
2752743adantl3 1165 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝐸𝑋))
276 iocleub 42079 . . . . . . . . . . . . . . 15 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
277205, 210, 211, 276syl3anc 1368 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
278277adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝐸𝑋) ≤ (𝑄‘(𝑖 + 1)))
279249, 265, 267, 275, 278ltletrd 10789 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) < (𝑄‘(𝑖 + 1)))
280244, 245, 249, 264, 279eliood 42074 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
281243, 280sseldd 3943 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (𝑦 + (𝑍𝑋)) ∈ 𝐷)
282240, 131syl 17 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝐵𝑋) / 𝑇) ∈ ℝ)
283282flcld 13163 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → (⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
284283znegcld 12077 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
285 negex 10873 . . . . . . . . . . 11 -(⌊‘((𝐵𝑋) / 𝑇)) ∈ V
286 eleq1 2901 . . . . . . . . . . . . 13 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ))
2872863anbi3d 1439 . . . . . . . . . . . 12 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)))
288 oveq1 7147 . . . . . . . . . . . . . 14 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (𝑘 · 𝑇) = (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇))
289288oveq2d 7156 . . . . . . . . . . . . 13 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
290289eleq1d 2898 . . . . . . . . . . . 12 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
291287, 290imbi12d 348 . . . . . . . . . . 11 (𝑘 = -(⌊‘((𝐵𝑋) / 𝑇)) → (((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)))
292 ovex 7173 . . . . . . . . . . . 12 (𝑦 + (𝑍𝑋)) ∈ V
293 eleq1 2901 . . . . . . . . . . . . . 14 (𝑥 = (𝑦 + (𝑍𝑋)) → (𝑥𝐷 ↔ (𝑦 + (𝑍𝑋)) ∈ 𝐷))
2942933anbi2d 1438 . . . . . . . . . . . . 13 (𝑥 = (𝑦 + (𝑍𝑋)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ)))
295 oveq1 7147 . . . . . . . . . . . . . 14 (𝑥 = (𝑦 + (𝑍𝑋)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)))
296295eleq1d 2898 . . . . . . . . . . . . 13 (𝑥 = (𝑦 + (𝑍𝑋)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷))
297294, 296imbi12d 348 . . . . . . . . . . . 12 (𝑥 = (𝑦 + (𝑍𝑋)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)))
298 fourierdlem41.dper . . . . . . . . . . . 12 ((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)
299292, 297, 298vtocl 3534 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)
300285, 291, 299vtocl 3534 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 + (𝑍𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
301240, 281, 284, 300syl3anc 1368 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
302239, 301eqeltrd 2914 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)) → 𝑦𝐷)
303302ralrimiva 3174 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑦𝐷)
304 dfss3 3930 . . . . . . 7 ((((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷 ↔ ∀𝑦 ∈ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋)𝑦𝐷)
305303, 304sylibr 237 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷)
306 breq1 5045 . . . . . . . 8 (𝑦 = ((𝑄𝑖) − (𝑍𝑋)) → (𝑦 < 𝑋 ↔ ((𝑄𝑖) − (𝑍𝑋)) < 𝑋))
307 oveq1 7147 . . . . . . . . 9 (𝑦 = ((𝑄𝑖) − (𝑍𝑋)) → (𝑦(,)𝑋) = (((𝑄𝑖) − (𝑍𝑋))(,)𝑋))
308307sseq1d 3973 . . . . . . . 8 (𝑦 = ((𝑄𝑖) − (𝑍𝑋)) → ((𝑦(,)𝑋) ⊆ 𝐷 ↔ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷))
309306, 308anbi12d 633 . . . . . . 7 (𝑦 = ((𝑄𝑖) − (𝑍𝑋)) → ((𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ↔ (((𝑄𝑖) − (𝑍𝑋)) < 𝑋 ∧ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷)))
310309rspcev 3598 . . . . . 6 ((((𝑄𝑖) − (𝑍𝑋)) ∈ ℝ ∧ (((𝑄𝑖) − (𝑍𝑋)) < 𝑋 ∧ (((𝑄𝑖) − (𝑍𝑋))(,)𝑋) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
311203, 221, 305, 310syl12anc 835 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1)))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
3123113exp 1116 . . . 4 (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))))
313312rexlimdv 3269 . . 3 (𝜑 → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,](𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷)))
314196, 313mpd 15 . 2 (𝜑 → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
315 0zd 11981 . . . . . . . . . 10 (𝜑 → 0 ∈ ℤ)
3163nnzd 12074 . . . . . . . . . 10 (𝜑𝑀 ∈ ℤ)
317 1zzd 12001 . . . . . . . . . 10 (𝜑 → 1 ∈ ℤ)
318315, 316, 3173jca 1125 . . . . . . . . 9 (𝜑 → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 1 ∈ ℤ))
319 0le1 11152 . . . . . . . . . 10 0 ≤ 1
320319a1i 11 . . . . . . . . 9 (𝜑 → 0 ≤ 1)
3213nnge1d 11673 . . . . . . . . 9 (𝜑 → 1 ≤ 𝑀)
322318, 320, 321jca32 519 . . . . . . . 8 (𝜑 → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 1 ∈ ℤ) ∧ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
323 elfz2 12892 . . . . . . . 8 (1 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 1 ∈ ℤ) ∧ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
324322, 323sylibr 237 . . . . . . 7 (𝜑 → 1 ∈ (0...𝑀))
325101, 324ffvelrnd 6834 . . . . . 6 (𝜑 → (𝑄‘1) ∈ ℝ)
326136, 52resubcld 11057 . . . . . 6 (𝜑 → ((𝑍𝑋) − 𝑇) ∈ ℝ)
327325, 326resubcld 11057 . . . . 5 (𝜑 → ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ)
328327adantr 484 . . . 4 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ)
32938recnd 10658 . . . . . . . . . 10 (𝜑𝐴 ∈ ℂ)
330329, 225pncand 10987 . . . . . . . . 9 (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
331330adantr 484 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
33243oveq2i 7151 . . . . . . . . . . 11 (𝐴 + 𝑇) = (𝐴 + (𝐵𝐴))
333332a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝐴 + 𝑇) = (𝐴 + (𝐵𝐴)))
33440recnd 10658 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℂ)
335329, 334pncan3d 10989 . . . . . . . . . . 11 (𝜑 → (𝐴 + (𝐵𝐴)) = 𝐵)
336335adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝐴 + (𝐵𝐴)) = 𝐵)
337 id 22 . . . . . . . . . . . 12 ((𝐸𝑋) = 𝐵 → (𝐸𝑋) = 𝐵)
338337eqcomd 2828 . . . . . . . . . . 11 ((𝐸𝑋) = 𝐵𝐵 = (𝐸𝑋))
339338adantl 485 . . . . . . . . . 10 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → 𝐵 = (𝐸𝑋))
340333, 336, 3393eqtrrd 2862 . . . . . . . . 9 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝐸𝑋) = (𝐴 + 𝑇))
341340oveq1d 7155 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝐸𝑋) − 𝑇) = ((𝐴 + 𝑇) − 𝑇))
34233adantr 484 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑄‘0) = 𝐴)
343331, 341, 3423eqtr4rd 2868 . . . . . . 7 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑄‘0) = ((𝐸𝑋) − 𝑇))
344343oveq1d 7155 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑄‘0) − ((𝑍𝑋) − 𝑇)) = (((𝐸𝑋) − 𝑇) − ((𝑍𝑋) − 𝑇)))
345139recnd 10658 . . . . . . . 8 (𝜑 → (𝐸𝑋) ∈ ℂ)
346345, 217, 225nnncan2d 11021 . . . . . . 7 (𝜑 → (((𝐸𝑋) − 𝑇) − ((𝑍𝑋) − 𝑇)) = ((𝐸𝑋) − (𝑍𝑋)))
347346adantr 484 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (((𝐸𝑋) − 𝑇) − ((𝑍𝑋) − 𝑇)) = ((𝐸𝑋) − (𝑍𝑋)))
348219adantr 484 . . . . . 6 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝐸𝑋) − (𝑍𝑋)) = 𝑋)
349344, 347, 3483eqtrrd 2862 . . . . 5 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → 𝑋 = ((𝑄‘0) − ((𝑍𝑋) − 𝑇)))
35033, 38eqeltrd 2914 . . . . . . 7 (𝜑 → (𝑄‘0) ∈ ℝ)
3513nngt0d 11674 . . . . . . . . . 10 (𝜑 → 0 < 𝑀)
352 fzolb 13039 . . . . . . . . . 10 (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
353315, 316, 351, 352syl3anbrc 1340 . . . . . . . . 9 (𝜑 → 0 ∈ (0..^𝑀))
354 0re 10632 . . . . . . . . . 10 0 ∈ ℝ
355 eleq1 2901 . . . . . . . . . . . . 13 (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀)))
356355anbi2d 631 . . . . . . . . . . . 12 (𝑖 = 0 → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀))))
357 fveq2 6652 . . . . . . . . . . . . 13 (𝑖 = 0 → (𝑄𝑖) = (𝑄‘0))
358 oveq1 7147 . . . . . . . . . . . . . 14 (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
359358fveq2d 6656 . . . . . . . . . . . . 13 (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1)))
360357, 359breq12d 5055 . . . . . . . . . . . 12 (𝑖 = 0 → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1))))
361356, 360imbi12d 348 . . . . . . . . . . 11 (𝑖 = 0 → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))))
362361, 152vtoclg 3542 . . . . . . . . . 10 (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))
363354, 362ax-mp 5 . . . . . . . . 9 ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))
364353, 363mpdan 686 . . . . . . . 8 (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1)))
365 0p1e1 11747 . . . . . . . . . 10 (0 + 1) = 1
366365fveq2i 6655 . . . . . . . . 9 (𝑄‘(0 + 1)) = (𝑄‘1)
367366a1i 11 . . . . . . . 8 (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1))
368364, 367breqtrd 5068 . . . . . . 7 (𝜑 → (𝑄‘0) < (𝑄‘1))
369350, 325, 326, 368ltsub1dd 11241 . . . . . 6 (𝜑 → ((𝑄‘0) − ((𝑍𝑋) − 𝑇)) < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
370369adantr 484 . . . . 5 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑄‘0) − ((𝑍𝑋) − 𝑇)) < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
371349, 370eqbrtrd 5064 . . . 4 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → 𝑋 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
372 elioore 12756 . . . . . . . . 9 (𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) → 𝑦 ∈ ℝ)
373135eqcomd 2828 . . . . . . . . . . . . . . . 16 (𝜑 → ((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = (𝑍𝑋))
374373negeqd 10869 . . . . . . . . . . . . . . 15 (𝜑 → -((⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = -(𝑍𝑋))
375226, 374eqtrd 2857 . . . . . . . . . . . . . 14 (𝜑 → (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) = -(𝑍𝑋))
376225mulid2d 10648 . . . . . . . . . . . . . 14 (𝜑 → (1 · 𝑇) = 𝑇)
377375, 376oveq12d 7158 . . . . . . . . . . . . 13 (𝜑 → ((-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) + (1 · 𝑇)) = (-(𝑍𝑋) + 𝑇))
378224negcld 10973 . . . . . . . . . . . . . 14 (𝜑 → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℂ)
379 1cnd 10625 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℂ)
380378, 379, 225adddird 10655 . . . . . . . . . . . . 13 (𝜑 → ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇) = ((-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇) + (1 · 𝑇)))
381217, 225negsubdid 11001 . . . . . . . . . . . . 13 (𝜑 → -((𝑍𝑋) − 𝑇) = (-(𝑍𝑋) + 𝑇))
382377, 380, 3813eqtr4d 2867 . . . . . . . . . . . 12 (𝜑 → ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇) = -((𝑍𝑋) − 𝑇))
383382oveq2d 7156 . . . . . . . . . . 11 (𝜑 → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) + -((𝑍𝑋) − 𝑇)))
384383adantr 484 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) + -((𝑍𝑋) − 𝑇)))
385326adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → ((𝑍𝑋) − 𝑇) ∈ ℝ)
386229, 385readdcld 10659 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ℝ)
387386recnd 10658 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ℂ)
388385recnd 10658 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → ((𝑍𝑋) − 𝑇) ∈ ℂ)
389387, 388negsubd 10992 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + -((𝑍𝑋) − 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) − ((𝑍𝑋) − 𝑇)))
390235, 388pncand 10987 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) − ((𝑍𝑋) − 𝑇)) = 𝑦)
391384, 389, 3903eqtrrd 2862 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → 𝑦 = ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)))
392372, 391sylan2 595 . . . . . . . 8 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 = ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)))
393392adantlr 714 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 = ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)))
394 simpll 766 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝜑)
395367eqcomd 2828 . . . . . . . . . . . 12 (𝜑 → (𝑄‘1) = (𝑄‘(0 + 1)))
396395oveq2d 7156 . . . . . . . . . . 11 (𝜑 → ((𝑄‘0)(,)(𝑄‘1)) = ((𝑄‘0)(,)(𝑄‘(0 + 1))))
397357, 359oveq12d 7158 . . . . . . . . . . . . . . . 16 (𝑖 = 0 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘0)(,)(𝑄‘(0 + 1))))
398397sseq1d 3973 . . . . . . . . . . . . . . 15 (𝑖 = 0 → (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷 ↔ ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷))
399356, 398imbi12d 348 . . . . . . . . . . . . . 14 (𝑖 = 0 → (((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)))
400399, 241vtoclg 3542 . . . . . . . . . . . . 13 (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷))
401354, 400ax-mp 5 . . . . . . . . . . . 12 ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)
402353, 401mpdan 686 . . . . . . . . . . 11 (𝜑 → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)
403396, 402eqsstrd 3980 . . . . . . . . . 10 (𝜑 → ((𝑄‘0)(,)(𝑄‘1)) ⊆ 𝐷)
404403ad2antrr 725 . . . . . . . . 9 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑄‘0)(,)(𝑄‘1)) ⊆ 𝐷)
40533, 39eqeltrd 2914 . . . . . . . . . . 11 (𝜑 → (𝑄‘0) ∈ ℝ*)
406405ad2antrr 725 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘0) ∈ ℝ*)
407325rexrd 10680 . . . . . . . . . . 11 (𝜑 → (𝑄‘1) ∈ ℝ*)
408407ad2antrr 725 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘1) ∈ ℝ*)
409372, 386sylan2 595 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ℝ)
410409adantlr 714 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ℝ)
411345, 216, 217subaddd 11004 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐸𝑋) − 𝑋) = (𝑍𝑋) ↔ (𝑋 + (𝑍𝑋)) = (𝐸𝑋)))
412272, 411mpbird 260 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸𝑋) − 𝑋) = (𝑍𝑋))
413 oveq1 7147 . . . . . . . . . . . . . . . 16 ((𝐸𝑋) = 𝐵 → ((𝐸𝑋) − 𝑋) = (𝐵𝑋))
414412, 413sylan9req 2878 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑍𝑋) = (𝐵𝑋))
415414oveq1d 7155 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑍𝑋) − 𝑇) = ((𝐵𝑋) − 𝑇))
416415oveq2d 7156 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑋 + ((𝑍𝑋) − 𝑇)) = (𝑋 + ((𝐵𝑋) − 𝑇)))
417130recnd 10658 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵𝑋) ∈ ℂ)
418216, 417, 225addsubassd 11006 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑋 + (𝐵𝑋)) − 𝑇) = (𝑋 + ((𝐵𝑋) − 𝑇)))
419418eqcomd 2828 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 + ((𝐵𝑋) − 𝑇)) = ((𝑋 + (𝐵𝑋)) − 𝑇))
420419adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑋 + ((𝐵𝑋) − 𝑇)) = ((𝑋 + (𝐵𝑋)) − 𝑇))
421334, 225, 329subsub23d 41857 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵𝑇) = 𝐴 ↔ (𝐵𝐴) = 𝑇))
42258, 421mpbird 260 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵𝑇) = 𝐴)
423216, 334pncan3d 10989 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋 + (𝐵𝑋)) = 𝐵)
424423oveq1d 7155 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑋 + (𝐵𝑋)) − 𝑇) = (𝐵𝑇))
425422, 424, 333eqtr4d 2867 . . . . . . . . . . . . . 14 (𝜑 → ((𝑋 + (𝐵𝑋)) − 𝑇) = (𝑄‘0))
426425adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ((𝑋 + (𝐵𝑋)) − 𝑇) = (𝑄‘0))
427416, 420, 4263eqtrrd 2862 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑄‘0) = (𝑋 + ((𝑍𝑋) − 𝑇)))
428427adantr 484 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘0) = (𝑋 + ((𝑍𝑋) − 𝑇)))
42974adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑋 ∈ ℝ)
430372adantl 485 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 ∈ ℝ)
431326adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑍𝑋) − 𝑇) ∈ ℝ)
432254adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑋 ∈ ℝ*)
433327rexrd 10680 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ*)
434433adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ*)
435 simpr 488 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))))
436 ioogtlb 42071 . . . . . . . . . . . . . 14 ((𝑋 ∈ ℝ* ∧ ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ*𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑋 < 𝑦)
437432, 434, 435, 436syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑋 < 𝑦)
438429, 430, 431, 437ltadd1dd 11240 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑋 + ((𝑍𝑋) − 𝑇)) < (𝑦 + ((𝑍𝑋) − 𝑇)))
439438adantlr 714 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑋 + ((𝑍𝑋) − 𝑇)) < (𝑦 + ((𝑍𝑋) − 𝑇)))
440428, 439eqbrtrd 5064 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘0) < (𝑦 + ((𝑍𝑋) − 𝑇)))
441 iooltub 42086 . . . . . . . . . . . . 13 ((𝑋 ∈ ℝ* ∧ ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ*𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
442432, 434, 435, 441syl3anc 1368 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)))
443325adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑄‘1) ∈ ℝ)
444430, 431, 443ltaddsubd 11229 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑦 + ((𝑍𝑋) − 𝑇)) < (𝑄‘1) ↔ 𝑦 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇))))
445442, 444mpbird 260 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) < (𝑄‘1))
446445adantlr 714 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) < (𝑄‘1))
447406, 408, 410, 440, 446eliood 42074 . . . . . . . . 9 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ ((𝑄‘0)(,)(𝑄‘1)))
448404, 447sseldd 3943 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷)
449132znegcld 12077 . . . . . . . . . 10 (𝜑 → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
450449peano2zd 12078 . . . . . . . . 9 (𝜑 → (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ)
451450ad2antrr 725 . . . . . . . 8 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ)
452 ovex 7173 . . . . . . . . 9 (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ V
453 eleq1 2901 . . . . . . . . . . 11 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → (𝑘 ∈ ℤ ↔ (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ))
4544533anbi3d 1439 . . . . . . . . . 10 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ)))
455 oveq1 7147 . . . . . . . . . . . 12 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → (𝑘 · 𝑇) = ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇))
456455oveq2d 7156 . . . . . . . . . . 11 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)))
457456eleq1d 2898 . . . . . . . . . 10 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → (((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷))
458454, 457imbi12d 348 . . . . . . . . 9 (𝑘 = (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) → (((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)))
459 ovex 7173 . . . . . . . . . 10 (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ V
460 eleq1 2901 . . . . . . . . . . . 12 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → (𝑥𝐷 ↔ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷))
4614603anbi2d 1438 . . . . . . . . . . 11 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → ((𝜑𝑥𝐷𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ)))
462 oveq1 7147 . . . . . . . . . . . 12 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)))
463462eleq1d 2898 . . . . . . . . . . 11 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷))
464461, 463imbi12d 348 . . . . . . . . . 10 (𝑥 = (𝑦 + ((𝑍𝑋) − 𝑇)) → (((𝜑𝑥𝐷𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷)))
465459, 464, 298vtocl 3534 . . . . . . . . 9 ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷𝑘 ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷)
466452, 458, 465vtocl 3534 . . . . . . . 8 ((𝜑 ∧ (𝑦 + ((𝑍𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵𝑋) / 𝑇)) + 1) ∈ ℤ) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)
467394, 448, 451, 466syl3anc 1368 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → ((𝑦 + ((𝑍𝑋) − 𝑇)) + ((-(⌊‘((𝐵𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)
468393, 467eqeltrd 2914 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))) → 𝑦𝐷)
469468ralrimiva 3174 . . . . 5 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ∀𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))𝑦𝐷)
470 dfss3 3930 . . . . 5 ((𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷 ↔ ∀𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇)))𝑦𝐷)
471469, 470sylibr 237 . . . 4 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷)
472 breq2 5046 . . . . . 6 (𝑦 = ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) → (𝑋 < 𝑦𝑋 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇))))
473 oveq2 7148 . . . . . . 7 (𝑦 = ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) → (𝑋(,)𝑦) = (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))))
474473sseq1d 3973 . . . . . 6 (𝑦 = ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) → ((𝑋(,)𝑦) ⊆ 𝐷 ↔ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷))
475472, 474anbi12d 633 . . . . 5 (𝑦 = ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) → ((𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷) ↔ (𝑋 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∧ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷)))
476475rspcev 3598 . . . 4 ((((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∈ ℝ ∧ (𝑋 < ((𝑄‘1) − ((𝑍𝑋) − 𝑇)) ∧ (𝑋(,)((𝑄‘1) − ((𝑍𝑋) − 𝑇))) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
477328, 371, 471, 476syl12anc 835 . . 3 ((𝜑 ∧ (𝐸𝑋) = 𝐵) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
47815adantlr 714 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋))
479 simp2 1134 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ (0...𝑀))
480253ad2ant2 1131 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ ℝ)
481943ad2ant2 1131 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑀 ∈ ℝ)
482963ad2ant2 1131 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗𝑀)
483 id 22 . . . . . . . . . . . . . . . . . 18 ((𝑄𝑗) = (𝐸𝑋) → (𝑄𝑗) = (𝐸𝑋))
484483eqcomd 2828 . . . . . . . . . . . . . . . . 17 ((𝑄𝑗) = (𝐸𝑋) → (𝐸𝑋) = (𝑄𝑗))
485484adantr 484 . . . . . . . . . . . . . . . 16 (((𝑄𝑗) = (𝐸𝑋) ∧ 𝑀 = 𝑗) → (𝐸𝑋) = (𝑄𝑗))
4864853ad2antl3 1184 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → (𝐸𝑋) = (𝑄𝑗))
487 fveq2 6652 . . . . . . . . . . . . . . . . 17 (𝑀 = 𝑗 → (𝑄𝑀) = (𝑄𝑗))
488487eqcomd 2828 . . . . . . . . . . . . . . . 16 (𝑀 = 𝑗 → (𝑄𝑗) = (𝑄𝑀))
489488adantl 485 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → (𝑄𝑗) = (𝑄𝑀))
490180ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑀 = 𝑗) → (𝑄𝑀) = 𝐵)
4914903ad2antl1 1182 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → (𝑄𝑀) = 𝐵)
492486, 489, 4913eqtrd 2861 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → (𝐸𝑋) = 𝐵)
493 neneq 3017 . . . . . . . . . . . . . . . 16 ((𝐸𝑋) ≠ 𝐵 → ¬ (𝐸𝑋) = 𝐵)
494493ad2antlr 726 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑀 = 𝑗) → ¬ (𝐸𝑋) = 𝐵)
4954943ad2antl1 1182 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) ∧ 𝑀 = 𝑗) → ¬ (𝐸𝑋) = 𝐵)
496492, 495pm2.65da 816 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → ¬ 𝑀 = 𝑗)
497496neqned 3018 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑀𝑗)
498480, 481, 482, 497leneltd 10783 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 < 𝑀)
499 elfzfzo 41846 . . . . . . . . . . 11 (𝑗 ∈ (0..^𝑀) ↔ (𝑗 ∈ (0...𝑀) ∧ 𝑗 < 𝑀))
500479, 498, 499sylanbrc 586 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝑗 ∈ (0..^𝑀))
501117adantlr 714 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ*)
5025013adant3 1129 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ∈ ℝ*)
503 simp1l 1194 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → 𝜑)
504101adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
505 fzofzp1 13129 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0..^𝑀) → (𝑗 + 1) ∈ (0...𝑀))
506505adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑗 + 1) ∈ (0...𝑀))
507504, 506ffvelrnd 6834 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ)
508507rexrd 10680 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ*)
509503, 500, 508syl2anc 587 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄‘(𝑗 + 1)) ∈ ℝ*)
5101413adant1r 1174 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ℝ*)
51137, 160eqbrtrd 5064 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ≤ (𝐸𝑋))
512511adantlr 714 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ≤ (𝐸𝑋))
5135123adant2 1128 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) ≤ (𝐸𝑋))
5144843ad2ant3 1132 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) = (𝑄𝑗))
515 eleq1 2901 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 → (𝑖 ∈ (0..^𝑀) ↔ 𝑗 ∈ (0..^𝑀)))
516515anbi2d 631 . . . . . . . . . . . . . . 15 (𝑖 = 𝑗 → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑𝑗 ∈ (0..^𝑀))))
517 fveq2 6652 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 → (𝑄𝑖) = (𝑄𝑗))
518 oveq1 7147 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
519518fveq2d 6656 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑗 + 1)))
520517, 519breq12d 5055 . . . . . . . . . . . . . . 15 (𝑖 = 𝑗 → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄𝑗) < (𝑄‘(𝑗 + 1))))
521516, 520imbi12d 348 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄𝑗) < (𝑄‘(𝑗 + 1)))))
522521, 152chvarvv 2005 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄𝑗) < (𝑄‘(𝑗 + 1)))
523503, 500, 522syl2anc 587 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝑄𝑗) < (𝑄‘(𝑗 + 1)))
524514, 523eqbrtrd 5064 . . . . . . . . . . 11 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) < (𝑄‘(𝑗 + 1)))
525502, 509, 510, 513, 524elicod 12775 . . . . . . . . . 10 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → (𝐸𝑋) ∈ ((𝑄𝑗)[,)(𝑄‘(𝑗 + 1))))
526517, 519oveq12d 7158 . . . . . . . . . . . 12 (𝑖 = 𝑗 → ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑗)[,)(𝑄‘(𝑗 + 1))))
527526eleq2d 2899 . . . . . . . . . . 11 (𝑖 = 𝑗 → ((𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) ↔ (𝐸𝑋) ∈ ((𝑄𝑗)[,)(𝑄‘(𝑗 + 1)))))
528527rspcev 3598 . . . . . . . . . 10 ((𝑗 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑗)[,)(𝑄‘(𝑗 + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
529500, 525, 528syl2anc 587 . . . . . . . . 9 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = (𝐸𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
5305293exp 1116 . . . . . . . 8 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → (𝑗 ∈ (0...𝑀) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))))
531530adantr 484 . . . . . . 7 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝐸𝑋) ∈ ran 𝑄) → (𝑗 ∈ (0...𝑀) → ((𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))))
532531rexlimdv 3269 . . . . . 6 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = (𝐸𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))))
533478, 532mpd 15 . . . . 5 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
534 ioossico 12816 . . . . . . . . . . 11 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))
535 simpr 488 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
536534, 535sseldi 3940 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
537536ex 416 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))))
538537adantlr 714 . . . . . . . 8 (((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))))
539538reximdva 3260 . . . . . . 7 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))))
540190, 539mpd 15 . . . . . 6 ((𝜑 ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
541540adantlr 714 . . . . 5 (((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) ∧ ¬ (𝐸𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
542533, 541pm2.61dan 812 . . . 4 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → ∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
543208, 250resubcld 11057 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ)
5445433adant3 1129 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ)
545219eqcomd 2828 . . . . . . . . . 10 (𝜑𝑋 = ((𝐸𝑋) − (𝑍𝑋)))
5465453ad2ant1 1130 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → 𝑋 = ((𝐸𝑋) − (𝑍𝑋)))
5471393ad2ant1 1130 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ℝ)
5482083adant3 1129 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
5491363ad2ant1 1130 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑍𝑋) ∈ ℝ)
550200rexrd 10680 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ*)
5515503adant3 1129 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ*)
5522093adant3 1129 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
553 simp3 1135 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))))
554 icoltub 42084 . . . . . . . . . . 11 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) < (𝑄‘(𝑖 + 1)))
555551, 552, 553, 554syl3anc 1368 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸𝑋) < (𝑄‘(𝑖 + 1)))
556547, 548, 549, 555ltsub1dd 11241 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝐸𝑋) − (𝑍𝑋)) < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))
557546, 556eqbrtrd 5064 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → 𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))
558 elioore 12756 . . . . . . . . . . . . 13 (𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) → 𝑦 ∈ ℝ)
559558, 237sylan2 595 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
5605593ad2antl1 1182 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 = ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)))
561 simpl1 1188 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝜑)
5622413adant3 1129 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
563562adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
564551adantr 484 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄𝑖) ∈ ℝ*)
565552adantr 484 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
566558adantl 485 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 ∈ ℝ)
567136adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑍𝑋) ∈ ℝ)
568566, 567readdcld 10659 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
5695683ad2antl1 1182 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) ∈ ℝ)
5702003adant3 1129 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
571570adantr 484 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄𝑖) ∈ ℝ)
572561, 139syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝐸𝑋) ∈ ℝ)
573 icogelb 12776 . . . . . . . . . . . . . . . . 17 (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ≤ (𝐸𝑋))
574551, 552, 553, 573syl3anc 1368 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ≤ (𝐸𝑋))
575574adantr 484 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄𝑖) ≤ (𝐸𝑋))
576138ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝐸𝑋) = (𝑋 + (𝑍𝑋)))
57774ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑋 ∈ ℝ)
578558adantl 485 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 ∈ ℝ)
579136ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑍𝑋) ∈ ℝ)
580254ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑋 ∈ ℝ*)
581543rexrd 10680 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ*)
582581adantr 484 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ*)
583 simpr 488 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))))
584 ioogtlb 42071 . . . . . . . . . . . . . . . . . . 19 ((𝑋 ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ*𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑋 < 𝑦)
585580, 582, 583, 584syl3anc 1368 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑋 < 𝑦)
586577, 578, 579, 585ltadd1dd 11240 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑋 + (𝑍𝑋)) < (𝑦 + (𝑍𝑋)))
587576, 586eqbrtrd 5064 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝐸𝑋) < (𝑦 + (𝑍𝑋)))
5885873adantl3 1165 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝐸𝑋) < (𝑦 + (𝑍𝑋)))
589571, 572, 569, 575, 588lelttrd 10787 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑄𝑖) < (𝑦 + (𝑍𝑋)))
590543adantr 484 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ)
591 iooltub 42086 . . . . . . . . . . . . . . . . . 18 ((𝑋 ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ*𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))
592580, 582, 583, 591syl3anc 1368 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))
593578, 590, 579, 592ltadd1dd 11240 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) < (((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) + (𝑍𝑋)))
594208recnd 10658 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
595217adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑍𝑋) ∈ ℂ)
596594, 595npcand 10990 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) + (𝑍𝑋)) = (𝑄‘(𝑖 + 1)))
597596adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) + (𝑍𝑋)) = (𝑄‘(𝑖 + 1)))
598593, 597breqtrd 5068 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) < (𝑄‘(𝑖 + 1)))
5995983adantl3 1165 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) < (𝑄‘(𝑖 + 1)))
600564, 565, 569, 589, 599eliood 42074 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
601563, 600sseldd 3943 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → (𝑦 + (𝑍𝑋)) ∈ 𝐷)
602561, 449syl 17 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → -(⌊‘((𝐵𝑋) / 𝑇)) ∈ ℤ)
603561, 601, 602, 300syl3anc 1368 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → ((𝑦 + (𝑍𝑋)) + (-(⌊‘((𝐵𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
604560, 603eqeltrd 2914 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))) → 𝑦𝐷)
605604ralrimiva 3174 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))𝑦𝐷)
606 dfss3 3930 . . . . . . . . 9 ((𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷 ↔ ∀𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋)))𝑦𝐷)
607605, 606sylibr 237 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷)
608 breq2 5046 . . . . . . . . . 10 (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) → (𝑋 < 𝑦𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋))))
609 oveq2 7148 . . . . . . . . . . 11 (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) → (𝑋(,)𝑦) = (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))))
610609sseq1d 3973 . . . . . . . . . 10 (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) → ((𝑋(,)𝑦) ⊆ 𝐷 ↔ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷))
611608, 610anbi12d 633 . . . . . . . . 9 (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) → ((𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷) ↔ (𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∧ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷)))
612611rspcev 3598 . . . . . . . 8 ((((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∈ ℝ ∧ (𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍𝑋)) ∧ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍𝑋))) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
613544, 557, 607, 612syl12anc 835 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
6146133exp 1116 . . . . . 6 (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))))
615614adantr 484 . . . . 5 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → (𝑖 ∈ (0..^𝑀) → ((𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))))
616615rexlimdv 3269 . . . 4 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → (∃𝑖 ∈ (0..^𝑀)(𝐸𝑋) ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))
617542, 616mpd 15 . . 3 ((𝜑 ∧ (𝐸𝑋) ≠ 𝐵) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
618477, 617pm2.61dane 3098 . 2 (𝜑 → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
619314, 618jca 515 1 (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ∧ ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2114   ≠ wne 3011  ∀wral 3130  ∃wrex 3131  {crab 3134   ⊆ wss 3908   class class class wbr 5042   ↦ cmpt 5122  ran crn 5533   Fn wfn 6329  ⟶wf 6330  ‘cfv 6334  (class class class)co 7140   ↑m cmap 8393  supcsup 8892  ℂcc 10524  ℝcr 10525  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531  ℝ*cxr 10663   < clt 10664   ≤ cle 10665   − cmin 10859  -cneg 10860   / cdiv 11286  ℕcn 11625  ℤcz 11969  ℤ≥cuz 12231  (,)cioo 12726  (,]cioc 12727  [,)cico 12728  [,]cicc 12729  ...cfz 12885  ..^cfzo 13028  ⌊cfl 13155 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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rmo 3138  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-om 7566  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-er 8276  df-map 8395  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-sup 8894  df-inf 8895  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  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 12886  df-fzo 13029  df-fl 13157 This theorem is referenced by:  fourierdlem113  42800
 Copyright terms: Public domain W3C validator