Step | Hyp | Ref
| Expression |
1 | | fourierdlem19.a |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
2 | | fourierdlem19.x |
. . . . . 6
โข (๐ โ ๐ โ โ) |
3 | 1, 2 | readdcld 11242 |
. . . . 5
โข (๐ โ (๐ด + ๐) โ โ) |
4 | 3 | rexrd 11263 |
. . . 4
โข (๐ โ (๐ด + ๐) โ
โ*) |
5 | | fourierdlem19.b |
. . . . . 6
โข (๐ โ ๐ต โ โ) |
6 | 5, 2 | readdcld 11242 |
. . . . 5
โข (๐ โ (๐ต + ๐) โ โ) |
7 | 6 | rexrd 11263 |
. . . 4
โข (๐ โ (๐ต + ๐) โ
โ*) |
8 | | fourierdlem19.d |
. . . . . 6
โข ๐ท = {๐ฆ โ ((๐ด + ๐)(,](๐ต + ๐)) โฃ โ๐ โ โค (๐ฆ + (๐ ยท ๐)) โ ๐ถ} |
9 | | ssrab2 4077 |
. . . . . 6
โข {๐ฆ โ ((๐ด + ๐)(,](๐ต + ๐)) โฃ โ๐ โ โค (๐ฆ + (๐ ยท ๐)) โ ๐ถ} โ ((๐ด + ๐)(,](๐ต + ๐)) |
10 | 8, 9 | eqsstri 4016 |
. . . . 5
โข ๐ท โ ((๐ด + ๐)(,](๐ต + ๐)) |
11 | | fourierdlem19.z |
. . . . 5
โข (๐ โ ๐ โ ๐ท) |
12 | 10, 11 | sselid 3980 |
. . . 4
โข (๐ โ ๐ โ ((๐ด + ๐)(,](๐ต + ๐))) |
13 | | iocleub 44206 |
. . . 4
โข (((๐ด + ๐) โ โ* โง (๐ต + ๐) โ โ* โง ๐ โ ((๐ด + ๐)(,](๐ต + ๐))) โ ๐ โค (๐ต + ๐)) |
14 | 4, 7, 12, 13 | syl3anc 1371 |
. . 3
โข (๐ โ ๐ โค (๐ต + ๐)) |
15 | 14 | adantr 481 |
. 2
โข ((๐ โง ๐ < ๐) โ ๐ โค (๐ต + ๐)) |
16 | 6 | adantr 481 |
. . . 4
โข ((๐ โง ๐ < ๐) โ (๐ต + ๐) โ โ) |
17 | | iocssre 13403 |
. . . . . . . 8
โข (((๐ด + ๐) โ โ* โง (๐ต + ๐) โ โ) โ ((๐ด + ๐)(,](๐ต + ๐)) โ โ) |
18 | 4, 6, 17 | syl2anc 584 |
. . . . . . 7
โข (๐ โ ((๐ด + ๐)(,](๐ต + ๐)) โ โ) |
19 | | fourierdlem19.w |
. . . . . . . 8
โข (๐ โ ๐ โ ๐ท) |
20 | 10, 19 | sselid 3980 |
. . . . . . 7
โข (๐ โ ๐ โ ((๐ด + ๐)(,](๐ต + ๐))) |
21 | 18, 20 | sseldd 3983 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
22 | | fourierdlem19.t |
. . . . . . 7
โข ๐ = (๐ต โ ๐ด) |
23 | 5, 1 | resubcld 11641 |
. . . . . . 7
โข (๐ โ (๐ต โ ๐ด) โ โ) |
24 | 22, 23 | eqeltrid 2837 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
25 | 21, 24 | readdcld 11242 |
. . . . 5
โข (๐ โ (๐ + ๐) โ โ) |
26 | 25 | adantr 481 |
. . . 4
โข ((๐ โง ๐ < ๐) โ (๐ + ๐) โ โ) |
27 | 18, 12 | sseldd 3983 |
. . . . 5
โข (๐ โ ๐ โ โ) |
28 | 27 | adantr 481 |
. . . 4
โข ((๐ โง ๐ < ๐) โ ๐ โ โ) |
29 | 22 | eqcomi 2741 |
. . . . . . . . . . 11
โข (๐ต โ ๐ด) = ๐ |
30 | 29 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ (๐ต โ ๐ด) = ๐) |
31 | 5 | recnd 11241 |
. . . . . . . . . . 11
โข (๐ โ ๐ต โ โ) |
32 | 1 | recnd 11241 |
. . . . . . . . . . 11
โข (๐ โ ๐ด โ โ) |
33 | 24 | recnd 11241 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
34 | 31, 32, 33 | subaddd 11588 |
. . . . . . . . . 10
โข (๐ โ ((๐ต โ ๐ด) = ๐ โ (๐ด + ๐) = ๐ต)) |
35 | 30, 34 | mpbid 231 |
. . . . . . . . 9
โข (๐ โ (๐ด + ๐) = ๐ต) |
36 | 35 | eqcomd 2738 |
. . . . . . . 8
โข (๐ โ ๐ต = (๐ด + ๐)) |
37 | 36 | oveq1d 7423 |
. . . . . . 7
โข (๐ โ (๐ต + ๐) = ((๐ด + ๐) + ๐)) |
38 | 2 | recnd 11241 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
39 | 32, 33, 38 | add32d 11440 |
. . . . . . 7
โข (๐ โ ((๐ด + ๐) + ๐) = ((๐ด + ๐) + ๐)) |
40 | 37, 39 | eqtrd 2772 |
. . . . . 6
โข (๐ โ (๐ต + ๐) = ((๐ด + ๐) + ๐)) |
41 | | iocgtlb 44205 |
. . . . . . . 8
โข (((๐ด + ๐) โ โ* โง (๐ต + ๐) โ โ* โง ๐ โ ((๐ด + ๐)(,](๐ต + ๐))) โ (๐ด + ๐) < ๐) |
42 | 4, 7, 20, 41 | syl3anc 1371 |
. . . . . . 7
โข (๐ โ (๐ด + ๐) < ๐) |
43 | 3, 21, 24, 42 | ltadd1dd 11824 |
. . . . . 6
โข (๐ โ ((๐ด + ๐) + ๐) < (๐ + ๐)) |
44 | 40, 43 | eqbrtrd 5170 |
. . . . 5
โข (๐ โ (๐ต + ๐) < (๐ + ๐)) |
45 | 44 | adantr 481 |
. . . 4
โข ((๐ โง ๐ < ๐) โ (๐ต + ๐) < (๐ + ๐)) |
46 | | fourierdlem19.e |
. . . . . . . . . . . . 13
โข ๐ธ = (๐ฅ โ โ โฆ (๐ฅ + ((โโ((๐ต โ ๐ฅ) / ๐)) ยท ๐))) |
47 | 46 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ ๐ธ = (๐ฅ โ โ โฆ (๐ฅ + ((โโ((๐ต โ ๐ฅ) / ๐)) ยท ๐)))) |
48 | | id 22 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ โ ๐ฅ = ๐) |
49 | | oveq2 7416 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ = ๐ โ (๐ต โ ๐ฅ) = (๐ต โ ๐)) |
50 | 49 | oveq1d 7423 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = ๐ โ ((๐ต โ ๐ฅ) / ๐) = ((๐ต โ ๐) / ๐)) |
51 | 50 | fveq2d 6895 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ โ (โโ((๐ต โ ๐ฅ) / ๐)) = (โโ((๐ต โ ๐) / ๐))) |
52 | 51 | oveq1d 7423 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ โ ((โโ((๐ต โ ๐ฅ) / ๐)) ยท ๐) = ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) |
53 | 48, 52 | oveq12d 7426 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ โ (๐ฅ + ((โโ((๐ต โ ๐ฅ) / ๐)) ยท ๐)) = (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐))) |
54 | 53 | adantl 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ = ๐) โ (๐ฅ + ((โโ((๐ต โ ๐ฅ) / ๐)) ยท ๐)) = (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐))) |
55 | 5, 21 | resubcld 11641 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ต โ ๐) โ โ) |
56 | | fourierdlem19.altb |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐ด < ๐ต) |
57 | 1, 5 | posdifd 11800 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐ด < ๐ต โ 0 < (๐ต โ ๐ด))) |
58 | 56, 57 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ 0 < (๐ต โ ๐ด)) |
59 | 58, 22 | breqtrrdi 5190 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 0 < ๐) |
60 | 59 | gt0ne0d 11777 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ โ 0) |
61 | 55, 24, 60 | redivcld 12041 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ต โ ๐) / ๐) โ โ) |
62 | 61 | flcld 13762 |
. . . . . . . . . . . . . . 15
โข (๐ โ (โโ((๐ต โ ๐) / ๐)) โ โค) |
63 | 62 | zred 12665 |
. . . . . . . . . . . . . 14
โข (๐ โ (โโ((๐ต โ ๐) / ๐)) โ โ) |
64 | 63, 24 | remulcld 11243 |
. . . . . . . . . . . . 13
โข (๐ โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐) โ โ) |
65 | 21, 64 | readdcld 11242 |
. . . . . . . . . . . 12
โข (๐ โ (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) โ โ) |
66 | 47, 54, 21, 65 | fvmptd 7005 |
. . . . . . . . . . 11
โข (๐ โ (๐ธโ๐) = (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐))) |
67 | 66, 65 | eqeltrd 2833 |
. . . . . . . . . 10
โข (๐ โ (๐ธโ๐) โ โ) |
68 | 67 | recnd 11241 |
. . . . . . . . 9
โข (๐ โ (๐ธโ๐) โ โ) |
69 | 68 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ๐ < ๐) โ (๐ธโ๐) โ โ) |
70 | 64 | recnd 11241 |
. . . . . . . . 9
โข (๐ โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐) โ โ) |
71 | 70 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ๐ < ๐) โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐) โ โ) |
72 | 33 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ๐ < ๐) โ ๐ โ โ) |
73 | 69, 71, 72 | subsubd 11598 |
. . . . . . 7
โข ((๐ โง ๐ < ๐) โ ((๐ธโ๐) โ (((โโ((๐ต โ ๐) / ๐)) ยท ๐) โ ๐)) = (((๐ธโ๐) โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) + ๐)) |
74 | 73 | eqcomd 2738 |
. . . . . 6
โข ((๐ โง ๐ < ๐) โ (((๐ธโ๐) โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) + ๐) = ((๐ธโ๐) โ (((โโ((๐ต โ ๐) / ๐)) ยท ๐) โ ๐))) |
75 | 5, 27 | resubcld 11641 |
. . . . . . . . . . . 12
โข (๐ โ (๐ต โ ๐) โ โ) |
76 | 75, 24, 60 | redivcld 12041 |
. . . . . . . . . . 11
โข (๐ โ ((๐ต โ ๐) / ๐) โ โ) |
77 | 76 | flcld 13762 |
. . . . . . . . . 10
โข (๐ โ (โโ((๐ต โ ๐) / ๐)) โ โค) |
78 | 77 | zred 12665 |
. . . . . . . . 9
โข (๐ โ (โโ((๐ต โ ๐) / ๐)) โ โ) |
79 | 78 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ๐ < ๐) โ (โโ((๐ต โ ๐) / ๐)) โ โ) |
80 | 24 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ๐ < ๐) โ ๐ โ โ) |
81 | 79, 80 | remulcld 11243 |
. . . . . . 7
โข ((๐ โง ๐ < ๐) โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐) โ โ) |
82 | 63 | adantr 481 |
. . . . . . . . 9
โข ((๐ โง ๐ < ๐) โ (โโ((๐ต โ ๐) / ๐)) โ โ) |
83 | 82, 80 | remulcld 11243 |
. . . . . . . 8
โข ((๐ โง ๐ < ๐) โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐) โ โ) |
84 | 83, 80 | resubcld 11641 |
. . . . . . 7
โข ((๐ โง ๐ < ๐) โ (((โโ((๐ต โ ๐) / ๐)) ยท ๐) โ ๐) โ โ) |
85 | 67 | adantr 481 |
. . . . . . 7
โข ((๐ โง ๐ < ๐) โ (๐ธโ๐) โ โ) |
86 | 78, 24 | remulcld 11243 |
. . . . . . . . . . . 12
โข (๐ โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐) โ โ) |
87 | 86 | recnd 11241 |
. . . . . . . . . . 11
โข (๐ โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐) โ โ) |
88 | 87, 33 | pncand 11571 |
. . . . . . . . . 10
โข (๐ โ ((((โโ((๐ต โ ๐) / ๐)) ยท ๐) + ๐) โ ๐) = ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) |
89 | 88 | eqcomd 2738 |
. . . . . . . . 9
โข (๐ โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐) = ((((โโ((๐ต โ ๐) / ๐)) ยท ๐) + ๐) โ ๐)) |
90 | 89 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ๐ < ๐) โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐) = ((((โโ((๐ต โ ๐) / ๐)) ยท ๐) + ๐) โ ๐)) |
91 | 81, 80 | readdcld 11242 |
. . . . . . . . 9
โข ((๐ โง ๐ < ๐) โ (((โโ((๐ต โ ๐) / ๐)) ยท ๐) + ๐) โ โ) |
92 | 78 | recnd 11241 |
. . . . . . . . . . . . 13
โข (๐ โ (โโ((๐ต โ ๐) / ๐)) โ โ) |
93 | 92, 33 | adddirp1d 11239 |
. . . . . . . . . . . 12
โข (๐ โ (((โโ((๐ต โ ๐) / ๐)) + 1) ยท ๐) = (((โโ((๐ต โ ๐) / ๐)) ยท ๐) + ๐)) |
94 | 93 | eqcomd 2738 |
. . . . . . . . . . 11
โข (๐ โ (((โโ((๐ต โ ๐) / ๐)) ยท ๐) + ๐) = (((โโ((๐ต โ ๐) / ๐)) + 1) ยท ๐)) |
95 | 94 | adantr 481 |
. . . . . . . . . 10
โข ((๐ โง ๐ < ๐) โ (((โโ((๐ต โ ๐) / ๐)) ยท ๐) + ๐) = (((โโ((๐ต โ ๐) / ๐)) + 1) ยท ๐)) |
96 | | 1red 11214 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ < ๐) โ 1 โ โ) |
97 | 79, 96 | readdcld 11242 |
. . . . . . . . . . 11
โข ((๐ โง ๐ < ๐) โ ((โโ((๐ต โ ๐) / ๐)) + 1) โ โ) |
98 | | 0red 11216 |
. . . . . . . . . . . . 13
โข (๐ โ 0 โ
โ) |
99 | 98, 24, 59 | ltled 11361 |
. . . . . . . . . . . 12
โข (๐ โ 0 โค ๐) |
100 | 99 | adantr 481 |
. . . . . . . . . . 11
โข ((๐ โง ๐ < ๐) โ 0 โค ๐) |
101 | 85, 28 | resubcld 11641 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ < ๐) โ ((๐ธโ๐) โ ๐) โ โ) |
102 | 21 | adantr 481 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ < ๐) โ ๐ โ โ) |
103 | 85, 102 | resubcld 11641 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ < ๐) โ ((๐ธโ๐) โ ๐) โ โ) |
104 | 24, 59 | elrpd 13012 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ
โ+) |
105 | 104 | adantr 481 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ < ๐) โ ๐ โ
โ+) |
106 | | simpr 485 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ < ๐) โ ๐ < ๐) |
107 | 102, 28, 85, 106 | ltsub2dd 11826 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ < ๐) โ ((๐ธโ๐) โ ๐) < ((๐ธโ๐) โ ๐)) |
108 | 101, 103,
105, 107 | ltdiv1dd 13072 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ < ๐) โ (((๐ธโ๐) โ ๐) / ๐) < (((๐ธโ๐) โ ๐) / ๐)) |
109 | | fourierdlem19.ezew |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐ธโ๐) = (๐ธโ๐)) |
110 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ = ๐ โ ๐ฅ = ๐) |
111 | | oveq2 7416 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฅ = ๐ โ (๐ต โ ๐ฅ) = (๐ต โ ๐)) |
112 | 111 | oveq1d 7423 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฅ = ๐ โ ((๐ต โ ๐ฅ) / ๐) = ((๐ต โ ๐) / ๐)) |
113 | 112 | fveq2d 6895 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฅ = ๐ โ (โโ((๐ต โ ๐ฅ) / ๐)) = (โโ((๐ต โ ๐) / ๐))) |
114 | 113 | oveq1d 7423 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ = ๐ โ ((โโ((๐ต โ ๐ฅ) / ๐)) ยท ๐) = ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) |
115 | 110, 114 | oveq12d 7426 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฅ = ๐ โ (๐ฅ + ((โโ((๐ต โ ๐ฅ) / ๐)) ยท ๐)) = (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐))) |
116 | 115 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ฅ = ๐) โ (๐ฅ + ((โโ((๐ต โ ๐ฅ) / ๐)) ยท ๐)) = (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐))) |
117 | 27, 86 | readdcld 11242 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) โ โ) |
118 | 47, 116, 27, 117 | fvmptd 7005 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐ธโ๐) = (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐))) |
119 | 109, 118 | eqtr3d 2774 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐ธโ๐) = (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐))) |
120 | 119 | oveq1d 7423 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐ธโ๐) โ ๐) = ((๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) โ ๐)) |
121 | 27 | recnd 11241 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐ โ โ) |
122 | 121, 87 | pncan2d 11572 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) โ ๐) = ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) |
123 | 120, 122 | eqtrd 2772 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ธโ๐) โ ๐) = ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) |
124 | 123 | oveq1d 7423 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((๐ธโ๐) โ ๐) / ๐) = (((โโ((๐ต โ ๐) / ๐)) ยท ๐) / ๐)) |
125 | 92, 33, 60 | divcan4d 11995 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((โโ((๐ต โ ๐) / ๐)) ยท ๐) / ๐) = (โโ((๐ต โ ๐) / ๐))) |
126 | 124, 125 | eqtr2d 2773 |
. . . . . . . . . . . . . 14
โข (๐ โ (โโ((๐ต โ ๐) / ๐)) = (((๐ธโ๐) โ ๐) / ๐)) |
127 | 126 | adantr 481 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ < ๐) โ (โโ((๐ต โ ๐) / ๐)) = (((๐ธโ๐) โ ๐) / ๐)) |
128 | 66 | oveq1d 7423 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ธโ๐) โ ๐) = ((๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) โ ๐)) |
129 | 128 | oveq1d 7423 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((๐ธโ๐) โ ๐) / ๐) = (((๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) โ ๐) / ๐)) |
130 | 21 | recnd 11241 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ โ โ) |
131 | 130, 70 | pncan2d 11572 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) โ ๐) = ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) |
132 | 131 | oveq1d 7423 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) โ ๐) / ๐) = (((โโ((๐ต โ ๐) / ๐)) ยท ๐) / ๐)) |
133 | 63 | recnd 11241 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (โโ((๐ต โ ๐) / ๐)) โ โ) |
134 | 133, 33, 60 | divcan4d 11995 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((โโ((๐ต โ ๐) / ๐)) ยท ๐) / ๐) = (โโ((๐ต โ ๐) / ๐))) |
135 | 129, 132,
134 | 3eqtrrd 2777 |
. . . . . . . . . . . . . 14
โข (๐ โ (โโ((๐ต โ ๐) / ๐)) = (((๐ธโ๐) โ ๐) / ๐)) |
136 | 135 | adantr 481 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ < ๐) โ (โโ((๐ต โ ๐) / ๐)) = (((๐ธโ๐) โ ๐) / ๐)) |
137 | 108, 127,
136 | 3brtr4d 5180 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ < ๐) โ (โโ((๐ต โ ๐) / ๐)) < (โโ((๐ต โ ๐) / ๐))) |
138 | 77 | adantr 481 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ < ๐) โ (โโ((๐ต โ ๐) / ๐)) โ โค) |
139 | 62 | adantr 481 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ < ๐) โ (โโ((๐ต โ ๐) / ๐)) โ โค) |
140 | | zltp1le 12611 |
. . . . . . . . . . . . 13
โข
(((โโ((๐ต
โ ๐) / ๐)) โ โค โง
(โโ((๐ต โ
๐) / ๐)) โ โค) โ
((โโ((๐ต โ
๐) / ๐)) < (โโ((๐ต โ ๐) / ๐)) โ ((โโ((๐ต โ ๐) / ๐)) + 1) โค (โโ((๐ต โ ๐) / ๐)))) |
141 | 138, 139,
140 | syl2anc 584 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ < ๐) โ ((โโ((๐ต โ ๐) / ๐)) < (โโ((๐ต โ ๐) / ๐)) โ ((โโ((๐ต โ ๐) / ๐)) + 1) โค (โโ((๐ต โ ๐) / ๐)))) |
142 | 137, 141 | mpbid 231 |
. . . . . . . . . . 11
โข ((๐ โง ๐ < ๐) โ ((โโ((๐ต โ ๐) / ๐)) + 1) โค (โโ((๐ต โ ๐) / ๐))) |
143 | 97, 82, 80, 100, 142 | lemul1ad 12152 |
. . . . . . . . . 10
โข ((๐ โง ๐ < ๐) โ (((โโ((๐ต โ ๐) / ๐)) + 1) ยท ๐) โค ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) |
144 | 95, 143 | eqbrtrd 5170 |
. . . . . . . . 9
โข ((๐ โง ๐ < ๐) โ (((โโ((๐ต โ ๐) / ๐)) ยท ๐) + ๐) โค ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) |
145 | 91, 83, 80, 144 | lesub1dd 11829 |
. . . . . . . 8
โข ((๐ โง ๐ < ๐) โ ((((โโ((๐ต โ ๐) / ๐)) ยท ๐) + ๐) โ ๐) โค (((โโ((๐ต โ ๐) / ๐)) ยท ๐) โ ๐)) |
146 | 90, 145 | eqbrtrd 5170 |
. . . . . . 7
โข ((๐ โง ๐ < ๐) โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐) โค (((โโ((๐ต โ ๐) / ๐)) ยท ๐) โ ๐)) |
147 | 81, 84, 85, 146 | lesub2dd 11830 |
. . . . . 6
โข ((๐ โง ๐ < ๐) โ ((๐ธโ๐) โ (((โโ((๐ต โ ๐) / ๐)) ยท ๐) โ ๐)) โค ((๐ธโ๐) โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐))) |
148 | 74, 147 | eqbrtrd 5170 |
. . . . 5
โข ((๐ โง ๐ < ๐) โ (((๐ธโ๐) โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) + ๐) โค ((๐ธโ๐) โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐))) |
149 | 66 | eqcomd 2738 |
. . . . . . . . 9
โข (๐ โ (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) = (๐ธโ๐)) |
150 | 68, 70, 130 | subadd2d 11589 |
. . . . . . . . 9
โข (๐ โ (((๐ธโ๐) โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) = ๐ โ (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) = (๐ธโ๐))) |
151 | 149, 150 | mpbird 256 |
. . . . . . . 8
โข (๐ โ ((๐ธโ๐) โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) = ๐) |
152 | 151 | eqcomd 2738 |
. . . . . . 7
โข (๐ โ ๐ = ((๐ธโ๐) โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐))) |
153 | 152 | oveq1d 7423 |
. . . . . 6
โข (๐ โ (๐ + ๐) = (((๐ธโ๐) โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) + ๐)) |
154 | 153 | adantr 481 |
. . . . 5
โข ((๐ โง ๐ < ๐) โ (๐ + ๐) = (((๐ธโ๐) โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) + ๐)) |
155 | 118 | eqcomd 2738 |
. . . . . . . 8
โข (๐ โ (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) = (๐ธโ๐)) |
156 | 1 | rexrd 11263 |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ
โ*) |
157 | | iocssre 13403 |
. . . . . . . . . . . 12
โข ((๐ด โ โ*
โง ๐ต โ โ)
โ (๐ด(,]๐ต) โ
โ) |
158 | 156, 5, 157 | syl2anc 584 |
. . . . . . . . . . 11
โข (๐ โ (๐ด(,]๐ต) โ โ) |
159 | 1, 5, 56, 22, 46 | fourierdlem4 44817 |
. . . . . . . . . . . 12
โข (๐ โ ๐ธ:โโถ(๐ด(,]๐ต)) |
160 | 159, 27 | ffvelcdmd 7087 |
. . . . . . . . . . 11
โข (๐ โ (๐ธโ๐) โ (๐ด(,]๐ต)) |
161 | 158, 160 | sseldd 3983 |
. . . . . . . . . 10
โข (๐ โ (๐ธโ๐) โ โ) |
162 | 161 | recnd 11241 |
. . . . . . . . 9
โข (๐ โ (๐ธโ๐) โ โ) |
163 | 162, 87, 121 | subadd2d 11589 |
. . . . . . . 8
โข (๐ โ (((๐ธโ๐) โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) = ๐ โ (๐ + ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) = (๐ธโ๐))) |
164 | 155, 163 | mpbird 256 |
. . . . . . 7
โข (๐ โ ((๐ธโ๐) โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) = ๐) |
165 | 109 | oveq1d 7423 |
. . . . . . 7
โข (๐ โ ((๐ธโ๐) โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐)) = ((๐ธโ๐) โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐))) |
166 | 164, 165 | eqtr3d 2774 |
. . . . . 6
โข (๐ โ ๐ = ((๐ธโ๐) โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐))) |
167 | 166 | adantr 481 |
. . . . 5
โข ((๐ โง ๐ < ๐) โ ๐ = ((๐ธโ๐) โ ((โโ((๐ต โ ๐) / ๐)) ยท ๐))) |
168 | 148, 154,
167 | 3brtr4d 5180 |
. . . 4
โข ((๐ โง ๐ < ๐) โ (๐ + ๐) โค ๐) |
169 | 16, 26, 28, 45, 168 | ltletrd 11373 |
. . 3
โข ((๐ โง ๐ < ๐) โ (๐ต + ๐) < ๐) |
170 | 16, 28 | ltnled 11360 |
. . 3
โข ((๐ โง ๐ < ๐) โ ((๐ต + ๐) < ๐ โ ยฌ ๐ โค (๐ต + ๐))) |
171 | 169, 170 | mpbid 231 |
. 2
โข ((๐ โง ๐ < ๐) โ ยฌ ๐ โค (๐ต + ๐)) |
172 | 15, 171 | pm2.65da 815 |
1
โข (๐ โ ยฌ ๐ < ๐) |