Step | Hyp | Ref
| Expression |
1 | | fourierdlem40.h |
. . . . 5
β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) |
2 | 1 | reseq1i 5934 |
. . . 4
β’ (π» βΎ (π΄(,)π΅)) = ((π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) βΎ (π΄(,)π΅)) |
3 | 2 | a1i 11 |
. . 3
β’ (π β (π» βΎ (π΄(,)π΅)) = ((π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) βΎ (π΄(,)π΅))) |
4 | | pire 25831 |
. . . . . . . . 9
β’ Ο
β β |
5 | 4 | renegcli 11467 |
. . . . . . . 8
β’ -Ο
β β |
6 | 5 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β (π΄(,)π΅)) β -Ο β
β) |
7 | 4 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β (π΄(,)π΅)) β Ο β
β) |
8 | | elioore 13300 |
. . . . . . . 8
β’ (π β (π΄(,)π΅) β π β β) |
9 | 8 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β (π΄(,)π΅)) β π β β) |
10 | 5 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β -Ο β
β) |
11 | 4 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β Ο β
β) |
12 | 10, 11 | iccssred 13357 |
. . . . . . . . . . 11
β’ (π β (-Ο[,]Ο) β
β) |
13 | | fourierdlem40.a |
. . . . . . . . . . 11
β’ (π β π΄ β (-Ο[,]Ο)) |
14 | 12, 13 | sseldd 3946 |
. . . . . . . . . 10
β’ (π β π΄ β β) |
15 | 14 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β π΄ β β) |
16 | 5, 4 | elicc2i 13336 |
. . . . . . . . . . . 12
β’ (π΄ β (-Ο[,]Ο) β
(π΄ β β β§
-Ο β€ π΄ β§ π΄ β€ Ο)) |
17 | 16 | simp2bi 1147 |
. . . . . . . . . . 11
β’ (π΄ β (-Ο[,]Ο) β
-Ο β€ π΄) |
18 | 13, 17 | syl 17 |
. . . . . . . . . 10
β’ (π β -Ο β€ π΄) |
19 | 18 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β -Ο β€ π΄) |
20 | 15 | rexrd 11210 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β π΄ β
β*) |
21 | | fourierdlem40.b |
. . . . . . . . . . . . 13
β’ (π β π΅ β (-Ο[,]Ο)) |
22 | 12, 21 | sseldd 3946 |
. . . . . . . . . . . 12
β’ (π β π΅ β β) |
23 | 22 | rexrd 11210 |
. . . . . . . . . . 11
β’ (π β π΅ β
β*) |
24 | 23 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β π΅ β
β*) |
25 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β π β (π΄(,)π΅)) |
26 | | ioogtlb 43819 |
. . . . . . . . . 10
β’ ((π΄ β β*
β§ π΅ β
β* β§ π
β (π΄(,)π΅)) β π΄ < π ) |
27 | 20, 24, 25, 26 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β π΄ < π ) |
28 | 6, 15, 9, 19, 27 | lelttrd 11318 |
. . . . . . . 8
β’ ((π β§ π β (π΄(,)π΅)) β -Ο < π ) |
29 | 6, 9, 28 | ltled 11308 |
. . . . . . 7
β’ ((π β§ π β (π΄(,)π΅)) β -Ο β€ π ) |
30 | 22 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β π΅ β β) |
31 | | iooltub 43834 |
. . . . . . . . . 10
β’ ((π΄ β β*
β§ π΅ β
β* β§ π
β (π΄(,)π΅)) β π < π΅) |
32 | 20, 24, 25, 31 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β π < π΅) |
33 | 5, 4 | elicc2i 13336 |
. . . . . . . . . . . 12
β’ (π΅ β (-Ο[,]Ο) β
(π΅ β β β§
-Ο β€ π΅ β§ π΅ β€ Ο)) |
34 | 33 | simp3bi 1148 |
. . . . . . . . . . 11
β’ (π΅ β (-Ο[,]Ο) β
π΅ β€
Ο) |
35 | 21, 34 | syl 17 |
. . . . . . . . . 10
β’ (π β π΅ β€ Ο) |
36 | 35 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β π΅ β€ Ο) |
37 | 9, 30, 7, 32, 36 | ltletrd 11320 |
. . . . . . . 8
β’ ((π β§ π β (π΄(,)π΅)) β π < Ο) |
38 | 9, 7, 37 | ltled 11308 |
. . . . . . 7
β’ ((π β§ π β (π΄(,)π΅)) β π β€ Ο) |
39 | 6, 7, 9, 29, 38 | eliccd 43828 |
. . . . . 6
β’ ((π β§ π β (π΄(,)π΅)) β π β (-Ο[,]Ο)) |
40 | 39 | ex 414 |
. . . . 5
β’ (π β (π β (π΄(,)π΅) β π β (-Ο[,]Ο))) |
41 | 40 | ssrdv 3951 |
. . . 4
β’ (π β (π΄(,)π΅) β (-Ο[,]Ο)) |
42 | 41 | resmptd 5995 |
. . 3
β’ (π β ((π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) βΎ (π΄(,)π΅)) = (π β (π΄(,)π΅) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π )))) |
43 | | eleq1 2822 |
. . . . . . . . 9
β’ (π = 0 β (π β (π΄(,)π΅) β 0 β (π΄(,)π΅))) |
44 | 43 | biimpac 480 |
. . . . . . . 8
β’ ((π β (π΄(,)π΅) β§ π = 0) β 0 β (π΄(,)π΅)) |
45 | 44 | adantll 713 |
. . . . . . 7
β’ (((π β§ π β (π΄(,)π΅)) β§ π = 0) β 0 β (π΄(,)π΅)) |
46 | | fourierdlem40.nxelab |
. . . . . . . 8
β’ (π β Β¬ 0 β (π΄(,)π΅)) |
47 | 46 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β (π΄(,)π΅)) β§ π = 0) β Β¬ 0 β (π΄(,)π΅)) |
48 | 45, 47 | pm2.65da 816 |
. . . . . 6
β’ ((π β§ π β (π΄(,)π΅)) β Β¬ π = 0) |
49 | 48 | iffalsed 4498 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π )) = (((πΉβ(π + π )) β if(0 < π , π, π)) / π )) |
50 | | fourierdlem40.f |
. . . . . . . . . 10
β’ (π β πΉ:ββΆβ) |
51 | 50 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β πΉ:ββΆβ) |
52 | | fourierdlem40.x |
. . . . . . . . . . 11
β’ (π β π β β) |
53 | 52 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β π β β) |
54 | 53, 9 | readdcld 11189 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β (π + π ) β β) |
55 | 51, 54 | ffvelcdmd 7037 |
. . . . . . . 8
β’ ((π β§ π β (π΄(,)π΅)) β (πΉβ(π + π )) β β) |
56 | | fourierdlem40.y |
. . . . . . . . . 10
β’ (π β π β β) |
57 | | fourierdlem40.w |
. . . . . . . . . 10
β’ (π β π β β) |
58 | 56, 57 | ifcld 4533 |
. . . . . . . . 9
β’ (π β if(0 < π , π, π) β β) |
59 | 58 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (π΄(,)π΅)) β if(0 < π , π, π) β β) |
60 | 55, 59 | resubcld 11588 |
. . . . . . 7
β’ ((π β§ π β (π΄(,)π΅)) β ((πΉβ(π + π )) β if(0 < π , π, π)) β β) |
61 | 60 | recnd 11188 |
. . . . . 6
β’ ((π β§ π β (π΄(,)π΅)) β ((πΉβ(π + π )) β if(0 < π , π, π)) β β) |
62 | 9 | recnd 11188 |
. . . . . 6
β’ ((π β§ π β (π΄(,)π΅)) β π β β) |
63 | 48 | neqned 2947 |
. . . . . 6
β’ ((π β§ π β (π΄(,)π΅)) β π β 0) |
64 | 61, 62, 63 | divrecd 11939 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β (((πΉβ(π + π )) β if(0 < π , π, π)) / π ) = (((πΉβ(π + π )) β if(0 < π , π, π)) Β· (1 / π ))) |
65 | 49, 64 | eqtrd 2773 |
. . . 4
β’ ((π β§ π β (π΄(,)π΅)) β if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π )) = (((πΉβ(π + π )) β if(0 < π , π, π)) Β· (1 / π ))) |
66 | 65 | mpteq2dva 5206 |
. . 3
β’ (π β (π β (π΄(,)π΅) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) = (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β if(0 < π , π, π)) Β· (1 / π )))) |
67 | 3, 42, 66 | 3eqtrd 2777 |
. 2
β’ (π β (π» βΎ (π΄(,)π΅)) = (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β if(0 < π , π, π)) Β· (1 / π )))) |
68 | 55 | recnd 11188 |
. . . . . . 7
β’ ((π β§ π β (π΄(,)π΅)) β (πΉβ(π + π )) β β) |
69 | 59 | recnd 11188 |
. . . . . . 7
β’ ((π β§ π β (π΄(,)π΅)) β if(0 < π , π, π) β β) |
70 | 68, 69 | negsubd 11523 |
. . . . . 6
β’ ((π β§ π β (π΄(,)π΅)) β ((πΉβ(π + π )) + -if(0 < π , π, π)) = ((πΉβ(π + π )) β if(0 < π , π, π))) |
71 | 70 | eqcomd 2739 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β ((πΉβ(π + π )) β if(0 < π , π, π)) = ((πΉβ(π + π )) + -if(0 < π , π, π))) |
72 | 71 | mpteq2dva 5206 |
. . . 4
β’ (π β (π β (π΄(,)π΅) β¦ ((πΉβ(π + π )) β if(0 < π , π, π))) = (π β (π΄(,)π΅) β¦ ((πΉβ(π + π )) + -if(0 < π , π, π)))) |
73 | 14, 52 | readdcld 11189 |
. . . . . . . . . . . 12
β’ (π β (π΄ + π) β β) |
74 | 73 | rexrd 11210 |
. . . . . . . . . . 11
β’ (π β (π΄ + π) β
β*) |
75 | 74 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β (π΄ + π) β
β*) |
76 | 22, 52 | readdcld 11189 |
. . . . . . . . . . . 12
β’ (π β (π΅ + π) β β) |
77 | 76 | rexrd 11210 |
. . . . . . . . . . 11
β’ (π β (π΅ + π) β
β*) |
78 | 77 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β (π΅ + π) β
β*) |
79 | 14 | recnd 11188 |
. . . . . . . . . . . . 13
β’ (π β π΄ β β) |
80 | 52 | recnd 11188 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
81 | 79, 80 | addcomd 11362 |
. . . . . . . . . . . 12
β’ (π β (π΄ + π) = (π + π΄)) |
82 | 81 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄(,)π΅)) β (π΄ + π) = (π + π΄)) |
83 | 15, 9, 53, 27 | ltadd2dd 11319 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄(,)π΅)) β (π + π΄) < (π + π )) |
84 | 82, 83 | eqbrtrd 5128 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β (π΄ + π) < (π + π )) |
85 | 9, 30, 53, 32 | ltadd2dd 11319 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄(,)π΅)) β (π + π ) < (π + π΅)) |
86 | 22 | recnd 11188 |
. . . . . . . . . . . . 13
β’ (π β π΅ β β) |
87 | 80, 86 | addcomd 11362 |
. . . . . . . . . . . 12
β’ (π β (π + π΅) = (π΅ + π)) |
88 | 87 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄(,)π΅)) β (π + π΅) = (π΅ + π)) |
89 | 85, 88 | breqtrd 5132 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄(,)π΅)) β (π + π ) < (π΅ + π)) |
90 | 75, 78, 54, 84, 89 | eliood 43822 |
. . . . . . . . 9
β’ ((π β§ π β (π΄(,)π΅)) β (π + π ) β ((π΄ + π)(,)(π΅ + π))) |
91 | | fvres 6862 |
. . . . . . . . 9
β’ ((π + π ) β ((π΄ + π)(,)(π΅ + π)) β ((πΉ βΎ ((π΄ + π)(,)(π΅ + π)))β(π + π )) = (πΉβ(π + π ))) |
92 | 90, 91 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β (π΄(,)π΅)) β ((πΉ βΎ ((π΄ + π)(,)(π΅ + π)))β(π + π )) = (πΉβ(π + π ))) |
93 | 92 | eqcomd 2739 |
. . . . . . 7
β’ ((π β§ π β (π΄(,)π΅)) β (πΉβ(π + π )) = ((πΉ βΎ ((π΄ + π)(,)(π΅ + π)))β(π + π ))) |
94 | 93 | mpteq2dva 5206 |
. . . . . 6
β’ (π β (π β (π΄(,)π΅) β¦ (πΉβ(π + π ))) = (π β (π΄(,)π΅) β¦ ((πΉ βΎ ((π΄ + π)(,)(π΅ + π)))β(π + π )))) |
95 | | ioosscn 13332 |
. . . . . . . 8
β’ ((π΄ + π)(,)(π΅ + π)) β β |
96 | 95 | a1i 11 |
. . . . . . 7
β’ (π β ((π΄ + π)(,)(π΅ + π)) β β) |
97 | | fourierdlem40.fcn |
. . . . . . 7
β’ (π β (πΉ βΎ ((π΄ + π)(,)(π΅ + π))) β (((π΄ + π)(,)(π΅ + π))βcnββ)) |
98 | | ioosscn 13332 |
. . . . . . . 8
β’ (π΄(,)π΅) β β |
99 | 98 | a1i 11 |
. . . . . . 7
β’ (π β (π΄(,)π΅) β β) |
100 | 96, 97, 99, 80, 90 | fourierdlem23 44457 |
. . . . . 6
β’ (π β (π β (π΄(,)π΅) β¦ ((πΉ βΎ ((π΄ + π)(,)(π΅ + π)))β(π + π ))) β ((π΄(,)π΅)βcnββ)) |
101 | 94, 100 | eqeltrd 2834 |
. . . . 5
β’ (π β (π β (π΄(,)π΅) β¦ (πΉβ(π + π ))) β ((π΄(,)π΅)βcnββ)) |
102 | | 0red 11163 |
. . . . . . . . . . 11
β’ (((π β§ 0 β€ π΄) β§ π β (π΄(,)π΅)) β 0 β β) |
103 | 14 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ 0 β€ π΄) β§ π β (π΄(,)π΅)) β π΄ β β) |
104 | 8 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ 0 β€ π΄) β§ π β (π΄(,)π΅)) β π β β) |
105 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ 0 β€ π΄) β§ π β (π΄(,)π΅)) β 0 β€ π΄) |
106 | 27 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ 0 β€ π΄) β§ π β (π΄(,)π΅)) β π΄ < π ) |
107 | 102, 103,
104, 105, 106 | lelttrd 11318 |
. . . . . . . . . 10
β’ (((π β§ 0 β€ π΄) β§ π β (π΄(,)π΅)) β 0 < π ) |
108 | 107 | iftrued 4495 |
. . . . . . . . 9
β’ (((π β§ 0 β€ π΄) β§ π β (π΄(,)π΅)) β if(0 < π , π, π) = π) |
109 | 108 | negeqd 11400 |
. . . . . . . 8
β’ (((π β§ 0 β€ π΄) β§ π β (π΄(,)π΅)) β -if(0 < π , π, π) = -π) |
110 | 109 | mpteq2dva 5206 |
. . . . . . 7
β’ ((π β§ 0 β€ π΄) β (π β (π΄(,)π΅) β¦ -if(0 < π , π, π)) = (π β (π΄(,)π΅) β¦ -π)) |
111 | 56 | renegcld 11587 |
. . . . . . . . . 10
β’ (π β -π β β) |
112 | 111 | recnd 11188 |
. . . . . . . . 9
β’ (π β -π β β) |
113 | | ssid 3967 |
. . . . . . . . . 10
β’ β
β β |
114 | 113 | a1i 11 |
. . . . . . . . 9
β’ (π β β β
β) |
115 | 99, 112, 114 | constcncfg 44199 |
. . . . . . . 8
β’ (π β (π β (π΄(,)π΅) β¦ -π) β ((π΄(,)π΅)βcnββ)) |
116 | 115 | adantr 482 |
. . . . . . 7
β’ ((π β§ 0 β€ π΄) β (π β (π΄(,)π΅) β¦ -π) β ((π΄(,)π΅)βcnββ)) |
117 | 110, 116 | eqeltrd 2834 |
. . . . . 6
β’ ((π β§ 0 β€ π΄) β (π β (π΄(,)π΅) β¦ -if(0 < π , π, π)) β ((π΄(,)π΅)βcnββ)) |
118 | 14 | rexrd 11210 |
. . . . . . . . . 10
β’ (π β π΄ β
β*) |
119 | 118 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ Β¬ 0 β€ π΄) β§ Β¬ π΅ β€ 0) β π΄ β
β*) |
120 | 23 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ Β¬ 0 β€ π΄) β§ Β¬ π΅ β€ 0) β π΅ β
β*) |
121 | | 0red 11163 |
. . . . . . . . 9
β’ (((π β§ Β¬ 0 β€ π΄) β§ Β¬ π΅ β€ 0) β 0 β
β) |
122 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ 0 β€ π΄) β Β¬ 0 β€ π΄) |
123 | 14 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ 0 β€ π΄) β π΄ β β) |
124 | | 0red 11163 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ 0 β€ π΄) β 0 β
β) |
125 | 123, 124 | ltnled 11307 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ 0 β€ π΄) β (π΄ < 0 β Β¬ 0 β€ π΄)) |
126 | 122, 125 | mpbird 257 |
. . . . . . . . . 10
β’ ((π β§ Β¬ 0 β€ π΄) β π΄ < 0) |
127 | 126 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ Β¬ 0 β€ π΄) β§ Β¬ π΅ β€ 0) β π΄ < 0) |
128 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ π΅ β€ 0) β Β¬ π΅ β€ 0) |
129 | | 0red 11163 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ π΅ β€ 0) β 0 β
β) |
130 | 22 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ π΅ β€ 0) β π΅ β β) |
131 | 129, 130 | ltnled 11307 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ π΅ β€ 0) β (0 < π΅ β Β¬ π΅ β€ 0)) |
132 | 128, 131 | mpbird 257 |
. . . . . . . . . 10
β’ ((π β§ Β¬ π΅ β€ 0) β 0 < π΅) |
133 | 132 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ Β¬ 0 β€ π΄) β§ Β¬ π΅ β€ 0) β 0 < π΅) |
134 | 119, 120,
121, 127, 133 | eliood 43822 |
. . . . . . . 8
β’ (((π β§ Β¬ 0 β€ π΄) β§ Β¬ π΅ β€ 0) β 0 β (π΄(,)π΅)) |
135 | 46 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ Β¬ 0 β€ π΄) β§ Β¬ π΅ β€ 0) β Β¬ 0 β (π΄(,)π΅)) |
136 | 134, 135 | condan 817 |
. . . . . . 7
β’ ((π β§ Β¬ 0 β€ π΄) β π΅ β€ 0) |
137 | 8 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ π΅ β€ 0) β§ π β (π΄(,)π΅)) β π β β) |
138 | | 0red 11163 |
. . . . . . . . . . . 12
β’ (((π β§ π΅ β€ 0) β§ π β (π΄(,)π΅)) β 0 β β) |
139 | 22 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π΅ β€ 0) β§ π β (π΄(,)π΅)) β π΅ β β) |
140 | 32 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ π΅ β€ 0) β§ π β (π΄(,)π΅)) β π < π΅) |
141 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π β§ π΅ β€ 0) β§ π β (π΄(,)π΅)) β π΅ β€ 0) |
142 | 137, 139,
138, 140, 141 | ltletrd 11320 |
. . . . . . . . . . . 12
β’ (((π β§ π΅ β€ 0) β§ π β (π΄(,)π΅)) β π < 0) |
143 | 137, 138,
142 | ltnsymd 11309 |
. . . . . . . . . . 11
β’ (((π β§ π΅ β€ 0) β§ π β (π΄(,)π΅)) β Β¬ 0 < π ) |
144 | 143 | iffalsed 4498 |
. . . . . . . . . 10
β’ (((π β§ π΅ β€ 0) β§ π β (π΄(,)π΅)) β if(0 < π , π, π) = π) |
145 | 144 | negeqd 11400 |
. . . . . . . . 9
β’ (((π β§ π΅ β€ 0) β§ π β (π΄(,)π΅)) β -if(0 < π , π, π) = -π) |
146 | 145 | mpteq2dva 5206 |
. . . . . . . 8
β’ ((π β§ π΅ β€ 0) β (π β (π΄(,)π΅) β¦ -if(0 < π , π, π)) = (π β (π΄(,)π΅) β¦ -π)) |
147 | 57 | recnd 11188 |
. . . . . . . . . . 11
β’ (π β π β β) |
148 | 147 | negcld 11504 |
. . . . . . . . . 10
β’ (π β -π β β) |
149 | 99, 148, 114 | constcncfg 44199 |
. . . . . . . . 9
β’ (π β (π β (π΄(,)π΅) β¦ -π) β ((π΄(,)π΅)βcnββ)) |
150 | 149 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π΅ β€ 0) β (π β (π΄(,)π΅) β¦ -π) β ((π΄(,)π΅)βcnββ)) |
151 | 146, 150 | eqeltrd 2834 |
. . . . . . 7
β’ ((π β§ π΅ β€ 0) β (π β (π΄(,)π΅) β¦ -if(0 < π , π, π)) β ((π΄(,)π΅)βcnββ)) |
152 | 136, 151 | syldan 592 |
. . . . . 6
β’ ((π β§ Β¬ 0 β€ π΄) β (π β (π΄(,)π΅) β¦ -if(0 < π , π, π)) β ((π΄(,)π΅)βcnββ)) |
153 | 117, 152 | pm2.61dan 812 |
. . . . 5
β’ (π β (π β (π΄(,)π΅) β¦ -if(0 < π , π, π)) β ((π΄(,)π΅)βcnββ)) |
154 | 101, 153 | addcncf 24824 |
. . . 4
β’ (π β (π β (π΄(,)π΅) β¦ ((πΉβ(π + π )) + -if(0 < π , π, π))) β ((π΄(,)π΅)βcnββ)) |
155 | 72, 154 | eqeltrd 2834 |
. . 3
β’ (π β (π β (π΄(,)π΅) β¦ ((πΉβ(π + π )) β if(0 < π , π, π))) β ((π΄(,)π΅)βcnββ)) |
156 | | eqid 2733 |
. . . 4
β’ (π β (β β {0})
β¦ (1 / π )) = (π β (β β {0})
β¦ (1 / π )) |
157 | | 1cnd 11155 |
. . . . 5
β’ (π β 1 β
β) |
158 | 156 | cdivcncf 24300 |
. . . . 5
β’ (1 β
β β (π β
(β β {0}) β¦ (1 / π )) β ((β β {0})βcnββ)) |
159 | 157, 158 | syl 17 |
. . . 4
β’ (π β (π β (β β {0}) β¦ (1 /
π )) β ((β
β {0})βcnββ)) |
160 | | velsn 4603 |
. . . . . . . 8
β’ (π β {0} β π = 0) |
161 | 48, 160 | sylnibr 329 |
. . . . . . 7
β’ ((π β§ π β (π΄(,)π΅)) β Β¬ π β {0}) |
162 | 62, 161 | eldifd 3922 |
. . . . . 6
β’ ((π β§ π β (π΄(,)π΅)) β π β (β β
{0})) |
163 | 162 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ β (π΄(,)π΅)π β (β β
{0})) |
164 | | dfss3 3933 |
. . . . 5
β’ ((π΄(,)π΅) β (β β {0}) β
βπ β (π΄(,)π΅)π β (β β
{0})) |
165 | 163, 164 | sylibr 233 |
. . . 4
β’ (π β (π΄(,)π΅) β (β β
{0})) |
166 | 9, 63 | rereccld 11987 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β (1 / π ) β β) |
167 | 166 | recnd 11188 |
. . . 4
β’ ((π β§ π β (π΄(,)π΅)) β (1 / π ) β β) |
168 | 156, 159,
165, 114, 167 | cncfmptssg 44198 |
. . 3
β’ (π β (π β (π΄(,)π΅) β¦ (1 / π )) β ((π΄(,)π΅)βcnββ)) |
169 | 155, 168 | mulcncf 24826 |
. 2
β’ (π β (π β (π΄(,)π΅) β¦ (((πΉβ(π + π )) β if(0 < π , π, π)) Β· (1 / π ))) β ((π΄(,)π΅)βcnββ)) |
170 | 67, 169 | eqeltrd 2834 |
1
β’ (π β (π» βΎ (π΄(,)π΅)) β ((π΄(,)π΅)βcnββ)) |