Step | Hyp | Ref
| Expression |
1 | | hashgcdlem.f |
. 2
โข ๐น = (๐ฅ โ ๐ด โฆ (๐ฅ ยท ๐)) |
2 | | oveq1 7369 |
. . . . 5
โข (๐ฆ = ๐ฅ โ (๐ฆ gcd (๐ / ๐)) = (๐ฅ gcd (๐ / ๐))) |
3 | 2 | eqeq1d 2739 |
. . . 4
โข (๐ฆ = ๐ฅ โ ((๐ฆ gcd (๐ / ๐)) = 1 โ (๐ฅ gcd (๐ / ๐)) = 1)) |
4 | | hashgcdlem.a |
. . . 4
โข ๐ด = {๐ฆ โ (0..^(๐ / ๐)) โฃ (๐ฆ gcd (๐ / ๐)) = 1} |
5 | 3, 4 | elrab2 3653 |
. . 3
โข (๐ฅ โ ๐ด โ (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) |
6 | | elfzonn0 13624 |
. . . . . . 7
โข (๐ฅ โ (0..^(๐ / ๐)) โ ๐ฅ โ โ0) |
7 | 6 | ad2antrl 727 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ ๐ฅ โ โ0) |
8 | | nnnn0 12427 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ0) |
9 | 8 | 3ad2ant2 1135 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โ ๐ โ
โ0) |
10 | 9 | adantr 482 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ ๐ โ
โ0) |
11 | 7, 10 | nn0mulcld 12485 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ (๐ฅ ยท ๐) โ
โ0) |
12 | | simpl1 1192 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ ๐ โ โ) |
13 | | elfzolt2 13588 |
. . . . . . 7
โข (๐ฅ โ (0..^(๐ / ๐)) โ ๐ฅ < (๐ / ๐)) |
14 | 13 | ad2antrl 727 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ ๐ฅ < (๐ / ๐)) |
15 | | elfzoelz 13579 |
. . . . . . . . 9
โข (๐ฅ โ (0..^(๐ / ๐)) โ ๐ฅ โ โค) |
16 | 15 | ad2antrl 727 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ ๐ฅ โ โค) |
17 | 16 | zred 12614 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ ๐ฅ โ โ) |
18 | | nnre 12167 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
19 | 18 | 3ad2ant1 1134 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โ ๐ โ โ) |
20 | 19 | adantr 482 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ ๐ โ โ) |
21 | | nnre 12167 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
22 | | nngt0 12191 |
. . . . . . . . . 10
โข (๐ โ โ โ 0 <
๐) |
23 | 21, 22 | jca 513 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ โ โ โง 0 <
๐)) |
24 | 23 | 3ad2ant2 1135 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โ (๐ โ โ โง 0 < ๐)) |
25 | 24 | adantr 482 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ (๐ โ โ โง 0 < ๐)) |
26 | | ltmuldiv 12035 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ โ โ โง (๐ โ โ โง 0 <
๐)) โ ((๐ฅ ยท ๐) < ๐ โ ๐ฅ < (๐ / ๐))) |
27 | 17, 20, 25, 26 | syl3anc 1372 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ ((๐ฅ ยท ๐) < ๐ โ ๐ฅ < (๐ / ๐))) |
28 | 14, 27 | mpbird 257 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ (๐ฅ ยท ๐) < ๐) |
29 | | elfzo0 13620 |
. . . . 5
โข ((๐ฅ ยท ๐) โ (0..^๐) โ ((๐ฅ ยท ๐) โ โ0 โง ๐ โ โ โง (๐ฅ ยท ๐) < ๐)) |
30 | 11, 12, 28, 29 | syl3anbrc 1344 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ (๐ฅ ยท ๐) โ (0..^๐)) |
31 | | nncn 12168 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
32 | 31 | 3ad2ant1 1134 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โ ๐ โ โ) |
33 | | nncn 12168 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
34 | 33 | 3ad2ant2 1135 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โ ๐ โ โ) |
35 | | nnne0 12194 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ 0) |
36 | 35 | 3ad2ant2 1135 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โ ๐ โ 0) |
37 | 32, 34, 36 | divcan1d 11939 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โ ((๐ / ๐) ยท ๐) = ๐) |
38 | 37 | adantr 482 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ ((๐ / ๐) ยท ๐) = ๐) |
39 | 38 | eqcomd 2743 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ ๐ = ((๐ / ๐) ยท ๐)) |
40 | 39 | oveq2d 7378 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ ((๐ฅ ยท ๐) gcd ๐) = ((๐ฅ ยท ๐) gcd ((๐ / ๐) ยท ๐))) |
41 | | nndivdvds 16152 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โฅ ๐ โ (๐ / ๐) โ โ)) |
42 | 41 | biimp3a 1470 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โ (๐ / ๐) โ โ) |
43 | 42 | nnzd 12533 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โ (๐ / ๐) โ โค) |
44 | 43 | adantr 482 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ (๐ / ๐) โ โค) |
45 | | mulgcdr 16438 |
. . . . . 6
โข ((๐ฅ โ โค โง (๐ / ๐) โ โค โง ๐ โ โ0) โ ((๐ฅ ยท ๐) gcd ((๐ / ๐) ยท ๐)) = ((๐ฅ gcd (๐ / ๐)) ยท ๐)) |
46 | 16, 44, 10, 45 | syl3anc 1372 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ ((๐ฅ ยท ๐) gcd ((๐ / ๐) ยท ๐)) = ((๐ฅ gcd (๐ / ๐)) ยท ๐)) |
47 | | simprr 772 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ (๐ฅ gcd (๐ / ๐)) = 1) |
48 | 47 | oveq1d 7377 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ ((๐ฅ gcd (๐ / ๐)) ยท ๐) = (1 ยท ๐)) |
49 | 34 | mulid2d 11180 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โ (1 ยท ๐) = ๐) |
50 | 49 | adantr 482 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ (1 ยท ๐) = ๐) |
51 | 48, 50 | eqtrd 2777 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ ((๐ฅ gcd (๐ / ๐)) ยท ๐) = ๐) |
52 | 40, 46, 51 | 3eqtrd 2781 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ ((๐ฅ ยท ๐) gcd ๐) = ๐) |
53 | | oveq1 7369 |
. . . . . 6
โข (๐ง = (๐ฅ ยท ๐) โ (๐ง gcd ๐) = ((๐ฅ ยท ๐) gcd ๐)) |
54 | 53 | eqeq1d 2739 |
. . . . 5
โข (๐ง = (๐ฅ ยท ๐) โ ((๐ง gcd ๐) = ๐ โ ((๐ฅ ยท ๐) gcd ๐) = ๐)) |
55 | | hashgcdlem.b |
. . . . 5
โข ๐ต = {๐ง โ (0..^๐) โฃ (๐ง gcd ๐) = ๐} |
56 | 54, 55 | elrab2 3653 |
. . . 4
โข ((๐ฅ ยท ๐) โ ๐ต โ ((๐ฅ ยท ๐) โ (0..^๐) โง ((๐ฅ ยท ๐) gcd ๐) = ๐)) |
57 | 30, 52, 56 | sylanbrc 584 |
. . 3
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง (๐ฅ gcd (๐ / ๐)) = 1)) โ (๐ฅ ยท ๐) โ ๐ต) |
58 | 5, 57 | sylan2b 595 |
. 2
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง ๐ฅ โ ๐ด) โ (๐ฅ ยท ๐) โ ๐ต) |
59 | | oveq1 7369 |
. . . . 5
โข (๐ง = ๐ค โ (๐ง gcd ๐) = (๐ค gcd ๐)) |
60 | 59 | eqeq1d 2739 |
. . . 4
โข (๐ง = ๐ค โ ((๐ง gcd ๐) = ๐ โ (๐ค gcd ๐) = ๐)) |
61 | 60, 55 | elrab2 3653 |
. . 3
โข (๐ค โ ๐ต โ (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) |
62 | | simprr 772 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ (๐ค gcd ๐) = ๐) |
63 | | elfzoelz 13579 |
. . . . . . . . . . 11
โข (๐ค โ (0..^๐) โ ๐ค โ โค) |
64 | 63 | ad2antrl 727 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ ๐ค โ โค) |
65 | | simpl1 1192 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ ๐ โ โ) |
66 | 65 | nnzd 12533 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ ๐ โ โค) |
67 | | gcddvds 16390 |
. . . . . . . . . 10
โข ((๐ค โ โค โง ๐ โ โค) โ ((๐ค gcd ๐) โฅ ๐ค โง (๐ค gcd ๐) โฅ ๐)) |
68 | 64, 66, 67 | syl2anc 585 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ ((๐ค gcd ๐) โฅ ๐ค โง (๐ค gcd ๐) โฅ ๐)) |
69 | 68 | simpld 496 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ (๐ค gcd ๐) โฅ ๐ค) |
70 | 62, 69 | eqbrtrrd 5134 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ ๐ โฅ ๐ค) |
71 | | nnz 12527 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โค) |
72 | 71 | 3ad2ant2 1135 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โ ๐ โ โค) |
73 | 72 | adantr 482 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ ๐ โ โค) |
74 | 36 | adantr 482 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ ๐ โ 0) |
75 | | dvdsval2 16146 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ 0 โง ๐ค โ โค) โ (๐ โฅ ๐ค โ (๐ค / ๐) โ โค)) |
76 | 73, 74, 64, 75 | syl3anc 1372 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ (๐ โฅ ๐ค โ (๐ค / ๐) โ โค)) |
77 | 70, 76 | mpbid 231 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ (๐ค / ๐) โ โค) |
78 | | elfzofz 13595 |
. . . . . . . . 9
โข (๐ค โ (0..^๐) โ ๐ค โ (0...๐)) |
79 | 78 | ad2antrl 727 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ ๐ค โ (0...๐)) |
80 | | elfznn0 13541 |
. . . . . . . 8
โข (๐ค โ (0...๐) โ ๐ค โ โ0) |
81 | | nn0re 12429 |
. . . . . . . . 9
โข (๐ค โ โ0
โ ๐ค โ
โ) |
82 | | nn0ge0 12445 |
. . . . . . . . 9
โข (๐ค โ โ0
โ 0 โค ๐ค) |
83 | 81, 82 | jca 513 |
. . . . . . . 8
โข (๐ค โ โ0
โ (๐ค โ โ
โง 0 โค ๐ค)) |
84 | 79, 80, 83 | 3syl 18 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ (๐ค โ โ โง 0 โค ๐ค)) |
85 | 24 | adantr 482 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ (๐ โ โ โง 0 < ๐)) |
86 | | divge0 12031 |
. . . . . . 7
โข (((๐ค โ โ โง 0 โค
๐ค) โง (๐ โ โ โง 0 < ๐)) โ 0 โค (๐ค / ๐)) |
87 | 84, 85, 86 | syl2anc 585 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ 0 โค (๐ค / ๐)) |
88 | | elnn0z 12519 |
. . . . . 6
โข ((๐ค / ๐) โ โ0 โ ((๐ค / ๐) โ โค โง 0 โค (๐ค / ๐))) |
89 | 77, 87, 88 | sylanbrc 584 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ (๐ค / ๐) โ
โ0) |
90 | 42 | adantr 482 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ (๐ / ๐) โ โ) |
91 | | elfzolt2 13588 |
. . . . . . 7
โข (๐ค โ (0..^๐) โ ๐ค < ๐) |
92 | 91 | ad2antrl 727 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ ๐ค < ๐) |
93 | 64 | zred 12614 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ ๐ค โ โ) |
94 | 19 | adantr 482 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ ๐ โ โ) |
95 | | ltdiv1 12026 |
. . . . . . 7
โข ((๐ค โ โ โง ๐ โ โ โง (๐ โ โ โง 0 <
๐)) โ (๐ค < ๐ โ (๐ค / ๐) < (๐ / ๐))) |
96 | 93, 94, 85, 95 | syl3anc 1372 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ (๐ค < ๐ โ (๐ค / ๐) < (๐ / ๐))) |
97 | 92, 96 | mpbid 231 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ (๐ค / ๐) < (๐ / ๐)) |
98 | | elfzo0 13620 |
. . . . 5
โข ((๐ค / ๐) โ (0..^(๐ / ๐)) โ ((๐ค / ๐) โ โ0 โง (๐ / ๐) โ โ โง (๐ค / ๐) < (๐ / ๐))) |
99 | 89, 90, 97, 98 | syl3anbrc 1344 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ (๐ค / ๐) โ (0..^(๐ / ๐))) |
100 | 62 | oveq1d 7377 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ ((๐ค gcd ๐) / ๐) = (๐ / ๐)) |
101 | | simpl2 1193 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ ๐ โ โ) |
102 | | simpl3 1194 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ ๐ โฅ ๐) |
103 | | gcddiv 16439 |
. . . . . 6
โข (((๐ค โ โค โง ๐ โ โค โง ๐ โ โ) โง (๐ โฅ ๐ค โง ๐ โฅ ๐)) โ ((๐ค gcd ๐) / ๐) = ((๐ค / ๐) gcd (๐ / ๐))) |
104 | 64, 66, 101, 70, 102, 103 | syl32anc 1379 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ ((๐ค gcd ๐) / ๐) = ((๐ค / ๐) gcd (๐ / ๐))) |
105 | 34, 36 | dividd 11936 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โ (๐ / ๐) = 1) |
106 | 105 | adantr 482 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ (๐ / ๐) = 1) |
107 | 100, 104,
106 | 3eqtr3d 2785 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ ((๐ค / ๐) gcd (๐ / ๐)) = 1) |
108 | | oveq1 7369 |
. . . . . 6
โข (๐ฆ = (๐ค / ๐) โ (๐ฆ gcd (๐ / ๐)) = ((๐ค / ๐) gcd (๐ / ๐))) |
109 | 108 | eqeq1d 2739 |
. . . . 5
โข (๐ฆ = (๐ค / ๐) โ ((๐ฆ gcd (๐ / ๐)) = 1 โ ((๐ค / ๐) gcd (๐ / ๐)) = 1)) |
110 | 109, 4 | elrab2 3653 |
. . . 4
โข ((๐ค / ๐) โ ๐ด โ ((๐ค / ๐) โ (0..^(๐ / ๐)) โง ((๐ค / ๐) gcd (๐ / ๐)) = 1)) |
111 | 99, 107, 110 | sylanbrc 584 |
. . 3
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ค โ (0..^๐) โง (๐ค gcd ๐) = ๐)) โ (๐ค / ๐) โ ๐ด) |
112 | 61, 111 | sylan2b 595 |
. 2
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง ๐ค โ ๐ต) โ (๐ค / ๐) โ ๐ด) |
113 | 5 | simplbi 499 |
. . . 4
โข (๐ฅ โ ๐ด โ ๐ฅ โ (0..^(๐ / ๐))) |
114 | 61 | simplbi 499 |
. . . 4
โข (๐ค โ ๐ต โ ๐ค โ (0..^๐)) |
115 | 113, 114 | anim12i 614 |
. . 3
โข ((๐ฅ โ ๐ด โง ๐ค โ ๐ต) โ (๐ฅ โ (0..^(๐ / ๐)) โง ๐ค โ (0..^๐))) |
116 | 63 | ad2antll 728 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง ๐ค โ (0..^๐))) โ ๐ค โ โค) |
117 | 116 | zcnd 12615 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง ๐ค โ (0..^๐))) โ ๐ค โ โ) |
118 | 34 | adantr 482 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง ๐ค โ (0..^๐))) โ ๐ โ โ) |
119 | 36 | adantr 482 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง ๐ค โ (0..^๐))) โ ๐ โ 0) |
120 | 117, 118,
119 | divcan1d 11939 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง ๐ค โ (0..^๐))) โ ((๐ค / ๐) ยท ๐) = ๐ค) |
121 | 120 | eqcomd 2743 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง ๐ค โ (0..^๐))) โ ๐ค = ((๐ค / ๐) ยท ๐)) |
122 | | oveq1 7369 |
. . . . . 6
โข (๐ฅ = (๐ค / ๐) โ (๐ฅ ยท ๐) = ((๐ค / ๐) ยท ๐)) |
123 | 122 | eqeq2d 2748 |
. . . . 5
โข (๐ฅ = (๐ค / ๐) โ (๐ค = (๐ฅ ยท ๐) โ ๐ค = ((๐ค / ๐) ยท ๐))) |
124 | 121, 123 | syl5ibrcom 247 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง ๐ค โ (0..^๐))) โ (๐ฅ = (๐ค / ๐) โ ๐ค = (๐ฅ ยท ๐))) |
125 | 15 | ad2antrl 727 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง ๐ค โ (0..^๐))) โ ๐ฅ โ โค) |
126 | 125 | zcnd 12615 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง ๐ค โ (0..^๐))) โ ๐ฅ โ โ) |
127 | 126, 118,
119 | divcan4d 11944 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง ๐ค โ (0..^๐))) โ ((๐ฅ ยท ๐) / ๐) = ๐ฅ) |
128 | 127 | eqcomd 2743 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง ๐ค โ (0..^๐))) โ ๐ฅ = ((๐ฅ ยท ๐) / ๐)) |
129 | | oveq1 7369 |
. . . . . 6
โข (๐ค = (๐ฅ ยท ๐) โ (๐ค / ๐) = ((๐ฅ ยท ๐) / ๐)) |
130 | 129 | eqeq2d 2748 |
. . . . 5
โข (๐ค = (๐ฅ ยท ๐) โ (๐ฅ = (๐ค / ๐) โ ๐ฅ = ((๐ฅ ยท ๐) / ๐))) |
131 | 128, 130 | syl5ibrcom 247 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง ๐ค โ (0..^๐))) โ (๐ค = (๐ฅ ยท ๐) โ ๐ฅ = (๐ค / ๐))) |
132 | 124, 131 | impbid 211 |
. . 3
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ (0..^(๐ / ๐)) โง ๐ค โ (0..^๐))) โ (๐ฅ = (๐ค / ๐) โ ๐ค = (๐ฅ ยท ๐))) |
133 | 115, 132 | sylan2 594 |
. 2
โข (((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โง (๐ฅ โ ๐ด โง ๐ค โ ๐ต)) โ (๐ฅ = (๐ค / ๐) โ ๐ค = (๐ฅ ยท ๐))) |
134 | 1, 58, 112, 133 | f1o2d 7612 |
1
โข ((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โ ๐น:๐ดโ1-1-ontoโ๐ต) |