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