Step | Hyp | Ref
| Expression |
1 | | eulerth.1 |
. . . . . 6
โข (๐ โ (๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1)) |
2 | 1 | simp1d 1009 |
. . . . 5
โข (๐ โ ๐ โ โ) |
3 | 2 | phicld 12218 |
. . . 4
โข (๐ โ (ฯโ๐) โ
โ) |
4 | | elnnuz 9564 |
. . . 4
โข
((ฯโ๐)
โ โ โ (ฯโ๐) โ
(โคโฅโ1)) |
5 | 3, 4 | sylib 122 |
. . 3
โข (๐ โ (ฯโ๐) โ
(โคโฅโ1)) |
6 | | eluzfz2 10032 |
. . 3
โข
((ฯโ๐)
โ (โคโฅโ1) โ (ฯโ๐) โ (1...(ฯโ๐))) |
7 | 5, 6 | syl 14 |
. 2
โข (๐ โ (ฯโ๐) โ
(1...(ฯโ๐))) |
8 | | oveq2 5883 |
. . . . . . 7
โข (๐ค = 1 โ (1...๐ค) = (1...1)) |
9 | 8 | prodeq1d 11572 |
. . . . . 6
โข (๐ค = 1 โ โ๐ฅ โ (1...๐ค)(๐นโ๐ฅ) = โ๐ฅ โ (1...1)(๐นโ๐ฅ)) |
10 | 9 | oveq2d 5891 |
. . . . 5
โข (๐ค = 1 โ (๐ gcd โ๐ฅ โ (1...๐ค)(๐นโ๐ฅ)) = (๐ gcd โ๐ฅ โ (1...1)(๐นโ๐ฅ))) |
11 | 10 | eqeq1d 2186 |
. . . 4
โข (๐ค = 1 โ ((๐ gcd โ๐ฅ โ (1...๐ค)(๐นโ๐ฅ)) = 1 โ (๐ gcd โ๐ฅ โ (1...1)(๐นโ๐ฅ)) = 1)) |
12 | 11 | imbi2d 230 |
. . 3
โข (๐ค = 1 โ ((๐ โ (๐ gcd โ๐ฅ โ (1...๐ค)(๐นโ๐ฅ)) = 1) โ (๐ โ (๐ gcd โ๐ฅ โ (1...1)(๐นโ๐ฅ)) = 1))) |
13 | | oveq2 5883 |
. . . . . . 7
โข (๐ค = ๐ โ (1...๐ค) = (1...๐)) |
14 | 13 | prodeq1d 11572 |
. . . . . 6
โข (๐ค = ๐ โ โ๐ฅ โ (1...๐ค)(๐นโ๐ฅ) = โ๐ฅ โ (1...๐)(๐นโ๐ฅ)) |
15 | 14 | oveq2d 5891 |
. . . . 5
โข (๐ค = ๐ โ (๐ gcd โ๐ฅ โ (1...๐ค)(๐นโ๐ฅ)) = (๐ gcd โ๐ฅ โ (1...๐)(๐นโ๐ฅ))) |
16 | 15 | eqeq1d 2186 |
. . . 4
โข (๐ค = ๐ โ ((๐ gcd โ๐ฅ โ (1...๐ค)(๐นโ๐ฅ)) = 1 โ (๐ gcd โ๐ฅ โ (1...๐)(๐นโ๐ฅ)) = 1)) |
17 | 16 | imbi2d 230 |
. . 3
โข (๐ค = ๐ โ ((๐ โ (๐ gcd โ๐ฅ โ (1...๐ค)(๐นโ๐ฅ)) = 1) โ (๐ โ (๐ gcd โ๐ฅ โ (1...๐)(๐นโ๐ฅ)) = 1))) |
18 | | oveq2 5883 |
. . . . . . 7
โข (๐ค = (๐ + 1) โ (1...๐ค) = (1...(๐ + 1))) |
19 | 18 | prodeq1d 11572 |
. . . . . 6
โข (๐ค = (๐ + 1) โ โ๐ฅ โ (1...๐ค)(๐นโ๐ฅ) = โ๐ฅ โ (1...(๐ + 1))(๐นโ๐ฅ)) |
20 | 19 | oveq2d 5891 |
. . . . 5
โข (๐ค = (๐ + 1) โ (๐ gcd โ๐ฅ โ (1...๐ค)(๐นโ๐ฅ)) = (๐ gcd โ๐ฅ โ (1...(๐ + 1))(๐นโ๐ฅ))) |
21 | 20 | eqeq1d 2186 |
. . . 4
โข (๐ค = (๐ + 1) โ ((๐ gcd โ๐ฅ โ (1...๐ค)(๐นโ๐ฅ)) = 1 โ (๐ gcd โ๐ฅ โ (1...(๐ + 1))(๐นโ๐ฅ)) = 1)) |
22 | 21 | imbi2d 230 |
. . 3
โข (๐ค = (๐ + 1) โ ((๐ โ (๐ gcd โ๐ฅ โ (1...๐ค)(๐นโ๐ฅ)) = 1) โ (๐ โ (๐ gcd โ๐ฅ โ (1...(๐ + 1))(๐นโ๐ฅ)) = 1))) |
23 | | oveq2 5883 |
. . . . . . 7
โข (๐ค = (ฯโ๐) โ (1...๐ค) = (1...(ฯโ๐))) |
24 | 23 | prodeq1d 11572 |
. . . . . 6
โข (๐ค = (ฯโ๐) โ โ๐ฅ โ (1...๐ค)(๐นโ๐ฅ) = โ๐ฅ โ (1...(ฯโ๐))(๐นโ๐ฅ)) |
25 | 24 | oveq2d 5891 |
. . . . 5
โข (๐ค = (ฯโ๐) โ (๐ gcd โ๐ฅ โ (1...๐ค)(๐นโ๐ฅ)) = (๐ gcd โ๐ฅ โ (1...(ฯโ๐))(๐นโ๐ฅ))) |
26 | 25 | eqeq1d 2186 |
. . . 4
โข (๐ค = (ฯโ๐) โ ((๐ gcd โ๐ฅ โ (1...๐ค)(๐นโ๐ฅ)) = 1 โ (๐ gcd โ๐ฅ โ (1...(ฯโ๐))(๐นโ๐ฅ)) = 1)) |
27 | 26 | imbi2d 230 |
. . 3
โข (๐ค = (ฯโ๐) โ ((๐ โ (๐ gcd โ๐ฅ โ (1...๐ค)(๐นโ๐ฅ)) = 1) โ (๐ โ (๐ gcd โ๐ฅ โ (1...(ฯโ๐))(๐นโ๐ฅ)) = 1))) |
28 | | 1z 9279 |
. . . . . . 7
โข 1 โ
โค |
29 | | eulerth.2 |
. . . . . . . . . . 11
โข ๐ = {๐ฆ โ (0..^๐) โฃ (๐ฆ gcd ๐) = 1} |
30 | | ssrab2 3241 |
. . . . . . . . . . 11
โข {๐ฆ โ (0..^๐) โฃ (๐ฆ gcd ๐) = 1} โ (0..^๐) |
31 | 29, 30 | eqsstri 3188 |
. . . . . . . . . 10
โข ๐ โ (0..^๐) |
32 | | fzo0ssnn0 10215 |
. . . . . . . . . 10
โข
(0..^๐) โ
โ0 |
33 | 31, 32 | sstri 3165 |
. . . . . . . . 9
โข ๐ โ
โ0 |
34 | | nn0sscn 9181 |
. . . . . . . . 9
โข
โ0 โ โ |
35 | 33, 34 | sstri 3165 |
. . . . . . . 8
โข ๐ โ
โ |
36 | | eulerth.4 |
. . . . . . . . . 10
โข (๐ โ ๐น:(1...(ฯโ๐))โ1-1-ontoโ๐) |
37 | | f1of 5462 |
. . . . . . . . . 10
โข (๐น:(1...(ฯโ๐))โ1-1-ontoโ๐ โ ๐น:(1...(ฯโ๐))โถ๐) |
38 | 36, 37 | syl 14 |
. . . . . . . . 9
โข (๐ โ ๐น:(1...(ฯโ๐))โถ๐) |
39 | 3 | nnge1d 8962 |
. . . . . . . . . 10
โข (๐ โ 1 โค (ฯโ๐)) |
40 | | uzid 9542 |
. . . . . . . . . . . 12
โข (1 โ
โค โ 1 โ (โคโฅโ1)) |
41 | 28, 40 | ax-mp 5 |
. . . . . . . . . . 11
โข 1 โ
(โคโฅโ1) |
42 | 3 | nnzd 9374 |
. . . . . . . . . . 11
โข (๐ โ (ฯโ๐) โ
โค) |
43 | | elfz5 10017 |
. . . . . . . . . . 11
โข ((1
โ (โคโฅโ1) โง (ฯโ๐) โ โค) โ (1 โ
(1...(ฯโ๐))
โ 1 โค (ฯโ๐))) |
44 | 41, 42, 43 | sylancr 414 |
. . . . . . . . . 10
โข (๐ โ (1 โ
(1...(ฯโ๐))
โ 1 โค (ฯโ๐))) |
45 | 39, 44 | mpbird 167 |
. . . . . . . . 9
โข (๐ โ 1 โ
(1...(ฯโ๐))) |
46 | 38, 45 | ffvelcdmd 5653 |
. . . . . . . 8
โข (๐ โ (๐นโ1) โ ๐) |
47 | 35, 46 | sselid 3154 |
. . . . . . 7
โข (๐ โ (๐นโ1) โ โ) |
48 | | fveq2 5516 |
. . . . . . . 8
โข (๐ฅ = 1 โ (๐นโ๐ฅ) = (๐นโ1)) |
49 | 48 | fprod1 11602 |
. . . . . . 7
โข ((1
โ โค โง (๐นโ1) โ โ) โ
โ๐ฅ โ
(1...1)(๐นโ๐ฅ) = (๐นโ1)) |
50 | 28, 47, 49 | sylancr 414 |
. . . . . 6
โข (๐ โ โ๐ฅ โ (1...1)(๐นโ๐ฅ) = (๐นโ1)) |
51 | 50 | oveq2d 5891 |
. . . . 5
โข (๐ โ (๐ gcd โ๐ฅ โ (1...1)(๐นโ๐ฅ)) = (๐ gcd (๐นโ1))) |
52 | 2 | nnzd 9374 |
. . . . . 6
โข (๐ โ ๐ โ โค) |
53 | | nn0ssz 9271 |
. . . . . . . 8
โข
โ0 โ โค |
54 | 33, 53 | sstri 3165 |
. . . . . . 7
โข ๐ โ
โค |
55 | 54, 46 | sselid 3154 |
. . . . . 6
โข (๐ โ (๐นโ1) โ โค) |
56 | | gcdcom 11974 |
. . . . . 6
โข ((๐ โ โค โง (๐นโ1) โ โค) โ
(๐ gcd (๐นโ1)) = ((๐นโ1) gcd ๐)) |
57 | 52, 55, 56 | syl2anc 411 |
. . . . 5
โข (๐ โ (๐ gcd (๐นโ1)) = ((๐นโ1) gcd ๐)) |
58 | | oveq1 5882 |
. . . . . . . . 9
โข (๐ฆ = (๐นโ1) โ (๐ฆ gcd ๐) = ((๐นโ1) gcd ๐)) |
59 | 58 | eqeq1d 2186 |
. . . . . . . 8
โข (๐ฆ = (๐นโ1) โ ((๐ฆ gcd ๐) = 1 โ ((๐นโ1) gcd ๐) = 1)) |
60 | 59, 29 | elrab2 2897 |
. . . . . . 7
โข ((๐นโ1) โ ๐ โ ((๐นโ1) โ (0..^๐) โง ((๐นโ1) gcd ๐) = 1)) |
61 | 46, 60 | sylib 122 |
. . . . . 6
โข (๐ โ ((๐นโ1) โ (0..^๐) โง ((๐นโ1) gcd ๐) = 1)) |
62 | 61 | simprd 114 |
. . . . 5
โข (๐ โ ((๐นโ1) gcd ๐) = 1) |
63 | 51, 57, 62 | 3eqtrd 2214 |
. . . 4
โข (๐ โ (๐ gcd โ๐ฅ โ (1...1)(๐นโ๐ฅ)) = 1) |
64 | 63 | a1i 9 |
. . 3
โข
((ฯโ๐)
โ (โคโฅโ1) โ (๐ โ (๐ gcd โ๐ฅ โ (1...1)(๐นโ๐ฅ)) = 1)) |
65 | | simpr 110 |
. . . . . . . 8
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง (๐ gcd โ๐ฅ โ (1...๐)(๐นโ๐ฅ)) = 1) โ (๐ gcd โ๐ฅ โ (1...๐)(๐นโ๐ฅ)) = 1) |
66 | 38 | adantr 276 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (1..^(ฯโ๐))) โ ๐น:(1...(ฯโ๐))โถ๐) |
67 | | fzofzp1 10227 |
. . . . . . . . . . . . . 14
โข (๐ โ (1..^(ฯโ๐)) โ (๐ + 1) โ (1...(ฯโ๐))) |
68 | 67 | adantl 277 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (1..^(ฯโ๐))) โ (๐ + 1) โ (1...(ฯโ๐))) |
69 | 66, 68 | ffvelcdmd 5653 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (1..^(ฯโ๐))) โ (๐นโ(๐ + 1)) โ ๐) |
70 | 54, 69 | sselid 3154 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (1..^(ฯโ๐))) โ (๐นโ(๐ + 1)) โ โค) |
71 | 52 | adantr 276 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (1..^(ฯโ๐))) โ ๐ โ โค) |
72 | | gcdcom 11974 |
. . . . . . . . . . 11
โข (((๐นโ(๐ + 1)) โ โค โง ๐ โ โค) โ ((๐นโ(๐ + 1)) gcd ๐) = (๐ gcd (๐นโ(๐ + 1)))) |
73 | 70, 71, 72 | syl2anc 411 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (1..^(ฯโ๐))) โ ((๐นโ(๐ + 1)) gcd ๐) = (๐ gcd (๐นโ(๐ + 1)))) |
74 | | oveq1 5882 |
. . . . . . . . . . . . . 14
โข (๐ฆ = (๐นโ(๐ + 1)) โ (๐ฆ gcd ๐) = ((๐นโ(๐ + 1)) gcd ๐)) |
75 | 74 | eqeq1d 2186 |
. . . . . . . . . . . . 13
โข (๐ฆ = (๐นโ(๐ + 1)) โ ((๐ฆ gcd ๐) = 1 โ ((๐นโ(๐ + 1)) gcd ๐) = 1)) |
76 | 75, 29 | elrab2 2897 |
. . . . . . . . . . . 12
โข ((๐นโ(๐ + 1)) โ ๐ โ ((๐นโ(๐ + 1)) โ (0..^๐) โง ((๐นโ(๐ + 1)) gcd ๐) = 1)) |
77 | 76 | simprbi 275 |
. . . . . . . . . . 11
โข ((๐นโ(๐ + 1)) โ ๐ โ ((๐นโ(๐ + 1)) gcd ๐) = 1) |
78 | 69, 77 | syl 14 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (1..^(ฯโ๐))) โ ((๐นโ(๐ + 1)) gcd ๐) = 1) |
79 | 73, 78 | eqtr3d 2212 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (1..^(ฯโ๐))) โ (๐ gcd (๐นโ(๐ + 1))) = 1) |
80 | 79 | adantr 276 |
. . . . . . . 8
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง (๐ gcd โ๐ฅ โ (1...๐)(๐นโ๐ฅ)) = 1) โ (๐ gcd (๐นโ(๐ + 1))) = 1) |
81 | 28 | a1i 9 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (1..^(ฯโ๐))) โ 1 โ
โค) |
82 | | elfzoelz 10147 |
. . . . . . . . . . . . 13
โข (๐ โ (1..^(ฯโ๐)) โ ๐ โ โค) |
83 | 82 | adantl 277 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (1..^(ฯโ๐))) โ ๐ โ โค) |
84 | 81, 83 | fzfigd 10431 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (1..^(ฯโ๐))) โ (1...๐) โ Fin) |
85 | 38 | ad2antrr 488 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...๐)) โ ๐น:(1...(ฯโ๐))โถ๐) |
86 | | elfznn 10054 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ (1...๐) โ ๐ฅ โ โ) |
87 | 86 | nnred 8932 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ (1...๐) โ ๐ฅ โ โ) |
88 | 87 | adantl 277 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...๐)) โ ๐ฅ โ โ) |
89 | 3 | nnred 8932 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (ฯโ๐) โ
โ) |
90 | 89 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...๐)) โ (ฯโ๐) โ โ) |
91 | 82 | ad2antlr 489 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...๐)) โ ๐ โ โค) |
92 | 91 | zred 9375 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...๐)) โ ๐ โ โ) |
93 | | elfzle2 10028 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ (1...๐) โ ๐ฅ โค ๐) |
94 | 93 | adantl 277 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...๐)) โ ๐ฅ โค ๐) |
95 | | elfzolt2 10156 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (1..^(ฯโ๐)) โ ๐ < (ฯโ๐)) |
96 | 95 | ad2antlr 489 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...๐)) โ ๐ < (ฯโ๐)) |
97 | 88, 92, 90, 94, 96 | lelttrd 8082 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...๐)) โ ๐ฅ < (ฯโ๐)) |
98 | 88, 90, 97 | ltled 8076 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...๐)) โ ๐ฅ โค (ฯโ๐)) |
99 | | elfzuz 10021 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ (1...๐) โ ๐ฅ โ
(โคโฅโ1)) |
100 | 42 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...๐)) โ (ฯโ๐) โ โค) |
101 | | elfz5 10017 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ
(โคโฅโ1) โง (ฯโ๐) โ โค) โ (๐ฅ โ (1...(ฯโ๐)) โ ๐ฅ โค (ฯโ๐))) |
102 | 99, 100, 101 | syl2an2 594 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...๐)) โ (๐ฅ โ (1...(ฯโ๐)) โ ๐ฅ โค (ฯโ๐))) |
103 | 98, 102 | mpbird 167 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...๐)) โ ๐ฅ โ (1...(ฯโ๐))) |
104 | 85, 103 | ffvelcdmd 5653 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...๐)) โ (๐นโ๐ฅ) โ ๐) |
105 | 54, 104 | sselid 3154 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...๐)) โ (๐นโ๐ฅ) โ โค) |
106 | 84, 105 | fprodzcl 11617 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (1..^(ฯโ๐))) โ โ๐ฅ โ (1...๐)(๐นโ๐ฅ) โ โค) |
107 | | rpmul 12098 |
. . . . . . . . . 10
โข ((๐ โ โค โง
โ๐ฅ โ (1...๐)(๐นโ๐ฅ) โ โค โง (๐นโ(๐ + 1)) โ โค) โ (((๐ gcd โ๐ฅ โ (1...๐)(๐นโ๐ฅ)) = 1 โง (๐ gcd (๐นโ(๐ + 1))) = 1) โ (๐ gcd (โ๐ฅ โ (1...๐)(๐นโ๐ฅ) ยท (๐นโ(๐ + 1)))) = 1)) |
108 | 71, 106, 70, 107 | syl3anc 1238 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (1..^(ฯโ๐))) โ (((๐ gcd โ๐ฅ โ (1...๐)(๐นโ๐ฅ)) = 1 โง (๐ gcd (๐นโ(๐ + 1))) = 1) โ (๐ gcd (โ๐ฅ โ (1...๐)(๐นโ๐ฅ) ยท (๐นโ(๐ + 1)))) = 1)) |
109 | 108 | adantr 276 |
. . . . . . . 8
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง (๐ gcd โ๐ฅ โ (1...๐)(๐นโ๐ฅ)) = 1) โ (((๐ gcd โ๐ฅ โ (1...๐)(๐นโ๐ฅ)) = 1 โง (๐ gcd (๐นโ(๐ + 1))) = 1) โ (๐ gcd (โ๐ฅ โ (1...๐)(๐นโ๐ฅ) ยท (๐นโ(๐ + 1)))) = 1)) |
110 | 65, 80, 109 | mp2and 433 |
. . . . . . 7
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง (๐ gcd โ๐ฅ โ (1...๐)(๐นโ๐ฅ)) = 1) โ (๐ gcd (โ๐ฅ โ (1...๐)(๐นโ๐ฅ) ยท (๐นโ(๐ + 1)))) = 1) |
111 | | elfzouz 10151 |
. . . . . . . . . . . 12
โข (๐ โ (1..^(ฯโ๐)) โ ๐ โ
(โคโฅโ1)) |
112 | 111 | adantl 277 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (1..^(ฯโ๐))) โ ๐ โ
(โคโฅโ1)) |
113 | 38 | ad2antrr 488 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...(๐ + 1))) โ ๐น:(1...(ฯโ๐))โถ๐) |
114 | | elfzelz 10025 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ (1...(๐ + 1)) โ ๐ฅ โ โค) |
115 | 114 | zred 9375 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ (1...(๐ + 1)) โ ๐ฅ โ โ) |
116 | 115 | adantl 277 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...(๐ + 1))) โ ๐ฅ โ โ) |
117 | 82 | ad2antlr 489 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...(๐ + 1))) โ ๐ โ โค) |
118 | 117 | peano2zd 9378 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...(๐ + 1))) โ (๐ + 1) โ โค) |
119 | 118 | zred 9375 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...(๐ + 1))) โ (๐ + 1) โ โ) |
120 | 89 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...(๐ + 1))) โ (ฯโ๐) โ
โ) |
121 | | elfzle2 10028 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ (1...(๐ + 1)) โ ๐ฅ โค (๐ + 1)) |
122 | 121 | adantl 277 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...(๐ + 1))) โ ๐ฅ โค (๐ + 1)) |
123 | | elfzle2 10028 |
. . . . . . . . . . . . . . . . 17
โข ((๐ + 1) โ
(1...(ฯโ๐))
โ (๐ + 1) โค
(ฯโ๐)) |
124 | 67, 123 | syl 14 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1..^(ฯโ๐)) โ (๐ + 1) โค (ฯโ๐)) |
125 | 124 | ad2antlr 489 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...(๐ + 1))) โ (๐ + 1) โค (ฯโ๐)) |
126 | 116, 119,
120, 122, 125 | letrd 8081 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...(๐ + 1))) โ ๐ฅ โค (ฯโ๐)) |
127 | | elfzuz 10021 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ (1...(๐ + 1)) โ ๐ฅ โ
(โคโฅโ1)) |
128 | 42 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...(๐ + 1))) โ (ฯโ๐) โ
โค) |
129 | 127, 128,
101 | syl2an2 594 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...(๐ + 1))) โ (๐ฅ โ (1...(ฯโ๐)) โ ๐ฅ โค (ฯโ๐))) |
130 | 126, 129 | mpbird 167 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...(๐ + 1))) โ ๐ฅ โ (1...(ฯโ๐))) |
131 | 113, 130 | ffvelcdmd 5653 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...(๐ + 1))) โ (๐นโ๐ฅ) โ ๐) |
132 | 35, 131 | sselid 3154 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง ๐ฅ โ (1...(๐ + 1))) โ (๐นโ๐ฅ) โ โ) |
133 | | fveq2 5516 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ + 1) โ (๐นโ๐ฅ) = (๐นโ(๐ + 1))) |
134 | 112, 132,
133 | fprodp1 11608 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (1..^(ฯโ๐))) โ โ๐ฅ โ (1...(๐ + 1))(๐นโ๐ฅ) = (โ๐ฅ โ (1...๐)(๐นโ๐ฅ) ยท (๐นโ(๐ + 1)))) |
135 | 134 | oveq2d 5891 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (1..^(ฯโ๐))) โ (๐ gcd โ๐ฅ โ (1...(๐ + 1))(๐นโ๐ฅ)) = (๐ gcd (โ๐ฅ โ (1...๐)(๐นโ๐ฅ) ยท (๐นโ(๐ + 1))))) |
136 | 135 | eqeq1d 2186 |
. . . . . . . 8
โข ((๐ โง ๐ โ (1..^(ฯโ๐))) โ ((๐ gcd โ๐ฅ โ (1...(๐ + 1))(๐นโ๐ฅ)) = 1 โ (๐ gcd (โ๐ฅ โ (1...๐)(๐นโ๐ฅ) ยท (๐นโ(๐ + 1)))) = 1)) |
137 | 136 | adantr 276 |
. . . . . . 7
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง (๐ gcd โ๐ฅ โ (1...๐)(๐นโ๐ฅ)) = 1) โ ((๐ gcd โ๐ฅ โ (1...(๐ + 1))(๐นโ๐ฅ)) = 1 โ (๐ gcd (โ๐ฅ โ (1...๐)(๐นโ๐ฅ) ยท (๐นโ(๐ + 1)))) = 1)) |
138 | 110, 137 | mpbird 167 |
. . . . . 6
โข (((๐ โง ๐ โ (1..^(ฯโ๐))) โง (๐ gcd โ๐ฅ โ (1...๐)(๐นโ๐ฅ)) = 1) โ (๐ gcd โ๐ฅ โ (1...(๐ + 1))(๐นโ๐ฅ)) = 1) |
139 | 138 | ex 115 |
. . . . 5
โข ((๐ โง ๐ โ (1..^(ฯโ๐))) โ ((๐ gcd โ๐ฅ โ (1...๐)(๐นโ๐ฅ)) = 1 โ (๐ gcd โ๐ฅ โ (1...(๐ + 1))(๐นโ๐ฅ)) = 1)) |
140 | 139 | expcom 116 |
. . . 4
โข (๐ โ (1..^(ฯโ๐)) โ (๐ โ ((๐ gcd โ๐ฅ โ (1...๐)(๐นโ๐ฅ)) = 1 โ (๐ gcd โ๐ฅ โ (1...(๐ + 1))(๐นโ๐ฅ)) = 1))) |
141 | 140 | a2d 26 |
. . 3
โข (๐ โ (1..^(ฯโ๐)) โ ((๐ โ (๐ gcd โ๐ฅ โ (1...๐)(๐นโ๐ฅ)) = 1) โ (๐ โ (๐ gcd โ๐ฅ โ (1...(๐ + 1))(๐นโ๐ฅ)) = 1))) |
142 | 12, 17, 22, 27, 64, 141 | fzind2 10239 |
. 2
โข
((ฯโ๐)
โ (1...(ฯโ๐)) โ (๐ โ (๐ gcd โ๐ฅ โ (1...(ฯโ๐))(๐นโ๐ฅ)) = 1)) |
143 | 7, 142 | mpcom 36 |
1
โข (๐ โ (๐ gcd โ๐ฅ โ (1...(ฯโ๐))(๐นโ๐ฅ)) = 1) |