Step | Hyp | Ref
| Expression |
1 | | fourierdlem52.tf |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ Fin) |
2 | | fourierdlem52.t |
. . . . . 6
⊢ (𝜑 → 𝑇 ⊆ (𝐴[,]𝐵)) |
3 | | fourierdlem52.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
4 | | fourierdlem52.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
5 | 3, 4 | iccssred 38574 |
. . . . . 6
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
6 | 2, 5 | sstrd 3578 |
. . . . 5
⊢ (𝜑 → 𝑇 ⊆ ℝ) |
7 | | fourierdlem52.s |
. . . . 5
⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇)) |
8 | | fourierdlem52.n |
. . . . 5
⊢ 𝑁 = ((#‘𝑇) − 1) |
9 | 1, 6, 7, 8 | fourierdlem36 39036 |
. . . 4
⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝑇)) |
10 | | isof1o 6473 |
. . . 4
⊢ (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto→𝑇) |
11 | | f1of 6050 |
. . . 4
⊢ (𝑆:(0...𝑁)–1-1-onto→𝑇 → 𝑆:(0...𝑁)⟶𝑇) |
12 | 9, 10, 11 | 3syl 18 |
. . 3
⊢ (𝜑 → 𝑆:(0...𝑁)⟶𝑇) |
13 | 12, 2 | fssd 5970 |
. 2
⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐴[,]𝐵)) |
14 | | f1ofo 6057 |
. . . . . 6
⊢ (𝑆:(0...𝑁)–1-1-onto→𝑇 → 𝑆:(0...𝑁)–onto→𝑇) |
15 | 9, 10, 14 | 3syl 18 |
. . . . 5
⊢ (𝜑 → 𝑆:(0...𝑁)–onto→𝑇) |
16 | | fourierdlem52.at |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑇) |
17 | | foelrn 6286 |
. . . . 5
⊢ ((𝑆:(0...𝑁)–onto→𝑇 ∧ 𝐴 ∈ 𝑇) → ∃𝑗 ∈ (0...𝑁)𝐴 = (𝑆‘𝑗)) |
18 | 15, 16, 17 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ∃𝑗 ∈ (0...𝑁)𝐴 = (𝑆‘𝑗)) |
19 | | elfzle1 12215 |
. . . . . . . . 9
⊢ (𝑗 ∈ (0...𝑁) → 0 ≤ 𝑗) |
20 | 19 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 0 ≤ 𝑗) |
21 | 9 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑆 Isom < , < ((0...𝑁), 𝑇)) |
22 | | ressxr 9962 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℝ* |
23 | 6, 22 | syl6ss 3580 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ⊆
ℝ*) |
24 | 23 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑇 ⊆
ℝ*) |
25 | | fzssz 12214 |
. . . . . . . . . . 11
⊢
(0...𝑁) ⊆
ℤ |
26 | | zssre 11261 |
. . . . . . . . . . . 12
⊢ ℤ
⊆ ℝ |
27 | 26, 22 | sstri 3577 |
. . . . . . . . . . 11
⊢ ℤ
⊆ ℝ* |
28 | 25, 27 | sstri 3577 |
. . . . . . . . . 10
⊢
(0...𝑁) ⊆
ℝ* |
29 | 24, 28 | jctil 558 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((0...𝑁) ⊆ ℝ* ∧ 𝑇 ⊆
ℝ*)) |
30 | | hashcl 13009 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇 ∈ Fin →
(#‘𝑇) ∈
ℕ0) |
31 | 1, 30 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (#‘𝑇) ∈
ℕ0) |
32 | | ne0i 3880 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ 𝑇 → 𝑇 ≠ ∅) |
33 | 16, 32 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑇 ≠ ∅) |
34 | | hashge1 13039 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑇 ∈ Fin ∧ 𝑇 ≠ ∅) → 1 ≤
(#‘𝑇)) |
35 | 1, 33, 34 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ≤ (#‘𝑇)) |
36 | | elnnnn0c 11215 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑇) ∈
ℕ ↔ ((#‘𝑇)
∈ ℕ0 ∧ 1 ≤ (#‘𝑇))) |
37 | 31, 35, 36 | sylanbrc 695 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (#‘𝑇) ∈ ℕ) |
38 | | nnm1nn0 11211 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑇) ∈
ℕ → ((#‘𝑇)
− 1) ∈ ℕ0) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((#‘𝑇) − 1) ∈
ℕ0) |
40 | 8, 39 | syl5eqel 2692 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
41 | | nn0uz 11598 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
42 | 40, 41 | syl6eleq 2698 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
43 | | eluzfz1 12219 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑁)) |
44 | 42, 43 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈ (0...𝑁)) |
45 | 44 | anim1i 590 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (0 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) |
46 | | leisorel 13101 |
. . . . . . . . 9
⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ ((0...𝑁) ⊆ ℝ* ∧ 𝑇 ⊆ ℝ*)
∧ (0 ∈ (0...𝑁)
∧ 𝑗 ∈ (0...𝑁))) → (0 ≤ 𝑗 ↔ (𝑆‘0) ≤ (𝑆‘𝑗))) |
47 | 21, 29, 45, 46 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (0 ≤ 𝑗 ↔ (𝑆‘0) ≤ (𝑆‘𝑗))) |
48 | 20, 47 | mpbid 221 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑆‘0) ≤ (𝑆‘𝑗)) |
49 | 48 | 3adant3 1074 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐴 = (𝑆‘𝑗)) → (𝑆‘0) ≤ (𝑆‘𝑗)) |
50 | | eqcom 2617 |
. . . . . . . 8
⊢ (𝐴 = (𝑆‘𝑗) ↔ (𝑆‘𝑗) = 𝐴) |
51 | 50 | biimpi 205 |
. . . . . . 7
⊢ (𝐴 = (𝑆‘𝑗) → (𝑆‘𝑗) = 𝐴) |
52 | 51 | 3ad2ant3 1077 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐴 = (𝑆‘𝑗)) → (𝑆‘𝑗) = 𝐴) |
53 | 49, 52 | breqtrd 4609 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐴 = (𝑆‘𝑗)) → (𝑆‘0) ≤ 𝐴) |
54 | 53 | rexlimdv3a 3015 |
. . . 4
⊢ (𝜑 → (∃𝑗 ∈ (0...𝑁)𝐴 = (𝑆‘𝑗) → (𝑆‘0) ≤ 𝐴)) |
55 | 18, 54 | mpd 15 |
. . 3
⊢ (𝜑 → (𝑆‘0) ≤ 𝐴) |
56 | 3 | rexrd 9968 |
. . . 4
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
57 | 4 | rexrd 9968 |
. . . 4
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
58 | 13, 44 | ffvelrnd 6268 |
. . . 4
⊢ (𝜑 → (𝑆‘0) ∈ (𝐴[,]𝐵)) |
59 | | iccgelb 12101 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝑆‘0) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑆‘0)) |
60 | 56, 57, 58, 59 | syl3anc 1318 |
. . 3
⊢ (𝜑 → 𝐴 ≤ (𝑆‘0)) |
61 | 5, 58 | sseldd 3569 |
. . . 4
⊢ (𝜑 → (𝑆‘0) ∈ ℝ) |
62 | 61, 3 | letri3d 10058 |
. . 3
⊢ (𝜑 → ((𝑆‘0) = 𝐴 ↔ ((𝑆‘0) ≤ 𝐴 ∧ 𝐴 ≤ (𝑆‘0)))) |
63 | 55, 60, 62 | mpbir2and 959 |
. 2
⊢ (𝜑 → (𝑆‘0) = 𝐴) |
64 | | eluzfz2 12220 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘0) → 𝑁 ∈ (0...𝑁)) |
65 | 42, 64 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ (0...𝑁)) |
66 | 13, 65 | ffvelrnd 6268 |
. . . 4
⊢ (𝜑 → (𝑆‘𝑁) ∈ (𝐴[,]𝐵)) |
67 | | iccleub 12100 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝑆‘𝑁) ∈ (𝐴[,]𝐵)) → (𝑆‘𝑁) ≤ 𝐵) |
68 | 56, 57, 66, 67 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (𝑆‘𝑁) ≤ 𝐵) |
69 | | fourierdlem52.bt |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑇) |
70 | | foelrn 6286 |
. . . . 5
⊢ ((𝑆:(0...𝑁)–onto→𝑇 ∧ 𝐵 ∈ 𝑇) → ∃𝑗 ∈ (0...𝑁)𝐵 = (𝑆‘𝑗)) |
71 | 15, 69, 70 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ∃𝑗 ∈ (0...𝑁)𝐵 = (𝑆‘𝑗)) |
72 | | simp3 1056 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐵 = (𝑆‘𝑗)) → 𝐵 = (𝑆‘𝑗)) |
73 | | elfzle2 12216 |
. . . . . . . 8
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ≤ 𝑁) |
74 | 73 | 3ad2ant2 1076 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐵 = (𝑆‘𝑗)) → 𝑗 ≤ 𝑁) |
75 | 9 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐵 = (𝑆‘𝑗)) → 𝑆 Isom < , < ((0...𝑁), 𝑇)) |
76 | 29 | 3adant3 1074 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐵 = (𝑆‘𝑗)) → ((0...𝑁) ⊆ ℝ* ∧ 𝑇 ⊆
ℝ*)) |
77 | | simp2 1055 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐵 = (𝑆‘𝑗)) → 𝑗 ∈ (0...𝑁)) |
78 | 65 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐵 = (𝑆‘𝑗)) → 𝑁 ∈ (0...𝑁)) |
79 | | leisorel 13101 |
. . . . . . . 8
⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ ((0...𝑁) ⊆ ℝ* ∧ 𝑇 ⊆ ℝ*)
∧ (𝑗 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...𝑁))) → (𝑗 ≤ 𝑁 ↔ (𝑆‘𝑗) ≤ (𝑆‘𝑁))) |
80 | 75, 76, 77, 78, 79 | syl112anc 1322 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐵 = (𝑆‘𝑗)) → (𝑗 ≤ 𝑁 ↔ (𝑆‘𝑗) ≤ (𝑆‘𝑁))) |
81 | 74, 80 | mpbid 221 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐵 = (𝑆‘𝑗)) → (𝑆‘𝑗) ≤ (𝑆‘𝑁)) |
82 | 72, 81 | eqbrtrd 4605 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐵 = (𝑆‘𝑗)) → 𝐵 ≤ (𝑆‘𝑁)) |
83 | 82 | rexlimdv3a 3015 |
. . . 4
⊢ (𝜑 → (∃𝑗 ∈ (0...𝑁)𝐵 = (𝑆‘𝑗) → 𝐵 ≤ (𝑆‘𝑁))) |
84 | 71, 83 | mpd 15 |
. . 3
⊢ (𝜑 → 𝐵 ≤ (𝑆‘𝑁)) |
85 | 5, 66 | sseldd 3569 |
. . . 4
⊢ (𝜑 → (𝑆‘𝑁) ∈ ℝ) |
86 | 85, 4 | letri3d 10058 |
. . 3
⊢ (𝜑 → ((𝑆‘𝑁) = 𝐵 ↔ ((𝑆‘𝑁) ≤ 𝐵 ∧ 𝐵 ≤ (𝑆‘𝑁)))) |
87 | 68, 84, 86 | mpbir2and 959 |
. 2
⊢ (𝜑 → (𝑆‘𝑁) = 𝐵) |
88 | 13, 63, 87 | jca31 555 |
1
⊢ (𝜑 → ((𝑆:(0...𝑁)⟶(𝐴[,]𝐵) ∧ (𝑆‘0) = 𝐴) ∧ (𝑆‘𝑁) = 𝐵)) |