This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hashgcdlem

Description: A correspondence between elements of specific GCD and relative primes in a smaller ring. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Hypotheses hashgcdlem.a 
|- A = { y e. ( 0 ..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 }
hashgcdlem.b 
|- B = { z e. ( 0 ..^ M ) | ( z gcd M ) = N }
hashgcdlem.f 
|- F = ( x e. A |-> ( x x. N ) )
Assertion hashgcdlem 
|- ( ( M e. NN /\ N e. NN /\ N || M ) -> F : A -1-1-onto-> B )

Proof

Step Hyp Ref Expression
1 hashgcdlem.a 
 |-  A = { y e. ( 0 ..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 }
2 hashgcdlem.b 
 |-  B = { z e. ( 0 ..^ M ) | ( z gcd M ) = N }
3 hashgcdlem.f 
 |-  F = ( x e. A |-> ( x x. N ) )
4 oveq1 
 |-  ( y = x -> ( y gcd ( M / N ) ) = ( x gcd ( M / N ) ) )
5 4 eqeq1d 
 |-  ( y = x -> ( ( y gcd ( M / N ) ) = 1 <-> ( x gcd ( M / N ) ) = 1 ) )
6 5 1 elrab2 
 |-  ( x e. A <-> ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) )
7 elfzonn0 
 |-  ( x e. ( 0 ..^ ( M / N ) ) -> x e. NN0 )
8 7 ad2antrl 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> x e. NN0 )
9 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
10 9 3ad2ant2 
 |-  ( ( M e. NN /\ N e. NN /\ N || M ) -> N e. NN0 )
11 10 adantr 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> N e. NN0 )
12 8 11 nn0mulcld 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> ( x x. N ) e. NN0 )
13 simpl1 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> M e. NN )
14 elfzolt2 
 |-  ( x e. ( 0 ..^ ( M / N ) ) -> x < ( M / N ) )
15 14 ad2antrl 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> x < ( M / N ) )
16 elfzoelz 
 |-  ( x e. ( 0 ..^ ( M / N ) ) -> x e. ZZ )
17 16 ad2antrl 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> x e. ZZ )
18 17 zred 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> x e. RR )
19 nnre 
 |-  ( M e. NN -> M e. RR )
20 19 3ad2ant1 
 |-  ( ( M e. NN /\ N e. NN /\ N || M ) -> M e. RR )
21 20 adantr 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> M e. RR )
22 nnre 
 |-  ( N e. NN -> N e. RR )
23 nngt0 
 |-  ( N e. NN -> 0 < N )
24 22 23 jca 
 |-  ( N e. NN -> ( N e. RR /\ 0 < N ) )
25 24 3ad2ant2 
 |-  ( ( M e. NN /\ N e. NN /\ N || M ) -> ( N e. RR /\ 0 < N ) )
26 25 adantr 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> ( N e. RR /\ 0 < N ) )
27 ltmuldiv 
 |-  ( ( x e. RR /\ M e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( x x. N ) < M <-> x < ( M / N ) ) )
28 18 21 26 27 syl3anc 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> ( ( x x. N ) < M <-> x < ( M / N ) ) )
29 15 28 mpbird 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> ( x x. N ) < M )
30 elfzo0 
 |-  ( ( x x. N ) e. ( 0 ..^ M ) <-> ( ( x x. N ) e. NN0 /\ M e. NN /\ ( x x. N ) < M ) )
31 12 13 29 30 syl3anbrc 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> ( x x. N ) e. ( 0 ..^ M ) )
32 nncn 
 |-  ( M e. NN -> M e. CC )
33 32 3ad2ant1 
 |-  ( ( M e. NN /\ N e. NN /\ N || M ) -> M e. CC )
34 nncn 
 |-  ( N e. NN -> N e. CC )
35 34 3ad2ant2 
 |-  ( ( M e. NN /\ N e. NN /\ N || M ) -> N e. CC )
