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 44056

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 4025	. . . 4 ⊢ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ (0..^𝑀)
3		fzossfz 13507	. . . . . . . 8 ⊢ (0..^𝑀) ⊆ (0...𝑀)
4		fzssz 13359	. . . . . . . 8 ⊢ (0...𝑀) ⊆ ℤ
5	3, 4	sstri 3941	. . . . . . 7 ⊢ (0..^𝑀) ⊆ ℤ
6	2, 5	sstri 3941	. . . . . 6 ⊢ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ
7	6	a1i 11	. . . . 5 ⊢ (𝜑 → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ)
8		0zd 12432	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℤ)
9		fourierdlem64.m	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
10	9	nnzd 12526	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
11	9	nngt0d 12123	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝑀)
12		fzolb 13494	. . . . . . . 8 ⊢ (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
13	8, 10, 11, 12	syl3anbrc 1342	. . . . . . 7 ⊢ (𝜑 → 0 ∈ (0..^𝑀))
14		fourierdlem64.l	. . . . . . . . . 10 ⊢ 𝐿 = sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < )
15		ssrab2 4025	. . . . . . . . . . . 12 ⊢ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ
16	15	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ)
17		fourierdlem64.h	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
18		fourierdlem64.c	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐶 ∈ ℝ)
19		fourierdlem64.d	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 ∈ ℝ)
20		prssi 4768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → {𝐶, 𝐷} ⊆ ℝ)
21	18, 19, 20	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ ℝ)
22		ssrab2 4025	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷)
23	22	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷))
24	18, 19	iccssred 13267	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐶[,]𝐷) ⊆ ℝ)
25	23, 24	sstrd 3942	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ ℝ)
26	21, 25	unssd 4133	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ ℝ)
27	17, 26	eqsstrid 3980	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻 ⊆ ℝ)
28		fourierdlem64.t	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑇 = (𝐵 − 𝐴)
29		fourierdlem64.p	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
30		fourierdlem64.q	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
31		fourierdlem64.cltd	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐶 < 𝐷)
32		eqid 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
33		fourierdlem64.n	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑁 = ((♯‘𝐻) − 1)
34		fourierdlem64.v	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑉 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
35	28, 29, 9, 30, 18, 19, 31, 32, 17, 33, 34	fourierdlem54 44046	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑉 ∈ ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑁)) ∧ 𝑉 Isom < , < ((0...𝑁), 𝐻)))
36	35	simprd 496	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑉 Isom < , < ((0...𝑁), 𝐻))
37		isof1o 7250	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑉 Isom < , < ((0...𝑁), 𝐻) → 𝑉:(0...𝑁)–1-1-onto→𝐻)
38		f1of 6767	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑉:(0...𝑁)–1-1-onto→𝐻 → 𝑉:(0...𝑁)⟶𝐻)
39	36, 37, 38	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑉:(0...𝑁)⟶𝐻)
40		fourierdlem64.j	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
41		elfzofz 13504	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
42	40, 41	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐽 ∈ (0...𝑁))
43	39, 42	ffvelcdmd 7018	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑉‘𝐽) ∈ 𝐻)
44	27, 43	sseldd 3933	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑉‘𝐽) ∈ ℝ)
45	29	fourierdlem2 43995	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
46	9, 45	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
47	30, 46	mpbid 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
48	47	simpld 495	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
49		elmapi 8708	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
50	48, 49	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
51	9	nnnn0d 12394	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
52		nn0uz 12721	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ₀ = (ℤ_≥‘0)
53	51, 52	eleqtrdi 2847	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
54		eluzfz1 13364	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 ∈ (0...𝑀))
56	50, 55	ffvelcdmd 7018	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
57	44, 56	resubcld 11504	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑉‘𝐽) − (𝑄‘0)) ∈ ℝ)
58	29, 9, 30	fourierdlem11 44004	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
59	58	simp2d 1142	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ)
60	58	simp1d 1141	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℝ)
61	59, 60	resubcld 11504	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
62	28, 61	eqeltrid 2841	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ∈ ℝ)
63	58	simp3d 1143	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 < 𝐵)
64	60, 59	posdifd 11663	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
65	63, 64	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
66	65, 28	breqtrrdi 5134	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝑇)
67	66	gt0ne0d 11640	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ≠ 0)
68	57, 62, 67	redivcld 11904	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∈ ℝ)
69		btwnz 12524	. . . . . . . . . . . . . . 15 ⊢ ((((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∈ ℝ → (∃𝑘 ∈ ℤ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∧ ∃𝑧 ∈ ℤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) < 𝑧))
70	68, 69	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑘 ∈ ℤ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∧ ∃𝑧 ∈ ℤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) < 𝑧))
71	70	simpld 495	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∃𝑘 ∈ ℤ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
72		zre 12424	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℝ)
73	56	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (𝑄‘0) ∈ ℝ)
74		simplr 766	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → 𝑘 ∈ ℝ)
75	62	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → 𝑇 ∈ ℝ)
76	74, 75	remulcld 11106	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (𝑘 · 𝑇) ∈ ℝ)
77	73, 76	readdcld 11105	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑄‘0) + (𝑘 · 𝑇)) ∈ ℝ)
78	44	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (𝑉‘𝐽) ∈ ℝ)
79		simpr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
80	57	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑉‘𝐽) − (𝑄‘0)) ∈ ℝ)
81	62, 66	elrpd 12870	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑇 ∈ ℝ⁺)
82	81	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → 𝑇 ∈ ℝ⁺)
83	74, 80, 82	ltmuldivd 12920	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑘 · 𝑇) < ((𝑉‘𝐽) − (𝑄‘0)) ↔ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)))
84	79, 83	mpbird 256	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (𝑘 · 𝑇) < ((𝑉‘𝐽) − (𝑄‘0)))
85	56	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (𝑄‘0) ∈ ℝ)
86		simpr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → 𝑘 ∈ ℝ)
87	62	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → 𝑇 ∈ ℝ)
88	86, 87	remulcld 11106	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (𝑘 · 𝑇) ∈ ℝ)
89	44	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (𝑉‘𝐽) ∈ ℝ)
90	85, 88, 89	ltaddsub2d 11677	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (((𝑄‘0) + (𝑘 · 𝑇)) < (𝑉‘𝐽) ↔ (𝑘 · 𝑇) < ((𝑉‘𝐽) − (𝑄‘0))))
91	90	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → (((𝑄‘0) + (𝑘 · 𝑇)) < (𝑉‘𝐽) ↔ (𝑘 · 𝑇) < ((𝑉‘𝐽) − (𝑄‘0))))
92	84, 91	mpbird 256	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑄‘0) + (𝑘 · 𝑇)) < (𝑉‘𝐽))
93	77, 78, 92	ltled 11224	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℝ) ∧ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽))
94	93	ex 413	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)))
95	72, 94	sylan2 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)))
96	95	reximdva 3161	. . . . . . . . . . . . 13 ⊢ (𝜑 → (∃𝑘 ∈ ℤ 𝑘 < (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → ∃𝑘 ∈ ℤ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)))
97	71, 96	mpd 15	. . . . . . . . . . . 12 ⊢ (𝜑 → ∃𝑘 ∈ ℤ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽))
98		rabn0 4332	. . . . . . . . . . . 12 ⊢ ({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ↔ ∃𝑘 ∈ ℤ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽))
99	97, 98	sylibr 233	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
100		simpl 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝜑)
101	16	sselda 3932	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝑗 ∈ ℤ)
102		oveq1 7344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑗 → (𝑘 · 𝑇) = (𝑗 · 𝑇))
103	102	oveq2d 7353	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((𝑄‘0) + (𝑘 · 𝑇)) = ((𝑄‘0) + (𝑗 · 𝑇)))
104	103	breq1d 5102	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → (((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)))
105	104	elrab 3634	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ (𝑗 ∈ ℤ ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)))
106	105	simprbi 497	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} → ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽))
107	106	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽))
108		zre 12424	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℤ → 𝑗 ∈ ℝ)
109		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽))
110	56	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝑄‘0) ∈ ℝ)
111		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℝ) → 𝑗 ∈ ℝ)
112	62	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℝ) → 𝑇 ∈ ℝ)
113	111, 112	remulcld 11106	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℝ) → (𝑗 · 𝑇) ∈ ℝ)
114	113	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝑗 · 𝑇) ∈ ℝ)
115	44	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝑉‘𝐽) ∈ ℝ)
116	110, 114, 115	leaddsub2d 11678	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽) ↔ (𝑗 · 𝑇) ≤ ((𝑉‘𝐽) − (𝑄‘0))))
117	109, 116	mpbid 231	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝑗 · 𝑇) ≤ ((𝑉‘𝐽) − (𝑄‘0)))
118		simplr 766	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → 𝑗 ∈ ℝ)
119	57	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑉‘𝐽) − (𝑄‘0)) ∈ ℝ)
120	81	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → 𝑇 ∈ ℝ⁺)
121	118, 119, 120	lemuldivd 12922	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑗 · 𝑇) ≤ ((𝑉‘𝐽) − (𝑄‘0)) ↔ 𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)))
122	117, 121	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ℝ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → 𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
123	108, 122	sylanl2 678	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ ((𝑄‘0) + (𝑗 · 𝑇)) ≤ (𝑉‘𝐽)) → 𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
124	100, 101, 107, 123	syl21anc 835	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
125	124	ralrimiva 3139	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇))
126		breq2 5096	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → (𝑗 ≤ 𝑏 ↔ 𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)))
127	126	ralbidv 3170	. . . . . . . . . . . . 13 ⊢ (𝑏 = (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) → (∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏 ↔ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)))
128	127	rspcev 3570	. . . . . . . . . . . 12 ⊢ (((((𝑉‘𝐽) − (𝑄‘0)) / 𝑇) ∈ ℝ ∧ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ (((𝑉‘𝐽) − (𝑄‘0)) / 𝑇)) → ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏)
129	68, 125, 128	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏)
130		suprzcl 12501	. . . . . . . . . . 11 ⊢ (({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ ∧ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ∧ ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏) → sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)})
131	16, 99, 129, 130	syl3anc 1370	. . . . . . . . . 10 ⊢ (𝜑 → sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)})
132	14, 131	eqeltrid 2841	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)})
133		oveq1 7344	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝐿 → (𝑘 · 𝑇) = (𝐿 · 𝑇))
134	133	oveq2d 7353	. . . . . . . . . . 11 ⊢ (𝑘 = 𝐿 → ((𝑄‘0) + (𝑘 · 𝑇)) = ((𝑄‘0) + (𝐿 · 𝑇)))
135	134	breq1d 5102	. . . . . . . . . 10 ⊢ (𝑘 = 𝐿 → (((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
136	135	elrab 3634	. . . . . . . . 9 ⊢ (𝐿 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ (𝐿 ∈ ℤ ∧ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
137	132, 136	sylib 217	. . . . . . . 8 ⊢ (𝜑 → (𝐿 ∈ ℤ ∧ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
138	137	simprd 496	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
139		fveq2 6825	. . . . . . . . . 10 ⊢ (𝑗 = 0 → (𝑄‘𝑗) = (𝑄‘0))
140	139	oveq1d 7352	. . . . . . . . 9 ⊢ (𝑗 = 0 → ((𝑄‘𝑗) + (𝐿 · 𝑇)) = ((𝑄‘0) + (𝐿 · 𝑇)))
141	140	breq1d 5102	. . . . . . . 8 ⊢ (𝑗 = 0 → (((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
142	141	elrab 3634	. . . . . . 7 ⊢ (0 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ (0 ∈ (0..^𝑀) ∧ ((𝑄‘0) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
143	13, 138, 142	sylanbrc 583	. . . . . 6 ⊢ (𝜑 → 0 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
144		ne0i 4281	. . . . . 6 ⊢ (0 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
145	143, 144	syl 17	. . . . 5 ⊢ (𝜑 → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
146	9	nnred 12089	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℝ)
147	2	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ (0..^𝑀))
148	147	sselda 3932	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝑘 ∈ (0..^𝑀))
149		elfzoelz 13488	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0..^𝑀) → 𝑘 ∈ ℤ)
150	149	zred 12527	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0..^𝑀) → 𝑘 ∈ ℝ)
151	150	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑘 ∈ ℝ)
152	146	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑀 ∈ ℝ)
153		elfzolt2 13497	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0..^𝑀) → 𝑘 < 𝑀)
154	153	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑘 < 𝑀)
155	151, 152, 154	ltled 11224	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑘 ≤ 𝑀)
156	148, 155	syldan 591	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}) → 𝑘 ≤ 𝑀)
157	156	ralrimiva 3139	. . . . . 6 ⊢ (𝜑 → ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑀)
158		breq2 5096	. . . . . . . 8 ⊢ (𝑏 = 𝑀 → (𝑘 ≤ 𝑏 ↔ 𝑘 ≤ 𝑀))
159	158	ralbidv 3170	. . . . . . 7 ⊢ (𝑏 = 𝑀 → (∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏 ↔ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑀))
160	159	rspcev 3570	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑀) → ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏)
161	146, 157, 160	syl2anc 584	. . . . 5 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏)
162		suprzcl 12501	. . . . 5 ⊢ (({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℤ ∧ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ∧ ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏) → sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
163	7, 145, 161, 162	syl3anc 1370	. . . 4 ⊢ (𝜑 → sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
164	2, 163	sselid 3930	. . 3 ⊢ (𝜑 → sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ (0..^𝑀))
165	1, 164	eqeltrid 2841	. 2 ⊢ (𝜑 → 𝐼 ∈ (0..^𝑀))
166	15, 131	sselid 3930	. . 3 ⊢ (𝜑 → sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ ℤ)
167	14, 166	eqeltrid 2841	. 2 ⊢ (𝜑 → 𝐿 ∈ ℤ)
168	3, 165	sselid 3930	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ (0...𝑀))
169	50, 168	ffvelcdmd 7018	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝐼) ∈ ℝ)
170	167	zred 12527	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ ℝ)
171	170, 62	remulcld 11106	. . . . . . . . 9 ⊢ (𝜑 → (𝐿 · 𝑇) ∈ ℝ)
172	169, 171	readdcld 11105	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ∈ ℝ)
173	172	rexrd 11126	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ∈ ℝ^*)
174	173	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ∈ ℝ^*)
175		fzofzp1 13585	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (0..^𝑀) → (𝐼 + 1) ∈ (0...𝑀))
176	165, 175	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼 + 1) ∈ (0...𝑀))
177	50, 176	ffvelcdmd 7018	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ)
178	177, 171	readdcld 11105	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
179	178	rexrd 11126	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ^*)
180	179	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ^*)
181		elioore 13210	. . . . . . 7 ⊢ (𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) → 𝑥 ∈ ℝ)
182	181	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 ∈ ℝ)
183	172	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ∈ ℝ)
184	44	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘𝐽) ∈ ℝ)
185	1, 163	eqeltrid 2841	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
186		fveq2 6825	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐼 → (𝑄‘𝑗) = (𝑄‘𝐼))
187	186	oveq1d 7352	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝐼 → ((𝑄‘𝑗) + (𝐿 · 𝑇)) = ((𝑄‘𝐼) + (𝐿 · 𝑇)))
188	187	breq1d 5102	. . . . . . . . . . 11 ⊢ (𝑗 = 𝐼 → (((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
189	188	elrab 3634	. . . . . . . . . 10 ⊢ (𝐼 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ (𝐼 ∈ (0..^𝑀) ∧ ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
190	185, 189	sylib 217	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 ∈ (0..^𝑀) ∧ ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
191	190	simprd 496	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
192	191	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝐼) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
193	184	rexrd 11126	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘𝐽) ∈ ℝ^*)
194		fzofzp1 13585	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
195	40, 194	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
196	39, 195	ffvelcdmd 7018	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ∈ 𝐻)
197	27, 196	sseldd 3933	. . . . . . . . . 10 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ∈ ℝ)
198	197	rexrd 11126	. . . . . . . . 9 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ∈ ℝ^*)
199	198	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘(𝐽 + 1)) ∈ ℝ^*)
200		simpr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))))
201		ioogtlb 43378	. . . . . . . 8 ⊢ (((𝑉‘𝐽) ∈ ℝ^* ∧ (𝑉‘(𝐽 + 1)) ∈ ℝ^* ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘𝐽) < 𝑥)
202	193, 199, 200, 201	syl3anc 1370	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘𝐽) < 𝑥)
203	183, 184, 182, 192, 202	lelttrd 11234	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝐼) + (𝐿 · 𝑇)) < 𝑥)
204		zssre 12427	. . . . . . . . . . . . . . . 16 ⊢ ℤ ⊆ ℝ
205	15, 204	sstri 3941	. . . . . . . . . . . . . . 15 ⊢ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ
206	205	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ)
207	99	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
208	129	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏)
209	167	peano2zd 12530	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐿 + 1) ∈ ℤ)
210	209	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐿 + 1) ∈ ℤ)
211		oveq1 7344	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐼 = (𝑀 − 1) → (𝐼 + 1) = ((𝑀 − 1) + 1))
212	146	recnd 11104	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑀 ∈ ℂ)
213		1cnd 11071	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 ∈ ℂ)
214	212, 213	npcand 11437	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
215	211, 214	sylan9eqr 2798	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝐼 + 1) = 𝑀)
216	215	fveq2d 6829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑄‘(𝐼 + 1)) = (𝑄‘𝑀))
217	47	simprd 496	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
218	217	simpld 495	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
219	218	simprd 496	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
220	219	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑄‘𝑀) = 𝐵)
221	59	recnd 11104	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐵 ∈ ℂ)
222	60	recnd 11104	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐴 ∈ ℂ)
223	221, 222	npcand 11437	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐵 − 𝐴) + 𝐴) = 𝐵)
224	223	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐵 = ((𝐵 − 𝐴) + 𝐴))
225	28	eqcomi 2745	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐵 − 𝐴) = 𝑇
226	225	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐵 − 𝐴) = 𝑇)
227	226	oveq1d 7352	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐵 − 𝐴) + 𝐴) = (𝑇 + 𝐴))
228	218	simpld 495	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
229	228	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐴 = (𝑄‘0))
230	229	oveq2d 7353	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑇 + 𝐴) = (𝑇 + (𝑄‘0)))
231	224, 227, 230	3eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐵 = (𝑇 + (𝑄‘0)))
232	231	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → 𝐵 = (𝑇 + (𝑄‘0)))
233	216, 220, 232	3eqtrd 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑄‘(𝐼 + 1)) = (𝑇 + (𝑄‘0)))
234	62	recnd 11104	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑇 ∈ ℂ)
235	228, 222	eqeltrd 2837	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑄‘0) ∈ ℂ)
236	234, 235	addcomd 11278	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑇 + (𝑄‘0)) = ((𝑄‘0) + 𝑇))
237	236	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑇 + (𝑄‘0)) = ((𝑄‘0) + 𝑇))
238	233, 237	eqtrd 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (𝑄‘(𝐼 + 1)) = ((𝑄‘0) + 𝑇))
239	238	oveq1d 7352	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (((𝑄‘0) + 𝑇) + (𝐿 · 𝑇)))
240	171	recnd 11104	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 · 𝑇) ∈ ℂ)
241	235, 234, 240	addassd 11098	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝑄‘0) + 𝑇) + (𝐿 · 𝑇)) = ((𝑄‘0) + (𝑇 + (𝐿 · 𝑇))))
242	234	mulid2d 11094	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (1 · 𝑇) = 𝑇)
243	242, 234	eqeltrd 2837	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 · 𝑇) ∈ ℂ)
244	243, 240	addcomd 11278	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1 · 𝑇) + (𝐿 · 𝑇)) = ((𝐿 · 𝑇) + (1 · 𝑇)))
245	242	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑇 = (1 · 𝑇))
246	245	oveq1d 7352	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑇 + (𝐿 · 𝑇)) = ((1 · 𝑇) + (𝐿 · 𝑇)))
247	170	recnd 11104	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐿 ∈ ℂ)
248	247, 213, 234	adddird 11101	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝐿 + 1) · 𝑇) = ((𝐿 · 𝑇) + (1 · 𝑇)))
249	244, 246, 248	3eqtr4d 2786	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑇 + (𝐿 · 𝑇)) = ((𝐿 + 1) · 𝑇))
250	249	oveq2d 7353	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑄‘0) + (𝑇 + (𝐿 · 𝑇))) = ((𝑄‘0) + ((𝐿 + 1) · 𝑇)))
251	241, 250	eqtrd 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑄‘0) + 𝑇) + (𝐿 · 𝑇)) = ((𝑄‘0) + ((𝐿 + 1) · 𝑇)))
252	251	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → (((𝑄‘0) + 𝑇) + (𝐿 · 𝑇)) = ((𝑄‘0) + ((𝐿 + 1) · 𝑇)))
253	239, 252	eqtr2d 2777	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
254	253	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
255		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
256	254, 255	eqbrtrd 5114	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) ≤ (𝑉‘𝐽))
257		oveq1 7344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (𝐿 + 1) → (𝑘 · 𝑇) = ((𝐿 + 1) · 𝑇))
258	257	oveq2d 7353	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (𝐿 + 1) → ((𝑄‘0) + (𝑘 · 𝑇)) = ((𝑄‘0) + ((𝐿 + 1) · 𝑇)))
259	258	breq1d 5102	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝐿 + 1) → (((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) ≤ (𝑉‘𝐽)))
260	259	elrab 3634	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 + 1) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ ((𝐿 + 1) ∈ ℤ ∧ ((𝑄‘0) + ((𝐿 + 1) · 𝑇)) ≤ (𝑉‘𝐽)))
261	210, 256, 260	sylanbrc 583	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐿 + 1) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)})
262		suprub 12037	. . . . . . . . . . . . . 14 ⊢ ((({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ ∧ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ∧ ∃𝑏 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}𝑗 ≤ 𝑏) ∧ (𝐿 + 1) ∈ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}) → (𝐿 + 1) ≤ sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ))
263	206, 207, 208, 261, 262	syl31anc 1372	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐿 + 1) ≤ sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ))
264	263, 14	breqtrrdi 5134	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐿 + 1) ≤ 𝐿)
265	170	ltp1d 12006	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 < (𝐿 + 1))
266		peano2re 11249	. . . . . . . . . . . . . . . 16 ⊢ (𝐿 ∈ ℝ → (𝐿 + 1) ∈ ℝ)
267	170, 266	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐿 + 1) ∈ ℝ)
268	170, 267	ltnled 11223	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 < (𝐿 + 1) ↔ ¬ (𝐿 + 1) ≤ 𝐿))
269	265, 268	mpbid 231	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ (𝐿 + 1) ≤ 𝐿)
270	269	ad2antrr 723	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐼 = (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ¬ (𝐿 + 1) ≤ 𝐿)
271	264, 270	pm2.65da 814	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐼 = (𝑀 − 1)) → ¬ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
272	5, 165	sselid 3930	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐼 ∈ ℤ)
273	272	zred 12527	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐼 ∈ ℝ)
274	273	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → 𝐼 ∈ ℝ)
275		peano2rem 11389	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℝ → (𝑀 − 1) ∈ ℝ)
276	146, 275	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 − 1) ∈ ℝ)
277	276	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → (𝑀 − 1) ∈ ℝ)
278		elfzolt2 13497	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 ∈ (0..^𝑀) → 𝐼 < 𝑀)
279		elfzoelz 13488	. . . . . . . . . . . . . . . . 17 ⊢ (𝐼 ∈ (0..^𝑀) → 𝐼 ∈ ℤ)
280		elfzoel2 13487	. . . . . . . . . . . . . . . . 17 ⊢ (𝐼 ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
281		zltlem1 12474	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐼 < 𝑀 ↔ 𝐼 ≤ (𝑀 − 1)))
282	279, 280, 281	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 ∈ (0..^𝑀) → (𝐼 < 𝑀 ↔ 𝐼 ≤ (𝑀 − 1)))
283	278, 282	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (𝐼 ∈ (0..^𝑀) → 𝐼 ≤ (𝑀 − 1))
284	165, 283	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐼 ≤ (𝑀 − 1))
285	284	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → 𝐼 ≤ (𝑀 − 1))
286		neqne 2948	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝐼 = (𝑀 − 1) → 𝐼 ≠ (𝑀 − 1))
287	286	necomd 2996	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐼 = (𝑀 − 1) → (𝑀 − 1) ≠ 𝐼)
288	287	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → (𝑀 − 1) ≠ 𝐼)
289	274, 277, 285, 288	leneltd 11230	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → 𝐼 < (𝑀 − 1))
290	6, 204	sstri 3941	. . . . . . . . . . . . . . . 16 ⊢ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ
291	290	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ)
292	145	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅)
293	161	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏)
294	176	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝐼 + 1) ∈ (0...𝑀))
295	273	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → 𝐼 ∈ ℝ)
296	276	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝑀 − 1) ∈ ℝ)
297		1red 11077	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → 1 ∈ ℝ)
298		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → 𝐼 < (𝑀 − 1))
299	295, 296, 297, 298	ltadd1dd 11687	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝐼 + 1) < ((𝑀 − 1) + 1))
300	214	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → ((𝑀 − 1) + 1) = 𝑀)
301	299, 300	breqtrd 5118	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝐼 + 1) < 𝑀)
302		elfzfzo 43159	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 + 1) ∈ (0..^𝑀) ↔ ((𝐼 + 1) ∈ (0...𝑀) ∧ (𝐼 + 1) < 𝑀))
303	294, 301, 302	sylanbrc 583	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → (𝐼 + 1) ∈ (0..^𝑀))
304	303	anim1i 615	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ((𝐼 + 1) ∈ (0..^𝑀) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
305		fveq2 6825	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝐼 + 1) → (𝑄‘𝑗) = (𝑄‘(𝐼 + 1)))
306	305	oveq1d 7352	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝐼 + 1) → ((𝑄‘𝑗) + (𝐿 · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
307	306	breq1d 5102	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝐼 + 1) → (((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
308	307	elrab 3634	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 + 1) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ↔ ((𝐼 + 1) ∈ (0..^𝑀) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
309	304, 308	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐼 + 1) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)})
310		suprub 12037	. . . . . . . . . . . . . . 15 ⊢ ((({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ⊆ ℝ ∧ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)} ≠ ∅ ∧ ∃𝑏 ∈ ℝ ∀𝑘 ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}𝑘 ≤ 𝑏) ∧ (𝐼 + 1) ∈ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}) → (𝐼 + 1) ≤ sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ))
311	291, 292, 293, 309, 310	syl31anc 1372	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐼 + 1) ≤ sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ))
312	311, 1	breqtrrdi 5134	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → (𝐼 + 1) ≤ 𝐼)
313	273	ltp1d 12006	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐼 < (𝐼 + 1))
314		peano2re 11249	. . . . . . . . . . . . . . . . 17 ⊢ (𝐼 ∈ ℝ → (𝐼 + 1) ∈ ℝ)
315	273, 314	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐼 + 1) ∈ ℝ)
316	273, 315	ltnled 11223	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐼 < (𝐼 + 1) ↔ ¬ (𝐼 + 1) ≤ 𝐼))
317	313, 316	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (𝐼 + 1) ≤ 𝐼)
318	317	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐼 < (𝑀 − 1)) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)) → ¬ (𝐼 + 1) ≤ 𝐼)
319	312, 318	pm2.65da 814	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐼 < (𝑀 − 1)) → ¬ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
320	289, 319	syldan 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝐼 = (𝑀 − 1)) → ¬ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
321	271, 320	pm2.61dan 810	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽))
322	44, 178	ltnled 11223	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ↔ ¬ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)))
323	321, 322	mpbird 256	. . . . . . . . 9 ⊢ (𝜑 → (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
324	197	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ∈ ℝ)
325	19	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐷 ∈ ℝ)
326	178	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
327	18	rexrd 11126	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
328	19	rexrd 11126	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷 ∈ ℝ^*)
329	18, 19, 31	ltled 11224	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐶 ≤ 𝐷)
330		lbicc2 13297	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷) → 𝐶 ∈ (𝐶[,]𝐷))
331	327, 328, 329, 330	syl3anc 1370	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐶 ∈ (𝐶[,]𝐷))
332		ubicc2 13298	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 ≤ 𝐷) → 𝐷 ∈ (𝐶[,]𝐷))
333	327, 328, 329, 332	syl3anc 1370	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 ∈ (𝐶[,]𝐷))
334	331, 333	jca 512	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)))
335		prssg 4766	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷)))
336	18, 19, 335	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷)))
337	334, 336	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → {𝐶, 𝐷} ⊆ (𝐶[,]𝐷))
338	337, 23	unssd 4133	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ (𝐶[,]𝐷))
339	17, 338	eqsstrid 3980	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻 ⊆ (𝐶[,]𝐷))
340	339, 196	sseldd 3933	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ∈ (𝐶[,]𝐷))
341		iccleub 13235	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ (𝑉‘(𝐽 + 1)) ∈ (𝐶[,]𝐷)) → (𝑉‘(𝐽 + 1)) ≤ 𝐷)
342	327, 328, 340, 341	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ≤ 𝐷)
343	342	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ 𝐷)
344		simpr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
345	324, 325, 326, 343, 344	letrd 11233	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
346	345	adantlr 712	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
347		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
348	178	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
349	19	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐷 ∈ ℝ)
350	348, 349	ltnled 11223	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷 ↔ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
351	347, 350	mpbird 256	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷)
352	351	adantlr 712	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷)
353		simpll 764	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
354		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
355	178	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
356	197	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ∈ ℝ)
357	355, 356	ltnled 11223	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)) ↔ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
358	354, 357	mpbird 256	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)))
359	358	ad4ant14 749	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)))
360	18	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → 𝐶 ∈ ℝ)
361	19	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → 𝐷 ∈ ℝ)
362	178	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
363	18	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐶 ∈ ℝ)
364	178	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
365	44	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) ∈ ℝ)
366	339, 43	sseldd 3933	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑉‘𝐽) ∈ (𝐶[,]𝐷))
367		iccgelb 13236	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ (𝑉‘𝐽) ∈ (𝐶[,]𝐷)) → 𝐶 ≤ (𝑉‘𝐽))
368	327, 328, 366, 367	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐶 ≤ (𝑉‘𝐽))
369	368	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐶 ≤ (𝑉‘𝐽))
370		simpr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
371	363, 365, 364, 369, 370	lelttrd 11234	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐶 < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
372	363, 364, 371	ltled 11224	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐶 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
373	372	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → 𝐶 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
374	178	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
375	19	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → 𝐷 ∈ ℝ)
376		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷)
377	374, 375, 376	ltled 11224	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ 𝐷)
378	377	adantlr 712	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ≤ 𝐷)
379	360, 361, 362, 373, 378	eliccd 43387	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ (𝐶[,]𝐷))
380	167	znegcld 12529	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → -𝐿 ∈ ℤ)
381	247, 234	mulneg1d 11529	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (-𝐿 · 𝑇) = -(𝐿 · 𝑇))
382	381	oveq2d 7353	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)) = (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + -(𝐿 · 𝑇)))
383	178	recnd 11104	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℂ)
384	383, 240	negsubd 11439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + -(𝐿 · 𝑇)) = (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) − (𝐿 · 𝑇)))
385	177	recnd 11104	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℂ)
386	385, 240	pncand 11434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) − (𝐿 · 𝑇)) = (𝑄‘(𝐼 + 1)))
387	382, 384, 386	3eqtrd 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)) = (𝑄‘(𝐼 + 1)))
388		ffn 6651	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
389	50, 388	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
390		fnfvelrn 7014	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 Fn (0...𝑀) ∧ (𝐼 + 1) ∈ (0...𝑀)) → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
391	389, 176, 390	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
392	387, 391	eqeltrd 2837	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)) ∈ ran 𝑄)
393		oveq1 7344	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = -𝐿 → (𝑘 · 𝑇) = (-𝐿 · 𝑇))
394	393	oveq2d 7353	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = -𝐿 → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) = (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)))
395	394	eleq1d 2821	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = -𝐿 → ((((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)) ∈ ran 𝑄))
396	395	rspcev 3570	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-𝐿 ∈ ℤ ∧ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (-𝐿 · 𝑇)) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
397	380, 392, 396	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
398	397	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
399		oveq1 7344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → (𝑦 + (𝑘 · 𝑇)) = (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)))
400	399	eleq1d 2821	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
401	400	rexbidv 3171	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
402	401	elrab 3634	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} ↔ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
403	379, 398, 402	sylanbrc 583	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
404		elun2 4124	. . . . . . . . . . . . . . . 16 ⊢ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
405	403, 404	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
406	17	eqcomi 2745	. . . . . . . . . . . . . . 15 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = 𝐻
407	405, 406	eleqtrdi 2847	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻)
408	407	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻)
409		f1ofo 6774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑉:(0...𝑁)–1-1-onto→𝐻 → 𝑉:(0...𝑁)–onto→𝐻)
410	36, 37, 409	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑉:(0...𝑁)–onto→𝐻)
411		foelrn 7038	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑉:(0...𝑁)–onto→𝐻 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
412	410, 411	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
413		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
414	413	eqcomd 2742	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗) → (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
415	414	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → (((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗) → (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
416	415	reximdv 3163	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → (∃𝑗 ∈ (0...𝑁)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗) → ∃𝑗 ∈ (0...𝑁)(𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
417	412, 416	mpd 15	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
418	417	ad4ant14 749	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
419		simpl 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
420	413	eqcoms 2744	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
421	420	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) = (𝑉‘𝑗))
422	419, 421	breqtrd 5118	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) < (𝑉‘𝑗))
423	422	adantll 711	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) < (𝑉‘𝑗))
424	423	adantlr 712	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝐽) < (𝑉‘𝑗))
425	36	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑉 Isom < , < ((0...𝑁), 𝐻))
426	42	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐽 ∈ (0...𝑁))
427		simplr 766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑗 ∈ (0...𝑁))
428		isorel 7253	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑉 Isom < , < ((0...𝑁), 𝐻) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) → (𝐽 < 𝑗 ↔ (𝑉‘𝐽) < (𝑉‘𝑗)))
429	425, 426, 427, 428	syl12anc 834	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝐽 < 𝑗 ↔ (𝑉‘𝐽) < (𝑉‘𝑗)))
430	424, 429	mpbird 256	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐽 < 𝑗)
431	430	adantllr 716	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝐽 < 𝑗)
432		simpr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
433		simpl 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)))
434	432, 433	eqbrtrd 5114	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝑗) < (𝑉‘(𝐽 + 1)))
435	434	adantll 711	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝑗) < (𝑉‘(𝐽 + 1)))
436	435	adantlr 712	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘𝑗) < (𝑉‘(𝐽 + 1)))
437	36	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑉 Isom < , < ((0...𝑁), 𝐻))
438		simplr 766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑗 ∈ (0...𝑁))
439	195	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝐽 + 1) ∈ (0...𝑁))
440		isorel 7253	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑉 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝑗 < (𝐽 + 1) ↔ (𝑉‘𝑗) < (𝑉‘(𝐽 + 1))))
441	437, 438, 439, 440	syl12anc 834	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑗 < (𝐽 + 1) ↔ (𝑉‘𝑗) < (𝑉‘(𝐽 + 1))))
442	436, 441	mpbird 256	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑗 < (𝐽 + 1))
443	442	adantl3r 747	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑗 < (𝐽 + 1))
444	431, 443	jca 512	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
445	444	ex 413	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))))
446	445	adantlr 712	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < (𝑉‘(𝐽 + 1))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ 𝐻) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑉‘𝑗) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) → (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))))
447	446	reximdva 3161	. . . . . . . . . . . . . 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 835	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
450		elfzelz 13357	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
451	450	ad2antlr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝑗 ∈ ℤ)
452		elfzelz 13357	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 ∈ (0...𝑁) → 𝐽 ∈ ℤ)
453	42, 452	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐽 ∈ ℤ)
454	453	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝐽 ∈ ℤ)
455		simprl 768	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝐽 < 𝑗)
456		simprr 770	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝑗 < (𝐽 + 1))
457		btwnnz 12497	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ)
458	454, 455, 456, 457	syl3anc 1370	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → ¬ 𝑗 ∈ ℤ)
459	451, 458	pm2.65da 814	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ¬ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
460	459	nrexdv 3142	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
461	460	ad3antrrr 727	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) ∧ ¬ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ¬ ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
462	449, 461	condan 815	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) < 𝐷) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
463	352, 462	syldan 591	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ∧ ¬ 𝐷 ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
464	346, 463	pm2.61dan 810	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑉‘𝐽) < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
465	323, 464	mpdan 684	. . . . . . . 8 ⊢ (𝜑 → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
466	465	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
467	182	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑥 ∈ ℝ)
468	197	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ∈ ℝ)
469	178	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)) ∈ ℝ)
470		iooltub 43393	. . . . . . . . . 10 ⊢ (((𝑉‘𝐽) ∈ ℝ^* ∧ (𝑉‘(𝐽 + 1)) ∈ ℝ^* ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 < (𝑉‘(𝐽 + 1)))
471	193, 199, 200, 470	syl3anc 1370	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 < (𝑉‘(𝐽 + 1)))
472	471	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑥 < (𝑉‘(𝐽 + 1)))
473		simpr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
474	467, 468, 469, 472, 473	ltletrd 11236	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∧ (𝑉‘(𝐽 + 1)) ≤ ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) → 𝑥 < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
475	466, 474	mpdan 684	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 < ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
476	174, 180, 182, 203, 475	eliood 43381	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑥 ∈ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
477	476	ralrimiva 3139	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))𝑥 ∈ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
478		dfss3 3920	. . . 4 ⊢ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))) ↔ ∀𝑥 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))𝑥 ∈ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
479	477, 478	sylibr 233	. . 3 ⊢ (𝜑 → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
480		fveq2 6825	. . . . . . 7 ⊢ (𝑖 = 𝐼 → (𝑄‘𝑖) = (𝑄‘𝐼))
481	480	oveq1d 7352	. . . . . 6 ⊢ (𝑖 = 𝐼 → ((𝑄‘𝑖) + (𝑙 · 𝑇)) = ((𝑄‘𝐼) + (𝑙 · 𝑇)))
482		oveq1 7344	. . . . . . . 8 ⊢ (𝑖 = 𝐼 → (𝑖 + 1) = (𝐼 + 1))
483	482	fveq2d 6829	. . . . . . 7 ⊢ (𝑖 = 𝐼 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝐼 + 1)))
484	483	oveq1d 7352	. . . . . 6 ⊢ (𝑖 = 𝐼 → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇)))
485	481, 484	oveq12d 7355	. . . . 5 ⊢ (𝑖 = 𝐼 → (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) = (((𝑄‘𝐼) + (𝑙 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇))))
486	485	sseq2d 3964	. . . 4 ⊢ (𝑖 = 𝐼 → (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) ↔ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝑙 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇)))))
487		oveq1 7344	. . . . . . 7 ⊢ (𝑙 = 𝐿 → (𝑙 · 𝑇) = (𝐿 · 𝑇))
488	487	oveq2d 7353	. . . . . 6 ⊢ (𝑙 = 𝐿 → ((𝑄‘𝐼) + (𝑙 · 𝑇)) = ((𝑄‘𝐼) + (𝐿 · 𝑇)))
489	487	oveq2d 7353	. . . . . 6 ⊢ (𝑙 = 𝐿 → ((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇)) = ((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))
490	488, 489	oveq12d 7355	. . . . 5 ⊢ (𝑙 = 𝐿 → (((𝑄‘𝐼) + (𝑙 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇))) = (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇))))
491	490	sseq2d 3964	. . . 4 ⊢ (𝑙 = 𝐿 → (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝑙 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝑙 · 𝑇))) ↔ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))))
492	486, 491	rspc2ev 3581	. . 3 ⊢ ((𝐼 ∈ (0..^𝑀) ∧ 𝐿 ∈ ℤ ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝐼) + (𝐿 · 𝑇))(,)((𝑄‘(𝐼 + 1)) + (𝐿 · 𝑇)))) → ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
493	165, 167, 479, 492	syl3anc 1370	. 2 ⊢ (𝜑 → ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
494	165, 167, 493	jca31 515	1 ⊢ (𝜑 → ((𝐼 ∈ (0..^𝑀) ∧ 𝐿 ∈ ℤ) ∧ ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1540 ∈ wcel 2105 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 {crab 3403 ∪ cun 3896 ⊆ wss 3898 ∅c0 4269 {cpr 4575 class class class wbr 5092 ↦ cmpt 5175 ran crn 5621 ℩cio 6429 Fn wfn 6474 ⟶wf 6475 –onto→wfo 6477 –1-1-onto→wf1o 6478 ‘cfv 6479 Isom wiso 6480 (class class class)co 7337 ↑_m cmap 8686 supcsup 9297 ℂcc 10970 ℝcr 10971 0cc0 10972 1c1 10973 + caddc 10975 · cmul 10977 ℝ^*cxr 11109 < clt 11110 ≤ cle 11111 − cmin 11306 -cneg 11307 / cdiv 11733 ℕcn 12074 ℕ₀cn0 12334 ℤcz 12420 ℤ_≥cuz 12683 ℝ⁺crp 12831 (,)cioo 13180 [,]cicc 13183 ...cfz 13340 ..^cfzo 13483 ♯chash 14145

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-rep 5229 ax-sep 5243 ax-nul 5250 ax-pow 5308 ax-pr 5372 ax-un 7650 ax-inf2 9498 ax-cnex 11028 ax-resscn 11029 ax-1cn 11030 ax-icn 11031 ax-addcl 11032 ax-addrcl 11033 ax-mulcl 11034 ax-mulrcl 11035 ax-mulcom 11036 ax-addass 11037 ax-mulass 11038 ax-distr 11039 ax-i2m1 11040 ax-1ne0 11041 ax-1rid 11042 ax-rnegex 11043 ax-rrecex 11044 ax-cnre 11045 ax-pre-lttri 11046 ax-pre-lttrn 11047 ax-pre-ltadd 11048 ax-pre-mulgt0 11049 ax-pre-sup 11050

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3349 df-reu 3350 df-rab 3404 df-v 3443 df-sbc 3728 df-csb 3844 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3917 df-nul 4270 df-if 4474 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4853 df-int 4895 df-iun 4943 df-iin 4944 df-br 5093 df-opab 5155 df-mpt 5176 df-tr 5210 df-id 5518 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5575 df-se 5576 df-we 5577 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 df-pred 6238 df-ord 6305 df-on 6306 df-lim 6307 df-suc 6308 df-iota 6431 df-fun 6481 df-fn 6482 df-f 6483 df-f1 6484 df-fo 6485 df-f1o 6486 df-fv 6487 df-isom 6488 df-riota 7293 df-ov 7340 df-oprab 7341 df-mpo 7342 df-om 7781 df-1st 7899 df-2nd 7900 df-frecs 8167 df-wrecs 8198 df-recs 8272 df-rdg 8311 df-1o 8367 df-oadd 8371 df-er 8569 df-map 8688 df-en 8805 df-dom 8806 df-sdom 8807 df-fin 8808 df-fi 9268 df-sup 9299 df-inf 9300 df-oi 9367 df-dju 9758 df-card 9796 df-pnf 11112 df-mnf 11113 df-xr 11114 df-ltxr 11115 df-le 11116 df-sub 11308 df-neg 11309 df-div 11734 df-nn 12075 df-2 12137 df-3 12138 df-n0 12335 df-xnn0 12407 df-z 12421 df-uz 12684 df-q 12790 df-rp 12832 df-xneg 12949 df-xadd 12950 df-xmul 12951 df-ioo 13184 df-icc 13187 df-fz 13341 df-fzo 13484 df-seq 13823 df-exp 13884 df-hash 14146 df-cj 14909 df-re 14910 df-im 14911 df-sqrt 15045 df-abs 15046 df-rest 17230 df-topgen 17251 df-psmet 20695 df-xmet 20696 df-met 20697 df-bl 20698 df-mopn 20699 df-top 22149 df-topon 22166 df-bases 22202 df-cld 22276 df-ntr 22277 df-cls 22278 df-nei 22355 df-lp 22393 df-cmp 22644

This theorem is referenced by: fourierdlem97 44089

W3C validator