Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . 4
โข (((๐ โง 1 < (๐ gcd ๐
)) โง ๐
โค (๐
/ (๐ gcd ๐
))) โ ๐
โค (๐
/ (๐ gcd ๐
))) |
2 | | aks4d1p5.1 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ
(โคโฅโ3)) |
3 | | aks4d1p5.2 |
. . . . . . . . . . . . . 14
โข ๐ด = ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)) |
4 | | aks4d1p5.3 |
. . . . . . . . . . . . . 14
โข ๐ต = (โโ((2
logb ๐)โ5)) |
5 | | aks4d1p5.4 |
. . . . . . . . . . . . . 14
โข ๐
= inf({๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด}, โ, < ) |
6 | 2, 3, 4, 5 | aks4d1p4 40582 |
. . . . . . . . . . . . 13
โข (๐ โ (๐
โ (1...๐ต) โง ยฌ ๐
โฅ ๐ด)) |
7 | 6 | simpld 496 |
. . . . . . . . . . . 12
โข (๐ โ ๐
โ (1...๐ต)) |
8 | | elfznn 13476 |
. . . . . . . . . . . 12
โข (๐
โ (1...๐ต) โ ๐
โ โ) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ๐
โ โ) |
10 | 9 | nnred 12173 |
. . . . . . . . . 10
โข (๐ โ ๐
โ โ) |
11 | | eluzelz 12778 |
. . . . . . . . . . . . . . 15
โข (๐ โ
(โคโฅโ3) โ ๐ โ โค) |
12 | 2, 11 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ โค) |
13 | | 0red 11163 |
. . . . . . . . . . . . . . 15
โข (๐ โ 0 โ
โ) |
14 | | 3re 12238 |
. . . . . . . . . . . . . . . 16
โข 3 โ
โ |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ 3 โ
โ) |
16 | 12 | zred 12612 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ โ) |
17 | | 3pos 12263 |
. . . . . . . . . . . . . . . 16
โข 0 <
3 |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ 0 < 3) |
19 | | eluzle 12781 |
. . . . . . . . . . . . . . . 16
โข (๐ โ
(โคโฅโ3) โ 3 โค ๐) |
20 | 2, 19 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ 3 โค ๐) |
21 | 13, 15, 16, 18, 20 | ltletrd 11320 |
. . . . . . . . . . . . . 14
โข (๐ โ 0 < ๐) |
22 | 12, 21 | jca 513 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ โ โค โง 0 < ๐)) |
23 | | elnnz 12514 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ โ โค โง 0 <
๐)) |
24 | 22, 23 | sylibr 233 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
25 | | gcdnncl 16392 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐
โ โ) โ (๐ gcd ๐
) โ โ) |
26 | 24, 9, 25 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ โ (๐ gcd ๐
) โ โ) |
27 | 26 | nnred 12173 |
. . . . . . . . . 10
โข (๐ โ (๐ gcd ๐
) โ โ) |
28 | 26 | nnne0d 12208 |
. . . . . . . . . 10
โข (๐ โ (๐ gcd ๐
) โ 0) |
29 | 10, 27, 28 | redivcld 11988 |
. . . . . . . . 9
โข (๐ โ (๐
/ (๐ gcd ๐
)) โ โ) |
30 | 29 | adantr 482 |
. . . . . . . 8
โข ((๐ โง 1 < (๐ gcd ๐
)) โ (๐
/ (๐ gcd ๐
)) โ โ) |
31 | 10 | adantr 482 |
. . . . . . . 8
โข ((๐ โง 1 < (๐ gcd ๐
)) โ ๐
โ โ) |
32 | 30, 31 | ltnled 11307 |
. . . . . . 7
โข ((๐ โง 1 < (๐ gcd ๐
)) โ ((๐
/ (๐ gcd ๐
)) < ๐
โ ยฌ ๐
โค (๐
/ (๐ gcd ๐
)))) |
33 | 32 | biimprd 248 |
. . . . . 6
โข ((๐ โง 1 < (๐ gcd ๐
)) โ (ยฌ ๐
โค (๐
/ (๐ gcd ๐
)) โ (๐
/ (๐ gcd ๐
)) < ๐
)) |
34 | 33 | imp 408 |
. . . . 5
โข (((๐ โง 1 < (๐ gcd ๐
)) โง ยฌ ๐
โค (๐
/ (๐ gcd ๐
))) โ (๐
/ (๐ gcd ๐
)) < ๐
) |
35 | 5 | a1i 11 |
. . . . . . . 8
โข ((๐ โง 1 < (๐ gcd ๐
)) โ ๐
= inf({๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด}, โ, < )) |
36 | | ssrab2 4038 |
. . . . . . . . . . . 12
โข {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ (1...๐ต) |
37 | 36 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ (1...๐ต)) |
38 | | elfznn 13476 |
. . . . . . . . . . . . . . 15
โข (๐ โ (1...๐ต) โ ๐ โ โ) |
39 | 38 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...๐ต)) โ ๐ โ โ) |
40 | 39 | nnred 12173 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (1...๐ต)) โ ๐ โ โ) |
41 | 40 | ex 414 |
. . . . . . . . . . . 12
โข (๐ โ (๐ โ (1...๐ต) โ ๐ โ โ)) |
42 | 41 | ssrdv 3951 |
. . . . . . . . . . 11
โข (๐ โ (1...๐ต) โ โ) |
43 | 37, 42 | sstrd 3955 |
. . . . . . . . . 10
โข (๐ โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ โ) |
44 | 43 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง 1 < (๐ gcd ๐
)) โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ โ) |
45 | | fzfid 13884 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐ต) โ Fin) |
46 | 45, 37 | ssfid 9214 |
. . . . . . . . . . 11
โข (๐ โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ Fin) |
47 | 46 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง 1 < (๐ gcd ๐
)) โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ Fin) |
48 | 2, 3, 4 | aks4d1p3 40581 |
. . . . . . . . . . . 12
โข (๐ โ โ๐ โ (1...๐ต) ยฌ ๐ โฅ ๐ด) |
49 | | rabn0 4346 |
. . . . . . . . . . . 12
โข ({๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ โ
โ โ๐ โ (1...๐ต) ยฌ ๐ โฅ ๐ด) |
50 | 48, 49 | sylibr 233 |
. . . . . . . . . . 11
โข (๐ โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ โ
) |
51 | 50 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง 1 < (๐ gcd ๐
)) โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ โ
) |
52 | | fiminre 12107 |
. . . . . . . . . 10
โข (({๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ โ โง {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ Fin โง {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ โ
) โ โ๐ฅ โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด}โ๐ฆ โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด}๐ฅ โค ๐ฆ) |
53 | 44, 47, 51, 52 | syl3anc 1372 |
. . . . . . . . 9
โข ((๐ โง 1 < (๐ gcd ๐
)) โ โ๐ฅ โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด}โ๐ฆ โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด}๐ฅ โค ๐ฆ) |
54 | | breq1 5109 |
. . . . . . . . . . 11
โข (๐ = (๐
/ (๐ gcd ๐
)) โ (๐ โฅ ๐ด โ (๐
/ (๐ gcd ๐
)) โฅ ๐ด)) |
55 | 54 | notbid 318 |
. . . . . . . . . 10
โข (๐ = (๐
/ (๐ gcd ๐
)) โ (ยฌ ๐ โฅ ๐ด โ ยฌ (๐
/ (๐ gcd ๐
)) โฅ ๐ด)) |
56 | | 1zzd 12539 |
. . . . . . . . . . 11
โข ((๐ โง 1 < (๐ gcd ๐
)) โ 1 โ โค) |
57 | 4 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ต = (โโ((2 logb ๐)โ5))) |
58 | | 2re 12232 |
. . . . . . . . . . . . . . . . 17
โข 2 โ
โ |
59 | 58 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 2 โ
โ) |
60 | | 2pos 12261 |
. . . . . . . . . . . . . . . . 17
โข 0 <
2 |
61 | 60 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 0 < 2) |
62 | | 1red 11161 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 1 โ
โ) |
63 | | 1lt2 12329 |
. . . . . . . . . . . . . . . . . . 19
โข 1 <
2 |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 1 < 2) |
65 | 62, 64 | ltned 11296 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 1 โ 2) |
66 | 65 | necomd 2996 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 2 โ 1) |
67 | 59, 61, 16, 21, 66 | relogbcld 40476 |
. . . . . . . . . . . . . . 15
โข (๐ โ (2 logb ๐) โ
โ) |
68 | | 5nn0 12438 |
. . . . . . . . . . . . . . . 16
โข 5 โ
โ0 |
69 | 68 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ 5 โ
โ0) |
70 | 67, 69 | reexpcld 14074 |
. . . . . . . . . . . . . 14
โข (๐ โ ((2 logb ๐)โ5) โ
โ) |
71 | | ceilcl 13753 |
. . . . . . . . . . . . . 14
โข (((2
logb ๐)โ5)
โ โ โ (โโ((2 logb ๐)โ5)) โ โค) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (โโ((2
logb ๐)โ5))
โ โค) |
73 | 57, 72 | eqeltrd 2834 |
. . . . . . . . . . . 12
โข (๐ โ ๐ต โ โค) |
74 | 73 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง 1 < (๐ gcd ๐
)) โ ๐ต โ โค) |
75 | 24 | nnzd 12531 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ โค) |
76 | | divgcdnnr 16401 |
. . . . . . . . . . . . . 14
โข ((๐
โ โ โง ๐ โ โค) โ (๐
/ (๐ gcd ๐
)) โ โ) |
77 | 9, 75, 76 | syl2anc 585 |
. . . . . . . . . . . . 13
โข (๐ โ (๐
/ (๐ gcd ๐
)) โ โ) |
78 | 77 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง 1 < (๐ gcd ๐
)) โ (๐
/ (๐ gcd ๐
)) โ โ) |
79 | 78 | nnzd 12531 |
. . . . . . . . . . 11
โข ((๐ โง 1 < (๐ gcd ๐
)) โ (๐
/ (๐ gcd ๐
)) โ โค) |
80 | 78 | nnge1d 12206 |
. . . . . . . . . . 11
โข ((๐ โง 1 < (๐ gcd ๐
)) โ 1 โค (๐
/ (๐ gcd ๐
))) |
81 | 74 | zred 12612 |
. . . . . . . . . . . 12
โข ((๐ โง 1 < (๐ gcd ๐
)) โ ๐ต โ โ) |
82 | 9 | nnrpd 12960 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐
โ
โ+) |
83 | 82 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง 1 < (๐ gcd ๐
)) โ ๐
โ
โ+) |
84 | 26 | nnrpd 12960 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ gcd ๐
) โ
โ+) |
85 | 84 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง 1 < (๐ gcd ๐
)) โ (๐ gcd ๐
) โ
โ+) |
86 | 31 | recnd 11188 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง 1 < (๐ gcd ๐
)) โ ๐
โ โ) |
87 | 83 | rpne0d 12967 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง 1 < (๐ gcd ๐
)) โ ๐
โ 0) |
88 | 86, 87 | dividd 11934 |
. . . . . . . . . . . . . . 15
โข ((๐ โง 1 < (๐ gcd ๐
)) โ (๐
/ ๐
) = 1) |
89 | | simpr 486 |
. . . . . . . . . . . . . . 15
โข ((๐ โง 1 < (๐ gcd ๐
)) โ 1 < (๐ gcd ๐
)) |
90 | 88, 89 | eqbrtrd 5128 |
. . . . . . . . . . . . . 14
โข ((๐ โง 1 < (๐ gcd ๐
)) โ (๐
/ ๐
) < (๐ gcd ๐
)) |
91 | 31, 83, 85, 90 | ltdiv23d 13029 |
. . . . . . . . . . . . 13
โข ((๐ โง 1 < (๐ gcd ๐
)) โ (๐
/ (๐ gcd ๐
)) < ๐
) |
92 | 30, 31, 91 | ltled 11308 |
. . . . . . . . . . . 12
โข ((๐ โง 1 < (๐ gcd ๐
)) โ (๐
/ (๐ gcd ๐
)) โค ๐
) |
93 | | elfzle2 13451 |
. . . . . . . . . . . . . 14
โข (๐
โ (1...๐ต) โ ๐
โค ๐ต) |
94 | 7, 93 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ ๐
โค ๐ต) |
95 | 94 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง 1 < (๐ gcd ๐
)) โ ๐
โค ๐ต) |
96 | 30, 31, 81, 92, 95 | letrd 11317 |
. . . . . . . . . . 11
โข ((๐ โง 1 < (๐ gcd ๐
)) โ (๐
/ (๐ gcd ๐
)) โค ๐ต) |
97 | 56, 74, 79, 80, 96 | elfzd 13438 |
. . . . . . . . . 10
โข ((๐ โง 1 < (๐ gcd ๐
)) โ (๐
/ (๐ gcd ๐
)) โ (1...๐ต)) |
98 | | aks4d1p5.5 |
. . . . . . . . . . 11
โข (((๐ โง 1 < (๐ gcd ๐
)) โง (๐
/ (๐ gcd ๐
)) โฅ ๐ด) โ ยฌ (๐
/ (๐ gcd ๐
)) โฅ ๐ด) |
99 | | simpr 486 |
. . . . . . . . . . 11
โข (((๐ โง 1 < (๐ gcd ๐
)) โง ยฌ (๐
/ (๐ gcd ๐
)) โฅ ๐ด) โ ยฌ (๐
/ (๐ gcd ๐
)) โฅ ๐ด) |
100 | | exmidd 895 |
. . . . . . . . . . 11
โข ((๐ โง 1 < (๐ gcd ๐
)) โ ((๐
/ (๐ gcd ๐
)) โฅ ๐ด โจ ยฌ (๐
/ (๐ gcd ๐
)) โฅ ๐ด)) |
101 | 98, 99, 100 | mpjaodan 958 |
. . . . . . . . . 10
โข ((๐ โง 1 < (๐ gcd ๐
)) โ ยฌ (๐
/ (๐ gcd ๐
)) โฅ ๐ด) |
102 | 55, 97, 101 | elrabd 3648 |
. . . . . . . . 9
โข ((๐ โง 1 < (๐ gcd ๐
)) โ (๐
/ (๐ gcd ๐
)) โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด}) |
103 | | lbinfle 12115 |
. . . . . . . . 9
โข (({๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ โ โง โ๐ฅ โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด}โ๐ฆ โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด}๐ฅ โค ๐ฆ โง (๐
/ (๐ gcd ๐
)) โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด}) โ inf({๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด}, โ, < ) โค (๐
/ (๐ gcd ๐
))) |
104 | 44, 53, 102, 103 | syl3anc 1372 |
. . . . . . . 8
โข ((๐ โง 1 < (๐ gcd ๐
)) โ inf({๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด}, โ, < ) โค (๐
/ (๐ gcd ๐
))) |
105 | 35, 104 | eqbrtrd 5128 |
. . . . . . 7
โข ((๐ โง 1 < (๐ gcd ๐
)) โ ๐
โค (๐
/ (๐ gcd ๐
))) |
106 | 31, 30 | lenltd 11306 |
. . . . . . 7
โข ((๐ โง 1 < (๐ gcd ๐
)) โ (๐
โค (๐
/ (๐ gcd ๐
)) โ ยฌ (๐
/ (๐ gcd ๐
)) < ๐
)) |
107 | 105, 106 | mpbid 231 |
. . . . . 6
โข ((๐ โง 1 < (๐ gcd ๐
)) โ ยฌ (๐
/ (๐ gcd ๐
)) < ๐
) |
108 | 107 | adantr 482 |
. . . . 5
โข (((๐ โง 1 < (๐ gcd ๐
)) โง ยฌ ๐
โค (๐
/ (๐ gcd ๐
))) โ ยฌ (๐
/ (๐ gcd ๐
)) < ๐
) |
109 | 34, 108 | pm2.21dd 194 |
. . . 4
โข (((๐ โง 1 < (๐ gcd ๐
)) โง ยฌ ๐
โค (๐
/ (๐ gcd ๐
))) โ ๐
โค (๐
/ (๐ gcd ๐
))) |
110 | 1, 109 | pm2.61dan 812 |
. . 3
โข ((๐ โง 1 < (๐ gcd ๐
)) โ ๐
โค (๐
/ (๐ gcd ๐
))) |
111 | 82 | rpred 12962 |
. . . . . 6
โข (๐ โ ๐
โ โ) |
112 | 111 | adantr 482 |
. . . . 5
โข ((๐ โง 1 < (๐ gcd ๐
)) โ ๐
โ โ) |
113 | 91, 107 | pm2.21dd 194 |
. . . . . 6
โข ((๐ โง 1 < (๐ gcd ๐
)) โ (๐ gcd ๐
) โ โ) |
114 | 113 | nnrpd 12960 |
. . . . 5
โข ((๐ โง 1 < (๐ gcd ๐
)) โ (๐ gcd ๐
) โ
โ+) |
115 | 112 | recnd 11188 |
. . . . . . 7
โข ((๐ โง 1 < (๐ gcd ๐
)) โ ๐
โ โ) |
116 | 115, 87 | dividd 11934 |
. . . . . 6
โข ((๐ โง 1 < (๐ gcd ๐
)) โ (๐
/ ๐
) = 1) |
117 | 116, 89 | eqbrtrd 5128 |
. . . . 5
โข ((๐ โง 1 < (๐ gcd ๐
)) โ (๐
/ ๐
) < (๐ gcd ๐
)) |
118 | 112, 83, 114, 117 | ltdiv23d 13029 |
. . . 4
โข ((๐ โง 1 < (๐ gcd ๐
)) โ (๐
/ (๐ gcd ๐
)) < ๐
) |
119 | 77 | nnred 12173 |
. . . . . 6
โข (๐ โ (๐
/ (๐ gcd ๐
)) โ โ) |
120 | 119, 111 | ltnled 11307 |
. . . . 5
โข (๐ โ ((๐
/ (๐ gcd ๐
)) < ๐
โ ยฌ ๐
โค (๐
/ (๐ gcd ๐
)))) |
121 | 120 | adantr 482 |
. . . 4
โข ((๐ โง 1 < (๐ gcd ๐
)) โ ((๐
/ (๐ gcd ๐
)) < ๐
โ ยฌ ๐
โค (๐
/ (๐ gcd ๐
)))) |
122 | 118, 121 | mpbid 231 |
. . 3
โข ((๐ โง 1 < (๐ gcd ๐
)) โ ยฌ ๐
โค (๐
/ (๐ gcd ๐
))) |
123 | 110, 122 | pm2.21dd 194 |
. 2
โข ((๐ โง 1 < (๐ gcd ๐
)) โ (๐ gcd ๐
) = 1) |
124 | | simpr 486 |
. . 3
โข (((๐ โง ยฌ 1 < (๐ gcd ๐
)) โง (๐ gcd ๐
) = 1) โ (๐ gcd ๐
) = 1) |
125 | 26 | adantr 482 |
. . . . . . 7
โข ((๐ โง ยฌ 1 < (๐ gcd ๐
)) โ (๐ gcd ๐
) โ โ) |
126 | 125 | nnred 12173 |
. . . . . 6
โข ((๐ โง ยฌ 1 < (๐ gcd ๐
)) โ (๐ gcd ๐
) โ โ) |
127 | 126 | adantr 482 |
. . . . 5
โข (((๐ โง ยฌ 1 < (๐ gcd ๐
)) โง (๐ gcd ๐
) โ (โคโฅโ2))
โ (๐ gcd ๐
) โ
โ) |
128 | 58 | a1i 11 |
. . . . 5
โข (((๐ โง ยฌ 1 < (๐ gcd ๐
)) โง (๐ gcd ๐
) โ (โคโฅโ2))
โ 2 โ โ) |
129 | | 1red 11161 |
. . . . . 6
โข (((๐ โง ยฌ 1 < (๐ gcd ๐
)) โง (๐ gcd ๐
) โ (โคโฅโ2))
โ 1 โ โ) |
130 | 27, 62 | lenltd 11306 |
. . . . . . . . 9
โข (๐ โ ((๐ gcd ๐
) โค 1 โ ยฌ 1 < (๐ gcd ๐
))) |
131 | 130 | biimprd 248 |
. . . . . . . 8
โข (๐ โ (ยฌ 1 < (๐ gcd ๐
) โ (๐ gcd ๐
) โค 1)) |
132 | 131 | imp 408 |
. . . . . . 7
โข ((๐ โง ยฌ 1 < (๐ gcd ๐
)) โ (๐ gcd ๐
) โค 1) |
133 | 132 | adantr 482 |
. . . . . 6
โข (((๐ โง ยฌ 1 < (๐ gcd ๐
)) โง (๐ gcd ๐
) โ (โคโฅโ2))
โ (๐ gcd ๐
) โค 1) |
134 | 63 | a1i 11 |
. . . . . 6
โข (((๐ โง ยฌ 1 < (๐ gcd ๐
)) โง (๐ gcd ๐
) โ (โคโฅโ2))
โ 1 < 2) |
135 | 127, 129,
128, 133, 134 | lelttrd 11318 |
. . . . 5
โข (((๐ โง ยฌ 1 < (๐ gcd ๐
)) โง (๐ gcd ๐
) โ (โคโฅโ2))
โ (๐ gcd ๐
) < 2) |
136 | | eluzle 12781 |
. . . . . 6
โข ((๐ gcd ๐
) โ (โคโฅโ2)
โ 2 โค (๐ gcd ๐
)) |
137 | 136 | adantl 483 |
. . . . 5
โข (((๐ โง ยฌ 1 < (๐ gcd ๐
)) โง (๐ gcd ๐
) โ (โคโฅโ2))
โ 2 โค (๐ gcd ๐
)) |
138 | 127, 128,
127, 135, 137 | ltletrd 11320 |
. . . 4
โข (((๐ โง ยฌ 1 < (๐ gcd ๐
)) โง (๐ gcd ๐
) โ (โคโฅโ2))
โ (๐ gcd ๐
) < (๐ gcd ๐
)) |
139 | 127 | ltnrd 11294 |
. . . 4
โข (((๐ โง ยฌ 1 < (๐ gcd ๐
)) โง (๐ gcd ๐
) โ (โคโฅโ2))
โ ยฌ (๐ gcd ๐
) < (๐ gcd ๐
)) |
140 | 138, 139 | pm2.21dd 194 |
. . 3
โข (((๐ โง ยฌ 1 < (๐ gcd ๐
)) โง (๐ gcd ๐
) โ (โคโฅโ2))
โ (๐ gcd ๐
) = 1) |
141 | | elnn1uz2 12855 |
. . . 4
โข ((๐ gcd ๐
) โ โ โ ((๐ gcd ๐
) = 1 โจ (๐ gcd ๐
) โ
(โคโฅโ2))) |
142 | 125, 141 | sylib 217 |
. . 3
โข ((๐ โง ยฌ 1 < (๐ gcd ๐
)) โ ((๐ gcd ๐
) = 1 โจ (๐ gcd ๐
) โ
(โคโฅโ2))) |
143 | 124, 140,
142 | mpjaodan 958 |
. 2
โข ((๐ โง ยฌ 1 < (๐ gcd ๐
)) โ (๐ gcd ๐
) = 1) |
144 | 123, 143 | pm2.61dan 812 |
1
โข (๐ โ (๐ gcd ๐
) = 1) |