| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fourierdlem34.q | . . . . 5
⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) | 
| 2 |  | fourierdlem34.m | . . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 3 |  | fourierdlem34.p | . . . . . . 7
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) | 
| 4 | 3 | fourierdlem2 46129 | . . . . . 6
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) | 
| 5 | 2, 4 | syl 17 | . . . . 5
⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) | 
| 6 | 1, 5 | mpbid 232 | . . . 4
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) | 
| 7 | 6 | simpld 494 | . . 3
⊢ (𝜑 → 𝑄 ∈ (ℝ ↑m
(0...𝑀))) | 
| 8 |  | elmapi 8890 | . . 3
⊢ (𝑄 ∈ (ℝ
↑m (0...𝑀))
→ 𝑄:(0...𝑀)⟶ℝ) | 
| 9 | 7, 8 | syl 17 | . 2
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) | 
| 10 |  | simplr 768 | . . . . . 6
⊢
(((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = (𝑄‘𝑗)) ∧ ¬ 𝑖 = 𝑗) → (𝑄‘𝑖) = (𝑄‘𝑗)) | 
| 11 | 9 | ffvelcdmda 7103 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ) | 
| 12 | 11 | ad2antrr 726 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑄‘𝑖) ∈ ℝ) | 
| 13 | 9 | ffvelcdmda 7103 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑀)) → (𝑄‘𝑘) ∈ ℝ) | 
| 14 | 13 | ad4ant14 752 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑘 ∈ (0...𝑀)) → (𝑄‘𝑘) ∈ ℝ) | 
| 15 | 14 | adantllr 719 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑘 ∈ (0...𝑀)) → (𝑄‘𝑘) ∈ ℝ) | 
| 16 |  | eleq1w 2823 | . . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 𝑘 → (𝑖 ∈ (0..^𝑀) ↔ 𝑘 ∈ (0..^𝑀))) | 
| 17 | 16 | anbi2d 630 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑘 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑘 ∈ (0..^𝑀)))) | 
| 18 |  | fveq2 6905 | . . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 𝑘 → (𝑄‘𝑖) = (𝑄‘𝑘)) | 
| 19 |  | oveq1 7439 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1)) | 
| 20 | 19 | fveq2d 6909 | . . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 𝑘 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑘 + 1))) | 
| 21 | 18, 20 | breq12d 5155 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑘 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘𝑘) < (𝑄‘(𝑘 + 1)))) | 
| 22 | 17, 21 | imbi12d 344 | . . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → (𝑄‘𝑘) < (𝑄‘(𝑘 + 1))))) | 
| 23 | 6 | simprrd 773 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) | 
| 24 | 23 | r19.21bi 3250 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) | 
| 25 | 22, 24 | chvarvv 1997 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → (𝑄‘𝑘) < (𝑄‘(𝑘 + 1))) | 
| 26 | 25 | ad4ant14 752 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑘 ∈ (0..^𝑀)) → (𝑄‘𝑘) < (𝑄‘(𝑘 + 1))) | 
| 27 | 26 | adantllr 719 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) ∧ 𝑘 ∈ (0..^𝑀)) → (𝑄‘𝑘) < (𝑄‘(𝑘 + 1))) | 
| 28 |  | simpllr 775 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑖 ∈ (0...𝑀)) | 
| 29 |  | simplr 768 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑗 ∈ (0...𝑀)) | 
| 30 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → 𝑖 < 𝑗) | 
| 31 | 15, 27, 28, 29, 30 | monoords 45314 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑄‘𝑖) < (𝑄‘𝑗)) | 
| 32 | 12, 31 | ltned 11398 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → (𝑄‘𝑖) ≠ (𝑄‘𝑗)) | 
| 33 | 32 | neneqd 2944 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 < 𝑗) → ¬ (𝑄‘𝑖) = (𝑄‘𝑗)) | 
| 34 | 33 | adantlr 715 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑗) ∧ 𝑖 < 𝑗) → ¬ (𝑄‘𝑖) = (𝑄‘𝑗)) | 
| 35 |  | simpll 766 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑗) ∧ ¬ 𝑖 < 𝑗) → ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀))) | 
| 36 |  | elfzelz 13565 | . . . . . . . . . . . 12
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ) | 
| 37 | 36 | zred 12724 | . . . . . . . . . . 11
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ) | 
| 38 | 37 | ad3antlr 731 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑗) ∧ ¬ 𝑖 < 𝑗) → 𝑗 ∈ ℝ) | 
| 39 |  | elfzelz 13565 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℤ) | 
| 40 | 39 | zred 12724 | . . . . . . . . . . 11
⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℝ) | 
| 41 | 40 | ad4antlr 733 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑗) ∧ ¬ 𝑖 < 𝑗) → 𝑖 ∈ ℝ) | 
| 42 |  | neqne 2947 | . . . . . . . . . . . 12
⊢ (¬
𝑖 = 𝑗 → 𝑖 ≠ 𝑗) | 
| 43 | 42 | necomd 2995 | . . . . . . . . . . 11
⊢ (¬
𝑖 = 𝑗 → 𝑗 ≠ 𝑖) | 
| 44 | 43 | ad2antlr 727 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑗) ∧ ¬ 𝑖 < 𝑗) → 𝑗 ≠ 𝑖) | 
| 45 |  | simpr 484 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑗) ∧ ¬ 𝑖 < 𝑗) → ¬ 𝑖 < 𝑗) | 
| 46 | 38, 41, 44, 45 | lttri5d 45316 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑗) ∧ ¬ 𝑖 < 𝑗) → 𝑗 < 𝑖) | 
| 47 | 9 | ffvelcdmda 7103 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑄‘𝑗) ∈ ℝ) | 
| 48 | 47 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 < 𝑖) → (𝑄‘𝑗) ∈ ℝ) | 
| 49 | 48 | adantllr 719 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 < 𝑖) → (𝑄‘𝑗) ∈ ℝ) | 
| 50 |  | simp-4l 782 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 < 𝑖) ∧ 𝑘 ∈ (0...𝑀)) → 𝜑) | 
| 51 | 50, 13 | sylancom 588 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 < 𝑖) ∧ 𝑘 ∈ (0...𝑀)) → (𝑄‘𝑘) ∈ ℝ) | 
| 52 |  | simp-4l 782 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 < 𝑖) ∧ 𝑘 ∈ (0..^𝑀)) → 𝜑) | 
| 53 | 52, 25 | sylancom 588 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 < 𝑖) ∧ 𝑘 ∈ (0..^𝑀)) → (𝑄‘𝑘) < (𝑄‘(𝑘 + 1))) | 
| 54 |  | simplr 768 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 < 𝑖) → 𝑗 ∈ (0...𝑀)) | 
| 55 |  | simpllr 775 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 < 𝑖) → 𝑖 ∈ (0...𝑀)) | 
| 56 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 < 𝑖) → 𝑗 < 𝑖) | 
| 57 | 51, 53, 54, 55, 56 | monoords 45314 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 < 𝑖) → (𝑄‘𝑗) < (𝑄‘𝑖)) | 
| 58 | 49, 57 | gtned 11397 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 < 𝑖) → (𝑄‘𝑖) ≠ (𝑄‘𝑗)) | 
| 59 | 58 | neneqd 2944 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑗 < 𝑖) → ¬ (𝑄‘𝑖) = (𝑄‘𝑗)) | 
| 60 | 35, 46, 59 | syl2anc 584 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑗) ∧ ¬ 𝑖 < 𝑗) → ¬ (𝑄‘𝑖) = (𝑄‘𝑗)) | 
| 61 | 34, 60 | pm2.61dan 812 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑗) → ¬ (𝑄‘𝑖) = (𝑄‘𝑗)) | 
| 62 | 61 | adantlr 715 | . . . . . 6
⊢
(((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = (𝑄‘𝑗)) ∧ ¬ 𝑖 = 𝑗) → ¬ (𝑄‘𝑖) = (𝑄‘𝑗)) | 
| 63 | 10, 62 | condan 817 | . . . . 5
⊢ ((((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = (𝑄‘𝑗)) → 𝑖 = 𝑗) | 
| 64 | 63 | ex 412 | . . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑄‘𝑖) = (𝑄‘𝑗) → 𝑖 = 𝑗)) | 
| 65 | 64 | ralrimiva 3145 | . . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ∀𝑗 ∈ (0...𝑀)((𝑄‘𝑖) = (𝑄‘𝑗) → 𝑖 = 𝑗)) | 
| 66 | 65 | ralrimiva 3145 | . 2
⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)∀𝑗 ∈ (0...𝑀)((𝑄‘𝑖) = (𝑄‘𝑗) → 𝑖 = 𝑗)) | 
| 67 |  | dff13 7276 | . 2
⊢ (𝑄:(0...𝑀)–1-1→ℝ ↔ (𝑄:(0...𝑀)⟶ℝ ∧ ∀𝑖 ∈ (0...𝑀)∀𝑗 ∈ (0...𝑀)((𝑄‘𝑖) = (𝑄‘𝑗) → 𝑖 = 𝑗))) | 
| 68 | 9, 66, 67 | sylanbrc 583 | 1
⊢ (𝜑 → 𝑄:(0...𝑀)–1-1→ℝ) |