Step | Hyp | Ref
| Expression |
1 | | fourierdlem25.i |
. . 3
⊢ 𝐼 = sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}, ℝ, < ) |
2 | | ssrab2 3998 |
. . . 4
⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ⊆ (0..^𝑀) |
3 | | ltso 10918 |
. . . . . 6
⊢ < Or
ℝ |
4 | 3 | a1i 11 |
. . . . 5
⊢ (𝜑 → < Or
ℝ) |
5 | | fzofi 13552 |
. . . . . . 7
⊢
(0..^𝑀) ∈
Fin |
6 | | ssfi 8856 |
. . . . . . 7
⊢
(((0..^𝑀) ∈ Fin
∧ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ⊆ (0..^𝑀)) → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ∈ Fin) |
7 | 5, 2, 6 | mp2an 692 |
. . . . . 6
⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ∈ Fin |
8 | 7 | a1i 11 |
. . . . 5
⊢ (𝜑 → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ∈ Fin) |
9 | | 0zd 12193 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℤ) |
10 | | fourierdlem25.m |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℕ) |
11 | 10 | nnzd 12286 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
12 | 10 | nngt0d 11884 |
. . . . . . . 8
⊢ (𝜑 → 0 < 𝑀) |
13 | | fzolb 13254 |
. . . . . . . 8
⊢ (0 ∈
(0..^𝑀) ↔ (0 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 0 < 𝑀)) |
14 | 9, 11, 12, 13 | syl3anbrc 1345 |
. . . . . . 7
⊢ (𝜑 → 0 ∈ (0..^𝑀)) |
15 | | fourierdlem25.qf |
. . . . . . . . 9
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) |
16 | | elfzofz 13263 |
. . . . . . . . . 10
⊢ (0 ∈
(0..^𝑀) → 0 ∈
(0...𝑀)) |
17 | 14, 16 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ (0...𝑀)) |
18 | 15, 17 | ffvelrnd 6910 |
. . . . . . . 8
⊢ (𝜑 → (𝑄‘0) ∈ ℝ) |
19 | 10 | nnnn0d 12155 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
20 | | nn0uz 12481 |
. . . . . . . . . . . . 13
⊢
ℕ0 = (ℤ≥‘0) |
21 | 19, 20 | eleqtrdi 2848 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
22 | | eluzfz2 13125 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈
(ℤ≥‘0) → 𝑀 ∈ (0...𝑀)) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ (0...𝑀)) |
24 | 15, 23 | ffvelrnd 6910 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ) |
25 | 18, 24 | iccssred 13027 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑄‘0)[,](𝑄‘𝑀)) ⊆ ℝ) |
26 | | fourierdlem25.cel |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) |
27 | 25, 26 | sseldd 3907 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℝ) |
28 | 18 | rexrd 10888 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄‘0) ∈
ℝ*) |
29 | 24 | rexrd 10888 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄‘𝑀) ∈
ℝ*) |
30 | | iccgelb 12996 |
. . . . . . . . 9
⊢ (((𝑄‘0) ∈
ℝ* ∧ (𝑄‘𝑀) ∈ ℝ* ∧ 𝐶 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → (𝑄‘0) ≤ 𝐶) |
31 | 28, 29, 26, 30 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝑄‘0) ≤ 𝐶) |
32 | | fourierdlem25.cnel |
. . . . . . . . . 10
⊢ (𝜑 → ¬ 𝐶 ∈ ran 𝑄) |
33 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐶 = (𝑄‘0)) → 𝐶 = (𝑄‘0)) |
34 | 15 | ffnd 6551 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 Fn (0...𝑀)) |
35 | 34 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐶 = (𝑄‘0)) → 𝑄 Fn (0...𝑀)) |
36 | 17 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐶 = (𝑄‘0)) → 0 ∈ (0...𝑀)) |
37 | | fnfvelrn 6906 |
. . . . . . . . . . . 12
⊢ ((𝑄 Fn (0...𝑀) ∧ 0 ∈ (0...𝑀)) → (𝑄‘0) ∈ ran 𝑄) |
38 | 35, 36, 37 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐶 = (𝑄‘0)) → (𝑄‘0) ∈ ran 𝑄) |
39 | 33, 38 | eqeltrd 2838 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐶 = (𝑄‘0)) → 𝐶 ∈ ran 𝑄) |
40 | 32, 39 | mtand 816 |
. . . . . . . . 9
⊢ (𝜑 → ¬ 𝐶 = (𝑄‘0)) |
41 | 40 | neqned 2947 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ≠ (𝑄‘0)) |
42 | 18, 27, 31, 41 | leneltd 10991 |
. . . . . . 7
⊢ (𝜑 → (𝑄‘0) < 𝐶) |
43 | | fveq2 6722 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (𝑄‘𝑘) = (𝑄‘0)) |
44 | 43 | breq1d 5068 |
. . . . . . . 8
⊢ (𝑘 = 0 → ((𝑄‘𝑘) < 𝐶 ↔ (𝑄‘0) < 𝐶)) |
45 | 44 | elrab 3607 |
. . . . . . 7
⊢ (0 ∈
{𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) < 𝐶)) |
46 | 14, 42, 45 | sylanbrc 586 |
. . . . . 6
⊢ (𝜑 → 0 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}) |
47 | 46 | ne0d 4255 |
. . . . 5
⊢ (𝜑 → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ≠ ∅) |
48 | | fzossfz 13266 |
. . . . . . . 8
⊢
(0..^𝑀) ⊆
(0...𝑀) |
49 | | fzssz 13119 |
. . . . . . . . 9
⊢
(0...𝑀) ⊆
ℤ |
50 | | zssre 12188 |
. . . . . . . . 9
⊢ ℤ
⊆ ℝ |
51 | 49, 50 | sstri 3915 |
. . . . . . . 8
⊢
(0...𝑀) ⊆
ℝ |
52 | 48, 51 | sstri 3915 |
. . . . . . 7
⊢
(0..^𝑀) ⊆
ℝ |
53 | 2, 52 | sstri 3915 |
. . . . . 6
⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ⊆ ℝ |
54 | 53 | a1i 11 |
. . . . 5
⊢ (𝜑 → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ⊆ ℝ) |
55 | | fisupcl 9090 |
. . . . 5
⊢ (( <
Or ℝ ∧ ({𝑘 ∈
(0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ∈ Fin ∧ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ≠ ∅ ∧ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ⊆ ℝ)) → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}, ℝ, < ) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}) |
56 | 4, 8, 47, 54, 55 | syl13anc 1374 |
. . . 4
⊢ (𝜑 → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}, ℝ, < ) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}) |
57 | 2, 56 | sseldi 3904 |
. . 3
⊢ (𝜑 → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}, ℝ, < ) ∈ (0..^𝑀)) |
58 | 1, 57 | eqeltrid 2842 |
. 2
⊢ (𝜑 → 𝐼 ∈ (0..^𝑀)) |
59 | 48, 58 | sseldi 3904 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ (0...𝑀)) |
60 | 15, 59 | ffvelrnd 6910 |
. . . 4
⊢ (𝜑 → (𝑄‘𝐼) ∈ ℝ) |
61 | 60 | rexrd 10888 |
. . 3
⊢ (𝜑 → (𝑄‘𝐼) ∈
ℝ*) |
62 | | fzofzp1 13344 |
. . . . . 6
⊢ (𝐼 ∈ (0..^𝑀) → (𝐼 + 1) ∈ (0...𝑀)) |
63 | 58, 62 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐼 + 1) ∈ (0...𝑀)) |
64 | 15, 63 | ffvelrnd 6910 |
. . . 4
⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ) |
65 | 64 | rexrd 10888 |
. . 3
⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈
ℝ*) |
66 | 1, 56 | eqeltrid 2842 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}) |
67 | | fveq2 6722 |
. . . . . . 7
⊢ (𝑘 = 𝐼 → (𝑄‘𝑘) = (𝑄‘𝐼)) |
68 | 67 | breq1d 5068 |
. . . . . 6
⊢ (𝑘 = 𝐼 → ((𝑄‘𝑘) < 𝐶 ↔ (𝑄‘𝐼) < 𝐶)) |
69 | 68 | elrab 3607 |
. . . . 5
⊢ (𝐼 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ↔ (𝐼 ∈ (0..^𝑀) ∧ (𝑄‘𝐼) < 𝐶)) |
70 | 66, 69 | sylib 221 |
. . . 4
⊢ (𝜑 → (𝐼 ∈ (0..^𝑀) ∧ (𝑄‘𝐼) < 𝐶)) |
71 | 70 | simprd 499 |
. . 3
⊢ (𝜑 → (𝑄‘𝐼) < 𝐶) |
72 | 52, 58 | sseldi 3904 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ ℝ) |
73 | | ltp1 11677 |
. . . . . . . . . 10
⊢ (𝐼 ∈ ℝ → 𝐼 < (𝐼 + 1)) |
74 | | id 22 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ ℝ → 𝐼 ∈
ℝ) |
75 | | peano2re 11010 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ ℝ → (𝐼 + 1) ∈
ℝ) |
76 | 74, 75 | ltnled 10984 |
. . . . . . . . . 10
⊢ (𝐼 ∈ ℝ → (𝐼 < (𝐼 + 1) ↔ ¬ (𝐼 + 1) ≤ 𝐼)) |
77 | 73, 76 | mpbid 235 |
. . . . . . . . 9
⊢ (𝐼 ∈ ℝ → ¬
(𝐼 + 1) ≤ 𝐼) |
78 | 72, 77 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ¬ (𝐼 + 1) ≤ 𝐼) |
79 | 48, 49 | sstri 3915 |
. . . . . . . . . . . 12
⊢
(0..^𝑀) ⊆
ℤ |
80 | 2, 79 | sstri 3915 |
. . . . . . . . . . 11
⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ⊆ ℤ |
81 | 80 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ⊆ ℤ) |
82 | | elrabi 3601 |
. . . . . . . . . . . . . . 15
⊢ (ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} → ℎ ∈ (0..^𝑀)) |
83 | | elfzo0le 13291 |
. . . . . . . . . . . . . . 15
⊢ (ℎ ∈ (0..^𝑀) → ℎ ≤ 𝑀) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} → ℎ ≤ 𝑀) |
85 | 84 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}) → ℎ ≤ 𝑀) |
86 | 85 | ralrimiva 3105 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}ℎ ≤ 𝑀) |
87 | | breq2 5062 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑀 → (ℎ ≤ 𝑚 ↔ ℎ ≤ 𝑀)) |
88 | 87 | ralbidv 3118 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑀 → (∀ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}ℎ ≤ 𝑚 ↔ ∀ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}ℎ ≤ 𝑀)) |
89 | 88 | rspcev 3542 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧
∀ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}ℎ ≤ 𝑀) → ∃𝑚 ∈ ℤ ∀ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}ℎ ≤ 𝑚) |
90 | 11, 86, 89 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → ∃𝑚 ∈ ℤ ∀ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}ℎ ≤ 𝑚) |
91 | 90 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → ∃𝑚 ∈ ℤ ∀ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}ℎ ≤ 𝑚) |
92 | | elfzuz 13113 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 + 1) ∈ (0...𝑀) → (𝐼 + 1) ∈
(ℤ≥‘0)) |
93 | 63, 92 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐼 + 1) ∈
(ℤ≥‘0)) |
94 | 93 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) ∈
(ℤ≥‘0)) |
95 | 11 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → 𝑀 ∈ ℤ) |
96 | 51, 63 | sseldi 3904 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐼 + 1) ∈ ℝ) |
97 | 96 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) ∈ ℝ) |
98 | 95 | zred 12287 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → 𝑀 ∈ ℝ) |
99 | | elfzle2 13121 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 + 1) ∈ (0...𝑀) → (𝐼 + 1) ≤ 𝑀) |
100 | 63, 99 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐼 + 1) ≤ 𝑀) |
101 | 100 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) ≤ 𝑀) |
102 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝑄‘(𝐼 + 1)) < 𝐶) |
103 | 64 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝑄‘(𝐼 + 1)) ∈ ℝ) |
104 | 27 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → 𝐶 ∈ ℝ) |
105 | 103, 104 | ltnled 10984 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → ((𝑄‘(𝐼 + 1)) < 𝐶 ↔ ¬ 𝐶 ≤ (𝑄‘(𝐼 + 1)))) |
106 | 102, 105 | mpbid 235 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → ¬ 𝐶 ≤ (𝑄‘(𝐼 + 1))) |
107 | | iccleub 12995 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑄‘0) ∈
ℝ* ∧ (𝑄‘𝑀) ∈ ℝ* ∧ 𝐶 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝐶 ≤ (𝑄‘𝑀)) |
108 | 28, 29, 26, 107 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐶 ≤ (𝑄‘𝑀)) |
109 | 108 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑀 = (𝐼 + 1)) → 𝐶 ≤ (𝑄‘𝑀)) |
110 | | fveq2 6722 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 = (𝐼 + 1) → (𝑄‘𝑀) = (𝑄‘(𝐼 + 1))) |
111 | 110 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑀 = (𝐼 + 1)) → (𝑄‘𝑀) = (𝑄‘(𝐼 + 1))) |
112 | 109, 111 | breqtrd 5084 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑀 = (𝐼 + 1)) → 𝐶 ≤ (𝑄‘(𝐼 + 1))) |
113 | 112 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) ∧ 𝑀 = (𝐼 + 1)) → 𝐶 ≤ (𝑄‘(𝐼 + 1))) |
114 | 106, 113 | mtand 816 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → ¬ 𝑀 = (𝐼 + 1)) |
115 | 114 | neqned 2947 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → 𝑀 ≠ (𝐼 + 1)) |
116 | 97, 98, 101, 115 | leneltd 10991 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) < 𝑀) |
117 | | elfzo2 13251 |
. . . . . . . . . . . 12
⊢ ((𝐼 + 1) ∈ (0..^𝑀) ↔ ((𝐼 + 1) ∈
(ℤ≥‘0) ∧ 𝑀 ∈ ℤ ∧ (𝐼 + 1) < 𝑀)) |
118 | 94, 95, 116, 117 | syl3anbrc 1345 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) ∈ (0..^𝑀)) |
119 | | fveq2 6722 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝐼 + 1) → (𝑄‘𝑘) = (𝑄‘(𝐼 + 1))) |
120 | 119 | breq1d 5068 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝐼 + 1) → ((𝑄‘𝑘) < 𝐶 ↔ (𝑄‘(𝐼 + 1)) < 𝐶)) |
121 | 120 | elrab 3607 |
. . . . . . . . . . 11
⊢ ((𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ↔ ((𝐼 + 1) ∈ (0..^𝑀) ∧ (𝑄‘(𝐼 + 1)) < 𝐶)) |
122 | 118, 102,
121 | sylanbrc 586 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}) |
123 | | suprzub 12540 |
. . . . . . . . . 10
⊢ (({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ⊆ ℤ ∧ ∃𝑚 ∈ ℤ ∀ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}ℎ ≤ 𝑚 ∧ (𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}) → (𝐼 + 1) ≤ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}, ℝ, < )) |
124 | 81, 91, 122, 123 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) ≤ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}, ℝ, < )) |
125 | 124, 1 | breqtrrdi 5100 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) ≤ 𝐼) |
126 | 78, 125 | mtand 816 |
. . . . . . 7
⊢ (𝜑 → ¬ (𝑄‘(𝐼 + 1)) < 𝐶) |
127 | | eqcom 2744 |
. . . . . . . . . . 11
⊢ ((𝑄‘(𝐼 + 1)) = 𝐶 ↔ 𝐶 = (𝑄‘(𝐼 + 1))) |
128 | 127 | biimpi 219 |
. . . . . . . . . 10
⊢ ((𝑄‘(𝐼 + 1)) = 𝐶 → 𝐶 = (𝑄‘(𝐼 + 1))) |
129 | 128 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = 𝐶) → 𝐶 = (𝑄‘(𝐼 + 1))) |
130 | 34 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = 𝐶) → 𝑄 Fn (0...𝑀)) |
131 | 63 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = 𝐶) → (𝐼 + 1) ∈ (0...𝑀)) |
132 | | fnfvelrn 6906 |
. . . . . . . . . 10
⊢ ((𝑄 Fn (0...𝑀) ∧ (𝐼 + 1) ∈ (0...𝑀)) → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄) |
133 | 130, 131,
132 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = 𝐶) → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄) |
134 | 129, 133 | eqeltrd 2838 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = 𝐶) → 𝐶 ∈ ran 𝑄) |
135 | 32, 134 | mtand 816 |
. . . . . . 7
⊢ (𝜑 → ¬ (𝑄‘(𝐼 + 1)) = 𝐶) |
136 | 126, 135 | jca 515 |
. . . . . 6
⊢ (𝜑 → (¬ (𝑄‘(𝐼 + 1)) < 𝐶 ∧ ¬ (𝑄‘(𝐼 + 1)) = 𝐶)) |
137 | | pm4.56 989 |
. . . . . 6
⊢ ((¬
(𝑄‘(𝐼 + 1)) < 𝐶 ∧ ¬ (𝑄‘(𝐼 + 1)) = 𝐶) ↔ ¬ ((𝑄‘(𝐼 + 1)) < 𝐶 ∨ (𝑄‘(𝐼 + 1)) = 𝐶)) |
138 | 136, 137 | sylib 221 |
. . . . 5
⊢ (𝜑 → ¬ ((𝑄‘(𝐼 + 1)) < 𝐶 ∨ (𝑄‘(𝐼 + 1)) = 𝐶)) |
139 | 64, 27 | leloed 10980 |
. . . . 5
⊢ (𝜑 → ((𝑄‘(𝐼 + 1)) ≤ 𝐶 ↔ ((𝑄‘(𝐼 + 1)) < 𝐶 ∨ (𝑄‘(𝐼 + 1)) = 𝐶))) |
140 | 138, 139 | mtbird 328 |
. . . 4
⊢ (𝜑 → ¬ (𝑄‘(𝐼 + 1)) ≤ 𝐶) |
141 | 27, 64 | ltnled 10984 |
. . . 4
⊢ (𝜑 → (𝐶 < (𝑄‘(𝐼 + 1)) ↔ ¬ (𝑄‘(𝐼 + 1)) ≤ 𝐶)) |
142 | 140, 141 | mpbird 260 |
. . 3
⊢ (𝜑 → 𝐶 < (𝑄‘(𝐼 + 1))) |
143 | 61, 65, 27, 71, 142 | eliood 42719 |
. 2
⊢ (𝜑 → 𝐶 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) |
144 | | fveq2 6722 |
. . . . 5
⊢ (𝑗 = 𝐼 → (𝑄‘𝑗) = (𝑄‘𝐼)) |
145 | | oveq1 7225 |
. . . . . 6
⊢ (𝑗 = 𝐼 → (𝑗 + 1) = (𝐼 + 1)) |
146 | 145 | fveq2d 6726 |
. . . . 5
⊢ (𝑗 = 𝐼 → (𝑄‘(𝑗 + 1)) = (𝑄‘(𝐼 + 1))) |
147 | 144, 146 | oveq12d 7236 |
. . . 4
⊢ (𝑗 = 𝐼 → ((𝑄‘𝑗)(,)(𝑄‘(𝑗 + 1))) = ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) |
148 | 147 | eleq2d 2823 |
. . 3
⊢ (𝑗 = 𝐼 → (𝐶 ∈ ((𝑄‘𝑗)(,)(𝑄‘(𝑗 + 1))) ↔ 𝐶 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))) |
149 | 148 | rspcev 3542 |
. 2
⊢ ((𝐼 ∈ (0..^𝑀) ∧ 𝐶 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → ∃𝑗 ∈ (0..^𝑀)𝐶 ∈ ((𝑄‘𝑗)(,)(𝑄‘(𝑗 + 1)))) |
150 | 58, 143, 149 | syl2anc 587 |
1
⊢ (𝜑 → ∃𝑗 ∈ (0..^𝑀)𝐶 ∈ ((𝑄‘𝑗)(,)(𝑄‘(𝑗 + 1)))) |