fourierdlem64 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem64 47274

Description: The partition 𝑉 is finer than 𝑄, when 𝑄 is moved on the same interval where 𝑉 lies. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem64.t	⊢ 𝑇 = (𝐵 − 𝐴)
fourierdlem64.p	⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem64.m	⊢ (𝜑 → 𝑀 ∈ ℕ)
fourierdlem64.q	⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
fourierdlem64.c	⊢ (𝜑 → 𝐶 ∈ ℝ)
fourierdlem64.d	⊢ (𝜑 → 𝐷 ∈ ℝ)
fourierdlem64.cltd	⊢ (𝜑 → 𝐶 < 𝐷)
fourierdlem64.h	⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
fourierdlem64.n	⊢ 𝑁 = ((♯‘𝐻) − 1)
fourierdlem64.v	⊢ 𝑉 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
fourierdlem64.j	⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
fourierdlem64.l	⊢ 𝐿 = sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < )
fourierdlem64.i	⊢ 𝐼 = sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < )

**Assertion**
Ref	Expression
fourierdlem64	⊢ (𝜑 → ((𝐼 ∈ (0..^𝑀) ∧ 𝐿 ∈ ℤ) ∧ ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))))

Distinct variable groups: 𝐴,𝑖,𝑚,𝑝 𝑉,𝑝 𝑇,𝑙 𝑦,𝑄 𝑉,𝑙 𝑄,𝑙,𝑖 𝑄,𝑝 𝜑,𝑗 𝑗,𝐿 𝑓,𝑉 𝜑,𝑓 𝑗,𝑉 𝑇,𝑖,𝑦 𝐿,𝑙 𝑖,𝑉,𝑘,𝑦 𝑇,𝑗,𝑘 𝑓,𝑁 𝜑,𝑖,𝑘 𝑄,𝑗,𝑘 𝑖,𝑀,𝑚,𝑝 𝑖,𝑁,𝑦 𝑖,𝐽,𝑙 𝑘,𝐿,𝑦 𝑗,𝐽,𝑘 𝑗,𝐻 𝑦,𝐻 𝐵,𝑖,𝑚,𝑝 𝑗,𝐼,𝑘 𝑦,𝐼,𝑖 𝐼,𝑙 𝐶,𝑚,𝑝 𝐷,𝑚,𝑝 𝑗,𝑀,𝑘 𝑗,𝑁 𝑓,𝐻 𝑚,𝑁,𝑝 𝑦,𝐷 𝑦,𝐶 Allowed substitution hints: 𝜑(𝑦, 𝑚, 𝑝, 𝑙) 𝐴(𝑦, 𝑓, 𝑗, 𝑘, 𝑙) 𝐵(𝑦, 𝑓, 𝑗, 𝑘, 𝑙) 𝐶(𝑓, 𝑖, 𝑗, 𝑘, 𝑙) 𝐷(𝑓, 𝑖, 𝑗, 𝑘, 𝑙) 𝑃(𝑦, 𝑓, 𝑖, 𝑗, 𝑘, 𝑚, 𝑝, 𝑙) 𝑄(𝑓, 𝑚) 𝑇(𝑓, 𝑚, 𝑝) 𝐻(𝑖, 𝑘, 𝑚, 𝑝, 𝑙) 𝐼(𝑓, 𝑚, 𝑝) 𝐽(𝑦, 𝑓, 𝑚, 𝑝) 𝐿(𝑓, 𝑖, 𝑚, 𝑝) 𝑀(𝑦, 𝑓, 𝑙) 𝑁(𝑘, 𝑙) 𝑉(𝑚)

