Step | Hyp | Ref
| Expression |
1 | | elfzoelz 10146 |
. . . . . 6
โข (๐ฅ โ (0..^(๐ ยท ๐)) โ ๐ฅ โ โค) |
2 | | crth.1 |
. . . . . 6
โข ๐ = (0..^(๐ ยท ๐)) |
3 | 1, 2 | eleq2s 2272 |
. . . . 5
โข (๐ฅ โ ๐ โ ๐ฅ โ โค) |
4 | | simpr 110 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โค) โ ๐ฅ โ โค) |
5 | | crth.4 |
. . . . . . . . . 10
โข (๐ โ (๐ โ โ โง ๐ โ โ โง (๐ gcd ๐) = 1)) |
6 | 5 | simp1d 1009 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
7 | 6 | adantr 276 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โค) โ ๐ โ โ) |
8 | | zmodfzo 10346 |
. . . . . . . 8
โข ((๐ฅ โ โค โง ๐ โ โ) โ (๐ฅ mod ๐) โ (0..^๐)) |
9 | 4, 7, 8 | syl2anc 411 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โค) โ (๐ฅ mod ๐) โ (0..^๐)) |
10 | 5 | simp2d 1010 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
11 | 10 | adantr 276 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โค) โ ๐ โ โ) |
12 | | zmodfzo 10346 |
. . . . . . . 8
โข ((๐ฅ โ โค โง ๐ โ โ) โ (๐ฅ mod ๐) โ (0..^๐)) |
13 | 4, 11, 12 | syl2anc 411 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โค) โ (๐ฅ mod ๐) โ (0..^๐)) |
14 | | opelxpi 4658 |
. . . . . . 7
โข (((๐ฅ mod ๐) โ (0..^๐) โง (๐ฅ mod ๐) โ (0..^๐)) โ โจ(๐ฅ mod ๐), (๐ฅ mod ๐)โฉ โ ((0..^๐) ร (0..^๐))) |
15 | 9, 13, 14 | syl2anc 411 |
. . . . . 6
โข ((๐ โง ๐ฅ โ โค) โ โจ(๐ฅ mod ๐), (๐ฅ mod ๐)โฉ โ ((0..^๐) ร (0..^๐))) |
16 | | crth.2 |
. . . . . 6
โข ๐ = ((0..^๐) ร (0..^๐)) |
17 | 15, 16 | eleqtrrdi 2271 |
. . . . 5
โข ((๐ โง ๐ฅ โ โค) โ โจ(๐ฅ mod ๐), (๐ฅ mod ๐)โฉ โ ๐) |
18 | 3, 17 | sylan2 286 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐) โ โจ(๐ฅ mod ๐), (๐ฅ mod ๐)โฉ โ ๐) |
19 | | crth.3 |
. . . 4
โข ๐น = (๐ฅ โ ๐ โฆ โจ(๐ฅ mod ๐), (๐ฅ mod ๐)โฉ) |
20 | 18, 19 | fmptd 5670 |
. . 3
โข (๐ โ ๐น:๐โถ๐) |
21 | | simprl 529 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ฆ โ ๐) |
22 | | elfzoelz 10146 |
. . . . . . . . . . . . 13
โข (๐ฆ โ (0..^(๐ ยท ๐)) โ ๐ฆ โ โค) |
23 | 22, 2 | eleq2s 2272 |
. . . . . . . . . . . 12
โข (๐ฆ โ ๐ โ ๐ฆ โ โค) |
24 | 23 | ad2antrl 490 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ฆ โ โค) |
25 | | zq 9625 |
. . . . . . . . . . 11
โข (๐ฆ โ โค โ ๐ฆ โ
โ) |
26 | 24, 25 | syl 14 |
. . . . . . . . . 10
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ฆ โ โ) |
27 | 6 | adantr 276 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ โ โ) |
28 | | nnq 9632 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
29 | 27, 28 | syl 14 |
. . . . . . . . . 10
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ โ โ) |
30 | 27 | nngt0d 8962 |
. . . . . . . . . 10
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ 0 < ๐) |
31 | 26, 29, 30 | modqcld 10327 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ฆ mod ๐) โ โ) |
32 | 10 | adantr 276 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ โ โ) |
33 | | nnq 9632 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
34 | 32, 33 | syl 14 |
. . . . . . . . . 10
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ โ โ) |
35 | 32 | nngt0d 8962 |
. . . . . . . . . 10
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ 0 < ๐) |
36 | 26, 34, 35 | modqcld 10327 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ฆ mod ๐) โ โ) |
37 | | opexg 4228 |
. . . . . . . . 9
โข (((๐ฆ mod ๐) โ โ โง (๐ฆ mod ๐) โ โ) โ โจ(๐ฆ mod ๐), (๐ฆ mod ๐)โฉ โ V) |
38 | 31, 36, 37 | syl2anc 411 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ โจ(๐ฆ mod ๐), (๐ฆ mod ๐)โฉ โ V) |
39 | | oveq1 5881 |
. . . . . . . . . 10
โข (๐ฅ = ๐ฆ โ (๐ฅ mod ๐) = (๐ฆ mod ๐)) |
40 | | oveq1 5881 |
. . . . . . . . . 10
โข (๐ฅ = ๐ฆ โ (๐ฅ mod ๐) = (๐ฆ mod ๐)) |
41 | 39, 40 | opeq12d 3786 |
. . . . . . . . 9
โข (๐ฅ = ๐ฆ โ โจ(๐ฅ mod ๐), (๐ฅ mod ๐)โฉ = โจ(๐ฆ mod ๐), (๐ฆ mod ๐)โฉ) |
42 | 41, 19 | fvmptg 5592 |
. . . . . . . 8
โข ((๐ฆ โ ๐ โง โจ(๐ฆ mod ๐), (๐ฆ mod ๐)โฉ โ V) โ (๐นโ๐ฆ) = โจ(๐ฆ mod ๐), (๐ฆ mod ๐)โฉ) |
43 | 21, 38, 42 | syl2anc 411 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐นโ๐ฆ) = โจ(๐ฆ mod ๐), (๐ฆ mod ๐)โฉ) |
44 | | simprr 531 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ง โ ๐) |
45 | | elfzoelz 10146 |
. . . . . . . . . . . . 13
โข (๐ง โ (0..^(๐ ยท ๐)) โ ๐ง โ โค) |
46 | 45, 2 | eleq2s 2272 |
. . . . . . . . . . . 12
โข (๐ง โ ๐ โ ๐ง โ โค) |
47 | 44, 46 | syl 14 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ง โ โค) |
48 | | zq 9625 |
. . . . . . . . . . 11
โข (๐ง โ โค โ ๐ง โ
โ) |
49 | 47, 48 | syl 14 |
. . . . . . . . . 10
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ง โ โ) |
50 | 49, 29, 30 | modqcld 10327 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ง mod ๐) โ โ) |
51 | 49, 34, 35 | modqcld 10327 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ง mod ๐) โ โ) |
52 | | opexg 4228 |
. . . . . . . . 9
โข (((๐ง mod ๐) โ โ โง (๐ง mod ๐) โ โ) โ โจ(๐ง mod ๐), (๐ง mod ๐)โฉ โ V) |
53 | 50, 51, 52 | syl2anc 411 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ โจ(๐ง mod ๐), (๐ง mod ๐)โฉ โ V) |
54 | | oveq1 5881 |
. . . . . . . . . 10
โข (๐ฅ = ๐ง โ (๐ฅ mod ๐) = (๐ง mod ๐)) |
55 | | oveq1 5881 |
. . . . . . . . . 10
โข (๐ฅ = ๐ง โ (๐ฅ mod ๐) = (๐ง mod ๐)) |
56 | 54, 55 | opeq12d 3786 |
. . . . . . . . 9
โข (๐ฅ = ๐ง โ โจ(๐ฅ mod ๐), (๐ฅ mod ๐)โฉ = โจ(๐ง mod ๐), (๐ง mod ๐)โฉ) |
57 | 56, 19 | fvmptg 5592 |
. . . . . . . 8
โข ((๐ง โ ๐ โง โจ(๐ง mod ๐), (๐ง mod ๐)โฉ โ V) โ (๐นโ๐ง) = โจ(๐ง mod ๐), (๐ง mod ๐)โฉ) |
58 | 44, 53, 57 | syl2anc 411 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐นโ๐ง) = โจ(๐ง mod ๐), (๐ง mod ๐)โฉ) |
59 | 43, 58 | eqeq12d 2192 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ฆ) = (๐นโ๐ง) โ โจ(๐ฆ mod ๐), (๐ฆ mod ๐)โฉ = โจ(๐ง mod ๐), (๐ง mod ๐)โฉ)) |
60 | | opthg 4238 |
. . . . . . 7
โข (((๐ฆ mod ๐) โ โ โง (๐ฆ mod ๐) โ โ) โ (โจ(๐ฆ mod ๐), (๐ฆ mod ๐)โฉ = โจ(๐ง mod ๐), (๐ง mod ๐)โฉ โ ((๐ฆ mod ๐) = (๐ง mod ๐) โง (๐ฆ mod ๐) = (๐ง mod ๐)))) |
61 | 31, 36, 60 | syl2anc 411 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (โจ(๐ฆ mod ๐), (๐ฆ mod ๐)โฉ = โจ(๐ง mod ๐), (๐ง mod ๐)โฉ โ ((๐ฆ mod ๐) = (๐ง mod ๐) โง (๐ฆ mod ๐) = (๐ง mod ๐)))) |
62 | 59, 61 | bitrd 188 |
. . . . 5
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ฆ) = (๐นโ๐ง) โ ((๐ฆ mod ๐) = (๐ง mod ๐) โง (๐ฆ mod ๐) = (๐ง mod ๐)))) |
63 | 27 | nnzd 9373 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ โ โค) |
64 | 32 | nnzd 9373 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ โ โค) |
65 | 21, 2 | eleqtrdi 2270 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ฆ โ (0..^(๐ ยท ๐))) |
66 | 65, 22 | syl 14 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ฆ โ โค) |
67 | 44, 2 | eleqtrdi 2270 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ง โ (0..^(๐ ยท ๐))) |
68 | 67, 45 | syl 14 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ง โ โค) |
69 | 66, 68 | zsubcld 9379 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ฆ โ ๐ง) โ โค) |
70 | 5 | simp3d 1011 |
. . . . . . . 8
โข (๐ โ (๐ gcd ๐) = 1) |
71 | 70 | adantr 276 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ gcd ๐) = 1) |
72 | | coprmdvds2 12092 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โค โง (๐ฆ โ ๐ง) โ โค) โง (๐ gcd ๐) = 1) โ ((๐ โฅ (๐ฆ โ ๐ง) โง ๐ โฅ (๐ฆ โ ๐ง)) โ (๐ ยท ๐) โฅ (๐ฆ โ ๐ง))) |
73 | 63, 64, 69, 71, 72 | syl31anc 1241 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐ โฅ (๐ฆ โ ๐ง) โง ๐ โฅ (๐ฆ โ ๐ง)) โ (๐ ยท ๐) โฅ (๐ฆ โ ๐ง))) |
74 | | moddvds 11805 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ฆ โ โค โง ๐ง โ โค) โ ((๐ฆ mod ๐) = (๐ง mod ๐) โ ๐ โฅ (๐ฆ โ ๐ง))) |
75 | 27, 66, 68, 74 | syl3anc 1238 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐ฆ mod ๐) = (๐ง mod ๐) โ ๐ โฅ (๐ฆ โ ๐ง))) |
76 | | moddvds 11805 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ฆ โ โค โง ๐ง โ โค) โ ((๐ฆ mod ๐) = (๐ง mod ๐) โ ๐ โฅ (๐ฆ โ ๐ง))) |
77 | 32, 66, 68, 76 | syl3anc 1238 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐ฆ mod ๐) = (๐ง mod ๐) โ ๐ โฅ (๐ฆ โ ๐ง))) |
78 | 75, 77 | anbi12d 473 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (((๐ฆ mod ๐) = (๐ง mod ๐) โง (๐ฆ mod ๐) = (๐ง mod ๐)) โ (๐ โฅ (๐ฆ โ ๐ง) โง ๐ โฅ (๐ฆ โ ๐ง)))) |
79 | | qmulcl 9636 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
80 | 29, 34, 79 | syl2anc 411 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ ยท ๐) โ โ) |
81 | | elfzole1 10154 |
. . . . . . . . . 10
โข (๐ฆ โ (0..^(๐ ยท ๐)) โ 0 โค ๐ฆ) |
82 | 65, 81 | syl 14 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ 0 โค ๐ฆ) |
83 | | elfzolt2 10155 |
. . . . . . . . . 10
โข (๐ฆ โ (0..^(๐ ยท ๐)) โ ๐ฆ < (๐ ยท ๐)) |
84 | 65, 83 | syl 14 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ฆ < (๐ ยท ๐)) |
85 | | modqid 10348 |
. . . . . . . . 9
โข (((๐ฆ โ โ โง (๐ ยท ๐) โ โ) โง (0 โค ๐ฆ โง ๐ฆ < (๐ ยท ๐))) โ (๐ฆ mod (๐ ยท ๐)) = ๐ฆ) |
86 | 26, 80, 82, 84, 85 | syl22anc 1239 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ฆ mod (๐ ยท ๐)) = ๐ฆ) |
87 | | elfzole1 10154 |
. . . . . . . . . 10
โข (๐ง โ (0..^(๐ ยท ๐)) โ 0 โค ๐ง) |
88 | 67, 87 | syl 14 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ 0 โค ๐ง) |
89 | | elfzolt2 10155 |
. . . . . . . . . 10
โข (๐ง โ (0..^(๐ ยท ๐)) โ ๐ง < (๐ ยท ๐)) |
90 | 67, 89 | syl 14 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ง < (๐ ยท ๐)) |
91 | | modqid 10348 |
. . . . . . . . 9
โข (((๐ง โ โ โง (๐ ยท ๐) โ โ) โง (0 โค ๐ง โง ๐ง < (๐ ยท ๐))) โ (๐ง mod (๐ ยท ๐)) = ๐ง) |
92 | 49, 80, 88, 90, 91 | syl22anc 1239 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ง mod (๐ ยท ๐)) = ๐ง) |
93 | 86, 92 | eqeq12d 2192 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐ฆ mod (๐ ยท ๐)) = (๐ง mod (๐ ยท ๐)) โ ๐ฆ = ๐ง)) |
94 | 27, 32 | nnmulcld 8967 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ ยท ๐) โ โ) |
95 | | moddvds 11805 |
. . . . . . . 8
โข (((๐ ยท ๐) โ โ โง ๐ฆ โ โค โง ๐ง โ โค) โ ((๐ฆ mod (๐ ยท ๐)) = (๐ง mod (๐ ยท ๐)) โ (๐ ยท ๐) โฅ (๐ฆ โ ๐ง))) |
96 | 94, 66, 68, 95 | syl3anc 1238 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐ฆ mod (๐ ยท ๐)) = (๐ง mod (๐ ยท ๐)) โ (๐ ยท ๐) โฅ (๐ฆ โ ๐ง))) |
97 | 93, 96 | bitr3d 190 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ฆ = ๐ง โ (๐ ยท ๐) โฅ (๐ฆ โ ๐ง))) |
98 | 73, 78, 97 | 3imtr4d 203 |
. . . . 5
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (((๐ฆ mod ๐) = (๐ง mod ๐) โง (๐ฆ mod ๐) = (๐ง mod ๐)) โ ๐ฆ = ๐ง)) |
99 | 62, 98 | sylbid 150 |
. . . 4
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ฆ) = (๐นโ๐ง) โ ๐ฆ = ๐ง)) |
100 | 99 | ralrimivva 2559 |
. . 3
โข (๐ โ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐นโ๐ฆ) = (๐นโ๐ง) โ ๐ฆ = ๐ง)) |
101 | | dff13 5768 |
. . 3
โข (๐น:๐โ1-1โ๐ โ (๐น:๐โถ๐ โง โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐นโ๐ฆ) = (๐นโ๐ง) โ ๐ฆ = ๐ง))) |
102 | 20, 100, 101 | sylanbrc 417 |
. 2
โข (๐ โ ๐น:๐โ1-1โ๐) |
103 | | nnnn0 9182 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ0) |
104 | | nnnn0 9182 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ0) |
105 | | hashfzo0 10802 |
. . . . . . . . 9
โข (๐ โ โ0
โ (โฏโ(0..^๐)) = ๐) |
106 | | hashfzo0 10802 |
. . . . . . . . 9
โข (๐ โ โ0
โ (โฏโ(0..^๐)) = ๐) |
107 | 105, 106 | oveqan12d 5893 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((โฏโ(0..^๐)) ยท (โฏโ(0..^๐))) = (๐ ยท ๐)) |
108 | | 0z 9263 |
. . . . . . . . . 10
โข 0 โ
โค |
109 | | simpl 109 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ
โ0) |
110 | 109 | nn0zd 9372 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ โค) |
111 | | fzofig 10431 |
. . . . . . . . . 10
โข ((0
โ โค โง ๐
โ โค) โ (0..^๐) โ Fin) |
112 | 108, 110,
111 | sylancr 414 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (0..^๐) โ Fin) |
113 | | nn0z 9272 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ ๐ โ
โค) |
114 | 113 | adantl 277 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ โค) |
115 | | fzofig 10431 |
. . . . . . . . . 10
โข ((0
โ โค โง ๐
โ โค) โ (0..^๐) โ Fin) |
116 | 108, 114,
115 | sylancr 414 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (0..^๐) โ Fin) |
117 | | hashxp 10805 |
. . . . . . . . 9
โข
(((0..^๐) โ Fin
โง (0..^๐) โ Fin)
โ (โฏโ((0..^๐) ร (0..^๐))) = ((โฏโ(0..^๐)) ยท (โฏโ(0..^๐)))) |
118 | 112, 116,
117 | syl2anc 411 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (โฏโ((0..^๐) ร (0..^๐))) = ((โฏโ(0..^๐)) ยท (โฏโ(0..^๐)))) |
119 | | nn0mulcl 9211 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ ยท ๐) โ
โ0) |
120 | | hashfzo0 10802 |
. . . . . . . . 9
โข ((๐ ยท ๐) โ โ0 โ
(โฏโ(0..^(๐
ยท ๐))) = (๐ ยท ๐)) |
121 | 119, 120 | syl 14 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (โฏโ(0..^(๐ ยท ๐))) = (๐ ยท ๐)) |
122 | 107, 118,
121 | 3eqtr4rd 2221 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (โฏโ(0..^(๐ ยท ๐))) = (โฏโ((0..^๐) ร (0..^๐)))) |
123 | 119 | nn0zd 9372 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ ยท ๐) โ โค) |
124 | | fzofig 10431 |
. . . . . . . . 9
โข ((0
โ โค โง (๐
ยท ๐) โ โค)
โ (0..^(๐ ยท
๐)) โ
Fin) |
125 | 108, 123,
124 | sylancr 414 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (0..^(๐ ยท ๐)) โ Fin) |
126 | | xpfi 6928 |
. . . . . . . . 9
โข
(((0..^๐) โ Fin
โง (0..^๐) โ Fin)
โ ((0..^๐) ร
(0..^๐)) โ
Fin) |
127 | 112, 116,
126 | syl2anc 411 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((0..^๐) ร (0..^๐)) โ Fin) |
128 | | hashen 10763 |
. . . . . . . 8
โข
(((0..^(๐ ยท
๐)) โ Fin โง
((0..^๐) ร (0..^๐)) โ Fin) โ
((โฏโ(0..^(๐
ยท ๐))) =
(โฏโ((0..^๐)
ร (0..^๐))) โ
(0..^(๐ ยท ๐)) โ ((0..^๐) ร (0..^๐)))) |
129 | 125, 127,
128 | syl2anc 411 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((โฏโ(0..^(๐ ยท ๐))) = (โฏโ((0..^๐) ร (0..^๐))) โ (0..^(๐ ยท ๐)) โ ((0..^๐) ร (0..^๐)))) |
130 | 122, 129 | mpbid 147 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (0..^(๐ ยท ๐)) โ ((0..^๐) ร (0..^๐))) |
131 | 103, 104,
130 | syl2an 289 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ
(0..^(๐ ยท ๐)) โ ((0..^๐) ร (0..^๐))) |
132 | 6, 10, 131 | syl2anc 411 |
. . . 4
โข (๐ โ (0..^(๐ ยท ๐)) โ ((0..^๐) ร (0..^๐))) |
133 | 132, 2, 16 | 3brtr4g 4037 |
. . 3
โข (๐ โ ๐ โ ๐) |
134 | 6 | nnnn0d 9228 |
. . . . 5
โข (๐ โ ๐ โ
โ0) |
135 | 10 | nnnn0d 9228 |
. . . . 5
โข (๐ โ ๐ โ
โ0) |
136 | 134, 135,
127 | syl2anc 411 |
. . . 4
โข (๐ โ ((0..^๐) ร (0..^๐)) โ Fin) |
137 | 16, 136 | eqeltrid 2264 |
. . 3
โข (๐ โ ๐ โ Fin) |
138 | | f1finf1o 6945 |
. . 3
โข ((๐ โ ๐ โง ๐ โ Fin) โ (๐น:๐โ1-1โ๐ โ ๐น:๐โ1-1-ontoโ๐)) |
139 | 133, 137,
138 | syl2anc 411 |
. 2
โข (๐ โ (๐น:๐โ1-1โ๐ โ ๐น:๐โ1-1-ontoโ๐)) |
140 | 102, 139 | mpbid 147 |
1
โข (๐ โ ๐น:๐โ1-1-ontoโ๐) |