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 43696

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 485	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (𝐸‘𝑋) ∈ ran 𝑄)
2		fourierdlem41.q	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
3		fourierdlem41.m	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℕ)
4		fourierdlem41.p	. . . . . . . . . . . . 13 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
5	4	fourierdlem2 43657	. . . . . . . . . . . 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 495	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
9		elmapi 8646	. . . . . . . . 9 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
10		ffn 6609	. . . . . . . . 9 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
11	8, 9, 10	3syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
12	11	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → 𝑄 Fn (0...𝑀))
13		fvelrnb 6839	. . . . . . 7 ⊢ (𝑄 Fn (0...𝑀) → ((𝐸‘𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋)))
14	12, 13	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ((𝐸‘𝑋) ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋)))
15	1, 14	mpbid 231	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋))
16		0zd 12340	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 ∈ ℤ)
17		elfzelz 13265	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
18	17	3ad2ant2 1133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ ℤ)
19		1zzd 12360	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 1 ∈ ℤ)
20	18, 19	zsubcld 12440	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ ℤ)
21		simpll 764	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → 𝜑)
22		elfzle1 13268	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
23	22	anim1i 615	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → (0 ≤ 𝑗 ∧ ¬ 0 < 𝑗))
24		0red 10987	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 0 ∈ ℝ)
25	17	zred 12435	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
26	25	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 𝑗 ∈ ℝ)
27	24, 26	eqleltd 11128	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → (0 = 𝑗 ↔ (0 ≤ 𝑗 ∧ ¬ 0 < 𝑗)))
28	23, 27	mpbird 256	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 0 = 𝑗)
29	28	eqcomd 2745	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ ¬ 0 < 𝑗) → 𝑗 = 0)
30	29	adantll 711	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → 𝑗 = 0)
31		fveq2 6783	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 0 → (𝑄‘𝑗) = (𝑄‘0))
32	7	simprld 769	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
33	32	simpld 495	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
34	31, 33	sylan9eqr 2801	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 = 0) → (𝑄‘𝑗) = 𝐴)
35	21, 30, 34	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 0 < 𝑗) → (𝑄‘𝑗) = 𝐴)
36	35	3adantl3 1167	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄‘𝑗) = 𝐴)
37		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) = (𝐸‘𝑋))
38		fourierdlem41.a	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ ℝ)
39	38	rexrd 11034	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
40		fourierdlem41.b	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ ℝ)
41	40	rexrd 11034	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
42		fourierdlem41.altb	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐴 < 𝐵)
43		fourierdlem41.t	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑇 = (𝐵 − 𝐴)
44		eqid 2739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
45	38, 40, 42, 43, 44	fourierdlem4 43659	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))):ℝ⟶(𝐴(,]𝐵))
46		fourierdlem41.e	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥)))
47	46	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥))))
48		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
49	40	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
50	49, 48	resubcld 11412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) ∈ ℝ)
51	40, 38	resubcld 11412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
52	43, 51	eqeltrid 2844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → 𝑇 ∈ ℝ)
53	52	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
54		0red 10987	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 0 ∈ ℝ)
55	38, 40	posdifd 11571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
56	42, 55	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
57	43	eqcomi 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝐵 − 𝐴) = 𝑇
58	57	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (𝐵 − 𝐴) = 𝑇)
59	56, 58	breqtrd 5101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 0 < 𝑇)
60	54, 59	gtned 11119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → 𝑇 ≠ 0)
61	60	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ≠ 0)
62	50, 53, 61	redivcld 11812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) ∈ ℝ)
63	62	flcld 13527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)
64	63	zred 12435	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℝ)
65	64, 53	remulcld 11014	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
66		fourierdlem41.z	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
67	66	fvmpt2 6895	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℝ ∧ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ ℝ) → (𝑍‘𝑥) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
68	48, 65, 67	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑍‘𝑥) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
69	68	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (𝑍‘𝑥)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
70	69	mpteq2dva 5175	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
71	47, 70	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
72	71	feq1d 6594	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐸:ℝ⟶(𝐴(,]𝐵) ↔ (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))):ℝ⟶(𝐴(,]𝐵)))
73	45, 72	mpbird 256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
74		fourierdlem41.x	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑋 ∈ ℝ)
75	73, 74	ffvelrnd 6971	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐸‘𝑋) ∈ (𝐴(,]𝐵))
76		iocgtlb 43047	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝐸‘𝑋) ∈ (𝐴(,]𝐵)) → 𝐴 < (𝐸‘𝑋))
77	39, 41, 75, 76	syl3anc 1370	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 < (𝐸‘𝑋))
78	38, 77	gtned 11119	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸‘𝑋) ≠ 𝐴)
79	78	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≠ 𝐴)
80	37, 79	eqnetrd 3012	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ≠ 𝐴)
81	80	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄‘𝑗) ≠ 𝐴)
82	81	3adantl2 1166	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ ¬ 0 < 𝑗) → (𝑄‘𝑗) ≠ 𝐴)
83	82	neneqd 2949	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ ¬ 0 < 𝑗) → ¬ (𝑄‘𝑗) = 𝐴)
84	36, 83	condan 815	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 < 𝑗)
85		zltlem1 12382	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (0 < 𝑗 ↔ 0 ≤ (𝑗 − 1)))
86	16, 18, 85	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (0 < 𝑗 ↔ 0 ≤ (𝑗 − 1)))
87	84, 86	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 0 ≤ (𝑗 − 1))
88		eluz2 12597	. . . . . . . . . . 11 ⊢ ((𝑗 − 1) ∈ (ℤ_≥‘0) ↔ (0 ∈ ℤ ∧ (𝑗 − 1) ∈ ℤ ∧ 0 ≤ (𝑗 − 1)))
89	16, 20, 87, 88	syl3anbrc 1342	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ (ℤ_≥‘0))
90		elfzel2 13263	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
91	90	3ad2ant2 1133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑀 ∈ ℤ)
92		1red 10985	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → 1 ∈ ℝ)
93	25, 92	resubcld 11412	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
94	90	zred 12435	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
95	25	ltm1d 11916	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑗)
96		elfzle2 13269	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀)
97	93, 25, 94, 95, 96	ltletrd 11144	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
98	97	3ad2ant2 1133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) < 𝑀)
99		elfzo2 13399	. . . . . . . . . 10 ⊢ ((𝑗 − 1) ∈ (0..^𝑀) ↔ ((𝑗 − 1) ∈ (ℤ_≥‘0) ∧ 𝑀 ∈ ℤ ∧ (𝑗 − 1) < 𝑀))
100	89, 91, 98, 99	syl3anbrc 1342	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ (0..^𝑀))
101	8, 9	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
102	101	3ad2ant1 1132	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑄:(0...𝑀)⟶ℝ)
103	93, 94, 97	ltled 11132	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ≤ 𝑀)
104	103	3ad2ant2 1133	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ≤ 𝑀)
105	16, 91, 20, 87, 104	elfzd 13256	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑗 − 1) ∈ (0...𝑀))
106	102, 105	ffvelrnd 6971	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ)
107	106	rexrd 11034	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) ∈ ℝ^*)
108	25	recnd 11012	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
109		1cnd 10979	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 1 ∈ ℂ)
110	108, 109	npcand 11345	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → ((𝑗 − 1) + 1) = 𝑗)
111	110	fveq2d 6787	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄‘𝑗))
112	111	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄‘𝑗))
113	101	ffvelrnda 6970	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ)
114	113	rexrd 11034	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ^*)
115	112, 114	eqeltrd 2840	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘((𝑗 − 1) + 1)) ∈ ℝ^*)
116	115	3adant3 1131	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘((𝑗 − 1) + 1)) ∈ ℝ^*)
117		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋)
118		fveq2 6783	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → (𝑍‘𝑥) = (𝑍‘𝑋))
119	117, 118	oveq12d 7302	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → (𝑥 + (𝑍‘𝑥)) = (𝑋 + (𝑍‘𝑋)))
120	119	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥 + (𝑍‘𝑥)) = (𝑋 + (𝑍‘𝑋)))
121	66	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
122		oveq2 7292	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑋 → (𝐵 − 𝑥) = (𝐵 − 𝑋))
123	122	oveq1d 7299	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑋 → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − 𝑋) / 𝑇))
124	123	fveq2d 6787	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑋 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑋) / 𝑇)))
125	124	oveq1d 7299	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑋 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
126	125	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 = 𝑋) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
127	40, 74	resubcld 11412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ)
128	127, 52, 60	redivcld 11812	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐵 − 𝑋) / 𝑇) ∈ ℝ)
129	128	flcld 13527	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
130	129	zred 12435	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℝ)
131	130, 52	remulcld 11014	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
132	121, 126, 74, 131	fvmptd 6891	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑍‘𝑋) = ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
133	132, 131	eqeltrd 2840	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍‘𝑋) ∈ ℝ)
134	74, 133	readdcld 11013	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 + (𝑍‘𝑋)) ∈ ℝ)
135	47, 120, 74, 134	fvmptd 6891	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸‘𝑋) = (𝑋 + (𝑍‘𝑋)))
136	135, 134	eqeltrd 2840	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℝ)
137	136	rexrd 11034	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℝ^*)
138	137	3ad2ant1 1132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ℝ^*)
139		simp1 1135	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝜑)
140		ovex 7317	. . . . . . . . . . . . . 14 ⊢ (𝑗 − 1) ∈ V
141		eleq1 2827	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑗 − 1) → (𝑖 ∈ (0..^𝑀) ↔ (𝑗 − 1) ∈ (0..^𝑀)))
142	141	anbi2d 629	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑗 − 1) → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀))))
143		fveq2 6783	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑗 − 1) → (𝑄‘𝑖) = (𝑄‘(𝑗 − 1)))
144		oveq1 7291	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑗 − 1) → (𝑖 + 1) = ((𝑗 − 1) + 1))
145	144	fveq2d 6787	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑗 − 1) → (𝑄‘(𝑖 + 1)) = (𝑄‘((𝑗 − 1) + 1)))
146	143, 145	breq12d 5088	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑗 − 1) → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1))))
147	142, 146	imbi12d 345	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑗 − 1) → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))))
148	7	simprrd 771	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
149	148	r19.21bi 3135	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
150	140, 147, 149	vtocl 3499	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 − 1) ∈ (0..^𝑀)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
151	139, 100, 150	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘((𝑗 − 1) + 1)))
152	111	3ad2ant2 1133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘((𝑗 − 1) + 1)) = (𝑄‘𝑗))
153	151, 152	breqtrd 5101	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) < (𝑄‘𝑗))
154		simp3 1137	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) = (𝐸‘𝑋))
155	153, 154	breqtrd 5101	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 − 1)) < (𝐸‘𝑋))
156	136	leidd 11550	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘𝑋) ≤ (𝐸‘𝑋))
157	156	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝐸‘𝑋))
158	37	eqcomd 2745	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) = (𝑄‘𝑗))
159	157, 158	breqtrd 5101	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘𝑗))
160	159	3adant2 1130	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘𝑗))
161	110	eqcomd 2745	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 = ((𝑗 − 1) + 1))
162	161	fveq2d 6787	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (𝑄‘𝑗) = (𝑄‘((𝑗 − 1) + 1)))
163	162	3ad2ant2 1133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) = (𝑄‘((𝑗 − 1) + 1)))
164	160, 163	breqtrd 5101	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘((𝑗 − 1) + 1)))
165	107, 116, 138, 155, 164	eliocd 43052	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
166	143, 145	oveq12d 7302	. . . . . . . . . . 11 ⊢ (𝑖 = (𝑗 − 1) → ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) = ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1))))
167	166	eleq2d 2825	. . . . . . . . . 10 ⊢ (𝑖 = (𝑗 − 1) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) ↔ (𝐸‘𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))))
168	167	rspcev 3562	. . . . . . . . 9 ⊢ (((𝑗 − 1) ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘(𝑗 − 1))(,](𝑄‘((𝑗 − 1) + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
169	100, 165, 168	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
170	169	3exp 1118	. . . . . . 7 ⊢ (𝜑 → (𝑗 ∈ (0...𝑀) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))))
171	170	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (𝑗 ∈ (0...𝑀) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))))
172	171	rexlimdv 3213	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
173	15, 172	mpd 15	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
174	3	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → 𝑀 ∈ ℕ)
175	101	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ)
176		iocssicc 13178	. . . . . . . 8 ⊢ ((𝑄‘0)(,](𝑄‘𝑀)) ⊆ ((𝑄‘0)[,](𝑄‘𝑀))
177	32	simprd 496	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
178	33, 177	oveq12d 7302	. . . . . . . . 9 ⊢ (𝜑 → ((𝑄‘0)(,](𝑄‘𝑀)) = (𝐴(,]𝐵))
179	75, 178	eleqtrrd 2843	. . . . . . . 8 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ((𝑄‘0)(,](𝑄‘𝑀)))
180	176, 179	sselid 3920	. . . . . . 7 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ((𝑄‘0)[,](𝑄‘𝑀)))
181	180	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → (𝐸‘𝑋) ∈ ((𝑄‘0)[,](𝑄‘𝑀)))
182		simpr 485	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ¬ (𝐸‘𝑋) ∈ ran 𝑄)
183		fveq2 6783	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → (𝑄‘𝑘) = (𝑄‘𝑗))
184	183	breq1d 5085	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → ((𝑄‘𝑘) < (𝐸‘𝑋) ↔ (𝑄‘𝑗) < (𝐸‘𝑋)))
185	184	cbvrabv 3427	. . . . . . 7 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < (𝐸‘𝑋)} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < (𝐸‘𝑋)}
186	185	supeq1i 9215	. . . . . 6 ⊢ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < (𝐸‘𝑋)}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < (𝐸‘𝑋)}, ℝ, < )
187	174, 175, 181, 182, 186	fourierdlem25 43680	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
188		ioossioc 43037	. . . . . . . 8 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))
189	188	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
190	189	sseld 3921	. . . . . 6 ⊢ (((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
191	190	reximdva 3204	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))))
192	187, 191	mpd 15	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
193	173, 192	pm2.61dan 810	. . 3 ⊢ (𝜑 → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
194	101	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
195		elfzofz 13412	. . . . . . . . . 10 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
196	195	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
197	194, 196	ffvelrnd 6971	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
198	197	3adant3 1131	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
199	133	3ad2ant1 1132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑍‘𝑋) ∈ ℝ)
200	198, 199	resubcld 11412	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ)
201	136	3ad2ant1 1132	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ℝ)
202	198	rexrd 11034	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ^*)
203		fzofzp1 13493	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
204	203	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
205	194, 204	ffvelrnd 6971	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
206	205	rexrd 11034	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
207	206	3adant3 1131	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
208		simp3 1137	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))))
209		iocgtlb 43047	. . . . . . . . 9 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝐸‘𝑋))
210	202, 207, 208, 209	syl3anc 1370	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝐸‘𝑋))
211	198, 201, 199, 210	ltsub1dd 11596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < ((𝐸‘𝑋) − (𝑍‘𝑋)))
212	135	oveq1d 7299	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸‘𝑋) − (𝑍‘𝑋)) = ((𝑋 + (𝑍‘𝑋)) − (𝑍‘𝑋)))
213	74	recnd 11012	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℂ)
214	133	recnd 11012	. . . . . . . . . 10 ⊢ (𝜑 → (𝑍‘𝑋) ∈ ℂ)
215	213, 214	pncand 11342	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋 + (𝑍‘𝑋)) − (𝑍‘𝑋)) = 𝑋)
216	212, 215	eqtrd 2779	. . . . . . . 8 ⊢ (𝜑 → ((𝐸‘𝑋) − (𝑍‘𝑋)) = 𝑋)
217	216	3ad2ant1 1132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝐸‘𝑋) − (𝑍‘𝑋)) = 𝑋)
218	211, 217	breqtrd 5101	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋)
219		elioore 13118	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) → 𝑦 ∈ ℝ)
220	132	oveq2d 7300	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑦 + (𝑍‘𝑋)) = (𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
221	130	recnd 11012	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℂ)
222	52	recnd 11012	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑇 ∈ ℂ)
223	221, 222	mulneg1d 11437	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
224	220, 223	oveq12d 7302	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
225	224	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
226		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
227	131	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℝ)
228	226, 227	readdcld 11013	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ ℝ)
229	228	recnd 11012	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ ℂ)
230	227	recnd 11012	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) ∈ ℂ)
231	229, 230	negsubd 11347	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) + -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) − ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
232	226	recnd 11012	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
233	232, 230	pncand 11342	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) − ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) = 𝑦)
234	225, 231, 233	3eqtrrd 2784	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
235	219, 234	sylan2 593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
236	235	3ad2antl1 1184	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
237		simpl1 1190	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝜑)
238		fourierdlem41.qssd	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
239	238	3adant3 1131	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
240	239	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
241	202	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) ∈ ℝ^*)
242	207	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
243	219	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
244	133	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑍‘𝑋) ∈ ℝ)
245	243, 244	readdcld 11013	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
246	245	3ad2antl1 1184	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
247	133	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑍‘𝑋) ∈ ℝ)
248	197, 247	resubcld 11412	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ)
249	248	rexrd 11034	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ^*)
250	249	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ^*)
251	74	rexrd 11034	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ∈ ℝ^*)
252	251	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑋 ∈ ℝ^*)
253		simpr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋))
254		ioogtlb 43040	. . . . . . . . . . . . . . 15 ⊢ ((((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ^* ∧ 𝑋 ∈ ℝ^* ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑦)
255	250, 252, 253, 254	syl3anc 1370	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑦)
256	197	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) ∈ ℝ)
257	133	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑍‘𝑋) ∈ ℝ)
258	219	adantl 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ ℝ)
259	256, 257, 258	ltsubaddd 11580	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑦 ↔ (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋))))
260	255, 259	mpbid 231	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋)))
261	260	3adantl3 1167	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋)))
262	237, 136	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝐸‘𝑋) ∈ ℝ)
263	205	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
264	263	3adantl3 1167	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
265	74	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑋 ∈ ℝ)
266		iooltub 43055	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ^* ∧ 𝑋 ∈ ℝ^* ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 < 𝑋)
267	250, 252, 253, 266	syl3anc 1370	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 < 𝑋)
268	258, 265, 257, 267	ltadd1dd 11595	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝑋 + (𝑍‘𝑋)))
269	135	eqcomd 2745	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 + (𝑍‘𝑋)) = (𝐸‘𝑋))
270	269	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑋 + (𝑍‘𝑋)) = (𝐸‘𝑋))
271	268, 270	breqtrd 5101	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝐸‘𝑋))
272	271	3adantl3 1167	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝐸‘𝑋))
273		iocleub 43048	. . . . . . . . . . . . . . 15 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ≤ (𝑄‘(𝑖 + 1)))
274	202, 207, 208, 273	syl3anc 1370	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ≤ (𝑄‘(𝑖 + 1)))
275	274	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝐸‘𝑋) ≤ (𝑄‘(𝑖 + 1)))
276	246, 262, 264, 272, 275	ltletrd 11144	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) < (𝑄‘(𝑖 + 1)))
277	241, 242, 246, 261, 276	eliood 43043	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
278	240, 277	sseldd 3923	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (𝑦 + (𝑍‘𝑋)) ∈ 𝐷)
279	237, 128	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝐵 − 𝑋) / 𝑇) ∈ ℝ)
280	279	flcld 13527	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → (⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
281	280	znegcld 12437	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
282		negex 11228	. . . . . . . . . . 11 ⊢ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ V
283		eleq1 2827	. . . . . . . . . . . . 13 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑘 ∈ ℤ ↔ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ))
284	283	3anbi3d 1441	. . . . . . . . . . . 12 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)))
285		oveq1 7291	. . . . . . . . . . . . . 14 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (𝑘 · 𝑇) = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇))
286	285	oveq2d 7300	. . . . . . . . . . . . 13 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
287	286	eleq1d 2824	. . . . . . . . . . . 12 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷))
288	284, 287	imbi12d 345	. . . . . . . . . . 11 ⊢ (𝑘 = -(⌊‘((𝐵 − 𝑋) / 𝑇)) → (((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)))
289		ovex 7317	. . . . . . . . . . . 12 ⊢ (𝑦 + (𝑍‘𝑋)) ∈ V
290		eleq1 2827	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → (𝑥 ∈ 𝐷 ↔ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷))
291	290	3anbi2d 1440	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ)))
292		oveq1 7291	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)))
293	292	eleq1d 2824	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷))
294	291, 293	imbi12d 345	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 + (𝑍‘𝑋)) → (((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)))
295		fourierdlem41.dper	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)
296	289, 294, 295	vtocl 3499	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (𝑘 · 𝑇)) ∈ 𝐷)
297	282, 288, 296	vtocl 3499	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 + (𝑍‘𝑋)) ∈ 𝐷 ∧ -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ) → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
298	237, 278, 281, 297	syl3anc 1370	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
299	236, 298	eqeltrd 2840	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)) → 𝑦 ∈ 𝐷)
300	299	ralrimiva 3104	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑦 ∈ 𝐷)
301		dfss3 3910	. . . . . . 7 ⊢ ((((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷 ↔ ∀𝑦 ∈ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋)𝑦 ∈ 𝐷)
302	300, 301	sylibr 233	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷)
303		breq1 5078	. . . . . . . 8 ⊢ (𝑦 = ((𝑄‘𝑖) − (𝑍‘𝑋)) → (𝑦 < 𝑋 ↔ ((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋))
304		oveq1 7291	. . . . . . . . 9 ⊢ (𝑦 = ((𝑄‘𝑖) − (𝑍‘𝑋)) → (𝑦(,)𝑋) = (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋))
305	304	sseq1d 3953	. . . . . . . 8 ⊢ (𝑦 = ((𝑄‘𝑖) − (𝑍‘𝑋)) → ((𝑦(,)𝑋) ⊆ 𝐷 ↔ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷))
306	303, 305	anbi12d 631	. . . . . . 7 ⊢ (𝑦 = ((𝑄‘𝑖) − (𝑍‘𝑋)) → ((𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ↔ (((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋 ∧ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷)))
307	306	rspcev 3562	. . . . . 6 ⊢ ((((𝑄‘𝑖) − (𝑍‘𝑋)) ∈ ℝ ∧ (((𝑄‘𝑖) − (𝑍‘𝑋)) < 𝑋 ∧ (((𝑄‘𝑖) − (𝑍‘𝑋))(,)𝑋) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
308	200, 218, 302, 307	syl12anc 834	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1)))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
309	308	3exp 1118	. . . 4 ⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))))
310	309	rexlimdv 3213	. . 3 ⊢ (𝜑 → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,](𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷)))
311	193, 310	mpd 15	. 2 ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷))
312		0zd 12340	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℤ)
313	3	nnzd 12434	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
314		1zzd 12360	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℤ)
315		0le1 11507	. . . . . . . . 9 ⊢ 0 ≤ 1
316	315	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ 1)
317	3	nnge1d 12030	. . . . . . . 8 ⊢ (𝜑 → 1 ≤ 𝑀)
318	312, 313, 314, 316, 317	elfzd 13256	. . . . . . 7 ⊢ (𝜑 → 1 ∈ (0...𝑀))
319	101, 318	ffvelrnd 6971	. . . . . 6 ⊢ (𝜑 → (𝑄‘1) ∈ ℝ)
320	133, 52	resubcld 11412	. . . . . 6 ⊢ (𝜑 → ((𝑍‘𝑋) − 𝑇) ∈ ℝ)
321	319, 320	resubcld 11412	. . . . 5 ⊢ (𝜑 → ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
322	321	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
323	38	recnd 11012	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℂ)
324	323, 222	pncand 11342	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
325	324	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
326	43	oveq2i 7295	. . . . . . . . . . 11 ⊢ (𝐴 + 𝑇) = (𝐴 + (𝐵 − 𝐴))
327	326	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝐴 + 𝑇) = (𝐴 + (𝐵 − 𝐴)))
328	40	recnd 11012	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℂ)
329	323, 328	pncan3d 11344	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
330	329	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
331		id 22	. . . . . . . . . . . 12 ⊢ ((𝐸‘𝑋) = 𝐵 → (𝐸‘𝑋) = 𝐵)
332	331	eqcomd 2745	. . . . . . . . . . 11 ⊢ ((𝐸‘𝑋) = 𝐵 → 𝐵 = (𝐸‘𝑋))
333	332	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → 𝐵 = (𝐸‘𝑋))
334	327, 330, 333	3eqtrrd 2784	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝐸‘𝑋) = (𝐴 + 𝑇))
335	334	oveq1d 7299	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝐸‘𝑋) − 𝑇) = ((𝐴 + 𝑇) − 𝑇))
336	33	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑄‘0) = 𝐴)
337	325, 335, 336	3eqtr4rd 2790	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑄‘0) = ((𝐸‘𝑋) − 𝑇))
338	337	oveq1d 7299	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑄‘0) − ((𝑍‘𝑋) − 𝑇)) = (((𝐸‘𝑋) − 𝑇) − ((𝑍‘𝑋) − 𝑇)))
339	136	recnd 11012	. . . . . . . 8 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℂ)
340	339, 214, 222	nnncan2d 11376	. . . . . . 7 ⊢ (𝜑 → (((𝐸‘𝑋) − 𝑇) − ((𝑍‘𝑋) − 𝑇)) = ((𝐸‘𝑋) − (𝑍‘𝑋)))
341	340	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (((𝐸‘𝑋) − 𝑇) − ((𝑍‘𝑋) − 𝑇)) = ((𝐸‘𝑋) − (𝑍‘𝑋)))
342	216	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝐸‘𝑋) − (𝑍‘𝑋)) = 𝑋)
343	338, 341, 342	3eqtrrd 2784	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → 𝑋 = ((𝑄‘0) − ((𝑍‘𝑋) − 𝑇)))
344	33, 38	eqeltrd 2840	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
345	3	nngt0d 12031	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝑀)
346		fzolb 13402	. . . . . . . . . 10 ⊢ (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
347	312, 313, 345, 346	syl3anbrc 1342	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0..^𝑀))
348		0re 10986	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
349		eleq1 2827	. . . . . . . . . . . . 13 ⊢ (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀)))
350	349	anbi2d 629	. . . . . . . . . . . 12 ⊢ (𝑖 = 0 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀))))
351		fveq2 6783	. . . . . . . . . . . . 13 ⊢ (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0))
352		oveq1 7291	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
353	352	fveq2d 6787	. . . . . . . . . . . . 13 ⊢ (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1)))
354	351, 353	breq12d 5088	. . . . . . . . . . . 12 ⊢ (𝑖 = 0 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1))))
355	350, 354	imbi12d 345	. . . . . . . . . . 11 ⊢ (𝑖 = 0 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))))
356	355, 149	vtoclg 3506	. . . . . . . . . 10 ⊢ (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))
357	348, 356	ax-mp 5	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))
358	347, 357	mpdan 684	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1)))
359		0p1e1 12104	. . . . . . . . . 10 ⊢ (0 + 1) = 1
360	359	fveq2i 6786	. . . . . . . . 9 ⊢ (𝑄‘(0 + 1)) = (𝑄‘1)
361	360	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1))
362	358, 361	breqtrd 5101	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) < (𝑄‘1))
363	344, 319, 320, 362	ltsub1dd 11596	. . . . . 6 ⊢ (𝜑 → ((𝑄‘0) − ((𝑍‘𝑋) − 𝑇)) < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
364	363	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑄‘0) − ((𝑍‘𝑋) − 𝑇)) < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
365	343, 364	eqbrtrd 5097	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → 𝑋 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
366		elioore 13118	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) → 𝑦 ∈ ℝ)
367	132	eqcomd 2745	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = (𝑍‘𝑋))
368	367	negeqd 11224	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → -((⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = -(𝑍‘𝑋))
369	223, 368	eqtrd 2779	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) = -(𝑍‘𝑋))
370	222	mulid2d 11002	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 · 𝑇) = 𝑇)
371	369, 370	oveq12d 7302	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) + (1 · 𝑇)) = (-(𝑍‘𝑋) + 𝑇))
372	221	negcld 11328	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℂ)
373		1cnd 10979	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℂ)
374	372, 373, 222	adddird 11009	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇) = ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇) + (1 · 𝑇)))
375	214, 222	negsubdid 11356	. . . . . . . . . . . . 13 ⊢ (𝜑 → -((𝑍‘𝑋) − 𝑇) = (-(𝑍‘𝑋) + 𝑇))
376	371, 374, 375	3eqtr4d 2789	. . . . . . . . . . . 12 ⊢ (𝜑 → ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇) = -((𝑍‘𝑋) − 𝑇))
377	376	oveq2d 7300	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + -((𝑍‘𝑋) − 𝑇)))
378	377	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + -((𝑍‘𝑋) − 𝑇)))
379	320	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑍‘𝑋) − 𝑇) ∈ ℝ)
380	226, 379	readdcld 11013	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
381	380	recnd 11012	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ℂ)
382	379	recnd 11012	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑍‘𝑋) − 𝑇) ∈ ℂ)
383	381, 382	negsubd 11347	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + -((𝑍‘𝑋) − 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) − ((𝑍‘𝑋) − 𝑇)))
384	232, 382	pncand 11342	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) − ((𝑍‘𝑋) − 𝑇)) = 𝑦)
385	378, 383, 384	3eqtrrd 2784	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)))
386	366, 385	sylan2 593	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)))
387	386	adantlr 712	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)))
388		simpll 764	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝜑)
389	361	eqcomd 2745	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘1) = (𝑄‘(0 + 1)))
390	389	oveq2d 7300	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄‘0)(,)(𝑄‘1)) = ((𝑄‘0)(,)(𝑄‘(0 + 1))))
391	351, 353	oveq12d 7302	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 0 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘0)(,)(𝑄‘(0 + 1))))
392	391	sseq1d 3953	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 0 → (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷 ↔ ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷))
393	350, 392	imbi12d 345	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 0 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)))
394	393, 238	vtoclg 3506	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷))
395	348, 394	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)
396	347, 395	mpdan 684	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄‘0)(,)(𝑄‘(0 + 1))) ⊆ 𝐷)
397	390, 396	eqsstrd 3960	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑄‘0)(,)(𝑄‘1)) ⊆ 𝐷)
398	397	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑄‘0)(,)(𝑄‘1)) ⊆ 𝐷)
399	33, 39	eqeltrd 2840	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ^*)
400	399	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘0) ∈ ℝ^*)
401	319	rexrd 11034	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄‘1) ∈ ℝ^*)
402	401	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘1) ∈ ℝ^*)
403	366, 380	sylan2 593	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
404	403	adantlr 712	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ℝ)
405	339, 213, 214	subaddd 11359	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐸‘𝑋) − 𝑋) = (𝑍‘𝑋) ↔ (𝑋 + (𝑍‘𝑋)) = (𝐸‘𝑋)))
406	269, 405	mpbird 256	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸‘𝑋) − 𝑋) = (𝑍‘𝑋))
407		oveq1 7291	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸‘𝑋) = 𝐵 → ((𝐸‘𝑋) − 𝑋) = (𝐵 − 𝑋))
408	406, 407	sylan9req 2800	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑍‘𝑋) = (𝐵 − 𝑋))
409	408	oveq1d 7299	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑍‘𝑋) − 𝑇) = ((𝐵 − 𝑋) − 𝑇))
410	409	oveq2d 7300	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑋 + ((𝑍‘𝑋) − 𝑇)) = (𝑋 + ((𝐵 − 𝑋) − 𝑇)))
411	127	recnd 11012	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℂ)
412	213, 411, 222	addsubassd 11361	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 + (𝐵 − 𝑋)) − 𝑇) = (𝑋 + ((𝐵 − 𝑋) − 𝑇)))
413	412	eqcomd 2745	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 + ((𝐵 − 𝑋) − 𝑇)) = ((𝑋 + (𝐵 − 𝑋)) − 𝑇))
414	413	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑋 + ((𝐵 − 𝑋) − 𝑇)) = ((𝑋 + (𝐵 − 𝑋)) − 𝑇))
415	328, 222, 323	subsub23d 42833	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 − 𝑇) = 𝐴 ↔ (𝐵 − 𝐴) = 𝑇))
416	58, 415	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 − 𝑇) = 𝐴)
417	213, 328	pncan3d 11344	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋 + (𝐵 − 𝑋)) = 𝐵)
418	417	oveq1d 7299	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋 + (𝐵 − 𝑋)) − 𝑇) = (𝐵 − 𝑇))
419	416, 418, 33	3eqtr4d 2789	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑋 + (𝐵 − 𝑋)) − 𝑇) = (𝑄‘0))
420	419	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ((𝑋 + (𝐵 − 𝑋)) − 𝑇) = (𝑄‘0))
421	410, 414, 420	3eqtrrd 2784	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑄‘0) = (𝑋 + ((𝑍‘𝑋) − 𝑇)))
422	421	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘0) = (𝑋 + ((𝑍‘𝑋) − 𝑇)))
423	74	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑋 ∈ ℝ)
424	366	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 ∈ ℝ)
425	320	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑍‘𝑋) − 𝑇) ∈ ℝ)
426	251	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑋 ∈ ℝ^*)
427	321	rexrd 11034	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ^*)
428	427	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ^*)
429		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))))
430		ioogtlb 43040	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ ℝ^* ∧ ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ^* ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑋 < 𝑦)
431	426, 428, 429, 430	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑋 < 𝑦)
432	423, 424, 425, 431	ltadd1dd 11595	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑋 + ((𝑍‘𝑋) − 𝑇)) < (𝑦 + ((𝑍‘𝑋) − 𝑇)))
433	432	adantlr 712	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑋 + ((𝑍‘𝑋) − 𝑇)) < (𝑦 + ((𝑍‘𝑋) − 𝑇)))
434	422, 433	eqbrtrd 5097	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘0) < (𝑦 + ((𝑍‘𝑋) − 𝑇)))
435		iooltub 43055	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ ℝ^* ∧ ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ^* ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
436	426, 428, 429, 435	syl3anc 1370	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))
437	319	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑄‘1) ∈ ℝ)
438	424, 425, 437	ltaddsubd 11584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) < (𝑄‘1) ↔ 𝑦 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))))
439	436, 438	mpbird 256	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) < (𝑄‘1))
440	439	adantlr 712	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) < (𝑄‘1))
441	400, 402, 404, 434, 440	eliood 43043	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ ((𝑄‘0)(,)(𝑄‘1)))
442	398, 441	sseldd 3923	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷)
443	129	znegcld 12437	. . . . . . . . . 10 ⊢ (𝜑 → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
444	443	peano2zd 12438	. . . . . . . . 9 ⊢ (𝜑 → (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ)
445	444	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ)
446		ovex 7317	. . . . . . . . 9 ⊢ (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ V
447		eleq1 2827	. . . . . . . . . . 11 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → (𝑘 ∈ ℤ ↔ (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ))
448	447	3anbi3d 1441	. . . . . . . . . 10 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ)))
449		oveq1 7291	. . . . . . . . . . . 12 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → (𝑘 · 𝑇) = ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇))
450	449	oveq2d 7300	. . . . . . . . . . 11 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)))
451	450	eleq1d 2824	. . . . . . . . . 10 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → (((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷))
452	448, 451	imbi12d 345	. . . . . . . . 9 ⊢ (𝑘 = (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) → (((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)))
453		ovex 7317	. . . . . . . . . 10 ⊢ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ V
454		eleq1 2827	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → (𝑥 ∈ 𝐷 ↔ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷))
455	454	3anbi2d 1440	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ)))
456		oveq1 7291	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)))
457	456	eleq1d 2824	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → ((𝑥 + (𝑘 · 𝑇)) ∈ 𝐷 ↔ ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷))
458	455, 457	imbi12d 345	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 + ((𝑍‘𝑋) − 𝑇)) → (((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) ↔ ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷)))
459	453, 458, 295	vtocl 3499	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + (𝑘 · 𝑇)) ∈ 𝐷)
460	446, 452, 459	vtocl 3499	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 + ((𝑍‘𝑋) − 𝑇)) ∈ 𝐷 ∧ (-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) ∈ ℤ) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)
461	388, 442, 445, 460	syl3anc 1370	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → ((𝑦 + ((𝑍‘𝑋) − 𝑇)) + ((-(⌊‘((𝐵 − 𝑋) / 𝑇)) + 1) · 𝑇)) ∈ 𝐷)
462	387, 461	eqeltrd 2840	. . . . . 6 ⊢ (((𝜑 ∧ (𝐸‘𝑋) = 𝐵) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))) → 𝑦 ∈ 𝐷)
463	462	ralrimiva 3104	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ∀𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))𝑦 ∈ 𝐷)
464		dfss3 3910	. . . . 5 ⊢ ((𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷 ↔ ∀𝑦 ∈ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)))𝑦 ∈ 𝐷)
465	463, 464	sylibr 233	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷)
466		breq2 5079	. . . . . 6 ⊢ (𝑦 = ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) → (𝑋 < 𝑦 ↔ 𝑋 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))))
467		oveq2 7292	. . . . . . 7 ⊢ (𝑦 = ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) → (𝑋(,)𝑦) = (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))))
468	467	sseq1d 3953	. . . . . 6 ⊢ (𝑦 = ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) → ((𝑋(,)𝑦) ⊆ 𝐷 ↔ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷))
469	466, 468	anbi12d 631	. . . . 5 ⊢ (𝑦 = ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) → ((𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷) ↔ (𝑋 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∧ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷)))
470	469	rspcev 3562	. . . 4 ⊢ ((((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∈ ℝ ∧ (𝑋 < ((𝑄‘1) − ((𝑍‘𝑋) − 𝑇)) ∧ (𝑋(,)((𝑄‘1) − ((𝑍‘𝑋) − 𝑇))) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
471	322, 365, 465, 470	syl12anc 834	. . 3 ⊢ ((𝜑 ∧ (𝐸‘𝑋) = 𝐵) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
472	15	adantlr 712	. . . . . 6 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋))
473		simp2 1136	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ (0...𝑀))
474	25	3ad2ant2 1133	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ ℝ)
475	94	3ad2ant2 1133	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑀 ∈ ℝ)
476	96	3ad2ant2 1133	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ≤ 𝑀)
477		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑄‘𝑗) = (𝐸‘𝑋) → (𝑄‘𝑗) = (𝐸‘𝑋))
478	477	eqcomd 2745	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄‘𝑗) = (𝐸‘𝑋) → (𝐸‘𝑋) = (𝑄‘𝑗))
479	478	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝑄‘𝑗) = (𝐸‘𝑋) ∧ 𝑀 = 𝑗) → (𝐸‘𝑋) = (𝑄‘𝑗))
480	479	3ad2antl3 1186	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → (𝐸‘𝑋) = (𝑄‘𝑗))
481		fveq2 6783	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 = 𝑗 → (𝑄‘𝑀) = (𝑄‘𝑗))
482	481	eqcomd 2745	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 = 𝑗 → (𝑄‘𝑗) = (𝑄‘𝑀))
483	482	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → (𝑄‘𝑗) = (𝑄‘𝑀))
484	177	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑀 = 𝑗) → (𝑄‘𝑀) = 𝐵)
485	484	3ad2antl1 1184	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → (𝑄‘𝑀) = 𝐵)
486	480, 483, 485	3eqtrd 2783	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → (𝐸‘𝑋) = 𝐵)
487		neneq 2950	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸‘𝑋) ≠ 𝐵 → ¬ (𝐸‘𝑋) = 𝐵)
488	487	ad2antlr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑀 = 𝑗) → ¬ (𝐸‘𝑋) = 𝐵)
489	488	3ad2antl1 1184	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) ∧ 𝑀 = 𝑗) → ¬ (𝐸‘𝑋) = 𝐵)
490	486, 489	pm2.65da 814	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → ¬ 𝑀 = 𝑗)
491	490	neqned 2951	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑀 ≠ 𝑗)
492	474, 475, 476, 491	leneltd 11138	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 < 𝑀)
493		elfzfzo 42822	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0..^𝑀) ↔ (𝑗 ∈ (0...𝑀) ∧ 𝑗 < 𝑀))
494	473, 492, 493	sylanbrc 583	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝑗 ∈ (0..^𝑀))
495	114	adantlr 712	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ^*)
496	495	3adant3 1131	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ∈ ℝ^*)
497		simp1l 1196	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → 𝜑)
498	101	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
499		fzofzp1 13493	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0..^𝑀) → (𝑗 + 1) ∈ (0...𝑀))
500	499	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑗 + 1) ∈ (0...𝑀))
501	498, 500	ffvelrnd 6971	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ)
502	501	rexrd 11034	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ^*)
503	497, 494, 502	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘(𝑗 + 1)) ∈ ℝ^*)
504	138	3adant1r 1176	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ℝ^*)
505	37, 157	eqbrtrd 5097	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ≤ (𝐸‘𝑋))
506	505	adantlr 712	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ≤ (𝐸‘𝑋))
507	506	3adant2 1130	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) ≤ (𝐸‘𝑋))
508	478	3ad2ant3 1134	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) = (𝑄‘𝑗))
509		eleq1 2827	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑖 ∈ (0..^𝑀) ↔ 𝑗 ∈ (0..^𝑀)))
510	509	anbi2d 629	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑗 ∈ (0..^𝑀))))
511		fveq2 6783	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑄‘𝑖) = (𝑄‘𝑗))
512		oveq1 7291	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
513	512	fveq2d 6787	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑗 + 1)))
514	511, 513	breq12d 5088	. . . . . . . . . . . . . . 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 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))
518	508, 517	eqbrtrd 5097	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) < (𝑄‘(𝑗 + 1)))
519	496, 503, 504, 507, 518	elicod 13138	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → (𝐸‘𝑋) ∈ ((𝑄‘𝑗)[,)(𝑄‘(𝑗 + 1))))
520	511, 513	oveq12d 7302	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) = ((𝑄‘𝑗)[,)(𝑄‘(𝑗 + 1))))
521	520	eleq2d 2825	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) ↔ (𝐸‘𝑋) ∈ ((𝑄‘𝑗)[,)(𝑄‘(𝑗 + 1)))))
522	521	rspcev 3562	. . . . . . . . . 10 ⊢ ((𝑗 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑗)[,)(𝑄‘(𝑗 + 1)))) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
523	494, 519, 522	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = (𝐸‘𝑋)) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
524	523	3exp 1118	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → (𝑗 ∈ (0...𝑀) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))))
525	524	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (𝑗 ∈ (0...𝑀) → ((𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))))
526	525	rexlimdv 3213	. . . . . 6 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = (𝐸‘𝑋) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))))
527	472, 526	mpd 15	. . . . 5 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
528		ioossico 13179	. . . . . . . . . . 11 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))
529		simpr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
530	528, 529	sselid 3920	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
531	530	ex 413	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))))
532	531	adantlr 712	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))))
533	532	reximdva 3204	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))))
534	187, 533	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
535	534	adantlr 712	. . . . 5 ⊢ (((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) ∧ ¬ (𝐸‘𝑋) ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
536	527, 535	pm2.61dan 810	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → ∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
537	205, 247	resubcld 11412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ)
538	537	3adant3 1131	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ)
539	216	eqcomd 2745	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 = ((𝐸‘𝑋) − (𝑍‘𝑋)))
540	539	3ad2ant1 1132	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → 𝑋 = ((𝐸‘𝑋) − (𝑍‘𝑋)))
541	136	3ad2ant1 1132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ℝ)
542	205	3adant3 1131	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
543	133	3ad2ant1 1132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑍‘𝑋) ∈ ℝ)
544	197	rexrd 11034	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ^*)
545	544	3adant3 1131	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ^*)
546	206	3adant3 1131	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
547		simp3 1137	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
548		icoltub 43053	. . . . . . . . . . 11 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) < (𝑄‘(𝑖 + 1)))
549	545, 546, 547, 548	syl3anc 1370	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝐸‘𝑋) < (𝑄‘(𝑖 + 1)))
550	541, 542, 543, 549	ltsub1dd 11596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝐸‘𝑋) − (𝑍‘𝑋)) < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))
551	540, 550	eqbrtrd 5097	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → 𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))
552		elioore 13118	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) → 𝑦 ∈ ℝ)
553	552, 234	sylan2 593	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
554	553	3ad2antl1 1184	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 = ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)))
555		simpl1 1190	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝜑)
556	238	3adant3 1131	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
557	556	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)
558	545	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘𝑖) ∈ ℝ^*)
559	546	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
560	552	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 ∈ ℝ)
561	133	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑍‘𝑋) ∈ ℝ)
562	560, 561	readdcld 11013	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
563	562	3ad2antl1 1184	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) ∈ ℝ)
564	197	3adant3 1131	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
565	564	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘𝑖) ∈ ℝ)
566	555, 136	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝐸‘𝑋) ∈ ℝ)
567		icogelb 13139	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ≤ (𝐸‘𝑋))
568	545, 546, 547, 567	syl3anc 1370	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ≤ (𝐸‘𝑋))
569	568	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘𝑖) ≤ (𝐸‘𝑋))
570	135	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝐸‘𝑋) = (𝑋 + (𝑍‘𝑋)))
571	74	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑋 ∈ ℝ)
572	552	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 ∈ ℝ)
573	133	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑍‘𝑋) ∈ ℝ)
574	251	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑋 ∈ ℝ^*)
575	537	rexrd 11034	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ^*)
576	575	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ^*)
577		simpr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))))
578		ioogtlb 43040	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋 ∈ ℝ^* ∧ ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ^* ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑋 < 𝑦)
579	574, 576, 577, 578	syl3anc 1370	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑋 < 𝑦)
580	571, 572, 573, 579	ltadd1dd 11595	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑋 + (𝑍‘𝑋)) < (𝑦 + (𝑍‘𝑋)))
581	570, 580	eqbrtrd 5097	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝐸‘𝑋) < (𝑦 + (𝑍‘𝑋)))
582	581	3adantl3 1167	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝐸‘𝑋) < (𝑦 + (𝑍‘𝑋)))
583	565, 566, 563, 569, 582	lelttrd 11142	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑄‘𝑖) < (𝑦 + (𝑍‘𝑋)))
584	537	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ)
585		iooltub 43055	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋 ∈ ℝ^* ∧ ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ^* ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))
586	574, 576, 577, 585	syl3anc 1370	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))
587	572, 584, 573, 586	ltadd1dd 11595	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) < (((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) + (𝑍‘𝑋)))
588	205	recnd 11012	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
589	214	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑍‘𝑋) ∈ ℂ)
590	588, 589	npcand 11345	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) + (𝑍‘𝑋)) = (𝑄‘(𝑖 + 1)))
591	590	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) + (𝑍‘𝑋)) = (𝑄‘(𝑖 + 1)))
592	587, 591	breqtrd 5101	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) < (𝑄‘(𝑖 + 1)))
593	592	3adantl3 1167	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) < (𝑄‘(𝑖 + 1)))
594	558, 559, 563, 583, 593	eliood 43043	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
595	557, 594	sseldd 3923	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → (𝑦 + (𝑍‘𝑋)) ∈ 𝐷)
596	555, 443	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → -(⌊‘((𝐵 − 𝑋) / 𝑇)) ∈ ℤ)
597	555, 595, 596, 297	syl3anc 1370	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → ((𝑦 + (𝑍‘𝑋)) + (-(⌊‘((𝐵 − 𝑋) / 𝑇)) · 𝑇)) ∈ 𝐷)
598	554, 597	eqeltrd 2840	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))) → 𝑦 ∈ 𝐷)
599	598	ralrimiva 3104	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ∀𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))𝑦 ∈ 𝐷)
600		dfss3 3910	. . . . . . . . 9 ⊢ ((𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷 ↔ ∀𝑦 ∈ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)))𝑦 ∈ 𝐷)
601	599, 600	sylibr 233	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷)
602		breq2 5079	. . . . . . . . . 10 ⊢ (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) → (𝑋 < 𝑦 ↔ 𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))))
603		oveq2 7292	. . . . . . . . . . 11 ⊢ (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) → (𝑋(,)𝑦) = (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))))
604	603	sseq1d 3953	. . . . . . . . . 10 ⊢ (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) → ((𝑋(,)𝑦) ⊆ 𝐷 ↔ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷))
605	602, 604	anbi12d 631	. . . . . . . . 9 ⊢ (𝑦 = ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) → ((𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷) ↔ (𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∧ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷)))
606	605	rspcev 3562	. . . . . . . 8 ⊢ ((((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∈ ℝ ∧ (𝑋 < ((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋)) ∧ (𝑋(,)((𝑄‘(𝑖 + 1)) − (𝑍‘𝑋))) ⊆ 𝐷)) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
607	538, 551, 601, 606	syl12anc 834	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
608	607	3exp 1118	. . . . . 6 ⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))))
609	608	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → (𝑖 ∈ (0..^𝑀) → ((𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))))
610	609	rexlimdv 3213	. . . 4 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → (∃𝑖 ∈ (0..^𝑀)(𝐸‘𝑋) ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))
611	536, 610	mpd 15	. . 3 ⊢ ((𝜑 ∧ (𝐸‘𝑋) ≠ 𝐵) → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
612	471, 611	pm2.61dane 3033	. 2 ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))
613	311, 612	jca 512	1 ⊢ (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ∧ ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ≠ wne 2944 ∀wral 3065 ∃wrex 3066 {crab 3069 ⊆ wss 3888 class class class wbr 5075 ↦ cmpt 5158 ran crn 5591 Fn wfn 6432 ⟶wf 6433 ‘cfv 6437 (class class class)co 7284 ↑_m cmap 8624 supcsup 9208 ℂcc 10878 ℝcr 10879 0cc0 10880 1c1 10881 + caddc 10883 · cmul 10885 ℝ^*cxr 11017 < clt 11018 ≤ cle 11019 − cmin 11214 -cneg 11215 / cdiv 11641 ℕcn 11982 ℤcz 12328 ℤ_≥cuz 12591 (,)cioo 13088 (,]cioc 13089 [,)cico 13090 [,]cicc 13091 ...cfz 13248 ..^cfzo 13391 ⌊cfl 13519

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 2710 ax-sep 5224 ax-nul 5231 ax-pow 5289 ax-pr 5353 ax-un 7597 ax-cnex 10936 ax-resscn 10937 ax-1cn 10938 ax-icn 10939 ax-addcl 10940 ax-addrcl 10941 ax-mulcl 10942 ax-mulrcl 10943 ax-mulcom 10944 ax-addass 10945 ax-mulass 10946 ax-distr 10947 ax-i2m1 10948 ax-1ne0 10949 ax-1rid 10950 ax-rnegex 10951 ax-rrecex 10952 ax-cnre 10953 ax-pre-lttri 10954 ax-pre-lttrn 10955 ax-pre-ltadd 10956 ax-pre-mulgt0 10957 ax-pre-sup 10958

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3070 df-rex 3071 df-rmo 3072 df-reu 3073 df-rab 3074 df-v 3435 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-pss 3907 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4841 df-iun 4927 df-br 5076 df-opab 5138 df-mpt 5159 df-tr 5193 df-id 5490 df-eprel 5496 df-po 5504 df-so 5505 df-fr 5545 df-we 5547 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-pred 6206 df-ord 6273 df-on 6274 df-lim 6275 df-suc 6276 df-iota 6395 df-fun 6439 df-fn 6440 df-f 6441 df-f1 6442 df-fo 6443 df-f1o 6444 df-fv 6445 df-riota 7241 df-ov 7287 df-oprab 7288 df-mpo 7289 df-om 7722 df-1st 7840 df-2nd 7841 df-frecs 8106 df-wrecs 8137 df-recs 8211 df-rdg 8250 df-1o 8306 df-er 8507 df-map 8626 df-en 8743 df-dom 8744 df-sdom 8745 df-fin 8746 df-sup 9210 df-inf 9211 df-pnf 11020 df-mnf 11021 df-xr 11022 df-ltxr 11023 df-le 11024 df-sub 11216 df-neg 11217 df-div 11642 df-nn 11983 df-n0 12243 df-z 12329 df-uz 12592 df-rp 12740 df-ioo 13092 df-ioc 13093 df-ico 13094 df-icc 13095 df-fz 13249 df-fzo 13392 df-fl 13521

This theorem is referenced by: fourierdlem113 43767

W3C validator