36 nnne0 
 |-  ( N e. NN -> N =/= 0 )
37 36 3ad2ant2 
 |-  ( ( M e. NN /\ N e. NN /\ N || M ) -> N =/= 0 )
38 33 35 37 divcan1d 
 |-  ( ( M e. NN /\ N e. NN /\ N || M ) -> ( ( M / N ) x. N ) = M )
39 38 adantr 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> ( ( M / N ) x. N ) = M )
40 39 eqcomd 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> M = ( ( M / N ) x. N ) )
41 40 oveq2d 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> ( ( x x. N ) gcd M ) = ( ( x x. N ) gcd ( ( M / N ) x. N ) ) )
42 nndivdvds 
 |-  ( ( M e. NN /\ N e. NN ) -> ( N || M <-> ( M / N ) e. NN ) )
43 42 biimp3a 
 |-  ( ( M e. NN /\ N e. NN /\ N || M ) -> ( M / N ) e. NN )
44 43 nnzd 
 |-  ( ( M e. NN /\ N e. NN /\ N || M ) -> ( M / N ) e. ZZ )
45 44 adantr 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> ( M / N ) e. ZZ )
46 mulgcdr 
 |-  ( ( x e. ZZ /\ ( M / N ) e. ZZ /\ N e. NN0 ) -> ( ( x x. N ) gcd ( ( M / N ) x. N ) ) = ( ( x gcd ( M / N ) ) x. N ) )
47 17 45 11 46 syl3anc 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> ( ( x x. N ) gcd ( ( M / N ) x. N ) ) = ( ( x gcd ( M / N ) ) x. N ) )
48 simprr 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> ( x gcd ( M / N ) ) = 1 )
49 48 oveq1d 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> ( ( x gcd ( M / N ) ) x. N ) = ( 1 x. N ) )
50 35 mullidd 
 |-  ( ( M e. NN /\ N e. NN /\ N || M ) -> ( 1 x. N ) = N )
51 50 adantr 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> ( 1 x. N ) = N )
52 49 51 eqtrd 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> ( ( x gcd ( M / N ) ) x. N ) = N )
53 41 47 52 3eqtrd 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> ( ( x x. N ) gcd M ) = N )
54 oveq1 
 |-  ( z = ( x x. N ) -> ( z gcd M ) = ( ( x x. N ) gcd M ) )
55 54 eqeq1d 
 |-  ( z = ( x x. N ) -> ( ( z gcd M ) = N <-> ( ( x x. N ) gcd M ) = N ) )
56 55 2 elrab2 
 |-  ( ( x x. N ) e. B <-> ( ( x x. N ) e. ( 0 ..^ M ) /\ ( ( x x. N ) gcd M ) = N ) )
57 31 53 56 sylanbrc 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ ( x gcd ( M / N ) ) = 1 ) ) -> ( x x. N ) e. B )
58 6 57 sylan2b 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ x e. A ) -> ( x x. N ) e. B )
59 oveq1 
 |-  ( z = w -> ( z gcd M ) = ( w gcd M ) )
60 59 eqeq1d 
 |-  ( z = w -> ( ( z gcd M ) = N <-> ( w gcd M ) = N ) )
61 60 2 elrab2 
 |-  ( w e. B <-> ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) )
62 simprr 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> ( w gcd M ) = N )
63 elfzoelz 
 |-  ( w e. ( 0 ..^ M ) -> w e. ZZ )
64 63 ad2antrl 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> w e. ZZ )
65 simpl1 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> M e. NN )
66 65 nnzd 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> M e. ZZ )
67 gcddvds 
 |-  ( ( w e. ZZ /\ M e. ZZ ) -> ( ( w gcd M ) || w /\ ( w gcd M ) || M ) )
