Metamath Proof Explorer

Theorem jm2.20nn

Description: Lemma 2.20 of JonesMatijasevic p. 696, the "first step down lemma". (Contributed by Stefan O'Rear, 27-Sep-2014)

Ref Expression
Assertion jm2.20nn 
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( ( A rmY N ) ^ 2 ) || ( A rmY M ) <-> ( N x. ( A rmY N ) ) || M ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> A e. ( ZZ>= ` 2 ) )
2 nnz 
 |-  ( N e. NN -> N e. ZZ )
3 2 3ad2ant3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> N e. ZZ )
4 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
5 4 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. ZZ )
6 1 3 5 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( A rmY N ) e. ZZ )
7 6 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( A rmY N ) e. CC )
8 7 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( A rmY N ) e. CC )
9 8 sqvald 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmY N ) ^ 2 ) = ( ( A rmY N ) x. ( A rmY N ) ) )
10 zsqcl 
 |-  ( ( A rmY N ) e. ZZ -> ( ( A rmY N ) ^ 2 ) e. ZZ )
11 6 10 syl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( A rmY N ) ^ 2 ) e. ZZ )
12 11 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmY N ) ^ 2 ) e. ZZ )
13 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
14 13 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
15 1 3 14 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( A rmX N ) e. NN0 )
16 15 nn0zd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( A rmX N ) e. ZZ )
17 16 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( A rmX N ) e. ZZ )
18 7 sqvald 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( A rmY N ) ^ 2 ) = ( ( A rmY N ) x. ( A rmY N ) ) )
19 18 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmY N ) ^ 2 ) = ( ( A rmY N ) x. ( A rmY N ) ) )
20 simpr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmY N ) ^ 2 ) || ( A rmY M ) )
21 19 20 eqbrtrrd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmY N ) x. ( A rmY N ) ) || ( A rmY M ) )
22 nnz 
 |-  ( M e. NN -> M e. ZZ )
23 22 3ad2ant2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> M e. ZZ )
24 4 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( A rmY M ) e. ZZ )
25 1 23 24 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( A rmY M ) e. ZZ )
26 muldvds1 
 |-  ( ( ( A rmY N ) e. ZZ /\ ( A rmY N ) e. ZZ /\ ( A rmY M ) e. ZZ ) -> ( ( ( A rmY N ) x. ( A rmY N ) ) || ( A rmY M ) -> ( A rmY N ) || ( A rmY M ) ) )
27 6 6 25 26 syl3anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( ( A rmY N ) x. ( A rmY N ) ) || ( A rmY M ) -> ( A rmY N ) || ( A rmY M ) ) )
28 27 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( ( A rmY N ) x. ( A rmY N ) ) || ( A rmY M ) -> ( A rmY N ) || ( A rmY M ) ) )
29 21 28 mpd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( A rmY N ) || ( A rmY M ) )
30 simpl1 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> A e. ( ZZ>= ` 2 ) )
31 3 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> N e. ZZ )
32 23 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> M e. ZZ )
33 jm2.19 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ M e. ZZ ) -> ( N || M <-> ( A rmY N ) || ( A rmY M ) ) )
34 30 31 32 33 syl3anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( N || M <-> ( A rmY N ) || ( A rmY M ) ) )
35 29 34 mpbird 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> N || M )
36 simpl2 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> M e. NN )
37 simpl3 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> N e. NN )
38 nndivdvds 
 |-  ( ( M e. NN /\ N e. NN ) -> ( N || M <-> ( M / N ) e. NN ) )
39 36 37 38 syl2anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( N || M <-> ( M / N ) e. NN ) )
40 35 39 mpbid 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( M / N ) e. NN )
41 nnm1nn0 
 |-  ( ( M / N ) e. NN -> ( ( M / N ) - 1 ) e. NN0 )
42 40 41 syl 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( M / N ) - 1 ) e. NN0 )
43 zexpcl 
 |-  ( ( ( A rmX N ) e. ZZ /\ ( ( M / N ) - 1 ) e. NN0 ) -> ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) e. ZZ )
44 17 42 43 syl2anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) e. ZZ )
45 40 nnzd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( M / N ) e. ZZ )
46 6 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( A rmY N ) e. ZZ )
47 45 46 zmulcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( M / N ) x. ( A rmY N ) ) e. ZZ )
48 25 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( A rmY M ) e. ZZ )
49 nncn 
 |-  ( M e. NN -> M e. CC )
50 49 3ad2ant2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> M e. CC )
51 nncn 
 |-  ( N e. NN -> N e. CC )
