Step | Hyp | Ref
| Expression |
1 | | pellexlem4 41184 |
. . 3
โข ((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โ {โจ๐ฆ,
๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โ โ) |
2 | | fzfi 13884 |
. . . 4
โข
(-(โโ(1 + (2 ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))
โ Fin |
3 | | diffi 9130 |
. . . 4
โข
((-(โโ(1 + (2 ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))
โ Fin โ ((-(โโ(1 + (2 ยท (โโ๐ท))))...(โโ(1 + (2
ยท (โโ๐ท))))) โ {0}) โ
Fin) |
4 | 2, 3 | mp1i 13 |
. . 3
โข ((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โ ((-(โโ(1 + (2 ยท (โโ๐ท))))...(โโ(1 + (2
ยท (โโ๐ท))))) โ {0}) โ
Fin) |
5 | | elopab 5489 |
. . . . 5
โข (๐ โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โ โ๐ฆโ๐ง(๐ = โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท))))))) |
6 | | fveq2 6847 |
. . . . . . . . . . . 12
โข (๐ = โจ๐ฆ, ๐งโฉ โ (1st โ๐) = (1st
โโจ๐ฆ, ๐งโฉ)) |
7 | 6 | oveq1d 7377 |
. . . . . . . . . . 11
โข (๐ = โจ๐ฆ, ๐งโฉ โ ((1st โ๐)โ2) = ((1st
โโจ๐ฆ, ๐งโฉ)โ2)) |
8 | | fveq2 6847 |
. . . . . . . . . . . . 13
โข (๐ = โจ๐ฆ, ๐งโฉ โ (2nd โ๐) = (2nd
โโจ๐ฆ, ๐งโฉ)) |
9 | 8 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ = โจ๐ฆ, ๐งโฉ โ ((2nd โ๐)โ2) = ((2nd
โโจ๐ฆ, ๐งโฉ)โ2)) |
10 | 9 | oveq2d 7378 |
. . . . . . . . . . 11
โข (๐ = โจ๐ฆ, ๐งโฉ โ (๐ท ยท ((2nd โ๐)โ2)) = (๐ท ยท ((2nd
โโจ๐ฆ, ๐งโฉ)โ2))) |
11 | 7, 10 | oveq12d 7380 |
. . . . . . . . . 10
โข (๐ = โจ๐ฆ, ๐งโฉ โ (((1st โ๐)โ2) โ (๐ท ยท ((2nd
โ๐)โ2))) =
(((1st โโจ๐ฆ, ๐งโฉ)โ2) โ (๐ท ยท ((2nd
โโจ๐ฆ, ๐งโฉ)โ2)))) |
12 | | vex 3452 |
. . . . . . . . . . . . 13
โข ๐ฆ โ V |
13 | | vex 3452 |
. . . . . . . . . . . . 13
โข ๐ง โ V |
14 | 12, 13 | op1st 7934 |
. . . . . . . . . . . 12
โข
(1st โโจ๐ฆ, ๐งโฉ) = ๐ฆ |
15 | 14 | oveq1i 7372 |
. . . . . . . . . . 11
โข
((1st โโจ๐ฆ, ๐งโฉ)โ2) = (๐ฆโ2) |
16 | 12, 13 | op2nd 7935 |
. . . . . . . . . . . . 13
โข
(2nd โโจ๐ฆ, ๐งโฉ) = ๐ง |
17 | 16 | oveq1i 7372 |
. . . . . . . . . . . 12
โข
((2nd โโจ๐ฆ, ๐งโฉ)โ2) = (๐งโ2) |
18 | 17 | oveq2i 7373 |
. . . . . . . . . . 11
โข (๐ท ยท ((2nd
โโจ๐ฆ, ๐งโฉ)โ2)) = (๐ท ยท (๐งโ2)) |
19 | 15, 18 | oveq12i 7374 |
. . . . . . . . . 10
โข
(((1st โโจ๐ฆ, ๐งโฉ)โ2) โ (๐ท ยท ((2nd
โโจ๐ฆ, ๐งโฉ)โ2))) = ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) |
20 | 11, 19 | eqtrdi 2793 |
. . . . . . . . 9
โข (๐ = โจ๐ฆ, ๐งโฉ โ (((1st โ๐)โ2) โ (๐ท ยท ((2nd
โ๐)โ2))) =
((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) |
21 | 20 | ad2antrl 727 |
. . . . . . . 8
โข (((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง (๐ =
โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))))
โ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) |
22 | | simprrl 780 |
. . . . . . . . . . 11
โข ((๐ท โ โ โง (๐ = โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))))
โ (๐ฆ โ โ
โง ๐ง โ
โ)) |
23 | | simpl 484 |
. . . . . . . . . . 11
โข ((๐ท โ โ โง (๐ = โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))))
โ ๐ท โ
โ) |
24 | | simprr 772 |
. . . . . . . . . . . 12
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))
โ (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))) |
25 | 24 | ad2antll 728 |
. . . . . . . . . . 11
โข ((๐ท โ โ โง (๐ = โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))))
โ (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))) |
26 | | nnz 12527 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ โ โ ๐ฆ โ
โค) |
27 | 26 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ ๐ฆ โ โค) |
28 | | zsqcl 14041 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โค โ (๐ฆโ2) โ
โค) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ (๐ฆโ2) โ โค) |
30 | | nnz 12527 |
. . . . . . . . . . . . . . 15
โข (๐ท โ โ โ ๐ท โ
โค) |
31 | 30 | ad2antrl 727 |
. . . . . . . . . . . . . 14
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ ๐ท โ โค) |
32 | | simplr 768 |
. . . . . . . . . . . . . . . 16
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ ๐ง โ โ) |
33 | 32 | nnzd 12533 |
. . . . . . . . . . . . . . 15
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ ๐ง โ โค) |
34 | | zsqcl 14041 |
. . . . . . . . . . . . . . 15
โข (๐ง โ โค โ (๐งโ2) โ
โค) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . 14
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ (๐งโ2) โ โค) |
36 | 31, 35 | zmulcld 12620 |
. . . . . . . . . . . . 13
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ (๐ท ยท (๐งโ2)) โ โค) |
37 | 29, 36 | zsubcld 12619 |
. . . . . . . . . . . 12
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ โค) |
38 | | 1re 11162 |
. . . . . . . . . . . . . . 15
โข 1 โ
โ |
39 | | 2re 12234 |
. . . . . . . . . . . . . . . 16
โข 2 โ
โ |
40 | | nnre 12167 |
. . . . . . . . . . . . . . . . . 18
โข (๐ท โ โ โ ๐ท โ
โ) |
41 | 40 | ad2antrl 727 |
. . . . . . . . . . . . . . . . 17
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ ๐ท โ โ) |
42 | | nnnn0 12427 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ท โ โ โ ๐ท โ
โ0) |
43 | 42 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ ๐ท โ
โ0) |
44 | 43 | nn0ge0d 12483 |
. . . . . . . . . . . . . . . . 17
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ 0 โค ๐ท) |
45 | 41, 44 | resqrtcld 15309 |
. . . . . . . . . . . . . . . 16
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ (โโ๐ท) โ
โ) |
46 | | remulcl 11143 |
. . . . . . . . . . . . . . . 16
โข ((2
โ โ โง (โโ๐ท) โ โ) โ (2 ยท
(โโ๐ท)) โ
โ) |
47 | 39, 45, 46 | sylancr 588 |
. . . . . . . . . . . . . . 15
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ (2 ยท
(โโ๐ท)) โ
โ) |
48 | | readdcl 11141 |
. . . . . . . . . . . . . . 15
โข ((1
โ โ โง (2 ยท (โโ๐ท)) โ โ) โ (1 + (2 ยท
(โโ๐ท))) โ
โ) |
49 | 38, 47, 48 | sylancr 588 |
. . . . . . . . . . . . . 14
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ (1 + (2 ยท
(โโ๐ท))) โ
โ) |
50 | 49 | flcld 13710 |
. . . . . . . . . . . . 13
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ (โโ(1 + (2 ยท
(โโ๐ท)))) โ
โค) |
51 | 50 | znegcld 12616 |
. . . . . . . . . . . 12
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ -(โโ(1 + (2
ยท (โโ๐ท)))) โ โค) |
52 | 37 | zred 12614 |
. . . . . . . . . . . . 13
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ โ) |
53 | 50 | zred 12614 |
. . . . . . . . . . . . 13
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ (โโ(1 + (2 ยท
(โโ๐ท)))) โ
โ) |
54 | | nn0abscl 15204 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ โค โ
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) โ
โ0) |
55 | 37, 54 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) โ
โ0) |
56 | 55 | nn0zd 12532 |
. . . . . . . . . . . . . . . 16
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) โ โค) |
57 | 56 | zred 12614 |
. . . . . . . . . . . . . . 15
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) โ โ) |
58 | | peano2re 11335 |
. . . . . . . . . . . . . . . 16
โข
((โโ(1 + (2 ยท (โโ๐ท)))) โ โ โ
((โโ(1 + (2 ยท (โโ๐ท)))) + 1) โ โ) |
59 | 53, 58 | syl 17 |
. . . . . . . . . . . . . . 15
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ ((โโ(1 + (2
ยท (โโ๐ท)))) + 1) โ โ) |
60 | | simprr 772 |
. . . . . . . . . . . . . . 15
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))) |
61 | | flltp1 13712 |
. . . . . . . . . . . . . . . 16
โข ((1 + (2
ยท (โโ๐ท))) โ โ โ (1 + (2 ยท
(โโ๐ท))) <
((โโ(1 + (2 ยท (โโ๐ท)))) + 1)) |
62 | 49, 61 | syl 17 |
. . . . . . . . . . . . . . 15
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ (1 + (2 ยท
(โโ๐ท))) <
((โโ(1 + (2 ยท (โโ๐ท)))) + 1)) |
63 | 57, 49, 59, 60, 62 | lttrd 11323 |
. . . . . . . . . . . . . 14
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < ((โโ(1 + (2
ยท (โโ๐ท)))) + 1)) |
64 | | zleltp1 12561 |
. . . . . . . . . . . . . . 15
โข
(((absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) โ โค โง
(โโ(1 + (2 ยท (โโ๐ท)))) โ โค) โ
((absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) โค
(โโ(1 + (2 ยท (โโ๐ท)))) โ (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < ((โโ(1 + (2
ยท (โโ๐ท)))) + 1))) |
65 | 56, 50, 64 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ ((absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) โค (โโ(1 + (2
ยท (โโ๐ท)))) โ (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < ((โโ(1 + (2
ยท (โโ๐ท)))) + 1))) |
66 | 63, 65 | mpbird 257 |
. . . . . . . . . . . . 13
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) โค (โโ(1 + (2
ยท (โโ๐ท))))) |
67 | | absle 15207 |
. . . . . . . . . . . . . 14
โข ((((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ โ โง
(โโ(1 + (2 ยท (โโ๐ท)))) โ โ) โ
((absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) โค
(โโ(1 + (2 ยท (โโ๐ท)))) โ (-(โโ(1 + (2
ยท (โโ๐ท)))) โค ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โค (โโ(1 + (2
ยท (โโ๐ท))))))) |
68 | 67 | biimpa 478 |
. . . . . . . . . . . . 13
โข
(((((๐ฆโ2)
โ (๐ท ยท (๐งโ2))) โ โ โง
(โโ(1 + (2 ยท (โโ๐ท)))) โ โ) โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) โค
(โโ(1 + (2 ยท (โโ๐ท))))) โ (-(โโ(1 + (2
ยท (โโ๐ท)))) โค ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โค (โโ(1 + (2
ยท (โโ๐ท)))))) |
69 | 52, 53, 66, 68 | syl21anc 837 |
. . . . . . . . . . . 12
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ (-(โโ(1 + (2
ยท (โโ๐ท)))) โค ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โค (โโ(1 + (2
ยท (โโ๐ท)))))) |
70 | | elfz 13437 |
. . . . . . . . . . . . 13
โข ((((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ โค โง
-(โโ(1 + (2 ยท (โโ๐ท)))) โ โค โง (โโ(1
+ (2 ยท (โโ๐ท)))) โ โค) โ (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ (-(โโ(1 + (2
ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))
โ (-(โโ(1 + (2 ยท (โโ๐ท)))) โค ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โค (โโ(1 + (2
ยท (โโ๐ท))))))) |
71 | 70 | biimpar 479 |
. . . . . . . . . . . 12
โข
(((((๐ฆโ2)
โ (๐ท ยท (๐งโ2))) โ โค โง
-(โโ(1 + (2 ยท (โโ๐ท)))) โ โค โง (โโ(1
+ (2 ยท (โโ๐ท)))) โ โค) โง
(-(โโ(1 + (2 ยท (โโ๐ท)))) โค ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โค (โโ(1 + (2
ยท (โโ๐ท)))))) โ ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ (-(โโ(1 + (2
ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))) |
72 | 37, 51, 50, 69, 71 | syl31anc 1374 |
. . . . . . . . . . 11
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (๐ท โ โ โง
(absโ((๐ฆโ2)
โ (๐ท ยท (๐งโ2)))) < (1 + (2
ยท (โโ๐ท))))) โ ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ (-(โโ(1 + (2
ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))) |
73 | 22, 23, 25, 72 | syl12anc 836 |
. . . . . . . . . 10
โข ((๐ท โ โ โง (๐ = โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))))
โ ((๐ฆโ2) โ
(๐ท ยท (๐งโ2))) โ
(-(โโ(1 + (2 ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))) |
74 | 73 | adantlr 714 |
. . . . . . . . 9
โข (((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง (๐ =
โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))))
โ ((๐ฆโ2) โ
(๐ท ยท (๐งโ2))) โ
(-(โโ(1 + (2 ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))) |
75 | | simprl 770 |
. . . . . . . . . 10
โข (((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))
โ ((๐ฆโ2) โ
(๐ท ยท (๐งโ2))) โ
0) |
76 | 75 | ad2antll 728 |
. . . . . . . . 9
โข (((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง (๐ =
โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))))
โ ((๐ฆโ2) โ
(๐ท ยท (๐งโ2))) โ
0) |
77 | | eldifsn 4752 |
. . . . . . . . 9
โข (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ ((-(โโ(1 + (2
ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))
โ {0}) โ (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ (-(โโ(1 + (2
ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท))))) โง
((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0)) |
78 | 74, 76, 77 | sylanbrc 584 |
. . . . . . . 8
โข (((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง (๐ =
โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))))
โ ((๐ฆโ2) โ
(๐ท ยท (๐งโ2))) โ
((-(โโ(1 + (2 ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))
โ {0})) |
79 | 21, 78 | eqeltrd 2838 |
. . . . . . 7
โข (((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง (๐ =
โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))))
โ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) โ
((-(โโ(1 + (2 ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))
โ {0})) |
80 | 79 | ex 414 |
. . . . . 6
โข ((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โ ((๐ =
โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท))))))
โ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) โ
((-(โโ(1 + (2 ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))
โ {0}))) |
81 | 80 | exlimdvv 1938 |
. . . . 5
โข ((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โ (โ๐ฆโ๐ง(๐ = โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท))))))
โ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) โ
((-(โโ(1 + (2 ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))
โ {0}))) |
82 | 5, 81 | biimtrid 241 |
. . . 4
โข ((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โ (๐ โ
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) โ
((-(โโ(1 + (2 ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))
โ {0}))) |
83 | 82 | imp 408 |
. . 3
โข (((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง ๐ โ
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))})
โ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) โ
((-(โโ(1 + (2 ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))
โ {0})) |
84 | 1, 4, 83 | fiphp3d 41171 |
. 2
โข ((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โ โ๐ฅ
โ ((-(โโ(1 + (2 ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))
โ {0}){๐ โ
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โ โ) |
85 | | eldif 3925 |
. . . . . 6
โข (๐ฅ โ ((-(โโ(1 +
(2 ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))
โ {0}) โ (๐ฅ
โ (-(โโ(1 + (2 ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท))))) โง
ยฌ ๐ฅ โ
{0})) |
86 | | elfzelz 13448 |
. . . . . . . 8
โข (๐ฅ โ (-(โโ(1 + (2
ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))
โ ๐ฅ โ
โค) |
87 | | simp2 1138 |
. . . . . . . . . 10
โข (((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง ๐ฅ โ
โค โง ยฌ ๐ฅ
โ {0}) โ ๐ฅ โ
โค) |
88 | | velsn 4607 |
. . . . . . . . . . . . 13
โข (๐ฅ โ {0} โ ๐ฅ = 0) |
89 | 88 | biimpri 227 |
. . . . . . . . . . . 12
โข (๐ฅ = 0 โ ๐ฅ โ {0}) |
90 | 89 | necon3bi 2971 |
. . . . . . . . . . 11
โข (ยฌ
๐ฅ โ {0} โ ๐ฅ โ 0) |
91 | 90 | 3ad2ant3 1136 |
. . . . . . . . . 10
โข (((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง ๐ฅ โ
โค โง ยฌ ๐ฅ
โ {0}) โ ๐ฅ โ
0) |
92 | 87, 91 | jca 513 |
. . . . . . . . 9
โข (((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง ๐ฅ โ
โค โง ยฌ ๐ฅ
โ {0}) โ (๐ฅ
โ โค โง ๐ฅ โ
0)) |
93 | 92 | 3exp 1120 |
. . . . . . . 8
โข ((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โ (๐ฅ โ
โค โ (ยฌ ๐ฅ
โ {0} โ (๐ฅ โ
โค โง ๐ฅ โ
0)))) |
94 | 86, 93 | syl5 34 |
. . . . . . 7
โข ((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โ (๐ฅ โ
(-(โโ(1 + (2 ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))
โ (ยฌ ๐ฅ โ {0}
โ (๐ฅ โ โค
โง ๐ฅ โ
0)))) |
95 | 94 | impd 412 |
. . . . . 6
โข ((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โ ((๐ฅ โ
(-(โโ(1 + (2 ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท))))) โง
ยฌ ๐ฅ โ {0}) โ
(๐ฅ โ โค โง
๐ฅ โ
0))) |
96 | 85, 95 | biimtrid 241 |
. . . . 5
โข ((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โ (๐ฅ โ
((-(โโ(1 + (2 ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))
โ {0}) โ (๐ฅ
โ โค โง ๐ฅ โ
0))) |
97 | | simp2l 1200 |
. . . . . . 7
โข (((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง (๐ฅ โ
โค โง ๐ฅ โ 0)
โง {๐ โ
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โ โ) โ ๐ฅ โ โค) |
98 | | simp2r 1201 |
. . . . . . 7
โข (((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง (๐ฅ โ
โค โง ๐ฅ โ 0)
โง {๐ โ
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โ โ) โ ๐ฅ โ 0) |
99 | | nnex 12166 |
. . . . . . . . . . 11
โข โ
โ V |
100 | 99, 99 | xpex 7692 |
. . . . . . . . . 10
โข (โ
ร โ) โ V |
101 | | opabssxp 5729 |
. . . . . . . . . 10
โข
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)} โ (โ ร
โ) |
102 | | ssdomg 8947 |
. . . . . . . . . 10
โข ((โ
ร โ) โ V โ ({โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)} โ (โ ร โ) โ
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)} โผ (โ ร
โ))) |
103 | 100, 101,
102 | mp2 9 |
. . . . . . . . 9
โข
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)} โผ (โ ร
โ) |
104 | | xpnnen 16100 |
. . . . . . . . 9
โข (โ
ร โ) โ โ |
105 | | domentr 8960 |
. . . . . . . . 9
โข
(({โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)} โผ (โ ร โ) โง
(โ ร โ) โ โ) โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)} โผ โ) |
106 | 103, 104,
105 | mp2an 691 |
. . . . . . . 8
โข
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)} โผ โ |
107 | | ensym 8950 |
. . . . . . . . . 10
โข ({๐ โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โ โ โ โ โ
{๐ โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ}) |
108 | 107 | 3ad2ant3 1136 |
. . . . . . . . 9
โข (((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง (๐ฅ โ
โค โง ๐ฅ โ 0)
โง {๐ โ
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โ โ) โ โ โ
{๐ โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ}) |
109 | 100, 101 | ssexi 5284 |
. . . . . . . . . 10
โข
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)} โ V |
110 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ (1st โ๐) = (1st โ๐)) |
111 | 110 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ ((1st โ๐)โ2) = ((1st
โ๐)โ2)) |
112 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = ๐ โ (2nd โ๐) = (2nd โ๐)) |
113 | 112 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ ((2nd โ๐)โ2) = ((2nd
โ๐)โ2)) |
114 | 113 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ (๐ท ยท ((2nd โ๐)โ2)) = (๐ท ยท ((2nd โ๐)โ2))) |
115 | 111, 114 | oveq12d 7380 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ (((1st โ๐)โ2) โ (๐ท ยท ((2nd
โ๐)โ2))) =
(((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2)))) |
116 | 115 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ ((((1st โ๐)โ2) โ (๐ท ยท ((2nd
โ๐)โ2))) = ๐ฅ โ (((1st
โ๐)โ2) โ
(๐ท ยท
((2nd โ๐)โ2))) = ๐ฅ)) |
117 | 116 | elrab 3650 |
. . . . . . . . . . . . 13
โข (๐ โ {๐ โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โ (๐ โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โง (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ)) |
118 | | simprl 770 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ท โ
โ โง ยฌ (โโ๐ท) โ โ) โง (๐ฅ โ โค โง ๐ฅ โ 0)) โง (((1st
โ๐)โ2) โ
(๐ท ยท
((2nd โ๐)โ2))) = ๐ฅ) โง (๐ = โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))))
โ ๐ = โจ๐ฆ, ๐งโฉ) |
119 | | simprrl 780 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ท โ
โ โง ยฌ (โโ๐ท) โ โ) โง (๐ฅ โ โค โง ๐ฅ โ 0)) โง (((1st
โ๐)โ2) โ
(๐ท ยท
((2nd โ๐)โ2))) = ๐ฅ) โง (๐ = โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))))
โ (๐ฆ โ โ
โง ๐ง โ
โ)) |
120 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ = โจ๐ฆ, ๐งโฉ โ (1st โ๐) = (1st
โโจ๐ฆ, ๐งโฉ)) |
121 | 120 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = โจ๐ฆ, ๐งโฉ โ ((1st โ๐)โ2) = ((1st
โโจ๐ฆ, ๐งโฉ)โ2)) |
122 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ = โจ๐ฆ, ๐งโฉ โ (2nd โ๐) = (2nd
โโจ๐ฆ, ๐งโฉ)) |
123 | 122 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ = โจ๐ฆ, ๐งโฉ โ ((2nd โ๐)โ2) = ((2nd
โโจ๐ฆ, ๐งโฉ)โ2)) |
124 | 123 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = โจ๐ฆ, ๐งโฉ โ (๐ท ยท ((2nd โ๐)โ2)) = (๐ท ยท ((2nd
โโจ๐ฆ, ๐งโฉ)โ2))) |
125 | 121, 124 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ = โจ๐ฆ, ๐งโฉ โ (((1st โ๐)โ2) โ (๐ท ยท ((2nd
โ๐)โ2))) =
(((1st โโจ๐ฆ, ๐งโฉ)โ2) โ (๐ท ยท ((2nd
โโจ๐ฆ, ๐งโฉ)โ2)))) |
126 | 125, 19 | eqtr2di 2794 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = โจ๐ฆ, ๐งโฉ โ ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = (((1st โ๐)โ2) โ (๐ท ยท ((2nd
โ๐)โ2)))) |
127 | 126 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . 20
โข
(((((๐ท โ
โ โง ยฌ (โโ๐ท) โ โ) โง (๐ฅ โ โค โง ๐ฅ โ 0)) โง (((1st
โ๐)โ2) โ
(๐ท ยท
((2nd โ๐)โ2))) = ๐ฅ) โง (๐ = โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))))
โ ((๐ฆโ2) โ
(๐ท ยท (๐งโ2))) = (((1st
โ๐)โ2) โ
(๐ท ยท
((2nd โ๐)โ2)))) |
128 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . 20
โข
(((((๐ท โ
โ โง ยฌ (โโ๐ท) โ โ) โง (๐ฅ โ โค โง ๐ฅ โ 0)) โง (((1st
โ๐)โ2) โ
(๐ท ยท
((2nd โ๐)โ2))) = ๐ฅ) โง (๐ = โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))))
โ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ) |
129 | 127, 128 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ท โ
โ โง ยฌ (โโ๐ท) โ โ) โง (๐ฅ โ โค โง ๐ฅ โ 0)) โง (((1st
โ๐)โ2) โ
(๐ท ยท
((2nd โ๐)โ2))) = ๐ฅ) โง (๐ = โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))))
โ ((๐ฆโ2) โ
(๐ท ยท (๐งโ2))) = ๐ฅ) |
130 | 118, 119,
129 | jca32 517 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ท โ
โ โง ยฌ (โโ๐ท) โ โ) โง (๐ฅ โ โค โง ๐ฅ โ 0)) โง (((1st
โ๐)โ2) โ
(๐ท ยท
((2nd โ๐)โ2))) = ๐ฅ) โง (๐ = โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))))
โ (๐ = โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ))) |
131 | 130 | ex 414 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง (๐ฅ โ
โค โง ๐ฅ โ 0))
โง (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ) โ ((๐ = โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท))))))
โ (๐ = โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)))) |
132 | 131 | 2eximdv 1923 |
. . . . . . . . . . . . . . . 16
โข ((((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง (๐ฅ โ
โค โง ๐ฅ โ 0))
โง (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ) โ (โ๐ฆโ๐ง(๐ = โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท))))))
โ โ๐ฆโ๐ง(๐ = โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)))) |
133 | | elopab 5489 |
. . . . . . . . . . . . . . . 16
โข (๐ โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โ โ๐ฆโ๐ง(๐ = โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท))))))) |
134 | | elopab 5489 |
. . . . . . . . . . . . . . . 16
โข (๐ โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)} โ โ๐ฆโ๐ง(๐ = โจ๐ฆ, ๐งโฉ โง ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ))) |
135 | 132, 133,
134 | 3imtr4g 296 |
. . . . . . . . . . . . . . 15
โข ((((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง (๐ฅ โ
โค โง ๐ฅ โ 0))
โง (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ) โ (๐ โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โ ๐ โ
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)})) |
136 | 135 | expimpd 455 |
. . . . . . . . . . . . . 14
โข (((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง (๐ฅ โ
โค โง ๐ฅ โ 0))
โ (((((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ โง ๐ โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))})
โ ๐ โ
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)})) |
137 | 136 | ancomsd 467 |
. . . . . . . . . . . . 13
โข (((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง (๐ฅ โ
โค โง ๐ฅ โ 0))
โ ((๐ โ
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โง (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ) โ ๐ โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)})) |
138 | 117, 137 | biimtrid 241 |
. . . . . . . . . . . 12
โข (((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง (๐ฅ โ
โค โง ๐ฅ โ 0))
โ (๐ โ {๐ โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โ ๐ โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)})) |
139 | 138 | ssrdv 3955 |
. . . . . . . . . . 11
โข (((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง (๐ฅ โ
โค โง ๐ฅ โ 0))
โ {๐ โ
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)}) |
140 | 139 | 3adant3 1133 |
. . . . . . . . . 10
โข (((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง (๐ฅ โ
โค โง ๐ฅ โ 0)
โง {๐ โ
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โ โ) โ {๐ โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)}) |
141 | | ssdomg 8947 |
. . . . . . . . . 10
โข
({โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)} โ V โ ({๐ โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)} โ {๐ โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โผ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)})) |
142 | 109, 140,
141 | mpsyl 68 |
. . . . . . . . 9
โข (((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง (๐ฅ โ
โค โง ๐ฅ โ 0)
โง {๐ โ
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โ โ) โ {๐ โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โผ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)}) |
143 | | endomtr 8959 |
. . . . . . . . 9
โข ((โ
โ {๐ โ
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โง {๐ โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โผ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)}) โ โ โผ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)}) |
144 | 108, 142,
143 | syl2anc 585 |
. . . . . . . 8
โข (((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง (๐ฅ โ
โค โง ๐ฅ โ 0)
โง {๐ โ
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โ โ) โ โ โผ
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)}) |
145 | | sbth 9044 |
. . . . . . . 8
โข
(({โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)} โผ โ โง โ โผ
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)}) โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)} โ โ) |
146 | 106, 144,
145 | sylancr 588 |
. . . . . . 7
โข (((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง (๐ฅ โ
โค โง ๐ฅ โ 0)
โง {๐ โ
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โ โ) โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)} โ โ) |
147 | 97, 98, 146 | jca32 517 |
. . . . . 6
โข (((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โง (๐ฅ โ
โค โง ๐ฅ โ 0)
โง {๐ โ
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โ โ) โ (๐ฅ โ โค โง (๐ฅ โ 0 โง {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)} โ โ))) |
148 | 147 | 3exp 1120 |
. . . . 5
โข ((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โ ((๐ฅ โ
โค โง ๐ฅ โ 0)
โ ({๐ โ
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โ โ โ (๐ฅ โ โค โง (๐ฅ โ 0 โง {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)} โ โ))))) |
149 | 96, 148 | syld 47 |
. . . 4
โข ((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โ (๐ฅ โ
((-(โโ(1 + (2 ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))
โ {0}) โ ({๐
โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โ โ โ (๐ฅ โ โค โง (๐ฅ โ 0 โง {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)} โ โ))))) |
150 | 149 | impd 412 |
. . 3
โข ((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โ ((๐ฅ โ
((-(โโ(1 + (2 ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))
โ {0}) โง {๐
โ {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โ โ) โ (๐ฅ โ โค โง (๐ฅ โ 0 โง {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)} โ โ)))) |
151 | 150 | reximdv2 3162 |
. 2
โข ((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โ (โ๐ฅ
โ ((-(โโ(1 + (2 ยท (โโ๐ท))))...(โโ(1 + (2 ยท
(โโ๐ท)))))
โ {0}){๐ โ
{โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง (((๐ฆโ2) โ (๐ท ยท (๐งโ2))) โ 0 โง (absโ((๐ฆโ2) โ (๐ท ยท (๐งโ2)))) < (1 + (2 ยท
(โโ๐ท)))))}
โฃ (((1st โ๐)โ2) โ (๐ท ยท ((2nd โ๐)โ2))) = ๐ฅ} โ โ โ โ๐ฅ โ โค (๐ฅ โ 0 โง {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)} โ โ))) |
152 | 84, 151 | mpd 15 |
1
โข ((๐ท โ โ โง ยฌ
(โโ๐ท) โ
โ) โ โ๐ฅ
โ โค (๐ฅ โ 0
โง {โจ๐ฆ, ๐งโฉ โฃ ((๐ฆ โ โ โง ๐ง โ โ) โง ((๐ฆโ2) โ (๐ท ยท (๐งโ2))) = ๐ฅ)} โ โ)) |