Metamath Proof Explorer

Theorem jm2.19lem3

Description: Lemma for jm2.19 . (Contributed by Stefan O'Rear, 26-Sep-2014)

Ref Expression
Assertion jm2.19lem3 
|- ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) /\ I e. NN0 ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( I x. M ) ) ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( a = 0 -> ( a x. M ) = ( 0 x. M ) )
2 1 oveq2d 
 |-  ( a = 0 -> ( N + ( a x. M ) ) = ( N + ( 0 x. M ) ) )
3 2 oveq2d 
 |-  ( a = 0 -> ( A rmY ( N + ( a x. M ) ) ) = ( A rmY ( N + ( 0 x. M ) ) ) )
4 3 breq2d 
 |-  ( a = 0 -> ( ( A rmY M ) || ( A rmY ( N + ( a x. M ) ) ) <-> ( A rmY M ) || ( A rmY ( N + ( 0 x. M ) ) ) ) )
5 4 bibi2d 
 |-  ( a = 0 -> ( ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( a x. M ) ) ) ) <-> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( 0 x. M ) ) ) ) ) )
6 5 imbi2d 
 |-  ( a = 0 -> ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( a x. M ) ) ) ) ) <-> ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( 0 x. M ) ) ) ) ) ) )
7 oveq1 
 |-  ( a = b -> ( a x. M ) = ( b x. M ) )
8 7 oveq2d 
 |-  ( a = b -> ( N + ( a x. M ) ) = ( N + ( b x. M ) ) )
9 8 oveq2d 
 |-  ( a = b -> ( A rmY ( N + ( a x. M ) ) ) = ( A rmY ( N + ( b x. M ) ) ) )
10 9 breq2d 
 |-  ( a = b -> ( ( A rmY M ) || ( A rmY ( N + ( a x. M ) ) ) <-> ( A rmY M ) || ( A rmY ( N + ( b x. M ) ) ) ) )
11 10 bibi2d 
 |-  ( a = b -> ( ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( a x. M ) ) ) ) <-> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( b x. M ) ) ) ) ) )
12 11 imbi2d 
 |-  ( a = b -> ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( a x. M ) ) ) ) ) <-> ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( b x. M ) ) ) ) ) ) )
13 oveq1 
 |-  ( a = ( b + 1 ) -> ( a x. M ) = ( ( b + 1 ) x. M ) )
14 13 oveq2d 
 |-  ( a = ( b + 1 ) -> ( N + ( a x. M ) ) = ( N + ( ( b + 1 ) x. M ) ) )
15 14 oveq2d 
 |-  ( a = ( b + 1 ) -> ( A rmY ( N + ( a x. M ) ) ) = ( A rmY ( N + ( ( b + 1 ) x. M ) ) ) )
16 15 breq2d 
 |-  ( a = ( b + 1 ) -> ( ( A rmY M ) || ( A rmY ( N + ( a x. M ) ) ) <-> ( A rmY M ) || ( A rmY ( N + ( ( b + 1 ) x. M ) ) ) ) )
17 16 bibi2d 
 |-  ( a = ( b + 1 ) -> ( ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( a x. M ) ) ) ) <-> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( ( b + 1 ) x. M ) ) ) ) ) )
18 17 imbi2d 
 |-  ( a = ( b + 1 ) -> ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( a x. M ) ) ) ) ) <-> ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( ( b + 1 ) x. M ) ) ) ) ) ) )
19 oveq1 
 |-  ( a = I -> ( a x. M ) = ( I x. M ) )
20 19 oveq2d 
 |-  ( a = I -> ( N + ( a x. M ) ) = ( N + ( I x. M ) ) )
21 20 oveq2d 
 |-  ( a = I -> ( A rmY ( N + ( a x. M ) ) ) = ( A rmY ( N + ( I x. M ) ) ) )
22 21 breq2d 
 |-  ( a = I -> ( ( A rmY M ) || ( A rmY ( N + ( a x. M ) ) ) <-> ( A rmY M ) || ( A rmY ( N + ( I x. M ) ) ) ) )
23 22 bibi2d 
 |-  ( a = I -> ( ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( a x. M ) ) ) ) <-> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( I x. M ) ) ) ) ) )
24 23 imbi2d 
 |-  ( a = I -> ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( a x. M ) ) ) ) ) <-> ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( I x. M ) ) ) ) ) ) )
25 zcn 
 |-  ( M e. ZZ -> M e. CC )