52 51 3ad2ant3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> N e. CC )
53 nnne0 
 |-  ( N e. NN -> N =/= 0 )
54 53 3ad2ant3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> N =/= 0 )
55 50 52 54 divcan2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( N x. ( M / N ) ) = M )
56 55 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( A rmY ( N x. ( M / N ) ) ) = ( A rmY M ) )
57 56 25 eqeltrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( A rmY ( N x. ( M / N ) ) ) e. ZZ )
58 57 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( A rmY ( N x. ( M / N ) ) ) e. ZZ )
59 44 46 zmulcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) e. ZZ )
60 45 59 zmulcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) e. ZZ )
61 58 60 zsubcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmY ( N x. ( M / N ) ) ) - ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) ) e. ZZ )
62 3nn0 
 |-  3 e. NN0
63 62 a1i 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> 3 e. NN0 )
64 zexpcl 
 |-  ( ( ( A rmY N ) e. ZZ /\ 3 e. NN0 ) -> ( ( A rmY N ) ^ 3 ) e. ZZ )
65 6 63 64 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( A rmY N ) ^ 3 ) e. ZZ )
66 65 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmY N ) ^ 3 ) e. ZZ )
67 2nn0 
 |-  2 e. NN0
68 67 a1i 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> 2 e. NN0 )
69 3z 
 |-  3 e. ZZ
70 2re 
 |-  2 e. RR
71 3re 
 |-  3 e. RR
72 2lt3 
 |-  2 < 3
73 70 71 72 ltleii 
 |-  2 <_ 3
74 2z 
 |-  2 e. ZZ
75 74 eluz1i 
 |-  ( 3 e. ( ZZ>= ` 2 ) <-> ( 3 e. ZZ /\ 2 <_ 3 ) )
76 69 73 75 mpbir2an 
 |-  3 e. ( ZZ>= ` 2 )
77 76 a1i 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> 3 e. ( ZZ>= ` 2 ) )
78 dvdsexp 
 |-  ( ( ( A rmY N ) e. ZZ /\ 2 e. NN0 /\ 3 e. ( ZZ>= ` 2 ) ) -> ( ( A rmY N ) ^ 2 ) || ( ( A rmY N ) ^ 3 ) )
79 6 68 77 78 syl3anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( A rmY N ) ^ 2 ) || ( ( A rmY N ) ^ 3 ) )
80 79 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmY N ) ^ 2 ) || ( ( A rmY N ) ^ 3 ) )
81 jm2.23 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ ( M / N ) e. NN ) -> ( ( A rmY N ) ^ 3 ) || ( ( A rmY ( N x. ( M / N ) ) ) - ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) ) )
82 30 31 40 81 syl3anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmY N ) ^ 3 ) || ( ( A rmY ( N x. ( M / N ) ) ) - ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) ) )
83 12 66 61 80 82 dvdstrd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmY N ) ^ 2 ) || ( ( A rmY ( N x. ( M / N ) ) ) - ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) ) )
84 dvds2sub 
 |-  ( ( ( ( A rmY N ) ^ 2 ) e. ZZ /\ ( A rmY M ) e. ZZ /\ ( ( A rmY ( N x. ( M / N ) ) ) - ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) ) e. ZZ ) -> ( ( ( ( A rmY N ) ^ 2 ) || ( A rmY M ) /\ ( ( A rmY N ) ^ 2 ) || ( ( A rmY ( N x. ( M / N ) ) ) - ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) ) ) -> ( ( A rmY N ) ^ 2 ) || ( ( A rmY M ) - ( ( A rmY ( N x. ( M / N ) ) ) - ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) ) ) ) )
85 84 imp 
 |-  ( ( ( ( ( A rmY N ) ^ 2 ) e. ZZ /\ ( A rmY M ) e. ZZ /\ ( ( A rmY ( N x. ( M / N ) ) ) - ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) ) e. ZZ ) /\ ( ( ( A rmY N ) ^ 2 ) || ( A rmY M ) /\ ( ( A rmY N ) ^ 2 ) || ( ( A rmY ( N x. ( M / N ) ) ) - ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) ) ) ) -> ( ( A rmY N ) ^ 2 ) || ( ( A rmY M ) - ( ( A rmY ( N x. ( M / N ) ) ) - ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) ) ) )
