| 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 13474 |
. . . . . 6
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
| 6 | 2, 5 | sstrd 3994 |
. . . . 5
⊢ (𝜑 → 𝑇 ⊆ ℝ) |
| 7 | | fourierdlem52.s |
. . . . 5
⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇)) |
| 8 | | fourierdlem52.n |
. . . . 5
⊢ 𝑁 = ((♯‘𝑇) − 1) |
| 9 | 1, 6, 7, 8 | fourierdlem36 46158 |
. . . 4
⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝑇)) |
| 10 | | isof1o 7343 |
. . . 4
⊢ (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto→𝑇) |
| 11 | | f1of 6848 |
. . . 4
⊢ (𝑆:(0...𝑁)–1-1-onto→𝑇 → 𝑆:(0...𝑁)⟶𝑇) |
| 12 | 9, 10, 11 | 3syl 18 |
. . 3
⊢ (𝜑 → 𝑆:(0...𝑁)⟶𝑇) |
| 13 | 12, 2 | fssd 6753 |
. 2
⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐴[,]𝐵)) |
| 14 | | f1ofo 6855 |
. . . . . 6
⊢ (𝑆:(0...𝑁)–1-1-onto→𝑇 → 𝑆:(0...𝑁)–onto→𝑇) |
| 15 | 9, 10, 14 | 3syl 18 |
. . . . 5
⊢ (𝜑 → 𝑆:(0...𝑁)–onto→𝑇) |
| 16 | | fourierdlem52.at |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑇) |
| 17 | | foelrn 7127 |
. . . . 5
⊢ ((𝑆:(0...𝑁)–onto→𝑇 ∧ 𝐴 ∈ 𝑇) → ∃𝑗 ∈ (0...𝑁)𝐴 = (𝑆‘𝑗)) |
| 18 | 15, 16, 17 | syl2anc 584 |
. . . 4
⊢ (𝜑 → ∃𝑗 ∈ (0...𝑁)𝐴 = (𝑆‘𝑗)) |
| 19 | | elfzle1 13567 |
. . . . . . . . 9
⊢ (𝑗 ∈ (0...𝑁) → 0 ≤ 𝑗) |
| 20 | 19 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 0 ≤ 𝑗) |
| 21 | 9 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑆 Isom < , < ((0...𝑁), 𝑇)) |
| 22 | | ressxr 11305 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℝ* |
| 23 | 6, 22 | sstrdi 3996 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ⊆
ℝ*) |
| 24 | 23 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑇 ⊆
ℝ*) |
| 25 | | fzssz 13566 |
. . . . . . . . . . 11
⊢
(0...𝑁) ⊆
ℤ |
| 26 | | zssre 12620 |
. . . . . . . . . . . 12
⊢ ℤ
⊆ ℝ |
| 27 | 26, 22 | sstri 3993 |
. . . . . . . . . . 11
⊢ ℤ
⊆ ℝ* |
| 28 | 25, 27 | sstri 3993 |
. . . . . . . . . 10
⊢
(0...𝑁) ⊆
ℝ* |
| 29 | 24, 28 | jctil 519 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((0...𝑁) ⊆ ℝ* ∧ 𝑇 ⊆
ℝ*)) |
| 30 | | hashcl 14395 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇 ∈ Fin →
(♯‘𝑇) ∈
ℕ0) |
| 31 | 1, 30 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘𝑇) ∈
ℕ0) |
| 32 | 16 | ne0d 4342 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑇 ≠ ∅) |
| 33 | | hashge1 14428 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑇 ∈ Fin ∧ 𝑇 ≠ ∅) → 1 ≤
(♯‘𝑇)) |
| 34 | 1, 32, 33 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ≤
(♯‘𝑇)) |
| 35 | | elnnnn0c 12571 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑇)
∈ ℕ ↔ ((♯‘𝑇) ∈ ℕ0 ∧ 1 ≤
(♯‘𝑇))) |
| 36 | 31, 34, 35 | sylanbrc 583 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (♯‘𝑇) ∈
ℕ) |
| 37 | | nnm1nn0 12567 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑇)
∈ ℕ → ((♯‘𝑇) − 1) ∈
ℕ0) |
| 38 | 36, 37 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((♯‘𝑇) − 1) ∈
ℕ0) |
| 39 | 8, 38 | eqeltrid 2845 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 40 | | nn0uz 12920 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
| 41 | 39, 40 | eleqtrdi 2851 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
| 42 | | eluzfz1 13571 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑁)) |
| 43 | 41, 42 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈ (0...𝑁)) |
| 44 | 43 | anim1i 615 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (0 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) |
| 45 | | leisorel 14499 |
. . . . . . . . 9
⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ ((0...𝑁) ⊆ ℝ* ∧ 𝑇 ⊆ ℝ*)
∧ (0 ∈ (0...𝑁)
∧ 𝑗 ∈ (0...𝑁))) → (0 ≤ 𝑗 ↔ (𝑆‘0) ≤ (𝑆‘𝑗))) |
| 46 | 21, 29, 44, 45 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (0 ≤ 𝑗 ↔ (𝑆‘0) ≤ (𝑆‘𝑗))) |
| 47 | 20, 46 | mpbid 232 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑆‘0) ≤ (𝑆‘𝑗)) |
| 48 | 47 | 3adant3 1133 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐴 = (𝑆‘𝑗)) → (𝑆‘0) ≤ (𝑆‘𝑗)) |
| 49 | | eqcom 2744 |
. . . . . . . 8
⊢ (𝐴 = (𝑆‘𝑗) ↔ (𝑆‘𝑗) = 𝐴) |
| 50 | 49 | biimpi 216 |
. . . . . . 7
⊢ (𝐴 = (𝑆‘𝑗) → (𝑆‘𝑗) = 𝐴) |
| 51 | 50 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐴 = (𝑆‘𝑗)) → (𝑆‘𝑗) = 𝐴) |
| 52 | 48, 51 | breqtrd 5169 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐴 = (𝑆‘𝑗)) → (𝑆‘0) ≤ 𝐴) |
| 53 | 52 | rexlimdv3a 3159 |
. . . 4
⊢ (𝜑 → (∃𝑗 ∈ (0...𝑁)𝐴 = (𝑆‘𝑗) → (𝑆‘0) ≤ 𝐴)) |
| 54 | 18, 53 | mpd 15 |
. . 3
⊢ (𝜑 → (𝑆‘0) ≤ 𝐴) |
| 55 | 3 | rexrd 11311 |
. . . 4
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
| 56 | 4 | rexrd 11311 |
. . . 4
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
| 57 | 13, 43 | ffvelcdmd 7105 |
. . . 4
⊢ (𝜑 → (𝑆‘0) ∈ (𝐴[,]𝐵)) |
| 58 | | iccgelb 13443 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝑆‘0) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑆‘0)) |
| 59 | 55, 56, 57, 58 | syl3anc 1373 |
. . 3
⊢ (𝜑 → 𝐴 ≤ (𝑆‘0)) |
| 60 | 5, 57 | sseldd 3984 |
. . . 4
⊢ (𝜑 → (𝑆‘0) ∈ ℝ) |
| 61 | 60, 3 | letri3d 11403 |
. . 3
⊢ (𝜑 → ((𝑆‘0) = 𝐴 ↔ ((𝑆‘0) ≤ 𝐴 ∧ 𝐴 ≤ (𝑆‘0)))) |
| 62 | 54, 59, 61 | mpbir2and 713 |
. 2
⊢ (𝜑 → (𝑆‘0) = 𝐴) |
| 63 | | eluzfz2 13572 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘0) → 𝑁 ∈ (0...𝑁)) |
| 64 | 41, 63 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ (0...𝑁)) |
| 65 | 13, 64 | ffvelcdmd 7105 |
. . . 4
⊢ (𝜑 → (𝑆‘𝑁) ∈ (𝐴[,]𝐵)) |
| 66 | | iccleub 13442 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝑆‘𝑁) ∈ (𝐴[,]𝐵)) → (𝑆‘𝑁) ≤ 𝐵) |
| 67 | 55, 56, 65, 66 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (𝑆‘𝑁) ≤ 𝐵) |
| 68 | | fourierdlem52.bt |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑇) |
| 69 | | foelrn 7127 |
. . . . 5
⊢ ((𝑆:(0...𝑁)–onto→𝑇 ∧ 𝐵 ∈ 𝑇) → ∃𝑗 ∈ (0...𝑁)𝐵 = (𝑆‘𝑗)) |
| 70 | 15, 68, 69 | syl2anc 584 |
. . . 4
⊢ (𝜑 → ∃𝑗 ∈ (0...𝑁)𝐵 = (𝑆‘𝑗)) |
| 71 | | simp3 1139 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐵 = (𝑆‘𝑗)) → 𝐵 = (𝑆‘𝑗)) |
| 72 | | elfzle2 13568 |
. . . . . . . 8
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ≤ 𝑁) |
| 73 | 72 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐵 = (𝑆‘𝑗)) → 𝑗 ≤ 𝑁) |
| 74 | 9 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐵 = (𝑆‘𝑗)) → 𝑆 Isom < , < ((0...𝑁), 𝑇)) |
| 75 | 29 | 3adant3 1133 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐵 = (𝑆‘𝑗)) → ((0...𝑁) ⊆ ℝ* ∧ 𝑇 ⊆
ℝ*)) |
| 76 | | simp2 1138 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐵 = (𝑆‘𝑗)) → 𝑗 ∈ (0...𝑁)) |
| 77 | 64 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐵 = (𝑆‘𝑗)) → 𝑁 ∈ (0...𝑁)) |
| 78 | | leisorel 14499 |
. . . . . . . 8
⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ ((0...𝑁) ⊆ ℝ* ∧ 𝑇 ⊆ ℝ*)
∧ (𝑗 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...𝑁))) → (𝑗 ≤ 𝑁 ↔ (𝑆‘𝑗) ≤ (𝑆‘𝑁))) |
| 79 | 74, 75, 76, 77, 78 | syl112anc 1376 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐵 = (𝑆‘𝑗)) → (𝑗 ≤ 𝑁 ↔ (𝑆‘𝑗) ≤ (𝑆‘𝑁))) |
| 80 | 73, 79 | mpbid 232 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐵 = (𝑆‘𝑗)) → (𝑆‘𝑗) ≤ (𝑆‘𝑁)) |
| 81 | 71, 80 | eqbrtrd 5165 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝐵 = (𝑆‘𝑗)) → 𝐵 ≤ (𝑆‘𝑁)) |
| 82 | 81 | rexlimdv3a 3159 |
. . . 4
⊢ (𝜑 → (∃𝑗 ∈ (0...𝑁)𝐵 = (𝑆‘𝑗) → 𝐵 ≤ (𝑆‘𝑁))) |
| 83 | 70, 82 | mpd 15 |
. . 3
⊢ (𝜑 → 𝐵 ≤ (𝑆‘𝑁)) |
| 84 | 5, 65 | sseldd 3984 |
. . . 4
⊢ (𝜑 → (𝑆‘𝑁) ∈ ℝ) |
| 85 | 84, 4 | letri3d 11403 |
. . 3
⊢ (𝜑 → ((𝑆‘𝑁) = 𝐵 ↔ ((𝑆‘𝑁) ≤ 𝐵 ∧ 𝐵 ≤ (𝑆‘𝑁)))) |
| 86 | 67, 83, 85 | mpbir2and 713 |
. 2
⊢ (𝜑 → (𝑆‘𝑁) = 𝐵) |
| 87 | 13, 62, 86 | jca31 514 |
1
⊢ (𝜑 → ((𝑆:(0...𝑁)⟶(𝐴[,]𝐵) ∧ (𝑆‘0) = 𝐴) ∧ (𝑆‘𝑁) = 𝐵)) |