Theorem fourierdlem12 39012

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 39002	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	3, 5	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
7	2, 6	mpbid 221	. . . . . . 7 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
8	7	simpld 474	. . . . . 6 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)))
9		elmapi 7765	. . . . . 6 ⊢ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
10		ffn 5958	. . . . . 6 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
11	8, 9, 10	3syl 18	. . . . 5 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
12		fvelrnb 6153	. . . . 5 ⊢ (𝑄 Fn (0...𝑀) → (𝑋 ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋))
13	11, 12	syl 17	. . . 4 ⊢ (𝜑 → (𝑋 ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋))
14	1, 13	mpbid 221	. . 3 ⊢ (𝜑 → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋)
15	14	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋)
16	8, 9	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
17	16	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
18		fzofzp1 12431	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
19	18	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
20	17, 19	ffvelrnd 6268	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
21	20	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
22	21	3ad2antl1 1216	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
23		frn 5966	. . . . . . . . . . . 12 ⊢ (𝑄:(0...𝑀)⟶ℝ → ran 𝑄 ⊆ ℝ)
24	16, 23	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝑄 ⊆ ℝ)
25	24, 1	sseldd 3569	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℝ)
26	25	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑖 < 𝑗) → 𝑋 ∈ ℝ)
27	26	3ad2antl1 1216	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → 𝑋 ∈ ℝ)
28	17	ffvelrnda 6267	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ)
29	28	3adant3 1074	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) ∈ ℝ)
30	29	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘𝑗) ∈ ℝ)
31		simpr 476	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑖 < 𝑗)
32		elfzoelz 12339	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℤ)
33	32	ad2antrr 758	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑖 ∈ ℤ)
34		elfzelz 12213	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
35	34	ad2antlr 759	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ ℤ)
36		zltp1le 11304	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑖 < 𝑗 ↔ (𝑖 + 1) ≤ 𝑗))
37	33, 35, 36	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑖 < 𝑗 ↔ (𝑖 + 1) ≤ 𝑗))
38	31, 37	mpbid 221	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑖 + 1) ≤ 𝑗)
39	33	peano2zd 11361	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑖 + 1) ∈ ℤ)
40		eluz 11577	. . . . . . . . . . . . . 14 ⊢ (((𝑖 + 1) ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ (ℤ≥‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑗))
41	39, 35, 40	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑗 ∈ (ℤ≥‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑗))
42	38, 41	mpbird 246	. . . . . . . . . . . 12 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ (ℤ≥‘(𝑖 + 1)))
43	42	adantlll 750	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ (ℤ≥‘(𝑖 + 1)))
44	17	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑄:(0...𝑀)⟶ℝ)
45		0red 9920	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ∈ ℝ)
46		elfzelz 12213	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ((𝑖 + 1)...𝑗) → 𝑤 ∈ ℤ)
47	46	zred 11358	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ((𝑖 + 1)...𝑗) → 𝑤 ∈ ℝ)
48	47	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ ℝ)
49	32	peano2zd 11361	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ ℤ)
50	49	zred 11358	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ ℝ)
51	50	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑖 + 1) ∈ ℝ)
52	32	zred 11358	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℝ)
53	52	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑖 ∈ ℝ)
54		elfzole1 12347	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → 0 ≤ 𝑖)
55	54	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ≤ 𝑖)
56	53	ltp1d 10833	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑖 < (𝑖 + 1))
57	45, 53, 51, 55, 56	lelttrd 10074	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 < (𝑖 + 1))
58		elfzle1 12215	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ((𝑖 + 1)...𝑗) → (𝑖 + 1) ≤ 𝑤)
59	58	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑖 + 1) ≤ 𝑤)
60	45, 51, 48, 57, 59	ltletrd 10076	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 < 𝑤)
61	45, 48, 60	ltled 10064	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ≤ 𝑤)
62	61	adantlr 747	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ≤ 𝑤)
63	47	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ ℝ)
64	34	zred 11358	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
65	64	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑗 ∈ ℝ)
66		elfzel2 12211	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
67	66	zred 11358	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
68	67	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑀 ∈ ℝ)
69		elfzle2 12216	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ((𝑖 + 1)...𝑗) → 𝑤 ≤ 𝑗)
70	69	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ≤ 𝑗)
71		elfzle2 12216	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀)
72	71	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑗 ≤ 𝑀)
73	63, 65, 68, 70, 72	letrd 10073	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ≤ 𝑀)
74	73	adantll 746	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ≤ 𝑀)
75	46	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ ℤ)
76		0zd 11266	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ∈ ℤ)
77	66	ad2antlr 759	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑀 ∈ ℤ)
78		elfz 12203	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑤 ∈ (0...𝑀) ↔ (0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀)))
79	75, 76, 77, 78	syl3anc 1318	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑤 ∈ (0...𝑀) ↔ (0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀)))
80	62, 74, 79	mpbir2and 959	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ (0...𝑀))
81	80	adantlll 750	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ (0...𝑀))
82	44, 81	ffvelrnd 6268	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑄‘𝑤) ∈ ℝ)
83	82	adantlr 747	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑄‘𝑤) ∈ ℝ)
84		simp-4l 802	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝜑)
85		0red 9920	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ∈ ℝ)
86		elfzelz 12213	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → 𝑤 ∈ ℤ)
87	86	zred 11358	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → 𝑤 ∈ ℝ)
88	87	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℝ)
89		0red 9920	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ∈ ℝ)
90	50	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑖 + 1) ∈ ℝ)
91	87	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℝ)
92		0red 9920	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → 0 ∈ ℝ)
93	52	ltp1d 10833	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 < (𝑖 + 1))
94	92, 52, 50, 54, 93	lelttrd 10074	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (0..^𝑀) → 0 < (𝑖 + 1))
95	94	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 < (𝑖 + 1))
96		elfzle1 12215	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → (𝑖 + 1) ≤ 𝑤)
97	96	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑖 + 1) ≤ 𝑤)
98	89, 90, 91, 95, 97	ltletrd 10076	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 < 𝑤)
99	98	adantlr 747	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 < 𝑤)
100	85, 88, 99	ltled 10064	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ≤ 𝑤)
101	100	adantlll 750	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ≤ 𝑤)
102	101	adantlr 747	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ≤ 𝑤)
103	87	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℝ)
104		peano2rem 10227	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℝ → (𝑗 − 1) ∈ ℝ)
105	64, 104	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
106	105	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑗 − 1) ∈ ℝ)
107	67	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑀 ∈ ℝ)
108		elfzle2 12216	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → 𝑤 ≤ (𝑗 − 1))
109	108	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ≤ (𝑗 − 1))
110		zlem1lt 11306	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑗 ≤ 𝑀 ↔ (𝑗 − 1) < 𝑀))
111	34, 66, 110	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 ≤ 𝑀 ↔ (𝑗 − 1) < 𝑀))
112	71, 111	mpbid 221	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
113	112	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑗 − 1) < 𝑀)
114	103, 106, 107, 109, 113	lelttrd 10074	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 < 𝑀)
115	114	adantlr 747	. . . . . . . . . . . . . 14 ⊢ (((𝑗 ∈ (0...𝑀) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 < 𝑀)
116	115	adantlll 750	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 < 𝑀)
117	86	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℤ)
118		0zd 11266	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ∈ ℤ)
119	66	ad3antlr 763	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑀 ∈ ℤ)
120		elfzo 12341	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑤 ∈ (0..^𝑀) ↔ (0 ≤ 𝑤 ∧ 𝑤 < 𝑀)))
121	117, 118, 119, 120	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑤 ∈ (0..^𝑀) ↔ (0 ≤ 𝑤 ∧ 𝑤 < 𝑀)))
122	102, 116, 121	mpbir2and 959	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ (0..^𝑀))
123	16	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
124		elfzofz 12354	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (0..^𝑀) → 𝑤 ∈ (0...𝑀))
125	124	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → 𝑤 ∈ (0...𝑀))
126	123, 125	ffvelrnd 6268	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘𝑤) ∈ ℝ)
127		fzofzp1 12431	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (0..^𝑀) → (𝑤 + 1) ∈ (0...𝑀))
128	127	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑤 + 1) ∈ (0...𝑀))
129	123, 128	ffvelrnd 6268	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘(𝑤 + 1)) ∈ ℝ)
130		eleq1 2676	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑤 → (𝑖 ∈ (0..^𝑀) ↔ 𝑤 ∈ (0..^𝑀)))
131	130	anbi2d 736	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑤 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑤 ∈ (0..^𝑀))))
132		fveq2 6103	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑤 → (𝑄‘𝑖) = (𝑄‘𝑤))
133		oveq1 6556	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑤 → (𝑖 + 1) = (𝑤 + 1))
134	133	fveq2d 6107	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑤 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑤 + 1)))
135	132, 134	breq12d 4596	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑤 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘𝑤) < (𝑄‘(𝑤 + 1))))
136	131, 135	imbi12d 333	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑤 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘𝑤) < (𝑄‘(𝑤 + 1)))))
137	7	simprrd 793	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
138	137	r19.21bi 2916	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
139	136, 138	chvarv 2251	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘𝑤) < (𝑄‘(𝑤 + 1)))
140	126, 129, 139	ltled 10064	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘𝑤) ≤ (𝑄‘(𝑤 + 1)))
141	84, 122, 140	syl2anc 691	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑄‘𝑤) ≤ (𝑄‘(𝑤 + 1)))
142	43, 83, 141	monoord 12693	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ≤ (𝑄‘𝑗))
143	142	3adantl3 1212	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ≤ (𝑄‘𝑗))
144	16	ffvelrnda 6267	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ)
145	144	3adant3 1074	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) ∈ ℝ)
146		simp3 1056	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) = 𝑋)
147	145, 146	eqled 10019	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) ≤ 𝑋)
148	147	3adant1r 1311	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) ≤ 𝑋)
149	148	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘𝑗) ≤ 𝑋)
150	22, 30, 27, 143, 149	letrd 10073	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ≤ 𝑋)
151	22, 27, 150	lensymd 10067	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → ¬ 𝑋 < (𝑄‘(𝑖 + 1)))
152	151	intnand 953	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → ¬ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1))))
153	64	ad2antlr 759	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → 𝑗 ∈ ℝ)
154	52	ad3antlr 763	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → 𝑖 ∈ ℝ)
155		simpr 476	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → ¬ 𝑖 < 𝑗)
156	153, 154, 155	nltled 10066	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → 𝑗 ≤ 𝑖)
157	156	3adantl3 1212	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ ¬ 𝑖 < 𝑗) → 𝑗 ≤ 𝑖)
158		eqcom 2617	. . . . . . . . . . . . 13 ⊢ ((𝑄‘𝑗) = 𝑋 ↔ 𝑋 = (𝑄‘𝑗))
159	158	biimpi 205	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑗) = 𝑋 → 𝑋 = (𝑄‘𝑗))
160	159	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑄‘𝑗) = 𝑋 ∧ 𝑗 ≤ 𝑖) → 𝑋 = (𝑄‘𝑗))
161	160	3ad2antl3 1218	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → 𝑋 = (𝑄‘𝑗))
162	34	ad2antlr 759	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑗 ∈ ℤ)
163	32	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑖 ∈ ℤ)
164		simpr 476	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑗 ≤ 𝑖)
165		eluz2 11569	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ≥‘𝑗) ↔ (𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑗 ≤ 𝑖))
166	162, 163, 164, 165	syl3anbrc 1239	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑖 ∈ (ℤ≥‘𝑗))
167	166	adantlll 750	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑖 ∈ (ℤ≥‘𝑗))
168	17	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑄:(0...𝑀)⟶ℝ)
169		0zd 11266	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ∈ ℤ)
170	66	ad2antlr 759	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑀 ∈ ℤ)
171		elfzelz 12213	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ (𝑗...𝑖) → 𝑤 ∈ ℤ)
172	171	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ ℤ)
173	169, 170, 172	3jca 1235	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ))
174		0red 9920	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ∈ ℝ)
175	64	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑗 ∈ ℝ)
176	171	zred 11358	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝑗...𝑖) → 𝑤 ∈ ℝ)
177	176	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ ℝ)
178		elfzle1 12215	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
179	178	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ≤ 𝑗)
180		elfzle1 12215	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝑗...𝑖) → 𝑗 ≤ 𝑤)
181	180	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑗 ≤ 𝑤)
182	174, 175, 177, 179, 181	letrd 10073	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ≤ 𝑤)
183	182	adantll 746	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ≤ 𝑤)
184	176	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ ℝ)
185		elfzoel2 12338	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
186	185	zred 11358	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑀 ∈ ℝ)
187	186	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑀 ∈ ℝ)
188	52	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑖 ∈ ℝ)
189		elfzle2 12216	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ (𝑗...𝑖) → 𝑤 ≤ 𝑖)
190	189	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ≤ 𝑖)
191		elfzolt2 12348	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 < 𝑀)
192	191	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑖 < 𝑀)
193	184, 188, 187, 190, 192	lelttrd 10074	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 < 𝑀)
194	184, 187, 193	ltled 10064	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ≤ 𝑀)
195	194	adantlr 747	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ≤ 𝑀)
196	173, 183, 195	jca32 556	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ (0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀)))
197	196	adantlll 750	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ (0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀)))
198		elfz2 12204	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ (0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀)))
199	197, 198	sylibr 223	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ (0...𝑀))
200	168, 199	ffvelrnd 6268	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → (𝑄‘𝑤) ∈ ℝ)
201	200	adantlr 747	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) ∧ 𝑤 ∈ (𝑗...𝑖)) → (𝑄‘𝑤) ∈ ℝ)
202		simplll 794	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝜑)
203		0red 9920	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ∈ ℝ)
204	64	ad2antlr 759	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑗 ∈ ℝ)
205		elfzelz 12213	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑤 ∈ ℤ)
206	205	zred 11358	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑤 ∈ ℝ)
207	206	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ ℝ)
208	178	ad2antlr 759	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ≤ 𝑗)
209		elfzle1 12215	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑗 ≤ 𝑤)
210	209	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑗 ≤ 𝑤)
211	203, 204, 207, 208, 210	letrd 10073	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ≤ 𝑤)
212	206	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ ℝ)
213	52	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑖 ∈ ℝ)
214	186	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑀 ∈ ℝ)
215		peano2rem 10227	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ ℝ → (𝑖 − 1) ∈ ℝ)
216	213, 215	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑖 − 1) ∈ ℝ)
217		elfzle2 12216	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑤 ≤ (𝑖 − 1))
218	217	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ≤ (𝑖 − 1))
219	213	ltm1d 10835	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑖 − 1) < 𝑖)
220	212, 216, 213, 218, 219	lelttrd 10074	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 < 𝑖)
221	191	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑖 < 𝑀)
222	212, 213, 214, 220, 221	lttrd 10077	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 < 𝑀)
223	222	adantlr 747	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 < 𝑀)
224	205	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ ℤ)
225		0zd 11266	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ∈ ℤ)
226	185	ad2antrr 758	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑀 ∈ ℤ)
227	224, 225, 226, 120	syl3anc 1318	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑤 ∈ (0..^𝑀) ↔ (0 ≤ 𝑤 ∧ 𝑤 < 𝑀)))
228	211, 223, 227	mpbir2and 959	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ (0..^𝑀))
229	228	adantlll 750	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ (0..^𝑀))
230	202, 229, 140	syl2anc 691	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑄‘𝑤) ≤ (𝑄‘(𝑤 + 1)))
231	230	adantlr 747	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑄‘𝑤) ≤ (𝑄‘(𝑤 + 1)))
232	167, 201, 231	monoord 12693	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → (𝑄‘𝑗) ≤ (𝑄‘𝑖))
233	232	3adantl3 1212	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → (𝑄‘𝑗) ≤ (𝑄‘𝑖))
234	161, 233	eqbrtrd 4605	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → 𝑋 ≤ (𝑄‘𝑖))
235	25	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
236		elfzofz 12354	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
237	236	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
238	17, 237	ffvelrnd 6268	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
239	235, 238	lenltd 10062	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 ≤ (𝑄‘𝑖) ↔ ¬ (𝑄‘𝑖) < 𝑋))
240	239	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ≤ 𝑖) → (𝑋 ≤ (𝑄‘𝑖) ↔ ¬ (𝑄‘𝑖) < 𝑋))
241	240	3ad2antl1 1216	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → (𝑋 ≤ (𝑄‘𝑖) ↔ ¬ (𝑄‘𝑖) < 𝑋))
242	234, 241	mpbid 221	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → ¬ (𝑄‘𝑖) < 𝑋)
243	157, 242	syldan 486	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ ¬ 𝑖 < 𝑗) → ¬ (𝑄‘𝑖) < 𝑋)
244	243	intnanrd 954	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ ¬ 𝑖 < 𝑗) → ¬ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1))))
245	152, 244	pm2.61dan 828	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → ¬ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1))))
246	245	intnand 953	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → ¬ (((𝑄‘𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑋 ∈ ℝ*) ∧ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1)))))
247		elioo3g 12075	. . . 4 ⊢ (𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ (((𝑄‘𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑋 ∈ ℝ*) ∧ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1)))))
248	246, 247	sylnibr 318	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → ¬ 𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
249	248	rexlimdv3a 3015	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋 → ¬ 𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
250	15, 249	mpd 15	1 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  {crab 2900   ⊆ wss 3540   class class class wbr 4583   ↦ cmpt 4643  ran crn 5039   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↑_𝑚 cmap 7744  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818  ℝ^*cxr 9952   < clt 9953   ≤ cle 9954   − cmin 10145  ℕcn 10897  ℤcz 11254  ℤ_≥cuz 11563  (,)cioo 12046  ...cfz 12197  ..^cfzo 12334

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-n0 11170  df-z 11255  df-uz 11564  df-ioo 12050  df-fz 12198  df-fzo 12335

This theorem is referenced by:  fourierdlem38  39038  fourierdlem74  39073  fourierdlem75  39074  fourierdlem88  39087  fourierdlem103  39102  fourierdlem104  39103