86 12 48 61 20 83 85 syl32anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmY N ) ^ 2 ) || ( ( A rmY M ) - ( ( A rmY ( N x. ( M / N ) ) ) - ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) ) ) )
87 55 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( N x. ( M / N ) ) = M )
88 87 oveq2d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( A rmY ( N x. ( M / N ) ) ) = ( A rmY M ) )
89 88 oveq1d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmY ( N x. ( M / N ) ) ) - ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) ) = ( ( A rmY M ) - ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) ) )
90 89 oveq2d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmY M ) - ( ( A rmY ( N x. ( M / N ) ) ) - ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) ) ) = ( ( A rmY M ) - ( ( A rmY M ) - ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) ) ) )
91 25 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( A rmY M ) e. CC )
92 91 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( A rmY M ) e. CC )
93 60 zcnd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) e. CC )
94 92 93 nncand 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmY M ) - ( ( A rmY M ) - ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) ) ) = ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) )
95 45 zcnd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( M / N ) e. CC )
96 44 zcnd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) e. CC )
97 95 96 8 mul12d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) = ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( ( M / N ) x. ( A rmY N ) ) ) )
98 94 97 eqtrd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmY M ) - ( ( A rmY M ) - ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) ) ) = ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( ( M / N ) x. ( A rmY N ) ) ) )
99 90 98 eqtrd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmY M ) - ( ( A rmY ( N x. ( M / N ) ) ) - ( ( M / N ) x. ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( A rmY N ) ) ) ) ) = ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( ( M / N ) x. ( A rmY N ) ) ) )
100 86 99 breqtrd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmY N ) ^ 2 ) || ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( ( M / N ) x. ( A rmY N ) ) ) )
101 6 16 gcdcomd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( A rmY N ) gcd ( A rmX N ) ) = ( ( A rmX N ) gcd ( A rmY N ) ) )
102 jm2.19lem1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) gcd ( A rmY N ) ) = 1 )
103 1 3 102 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( A rmX N ) gcd ( A rmY N ) ) = 1 )
104 101 103 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( A rmY N ) gcd ( A rmX N ) ) = 1 )
105 104 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmY N ) gcd ( A rmX N ) ) = 1 )
106 67 a1i 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> 2 e. NN0 )
107 rpexp12i 
 |-  ( ( ( A rmY N ) e. ZZ /\ ( A rmX N ) e. ZZ /\ ( 2 e. NN0 /\ ( ( M / N ) - 1 ) e. NN0 ) ) -> ( ( ( A rmY N ) gcd ( A rmX N ) ) = 1 -> ( ( ( A rmY N ) ^ 2 ) gcd ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) ) = 1 ) )
108 46 17 106 42 107 syl112anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( ( A rmY N ) gcd ( A rmX N ) ) = 1 -> ( ( ( A rmY N ) ^ 2 ) gcd ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) ) = 1 ) )
109 105 108 mpd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( ( A rmY N ) ^ 2 ) gcd ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) ) = 1 )
110 coprmdvds 
 |-  ( ( ( ( A rmY N ) ^ 2 ) e. ZZ /\ ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) e. ZZ /\ ( ( M / N ) x. ( A rmY N ) ) e. ZZ ) -> ( ( ( ( A rmY N ) ^ 2 ) || ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( ( M / N ) x. ( A rmY N ) ) ) /\ ( ( ( A rmY N ) ^ 2 ) gcd ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) ) = 1 ) -> ( ( A rmY N ) ^ 2 ) || ( ( M / N ) x. ( A rmY N ) ) ) )
111 110 imp 
 |-  ( ( ( ( ( A rmY N ) ^ 2 ) e. ZZ /\ ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) e. ZZ /\ ( ( M / N ) x. ( A rmY N ) ) e. ZZ ) /\ ( ( ( A rmY N ) ^ 2 ) || ( ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) x. ( ( M / N ) x. ( A rmY N ) ) ) /\ ( ( ( A rmY N ) ^ 2 ) gcd ( ( A rmX N ) ^ ( ( M / N ) - 1 ) ) ) = 1 ) ) -> ( ( A rmY N ) ^ 2 ) || ( ( M / N ) x. ( A rmY N ) ) )
112 12 44 47 100 109 111 syl32anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmY N ) ^ 2 ) || ( ( M / N ) x. ( A rmY N ) ) )
113 9 112 eqbrtrrd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( A rmY N ) x. ( A rmY N ) ) || ( ( M / N ) x. ( A rmY N ) ) )
114 rmy0 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY 0 ) = 0 )
115 114 3ad2ant1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( A rmY 0 ) = 0 )
116 nngt0 
 |-  ( N e. NN -> 0 < N )