Proof of Theorem fourierdlem64 Dummy variables 𝑏 𝑥 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem64.i	. . 3 ⊢ 𝐼 = sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < )
2		ssrab2 4005	. . . 4 ⊢ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ (0..^𝑀)
3		fzossfz 13817	. . . . . . . 8 ⊢ (0..^𝑀) ⊆ (0...𝑀)
4		fzssz 13662	. . . . . . . 8 ⊢ (0...𝑀) ⊆ ℤ
5	3, 4	sstri 3917	. . . . . . 7 ⊢ (0..^𝑀) ⊆ ℤ
6	2, 5	sstri 3917	. . . . . 6 ⊢ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ
7	6	a1i 11	. . . . 5 ⊢ (𝜑 → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ)
8		0zd 12709	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℤ)
9		fourierdlem64.m	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
10	9	nnzd 12723	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
11	9	nngt0d 12391	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝑀)
12		fzolb 13804	. . . . . . . 8 ⊢ (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
13	8, 10, 11, 12	syl3anbrc 1362	. . . . . . 7 ⊢ (𝜑 → 0 ∈ (0..^𝑀))
14		fourierdlem64.l	. . . . . . . . . 10 ⊢ 𝐿 = sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < )
15		ssrab2 4005	. . . . . . . . . . . 12 ⊢ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ
16	15	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ)
17		fourierdlem64.h	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
18		fourierdlem64.c	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐶 ∈ ℝ)
19		fourierdlem64.d	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 ∈ ℝ)
20		prssi 4776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → {𝐶, 𝐷} ⊆ ℝ)
21	18, 19, 20	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ ℝ)
22		ssrab2 4005	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷)
23	22	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷))
24	18, 19	iccssred 13569	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐶[,]𝐷) ⊆ ℝ)
25	23, 24	sstrd 3918	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ ℝ)
26	21, 25	unssd 4190	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ ℝ)
27	17, 26	eqsstrid 3946	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ⊆ ℝ)
28		fourierdlem64.t	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑇 = (𝐵 − 𝐴)
29		fourierdlem64.p	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
30		fourierdlem64.q	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
31		fourierdlem64.cltd	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐶 < 𝐷)
32		eqid 2760	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
33		fourierdlem64.n	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑁 = ((♯‘𝐻) − 1)
34		fourierdlem64.v	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑉 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
35	28, 29, 9, 30, 18, 19, 31, 32, 17, 33, 34	fourierdlem54 47264	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑉 ∈ ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑁)) ∧ 𝑉 Isom < , < ((0...𝑁), 𝐻)))
36	35	simprd 501	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑉 Isom < , < ((0...𝑁), 𝐻))
37		isof1o 7332	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑉 Isom < , < ((0...𝑁), 𝐻) → 𝑉:(0...𝑁)–1-1-onto→𝐻)
38		f1of 6825	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑉:(0...𝑁)–1-1-onto→𝐻 → 𝑉:(0...𝑁)⟶𝐻)
39	36, 37, 38	3syl 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑉:(0...𝑁)⟶𝐻)
40		fourierdlem64.j	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
41		elfzofz 13814	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
42	40, 41	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐽 ∈ (0...𝑁))
43	39, 42	ffvelcdmd 7086	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑉‘𝐽) ∈ 𝐻)
44	27, 43	sseldd 3909	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑉‘𝐽) ∈ ℝ)
45	29	fourierdlem2 47213	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
46	9, 45	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
47	30, 46	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
48	47	simpld 500	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
49		elmapi 8873	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
50	48, 49	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
51	9	nnnn0d 12671	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
52		nn0uz 13007	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ₀ = (ℤ_≥‘0)
53	51, 52	eleqtrdi 2870	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
54		eluzfz1 13668	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
55	53, 54	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 ∈ (0...𝑀))
56	50, 55	ffvelcdmd 7086	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
57	44, 56	resubcld 11748	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑉‘𝐽) − (𝑄‘0)) ∈ ℝ)
58	29, 9, 30	fourierdlem11 47222	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
59	58	simp2d 1161	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ)
60	58	simp1d 1160	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℝ)
61	59, 60	resubcld 11748	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
62	28, 61	eqeltrid 2864	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ∈ ℝ)
63	58	simp3d 1162	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 < 𝐵)
64	60, 59	posdifd 11907	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
65	63, 64	mpbid 235	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
66	65, 28	breqtrrdi 5146	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝑇)
67	66	gt0ne0d 11884	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ≠ 0)
68	57, 62, 67	redivcld 12149	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∈ ℝ)
69		btwnz 12806	. . . . . . . . . . . . . . 15 ⊢ ((((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∈ ℝ → (∃𝑘 ∈ ℤ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∧ ∃𝑧 ∈ ℤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) < 𝑧))
70	68, 69	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑘 ∈ ℤ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∧ ∃𝑧 ∈ ℤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) < 𝑧))
71	70	simpld 500	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∃𝑘 ∈ ℤ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
72		zre 12701	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℝ)
73	56	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (𝑄‘0) ∈ ℝ)
74		simplr 781	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → 𝑘 ∈ ℝ)
75	62	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → 𝑇 ∈ ℝ)
76	74, 75	remulcld 11343	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (𝑘 · 𝑇) ∈ ℝ)
77	73, 76	readdcld 11342	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑄‘0) + (𝑘 · 𝑇)) ∈ ℝ)
78	44	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (𝑉‘𝐽) ∈ ℝ)
79		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
80	57	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑉‘𝐽) − (𝑄‘0)) ∈ ℝ)
81	62, 66	elrpd 13165	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑇 ∈ ℝ⁺)
82	81	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → 𝑇 ∈ ℝ⁺)
83	74, 80, 82	ltmuldivd 13215	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑘 · 𝑇) < ((𝑉‘𝐽) − (𝑄‘0)) ↔ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)))
84	79, 83	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (𝑘 · 𝑇) < ((𝑉‘𝐽) − (𝑄‘0)))
85	56	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (𝑄‘0) ∈ ℝ)
86		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → 𝑘 ∈ ℝ)
87	62	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → 𝑇 ∈ ℝ)
88	86, 87	remulcld 11343	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (𝑘 · 𝑇) ∈ ℝ)
89	44	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (𝑉‘𝐽) ∈ ℝ)
90	85, 88, 89	ltaddsub2d 11921	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (((𝑄‘0) + (𝑘 · 𝑇)) < (𝑉‘𝐽) ↔ (𝑘 · 𝑇) < ((𝑉‘𝐽) − (𝑄‘0))))
91	90	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (((𝑄‘0) + (𝑘 · 𝑇)) < (𝑉‘𝐽) ↔ (𝑘 · 𝑇) < ((𝑉‘𝐽) − (𝑄‘0))))
92	84, 91	mpbird 260	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑄‘0) + (𝑘 · 𝑇)) < (𝑉‘𝐽))
93	77, 78, 92	ltled 11462	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽))
94	93	ex 418	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)))
95	72, 94	sylan2 605	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)))
96	95	reximdva 3175	. . . . . . . . . . . . 13 ⊢ (𝜑 → (∃𝑘 ∈ ℤ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → ∃𝑘 ∈ ℤ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)))
97	71, 96	mpd 16	. . . . . . . . . . . 12 ⊢ (𝜑 → ∃𝑘 ∈ ℤ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽))
98		rabn0 4338	. . . . . . . . . . . 12 ⊢ ({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ↔ ∃𝑘 ∈ ℤ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽))
99	97, 98	sylibr 237	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
100		simpl 488	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝜑)
101	16	sselda 3908	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝑗 ∈ ℤ)
102		oveq1 7428	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑗 → (𝑘 · 𝑇) = (𝑗 · 𝑇))
103	102	oveq2d 7437	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((𝑄‘0) + (𝑘 · 𝑇)) = ((𝑄‘0) + (𝑗 · 𝑇)))
104	103	breq1d 5112	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → (((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)))
105	104	elrab 3644	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ (𝑗 ∈ ℤ ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)))
106	105	simprbi 503	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} → ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽))
107	106	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽))
108		zre 12701	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℤ → 𝑗 ∈ ℝ)
109		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽))
110	56	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝑄‘0) ∈ ℝ)
111		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℝ) → 𝑗 ∈ ℝ)
112	62	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℝ) → 𝑇 ∈ ℝ)
113	111, 112	remulcld 11343	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℝ) → (𝑗 · 𝑇) ∈ ℝ)
114	113	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝑗 · 𝑇) ∈ ℝ)
115	44	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝑉‘𝐽) ∈ ℝ)
116	110, 114, 115	leaddsub2d 11922	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽) ↔ (𝑗 · 𝑇) ≤ ((𝑉‘𝐽) − (𝑄‘0))))
117	109, 116	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝑗 · 𝑇) ≤ ((𝑉‘𝐽) − (𝑄‘0)))
118		simplr 781	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → 𝑗 ∈ ℝ)
119	57	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑉‘𝐽) − (𝑄‘0)) ∈ ℝ)
120	81	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → 𝑇 ∈ ℝ⁺)
121	118, 119, 120	lemuldivd 13217	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑗 · 𝑇) ≤ ((𝑉‘𝐽) − (𝑄‘0)) ↔ 𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)))
122	117, 121	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → 𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
123	108, 122	sylanl2 694	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → 𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
124	100, 101, 107, 123	syl21anc 851	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
125	124	ralrimiva 3154	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
126		breq2 5106	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → (𝑗 ≤ 𝑏 ↔ 𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)))
127	126	ralbidv 3185	. . . . . . . . . . . . 13 ⊢ (𝑏 = (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → (∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏 ↔ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)))
128	127	rspcev 3576	. . . . . . . . . . . 12 ⊢ (((((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∈ ℝ ∧ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏)
129	68, 125, 128	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏)
130		suprzcl 12783	. . . . . . . . . . 11 ⊢ (({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ ∧ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ∧ ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏) → sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)})
131	16, 99, 129, 130	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝜑 → sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)})
132	14, 131	eqeltrid 2864	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)})
133		oveq1 7428	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝐿 → (𝑘 · 𝑇) = (𝐿 · 𝑇))
134	133	oveq2d 7437	. . . . . . . . . . 11 ⊢ (𝑘 = 𝐿 → ((𝑄‘0) + (𝑘 · 𝑇)) = ((𝑄‘0) + (𝐿 · 𝑇)))
135	134	breq1d 5112	. . . . . . . . . 10 ⊢ (𝑘 = 𝐿 → (((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
136	135	elrab 3644	. . . . . . . . 9 ⊢ (𝐿 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ (𝐿 ∈ ℤ ∧ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
137	132, 136	sylib 221	. . . . . . . 8 ⊢ (𝜑 → (𝐿 ∈ ℤ ∧ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
138	137	simprd 501	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
139		fveq2 6886	. . . . . . . . . 10 ⊢ (𝑗 = 0 → (𝑄‘𝑗) = (𝑄‘0))
140	139	oveq1d 7436	. . . . . . . . 9 ⊢ (𝑗 = 0 → ((𝑄‘𝑗) + (𝐿 · 𝑇)) = ((𝑄‘0) + (𝐿 · 𝑇)))
141	140	breq1d 5112	. . . . . . . 8 ⊢ (𝑗 = 0 → (((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
142	141	elrab 3644	. . . . . . 7 ⊢ (0 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ (0 ∈ (0..^𝑀) ∧ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
143	13, 138, 142	sylanbrc 595	. . . . . 6 ⊢ (𝜑 → 0 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
144		ne0i 4286	. . . . . 6 ⊢ (0 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
145	143, 144	syl 18	. . . . 5 ⊢ (𝜑 → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
146	9	nnred 12354	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℝ)
147	2	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ (0..^𝑀))
148	147	sselda 3908	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝑘 ∈ (0..^𝑀))
149		elfzoelz 13797	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0..^𝑀) → 𝑘 ∈ ℤ)
150	149	zred 12807	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0..^𝑀) → 𝑘 ∈ ℝ)
151	150	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑘 ∈ ℝ)
152	146	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑀 ∈ ℝ)
153		elfzolt2 13807	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0..^𝑀) → 𝑘 < 𝑀)
154	153	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑘 < 𝑀)
155	151, 152, 154	ltled 11462	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑘 ≤ 𝑀)
156	148, 155	syldan 603	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝑘 ≤ 𝑀)
157	156	ralrimiva 3154	. . . . . 6 ⊢ (𝜑 → ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑀)
158		breq2 5106	. . . . . . . 8 ⊢ (𝑏 = 𝑀 → (𝑘 ≤ 𝑏 ↔ 𝑘 ≤ 𝑀))
159	158	ralbidv 3185	. . . . . . 7 ⊢ (𝑏 = 𝑀 → (∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏 ↔ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑀))
160	159	rspcev 3576	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑀) → ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏)
161	146, 157, 160	syl2anc 596	. . . . 5 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏)
162		suprzcl 12783	. . . . 5 ⊢ (({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ ∧ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ∧ ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏) → sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
163	7, 145, 161, 162	syl3anc 1398	. . . 4 ⊢ (𝜑 → sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
164	2, 163	sselid 3906	. . 3 ⊢ (𝜑 → sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ (0..^𝑀))
165	1, 164	eqeltrid 2864	. 2 ⊢ (𝜑 → 𝐼 ∈ (0..^𝑀))
166	15, 131	sselid 3906	. . 3 ⊢ (𝜑 → sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ ℤ)
167	14, 166	eqeltrid 2864	. 2 ⊢ (𝜑 → 𝐿 ∈ ℤ)
168	3, 165	sselid 3906	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ (0...𝑀))
169	50, 168	ffvelcdmd 7086	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝐼) ∈ ℝ)
170	167	zred 12807	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ ℝ)
171	170, 62	remulcld 11343	. . . . . . . . 9 ⊢ (𝜑 → (𝐿 · 𝑇) ∈ ℝ)
172	169, 171	readdcld 11342	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ∈ ℝ)
173	172	rexrd 11363	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ∈ ℝ^*)
174	173	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ∈ ℝ^*)
175		fzofzp1 13903	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (0..^𝑀) → (𝐼 + 1) ∈ (0...𝑀))
176	165, 175	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼 + 1) ∈ (0...𝑀))
177	50, 176	ffvelcdmd 7086	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ)
178	177, 171	readdcld 11342	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
179	178	rexrd 11363	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ^*)
180	179	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ^*)
181		elioore 13510	. . . . . . 7 ⊢ (𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) → 𝑥 ∈ ℝ)
182	181	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 ∈ ℝ)
183	172	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ∈ ℝ)
184	44	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘𝐽) ∈ ℝ)
185	1, 163	eqeltrid 2864	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
186		fveq2 6886	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐼 → (𝑄‘𝑗) = (𝑄‘𝐼))
187	186	oveq1d 7436	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝐼 → ((𝑄‘𝑗) + (𝐿 · 𝑇)) = ((𝑄‘𝐼) + (𝐿 · 𝑇)))
188	187	breq1d 5112	. . . . . . . . . . 11 ⊢ (𝑗 = 𝐼 → (((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
189	188	elrab 3644	. . . . . . . . . 10 ⊢ (𝐼 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ (𝐼 ∈ (0..^𝑀) ∧ ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
190	185, 189	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 ∈ (0..^𝑀) ∧ ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
191	190	simprd 501	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
192	191	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
193	184	rexrd 11363	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘𝐽) ∈ ℝ^*)
194		fzofzp1 13903	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
195	40, 194	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
196	39, 195	ffvelcdmd 7086	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ∈ 𝐻)
197	27, 196	sseldd 3909	. . . . . . . . . 10 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ∈ ℝ)
198	197	rexrd 11363	. . . . . . . . 9 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ∈ ℝ^*)
199	198	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘(𝐽 + 1)) ∈ ℝ^*)
200		simpr 490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))))
201		ioogtlb 46601	. . . . . . . 8 ⊢ (((𝑉‘𝐽) ∈ ℝ^* ∧ (𝑉‘(𝐽 + 1)) ∈ ℝ^* ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘𝐽) < 𝑥)
202	193, 199, 200, 201	syl3anc 1398	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘𝐽) < 𝑥)
203	183, 184, 182, 192, 202	lelttrd 11472	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝐼) + (𝐿 · 𝑇)) < 𝑥)
204		zssre 12704	. . . . . . . . . . . . . . . 16 ⊢ ℤ ⊆ ℝ
205	15, 204	sstri 3917	. . . . . . . . . . . . . . 15 ⊢ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ
206	205	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ)
207	99	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
208	129	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏)
209	167	peano2zd 12810	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐿 + 1) ∈ ℤ)
210	209	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐿 + 1) ∈ ℤ)
211		oveq1 7428	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐼 = (𝑀 − 1) → (𝐼 + 1) = ((𝑀 − 1) + 1))
212	146	recnd 11341	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑀 ∈ ℂ)
213		1cnd 11306	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 ∈ ℂ)
214	212, 213	npcand 11677	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
215	211, 214	sylan9eqr 2817	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝐼 + 1) = 𝑀)
216	215	fveq2d 6890	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑄‘(𝐼 + 1)) = (𝑄‘𝑀))
217	47	simprd 501	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
218	217	simpld 500	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
219	218	simprd 501	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
220	219	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑄‘𝑀) = 𝐵)
221	59	recnd 11341	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐵 ∈ ℂ)
222	60	recnd 11341	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐴 ∈ ℂ)
223	221, 222	npcand 11677	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐵 − 𝐴) + 𝐴) = 𝐵)
224	223	eqcomd 2766	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐵 = ((𝐵 − 𝐴) + 𝐴))
225	28	eqcomi 2769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐵 − 𝐴) = 𝑇
226	225	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐵 − 𝐴) = 𝑇)
227	226	oveq1d 7436	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐵 − 𝐴) + 𝐴) = (𝑇 + 𝐴))
228	218	simpld 500	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
229	228	eqcomd 2766	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐴 = (𝑄‘0))
230	229	oveq2d 7437	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑇 + 𝐴) = (𝑇 + (𝑄‘0)))
231	224, 227, 230	3eqtrd 2799	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐵 = (𝑇 + (𝑄‘0)))
232	231	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → 𝐵 = (𝑇 + (𝑄‘0)))
233	216, 220, 232	3eqtrd 2799	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑄‘(𝐼 + 1)) = (𝑇 + (𝑄‘0)))
234	62	recnd 11341	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑇 ∈ ℂ)
235	228, 222	eqeltrd 2860	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑄‘0) ∈ ℂ)
236	234, 235	addcomd 11516	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑇 + (𝑄‘0)) = ((𝑄‘0) + 𝑇))
237	236	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑇 + (𝑄‘0)) = ((𝑄‘0) + 𝑇))
238	233, 237	eqtrd 2795	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑄‘(𝐼 + 1)) = ((𝑄‘0) + 𝑇))
239	238	oveq1d 7436	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (((𝑄‘0) + 𝑇) + (𝐿 · 𝑇)))
240	171	recnd 11341	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 · 𝑇) ∈ ℂ)
241	235, 234, 240	addassd 11335	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝑄‘0) + 𝑇) + (𝐿 · 𝑇)) = ((𝑄‘0) + (𝑇 + (𝐿 · 𝑇))))
242	234	mullidd 11331	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (1 · 𝑇) = 𝑇)
243	242, 234	eqeltrd 2860	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 · 𝑇) ∈ ℂ)
244	243, 240	addcomd 11516	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1 · 𝑇) + (𝐿 · 𝑇)) = ((𝐿 · 𝑇) + (1 · 𝑇)))
245	242	eqcomd 2766	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑇 = (1 · 𝑇))
246	245	oveq1d 7436	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑇 + (𝐿 · 𝑇)) = ((1 · 𝑇) + (𝐿 · 𝑇)))
247	170	recnd 11341	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐿 ∈ ℂ)
248	247, 213, 234	adddird 11338	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝐿 + 1) · 𝑇) = ((𝐿 · 𝑇) + (1 · 𝑇)))
249	244, 246, 248	3eqtr4d 2805	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑇 + (𝐿 · 𝑇)) = ((𝐿 + 1) · 𝑇))
250	249	oveq2d 7437	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑄‘0) + (𝑇 + (𝐿 · 𝑇))) = ((𝑄‘0) + ((𝐿 + 1) · 𝑇)))
251	241, 250	eqtrd 2795	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑄‘0) + 𝑇) + (𝐿 · 𝑇)) = ((𝑄‘0) + ((𝐿 + 1) · 𝑇)))
252	251	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (((𝑄‘0) + 𝑇) + (𝐿 · 𝑇)) = ((𝑄‘0) + ((𝐿 + 1) · 𝑇)))
253	239, 252	eqtr2d 2796	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
254	253	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
255		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
256	254, 255	eqbrtrd 5126	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) ≤ (𝑉‘𝐽))
257		oveq1 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (𝐿 + 1) → (𝑘 · 𝑇) = ((𝐿 + 1) · 𝑇))
258	257	oveq2d 7437	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (𝐿 + 1) → ((𝑄‘0) + (𝑘 · 𝑇)) = ((𝑄‘0) + ((𝐿 + 1) · 𝑇)))
259	258	breq1d 5112	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝐿 + 1) → (((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) ≤ (𝑉‘𝐽)))
260	259	elrab 3644	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 + 1) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ ((𝐿 + 1) ∈ ℤ ∧ ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) ≤ (𝑉‘𝐽)))
261	210, 256, 260	sylanbrc 595	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐿 + 1) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)})
262		suprub 12282	. . . . . . . . . . . . . 14 ⊢ ((({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ ∧ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ∧ ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏) ∧ (𝐿 + 1) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → (𝐿 + 1) ≤ sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ))
263	206, 207, 208, 261, 262	syl31anc 1400	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐿 + 1) ≤ sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ))
264	263, 14	breqtrrdi 5146	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐿 + 1) ≤ 𝐿)
265	170	ltp1d 12251	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 < (𝐿 + 1))
266		peano2re 11487	. . . . . . . . . . . . . . . 16 ⊢ (𝐿 ∈ ℝ → (𝐿 + 1) ∈ ℝ)
267	170, 266	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐿 + 1) ∈ ℝ)
268	170, 267	ltnled 11461	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 < (𝐿 + 1) ↔ ¬ (𝐿 + 1) ≤ 𝐿))
269	265, 268	mpbid 235	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ (𝐿 + 1) ≤ 𝐿)
270	269	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ¬ (𝐿 + 1) ≤ 𝐿)
271	264, 270	pm2.65da 829	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → ¬ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
272	5, 165	sselid 3906	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐼 ∈ ℤ)
273	272	zred 12807	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐼 ∈ ℝ)
274	273	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → 𝐼 ∈ ℝ)
275		peano2rem 11629	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℝ → (𝑀 − 1) ∈ ℝ)
276	146, 275	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 − 1) ∈ ℝ)
277	276	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → (𝑀 − 1) ∈ ℝ)
278		elfzolt2 13807	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 ∈ (0..^𝑀) → 𝐼 < 𝑀)
279		elfzoelz 13797	. . . . . . . . . . . . . . . . 17 ⊢ (𝐼 ∈ (0..^𝑀) → 𝐼 ∈ ℤ)
280		elfzoel2 13796	. . . . . . . . . . . . . . . . 17 ⊢ (𝐼 ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
281		zltlem1 12753	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐼 < 𝑀 ↔ 𝐼 ≤ (𝑀 − 1)))
282	279, 280, 281	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 ∈ (0..^𝑀) → (𝐼 < 𝑀 ↔ 𝐼 ≤ (𝑀 − 1)))
283	278, 282	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (𝐼 ∈ (0..^𝑀) → 𝐼 ≤ (𝑀 − 1))
284	165, 283	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐼 ≤ (𝑀 − 1))
285	284	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → 𝐼 ≤ (𝑀 − 1))
286		neqne 2963	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝐼 = (𝑀 − 1) → 𝐼 ≠ (𝑀 − 1))
287	286	necomd 3010	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐼 = (𝑀 − 1) → (𝑀 − 1) ≠ 𝐼)
288	287	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → (𝑀 − 1) ≠ 𝐼)
289	274, 277, 285, 288	leneltd 11468	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → 𝐼 < (𝑀 − 1))
290	6, 204	sstri 3917	. . . . . . . . . . . . . . . 16 ⊢ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ
291	290	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ)
292	145	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
293	161	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏)
294	176	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝐼 + 1) ∈ (0...𝑀))
295	273	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → 𝐼 ∈ ℝ)
296	276	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝑀 − 1) ∈ ℝ)
297		1red 11313	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → 1 ∈ ℝ)
298		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → 𝐼 < (𝑀 − 1))
299	295, 296, 297, 298	ltadd1dd 11931	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝐼 + 1) < ((𝑀 − 1) + 1))
300	214	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → ((𝑀 − 1) + 1) = 𝑀)
301	299, 300	breqtrd 5130	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝐼 + 1) < 𝑀)
302		elfzfzo 46387	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 + 1) ∈ (0..^𝑀) ↔ ((𝐼 + 1) ∈ (0...𝑀) ∧ (𝐼 + 1) < 𝑀))
303	294, 301, 302	sylanbrc 595	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝐼 + 1) ∈ (0..^𝑀))
304	303	anim1i 627	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝐼 + 1) ∈ (0..^𝑀) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
305		fveq2 6886	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝐼 + 1) → (𝑄‘𝑗) = (𝑄‘(𝐼 + 1)))
306	305	oveq1d 7436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝐼 + 1) → ((𝑄‘𝑗) + (𝐿 · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
307	306	breq1d 5112	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝐼 + 1) → (((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
308	307	elrab 3644	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 + 1) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ ((𝐼 + 1) ∈ (0..^𝑀) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
309	304, 308	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐼 + 1) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
310		suprub 12282	. . . . . . . . . . . . . . 15 ⊢ ((({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ ∧ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ∧ ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏) ∧ (𝐼 + 1) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}) → (𝐼 + 1) ≤ sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ))
311	291, 292, 293, 309, 310	syl31anc 1400	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐼 + 1) ≤ sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ))
312	311, 1	breqtrrdi 5146	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐼 + 1) ≤ 𝐼)
313	273	ltp1d 12251	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐼 < (𝐼 + 1))
314		peano2re 11487	. . . . . . . . . . . . . . . . 17 ⊢ (𝐼 ∈ ℝ → (𝐼 + 1) ∈ ℝ)
315	273, 314	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐼 + 1) ∈ ℝ)
316	273, 315	ltnled 11461	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐼 < (𝐼 + 1) ↔ ¬ (𝐼 + 1) ≤ 𝐼))
317	313, 316	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (𝐼 + 1) ≤ 𝐼)
318	317	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ¬ (𝐼 + 1) ≤ 𝐼)
319	312, 318	pm2.65da 829	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → ¬ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
320	289, 319	syldan 603	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → ¬ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
321	271, 320	pm2.61dan 825	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
322	44, 178	ltnled 11461	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ↔ ¬ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
323	321, 322	mpbird 260	. . . . . . . . 9 ⊢ (𝜑 → (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
324	197	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ∈ ℝ)
325	19	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐷 ∈ ℝ)
326	178	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
327	18	rexrd 11363	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
328	19	rexrd 11363	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷 ∈ ℝ^*)
329	18, 19, 31	ltled 11462	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐶 ≤ 𝐷)
330		lbicc2 13599	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷) → 𝐶 ∈ (𝐶[,]𝐷))
331	327, 328, 329, 330	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐶 ∈ (𝐶[,]𝐷))
332		ubicc2 13600	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷) → 𝐷 ∈ (𝐶[,]𝐷))
333	327, 328, 329, 332	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 ∈ (𝐶[,]𝐷))
334	331, 333	jca 521	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)))
335		prssg 4774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷)))
336	18, 19, 335	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷)))
337	334, 336	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ (𝐶[,]𝐷))
338	337, 23	unssd 4190	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ (𝐶[,]𝐷))
339	17, 338	eqsstrid 3946	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻 ⊆ (𝐶[,]𝐷))
340	339, 196	sseldd 3909	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ∈ (𝐶[,]𝐷))
341		iccleub 13536	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ (𝑉‘(𝐽 + 1)) ∈ (𝐶[,]𝐷)) → (𝑉‘(𝐽 + 1)) ≤ 𝐷)
342	327, 328, 340, 341	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ≤ 𝐷)
343	342	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ 𝐷)
344		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
345	324, 325, 326, 343, 344	letrd 11471	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
346	345	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
347		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
348	178	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
349	19	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐷 ∈ ℝ)
350	348, 349	ltnled 11461	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷 ↔ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
351	347, 350	mpbird 260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷)
352	351	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷)
353		simpll 779	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
354		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
355	178	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
356	197	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ∈ ℝ)
357	355, 356	ltnled 11461	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)) ↔ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
358	354, 357	mpbird 260	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)))
359	358	ad4ant14 765	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)))
360	18	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → 𝐶 ∈ ℝ)
361	19	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → 𝐷 ∈ ℝ)
362	178	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
363	18	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐶 ∈ ℝ)
364	178	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
365	44	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) ∈ ℝ)
366	339, 43	sseldd 3909	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑉‘𝐽) ∈ (𝐶[,]𝐷))
367		iccgelb 13537	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ (𝑉‘𝐽) ∈ (𝐶[,]𝐷)) → 𝐶 ≤ (𝑉‘𝐽))
368	327, 328, 366, 367	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐶 ≤ (𝑉‘𝐽))
369	368	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐶 ≤ (𝑉‘𝐽))
370		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
371	363, 365, 364, 369, 370	lelttrd 11472	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐶 < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
372	363, 364, 371	ltled 11462	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐶 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
373	372	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → 𝐶 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
374	178	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
375	19	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → 𝐷 ∈ ℝ)
376		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷)
377	374, 375, 376	ltled 11462	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ 𝐷)
378	377	adantlr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ 𝐷)
379	360, 361, 362, 373, 378	eliccd 46610	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ (𝐶[,]𝐷))
380	167	znegcld 12809	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → -𝐿 ∈ ℤ)
381	247, 234	mulneg1d 11773	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ( -𝐿 · 𝑇) = -(𝐿 · 𝑇))
382	381	oveq2d 7437	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + ( -𝐿 · 𝑇)) = (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + -(𝐿 · 𝑇)))
383	178	recnd 11341	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℂ)
384	383, 240	negsubd 11679	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + -(𝐿 · 𝑇)) = (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) − (𝐿 · 𝑇)))
385	177	recnd 11341	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℂ)
386	385, 240	pncand 11674	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) − (𝐿 · 𝑇)) = (𝑄‘(𝐼 + 1)))
387	382, 384, 386	3eqtrd 2799	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + ( -𝐿 · 𝑇)) = (𝑄‘(𝐼 + 1)))
388		ffn 6710	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
389	50, 388	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
390		fnfvelrn 7081	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 Fn (0...𝑀) ∧ (𝐼 + 1) ∈ (0...𝑀)) → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
391	389, 176, 390	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
392	387, 391	eqeltrd 2860	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + ( -𝐿 · 𝑇)) ∈ ran 𝑄)
393		oveq1 7428	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = -𝐿 → (𝑘 · 𝑇) = ( -𝐿 · 𝑇))
394	393	oveq2d 7437	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = -𝐿 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) = (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + ( -𝐿 · 𝑇)))
395	394	eleq1d 2845	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = -𝐿 → ((((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + ( -𝐿 · 𝑇)) ∈ ran 𝑄))
396	395	rspcev 3576	. . . . . . . . . . . . . . . . . . 19 ⊢ (( -𝐿 ∈ ℤ ∧ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + ( -𝐿 · 𝑇)) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
397	380, 392, 396	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
398	397	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
399		oveq1 7428	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → (𝑦 + (𝑘 · 𝑇)) = (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)))
400	399	eleq1d 2845	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
401	400	rexbidv 3186	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
402	401	elrab 3644	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} ↔ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
403	379, 398, 402	sylanbrc 595	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
404		elun2 4181	. . . . . . . . . . . . . . . 16 ⊢ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
405	403, 404	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
406	17	eqcomi 2769	. . . . . . . . . . . . . . 15 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = 𝐻
407	405, 406	eleqtrdi 2870	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻)
408	407	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻)
409		f1ofo 6833	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑉:(0...𝑁)–1-1-onto→𝐻 → 𝑉:(0...𝑁)–onto→𝐻)
410	36, 37, 409	3syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑉:(0...𝑁)–onto→𝐻)
411		foelrn 7108	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑉:(0...𝑁)–onto→𝐻 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
412	410, 411	sylan 592	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
413		id 23	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
414	413	eqcomd 2766	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗) → (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
415	414	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗) → (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
416	415	reximdv 3177	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → (∃𝑗 ∈ (0...𝑁)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗) → ∃𝑗 ∈ (0...𝑁)(𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
417	412, 416	mpd 16	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
418	417	ad4ant14 765	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
419		simpl 488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
420	413	eqcoms 2768	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
421	420	adantl 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
422	419, 421	breqtrd 5130	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) < (𝑉‘𝑗))
423	422	adantll 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) < (𝑉‘𝑗))
424	423	adantlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) < (𝑉‘𝑗))
425	36	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑉 Isom < , < ((0...𝑁), 𝐻))
426	42	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐽 ∈ (0...𝑁))
427		simplr 781	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑗 ∈ (0...𝑁))
428		isorel 7335	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑉 Isom < , < ((0...𝑁), 𝐻) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) → (𝐽 < 𝑗 ↔ (𝑉‘𝐽) < (𝑉‘𝑗)))
429	425, 426, 427, 428	syl12anc 850	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝐽 < 𝑗 ↔ (𝑉‘𝐽) < (𝑉‘𝑗)))
430	424, 429	mpbird 260	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐽 < 𝑗)
431	430	adantllr 732	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐽 < 𝑗)
432		simpr 490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
433		simpl 488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)))
434	432, 433	eqbrtrd 5126	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝑗) < (𝑉‘(𝐽 + 1)))
435	434	adantll 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝑗) < (𝑉‘(𝐽 + 1)))
436	435	adantlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝑗) < (𝑉‘(𝐽 + 1)))
437	36	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑉 Isom < , < ((0...𝑁), 𝐻))
438		simplr 781	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑗 ∈ (0...𝑁))
439	195	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝐽 + 1) ∈ (0...𝑁))
440		isorel 7335	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑉 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝑗 < (𝐽 + 1) ↔ (𝑉‘𝑗) < (𝑉‘(𝐽 + 1))))
441	437, 438, 439, 440	syl12anc 850	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑗 < (𝐽 + 1) ↔ (𝑉‘𝑗) < (𝑉‘(𝐽 + 1))))
442	436, 441	mpbird 260	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑗 < (𝐽 + 1))
443	442	adantl3r 763	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑗 < (𝐽 + 1))
444	431, 443	jca 521	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
445	444	ex 418	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))))
446	445	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))))
447	446	reximdva 3175	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → (∃𝑗 ∈ (0...𝑁)(𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))))
448	418, 447	mpd 16	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
449	353, 359, 408, 448	syl21anc 851	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
450		elfzelz 13660	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
451	450	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝑗 ∈ ℤ)
452		elfzelz 13660	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 ∈ (0...𝑁) → 𝐽 ∈ ℤ)
453	42, 452	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐽 ∈ ℤ)
454	453	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝐽 ∈ ℤ)
455		simprl 783	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝐽 < 𝑗)
456		simprr 785	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝑗 < (𝐽 + 1))
457		btwnnz 12779	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ)
458	454, 455, 456, 457	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → ¬ 𝑗 ∈ ℤ)
459	451, 458	pm2.65da 829	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ¬ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
460	459	nrexdv 3157	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
461	460	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ¬ ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
462	449, 461	condan 830	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
463	352, 462	syldan 603	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
464	346, 463	pm2.61dan 825	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
465	323, 464	mpdan 700	. . . . . . . 8 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
466	465	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
467	182	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑥 ∈ ℝ)
468	197	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ∈ ℝ)
469	178	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
470		iooltub 46616	. . . . . . . . . 10 ⊢ (((𝑉‘𝐽) ∈ ℝ^* ∧ (𝑉‘(𝐽 + 1)) ∈ ℝ^* ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 < (𝑉‘(𝐽 + 1)))
471	193, 199, 200, 470	syl3anc 1398	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 < (𝑉‘(𝐽 + 1)))
472	471	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑥 < (𝑉‘(𝐽 + 1)))
473		simpr 490	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
474	467, 468, 469, 472, 473	ltletrd 11474	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑥 < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
475	466, 474	mpdan 700	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
476	174, 180, 182, 203, 475	eliood 46604	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 ∈ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
477	476	ralrimiva 3154	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))𝑥 ∈ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
478		dfss3 3897	. . . 4 ⊢ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ↔ ∀𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))𝑥 ∈ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
479	477, 478	sylibr 237	. . 3 ⊢ (𝜑 → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
480		fveq2 6886	. . . . . . 7 ⊢ (𝑖 = 𝐼 → (𝑄‘𝑖) = (𝑄‘𝐼))
481	480	oveq1d 7436	. . . . . 6 ⊢ (𝑖 = 𝐼 → ((𝑄‘𝑖) + (𝑙 · 𝑇)) = ((𝑄‘𝐼) + (𝑙 · 𝑇)))
482		oveq1 7428	. . . . . . . 8 ⊢ (𝑖 = 𝐼 → (𝑖 + 1) = (𝐼 + 1))
483	482	fveq2d 6890	. . . . . . 7 ⊢ (𝑖 = 𝐼 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝐼 + 1)))
484	483	oveq1d 7436	. . . . . 6 ⊢ (𝑖 = 𝐼 → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇)))
485	481, 484	oveq12d 7439	. . . . 5 ⊢ (𝑖 = 𝐼 → (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) = (((𝑄‘𝐼) + (𝑙 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇))))
486	485	sseq2d 3940	. . . 4 ⊢ (𝑖 = 𝐼 → (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) ↔ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝑙 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇)))))
487		oveq1 7428	. . . . . . 7 ⊢ (𝑙 = 𝐿 → (𝑙 · 𝑇) = (𝐿 · 𝑇))
488	487	oveq2d 7437	. . . . . 6 ⊢ (𝑙 = 𝐿 → ((𝑄‘𝐼) + (𝑙 · 𝑇)) = ((𝑄‘𝐼) + (𝐿 · 𝑇)))
489	487	oveq2d 7437	. . . . . 6 ⊢ (𝑙 = 𝐿 → ((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
490	488, 489	oveq12d 7439	. . . . 5 ⊢ (𝑙 = 𝐿 → (((𝑄‘𝐼) + (𝑙 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇))) = (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
491	490	sseq2d 3940	. . . 4 ⊢ (𝑙 = 𝐿 → (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝑙 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇))) ↔ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))))
492	486, 491	rspc2ev 3588	. . 3 ⊢ ((𝐼 ∈ (0..^𝑀) ∧ 𝐿 ∈ ℤ ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))) → ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
493	165, 167, 479, 492	syl3anc 1398	. 2 ⊢ (𝜑 → ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
494	165, 167, 493	jca31 524	1 ⊢ (𝜑 → ((𝐼 ∈ (0..^𝑀) ∧ 𝐿 ∈ ℤ) ∧ ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 {crab 3412 ⊆ wss 3895 ∪ cun 4149 ∅c0 4278 {cpr 4586 class class class wbr 5102 ↦ cmpt 5185 ran crn 5651 ℩cio 6492 Fn wfn 6534 ⟶wf 6535 –onto→wfo 6537 –1-1-onto→wf1o 6538 ‘cfv 6539 Isom wiso 6540 (class class class)co 7421 ↑_m cmap 8851 supcsup 9436 ℂcc 11202 ℝcr 11203 0cc0 11204 1c1 11205 + caddc 11207 · cmul 11209 ℝ^*cxr 11346 < clt 11347 ≤ cle 11348 − cmin 11545 -cneg 11546 / cdiv 11977 ℕcn 12339 ℕ₀cn0 12610 ℤcz 12697 ℤ_≥cuz 12969 ℝ⁺crp 13124 (,)cioo 13480 [,]cicc 13483 ...cfz 13643 ..^cfzo 13792 ♯chash 14478

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-inf2 9646 ax-cnex 11260 ax-resscn 11261 ax-1cn 11262 ax-icn 11263 ax-addcl 11264 ax-addrcl 11265 ax-mulcl 11266 ax-mulrcl 11267 ax-mulcom 11268 ax-addass 11269 ax-mulass 11270 ax-distr 11271 ax-i2m1 11272 ax-1ne0 11273 ax-1rid 11274 ax-rnegex 11275 ax-rrecex 11276 ax-cnre 11277 ax-pre-lttri 11278 ax-pre-lttrn 11279 ax-pre-ltadd 11280 ax-pre-mulgt0 11281 ax-pre-sup 11282

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-isom 6548 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-om 7879 df-1st 8002 df-2nd 8003 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-1o 8480 df-2o 8481 df-oadd 8484 df-er 8721 df-map 8853 df-en 8978 df-dom 8979 df-sdom 8980 df-fin 8981 df-fi 9407 df-sup 9438 df-inf 9439 df-oi 9508 df-dju 9986 df-card 10024 df-pnf 11349 df-mnf 11350 df-xr 11351 df-ltxr 11352 df-le 11353 df-sub 11547 df-neg 11548 df-div 11978 df-nn 12340 df-2 12409 df-3 12410 df-n0 12611 df-xnn0 12684 df-z 12698 df-uz 12970 df-q 13080 df-rp 13125 df-xneg 13245 df-xadd 13246 df-xmul 13247 df-ioo 13484 df-icc 13487 df-fz 13644 df-fzo 13793 df-seq 14149 df-exp 14209 df-hash 14479 df-cj 15272 df-re 15273 df-im 15274 df-sqrt 15408 df-abs 15409 df-rest 17599 df-topgen 17620 df-psmet 21676 df-xmet 21677 df-met 21678 df-bl 21679 df-mopn 21680 df-top 23218 df-topon 23235 df-bases 23270 df-cld 23343 df-ntr 23344 df-cls 23345 df-nei 23422 df-lp 23460 df-cmp 23711

This theorem is used by: fourierdlem97 47307

W3C validator