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 46917

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 4035	. . . 4 ⊢ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ (0..^𝑀)
3		fzossfz 13719	. . . . . . . 8 ⊢ (0..^𝑀) ⊆ (0...𝑀)
4		fzssz 13565	. . . . . . . 8 ⊢ (0...𝑀) ⊆ ℤ
5	3, 4	sstri 3947	. . . . . . 7 ⊢ (0..^𝑀) ⊆ ℤ
6	2, 5	sstri 3947	. . . . . 6 ⊢ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ
7	6	a1i 11	. . . . 5 ⊢ (𝜑 → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ)
8		0zd 12614	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℤ)
9		fourierdlem64.m	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
10	9	nnzd 12628	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
11	9	nngt0d 12296	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝑀)
12		fzolb 13706	. . . . . . . 8 ⊢ (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
13	8, 10, 11, 12	syl3anbrc 1362	. . . . . . 7 ⊢ (𝜑 → 0 ∈ (0..^𝑀))
14		fourierdlem64.l	. . . . . . . . . 10 ⊢ 𝐿 = sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < )
15		ssrab2 4035	. . . . . . . . . . . 12 ⊢ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ
16	15	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ)
17		fourierdlem64.h	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
18		fourierdlem64.c	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐶 ∈ ℝ)
19		fourierdlem64.d	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 ∈ ℝ)
20		prssi 4789	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → {𝐶, 𝐷} ⊆ ℝ)
21	18, 19, 20	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ ℝ)
22		ssrab2 4035	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷)
23	22	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷))
24	18, 19	iccssred 13472	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐶[,]𝐷) ⊆ ℝ)
25	23, 24	sstrd 3948	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ ℝ)
26	21, 25	unssd 4145	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ ℝ)
27	17, 26	eqsstrid 3976	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ⊆ ℝ)
28		fourierdlem64.t	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑇 = (𝐵 − 𝐴)
29		fourierdlem64.p	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
30		fourierdlem64.q	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
31		fourierdlem64.cltd	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐶 < 𝐷)
32		eqid 2765	. . . . . . . . . . . . . . . . . . . . . 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 46907	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑉 ∈ ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑁)) ∧ 𝑉 Isom < , < ((0...𝑁), 𝐻)))
36	35	simprd 501	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑉 Isom < , < ((0...𝑁), 𝐻))
37		isof1o 7327	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑉 Isom < , < ((0...𝑁), 𝐻) → 𝑉:(0...𝑁)–1-1-onto→𝐻)
38		f1of 6824	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑉:(0...𝑁)–1-1-onto→𝐻 → 𝑉:(0...𝑁)⟶𝐻)
39	36, 37, 38	3syl 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑉:(0...𝑁)⟶𝐻)
40		fourierdlem64.j	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
41		elfzofz 13716	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
42	40, 41	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐽 ∈ (0...𝑁))
43	39, 42	ffvelcdmd 7084	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑉‘𝐽) ∈ 𝐻)
44	27, 43	sseldd 3939	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑉‘𝐽) ∈ ℝ)
45	29	fourierdlem2 46856	. . . . . . . . . . . . . . . . . . . . . 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 8848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
50	48, 49	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
51	9	nnnn0d 12576	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
52		nn0uz 12911	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ₀ = (ℤ_≥‘0)
53	51, 52	eleqtrdi 2875	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
54		eluzfz1 13570	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
55	53, 54	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 ∈ (0...𝑀))
56	50, 55	ffvelcdmd 7084	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
57	44, 56	resubcld 11653	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑉‘𝐽) − (𝑄‘0)) ∈ ℝ)
58	29, 9, 30	fourierdlem11 46865	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
59	58	simp2d 1161	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ)
60	58	simp1d 1160	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℝ)
61	59, 60	resubcld 11653	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
62	28, 61	eqeltrid 2869	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ∈ ℝ)
63	58	simp3d 1162	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 < 𝐵)
64	60, 59	posdifd 11812	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
65	63, 64	mpbid 235	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
66	65, 28	breqtrrdi 5155	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝑇)
67	66	gt0ne0d 11789	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ≠ 0)
68	57, 62, 67	redivcld 12054	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∈ ℝ)
69		btwnz 12710	. . . . . . . . . . . . . . 15 ⊢ ((((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∈ ℝ → (∃𝑘 ∈ ℤ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∧ ∃𝑧 ∈ ℤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) < 𝑧))
70	68, 69	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑘 ∈ ℤ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∧ ∃𝑧 ∈ ℤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) < 𝑧))
71	70	simpld 500	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∃𝑘 ∈ ℤ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
72		zre 12606	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℝ)
73	56	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (𝑄‘0) ∈ ℝ)
74		simplr 781	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → 𝑘 ∈ ℝ)
75	62	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → 𝑇 ∈ ℝ)
76	74, 75	remulcld 11250	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (𝑘 · 𝑇) ∈ ℝ)
77	73, 76	readdcld 11249	. . . . . . . . . . . . . . . . 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 13068	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑇 ∈ ℝ⁺)
82	81	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → 𝑇 ∈ ℝ⁺)
83	74, 80, 82	ltmuldivd 13118	. . . . . . . . . . . . . . . . . . 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 11250	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (𝑘 · 𝑇) ∈ ℝ)
89	44	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (𝑉‘𝐽) ∈ ℝ)
90	85, 88, 89	ltaddsub2d 11826	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (((𝑄‘0) + (𝑘 · 𝑇)) < (𝑉‘𝐽) ↔ (𝑘 · 𝑇) < ((𝑉‘𝐽) − (𝑄‘0))))
91	90	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (((𝑄‘0) + (𝑘 · 𝑇)) < (𝑉‘𝐽) ↔ (𝑘 · 𝑇) < ((𝑉‘𝐽) − (𝑄‘0))))
92	84, 91	mpbird 260	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑄‘0) + (𝑘 · 𝑇)) < (𝑉‘𝐽))
93	77, 78, 92	ltled 11369	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽))
94	93	ex 418	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)))
95	72, 94	sylan2 605	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)))
96	95	reximdva 3180	. . . . . . . . . . . . 13 ⊢ (𝜑 → (∃𝑘 ∈ ℤ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → ∃𝑘 ∈ ℤ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)))
97	71, 96	mpd 16	. . . . . . . . . . . 12 ⊢ (𝜑 → ∃𝑘 ∈ ℤ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽))
98		rabn0 4346	. . . . . . . . . . . 12 ⊢ ({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ↔ ∃𝑘 ∈ ℤ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽))
99	97, 98	sylibr 237	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
100		simpl 488	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝜑)
101	16	sselda 3938	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝑗 ∈ ℤ)
102		oveq1 7423	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑗 → (𝑘 · 𝑇) = (𝑗 · 𝑇))
103	102	oveq2d 7432	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((𝑄‘0) + (𝑘 · 𝑇)) = ((𝑄‘0) + (𝑗 · 𝑇)))
104	103	breq1d 5121	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → (((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)))
105	104	elrab 3652	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ (𝑗 ∈ ℤ ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)))
106	105	simprbi 503	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} → ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽))
107	106	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽))
108		zre 12606	. . . . . . . . . . . . . . 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 11250	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℝ) → (𝑗 · 𝑇) ∈ ℝ)
114	113	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝑗 · 𝑇) ∈ ℝ)
115	44	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝑉‘𝐽) ∈ ℝ)
116	110, 114, 115	leaddsub2d 11827	. . . . . . . . . . . . . . . . 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 13120	. . . . . . . . . . . . . . . 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 3159	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
126		breq2 5115	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → (𝑗 ≤ 𝑏 ↔ 𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)))
127	126	ralbidv 3190	. . . . . . . . . . . . 13 ⊢ (𝑏 = (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → (∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏 ↔ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)))
128	127	rspcev 3583	. . . . . . . . . . . 12 ⊢ (((((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∈ ℝ ∧ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏)
129	68, 125, 128	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏)
130		suprzcl 12687	. . . . . . . . . . 11 ⊢ (({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ ∧ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ∧ ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏) → sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)})
131	16, 99, 129, 130	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝜑 → sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)})
132	14, 131	eqeltrid 2869	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)})
133		oveq1 7423	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝐿 → (𝑘 · 𝑇) = (𝐿 · 𝑇))
134	133	oveq2d 7432	. . . . . . . . . . 11 ⊢ (𝑘 = 𝐿 → ((𝑄‘0) + (𝑘 · 𝑇)) = ((𝑄‘0) + (𝐿 · 𝑇)))
135	134	breq1d 5121	. . . . . . . . . 10 ⊢ (𝑘 = 𝐿 → (((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
136	135	elrab 3652	. . . . . . . . 9 ⊢ (𝐿 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ (𝐿 ∈ ℤ ∧ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
137	132, 136	sylib 221	. . . . . . . 8 ⊢ (𝜑 → (𝐿 ∈ ℤ ∧ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
138	137	simprd 501	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
139		fveq2 6885	. . . . . . . . . 10 ⊢ (𝑗 = 0 → (𝑄‘𝑗) = (𝑄‘0))
140	139	oveq1d 7431	. . . . . . . . 9 ⊢ (𝑗 = 0 → ((𝑄‘𝑗) + (𝐿 · 𝑇)) = ((𝑄‘0) + (𝐿 · 𝑇)))
141	140	breq1d 5121	. . . . . . . 8 ⊢ (𝑗 = 0 → (((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
142	141	elrab 3652	. . . . . . 7 ⊢ (0 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ (0 ∈ (0..^𝑀) ∧ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
143	13, 138, 142	sylanbrc 595	. . . . . 6 ⊢ (𝜑 → 0 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
144		ne0i 4294	. . . . . 6 ⊢ (0 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
145	143, 144	syl 18	. . . . 5 ⊢ (𝜑 → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
146	9	nnred 12259	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℝ)
147	2	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ (0..^𝑀))
148	147	sselda 3938	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝑘 ∈ (0..^𝑀))
149		elfzoelz 13699	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0..^𝑀) → 𝑘 ∈ ℤ)
150	149	zred 12711	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0..^𝑀) → 𝑘 ∈ ℝ)
151	150	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑘 ∈ ℝ)
152	146	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑀 ∈ ℝ)
153		elfzolt2 13709	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0..^𝑀) → 𝑘 < 𝑀)
154	153	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑘 < 𝑀)
155	151, 152, 154	ltled 11369	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑘 ≤ 𝑀)
156	148, 155	syldan 603	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝑘 ≤ 𝑀)
157	156	ralrimiva 3159	. . . . . 6 ⊢ (𝜑 → ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑀)
158		breq2 5115	. . . . . . . 8 ⊢ (𝑏 = 𝑀 → (𝑘 ≤ 𝑏 ↔ 𝑘 ≤ 𝑀))
159	158	ralbidv 3190	. . . . . . 7 ⊢ (𝑏 = 𝑀 → (∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏 ↔ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑀))
160	159	rspcev 3583	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑀) → ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏)
161	146, 157, 160	syl2anc 596	. . . . 5 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏)
162		suprzcl 12687	. . . . 5 ⊢ (({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ ∧ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ∧ ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏) → sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
163	7, 145, 161, 162	syl3anc 1398	. . . 4 ⊢ (𝜑 → sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
164	2, 163	sselid 3936	. . 3 ⊢ (𝜑 → sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ (0..^𝑀))
165	1, 164	eqeltrid 2869	. 2 ⊢ (𝜑 → 𝐼 ∈ (0..^𝑀))
166	15, 131	sselid 3936	. . 3 ⊢ (𝜑 → sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ ℤ)
167	14, 166	eqeltrid 2869	. 2 ⊢ (𝜑 → 𝐿 ∈ ℤ)
168	3, 165	sselid 3936	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ (0...𝑀))
169	50, 168	ffvelcdmd 7084	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝐼) ∈ ℝ)
170	167	zred 12711	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ ℝ)
171	170, 62	remulcld 11250	. . . . . . . . 9 ⊢ (𝜑 → (𝐿 · 𝑇) ∈ ℝ)
172	169, 171	readdcld 11249	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ∈ ℝ)
173	172	rexrd 11270	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ∈ ℝ^*)
174	173	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ∈ ℝ^*)
175		fzofzp1 13805	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (0..^𝑀) → (𝐼 + 1) ∈ (0...𝑀))
176	165, 175	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼 + 1) ∈ (0...𝑀))
177	50, 176	ffvelcdmd 7084	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ)
178	177, 171	readdcld 11249	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
179	178	rexrd 11270	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ^*)
180	179	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ^*)
181		elioore 13413	. . . . . . 7 ⊢ (𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) → 𝑥 ∈ ℝ)
182	181	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 ∈ ℝ)
183	172	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ∈ ℝ)
184	44	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘𝐽) ∈ ℝ)
185	1, 163	eqeltrid 2869	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
186		fveq2 6885	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐼 → (𝑄‘𝑗) = (𝑄‘𝐼))
187	186	oveq1d 7431	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝐼 → ((𝑄‘𝑗) + (𝐿 · 𝑇)) = ((𝑄‘𝐼) + (𝐿 · 𝑇)))
188	187	breq1d 5121	. . . . . . . . . . 11 ⊢ (𝑗 = 𝐼 → (((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
189	188	elrab 3652	. . . . . . . . . 10 ⊢ (𝐼 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ (𝐼 ∈ (0..^𝑀) ∧ ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
190	185, 189	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 ∈ (0..^𝑀) ∧ ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
191	190	simprd 501	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
192	191	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
193	184	rexrd 11270	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘𝐽) ∈ ℝ^*)
194		fzofzp1 13805	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
195	40, 194	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
196	39, 195	ffvelcdmd 7084	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ∈ 𝐻)
197	27, 196	sseldd 3939	. . . . . . . . . 10 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ∈ ℝ)
198	197	rexrd 11270	. . . . . . . . 9 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ∈ ℝ^*)
199	198	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘(𝐽 + 1)) ∈ ℝ^*)
200		simpr 490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))))
201		ioogtlb 46244	. . . . . . . 8 ⊢ (((𝑉‘𝐽) ∈ ℝ^* ∧ (𝑉‘(𝐽 + 1)) ∈ ℝ^* ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘𝐽) < 𝑥)
202	193, 199, 200, 201	syl3anc 1398	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘𝐽) < 𝑥)
203	183, 184, 182, 192, 202	lelttrd 11379	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝐼) + (𝐿 · 𝑇)) < 𝑥)
204		zssre 12609	. . . . . . . . . . . . . . . 16 ⊢ ℤ ⊆ ℝ
205	15, 204	sstri 3947	. . . . . . . . . . . . . . 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 12714	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐿 + 1) ∈ ℤ)
210	209	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐿 + 1) ∈ ℤ)
211		oveq1 7423	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐼 = (𝑀 − 1) → (𝐼 + 1) = ((𝑀 − 1) + 1))
212	146	recnd 11248	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑀 ∈ ℂ)
213		1cnd 11213	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 ∈ ℂ)
214	212, 213	npcand 11584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
215	211, 214	sylan9eqr 2822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝐼 + 1) = 𝑀)
216	215	fveq2d 6889	. . . . . . . . . . . . . . . . . . . . 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 11248	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐵 ∈ ℂ)
222	60	recnd 11248	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐴 ∈ ℂ)
223	221, 222	npcand 11584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐵 − 𝐴) + 𝐴) = 𝐵)
224	223	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐵 = ((𝐵 − 𝐴) + 𝐴))
225	28	eqcomi 2774	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐵 − 𝐴) = 𝑇
226	225	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐵 − 𝐴) = 𝑇)
227	226	oveq1d 7431	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐵 − 𝐴) + 𝐴) = (𝑇 + 𝐴))
228	218	simpld 500	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
229	228	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐴 = (𝑄‘0))
230	229	oveq2d 7432	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑇 + 𝐴) = (𝑇 + (𝑄‘0)))
231	224, 227, 230	3eqtrd 2804	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐵 = (𝑇 + (𝑄‘0)))
232	231	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → 𝐵 = (𝑇 + (𝑄‘0)))
233	216, 220, 232	3eqtrd 2804	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑄‘(𝐼 + 1)) = (𝑇 + (𝑄‘0)))
234	62	recnd 11248	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑇 ∈ ℂ)
235	228, 222	eqeltrd 2865	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑄‘0) ∈ ℂ)
236	234, 235	addcomd 11423	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑇 + (𝑄‘0)) = ((𝑄‘0) + 𝑇))
237	236	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑇 + (𝑄‘0)) = ((𝑄‘0) + 𝑇))
238	233, 237	eqtrd 2800	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑄‘(𝐼 + 1)) = ((𝑄‘0) + 𝑇))
239	238	oveq1d 7431	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (((𝑄‘0) + 𝑇) + (𝐿 · 𝑇)))
240	171	recnd 11248	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 · 𝑇) ∈ ℂ)
241	235, 234, 240	addassd 11242	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝑄‘0) + 𝑇) + (𝐿 · 𝑇)) = ((𝑄‘0) + (𝑇 + (𝐿 · 𝑇))))
242	234	mullidd 11238	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (1 · 𝑇) = 𝑇)
243	242, 234	eqeltrd 2865	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 · 𝑇) ∈ ℂ)
244	243, 240	addcomd 11423	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1 · 𝑇) + (𝐿 · 𝑇)) = ((𝐿 · 𝑇) + (1 · 𝑇)))
245	242	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑇 = (1 · 𝑇))
246	245	oveq1d 7431	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑇 + (𝐿 · 𝑇)) = ((1 · 𝑇) + (𝐿 · 𝑇)))
247	170	recnd 11248	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐿 ∈ ℂ)
248	247, 213, 234	adddird 11245	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝐿 + 1) · 𝑇) = ((𝐿 · 𝑇) + (1 · 𝑇)))
249	244, 246, 248	3eqtr4d 2810	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑇 + (𝐿 · 𝑇)) = ((𝐿 + 1) · 𝑇))
250	249	oveq2d 7432	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑄‘0) + (𝑇 + (𝐿 · 𝑇))) = ((𝑄‘0) + ((𝐿 + 1) · 𝑇)))
251	241, 250	eqtrd 2800	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑄‘0) + 𝑇) + (𝐿 · 𝑇)) = ((𝑄‘0) + ((𝐿 + 1) · 𝑇)))
252	251	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (((𝑄‘0) + 𝑇) + (𝐿 · 𝑇)) = ((𝑄‘0) + ((𝐿 + 1) · 𝑇)))
253	239, 252	eqtr2d 2801	. . . . . . . . . . . . . . . . 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 5135	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) ≤ (𝑉‘𝐽))
257		oveq1 7423	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (𝐿 + 1) → (𝑘 · 𝑇) = ((𝐿 + 1) · 𝑇))
258	257	oveq2d 7432	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (𝐿 + 1) → ((𝑄‘0) + (𝑘 · 𝑇)) = ((𝑄‘0) + ((𝐿 + 1) · 𝑇)))
259	258	breq1d 5121	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝐿 + 1) → (((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) ≤ (𝑉‘𝐽)))
260	259	elrab 3652	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 + 1) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ ((𝐿 + 1) ∈ ℤ ∧ ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) ≤ (𝑉‘𝐽)))
261	210, 256, 260	sylanbrc 595	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐿 + 1) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)})
262		suprub 12187	. . . . . . . . . . . . . 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 5155	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐿 + 1) ≤ 𝐿)
265	170	ltp1d 12156	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 < (𝐿 + 1))
266		peano2re 11394	. . . . . . . . . . . . . . . 16 ⊢ (𝐿 ∈ ℝ → (𝐿 + 1) ∈ ℝ)
267	170, 266	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐿 + 1) ∈ ℝ)
268	170, 267	ltnled 11368	. . . . . . . . . . . . . 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 3936	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐼 ∈ ℤ)
273	272	zred 12711	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐼 ∈ ℝ)
274	273	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → 𝐼 ∈ ℝ)
275		peano2rem 11536	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℝ → (𝑀 − 1) ∈ ℝ)
276	146, 275	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 − 1) ∈ ℝ)
277	276	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → (𝑀 − 1) ∈ ℝ)
278		elfzolt2 13709	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 ∈ (0..^𝑀) → 𝐼 < 𝑀)
279		elfzoelz 13699	. . . . . . . . . . . . . . . . 17 ⊢ (𝐼 ∈ (0..^𝑀) → 𝐼 ∈ ℤ)
280		elfzoel2 13698	. . . . . . . . . . . . . . . . 17 ⊢ (𝐼 ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
281		zltlem1 12658	. . . . . . . . . . . . . . . . 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 2968	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝐼 = (𝑀 − 1) → 𝐼 ≠ (𝑀 − 1))
287	286	necomd 3015	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐼 = (𝑀 − 1) → (𝑀 − 1) ≠ 𝐼)
288	287	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → (𝑀 − 1) ≠ 𝐼)
289	274, 277, 285, 288	leneltd 11375	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → 𝐼 < (𝑀 − 1))
290	6, 204	sstri 3947	. . . . . . . . . . . . . . . 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 11220	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → 1 ∈ ℝ)
298		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → 𝐼 < (𝑀 − 1))
299	295, 296, 297, 298	ltadd1dd 11836	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝐼 + 1) < ((𝑀 − 1) + 1))
300	214	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → ((𝑀 − 1) + 1) = 𝑀)
301	299, 300	breqtrd 5139	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝐼 + 1) < 𝑀)
302		elfzfzo 46029	. . . . . . . . . . . . . . . . . 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 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝐼 + 1) → (𝑄‘𝑗) = (𝑄‘(𝐼 + 1)))
306	305	oveq1d 7431	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝐼 + 1) → ((𝑄‘𝑗) + (𝐿 · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
307	306	breq1d 5121	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝐼 + 1) → (((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
308	307	elrab 3652	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 + 1) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ ((𝐼 + 1) ∈ (0..^𝑀) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
309	304, 308	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐼 + 1) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
310		suprub 12187	. . . . . . . . . . . . . . 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 5155	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐼 + 1) ≤ 𝐼)
313	273	ltp1d 12156	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐼 < (𝐼 + 1))
314		peano2re 11394	. . . . . . . . . . . . . . . . 17 ⊢ (𝐼 ∈ ℝ → (𝐼 + 1) ∈ ℝ)
315	273, 314	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐼 + 1) ∈ ℝ)
316	273, 315	ltnled 11368	. . . . . . . . . . . . . . 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 11368	. . . . . . . . . 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 11270	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
328	19	rexrd 11270	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷 ∈ ℝ^*)
329	18, 19, 31	ltled 11369	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐶 ≤ 𝐷)
330		lbicc2 13502	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷) → 𝐶 ∈ (𝐶[,]𝐷))
331	327, 328, 329, 330	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐶 ∈ (𝐶[,]𝐷))
332		ubicc2 13503	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷) → 𝐷 ∈ (𝐶[,]𝐷))
333	327, 328, 329, 332	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 ∈ (𝐶[,]𝐷))
334	331, 333	jca 521	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)))
335		prssg 4787	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷)))
336	18, 19, 335	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷)))
337	334, 336	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ (𝐶[,]𝐷))
338	337, 23	unssd 4145	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ (𝐶[,]𝐷))
339	17, 338	eqsstrid 3976	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻 ⊆ (𝐶[,]𝐷))
340	339, 196	sseldd 3939	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ∈ (𝐶[,]𝐷))
341		iccleub 13439	. . . . . . . . . . . . . 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 11378	. . . . . . . . . . 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 11368	. . . . . . . . . . . . 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 11368	. . . . . . . . . . . . . . 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 3939	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑉‘𝐽) ∈ (𝐶[,]𝐷))
367		iccgelb 13440	. . . . . . . . . . . . . . . . . . . . . . 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 11379	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐶 < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
372	363, 364, 371	ltled 11369	. . . . . . . . . . . . . . . . . . 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 11369	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ 𝐷)
378	377	adantlr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ 𝐷)
379	360, 361, 362, 373, 378	eliccd 46253	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ (𝐶[,]𝐷))
380	167	znegcld 12713	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → -𝐿 ∈ ℤ)
381	247, 234	mulneg1d 11678	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (-𝐿 · 𝑇) = -(𝐿 · 𝑇))
382	381	oveq2d 7432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)) = (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + -(𝐿 · 𝑇)))
383	178	recnd 11248	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℂ)
384	383, 240	negsubd 11586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + -(𝐿 · 𝑇)) = (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) − (𝐿 · 𝑇)))
385	177	recnd 11248	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℂ)
386	385, 240	pncand 11581	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) − (𝐿 · 𝑇)) = (𝑄‘(𝐼 + 1)))
387	382, 384, 386	3eqtrd 2804	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)) = (𝑄‘(𝐼 + 1)))
388		ffn 6709	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
389	50, 388	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
390		fnfvelrn 7079	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 Fn (0...𝑀) ∧ (𝐼 + 1) ∈ (0...𝑀)) → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
391	389, 176, 390	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
392	387, 391	eqeltrd 2865	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)) ∈ ran 𝑄)
393		oveq1 7423	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = -𝐿 → (𝑘 · 𝑇) = (-𝐿 · 𝑇))
394	393	oveq2d 7432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = -𝐿 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) = (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)))
395	394	eleq1d 2850	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = -𝐿 → ((((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)) ∈ ran 𝑄))
396	395	rspcev 3583	. . . . . . . . . . . . . . . . . . 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 7423	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → (𝑦 + (𝑘 · 𝑇)) = (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)))
400	399	eleq1d 2850	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
401	400	rexbidv 3191	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
402	401	elrab 3652	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} ↔ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
403	379, 398, 402	sylanbrc 595	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
404		elun2 4136	. . . . . . . . . . . . . . . 16 ⊢ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
405	403, 404	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
406	17	eqcomi 2774	. . . . . . . . . . . . . . 15 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = 𝐻
407	405, 406	eleqtrdi 2875	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻)
408	407	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻)
409		f1ofo 6832	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑉:(0...𝑁)–1-1-onto→𝐻 → 𝑉:(0...𝑁)–onto→𝐻)
410	36, 37, 409	3syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑉:(0...𝑁)–onto→𝐻)
411		foelrn 7106	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑉:(0...𝑁)–onto→𝐻 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
412	410, 411	sylan 592	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
413		id 23	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
414	413	eqcomd 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗) → (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
415	414	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗) → (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
416	415	reximdv 3182	. . . . . . . . . . . . . . . 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 2773	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
421	420	adantl 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
422	419, 421	breqtrd 5139	. . . . . . . . . . . . . . . . . . . . . 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 7330	. . . . . . . . . . . . . . . . . . . . 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 5135	. . . . . . . . . . . . . . . . . . . . . 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 7330	. . . . . . . . . . . . . . . . . . . . 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 3180	. . . . . . . . . . . . . 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 13563	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
451	450	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝑗 ∈ ℤ)
452		elfzelz 13563	. . . . . . . . . . . . . . . . . 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 12683	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ)
458	454, 455, 456, 457	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → ¬ 𝑗 ∈ ℤ)
459	451, 458	pm2.65da 829	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ¬ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
460	459	nrexdv 3162	. . . . . . . . . . . . 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 46259	. . . . . . . . . 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 11381	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑥 < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
475	466, 474	mpdan 700	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
476	174, 180, 182, 203, 475	eliood 46247	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 ∈ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
477	476	ralrimiva 3159	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))𝑥 ∈ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
478		dfss3 3927	. . . 4 ⊢ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ↔ ∀𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))𝑥 ∈ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
479	477, 478	sylibr 237	. . 3 ⊢ (𝜑 → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
480		fveq2 6885	. . . . . . 7 ⊢ (𝑖 = 𝐼 → (𝑄‘𝑖) = (𝑄‘𝐼))
481	480	oveq1d 7431	. . . . . 6 ⊢ (𝑖 = 𝐼 → ((𝑄‘𝑖) + (𝑙 · 𝑇)) = ((𝑄‘𝐼) + (𝑙 · 𝑇)))
482		oveq1 7423	. . . . . . . 8 ⊢ (𝑖 = 𝐼 → (𝑖 + 1) = (𝐼 + 1))
483	482	fveq2d 6889	. . . . . . 7 ⊢ (𝑖 = 𝐼 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝐼 + 1)))
484	483	oveq1d 7431	. . . . . 6 ⊢ (𝑖 = 𝐼 → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇)))
485	481, 484	oveq12d 7434	. . . . 5 ⊢ (𝑖 = 𝐼 → (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) = (((𝑄‘𝐼) + (𝑙 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇))))
486	485	sseq2d 3970	. . . 4 ⊢ (𝑖 = 𝐼 → (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) ↔ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝑙 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇)))))
487		oveq1 7423	. . . . . . 7 ⊢ (𝑙 = 𝐿 → (𝑙 · 𝑇) = (𝐿 · 𝑇))
488	487	oveq2d 7432	. . . . . 6 ⊢ (𝑙 = 𝐿 → ((𝑄‘𝐼) + (𝑙 · 𝑇)) = ((𝑄‘𝐼) + (𝐿 · 𝑇)))
489	487	oveq2d 7432	. . . . . 6 ⊢ (𝑙 = 𝐿 → ((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
490	488, 489	oveq12d 7434	. . . . 5 ⊢ (𝑙 = 𝐿 → (((𝑄‘𝐼) + (𝑙 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇))) = (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
491	490	sseq2d 3970	. . . 4 ⊢ (𝑙 = 𝐿 → (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝑙 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇))) ↔ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))))
492	486, 491	rspc2ev 3596	. . 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 1570 ∈ wcel 2146 ≠ wne 2960 ∀wral 3081 ∃wrex 3091 {crab 3418 ∪ cun 3904 ⊆ wss 3906 ∅c0 4286 {cpr 4593 class class class wbr 5111 ↦ cmpt 5194 ran crn 5664 ℩cio 6494 Fn wfn 6535 ⟶wf 6536 –onto→wfo 6538 –1-1-onto→wf1o 6539 ‘cfv 6540 Isom wiso 6541 (class class class)co 7416 ↑_m cmap 8826 supcsup 9403 ℂcc 11109 ℝcr 11110 0cc0 11111 1c1 11112 + caddc 11114 · cmul 11116 ℝ^*cxr 11253 < clt 11254 ≤ cle 11255 − cmin 11452 -cneg 11453 / cdiv 11882 ℕcn 12244 ℕ₀cn0 12515 ℤcz 12602 ℤ_≥cuz 12873 ℝ⁺crp 13027 (,)cioo 13383 [,]cicc 13386 ...cfz 13546 ..^cfzo 13694 ♯chash 14379

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7738 ax-inf2 9613 ax-cnex 11167 ax-resscn 11168 ax-1cn 11169 ax-icn 11170 ax-addcl 11171 ax-addrcl 11172 ax-mulcl 11173 ax-mulrcl 11174 ax-mulcom 11175 ax-addass 11176 ax-mulass 11177 ax-distr 11178 ax-i2m1 11179 ax-1ne0 11180 ax-1rid 11181 ax-rnegex 11182 ax-rrecex 11183 ax-cnre 11184 ax-pre-lttri 11185 ax-pre-lttrn 11186 ax-pre-ltadd 11187 ax-pre-mulgt0 11188 ax-pre-sup 11189

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7865 df-1st 7988 df-2nd 7989 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-2o 8456 df-oadd 8459 df-er 8696 df-map 8828 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-fi 9374 df-sup 9405 df-inf 9406 df-oi 9475 df-dju 9899 df-card 9937 df-pnf 11256 df-mnf 11257 df-xr 11258 df-ltxr 11259 df-le 11260 df-sub 11454 df-neg 11455 df-div 11883 df-nn 12245 df-2 12314 df-3 12315 df-n0 12516 df-xnn0 12589 df-z 12603 df-uz 12874 df-q 12984 df-rp 13028 df-xneg 13148 df-xadd 13149 df-xmul 13150 df-ioo 13387 df-icc 13390 df-fz 13547 df-fzo 13695 df-seq 14051 df-exp 14111 df-hash 14380 df-cj 15169 df-re 15170 df-im 15171 df-sqrt 15305 df-abs 15306 df-rest 17492 df-topgen 17513 df-psmet 21543 df-xmet 21544 df-met 21545 df-bl 21546 df-mopn 21547 df-top 23080 df-topon 23097 df-bases 23132 df-cld 23205 df-ntr 23206 df-cls 23207 df-nei 23284 df-lp 23322 df-cmp 23573

This theorem is used by: fourierdlem97 46950

W3C validator