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 45481

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 4073	. . . 4 ⊢ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ (0..^𝑀)
3		fzossfz 13675	. . . . . . . 8 ⊢ (0..^𝑀) ⊆ (0...𝑀)
4		fzssz 13527	. . . . . . . 8 ⊢ (0...𝑀) ⊆ ℤ
5	3, 4	sstri 3987	. . . . . . 7 ⊢ (0..^𝑀) ⊆ ℤ
6	2, 5	sstri 3987	. . . . . 6 ⊢ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ
7	6	a1i 11	. . . . 5 ⊢ (𝜑 → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ)
8		0zd 12592	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℤ)
9		fourierdlem64.m	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
10	9	nnzd 12607	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
11	9	nngt0d 12283	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝑀)
12		fzolb 13662	. . . . . . . 8 ⊢ (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
13	8, 10, 11, 12	syl3anbrc 1341	. . . . . . 7 ⊢ (𝜑 → 0 ∈ (0..^𝑀))
14		fourierdlem64.l	. . . . . . . . . 10 ⊢ 𝐿 = sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < )
15		ssrab2 4073	. . . . . . . . . . . 12 ⊢ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ
16	15	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ)
17		fourierdlem64.h	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
18		fourierdlem64.c	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐶 ∈ ℝ)
19		fourierdlem64.d	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 ∈ ℝ)
20		prssi 4820	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → {𝐶, 𝐷} ⊆ ℝ)
21	18, 19, 20	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ ℝ)
22		ssrab2 4073	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷)
23	22	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷))
24	18, 19	iccssred 13435	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐶[,]𝐷) ⊆ ℝ)
25	23, 24	sstrd 3988	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ ℝ)
26	21, 25	unssd 4182	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ ℝ)
27	17, 26	eqsstrid 4026	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ⊆ ℝ)
28		fourierdlem64.t	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑇 = (𝐵 − 𝐴)
29		fourierdlem64.p	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
30		fourierdlem64.q	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
31		fourierdlem64.cltd	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐶 < 𝐷)
32		eqid 2727	. . . . . . . . . . . . . . . . . . . . . 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 45471	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑉 ∈ ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑁)) ∧ 𝑉 Isom < , < ((0...𝑁), 𝐻)))
36	35	simprd 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑉 Isom < , < ((0...𝑁), 𝐻))
37		isof1o 7325	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑉 Isom < , < ((0...𝑁), 𝐻) → 𝑉:(0...𝑁)–1-1-onto→𝐻)
38		f1of 6833	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑉:(0...𝑁)–1-1-onto→𝐻 → 𝑉:(0...𝑁)⟶𝐻)
39	36, 37, 38	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑉:(0...𝑁)⟶𝐻)
40		fourierdlem64.j	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
41		elfzofz 13672	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
42	40, 41	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐽 ∈ (0...𝑁))
43	39, 42	ffvelcdmd 7089	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑉‘𝐽) ∈ 𝐻)
44	27, 43	sseldd 3979	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑉‘𝐽) ∈ ℝ)
45	29	fourierdlem2 45420	. . . . . . . . . . . . . . . . . . . . . 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 494	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
49		elmapi 8859	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
50	48, 49	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
51	9	nnnn0d 12554	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
52		nn0uz 12886	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ₀ = (ℤ_≥‘0)
53	51, 52	eleqtrdi 2838	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
54		eluzfz1 13532	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 ∈ (0...𝑀))
56	50, 55	ffvelcdmd 7089	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
57	44, 56	resubcld 11664	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑉‘𝐽) − (𝑄‘0)) ∈ ℝ)
58	29, 9, 30	fourierdlem11 45429	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
59	58	simp2d 1141	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ)
60	58	simp1d 1140	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℝ)
61	59, 60	resubcld 11664	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
62	28, 61	eqeltrid 2832	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ∈ ℝ)
63	58	simp3d 1142	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 < 𝐵)
64	60, 59	posdifd 11823	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
65	63, 64	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
66	65, 28	breqtrrdi 5184	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝑇)
67	66	gt0ne0d 11800	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ≠ 0)
68	57, 62, 67	redivcld 12064	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∈ ℝ)
69		btwnz 12687	. . . . . . . . . . . . . . 15 ⊢ ((((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∈ ℝ → (∃𝑘 ∈ ℤ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∧ ∃𝑧 ∈ ℤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) < 𝑧))
70	68, 69	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑘 ∈ ℤ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∧ ∃𝑧 ∈ ℤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) < 𝑧))
71	70	simpld 494	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∃𝑘 ∈ ℤ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
72		zre 12584	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℝ)
73	56	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (𝑄‘0) ∈ ℝ)
74		simplr 768	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → 𝑘 ∈ ℝ)
75	62	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → 𝑇 ∈ ℝ)
76	74, 75	remulcld 11266	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (𝑘 · 𝑇) ∈ ℝ)
77	73, 76	readdcld 11265	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑄‘0) + (𝑘 · 𝑇)) ∈ ℝ)
78	44	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (𝑉‘𝐽) ∈ ℝ)
79		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
80	57	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑉‘𝐽) − (𝑄‘0)) ∈ ℝ)
81	62, 66	elrpd 13037	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑇 ∈ ℝ⁺)
82	81	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → 𝑇 ∈ ℝ⁺)
83	74, 80, 82	ltmuldivd 13087	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑘 · 𝑇) < ((𝑉‘𝐽) − (𝑄‘0)) ↔ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)))
84	79, 83	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (𝑘 · 𝑇) < ((𝑉‘𝐽) − (𝑄‘0)))
85	56	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (𝑄‘0) ∈ ℝ)
86		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → 𝑘 ∈ ℝ)
87	62	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → 𝑇 ∈ ℝ)
88	86, 87	remulcld 11266	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (𝑘 · 𝑇) ∈ ℝ)
89	44	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (𝑉‘𝐽) ∈ ℝ)
90	85, 88, 89	ltaddsub2d 11837	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (((𝑄‘0) + (𝑘 · 𝑇)) < (𝑉‘𝐽) ↔ (𝑘 · 𝑇) < ((𝑉‘𝐽) − (𝑄‘0))))
91	90	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (((𝑄‘0) + (𝑘 · 𝑇)) < (𝑉‘𝐽) ↔ (𝑘 · 𝑇) < ((𝑉‘𝐽) − (𝑄‘0))))
92	84, 91	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑄‘0) + (𝑘 · 𝑇)) < (𝑉‘𝐽))
93	77, 78, 92	ltled 11384	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽))
94	93	ex 412	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)))
95	72, 94	sylan2 592	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)))
96	95	reximdva 3163	. . . . . . . . . . . . 13 ⊢ (𝜑 → (∃𝑘 ∈ ℤ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → ∃𝑘 ∈ ℤ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)))
97	71, 96	mpd 15	. . . . . . . . . . . 12 ⊢ (𝜑 → ∃𝑘 ∈ ℤ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽))
98		rabn0 4381	. . . . . . . . . . . 12 ⊢ ({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ↔ ∃𝑘 ∈ ℤ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽))
99	97, 98	sylibr 233	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
100		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝜑)
101	16	sselda 3978	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝑗 ∈ ℤ)
102		oveq1 7421	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑗 → (𝑘 · 𝑇) = (𝑗 · 𝑇))
103	102	oveq2d 7430	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((𝑄‘0) + (𝑘 · 𝑇)) = ((𝑄‘0) + (𝑗 · 𝑇)))
104	103	breq1d 5152	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → (((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)))
105	104	elrab 3680	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ (𝑗 ∈ ℤ ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)))
106	105	simprbi 496	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} → ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽))
107	106	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽))
108		zre 12584	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℤ → 𝑗 ∈ ℝ)
109		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽))
110	56	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝑄‘0) ∈ ℝ)
111		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℝ) → 𝑗 ∈ ℝ)
112	62	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℝ) → 𝑇 ∈ ℝ)
113	111, 112	remulcld 11266	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℝ) → (𝑗 · 𝑇) ∈ ℝ)
114	113	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝑗 · 𝑇) ∈ ℝ)
115	44	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝑉‘𝐽) ∈ ℝ)
116	110, 114, 115	leaddsub2d 11838	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽) ↔ (𝑗 · 𝑇) ≤ ((𝑉‘𝐽) − (𝑄‘0))))
117	109, 116	mpbid 231	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝑗 · 𝑇) ≤ ((𝑉‘𝐽) − (𝑄‘0)))
118		simplr 768	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → 𝑗 ∈ ℝ)
119	57	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑉‘𝐽) − (𝑄‘0)) ∈ ℝ)
120	81	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → 𝑇 ∈ ℝ⁺)
121	118, 119, 120	lemuldivd 13089	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑗 · 𝑇) ≤ ((𝑉‘𝐽) − (𝑄‘0)) ↔ 𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)))
122	117, 121	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → 𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
123	108, 122	sylanl2 680	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → 𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
124	100, 101, 107, 123	syl21anc 837	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
125	124	ralrimiva 3141	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
126		breq2 5146	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → (𝑗 ≤ 𝑏 ↔ 𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)))
127	126	ralbidv 3172	. . . . . . . . . . . . 13 ⊢ (𝑏 = (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → (∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏 ↔ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)))
128	127	rspcev 3607	. . . . . . . . . . . 12 ⊢ (((((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∈ ℝ ∧ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏)
129	68, 125, 128	syl2anc 583	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏)
130		suprzcl 12664	. . . . . . . . . . 11 ⊢ (({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ ∧ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ∧ ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏) → sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)})
131	16, 99, 129, 130	syl3anc 1369	. . . . . . . . . 10 ⊢ (𝜑 → sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)})
132	14, 131	eqeltrid 2832	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)})
133		oveq1 7421	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝐿 → (𝑘 · 𝑇) = (𝐿 · 𝑇))
134	133	oveq2d 7430	. . . . . . . . . . 11 ⊢ (𝑘 = 𝐿 → ((𝑄‘0) + (𝑘 · 𝑇)) = ((𝑄‘0) + (𝐿 · 𝑇)))
135	134	breq1d 5152	. . . . . . . . . 10 ⊢ (𝑘 = 𝐿 → (((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
136	135	elrab 3680	. . . . . . . . 9 ⊢ (𝐿 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ (𝐿 ∈ ℤ ∧ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
137	132, 136	sylib 217	. . . . . . . 8 ⊢ (𝜑 → (𝐿 ∈ ℤ ∧ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
138	137	simprd 495	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
139		fveq2 6891	. . . . . . . . . 10 ⊢ (𝑗 = 0 → (𝑄‘𝑗) = (𝑄‘0))
140	139	oveq1d 7429	. . . . . . . . 9 ⊢ (𝑗 = 0 → ((𝑄‘𝑗) + (𝐿 · 𝑇)) = ((𝑄‘0) + (𝐿 · 𝑇)))
141	140	breq1d 5152	. . . . . . . 8 ⊢ (𝑗 = 0 → (((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
142	141	elrab 3680	. . . . . . 7 ⊢ (0 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ (0 ∈ (0..^𝑀) ∧ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
143	13, 138, 142	sylanbrc 582	. . . . . 6 ⊢ (𝜑 → 0 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
144		ne0i 4330	. . . . . 6 ⊢ (0 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
145	143, 144	syl 17	. . . . 5 ⊢ (𝜑 → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
146	9	nnred 12249	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℝ)
147	2	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ (0..^𝑀))
148	147	sselda 3978	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝑘 ∈ (0..^𝑀))
149		elfzoelz 13656	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0..^𝑀) → 𝑘 ∈ ℤ)
150	149	zred 12688	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0..^𝑀) → 𝑘 ∈ ℝ)
151	150	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑘 ∈ ℝ)
152	146	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑀 ∈ ℝ)
153		elfzolt2 13665	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0..^𝑀) → 𝑘 < 𝑀)
154	153	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑘 < 𝑀)
155	151, 152, 154	ltled 11384	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑘 ≤ 𝑀)
156	148, 155	syldan 590	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝑘 ≤ 𝑀)
157	156	ralrimiva 3141	. . . . . 6 ⊢ (𝜑 → ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑀)
158		breq2 5146	. . . . . . . 8 ⊢ (𝑏 = 𝑀 → (𝑘 ≤ 𝑏 ↔ 𝑘 ≤ 𝑀))
159	158	ralbidv 3172	. . . . . . 7 ⊢ (𝑏 = 𝑀 → (∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏 ↔ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑀))
160	159	rspcev 3607	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑀) → ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏)
161	146, 157, 160	syl2anc 583	. . . . 5 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏)
162		suprzcl 12664	. . . . 5 ⊢ (({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ ∧ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ∧ ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏) → sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
163	7, 145, 161, 162	syl3anc 1369	. . . 4 ⊢ (𝜑 → sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
164	2, 163	sselid 3976	. . 3 ⊢ (𝜑 → sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ (0..^𝑀))
165	1, 164	eqeltrid 2832	. 2 ⊢ (𝜑 → 𝐼 ∈ (0..^𝑀))
166	15, 131	sselid 3976	. . 3 ⊢ (𝜑 → sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ ℤ)
167	14, 166	eqeltrid 2832	. 2 ⊢ (𝜑 → 𝐿 ∈ ℤ)
168	3, 165	sselid 3976	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ (0...𝑀))
169	50, 168	ffvelcdmd 7089	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝐼) ∈ ℝ)
170	167	zred 12688	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ ℝ)
171	170, 62	remulcld 11266	. . . . . . . . 9 ⊢ (𝜑 → (𝐿 · 𝑇) ∈ ℝ)
172	169, 171	readdcld 11265	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ∈ ℝ)
173	172	rexrd 11286	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ∈ ℝ^*)
174	173	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ∈ ℝ^*)
175		fzofzp1 13753	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (0..^𝑀) → (𝐼 + 1) ∈ (0...𝑀))
176	165, 175	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼 + 1) ∈ (0...𝑀))
177	50, 176	ffvelcdmd 7089	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ)
178	177, 171	readdcld 11265	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
179	178	rexrd 11286	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ^*)
180	179	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ^*)
181		elioore 13378	. . . . . . 7 ⊢ (𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) → 𝑥 ∈ ℝ)
182	181	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 ∈ ℝ)
183	172	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ∈ ℝ)
184	44	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘𝐽) ∈ ℝ)
185	1, 163	eqeltrid 2832	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
186		fveq2 6891	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐼 → (𝑄‘𝑗) = (𝑄‘𝐼))
187	186	oveq1d 7429	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝐼 → ((𝑄‘𝑗) + (𝐿 · 𝑇)) = ((𝑄‘𝐼) + (𝐿 · 𝑇)))
188	187	breq1d 5152	. . . . . . . . . . 11 ⊢ (𝑗 = 𝐼 → (((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
189	188	elrab 3680	. . . . . . . . . 10 ⊢ (𝐼 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ (𝐼 ∈ (0..^𝑀) ∧ ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
190	185, 189	sylib 217	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 ∈ (0..^𝑀) ∧ ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
191	190	simprd 495	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
192	191	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
193	184	rexrd 11286	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘𝐽) ∈ ℝ^*)
194		fzofzp1 13753	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
195	40, 194	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
196	39, 195	ffvelcdmd 7089	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ∈ 𝐻)
197	27, 196	sseldd 3979	. . . . . . . . . 10 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ∈ ℝ)
198	197	rexrd 11286	. . . . . . . . 9 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ∈ ℝ^*)
199	198	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘(𝐽 + 1)) ∈ ℝ^*)
200		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))))
201		ioogtlb 44803	. . . . . . . 8 ⊢ (((𝑉‘𝐽) ∈ ℝ^* ∧ (𝑉‘(𝐽 + 1)) ∈ ℝ^* ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘𝐽) < 𝑥)
202	193, 199, 200, 201	syl3anc 1369	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘𝐽) < 𝑥)
203	183, 184, 182, 192, 202	lelttrd 11394	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝐼) + (𝐿 · 𝑇)) < 𝑥)
204		zssre 12587	. . . . . . . . . . . . . . . 16 ⊢ ℤ ⊆ ℝ
205	15, 204	sstri 3987	. . . . . . . . . . . . . . 15 ⊢ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ
206	205	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ)
207	99	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
208	129	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏)
209	167	peano2zd 12691	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐿 + 1) ∈ ℤ)
210	209	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐿 + 1) ∈ ℤ)
211		oveq1 7421	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐼 = (𝑀 − 1) → (𝐼 + 1) = ((𝑀 − 1) + 1))
212	146	recnd 11264	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑀 ∈ ℂ)
213		1cnd 11231	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 ∈ ℂ)
214	212, 213	npcand 11597	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
215	211, 214	sylan9eqr 2789	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝐼 + 1) = 𝑀)
216	215	fveq2d 6895	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑄‘(𝐼 + 1)) = (𝑄‘𝑀))
217	47	simprd 495	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
218	217	simpld 494	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
219	218	simprd 495	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
220	219	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑄‘𝑀) = 𝐵)
221	59	recnd 11264	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐵 ∈ ℂ)
222	60	recnd 11264	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐴 ∈ ℂ)
223	221, 222	npcand 11597	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐵 − 𝐴) + 𝐴) = 𝐵)
224	223	eqcomd 2733	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐵 = ((𝐵 − 𝐴) + 𝐴))
225	28	eqcomi 2736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐵 − 𝐴) = 𝑇
226	225	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐵 − 𝐴) = 𝑇)
227	226	oveq1d 7429	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐵 − 𝐴) + 𝐴) = (𝑇 + 𝐴))
228	218	simpld 494	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
229	228	eqcomd 2733	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐴 = (𝑄‘0))
230	229	oveq2d 7430	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑇 + 𝐴) = (𝑇 + (𝑄‘0)))
231	224, 227, 230	3eqtrd 2771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐵 = (𝑇 + (𝑄‘0)))
232	231	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → 𝐵 = (𝑇 + (𝑄‘0)))
233	216, 220, 232	3eqtrd 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑄‘(𝐼 + 1)) = (𝑇 + (𝑄‘0)))
234	62	recnd 11264	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑇 ∈ ℂ)
235	228, 222	eqeltrd 2828	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑄‘0) ∈ ℂ)
236	234, 235	addcomd 11438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑇 + (𝑄‘0)) = ((𝑄‘0) + 𝑇))
237	236	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑇 + (𝑄‘0)) = ((𝑄‘0) + 𝑇))
238	233, 237	eqtrd 2767	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑄‘(𝐼 + 1)) = ((𝑄‘0) + 𝑇))
239	238	oveq1d 7429	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (((𝑄‘0) + 𝑇) + (𝐿 · 𝑇)))
240	171	recnd 11264	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 · 𝑇) ∈ ℂ)
241	235, 234, 240	addassd 11258	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝑄‘0) + 𝑇) + (𝐿 · 𝑇)) = ((𝑄‘0) + (𝑇 + (𝐿 · 𝑇))))
242	234	mullidd 11254	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (1 · 𝑇) = 𝑇)
243	242, 234	eqeltrd 2828	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 · 𝑇) ∈ ℂ)
244	243, 240	addcomd 11438	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1 · 𝑇) + (𝐿 · 𝑇)) = ((𝐿 · 𝑇) + (1 · 𝑇)))
245	242	eqcomd 2733	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑇 = (1 · 𝑇))
246	245	oveq1d 7429	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑇 + (𝐿 · 𝑇)) = ((1 · 𝑇) + (𝐿 · 𝑇)))
247	170	recnd 11264	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐿 ∈ ℂ)
248	247, 213, 234	adddird 11261	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝐿 + 1) · 𝑇) = ((𝐿 · 𝑇) + (1 · 𝑇)))
249	244, 246, 248	3eqtr4d 2777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑇 + (𝐿 · 𝑇)) = ((𝐿 + 1) · 𝑇))
250	249	oveq2d 7430	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑄‘0) + (𝑇 + (𝐿 · 𝑇))) = ((𝑄‘0) + ((𝐿 + 1) · 𝑇)))
251	241, 250	eqtrd 2767	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑄‘0) + 𝑇) + (𝐿 · 𝑇)) = ((𝑄‘0) + ((𝐿 + 1) · 𝑇)))
252	251	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (((𝑄‘0) + 𝑇) + (𝐿 · 𝑇)) = ((𝑄‘0) + ((𝐿 + 1) · 𝑇)))
253	239, 252	eqtr2d 2768	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
254	253	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
255		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
256	254, 255	eqbrtrd 5164	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) ≤ (𝑉‘𝐽))
257		oveq1 7421	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (𝐿 + 1) → (𝑘 · 𝑇) = ((𝐿 + 1) · 𝑇))
258	257	oveq2d 7430	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (𝐿 + 1) → ((𝑄‘0) + (𝑘 · 𝑇)) = ((𝑄‘0) + ((𝐿 + 1) · 𝑇)))
259	258	breq1d 5152	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝐿 + 1) → (((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) ≤ (𝑉‘𝐽)))
260	259	elrab 3680	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 + 1) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ ((𝐿 + 1) ∈ ℤ ∧ ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) ≤ (𝑉‘𝐽)))
261	210, 256, 260	sylanbrc 582	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐿 + 1) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)})
262		suprub 12197	. . . . . . . . . . . . . 14 ⊢ ((({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ ∧ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ∧ ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏) ∧ (𝐿 + 1) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → (𝐿 + 1) ≤ sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ))
263	206, 207, 208, 261, 262	syl31anc 1371	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐿 + 1) ≤ sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ))
264	263, 14	breqtrrdi 5184	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐿 + 1) ≤ 𝐿)
265	170	ltp1d 12166	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 < (𝐿 + 1))
266		peano2re 11409	. . . . . . . . . . . . . . . 16 ⊢ (𝐿 ∈ ℝ → (𝐿 + 1) ∈ ℝ)
267	170, 266	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐿 + 1) ∈ ℝ)
268	170, 267	ltnled 11383	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 < (𝐿 + 1) ↔ ¬ (𝐿 + 1) ≤ 𝐿))
269	265, 268	mpbid 231	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ (𝐿 + 1) ≤ 𝐿)
270	269	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ¬ (𝐿 + 1) ≤ 𝐿)
271	264, 270	pm2.65da 816	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → ¬ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
272	5, 165	sselid 3976	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐼 ∈ ℤ)
273	272	zred 12688	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐼 ∈ ℝ)
274	273	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → 𝐼 ∈ ℝ)
275		peano2rem 11549	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℝ → (𝑀 − 1) ∈ ℝ)
276	146, 275	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 − 1) ∈ ℝ)
277	276	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → (𝑀 − 1) ∈ ℝ)
278		elfzolt2 13665	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 ∈ (0..^𝑀) → 𝐼 < 𝑀)
279		elfzoelz 13656	. . . . . . . . . . . . . . . . 17 ⊢ (𝐼 ∈ (0..^𝑀) → 𝐼 ∈ ℤ)
280		elfzoel2 13655	. . . . . . . . . . . . . . . . 17 ⊢ (𝐼 ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
281		zltlem1 12637	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐼 < 𝑀 ↔ 𝐼 ≤ (𝑀 − 1)))
282	279, 280, 281	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 ∈ (0..^𝑀) → (𝐼 < 𝑀 ↔ 𝐼 ≤ (𝑀 − 1)))
283	278, 282	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (𝐼 ∈ (0..^𝑀) → 𝐼 ≤ (𝑀 − 1))
284	165, 283	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐼 ≤ (𝑀 − 1))
285	284	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → 𝐼 ≤ (𝑀 − 1))
286		neqne 2943	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝐼 = (𝑀 − 1) → 𝐼 ≠ (𝑀 − 1))
287	286	necomd 2991	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐼 = (𝑀 − 1) → (𝑀 − 1) ≠ 𝐼)
288	287	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → (𝑀 − 1) ≠ 𝐼)
289	274, 277, 285, 288	leneltd 11390	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → 𝐼 < (𝑀 − 1))
290	6, 204	sstri 3987	. . . . . . . . . . . . . . . 16 ⊢ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ
291	290	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ)
292	145	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
293	161	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏)
294	176	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝐼 + 1) ∈ (0...𝑀))
295	273	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → 𝐼 ∈ ℝ)
296	276	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝑀 − 1) ∈ ℝ)
297		1red 11237	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → 1 ∈ ℝ)
298		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → 𝐼 < (𝑀 − 1))
299	295, 296, 297, 298	ltadd1dd 11847	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝐼 + 1) < ((𝑀 − 1) + 1))
300	214	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → ((𝑀 − 1) + 1) = 𝑀)
301	299, 300	breqtrd 5168	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝐼 + 1) < 𝑀)
302		elfzfzo 44581	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 + 1) ∈ (0..^𝑀) ↔ ((𝐼 + 1) ∈ (0...𝑀) ∧ (𝐼 + 1) < 𝑀))
303	294, 301, 302	sylanbrc 582	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝐼 + 1) ∈ (0..^𝑀))
304	303	anim1i 614	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝐼 + 1) ∈ (0..^𝑀) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
305		fveq2 6891	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝐼 + 1) → (𝑄‘𝑗) = (𝑄‘(𝐼 + 1)))
306	305	oveq1d 7429	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝐼 + 1) → ((𝑄‘𝑗) + (𝐿 · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
307	306	breq1d 5152	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝐼 + 1) → (((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
308	307	elrab 3680	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 + 1) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ ((𝐼 + 1) ∈ (0..^𝑀) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
309	304, 308	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐼 + 1) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
310		suprub 12197	. . . . . . . . . . . . . . 15 ⊢ ((({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ ∧ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ∧ ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏) ∧ (𝐼 + 1) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}) → (𝐼 + 1) ≤ sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ))
311	291, 292, 293, 309, 310	syl31anc 1371	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐼 + 1) ≤ sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ))
312	311, 1	breqtrrdi 5184	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐼 + 1) ≤ 𝐼)
313	273	ltp1d 12166	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐼 < (𝐼 + 1))
314		peano2re 11409	. . . . . . . . . . . . . . . . 17 ⊢ (𝐼 ∈ ℝ → (𝐼 + 1) ∈ ℝ)
315	273, 314	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐼 + 1) ∈ ℝ)
316	273, 315	ltnled 11383	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐼 < (𝐼 + 1) ↔ ¬ (𝐼 + 1) ≤ 𝐼))
317	313, 316	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (𝐼 + 1) ≤ 𝐼)
318	317	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ¬ (𝐼 + 1) ≤ 𝐼)
319	312, 318	pm2.65da 816	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → ¬ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
320	289, 319	syldan 590	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → ¬ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
321	271, 320	pm2.61dan 812	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
322	44, 178	ltnled 11383	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ↔ ¬ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
323	321, 322	mpbird 257	. . . . . . . . 9 ⊢ (𝜑 → (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
324	197	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ∈ ℝ)
325	19	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐷 ∈ ℝ)
326	178	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
327	18	rexrd 11286	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
328	19	rexrd 11286	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷 ∈ ℝ^*)
329	18, 19, 31	ltled 11384	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐶 ≤ 𝐷)
330		lbicc2 13465	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷) → 𝐶 ∈ (𝐶[,]𝐷))
331	327, 328, 329, 330	syl3anc 1369	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐶 ∈ (𝐶[,]𝐷))
332		ubicc2 13466	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷) → 𝐷 ∈ (𝐶[,]𝐷))
333	327, 328, 329, 332	syl3anc 1369	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 ∈ (𝐶[,]𝐷))
334	331, 333	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)))
335		prssg 4818	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷)))
336	18, 19, 335	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷)))
337	334, 336	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ (𝐶[,]𝐷))
338	337, 23	unssd 4182	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ (𝐶[,]𝐷))
339	17, 338	eqsstrid 4026	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻 ⊆ (𝐶[,]𝐷))
340	339, 196	sseldd 3979	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ∈ (𝐶[,]𝐷))
341		iccleub 13403	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ (𝑉‘(𝐽 + 1)) ∈ (𝐶[,]𝐷)) → (𝑉‘(𝐽 + 1)) ≤ 𝐷)
342	327, 328, 340, 341	syl3anc 1369	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ≤ 𝐷)
343	342	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ 𝐷)
344		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
345	324, 325, 326, 343, 344	letrd 11393	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
346	345	adantlr 714	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
347		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
348	178	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
349	19	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐷 ∈ ℝ)
350	348, 349	ltnled 11383	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷 ↔ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
351	347, 350	mpbird 257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷)
352	351	adantlr 714	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷)
353		simpll 766	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
354		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
355	178	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
356	197	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ∈ ℝ)
357	355, 356	ltnled 11383	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)) ↔ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
358	354, 357	mpbird 257	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)))
359	358	ad4ant14 751	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)))
360	18	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → 𝐶 ∈ ℝ)
361	19	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → 𝐷 ∈ ℝ)
362	178	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
363	18	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐶 ∈ ℝ)
364	178	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
365	44	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) ∈ ℝ)
366	339, 43	sseldd 3979	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑉‘𝐽) ∈ (𝐶[,]𝐷))
367		iccgelb 13404	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ (𝑉‘𝐽) ∈ (𝐶[,]𝐷)) → 𝐶 ≤ (𝑉‘𝐽))
368	327, 328, 366, 367	syl3anc 1369	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐶 ≤ (𝑉‘𝐽))
369	368	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐶 ≤ (𝑉‘𝐽))
370		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
371	363, 365, 364, 369, 370	lelttrd 11394	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐶 < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
372	363, 364, 371	ltled 11384	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐶 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
373	372	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → 𝐶 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
374	178	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
375	19	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → 𝐷 ∈ ℝ)
376		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷)
377	374, 375, 376	ltled 11384	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ 𝐷)
378	377	adantlr 714	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ 𝐷)
379	360, 361, 362, 373, 378	eliccd 44812	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ (𝐶[,]𝐷))
380	167	znegcld 12690	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → -𝐿 ∈ ℤ)
381	247, 234	mulneg1d 11689	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (-𝐿 · 𝑇) = -(𝐿 · 𝑇))
382	381	oveq2d 7430	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)) = (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + -(𝐿 · 𝑇)))
383	178	recnd 11264	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℂ)
384	383, 240	negsubd 11599	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + -(𝐿 · 𝑇)) = (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) − (𝐿 · 𝑇)))
385	177	recnd 11264	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℂ)
386	385, 240	pncand 11594	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) − (𝐿 · 𝑇)) = (𝑄‘(𝐼 + 1)))
387	382, 384, 386	3eqtrd 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)) = (𝑄‘(𝐼 + 1)))
388		ffn 6716	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
389	50, 388	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
390		fnfvelrn 7084	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 Fn (0...𝑀) ∧ (𝐼 + 1) ∈ (0...𝑀)) → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
391	389, 176, 390	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
392	387, 391	eqeltrd 2828	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)) ∈ ran 𝑄)
393		oveq1 7421	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = -𝐿 → (𝑘 · 𝑇) = (-𝐿 · 𝑇))
394	393	oveq2d 7430	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = -𝐿 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) = (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)))
395	394	eleq1d 2813	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = -𝐿 → ((((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)) ∈ ran 𝑄))
396	395	rspcev 3607	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-𝐿 ∈ ℤ ∧ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
397	380, 392, 396	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
398	397	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
399		oveq1 7421	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → (𝑦 + (𝑘 · 𝑇)) = (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)))
400	399	eleq1d 2813	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
401	400	rexbidv 3173	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
402	401	elrab 3680	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} ↔ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
403	379, 398, 402	sylanbrc 582	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
404		elun2 4173	. . . . . . . . . . . . . . . 16 ⊢ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
405	403, 404	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
406	17	eqcomi 2736	. . . . . . . . . . . . . . 15 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = 𝐻
407	405, 406	eleqtrdi 2838	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻)
408	407	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻)
409		f1ofo 6840	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑉:(0...𝑁)–1-1-onto→𝐻 → 𝑉:(0...𝑁)–onto→𝐻)
410	36, 37, 409	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑉:(0...𝑁)–onto→𝐻)
411		foelrn 7111	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑉:(0...𝑁)–onto→𝐻 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
412	410, 411	sylan 579	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
413		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
414	413	eqcomd 2733	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗) → (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
415	414	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗) → (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
416	415	reximdv 3165	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → (∃𝑗 ∈ (0...𝑁)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗) → ∃𝑗 ∈ (0...𝑁)(𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
417	412, 416	mpd 15	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
418	417	ad4ant14 751	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
419		simpl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
420	413	eqcoms 2735	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
421	420	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
422	419, 421	breqtrd 5168	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) < (𝑉‘𝑗))
423	422	adantll 713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) < (𝑉‘𝑗))
424	423	adantlr 714	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) < (𝑉‘𝑗))
425	36	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑉 Isom < , < ((0...𝑁), 𝐻))
426	42	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐽 ∈ (0...𝑁))
427		simplr 768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑗 ∈ (0...𝑁))
428		isorel 7328	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑉 Isom < , < ((0...𝑁), 𝐻) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) → (𝐽 < 𝑗 ↔ (𝑉‘𝐽) < (𝑉‘𝑗)))
429	425, 426, 427, 428	syl12anc 836	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝐽 < 𝑗 ↔ (𝑉‘𝐽) < (𝑉‘𝑗)))
430	424, 429	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐽 < 𝑗)
431	430	adantllr 718	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐽 < 𝑗)
432		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
433		simpl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)))
434	432, 433	eqbrtrd 5164	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝑗) < (𝑉‘(𝐽 + 1)))
435	434	adantll 713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝑗) < (𝑉‘(𝐽 + 1)))
436	435	adantlr 714	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝑗) < (𝑉‘(𝐽 + 1)))
437	36	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑉 Isom < , < ((0...𝑁), 𝐻))
438		simplr 768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑗 ∈ (0...𝑁))
439	195	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝐽 + 1) ∈ (0...𝑁))
440		isorel 7328	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑉 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝑗 < (𝐽 + 1) ↔ (𝑉‘𝑗) < (𝑉‘(𝐽 + 1))))
441	437, 438, 439, 440	syl12anc 836	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑗 < (𝐽 + 1) ↔ (𝑉‘𝑗) < (𝑉‘(𝐽 + 1))))
442	436, 441	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑗 < (𝐽 + 1))
443	442	adantl3r 749	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑗 < (𝐽 + 1))
444	431, 443	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
445	444	ex 412	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))))
446	445	adantlr 714	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))))
447	446	reximdva 3163	. . . . . . . . . . . . . 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 837	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
450		elfzelz 13525	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
451	450	ad2antlr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝑗 ∈ ℤ)
452		elfzelz 13525	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 ∈ (0...𝑁) → 𝐽 ∈ ℤ)
453	42, 452	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐽 ∈ ℤ)
454	453	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝐽 ∈ ℤ)
455		simprl 770	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝐽 < 𝑗)
456		simprr 772	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝑗 < (𝐽 + 1))
457		btwnnz 12660	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ)
458	454, 455, 456, 457	syl3anc 1369	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → ¬ 𝑗 ∈ ℤ)
459	451, 458	pm2.65da 816	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ¬ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
460	459	nrexdv 3144	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
461	460	ad3antrrr 729	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ¬ ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
462	449, 461	condan 817	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
463	352, 462	syldan 590	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
464	346, 463	pm2.61dan 812	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
465	323, 464	mpdan 686	. . . . . . . 8 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
466	465	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
467	182	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑥 ∈ ℝ)
468	197	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ∈ ℝ)
469	178	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
470		iooltub 44818	. . . . . . . . . 10 ⊢ (((𝑉‘𝐽) ∈ ℝ^* ∧ (𝑉‘(𝐽 + 1)) ∈ ℝ^* ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 < (𝑉‘(𝐽 + 1)))
471	193, 199, 200, 470	syl3anc 1369	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 < (𝑉‘(𝐽 + 1)))
472	471	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑥 < (𝑉‘(𝐽 + 1)))
473		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
474	467, 468, 469, 472, 473	ltletrd 11396	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑥 < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
475	466, 474	mpdan 686	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
476	174, 180, 182, 203, 475	eliood 44806	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 ∈ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
477	476	ralrimiva 3141	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))𝑥 ∈ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
478		dfss3 3966	. . . 4 ⊢ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ↔ ∀𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))𝑥 ∈ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
479	477, 478	sylibr 233	. . 3 ⊢ (𝜑 → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
480		fveq2 6891	. . . . . . 7 ⊢ (𝑖 = 𝐼 → (𝑄‘𝑖) = (𝑄‘𝐼))
481	480	oveq1d 7429	. . . . . 6 ⊢ (𝑖 = 𝐼 → ((𝑄‘𝑖) + (𝑙 · 𝑇)) = ((𝑄‘𝐼) + (𝑙 · 𝑇)))
482		oveq1 7421	. . . . . . . 8 ⊢ (𝑖 = 𝐼 → (𝑖 + 1) = (𝐼 + 1))
483	482	fveq2d 6895	. . . . . . 7 ⊢ (𝑖 = 𝐼 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝐼 + 1)))
484	483	oveq1d 7429	. . . . . 6 ⊢ (𝑖 = 𝐼 → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇)))
485	481, 484	oveq12d 7432	. . . . 5 ⊢ (𝑖 = 𝐼 → (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) = (((𝑄‘𝐼) + (𝑙 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇))))
486	485	sseq2d 4010	. . . 4 ⊢ (𝑖 = 𝐼 → (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) ↔ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝑙 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇)))))
487		oveq1 7421	. . . . . . 7 ⊢ (𝑙 = 𝐿 → (𝑙 · 𝑇) = (𝐿 · 𝑇))
488	487	oveq2d 7430	. . . . . 6 ⊢ (𝑙 = 𝐿 → ((𝑄‘𝐼) + (𝑙 · 𝑇)) = ((𝑄‘𝐼) + (𝐿 · 𝑇)))
489	487	oveq2d 7430	. . . . . 6 ⊢ (𝑙 = 𝐿 → ((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
490	488, 489	oveq12d 7432	. . . . 5 ⊢ (𝑙 = 𝐿 → (((𝑄‘𝐼) + (𝑙 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇))) = (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
491	490	sseq2d 4010	. . . 4 ⊢ (𝑙 = 𝐿 → (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝑙 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇))) ↔ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))))
492	486, 491	rspc2ev 3620	. . 3 ⊢ ((𝐼 ∈ (0..^𝑀) ∧ 𝐿 ∈ ℤ ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))) → ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
493	165, 167, 479, 492	syl3anc 1369	. 2 ⊢ (𝜑 → ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
494	165, 167, 493	jca31 514	1 ⊢ (𝜑 → ((𝐼 ∈ (0..^𝑀) ∧ 𝐿 ∈ ℤ) ∧ ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1534 ∈ wcel 2099 ≠ wne 2935 ∀wral 3056 ∃wrex 3065 {crab 3427 ∪ cun 3942 ⊆ wss 3944 ∅c0 4318 {cpr 4626 class class class wbr 5142 ↦ cmpt 5225 ran crn 5673 ℩cio 6492 Fn wfn 6537 ⟶wf 6538 –onto→wfo 6540 –1-1-onto→wf1o 6541 ‘cfv 6542 Isom wiso 6543 (class class class)co 7414 ↑_m cmap 8836 supcsup 9455 ℂcc 11128 ℝcr 11129 0cc0 11130 1c1 11131 + caddc 11133 · cmul 11135 ℝ^*cxr 11269 < clt 11270 ≤ cle 11271 − cmin 11466 -cneg 11467 / cdiv 11893 ℕcn 12234 ℕ₀cn0 12494 ℤcz 12580 ℤ_≥cuz 12844 ℝ⁺crp 12998 (,)cioo 13348 [,]cicc 13351 ...cfz 13508 ..^cfzo 13651 ♯chash 14313

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2164 ax-ext 2698 ax-rep 5279 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7734 ax-inf2 9656 ax-cnex 11186 ax-resscn 11187 ax-1cn 11188 ax-icn 11189 ax-addcl 11190 ax-addrcl 11191 ax-mulcl 11192 ax-mulrcl 11193 ax-mulcom 11194 ax-addass 11195 ax-mulass 11196 ax-distr 11197 ax-i2m1 11198 ax-1ne0 11199 ax-1rid 11200 ax-rnegex 11201 ax-rrecex 11202 ax-cnre 11203 ax-pre-lttri 11204 ax-pre-lttrn 11205 ax-pre-ltadd 11206 ax-pre-mulgt0 11207 ax-pre-sup 11208

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ne 2936 df-nel 3042 df-ral 3057 df-rex 3066 df-rmo 3371 df-reu 3372 df-rab 3428 df-v 3471 df-sbc 3775 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-int 4945 df-iun 4993 df-iin 4994 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-se 5628 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-isom 6551 df-riota 7370 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7865 df-1st 7987 df-2nd 7988 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-oadd 8484 df-er 8718 df-map 8838 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-fi 9426 df-sup 9457 df-inf 9458 df-oi 9525 df-dju 9916 df-card 9954 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11468 df-neg 11469 df-div 11894 df-nn 12235 df-2 12297 df-3 12298 df-n0 12495 df-xnn0 12567 df-z 12581 df-uz 12845 df-q 12955 df-rp 12999 df-xneg 13116 df-xadd 13117 df-xmul 13118 df-ioo 13352 df-icc 13355 df-fz 13509 df-fzo 13652 df-seq 13991 df-exp 14051 df-hash 14314 df-cj 15070 df-re 15071 df-im 15072 df-sqrt 15206 df-abs 15207 df-rest 17395 df-topgen 17416 df-psmet 21258 df-xmet 21259 df-met 21260 df-bl 21261 df-mopn 21262 df-top 22783 df-topon 22800 df-bases 22836 df-cld 22910 df-ntr 22911 df-cls 22912 df-nei 22989 df-lp 23027 df-cmp 23278

This theorem is referenced by: fourierdlem97 45514

W3C validator