Step | Hyp | Ref
| Expression |
1 | | lgsqr.1 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ (โ โ
{2})) |
2 | 1 | eldifad 3923 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
3 | | lgsqr.y |
. . . . . . . . . . . . 13
โข ๐ =
(โค/nโคโ๐) |
4 | 3 | znfld 20970 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ Field) |
5 | 2, 4 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ Field) |
6 | | fldidom 20778 |
. . . . . . . . . . 11
โข (๐ โ Field โ ๐ โ IDomn) |
7 | 5, 6 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ๐ โ IDomn) |
8 | | isidom 20777 |
. . . . . . . . . . 11
โข (๐ โ IDomn โ (๐ โ CRing โง ๐ โ Domn)) |
9 | 8 | simplbi 499 |
. . . . . . . . . 10
โข (๐ โ IDomn โ ๐ โ CRing) |
10 | 7, 9 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐ โ CRing) |
11 | | crngring 19977 |
. . . . . . . . 9
โข (๐ โ CRing โ ๐ โ Ring) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐ โ Ring) |
13 | | lgsqr.l |
. . . . . . . . 9
โข ๐ฟ = (โคRHomโ๐) |
14 | 13 | zrhrhm 20915 |
. . . . . . . 8
โข (๐ โ Ring โ ๐ฟ โ (โคring
RingHom ๐)) |
15 | 12, 14 | syl 17 |
. . . . . . 7
โข (๐ โ ๐ฟ โ (โคring RingHom
๐)) |
16 | | zringbas 20878 |
. . . . . . . 8
โข โค =
(Baseโโคring) |
17 | | eqid 2737 |
. . . . . . . 8
โข
(Baseโ๐) =
(Baseโ๐) |
18 | 16, 17 | rhmf 20159 |
. . . . . . 7
โข (๐ฟ โ (โคring
RingHom ๐) โ ๐ฟ:โคโถ(Baseโ๐)) |
19 | 15, 18 | syl 17 |
. . . . . 6
โข (๐ โ ๐ฟ:โคโถ(Baseโ๐)) |
20 | 19 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ ๐ฟ:โคโถ(Baseโ๐)) |
21 | | elfzelz 13442 |
. . . . . . 7
โข (๐ฆ โ (1...((๐ โ 1) / 2)) โ ๐ฆ โ โค) |
22 | 21 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ ๐ฆ โ โค) |
23 | | zsqcl 14035 |
. . . . . 6
โข (๐ฆ โ โค โ (๐ฆโ2) โ
โค) |
24 | 22, 23 | syl 17 |
. . . . 5
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ (๐ฆโ2) โ
โค) |
25 | 20, 24 | ffvelcdmd 7037 |
. . . 4
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ (๐ฟโ(๐ฆโ2)) โ (Baseโ๐)) |
26 | | lgsqr.s |
. . . . 5
โข ๐ = (Poly1โ๐) |
27 | | lgsqr.b |
. . . . 5
โข ๐ต = (Baseโ๐) |
28 | | lgsqr.d |
. . . . 5
โข ๐ท = ( deg1
โ๐) |
29 | | lgsqr.o |
. . . . 5
โข ๐ = (eval1โ๐) |
30 | | lgsqr.e |
. . . . 5
โข โ =
(.gโ(mulGrpโ๐)) |
31 | | lgsqr.x |
. . . . 5
โข ๐ = (var1โ๐) |
32 | | lgsqr.m |
. . . . 5
โข โ =
(-gโ๐) |
33 | | lgsqr.u |
. . . . 5
โข 1 =
(1rโ๐) |
34 | | lgsqr.t |
. . . . 5
โข ๐ = ((((๐ โ 1) / 2) โ ๐) โ 1 ) |
35 | 1 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ ๐ โ (โ โ
{2})) |
36 | | elfznn 13471 |
. . . . . . . . . . 11
โข (๐ฆ โ (1...((๐ โ 1) / 2)) โ ๐ฆ โ โ) |
37 | 36 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ ๐ฆ โ โ) |
38 | 37 | nncnd 12170 |
. . . . . . . . 9
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ ๐ฆ โ โ) |
39 | | oddprm 16683 |
. . . . . . . . . . . 12
โข (๐ โ (โ โ {2})
โ ((๐ โ 1) / 2)
โ โ) |
40 | 1, 39 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ((๐ โ 1) / 2) โ
โ) |
41 | 40 | nnnn0d 12474 |
. . . . . . . . . 10
โข (๐ โ ((๐ โ 1) / 2) โ
โ0) |
42 | 41 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ ((๐ โ 1) / 2) โ
โ0) |
43 | | 2nn0 12431 |
. . . . . . . . . 10
โข 2 โ
โ0 |
44 | 43 | a1i 11 |
. . . . . . . . 9
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ 2 โ
โ0) |
45 | 38, 42, 44 | expmuld 14055 |
. . . . . . . 8
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ (๐ฆโ(2 ยท ((๐ โ 1) / 2))) = ((๐ฆโ2)โ((๐ โ 1) /
2))) |
46 | | prmnn 16551 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ๐ โ
โ) |
47 | 2, 46 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ โ) |
48 | 47 | nnred 12169 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ โ) |
49 | | peano2rem 11469 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ โ 1) โ โ) |
51 | 50 | recnd 11184 |
. . . . . . . . . . . 12
โข (๐ โ (๐ โ 1) โ โ) |
52 | | 2cnd 12232 |
. . . . . . . . . . . 12
โข (๐ โ 2 โ
โ) |
53 | | 2ne0 12258 |
. . . . . . . . . . . . 13
โข 2 โ
0 |
54 | 53 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 2 โ 0) |
55 | 51, 52, 54 | divcan2d 11934 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท ((๐ โ 1) / 2)) = (๐ โ 1)) |
56 | | phiprm 16650 |
. . . . . . . . . . . 12
โข (๐ โ โ โ
(ฯโ๐) = (๐ โ 1)) |
57 | 2, 56 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (ฯโ๐) = (๐ โ 1)) |
58 | 55, 57 | eqtr4d 2780 |
. . . . . . . . . 10
โข (๐ โ (2 ยท ((๐ โ 1) / 2)) =
(ฯโ๐)) |
59 | 58 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ (2 ยท
((๐ โ 1) / 2)) =
(ฯโ๐)) |
60 | 59 | oveq2d 7374 |
. . . . . . . 8
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ (๐ฆโ(2 ยท ((๐ โ 1) / 2))) = (๐ฆโ(ฯโ๐))) |
61 | 45, 60 | eqtr3d 2779 |
. . . . . . 7
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ ((๐ฆโ2)โ((๐ โ 1) / 2)) = (๐ฆโ(ฯโ๐))) |
62 | 61 | oveq1d 7373 |
. . . . . 6
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ (((๐ฆโ2)โ((๐ โ 1) / 2)) mod ๐) = ((๐ฆโ(ฯโ๐)) mod ๐)) |
63 | 2 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ ๐ โ โ) |
64 | 63, 46 | syl 17 |
. . . . . . 7
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ ๐ โ โ) |
65 | 47 | nnzd 12527 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โค) |
66 | 65 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ ๐ โ โค) |
67 | 22, 66 | gcdcomd 16395 |
. . . . . . . 8
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ (๐ฆ gcd ๐) = (๐ gcd ๐ฆ)) |
68 | 37 | nnred 12169 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ ๐ฆ โ โ) |
69 | 50 | rehalfcld 12401 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ โ 1) / 2) โ
โ) |
70 | 69 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ ((๐ โ 1) / 2) โ
โ) |
71 | 48 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ ๐ โ โ) |
72 | | elfzle2 13446 |
. . . . . . . . . . . . 13
โข (๐ฆ โ (1...((๐ โ 1) / 2)) โ ๐ฆ โค ((๐ โ 1) / 2)) |
73 | 72 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ ๐ฆ โค ((๐ โ 1) / 2)) |
74 | | prmuz2 16573 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
75 | 2, 74 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ โ
(โคโฅโ2)) |
76 | | uz2m1nn 12849 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ
(โคโฅโ2) โ (๐ โ 1) โ โ) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ โ 1) โ โ) |
78 | 77 | nnrpd 12956 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ โ 1) โ
โ+) |
79 | | rphalflt 12945 |
. . . . . . . . . . . . . . 15
โข ((๐ โ 1) โ
โ+ โ ((๐ โ 1) / 2) < (๐ โ 1)) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ โ 1) / 2) < (๐ โ 1)) |
81 | 48 | ltm1d 12088 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ โ 1) < ๐) |
82 | 69, 50, 48, 80, 81 | lttrd 11317 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ โ 1) / 2) < ๐) |
83 | 82 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ ((๐ โ 1) / 2) < ๐) |
84 | 68, 70, 71, 73, 83 | lelttrd 11314 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ ๐ฆ < ๐) |
85 | 68, 71 | ltnled 11303 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ (๐ฆ < ๐ โ ยฌ ๐ โค ๐ฆ)) |
86 | 84, 85 | mpbid 231 |
. . . . . . . . . 10
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ ยฌ ๐ โค ๐ฆ) |
87 | | dvdsle 16193 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ฆ โ โ) โ (๐ โฅ ๐ฆ โ ๐ โค ๐ฆ)) |
88 | 66, 37, 87 | syl2anc 585 |
. . . . . . . . . 10
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ (๐ โฅ ๐ฆ โ ๐ โค ๐ฆ)) |
89 | 86, 88 | mtod 197 |
. . . . . . . . 9
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ ยฌ ๐ โฅ ๐ฆ) |
90 | | coprm 16588 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ฆ โ โค) โ (ยฌ
๐ โฅ ๐ฆ โ (๐ gcd ๐ฆ) = 1)) |
91 | 63, 22, 90 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ (ยฌ ๐ โฅ ๐ฆ โ (๐ gcd ๐ฆ) = 1)) |
92 | 89, 91 | mpbid 231 |
. . . . . . . 8
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ (๐ gcd ๐ฆ) = 1) |
93 | 67, 92 | eqtrd 2777 |
. . . . . . 7
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ (๐ฆ gcd ๐) = 1) |
94 | | eulerth 16656 |
. . . . . . 7
โข ((๐ โ โ โง ๐ฆ โ โค โง (๐ฆ gcd ๐) = 1) โ ((๐ฆโ(ฯโ๐)) mod ๐) = (1 mod ๐)) |
95 | 64, 22, 93, 94 | syl3anc 1372 |
. . . . . 6
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ ((๐ฆโ(ฯโ๐)) mod ๐) = (1 mod ๐)) |
96 | 62, 95 | eqtrd 2777 |
. . . . 5
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ (((๐ฆโ2)โ((๐ โ 1) / 2)) mod ๐) = (1 mod ๐)) |
97 | 3, 26, 27, 28, 29, 30, 31, 32, 33, 34, 13, 35, 24, 96 | lgsqrlem1 26697 |
. . . 4
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ ((๐โ๐)โ(๐ฟโ(๐ฆโ2))) = (0gโ๐)) |
98 | | eqid 2737 |
. . . . . . . 8
โข (๐ โs
(Baseโ๐)) = (๐ โs
(Baseโ๐)) |
99 | | eqid 2737 |
. . . . . . . 8
โข
(Baseโ(๐
โs (Baseโ๐))) = (Baseโ(๐ โs (Baseโ๐))) |
100 | | fvexd 6858 |
. . . . . . . 8
โข (๐ โ (Baseโ๐) โ V) |
101 | 29, 26, 98, 17 | evl1rhm 21701 |
. . . . . . . . . . 11
โข (๐ โ CRing โ ๐ โ (๐ RingHom (๐ โs (Baseโ๐)))) |
102 | 10, 101 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ๐ โ (๐ RingHom (๐ โs (Baseโ๐)))) |
103 | 27, 99 | rhmf 20159 |
. . . . . . . . . 10
โข (๐ โ (๐ RingHom (๐ โs (Baseโ๐))) โ ๐:๐ตโถ(Baseโ(๐ โs (Baseโ๐)))) |
104 | 102, 103 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐:๐ตโถ(Baseโ(๐ โs (Baseโ๐)))) |
105 | 26 | ply1ring 21622 |
. . . . . . . . . . . . 13
โข (๐ โ Ring โ ๐ โ Ring) |
106 | 12, 105 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ Ring) |
107 | | ringgrp 19970 |
. . . . . . . . . . . 12
โข (๐ โ Ring โ ๐ โ Grp) |
108 | 106, 107 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ Grp) |
109 | | eqid 2737 |
. . . . . . . . . . . . 13
โข
(mulGrpโ๐) =
(mulGrpโ๐) |
110 | 109, 27 | mgpbas 19903 |
. . . . . . . . . . . 12
โข ๐ต =
(Baseโ(mulGrpโ๐)) |
111 | 109 | ringmgp 19971 |
. . . . . . . . . . . . 13
โข (๐ โ Ring โ
(mulGrpโ๐) โ
Mnd) |
112 | 106, 111 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ (mulGrpโ๐) โ Mnd) |
113 | 31, 26, 27 | vr1cl 21591 |
. . . . . . . . . . . . 13
โข (๐ โ Ring โ ๐ โ ๐ต) |
114 | 12, 113 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ ๐ต) |
115 | 110, 30, 112, 41, 114 | mulgnn0cld 18898 |
. . . . . . . . . . 11
โข (๐ โ (((๐ โ 1) / 2) โ ๐) โ ๐ต) |
116 | 27, 33 | ringidcl 19990 |
. . . . . . . . . . . 12
โข (๐ โ Ring โ 1 โ ๐ต) |
117 | 106, 116 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ 1 โ ๐ต) |
118 | 27, 32 | grpsubcl 18828 |
. . . . . . . . . . 11
โข ((๐ โ Grp โง (((๐ โ 1) / 2) โ ๐) โ ๐ต โง 1 โ ๐ต) โ ((((๐ โ 1) / 2) โ ๐) โ 1 ) โ ๐ต) |
119 | 108, 115,
117, 118 | syl3anc 1372 |
. . . . . . . . . 10
โข (๐ โ ((((๐ โ 1) / 2) โ ๐) โ 1 ) โ ๐ต) |
120 | 34, 119 | eqeltrid 2842 |
. . . . . . . . 9
โข (๐ โ ๐ โ ๐ต) |
121 | 104, 120 | ffvelcdmd 7037 |
. . . . . . . 8
โข (๐ โ (๐โ๐) โ (Baseโ(๐ โs (Baseโ๐)))) |
122 | 98, 17, 99, 5, 100, 121 | pwselbas 17372 |
. . . . . . 7
โข (๐ โ (๐โ๐):(Baseโ๐)โถ(Baseโ๐)) |
123 | 122 | ffnd 6670 |
. . . . . 6
โข (๐ โ (๐โ๐) Fn (Baseโ๐)) |
124 | 123 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ (๐โ๐) Fn (Baseโ๐)) |
125 | | fniniseg 7011 |
. . . . 5
โข ((๐โ๐) Fn (Baseโ๐) โ ((๐ฟโ(๐ฆโ2)) โ (โก(๐โ๐) โ {(0gโ๐)}) โ ((๐ฟโ(๐ฆโ2)) โ (Baseโ๐) โง ((๐โ๐)โ(๐ฟโ(๐ฆโ2))) = (0gโ๐)))) |
126 | 124, 125 | syl 17 |
. . . 4
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ ((๐ฟโ(๐ฆโ2)) โ (โก(๐โ๐) โ {(0gโ๐)}) โ ((๐ฟโ(๐ฆโ2)) โ (Baseโ๐) โง ((๐โ๐)โ(๐ฟโ(๐ฆโ2))) = (0gโ๐)))) |
127 | 25, 97, 126 | mpbir2and 712 |
. . 3
โข ((๐ โง ๐ฆ โ (1...((๐ โ 1) / 2))) โ (๐ฟโ(๐ฆโ2)) โ (โก(๐โ๐) โ {(0gโ๐)})) |
128 | | lgsqr.g |
. . 3
โข ๐บ = (๐ฆ โ (1...((๐ โ 1) / 2)) โฆ (๐ฟโ(๐ฆโ2))) |
129 | 127, 128 | fmptd 7063 |
. 2
โข (๐ โ ๐บ:(1...((๐ โ 1) / 2))โถ(โก(๐โ๐) โ {(0gโ๐)})) |
130 | | fvoveq1 7381 |
. . . . . . . 8
โข (๐ฆ = ๐ฅ โ (๐ฟโ(๐ฆโ2)) = (๐ฟโ(๐ฅโ2))) |
131 | | fvex 6856 |
. . . . . . . 8
โข (๐ฟโ(๐ฅโ2)) โ V |
132 | 130, 128,
131 | fvmpt 6949 |
. . . . . . 7
โข (๐ฅ โ (1...((๐ โ 1) / 2)) โ (๐บโ๐ฅ) = (๐ฟโ(๐ฅโ2))) |
133 | 132 | ad2antrl 727 |
. . . . . 6
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐บโ๐ฅ) = (๐ฟโ(๐ฅโ2))) |
134 | | fvoveq1 7381 |
. . . . . . . 8
โข (๐ฆ = ๐ง โ (๐ฟโ(๐ฆโ2)) = (๐ฟโ(๐งโ2))) |
135 | | fvex 6856 |
. . . . . . . 8
โข (๐ฟโ(๐งโ2)) โ V |
136 | 134, 128,
135 | fvmpt 6949 |
. . . . . . 7
โข (๐ง โ (1...((๐ โ 1) / 2)) โ (๐บโ๐ง) = (๐ฟโ(๐งโ2))) |
137 | 136 | ad2antll 728 |
. . . . . 6
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐บโ๐ง) = (๐ฟโ(๐งโ2))) |
138 | 133, 137 | eqeq12d 2753 |
. . . . 5
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ((๐บโ๐ฅ) = (๐บโ๐ง) โ (๐ฟโ(๐ฅโ2)) = (๐ฟโ(๐งโ2)))) |
139 | 47 | nnnn0d 12474 |
. . . . . . 7
โข (๐ โ ๐ โ
โ0) |
140 | 139 | adantr 482 |
. . . . . 6
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ๐ โ
โ0) |
141 | | elfzelz 13442 |
. . . . . . . 8
โข (๐ฅ โ (1...((๐ โ 1) / 2)) โ ๐ฅ โ โค) |
142 | 141 | ad2antrl 727 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ๐ฅ โ
โค) |
143 | | zsqcl 14035 |
. . . . . . 7
โข (๐ฅ โ โค โ (๐ฅโ2) โ
โค) |
144 | 142, 143 | syl 17 |
. . . . . 6
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐ฅโ2) โ
โค) |
145 | | elfzelz 13442 |
. . . . . . . 8
โข (๐ง โ (1...((๐ โ 1) / 2)) โ ๐ง โ โค) |
146 | 145 | ad2antll 728 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ๐ง โ
โค) |
147 | | zsqcl 14035 |
. . . . . . 7
โข (๐ง โ โค โ (๐งโ2) โ
โค) |
148 | 146, 147 | syl 17 |
. . . . . 6
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐งโ2) โ
โค) |
149 | 3, 13 | zndvds 20959 |
. . . . . 6
โข ((๐ โ โ0
โง (๐ฅโ2) โ
โค โง (๐งโ2)
โ โค) โ ((๐ฟโ(๐ฅโ2)) = (๐ฟโ(๐งโ2)) โ ๐ โฅ ((๐ฅโ2) โ (๐งโ2)))) |
150 | 140, 144,
148, 149 | syl3anc 1372 |
. . . . 5
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ((๐ฟโ(๐ฅโ2)) = (๐ฟโ(๐งโ2)) โ ๐ โฅ ((๐ฅโ2) โ (๐งโ2)))) |
151 | | elfznn 13471 |
. . . . . . . . 9
โข (๐ฅ โ (1...((๐ โ 1) / 2)) โ ๐ฅ โ โ) |
152 | 151 | ad2antrl 727 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ๐ฅ โ
โ) |
153 | 152 | nncnd 12170 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ๐ฅ โ
โ) |
154 | | elfznn 13471 |
. . . . . . . . 9
โข (๐ง โ (1...((๐ โ 1) / 2)) โ ๐ง โ โ) |
155 | 154 | ad2antll 728 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ๐ง โ
โ) |
156 | 155 | nncnd 12170 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ๐ง โ
โ) |
157 | | subsq 14115 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ง โ โ) โ ((๐ฅโ2) โ (๐งโ2)) = ((๐ฅ + ๐ง) ยท (๐ฅ โ ๐ง))) |
158 | 153, 156,
157 | syl2anc 585 |
. . . . . 6
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ((๐ฅโ2) โ (๐งโ2)) = ((๐ฅ + ๐ง) ยท (๐ฅ โ ๐ง))) |
159 | 158 | breq2d 5118 |
. . . . 5
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐ โฅ ((๐ฅโ2) โ (๐งโ2)) โ ๐ โฅ ((๐ฅ + ๐ง) ยท (๐ฅ โ ๐ง)))) |
160 | 138, 150,
159 | 3bitrd 305 |
. . . 4
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ((๐บโ๐ฅ) = (๐บโ๐ง) โ ๐ โฅ ((๐ฅ + ๐ง) ยท (๐ฅ โ ๐ง)))) |
161 | 2 | adantr 482 |
. . . . . 6
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ๐ โ โ) |
162 | 142, 146 | zaddcld 12612 |
. . . . . 6
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐ฅ + ๐ง) โ โค) |
163 | 142, 146 | zsubcld 12613 |
. . . . . 6
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐ฅ โ ๐ง) โ โค) |
164 | | euclemma 16590 |
. . . . . 6
โข ((๐ โ โ โง (๐ฅ + ๐ง) โ โค โง (๐ฅ โ ๐ง) โ โค) โ (๐ โฅ ((๐ฅ + ๐ง) ยท (๐ฅ โ ๐ง)) โ (๐ โฅ (๐ฅ + ๐ง) โจ ๐ โฅ (๐ฅ โ ๐ง)))) |
165 | 161, 162,
163, 164 | syl3anc 1372 |
. . . . 5
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐ โฅ ((๐ฅ + ๐ง) ยท (๐ฅ โ ๐ง)) โ (๐ โฅ (๐ฅ + ๐ง) โจ ๐ โฅ (๐ฅ โ ๐ง)))) |
166 | 161, 46 | syl 17 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ๐ โ โ) |
167 | 166 | nnzd 12527 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ๐ โ โค) |
168 | 152, 155 | nnaddcld 12206 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐ฅ + ๐ง) โ โ) |
169 | | dvdsle 16193 |
. . . . . . . 8
โข ((๐ โ โค โง (๐ฅ + ๐ง) โ โ) โ (๐ โฅ (๐ฅ + ๐ง) โ ๐ โค (๐ฅ + ๐ง))) |
170 | 167, 168,
169 | syl2anc 585 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐ โฅ (๐ฅ + ๐ง) โ ๐ โค (๐ฅ + ๐ง))) |
171 | 168 | nnred 12169 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐ฅ + ๐ง) โ โ) |
172 | 166 | nnred 12169 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ๐ โ โ) |
173 | 172, 49 | syl 17 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐ โ 1) โ
โ) |
174 | 152 | nnred 12169 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ๐ฅ โ
โ) |
175 | 155 | nnred 12169 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ๐ง โ
โ) |
176 | 69 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ((๐ โ 1) / 2) โ
โ) |
177 | | elfzle2 13446 |
. . . . . . . . . . . . 13
โข (๐ฅ โ (1...((๐ โ 1) / 2)) โ ๐ฅ โค ((๐ โ 1) / 2)) |
178 | 177 | ad2antrl 727 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ๐ฅ โค ((๐ โ 1) / 2)) |
179 | | elfzle2 13446 |
. . . . . . . . . . . . 13
โข (๐ง โ (1...((๐ โ 1) / 2)) โ ๐ง โค ((๐ โ 1) / 2)) |
180 | 179 | ad2antll 728 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ๐ง โค ((๐ โ 1) / 2)) |
181 | 174, 175,
176, 176, 178, 180 | le2addd 11775 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐ฅ + ๐ง) โค (((๐ โ 1) / 2) + ((๐ โ 1) / 2))) |
182 | 51 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐ โ 1) โ
โ) |
183 | 182 | 2halvesd 12400 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (((๐ โ 1) / 2) + ((๐ โ 1) / 2)) = (๐ โ 1)) |
184 | 181, 183 | breqtrd 5132 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐ฅ + ๐ง) โค (๐ โ 1)) |
185 | 172 | ltm1d 12088 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐ โ 1) < ๐) |
186 | 171, 173,
172, 184, 185 | lelttrd 11314 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐ฅ + ๐ง) < ๐) |
187 | 171, 172 | ltnled 11303 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ((๐ฅ + ๐ง) < ๐ โ ยฌ ๐ โค (๐ฅ + ๐ง))) |
188 | 186, 187 | mpbid 231 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ยฌ ๐ โค (๐ฅ + ๐ง)) |
189 | 188 | pm2.21d 121 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐ โค (๐ฅ + ๐ง) โ ๐ฅ = ๐ง)) |
190 | 170, 189 | syld 47 |
. . . . . 6
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐ โฅ (๐ฅ + ๐ง) โ ๐ฅ = ๐ง)) |
191 | | moddvds 16148 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ฅ โ โค โง ๐ง โ โค) โ ((๐ฅ mod ๐) = (๐ง mod ๐) โ ๐ โฅ (๐ฅ โ ๐ง))) |
192 | 166, 142,
146, 191 | syl3anc 1372 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ((๐ฅ mod ๐) = (๐ง mod ๐) โ ๐ โฅ (๐ฅ โ ๐ง))) |
193 | 166 | nnrpd 12956 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ๐ โ
โ+) |
194 | 152 | nnnn0d 12474 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ๐ฅ โ
โ0) |
195 | 194 | nn0ge0d 12477 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ 0 โค ๐ฅ) |
196 | 82 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ((๐ โ 1) / 2) < ๐) |
197 | 174, 176,
172, 178, 196 | lelttrd 11314 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ๐ฅ < ๐) |
198 | | modid 13802 |
. . . . . . . . . 10
โข (((๐ฅ โ โ โง ๐ โ โ+)
โง (0 โค ๐ฅ โง ๐ฅ < ๐)) โ (๐ฅ mod ๐) = ๐ฅ) |
199 | 174, 193,
195, 197, 198 | syl22anc 838 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐ฅ mod ๐) = ๐ฅ) |
200 | 155 | nnnn0d 12474 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ๐ง โ
โ0) |
201 | 200 | nn0ge0d 12477 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ 0 โค ๐ง) |
202 | 175, 176,
172, 180, 196 | lelttrd 11314 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ๐ง < ๐) |
203 | | modid 13802 |
. . . . . . . . . 10
โข (((๐ง โ โ โง ๐ โ โ+)
โง (0 โค ๐ง โง ๐ง < ๐)) โ (๐ง mod ๐) = ๐ง) |
204 | 175, 193,
201, 202, 203 | syl22anc 838 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐ง mod ๐) = ๐ง) |
205 | 199, 204 | eqeq12d 2753 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ((๐ฅ mod ๐) = (๐ง mod ๐) โ ๐ฅ = ๐ง)) |
206 | 192, 205 | bitr3d 281 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐ โฅ (๐ฅ โ ๐ง) โ ๐ฅ = ๐ง)) |
207 | 206 | biimpd 228 |
. . . . . 6
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐ โฅ (๐ฅ โ ๐ง) โ ๐ฅ = ๐ง)) |
208 | 190, 207 | jaod 858 |
. . . . 5
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ((๐ โฅ (๐ฅ + ๐ง) โจ ๐ โฅ (๐ฅ โ ๐ง)) โ ๐ฅ = ๐ง)) |
209 | 165, 208 | sylbid 239 |
. . . 4
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ (๐ โฅ ((๐ฅ + ๐ง) ยท (๐ฅ โ ๐ง)) โ ๐ฅ = ๐ง)) |
210 | 160, 209 | sylbid 239 |
. . 3
โข ((๐ โง (๐ฅ โ (1...((๐ โ 1) / 2)) โง ๐ง โ (1...((๐ โ 1) / 2)))) โ ((๐บโ๐ฅ) = (๐บโ๐ง) โ ๐ฅ = ๐ง)) |
211 | 210 | ralrimivva 3198 |
. 2
โข (๐ โ โ๐ฅ โ (1...((๐ โ 1) / 2))โ๐ง โ (1...((๐ โ 1) / 2))((๐บโ๐ฅ) = (๐บโ๐ง) โ ๐ฅ = ๐ง)) |
212 | | dff13 7203 |
. 2
โข (๐บ:(1...((๐ โ 1) / 2))โ1-1โ(โก(๐โ๐) โ {(0gโ๐)}) โ (๐บ:(1...((๐ โ 1) / 2))โถ(โก(๐โ๐) โ {(0gโ๐)}) โง โ๐ฅ โ (1...((๐ โ 1) / 2))โ๐ง โ (1...((๐ โ 1) / 2))((๐บโ๐ฅ) = (๐บโ๐ง) โ ๐ฅ = ๐ง))) |
213 | 129, 211,
212 | sylanbrc 584 |
1
โข (๐ โ ๐บ:(1...((๐ โ 1) / 2))โ1-1โ(โก(๐โ๐) โ {(0gโ๐)})) |