117 116 3ad2ant3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> 0 < N )
118 0zd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> 0 e. ZZ )
119 ltrmy 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ 0 e. ZZ /\ N e. ZZ ) -> ( 0 < N <-> ( A rmY 0 ) < ( A rmY N ) ) )
120 1 118 3 119 syl3anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( 0 < N <-> ( A rmY 0 ) < ( A rmY N ) ) )
121 117 120 mpbid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( A rmY 0 ) < ( A rmY N ) )
122 115 121 eqbrtrrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> 0 < ( A rmY N ) )
123 elnnz 
 |-  ( ( A rmY N ) e. NN <-> ( ( A rmY N ) e. ZZ /\ 0 < ( A rmY N ) ) )
124 6 122 123 sylanbrc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( A rmY N ) e. NN )
125 nnne0 
 |-  ( ( A rmY N ) e. NN -> ( A rmY N ) =/= 0 )
126 124 125 syl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( A rmY N ) =/= 0 )
127 126 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( A rmY N ) =/= 0 )
128 dvdsmulcr 
 |-  ( ( ( A rmY N ) e. ZZ /\ ( M / N ) e. ZZ /\ ( ( A rmY N ) e. ZZ /\ ( A rmY N ) =/= 0 ) ) -> ( ( ( A rmY N ) x. ( A rmY N ) ) || ( ( M / N ) x. ( A rmY N ) ) <-> ( A rmY N ) || ( M / N ) ) )
129 46 45 46 127 128 syl112anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( ( A rmY N ) x. ( A rmY N ) ) || ( ( M / N ) x. ( A rmY N ) ) <-> ( A rmY N ) || ( M / N ) ) )
130 113 129 mpbid 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( A rmY N ) || ( M / N ) )
131 54 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> N =/= 0 )
132 dvdscmulr 
 |-  ( ( ( A rmY N ) e. ZZ /\ ( M / N ) e. ZZ /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( N x. ( A rmY N ) ) || ( N x. ( M / N ) ) <-> ( A rmY N ) || ( M / N ) ) )
133 46 45 31 131 132 syl112anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( ( N x. ( A rmY N ) ) || ( N x. ( M / N ) ) <-> ( A rmY N ) || ( M / N ) ) )
134 130 133 mpbird 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( N x. ( A rmY N ) ) || ( N x. ( M / N ) ) )
135 134 87 breqtrd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( ( A rmY N ) ^ 2 ) || ( A rmY M ) ) -> ( N x. ( A rmY N ) ) || M )
136 11 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( N x. ( A rmY N ) ) || M ) -> ( ( A rmY N ) ^ 2 ) e. ZZ )
137 3 6 zmulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( N x. ( A rmY N ) ) e. ZZ )
138 4 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N x. ( A rmY N ) ) e. ZZ ) -> ( A rmY ( N x. ( A rmY N ) ) ) e. ZZ )
139 1 137 138 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( A rmY ( N x. ( A rmY N ) ) ) e. ZZ )
140 139 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( N x. ( A rmY N ) ) || M ) -> ( A rmY ( N x. ( A rmY N ) ) ) e. ZZ )
141 25 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( N x. ( A rmY N ) ) || M ) -> ( A rmY M ) e. ZZ )
142 nnm1nn0 
 |-  ( ( A rmY N ) e. NN -> ( ( A rmY N ) - 1 ) e. NN0 )
143 124 142 syl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( A rmY N ) - 1 ) e. NN0 )
144 zexpcl 
 |-  ( ( ( A rmX N ) e. ZZ /\ ( ( A rmY N ) - 1 ) e. NN0 ) -> ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) e. ZZ )
145 16 143 144 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) e. ZZ )
146 dvdsmul2 
 |-  ( ( ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) e. ZZ /\ ( ( A rmY N ) ^ 2 ) e. ZZ ) -> ( ( A rmY N ) ^ 2 ) || ( ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) x. ( ( A rmY N ) ^ 2 ) ) )
