Theorem fourierdlem12 40336

Description: A point of a partition is not an element of any open interval determined by the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fourierdlem12.1	⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem12.2	⊢ (𝜑 → 𝑀 ∈ ℕ)
fourierdlem12.3	⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
fourierdlem12.4	⊢ (𝜑 → 𝑋 ∈ ran 𝑄)

Assertion

Ref	Expression
fourierdlem12	⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))

Distinct variable groups:   𝐴,𝑚,𝑝   𝐵,𝑚,𝑝   𝑖,𝑀,𝑚,𝑝   𝑄,𝑖,𝑝   𝜑,𝑖

Allowed substitution hints:   𝜑(𝑚,𝑝)   𝐴(𝑖)   𝐵(𝑖)   𝑃(𝑖,𝑚,𝑝)   𝑄(𝑚)   𝑋(𝑖,𝑚,𝑝)

Proof of Theorem fourierdlem12

Dummy variables 𝑗 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem12.4	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ran 𝑄)
2		fourierdlem12.3	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
3		fourierdlem12.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
4		fourierdlem12.1	. . . . . . . . . 10 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
5	4	fourierdlem2 40326	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	3, 5	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
7	2, 6	mpbid 222	. . . . . . 7 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
8	7	simpld 475	. . . . . 6 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)))
9		elmapi 7879	. . . . . 6 ⊢ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
10		ffn 6045	. . . . . 6 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
11	8, 9, 10	3syl 18	. . . . 5 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
12		fvelrnb 6243	. . . . 5 ⊢ (𝑄 Fn (0...𝑀) → (𝑋 ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋))
13	11, 12	syl 17	. . . 4 ⊢ (𝜑 → (𝑋 ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋))
14	1, 13	mpbid 222	. . 3 ⊢ (𝜑 → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋)
15	14	adantr 481	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋)
16	8, 9	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
17	16	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
18		fzofzp1 12565	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
19	18	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
20	17, 19	ffvelrnd 6360	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
21	20	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
22	21	3ad2antl1 1223	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
23		frn 6053	. . . . . . . . . . . 12 ⊢ (𝑄:(0...𝑀)⟶ℝ → ran 𝑄 ⊆ ℝ)
24	16, 23	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝑄 ⊆ ℝ)
25	24, 1	sseldd 3604	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℝ)
26	25	ad2antrr 762	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑖 < 𝑗) → 𝑋 ∈ ℝ)
27	26	3ad2antl1 1223	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → 𝑋 ∈ ℝ)
28	17	ffvelrnda 6359	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ)
29	28	3adant3 1081	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) ∈ ℝ)
30	29	adantr 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘𝑗) ∈ ℝ)
31		simpr 477	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑖 < 𝑗)
32		elfzoelz 12470	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℤ)
33	32	ad2antrr 762	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑖 ∈ ℤ)
34		elfzelz 12342	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
35	34	ad2antlr 763	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ ℤ)
36		zltp1le 11427	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑖 < 𝑗 ↔ (𝑖 + 1) ≤ 𝑗))
37	33, 35, 36	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑖 < 𝑗 ↔ (𝑖 + 1) ≤ 𝑗))
38	31, 37	mpbid 222	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑖 + 1) ≤ 𝑗)
39	33	peano2zd 11485	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑖 + 1) ∈ ℤ)
40		eluz 11701	. . . . . . . . . . . . . 14 ⊢ (((𝑖 + 1) ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ (ℤ≥‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑗))
41	39, 35, 40	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑗 ∈ (ℤ≥‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑗))
42	38, 41	mpbird 247	. . . . . . . . . . . 12 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ (ℤ≥‘(𝑖 + 1)))
43	42	adantlll 754	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ (ℤ≥‘(𝑖 + 1)))
44	17	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑄:(0...𝑀)⟶ℝ)
45		0red 10041	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ∈ ℝ)
46		elfzelz 12342	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ((𝑖 + 1)...𝑗) → 𝑤 ∈ ℤ)
47	46	zred 11482	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ((𝑖 + 1)...𝑗) → 𝑤 ∈ ℝ)
48	47	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ ℝ)
49	32	peano2zd 11485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ ℤ)
50	49	zred 11482	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ ℝ)
51	50	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑖 + 1) ∈ ℝ)
52	32	zred 11482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℝ)
53	52	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑖 ∈ ℝ)
54		elfzole1 12478	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → 0 ≤ 𝑖)
55	54	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ≤ 𝑖)
56	53	ltp1d 10954	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑖 < (𝑖 + 1))
57	45, 53, 51, 55, 56	lelttrd 10195	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 < (𝑖 + 1))
58		elfzle1 12344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ((𝑖 + 1)...𝑗) → (𝑖 + 1) ≤ 𝑤)
59	58	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑖 + 1) ≤ 𝑤)
60	45, 51, 48, 57, 59	ltletrd 10197	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 < 𝑤)
61	45, 48, 60	ltled 10185	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ≤ 𝑤)
62	61	adantlr 751	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ≤ 𝑤)
63	47	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ ℝ)
64	34	zred 11482	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
65	64	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑗 ∈ ℝ)
66		elfzel2 12340	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
67	66	zred 11482	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
68	67	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑀 ∈ ℝ)
69		elfzle2 12345	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ((𝑖 + 1)...𝑗) → 𝑤 ≤ 𝑗)
70	69	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ≤ 𝑗)
71		elfzle2 12345	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀)
72	71	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑗 ≤ 𝑀)
73	63, 65, 68, 70, 72	letrd 10194	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ≤ 𝑀)
74	73	adantll 750	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ≤ 𝑀)
75	46	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ ℤ)
76		0zd 11389	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ∈ ℤ)
77	66	ad2antlr 763	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑀 ∈ ℤ)
78		elfz 12332	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑤 ∈ (0...𝑀) ↔ (0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀)))
79	75, 76, 77, 78	syl3anc 1326	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑤 ∈ (0...𝑀) ↔ (0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀)))
80	62, 74, 79	mpbir2and 957	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ (0...𝑀))
81	80	adantlll 754	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ (0...𝑀))
82	44, 81	ffvelrnd 6360	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑄‘𝑤) ∈ ℝ)
83	82	adantlr 751	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑄‘𝑤) ∈ ℝ)
84		simp-4l 806	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝜑)
85		0red 10041	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ∈ ℝ)
86		elfzelz 12342	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → 𝑤 ∈ ℤ)
87	86	zred 11482	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → 𝑤 ∈ ℝ)
88	87	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℝ)
89		0red 10041	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ∈ ℝ)
90	50	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑖 + 1) ∈ ℝ)
91	87	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℝ)
92		0red 10041	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → 0 ∈ ℝ)
93	52	ltp1d 10954	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 < (𝑖 + 1))
94	92, 52, 50, 54, 93	lelttrd 10195	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (0..^𝑀) → 0 < (𝑖 + 1))
95	94	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 < (𝑖 + 1))
96		elfzle1 12344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → (𝑖 + 1) ≤ 𝑤)
97	96	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑖 + 1) ≤ 𝑤)
98	89, 90, 91, 95, 97	ltletrd 10197	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 < 𝑤)
99	98	adantlr 751	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 < 𝑤)
100	85, 88, 99	ltled 10185	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ≤ 𝑤)
101	100	adantlll 754	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ≤ 𝑤)
102	101	adantlr 751	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ≤ 𝑤)
103	87	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℝ)
104		peano2rem 10348	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℝ → (𝑗 − 1) ∈ ℝ)
105	64, 104	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
106	105	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑗 − 1) ∈ ℝ)
107	67	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑀 ∈ ℝ)
108		elfzle2 12345	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → 𝑤 ≤ (𝑗 − 1))
109	108	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ≤ (𝑗 − 1))
110		zlem1lt 11429	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑗 ≤ 𝑀 ↔ (𝑗 − 1) < 𝑀))
111	34, 66, 110	syl2anc 693	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 ≤ 𝑀 ↔ (𝑗 − 1) < 𝑀))
112	71, 111	mpbid 222	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
113	112	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑗 − 1) < 𝑀)
114	103, 106, 107, 109, 113	lelttrd 10195	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 < 𝑀)
115	114	adantlr 751	. . . . . . . . . . . . . 14 ⊢ (((𝑗 ∈ (0...𝑀) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 < 𝑀)
116	115	adantlll 754	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 < 𝑀)
117	86	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℤ)
118		0zd 11389	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ∈ ℤ)
119	66	ad3antlr 767	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑀 ∈ ℤ)
120		elfzo 12472	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑤 ∈ (0..^𝑀) ↔ (0 ≤ 𝑤 ∧ 𝑤 < 𝑀)))
121	117, 118, 119, 120	syl3anc 1326	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑤 ∈ (0..^𝑀) ↔ (0 ≤ 𝑤 ∧ 𝑤 < 𝑀)))
122	102, 116, 121	mpbir2and 957	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ (0..^𝑀))
123	16	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
124		elfzofz 12485	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (0..^𝑀) → 𝑤 ∈ (0...𝑀))
125	124	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → 𝑤 ∈ (0...𝑀))
126	123, 125	ffvelrnd 6360	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘𝑤) ∈ ℝ)
127		fzofzp1 12565	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (0..^𝑀) → (𝑤 + 1) ∈ (0...𝑀))
128	127	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑤 + 1) ∈ (0...𝑀))
129	123, 128	ffvelrnd 6360	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘(𝑤 + 1)) ∈ ℝ)
130		eleq1 2689	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑤 → (𝑖 ∈ (0..^𝑀) ↔ 𝑤 ∈ (0..^𝑀)))
131	130	anbi2d 740	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑤 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑤 ∈ (0..^𝑀))))
132		fveq2 6191	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑤 → (𝑄‘𝑖) = (𝑄‘𝑤))
133		oveq1 6657	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑤 → (𝑖 + 1) = (𝑤 + 1))
134	133	fveq2d 6195	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑤 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑤 + 1)))
135	132, 134	breq12d 4666	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑤 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘𝑤) < (𝑄‘(𝑤 + 1))))
136	131, 135	imbi12d 334	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑤 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘𝑤) < (𝑄‘(𝑤 + 1)))))
137	7	simprrd 797	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
138	137	r19.21bi 2932	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
139	136, 138	chvarv 2263	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘𝑤) < (𝑄‘(𝑤 + 1)))
140	126, 129, 139	ltled 10185	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘𝑤) ≤ (𝑄‘(𝑤 + 1)))
141	84, 122, 140	syl2anc 693	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑄‘𝑤) ≤ (𝑄‘(𝑤 + 1)))
142	43, 83, 141	monoord 12831	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ≤ (𝑄‘𝑗))
143	142	3adantl3 1219	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ≤ (𝑄‘𝑗))
144	16	ffvelrnda 6359	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ)
145	144	3adant3 1081	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) ∈ ℝ)
146		simp3 1063	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) = 𝑋)
147	145, 146	eqled 10140	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) ≤ 𝑋)
148	147	3adant1r 1319	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) ≤ 𝑋)
149	148	adantr 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘𝑗) ≤ 𝑋)
150	22, 30, 27, 143, 149	letrd 10194	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ≤ 𝑋)
151	22, 27, 150	lensymd 10188	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → ¬ 𝑋 < (𝑄‘(𝑖 + 1)))
152	151	intnand 962	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → ¬ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1))))
153	64	ad2antlr 763	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → 𝑗 ∈ ℝ)
154	52	ad3antlr 767	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → 𝑖 ∈ ℝ)
155		simpr 477	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → ¬ 𝑖 < 𝑗)
156	153, 154, 155	nltled 10187	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → 𝑗 ≤ 𝑖)
157	156	3adantl3 1219	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ ¬ 𝑖 < 𝑗) → 𝑗 ≤ 𝑖)
158		eqcom 2629	. . . . . . . . . . . . 13 ⊢ ((𝑄‘𝑗) = 𝑋 ↔ 𝑋 = (𝑄‘𝑗))
159	158	biimpi 206	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑗) = 𝑋 → 𝑋 = (𝑄‘𝑗))
160	159	adantr 481	. . . . . . . . . . 11 ⊢ (((𝑄‘𝑗) = 𝑋 ∧ 𝑗 ≤ 𝑖) → 𝑋 = (𝑄‘𝑗))
161	160	3ad2antl3 1225	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → 𝑋 = (𝑄‘𝑗))
162	34	ad2antlr 763	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑗 ∈ ℤ)
163	32	ad2antrr 762	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑖 ∈ ℤ)
164		simpr 477	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑗 ≤ 𝑖)
165		eluz2 11693	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ≥‘𝑗) ↔ (𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑗 ≤ 𝑖))
166	162, 163, 164, 165	syl3anbrc 1246	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑖 ∈ (ℤ≥‘𝑗))
167	166	adantlll 754	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑖 ∈ (ℤ≥‘𝑗))
168	17	ad2antrr 762	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑄:(0...𝑀)⟶ℝ)
169		0zd 11389	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ∈ ℤ)
170	66	ad2antlr 763	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑀 ∈ ℤ)
171		elfzelz 12342	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ (𝑗...𝑖) → 𝑤 ∈ ℤ)
172	171	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ ℤ)
173	169, 170, 172	3jca 1242	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ))
174		0red 10041	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ∈ ℝ)
175	64	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑗 ∈ ℝ)
176	171	zred 11482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝑗...𝑖) → 𝑤 ∈ ℝ)
177	176	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ ℝ)
178		elfzle1 12344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
179	178	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ≤ 𝑗)
180		elfzle1 12344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝑗...𝑖) → 𝑗 ≤ 𝑤)
181	180	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑗 ≤ 𝑤)
182	174, 175, 177, 179, 181	letrd 10194	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ≤ 𝑤)
183	182	adantll 750	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ≤ 𝑤)
184	176	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ ℝ)
185		elfzoel2 12469	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
186	185	zred 11482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑀 ∈ ℝ)
187	186	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑀 ∈ ℝ)
188	52	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑖 ∈ ℝ)
189		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ (𝑗...𝑖) → 𝑤 ≤ 𝑖)
190	189	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ≤ 𝑖)
191		elfzolt2 12479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 < 𝑀)
192	191	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑖 < 𝑀)
193	184, 188, 187, 190, 192	lelttrd 10195	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 < 𝑀)
194	184, 187, 193	ltled 10185	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ≤ 𝑀)
195	194	adantlr 751	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ≤ 𝑀)
196	173, 183, 195	jca32 558	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ (0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀)))
197	196	adantlll 754	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ (0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀)))
198		elfz2 12333	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ (0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀)))
199	197, 198	sylibr 224	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ (0...𝑀))
200	168, 199	ffvelrnd 6360	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → (𝑄‘𝑤) ∈ ℝ)
201	200	adantlr 751	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) ∧ 𝑤 ∈ (𝑗...𝑖)) → (𝑄‘𝑤) ∈ ℝ)
202		simplll 798	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝜑)
203		0red 10041	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ∈ ℝ)
204	64	ad2antlr 763	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑗 ∈ ℝ)
205		elfzelz 12342	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑤 ∈ ℤ)
206	205	zred 11482	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑤 ∈ ℝ)
207	206	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ ℝ)
208	178	ad2antlr 763	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ≤ 𝑗)
209		elfzle1 12344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑗 ≤ 𝑤)
210	209	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑗 ≤ 𝑤)
211	203, 204, 207, 208, 210	letrd 10194	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ≤ 𝑤)
212	206	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ ℝ)
213	52	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑖 ∈ ℝ)
214	186	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑀 ∈ ℝ)
215		peano2rem 10348	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ ℝ → (𝑖 − 1) ∈ ℝ)
216	213, 215	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑖 − 1) ∈ ℝ)
217		elfzle2 12345	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑤 ≤ (𝑖 − 1))
218	217	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ≤ (𝑖 − 1))
219	213	ltm1d 10956	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑖 − 1) < 𝑖)
220	212, 216, 213, 218, 219	lelttrd 10195	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 < 𝑖)
221	191	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑖 < 𝑀)
222	212, 213, 214, 220, 221	lttrd 10198	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 < 𝑀)
223	222	adantlr 751	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 < 𝑀)
224	205	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ ℤ)
225		0zd 11389	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ∈ ℤ)
226	185	ad2antrr 762	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑀 ∈ ℤ)
227	224, 225, 226, 120	syl3anc 1326	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑤 ∈ (0..^𝑀) ↔ (0 ≤ 𝑤 ∧ 𝑤 < 𝑀)))
228	211, 223, 227	mpbir2and 957	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ (0..^𝑀))
229	228	adantlll 754	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ (0..^𝑀))
230	202, 229, 140	syl2anc 693	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑄‘𝑤) ≤ (𝑄‘(𝑤 + 1)))
231	230	adantlr 751	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑄‘𝑤) ≤ (𝑄‘(𝑤 + 1)))
232	167, 201, 231	monoord 12831	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → (𝑄‘𝑗) ≤ (𝑄‘𝑖))
233	232	3adantl3 1219	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → (𝑄‘𝑗) ≤ (𝑄‘𝑖))
234	161, 233	eqbrtrd 4675	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → 𝑋 ≤ (𝑄‘𝑖))
235	25	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
236		elfzofz 12485	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
237	236	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
238	17, 237	ffvelrnd 6360	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
239	235, 238	lenltd 10183	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 ≤ (𝑄‘𝑖) ↔ ¬ (𝑄‘𝑖) < 𝑋))
240	239	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ≤ 𝑖) → (𝑋 ≤ (𝑄‘𝑖) ↔ ¬ (𝑄‘𝑖) < 𝑋))
241	240	3ad2antl1 1223	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → (𝑋 ≤ (𝑄‘𝑖) ↔ ¬ (𝑄‘𝑖) < 𝑋))
242	234, 241	mpbid 222	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → ¬ (𝑄‘𝑖) < 𝑋)
243	157, 242	syldan 487	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ ¬ 𝑖 < 𝑗) → ¬ (𝑄‘𝑖) < 𝑋)
244	243	intnanrd 963	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ ¬ 𝑖 < 𝑗) → ¬ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1))))
245	152, 244	pm2.61dan 832	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → ¬ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1))))
246	245	intnand 962	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → ¬ (((𝑄‘𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑋 ∈ ℝ*) ∧ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1)))))
247		elioo3g 12204	. . . 4 ⊢ (𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ (((𝑄‘𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑋 ∈ ℝ*) ∧ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1)))))
248	246, 247	sylnibr 319	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → ¬ 𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
249	248	rexlimdv3a 3033	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋 → ¬ 𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
250	15, 249	mpd 15	1 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990  ∀wral 2912  ∃wrex 2913  {crab 2916   ⊆ wss 3574   class class class wbr 4653   ↦ cmpt 4729  ran crn 5115   Fn wfn 5883  ⟶wf 5884  ‘cfv 5888  (class class class)co 6650   ↑_𝑚 cmap 7857  ℝcr 9935  0cc0 9936  1c1 9937   + caddc 9939  ℝ^*cxr 10073   < clt 10074   ≤ cle 10075   − cmin 10266  ℕcn 11020  ℤcz 11377  ℤ_≥cuz 11687  (,)cioo 12175  ...cfz 12326  ..^cfzo 12465

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-n0 11293  df-z 11378  df-uz 11688  df-ioo 12179  df-fz 12327  df-fzo 12466

This theorem is referenced by:  fourierdlem38  40362  fourierdlem74  40397  fourierdlem75  40398  fourierdlem88  40411  fourierdlem103  40426  fourierdlem104  40427