fourierdlem41 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem41 46168

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 484	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (𝐸‘𝑋) ∈ ran 𝑄)
2		fourierdlem41.q	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
3		fourierdlem41.m	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℕ)
4		fourierdlem41.p	. . . . . . . . . . . . 13 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
5	4	fourierdlem2 46129	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	3, 5	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
7	2, 6	mpbid 232	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
8	7	simpld 494	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
9		elmapi 8890	. . . . . . . . 9 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
10		ffn 6735	. . . . . . . . 9 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
11	8, 9, 10	3syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
12	11	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → 𝑄 Fn (0...𝑀))
13		fvelrnb 6968	. . . . . . 7 ⊢ (𝑄 Fn (0...𝑀) → ((𝐸‘𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋)))
14	12, 13	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ((𝐸‘𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋)))
15	1, 14	mpbid 232	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋))
16		0zd 12627	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 ∈ ℤ)
17		elfzelz 13565	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
18	17	3ad2ant2 1134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ ℤ)
19		1zzd 12650	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 1 ∈ ℤ)
20	18, 19	zsubcld 12729	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ ℤ)
21		simpll 766	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → 𝜑)
22		elfzle1 13568	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
23	22	anim1i 615	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → (0 ≤ 𝑗 ∧ ¬ 0 < 𝑗))
24		0red 11265	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 0 ∈ ℝ)
25	17	zred 12724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
26	25	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 𝑗 ∈ ℝ)
27	24, 26	eqleltd 11406	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → (0 = 𝑗 ↔ (0 ≤ 𝑗 ∧ ¬ 0 < 𝑗)))
28	23, 27	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 0 = 𝑗)
29	28	eqcomd 2742	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 𝑗 = 0)
30	29	adantll 714	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → 𝑗 = 0)
31		fveq2 6905	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 0 → (𝑄‘𝑗) = (𝑄‘0))
32	7	simprld 771	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
33	32	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
34	31, 33	sylan9eqr 2798	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 = 0) → (𝑄‘𝑗) = 𝐴)
35	21, 30, 34	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → (𝑄‘𝑗) = 𝐴)
36	35	3adantl3 1168	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄‘𝑗) = 𝐴)
37		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) = (𝐸‘𝑋))
38		fourierdlem41.a	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ ℝ)
39	38	rexrd 11312	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
40		fourierdlem41.b	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ ℝ)
41	40	rexrd 11312	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
42		fourierdlem41.altb	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐴 < 𝐵)
43		fourierdlem41.t	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑇 = (𝐵 − 𝐴)
44		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
45	38, 40, 42, 43, 44	fourierdlem4 46131	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))):ℝ⟶(𝐴(,]𝐵))
46		fourierdlem41.e	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥)))
47	46	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥))))
48		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
49	40	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
50	49, 48	resubcld 11692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) ∈ ℝ)
51	40, 38	resubcld 11692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
52	43, 51	eqeltrid 2844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → 𝑇 ∈ ℝ)
53	52	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
54		0red 11265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 0 ∈ ℝ)
55	38, 40	posdifd 11851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
56	42, 55	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
57	43	eqcomi 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝐵 − 𝐴) = 𝑇
58	57	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (𝐵 − 𝐴) = 𝑇)
59	56, 58	breqtrd 5168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 0 < 𝑇)
60	54, 59	gtned 11397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → 𝑇 ≠ 0)
61	60	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ≠ 0)
62	50, 53, 61	redivcld 12096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) ∈ ℝ)
63	62	flcld 13839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)
64	63	zred 12724	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℝ)
65	64, 53	remulcld 11292	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
66		fourierdlem41.z	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
67	66	fvmpt2 7026	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℝ ∧ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ ℝ) → (𝑍‘𝑥) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
68	48, 65, 67	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑍‘𝑥) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
69	68	oveq2d 7448	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (𝑍‘𝑥)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
70	69	mpteq2dva 5241	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
71	47, 70	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
72	71	feq1d 6719	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐸:ℝ⟶(𝐴(,]𝐵) ↔ (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))):ℝ⟶(𝐴(,]𝐵)))
73	45, 72	mpbird 257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
74		fourierdlem41.x	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑋 ∈ ℝ)
75	73, 74	ffvelcdmd 7104	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐸‘𝑋) ∈ (𝐴(,]𝐵))
76		iocgtlb 45520	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸‘𝑋))
77	39, 41, 75, 76	syl3anc 1372	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 < (𝐸‘𝑋))
78	38, 77	gtned 11397	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸‘𝑋) ≠ 𝐴)
79	78	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≠ 𝐴)
80	37, 79	eqnetrd 3007	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ≠ 𝐴)
81	80	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄‘𝑗) ≠ 𝐴)
82	81	3adantl2 1167	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄‘𝑗) ≠ 𝐴)
83	82	neneqd 2944	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ ¬ 0 < 𝑗) → ¬ (𝑄‘𝑗) = 𝐴)
84	36, 83	condan 817	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 < 𝑗)
85		zltlem1 12672	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (0 < 𝑗 ↔ 0 ≤ (𝑗 − 1)))
86	16, 18, 85	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (0 < 𝑗 ↔ 0 ≤ (𝑗 − 1)))
87	84, 86	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 ≤ (𝑗 − 1))
88		eluz2 12885	. . . . . . . . . . 11 ⊢ ((𝑗 − 1) ∈ (ℤ_≥‘0) ↔ (0 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ ∧ 0 ≤ (𝑗 − 1)))
89	16, 20, 87, 88	syl3anbrc 1343	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ (ℤ_≥‘0))
90		elfzel2 13563	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
91	90	3ad2ant2 1134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑀 ∈ ℤ)
92		1red 11263	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → 1 ∈ ℝ)
93	25, 92	resubcld 11692	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
94	90	zred 12724	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
95	25	ltm1d 12201	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑗)
96		elfzle2 13569	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀)
97	93, 25, 94, 95, 96	ltletrd 11422	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
98	97	3ad2ant2 1134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) < 𝑀)
99		elfzo2 13703	. . . . . . . . . 10 ⊢ ((𝑗 − 1) ∈ (0..^𝑀) ↔ ((𝑗 − 1) ∈ (ℤ_≥‘0) ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) < 𝑀))
100	89, 91, 98, 99	syl3anbrc 1343	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ (0..^𝑀))
101	8, 9	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
102	101	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑄:(0...𝑀)⟶ℝ)
103	93, 94, 97	ltled 11410	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ≤ 𝑀)
104	103	3ad2ant2 1134	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ≤ 𝑀)
105	16, 91, 20, 87, 104	elfzd 13556	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ (0...𝑀))
106	102, 105	ffvelcdmd 7104	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ)
107	106	rexrd 11312	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ^*)
108	25	recnd 11290	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
109		1cnd 11257	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 1 ∈ ℂ)
110	108, 109	npcand 11625	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → ((𝑗 − 1) + 1) = 𝑗)
111	110	fveq2d 6909	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄‘𝑗))
112	111	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄‘𝑗))
113	101	ffvelcdmda 7103	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ)
114	113	rexrd 11312	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ^*)
115	112, 114	eqeltrd 2840	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘((𝑗 − 1) + 1)) ∈ ℝ^*)
116	115	3adant3 1132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘((𝑗 − 1) + 1)) ∈ ℝ^*)
117		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋)
118		fveq2 6905	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → (𝑍‘𝑥) = (𝑍‘𝑋))
119	117, 118	oveq12d 7450	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → (𝑥 + (𝑍‘𝑥)) = (𝑋 + (𝑍‘𝑋)))
120	119	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥 + (𝑍‘𝑥)) = (𝑋 + (𝑍‘𝑋)))
121	66	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
122		oveq2 7440	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑋 → (𝐵 − 𝑥) = (𝐵 − 𝑋))
123	122	oveq1d 7447	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑋 → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − 𝑋) / 𝑇))
124	123	fveq2d 6909	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑋 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑋) / 𝑇)))
125	124	oveq1d 7447	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑋 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
126	125	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
127	40, 74	resubcld 11692	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ)
128	127, 52, 60	redivcld 12096	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐵 − 𝑋) / 𝑇) ∈ ℝ)
129	128	flcld 13839	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
130	129	zred 12724	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℝ)
131	130, 52	remulcld 11292	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
132	121, 126, 74, 131	fvmptd 7022	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑍‘𝑋) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
133	132, 131	eqeltrd 2840	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍‘𝑋) ∈ ℝ)
134	74, 133	readdcld 11291	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 + (𝑍‘𝑋)) ∈ ℝ)
135	47, 120, 74, 134	fvmptd 7022	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸‘𝑋) = (𝑋 + (𝑍‘𝑋)))
136	135, 134	eqeltrd 2840	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℝ)
137	136	rexrd 11312	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℝ^*)
138	137	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ℝ^*)
139		simp1 1136	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝜑)
140		ovex 7465	. . . . . . . . . . . . . 14 ⊢ (𝑗 − 1) ∈ V
141		eleq1 2828	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑗 − 1) → (𝑖 ∈ (0..^𝑀) ↔ (𝑗 − 1) ∈ (0..^𝑀)))
142	141	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑗 − 1) → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀))))
143		fveq2 6905	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑗 − 1) → (𝑄‘𝑖) = (𝑄‘(𝑗 − 1)))
144		oveq1 7439	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑗 − 1) → (𝑖 + 1) = ((𝑗 − 1) + 1))
145	144	fveq2d 6909	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑗 − 1) → (𝑄‘(𝑖 + 1)) = (𝑄‘((𝑗 − 1) + 1)))
146	143, 145	breq12d 5155	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑗 − 1) → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1))))
147	142, 146	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑗 − 1) → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))))
148	7	simprrd 773	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
149	148	r19.21bi 3250	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
150	140, 147, 149	vtocl 3557	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
151	139, 100, 150	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
152	111	3ad2ant2 1134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄‘𝑗))
153	151, 152	breqtrd 5168	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘𝑗))
154		simp3 1138	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) = (𝐸‘𝑋))
155	153, 154	breqtrd 5168	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) < (𝐸‘𝑋))
156	136	leidd 11830	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘𝑋) ≤ (𝐸‘𝑋))
157	156	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝐸‘𝑋))
158	37	eqcomd 2742	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) = (𝑄‘𝑗))
159	157, 158	breqtrd 5168	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘𝑗))
160	159	3adant2 1131	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘𝑗))
161	110	eqcomd 2742	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 = ((𝑗 − 1) + 1))
162	161	fveq2d 6909	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (𝑄‘𝑗) = (𝑄‘((𝑗 − 1) + 1)))
163	162	3ad2ant2 1134	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) = (𝑄‘((𝑗 − 1) + 1)))
164	160, 163	breqtrd 5168	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘((𝑗 − 1) + 1)))
165	107, 116, 138, 155, 164	eliocd 45525	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
166	143, 145	oveq12d 7450	. . . . . . . . . . 11 ⊢ (𝑖 = (𝑗 − 1) → ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
167	166	eleq2d 2826	. . . . . . . . . 10 ⊢ (𝑖 = (𝑗 − 1) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) ↔ (𝐸‘𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))))
168	167	rspcev 3621	. . . . . . . . 9 ⊢ (((𝑗 − 1) ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
169	100, 165, 168	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
170	169	3exp 1119	. . . . . . 7 ⊢ (𝜑 → (𝑗 ∈ (0...𝑀) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))))
171	170	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (𝑗 ∈ (0...𝑀) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))))
172	171	rexlimdv 3152	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
173	15, 172	mpd 15	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
174	3	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → 𝑀 ∈ ℕ)
175	101	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ)
176		iocssicc 13478	. . . . . . . 8 ⊢ ((𝑄‘0)(,](𝑄‘𝑀)) ⊆ ((𝑄‘0)[,](𝑄‘𝑀))
177	32	simprd 495	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
178	33, 177	oveq12d 7450	. . . . . . . . 9 ⊢ (𝜑 → ((𝑄‘0)(,](𝑄‘𝑀)) = (𝐴(,]𝐵))
179	75, 178	eleqtrrd 2843	. . . . . . . 8 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ((𝑄‘0)(,](𝑄‘𝑀)))
180	176, 179	sselid 3980	. . . . . . 7 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ((𝑄‘0)[,](𝑄‘𝑀)))
181	180	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → (𝐸‘𝑋) ∈ ((𝑄‘0)[,](𝑄‘𝑀)))
182		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ¬ (𝐸‘𝑋) ∈ ran 𝑄)
183		fveq2 6905	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → (𝑄‘𝑘) = (𝑄‘𝑗))
184	183	breq1d 5152	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → ((𝑄‘𝑘) < (𝐸‘𝑋) ↔ (𝑄‘𝑗) < (𝐸‘𝑋)))
185	184	cbvrabv 3446	. . . . . . 7 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < (𝐸‘𝑋)} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < (𝐸‘𝑋)}
186	185	supeq1i 9488	. . . . . 6 ⊢ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < (𝐸‘𝑋)}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < (𝐸‘𝑋)}, ℝ, < )
187	174, 175, 181, 182, 186	fourierdlem25 46152	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
188		ioossioc 45510	. . . . . . . 8 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))
189	188	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
190	189	sseld 3981	. . . . . 6 ⊢ (((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
191	190	reximdva 3167	. . . . 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 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
195		elfzofz 13716	. . . . . . . . . 10 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
196	195	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
197	194, 196	ffvelcdmd 7104	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
198	197	3adant3 1132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
199	133	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑍‘𝑋) ∈ ℝ)
200	198, 199	resubcld 11692	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ)
201	136	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ℝ)
202	198	rexrd 11312	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ^*)
203		fzofzp1 13804	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
204	203	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
205	194, 204	ffvelcdmd 7104	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
206	205	rexrd 11312	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
207	206	3adant3 1132	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
208		simp3 1138	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
209		iocgtlb 45520	. . . . . . . . 9 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝐸‘𝑋))
210	202, 207, 208, 209	syl3anc 1372	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝐸‘𝑋))
211	198, 201, 199, 210	ltsub1dd 11876	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < ((𝐸‘𝑋) − (𝑍‘𝑋)))
212	135	oveq1d 7447	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸‘𝑋) − (𝑍‘𝑋)) = ((𝑋 + (𝑍‘𝑋)) − (𝑍‘𝑋)))
213	74	recnd 11290	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℂ)
214	133	recnd 11290	. . . . . . . . . 10 ⊢ (𝜑 → (𝑍‘𝑋) ∈ ℂ)
215	213, 214	pncand 11622	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋 + (𝑍‘𝑋)) − (𝑍‘𝑋)) = 𝑋)
216	212, 215	eqtrd 2776	. . . . . . . 8 ⊢ (𝜑 → ((𝐸‘𝑋) − (𝑍‘𝑋)) = 𝑋)
217	216	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐸‘𝑋) − (𝑍‘𝑋)) = 𝑋)
218	211, 217	breqtrd 5168	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋)
219		elioore 13418	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) → 𝑦 ∈ ℝ)
220	132	oveq2d 7448	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑦 + (𝑍‘𝑋)) = (𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
221	130	recnd 11290	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℂ)
222	52	recnd 11290	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑇 ∈ ℂ)
223	221, 222	mulneg1d 11717	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
224	220, 223	oveq12d 7450	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
225	224	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
226		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
227	131	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
228	226, 227	readdcld 11291	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ ℝ)
229	228	recnd 11290	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ ℂ)
230	227	recnd 11290	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
231	229, 230	negsubd 11627	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) − ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
232	226	recnd 11290	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
233	232, 230	pncand 11622	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) − ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = 𝑦)
234	225, 231, 233	3eqtrrd 2781	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
235	219, 234	sylan2 593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
236	235	3ad2antl1 1185	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
237		simpl1 1191	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝜑)
238		fourierdlem41.qssd	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
239	238	3adant3 1132	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
240	239	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
241	202	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) ∈ ℝ^*)
242	207	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
243	219	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
244	133	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑍‘𝑋) ∈ ℝ)
245	243, 244	readdcld 11291	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
246	245	3ad2antl1 1185	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
247	133	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑍‘𝑋) ∈ ℝ)
248	197, 247	resubcld 11692	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ)
249	248	rexrd 11312	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ^*)
250	249	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ^*)
251	74	rexrd 11312	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ∈ ℝ^*)
252	251	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑋 ∈ ℝ^*)
253		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋))
254		ioogtlb 45513	. . . . . . . . . . . . . . 15 ⊢ ((((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ^* ∧ 𝑋 ∈ ℝ^* ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑦)
255	250, 252, 253, 254	syl3anc 1372	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑦)
256	197	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) ∈ ℝ)
257	133	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑍‘𝑋) ∈ ℝ)
258	219	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
259	256, 257, 258	ltsubaddd 11860	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑦 ↔ (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋))))
260	255, 259	mpbid 232	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋)))
261	260	3adantl3 1168	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋)))
262	237, 136	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝐸‘𝑋) ∈ ℝ)
263	205	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
264	263	3adantl3 1168	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
265	74	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑋 ∈ ℝ)
266		iooltub 45528	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ^* ∧ 𝑋 ∈ ℝ^* ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 < 𝑋)
267	250, 252, 253, 266	syl3anc 1372	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 < 𝑋)
268	258, 265, 257, 267	ltadd1dd 11875	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝑋 + (𝑍‘𝑋)))
269	135	eqcomd 2742	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 + (𝑍‘𝑋)) = (𝐸‘𝑋))
270	269	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑋 + (𝑍‘𝑋)) = (𝐸‘𝑋))
271	268, 270	breqtrd 5168	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝐸‘𝑋))
272	271	3adantl3 1168	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝐸‘𝑋))
273		iocleub 45521	. . . . . . . . . . . . . . 15 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ≤ (𝑄‘(𝑖 + 1)))
274	202, 207, 208, 273	syl3anc 1372	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ≤ (𝑄‘(𝑖 + 1)))
275	274	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘(𝑖 + 1)))
276	246, 262, 264, 272, 275	ltletrd 11422	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝑄‘(𝑖 + 1)))
277	241, 242, 246, 261, 276	eliood 45516	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
278	240, 277	sseldd 3983	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ 𝐷)
279	237, 128	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝐵 − 𝑋) / 𝑇) ∈ ℝ)
280	279	flcld 13839	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
281	280	znegcld 12726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
282		negex 11507	. . . . . . . . . . 11 ⊢ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ V
283		eleq1 2828	. . . . . . . . . . . . 13 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ))
284	283	3anbi3d 1443	. . . . . . . . . . . 12 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)))
285		oveq1 7439	. . . . . . . . . . . . . 14 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑘 · 𝑇) = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
286	285	oveq2d 7448	. . . . . . . . . . . . 13 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
287	286	eleq1d 2825	. . . . . . . . . . . 12 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
288	284, 287	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)))
289		ovex 7465	. . . . . . . . . . . 12 ⊢ (𝑦 + (𝑍‘𝑋)) ∈ V
290		eleq1 2828	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → (𝑥 ∈ 𝐷 ↔ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷))
291	290	3anbi2d 1442	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ)))
292		oveq1 7439	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)))
293	292	eleq1d 2825	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷))
294	291, 293	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → (((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)))
295		fourierdlem41.dper	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)
296	289, 294, 295	vtocl 3557	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)
297	282, 288, 296	vtocl 3557	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
298	237, 278, 281, 297	syl3anc 1372	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
299	236, 298	eqeltrd 2840	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ 𝐷)
300	299	ralrimiva 3145	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑦 ∈ 𝐷)
301		dfss3 3971	. . . . . . 7 ⊢ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷 ↔ ∀𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑦 ∈ 𝐷)
302	300, 301	sylibr 234	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷)
303		breq1 5145	. . . . . . . 8 ⊢ (𝑦 = ((𝑄‘𝑖) − (𝑍‘𝑋)) → (𝑦 < 𝑋 ↔ ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋))
304		oveq1 7439	. . . . . . . . 9 ⊢ (𝑦 = ((𝑄‘𝑖) − (𝑍‘𝑋)) → (𝑦(,)𝑋) = (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋))
305	304	sseq1d 4014	. . . . . . . 8 ⊢ (𝑦 = ((𝑄‘𝑖) − (𝑍‘𝑋)) → ((𝑦(,)𝑋) ⊆ 𝐷 ↔ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷))
306	303, 305	anbi12d 632	. . . . . . 7 ⊢ (𝑦 = ((𝑄‘𝑖) − (𝑍‘𝑋)) → ((𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ↔ (((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋 ∧ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷)))
307	306	rspcev 3621	. . . . . 6 ⊢ ((((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ ∧ (((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋 ∧ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
308	200, 218, 302, 307	syl12anc 836	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
309	308	3exp 1119	. . . 4 ⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))))
310	309	rexlimdv 3152	. . 3 ⊢ (𝜑 → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷)))
311	193, 310	mpd 15	. 2 ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
312		0zd 12627	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℤ)
313	3	nnzd 12642	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
314		1zzd 12650	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℤ)
315		0le1 11787	. . . . . . . . 9 ⊢ 0 ≤ 1
316	315	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ 1)
317	3	nnge1d 12315	. . . . . . . 8 ⊢ (𝜑 → 1 ≤ 𝑀)
318	312, 313, 314, 316, 317	elfzd 13556	. . . . . . 7 ⊢ (𝜑 → 1 ∈ (0...𝑀))
319	101, 318	ffvelcdmd 7104	. . . . . 6 ⊢ (𝜑 → (𝑄‘1) ∈ ℝ)
320	133, 52	resubcld 11692	. . . . . 6 ⊢ (𝜑 → ((𝑍‘𝑋) − 𝑇) ∈ ℝ)
321	319, 320	resubcld 11692	. . . . 5 ⊢ (𝜑 → ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
322	321	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
323	38	recnd 11290	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℂ)
324	323, 222	pncand 11622	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
325	324	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
326	43	oveq2i 7443	. . . . . . . . . . 11 ⊢ (𝐴 + 𝑇) = (𝐴 + (𝐵 − 𝐴))
327	326	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝐴 + 𝑇) = (𝐴 + (𝐵 − 𝐴)))
328	40	recnd 11290	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℂ)
329	323, 328	pncan3d 11624	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
330	329	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
331		id 22	. . . . . . . . . . . 12 ⊢ ((𝐸‘𝑋) = 𝐵 → (𝐸‘𝑋) = 𝐵)
332	331	eqcomd 2742	. . . . . . . . . . 11 ⊢ ((𝐸‘𝑋) = 𝐵 → 𝐵 = (𝐸‘𝑋))
333	332	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → 𝐵 = (𝐸‘𝑋))
334	327, 330, 333	3eqtrrd 2781	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝐸‘𝑋) = (𝐴 + 𝑇))
335	334	oveq1d 7447	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝐸‘𝑋) − 𝑇) = ((𝐴 + 𝑇) − 𝑇))
336	33	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑄‘0) = 𝐴)
337	325, 335, 336	3eqtr4rd 2787	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑄‘0) = ((𝐸‘𝑋) − 𝑇))
338	337	oveq1d 7447	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑄‘0) − ((𝑍‘𝑋) − 𝑇)) = (((𝐸‘𝑋) − 𝑇) − ((𝑍‘𝑋) − 𝑇)))
339	136	recnd 11290	. . . . . . . 8 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℂ)
340	339, 214, 222	nnncan2d 11656	. . . . . . 7 ⊢ (𝜑 → (((𝐸‘𝑋) − 𝑇) − ((𝑍‘𝑋) − 𝑇)) = ((𝐸‘𝑋) − (𝑍‘𝑋)))
341	340	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (((𝐸‘𝑋) − 𝑇) − ((𝑍‘𝑋) − 𝑇)) = ((𝐸‘𝑋) − (𝑍‘𝑋)))
342	216	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝐸‘𝑋) − (𝑍‘𝑋)) = 𝑋)
343	338, 341, 342	3eqtrrd 2781	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → 𝑋 = ((𝑄‘0) − ((𝑍‘𝑋) − 𝑇)))
344	33, 38	eqeltrd 2840	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
345	3	nngt0d 12316	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝑀)
346		fzolb 13706	. . . . . . . . . 10 ⊢ (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
347	312, 313, 345, 346	syl3anbrc 1343	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0..^𝑀))
348		0re 11264	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
349		eleq1 2828	. . . . . . . . . . . . 13 ⊢ (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀)))
350	349	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑖 = 0 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀))))
351		fveq2 6905	. . . . . . . . . . . . 13 ⊢ (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0))
352		oveq1 7439	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
353	352	fveq2d 6909	. . . . . . . . . . . . 13 ⊢ (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1)))
354	351, 353	breq12d 5155	. . . . . . . . . . . 12 ⊢ (𝑖 = 0 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1))))
355	350, 354	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑖 = 0 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))))
356	355, 149	vtoclg 3553	. . . . . . . . . 10 ⊢ (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))
357	348, 356	ax-mp 5	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))
358	347, 357	mpdan 687	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1)))
359		0p1e1 12389	. . . . . . . . . 10 ⊢ (0 + 1) = 1
360	359	fveq2i 6908	. . . . . . . . 9 ⊢ (𝑄‘(0 + 1)) = (𝑄‘1)
361	360	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1))
362	358, 361	breqtrd 5168	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) < (𝑄‘1))
363	344, 319, 320, 362	ltsub1dd 11876	. . . . . 6 ⊢ (𝜑 → ((𝑄‘0) − ((𝑍‘𝑋) − 𝑇)) < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
364	363	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑄‘0) − ((𝑍‘𝑋) − 𝑇)) < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
365	343, 364	eqbrtrd 5164	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → 𝑋 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
366		elioore 13418	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) → 𝑦 ∈ ℝ)
367	132	eqcomd 2742	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = (𝑍‘𝑋))
368	367	negeqd 11503	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = -(𝑍‘𝑋))
369	223, 368	eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = -(𝑍‘𝑋))
370	222	mullidd 11280	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 · 𝑇) = 𝑇)
371	369, 370	oveq12d 7450	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) + (1 · 𝑇)) = (-(𝑍‘𝑋) + 𝑇))
372	221	negcld 11608	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℂ)
373		1cnd 11257	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℂ)
374	372, 373, 222	adddird 11287	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇) = ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) + (1 · 𝑇)))
375	214, 222	negsubdid 11636	. . . . . . . . . . . . 13 ⊢ (𝜑 → -((𝑍‘𝑋) − 𝑇) = (-(𝑍‘𝑋) + 𝑇))
376	371, 374, 375	3eqtr4d 2786	. . . . . . . . . . . 12 ⊢ (𝜑 → ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇) = -((𝑍‘𝑋) − 𝑇))
377	376	oveq2d 7448	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + -((𝑍‘𝑋) − 𝑇)))
378	377	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + -((𝑍‘𝑋) − 𝑇)))
379	320	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑍‘𝑋) − 𝑇) ∈ ℝ)
380	226, 379	readdcld 11291	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
381	380	recnd 11290	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ℂ)
382	379	recnd 11290	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑍‘𝑋) − 𝑇) ∈ ℂ)
383	381, 382	negsubd 11627	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + -((𝑍‘𝑋) − 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) − ((𝑍‘𝑋) − 𝑇)))
384	232, 382	pncand 11622	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) − ((𝑍‘𝑋) − 𝑇)) = 𝑦)
385	378, 383, 384	3eqtrrd 2781	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)))
386	366, 385	sylan2 593	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)))
387	386	adantlr 715	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)))
388		simpll 766	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝜑)
389	361	eqcomd 2742	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘1) = (𝑄‘(0 + 1)))
390	389	oveq2d 7448	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄‘0)(,)(𝑄‘1)) = ((𝑄‘0)(,)(𝑄‘(0 + 1))))
391	351, 353	oveq12d 7450	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 0 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘0)(,)(𝑄‘(0 + 1))))
392	391	sseq1d 4014	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 0 → (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷 ↔ ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷))
393	350, 392	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 0 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)))
394	393, 238	vtoclg 3553	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷))
395	348, 394	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)
396	347, 395	mpdan 687	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)
397	390, 396	eqsstrd 4017	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑄‘0)(,)(𝑄‘1)) ⊆ 𝐷)
398	397	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑄‘0)(,)(𝑄‘1)) ⊆ 𝐷)
399	33, 39	eqeltrd 2840	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ^*)
400	399	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘0) ∈ ℝ^*)
401	319	rexrd 11312	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄‘1) ∈ ℝ^*)
402	401	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘1) ∈ ℝ^*)
403	366, 380	sylan2 593	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
404	403	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
405	339, 213, 214	subaddd 11639	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐸‘𝑋) − 𝑋) = (𝑍‘𝑋) ↔ (𝑋 + (𝑍‘𝑋)) = (𝐸‘𝑋)))
406	269, 405	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸‘𝑋) − 𝑋) = (𝑍‘𝑋))
407		oveq1 7439	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸‘𝑋) = 𝐵 → ((𝐸‘𝑋) − 𝑋) = (𝐵 − 𝑋))
408	406, 407	sylan9req 2797	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑍‘𝑋) = (𝐵 − 𝑋))
409	408	oveq1d 7447	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑍‘𝑋) − 𝑇) = ((𝐵 − 𝑋) − 𝑇))
410	409	oveq2d 7448	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑋 + ((𝑍‘𝑋) − 𝑇)) = (𝑋 + ((𝐵 − 𝑋) − 𝑇)))
411	127	recnd 11290	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℂ)
412	213, 411, 222	addsubassd 11641	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 + (𝐵 − 𝑋)) − 𝑇) = (𝑋 + ((𝐵 − 𝑋) − 𝑇)))
413	412	eqcomd 2742	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 + ((𝐵 − 𝑋) − 𝑇)) = ((𝑋 + (𝐵 − 𝑋)) − 𝑇))
414	413	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑋 + ((𝐵 − 𝑋) − 𝑇)) = ((𝑋 + (𝐵 − 𝑋)) − 𝑇))
415	328, 222, 323	subsub23d 45304	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 − 𝑇) = 𝐴 ↔ (𝐵 − 𝐴) = 𝑇))
416	58, 415	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 − 𝑇) = 𝐴)
417	213, 328	pncan3d 11624	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 + (𝐵 − 𝑋)) = 𝐵)
418	417	oveq1d 7447	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 + (𝐵 − 𝑋)) − 𝑇) = (𝐵 − 𝑇))
419	416, 418, 33	3eqtr4d 2786	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑋 + (𝐵 − 𝑋)) − 𝑇) = (𝑄‘0))
420	419	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑋 + (𝐵 − 𝑋)) − 𝑇) = (𝑄‘0))
421	410, 414, 420	3eqtrrd 2781	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑄‘0) = (𝑋 + ((𝑍‘𝑋) − 𝑇)))
422	421	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘0) = (𝑋 + ((𝑍‘𝑋) − 𝑇)))
423	74	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑋 ∈ ℝ)
424	366	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 ∈ ℝ)
425	320	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑍‘𝑋) − 𝑇) ∈ ℝ)
426	251	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑋 ∈ ℝ^*)
427	321	rexrd 11312	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ^*)
428	427	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ^*)
429		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))))
430		ioogtlb 45513	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ ℝ^* ∧ ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ^* ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑋 < 𝑦)
431	426, 428, 429, 430	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑋 < 𝑦)
432	423, 424, 425, 431	ltadd1dd 11875	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑋 + ((𝑍‘𝑋) − 𝑇)) < (𝑦 + ((𝑍‘𝑋) − 𝑇)))
433	432	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑋 + ((𝑍‘𝑋) − 𝑇)) < (𝑦 + ((𝑍‘𝑋) − 𝑇)))
434	422, 433	eqbrtrd 5164	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘0) < (𝑦 + ((𝑍‘𝑋) − 𝑇)))
435		iooltub 45528	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ ℝ^* ∧ ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ^* ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
436	426, 428, 429, 435	syl3anc 1372	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
437	319	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘1) ∈ ℝ)
438	424, 425, 437	ltaddsubd 11864	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) < (𝑄‘1) ↔ 𝑦 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))))
439	436, 438	mpbird 257	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) < (𝑄‘1))
440	439	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) < (𝑄‘1))
441	400, 402, 404, 434, 440	eliood 45516	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ((𝑄‘0)(,)(𝑄‘1)))
442	398, 441	sseldd 3983	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷)
443	129	znegcld 12726	. . . . . . . . . 10 ⊢ (𝜑 → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
444	443	peano2zd 12727	. . . . . . . . 9 ⊢ (𝜑 → (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ)
445	444	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ)
446		ovex 7465	. . . . . . . . 9 ⊢ (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ V
447		eleq1 2828	. . . . . . . . . . 11 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → (𝑘 ∈ ℤ ↔ (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ))
448	447	3anbi3d 1443	. . . . . . . . . 10 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ)))
449		oveq1 7439	. . . . . . . . . . . 12 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → (𝑘 · 𝑇) = ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇))
450	449	oveq2d 7448	. . . . . . . . . . 11 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)))
451	450	eleq1d 2825	. . . . . . . . . 10 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → (((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷))
452	448, 451	imbi12d 344	. . . . . . . . 9 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → (((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)))
453		ovex 7465	. . . . . . . . . 10 ⊢ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ V
454		eleq1 2828	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → (𝑥 ∈ 𝐷 ↔ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷))
455	454	3anbi2d 1442	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ)))
456		oveq1 7439	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)))
457	456	eleq1d 2825	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷))
458	455, 457	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → (((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷)))
459	453, 458, 295	vtocl 3557	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷)
460	446, 452, 459	vtocl 3557	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)
461	388, 442, 445, 460	syl3anc 1372	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)
462	387, 461	eqeltrd 2840	. . . . . 6 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 ∈ 𝐷)
463	462	ralrimiva 3145	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ∀𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))𝑦 ∈ 𝐷)
464		dfss3 3971	. . . . 5 ⊢ ((𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷 ↔ ∀𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))𝑦 ∈ 𝐷)
465	463, 464	sylibr 234	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷)
466		breq2 5146	. . . . . 6 ⊢ (𝑦 = ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) → (𝑋 < 𝑦 ↔ 𝑋 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))))
467		oveq2 7440	. . . . . . 7 ⊢ (𝑦 = ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) → (𝑋(,)𝑦) = (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))))
468	467	sseq1d 4014	. . . . . 6 ⊢ (𝑦 = ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) → ((𝑋(,)𝑦) ⊆ 𝐷 ↔ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷))
469	466, 468	anbi12d 632	. . . . 5 ⊢ (𝑦 = ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) → ((𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷) ↔ (𝑋 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∧ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷)))
470	469	rspcev 3621	. . . 4 ⊢ ((((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ ∧ (𝑋 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∧ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
471	322, 365, 465, 470	syl12anc 836	. . 3 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
472	15	adantlr 715	. . . . . 6 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋))
473		simp2 1137	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ (0...𝑀))
474	25	3ad2ant2 1134	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ ℝ)
475	94	3ad2ant2 1134	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑀 ∈ ℝ)
476	96	3ad2ant2 1134	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ≤ 𝑀)
477		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑄‘𝑗) = (𝐸‘𝑋) → (𝑄‘𝑗) = (𝐸‘𝑋))
478	477	eqcomd 2742	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄‘𝑗) = (𝐸‘𝑋) → (𝐸‘𝑋) = (𝑄‘𝑗))
479	478	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑄‘𝑗) = (𝐸‘𝑋) ∧ 𝑀 = 𝑗) → (𝐸‘𝑋) = (𝑄‘𝑗))
480	479	3ad2antl3 1187	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → (𝐸‘𝑋) = (𝑄‘𝑗))
481		fveq2 6905	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 = 𝑗 → (𝑄‘𝑀) = (𝑄‘𝑗))
482	481	eqcomd 2742	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 = 𝑗 → (𝑄‘𝑗) = (𝑄‘𝑀))
483	482	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → (𝑄‘𝑗) = (𝑄‘𝑀))
484	177	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑀 = 𝑗) → (𝑄‘𝑀) = 𝐵)
485	484	3ad2antl1 1185	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → (𝑄‘𝑀) = 𝐵)
486	480, 483, 485	3eqtrd 2780	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → (𝐸‘𝑋) = 𝐵)
487		neneq 2945	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸‘𝑋) ≠ 𝐵 → ¬ (𝐸‘𝑋) = 𝐵)
488	487	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑀 = 𝑗) → ¬ (𝐸‘𝑋) = 𝐵)
489	488	3ad2antl1 1185	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → ¬ (𝐸‘𝑋) = 𝐵)
490	486, 489	pm2.65da 816	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → ¬ 𝑀 = 𝑗)
491	490	neqned 2946	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑀 ≠ 𝑗)
492	474, 475, 476, 491	leneltd 11416	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 < 𝑀)
493		elfzfzo 45293	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0..^𝑀) ↔ (𝑗 ∈ (0...𝑀) ∧ 𝑗 < 𝑀))
494	473, 492, 493	sylanbrc 583	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ (0..^𝑀))
495	114	adantlr 715	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ^*)
496	495	3adant3 1132	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ∈ ℝ^*)
497		simp1l 1197	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝜑)
498	101	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
499		fzofzp1 13804	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0..^𝑀) → (𝑗 + 1) ∈ (0...𝑀))
500	499	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑗 + 1) ∈ (0...𝑀))
501	498, 500	ffvelcdmd 7104	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ)
502	501	rexrd 11312	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ^*)
503	497, 494, 502	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 + 1)) ∈ ℝ^*)
504	138	3adant1r 1177	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ℝ^*)
505	37, 157	eqbrtrd 5164	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ≤ (𝐸‘𝑋))
506	505	adantlr 715	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ≤ (𝐸‘𝑋))
507	506	3adant2 1131	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ≤ (𝐸‘𝑋))
508	478	3ad2ant3 1135	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) = (𝑄‘𝑗))
509		eleq1 2828	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑖 ∈ (0..^𝑀) ↔ 𝑗 ∈ (0..^𝑀)))
510	509	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑗 ∈ (0..^𝑀))))
511		fveq2 6905	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑄‘𝑖) = (𝑄‘𝑗))
512		oveq1 7439	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
513	512	fveq2d 6909	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑗 + 1)))
514	511, 513	breq12d 5155	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑗 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘𝑗) < (𝑄‘(𝑗 + 1))))
515	510, 514	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))))
516	515, 149	chvarvv 1997	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))
517	497, 494, 516	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))
518	508, 517	eqbrtrd 5164	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) < (𝑄‘(𝑗 + 1)))
519	496, 503, 504, 507, 518	elicod 13438	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ((𝑄‘𝑗)[,)(𝑄‘(𝑗 + 1))))
520	511, 513	oveq12d 7450	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) = ((𝑄‘𝑗)[,)(𝑄‘(𝑗 + 1))))
521	520	eleq2d 2826	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) ↔ (𝐸‘𝑋) ∈ ((𝑄‘𝑗)[,)(𝑄‘(𝑗 + 1)))))
522	521	rspcev 3621	. . . . . . . . . 10 ⊢ ((𝑗 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑗)[,)(𝑄‘(𝑗 + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
523	494, 519, 522	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
524	523	3exp 1119	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → (𝑗 ∈ (0...𝑀) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))))
525	524	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (𝑗 ∈ (0...𝑀) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))))
526	525	rexlimdv 3152	. . . . . 6 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))))
527	472, 526	mpd 15	. . . . 5 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
528		ioossico 13479	. . . . . . . . . . 11 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))
529		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
530	528, 529	sselid 3980	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
531	530	ex 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))))
532	531	adantlr 715	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))))
533	532	reximdva 3167	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))))
534	187, 533	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
535	534	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
536	527, 535	pm2.61dan 812	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
537	205, 247	resubcld 11692	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ)
538	537	3adant3 1132	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ)
539	216	eqcomd 2742	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 = ((𝐸‘𝑋) − (𝑍‘𝑋)))
540	539	3ad2ant1 1133	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → 𝑋 = ((𝐸‘𝑋) − (𝑍‘𝑋)))
541	136	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ℝ)
542	205	3adant3 1132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
543	133	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑍‘𝑋) ∈ ℝ)
544	197	rexrd 11312	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ^*)
545	544	3adant3 1132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ^*)
546	206	3adant3 1132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
547		simp3 1138	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
548		icoltub 45526	. . . . . . . . . . 11 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) < (𝑄‘(𝑖 + 1)))
549	545, 546, 547, 548	syl3anc 1372	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) < (𝑄‘(𝑖 + 1)))
550	541, 542, 543, 549	ltsub1dd 11876	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝐸‘𝑋) − (𝑍‘𝑋)) < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))
551	540, 550	eqbrtrd 5164	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → 𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))
552		elioore 13418	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) → 𝑦 ∈ ℝ)
553	552, 234	sylan2 593	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
554	553	3ad2antl1 1185	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
555		simpl1 1191	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝜑)
556	238	3adant3 1132	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
557	556	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
558	545	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘𝑖) ∈ ℝ^*)
559	546	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
560	552	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 ∈ ℝ)
561	133	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑍‘𝑋) ∈ ℝ)
562	560, 561	readdcld 11291	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
563	562	3ad2antl1 1185	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
564	197	3adant3 1132	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
565	564	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘𝑖) ∈ ℝ)
566	555, 136	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝐸‘𝑋) ∈ ℝ)
567		icogelb 13439	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ≤ (𝐸‘𝑋))
568	545, 546, 547, 567	syl3anc 1372	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ≤ (𝐸‘𝑋))
569	568	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘𝑖) ≤ (𝐸‘𝑋))
570	135	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝐸‘𝑋) = (𝑋 + (𝑍‘𝑋)))
571	74	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑋 ∈ ℝ)
572	552	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 ∈ ℝ)
573	133	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑍‘𝑋) ∈ ℝ)
574	251	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑋 ∈ ℝ^*)
575	537	rexrd 11312	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ^*)
576	575	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ^*)
577		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))))
578		ioogtlb 45513	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋 ∈ ℝ^* ∧ ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ^* ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑋 < 𝑦)
579	574, 576, 577, 578	syl3anc 1372	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑋 < 𝑦)
580	571, 572, 573, 579	ltadd1dd 11875	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑋 + (𝑍‘𝑋)) < (𝑦 + (𝑍‘𝑋)))
581	570, 580	eqbrtrd 5164	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝐸‘𝑋) < (𝑦 + (𝑍‘𝑋)))
582	581	3adantl3 1168	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝐸‘𝑋) < (𝑦 + (𝑍‘𝑋)))
583	565, 566, 563, 569, 582	lelttrd 11420	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋)))
584	537	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ)
585		iooltub 45528	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋 ∈ ℝ^* ∧ ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ^* ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))
586	574, 576, 577, 585	syl3anc 1372	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))
587	572, 584, 573, 586	ltadd1dd 11875	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) < (((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) + (𝑍‘𝑋)))
588	205	recnd 11290	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
589	214	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑍‘𝑋) ∈ ℂ)
590	588, 589	npcand 11625	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) + (𝑍‘𝑋)) = (𝑄‘(𝑖 + 1)))
591	590	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) + (𝑍‘𝑋)) = (𝑄‘(𝑖 + 1)))
592	587, 591	breqtrd 5168	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) < (𝑄‘(𝑖 + 1)))
593	592	3adantl3 1168	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) < (𝑄‘(𝑖 + 1)))
594	558, 559, 563, 583, 593	eliood 45516	. . . . . . . . . . . . 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 2840	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 ∈ 𝐷)
599	598	ralrimiva 3145	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))𝑦 ∈ 𝐷)
600		dfss3 3971	. . . . . . . . 9 ⊢ ((𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷 ↔ ∀𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))𝑦 ∈ 𝐷)
601	599, 600	sylibr 234	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷)
602		breq2 5146	. . . . . . . . . 10 ⊢ (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) → (𝑋 < 𝑦 ↔ 𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))))
603		oveq2 7440	. . . . . . . . . . 11 ⊢ (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) → (𝑋(,)𝑦) = (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))))
604	603	sseq1d 4014	. . . . . . . . . 10 ⊢ (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) → ((𝑋(,)𝑦) ⊆ 𝐷 ↔ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷))
605	602, 604	anbi12d 632	. . . . . . . . 9 ⊢ (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) → ((𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷) ↔ (𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∧ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷)))
606	605	rspcev 3621	. . . . . . . 8 ⊢ ((((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ ∧ (𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∧ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
607	538, 551, 601, 606	syl12anc 836	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
608	607	3exp 1119	. . . . . 6 ⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))))
609	608	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → (𝑖 ∈ (0..^𝑀) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))))
610	609	rexlimdv 3152	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))
611	536, 610	mpd 15	. . 3 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
612	471, 611	pm2.61dane 3028	. 2 ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
613	311, 612	jca 511	1 ⊢ (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ∧ ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ≠ wne 2939 ∀wral 3060 ∃wrex 3069 {crab 3435 ⊆ wss 3950 class class class wbr 5142 ↦ cmpt 5224 ran crn 5685 Fn wfn 6555 ⟶wf 6556 ‘cfv 6560 (class class class)co 7432 ↑_m cmap 8867 supcsup 9481 ℂcc 11154 ℝcr 11155 0cc0 11156 1c1 11157 + caddc 11159 · cmul 11161 ℝ^*cxr 11295 < clt 11296 ≤ cle 11297 − cmin 11493 -cneg 11494 / cdiv 11921 ℕcn 12267 ℤcz 12615 ℤ_≥cuz 12879 (,)cioo 13388 (,]cioc 13389 [,)cico 13390 [,]cicc 13391 ...cfz 13548 ..^cfzo 13695 ⌊cfl 13831

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-sep 5295 ax-nul 5305 ax-pow 5364 ax-pr 5431 ax-un 7756 ax-cnex 11212 ax-resscn 11213 ax-1cn 11214 ax-icn 11215 ax-addcl 11216 ax-addrcl 11217 ax-mulcl 11218 ax-mulrcl 11219 ax-mulcom 11220 ax-addass 11221 ax-mulass 11222 ax-distr 11223 ax-i2m1 11224 ax-1ne0 11225 ax-1rid 11226 ax-rnegex 11227 ax-rrecex 11228 ax-cnre 11229 ax-pre-lttri 11230 ax-pre-lttrn 11231 ax-pre-ltadd 11232 ax-pre-mulgt0 11233 ax-pre-sup 11234

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3379 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-pss 3970 df-nul 4333 df-if 4525 df-pw 4601 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4907 df-iun 4992 df-br 5143 df-opab 5205 df-mpt 5225 df-tr 5259 df-id 5577 df-eprel 5583 df-po 5591 df-so 5592 df-fr 5636 df-we 5638 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-pred 6320 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6513 df-fun 6562 df-fn 6563 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 df-fv 6568 df-riota 7389 df-ov 7435 df-oprab 7436 df-mpo 7437 df-om 7889 df-1st 8015 df-2nd 8016 df-frecs 8307 df-wrecs 8338 df-recs 8412 df-rdg 8451 df-1o 8507 df-er 8746 df-map 8869 df-en 8987 df-dom 8988 df-sdom 8989 df-fin 8990 df-sup 9483 df-inf 9484 df-pnf 11298 df-mnf 11299 df-xr 11300 df-ltxr 11301 df-le 11302 df-sub 11495 df-neg 11496 df-div 11922 df-nn 12268 df-n0 12529 df-z 12616 df-uz 12880 df-rp 13036 df-ioo 13392 df-ioc 13393 df-ico 13394 df-icc 13395 df-fz 13549 df-fzo 13696 df-fl 13833

This theorem is referenced by: fourierdlem113 46239

W3C validator