Step | Hyp | Ref
| Expression |
1 | | fourierdlem12.4 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ran 𝑄) |
2 | | fourierdlem12.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) |
3 | | fourierdlem12.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℕ) |
4 | | fourierdlem12.1 |
. . . . . . . . . 10
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
5 | 4 | fourierdlem2 43232 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
6 | 3, 5 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
7 | 2, 6 | mpbid 235 |
. . . . . . 7
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
8 | 7 | simpld 498 |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈ (ℝ ↑m
(0...𝑀))) |
9 | | elmapi 8471 |
. . . . . 6
⊢ (𝑄 ∈ (ℝ
↑m (0...𝑀))
→ 𝑄:(0...𝑀)⟶ℝ) |
10 | | ffn 6514 |
. . . . . 6
⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀)) |
11 | 8, 9, 10 | 3syl 18 |
. . . . 5
⊢ (𝜑 → 𝑄 Fn (0...𝑀)) |
12 | | fvelrnb 6742 |
. . . . 5
⊢ (𝑄 Fn (0...𝑀) → (𝑋 ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋)) |
13 | 11, 12 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑋 ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋)) |
14 | 1, 13 | mpbid 235 |
. . 3
⊢ (𝜑 → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋) |
15 | 14 | adantr 484 |
. 2
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋) |
16 | 8, 9 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) |
17 | 16 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ) |
18 | | fzofzp1 13237 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀)) |
19 | 18 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀)) |
20 | 17, 19 | ffvelrnd 6874 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ) |
21 | 20 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ∈ ℝ) |
22 | 21 | 3ad2antl1 1186 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ∈ ℝ) |
23 | | frn 6521 |
. . . . . . . . . . . 12
⊢ (𝑄:(0...𝑀)⟶ℝ → ran 𝑄 ⊆
ℝ) |
24 | 16, 23 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝑄 ⊆ ℝ) |
25 | 24, 1 | sseldd 3888 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℝ) |
26 | 25 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑖 < 𝑗) → 𝑋 ∈ ℝ) |
27 | 26 | 3ad2antl1 1186 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → 𝑋 ∈ ℝ) |
28 | 17 | ffvelrnda 6873 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ) |
29 | 28 | 3adant3 1133 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) ∈ ℝ) |
30 | 29 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘𝑗) ∈ ℝ) |
31 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑖 < 𝑗) |
32 | | elfzoelz 13141 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℤ) |
33 | 32 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑖 ∈ ℤ) |
34 | | elfzelz 13010 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ) |
35 | 34 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ ℤ) |
36 | | zltp1le 12125 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑖 < 𝑗 ↔ (𝑖 + 1) ≤ 𝑗)) |
37 | 33, 35, 36 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑖 < 𝑗 ↔ (𝑖 + 1) ≤ 𝑗)) |
38 | 31, 37 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑖 + 1) ≤ 𝑗) |
39 | 33 | peano2zd 12183 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑖 + 1) ∈ ℤ) |
40 | | eluz 12350 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 + 1) ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑗 ∈
(ℤ≥‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑗)) |
41 | 39, 35, 40 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑗 ∈ (ℤ≥‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑗)) |
42 | 38, 41 | mpbird 260 |
. . . . . . . . . . . 12
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ (ℤ≥‘(𝑖 + 1))) |
43 | 42 | adantlll 718 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ (ℤ≥‘(𝑖 + 1))) |
44 | 17 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑄:(0...𝑀)⟶ℝ) |
45 | | 0zd 12086 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ∈ ℤ) |
46 | | elfzel2 13008 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ) |
47 | 46 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑀 ∈ ℤ) |
48 | | elfzelz 13010 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ((𝑖 + 1)...𝑗) → 𝑤 ∈ ℤ) |
49 | 48 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ ℤ) |
50 | | 0red 10734 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ∈ ℝ) |
51 | 48 | zred 12180 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ ((𝑖 + 1)...𝑗) → 𝑤 ∈ ℝ) |
52 | 51 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ ℝ) |
53 | 32 | peano2zd 12183 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ ℤ) |
54 | 53 | zred 12180 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ ℝ) |
55 | 54 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑖 + 1) ∈ ℝ) |
56 | 32 | zred 12180 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℝ) |
57 | 56 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑖 ∈ ℝ) |
58 | | elfzole1 13149 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (0..^𝑀) → 0 ≤ 𝑖) |
59 | 58 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ≤ 𝑖) |
60 | 57 | ltp1d 11660 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑖 < (𝑖 + 1)) |
61 | 50, 57, 55, 59, 60 | lelttrd 10888 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 < (𝑖 + 1)) |
62 | | elfzle1 13013 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ ((𝑖 + 1)...𝑗) → (𝑖 + 1) ≤ 𝑤) |
63 | 62 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑖 + 1) ≤ 𝑤) |
64 | 50, 55, 52, 61, 63 | ltletrd 10890 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 < 𝑤) |
65 | 50, 52, 64 | ltled 10878 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ≤ 𝑤) |
66 | 65 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 0 ≤ 𝑤) |
67 | 51 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ ℝ) |
68 | 34 | zred 12180 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ) |
69 | 68 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑗 ∈ ℝ) |
70 | 46 | zred 12180 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ) |
71 | 70 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑀 ∈ ℝ) |
72 | | elfzle2 13014 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ ((𝑖 + 1)...𝑗) → 𝑤 ≤ 𝑗) |
73 | 72 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ≤ 𝑗) |
74 | | elfzle2 13014 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀) |
75 | 74 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑗 ≤ 𝑀) |
76 | 67, 69, 71, 73, 75 | letrd 10887 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ≤ 𝑀) |
77 | 76 | adantll 714 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ≤ 𝑀) |
78 | 45, 47, 49, 66, 77 | elfzd 13001 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ (0...𝑀)) |
79 | 78 | adantlll 718 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → 𝑤 ∈ (0...𝑀)) |
80 | 44, 79 | ffvelrnd 6874 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑄‘𝑤) ∈ ℝ) |
81 | 80 | adantlr 715 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...𝑗)) → (𝑄‘𝑤) ∈ ℝ) |
82 | | simp-4l 783 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝜑) |
83 | | 0red 10734 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ∈
ℝ) |
84 | | elfzelz 13010 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → 𝑤 ∈ ℤ) |
85 | 84 | zred 12180 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → 𝑤 ∈ ℝ) |
86 | 85 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℝ) |
87 | | 0red 10734 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ∈
ℝ) |
88 | 54 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑖 + 1) ∈ ℝ) |
89 | 85 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℝ) |
90 | | 0red 10734 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (0..^𝑀) → 0 ∈ ℝ) |
91 | 56 | ltp1d 11660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 < (𝑖 + 1)) |
92 | 90, 56, 54, 58, 91 | lelttrd 10888 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (0..^𝑀) → 0 < (𝑖 + 1)) |
93 | 92 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 < (𝑖 + 1)) |
94 | | elfzle1 13013 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → (𝑖 + 1) ≤ 𝑤) |
95 | 94 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑖 + 1) ≤ 𝑤) |
96 | 87, 88, 89, 93, 95 | ltletrd 10890 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 < 𝑤) |
97 | 96 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 < 𝑤) |
98 | 83, 86, 97 | ltled 10878 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ≤ 𝑤) |
99 | 98 | adantlll 718 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ≤ 𝑤) |
100 | 99 | adantlr 715 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ≤ 𝑤) |
101 | 85 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℝ) |
102 | | peano2rem 11043 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℝ → (𝑗 − 1) ∈
ℝ) |
103 | 68, 102 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) ∈ ℝ) |
104 | 103 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑗 − 1) ∈ ℝ) |
105 | 70 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑀 ∈ ℝ) |
106 | | elfzle2 13014 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1)) → 𝑤 ≤ (𝑗 − 1)) |
107 | 106 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ≤ (𝑗 − 1)) |
108 | | zlem1lt 12127 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑗 ≤ 𝑀 ↔ (𝑗 − 1) < 𝑀)) |
109 | 34, 46, 108 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...𝑀) → (𝑗 ≤ 𝑀 ↔ (𝑗 − 1) < 𝑀)) |
110 | 74, 109 | mpbid 235 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 1) < 𝑀) |
111 | 110 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑗 − 1) < 𝑀) |
112 | 101, 104,
105, 107, 111 | lelttrd 10888 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 < 𝑀) |
113 | 112 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝑗 ∈ (0...𝑀) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 < 𝑀) |
114 | 113 | adantlll 718 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 < 𝑀) |
115 | 84 | adantl 485 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ ℤ) |
116 | | 0zd 12086 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 0 ∈
ℤ) |
117 | 46 | ad3antlr 731 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑀 ∈ ℤ) |
118 | | elfzo 13143 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ℤ ∧ 0 ∈
ℤ ∧ 𝑀 ∈
ℤ) → (𝑤 ∈
(0..^𝑀) ↔ (0 ≤
𝑤 ∧ 𝑤 < 𝑀))) |
119 | 115, 116,
117, 118 | syl3anc 1372 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑤 ∈ (0..^𝑀) ↔ (0 ≤ 𝑤 ∧ 𝑤 < 𝑀))) |
120 | 100, 114,
119 | mpbir2and 713 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → 𝑤 ∈ (0..^𝑀)) |
121 | 16 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ) |
122 | | elfzofz 13156 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ (0..^𝑀) → 𝑤 ∈ (0...𝑀)) |
123 | 122 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → 𝑤 ∈ (0...𝑀)) |
124 | 121, 123 | ffvelrnd 6874 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘𝑤) ∈ ℝ) |
125 | | fzofzp1 13237 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ (0..^𝑀) → (𝑤 + 1) ∈ (0...𝑀)) |
126 | 125 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑤 + 1) ∈ (0...𝑀)) |
127 | 121, 126 | ffvelrnd 6874 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘(𝑤 + 1)) ∈ ℝ) |
128 | | eleq1w 2816 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑤 → (𝑖 ∈ (0..^𝑀) ↔ 𝑤 ∈ (0..^𝑀))) |
129 | 128 | anbi2d 632 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑤 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑤 ∈ (0..^𝑀)))) |
130 | | fveq2 6686 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑤 → (𝑄‘𝑖) = (𝑄‘𝑤)) |
131 | | oveq1 7189 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 𝑤 → (𝑖 + 1) = (𝑤 + 1)) |
132 | 131 | fveq2d 6690 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑤 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑤 + 1))) |
133 | 130, 132 | breq12d 5053 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑤 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘𝑤) < (𝑄‘(𝑤 + 1)))) |
134 | 129, 133 | imbi12d 348 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑤 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘𝑤) < (𝑄‘(𝑤 + 1))))) |
135 | 7 | simprrd 774 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
136 | 135 | r19.21bi 3122 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
137 | 134, 136 | chvarvv 2010 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘𝑤) < (𝑄‘(𝑤 + 1))) |
138 | 124, 127,
137 | ltled 10878 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ (0..^𝑀)) → (𝑄‘𝑤) ≤ (𝑄‘(𝑤 + 1))) |
139 | 82, 120, 138 | syl2anc 587 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑤 ∈ ((𝑖 + 1)...(𝑗 − 1))) → (𝑄‘𝑤) ≤ (𝑄‘(𝑤 + 1))) |
140 | 43, 81, 139 | monoord 13504 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ≤ (𝑄‘𝑗)) |
141 | 140 | 3adantl3 1169 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ≤ (𝑄‘𝑗)) |
142 | 16 | ffvelrnda 6873 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ) |
143 | 142 | 3adant3 1133 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) ∈ ℝ) |
144 | | simp3 1139 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) = 𝑋) |
145 | 143, 144 | eqled 10833 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) ≤ 𝑋) |
146 | 145 | 3adant1r 1178 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → (𝑄‘𝑗) ≤ 𝑋) |
147 | 146 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘𝑗) ≤ 𝑋) |
148 | 22, 30, 27, 141, 147 | letrd 10887 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → (𝑄‘(𝑖 + 1)) ≤ 𝑋) |
149 | 22, 27, 148 | lensymd 10881 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → ¬ 𝑋 < (𝑄‘(𝑖 + 1))) |
150 | 149 | intnand 492 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑖 < 𝑗) → ¬ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1)))) |
151 | 68 | ad2antlr 727 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → 𝑗 ∈ ℝ) |
152 | 56 | ad3antlr 731 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → 𝑖 ∈ ℝ) |
153 | | simpr 488 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → ¬ 𝑖 < 𝑗) |
154 | 151, 152,
153 | nltled 10880 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 < 𝑗) → 𝑗 ≤ 𝑖) |
155 | 154 | 3adantl3 1169 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ ¬ 𝑖 < 𝑗) → 𝑗 ≤ 𝑖) |
156 | | eqcom 2746 |
. . . . . . . . . . . . 13
⊢ ((𝑄‘𝑗) = 𝑋 ↔ 𝑋 = (𝑄‘𝑗)) |
157 | 156 | biimpi 219 |
. . . . . . . . . . . 12
⊢ ((𝑄‘𝑗) = 𝑋 → 𝑋 = (𝑄‘𝑗)) |
158 | 157 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝑄‘𝑗) = 𝑋 ∧ 𝑗 ≤ 𝑖) → 𝑋 = (𝑄‘𝑗)) |
159 | 158 | 3ad2antl3 1188 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → 𝑋 = (𝑄‘𝑗)) |
160 | 34 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑗 ∈ ℤ) |
161 | 32 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑖 ∈ ℤ) |
162 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑗 ≤ 𝑖) |
163 | | eluz2 12342 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈
(ℤ≥‘𝑗) ↔ (𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑗 ≤ 𝑖)) |
164 | 160, 161,
162, 163 | syl3anbrc 1344 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑖 ∈ (ℤ≥‘𝑗)) |
165 | 164 | adantlll 718 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → 𝑖 ∈ (ℤ≥‘𝑗)) |
166 | 17 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑄:(0...𝑀)⟶ℝ) |
167 | | 0zd 12086 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ∈ ℤ) |
168 | 46 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑀 ∈ ℤ) |
169 | | elfzelz 13010 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ (𝑗...𝑖) → 𝑤 ∈ ℤ) |
170 | 169 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ ℤ) |
171 | 167, 168,
170 | 3jca 1129 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈
ℤ)) |
172 | | 0red 10734 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ∈ ℝ) |
173 | 68 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑗 ∈ ℝ) |
174 | 169 | zred 12180 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ (𝑗...𝑖) → 𝑤 ∈ ℝ) |
175 | 174 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ ℝ) |
176 | | elfzle1 13013 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗) |
177 | 176 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ≤ 𝑗) |
178 | | elfzle1 13013 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ (𝑗...𝑖) → 𝑗 ≤ 𝑤) |
179 | 178 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑗 ≤ 𝑤) |
180 | 172, 173,
175, 177, 179 | letrd 10887 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ≤ 𝑤) |
181 | 180 | adantll 714 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 0 ≤ 𝑤) |
182 | 174 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ ℝ) |
183 | | elfzoel2 13140 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ (0..^𝑀) → 𝑀 ∈ ℤ) |
184 | 183 | zred 12180 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (0..^𝑀) → 𝑀 ∈ ℝ) |
185 | 184 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑀 ∈ ℝ) |
186 | 56 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑖 ∈ ℝ) |
187 | | elfzle2 13014 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ (𝑗...𝑖) → 𝑤 ≤ 𝑖) |
188 | 187 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ≤ 𝑖) |
189 | | elfzolt2 13150 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 < 𝑀) |
190 | 189 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑖 < 𝑀) |
191 | 182, 186,
185, 188, 190 | lelttrd 10888 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 < 𝑀) |
192 | 182, 185,
191 | ltled 10878 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ≤ 𝑀) |
193 | 192 | adantlr 715 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ≤ 𝑀) |
194 | 171, 181,
193 | jca32 519 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ (0 ≤
𝑤 ∧ 𝑤 ≤ 𝑀))) |
195 | 194 | adantlll 718 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ (0 ≤
𝑤 ∧ 𝑤 ≤ 𝑀))) |
196 | | elfz2 13000 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ (0 ≤
𝑤 ∧ 𝑤 ≤ 𝑀))) |
197 | 195, 196 | sylibr 237 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → 𝑤 ∈ (0...𝑀)) |
198 | 166, 197 | ffvelrnd 6874 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...𝑖)) → (𝑄‘𝑤) ∈ ℝ) |
199 | 198 | adantlr 715 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) ∧ 𝑤 ∈ (𝑗...𝑖)) → (𝑄‘𝑤) ∈ ℝ) |
200 | | simplll 775 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝜑) |
201 | | 0red 10734 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ∈
ℝ) |
202 | 68 | ad2antlr 727 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑗 ∈ ℝ) |
203 | | elfzelz 13010 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑤 ∈ ℤ) |
204 | 203 | zred 12180 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑤 ∈ ℝ) |
205 | 204 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ ℝ) |
206 | 176 | ad2antlr 727 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ≤ 𝑗) |
207 | | elfzle1 13013 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑗 ≤ 𝑤) |
208 | 207 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑗 ≤ 𝑤) |
209 | 201, 202,
205, 206, 208 | letrd 10887 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ≤ 𝑤) |
210 | 204 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ ℝ) |
211 | 56 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑖 ∈ ℝ) |
212 | 184 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑀 ∈ ℝ) |
213 | | peano2rem 11043 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ ℝ → (𝑖 − 1) ∈
ℝ) |
214 | 211, 213 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑖 − 1) ∈ ℝ) |
215 | | elfzle2 13014 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ (𝑗...(𝑖 − 1)) → 𝑤 ≤ (𝑖 − 1)) |
216 | 215 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ≤ (𝑖 − 1)) |
217 | 211 | ltm1d 11662 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑖 − 1) < 𝑖) |
218 | 210, 214,
211, 216, 217 | lelttrd 10888 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 < 𝑖) |
219 | 189 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑖 < 𝑀) |
220 | 210, 211,
212, 218, 219 | lttrd 10891 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 < 𝑀) |
221 | 220 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 < 𝑀) |
222 | 203 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ ℤ) |
223 | | 0zd 12086 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 0 ∈
ℤ) |
224 | 183 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑀 ∈ ℤ) |
225 | 222, 223,
224, 118 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑤 ∈ (0..^𝑀) ↔ (0 ≤ 𝑤 ∧ 𝑤 < 𝑀))) |
226 | 209, 221,
225 | mpbir2and 713 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ (0..^𝑀)) |
227 | 226 | adantlll 718 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → 𝑤 ∈ (0..^𝑀)) |
228 | 200, 227,
138 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑄‘𝑤) ≤ (𝑄‘(𝑤 + 1))) |
229 | 228 | adantlr 715 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) ∧ 𝑤 ∈ (𝑗...(𝑖 − 1))) → (𝑄‘𝑤) ≤ (𝑄‘(𝑤 + 1))) |
230 | 165, 199,
229 | monoord 13504 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 ≤ 𝑖) → (𝑄‘𝑗) ≤ (𝑄‘𝑖)) |
231 | 230 | 3adantl3 1169 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → (𝑄‘𝑗) ≤ (𝑄‘𝑖)) |
232 | 159, 231 | eqbrtrd 5062 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → 𝑋 ≤ (𝑄‘𝑖)) |
233 | 25 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ) |
234 | | elfzofz 13156 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀)) |
235 | 234 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀)) |
236 | 17, 235 | ffvelrnd 6874 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ) |
237 | 233, 236 | lenltd 10876 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 ≤ (𝑄‘𝑖) ↔ ¬ (𝑄‘𝑖) < 𝑋)) |
238 | 237 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ≤ 𝑖) → (𝑋 ≤ (𝑄‘𝑖) ↔ ¬ (𝑄‘𝑖) < 𝑋)) |
239 | 238 | 3ad2antl1 1186 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → (𝑋 ≤ (𝑄‘𝑖) ↔ ¬ (𝑄‘𝑖) < 𝑋)) |
240 | 232, 239 | mpbid 235 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ 𝑗 ≤ 𝑖) → ¬ (𝑄‘𝑖) < 𝑋) |
241 | 155, 240 | syldan 594 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ ¬ 𝑖 < 𝑗) → ¬ (𝑄‘𝑖) < 𝑋) |
242 | 241 | intnanrd 493 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) ∧ ¬ 𝑖 < 𝑗) → ¬ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1)))) |
243 | 150, 242 | pm2.61dan 813 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → ¬ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1)))) |
244 | 243 | intnand 492 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → ¬ (((𝑄‘𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑋 ∈ ℝ*)
∧ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1))))) |
245 | | elioo3g 12862 |
. . . 4
⊢ (𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ (((𝑄‘𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑋 ∈ ℝ*)
∧ ((𝑄‘𝑖) < 𝑋 ∧ 𝑋 < (𝑄‘(𝑖 + 1))))) |
246 | 244, 245 | sylnibr 332 |
. . 3
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 ∈ (0...𝑀) ∧ (𝑄‘𝑗) = 𝑋) → ¬ 𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
247 | 246 | rexlimdv3a 3197 |
. 2
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑋 → ¬ 𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
248 | 15, 247 | mpd 15 |
1
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |