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 44401

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 4037	. . . 4 ⊢ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ (0..^𝑀)
3		fzossfz 13591	. . . . . . . 8 ⊢ (0..^𝑀) ⊆ (0...𝑀)
4		fzssz 13443	. . . . . . . 8 ⊢ (0...𝑀) ⊆ ℤ
5	3, 4	sstri 3953	. . . . . . 7 ⊢ (0..^𝑀) ⊆ ℤ
6	2, 5	sstri 3953	. . . . . 6 ⊢ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ
7	6	a1i 11	. . . . 5 ⊢ (𝜑 → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ)
8		0zd 12511	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℤ)
9		fourierdlem64.m	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
10	9	nnzd 12526	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
11	9	nngt0d 12202	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝑀)
12		fzolb 13578	. . . . . . . 8 ⊢ (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
13	8, 10, 11, 12	syl3anbrc 1343	. . . . . . 7 ⊢ (𝜑 → 0 ∈ (0..^𝑀))
14		fourierdlem64.l	. . . . . . . . . 10 ⊢ 𝐿 = sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < )
15		ssrab2 4037	. . . . . . . . . . . 12 ⊢ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ
16	15	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ)
17		fourierdlem64.h	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
18		fourierdlem64.c	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐶 ∈ ℝ)
19		fourierdlem64.d	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 ∈ ℝ)
20		prssi 4781	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → {𝐶, 𝐷} ⊆ ℝ)
21	18, 19, 20	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ ℝ)
22		ssrab2 4037	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷)
23	22	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷))
24	18, 19	iccssred 13351	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐶[,]𝐷) ⊆ ℝ)
25	23, 24	sstrd 3954	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ ℝ)
26	21, 25	unssd 4146	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ ℝ)
27	17, 26	eqsstrid 3992	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ⊆ ℝ)
28		fourierdlem64.t	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑇 = (𝐵 − 𝐴)
29		fourierdlem64.p	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
30		fourierdlem64.q	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
31		fourierdlem64.cltd	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐶 < 𝐷)
32		eqid 2736	. . . . . . . . . . . . . . . . . . . . . 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 44391	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑉 ∈ ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑁)) ∧ 𝑉 Isom < , < ((0...𝑁), 𝐻)))
36	35	simprd 496	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑉 Isom < , < ((0...𝑁), 𝐻))
37		isof1o 7268	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑉 Isom < , < ((0...𝑁), 𝐻) → 𝑉:(0...𝑁)–1-1-onto→𝐻)
38		f1of 6784	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑉:(0...𝑁)–1-1-onto→𝐻 → 𝑉:(0...𝑁)⟶𝐻)
39	36, 37, 38	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑉:(0...𝑁)⟶𝐻)
40		fourierdlem64.j	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
41		elfzofz 13588	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
42	40, 41	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐽 ∈ (0...𝑁))
43	39, 42	ffvelcdmd 7036	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑉‘𝐽) ∈ 𝐻)
44	27, 43	sseldd 3945	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑉‘𝐽) ∈ ℝ)
45	29	fourierdlem2 44340	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
46	9, 45	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
47	30, 46	mpbid 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
48	47	simpld 495	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
49		elmapi 8787	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
50	48, 49	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
51	9	nnnn0d 12473	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
52		nn0uz 12805	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ₀ = (ℤ_≥‘0)
53	51, 52	eleqtrdi 2848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
54		eluzfz1 13448	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 ∈ (0...𝑀))
56	50, 55	ffvelcdmd 7036	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
57	44, 56	resubcld 11583	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑉‘𝐽) − (𝑄‘0)) ∈ ℝ)
58	29, 9, 30	fourierdlem11 44349	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
59	58	simp2d 1143	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ)
60	58	simp1d 1142	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℝ)
61	59, 60	resubcld 11583	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
62	28, 61	eqeltrid 2842	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ∈ ℝ)
63	58	simp3d 1144	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 < 𝐵)
64	60, 59	posdifd 11742	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
65	63, 64	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
66	65, 28	breqtrrdi 5147	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝑇)
67	66	gt0ne0d 11719	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ≠ 0)
68	57, 62, 67	redivcld 11983	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∈ ℝ)
69		btwnz 12606	. . . . . . . . . . . . . . 15 ⊢ ((((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∈ ℝ → (∃𝑘 ∈ ℤ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∧ ∃𝑧 ∈ ℤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) < 𝑧))
70	68, 69	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑘 ∈ ℤ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∧ ∃𝑧 ∈ ℤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) < 𝑧))
71	70	simpld 495	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∃𝑘 ∈ ℤ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
72		zre 12503	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℝ)
73	56	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (𝑄‘0) ∈ ℝ)
74		simplr 767	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → 𝑘 ∈ ℝ)
75	62	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → 𝑇 ∈ ℝ)
76	74, 75	remulcld 11185	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (𝑘 · 𝑇) ∈ ℝ)
77	73, 76	readdcld 11184	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑄‘0) + (𝑘 · 𝑇)) ∈ ℝ)
78	44	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (𝑉‘𝐽) ∈ ℝ)
79		simpr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
80	57	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑉‘𝐽) − (𝑄‘0)) ∈ ℝ)
81	62, 66	elrpd 12954	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑇 ∈ ℝ⁺)
82	81	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → 𝑇 ∈ ℝ⁺)
83	74, 80, 82	ltmuldivd 13004	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑘 · 𝑇) < ((𝑉‘𝐽) − (𝑄‘0)) ↔ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)))
84	79, 83	mpbird 256	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (𝑘 · 𝑇) < ((𝑉‘𝐽) − (𝑄‘0)))
85	56	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (𝑄‘0) ∈ ℝ)
86		simpr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → 𝑘 ∈ ℝ)
87	62	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → 𝑇 ∈ ℝ)
88	86, 87	remulcld 11185	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (𝑘 · 𝑇) ∈ ℝ)
89	44	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (𝑉‘𝐽) ∈ ℝ)
90	85, 88, 89	ltaddsub2d 11756	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (((𝑄‘0) + (𝑘 · 𝑇)) < (𝑉‘𝐽) ↔ (𝑘 · 𝑇) < ((𝑉‘𝐽) − (𝑄‘0))))
91	90	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (((𝑄‘0) + (𝑘 · 𝑇)) < (𝑉‘𝐽) ↔ (𝑘 · 𝑇) < ((𝑉‘𝐽) − (𝑄‘0))))
92	84, 91	mpbird 256	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑄‘0) + (𝑘 · 𝑇)) < (𝑉‘𝐽))
93	77, 78, 92	ltled 11303	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽))
94	93	ex 413	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)))
95	72, 94	sylan2 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)))
96	95	reximdva 3165	. . . . . . . . . . . . 13 ⊢ (𝜑 → (∃𝑘 ∈ ℤ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → ∃𝑘 ∈ ℤ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)))
97	71, 96	mpd 15	. . . . . . . . . . . 12 ⊢ (𝜑 → ∃𝑘 ∈ ℤ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽))
98		rabn0 4345	. . . . . . . . . . . 12 ⊢ ({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ↔ ∃𝑘 ∈ ℤ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽))
99	97, 98	sylibr 233	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
100		simpl 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝜑)
101	16	sselda 3944	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝑗 ∈ ℤ)
102		oveq1 7364	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑗 → (𝑘 · 𝑇) = (𝑗 · 𝑇))
103	102	oveq2d 7373	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((𝑄‘0) + (𝑘 · 𝑇)) = ((𝑄‘0) + (𝑗 · 𝑇)))
104	103	breq1d 5115	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → (((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)))
105	104	elrab 3645	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ (𝑗 ∈ ℤ ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)))
106	105	simprbi 497	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} → ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽))
107	106	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽))
108		zre 12503	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℤ → 𝑗 ∈ ℝ)
109		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽))
110	56	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝑄‘0) ∈ ℝ)
111		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℝ) → 𝑗 ∈ ℝ)
112	62	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℝ) → 𝑇 ∈ ℝ)
113	111, 112	remulcld 11185	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℝ) → (𝑗 · 𝑇) ∈ ℝ)
114	113	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝑗 · 𝑇) ∈ ℝ)
115	44	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝑉‘𝐽) ∈ ℝ)
116	110, 114, 115	leaddsub2d 11757	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽) ↔ (𝑗 · 𝑇) ≤ ((𝑉‘𝐽) − (𝑄‘0))))
117	109, 116	mpbid 231	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝑗 · 𝑇) ≤ ((𝑉‘𝐽) − (𝑄‘0)))
118		simplr 767	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → 𝑗 ∈ ℝ)
119	57	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑉‘𝐽) − (𝑄‘0)) ∈ ℝ)
120	81	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → 𝑇 ∈ ℝ⁺)
121	118, 119, 120	lemuldivd 13006	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑗 · 𝑇) ≤ ((𝑉‘𝐽) − (𝑄‘0)) ↔ 𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)))
122	117, 121	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → 𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
123	108, 122	sylanl2 679	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → 𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
124	100, 101, 107, 123	syl21anc 836	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
125	124	ralrimiva 3143	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
126		breq2 5109	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → (𝑗 ≤ 𝑏 ↔ 𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)))
127	126	ralbidv 3174	. . . . . . . . . . . . 13 ⊢ (𝑏 = (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → (∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏 ↔ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)))
128	127	rspcev 3581	. . . . . . . . . . . 12 ⊢ (((((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∈ ℝ ∧ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏)
129	68, 125, 128	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏)
130		suprzcl 12583	. . . . . . . . . . 11 ⊢ (({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ ∧ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ∧ ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏) → sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)})
131	16, 99, 129, 130	syl3anc 1371	. . . . . . . . . 10 ⊢ (𝜑 → sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)})
132	14, 131	eqeltrid 2842	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)})
133		oveq1 7364	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝐿 → (𝑘 · 𝑇) = (𝐿 · 𝑇))
134	133	oveq2d 7373	. . . . . . . . . . 11 ⊢ (𝑘 = 𝐿 → ((𝑄‘0) + (𝑘 · 𝑇)) = ((𝑄‘0) + (𝐿 · 𝑇)))
135	134	breq1d 5115	. . . . . . . . . 10 ⊢ (𝑘 = 𝐿 → (((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
136	135	elrab 3645	. . . . . . . . 9 ⊢ (𝐿 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ (𝐿 ∈ ℤ ∧ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
137	132, 136	sylib 217	. . . . . . . 8 ⊢ (𝜑 → (𝐿 ∈ ℤ ∧ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
138	137	simprd 496	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
139		fveq2 6842	. . . . . . . . . 10 ⊢ (𝑗 = 0 → (𝑄‘𝑗) = (𝑄‘0))
140	139	oveq1d 7372	. . . . . . . . 9 ⊢ (𝑗 = 0 → ((𝑄‘𝑗) + (𝐿 · 𝑇)) = ((𝑄‘0) + (𝐿 · 𝑇)))
141	140	breq1d 5115	. . . . . . . 8 ⊢ (𝑗 = 0 → (((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
142	141	elrab 3645	. . . . . . 7 ⊢ (0 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ (0 ∈ (0..^𝑀) ∧ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
143	13, 138, 142	sylanbrc 583	. . . . . 6 ⊢ (𝜑 → 0 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
144		ne0i 4294	. . . . . 6 ⊢ (0 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
145	143, 144	syl 17	. . . . 5 ⊢ (𝜑 → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
146	9	nnred 12168	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℝ)
147	2	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ (0..^𝑀))
148	147	sselda 3944	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝑘 ∈ (0..^𝑀))
149		elfzoelz 13572	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0..^𝑀) → 𝑘 ∈ ℤ)
150	149	zred 12607	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0..^𝑀) → 𝑘 ∈ ℝ)
151	150	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑘 ∈ ℝ)
152	146	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑀 ∈ ℝ)
153		elfzolt2 13581	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0..^𝑀) → 𝑘 < 𝑀)
154	153	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑘 < 𝑀)
155	151, 152, 154	ltled 11303	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑘 ≤ 𝑀)
156	148, 155	syldan 591	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝑘 ≤ 𝑀)
157	156	ralrimiva 3143	. . . . . 6 ⊢ (𝜑 → ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑀)
158		breq2 5109	. . . . . . . 8 ⊢ (𝑏 = 𝑀 → (𝑘 ≤ 𝑏 ↔ 𝑘 ≤ 𝑀))
159	158	ralbidv 3174	. . . . . . 7 ⊢ (𝑏 = 𝑀 → (∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏 ↔ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑀))
160	159	rspcev 3581	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑀) → ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏)
161	146, 157, 160	syl2anc 584	. . . . 5 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏)
162		suprzcl 12583	. . . . 5 ⊢ (({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ ∧ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ∧ ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏) → sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
163	7, 145, 161, 162	syl3anc 1371	. . . 4 ⊢ (𝜑 → sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
164	2, 163	sselid 3942	. . 3 ⊢ (𝜑 → sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ (0..^𝑀))
165	1, 164	eqeltrid 2842	. 2 ⊢ (𝜑 → 𝐼 ∈ (0..^𝑀))
166	15, 131	sselid 3942	. . 3 ⊢ (𝜑 → sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ ℤ)
167	14, 166	eqeltrid 2842	. 2 ⊢ (𝜑 → 𝐿 ∈ ℤ)
168	3, 165	sselid 3942	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ (0...𝑀))
169	50, 168	ffvelcdmd 7036	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝐼) ∈ ℝ)
170	167	zred 12607	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ ℝ)
171	170, 62	remulcld 11185	. . . . . . . . 9 ⊢ (𝜑 → (𝐿 · 𝑇) ∈ ℝ)
172	169, 171	readdcld 11184	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ∈ ℝ)
173	172	rexrd 11205	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ∈ ℝ^*)
174	173	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ∈ ℝ^*)
175		fzofzp1 13669	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (0..^𝑀) → (𝐼 + 1) ∈ (0...𝑀))
176	165, 175	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼 + 1) ∈ (0...𝑀))
177	50, 176	ffvelcdmd 7036	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ)
178	177, 171	readdcld 11184	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
179	178	rexrd 11205	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ^*)
180	179	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ^*)
181		elioore 13294	. . . . . . 7 ⊢ (𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) → 𝑥 ∈ ℝ)
182	181	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 ∈ ℝ)
183	172	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ∈ ℝ)
184	44	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘𝐽) ∈ ℝ)
185	1, 163	eqeltrid 2842	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
186		fveq2 6842	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐼 → (𝑄‘𝑗) = (𝑄‘𝐼))
187	186	oveq1d 7372	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝐼 → ((𝑄‘𝑗) + (𝐿 · 𝑇)) = ((𝑄‘𝐼) + (𝐿 · 𝑇)))
188	187	breq1d 5115	. . . . . . . . . . 11 ⊢ (𝑗 = 𝐼 → (((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
189	188	elrab 3645	. . . . . . . . . 10 ⊢ (𝐼 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ (𝐼 ∈ (0..^𝑀) ∧ ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
190	185, 189	sylib 217	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 ∈ (0..^𝑀) ∧ ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
191	190	simprd 496	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
192	191	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
193	184	rexrd 11205	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘𝐽) ∈ ℝ^*)
194		fzofzp1 13669	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
195	40, 194	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
196	39, 195	ffvelcdmd 7036	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ∈ 𝐻)
197	27, 196	sseldd 3945	. . . . . . . . . 10 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ∈ ℝ)
198	197	rexrd 11205	. . . . . . . . 9 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ∈ ℝ^*)
199	198	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘(𝐽 + 1)) ∈ ℝ^*)
200		simpr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))))
201		ioogtlb 43723	. . . . . . . 8 ⊢ (((𝑉‘𝐽) ∈ ℝ^* ∧ (𝑉‘(𝐽 + 1)) ∈ ℝ^* ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘𝐽) < 𝑥)
202	193, 199, 200, 201	syl3anc 1371	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘𝐽) < 𝑥)
203	183, 184, 182, 192, 202	lelttrd 11313	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝐼) + (𝐿 · 𝑇)) < 𝑥)
204		zssre 12506	. . . . . . . . . . . . . . . 16 ⊢ ℤ ⊆ ℝ
205	15, 204	sstri 3953	. . . . . . . . . . . . . . 15 ⊢ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ
206	205	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ)
207	99	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
208	129	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏)
209	167	peano2zd 12610	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐿 + 1) ∈ ℤ)
210	209	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐿 + 1) ∈ ℤ)
211		oveq1 7364	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐼 = (𝑀 − 1) → (𝐼 + 1) = ((𝑀 − 1) + 1))
212	146	recnd 11183	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑀 ∈ ℂ)
213		1cnd 11150	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 ∈ ℂ)
214	212, 213	npcand 11516	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
215	211, 214	sylan9eqr 2798	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝐼 + 1) = 𝑀)
216	215	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑄‘(𝐼 + 1)) = (𝑄‘𝑀))
217	47	simprd 496	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
218	217	simpld 495	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
219	218	simprd 496	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
220	219	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑄‘𝑀) = 𝐵)
221	59	recnd 11183	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐵 ∈ ℂ)
222	60	recnd 11183	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐴 ∈ ℂ)
223	221, 222	npcand 11516	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐵 − 𝐴) + 𝐴) = 𝐵)
224	223	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐵 = ((𝐵 − 𝐴) + 𝐴))
225	28	eqcomi 2745	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐵 − 𝐴) = 𝑇
226	225	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐵 − 𝐴) = 𝑇)
227	226	oveq1d 7372	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐵 − 𝐴) + 𝐴) = (𝑇 + 𝐴))
228	218	simpld 495	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
229	228	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐴 = (𝑄‘0))
230	229	oveq2d 7373	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑇 + 𝐴) = (𝑇 + (𝑄‘0)))
231	224, 227, 230	3eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐵 = (𝑇 + (𝑄‘0)))
232	231	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → 𝐵 = (𝑇 + (𝑄‘0)))
233	216, 220, 232	3eqtrd 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑄‘(𝐼 + 1)) = (𝑇 + (𝑄‘0)))
234	62	recnd 11183	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑇 ∈ ℂ)
235	228, 222	eqeltrd 2838	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑄‘0) ∈ ℂ)
236	234, 235	addcomd 11357	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑇 + (𝑄‘0)) = ((𝑄‘0) + 𝑇))
237	236	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑇 + (𝑄‘0)) = ((𝑄‘0) + 𝑇))
238	233, 237	eqtrd 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑄‘(𝐼 + 1)) = ((𝑄‘0) + 𝑇))
239	238	oveq1d 7372	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (((𝑄‘0) + 𝑇) + (𝐿 · 𝑇)))
240	171	recnd 11183	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 · 𝑇) ∈ ℂ)
241	235, 234, 240	addassd 11177	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝑄‘0) + 𝑇) + (𝐿 · 𝑇)) = ((𝑄‘0) + (𝑇 + (𝐿 · 𝑇))))
242	234	mulid2d 11173	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (1 · 𝑇) = 𝑇)
243	242, 234	eqeltrd 2838	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 · 𝑇) ∈ ℂ)
244	243, 240	addcomd 11357	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1 · 𝑇) + (𝐿 · 𝑇)) = ((𝐿 · 𝑇) + (1 · 𝑇)))
245	242	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑇 = (1 · 𝑇))
246	245	oveq1d 7372	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑇 + (𝐿 · 𝑇)) = ((1 · 𝑇) + (𝐿 · 𝑇)))
247	170	recnd 11183	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐿 ∈ ℂ)
248	247, 213, 234	adddird 11180	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝐿 + 1) · 𝑇) = ((𝐿 · 𝑇) + (1 · 𝑇)))
249	244, 246, 248	3eqtr4d 2786	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑇 + (𝐿 · 𝑇)) = ((𝐿 + 1) · 𝑇))
250	249	oveq2d 7373	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑄‘0) + (𝑇 + (𝐿 · 𝑇))) = ((𝑄‘0) + ((𝐿 + 1) · 𝑇)))
251	241, 250	eqtrd 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑄‘0) + 𝑇) + (𝐿 · 𝑇)) = ((𝑄‘0) + ((𝐿 + 1) · 𝑇)))
252	251	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (((𝑄‘0) + 𝑇) + (𝐿 · 𝑇)) = ((𝑄‘0) + ((𝐿 + 1) · 𝑇)))
253	239, 252	eqtr2d 2777	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
254	253	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
255		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
256	254, 255	eqbrtrd 5127	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) ≤ (𝑉‘𝐽))
257		oveq1 7364	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (𝐿 + 1) → (𝑘 · 𝑇) = ((𝐿 + 1) · 𝑇))
258	257	oveq2d 7373	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (𝐿 + 1) → ((𝑄‘0) + (𝑘 · 𝑇)) = ((𝑄‘0) + ((𝐿 + 1) · 𝑇)))
259	258	breq1d 5115	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝐿 + 1) → (((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) ≤ (𝑉‘𝐽)))
260	259	elrab 3645	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 + 1) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ ((𝐿 + 1) ∈ ℤ ∧ ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) ≤ (𝑉‘𝐽)))
261	210, 256, 260	sylanbrc 583	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐿 + 1) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)})
262		suprub 12116	. . . . . . . . . . . . . 14 ⊢ ((({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ ∧ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ∧ ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏) ∧ (𝐿 + 1) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → (𝐿 + 1) ≤ sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ))
263	206, 207, 208, 261, 262	syl31anc 1373	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐿 + 1) ≤ sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ))
264	263, 14	breqtrrdi 5147	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐿 + 1) ≤ 𝐿)
265	170	ltp1d 12085	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 < (𝐿 + 1))
266		peano2re 11328	. . . . . . . . . . . . . . . 16 ⊢ (𝐿 ∈ ℝ → (𝐿 + 1) ∈ ℝ)
267	170, 266	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐿 + 1) ∈ ℝ)
268	170, 267	ltnled 11302	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 < (𝐿 + 1) ↔ ¬ (𝐿 + 1) ≤ 𝐿))
269	265, 268	mpbid 231	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ (𝐿 + 1) ≤ 𝐿)
270	269	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ¬ (𝐿 + 1) ≤ 𝐿)
271	264, 270	pm2.65da 815	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → ¬ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
272	5, 165	sselid 3942	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐼 ∈ ℤ)
273	272	zred 12607	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐼 ∈ ℝ)
274	273	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → 𝐼 ∈ ℝ)
275		peano2rem 11468	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℝ → (𝑀 − 1) ∈ ℝ)
276	146, 275	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 − 1) ∈ ℝ)
277	276	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → (𝑀 − 1) ∈ ℝ)
278		elfzolt2 13581	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 ∈ (0..^𝑀) → 𝐼 < 𝑀)
279		elfzoelz 13572	. . . . . . . . . . . . . . . . 17 ⊢ (𝐼 ∈ (0..^𝑀) → 𝐼 ∈ ℤ)
280		elfzoel2 13571	. . . . . . . . . . . . . . . . 17 ⊢ (𝐼 ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
281		zltlem1 12556	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐼 < 𝑀 ↔ 𝐼 ≤ (𝑀 − 1)))
282	279, 280, 281	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 ∈ (0..^𝑀) → (𝐼 < 𝑀 ↔ 𝐼 ≤ (𝑀 − 1)))
283	278, 282	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (𝐼 ∈ (0..^𝑀) → 𝐼 ≤ (𝑀 − 1))
284	165, 283	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐼 ≤ (𝑀 − 1))
285	284	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → 𝐼 ≤ (𝑀 − 1))
286		neqne 2951	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝐼 = (𝑀 − 1) → 𝐼 ≠ (𝑀 − 1))
287	286	necomd 2999	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐼 = (𝑀 − 1) → (𝑀 − 1) ≠ 𝐼)
288	287	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → (𝑀 − 1) ≠ 𝐼)
289	274, 277, 285, 288	leneltd 11309	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → 𝐼 < (𝑀 − 1))
290	6, 204	sstri 3953	. . . . . . . . . . . . . . . 16 ⊢ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ
291	290	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ)
292	145	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
293	161	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏)
294	176	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝐼 + 1) ∈ (0...𝑀))
295	273	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → 𝐼 ∈ ℝ)
296	276	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝑀 − 1) ∈ ℝ)
297		1red 11156	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → 1 ∈ ℝ)
298		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → 𝐼 < (𝑀 − 1))
299	295, 296, 297, 298	ltadd1dd 11766	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝐼 + 1) < ((𝑀 − 1) + 1))
300	214	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → ((𝑀 − 1) + 1) = 𝑀)
301	299, 300	breqtrd 5131	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝐼 + 1) < 𝑀)
302		elfzfzo 43500	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 + 1) ∈ (0..^𝑀) ↔ ((𝐼 + 1) ∈ (0...𝑀) ∧ (𝐼 + 1) < 𝑀))
303	294, 301, 302	sylanbrc 583	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝐼 + 1) ∈ (0..^𝑀))
304	303	anim1i 615	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝐼 + 1) ∈ (0..^𝑀) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
305		fveq2 6842	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝐼 + 1) → (𝑄‘𝑗) = (𝑄‘(𝐼 + 1)))
306	305	oveq1d 7372	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝐼 + 1) → ((𝑄‘𝑗) + (𝐿 · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
307	306	breq1d 5115	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝐼 + 1) → (((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
308	307	elrab 3645	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 + 1) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ ((𝐼 + 1) ∈ (0..^𝑀) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
309	304, 308	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐼 + 1) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
310		suprub 12116	. . . . . . . . . . . . . . 15 ⊢ ((({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ ∧ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ∧ ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏) ∧ (𝐼 + 1) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}) → (𝐼 + 1) ≤ sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ))
311	291, 292, 293, 309, 310	syl31anc 1373	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐼 + 1) ≤ sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ))
312	311, 1	breqtrrdi 5147	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐼 + 1) ≤ 𝐼)
313	273	ltp1d 12085	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐼 < (𝐼 + 1))
314		peano2re 11328	. . . . . . . . . . . . . . . . 17 ⊢ (𝐼 ∈ ℝ → (𝐼 + 1) ∈ ℝ)
315	273, 314	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐼 + 1) ∈ ℝ)
316	273, 315	ltnled 11302	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐼 < (𝐼 + 1) ↔ ¬ (𝐼 + 1) ≤ 𝐼))
317	313, 316	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (𝐼 + 1) ≤ 𝐼)
318	317	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ¬ (𝐼 + 1) ≤ 𝐼)
319	312, 318	pm2.65da 815	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → ¬ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
320	289, 319	syldan 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → ¬ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
321	271, 320	pm2.61dan 811	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
322	44, 178	ltnled 11302	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ↔ ¬ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
323	321, 322	mpbird 256	. . . . . . . . 9 ⊢ (𝜑 → (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
324	197	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ∈ ℝ)
325	19	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐷 ∈ ℝ)
326	178	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
327	18	rexrd 11205	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
328	19	rexrd 11205	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷 ∈ ℝ^*)
329	18, 19, 31	ltled 11303	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐶 ≤ 𝐷)
330		lbicc2 13381	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷) → 𝐶 ∈ (𝐶[,]𝐷))
331	327, 328, 329, 330	syl3anc 1371	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐶 ∈ (𝐶[,]𝐷))
332		ubicc2 13382	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷) → 𝐷 ∈ (𝐶[,]𝐷))
333	327, 328, 329, 332	syl3anc 1371	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 ∈ (𝐶[,]𝐷))
334	331, 333	jca 512	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)))
335		prssg 4779	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷)))
336	18, 19, 335	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷)))
337	334, 336	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ (𝐶[,]𝐷))
338	337, 23	unssd 4146	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ (𝐶[,]𝐷))
339	17, 338	eqsstrid 3992	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻 ⊆ (𝐶[,]𝐷))
340	339, 196	sseldd 3945	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ∈ (𝐶[,]𝐷))
341		iccleub 13319	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ (𝑉‘(𝐽 + 1)) ∈ (𝐶[,]𝐷)) → (𝑉‘(𝐽 + 1)) ≤ 𝐷)
342	327, 328, 340, 341	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ≤ 𝐷)
343	342	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ 𝐷)
344		simpr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
345	324, 325, 326, 343, 344	letrd 11312	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
346	345	adantlr 713	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
347		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
348	178	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
349	19	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐷 ∈ ℝ)
350	348, 349	ltnled 11302	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷 ↔ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
351	347, 350	mpbird 256	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷)
352	351	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷)
353		simpll 765	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
354		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
355	178	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
356	197	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ∈ ℝ)
357	355, 356	ltnled 11302	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)) ↔ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
358	354, 357	mpbird 256	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)))
359	358	ad4ant14 750	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)))
360	18	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → 𝐶 ∈ ℝ)
361	19	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → 𝐷 ∈ ℝ)
362	178	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
363	18	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐶 ∈ ℝ)
364	178	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
365	44	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) ∈ ℝ)
366	339, 43	sseldd 3945	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑉‘𝐽) ∈ (𝐶[,]𝐷))
367		iccgelb 13320	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ (𝑉‘𝐽) ∈ (𝐶[,]𝐷)) → 𝐶 ≤ (𝑉‘𝐽))
368	327, 328, 366, 367	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐶 ≤ (𝑉‘𝐽))
369	368	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐶 ≤ (𝑉‘𝐽))
370		simpr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
371	363, 365, 364, 369, 370	lelttrd 11313	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐶 < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
372	363, 364, 371	ltled 11303	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐶 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
373	372	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → 𝐶 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
374	178	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
375	19	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → 𝐷 ∈ ℝ)
376		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷)
377	374, 375, 376	ltled 11303	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ 𝐷)
378	377	adantlr 713	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ 𝐷)
379	360, 361, 362, 373, 378	eliccd 43732	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ (𝐶[,]𝐷))
380	167	znegcld 12609	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → -𝐿 ∈ ℤ)
381	247, 234	mulneg1d 11608	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (-𝐿 · 𝑇) = -(𝐿 · 𝑇))
382	381	oveq2d 7373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)) = (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + -(𝐿 · 𝑇)))
383	178	recnd 11183	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℂ)
384	383, 240	negsubd 11518	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + -(𝐿 · 𝑇)) = (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) − (𝐿 · 𝑇)))
385	177	recnd 11183	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℂ)
386	385, 240	pncand 11513	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) − (𝐿 · 𝑇)) = (𝑄‘(𝐼 + 1)))
387	382, 384, 386	3eqtrd 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)) = (𝑄‘(𝐼 + 1)))
388		ffn 6668	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
389	50, 388	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
390		fnfvelrn 7031	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 Fn (0...𝑀) ∧ (𝐼 + 1) ∈ (0...𝑀)) → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
391	389, 176, 390	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
392	387, 391	eqeltrd 2838	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)) ∈ ran 𝑄)
393		oveq1 7364	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = -𝐿 → (𝑘 · 𝑇) = (-𝐿 · 𝑇))
394	393	oveq2d 7373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = -𝐿 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) = (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)))
395	394	eleq1d 2822	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = -𝐿 → ((((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)) ∈ ran 𝑄))
396	395	rspcev 3581	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-𝐿 ∈ ℤ ∧ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
397	380, 392, 396	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
398	397	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
399		oveq1 7364	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → (𝑦 + (𝑘 · 𝑇)) = (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)))
400	399	eleq1d 2822	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
401	400	rexbidv 3175	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
402	401	elrab 3645	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} ↔ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
403	379, 398, 402	sylanbrc 583	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
404		elun2 4137	. . . . . . . . . . . . . . . 16 ⊢ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
405	403, 404	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
406	17	eqcomi 2745	. . . . . . . . . . . . . . 15 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = 𝐻
407	405, 406	eleqtrdi 2848	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻)
408	407	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻)
409		f1ofo 6791	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑉:(0...𝑁)–1-1-onto→𝐻 → 𝑉:(0...𝑁)–onto→𝐻)
410	36, 37, 409	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑉:(0...𝑁)–onto→𝐻)
411		foelrn 7056	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑉:(0...𝑁)–onto→𝐻 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
412	410, 411	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
413		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
414	413	eqcomd 2742	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗) → (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
415	414	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗) → (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
416	415	reximdv 3167	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → (∃𝑗 ∈ (0...𝑁)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗) → ∃𝑗 ∈ (0...𝑁)(𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
417	412, 416	mpd 15	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
418	417	ad4ant14 750	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
419		simpl 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
420	413	eqcoms 2744	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
421	420	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
422	419, 421	breqtrd 5131	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) < (𝑉‘𝑗))
423	422	adantll 712	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) < (𝑉‘𝑗))
424	423	adantlr 713	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) < (𝑉‘𝑗))
425	36	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑉 Isom < , < ((0...𝑁), 𝐻))
426	42	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐽 ∈ (0...𝑁))
427		simplr 767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑗 ∈ (0...𝑁))
428		isorel 7271	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑉 Isom < , < ((0...𝑁), 𝐻) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) → (𝐽 < 𝑗 ↔ (𝑉‘𝐽) < (𝑉‘𝑗)))
429	425, 426, 427, 428	syl12anc 835	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝐽 < 𝑗 ↔ (𝑉‘𝐽) < (𝑉‘𝑗)))
430	424, 429	mpbird 256	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐽 < 𝑗)
431	430	adantllr 717	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐽 < 𝑗)
432		simpr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
433		simpl 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)))
434	432, 433	eqbrtrd 5127	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝑗) < (𝑉‘(𝐽 + 1)))
435	434	adantll 712	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝑗) < (𝑉‘(𝐽 + 1)))
436	435	adantlr 713	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝑗) < (𝑉‘(𝐽 + 1)))
437	36	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑉 Isom < , < ((0...𝑁), 𝐻))
438		simplr 767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑗 ∈ (0...𝑁))
439	195	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝐽 + 1) ∈ (0...𝑁))
440		isorel 7271	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑉 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝑗 < (𝐽 + 1) ↔ (𝑉‘𝑗) < (𝑉‘(𝐽 + 1))))
441	437, 438, 439, 440	syl12anc 835	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑗 < (𝐽 + 1) ↔ (𝑉‘𝑗) < (𝑉‘(𝐽 + 1))))
442	436, 441	mpbird 256	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑗 < (𝐽 + 1))
443	442	adantl3r 748	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑗 < (𝐽 + 1))
444	431, 443	jca 512	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
445	444	ex 413	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))))
446	445	adantlr 713	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))))
447	446	reximdva 3165	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → (∃𝑗 ∈ (0...𝑁)(𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))))
448	418, 447	mpd 15	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
449	353, 359, 408, 448	syl21anc 836	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
450		elfzelz 13441	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
451	450	ad2antlr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝑗 ∈ ℤ)
452		elfzelz 13441	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 ∈ (0...𝑁) → 𝐽 ∈ ℤ)
453	42, 452	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐽 ∈ ℤ)
454	453	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝐽 ∈ ℤ)
455		simprl 769	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝐽 < 𝑗)
456		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝑗 < (𝐽 + 1))
457		btwnnz 12579	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ)
458	454, 455, 456, 457	syl3anc 1371	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → ¬ 𝑗 ∈ ℤ)
459	451, 458	pm2.65da 815	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ¬ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
460	459	nrexdv 3146	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
461	460	ad3antrrr 728	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ¬ ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
462	449, 461	condan 816	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
463	352, 462	syldan 591	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
464	346, 463	pm2.61dan 811	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
465	323, 464	mpdan 685	. . . . . . . 8 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
466	465	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
467	182	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑥 ∈ ℝ)
468	197	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ∈ ℝ)
469	178	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
470		iooltub 43738	. . . . . . . . . 10 ⊢ (((𝑉‘𝐽) ∈ ℝ^* ∧ (𝑉‘(𝐽 + 1)) ∈ ℝ^* ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 < (𝑉‘(𝐽 + 1)))
471	193, 199, 200, 470	syl3anc 1371	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 < (𝑉‘(𝐽 + 1)))
472	471	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑥 < (𝑉‘(𝐽 + 1)))
473		simpr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
474	467, 468, 469, 472, 473	ltletrd 11315	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑥 < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
475	466, 474	mpdan 685	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
476	174, 180, 182, 203, 475	eliood 43726	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 ∈ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
477	476	ralrimiva 3143	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))𝑥 ∈ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
478		dfss3 3932	. . . 4 ⊢ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ↔ ∀𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))𝑥 ∈ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
479	477, 478	sylibr 233	. . 3 ⊢ (𝜑 → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
480		fveq2 6842	. . . . . . 7 ⊢ (𝑖 = 𝐼 → (𝑄‘𝑖) = (𝑄‘𝐼))
481	480	oveq1d 7372	. . . . . 6 ⊢ (𝑖 = 𝐼 → ((𝑄‘𝑖) + (𝑙 · 𝑇)) = ((𝑄‘𝐼) + (𝑙 · 𝑇)))
482		oveq1 7364	. . . . . . . 8 ⊢ (𝑖 = 𝐼 → (𝑖 + 1) = (𝐼 + 1))
483	482	fveq2d 6846	. . . . . . 7 ⊢ (𝑖 = 𝐼 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝐼 + 1)))
484	483	oveq1d 7372	. . . . . 6 ⊢ (𝑖 = 𝐼 → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇)))
485	481, 484	oveq12d 7375	. . . . 5 ⊢ (𝑖 = 𝐼 → (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) = (((𝑄‘𝐼) + (𝑙 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇))))
486	485	sseq2d 3976	. . . 4 ⊢ (𝑖 = 𝐼 → (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) ↔ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝑙 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇)))))
487		oveq1 7364	. . . . . . 7 ⊢ (𝑙 = 𝐿 → (𝑙 · 𝑇) = (𝐿 · 𝑇))
488	487	oveq2d 7373	. . . . . 6 ⊢ (𝑙 = 𝐿 → ((𝑄‘𝐼) + (𝑙 · 𝑇)) = ((𝑄‘𝐼) + (𝐿 · 𝑇)))
489	487	oveq2d 7373	. . . . . 6 ⊢ (𝑙 = 𝐿 → ((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
490	488, 489	oveq12d 7375	. . . . 5 ⊢ (𝑙 = 𝐿 → (((𝑄‘𝐼) + (𝑙 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇))) = (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
491	490	sseq2d 3976	. . . 4 ⊢ (𝑙 = 𝐿 → (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝑙 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇))) ↔ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))))
492	486, 491	rspc2ev 3592	. . 3 ⊢ ((𝐼 ∈ (0..^𝑀) ∧ 𝐿 ∈ ℤ ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))) → ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
493	165, 167, 479, 492	syl3anc 1371	. 2 ⊢ (𝜑 → ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
494	165, 167, 493	jca31 515	1 ⊢ (𝜑 → ((𝐼 ∈ (0..^𝑀) ∧ 𝐿 ∈ ℤ) ∧ ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3073 {crab 3407 ∪ cun 3908 ⊆ wss 3910 ∅c0 4282 {cpr 4588 class class class wbr 5105 ↦ cmpt 5188 ran crn 5634 ℩cio 6446 Fn wfn 6491 ⟶wf 6492 –onto→wfo 6494 –1-1-onto→wf1o 6495 ‘cfv 6496 Isom wiso 6497 (class class class)co 7357 ↑_m cmap 8765 supcsup 9376 ℂcc 11049 ℝcr 11050 0cc0 11051 1c1 11052 + caddc 11054 · cmul 11056 ℝ^*cxr 11188 < clt 11189 ≤ cle 11190 − cmin 11385 -cneg 11386 / cdiv 11812 ℕcn 12153 ℕ₀cn0 12413 ℤcz 12499 ℤ_≥cuz 12763 ℝ⁺crp 12915 (,)cioo 13264 [,]cicc 13267 ...cfz 13424 ..^cfzo 13567 ♯chash 14230

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-inf2 9577 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128 ax-pre-sup 11129

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-iin 4957 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-se 5589 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-1o 8412 df-oadd 8416 df-er 8648 df-map 8767 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fi 9347 df-sup 9378 df-inf 9379 df-oi 9446 df-dju 9837 df-card 9875 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-div 11813 df-nn 12154 df-2 12216 df-3 12217 df-n0 12414 df-xnn0 12486 df-z 12500 df-uz 12764 df-q 12874 df-rp 12916 df-xneg 13033 df-xadd 13034 df-xmul 13035 df-ioo 13268 df-icc 13271 df-fz 13425 df-fzo 13568 df-seq 13907 df-exp 13968 df-hash 14231 df-cj 14984 df-re 14985 df-im 14986 df-sqrt 15120 df-abs 15121 df-rest 17304 df-topgen 17325 df-psmet 20788 df-xmet 20789 df-met 20790 df-bl 20791 df-mopn 20792 df-top 22243 df-topon 22260 df-bases 22296 df-cld 22370 df-ntr 22371 df-cls 22372 df-nei 22449 df-lp 22487 df-cmp 22738

This theorem is referenced by: fourierdlem97 44434

W3C validator