Step | Hyp | Ref
| Expression |
1 | | 2cnd 12286 |
. . . . . . 7
โข (๐ โ 2 โ
โ) |
2 | | knoppndvlem2.n |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
3 | | nnz 12575 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โค) |
4 | 2, 3 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐ โ โค) |
5 | 4 | zcnd 12663 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
6 | 1, 5 | mulcld 11230 |
. . . . . 6
โข (๐ โ (2 ยท ๐) โ
โ) |
7 | | 2ne0 12312 |
. . . . . . . 8
โข 2 โ
0 |
8 | 7 | a1i 11 |
. . . . . . 7
โข (๐ โ 2 โ 0) |
9 | | 0red 11213 |
. . . . . . . . 9
โข (๐ โ 0 โ
โ) |
10 | | 1red 11211 |
. . . . . . . . . 10
โข (๐ โ 1 โ
โ) |
11 | 4 | zred 12662 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
12 | | 0lt1 11732 |
. . . . . . . . . . 11
โข 0 <
1 |
13 | 12 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 0 < 1) |
14 | | nnge1 12236 |
. . . . . . . . . . 11
โข (๐ โ โ โ 1 โค
๐) |
15 | 2, 14 | syl 17 |
. . . . . . . . . 10
โข (๐ โ 1 โค ๐) |
16 | 9, 10, 11, 13, 15 | ltletrd 11370 |
. . . . . . . . 9
โข (๐ โ 0 < ๐) |
17 | 9, 16 | ltned 11346 |
. . . . . . . 8
โข (๐ โ 0 โ ๐) |
18 | 17 | necomd 2996 |
. . . . . . 7
โข (๐ โ ๐ โ 0) |
19 | 1, 5, 8, 18 | mulne0d 11862 |
. . . . . 6
โข (๐ โ (2 ยท ๐) โ 0) |
20 | | knoppndvlem2.i |
. . . . . 6
โข (๐ โ ๐ผ โ โค) |
21 | 6, 19, 20 | expclzd 14112 |
. . . . 5
โข (๐ โ ((2 ยท ๐)โ๐ผ) โ โ) |
22 | | knoppndvlem2.j |
. . . . . . . 8
โข (๐ โ ๐ฝ โ โค) |
23 | 22 | znegcld 12664 |
. . . . . . 7
โข (๐ โ -๐ฝ โ โค) |
24 | 6, 19, 23 | expclzd 14112 |
. . . . . 6
โข (๐ โ ((2 ยท ๐)โ-๐ฝ) โ โ) |
25 | 24, 1, 8 | divcld 11986 |
. . . . 5
โข (๐ โ (((2 ยท ๐)โ-๐ฝ) / 2) โ โ) |
26 | | knoppndvlem2.m |
. . . . . 6
โข (๐ โ ๐ โ โค) |
27 | 26 | zcnd 12663 |
. . . . 5
โข (๐ โ ๐ โ โ) |
28 | 21, 25, 27 | mulassd 11233 |
. . . 4
โข (๐ โ ((((2 ยท ๐)โ๐ผ) ยท (((2 ยท ๐)โ-๐ฝ) / 2)) ยท ๐) = (((2 ยท ๐)โ๐ผ) ยท ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐))) |
29 | 28 | eqcomd 2738 |
. . 3
โข (๐ โ (((2 ยท ๐)โ๐ผ) ยท ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐)) = ((((2 ยท ๐)โ๐ผ) ยท (((2 ยท ๐)โ-๐ฝ) / 2)) ยท ๐)) |
30 | 21, 24, 1, 8 | divassd 12021 |
. . . . . 6
โข (๐ โ ((((2 ยท ๐)โ๐ผ) ยท ((2 ยท ๐)โ-๐ฝ)) / 2) = (((2 ยท ๐)โ๐ผ) ยท (((2 ยท ๐)โ-๐ฝ) / 2))) |
31 | 30 | eqcomd 2738 |
. . . . 5
โข (๐ โ (((2 ยท ๐)โ๐ผ) ยท (((2 ยท ๐)โ-๐ฝ) / 2)) = ((((2 ยท ๐)โ๐ผ) ยท ((2 ยท ๐)โ-๐ฝ)) / 2)) |
32 | 6, 19 | jca 512 |
. . . . . . . . . 10
โข (๐ โ ((2 ยท ๐) โ โ โง (2
ยท ๐) โ
0)) |
33 | 20, 23 | jca 512 |
. . . . . . . . . 10
โข (๐ โ (๐ผ โ โค โง -๐ฝ โ โค)) |
34 | 32, 33 | jca 512 |
. . . . . . . . 9
โข (๐ โ (((2 ยท ๐) โ โ โง (2
ยท ๐) โ 0) โง
(๐ผ โ โค โง
-๐ฝ โ
โค))) |
35 | | expaddz 14068 |
. . . . . . . . 9
โข ((((2
ยท ๐) โ โ
โง (2 ยท ๐) โ
0) โง (๐ผ โ โค
โง -๐ฝ โ โค))
โ ((2 ยท ๐)โ(๐ผ + -๐ฝ)) = (((2 ยท ๐)โ๐ผ) ยท ((2 ยท ๐)โ-๐ฝ))) |
36 | 34, 35 | syl 17 |
. . . . . . . 8
โข (๐ โ ((2 ยท ๐)โ(๐ผ + -๐ฝ)) = (((2 ยท ๐)โ๐ผ) ยท ((2 ยท ๐)โ-๐ฝ))) |
37 | 36 | eqcomd 2738 |
. . . . . . 7
โข (๐ โ (((2 ยท ๐)โ๐ผ) ยท ((2 ยท ๐)โ-๐ฝ)) = ((2 ยท ๐)โ(๐ผ + -๐ฝ))) |
38 | 20 | zcnd 12663 |
. . . . . . . . 9
โข (๐ โ ๐ผ โ โ) |
39 | 22 | zcnd 12663 |
. . . . . . . . 9
โข (๐ โ ๐ฝ โ โ) |
40 | 38, 39 | negsubd 11573 |
. . . . . . . 8
โข (๐ โ (๐ผ + -๐ฝ) = (๐ผ โ ๐ฝ)) |
41 | 40 | oveq2d 7421 |
. . . . . . 7
โข (๐ โ ((2 ยท ๐)โ(๐ผ + -๐ฝ)) = ((2 ยท ๐)โ(๐ผ โ ๐ฝ))) |
42 | | knoppndvlem2.1 |
. . . . . . . . . 10
โข (๐ โ ๐ฝ < ๐ผ) |
43 | 22, 20 | jca 512 |
. . . . . . . . . . 11
โข (๐ โ (๐ฝ โ โค โง ๐ผ โ โค)) |
44 | | znnsub 12604 |
. . . . . . . . . . 11
โข ((๐ฝ โ โค โง ๐ผ โ โค) โ (๐ฝ < ๐ผ โ (๐ผ โ ๐ฝ) โ โ)) |
45 | 43, 44 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (๐ฝ < ๐ผ โ (๐ผ โ ๐ฝ) โ โ)) |
46 | 42, 45 | mpbid 231 |
. . . . . . . . 9
โข (๐ โ (๐ผ โ ๐ฝ) โ โ) |
47 | 6, 46 | jca 512 |
. . . . . . . 8
โข (๐ โ ((2 ยท ๐) โ โ โง (๐ผ โ ๐ฝ) โ โ)) |
48 | | expm1t 14052 |
. . . . . . . 8
โข (((2
ยท ๐) โ โ
โง (๐ผ โ ๐ฝ) โ โ) โ ((2
ยท ๐)โ(๐ผ โ ๐ฝ)) = (((2 ยท ๐)โ((๐ผ โ ๐ฝ) โ 1)) ยท (2 ยท ๐))) |
49 | 47, 48 | syl 17 |
. . . . . . 7
โข (๐ โ ((2 ยท ๐)โ(๐ผ โ ๐ฝ)) = (((2 ยท ๐)โ((๐ผ โ ๐ฝ) โ 1)) ยท (2 ยท ๐))) |
50 | 37, 41, 49 | 3eqtrd 2776 |
. . . . . 6
โข (๐ โ (((2 ยท ๐)โ๐ผ) ยท ((2 ยท ๐)โ-๐ฝ)) = (((2 ยท ๐)โ((๐ผ โ ๐ฝ) โ 1)) ยท (2 ยท ๐))) |
51 | 50 | oveq1d 7420 |
. . . . 5
โข (๐ โ ((((2 ยท ๐)โ๐ผ) ยท ((2 ยท ๐)โ-๐ฝ)) / 2) = ((((2 ยท ๐)โ((๐ผ โ ๐ฝ) โ 1)) ยท (2 ยท ๐)) / 2)) |
52 | 20, 22 | jca 512 |
. . . . . . . . . . . 12
โข (๐ โ (๐ผ โ โค โง ๐ฝ โ โค)) |
53 | | zsubcl 12600 |
. . . . . . . . . . . 12
โข ((๐ผ โ โค โง ๐ฝ โ โค) โ (๐ผ โ ๐ฝ) โ โค) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (๐ผ โ ๐ฝ) โ โค) |
55 | | peano2zm 12601 |
. . . . . . . . . . 11
โข ((๐ผ โ ๐ฝ) โ โค โ ((๐ผ โ ๐ฝ) โ 1) โ
โค) |
56 | 54, 55 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ((๐ผ โ ๐ฝ) โ 1) โ
โค) |
57 | 22 | zred 12662 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ฝ โ โ) |
58 | 20 | zred 12662 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ผ โ โ) |
59 | 57, 58 | posdifd 11797 |
. . . . . . . . . . . 12
โข (๐ โ (๐ฝ < ๐ผ โ 0 < (๐ผ โ ๐ฝ))) |
60 | 42, 59 | mpbid 231 |
. . . . . . . . . . 11
โข (๐ โ 0 < (๐ผ โ ๐ฝ)) |
61 | | 0zd 12566 |
. . . . . . . . . . . . 13
โข (๐ โ 0 โ
โค) |
62 | 61, 54 | jca 512 |
. . . . . . . . . . . 12
โข (๐ โ (0 โ โค โง
(๐ผ โ ๐ฝ) โ
โค)) |
63 | | zltlem1 12611 |
. . . . . . . . . . . 12
โข ((0
โ โค โง (๐ผ
โ ๐ฝ) โ โค)
โ (0 < (๐ผ โ
๐ฝ) โ 0 โค ((๐ผ โ ๐ฝ) โ 1))) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (0 < (๐ผ โ ๐ฝ) โ 0 โค ((๐ผ โ ๐ฝ) โ 1))) |
65 | 60, 64 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ 0 โค ((๐ผ โ ๐ฝ) โ 1)) |
66 | 56, 65 | jca 512 |
. . . . . . . . 9
โข (๐ โ (((๐ผ โ ๐ฝ) โ 1) โ โค โง 0 โค
((๐ผ โ ๐ฝ) โ 1))) |
67 | | elnn0z 12567 |
. . . . . . . . 9
โข (((๐ผ โ ๐ฝ) โ 1) โ โ0
โ (((๐ผ โ ๐ฝ) โ 1) โ โค
โง 0 โค ((๐ผ โ
๐ฝ) โ
1))) |
68 | 66, 67 | sylibr 233 |
. . . . . . . 8
โข (๐ โ ((๐ผ โ ๐ฝ) โ 1) โ
โ0) |
69 | 6, 68 | expcld 14107 |
. . . . . . 7
โข (๐ โ ((2 ยท ๐)โ((๐ผ โ ๐ฝ) โ 1)) โ
โ) |
70 | 69, 6, 1, 8 | divassd 12021 |
. . . . . 6
โข (๐ โ ((((2 ยท ๐)โ((๐ผ โ ๐ฝ) โ 1)) ยท (2 ยท ๐)) / 2) = (((2 ยท ๐)โ((๐ผ โ ๐ฝ) โ 1)) ยท ((2 ยท ๐) / 2))) |
71 | 5, 1, 8 | divcan3d 11991 |
. . . . . . 7
โข (๐ โ ((2 ยท ๐) / 2) = ๐) |
72 | 71 | oveq2d 7421 |
. . . . . 6
โข (๐ โ (((2 ยท ๐)โ((๐ผ โ ๐ฝ) โ 1)) ยท ((2 ยท ๐) / 2)) = (((2 ยท ๐)โ((๐ผ โ ๐ฝ) โ 1)) ยท ๐)) |
73 | 70, 72 | eqtrd 2772 |
. . . . 5
โข (๐ โ ((((2 ยท ๐)โ((๐ผ โ ๐ฝ) โ 1)) ยท (2 ยท ๐)) / 2) = (((2 ยท ๐)โ((๐ผ โ ๐ฝ) โ 1)) ยท ๐)) |
74 | 31, 51, 73 | 3eqtrd 2776 |
. . . 4
โข (๐ โ (((2 ยท ๐)โ๐ผ) ยท (((2 ยท ๐)โ-๐ฝ) / 2)) = (((2 ยท ๐)โ((๐ผ โ ๐ฝ) โ 1)) ยท ๐)) |
75 | 74 | oveq1d 7420 |
. . 3
โข (๐ โ ((((2 ยท ๐)โ๐ผ) ยท (((2 ยท ๐)โ-๐ฝ) / 2)) ยท ๐) = ((((2 ยท ๐)โ((๐ผ โ ๐ฝ) โ 1)) ยท ๐) ยท ๐)) |
76 | 29, 75 | eqtrd 2772 |
. 2
โข (๐ โ (((2 ยท ๐)โ๐ผ) ยท ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐)) = ((((2 ยท ๐)โ((๐ผ โ ๐ฝ) โ 1)) ยท ๐) ยท ๐)) |
77 | | 2z 12590 |
. . . . . . . . 9
โข 2 โ
โค |
78 | 77 | a1i 11 |
. . . . . . . 8
โข (๐ โ 2 โ
โค) |
79 | 78, 4 | jca 512 |
. . . . . . 7
โข (๐ โ (2 โ โค โง
๐ โ
โค)) |
80 | | zmulcl 12607 |
. . . . . . 7
โข ((2
โ โค โง ๐
โ โค) โ (2 ยท ๐) โ โค) |
81 | 79, 80 | syl 17 |
. . . . . 6
โข (๐ โ (2 ยท ๐) โ
โค) |
82 | 81, 68 | jca 512 |
. . . . 5
โข (๐ โ ((2 ยท ๐) โ โค โง ((๐ผ โ ๐ฝ) โ 1) โ
โ0)) |
83 | | zexpcl 14038 |
. . . . 5
โข (((2
ยท ๐) โ โค
โง ((๐ผ โ ๐ฝ) โ 1) โ
โ0) โ ((2 ยท ๐)โ((๐ผ โ ๐ฝ) โ 1)) โ
โค) |
84 | 82, 83 | syl 17 |
. . . 4
โข (๐ โ ((2 ยท ๐)โ((๐ผ โ ๐ฝ) โ 1)) โ
โค) |
85 | 84, 4 | zmulcld 12668 |
. . 3
โข (๐ โ (((2 ยท ๐)โ((๐ผ โ ๐ฝ) โ 1)) ยท ๐) โ โค) |
86 | 85, 26 | zmulcld 12668 |
. 2
โข (๐ โ ((((2 ยท ๐)โ((๐ผ โ ๐ฝ) โ 1)) ยท ๐) ยท ๐) โ โค) |
87 | 76, 86 | eqeltrd 2833 |
1
โข (๐ โ (((2 ยท ๐)โ๐ผ) ยท ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐)) โ โค) |