26 25 ad2antrl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> M e. CC )
27 26 mul02d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( 0 x. M ) = 0 )
28 27 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( N + ( 0 x. M ) ) = ( N + 0 ) )
29 zcn 
 |-  ( N e. ZZ -> N e. CC )
30 29 ad2antll 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> N e. CC )
31 30 addid1d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( N + 0 ) = N )
32 28 31 eqtr2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> N = ( N + ( 0 x. M ) ) )
33 32 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( A rmY N ) = ( A rmY ( N + ( 0 x. M ) ) ) )
34 33 breq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( 0 x. M ) ) ) ) )
35 simp3 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( b x. M ) ) ) ) ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( b x. M ) ) ) ) )
36 simprl 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> A e. ( ZZ>= ` 2 ) )
37 simprrl 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> M e. ZZ )
38 simprrr 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> N e. ZZ )
39 nn0z 
 |-  ( b e. NN0 -> b e. ZZ )
40 39 adantr 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> b e. ZZ )
41 40 37 zmulcld 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( b x. M ) e. ZZ )
42 38 41 zaddcld 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( N + ( b x. M ) ) e. ZZ )
43 jm2.19lem2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ ( N + ( b x. M ) ) e. ZZ ) -> ( ( A rmY M ) || ( A rmY ( N + ( b x. M ) ) ) <-> ( A rmY M ) || ( A rmY ( ( N + ( b x. M ) ) + M ) ) ) )
44 36 37 42 43 syl3anc 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmY M ) || ( A rmY ( N + ( b x. M ) ) ) <-> ( A rmY M ) || ( A rmY ( ( N + ( b x. M ) ) + M ) ) ) )
45 38 zcnd 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> N e. CC )
46 41 zcnd 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( b x. M ) e. CC )
47 37 zcnd 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> M e. CC )
48 45 46 47 addassd 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( N + ( b x. M ) ) + M ) = ( N + ( ( b x. M ) + M ) ) )
49 nn0cn 
 |-  ( b e. NN0 -> b e. CC )
50 49 adantr 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> b e. CC )
51 1cnd 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> 1 e. CC )
52 50 51 47 adddird 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( b + 1 ) x. M ) = ( ( b x. M ) + ( 1 x. M ) ) )
53 47 mulid2d 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( 1 x. M ) = M )
54 53 oveq2d 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( b x. M ) + ( 1 x. M ) ) = ( ( b x. M ) + M ) )
55 52 54 eqtr2d 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( b x. M ) + M ) = ( ( b + 1 ) x. M ) )
56 55 oveq2d 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( N + ( ( b x. M ) + M ) ) = ( N + ( ( b + 1 ) x. M ) ) )
57 48 56 eqtrd 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( N + ( b x. M ) ) + M ) = ( N + ( ( b + 1 ) x. M ) ) )
58 57 oveq2d 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmY ( ( N + ( b x. M ) ) + M ) ) = ( A rmY ( N + ( ( b + 1 ) x. M ) ) ) )
59 58 breq2d 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmY M ) || ( A rmY ( ( N + ( b x. M ) ) + M ) ) <-> ( A rmY M ) || ( A rmY ( N + ( ( b + 1 ) x. M ) ) ) ) )
60 44 59 bitrd 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmY M ) || ( A rmY ( N + ( b x. M ) ) ) <-> ( A rmY M ) || ( A rmY ( N + ( ( b + 1 ) x. M ) ) ) ) )
61 60 3adant3 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( b x. M ) ) ) ) ) -> ( ( A rmY M ) || ( A rmY ( N + ( b x. M ) ) ) <-> ( A rmY M ) || ( A rmY ( N + ( ( b + 1 ) x. M ) ) ) ) )
62 35 61 bitrd 
 |-  ( ( b e. NN0 /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( b x. M ) ) ) ) ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( ( b + 1 ) x. M ) ) ) ) )
63 62 3exp 
 |-  ( b e. NN0 -> ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( b x. M ) ) ) ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( ( b + 1 ) x. M ) ) ) ) ) ) )
64 63 a2d 
 |-  ( b e. NN0 -> ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( b x. M ) ) ) ) ) -> ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( ( b + 1 ) x. M ) ) ) ) ) ) )
65 6 12 18 24 34 64 nn0ind 
 |-  ( I e. NN0 -> ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( I x. M ) ) ) ) ) )
66 65 com12 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( I e. NN0 -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( I x. M ) ) ) ) ) )
67 66 3impia 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) /\ I e. NN0 ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( I x. M ) ) ) ) )