147 145 11 146 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( A rmY N ) ^ 2 ) || ( ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) x. ( ( A rmY N ) ^ 2 ) ) )
148 18 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) x. ( ( A rmY N ) ^ 2 ) ) = ( ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) x. ( ( A rmY N ) x. ( A rmY N ) ) ) )
149 145 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) e. CC )
150 149 7 7 mul12d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) x. ( ( A rmY N ) x. ( A rmY N ) ) ) = ( ( A rmY N ) x. ( ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) x. ( A rmY N ) ) ) )
151 148 150 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) x. ( ( A rmY N ) ^ 2 ) ) = ( ( A rmY N ) x. ( ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) x. ( A rmY N ) ) ) )
152 147 151 breqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( A rmY N ) ^ 2 ) || ( ( A rmY N ) x. ( ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) x. ( A rmY N ) ) ) )
153 145 6 zmulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) x. ( A rmY N ) ) e. ZZ )
154 6 153 zmulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( A rmY N ) x. ( ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) x. ( A rmY N ) ) ) e. ZZ )
155 139 154 zsubcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( A rmY ( N x. ( A rmY N ) ) ) - ( ( A rmY N ) x. ( ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) x. ( A rmY N ) ) ) ) e. ZZ )
156 jm2.23 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ ( A rmY N ) e. NN ) -> ( ( A rmY N ) ^ 3 ) || ( ( A rmY ( N x. ( A rmY N ) ) ) - ( ( A rmY N ) x. ( ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) x. ( A rmY N ) ) ) ) )
157 1 3 124 156 syl3anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( A rmY N ) ^ 3 ) || ( ( A rmY ( N x. ( A rmY N ) ) ) - ( ( A rmY N ) x. ( ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) x. ( A rmY N ) ) ) ) )
158 11 65 155 79 157 dvdstrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( A rmY N ) ^ 2 ) || ( ( A rmY ( N x. ( A rmY N ) ) ) - ( ( A rmY N ) x. ( ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) x. ( A rmY N ) ) ) ) )
159 dvdssub2 
 |-  ( ( ( ( ( A rmY N ) ^ 2 ) e. ZZ /\ ( A rmY ( N x. ( A rmY N ) ) ) e. ZZ /\ ( ( A rmY N ) x. ( ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) x. ( A rmY N ) ) ) e. ZZ ) /\ ( ( A rmY N ) ^ 2 ) || ( ( A rmY ( N x. ( A rmY N ) ) ) - ( ( A rmY N ) x. ( ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) x. ( A rmY N ) ) ) ) ) -> ( ( ( A rmY N ) ^ 2 ) || ( A rmY ( N x. ( A rmY N ) ) ) <-> ( ( A rmY N ) ^ 2 ) || ( ( A rmY N ) x. ( ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) x. ( A rmY N ) ) ) ) )
160 11 139 154 158 159 syl31anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( ( A rmY N ) ^ 2 ) || ( A rmY ( N x. ( A rmY N ) ) ) <-> ( ( A rmY N ) ^ 2 ) || ( ( A rmY N ) x. ( ( ( A rmX N ) ^ ( ( A rmY N ) - 1 ) ) x. ( A rmY N ) ) ) ) )
161 152 160 mpbird 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( A rmY N ) ^ 2 ) || ( A rmY ( N x. ( A rmY N ) ) ) )
162 161 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( N x. ( A rmY N ) ) || M ) -> ( ( A rmY N ) ^ 2 ) || ( A rmY ( N x. ( A rmY N ) ) ) )
163 simpr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( N x. ( A rmY N ) ) || M ) -> ( N x. ( A rmY N ) ) || M )
164 simpl1 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( N x. ( A rmY N ) ) || M ) -> A e. ( ZZ>= ` 2 ) )
165 137 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( N x. ( A rmY N ) ) || M ) -> ( N x. ( A rmY N ) ) e. ZZ )
166 23 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( N x. ( A rmY N ) ) || M ) -> M e. ZZ )
167 jm2.19 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N x. ( A rmY N ) ) e. ZZ /\ M e. ZZ ) -> ( ( N x. ( A rmY N ) ) || M <-> ( A rmY ( N x. ( A rmY N ) ) ) || ( A rmY M ) ) )
168 164 165 166 167 syl3anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( N x. ( A rmY N ) ) || M ) -> ( ( N x. ( A rmY N ) ) || M <-> ( A rmY ( N x. ( A rmY N ) ) ) || ( A rmY M ) ) )
169 163 168 mpbid 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( N x. ( A rmY N ) ) || M ) -> ( A rmY ( N x. ( A rmY N ) ) ) || ( A rmY M ) )
170 136 140 141 162 169 dvdstrd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) /\ ( N x. ( A rmY N ) ) || M ) -> ( ( A rmY N ) ^ 2 ) || ( A rmY M ) )
171 135 170 impbida 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( ( A rmY N ) ^ 2 ) || ( A rmY M ) <-> ( N x. ( A rmY N ) ) || M ) )