Step | Hyp | Ref
| Expression |
1 | | fourierdlem34.q |
. . . . 5
β’ (π β π β (πβπ)) |
2 | | fourierdlem34.m |
. . . . . 6
β’ (π β π β β) |
3 | | fourierdlem34.p |
. . . . . . 7
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
4 | 3 | fourierdlem2 44910 |
. . . . . 6
β’ (π β β β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
5 | 2, 4 | syl 17 |
. . . . 5
β’ (π β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
6 | 1, 5 | mpbid 231 |
. . . 4
β’ (π β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))))) |
7 | 6 | simpld 495 |
. . 3
β’ (π β π β (β βm
(0...π))) |
8 | | elmapi 8845 |
. . 3
β’ (π β (β
βm (0...π))
β π:(0...π)βΆβ) |
9 | 7, 8 | syl 17 |
. 2
β’ (π β π:(0...π)βΆβ) |
10 | | simplr 767 |
. . . . . 6
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ (πβπ) = (πβπ)) β§ Β¬ π = π) β (πβπ) = (πβπ)) |
11 | 9 | ffvelcdmda 7086 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...π)) β (πβπ) β β) |
12 | 11 | ad2antrr 724 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β (πβπ) β β) |
13 | 9 | ffvelcdmda 7086 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...π)) β (πβπ) β β) |
14 | 13 | ad4ant14 750 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β (0...π)) β (πβπ) β β) |
15 | 14 | adantllr 717 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β§ π β (0...π)) β (πβπ) β β) |
16 | | eleq1w 2816 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π β (0..^π) β π β (0..^π))) |
17 | 16 | anbi2d 629 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π β§ π β (0..^π)) β (π β§ π β (0..^π)))) |
18 | | fveq2 6891 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (πβπ) = (πβπ)) |
19 | | oveq1 7418 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (π + 1) = (π + 1)) |
20 | 19 | fveq2d 6895 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (πβ(π + 1)) = (πβ(π + 1))) |
21 | 18, 20 | breq12d 5161 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((πβπ) < (πβ(π + 1)) β (πβπ) < (πβ(π + 1)))) |
22 | 17, 21 | imbi12d 344 |
. . . . . . . . . . . . . . 15
β’ (π = π β (((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) β ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))))) |
23 | 6 | simprrd 772 |
. . . . . . . . . . . . . . . 16
β’ (π β βπ β (0..^π)(πβπ) < (πβ(π + 1))) |
24 | 23 | r19.21bi 3248 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
25 | 22, 24 | chvarvv 2002 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
26 | 25 | ad4ant14 750 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
27 | 26 | adantllr 717 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
28 | | simpllr 774 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β π β (0...π)) |
29 | | simplr 767 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β π β (0...π)) |
30 | | simpr 485 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β π < π) |
31 | 15, 27, 28, 29, 30 | monoords 44092 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β (πβπ) < (πβπ)) |
32 | 12, 31 | ltned 11352 |
. . . . . . . . . 10
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β (πβπ) β (πβπ)) |
33 | 32 | neneqd 2945 |
. . . . . . . . 9
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β Β¬ (πβπ) = (πβπ)) |
34 | 33 | adantlr 713 |
. . . . . . . 8
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ Β¬ π = π) β§ π < π) β Β¬ (πβπ) = (πβπ)) |
35 | | simpll 765 |
. . . . . . . . 9
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ Β¬ π = π) β§ Β¬ π < π) β ((π β§ π β (0...π)) β§ π β (0...π))) |
36 | | elfzelz 13503 |
. . . . . . . . . . . 12
β’ (π β (0...π) β π β β€) |
37 | 36 | zred 12668 |
. . . . . . . . . . 11
β’ (π β (0...π) β π β β) |
38 | 37 | ad3antlr 729 |
. . . . . . . . . 10
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ Β¬ π = π) β§ Β¬ π < π) β π β β) |
39 | | elfzelz 13503 |
. . . . . . . . . . . 12
β’ (π β (0...π) β π β β€) |
40 | 39 | zred 12668 |
. . . . . . . . . . 11
β’ (π β (0...π) β π β β) |
41 | 40 | ad4antlr 731 |
. . . . . . . . . 10
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ Β¬ π = π) β§ Β¬ π < π) β π β β) |
42 | | neqne 2948 |
. . . . . . . . . . . 12
β’ (Β¬
π = π β π β π) |
43 | 42 | necomd 2996 |
. . . . . . . . . . 11
β’ (Β¬
π = π β π β π) |
44 | 43 | ad2antlr 725 |
. . . . . . . . . 10
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ Β¬ π = π) β§ Β¬ π < π) β π β π) |
45 | | simpr 485 |
. . . . . . . . . 10
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ Β¬ π = π) β§ Β¬ π < π) β Β¬ π < π) |
46 | 38, 41, 44, 45 | lttri5d 44094 |
. . . . . . . . 9
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ Β¬ π = π) β§ Β¬ π < π) β π < π) |
47 | 9 | ffvelcdmda 7086 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...π)) β (πβπ) β β) |
48 | 47 | adantr 481 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ π < π) β (πβπ) β β) |
49 | 48 | adantllr 717 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β (πβπ) β β) |
50 | | simp-4l 781 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β§ π β (0...π)) β π) |
51 | 50, 13 | sylancom 588 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β§ π β (0...π)) β (πβπ) β β) |
52 | | simp-4l 781 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β§ π β (0..^π)) β π) |
53 | 52, 25 | sylancom 588 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
54 | | simplr 767 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β π β (0...π)) |
55 | | simpllr 774 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β π β (0...π)) |
56 | | simpr 485 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β π < π) |
57 | 51, 53, 54, 55, 56 | monoords 44092 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β (πβπ) < (πβπ)) |
58 | 49, 57 | gtned 11351 |
. . . . . . . . . 10
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β (πβπ) β (πβπ)) |
59 | 58 | neneqd 2945 |
. . . . . . . . 9
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β Β¬ (πβπ) = (πβπ)) |
60 | 35, 46, 59 | syl2anc 584 |
. . . . . . . 8
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ Β¬ π = π) β§ Β¬ π < π) β Β¬ (πβπ) = (πβπ)) |
61 | 34, 60 | pm2.61dan 811 |
. . . . . . 7
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ Β¬ π = π) β Β¬ (πβπ) = (πβπ)) |
62 | 61 | adantlr 713 |
. . . . . 6
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ (πβπ) = (πβπ)) β§ Β¬ π = π) β Β¬ (πβπ) = (πβπ)) |
63 | 10, 62 | condan 816 |
. . . . 5
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ (πβπ) = (πβπ)) β π = π) |
64 | 63 | ex 413 |
. . . 4
β’ (((π β§ π β (0...π)) β§ π β (0...π)) β ((πβπ) = (πβπ) β π = π)) |
65 | 64 | ralrimiva 3146 |
. . 3
β’ ((π β§ π β (0...π)) β βπ β (0...π)((πβπ) = (πβπ) β π = π)) |
66 | 65 | ralrimiva 3146 |
. 2
β’ (π β βπ β (0...π)βπ β (0...π)((πβπ) = (πβπ) β π = π)) |
67 | | dff13 7256 |
. 2
β’ (π:(0...π)β1-1ββ β (π:(0...π)βΆβ β§ βπ β (0...π)βπ β (0...π)((πβπ) = (πβπ) β π = π))) |
68 | 9, 66, 67 | sylanbrc 583 |
1
β’ (π β π:(0...π)β1-1ββ) |