Step | Hyp | Ref
| Expression |
1 | | fourierdlem77.bd |
. 2
β’ (π β βπ β β βπ β (-Ο[,]Ο)(absβ(π»βπ )) β€ π) |
2 | | pire 25867 |
. . . . . . . . . 10
β’ Ο
β β |
3 | 2 | renegcli 11486 |
. . . . . . . . 9
β’ -Ο
β β |
4 | 3 | a1i 11 |
. . . . . . . 8
β’ (β€
β -Ο β β) |
5 | 2 | a1i 11 |
. . . . . . . 8
β’ (β€
β Ο β β) |
6 | | pirp 25870 |
. . . . . . . . . . 11
β’ Ο
β β+ |
7 | | neglt 43672 |
. . . . . . . . . . 11
β’ (Ο
β β+ β -Ο < Ο) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . 10
β’ -Ο
< Ο |
9 | 3, 2, 8 | ltleii 11302 |
. . . . . . . . 9
β’ -Ο
β€ Ο |
10 | 9 | a1i 11 |
. . . . . . . 8
β’ (β€
β -Ο β€ Ο) |
11 | | fourierdlem77.k |
. . . . . . . . . 10
β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) |
12 | 11 | fourierdlem62 44562 |
. . . . . . . . 9
β’ πΎ β
((-Ο[,]Ο)βcnββ) |
13 | 12 | a1i 11 |
. . . . . . . 8
β’ (β€
β πΎ β
((-Ο[,]Ο)βcnββ)) |
14 | 4, 5, 10, 13 | evthiccabs 43887 |
. . . . . . 7
β’ (β€
β (βπ β
(-Ο[,]Ο)βπ
β (-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ)) β§ βπ₯ β (-Ο[,]Ο)βπ¦ β
(-Ο[,]Ο)(absβ(πΎβπ₯)) β€ (absβ(πΎβπ¦)))) |
15 | 14 | mptru 1548 |
. . . . . 6
β’
(βπ β
(-Ο[,]Ο)βπ
β (-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ)) β§ βπ₯ β (-Ο[,]Ο)βπ¦ β
(-Ο[,]Ο)(absβ(πΎβπ₯)) β€ (absβ(πΎβπ¦))) |
16 | 15 | simpli 484 |
. . . . 5
β’
βπ β
(-Ο[,]Ο)βπ
β (-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ)) |
17 | 16 | a1i 11 |
. . . 4
β’ ((π β§ π β β β§ βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π) β βπ β (-Ο[,]Ο)βπ β
(-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ))) |
18 | | simpl 483 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β (-Ο[,]Ο)) β
π β
β) |
19 | 11 | fourierdlem43 44544 |
. . . . . . . . . . . . . 14
β’ πΎ:(-Ο[,]Ο)βΆβ |
20 | 19 | ffvelcdmi 7054 |
. . . . . . . . . . . . 13
β’ (π β (-Ο[,]Ο) β
(πΎβπ) β β) |
21 | 20 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β (-Ο[,]Ο)) β
(πΎβπ) β β) |
22 | 18, 21 | remulcld 11209 |
. . . . . . . . . . 11
β’ ((π β β β§ π β (-Ο[,]Ο)) β
(π Β· (πΎβπ)) β β) |
23 | 22 | recnd 11207 |
. . . . . . . . . 10
β’ ((π β β β§ π β (-Ο[,]Ο)) β
(π Β· (πΎβπ)) β β) |
24 | 23 | abscld 15348 |
. . . . . . . . 9
β’ ((π β β β§ π β (-Ο[,]Ο)) β
(absβ(π Β·
(πΎβπ))) β β) |
25 | 23 | absge0d 15356 |
. . . . . . . . 9
β’ ((π β β β§ π β (-Ο[,]Ο)) β 0
β€ (absβ(π Β·
(πΎβπ)))) |
26 | 24, 25 | ge0p1rpd 13011 |
. . . . . . . 8
β’ ((π β β β§ π β (-Ο[,]Ο)) β
((absβ(π Β·
(πΎβπ))) + 1) β
β+) |
27 | 26 | 3ad2antl2 1186 |
. . . . . . 7
β’ (((π β§ π β β β§ βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β
((absβ(π Β·
(πΎβπ))) + 1) β
β+) |
28 | 27 | 3adant3 1132 |
. . . . . 6
β’ (((π β§ π β β β§ βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο) β§ βπ β
(-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β ((absβ(π Β· (πΎβπ))) + 1) β
β+) |
29 | | nfv 1917 |
. . . . . . . . 9
β’
β²π π |
30 | | nfv 1917 |
. . . . . . . . 9
β’
β²π π β β |
31 | | nfra1 3278 |
. . . . . . . . 9
β’
β²π βπ β (-Ο[,]Ο)(absβ(π»βπ )) β€ π |
32 | 29, 30, 31 | nf3an 1904 |
. . . . . . . 8
β’
β²π (π β§ π β β β§ βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π) |
33 | | nfv 1917 |
. . . . . . . 8
β’
β²π π β
(-Ο[,]Ο) |
34 | | nfra1 3278 |
. . . . . . . 8
β’
β²π βπ β (-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ)) |
35 | 32, 33, 34 | nf3an 1904 |
. . . . . . 7
β’
β²π ((π β§ π β β β§ βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο) β§ βπ β
(-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ))) |
36 | | simpl11 1248 |
. . . . . . . . . . 11
β’ ((((π β§ π β β β§ βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο) β§ βπ β
(-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β π) |
37 | | simpl12 1249 |
. . . . . . . . . . 11
β’ ((((π β§ π β β β§ βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο) β§ βπ β
(-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β π β
β) |
38 | 36, 37 | jca 512 |
. . . . . . . . . 10
β’ ((((π β§ π β β β§ βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο) β§ βπ β
(-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β (π β§ π β β)) |
39 | | simpl13 1250 |
. . . . . . . . . . 11
β’ ((((π β§ π β β β§ βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο) β§ βπ β
(-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π) |
40 | | rspa 3242 |
. . . . . . . . . . 11
β’
((βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π β§ π β (-Ο[,]Ο)) β
(absβ(π»βπ )) β€ π) |
41 | 39, 40 | sylancom 588 |
. . . . . . . . . 10
β’ ((((π β§ π β β β§ βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο) β§ βπ β
(-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β
(absβ(π»βπ )) β€ π) |
42 | | simpl2 1192 |
. . . . . . . . . 10
β’ ((((π β§ π β β β§ βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο) β§ βπ β
(-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β π β
(-Ο[,]Ο)) |
43 | 38, 41, 42 | jca31 515 |
. . . . . . . . 9
β’ ((((π β§ π β β β§ βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο) β§ βπ β
(-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β (((π β§ π β β) β§ (absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο))) |
44 | | rspa 3242 |
. . . . . . . . . 10
β’
((βπ β
(-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ)) β§ π β (-Ο[,]Ο)) β
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) |
45 | 44 | 3ad2antl3 1187 |
. . . . . . . . 9
β’ ((((π β§ π β β β§ βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο) β§ βπ β
(-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) |
46 | | simpr 485 |
. . . . . . . . 9
β’ ((((π β§ π β β β§ βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο) β§ βπ β
(-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β π β
(-Ο[,]Ο)) |
47 | | simp-5l 783 |
. . . . . . . . . . 11
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β π) |
48 | | simpr 485 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (-Ο[,]Ο)) β π β
(-Ο[,]Ο)) |
49 | | fourierdlem77.f |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΉ:ββΆβ) |
50 | | fourierdlem77.x |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β β) |
51 | | fourierdlem77.y |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β β) |
52 | | fourierdlem77.w |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β β) |
53 | | fourierdlem77.h |
. . . . . . . . . . . . . . . . . 18
β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) |
54 | 49, 50, 51, 52, 53 | fourierdlem9 44510 |
. . . . . . . . . . . . . . . . 17
β’ (π β π»:(-Ο[,]Ο)βΆβ) |
55 | 54 | ffvelcdmda 7055 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (-Ο[,]Ο)) β (π»βπ ) β β) |
56 | 19 | ffvelcdmi 7054 |
. . . . . . . . . . . . . . . . 17
β’ (π β (-Ο[,]Ο) β
(πΎβπ ) β β) |
57 | 56 | adantl 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (-Ο[,]Ο)) β (πΎβπ ) β β) |
58 | 55, 57 | remulcld 11209 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (-Ο[,]Ο)) β ((π»βπ ) Β· (πΎβπ )) β β) |
59 | | fourierdlem77.u |
. . . . . . . . . . . . . . . 16
β’ π = (π β (-Ο[,]Ο) β¦ ((π»βπ ) Β· (πΎβπ ))) |
60 | 59 | fvmpt2 6979 |
. . . . . . . . . . . . . . 15
β’ ((π β (-Ο[,]Ο) β§
((π»βπ ) Β· (πΎβπ )) β β) β (πβπ ) = ((π»βπ ) Β· (πΎβπ ))) |
61 | 48, 58, 60 | syl2anc 584 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (-Ο[,]Ο)) β (πβπ ) = ((π»βπ ) Β· (πΎβπ ))) |
62 | 61, 58 | eqeltrd 2832 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (-Ο[,]Ο)) β (πβπ ) β β) |
63 | 62 | recnd 11207 |
. . . . . . . . . . . 12
β’ ((π β§ π β (-Ο[,]Ο)) β (πβπ ) β β) |
64 | 63 | abscld 15348 |
. . . . . . . . . . 11
β’ ((π β§ π β (-Ο[,]Ο)) β
(absβ(πβπ )) β
β) |
65 | 47, 64 | sylancom 588 |
. . . . . . . . . 10
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β
(absβ(πβπ )) β
β) |
66 | | simp-5r 784 |
. . . . . . . . . . . 12
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β π β
β) |
67 | | simpllr 774 |
. . . . . . . . . . . 12
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β π β
(-Ο[,]Ο)) |
68 | 66, 67, 24 | syl2anc 584 |
. . . . . . . . . . 11
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β
(absβ(π Β·
(πΎβπ))) β β) |
69 | | peano2re 11352 |
. . . . . . . . . . 11
β’
((absβ(π
Β· (πΎβπ))) β β β
((absβ(π Β·
(πΎβπ))) + 1) β β) |
70 | 68, 69 | syl 17 |
. . . . . . . . . 10
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β
((absβ(π Β·
(πΎβπ))) + 1) β β) |
71 | 61 | fveq2d 6866 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (-Ο[,]Ο)) β
(absβ(πβπ )) = (absβ((π»βπ ) Β· (πΎβπ )))) |
72 | 47, 71 | sylancom 588 |
. . . . . . . . . . . 12
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β
(absβ(πβπ )) = (absβ((π»βπ ) Β· (πΎβπ )))) |
73 | 55 | recnd 11207 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (-Ο[,]Ο)) β (π»βπ ) β β) |
74 | 73 | abscld 15348 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (-Ο[,]Ο)) β
(absβ(π»βπ )) β
β) |
75 | 47, 74 | sylancom 588 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β
(absβ(π»βπ )) β
β) |
76 | | recn 11165 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β) |
77 | 76 | abscld 15348 |
. . . . . . . . . . . . . . 15
β’ (π β β β
(absβπ) β
β) |
78 | 66, 77 | syl 17 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β
(absβπ) β
β) |
79 | 56 | recnd 11207 |
. . . . . . . . . . . . . . . 16
β’ (π β (-Ο[,]Ο) β
(πΎβπ ) β β) |
80 | 79 | abscld 15348 |
. . . . . . . . . . . . . . 15
β’ (π β (-Ο[,]Ο) β
(absβ(πΎβπ )) β
β) |
81 | 80 | adantl 482 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β
(absβ(πΎβπ )) β
β) |
82 | 20 | recnd 11207 |
. . . . . . . . . . . . . . . 16
β’ (π β (-Ο[,]Ο) β
(πΎβπ) β β) |
83 | 82 | abscld 15348 |
. . . . . . . . . . . . . . 15
β’ (π β (-Ο[,]Ο) β
(absβ(πΎβπ)) β
β) |
84 | 67, 83 | syl 17 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β
(absβ(πΎβπ)) β
β) |
85 | 73 | absge0d 15356 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (-Ο[,]Ο)) β 0 β€
(absβ(π»βπ ))) |
86 | 47, 85 | sylancom 588 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β 0 β€
(absβ(π»βπ ))) |
87 | 82 | absge0d 15356 |
. . . . . . . . . . . . . . 15
β’ (π β (-Ο[,]Ο) β 0
β€ (absβ(πΎβπ))) |
88 | 67, 87 | syl 17 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β 0 β€
(absβ(πΎβπ))) |
89 | 74 | ad4ant14 750 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β β) β§ (absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β
(absβ(π»βπ )) β
β) |
90 | | simpllr 774 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β β) β§ (absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β π β
β) |
91 | 77 | ad3antlr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β β) β§ (absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β
(absβπ) β
β) |
92 | | simplr 767 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β β) β§ (absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β
(absβ(π»βπ )) β€ π) |
93 | 90 | leabsd 15326 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β β) β§ (absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β π β€ (absβπ)) |
94 | 89, 90, 91, 92, 93 | letrd 11336 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β β) β§ (absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β
(absβ(π»βπ )) β€ (absβπ)) |
95 | 94 | ad4ant14 750 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β
(absβ(π»βπ )) β€ (absβπ)) |
96 | | simplr 767 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) |
97 | 75, 78, 81, 84, 86, 88, 95, 96 | lemul12bd 12122 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β
((absβ(π»βπ )) Β· (absβ(πΎβπ ))) β€ ((absβπ) Β· (absβ(πΎβπ)))) |
98 | 57 | recnd 11207 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (-Ο[,]Ο)) β (πΎβπ ) β β) |
99 | 73, 98 | absmuld 15366 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (-Ο[,]Ο)) β
(absβ((π»βπ ) Β· (πΎβπ ))) = ((absβ(π»βπ )) Β· (absβ(πΎβπ )))) |
100 | 47, 99 | sylancom 588 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β
(absβ((π»βπ ) Β· (πΎβπ ))) = ((absβ(π»βπ )) Β· (absβ(πΎβπ )))) |
101 | 76 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β (-Ο[,]Ο)) β
π β
β) |
102 | 21 | recnd 11207 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β (-Ο[,]Ο)) β
(πΎβπ) β β) |
103 | 101, 102 | absmuld 15366 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β (-Ο[,]Ο)) β
(absβ(π Β·
(πΎβπ))) = ((absβπ) Β· (absβ(πΎβπ)))) |
104 | 66, 67, 103 | syl2anc 584 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β
(absβ(π Β·
(πΎβπ))) = ((absβπ) Β· (absβ(πΎβπ)))) |
105 | 97, 100, 104 | 3brtr4d 5157 |
. . . . . . . . . . . 12
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β
(absβ((π»βπ ) Β· (πΎβπ ))) β€ (absβ(π Β· (πΎβπ)))) |
106 | 72, 105 | eqbrtrd 5147 |
. . . . . . . . . . 11
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β
(absβ(πβπ )) β€ (absβ(π Β· (πΎβπ)))) |
107 | 68 | ltp1d 12109 |
. . . . . . . . . . 11
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β
(absβ(π Β·
(πΎβπ))) < ((absβ(π Β· (πΎβπ))) + 1)) |
108 | 65, 68, 70, 106, 107 | lelttrd 11337 |
. . . . . . . . . 10
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β
(absβ(πβπ )) < ((absβ(π Β· (πΎβπ))) + 1)) |
109 | 65, 70, 108 | ltled 11327 |
. . . . . . . . 9
β’
((((((π β§ π β β) β§
(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο)) β§
(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β
(absβ(πβπ )) β€ ((absβ(π Β· (πΎβπ))) + 1)) |
110 | 43, 45, 46, 109 | syl21anc 836 |
. . . . . . . 8
β’ ((((π β§ π β β β§ βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο) β§ βπ β
(-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β§ π β (-Ο[,]Ο)) β
(absβ(πβπ )) β€ ((absβ(π Β· (πΎβπ))) + 1)) |
111 | 110 | ex 413 |
. . . . . . 7
β’ (((π β§ π β β β§ βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο) β§ βπ β
(-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β (π β (-Ο[,]Ο) β
(absβ(πβπ )) β€ ((absβ(π Β· (πΎβπ))) + 1))) |
112 | 35, 111 | ralrimi 3251 |
. . . . . 6
β’ (((π β§ π β β β§ βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο) β§ βπ β
(-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β βπ β (-Ο[,]Ο)(absβ(πβπ )) β€ ((absβ(π Β· (πΎβπ))) + 1)) |
113 | | breq2 5129 |
. . . . . . . 8
β’ (π = ((absβ(π Β· (πΎβπ))) + 1) β ((absβ(πβπ )) β€ π β (absβ(πβπ )) β€ ((absβ(π Β· (πΎβπ))) + 1))) |
114 | 113 | ralbidv 3176 |
. . . . . . 7
β’ (π = ((absβ(π Β· (πΎβπ))) + 1) β (βπ β (-Ο[,]Ο)(absβ(πβπ )) β€ π β βπ β (-Ο[,]Ο)(absβ(πβπ )) β€ ((absβ(π Β· (πΎβπ))) + 1))) |
115 | 114 | rspcev 3595 |
. . . . . 6
β’
((((absβ(π
Β· (πΎβπ))) + 1) β
β+ β§ βπ β (-Ο[,]Ο)(absβ(πβπ )) β€ ((absβ(π Β· (πΎβπ))) + 1)) β βπ β β+ βπ β
(-Ο[,]Ο)(absβ(πβπ )) β€ π) |
116 | 28, 112, 115 | syl2anc 584 |
. . . . 5
β’ (((π β§ π β β β§ βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π) β§ π β (-Ο[,]Ο) β§ βπ β
(-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ))) β βπ β β+ βπ β
(-Ο[,]Ο)(absβ(πβπ )) β€ π) |
117 | 116 | rexlimdv3a 3158 |
. . . 4
β’ ((π β§ π β β β§ βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π) β (βπ β (-Ο[,]Ο)βπ β
(-Ο[,]Ο)(absβ(πΎβπ )) β€ (absβ(πΎβπ)) β βπ β β+ βπ β
(-Ο[,]Ο)(absβ(πβπ )) β€ π)) |
118 | 17, 117 | mpd 15 |
. . 3
β’ ((π β§ π β β β§ βπ β
(-Ο[,]Ο)(absβ(π»βπ )) β€ π) β βπ β β+ βπ β
(-Ο[,]Ο)(absβ(πβπ )) β€ π) |
119 | 118 | rexlimdv3a 3158 |
. 2
β’ (π β (βπ β β βπ β (-Ο[,]Ο)(absβ(π»βπ )) β€ π β βπ β β+ βπ β
(-Ο[,]Ο)(absβ(πβπ )) β€ π)) |
120 | 1, 119 | mpd 15 |
1
β’ (π β βπ β β+ βπ β
(-Ο[,]Ο)(absβ(πβπ )) β€ π) |