Step | Hyp | Ref
| Expression |
1 | | fourierdlem34.q |
. . . . 5
β’ (π β π β (πβπ)) |
2 | | fourierdlem34.m |
. . . . . 6
β’ (π β π β β) |
3 | | fourierdlem34.p |
. . . . . . 7
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
4 | 3 | fourierdlem2 44825 |
. . . . . 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 496 |
. . 3
β’ (π β π β (β βm
(0...π))) |
8 | | elmapi 8843 |
. . 3
β’ (π β (β
βm (0...π))
β π:(0...π)βΆβ) |
9 | 7, 8 | syl 17 |
. 2
β’ (π β π:(0...π)βΆβ) |
10 | | simplr 768 |
. . . . . 6
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ (πβπ) = (πβπ)) β§ Β¬ π = π) β (πβπ) = (πβπ)) |
11 | 9 | ffvelcdmda 7087 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...π)) β (πβπ) β β) |
12 | 11 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β (πβπ) β β) |
13 | 9 | ffvelcdmda 7087 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...π)) β (πβπ) β β) |
14 | 13 | ad4ant14 751 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β (0...π)) β (πβπ) β β) |
15 | 14 | adantllr 718 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β§ π β (0...π)) β (πβπ) β β) |
16 | | eleq1w 2817 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π β (0..^π) β π β (0..^π))) |
17 | 16 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π β§ π β (0..^π)) β (π β§ π β (0..^π)))) |
18 | | fveq2 6892 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (πβπ) = (πβπ)) |
19 | | oveq1 7416 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (π + 1) = (π + 1)) |
20 | 19 | fveq2d 6896 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (πβ(π + 1)) = (πβ(π + 1))) |
21 | 18, 20 | breq12d 5162 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((πβπ) < (πβ(π + 1)) β (πβπ) < (πβ(π + 1)))) |
22 | 17, 21 | imbi12d 345 |
. . . . . . . . . . . . . . 15
β’ (π = π β (((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) β ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))))) |
23 | 6 | simprrd 773 |
. . . . . . . . . . . . . . . 16
β’ (π β βπ β (0..^π)(πβπ) < (πβ(π + 1))) |
24 | 23 | r19.21bi 3249 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
25 | 22, 24 | chvarvv 2003 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
26 | 25 | ad4ant14 751 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
27 | 26 | adantllr 718 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
28 | | simpllr 775 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β π β (0...π)) |
29 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β π β (0...π)) |
30 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β π < π) |
31 | 15, 27, 28, 29, 30 | monoords 44007 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β (πβπ) < (πβπ)) |
32 | 12, 31 | ltned 11350 |
. . . . . . . . . 10
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β (πβπ) β (πβπ)) |
33 | 32 | neneqd 2946 |
. . . . . . . . 9
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β Β¬ (πβπ) = (πβπ)) |
34 | 33 | adantlr 714 |
. . . . . . . 8
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ Β¬ π = π) β§ π < π) β Β¬ (πβπ) = (πβπ)) |
35 | | simpll 766 |
. . . . . . . . 9
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ Β¬ π = π) β§ Β¬ π < π) β ((π β§ π β (0...π)) β§ π β (0...π))) |
36 | | elfzelz 13501 |
. . . . . . . . . . . 12
β’ (π β (0...π) β π β β€) |
37 | 36 | zred 12666 |
. . . . . . . . . . 11
β’ (π β (0...π) β π β β) |
38 | 37 | ad3antlr 730 |
. . . . . . . . . 10
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ Β¬ π = π) β§ Β¬ π < π) β π β β) |
39 | | elfzelz 13501 |
. . . . . . . . . . . 12
β’ (π β (0...π) β π β β€) |
40 | 39 | zred 12666 |
. . . . . . . . . . 11
β’ (π β (0...π) β π β β) |
41 | 40 | ad4antlr 732 |
. . . . . . . . . 10
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ Β¬ π = π) β§ Β¬ π < π) β π β β) |
42 | | neqne 2949 |
. . . . . . . . . . . 12
β’ (Β¬
π = π β π β π) |
43 | 42 | necomd 2997 |
. . . . . . . . . . 11
β’ (Β¬
π = π β π β π) |
44 | 43 | ad2antlr 726 |
. . . . . . . . . 10
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ Β¬ π = π) β§ Β¬ π < π) β π β π) |
45 | | simpr 486 |
. . . . . . . . . 10
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ Β¬ π = π) β§ Β¬ π < π) β Β¬ π < π) |
46 | 38, 41, 44, 45 | lttri5d 44009 |
. . . . . . . . 9
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ Β¬ π = π) β§ Β¬ π < π) β π < π) |
47 | 9 | ffvelcdmda 7087 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...π)) β (πβπ) β β) |
48 | 47 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ π < π) β (πβπ) β β) |
49 | 48 | adantllr 718 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β (πβπ) β β) |
50 | | simp-4l 782 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β§ π β (0...π)) β π) |
51 | 50, 13 | sylancom 589 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β§ π β (0...π)) β (πβπ) β β) |
52 | | simp-4l 782 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β§ π β (0..^π)) β π) |
53 | 52, 25 | sylancom 589 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
54 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β π β (0...π)) |
55 | | simpllr 775 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β π β (0...π)) |
56 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β π < π) |
57 | 51, 53, 54, 55, 56 | monoords 44007 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β (πβπ) < (πβπ)) |
58 | 49, 57 | gtned 11349 |
. . . . . . . . . 10
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β (πβπ) β (πβπ)) |
59 | 58 | neneqd 2946 |
. . . . . . . . 9
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ π < π) β Β¬ (πβπ) = (πβπ)) |
60 | 35, 46, 59 | syl2anc 585 |
. . . . . . . 8
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ Β¬ π = π) β§ Β¬ π < π) β Β¬ (πβπ) = (πβπ)) |
61 | 34, 60 | pm2.61dan 812 |
. . . . . . 7
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ Β¬ π = π) β Β¬ (πβπ) = (πβπ)) |
62 | 61 | adantlr 714 |
. . . . . 6
β’
(((((π β§ π β (0...π)) β§ π β (0...π)) β§ (πβπ) = (πβπ)) β§ Β¬ π = π) β Β¬ (πβπ) = (πβπ)) |
63 | 10, 62 | condan 817 |
. . . . 5
β’ ((((π β§ π β (0...π)) β§ π β (0...π)) β§ (πβπ) = (πβπ)) β π = π) |
64 | 63 | ex 414 |
. . . 4
β’ (((π β§ π β (0...π)) β§ π β (0...π)) β ((πβπ) = (πβπ) β π = π)) |
65 | 64 | ralrimiva 3147 |
. . 3
β’ ((π β§ π β (0...π)) β βπ β (0...π)((πβπ) = (πβπ) β π = π)) |
66 | 65 | ralrimiva 3147 |
. 2
β’ (π β βπ β (0...π)βπ β (0...π)((πβπ) = (πβπ) β π = π)) |
67 | | dff13 7254 |
. 2
β’ (π:(0...π)β1-1ββ β (π:(0...π)βΆβ β§ βπ β (0...π)βπ β (0...π)((πβπ) = (πβπ) β π = π))) |
68 | 9, 66, 67 | sylanbrc 584 |
1
β’ (π β π:(0...π)β1-1ββ) |