Theorem fourierdlem12 46134

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	⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (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	. . . . . . 7 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
3		fourierdlem12.2	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ)
4		fourierdlem12.1	. . . . . . . . 9 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
5	4	fourierdlem2 46124	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	3, 5	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
7	2, 6	mpbid 232	. . . . . 6 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
8	7	simpld 494	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑m (0...𝑀)))
9		elmapi 8889	. . . . 5 ⊢ (𝑄 ∈ (ℝ ↑m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
10		ffn 6736	. . . . 5 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
11		fvelrnb 6969	. . . . 5 ⊢ (𝑄 Fn (0...𝑀) → (𝑋 ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋))
12	8, 9, 10, 11	4syl 19	. . . 4 ⊢ (𝜑 → (𝑋 ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋))
13	1, 12	mpbid 232	. . 3 ⊢ (𝜑 → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋)
14	13	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋)
15	8, 9	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
16	15	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
17		fzofzp1 13803	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
18	17	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
19	16, 18	ffvelcdmd 7105	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
20	19	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
21	20	3ad2antl1 1186	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
22		frn 6743	. . . . . . . . . . . 12 ⊢ (𝑄:(0...𝑀)⟶ℝ → ran 𝑄 ⊆ ℝ)
23	15, 22	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝑄 ⊆ ℝ)
24	23, 1	sseldd 3984	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℝ)
25	24	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑖 < 𝑗) → 𝑋 ∈ ℝ)
26	25	3ad2antl1 1186	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → 𝑋 ∈ ℝ)
27	16	ffvelcdmda 7104	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ)
28	27	3adant3 1133	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) ∈ ℝ)
29	28	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘𝑗) ∈ ℝ)
30		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑖 < 𝑗)
31		elfzoelz 13699	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℤ)
32	31	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑖 ∈ ℤ)
33		elfzelz 13564	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
34	33	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ ℤ)
35		zltp1le 12667	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑖 < 𝑗 ↔ (𝑖 + 1) ≤ 𝑗))
36	32, 34, 35	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑖 < 𝑗 ↔ (𝑖 + 1) ≤ 𝑗))
37	30, 36	mpbid 232	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑖 + 1) ≤ 𝑗)
38	32	peano2zd 12725	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑖 + 1) ∈ ℤ)
39		eluz 12892	. . . . . . . . . . . . . 14 ⊢ (((𝑖 + 1) ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ (ℤ≥‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑗))
40	38, 34, 39	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑗 ∈ (ℤ≥‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑗))
41	37, 40	mpbird 257	. . . . . . . . . . . 12 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ (ℤ≥‘(𝑖 + 1)))
42	41	adantlll 718	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ (ℤ≥‘(𝑖 + 1)))
43	16	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑄:(0...𝑀)⟶ℝ)
44		0zd 12625	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ∈ ℤ)
45		elfzel2 13562	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
46	45	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑀 ∈ ℤ)
47		elfzelz 13564	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ((𝑖 + 1)...𝑗) → 𝑤 ∈ ℤ)
48	47	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ ℤ)
49		0red 11264	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ∈ ℝ)
50	47	zred 12722	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ((𝑖 + 1)...𝑗) → 𝑤 ∈ ℝ)
51	50	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ ℝ)
52	31	peano2zd 12725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ ℤ)
53	52	zred 12722	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ ℝ)
54	53	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑖 + 1) ∈ ℝ)
55	31	zred 12722	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℝ)
56	55	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑖 ∈ ℝ)
57		elfzole1 13707	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → 0 ≤ 𝑖)
58	57	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ≤ 𝑖)
59	56	ltp1d 12198	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑖 < (𝑖 + 1))
60	49, 56, 54, 58, 59	lelttrd 11419	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 < (𝑖 + 1))
61		elfzle1 13567	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ((𝑖 + 1)...𝑗) → (𝑖 + 1) ≤ 𝑤)
62	61	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑖 + 1) ≤ 𝑤)
63	49, 54, 51, 60, 62	ltletrd 11421	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 < 𝑤)
64	49, 51, 63	ltled 11409	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ≤ 𝑤)
65	64	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ≤ 𝑤)
66	50	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ ℝ)
67	33	zred 12722	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
68	67	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑗 ∈ ℝ)
69	45	zred 12722	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
70	69	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑀 ∈ ℝ)
71		elfzle2 13568	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ((𝑖 + 1)...𝑗) → 𝑤 ≤ 𝑗)
72	71	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ≤ 𝑗)
73		elfzle2 13568	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀)
74	73	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑗 ≤ 𝑀)
75	66, 68, 70, 72, 74	letrd 11418	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ≤ 𝑀)
76	75	adantll 714	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ≤ 𝑀)
77	44, 46, 48, 65, 76	elfzd 13555	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ (0...𝑀))
78	77	adantlll 718	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ (0...𝑀))
79	43, 78	ffvelcdmd 7105	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑄‘𝑤) ∈ ℝ)
80	79	adantlr 715	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑄‘𝑤) ∈ ℝ)
81		simp-4l 783	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝜑)
82		0red 11264	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ∈ ℝ)
83		elfzelz 13564	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → 𝑤 ∈ ℤ)
84	83	zred 12722	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → 𝑤 ∈ ℝ)
85	84	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℝ)
86		0red 11264	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ∈ ℝ)
87	53	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑖 + 1) ∈ ℝ)
88	84	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℝ)
89		0red 11264	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → 0 ∈ ℝ)
90	55	ltp1d 12198	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 < (𝑖 + 1))
91	89, 55, 53, 57, 90	lelttrd 11419	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (0..^𝑀) → 0 < (𝑖 + 1))
92	91	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 < (𝑖 + 1))
93		elfzle1 13567	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → (𝑖 + 1) ≤ 𝑤)
94	93	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑖 + 1) ≤ 𝑤)
95	86, 87, 88, 92, 94	ltletrd 11421	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 < 𝑤)
96	95	adantlr 715	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 < 𝑤)
97	82, 85, 96	ltled 11409	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ≤ 𝑤)
98	97	adantlll 718	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ≤ 𝑤)
99	98	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ≤ 𝑤)
100	84	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℝ)
101		peano2rem 11576	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℝ → (𝑗 − 1) ∈ ℝ)
102	67, 101	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
103	102	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑗 − 1) ∈ ℝ)
104	69	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑀 ∈ ℝ)
105		elfzle2 13568	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → 𝑤 ≤ (𝑗 − 1))
106	105	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ≤ (𝑗 − 1))
107		zlem1lt 12669	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑗 ≤ 𝑀 ↔ (𝑗 − 1) < 𝑀))
108	33, 45, 107	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 ≤ 𝑀 ↔ (𝑗 − 1) < 𝑀))
109	73, 108	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
110	109	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑗 − 1) < 𝑀)
111	100, 103, 104, 106, 110	lelttrd 11419	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 < 𝑀)
112	111	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝑗 ∈ (0...𝑀) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 < 𝑀)
113	112	adantlll 718	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 < 𝑀)
114	83	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℤ)
115		0zd 12625	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ∈ ℤ)
116	45	ad3antlr 731	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑀 ∈ ℤ)
117		elfzo 13701	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑤 ∈ (0..^𝑀) ↔ (0 ≤ 𝑤 ∧ 𝑤 < 𝑀)))
118	114, 115, 116, 117	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑤 ∈ (0..^𝑀) ↔ (0 ≤ 𝑤 ∧ 𝑤 < 𝑀)))
119	99, 113, 118	mpbir2and 713	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ (0..^𝑀))
120	15	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
121		elfzofz 13715	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (0..^𝑀) → 𝑤 ∈ (0...𝑀))
122	121	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → 𝑤 ∈ (0...𝑀))
123	120, 122	ffvelcdmd 7105	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘𝑤) ∈ ℝ)
124		fzofzp1 13803	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (0..^𝑀) → (𝑤 + 1) ∈ (0...𝑀))
125	124	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑤 + 1) ∈ (0...𝑀))
126	120, 125	ffvelcdmd 7105	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘(𝑤 + 1)) ∈ ℝ)
127		eleq1w 2824	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑤 → (𝑖 ∈ (0..^𝑀) ↔ 𝑤 ∈ (0..^𝑀)))
128	127	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑤 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑤 ∈ (0..^𝑀))))
129		fveq2 6906	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑤 → (𝑄‘𝑖) = (𝑄‘𝑤))
130		oveq1 7438	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑤 → (𝑖 + 1) = (𝑤 + 1))
131	130	fveq2d 6910	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑤 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑤 + 1)))
132	129, 131	breq12d 5156	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑤 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘𝑤) < (𝑄‘(𝑤 + 1))))
133	128, 132	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑤 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘𝑤) < (𝑄‘(𝑤 + 1)))))
134	7	simprrd 774	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
135	134	r19.21bi 3251	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
136	133, 135	chvarvv 1998	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘𝑤) < (𝑄‘(𝑤 + 1)))
137	123, 126, 136	ltled 11409	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘𝑤) ≤ (𝑄‘(𝑤 + 1)))
138	81, 119, 137	syl2anc 584	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑄‘𝑤) ≤ (𝑄‘(𝑤 + 1)))
139	42, 80, 138	monoord 14073	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ≤ (𝑄‘𝑗))
140	139	3adantl3 1169	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ≤ (𝑄‘𝑗))
141	15	ffvelcdmda 7104	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ)
142	141	3adant3 1133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) ∈ ℝ)
143		simp3 1139	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) = 𝑋)
144	142, 143	eqled 11364	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) ≤ 𝑋)
145	144	3adant1r 1178	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) ≤ 𝑋)
146	145	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘𝑗) ≤ 𝑋)
147	21, 29, 26, 140, 146	letrd 11418	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ≤ 𝑋)
148	21, 26, 147	lensymd 11412	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → ¬ 𝑋 < (𝑄‘(𝑖 + 1)))
149	148	intnand 488	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → ¬ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1))))
150	67	ad2antlr 727	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → 𝑗 ∈ ℝ)
151	55	ad3antlr 731	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → 𝑖 ∈ ℝ)
152		simpr 484	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → ¬ 𝑖 < 𝑗)
153	150, 151, 152	nltled 11411	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → 𝑗 ≤ 𝑖)
154	153	3adantl3 1169	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ ¬ 𝑖 < 𝑗) → 𝑗 ≤ 𝑖)
155		eqcom 2744	. . . . . . . . . . . . 13 ⊢ ((𝑄‘𝑗) = 𝑋 ↔ 𝑋 = (𝑄‘𝑗))
156	155	biimpi 216	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑗) = 𝑋 → 𝑋 = (𝑄‘𝑗))
157	156	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑄‘𝑗) = 𝑋 ∧ 𝑗 ≤ 𝑖) → 𝑋 = (𝑄‘𝑗))
158	157	3ad2antl3 1188	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → 𝑋 = (𝑄‘𝑗))
159	33	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑗 ∈ ℤ)
160	31	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑖 ∈ ℤ)
161		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑗 ≤ 𝑖)
162		eluz2 12884	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ≥‘𝑗) ↔ (𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑗 ≤ 𝑖))
163	159, 160, 161, 162	syl3anbrc 1344	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑖 ∈ (ℤ≥‘𝑗))
164	163	adantlll 718	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑖 ∈ (ℤ≥‘𝑗))
165	16	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑄:(0...𝑀)⟶ℝ)
166		0zd 12625	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ∈ ℤ)
167	45	ad2antlr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑀 ∈ ℤ)
168		elfzelz 13564	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ (𝑗...𝑖) → 𝑤 ∈ ℤ)
169	168	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ ℤ)
170	166, 167, 169	3jca 1129	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ))
171		0red 11264	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ∈ ℝ)
172	67	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑗 ∈ ℝ)
173	168	zred 12722	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝑗...𝑖) → 𝑤 ∈ ℝ)
174	173	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ ℝ)
175		elfzle1 13567	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
176	175	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ≤ 𝑗)
177		elfzle1 13567	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝑗...𝑖) → 𝑗 ≤ 𝑤)
178	177	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑗 ≤ 𝑤)
179	171, 172, 174, 176, 178	letrd 11418	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ≤ 𝑤)
180	179	adantll 714	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ≤ 𝑤)
181	173	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ ℝ)
182		elfzoel2 13698	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
183	182	zred 12722	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑀 ∈ ℝ)
184	183	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑀 ∈ ℝ)
185	55	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑖 ∈ ℝ)
186		elfzle2 13568	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ (𝑗...𝑖) → 𝑤 ≤ 𝑖)
187	186	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ≤ 𝑖)
188		elfzolt2 13708	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 < 𝑀)
189	188	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑖 < 𝑀)
190	181, 185, 184, 187, 189	lelttrd 11419	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 < 𝑀)
191	181, 184, 190	ltled 11409	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ≤ 𝑀)
192	191	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ≤ 𝑀)
193	170, 180, 192	jca32 515	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ (0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀)))
194	193	adantlll 718	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ (0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀)))
195		elfz2 13554	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ (0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀)))
196	194, 195	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ (0...𝑀))
197	165, 196	ffvelcdmd 7105	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → (𝑄‘𝑤) ∈ ℝ)
198	197	adantlr 715	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) ∧ 𝑤 ∈ (𝑗...𝑖)) → (𝑄‘𝑤) ∈ ℝ)
199		simplll 775	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝜑)
200		0red 11264	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ∈ ℝ)
201	67	ad2antlr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑗 ∈ ℝ)
202		elfzelz 13564	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑤 ∈ ℤ)
203	202	zred 12722	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑤 ∈ ℝ)
204	203	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ ℝ)
205	175	ad2antlr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ≤ 𝑗)
206		elfzle1 13567	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑗 ≤ 𝑤)
207	206	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑗 ≤ 𝑤)
208	200, 201, 204, 205, 207	letrd 11418	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ≤ 𝑤)
209	203	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ ℝ)
210	55	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑖 ∈ ℝ)
211	183	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑀 ∈ ℝ)
212		peano2rem 11576	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ ℝ → (𝑖 − 1) ∈ ℝ)
213	210, 212	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑖 − 1) ∈ ℝ)
214		elfzle2 13568	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑤 ≤ (𝑖 − 1))
215	214	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ≤ (𝑖 − 1))
216	210	ltm1d 12200	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑖 − 1) < 𝑖)
217	209, 213, 210, 215, 216	lelttrd 11419	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 < 𝑖)
218	188	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑖 < 𝑀)
219	209, 210, 211, 217, 218	lttrd 11422	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 < 𝑀)
220	219	adantlr 715	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 < 𝑀)
221	202	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ ℤ)
222		0zd 12625	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ∈ ℤ)
223	182	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑀 ∈ ℤ)
224	221, 222, 223, 117	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑤 ∈ (0..^𝑀) ↔ (0 ≤ 𝑤 ∧ 𝑤 < 𝑀)))
225	208, 220, 224	mpbir2and 713	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ (0..^𝑀))
226	225	adantlll 718	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ (0..^𝑀))
227	199, 226, 137	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑄‘𝑤) ≤ (𝑄‘(𝑤 + 1)))
228	227	adantlr 715	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑄‘𝑤) ≤ (𝑄‘(𝑤 + 1)))
229	164, 198, 228	monoord 14073	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → (𝑄‘𝑗) ≤ (𝑄‘𝑖))
230	229	3adantl3 1169	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → (𝑄‘𝑗) ≤ (𝑄‘𝑖))
231	158, 230	eqbrtrd 5165	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → 𝑋 ≤ (𝑄‘𝑖))
232	24	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
233		elfzofz 13715	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
234	233	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
235	16, 234	ffvelcdmd 7105	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
236	232, 235	lenltd 11407	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 ≤ (𝑄‘𝑖) ↔ ¬ (𝑄‘𝑖) < 𝑋))
237	236	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ≤ 𝑖) → (𝑋 ≤ (𝑄‘𝑖) ↔ ¬ (𝑄‘𝑖) < 𝑋))
238	237	3ad2antl1 1186	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → (𝑋 ≤ (𝑄‘𝑖) ↔ ¬ (𝑄‘𝑖) < 𝑋))
239	231, 238	mpbid 232	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → ¬ (𝑄‘𝑖) < 𝑋)
240	154, 239	syldan 591	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ ¬ 𝑖 < 𝑗) → ¬ (𝑄‘𝑖) < 𝑋)
241	240	intnanrd 489	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ ¬ 𝑖 < 𝑗) → ¬ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1))))
242	149, 241	pm2.61dan 813	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → ¬ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1))))
243	242	intnand 488	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → ¬ (((𝑄‘𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑋 ∈ ℝ*) ∧ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1)))))
244		elioo3g 13416	. . . 4 ⊢ (𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ (((𝑄‘𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑋 ∈ ℝ*) ∧ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1)))))
245	243, 244	sylnibr 329	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → ¬ 𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
246	245	rexlimdv3a 3159	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋 → ¬ 𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
247	14, 246	mpd 15	1 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108  ∀wral 3061  ∃wrex 3070  {crab 3436   ⊆ wss 3951   class class class wbr 5143   ↦ cmpt 5225  ran crn 5686   Fn wfn 6556  ⟶wf 6557  ‘cfv 6561  (class class class)co 7431   ↑_m cmap 8866  ℝcr 11154  0cc0 11155  1c1 11156   + caddc 11158  ℝ^*cxr 11294   < clt 11295   ≤ cle 11296   − cmin 11492  ℕcn 12266  ℤcz 12613  ℤ_≥cuz 12878  (,)cioo 13387  ...cfz 13547  ..^cfzo 13694

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-n0 12527  df-z 12614  df-uz 12879  df-ioo 13391  df-fz 13548  df-fzo 13695

This theorem is referenced by:  fourierdlem38  46160  fourierdlem74  46195  fourierdlem75  46196  fourierdlem88  46209  fourierdlem103  46224  fourierdlem104  46225