Step | Hyp | Ref
| Expression |
1 | | fourierdlem20.i |
. . 3
⊢ 𝐼 = sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ) |
2 | | ssrab2 3650 |
. . . 4
⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ (0..^𝑀) |
3 | | fzossfz 12357 |
. . . . . . . 8
⊢
(0..^𝑀) ⊆
(0...𝑀) |
4 | | fzssz 12214 |
. . . . . . . 8
⊢
(0...𝑀) ⊆
ℤ |
5 | 3, 4 | sstri 3577 |
. . . . . . 7
⊢
(0..^𝑀) ⊆
ℤ |
6 | 2, 5 | sstri 3577 |
. . . . . 6
⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℤ |
7 | 6 | a1i 11 |
. . . . 5
⊢ (𝜑 → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℤ) |
8 | | 0z 11265 |
. . . . . . . . . 10
⊢ 0 ∈
ℤ |
9 | | 0le0 10987 |
. . . . . . . . . 10
⊢ 0 ≤
0 |
10 | | eluz2 11569 |
. . . . . . . . . 10
⊢ (0 ∈
(ℤ≥‘0) ↔ (0 ∈ ℤ ∧ 0 ∈
ℤ ∧ 0 ≤ 0)) |
11 | 8, 8, 9, 10 | mpbir3an 1237 |
. . . . . . . . 9
⊢ 0 ∈
(ℤ≥‘0) |
12 | 11 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
(ℤ≥‘0)) |
13 | | fourierdlem20.m |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℕ) |
14 | 13 | nnzd 11357 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
15 | 13 | nngt0d 10941 |
. . . . . . . 8
⊢ (𝜑 → 0 < 𝑀) |
16 | | elfzo2 12342 |
. . . . . . . 8
⊢ (0 ∈
(0..^𝑀) ↔ (0 ∈
(ℤ≥‘0) ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀)) |
17 | 12, 14, 15, 16 | syl3anbrc 1239 |
. . . . . . 7
⊢ (𝜑 → 0 ∈ (0..^𝑀)) |
18 | | fourierdlem20.q |
. . . . . . . . 9
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) |
19 | 3, 17 | sseldi 3566 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ (0...𝑀)) |
20 | 18, 19 | ffvelrnd 6268 |
. . . . . . . 8
⊢ (𝜑 → (𝑄‘0) ∈ ℝ) |
21 | | fourierdlem20.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℝ) |
22 | | fourierdlem20.t |
. . . . . . . . . . 11
⊢ 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) |
23 | 21 | rexrd 9968 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
24 | | fourierdlem20.b |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ∈ ℝ) |
25 | 24 | rexrd 9968 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
26 | | fourierdlem20.aleb |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
27 | | lbicc2 12159 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
28 | 23, 25, 26, 27 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) |
29 | | ubicc2 12160 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) |
30 | 23, 25, 26, 29 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵)) |
31 | 28, 30 | jca 553 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵))) |
32 | | prssg 4290 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵))) |
33 | 23, 25, 32 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵))) |
34 | 31, 33 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)) |
35 | | inss2 3796 |
. . . . . . . . . . . . . 14
⊢ (ran
𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵) |
36 | | ioossicc 12130 |
. . . . . . . . . . . . . 14
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
37 | 35, 36 | sstri 3577 |
. . . . . . . . . . . . 13
⊢ (ran
𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵) |
38 | 37 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵)) |
39 | 34, 38 | unssd 3751 |
. . . . . . . . . . 11
⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ (𝐴[,]𝐵)) |
40 | 22, 39 | syl5eqss 3612 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ⊆ (𝐴[,]𝐵)) |
41 | 21, 24 | iccssred 38574 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
42 | 40, 41 | sstrd 3578 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ⊆ ℝ) |
43 | | fourierdlem20.s |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝑇)) |
44 | | isof1o 6473 |
. . . . . . . . . . 11
⊢ (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto→𝑇) |
45 | | f1of 6050 |
. . . . . . . . . . 11
⊢ (𝑆:(0...𝑁)–1-1-onto→𝑇 → 𝑆:(0...𝑁)⟶𝑇) |
46 | 43, 44, 45 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆:(0...𝑁)⟶𝑇) |
47 | | fourierdlem20.j |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ (0..^𝑁)) |
48 | | elfzofz 12354 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁)) |
49 | 47, 48 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ (0...𝑁)) |
50 | 46, 49 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆‘𝐽) ∈ 𝑇) |
51 | 42, 50 | sseldd 3569 |
. . . . . . . 8
⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ) |
52 | | fourierdlem20.q0 |
. . . . . . . 8
⊢ (𝜑 → (𝑄‘0) ≤ 𝐴) |
53 | 40, 50 | sseldd 3569 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆‘𝐽) ∈ (𝐴[,]𝐵)) |
54 | | iccgelb 12101 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝑆‘𝐽) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑆‘𝐽)) |
55 | 23, 25, 53, 54 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ≤ (𝑆‘𝐽)) |
56 | 20, 21, 51, 52, 55 | letrd 10073 |
. . . . . . 7
⊢ (𝜑 → (𝑄‘0) ≤ (𝑆‘𝐽)) |
57 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (𝑄‘𝑘) = (𝑄‘0)) |
58 | 57 | breq1d 4593 |
. . . . . . . 8
⊢ (𝑘 = 0 → ((𝑄‘𝑘) ≤ (𝑆‘𝐽) ↔ (𝑄‘0) ≤ (𝑆‘𝐽))) |
59 | 58 | elrab 3331 |
. . . . . . 7
⊢ (0 ∈
{𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ (𝑆‘𝐽))) |
60 | 17, 56, 59 | sylanbrc 695 |
. . . . . 6
⊢ (𝜑 → 0 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}) |
61 | | ne0i 3880 |
. . . . . 6
⊢ (0 ∈
{𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅) |
62 | 60, 61 | syl 17 |
. . . . 5
⊢ (𝜑 → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅) |
63 | 13 | nnred 10912 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℝ) |
64 | 2 | sseli 3564 |
. . . . . . . . 9
⊢ (𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} → 𝑗 ∈ (0..^𝑀)) |
65 | | elfzo0le 12379 |
. . . . . . . . 9
⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ≤ 𝑀) |
66 | 64, 65 | syl 17 |
. . . . . . . 8
⊢ (𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} → 𝑗 ≤ 𝑀) |
67 | 66 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}) → 𝑗 ≤ 𝑀) |
68 | 67 | ralrimiva 2949 |
. . . . . 6
⊢ (𝜑 → ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑀) |
69 | | breq2 4587 |
. . . . . . . 8
⊢ (𝑥 = 𝑀 → (𝑗 ≤ 𝑥 ↔ 𝑗 ≤ 𝑀)) |
70 | 69 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑥 = 𝑀 → (∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥 ↔ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑀)) |
71 | 70 | rspcev 3282 |
. . . . . 6
⊢ ((𝑀 ∈ ℝ ∧
∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑀) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥) |
72 | 63, 68, 71 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥) |
73 | | suprzcl 11333 |
. . . . 5
⊢ (({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℤ ∧ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥) → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}) |
74 | 7, 62, 72, 73 | syl3anc 1318 |
. . . 4
⊢ (𝜑 → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}) |
75 | 2, 74 | sseldi 3566 |
. . 3
⊢ (𝜑 → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ) ∈ (0..^𝑀)) |
76 | 1, 75 | syl5eqel 2692 |
. 2
⊢ (𝜑 → 𝐼 ∈ (0..^𝑀)) |
77 | 3, 76 | sseldi 3566 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ (0...𝑀)) |
78 | 18, 77 | ffvelrnd 6268 |
. . . 4
⊢ (𝜑 → (𝑄‘𝐼) ∈ ℝ) |
79 | 78 | rexrd 9968 |
. . 3
⊢ (𝜑 → (𝑄‘𝐼) ∈
ℝ*) |
80 | | fzofzp1 12431 |
. . . . . 6
⊢ (𝐼 ∈ (0..^𝑀) → (𝐼 + 1) ∈ (0...𝑀)) |
81 | 76, 80 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐼 + 1) ∈ (0...𝑀)) |
82 | 18, 81 | ffvelrnd 6268 |
. . . 4
⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ) |
83 | 82 | rexrd 9968 |
. . 3
⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈
ℝ*) |
84 | 1, 74 | syl5eqel 2692 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}) |
85 | | nfrab1 3099 |
. . . . . . . 8
⊢
Ⅎ𝑘{𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} |
86 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑘ℝ |
87 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑘
< |
88 | 85, 86, 87 | nfsup 8240 |
. . . . . . 7
⊢
Ⅎ𝑘sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ) |
89 | 1, 88 | nfcxfr 2749 |
. . . . . 6
⊢
Ⅎ𝑘𝐼 |
90 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑘(0..^𝑀) |
91 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑘𝑄 |
92 | 91, 89 | nffv 6110 |
. . . . . . 7
⊢
Ⅎ𝑘(𝑄‘𝐼) |
93 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑘
≤ |
94 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑘(𝑆‘𝐽) |
95 | 92, 93, 94 | nfbr 4629 |
. . . . . 6
⊢
Ⅎ𝑘(𝑄‘𝐼) ≤ (𝑆‘𝐽) |
96 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 𝐼 → (𝑄‘𝑘) = (𝑄‘𝐼)) |
97 | 96 | breq1d 4593 |
. . . . . 6
⊢ (𝑘 = 𝐼 → ((𝑄‘𝑘) ≤ (𝑆‘𝐽) ↔ (𝑄‘𝐼) ≤ (𝑆‘𝐽))) |
98 | 89, 90, 95, 97 | elrabf 3329 |
. . . . 5
⊢ (𝐼 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ↔ (𝐼 ∈ (0..^𝑀) ∧ (𝑄‘𝐼) ≤ (𝑆‘𝐽))) |
99 | 84, 98 | sylib 207 |
. . . 4
⊢ (𝜑 → (𝐼 ∈ (0..^𝑀) ∧ (𝑄‘𝐼) ≤ (𝑆‘𝐽))) |
100 | 99 | simprd 478 |
. . 3
⊢ (𝜑 → (𝑄‘𝐼) ≤ (𝑆‘𝐽)) |
101 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) |
102 | 83 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ∈
ℝ*) |
103 | | iccssxr 12127 |
. . . . . . . . . 10
⊢ (𝐴[,]𝐵) ⊆
ℝ* |
104 | 40, 103 | syl6ss 3580 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ⊆
ℝ*) |
105 | | fzofzp1 12431 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁)) |
106 | 47, 105 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁)) |
107 | 46, 106 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ 𝑇) |
108 | 104, 107 | sseldd 3569 |
. . . . . . . 8
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈
ℝ*) |
109 | 108 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → (𝑆‘(𝐽 + 1)) ∈
ℝ*) |
110 | | xrltnle 9984 |
. . . . . . 7
⊢ (((𝑄‘(𝐼 + 1)) ∈ ℝ* ∧
(𝑆‘(𝐽 + 1)) ∈ ℝ*) →
((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ↔ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1)))) |
111 | 102, 109,
110 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → ((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ↔ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1)))) |
112 | 101, 111 | mpbird 246 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) |
113 | | fzssz 12214 |
. . . . . 6
⊢
(0...𝑁) ⊆
ℤ |
114 | | f1ofo 6057 |
. . . . . . . . . 10
⊢ (𝑆:(0...𝑁)–1-1-onto→𝑇 → 𝑆:(0...𝑁)–onto→𝑇) |
115 | 43, 44, 114 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆:(0...𝑁)–onto→𝑇) |
116 | 115 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → 𝑆:(0...𝑁)–onto→𝑇) |
117 | | ffun 5961 |
. . . . . . . . . . . . . 14
⊢ (𝑄:(0...𝑀)⟶ℝ → Fun 𝑄) |
118 | 18, 117 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Fun 𝑄) |
119 | | fdm 5964 |
. . . . . . . . . . . . . . . 16
⊢ (𝑄:(0...𝑀)⟶ℝ → dom 𝑄 = (0...𝑀)) |
120 | 18, 119 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom 𝑄 = (0...𝑀)) |
121 | 120 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0...𝑀) = dom 𝑄) |
122 | 81, 121 | eleqtrd 2690 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐼 + 1) ∈ dom 𝑄) |
123 | | fvelrn 6260 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑄 ∧ (𝐼 + 1) ∈ dom 𝑄) → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄) |
124 | 118, 122,
123 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄) |
125 | 124 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄) |
126 | 23 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → 𝐴 ∈
ℝ*) |
127 | 25 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → 𝐵 ∈
ℝ*) |
128 | 82 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ℝ) |
129 | 41, 53 | sseldd 3569 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ) |
130 | 4 | sseli 3564 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐼 ∈ (0...𝑀) → 𝐼 ∈ ℤ) |
131 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐼 ∈ ℤ → 𝐼 ∈
ℝ) |
132 | 77, 130, 131 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐼 ∈ ℝ) |
133 | 132 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → 𝐼 ∈ ℝ) |
134 | 133 | ltp1d 10833 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → 𝐼 < (𝐼 + 1)) |
135 | 134 | adantlr 747 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → 𝐼 < (𝐼 + 1)) |
136 | | simplr 788 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ℝ) |
137 | 129 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → (𝑆‘𝐽) ∈ ℝ) |
138 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) |
139 | 136, 137,
138 | nltled 10066 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) |
140 | 132 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → 𝐼 ∈ ℝ) |
141 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → 1 ∈ ℝ) |
142 | 140, 141 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ∈ ℝ) |
143 | | elfzoelz 12339 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℤ) |
144 | 143 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℝ) |
145 | 144 | ssriv 3572 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(0..^𝑀) ⊆
ℝ |
146 | 2, 145 | sstri 3577 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℝ |
147 | 146 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℝ) |
148 | 62 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅) |
149 | 72 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥) |
150 | 82 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑄‘(𝐼 + 1)) ∈ ℝ) |
151 | 129 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘𝐽) ∈ ℝ) |
152 | 24 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → 𝐵 ∈ ℝ) |
153 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) |
154 | 42, 107 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ) |
155 | 154 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘(𝐽 + 1)) ∈ ℝ) |
156 | | elfzoelz 12339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ) |
157 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐽 ∈ ℤ → 𝐽 ∈
ℝ) |
158 | 47, 156, 157 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝐽 ∈ ℝ) |
159 | 158 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝐽 < (𝐽 + 1)) |
160 | | isorel 6476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝐽 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝐽 < (𝐽 + 1) ↔ (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))) |
161 | 43, 49, 106, 160 | syl12anc 1316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝐽 < (𝐽 + 1) ↔ (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))) |
162 | 159, 161 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1))) |
163 | 162 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1))) |
164 | 40, 107 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ (𝐴[,]𝐵)) |
165 | | iccleub 12100 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝑆‘(𝐽 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝐽 + 1)) ≤ 𝐵) |
166 | 23, 25, 164, 165 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ≤ 𝐵) |
167 | 166 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘(𝐽 + 1)) ≤ 𝐵) |
168 | 151, 155,
152, 163, 167 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘𝐽) < 𝐵) |
169 | 150, 151,
152, 153, 168 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑄‘(𝐼 + 1)) < 𝐵) |
170 | 169 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝑄‘(𝐼 + 1)) < 𝐵) |
171 | 24 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝐵 ∈ ℝ) |
172 | 82 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝑄‘(𝐼 + 1)) ∈ ℝ) |
173 | | fourierdlem20.qm |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐵 ≤ (𝑄‘𝑀)) |
174 | 173 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝐵 ≤ (𝑄‘𝑀)) |
175 | 14 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝑀 ∈ ℤ) |
176 | 81 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (0...𝑀)) |
177 | | fzval3 12404 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑀 ∈ ℤ →
(0...𝑀) = (0..^(𝑀 + 1))) |
178 | 14, 177 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → (0...𝑀) = (0..^(𝑀 + 1))) |
179 | 178 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (0...𝑀) = (0..^(𝑀 + 1))) |
180 | 176, 179 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (0..^(𝑀 + 1))) |
181 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → ¬ (𝐼 + 1) ∈ (0..^𝑀)) |
182 | 180, 181 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → ((𝐼 + 1) ∈ (0..^(𝑀 + 1)) ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀))) |
183 | | elfzonelfzo 12436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑀 ∈ ℤ → (((𝐼 + 1) ∈ (0..^(𝑀 + 1)) ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (𝑀..^(𝑀 + 1)))) |
184 | 175, 182,
183 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (𝑀..^(𝑀 + 1))) |
185 | | fzval3 12404 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = (𝑀..^(𝑀 + 1))) |
186 | 14, 185 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → (𝑀...𝑀) = (𝑀..^(𝑀 + 1))) |
187 | 186 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → (𝑀..^(𝑀 + 1)) = (𝑀...𝑀)) |
188 | 187 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝑀..^(𝑀 + 1)) = (𝑀...𝑀)) |
189 | 184, 188 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (𝑀...𝑀)) |
190 | | elfz1eq 12223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐼 + 1) ∈ (𝑀...𝑀) → (𝐼 + 1) = 𝑀) |
191 | 189, 190 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) = 𝑀) |
192 | 191 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝑀 = (𝐼 + 1)) |
193 | 192 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝑄‘𝑀) = (𝑄‘(𝐼 + 1))) |
194 | 174, 193 | breqtrd 4609 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝐵 ≤ (𝑄‘(𝐼 + 1))) |
195 | 171, 172,
194 | lensymd 10067 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → ¬ (𝑄‘(𝐼 + 1)) < 𝐵) |
196 | 195 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → ¬ (𝑄‘(𝐼 + 1)) < 𝐵) |
197 | 170, 196 | condan 831 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ∈ (0..^𝑀)) |
198 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑘
+ |
199 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑘1 |
200 | 89, 198, 199 | nfov 6575 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑘(𝐼 + 1) |
201 | 91, 200 | nffv 6110 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑘(𝑄‘(𝐼 + 1)) |
202 | 201, 93, 94 | nfbr 4629 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑘(𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽) |
203 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = (𝐼 + 1) → (𝑄‘𝑘) = (𝑄‘(𝐼 + 1))) |
204 | 203 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = (𝐼 + 1) → ((𝑄‘𝑘) ≤ (𝑆‘𝐽) ↔ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽))) |
205 | 200, 90, 202, 204 | elrabf 3329 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ↔ ((𝐼 + 1) ∈ (0..^𝑀) ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽))) |
206 | 197, 153,
205 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}) |
207 | | suprub 10863 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℝ ∧ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥) ∧ (𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}) → (𝐼 + 1) ≤ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < )) |
208 | 147, 148,
149, 206, 207 | syl31anc 1321 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ≤ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < )) |
209 | 208, 1 | syl6breqr 4625 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ≤ 𝐼) |
210 | 142, 140,
209 | lensymd 10067 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → ¬ 𝐼 < (𝐼 + 1)) |
211 | 210 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → ¬ 𝐼 < (𝐼 + 1)) |
212 | 139, 211 | syldan 486 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → ¬ 𝐼 < (𝐼 + 1)) |
213 | 135, 212 | condan 831 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) → (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) |
214 | 82, 213 | mpdan 699 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) |
215 | 21, 129, 82, 55, 214 | lelttrd 10074 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 < (𝑄‘(𝐼 + 1))) |
216 | 215 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → 𝐴 < (𝑄‘(𝐼 + 1))) |
217 | 154 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑆‘(𝐽 + 1)) ∈ ℝ) |
218 | 24 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → 𝐵 ∈ ℝ) |
219 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) |
220 | 166 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑆‘(𝐽 + 1)) ≤ 𝐵) |
221 | 128, 217,
218, 219, 220 | ltletrd 10076 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) < 𝐵) |
222 | 126, 127,
128, 216, 221 | eliood 38567 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ (𝐴(,)𝐵)) |
223 | 125, 222 | elind 3760 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ (ran 𝑄 ∩ (𝐴(,)𝐵))) |
224 | | elun2 3743 |
. . . . . . . . . 10
⊢ ((𝑄‘(𝐼 + 1)) ∈ (ran 𝑄 ∩ (𝐴(,)𝐵)) → (𝑄‘(𝐼 + 1)) ∈ ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))) |
225 | 223, 224 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))) |
226 | 225, 22 | syl6eleqr 2699 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ 𝑇) |
227 | | foelrn 6286 |
. . . . . . . 8
⊢ ((𝑆:(0...𝑁)–onto→𝑇 ∧ (𝑄‘(𝐼 + 1)) ∈ 𝑇) → ∃𝑗 ∈ (0...𝑁)(𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) |
228 | 116, 226,
227 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → ∃𝑗 ∈ (0...𝑁)(𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) |
229 | 214 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) |
230 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) |
231 | 229, 230 | breqtrd 4609 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑆‘𝑗)) |
232 | 231 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑆‘𝑗)) |
233 | 43 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝑆 Isom < , < ((0...𝑁), 𝑇)) |
234 | 49 | anim1i 590 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) |
235 | 234 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) |
236 | | isorel 6476 |
. . . . . . . . . . . . 13
⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗))) |
237 | 233, 235,
236 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗))) |
238 | 232, 237 | mpbird 246 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝐽 < 𝑗) |
239 | 238 | adantllr 751 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝐽 < 𝑗) |
240 | | eqcom 2617 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑄‘(𝐼 + 1)) = (𝑆‘𝑗) ↔ (𝑆‘𝑗) = (𝑄‘(𝐼 + 1))) |
241 | 240 | biimpi 205 |
. . . . . . . . . . . . . . 15
⊢ ((𝑄‘(𝐼 + 1)) = (𝑆‘𝑗) → (𝑆‘𝑗) = (𝑄‘(𝐼 + 1))) |
242 | 241 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) = (𝑄‘(𝐼 + 1))) |
243 | | simpl 472 |
. . . . . . . . . . . . . 14
⊢ (((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) |
244 | 242, 243 | eqbrtrd 4605 |
. . . . . . . . . . . . 13
⊢ (((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) |
245 | 244 | adantll 746 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) |
246 | 245 | adantlr 747 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) |
247 | 43 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑆 Isom < , < ((0...𝑁), 𝑇)) |
248 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁)) |
249 | 106 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐽 + 1) ∈ (0...𝑁)) |
250 | | isorel 6476 |
. . . . . . . . . . . . 13
⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) |
251 | 247, 248,
249, 250 | syl12anc 1316 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) |
252 | 251 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) |
253 | 246, 252 | mpbird 246 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝑗 < (𝐽 + 1)) |
254 | 239, 253 | jca 553 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) |
255 | 254 | ex 449 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑄‘(𝐼 + 1)) = (𝑆‘𝑗) → (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))) |
256 | 255 | reximdva 3000 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (∃𝑗 ∈ (0...𝑁)(𝑄‘(𝐼 + 1)) = (𝑆‘𝑗) → ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))) |
257 | 228, 256 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) |
258 | | ssrexv 3630 |
. . . . . 6
⊢
((0...𝑁) ⊆
ℤ → (∃𝑗
∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) → ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))) |
259 | 113, 257,
258 | mpsyl 66 |
. . . . 5
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) |
260 | 112, 259 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) |
261 | | simplr 788 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝑗 ∈ ℤ) |
262 | 47, 156 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ ℤ) |
263 | 262 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝐽 ∈ ℤ) |
264 | | simprl 790 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝐽 < 𝑗) |
265 | | simprr 792 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝑗 < (𝐽 + 1)) |
266 | | btwnnz 11329 |
. . . . . . . 8
⊢ ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ) |
267 | 263, 264,
265, 266 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → ¬ 𝑗 ∈ ℤ) |
268 | 261, 267 | pm2.65da 598 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℤ) → ¬ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) |
269 | 268 | nrexdv 2984 |
. . . . 5
⊢ (𝜑 → ¬ ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) |
270 | 269 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → ¬ ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) |
271 | 260, 270 | condan 831 |
. . 3
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) |
272 | | ioossioo 12136 |
. . 3
⊢ ((((𝑄‘𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ*) ∧
((𝑄‘𝐼) ≤ (𝑆‘𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1)))) → ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) |
273 | 79, 83, 100, 271, 272 | syl22anc 1319 |
. 2
⊢ (𝜑 → ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) |
274 | | fveq2 6103 |
. . . . 5
⊢ (𝑖 = 𝐼 → (𝑄‘𝑖) = (𝑄‘𝐼)) |
275 | | oveq1 6556 |
. . . . . 6
⊢ (𝑖 = 𝐼 → (𝑖 + 1) = (𝐼 + 1)) |
276 | 275 | fveq2d 6107 |
. . . . 5
⊢ (𝑖 = 𝐼 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝐼 + 1))) |
277 | 274, 276 | oveq12d 6567 |
. . . 4
⊢ (𝑖 = 𝐼 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) |
278 | 277 | sseq2d 3596 |
. . 3
⊢ (𝑖 = 𝐼 → (((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))) |
279 | 278 | rspcev 3282 |
. 2
⊢ ((𝐼 ∈ (0..^𝑀) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → ∃𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
280 | 76, 273, 279 | syl2anc 691 |
1
⊢ (𝜑 → ∃𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |