Theorem fourierdlem12 46947

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 46937	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	3, 5	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
7	2, 6	mpbid 235	. . . . . 6 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
8	7	simpld 500	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑m (0...𝑀)))
9		elmapi 8848	. . . . 5 ⊢ (𝑄 ∈ (ℝ ↑m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
10		ffn 6702	. . . . 5 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
11		fvelrnb 6938	. . . . 5 ⊢ (𝑄 Fn (0...𝑀) → (𝑋 ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋))
12	8, 9, 10, 11	4syl 20	. . . 4 ⊢ (𝜑 → (𝑋 ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋))
13	1, 12	mpbid 235	. . 3 ⊢ (𝜑 → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋)
14	13	adantr 486	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋)
15	8, 9	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
16	15	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
17		fzofzp1 13820	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
18	17	adantl 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
19	16, 18	ffvelcdmd 7078	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
20	19	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
21	20	3ad2antl1 1204	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
22		frn 6710	. . . . . . . . . . . 12 ⊢ (𝑄:(0...𝑀)⟶ℝ → ran 𝑄 ⊆ ℝ)
23	15, 22	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝑄 ⊆ ℝ)
24	23, 1	sseldd 3932	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℝ)
25	24	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑖 < 𝑗) → 𝑋 ∈ ℝ)
26	25	3ad2antl1 1204	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → 𝑋 ∈ ℝ)
27	16	ffvelcdmda 7077	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ)
28	27	3adant3 1150	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) ∈ ℝ)
29	28	adantr 486	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘𝑗) ∈ ℝ)
30		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑖 < 𝑗)
31		elfzoelz 13714	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℤ)
32	31	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑖 ∈ ℤ)
33		elfzelz 13578	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
34	33	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ ℤ)
35		zltp1le 12668	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑖 < 𝑗 ↔ (𝑖 + 1) ≤ 𝑗))
36	32, 34, 35	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑖 < 𝑗 ↔ (𝑖 + 1) ≤ 𝑗))
37	30, 36	mpbid 235	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑖 + 1) ≤ 𝑗)
38	32	peano2zd 12728	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑖 + 1) ∈ ℤ)
39		eluz 12901	. . . . . . . . . . . . . 14 ⊢ (((𝑖 + 1) ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ (ℤ≥‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑗))
40	38, 34, 39	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑗 ∈ (ℤ≥‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑗))
41	37, 40	mpbird 260	. . . . . . . . . . . 12 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ (ℤ≥‘(𝑖 + 1)))
42	41	adantlll 731	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ (ℤ≥‘(𝑖 + 1)))
43	16	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑄:(0...𝑀)⟶ℝ)
44		0zd 12627	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ∈ ℤ)
45		elfzel2 13576	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
46	45	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑀 ∈ ℤ)
47		elfzelz 13578	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ((𝑖 + 1)...𝑗) → 𝑤 ∈ ℤ)
48	47	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ ℤ)
49		0red 11235	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ∈ ℝ)
50	47	zred 12725	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ((𝑖 + 1)...𝑗) → 𝑤 ∈ ℝ)
51	50	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ ℝ)
52	31	peano2zd 12728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ ℤ)
53	52	zred 12725	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ ℝ)
54	53	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑖 + 1) ∈ ℝ)
55	31	zred 12725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℝ)
56	55	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑖 ∈ ℝ)
57		elfzole1 13723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → 0 ≤ 𝑖)
58	57	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ≤ 𝑖)
59	56	ltp1d 12169	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑖 < (𝑖 + 1))
60	49, 56, 54, 58, 59	lelttrd 11392	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 < (𝑖 + 1))
61		elfzle1 13581	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ((𝑖 + 1)...𝑗) → (𝑖 + 1) ≤ 𝑤)
62	61	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑖 + 1) ≤ 𝑤)
63	49, 54, 51, 60, 62	ltletrd 11394	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 < 𝑤)
64	49, 51, 63	ltled 11382	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ≤ 𝑤)
65	64	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ≤ 𝑤)
66	50	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ ℝ)
67	33	zred 12725	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
68	67	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑗 ∈ ℝ)
69	45	zred 12725	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
70	69	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑀 ∈ ℝ)
71		elfzle2 13582	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ((𝑖 + 1)...𝑗) → 𝑤 ≤ 𝑗)
72	71	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ≤ 𝑗)
73		elfzle2 13582	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀)
74	73	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑗 ≤ 𝑀)
75	66, 68, 70, 72, 74	letrd 11391	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ≤ 𝑀)
76	75	adantll 727	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ≤ 𝑀)
77	44, 46, 48, 65, 76	elfzd 13569	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ (0...𝑀))
78	77	adantlll 731	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ (0...𝑀))
79	43, 78	ffvelcdmd 7078	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑄‘𝑤) ∈ ℝ)
80	79	adantlr 728	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑄‘𝑤) ∈ ℝ)
81		simp-4l 795	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝜑)
82		0red 11235	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ∈ ℝ)
83		elfzelz 13578	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → 𝑤 ∈ ℤ)
84	83	zred 12725	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → 𝑤 ∈ ℝ)
85	84	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℝ)
86		0red 11235	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ∈ ℝ)
87	53	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑖 + 1) ∈ ℝ)
88	84	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℝ)
89		0red 11235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → 0 ∈ ℝ)
90	55	ltp1d 12169	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 < (𝑖 + 1))
91	89, 55, 53, 57, 90	lelttrd 11392	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (0..^𝑀) → 0 < (𝑖 + 1))
92	91	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 < (𝑖 + 1))
93		elfzle1 13581	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → (𝑖 + 1) ≤ 𝑤)
94	93	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑖 + 1) ≤ 𝑤)
95	86, 87, 88, 92, 94	ltletrd 11394	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 < 𝑤)
96	95	adantlr 728	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 < 𝑤)
97	82, 85, 96	ltled 11382	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ≤ 𝑤)
98	97	adantlll 731	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ≤ 𝑤)
99	98	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ≤ 𝑤)
100	84	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℝ)
101		peano2rem 11549	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℝ → (𝑗 − 1) ∈ ℝ)
102	67, 101	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
103	102	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑗 − 1) ∈ ℝ)
104	69	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑀 ∈ ℝ)
105		elfzle2 13582	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → 𝑤 ≤ (𝑗 − 1))
106	105	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ≤ (𝑗 − 1))
107		zlem1lt 12670	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑗 ≤ 𝑀 ↔ (𝑗 − 1) < 𝑀))
108	33, 45, 107	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 ≤ 𝑀 ↔ (𝑗 − 1) < 𝑀))
109	73, 108	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
110	109	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑗 − 1) < 𝑀)
111	100, 103, 104, 106, 110	lelttrd 11392	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 < 𝑀)
112	111	adantlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝑗 ∈ (0...𝑀) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 < 𝑀)
113	112	adantlll 731	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 < 𝑀)
114	83	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℤ)
115		0zd 12627	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ∈ ℤ)
116	45	ad3antlr 744	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑀 ∈ ℤ)
117		elfzo 13716	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑤 ∈ (0..^𝑀) ↔ (0 ≤ 𝑤 ∧ 𝑤 < 𝑀)))
118	114, 115, 116, 117	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑤 ∈ (0..^𝑀) ↔ (0 ≤ 𝑤 ∧ 𝑤 < 𝑀)))
119	99, 113, 118	mpbir2and 726	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ (0..^𝑀))
120	15	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
121		elfzofz 13731	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (0..^𝑀) → 𝑤 ∈ (0...𝑀))
122	121	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → 𝑤 ∈ (0...𝑀))
123	120, 122	ffvelcdmd 7078	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘𝑤) ∈ ℝ)
124		fzofzp1 13820	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (0..^𝑀) → (𝑤 + 1) ∈ (0...𝑀))
125	124	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑤 + 1) ∈ (0...𝑀))
126	120, 125	ffvelcdmd 7078	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘(𝑤 + 1)) ∈ ℝ)
127		eleq1w 2843	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑤 → (𝑖 ∈ (0..^𝑀) ↔ 𝑤 ∈ (0..^𝑀)))
128	127	anbi2d 642	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑤 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑤 ∈ (0..^𝑀))))
129		fveq2 6878	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑤 → (𝑄‘𝑖) = (𝑄‘𝑤))
130		oveq1 7420	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑤 → (𝑖 + 1) = (𝑤 + 1))
131	130	fveq2d 6882	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑤 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑤 + 1)))
132	129, 131	breq12d 5116	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑤 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘𝑤) < (𝑄‘(𝑤 + 1))))
133	128, 132	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑤 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘𝑤) < (𝑄‘(𝑤 + 1)))))
134	7	simprrd 786	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
135	134	r19.21bi 3254	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
136	133, 135	chvarvv 2022	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘𝑤) < (𝑄‘(𝑤 + 1)))
137	123, 126, 136	ltled 11382	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘𝑤) ≤ (𝑄‘(𝑤 + 1)))
138	81, 119, 137	syl2anc 596	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑄‘𝑤) ≤ (𝑄‘(𝑤 + 1)))
139	42, 80, 138	monoord 14096	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ≤ (𝑄‘𝑗))
140	139	3adantl3 1187	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ≤ (𝑄‘𝑗))
141	15	ffvelcdmda 7077	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ)
142	141	3adant3 1150	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) ∈ ℝ)
143		simp3 1156	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) = 𝑋)
144	142, 143	eqled 11337	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) ≤ 𝑋)
145	144	3adant1r 1196	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) ≤ 𝑋)
146	145	adantr 486	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘𝑗) ≤ 𝑋)
147	21, 29, 26, 140, 146	letrd 11391	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ≤ 𝑋)
148	21, 26, 147	lensymd 11385	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → ¬ 𝑋 < (𝑄‘(𝑖 + 1)))
149	148	intnand 494	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → ¬ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1))))
150	67	ad2antlr 740	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → 𝑗 ∈ ℝ)
151	55	ad3antlr 744	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → 𝑖 ∈ ℝ)
152		simpr 490	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → ¬ 𝑖 < 𝑗)
153	150, 151, 152	nltled 11384	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → 𝑗 ≤ 𝑖)
154	153	3adantl3 1187	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ ¬ 𝑖 < 𝑗) → 𝑗 ≤ 𝑖)
155		eqcom 2767	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑗) = 𝑋 ↔ 𝑋 = (𝑄‘𝑗))
156	155	birani 509	. . . . . . . . . . 11 ⊢ (((𝑄‘𝑗) = 𝑋 ∧ 𝑗 ≤ 𝑖) → 𝑋 = (𝑄‘𝑗))
157	156	3ad2antl3 1206	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → 𝑋 = (𝑄‘𝑗))
158	33	ad2antlr 740	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑗 ∈ ℤ)
159	31	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑖 ∈ ℤ)
160		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑗 ≤ 𝑖)
161		eluz2 12893	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ≥‘𝑗) ↔ (𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑗 ≤ 𝑖))
162	158, 159, 160, 161	syl3anbrc 1362	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑖 ∈ (ℤ≥‘𝑗))
163	162	adantlll 731	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑖 ∈ (ℤ≥‘𝑗))
164	16	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑄:(0...𝑀)⟶ℝ)
165		0zd 12627	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ∈ ℤ)
166	45	ad2antlr 740	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑀 ∈ ℤ)
167		elfzelz 13578	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ (𝑗...𝑖) → 𝑤 ∈ ℤ)
168	167	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ ℤ)
169	165, 166, 168	3jca 1146	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ))
170		0red 11235	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ∈ ℝ)
171	67	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑗 ∈ ℝ)
172	167	zred 12725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝑗...𝑖) → 𝑤 ∈ ℝ)
173	172	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ ℝ)
174		elfzle1 13581	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
175	174	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ≤ 𝑗)
176		elfzle1 13581	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝑗...𝑖) → 𝑗 ≤ 𝑤)
177	176	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑗 ≤ 𝑤)
178	170, 171, 173, 175, 177	letrd 11391	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ≤ 𝑤)
179	178	adantll 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ≤ 𝑤)
180	172	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ ℝ)
181		elfzoel2 13713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
182	181	zred 12725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑀 ∈ ℝ)
183	182	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑀 ∈ ℝ)
184	55	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑖 ∈ ℝ)
185		elfzle2 13582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ (𝑗...𝑖) → 𝑤 ≤ 𝑖)
186	185	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ≤ 𝑖)
187		elfzolt2 13724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 < 𝑀)
188	187	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑖 < 𝑀)
189	180, 184, 183, 186, 188	lelttrd 11392	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 < 𝑀)
190	180, 183, 189	ltled 11382	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ≤ 𝑀)
191	190	adantlr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ≤ 𝑀)
192	169, 179, 191	jca32 525	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ (0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀)))
193	192	adantlll 731	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ (0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀)))
194		elfz2 13568	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ (0 ≤ 𝑤 ∧ 𝑤 ≤ 𝑀)))
195	193, 194	sylibr 237	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ (0...𝑀))
196	164, 195	ffvelcdmd 7078	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → (𝑄‘𝑤) ∈ ℝ)
197	196	adantlr 728	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) ∧ 𝑤 ∈ (𝑗...𝑖)) → (𝑄‘𝑤) ∈ ℝ)
198		simplll 787	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝜑)
199		0red 11235	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ∈ ℝ)
200	67	ad2antlr 740	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑗 ∈ ℝ)
201		elfzelz 13578	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑤 ∈ ℤ)
202	201	zred 12725	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑤 ∈ ℝ)
203	202	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ ℝ)
204	174	ad2antlr 740	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ≤ 𝑗)
205		elfzle1 13581	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑗 ≤ 𝑤)
206	205	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑗 ≤ 𝑤)
207	199, 200, 203, 204, 206	letrd 11391	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ≤ 𝑤)
208	202	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ ℝ)
209	55	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑖 ∈ ℝ)
210	182	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑀 ∈ ℝ)
211		peano2rem 11549	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ ℝ → (𝑖 − 1) ∈ ℝ)
212	209, 211	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑖 − 1) ∈ ℝ)
213		elfzle2 13582	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑤 ≤ (𝑖 − 1))
214	213	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ≤ (𝑖 − 1))
215	209	ltm1d 12171	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑖 − 1) < 𝑖)
216	208, 212, 209, 214, 215	lelttrd 11392	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 < 𝑖)
217	187	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑖 < 𝑀)
218	208, 209, 210, 216, 217	lttrd 11395	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 < 𝑀)
219	218	adantlr 728	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 < 𝑀)
220	201	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ ℤ)
221		0zd 12627	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ∈ ℤ)
222	181	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑀 ∈ ℤ)
223	220, 221, 222, 117	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑤 ∈ (0..^𝑀) ↔ (0 ≤ 𝑤 ∧ 𝑤 < 𝑀)))
224	207, 219, 223	mpbir2and 726	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ (0..^𝑀))
225	224	adantlll 731	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ (0..^𝑀))
226	198, 225, 137	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑄‘𝑤) ≤ (𝑄‘(𝑤 + 1)))
227	226	adantlr 728	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑄‘𝑤) ≤ (𝑄‘(𝑤 + 1)))
228	163, 197, 227	monoord 14096	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → (𝑄‘𝑗) ≤ (𝑄‘𝑖))
229	228	3adantl3 1187	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → (𝑄‘𝑗) ≤ (𝑄‘𝑖))
230	157, 229	eqbrtrd 5127	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → 𝑋 ≤ (𝑄‘𝑖))
231	24	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
232		elfzofz 13731	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
233	232	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
234	16, 233	ffvelcdmd 7078	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
235	231, 234	lenltd 11380	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 ≤ (𝑄‘𝑖) ↔ ¬ (𝑄‘𝑖) < 𝑋))
236	235	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ≤ 𝑖) → (𝑋 ≤ (𝑄‘𝑖) ↔ ¬ (𝑄‘𝑖) < 𝑋))
237	236	3ad2antl1 1204	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → (𝑋 ≤ (𝑄‘𝑖) ↔ ¬ (𝑄‘𝑖) < 𝑋))
238	230, 237	mpbid 235	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → ¬ (𝑄‘𝑖) < 𝑋)
239	154, 238	syldan 603	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ ¬ 𝑖 < 𝑗) → ¬ (𝑄‘𝑖) < 𝑋)
240	239	intnanrd 495	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ ¬ 𝑖 < 𝑗) → ¬ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1))))
241	149, 240	pm2.61dan 825	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → ¬ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1))))
242	241	intnand 494	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → ¬ (((𝑄‘𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑋 ∈ ℝ*) ∧ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1)))))
243		elioo3g 13427	. . . 4 ⊢ (𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ (((𝑄‘𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑋 ∈ ℝ*) ∧ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1)))))
244	242, 243	sylnibr 332	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → ¬ 𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
245	244	rexlimdv3a 3167	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋 → ¬ 𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
246	14, 245	mpd 16	1 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3076  ∃wrex 3086  {crab 3412   ⊆ wss 3899   class class class wbr 5103   ↦ cmpt 5186  ran crn 5656   Fn wfn 6528  ⟶wf 6529  ‘cfv 6533  (class class class)co 7413   ↑_m cmap 8826  ℝcr 11123  0cc0 11124  1c1 11125   + caddc 11127  ℝ^*cxr 11266   < clt 11267   ≤ cle 11268   − cmin 11465  ℕcn 12257  ℤcz 12615  ℤ_≥cuz 12887  (,)cioo 13398  ...cfz 13561  ..^cfzo 13709

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7863  df-1st 7986  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-er 8696  df-map 8828  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11467  df-neg 11468  df-nn 12258  df-n0 12529  df-z 12616  df-uz 12888  df-ioo 13402  df-fz 13562  df-fzo 13710

This theorem is used by:  fourierdlem38  46973  fourierdlem74  47008  fourierdlem75  47009  fourierdlem88  47022  fourierdlem103  47037  fourierdlem104  47038