Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem12 Structured version   Visualization version   GIF version

Theorem fourierdlem12 40756
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.
StepHypRef Expression
1 fourierdlem12.4 . . . 4 (𝜑𝑋 ∈ ran 𝑄)
2 fourierdlem12.3 . . . . . . . 8 (𝜑𝑄 ∈ (𝑃𝑀))
3 fourierdlem12.2 . . . . . . . . 9 (𝜑𝑀 ∈ ℕ)
4 fourierdlem12.1 . . . . . . . . . 10 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
54fourierdlem2 40746 . . . . . . . . 9 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
63, 5syl 17 . . . . . . . 8 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
72, 6mpbid 222 . . . . . . 7 (𝜑 → (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
87simpld 477 . . . . . 6 (𝜑𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)))
9 elmapi 7996 . . . . . 6 (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
10 ffn 6158 . . . . . 6 (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
118, 9, 103syl 18 . . . . 5 (𝜑𝑄 Fn (0...𝑀))
12 fvelrnb 6357 . . . . 5 (𝑄 Fn (0...𝑀) → (𝑋 ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = 𝑋))
1311, 12syl 17 . . . 4 (𝜑 → (𝑋 ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = 𝑋))
141, 13mpbid 222 . . 3 (𝜑 → ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = 𝑋)
1514adantr 472 . 2 ((𝜑𝑖 ∈ (0..^𝑀)) → ∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = 𝑋)
168, 9syl 17 . . . . . . . . . . . 12 (𝜑𝑄:(0...𝑀)⟶ℝ)
1716adantr 472 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
18 fzofzp1 12680 . . . . . . . . . . . 12 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
1918adantl 473 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
2017, 19ffvelrnd 6475 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
2120adantr 472 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
22213ad2antl1 1177 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
23 frn 6166 . . . . . . . . . . . 12 (𝑄:(0...𝑀)⟶ℝ → ran 𝑄 ⊆ ℝ)
2416, 23syl 17 . . . . . . . . . . 11 (𝜑 → ran 𝑄 ⊆ ℝ)
2524, 1sseldd 3710 . . . . . . . . . 10 (𝜑𝑋 ∈ ℝ)
2625ad2antrr 764 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑖 < 𝑗) → 𝑋 ∈ ℝ)
27263ad2antl1 1177 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → 𝑋 ∈ ℝ)
2817ffvelrnda 6474 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ)
29283adant3 1124 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) → (𝑄𝑗) ∈ ℝ)
3029adantr 472 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄𝑗) ∈ ℝ)
31 simpr 479 . . . . . . . . . . . . . 14 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑖 < 𝑗)
32 elfzoelz 12585 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℤ)
3332ad2antrr 764 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑖 ∈ ℤ)
34 elfzelz 12456 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
3534ad2antlr 765 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ ℤ)
36 zltp1le 11540 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑖 < 𝑗 ↔ (𝑖 + 1) ≤ 𝑗))
3733, 35, 36syl2anc 696 . . . . . . . . . . . . . 14 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑖 < 𝑗 ↔ (𝑖 + 1) ≤ 𝑗))
3831, 37mpbid 222 . . . . . . . . . . . . 13 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑖 + 1) ≤ 𝑗)
3933peano2zd 11598 . . . . . . . . . . . . . 14 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑖 + 1) ∈ ℤ)
40 eluz 11814 . . . . . . . . . . . . . 14 (((𝑖 + 1) ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ (ℤ‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑗))
4139, 35, 40syl2anc 696 . . . . . . . . . . . . 13 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑗 ∈ (ℤ‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑗))
4238, 41mpbird 247 . . . . . . . . . . . 12 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ (ℤ‘(𝑖 + 1)))
4342adantlll 756 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ (ℤ‘(𝑖 + 1)))
4417ad2antrr 764 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑄:(0...𝑀)⟶ℝ)
45 0red 10154 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ∈ ℝ)
46 elfzelz 12456 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ((𝑖 + 1)...𝑗) → 𝑤 ∈ ℤ)
4746zred 11595 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ((𝑖 + 1)...𝑗) → 𝑤 ∈ ℝ)
4847adantl 473 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ ℝ)
4932peano2zd 11598 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ ℤ)
5049zred 11595 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ ℝ)
5150adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑖 + 1) ∈ ℝ)
5232zred 11595 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℝ)
5352adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑖 ∈ ℝ)
54 elfzole1 12593 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (0..^𝑀) → 0 ≤ 𝑖)
5554adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ≤ 𝑖)
5653ltp1d 11067 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑖 < (𝑖 + 1))
5745, 53, 51, 55, 56lelttrd 10308 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 < (𝑖 + 1))
58 elfzle1 12458 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ((𝑖 + 1)...𝑗) → (𝑖 + 1) ≤ 𝑤)
5958adantl 473 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑖 + 1) ≤ 𝑤)
6045, 51, 48, 57, 59ltletrd 10310 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 < 𝑤)
6145, 48, 60ltled 10298 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ≤ 𝑤)
6261adantlr 753 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ≤ 𝑤)
6347adantl 473 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ ℝ)
6434zred 11595 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
6564adantr 472 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑗 ∈ ℝ)
66 elfzel2 12454 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
6766zred 11595 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
6867adantr 472 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑀 ∈ ℝ)
69 elfzle2 12459 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ((𝑖 + 1)...𝑗) → 𝑤𝑗)
7069adantl 473 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤𝑗)
71 elfzle2 12459 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → 𝑗𝑀)
7271adantr 472 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑗𝑀)
7363, 65, 68, 70, 72letrd 10307 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤𝑀)
7473adantll 752 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤𝑀)
7546adantl 473 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ ℤ)
76 0zd 11502 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ∈ ℤ)
7766ad2antlr 765 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑀 ∈ ℤ)
78 elfz 12446 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑤 ∈ (0...𝑀) ↔ (0 ≤ 𝑤𝑤𝑀)))
7975, 76, 77, 78syl3anc 1439 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑤 ∈ (0...𝑀) ↔ (0 ≤ 𝑤𝑤𝑀)))
8062, 74, 79mpbir2and 995 . . . . . . . . . . . . . 14 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ (0...𝑀))
8180adantlll 756 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ (0...𝑀))
8244, 81ffvelrnd 6475 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑄𝑤) ∈ ℝ)
8382adantlr 753 . . . . . . . . . . 11 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑄𝑤) ∈ ℝ)
84 simp-4l 825 . . . . . . . . . . . 12 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝜑)
85 0red 10154 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ∈ ℝ)
86 elfzelz 12456 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → 𝑤 ∈ ℤ)
8786zred 11595 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → 𝑤 ∈ ℝ)
8887adantl 473 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℝ)
89 0red 10154 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ∈ ℝ)
9050adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑖 + 1) ∈ ℝ)
9187adantl 473 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℝ)
92 0red 10154 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (0..^𝑀) → 0 ∈ ℝ)
9352ltp1d 11067 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (0..^𝑀) → 𝑖 < (𝑖 + 1))
9492, 52, 50, 54, 93lelttrd 10308 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (0..^𝑀) → 0 < (𝑖 + 1))
9594adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 < (𝑖 + 1))
96 elfzle1 12458 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → (𝑖 + 1) ≤ 𝑤)
9796adantl 473 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑖 + 1) ≤ 𝑤)
9889, 90, 91, 95, 97ltletrd 10310 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 < 𝑤)
9998adantlr 753 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 < 𝑤)
10085, 88, 99ltled 10298 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ≤ 𝑤)
101100adantlll 756 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ≤ 𝑤)
102101adantlr 753 . . . . . . . . . . . . 13 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ≤ 𝑤)
10387adantl 473 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℝ)
104 peano2rem 10461 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℝ → (𝑗 − 1) ∈ ℝ)
10564, 104syl 17 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ)
106105adantr 472 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑗 − 1) ∈ ℝ)
10767adantr 472 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑀 ∈ ℝ)
108 elfzle2 12459 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → 𝑤 ≤ (𝑗 − 1))
109108adantl 473 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ≤ (𝑗 − 1))
110 zlem1lt 11542 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑗𝑀 ↔ (𝑗 − 1) < 𝑀))
11134, 66, 110syl2anc 696 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → (𝑗𝑀 ↔ (𝑗 − 1) < 𝑀))
11271, 111mpbid 222 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀)
113112adantr 472 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑗 − 1) < 𝑀)
114103, 106, 107, 109, 113lelttrd 10308 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 < 𝑀)
115114adantlr 753 . . . . . . . . . . . . . 14 (((𝑗 ∈ (0...𝑀) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 < 𝑀)
116115adantlll 756 . . . . . . . . . . . . 13 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 < 𝑀)
11786adantl 473 . . . . . . . . . . . . . 14 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℤ)
118 0zd 11502 . . . . . . . . . . . . . 14 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ∈ ℤ)
11966ad3antlr 769 . . . . . . . . . . . . . 14 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑀 ∈ ℤ)
120 elfzo 12587 . . . . . . . . . . . . . 14 ((𝑤 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑤 ∈ (0..^𝑀) ↔ (0 ≤ 𝑤𝑤 < 𝑀)))
121117, 118, 119, 120syl3anc 1439 . . . . . . . . . . . . 13 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑤 ∈ (0..^𝑀) ↔ (0 ≤ 𝑤𝑤 < 𝑀)))
122102, 116, 121mpbir2and 995 . . . . . . . . . . . 12 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ (0..^𝑀))
12316adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
124 elfzofz 12600 . . . . . . . . . . . . . . 15 (𝑤 ∈ (0..^𝑀) → 𝑤 ∈ (0...𝑀))
125124adantl 473 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ (0..^𝑀)) → 𝑤 ∈ (0...𝑀))
126123, 125ffvelrnd 6475 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ (0..^𝑀)) → (𝑄𝑤) ∈ ℝ)
127 fzofzp1 12680 . . . . . . . . . . . . . . 15 (𝑤 ∈ (0..^𝑀) → (𝑤 + 1) ∈ (0...𝑀))
128127adantl 473 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ (0..^𝑀)) → (𝑤 + 1) ∈ (0...𝑀))
129123, 128ffvelrnd 6475 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ (0..^𝑀)) → (𝑄‘(𝑤 + 1)) ∈ ℝ)
130 eleq1 2791 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑤 → (𝑖 ∈ (0..^𝑀) ↔ 𝑤 ∈ (0..^𝑀)))
131130anbi2d 742 . . . . . . . . . . . . . . 15 (𝑖 = 𝑤 → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑𝑤 ∈ (0..^𝑀))))
132 fveq2 6304 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑤 → (𝑄𝑖) = (𝑄𝑤))
133 oveq1 6772 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑤 → (𝑖 + 1) = (𝑤 + 1))
134133fveq2d 6308 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑤 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑤 + 1)))
135132, 134breq12d 4773 . . . . . . . . . . . . . . 15 (𝑖 = 𝑤 → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄𝑤) < (𝑄‘(𝑤 + 1))))
136131, 135imbi12d 333 . . . . . . . . . . . . . 14 (𝑖 = 𝑤 → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑𝑤 ∈ (0..^𝑀)) → (𝑄𝑤) < (𝑄‘(𝑤 + 1)))))
1377simprrd 814 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))
138137r19.21bi 3034 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
139136, 138chvarv 2372 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ (0..^𝑀)) → (𝑄𝑤) < (𝑄‘(𝑤 + 1)))
140126, 129, 139ltled 10298 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ (0..^𝑀)) → (𝑄𝑤) ≤ (𝑄‘(𝑤 + 1)))
14184, 122, 140syl2anc 696 . . . . . . . . . . 11 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑄𝑤) ≤ (𝑄‘(𝑤 + 1)))
14243, 83, 141monoord 12946 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ≤ (𝑄𝑗))
1431423adantl3 1154 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ≤ (𝑄𝑗))
14416ffvelrnda 6474 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑄𝑗) ∈ ℝ)
1451443adant3 1124 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) → (𝑄𝑗) ∈ ℝ)
146 simp3 1130 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) → (𝑄𝑗) = 𝑋)
147145, 146eqled 10253 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) → (𝑄𝑗) ≤ 𝑋)
1481473adant1r 1168 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) → (𝑄𝑗) ≤ 𝑋)
149148adantr 472 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄𝑗) ≤ 𝑋)
15022, 30, 27, 143, 149letrd 10307 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ≤ 𝑋)
15122, 27, 150lensymd 10301 . . . . . . 7 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → ¬ 𝑋 < (𝑄‘(𝑖 + 1)))
152151intnand 1000 . . . . . 6 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → ¬ ((𝑄𝑖) < 𝑋𝑋 < (𝑄‘(𝑖 + 1))))
15364ad2antlr 765 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → 𝑗 ∈ ℝ)
15452ad3antlr 769 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → 𝑖 ∈ ℝ)
155 simpr 479 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → ¬ 𝑖 < 𝑗)
156153, 154, 155nltled 10300 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → 𝑗𝑖)
1571563adantl3 1154 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) ∧ ¬ 𝑖 < 𝑗) → 𝑗𝑖)
158 eqcom 2731 . . . . . . . . . . . . 13 ((𝑄𝑗) = 𝑋𝑋 = (𝑄𝑗))
159158biimpi 206 . . . . . . . . . . . 12 ((𝑄𝑗) = 𝑋𝑋 = (𝑄𝑗))
160159adantr 472 . . . . . . . . . . 11 (((𝑄𝑗) = 𝑋𝑗𝑖) → 𝑋 = (𝑄𝑗))
1611603ad2antl3 1179 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) ∧ 𝑗𝑖) → 𝑋 = (𝑄𝑗))
16234ad2antlr 765 . . . . . . . . . . . . . 14 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗𝑖) → 𝑗 ∈ ℤ)
16332ad2antrr 764 . . . . . . . . . . . . . 14 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗𝑖) → 𝑖 ∈ ℤ)
164 simpr 479 . . . . . . . . . . . . . 14 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗𝑖) → 𝑗𝑖)
165 eluz2 11806 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ𝑗) ↔ (𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑗𝑖))
166162, 163, 164, 165syl3anbrc 1383 . . . . . . . . . . . . 13 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗𝑖) → 𝑖 ∈ (ℤ𝑗))
167166adantlll 756 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗𝑖) → 𝑖 ∈ (ℤ𝑗))
16817ad2antrr 764 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑄:(0...𝑀)⟶ℝ)
169 0zd 11502 . . . . . . . . . . . . . . . . . 18 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ∈ ℤ)
17066ad2antlr 765 . . . . . . . . . . . . . . . . . 18 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑀 ∈ ℤ)
171 elfzelz 12456 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ (𝑗...𝑖) → 𝑤 ∈ ℤ)
172171adantl 473 . . . . . . . . . . . . . . . . . 18 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ ℤ)
173169, 170, 1723jca 1379 . . . . . . . . . . . . . . . . 17 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ))
174 0red 10154 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ∈ ℝ)
17564adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑗 ∈ ℝ)
176171zred 11595 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ (𝑗...𝑖) → 𝑤 ∈ ℝ)
177176adantl 473 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ ℝ)
178 elfzle1 12458 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
179178adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ≤ 𝑗)
180 elfzle1 12458 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ (𝑗...𝑖) → 𝑗𝑤)
181180adantl 473 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑗𝑤)
182174, 175, 177, 179, 181letrd 10307 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ≤ 𝑤)
183182adantll 752 . . . . . . . . . . . . . . . . 17 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ≤ 𝑤)
184176adantl 473 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ ℝ)
185 elfzoel2 12584 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
186185zred 11595 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (0..^𝑀) → 𝑀 ∈ ℝ)
187186adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑀 ∈ ℝ)
18852adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑖 ∈ ℝ)
189 elfzle2 12459 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ (𝑗...𝑖) → 𝑤𝑖)
190189adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤𝑖)
191 elfzolt2 12594 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (0..^𝑀) → 𝑖 < 𝑀)
192191adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑖 < 𝑀)
193184, 188, 187, 190, 192lelttrd 10308 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 < 𝑀)
194184, 187, 193ltled 10298 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤𝑀)
195194adantlr 753 . . . . . . . . . . . . . . . . 17 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤𝑀)
196173, 183, 195jca32 559 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ (0 ≤ 𝑤𝑤𝑀)))
197196adantlll 756 . . . . . . . . . . . . . . 15 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ (0 ≤ 𝑤𝑤𝑀)))
198 elfz2 12447 . . . . . . . . . . . . . . 15 (𝑤 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ (0 ≤ 𝑤𝑤𝑀)))
199197, 198sylibr 224 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ (0...𝑀))
200168, 199ffvelrnd 6475 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → (𝑄𝑤) ∈ ℝ)
201200adantlr 753 . . . . . . . . . . . 12 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗𝑖) ∧ 𝑤 ∈ (𝑗...𝑖)) → (𝑄𝑤) ∈ ℝ)
202 simplll 815 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝜑)
203 0red 10154 . . . . . . . . . . . . . . . . 17 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ∈ ℝ)
20464ad2antlr 765 . . . . . . . . . . . . . . . . 17 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑗 ∈ ℝ)
205 elfzelz 12456 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑤 ∈ ℤ)
206205zred 11595 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑤 ∈ ℝ)
207206adantl 473 . . . . . . . . . . . . . . . . 17 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ ℝ)
208178ad2antlr 765 . . . . . . . . . . . . . . . . 17 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ≤ 𝑗)
209 elfzle1 12458 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑗𝑤)
210209adantl 473 . . . . . . . . . . . . . . . . 17 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑗𝑤)
211203, 204, 207, 208, 210letrd 10307 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ≤ 𝑤)
212206adantl 473 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ ℝ)
21352adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑖 ∈ ℝ)
214186adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑀 ∈ ℝ)
215 peano2rem 10461 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ ℝ → (𝑖 − 1) ∈ ℝ)
216213, 215syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑖 − 1) ∈ ℝ)
217 elfzle2 12459 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑤 ≤ (𝑖 − 1))
218217adantl 473 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ≤ (𝑖 − 1))
219213ltm1d 11069 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑖 − 1) < 𝑖)
220212, 216, 213, 218, 219lelttrd 10308 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 < 𝑖)
221191adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑖 < 𝑀)
222212, 213, 214, 220, 221lttrd 10311 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 < 𝑀)
223222adantlr 753 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 < 𝑀)
224205adantl 473 . . . . . . . . . . . . . . . . 17 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ ℤ)
225 0zd 11502 . . . . . . . . . . . . . . . . 17 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ∈ ℤ)
226185ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑀 ∈ ℤ)
227224, 225, 226, 120syl3anc 1439 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑤 ∈ (0..^𝑀) ↔ (0 ≤ 𝑤𝑤 < 𝑀)))
228211, 223, 227mpbir2and 995 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ (0..^𝑀))
229228adantlll 756 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ (0..^𝑀))
230202, 229, 140syl2anc 696 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑄𝑤) ≤ (𝑄‘(𝑤 + 1)))
231230adantlr 753 . . . . . . . . . . . 12 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗𝑖) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑄𝑤) ≤ (𝑄‘(𝑤 + 1)))
232167, 201, 231monoord 12946 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗𝑖) → (𝑄𝑗) ≤ (𝑄𝑖))
2332323adantl3 1154 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) ∧ 𝑗𝑖) → (𝑄𝑗) ≤ (𝑄𝑖))
234161, 233eqbrtrd 4782 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) ∧ 𝑗𝑖) → 𝑋 ≤ (𝑄𝑖))
23525adantr 472 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
236 elfzofz 12600 . . . . . . . . . . . . . 14 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
237236adantl 473 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
23817, 237ffvelrnd 6475 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
239235, 238lenltd 10296 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 ≤ (𝑄𝑖) ↔ ¬ (𝑄𝑖) < 𝑋))
240239adantr 472 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗𝑖) → (𝑋 ≤ (𝑄𝑖) ↔ ¬ (𝑄𝑖) < 𝑋))
2412403ad2antl1 1177 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) ∧ 𝑗𝑖) → (𝑋 ≤ (𝑄𝑖) ↔ ¬ (𝑄𝑖) < 𝑋))
242234, 241mpbid 222 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) ∧ 𝑗𝑖) → ¬ (𝑄𝑖) < 𝑋)
243157, 242syldan 488 . . . . . . 7 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) ∧ ¬ 𝑖 < 𝑗) → ¬ (𝑄𝑖) < 𝑋)
244243intnanrd 1001 . . . . . 6 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) ∧ ¬ 𝑖 < 𝑗) → ¬ ((𝑄𝑖) < 𝑋𝑋 < (𝑄‘(𝑖 + 1))))
245152, 244pm2.61dan 867 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) → ¬ ((𝑄𝑖) < 𝑋𝑋 < (𝑄‘(𝑖 + 1))))
246245intnand 1000 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) → ¬ (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ*𝑋 ∈ ℝ*) ∧ ((𝑄𝑖) < 𝑋𝑋 < (𝑄‘(𝑖 + 1)))))
247 elioo3g 12318 . . . 4 (𝑋 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ*𝑋 ∈ ℝ*) ∧ ((𝑄𝑖) < 𝑋𝑋 < (𝑄‘(𝑖 + 1)))))
248246, 247sylnibr 318 . . 3 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄𝑗) = 𝑋) → ¬ 𝑋 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
249248rexlimdv3a 3135 . 2 ((𝜑𝑖 ∈ (0..^𝑀)) → (∃𝑗 ∈ (0...𝑀)(𝑄𝑗) = 𝑋 → ¬ 𝑋 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
25015, 249mpd 15 1 ((𝜑𝑖 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072   = wceq 1596  wcel 2103  wral 3014  wrex 3015  {crab 3018  wss 3680   class class class wbr 4760  cmpt 4837  ran crn 5219   Fn wfn 5996  wf 5997  cfv 6001  (class class class)co 6765  𝑚 cmap 7974  cr 10048  0cc0 10049  1c1 10050   + caddc 10052  *cxr 10186   < clt 10187  cle 10188  cmin 10379  cn 11133  cz 11490  cuz 11800  (,)cioo 12289  ...cfz 12440  ..^cfzo 12580
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-om 7183  df-1st 7285  df-2nd 7286  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-er 7862  df-map 7976  df-en 8073  df-dom 8074  df-sdom 8075  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-nn 11134  df-n0 11406  df-z 11491  df-uz 11801  df-ioo 12293  df-fz 12441  df-fzo 12581
This theorem is referenced by:  fourierdlem38  40782  fourierdlem74  40817  fourierdlem75  40818  fourierdlem88  40831  fourierdlem103  40846  fourierdlem104  40847
  Copyright terms: Public domain W3C validator