68 64 66 67 syl2anc 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> ( ( w gcd M ) || w /\ ( w gcd M ) || M ) )
69 68 simpld 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> ( w gcd M ) || w )
70 62 69 eqbrtrrd 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> N || w )
71 nnz 
 |-  ( N e. NN -> N e. ZZ )
72 71 3ad2ant2 
 |-  ( ( M e. NN /\ N e. NN /\ N || M ) -> N e. ZZ )
73 72 adantr 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> N e. ZZ )
74 37 adantr 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> N =/= 0 )
75 dvdsval2 
 |-  ( ( N e. ZZ /\ N =/= 0 /\ w e. ZZ ) -> ( N || w <-> ( w / N ) e. ZZ ) )
76 73 74 64 75 syl3anc 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> ( N || w <-> ( w / N ) e. ZZ ) )
77 70 76 mpbid 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> ( w / N ) e. ZZ )
78 elfzofz 
 |-  ( w e. ( 0 ..^ M ) -> w e. ( 0 ... M ) )
79 78 ad2antrl 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> w e. ( 0 ... M ) )
80 elfznn0 
 |-  ( w e. ( 0 ... M ) -> w e. NN0 )
81 nn0re 
 |-  ( w e. NN0 -> w e. RR )
82 nn0ge0 
 |-  ( w e. NN0 -> 0 <_ w )
83 81 82 jca 
 |-  ( w e. NN0 -> ( w e. RR /\ 0 <_ w ) )
84 79 80 83 3syl 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> ( w e. RR /\ 0 <_ w ) )
85 25 adantr 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> ( N e. RR /\ 0 < N ) )
86 divge0 
 |-  ( ( ( w e. RR /\ 0 <_ w ) /\ ( N e. RR /\ 0 < N ) ) -> 0 <_ ( w / N ) )
87 84 85 86 syl2anc 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> 0 <_ ( w / N ) )
88 elnn0z 
 |-  ( ( w / N ) e. NN0 <-> ( ( w / N ) e. ZZ /\ 0 <_ ( w / N ) ) )
89 77 87 88 sylanbrc 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> ( w / N ) e. NN0 )
90 43 adantr 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> ( M / N ) e. NN )
91 elfzolt2 
 |-  ( w e. ( 0 ..^ M ) -> w < M )
92 91 ad2antrl 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> w < M )
93 64 zred 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> w e. RR )
94 20 adantr 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> M e. RR )
95 ltdiv1 
 |-  ( ( w e. RR /\ M e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( w < M <-> ( w / N ) < ( M / N ) ) )
96 93 94 85 95 syl3anc 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> ( w < M <-> ( w / N ) < ( M / N ) ) )
97 92 96 mpbid 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> ( w / N ) < ( M / N ) )
98 elfzo0 
 |-  ( ( w / N ) e. ( 0 ..^ ( M / N ) ) <-> ( ( w / N ) e. NN0 /\ ( M / N ) e. NN /\ ( w / N ) < ( M / N ) ) )
99 89 90 97 98 syl3anbrc 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> ( w / N ) e. ( 0 ..^ ( M / N ) ) )
100 62 oveq1d 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> ( ( w gcd M ) / N ) = ( N / N ) )
101 simpl2 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> N e. NN )
102 simpl3 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> N || M )
103 gcddiv 
 |-  ( ( ( w e. ZZ /\ M e. ZZ /\ N e. NN ) /\ ( N || w /\ N || M ) ) -> ( ( w gcd M ) / N ) = ( ( w / N ) gcd ( M / N ) ) )
104 64 66 101 70 102 103 syl32anc 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> ( ( w gcd M ) / N ) = ( ( w / N ) gcd ( M / N ) ) )
105 35 37 dividd 
 |-  ( ( M e. NN /\ N e. NN /\ N || M ) -> ( N / N ) = 1 )
106 105 adantr 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> ( N / N ) = 1 )
107 100 104 106 3eqtr3d 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> ( ( w / N ) gcd ( M / N ) ) = 1 )
108 oveq1 
 |-  ( y = ( w / N ) -> ( y gcd ( M / N ) ) = ( ( w / N ) gcd ( M / N ) ) )
