Theorem fourierdlem41 44851

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.

Step	Hyp	Ref	Expression
1		simpr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (𝐸‘𝑋) ∈ ran 𝑄)
2		fourierdlem41.q	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
3		fourierdlem41.m	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℕ)
4		fourierdlem41.p	. . . . . . . . . . . . 13 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
5	4	fourierdlem2 44812	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	3, 5	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
7	2, 6	mpbid 231	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
8	7	simpld 496	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑m (0...𝑀)))
9		elmapi 8840	. . . . . . . . 9 ⊢ (𝑄 ∈ (ℝ ↑m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
10		ffn 6715	. . . . . . . . 9 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
11	8, 9, 10	3syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
12	11	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → 𝑄 Fn (0...𝑀))
13		fvelrnb 6950	. . . . . . 7 ⊢ (𝑄 Fn (0...𝑀) → ((𝐸‘𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋)))
14	12, 13	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ((𝐸‘𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋)))
15	1, 14	mpbid 231	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋))
16		0zd 12567	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 ∈ ℤ)
17		elfzelz 13498	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
18	17	3ad2ant2 1135	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ ℤ)
19		1zzd 12590	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 1 ∈ ℤ)
20	18, 19	zsubcld 12668	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ ℤ)
21		simpll 766	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → 𝜑)
22		elfzle1 13501	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
23	22	anim1i 616	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → (0 ≤ 𝑗 ∧ ¬ 0 < 𝑗))
24		0red 11214	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 0 ∈ ℝ)
25	17	zred 12663	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
26	25	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 𝑗 ∈ ℝ)
27	24, 26	eqleltd 11355	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → (0 = 𝑗 ↔ (0 ≤ 𝑗 ∧ ¬ 0 < 𝑗)))
28	23, 27	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 0 = 𝑗)
29	28	eqcomd 2739	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 𝑗 = 0)
30	29	adantll 713	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → 𝑗 = 0)
31		fveq2 6889	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 0 → (𝑄‘𝑗) = (𝑄‘0))
32	7	simprld 771	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
33	32	simpld 496	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
34	31, 33	sylan9eqr 2795	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 = 0) → (𝑄‘𝑗) = 𝐴)
35	21, 30, 34	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → (𝑄‘𝑗) = 𝐴)
36	35	3adantl3 1169	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄‘𝑗) = 𝐴)
37		simpr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) = (𝐸‘𝑋))
38		fourierdlem41.a	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ ℝ)
39	38	rexrd 11261	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
40		fourierdlem41.b	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ ℝ)
41	40	rexrd 11261	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
42		fourierdlem41.altb	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐴 < 𝐵)
43		fourierdlem41.t	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑇 = (𝐵 − 𝐴)
44		eqid 2733	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
45	38, 40, 42, 43, 44	fourierdlem4 44814	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))):ℝ⟶(𝐴(,]𝐵))
46		fourierdlem41.e	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥)))
47	46	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥))))
48		simpr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
49	40	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
50	49, 48	resubcld 11639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) ∈ ℝ)
51	40, 38	resubcld 11639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
52	43, 51	eqeltrid 2838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → 𝑇 ∈ ℝ)
53	52	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
54		0red 11214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 0 ∈ ℝ)
55	38, 40	posdifd 11798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
56	42, 55	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
57	43	eqcomi 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝐵 − 𝐴) = 𝑇
58	57	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (𝐵 − 𝐴) = 𝑇)
59	56, 58	breqtrd 5174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 0 < 𝑇)
60	54, 59	gtned 11346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → 𝑇 ≠ 0)
61	60	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ≠ 0)
62	50, 53, 61	redivcld 12039	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) ∈ ℝ)
63	62	flcld 13760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)
64	63	zred 12663	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℝ)
65	64, 53	remulcld 11241	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
66		fourierdlem41.z	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
67	66	fvmpt2 7007	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℝ ∧ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ ℝ) → (𝑍‘𝑥) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
68	48, 65, 67	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑍‘𝑥) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
69	68	oveq2d 7422	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (𝑍‘𝑥)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
70	69	mpteq2dva 5248	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
71	47, 70	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
72	71	feq1d 6700	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐸:ℝ⟶(𝐴(,]𝐵) ↔ (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))):ℝ⟶(𝐴(,]𝐵)))
73	45, 72	mpbird 257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
74		fourierdlem41.x	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑋 ∈ ℝ)
75	73, 74	ffvelcdmd 7085	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐸‘𝑋) ∈ (𝐴(,]𝐵))
76		iocgtlb 44202	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸‘𝑋))
77	39, 41, 75, 76	syl3anc 1372	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 < (𝐸‘𝑋))
78	38, 77	gtned 11346	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸‘𝑋) ≠ 𝐴)
79	78	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≠ 𝐴)
80	37, 79	eqnetrd 3009	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ≠ 𝐴)
81	80	adantr 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄‘𝑗) ≠ 𝐴)
82	81	3adantl2 1168	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄‘𝑗) ≠ 𝐴)
83	82	neneqd 2946	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ ¬ 0 < 𝑗) → ¬ (𝑄‘𝑗) = 𝐴)
84	36, 83	condan 817	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 < 𝑗)
85		zltlem1 12612	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (0 < 𝑗 ↔ 0 ≤ (𝑗 − 1)))
86	16, 18, 85	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (0 < 𝑗 ↔ 0 ≤ (𝑗 − 1)))
87	84, 86	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 ≤ (𝑗 − 1))
88		eluz2 12825	. . . . . . . . . . 11 ⊢ ((𝑗 − 1) ∈ (ℤ≥‘0) ↔ (0 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ ∧ 0 ≤ (𝑗 − 1)))
89	16, 20, 87, 88	syl3anbrc 1344	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ (ℤ≥‘0))
90		elfzel2 13496	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
91	90	3ad2ant2 1135	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑀 ∈ ℤ)
92		1red 11212	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → 1 ∈ ℝ)
93	25, 92	resubcld 11639	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
94	90	zred 12663	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
95	25	ltm1d 12143	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑗)
96		elfzle2 13502	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀)
97	93, 25, 94, 95, 96	ltletrd 11371	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
98	97	3ad2ant2 1135	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) < 𝑀)
99		elfzo2 13632	. . . . . . . . . 10 ⊢ ((𝑗 − 1) ∈ (0..^𝑀) ↔ ((𝑗 − 1) ∈ (ℤ≥‘0) ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) < 𝑀))
100	89, 91, 98, 99	syl3anbrc 1344	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ (0..^𝑀))
101	8, 9	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
102	101	3ad2ant1 1134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑄:(0...𝑀)⟶ℝ)
103	93, 94, 97	ltled 11359	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ≤ 𝑀)
104	103	3ad2ant2 1135	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ≤ 𝑀)
105	16, 91, 20, 87, 104	elfzd 13489	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ (0...𝑀))
106	102, 105	ffvelcdmd 7085	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ)
107	106	rexrd 11261	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ*)
108	25	recnd 11239	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
109		1cnd 11206	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 1 ∈ ℂ)
110	108, 109	npcand 11572	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → ((𝑗 − 1) + 1) = 𝑗)
111	110	fveq2d 6893	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄‘𝑗))
112	111	adantl 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄‘𝑗))
113	101	ffvelcdmda 7084	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ)
114	113	rexrd 11261	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ*)
115	112, 114	eqeltrd 2834	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘((𝑗 − 1) + 1)) ∈ ℝ*)
116	115	3adant3 1133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘((𝑗 − 1) + 1)) ∈ ℝ*)
117		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋)
118		fveq2 6889	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → (𝑍‘𝑥) = (𝑍‘𝑋))
119	117, 118	oveq12d 7424	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → (𝑥 + (𝑍‘𝑥)) = (𝑋 + (𝑍‘𝑋)))
120	119	adantl 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥 + (𝑍‘𝑥)) = (𝑋 + (𝑍‘𝑋)))
121	66	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
122		oveq2 7414	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑋 → (𝐵 − 𝑥) = (𝐵 − 𝑋))
123	122	oveq1d 7421	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑋 → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − 𝑋) / 𝑇))
124	123	fveq2d 6893	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑋 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑋) / 𝑇)))
125	124	oveq1d 7421	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑋 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
126	125	adantl 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
127	40, 74	resubcld 11639	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ)
128	127, 52, 60	redivcld 12039	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐵 − 𝑋) / 𝑇) ∈ ℝ)
129	128	flcld 13760	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
130	129	zred 12663	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℝ)
131	130, 52	remulcld 11241	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
132	121, 126, 74, 131	fvmptd 7003	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑍‘𝑋) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
133	132, 131	eqeltrd 2834	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍‘𝑋) ∈ ℝ)
134	74, 133	readdcld 11240	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 + (𝑍‘𝑋)) ∈ ℝ)
135	47, 120, 74, 134	fvmptd 7003	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸‘𝑋) = (𝑋 + (𝑍‘𝑋)))
136	135, 134	eqeltrd 2834	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℝ)
137	136	rexrd 11261	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℝ*)
138	137	3ad2ant1 1134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ℝ*)
139		simp1 1137	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝜑)
140		ovex 7439	. . . . . . . . . . . . . 14 ⊢ (𝑗 − 1) ∈ V
141		eleq1 2822	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑗 − 1) → (𝑖 ∈ (0..^𝑀) ↔ (𝑗 − 1) ∈ (0..^𝑀)))
142	141	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑗 − 1) → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀))))
143		fveq2 6889	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑗 − 1) → (𝑄‘𝑖) = (𝑄‘(𝑗 − 1)))
144		oveq1 7413	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑗 − 1) → (𝑖 + 1) = ((𝑗 − 1) + 1))
145	144	fveq2d 6893	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑗 − 1) → (𝑄‘(𝑖 + 1)) = (𝑄‘((𝑗 − 1) + 1)))
146	143, 145	breq12d 5161	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑗 − 1) → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1))))
147	142, 146	imbi12d 345	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑗 − 1) → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))))
148	7	simprrd 773	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
149	148	r19.21bi 3249	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
150	140, 147, 149	vtocl 3550	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
151	139, 100, 150	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
152	111	3ad2ant2 1135	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄‘𝑗))
153	151, 152	breqtrd 5174	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘𝑗))
154		simp3 1139	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) = (𝐸‘𝑋))
155	153, 154	breqtrd 5174	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) < (𝐸‘𝑋))
156	136	leidd 11777	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘𝑋) ≤ (𝐸‘𝑋))
157	156	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝐸‘𝑋))
158	37	eqcomd 2739	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) = (𝑄‘𝑗))
159	157, 158	breqtrd 5174	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘𝑗))
160	159	3adant2 1132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘𝑗))
161	110	eqcomd 2739	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 = ((𝑗 − 1) + 1))
162	161	fveq2d 6893	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (𝑄‘𝑗) = (𝑄‘((𝑗 − 1) + 1)))
163	162	3ad2ant2 1135	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) = (𝑄‘((𝑗 − 1) + 1)))
164	160, 163	breqtrd 5174	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘((𝑗 − 1) + 1)))
165	107, 116, 138, 155, 164	eliocd 44207	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
166	143, 145	oveq12d 7424	. . . . . . . . . . 11 ⊢ (𝑖 = (𝑗 − 1) → ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
167	166	eleq2d 2820	. . . . . . . . . 10 ⊢ (𝑖 = (𝑗 − 1) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) ↔ (𝐸‘𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))))
168	167	rspcev 3613	. . . . . . . . 9 ⊢ (((𝑗 − 1) ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
169	100, 165, 168	syl2anc 585	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
170	169	3exp 1120	. . . . . . 7 ⊢ (𝜑 → (𝑗 ∈ (0...𝑀) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))))
171	170	adantr 482	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (𝑗 ∈ (0...𝑀) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))))
172	171	rexlimdv 3154	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
173	15, 172	mpd 15	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
174	3	adantr 482	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → 𝑀 ∈ ℕ)
175	101	adantr 482	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ)
176		iocssicc 13411	. . . . . . . 8 ⊢ ((𝑄‘0)(,](𝑄‘𝑀)) ⊆ ((𝑄‘0)[,](𝑄‘𝑀))
177	32	simprd 497	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
178	33, 177	oveq12d 7424	. . . . . . . . 9 ⊢ (𝜑 → ((𝑄‘0)(,](𝑄‘𝑀)) = (𝐴(,]𝐵))
179	75, 178	eleqtrrd 2837	. . . . . . . 8 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ((𝑄‘0)(,](𝑄‘𝑀)))
180	176, 179	sselid 3980	. . . . . . 7 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ((𝑄‘0)[,](𝑄‘𝑀)))
181	180	adantr 482	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → (𝐸‘𝑋) ∈ ((𝑄‘0)[,](𝑄‘𝑀)))
182		simpr 486	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ¬ (𝐸‘𝑋) ∈ ran 𝑄)
183		fveq2 6889	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → (𝑄‘𝑘) = (𝑄‘𝑗))
184	183	breq1d 5158	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → ((𝑄‘𝑘) < (𝐸‘𝑋) ↔ (𝑄‘𝑗) < (𝐸‘𝑋)))
185	184	cbvrabv 3443	. . . . . . 7 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < (𝐸‘𝑋)} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < (𝐸‘𝑋)}
186	185	supeq1i 9439	. . . . . 6 ⊢ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < (𝐸‘𝑋)}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < (𝐸‘𝑋)}, ℝ, < )
187	174, 175, 181, 182, 186	fourierdlem25 44835	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
188		ioossioc 44192	. . . . . . . 8 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))
189	188	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
190	189	sseld 3981	. . . . . 6 ⊢ (((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
191	190	reximdva 3169	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
192	187, 191	mpd 15	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
193	173, 192	pm2.61dan 812	. . 3 ⊢ (𝜑 → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
194	101	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
195		elfzofz 13645	. . . . . . . . . 10 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
196	195	adantl 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
197	194, 196	ffvelcdmd 7085	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
198	197	3adant3 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
199	133	3ad2ant1 1134	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑍‘𝑋) ∈ ℝ)
200	198, 199	resubcld 11639	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ)
201	136	3ad2ant1 1134	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ℝ)
202	198	rexrd 11261	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ*)
203		fzofzp1 13726	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
204	203	adantl 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
205	194, 204	ffvelcdmd 7085	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
206	205	rexrd 11261	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
207	206	3adant3 1133	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
208		simp3 1139	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
209		iocgtlb 44202	. . . . . . . . 9 ⊢ (((𝑄‘𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝐸‘𝑋))
210	202, 207, 208, 209	syl3anc 1372	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝐸‘𝑋))
211	198, 201, 199, 210	ltsub1dd 11823	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < ((𝐸‘𝑋) − (𝑍‘𝑋)))
212	135	oveq1d 7421	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸‘𝑋) − (𝑍‘𝑋)) = ((𝑋 + (𝑍‘𝑋)) − (𝑍‘𝑋)))
213	74	recnd 11239	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℂ)
214	133	recnd 11239	. . . . . . . . . 10 ⊢ (𝜑 → (𝑍‘𝑋) ∈ ℂ)
215	213, 214	pncand 11569	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋 + (𝑍‘𝑋)) − (𝑍‘𝑋)) = 𝑋)
216	212, 215	eqtrd 2773	. . . . . . . 8 ⊢ (𝜑 → ((𝐸‘𝑋) − (𝑍‘𝑋)) = 𝑋)
217	216	3ad2ant1 1134	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐸‘𝑋) − (𝑍‘𝑋)) = 𝑋)
218	211, 217	breqtrd 5174	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋)
219		elioore 13351	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) → 𝑦 ∈ ℝ)
220	132	oveq2d 7422	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑦 + (𝑍‘𝑋)) = (𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
221	130	recnd 11239	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℂ)
222	52	recnd 11239	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑇 ∈ ℂ)
223	221, 222	mulneg1d 11664	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
224	220, 223	oveq12d 7424	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
225	224	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
226		simpr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
227	131	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
228	226, 227	readdcld 11240	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ ℝ)
229	228	recnd 11239	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ ℂ)
230	227	recnd 11239	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
231	229, 230	negsubd 11574	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) − ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
232	226	recnd 11239	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
233	232, 230	pncand 11569	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) − ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = 𝑦)
234	225, 231, 233	3eqtrrd 2778	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
235	219, 234	sylan2 594	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
236	235	3ad2antl1 1186	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
237		simpl1 1192	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝜑)
238		fourierdlem41.qssd	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
239	238	3adant3 1133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
240	239	adantr 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
241	202	adantr 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) ∈ ℝ*)
242	207	adantr 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
243	219	adantl 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
244	133	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑍‘𝑋) ∈ ℝ)
245	243, 244	readdcld 11240	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
246	245	3ad2antl1 1186	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
247	133	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑍‘𝑋) ∈ ℝ)
248	197, 247	resubcld 11639	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ)
249	248	rexrd 11261	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ*)
250	249	adantr 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ*)
251	74	rexrd 11261	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ∈ ℝ*)
252	251	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑋 ∈ ℝ*)
253		simpr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋))
254		ioogtlb 44195	. . . . . . . . . . . . . . 15 ⊢ ((((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑦)
255	250, 252, 253, 254	syl3anc 1372	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑦)
256	197	adantr 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) ∈ ℝ)
257	133	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑍‘𝑋) ∈ ℝ)
258	219	adantl 483	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
259	256, 257, 258	ltsubaddd 11807	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑦 ↔ (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋))))
260	255, 259	mpbid 231	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋)))
261	260	3adantl3 1169	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋)))
262	237, 136	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝐸‘𝑋) ∈ ℝ)
263	205	adantr 482	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
264	263	3adantl3 1169	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
265	74	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑋 ∈ ℝ)
266		iooltub 44210	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 < 𝑋)
267	250, 252, 253, 266	syl3anc 1372	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 < 𝑋)
268	258, 265, 257, 267	ltadd1dd 11822	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝑋 + (𝑍‘𝑋)))
269	135	eqcomd 2739	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 + (𝑍‘𝑋)) = (𝐸‘𝑋))
270	269	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑋 + (𝑍‘𝑋)) = (𝐸‘𝑋))
271	268, 270	breqtrd 5174	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝐸‘𝑋))
272	271	3adantl3 1169	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝐸‘𝑋))
273		iocleub 44203	. . . . . . . . . . . . . . 15 ⊢ (((𝑄‘𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ≤ (𝑄‘(𝑖 + 1)))
274	202, 207, 208, 273	syl3anc 1372	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ≤ (𝑄‘(𝑖 + 1)))
275	274	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘(𝑖 + 1)))
276	246, 262, 264, 272, 275	ltletrd 11371	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝑄‘(𝑖 + 1)))
277	241, 242, 246, 261, 276	eliood 44198	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
278	240, 277	sseldd 3983	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ 𝐷)
279	237, 128	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝐵 − 𝑋) / 𝑇) ∈ ℝ)
280	279	flcld 13760	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
281	280	znegcld 12665	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
282		negex 11455	. . . . . . . . . . 11 ⊢ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ V
283		eleq1 2822	. . . . . . . . . . . . 13 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ))
284	283	3anbi3d 1443	. . . . . . . . . . . 12 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)))
285		oveq1 7413	. . . . . . . . . . . . . 14 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑘 · 𝑇) = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
286	285	oveq2d 7422	. . . . . . . . . . . . 13 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
287	286	eleq1d 2819	. . . . . . . . . . . 12 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
288	284, 287	imbi12d 345	. . . . . . . . . . 11 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)))
289		ovex 7439	. . . . . . . . . . . 12 ⊢ (𝑦 + (𝑍‘𝑋)) ∈ V
290		eleq1 2822	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → (𝑥 ∈ 𝐷 ↔ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷))
291	290	3anbi2d 1442	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ)))
292		oveq1 7413	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)))
293	292	eleq1d 2819	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷))
294	291, 293	imbi12d 345	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → (((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)))
295		fourierdlem41.dper	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)
296	289, 294, 295	vtocl 3550	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)
297	282, 288, 296	vtocl 3550	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
298	237, 278, 281, 297	syl3anc 1372	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
299	236, 298	eqeltrd 2834	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ 𝐷)
300	299	ralrimiva 3147	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑦 ∈ 𝐷)
301		dfss3 3970	. . . . . . 7 ⊢ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷 ↔ ∀𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑦 ∈ 𝐷)
302	300, 301	sylibr 233	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷)
303		breq1 5151	. . . . . . . 8 ⊢ (𝑦 = ((𝑄‘𝑖) − (𝑍‘𝑋)) → (𝑦 < 𝑋 ↔ ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋))
304		oveq1 7413	. . . . . . . . 9 ⊢ (𝑦 = ((𝑄‘𝑖) − (𝑍‘𝑋)) → (𝑦(,)𝑋) = (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋))
305	304	sseq1d 4013	. . . . . . . 8 ⊢ (𝑦 = ((𝑄‘𝑖) − (𝑍‘𝑋)) → ((𝑦(,)𝑋) ⊆ 𝐷 ↔ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷))
306	303, 305	anbi12d 632	. . . . . . 7 ⊢ (𝑦 = ((𝑄‘𝑖) − (𝑍‘𝑋)) → ((𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ↔ (((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋 ∧ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷)))
307	306	rspcev 3613	. . . . . 6 ⊢ ((((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ ∧ (((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋 ∧ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
308	200, 218, 302, 307	syl12anc 836	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
309	308	3exp 1120	. . . 4 ⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))))
310	309	rexlimdv 3154	. . 3 ⊢ (𝜑 → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷)))
311	193, 310	mpd 15	. 2 ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
312		0zd 12567	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℤ)
313	3	nnzd 12582	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
314		1zzd 12590	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℤ)
315		0le1 11734	. . . . . . . . 9 ⊢ 0 ≤ 1
316	315	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ 1)
317	3	nnge1d 12257	. . . . . . . 8 ⊢ (𝜑 → 1 ≤ 𝑀)
318	312, 313, 314, 316, 317	elfzd 13489	. . . . . . 7 ⊢ (𝜑 → 1 ∈ (0...𝑀))
319	101, 318	ffvelcdmd 7085	. . . . . 6 ⊢ (𝜑 → (𝑄‘1) ∈ ℝ)
320	133, 52	resubcld 11639	. . . . . 6 ⊢ (𝜑 → ((𝑍‘𝑋) − 𝑇) ∈ ℝ)
321	319, 320	resubcld 11639	. . . . 5 ⊢ (𝜑 → ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
322	321	adantr 482	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
323	38	recnd 11239	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℂ)
324	323, 222	pncand 11569	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
325	324	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
326	43	oveq2i 7417	. . . . . . . . . . 11 ⊢ (𝐴 + 𝑇) = (𝐴 + (𝐵 − 𝐴))
327	326	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝐴 + 𝑇) = (𝐴 + (𝐵 − 𝐴)))
328	40	recnd 11239	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℂ)
329	323, 328	pncan3d 11571	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
330	329	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
331		id 22	. . . . . . . . . . . 12 ⊢ ((𝐸‘𝑋) = 𝐵 → (𝐸‘𝑋) = 𝐵)
332	331	eqcomd 2739	. . . . . . . . . . 11 ⊢ ((𝐸‘𝑋) = 𝐵 → 𝐵 = (𝐸‘𝑋))
333	332	adantl 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → 𝐵 = (𝐸‘𝑋))
334	327, 330, 333	3eqtrrd 2778	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝐸‘𝑋) = (𝐴 + 𝑇))
335	334	oveq1d 7421	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝐸‘𝑋) − 𝑇) = ((𝐴 + 𝑇) − 𝑇))
336	33	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑄‘0) = 𝐴)
337	325, 335, 336	3eqtr4rd 2784	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑄‘0) = ((𝐸‘𝑋) − 𝑇))
338	337	oveq1d 7421	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑄‘0) − ((𝑍‘𝑋) − 𝑇)) = (((𝐸‘𝑋) − 𝑇) − ((𝑍‘𝑋) − 𝑇)))
339	136	recnd 11239	. . . . . . . 8 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℂ)
340	339, 214, 222	nnncan2d 11603	. . . . . . 7 ⊢ (𝜑 → (((𝐸‘𝑋) − 𝑇) − ((𝑍‘𝑋) − 𝑇)) = ((𝐸‘𝑋) − (𝑍‘𝑋)))
341	340	adantr 482	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (((𝐸‘𝑋) − 𝑇) − ((𝑍‘𝑋) − 𝑇)) = ((𝐸‘𝑋) − (𝑍‘𝑋)))
342	216	adantr 482	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝐸‘𝑋) − (𝑍‘𝑋)) = 𝑋)
343	338, 341, 342	3eqtrrd 2778	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → 𝑋 = ((𝑄‘0) − ((𝑍‘𝑋) − 𝑇)))
344	33, 38	eqeltrd 2834	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
345	3	nngt0d 12258	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝑀)
346		fzolb 13635	. . . . . . . . . 10 ⊢ (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
347	312, 313, 345, 346	syl3anbrc 1344	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0..^𝑀))
348		0re 11213	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
349		eleq1 2822	. . . . . . . . . . . . 13 ⊢ (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀)))
350	349	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑖 = 0 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀))))
351		fveq2 6889	. . . . . . . . . . . . 13 ⊢ (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0))
352		oveq1 7413	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
353	352	fveq2d 6893	. . . . . . . . . . . . 13 ⊢ (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1)))
354	351, 353	breq12d 5161	. . . . . . . . . . . 12 ⊢ (𝑖 = 0 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1))))
355	350, 354	imbi12d 345	. . . . . . . . . . 11 ⊢ (𝑖 = 0 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))))
356	355, 149	vtoclg 3557	. . . . . . . . . 10 ⊢ (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))
357	348, 356	ax-mp 5	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))
358	347, 357	mpdan 686	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1)))
359		0p1e1 12331	. . . . . . . . . 10 ⊢ (0 + 1) = 1
360	359	fveq2i 6892	. . . . . . . . 9 ⊢ (𝑄‘(0 + 1)) = (𝑄‘1)
361	360	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1))
362	358, 361	breqtrd 5174	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) < (𝑄‘1))
363	344, 319, 320, 362	ltsub1dd 11823	. . . . . 6 ⊢ (𝜑 → ((𝑄‘0) − ((𝑍‘𝑋) − 𝑇)) < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
364	363	adantr 482	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑄‘0) − ((𝑍‘𝑋) − 𝑇)) < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
365	343, 364	eqbrtrd 5170	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → 𝑋 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
366		elioore 13351	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) → 𝑦 ∈ ℝ)
367	132	eqcomd 2739	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = (𝑍‘𝑋))
368	367	negeqd 11451	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = -(𝑍‘𝑋))
369	223, 368	eqtrd 2773	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = -(𝑍‘𝑋))
370	222	mullidd 11229	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 · 𝑇) = 𝑇)
371	369, 370	oveq12d 7424	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) + (1 · 𝑇)) = (-(𝑍‘𝑋) + 𝑇))
372	221	negcld 11555	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℂ)
373		1cnd 11206	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℂ)
374	372, 373, 222	adddird 11236	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇) = ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) + (1 · 𝑇)))
375	214, 222	negsubdid 11583	. . . . . . . . . . . . 13 ⊢ (𝜑 → -((𝑍‘𝑋) − 𝑇) = (-(𝑍‘𝑋) + 𝑇))
376	371, 374, 375	3eqtr4d 2783	. . . . . . . . . . . 12 ⊢ (𝜑 → ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇) = -((𝑍‘𝑋) − 𝑇))
377	376	oveq2d 7422	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + -((𝑍‘𝑋) − 𝑇)))
378	377	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + -((𝑍‘𝑋) − 𝑇)))
379	320	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑍‘𝑋) − 𝑇) ∈ ℝ)
380	226, 379	readdcld 11240	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
381	380	recnd 11239	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ℂ)
382	379	recnd 11239	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑍‘𝑋) − 𝑇) ∈ ℂ)
383	381, 382	negsubd 11574	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + -((𝑍‘𝑋) − 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) − ((𝑍‘𝑋) − 𝑇)))
384	232, 382	pncand 11569	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) − ((𝑍‘𝑋) − 𝑇)) = 𝑦)
385	378, 383, 384	3eqtrrd 2778	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)))
386	366, 385	sylan2 594	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)))
387	386	adantlr 714	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)))
388		simpll 766	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝜑)
389	361	eqcomd 2739	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘1) = (𝑄‘(0 + 1)))
390	389	oveq2d 7422	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄‘0)(,)(𝑄‘1)) = ((𝑄‘0)(,)(𝑄‘(0 + 1))))
391	351, 353	oveq12d 7424	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 0 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘0)(,)(𝑄‘(0 + 1))))
392	391	sseq1d 4013	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 0 → (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷 ↔ ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷))
393	350, 392	imbi12d 345	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 0 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)))
394	393, 238	vtoclg 3557	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷))
395	348, 394	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)
396	347, 395	mpdan 686	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)
397	390, 396	eqsstrd 4020	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑄‘0)(,)(𝑄‘1)) ⊆ 𝐷)
398	397	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑄‘0)(,)(𝑄‘1)) ⊆ 𝐷)
399	33, 39	eqeltrd 2834	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ*)
400	399	ad2antrr 725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘0) ∈ ℝ*)
401	319	rexrd 11261	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄‘1) ∈ ℝ*)
402	401	ad2antrr 725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘1) ∈ ℝ*)
403	366, 380	sylan2 594	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
404	403	adantlr 714	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
405	339, 213, 214	subaddd 11586	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐸‘𝑋) − 𝑋) = (𝑍‘𝑋) ↔ (𝑋 + (𝑍‘𝑋)) = (𝐸‘𝑋)))
406	269, 405	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸‘𝑋) − 𝑋) = (𝑍‘𝑋))
407		oveq1 7413	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸‘𝑋) = 𝐵 → ((𝐸‘𝑋) − 𝑋) = (𝐵 − 𝑋))
408	406, 407	sylan9req 2794	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑍‘𝑋) = (𝐵 − 𝑋))
409	408	oveq1d 7421	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑍‘𝑋) − 𝑇) = ((𝐵 − 𝑋) − 𝑇))
410	409	oveq2d 7422	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑋 + ((𝑍‘𝑋) − 𝑇)) = (𝑋 + ((𝐵 − 𝑋) − 𝑇)))
411	127	recnd 11239	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℂ)
412	213, 411, 222	addsubassd 11588	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 + (𝐵 − 𝑋)) − 𝑇) = (𝑋 + ((𝐵 − 𝑋) − 𝑇)))
413	412	eqcomd 2739	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 + ((𝐵 − 𝑋) − 𝑇)) = ((𝑋 + (𝐵 − 𝑋)) − 𝑇))
414	413	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑋 + ((𝐵 − 𝑋) − 𝑇)) = ((𝑋 + (𝐵 − 𝑋)) − 𝑇))
415	328, 222, 323	subsub23d 43984	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 − 𝑇) = 𝐴 ↔ (𝐵 − 𝐴) = 𝑇))
416	58, 415	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 − 𝑇) = 𝐴)
417	213, 328	pncan3d 11571	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 + (𝐵 − 𝑋)) = 𝐵)
418	417	oveq1d 7421	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 + (𝐵 − 𝑋)) − 𝑇) = (𝐵 − 𝑇))
419	416, 418, 33	3eqtr4d 2783	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑋 + (𝐵 − 𝑋)) − 𝑇) = (𝑄‘0))
420	419	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑋 + (𝐵 − 𝑋)) − 𝑇) = (𝑄‘0))
421	410, 414, 420	3eqtrrd 2778	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑄‘0) = (𝑋 + ((𝑍‘𝑋) − 𝑇)))
422	421	adantr 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘0) = (𝑋 + ((𝑍‘𝑋) − 𝑇)))
423	74	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑋 ∈ ℝ)
424	366	adantl 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 ∈ ℝ)
425	320	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑍‘𝑋) − 𝑇) ∈ ℝ)
426	251	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑋 ∈ ℝ*)
427	321	rexrd 11261	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ*)
428	427	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ*)
429		simpr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))))
430		ioogtlb 44195	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ ℝ* ∧ ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ* ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑋 < 𝑦)
431	426, 428, 429, 430	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑋 < 𝑦)
432	423, 424, 425, 431	ltadd1dd 11822	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑋 + ((𝑍‘𝑋) − 𝑇)) < (𝑦 + ((𝑍‘𝑋) − 𝑇)))
433	432	adantlr 714	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑋 + ((𝑍‘𝑋) − 𝑇)) < (𝑦 + ((𝑍‘𝑋) − 𝑇)))
434	422, 433	eqbrtrd 5170	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘0) < (𝑦 + ((𝑍‘𝑋) − 𝑇)))
435		iooltub 44210	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ ℝ* ∧ ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ* ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
436	426, 428, 429, 435	syl3anc 1372	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
437	319	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘1) ∈ ℝ)
438	424, 425, 437	ltaddsubd 11811	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) < (𝑄‘1) ↔ 𝑦 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))))
439	436, 438	mpbird 257	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) < (𝑄‘1))
440	439	adantlr 714	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) < (𝑄‘1))
441	400, 402, 404, 434, 440	eliood 44198	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ((𝑄‘0)(,)(𝑄‘1)))
442	398, 441	sseldd 3983	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷)
443	129	znegcld 12665	. . . . . . . . . 10 ⊢ (𝜑 → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
444	443	peano2zd 12666	. . . . . . . . 9 ⊢ (𝜑 → (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ)
445	444	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ)
446		ovex 7439	. . . . . . . . 9 ⊢ (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ V
447		eleq1 2822	. . . . . . . . . . 11 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → (𝑘 ∈ ℤ ↔ (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ))
448	447	3anbi3d 1443	. . . . . . . . . 10 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ)))
449		oveq1 7413	. . . . . . . . . . . 12 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → (𝑘 · 𝑇) = ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇))
450	449	oveq2d 7422	. . . . . . . . . . 11 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)))
451	450	eleq1d 2819	. . . . . . . . . 10 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → (((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷))
452	448, 451	imbi12d 345	. . . . . . . . 9 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → (((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)))
453		ovex 7439	. . . . . . . . . 10 ⊢ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ V
454		eleq1 2822	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → (𝑥 ∈ 𝐷 ↔ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷))
455	454	3anbi2d 1442	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ)))
456		oveq1 7413	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)))
457	456	eleq1d 2819	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷))
458	455, 457	imbi12d 345	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → (((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷)))
459	453, 458, 295	vtocl 3550	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷)
460	446, 452, 459	vtocl 3550	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)
461	388, 442, 445, 460	syl3anc 1372	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)
462	387, 461	eqeltrd 2834	. . . . . 6 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 ∈ 𝐷)
463	462	ralrimiva 3147	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ∀𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))𝑦 ∈ 𝐷)
464		dfss3 3970	. . . . 5 ⊢ ((𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷 ↔ ∀𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))𝑦 ∈ 𝐷)
465	463, 464	sylibr 233	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷)
466		breq2 5152	. . . . . 6 ⊢ (𝑦 = ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) → (𝑋 < 𝑦 ↔ 𝑋 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))))
467		oveq2 7414	. . . . . . 7 ⊢ (𝑦 = ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) → (𝑋(,)𝑦) = (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))))
468	467	sseq1d 4013	. . . . . 6 ⊢ (𝑦 = ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) → ((𝑋(,)𝑦) ⊆ 𝐷 ↔ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷))
469	466, 468	anbi12d 632	. . . . 5 ⊢ (𝑦 = ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) → ((𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷) ↔ (𝑋 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∧ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷)))
470	469	rspcev 3613	. . . 4 ⊢ ((((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ ∧ (𝑋 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∧ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
471	322, 365, 465, 470	syl12anc 836	. . 3 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
472	15	adantlr 714	. . . . . 6 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋))
473		simp2 1138	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ (0...𝑀))
474	25	3ad2ant2 1135	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ ℝ)
475	94	3ad2ant2 1135	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑀 ∈ ℝ)
476	96	3ad2ant2 1135	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ≤ 𝑀)
477		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑄‘𝑗) = (𝐸‘𝑋) → (𝑄‘𝑗) = (𝐸‘𝑋))
478	477	eqcomd 2739	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄‘𝑗) = (𝐸‘𝑋) → (𝐸‘𝑋) = (𝑄‘𝑗))
479	478	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝑄‘𝑗) = (𝐸‘𝑋) ∧ 𝑀 = 𝑗) → (𝐸‘𝑋) = (𝑄‘𝑗))
480	479	3ad2antl3 1188	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → (𝐸‘𝑋) = (𝑄‘𝑗))
481		fveq2 6889	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 = 𝑗 → (𝑄‘𝑀) = (𝑄‘𝑗))
482	481	eqcomd 2739	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 = 𝑗 → (𝑄‘𝑗) = (𝑄‘𝑀))
483	482	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → (𝑄‘𝑗) = (𝑄‘𝑀))
484	177	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑀 = 𝑗) → (𝑄‘𝑀) = 𝐵)
485	484	3ad2antl1 1186	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → (𝑄‘𝑀) = 𝐵)
486	480, 483, 485	3eqtrd 2777	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → (𝐸‘𝑋) = 𝐵)
487		neneq 2947	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸‘𝑋) ≠ 𝐵 → ¬ (𝐸‘𝑋) = 𝐵)
488	487	ad2antlr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑀 = 𝑗) → ¬ (𝐸‘𝑋) = 𝐵)
489	488	3ad2antl1 1186	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → ¬ (𝐸‘𝑋) = 𝐵)
490	486, 489	pm2.65da 816	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → ¬ 𝑀 = 𝑗)
491	490	neqned 2948	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑀 ≠ 𝑗)
492	474, 475, 476, 491	leneltd 11365	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 < 𝑀)
493		elfzfzo 43973	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0..^𝑀) ↔ (𝑗 ∈ (0...𝑀) ∧ 𝑗 < 𝑀))
494	473, 492, 493	sylanbrc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ (0..^𝑀))
495	114	adantlr 714	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ*)
496	495	3adant3 1133	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ∈ ℝ*)
497		simp1l 1198	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝜑)
498	101	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
499		fzofzp1 13726	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0..^𝑀) → (𝑗 + 1) ∈ (0...𝑀))
500	499	adantl 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑗 + 1) ∈ (0...𝑀))
501	498, 500	ffvelcdmd 7085	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ)
502	501	rexrd 11261	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ*)
503	497, 494, 502	syl2anc 585	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 + 1)) ∈ ℝ*)
504	138	3adant1r 1178	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ℝ*)
505	37, 157	eqbrtrd 5170	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ≤ (𝐸‘𝑋))
506	505	adantlr 714	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ≤ (𝐸‘𝑋))
507	506	3adant2 1132	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ≤ (𝐸‘𝑋))
508	478	3ad2ant3 1136	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) = (𝑄‘𝑗))
509		eleq1 2822	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑖 ∈ (0..^𝑀) ↔ 𝑗 ∈ (0..^𝑀)))
510	509	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑗 ∈ (0..^𝑀))))
511		fveq2 6889	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑄‘𝑖) = (𝑄‘𝑗))
512		oveq1 7413	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
513	512	fveq2d 6893	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑗 + 1)))
514	511, 513	breq12d 5161	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑗 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘𝑗) < (𝑄‘(𝑗 + 1))))
515	510, 514	imbi12d 345	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))))
516	515, 149	chvarvv 2003	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))
517	497, 494, 516	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))
518	508, 517	eqbrtrd 5170	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) < (𝑄‘(𝑗 + 1)))
519	496, 503, 504, 507, 518	elicod 13371	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ((𝑄‘𝑗)[,)(𝑄‘(𝑗 + 1))))
520	511, 513	oveq12d 7424	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) = ((𝑄‘𝑗)[,)(𝑄‘(𝑗 + 1))))
521	520	eleq2d 2820	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) ↔ (𝐸‘𝑋) ∈ ((𝑄‘𝑗)[,)(𝑄‘(𝑗 + 1)))))
522	521	rspcev 3613	. . . . . . . . . 10 ⊢ ((𝑗 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑗)[,)(𝑄‘(𝑗 + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
523	494, 519, 522	syl2anc 585	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
524	523	3exp 1120	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → (𝑗 ∈ (0...𝑀) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))))
525	524	adantr 482	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (𝑗 ∈ (0...𝑀) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))))
526	525	rexlimdv 3154	. . . . . 6 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))))
527	472, 526	mpd 15	. . . . 5 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
528		ioossico 13412	. . . . . . . . . . 11 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))
529		simpr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
530	528, 529	sselid 3980	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
531	530	ex 414	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))))
532	531	adantlr 714	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))))
533	532	reximdva 3169	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))))
534	187, 533	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
535	534	adantlr 714	. . . . 5 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
536	527, 535	pm2.61dan 812	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
537	205, 247	resubcld 11639	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ)
538	537	3adant3 1133	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ)
539	216	eqcomd 2739	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 = ((𝐸‘𝑋) − (𝑍‘𝑋)))
540	539	3ad2ant1 1134	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → 𝑋 = ((𝐸‘𝑋) − (𝑍‘𝑋)))
541	136	3ad2ant1 1134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ℝ)
542	205	3adant3 1133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
543	133	3ad2ant1 1134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑍‘𝑋) ∈ ℝ)
544	197	rexrd 11261	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ*)
545	544	3adant3 1133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ*)
546	206	3adant3 1133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
547		simp3 1139	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
548		icoltub 44208	. . . . . . . . . . 11 ⊢ (((𝑄‘𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) < (𝑄‘(𝑖 + 1)))
549	545, 546, 547, 548	syl3anc 1372	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) < (𝑄‘(𝑖 + 1)))
550	541, 542, 543, 549	ltsub1dd 11823	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝐸‘𝑋) − (𝑍‘𝑋)) < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))
551	540, 550	eqbrtrd 5170	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → 𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))
552		elioore 13351	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) → 𝑦 ∈ ℝ)
553	552, 234	sylan2 594	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
554	553	3ad2antl1 1186	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
555		simpl1 1192	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝜑)
556	238	3adant3 1133	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
557	556	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
558	545	adantr 482	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘𝑖) ∈ ℝ*)
559	546	adantr 482	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
560	552	adantl 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 ∈ ℝ)
561	133	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑍‘𝑋) ∈ ℝ)
562	560, 561	readdcld 11240	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
563	562	3ad2antl1 1186	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
564	197	3adant3 1133	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
565	564	adantr 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘𝑖) ∈ ℝ)
566	555, 136	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝐸‘𝑋) ∈ ℝ)
567		icogelb 13372	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ≤ (𝐸‘𝑋))
568	545, 546, 547, 567	syl3anc 1372	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ≤ (𝐸‘𝑋))
569	568	adantr 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘𝑖) ≤ (𝐸‘𝑋))
570	135	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝐸‘𝑋) = (𝑋 + (𝑍‘𝑋)))
571	74	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑋 ∈ ℝ)
572	552	adantl 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 ∈ ℝ)
573	133	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑍‘𝑋) ∈ ℝ)
574	251	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑋 ∈ ℝ*)
575	537	rexrd 11261	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ*)
576	575	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ*)
577		simpr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))))
578		ioogtlb 44195	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋 ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ* ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑋 < 𝑦)
579	574, 576, 577, 578	syl3anc 1372	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑋 < 𝑦)
580	571, 572, 573, 579	ltadd1dd 11822	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑋 + (𝑍‘𝑋)) < (𝑦 + (𝑍‘𝑋)))
581	570, 580	eqbrtrd 5170	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝐸‘𝑋) < (𝑦 + (𝑍‘𝑋)))
582	581	3adantl3 1169	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝐸‘𝑋) < (𝑦 + (𝑍‘𝑋)))
583	565, 566, 563, 569, 582	lelttrd 11369	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋)))
584	537	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ)
585		iooltub 44210	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋 ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ* ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))
586	574, 576, 577, 585	syl3anc 1372	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))
587	572, 584, 573, 586	ltadd1dd 11822	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) < (((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) + (𝑍‘𝑋)))
588	205	recnd 11239	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
589	214	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑍‘𝑋) ∈ ℂ)
590	588, 589	npcand 11572	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) + (𝑍‘𝑋)) = (𝑄‘(𝑖 + 1)))
591	590	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) + (𝑍‘𝑋)) = (𝑄‘(𝑖 + 1)))
592	587, 591	breqtrd 5174	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) < (𝑄‘(𝑖 + 1)))
593	592	3adantl3 1169	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) < (𝑄‘(𝑖 + 1)))
594	558, 559, 563, 583, 593	eliood 44198	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
595	557, 594	sseldd 3983	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) ∈ 𝐷)
596	555, 443	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
597	555, 595, 596, 297	syl3anc 1372	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
598	554, 597	eqeltrd 2834	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 ∈ 𝐷)
599	598	ralrimiva 3147	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))𝑦 ∈ 𝐷)
600		dfss3 3970	. . . . . . . . 9 ⊢ ((𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷 ↔ ∀𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))𝑦 ∈ 𝐷)
601	599, 600	sylibr 233	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷)
602		breq2 5152	. . . . . . . . . 10 ⊢ (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) → (𝑋 < 𝑦 ↔ 𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))))
603		oveq2 7414	. . . . . . . . . . 11 ⊢ (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) → (𝑋(,)𝑦) = (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))))
604	603	sseq1d 4013	. . . . . . . . . 10 ⊢ (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) → ((𝑋(,)𝑦) ⊆ 𝐷 ↔ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷))
605	602, 604	anbi12d 632	. . . . . . . . 9 ⊢ (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) → ((𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷) ↔ (𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∧ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷)))
606	605	rspcev 3613	. . . . . . . 8 ⊢ ((((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ ∧ (𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∧ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
607	538, 551, 601, 606	syl12anc 836	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
608	607	3exp 1120	. . . . . 6 ⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))))
609	608	adantr 482	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → (𝑖 ∈ (0..^𝑀) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))))
610	609	rexlimdv 3154	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))
611	536, 610	mpd 15	. . 3 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
612	471, 611	pm2.61dane 3030	. 2 ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
613	311, 612	jca 513	1 ⊢ (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ∧ ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   ≠ wne 2941  ∀wral 3062  ∃wrex 3071  {crab 3433   ⊆ wss 3948   class class class wbr 5148   ↦ cmpt 5231  ran crn 5677   Fn wfn 6536  ⟶wf 6537  ‘cfv 6541  (class class class)co 7406   ↑_m cmap 8817  supcsup 9432  ℂcc 11105  ℝcr 11106  0cc0 11107  1c1 11108   + caddc 11110   · cmul 11112  ℝ^*cxr 11244   < clt 11245   ≤ cle 11246   − cmin 11441  -cneg 11442   / cdiv 11868  ℕcn 12209  ℤcz 12555  ℤ_≥cuz 12819  (,)cioo 13321  (,]cioc 13322  [,)cico 13323  [,]cicc 13324  ...cfz 13481  ..^cfzo 13624  ⌊cfl 13752

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-er 8700  df-map 8819  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-sup 9434  df-inf 9435  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-n0 12470  df-z 12556  df-uz 12820  df-rp 12972  df-ioo 13325  df-ioc 13326  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754

This theorem is referenced by:  fourierdlem113  44922