Step | Hyp | Ref
| Expression |
1 | | hgt749d.1 |
. 2
โข (๐ โ (;10โ;27) โค ๐) |
2 | | breq2 5153 |
. . . 4
โข (๐ = ๐ โ ((;10โ;27) โค ๐ โ (;10โ;27) โค ๐)) |
3 | | oveq1 7416 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐โ2) = (๐โ2)) |
4 | 3 | oveq2d 7425 |
. . . . . . . 8
โข (๐ = ๐ โ ((0._0_0_0_4_2_2_48)
ยท (๐โ2)) =
((0._0_0_0_4_2_2_48)
ยท (๐โ2))) |
5 | | oveq2 7417 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ ((ฮ โf
ยท โ)vts๐) = ((ฮ
โf ยท โ)vts๐)) |
6 | 5 | fveq1d 6894 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (((ฮ โf
ยท โ)vts๐)โ๐ฅ) = (((ฮ โf ยท
โ)vts๐)โ๐ฅ)) |
7 | | oveq2 7417 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ ((ฮ โf
ยท ๐)vts๐) = ((ฮ
โf ยท ๐)vts๐)) |
8 | 7 | fveq1d 6894 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (((ฮ โf
ยท ๐)vts๐)โ๐ฅ) = (((ฮ โf ยท
๐)vts๐)โ๐ฅ)) |
9 | 8 | oveq1d 7424 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2) = ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) |
10 | 6, 9 | oveq12d 7427 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((((ฮ โf
ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) = ((((ฮ โf
ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2))) |
11 | | negeq 11452 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ -๐ = -๐) |
12 | 11 | oveq1d 7424 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (-๐ ยท ๐ฅ) = (-๐ ยท ๐ฅ)) |
13 | 12 | oveq2d 7425 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((i ยท (2 ยท ฯ))
ยท (-๐ ยท ๐ฅ)) = ((i ยท (2 ยท
ฯ)) ยท (-๐
ยท ๐ฅ))) |
14 | 13 | fveq2d 6896 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (expโ((i ยท (2 ยท
ฯ)) ยท (-๐
ยท ๐ฅ))) =
(expโ((i ยท (2 ยท ฯ)) ยท (-๐ ยท ๐ฅ)))) |
15 | 10, 14 | oveq12d 7427 |
. . . . . . . . . 10
โข (๐ = ๐ โ (((((ฮ โf
ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) ยท (expโ((i ยท
(2 ยท ฯ)) ยท (-๐ ยท ๐ฅ)))) = (((((ฮ โf
ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) ยท (expโ((i ยท
(2 ยท ฯ)) ยท (-๐ ยท ๐ฅ))))) |
16 | 15 | adantr 482 |
. . . . . . . . 9
โข ((๐ = ๐ โง ๐ฅ โ (0(,)1)) โ (((((ฮ
โf ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) ยท (expโ((i ยท
(2 ยท ฯ)) ยท (-๐ ยท ๐ฅ)))) = (((((ฮ โf
ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) ยท (expโ((i ยท
(2 ยท ฯ)) ยท (-๐ ยท ๐ฅ))))) |
17 | 16 | itgeq2dv 25299 |
. . . . . . . 8
โข (๐ = ๐ โ โซ(0(,)1)(((((ฮ
โf ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) ยท (expโ((i ยท
(2 ยท ฯ)) ยท (-๐ ยท ๐ฅ)))) d๐ฅ = โซ(0(,)1)(((((ฮ
โf ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) ยท (expโ((i ยท
(2 ยท ฯ)) ยท (-๐ ยท ๐ฅ)))) d๐ฅ) |
18 | 4, 17 | breq12d 5162 |
. . . . . . 7
โข (๐ = ๐ โ (((0._0_0_0_4_2_2_48)
ยท (๐โ2)) โค
โซ(0(,)1)(((((ฮ โf ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) ยท (expโ((i ยท
(2 ยท ฯ)) ยท (-๐ ยท ๐ฅ)))) d๐ฅ โ ((0._0_0_0_4_2_2_48)
ยท (๐โ2)) โค
โซ(0(,)1)(((((ฮ โf ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) ยท (expโ((i ยท
(2 ยท ฯ)) ยท (-๐ ยท ๐ฅ)))) d๐ฅ)) |
19 | 18 | 3anbi3d 1443 |
. . . . . 6
โข (๐ = ๐ โ ((โ๐ โ โ (๐โ๐) โค (1._0_7_9_9_55)
โง โ๐ โ
โ (โโ๐) โค (1._4_14)
โง ((0._0_0_0_4_2_2_48)
ยท (๐โ2)) โค
โซ(0(,)1)(((((ฮ โf ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) ยท (expโ((i ยท
(2 ยท ฯ)) ยท (-๐ ยท ๐ฅ)))) d๐ฅ) โ (โ๐ โ โ (๐โ๐) โค (1._0_7_9_9_55)
โง โ๐ โ
โ (โโ๐) โค (1._4_14)
โง ((0._0_0_0_4_2_2_48)
ยท (๐โ2)) โค
โซ(0(,)1)(((((ฮ โf ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) ยท (expโ((i ยท
(2 ยท ฯ)) ยท (-๐ ยท ๐ฅ)))) d๐ฅ))) |
20 | 19 | rexbidv 3179 |
. . . . 5
โข (๐ = ๐ โ (โ๐ โ ((0[,)+โ) โm
โ)(โ๐ โ
โ (๐โ๐) โค (1._0_7_9_9_55)
โง โ๐ โ
โ (โโ๐) โค (1._4_14)
โง ((0._0_0_0_4_2_2_48)
ยท (๐โ2)) โค
โซ(0(,)1)(((((ฮ โf ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) ยท (expโ((i ยท
(2 ยท ฯ)) ยท (-๐ ยท ๐ฅ)))) d๐ฅ) โ โ๐ โ ((0[,)+โ) โm
โ)(โ๐ โ
โ (๐โ๐) โค (1._0_7_9_9_55)
โง โ๐ โ
โ (โโ๐) โค (1._4_14)
โง ((0._0_0_0_4_2_2_48)
ยท (๐โ2)) โค
โซ(0(,)1)(((((ฮ โf ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) ยท (expโ((i ยท
(2 ยท ฯ)) ยท (-๐ ยท ๐ฅ)))) d๐ฅ))) |
21 | 20 | rexbidv 3179 |
. . . 4
โข (๐ = ๐ โ (โโ โ ((0[,)+โ) โm
โ)โ๐ โ
((0[,)+โ) โm โ)(โ๐ โ โ (๐โ๐) โค (1._0_7_9_9_55)
โง โ๐ โ
โ (โโ๐) โค (1._4_14)
โง ((0._0_0_0_4_2_2_48)
ยท (๐โ2)) โค
โซ(0(,)1)(((((ฮ โf ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) ยท (expโ((i ยท
(2 ยท ฯ)) ยท (-๐ ยท ๐ฅ)))) d๐ฅ) โ โโ โ ((0[,)+โ) โm
โ)โ๐ โ
((0[,)+โ) โm โ)(โ๐ โ โ (๐โ๐) โค (1._0_7_9_9_55)
โง โ๐ โ
โ (โโ๐) โค (1._4_14)
โง ((0._0_0_0_4_2_2_48)
ยท (๐โ2)) โค
โซ(0(,)1)(((((ฮ โf ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) ยท (expโ((i ยท
(2 ยท ฯ)) ยท (-๐ ยท ๐ฅ)))) d๐ฅ))) |
22 | 2, 21 | imbi12d 345 |
. . 3
โข (๐ = ๐ โ (((;10โ;27) โค ๐ โ โโ โ ((0[,)+โ) โm
โ)โ๐ โ
((0[,)+โ) โm โ)(โ๐ โ โ (๐โ๐) โค (1._0_7_9_9_55)
โง โ๐ โ
โ (โโ๐) โค (1._4_14)
โง ((0._0_0_0_4_2_2_48)
ยท (๐โ2)) โค
โซ(0(,)1)(((((ฮ โf ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) ยท (expโ((i ยท
(2 ยท ฯ)) ยท (-๐ ยท ๐ฅ)))) d๐ฅ)) โ ((;10โ;27) โค ๐ โ โโ โ ((0[,)+โ) โm
โ)โ๐ โ
((0[,)+โ) โm โ)(โ๐ โ โ (๐โ๐) โค (1._0_7_9_9_55)
โง โ๐ โ
โ (โโ๐) โค (1._4_14)
โง ((0._0_0_0_4_2_2_48)
ยท (๐โ2)) โค
โซ(0(,)1)(((((ฮ โf ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) ยท (expโ((i ยท
(2 ยท ฯ)) ยท (-๐ ยท ๐ฅ)))) d๐ฅ)))) |
23 | | ax-hgt749 33656 |
. . . 4
โข
โ๐ โ
{๐ง โ โค โฃ
ยฌ 2 โฅ ๐ง} ((;10โ;27) โค ๐ โ โโ โ ((0[,)+โ) โm
โ)โ๐ โ
((0[,)+โ) โm โ)(โ๐ โ โ (๐โ๐) โค (1._0_7_9_9_55)
โง โ๐ โ
โ (โโ๐) โค (1._4_14)
โง ((0._0_0_0_4_2_2_48)
ยท (๐โ2)) โค
โซ(0(,)1)(((((ฮ โf ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) ยท (expโ((i ยท
(2 ยท ฯ)) ยท (-๐ ยท ๐ฅ)))) d๐ฅ)) |
24 | 23 | a1i 11 |
. . 3
โข (๐ โ โ๐ โ {๐ง โ โค โฃ ยฌ 2 โฅ ๐ง} ((;10โ;27) โค ๐ โ โโ โ ((0[,)+โ) โm
โ)โ๐ โ
((0[,)+โ) โm โ)(โ๐ โ โ (๐โ๐) โค (1._0_7_9_9_55)
โง โ๐ โ
โ (โโ๐) โค (1._4_14)
โง ((0._0_0_0_4_2_2_48)
ยท (๐โ2)) โค
โซ(0(,)1)(((((ฮ โf ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) ยท (expโ((i ยท
(2 ยท ฯ)) ยท (-๐ ยท ๐ฅ)))) d๐ฅ))) |
25 | | hgt749d.n |
. . . 4
โข (๐ โ ๐ โ ๐) |
26 | | hgt749d.o |
. . . 4
โข ๐ = {๐ง โ โค โฃ ยฌ 2 โฅ ๐ง} |
27 | 25, 26 | eleqtrdi 2844 |
. . 3
โข (๐ โ ๐ โ {๐ง โ โค โฃ ยฌ 2 โฅ ๐ง}) |
28 | 22, 24, 27 | rspcdva 3614 |
. 2
โข (๐ โ ((;10โ;27) โค ๐ โ โโ โ ((0[,)+โ) โm
โ)โ๐ โ
((0[,)+โ) โm โ)(โ๐ โ โ (๐โ๐) โค (1._0_7_9_9_55)
โง โ๐ โ
โ (โโ๐) โค (1._4_14)
โง ((0._0_0_0_4_2_2_48)
ยท (๐โ2)) โค
โซ(0(,)1)(((((ฮ โf ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) ยท (expโ((i ยท
(2 ยท ฯ)) ยท (-๐ ยท ๐ฅ)))) d๐ฅ))) |
29 | 1, 28 | mpd 15 |
1
โข (๐ โ โโ โ ((0[,)+โ) โm
โ)โ๐ โ
((0[,)+โ) โm โ)(โ๐ โ โ (๐โ๐) โค (1._0_7_9_9_55)
โง โ๐ โ
โ (โโ๐) โค (1._4_14)
โง ((0._0_0_0_4_2_2_48)
ยท (๐โ2)) โค
โซ(0(,)1)(((((ฮ โf ยท โ)vts๐)โ๐ฅ) ยท ((((ฮ โf
ยท ๐)vts๐)โ๐ฅ)โ2)) ยท (expโ((i ยท
(2 ยท ฯ)) ยท (-๐ ยท ๐ฅ)))) d๐ฅ)) |