109 108 eqeq1d 
 |-  ( y = ( w / N ) -> ( ( y gcd ( M / N ) ) = 1 <-> ( ( w / N ) gcd ( M / N ) ) = 1 ) )
110 109 1 elrab2 
 |-  ( ( w / N ) e. A <-> ( ( w / N ) e. ( 0 ..^ ( M / N ) ) /\ ( ( w / N ) gcd ( M / N ) ) = 1 ) )
111 99 107 110 sylanbrc 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( w e. ( 0 ..^ M ) /\ ( w gcd M ) = N ) ) -> ( w / N ) e. A )
112 61 111 sylan2b 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ w e. B ) -> ( w / N ) e. A )
113 6 simplbi 
 |-  ( x e. A -> x e. ( 0 ..^ ( M / N ) ) )
114 61 simplbi 
 |-  ( w e. B -> w e. ( 0 ..^ M ) )
115 113 114 anim12i 
 |-  ( ( x e. A /\ w e. B ) -> ( x e. ( 0 ..^ ( M / N ) ) /\ w e. ( 0 ..^ M ) ) )
116 63 ad2antll 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ w e. ( 0 ..^ M ) ) ) -> w e. ZZ )
117 116 zcnd 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ w e. ( 0 ..^ M ) ) ) -> w e. CC )
118 35 adantr 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ w e. ( 0 ..^ M ) ) ) -> N e. CC )
119 37 adantr 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ w e. ( 0 ..^ M ) ) ) -> N =/= 0 )
120 117 118 119 divcan1d 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ w e. ( 0 ..^ M ) ) ) -> ( ( w / N ) x. N ) = w )
121 120 eqcomd 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ w e. ( 0 ..^ M ) ) ) -> w = ( ( w / N ) x. N ) )
122 oveq1 
 |-  ( x = ( w / N ) -> ( x x. N ) = ( ( w / N ) x. N ) )
123 122 eqeq2d 
 |-  ( x = ( w / N ) -> ( w = ( x x. N ) <-> w = ( ( w / N ) x. N ) ) )
124 121 123 syl5ibrcom 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ w e. ( 0 ..^ M ) ) ) -> ( x = ( w / N ) -> w = ( x x. N ) ) )
125 16 ad2antrl 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ w e. ( 0 ..^ M ) ) ) -> x e. ZZ )
126 125 zcnd 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ w e. ( 0 ..^ M ) ) ) -> x e. CC )
127 126 118 119 divcan4d 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ w e. ( 0 ..^ M ) ) ) -> ( ( x x. N ) / N ) = x )
128 127 eqcomd 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ w e. ( 0 ..^ M ) ) ) -> x = ( ( x x. N ) / N ) )
129 oveq1 
 |-  ( w = ( x x. N ) -> ( w / N ) = ( ( x x. N ) / N ) )
130 129 eqeq2d 
 |-  ( w = ( x x. N ) -> ( x = ( w / N ) <-> x = ( ( x x. N ) / N ) ) )
131 128 130 syl5ibrcom 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ w e. ( 0 ..^ M ) ) ) -> ( w = ( x x. N ) -> x = ( w / N ) ) )
132 124 131 impbid 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. ( 0 ..^ ( M / N ) ) /\ w e. ( 0 ..^ M ) ) ) -> ( x = ( w / N ) <-> w = ( x x. N ) ) )
133 115 132 sylan2 
 |-  ( ( ( M e. NN /\ N e. NN /\ N || M ) /\ ( x e. A /\ w e. B ) ) -> ( x = ( w / N ) <-> w = ( x x. N ) ) )
134 3 58 112 133 f1o2d 
 |-  ( ( M e. NN /\ N e. NN /\ N || M ) -> F : A -1-1-onto-> B )