| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fourierdlem54.n | . . 3
⊢ 𝑁 = ((♯‘𝐻) − 1) | 
| 2 |  | 2z 12649 | . . . . . 6
⊢ 2 ∈
ℤ | 
| 3 | 2 | a1i 11 | . . . . 5
⊢ (𝜑 → 2 ∈
ℤ) | 
| 4 |  | fourierdlem54.c | . . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 5 |  | prid1g 4760 | . . . . . . . . . 10
⊢ (𝐶 ∈ ℝ → 𝐶 ∈ {𝐶, 𝐷}) | 
| 6 |  | elun1 4182 | . . . . . . . . . 10
⊢ (𝐶 ∈ {𝐶, 𝐷} → 𝐶 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})) | 
| 7 | 4, 5, 6 | 3syl 18 | . . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})) | 
| 8 |  | fourierdlem54.h | . . . . . . . . 9
⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) | 
| 9 | 7, 8 | eleqtrrdi 2852 | . . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ 𝐻) | 
| 10 | 9 | ne0d 4342 | . . . . . . 7
⊢ (𝜑 → 𝐻 ≠ ∅) | 
| 11 |  | prfi 9363 | . . . . . . . . . 10
⊢ {𝐶, 𝐷} ∈ Fin | 
| 12 |  | fourierdlem54.p | . . . . . . . . . . . . 13
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) | 
| 13 |  | fourierdlem54.m | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 14 |  | fourierdlem54.q | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) | 
| 15 | 12, 13, 14 | fourierdlem11 46133 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵)) | 
| 16 | 15 | simp1d 1143 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 17 | 15 | simp2d 1144 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 18 | 15 | simp3d 1145 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 < 𝐵) | 
| 19 |  | fourierdlem54.t | . . . . . . . . . . 11
⊢ 𝑇 = (𝐵 − 𝐴) | 
| 20 | 12, 13, 14 | fourierdlem15 46137 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵)) | 
| 21 |  | frn 6743 | . . . . . . . . . . . 12
⊢ (𝑄:(0...𝑀)⟶(𝐴[,]𝐵) → ran 𝑄 ⊆ (𝐴[,]𝐵)) | 
| 22 | 20, 21 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → ran 𝑄 ⊆ (𝐴[,]𝐵)) | 
| 23 | 12 | fourierdlem2 46124 | . . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) | 
| 24 | 13, 23 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) | 
| 25 | 14, 24 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) | 
| 26 | 25 | simpld 494 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑄 ∈ (ℝ ↑m
(0...𝑀))) | 
| 27 |  | elmapi 8889 | . . . . . . . . . . . . . 14
⊢ (𝑄 ∈ (ℝ
↑m (0...𝑀))
→ 𝑄:(0...𝑀)⟶ℝ) | 
| 28 |  | ffn 6736 | . . . . . . . . . . . . . 14
⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀)) | 
| 29 | 26, 27, 28 | 3syl 18 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 Fn (0...𝑀)) | 
| 30 |  | fzfid 14014 | . . . . . . . . . . . . 13
⊢ (𝜑 → (0...𝑀) ∈ Fin) | 
| 31 |  | fnfi 9218 | . . . . . . . . . . . . 13
⊢ ((𝑄 Fn (0...𝑀) ∧ (0...𝑀) ∈ Fin) → 𝑄 ∈ Fin) | 
| 32 | 29, 30, 31 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∈ Fin) | 
| 33 |  | rnfi 9380 | . . . . . . . . . . . 12
⊢ (𝑄 ∈ Fin → ran 𝑄 ∈ Fin) | 
| 34 | 32, 33 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → ran 𝑄 ∈ Fin) | 
| 35 | 25 | simprd 495 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) | 
| 36 | 35 | simpld 494 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵)) | 
| 37 | 36 | simpld 494 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑄‘0) = 𝐴) | 
| 38 | 13 | nnnn0d 12587 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈
ℕ0) | 
| 39 |  | nn0uz 12920 | . . . . . . . . . . . . . . 15
⊢
ℕ0 = (ℤ≥‘0) | 
| 40 | 38, 39 | eleqtrdi 2851 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) | 
| 41 |  | eluzfz1 13571 | . . . . . . . . . . . . . 14
⊢ (𝑀 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑀)) | 
| 42 | 40, 41 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈ (0...𝑀)) | 
| 43 |  | fnfvelrn 7100 | . . . . . . . . . . . . 13
⊢ ((𝑄 Fn (0...𝑀) ∧ 0 ∈ (0...𝑀)) → (𝑄‘0) ∈ ran 𝑄) | 
| 44 | 29, 42, 43 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑄‘0) ∈ ran 𝑄) | 
| 45 | 37, 44 | eqeltrrd 2842 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ran 𝑄) | 
| 46 | 36 | simprd 495 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑄‘𝑀) = 𝐵) | 
| 47 |  | eluzfz2 13572 | . . . . . . . . . . . . . 14
⊢ (𝑀 ∈
(ℤ≥‘0) → 𝑀 ∈ (0...𝑀)) | 
| 48 | 40, 47 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ (0...𝑀)) | 
| 49 |  | fnfvelrn 7100 | . . . . . . . . . . . . 13
⊢ ((𝑄 Fn (0...𝑀) ∧ 𝑀 ∈ (0...𝑀)) → (𝑄‘𝑀) ∈ ran 𝑄) | 
| 50 | 29, 48, 49 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑄‘𝑀) ∈ ran 𝑄) | 
| 51 | 46, 50 | eqeltrrd 2842 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ran 𝑄) | 
| 52 |  | eqid 2737 | . . . . . . . . . . 11
⊢ (abs
∘ − ) = (abs ∘ − ) | 
| 53 |  | eqid 2737 | . . . . . . . . . . 11
⊢ ((ran
𝑄 × ran 𝑄) ∖ I ) = ((ran 𝑄 × ran 𝑄) ∖ I ) | 
| 54 |  | eqid 2737 | . . . . . . . . . . 11
⊢ ran ((abs
∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I )) = ran ((abs ∘ − )
↾ ((ran 𝑄 × ran
𝑄) ∖ I
)) | 
| 55 |  | eqid 2737 | . . . . . . . . . . 11
⊢ inf(ran
((abs ∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I )), ℝ, < ) = inf(ran
((abs ∘ − ) ↾ ((ran 𝑄 × ran 𝑄) ∖ I )), ℝ, <
) | 
| 56 |  | fourierdlem54.d | . . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ ℝ) | 
| 57 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) | 
| 58 |  | eqid 2737 | . . . . . . . . . . 11
⊢
((topGen‘ran (,)) ↾t (𝐶[,]𝐷)) = ((topGen‘ran (,))
↾t (𝐶[,]𝐷)) | 
| 59 |  | oveq1 7438 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → (𝑥 + (𝑘 · 𝑇)) = (𝑤 + (𝑘 · 𝑇))) | 
| 60 | 59 | eleq1d 2826 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → ((𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄)) | 
| 61 | 60 | rexbidv 3179 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄)) | 
| 62 | 61 | cbvrabv 3447 | . . . . . . . . . . 11
⊢ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑤 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄} | 
| 63 |  | oveq1 7438 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑗 → (𝑖 · 𝑇) = (𝑗 · 𝑇)) | 
| 64 | 63 | oveq2d 7447 | . . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑗 → (𝑦 + (𝑖 · 𝑇)) = (𝑦 + (𝑗 · 𝑇))) | 
| 65 | 64 | eleq1d 2826 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑗 → ((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄)) | 
| 66 | 65 | anbi1d 631 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝑗 → (((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄) ↔ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄))) | 
| 67 |  | oveq1 7438 | . . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝑘 → (𝑙 · 𝑇) = (𝑘 · 𝑇)) | 
| 68 | 67 | oveq2d 7447 | . . . . . . . . . . . . . . 15
⊢ (𝑙 = 𝑘 → (𝑧 + (𝑙 · 𝑇)) = (𝑧 + (𝑘 · 𝑇))) | 
| 69 | 68 | eleq1d 2826 | . . . . . . . . . . . . . 14
⊢ (𝑙 = 𝑘 → ((𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄)) | 
| 70 | 69 | anbi2d 630 | . . . . . . . . . . . . 13
⊢ (𝑙 = 𝑘 → (((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄) ↔ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄))) | 
| 71 | 66, 70 | cbvrex2vw 3242 | . . . . . . . . . . . 12
⊢
(∃𝑖 ∈
ℤ ∃𝑙 ∈
ℤ ((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄) ↔ ∃𝑗 ∈ ℤ ∃𝑘 ∈ ℤ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄)) | 
| 72 | 71 | anbi2i 623 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 < 𝑧)) ∧ ∃𝑖 ∈ ℤ ∃𝑙 ∈ ℤ ((𝑦 + (𝑖 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄)) ↔ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 < 𝑧)) ∧ ∃𝑗 ∈ ℤ ∃𝑘 ∈ ℤ ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ∧ (𝑧 + (𝑘 · 𝑇)) ∈ ran 𝑄))) | 
| 73 | 16, 17, 18, 19, 22, 34, 45, 51, 52, 53, 54, 55, 4, 56, 57, 58, 62, 72 | fourierdlem42 46164 | . . . . . . . . . 10
⊢ (𝜑 → {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ∈ Fin) | 
| 74 |  | unfi 9211 | . . . . . . . . . 10
⊢ (({𝐶, 𝐷} ∈ Fin ∧ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ∈ Fin) → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ∈ Fin) | 
| 75 | 11, 73, 74 | sylancr 587 | . . . . . . . . 9
⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ∈ Fin) | 
| 76 | 8, 75 | eqeltrid 2845 | . . . . . . . 8
⊢ (𝜑 → 𝐻 ∈ Fin) | 
| 77 |  | hashnncl 14405 | . . . . . . . 8
⊢ (𝐻 ∈ Fin →
((♯‘𝐻) ∈
ℕ ↔ 𝐻 ≠
∅)) | 
| 78 | 76, 77 | syl 17 | . . . . . . 7
⊢ (𝜑 → ((♯‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅)) | 
| 79 | 10, 78 | mpbird 257 | . . . . . 6
⊢ (𝜑 → (♯‘𝐻) ∈
ℕ) | 
| 80 | 79 | nnzd 12640 | . . . . 5
⊢ (𝜑 → (♯‘𝐻) ∈
ℤ) | 
| 81 |  | fourierdlem54.cd | . . . . . . . . 9
⊢ (𝜑 → 𝐶 < 𝐷) | 
| 82 | 4, 81 | ltned 11397 | . . . . . . . 8
⊢ (𝜑 → 𝐶 ≠ 𝐷) | 
| 83 |  | hashprg 14434 | . . . . . . . . 9
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝐶 ≠ 𝐷 ↔ (♯‘{𝐶, 𝐷}) = 2)) | 
| 84 | 4, 56, 83 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝐶 ≠ 𝐷 ↔ (♯‘{𝐶, 𝐷}) = 2)) | 
| 85 | 82, 84 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → (♯‘{𝐶, 𝐷}) = 2) | 
| 86 | 85 | eqcomd 2743 | . . . . . 6
⊢ (𝜑 → 2 = (♯‘{𝐶, 𝐷})) | 
| 87 |  | ssun1 4178 | . . . . . . . . 9
⊢ {𝐶, 𝐷} ⊆ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) | 
| 88 | 87 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → {𝐶, 𝐷} ⊆ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})) | 
| 89 | 88, 8 | sseqtrrdi 4025 | . . . . . . 7
⊢ (𝜑 → {𝐶, 𝐷} ⊆ 𝐻) | 
| 90 |  | hashssle 45310 | . . . . . . 7
⊢ ((𝐻 ∈ Fin ∧ {𝐶, 𝐷} ⊆ 𝐻) → (♯‘{𝐶, 𝐷}) ≤ (♯‘𝐻)) | 
| 91 | 76, 89, 90 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (♯‘{𝐶, 𝐷}) ≤ (♯‘𝐻)) | 
| 92 | 86, 91 | eqbrtrd 5165 | . . . . 5
⊢ (𝜑 → 2 ≤
(♯‘𝐻)) | 
| 93 |  | eluz2 12884 | . . . . 5
⊢
((♯‘𝐻)
∈ (ℤ≥‘2) ↔ (2 ∈ ℤ ∧
(♯‘𝐻) ∈
ℤ ∧ 2 ≤ (♯‘𝐻))) | 
| 94 | 3, 80, 92, 93 | syl3anbrc 1344 | . . . 4
⊢ (𝜑 → (♯‘𝐻) ∈
(ℤ≥‘2)) | 
| 95 |  | uz2m1nn 12965 | . . . 4
⊢
((♯‘𝐻)
∈ (ℤ≥‘2) → ((♯‘𝐻) − 1) ∈
ℕ) | 
| 96 | 94, 95 | syl 17 | . . 3
⊢ (𝜑 → ((♯‘𝐻) − 1) ∈
ℕ) | 
| 97 | 1, 96 | eqeltrid 2845 | . 2
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 98 |  | prssg 4819 | . . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ↔ {𝐶, 𝐷} ⊆ ℝ)) | 
| 99 | 4, 56, 98 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ↔ {𝐶, 𝐷} ⊆ ℝ)) | 
| 100 | 4, 56, 99 | mpbi2and 712 | . . . . . . . . . . 11
⊢ (𝜑 → {𝐶, 𝐷} ⊆ ℝ) | 
| 101 |  | ssrab2 4080 | . . . . . . . . . . . 12
⊢ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷) | 
| 102 | 4, 56 | iccssred 13474 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐶[,]𝐷) ⊆ ℝ) | 
| 103 | 101, 102 | sstrid 3995 | . . . . . . . . . . 11
⊢ (𝜑 → {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ ℝ) | 
| 104 | 100, 103 | unssd 4192 | . . . . . . . . . 10
⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ ℝ) | 
| 105 | 8, 104 | eqsstrid 4022 | . . . . . . . . 9
⊢ (𝜑 → 𝐻 ⊆ ℝ) | 
| 106 |  | fourierdlem54.s | . . . . . . . . 9
⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) | 
| 107 | 76, 105, 106, 1 | fourierdlem36 46158 | . . . . . . . 8
⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝐻)) | 
| 108 |  | df-isom 6570 | . . . . . . . 8
⊢ (𝑆 Isom < , < ((0...𝑁), 𝐻) ↔ (𝑆:(0...𝑁)–1-1-onto→𝐻 ∧ ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)))) | 
| 109 | 107, 108 | sylib 218 | . . . . . . 7
⊢ (𝜑 → (𝑆:(0...𝑁)–1-1-onto→𝐻 ∧ ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)))) | 
| 110 | 109 | simpld 494 | . . . . . 6
⊢ (𝜑 → 𝑆:(0...𝑁)–1-1-onto→𝐻) | 
| 111 |  | f1of 6848 | . . . . . 6
⊢ (𝑆:(0...𝑁)–1-1-onto→𝐻 → 𝑆:(0...𝑁)⟶𝐻) | 
| 112 | 110, 111 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑆:(0...𝑁)⟶𝐻) | 
| 113 | 112, 105 | fssd 6753 | . . . 4
⊢ (𝜑 → 𝑆:(0...𝑁)⟶ℝ) | 
| 114 |  | reex 11246 | . . . . 5
⊢ ℝ
∈ V | 
| 115 |  | ovex 7464 | . . . . . 6
⊢
(0...𝑁) ∈
V | 
| 116 | 115 | a1i 11 | . . . . 5
⊢ (𝜑 → (0...𝑁) ∈ V) | 
| 117 |  | elmapg 8879 | . . . . 5
⊢ ((ℝ
∈ V ∧ (0...𝑁)
∈ V) → (𝑆 ∈
(ℝ ↑m (0...𝑁)) ↔ 𝑆:(0...𝑁)⟶ℝ)) | 
| 118 | 114, 116,
117 | sylancr 587 | . . . 4
⊢ (𝜑 → (𝑆 ∈ (ℝ ↑m
(0...𝑁)) ↔ 𝑆:(0...𝑁)⟶ℝ)) | 
| 119 | 113, 118 | mpbird 257 | . . 3
⊢ (𝜑 → 𝑆 ∈ (ℝ ↑m
(0...𝑁))) | 
| 120 |  | df-f1o 6568 | . . . . . . . . . . 11
⊢ (𝑆:(0...𝑁)–1-1-onto→𝐻 ↔ (𝑆:(0...𝑁)–1-1→𝐻 ∧ 𝑆:(0...𝑁)–onto→𝐻)) | 
| 121 | 110, 120 | sylib 218 | . . . . . . . . . 10
⊢ (𝜑 → (𝑆:(0...𝑁)–1-1→𝐻 ∧ 𝑆:(0...𝑁)–onto→𝐻)) | 
| 122 | 121 | simprd 495 | . . . . . . . . 9
⊢ (𝜑 → 𝑆:(0...𝑁)–onto→𝐻) | 
| 123 |  | dffo3 7122 | . . . . . . . . 9
⊢ (𝑆:(0...𝑁)–onto→𝐻 ↔ (𝑆:(0...𝑁)⟶𝐻 ∧ ∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦))) | 
| 124 | 122, 123 | sylib 218 | . . . . . . . 8
⊢ (𝜑 → (𝑆:(0...𝑁)⟶𝐻 ∧ ∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦))) | 
| 125 | 124 | simprd 495 | . . . . . . 7
⊢ (𝜑 → ∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦)) | 
| 126 |  | eqeq1 2741 | . . . . . . . . . 10
⊢ (ℎ = 𝐶 → (ℎ = (𝑆‘𝑦) ↔ 𝐶 = (𝑆‘𝑦))) | 
| 127 |  | eqcom 2744 | . . . . . . . . . 10
⊢ (𝐶 = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐶) | 
| 128 | 126, 127 | bitrdi 287 | . . . . . . . . 9
⊢ (ℎ = 𝐶 → (ℎ = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐶)) | 
| 129 | 128 | rexbidv 3179 | . . . . . . . 8
⊢ (ℎ = 𝐶 → (∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) ↔ ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶)) | 
| 130 | 129 | rspcv 3618 | . . . . . . 7
⊢ (𝐶 ∈ 𝐻 → (∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶)) | 
| 131 | 9, 125, 130 | sylc 65 | . . . . . 6
⊢ (𝜑 → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶) | 
| 132 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 0 → (𝑆‘𝑦) = (𝑆‘0)) | 
| 133 | 132 | eqcomd 2743 | . . . . . . . . . . . . 13
⊢ (𝑦 = 0 → (𝑆‘0) = (𝑆‘𝑦)) | 
| 134 | 133 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) = (𝑆‘𝑦)) | 
| 135 |  | simplr 769 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘𝑦) = 𝐶) | 
| 136 | 134, 135 | eqtrd 2777 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) = 𝐶) | 
| 137 | 4 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → 𝐶 ∈ ℝ) | 
| 138 | 136, 137 | eqeltrd 2841 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) ∈ ℝ) | 
| 139 | 138, 136 | eqled 11364 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) ≤ 𝐶) | 
| 140 | 139 | 3adantl2 1168 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ 𝑦 = 0) → (𝑆‘0) ≤ 𝐶) | 
| 141 | 4 | rexrd 11311 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐶 ∈
ℝ*) | 
| 142 | 56 | rexrd 11311 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐷 ∈
ℝ*) | 
| 143 | 4, 56, 81 | ltled 11409 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐶 ≤ 𝐷) | 
| 144 |  | lbicc2 13504 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ ℝ*
∧ 𝐷 ∈
ℝ* ∧ 𝐶
≤ 𝐷) → 𝐶 ∈ (𝐶[,]𝐷)) | 
| 145 | 141, 142,
143, 144 | syl3anc 1373 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ∈ (𝐶[,]𝐷)) | 
| 146 |  | ubicc2 13505 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ ℝ*
∧ 𝐷 ∈
ℝ* ∧ 𝐶
≤ 𝐷) → 𝐷 ∈ (𝐶[,]𝐷)) | 
| 147 | 141, 142,
143, 146 | syl3anc 1373 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐷 ∈ (𝐶[,]𝐷)) | 
| 148 |  | prssg 4819 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷))) | 
| 149 | 145, 147,
148 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐶 ∈ (𝐶[,]𝐷) ∧ 𝐷 ∈ (𝐶[,]𝐷)) ↔ {𝐶, 𝐷} ⊆ (𝐶[,]𝐷))) | 
| 150 | 145, 147,
149 | mpbi2and 712 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → {𝐶, 𝐷} ⊆ (𝐶[,]𝐷)) | 
| 151 | 101 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ⊆ (𝐶[,]𝐷)) | 
| 152 | 150, 151 | unssd 4192 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) ⊆ (𝐶[,]𝐷)) | 
| 153 | 8, 152 | eqsstrid 4022 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐻 ⊆ (𝐶[,]𝐷)) | 
| 154 |  | nnm1nn0 12567 | . . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝐻)
∈ ℕ → ((♯‘𝐻) − 1) ∈
ℕ0) | 
| 155 | 79, 154 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((♯‘𝐻) − 1) ∈
ℕ0) | 
| 156 | 1, 155 | eqeltrid 2845 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 157 | 156, 39 | eleqtrdi 2851 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) | 
| 158 |  | eluzfz1 13571 | . . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑁)) | 
| 159 | 157, 158 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ∈ (0...𝑁)) | 
| 160 | 112, 159 | ffvelcdmd 7105 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆‘0) ∈ 𝐻) | 
| 161 | 153, 160 | sseldd 3984 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑆‘0) ∈ (𝐶[,]𝐷)) | 
| 162 | 102, 161 | sseldd 3984 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑆‘0) ∈ ℝ) | 
| 163 | 162 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝑦 = 0) → (𝑆‘0) ∈ ℝ) | 
| 164 | 163 | 3ad2antl1 1186 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) ∈ ℝ) | 
| 165 | 4 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝑦 = 0) → 𝐶 ∈ ℝ) | 
| 166 | 165 | 3ad2antl1 1186 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 𝐶 ∈ ℝ) | 
| 167 |  | elfzelz 13564 | . . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (0...𝑁) → 𝑦 ∈ ℤ) | 
| 168 | 167 | zred 12722 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (0...𝑁) → 𝑦 ∈ ℝ) | 
| 169 | 168 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 𝑦 ∈ ℝ) | 
| 170 |  | elfzle1 13567 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (0...𝑁) → 0 ≤ 𝑦) | 
| 171 | 170 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 0 ≤ 𝑦) | 
| 172 |  | neqne 2948 | . . . . . . . . . . . . . 14
⊢ (¬
𝑦 = 0 → 𝑦 ≠ 0) | 
| 173 | 172 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 𝑦 ≠ 0) | 
| 174 | 169, 171,
173 | ne0gt0d 11398 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ (0...𝑁) ∧ ¬ 𝑦 = 0) → 0 < 𝑦) | 
| 175 | 174 | 3ad2antl2 1187 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 0 < 𝑦) | 
| 176 |  | simpl1 1192 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 𝜑) | 
| 177 |  | simpl2 1193 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → 𝑦 ∈ (0...𝑁)) | 
| 178 | 109 | simprd 495 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦))) | 
| 179 |  | breq1 5146 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 0 → (𝑥 < 𝑦 ↔ 0 < 𝑦)) | 
| 180 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 0 → (𝑆‘𝑥) = (𝑆‘0)) | 
| 181 | 180 | breq1d 5153 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 0 → ((𝑆‘𝑥) < (𝑆‘𝑦) ↔ (𝑆‘0) < (𝑆‘𝑦))) | 
| 182 | 179, 181 | bibi12d 345 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 0 → ((𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ (0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦)))) | 
| 183 | 182 | ralbidv 3178 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 0 → (∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ ∀𝑦 ∈ (0...𝑁)(0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦)))) | 
| 184 | 183 | rspcv 3618 | . . . . . . . . . . . . . 14
⊢ (0 ∈
(0...𝑁) →
(∀𝑥 ∈
(0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → ∀𝑦 ∈ (0...𝑁)(0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦)))) | 
| 185 | 159, 178,
184 | sylc 65 | . . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑦 ∈ (0...𝑁)(0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦))) | 
| 186 | 185 | r19.21bi 3251 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦))) | 
| 187 | 176, 177,
186 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (0 < 𝑦 ↔ (𝑆‘0) < (𝑆‘𝑦))) | 
| 188 | 175, 187 | mpbid 232 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) < (𝑆‘𝑦)) | 
| 189 |  | simpl3 1194 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘𝑦) = 𝐶) | 
| 190 | 188, 189 | breqtrd 5169 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) < 𝐶) | 
| 191 | 164, 166,
190 | ltled 11409 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) ∧ ¬ 𝑦 = 0) → (𝑆‘0) ≤ 𝐶) | 
| 192 | 140, 191 | pm2.61dan 813 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐶) → (𝑆‘0) ≤ 𝐶) | 
| 193 | 192 | rexlimdv3a 3159 | . . . . . 6
⊢ (𝜑 → (∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐶 → (𝑆‘0) ≤ 𝐶)) | 
| 194 | 131, 193 | mpd 15 | . . . . 5
⊢ (𝜑 → (𝑆‘0) ≤ 𝐶) | 
| 195 |  | elicc2 13452 | . . . . . . . 8
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘0) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘0) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘0) ∧ (𝑆‘0) ≤ 𝐷))) | 
| 196 | 4, 56, 195 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → ((𝑆‘0) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘0) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘0) ∧ (𝑆‘0) ≤ 𝐷))) | 
| 197 | 161, 196 | mpbid 232 | . . . . . 6
⊢ (𝜑 → ((𝑆‘0) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘0) ∧ (𝑆‘0) ≤ 𝐷)) | 
| 198 | 197 | simp2d 1144 | . . . . 5
⊢ (𝜑 → 𝐶 ≤ (𝑆‘0)) | 
| 199 | 162, 4 | letri3d 11403 | . . . . 5
⊢ (𝜑 → ((𝑆‘0) = 𝐶 ↔ ((𝑆‘0) ≤ 𝐶 ∧ 𝐶 ≤ (𝑆‘0)))) | 
| 200 | 194, 198,
199 | mpbir2and 713 | . . . 4
⊢ (𝜑 → (𝑆‘0) = 𝐶) | 
| 201 |  | eluzfz2 13572 | . . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘0) → 𝑁 ∈ (0...𝑁)) | 
| 202 | 157, 201 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ (0...𝑁)) | 
| 203 | 112, 202 | ffvelcdmd 7105 | . . . . . . . 8
⊢ (𝜑 → (𝑆‘𝑁) ∈ 𝐻) | 
| 204 | 153, 203 | sseldd 3984 | . . . . . . 7
⊢ (𝜑 → (𝑆‘𝑁) ∈ (𝐶[,]𝐷)) | 
| 205 |  | elicc2 13452 | . . . . . . . 8
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘𝑁) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘𝑁) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑁) ∧ (𝑆‘𝑁) ≤ 𝐷))) | 
| 206 | 4, 56, 205 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → ((𝑆‘𝑁) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘𝑁) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑁) ∧ (𝑆‘𝑁) ≤ 𝐷))) | 
| 207 | 204, 206 | mpbid 232 | . . . . . 6
⊢ (𝜑 → ((𝑆‘𝑁) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑁) ∧ (𝑆‘𝑁) ≤ 𝐷)) | 
| 208 | 207 | simp3d 1145 | . . . . 5
⊢ (𝜑 → (𝑆‘𝑁) ≤ 𝐷) | 
| 209 |  | prid2g 4761 | . . . . . . . . 9
⊢ (𝐷 ∈ ℝ → 𝐷 ∈ {𝐶, 𝐷}) | 
| 210 |  | elun1 4182 | . . . . . . . . 9
⊢ (𝐷 ∈ {𝐶, 𝐷} → 𝐷 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})) | 
| 211 | 56, 209, 210 | 3syl 18 | . . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})) | 
| 212 | 211, 8 | eleqtrrdi 2852 | . . . . . . 7
⊢ (𝜑 → 𝐷 ∈ 𝐻) | 
| 213 |  | eqeq1 2741 | . . . . . . . . . 10
⊢ (ℎ = 𝐷 → (ℎ = (𝑆‘𝑦) ↔ 𝐷 = (𝑆‘𝑦))) | 
| 214 |  | eqcom 2744 | . . . . . . . . . 10
⊢ (𝐷 = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐷) | 
| 215 | 213, 214 | bitrdi 287 | . . . . . . . . 9
⊢ (ℎ = 𝐷 → (ℎ = (𝑆‘𝑦) ↔ (𝑆‘𝑦) = 𝐷)) | 
| 216 | 215 | rexbidv 3179 | . . . . . . . 8
⊢ (ℎ = 𝐷 → (∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) ↔ ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷)) | 
| 217 | 216 | rspcv 3618 | . . . . . . 7
⊢ (𝐷 ∈ 𝐻 → (∀ℎ ∈ 𝐻 ∃𝑦 ∈ (0...𝑁)ℎ = (𝑆‘𝑦) → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷)) | 
| 218 | 212, 125,
217 | sylc 65 | . . . . . 6
⊢ (𝜑 → ∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷) | 
| 219 | 214 | biimpri 228 | . . . . . . . . 9
⊢ ((𝑆‘𝑦) = 𝐷 → 𝐷 = (𝑆‘𝑦)) | 
| 220 | 219 | 3ad2ant3 1136 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐷) → 𝐷 = (𝑆‘𝑦)) | 
| 221 | 113 | ffvelcdmda 7104 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑆‘𝑦) ∈ ℝ) | 
| 222 | 102, 204 | sseldd 3984 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑆‘𝑁) ∈ ℝ) | 
| 223 | 222 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑆‘𝑁) ∈ ℝ) | 
| 224 | 168 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → 𝑦 ∈ ℝ) | 
| 225 |  | elfzel2 13562 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (0...𝑁) → 𝑁 ∈ ℤ) | 
| 226 | 225 | zred 12722 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ (0...𝑁) → 𝑁 ∈ ℝ) | 
| 227 | 226 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → 𝑁 ∈ ℝ) | 
| 228 |  | elfzle2 13568 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ (0...𝑁) → 𝑦 ≤ 𝑁) | 
| 229 | 228 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → 𝑦 ≤ 𝑁) | 
| 230 | 224, 227,
229 | lensymd 11412 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → ¬ 𝑁 < 𝑦) | 
| 231 |  | breq1 5146 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑁 → (𝑥 < 𝑦 ↔ 𝑁 < 𝑦)) | 
| 232 |  | fveq2 6906 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑁 → (𝑆‘𝑥) = (𝑆‘𝑁)) | 
| 233 | 232 | breq1d 5153 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑁 → ((𝑆‘𝑥) < (𝑆‘𝑦) ↔ (𝑆‘𝑁) < (𝑆‘𝑦))) | 
| 234 | 231, 233 | bibi12d 345 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑁 → ((𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ (𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦)))) | 
| 235 | 234 | ralbidv 3178 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑁 → (∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ ∀𝑦 ∈ (0...𝑁)(𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦)))) | 
| 236 | 235 | rspcv 3618 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ (0...𝑁) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → ∀𝑦 ∈ (0...𝑁)(𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦)))) | 
| 237 | 202, 178,
236 | sylc 65 | . . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑦 ∈ (0...𝑁)(𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦))) | 
| 238 | 237 | r19.21bi 3251 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑁 < 𝑦 ↔ (𝑆‘𝑁) < (𝑆‘𝑦))) | 
| 239 | 230, 238 | mtbid 324 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → ¬ (𝑆‘𝑁) < (𝑆‘𝑦)) | 
| 240 | 221, 223,
239 | nltled 11411 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁)) → (𝑆‘𝑦) ≤ (𝑆‘𝑁)) | 
| 241 | 240 | 3adant3 1133 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐷) → (𝑆‘𝑦) ≤ (𝑆‘𝑁)) | 
| 242 | 220, 241 | eqbrtrd 5165 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (0...𝑁) ∧ (𝑆‘𝑦) = 𝐷) → 𝐷 ≤ (𝑆‘𝑁)) | 
| 243 | 242 | rexlimdv3a 3159 | . . . . . 6
⊢ (𝜑 → (∃𝑦 ∈ (0...𝑁)(𝑆‘𝑦) = 𝐷 → 𝐷 ≤ (𝑆‘𝑁))) | 
| 244 | 218, 243 | mpd 15 | . . . . 5
⊢ (𝜑 → 𝐷 ≤ (𝑆‘𝑁)) | 
| 245 | 222, 56 | letri3d 11403 | . . . . 5
⊢ (𝜑 → ((𝑆‘𝑁) = 𝐷 ↔ ((𝑆‘𝑁) ≤ 𝐷 ∧ 𝐷 ≤ (𝑆‘𝑁)))) | 
| 246 | 208, 244,
245 | mpbir2and 713 | . . . 4
⊢ (𝜑 → (𝑆‘𝑁) = 𝐷) | 
| 247 |  | elfzoelz 13699 | . . . . . . . . 9
⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℤ) | 
| 248 | 247 | zred 12722 | . . . . . . . 8
⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℝ) | 
| 249 | 248 | ltp1d 12198 | . . . . . . 7
⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 < (𝑖 + 1)) | 
| 250 | 249 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 < (𝑖 + 1)) | 
| 251 | 178 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → ∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦))) | 
| 252 |  | elfzofz 13715 | . . . . . . . . 9
⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0...𝑁)) | 
| 253 | 252 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0...𝑁)) | 
| 254 |  | fzofzp1 13803 | . . . . . . . . 9
⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0...𝑁)) | 
| 255 | 254 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0...𝑁)) | 
| 256 |  | breq1 5146 | . . . . . . . . . 10
⊢ (𝑥 = 𝑖 → (𝑥 < 𝑦 ↔ 𝑖 < 𝑦)) | 
| 257 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑖 → (𝑆‘𝑥) = (𝑆‘𝑖)) | 
| 258 | 257 | breq1d 5153 | . . . . . . . . . 10
⊢ (𝑥 = 𝑖 → ((𝑆‘𝑥) < (𝑆‘𝑦) ↔ (𝑆‘𝑖) < (𝑆‘𝑦))) | 
| 259 | 256, 258 | bibi12d 345 | . . . . . . . . 9
⊢ (𝑥 = 𝑖 → ((𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) ↔ (𝑖 < 𝑦 ↔ (𝑆‘𝑖) < (𝑆‘𝑦)))) | 
| 260 |  | breq2 5147 | . . . . . . . . . 10
⊢ (𝑦 = (𝑖 + 1) → (𝑖 < 𝑦 ↔ 𝑖 < (𝑖 + 1))) | 
| 261 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑦 = (𝑖 + 1) → (𝑆‘𝑦) = (𝑆‘(𝑖 + 1))) | 
| 262 | 261 | breq2d 5155 | . . . . . . . . . 10
⊢ (𝑦 = (𝑖 + 1) → ((𝑆‘𝑖) < (𝑆‘𝑦) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))) | 
| 263 | 260, 262 | bibi12d 345 | . . . . . . . . 9
⊢ (𝑦 = (𝑖 + 1) → ((𝑖 < 𝑦 ↔ (𝑆‘𝑖) < (𝑆‘𝑦)) ↔ (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))) | 
| 264 | 259, 263 | rspc2v 3633 | . . . . . . . 8
⊢ ((𝑖 ∈ (0...𝑁) ∧ (𝑖 + 1) ∈ (0...𝑁)) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))) | 
| 265 | 253, 255,
264 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (∀𝑥 ∈ (0...𝑁)∀𝑦 ∈ (0...𝑁)(𝑥 < 𝑦 ↔ (𝑆‘𝑥) < (𝑆‘𝑦)) → (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))) | 
| 266 | 251, 265 | mpd 15 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 < (𝑖 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))) | 
| 267 | 250, 266 | mpbid 232 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (𝑆‘𝑖) < (𝑆‘(𝑖 + 1))) | 
| 268 | 267 | ralrimiva 3146 | . . . 4
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))) | 
| 269 | 200, 246,
268 | jca31 514 | . . 3
⊢ (𝜑 → (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))) | 
| 270 |  | fourierdlem54.o | . . . . 5
⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) | 
| 271 | 270 | fourierdlem2 46124 | . . . 4
⊢ (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑m
(0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))) | 
| 272 | 97, 271 | syl 17 | . . 3
⊢ (𝜑 → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑m
(0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))) | 
| 273 | 119, 269,
272 | mpbir2and 713 | . 2
⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁)) | 
| 274 | 97, 273, 107 | jca31 514 | 1
⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻))) |