jm2.25

Description: Lemma for jm2.26 . Remainders mod X(2n) are negaperiodic mod 2n. (Contributed by Stefan O'Rear, 2-Oct-2014)

		Ref	Expression
	Assertion	jm2.25	\|- ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) /\ I e. ZZ ) -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( I x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( I x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		simprl	\|- ( ( I e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> A e. ( ZZ>= ` 2 ) )
2		simprrr	\|- ( ( I e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> N e. ZZ )
3		frmx	\|- rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
4	3	fovcl	\|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
5	4	nn0zd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. ZZ )
6	1 2 5	syl2anc	\|- ( ( I e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmX N ) e. ZZ )
7		simprrl	\|- ( ( I e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> M e. ZZ )
8		frmy	\|- rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
9	8	fovcl	\|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( A rmY M ) e. ZZ )
10	1 7 9	syl2anc	\|- ( ( I e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmY M ) e. ZZ )
11		congid	\|- ( ( ( A rmX N ) e. ZZ /\ ( A rmY M ) e. ZZ ) -> ( A rmX N ) \|\| ( ( A rmY M ) - ( A rmY M ) ) )
12	6 10 11	syl2anc	\|- ( ( I e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmX N ) \|\| ( ( A rmY M ) - ( A rmY M ) ) )
13		2cnd	\|- ( N e. ZZ -> 2 e. CC )
14		zcn	\|- ( N e. ZZ -> N e. CC )
15	13 14	mulcld	\|- ( N e. ZZ -> ( 2 x. N ) e. CC )
16	15	mul02d	\|- ( N e. ZZ -> ( 0 x. ( 2 x. N ) ) = 0 )
17	16	adantl	\|- ( ( M e. ZZ /\ N e. ZZ ) -> ( 0 x. ( 2 x. N ) ) = 0 )
18	17	oveq2d	\|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M + ( 0 x. ( 2 x. N ) ) ) = ( M + 0 ) )
19		zcn	\|- ( M e. ZZ -> M e. CC )
20	19	addid1d	\|- ( M e. ZZ -> ( M + 0 ) = M )
21	20	adantr	\|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M + 0 ) = M )
22	18 21	eqtrd	\|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M + ( 0 x. ( 2 x. N ) ) ) = M )
23	22	ad2antll	\|- ( ( I e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( M + ( 0 x. ( 2 x. N ) ) ) = M )
24	23	oveq2d	\|- ( ( I e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmY ( M + ( 0 x. ( 2 x. N ) ) ) ) = ( A rmY M ) )
25	24	oveq1d	\|- ( ( I e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmY ( M + ( 0 x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) = ( ( A rmY M ) - ( A rmY M ) ) )
26	12 25	breqtrrd	\|- ( ( I e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmX N ) \|\| ( ( A rmY ( M + ( 0 x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) )
27	26	orcd	\|- ( ( I e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( 0 x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( 0 x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) )
28	27	ex	\|- ( I e. ZZ -> ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( 0 x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( 0 x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) ) )
29		simprl	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> A e. ( ZZ>= ` 2 ) )
30		simprrr	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> N e. ZZ )
31	29 30 5	syl2anc	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmX N ) e. ZZ )
32		simprrl	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> M e. ZZ )
33	29 32 9	syl2anc	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmY M ) e. ZZ )
34		simpl	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> b e. ZZ )
35	34	peano2zd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( b + 1 ) e. ZZ )
36		eluzel2	\|- ( A e. ( ZZ>= ` 2 ) -> 2 e. ZZ )
37	36	ad2antrl	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> 2 e. ZZ )
38	37 30	zmulcld	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( 2 x. N ) e. ZZ )
39	35 38	zmulcld	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( b + 1 ) x. ( 2 x. N ) ) e. ZZ )
40	32 39	zaddcld	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) e. ZZ )
41	8	fovcl	\|- ( ( A e. ( ZZ>= ` 2 ) /\ ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) e. ZZ ) -> ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) e. ZZ )
42	29 40 41	syl2anc	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) e. ZZ )
43	34 38	zmulcld	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( b x. ( 2 x. N ) ) e. ZZ )
44	32 43	zaddcld	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( M + ( b x. ( 2 x. N ) ) ) e. ZZ )
45	8	fovcl	\|- ( ( A e. ( ZZ>= ` 2 ) /\ ( M + ( b x. ( 2 x. N ) ) ) e. ZZ ) -> ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) e. ZZ )
46	29 44 45	syl2anc	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) e. ZZ )
47	3	fovcl	\|- ( ( A e. ( ZZ>= ` 2 ) /\ ( 2 x. N ) e. ZZ ) -> ( A rmX ( 2 x. N ) ) e. NN0 )
48	47	nn0zd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ ( 2 x. N ) e. ZZ ) -> ( A rmX ( 2 x. N ) ) e. ZZ )
49	29 38 48	syl2anc	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmX ( 2 x. N ) ) e. ZZ )
50	46 49	zmulcld	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmX ( 2 x. N ) ) ) e. ZZ )
51	46	znegcld	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> -u ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) e. ZZ )
52	50 51	zsubcld	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmX ( 2 x. N ) ) ) - -u ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) ) e. ZZ )
53	3	fovcl	\|- ( ( A e. ( ZZ>= ` 2 ) /\ ( M + ( b x. ( 2 x. N ) ) ) e. ZZ ) -> ( A rmX ( M + ( b x. ( 2 x. N ) ) ) ) e. NN0 )
54	53	nn0zd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ ( M + ( b x. ( 2 x. N ) ) ) e. ZZ ) -> ( A rmX ( M + ( b x. ( 2 x. N ) ) ) ) e. ZZ )
55	29 44 54	syl2anc	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmX ( M + ( b x. ( 2 x. N ) ) ) ) e. ZZ )
56	8	fovcl	\|- ( ( A e. ( ZZ>= ` 2 ) /\ ( 2 x. N ) e. ZZ ) -> ( A rmY ( 2 x. N ) ) e. ZZ )
57	29 38 56	syl2anc	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmY ( 2 x. N ) ) e. ZZ )
58	55 57	zmulcld	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmX ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmY ( 2 x. N ) ) ) e. ZZ )
59	37 31	zmulcld	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( 2 x. ( A rmX N ) ) e. ZZ )
60		dvdsmul2	\|- ( ( ( 2 x. ( A rmX N ) ) e. ZZ /\ ( A rmX N ) e. ZZ ) -> ( A rmX N ) \|\| ( ( 2 x. ( A rmX N ) ) x. ( A rmX N ) ) )
61	59 31 60	syl2anc	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmX N ) \|\| ( ( 2 x. ( A rmX N ) ) x. ( A rmX N ) ) )
62		rmxdbl	\|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX ( 2 x. N ) ) = ( ( 2 x. ( ( A rmX N ) ^ 2 ) ) - 1 ) )
63	29 30 62	syl2anc	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmX ( 2 x. N ) ) = ( ( 2 x. ( ( A rmX N ) ^ 2 ) ) - 1 ) )
64	63	oveq1d	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmX ( 2 x. N ) ) + 1 ) = ( ( ( 2 x. ( ( A rmX N ) ^ 2 ) ) - 1 ) + 1 ) )
65		2cnd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> 2 e. CC )
66	29 30 4	syl2anc	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmX N ) e. NN0 )
67	66	nn0cnd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmX N ) e. CC )
68	67	sqcld	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmX N ) ^ 2 ) e. CC )
69	65 68	mulcld	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( 2 x. ( ( A rmX N ) ^ 2 ) ) e. CC )
70		1cnd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> 1 e. CC )
71	69 70	npcand	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( ( 2 x. ( ( A rmX N ) ^ 2 ) ) - 1 ) + 1 ) = ( 2 x. ( ( A rmX N ) ^ 2 ) ) )
72	67	sqvald	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmX N ) ^ 2 ) = ( ( A rmX N ) x. ( A rmX N ) ) )
73	72	oveq2d	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( 2 x. ( ( A rmX N ) ^ 2 ) ) = ( 2 x. ( ( A rmX N ) x. ( A rmX N ) ) ) )
74		mulass	\|- ( ( 2 e. CC /\ ( A rmX N ) e. CC /\ ( A rmX N ) e. CC ) -> ( ( 2 x. ( A rmX N ) ) x. ( A rmX N ) ) = ( 2 x. ( ( A rmX N ) x. ( A rmX N ) ) ) )
75	74	eqcomd	\|- ( ( 2 e. CC /\ ( A rmX N ) e. CC /\ ( A rmX N ) e. CC ) -> ( 2 x. ( ( A rmX N ) x. ( A rmX N ) ) ) = ( ( 2 x. ( A rmX N ) ) x. ( A rmX N ) ) )
76	65 67 67 75	syl3anc	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( 2 x. ( ( A rmX N ) x. ( A rmX N ) ) ) = ( ( 2 x. ( A rmX N ) ) x. ( A rmX N ) ) )
77	73 76	eqtrd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( 2 x. ( ( A rmX N ) ^ 2 ) ) = ( ( 2 x. ( A rmX N ) ) x. ( A rmX N ) ) )
78	64 71 77	3eqtrd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmX ( 2 x. N ) ) + 1 ) = ( ( 2 x. ( A rmX N ) ) x. ( A rmX N ) ) )
79	61 78	breqtrrd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmX N ) \|\| ( ( A rmX ( 2 x. N ) ) + 1 ) )
80	49	peano2zd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmX ( 2 x. N ) ) + 1 ) e. ZZ )
81		dvdsmultr2	\|- ( ( ( A rmX N ) e. ZZ /\ ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) e. ZZ /\ ( ( A rmX ( 2 x. N ) ) + 1 ) e. ZZ ) -> ( ( A rmX N ) \|\| ( ( A rmX ( 2 x. N ) ) + 1 ) -> ( A rmX N ) \|\| ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( ( A rmX ( 2 x. N ) ) + 1 ) ) ) )
82	31 46 80 81	syl3anc	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmX N ) \|\| ( ( A rmX ( 2 x. N ) ) + 1 ) -> ( A rmX N ) \|\| ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( ( A rmX ( 2 x. N ) ) + 1 ) ) ) )
83	79 82	mpd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmX N ) \|\| ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( ( A rmX ( 2 x. N ) ) + 1 ) ) )
84	46	zcnd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) e. CC )
85	84	mulid1d	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. 1 ) = ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) )
86	85	oveq2d	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmX ( 2 x. N ) ) ) + ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. 1 ) ) = ( ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmX ( 2 x. N ) ) ) + ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) ) )
87	49	zcnd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmX ( 2 x. N ) ) e. CC )
88	84 87 70	adddid	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( ( A rmX ( 2 x. N ) ) + 1 ) ) = ( ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmX ( 2 x. N ) ) ) + ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. 1 ) ) )
89	50	zcnd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmX ( 2 x. N ) ) ) e. CC )
90	89 84	subnegd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmX ( 2 x. N ) ) ) - -u ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) ) = ( ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmX ( 2 x. N ) ) ) + ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) ) )
91	86 88 90	3eqtr4d	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( ( A rmX ( 2 x. N ) ) + 1 ) ) = ( ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmX ( 2 x. N ) ) ) - -u ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) ) )
92	83 91	breqtrd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmX N ) \|\| ( ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmX ( 2 x. N ) ) ) - -u ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) ) )
93	8	fovcl	\|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. ZZ )
94	29 30 93	syl2anc	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmY N ) e. ZZ )
95	37 94	zmulcld	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( 2 x. ( A rmY N ) ) e. ZZ )
96		dvdsmul2	\|- ( ( ( 2 x. ( A rmY N ) ) e. ZZ /\ ( A rmX N ) e. ZZ ) -> ( A rmX N ) \|\| ( ( 2 x. ( A rmY N ) ) x. ( A rmX N ) ) )
97	95 31 96	syl2anc	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmX N ) \|\| ( ( 2 x. ( A rmY N ) ) x. ( A rmX N ) ) )
98		rmydbl	\|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY ( 2 x. N ) ) = ( ( 2 x. ( A rmX N ) ) x. ( A rmY N ) ) )
99	29 30 98	syl2anc	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmY ( 2 x. N ) ) = ( ( 2 x. ( A rmX N ) ) x. ( A rmY N ) ) )
100	94	zcnd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmY N ) e. CC )
101	65 67 100	mul32d	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( 2 x. ( A rmX N ) ) x. ( A rmY N ) ) = ( ( 2 x. ( A rmY N ) ) x. ( A rmX N ) ) )
102	99 101	eqtrd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmY ( 2 x. N ) ) = ( ( 2 x. ( A rmY N ) ) x. ( A rmX N ) ) )
103	97 102	breqtrrd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmX N ) \|\| ( A rmY ( 2 x. N ) ) )
104		dvdsmultr2	\|- ( ( ( A rmX N ) e. ZZ /\ ( A rmX ( M + ( b x. ( 2 x. N ) ) ) ) e. ZZ /\ ( A rmY ( 2 x. N ) ) e. ZZ ) -> ( ( A rmX N ) \|\| ( A rmY ( 2 x. N ) ) -> ( A rmX N ) \|\| ( ( A rmX ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmY ( 2 x. N ) ) ) ) )
105	31 55 57 104	syl3anc	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmX N ) \|\| ( A rmY ( 2 x. N ) ) -> ( A rmX N ) \|\| ( ( A rmX ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmY ( 2 x. N ) ) ) ) )
106	103 105	mpd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmX N ) \|\| ( ( A rmX ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmY ( 2 x. N ) ) ) )
107	31 52 58 92 106	dvds2addd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmX N ) \|\| ( ( ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmX ( 2 x. N ) ) ) - -u ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) ) + ( ( A rmX ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmY ( 2 x. N ) ) ) ) )
108	34	zcnd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> b e. CC )
109	38	zcnd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( 2 x. N ) e. CC )
110	108 70 109	adddird	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( b + 1 ) x. ( 2 x. N ) ) = ( ( b x. ( 2 x. N ) ) + ( 1 x. ( 2 x. N ) ) ) )
111	110	oveq2d	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) = ( M + ( ( b x. ( 2 x. N ) ) + ( 1 x. ( 2 x. N ) ) ) ) )
112	32	zcnd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> M e. CC )
113	43	zcnd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( b x. ( 2 x. N ) ) e. CC )
114		1zzd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> 1 e. ZZ )
115	114 38	zmulcld	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( 1 x. ( 2 x. N ) ) e. ZZ )
116	115	zcnd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( 1 x. ( 2 x. N ) ) e. CC )
117	112 113 116	addassd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( M + ( b x. ( 2 x. N ) ) ) + ( 1 x. ( 2 x. N ) ) ) = ( M + ( ( b x. ( 2 x. N ) ) + ( 1 x. ( 2 x. N ) ) ) ) )
118	109	mulid2d	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( 1 x. ( 2 x. N ) ) = ( 2 x. N ) )
119	118	oveq2d	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( M + ( b x. ( 2 x. N ) ) ) + ( 1 x. ( 2 x. N ) ) ) = ( ( M + ( b x. ( 2 x. N ) ) ) + ( 2 x. N ) ) )
120	111 117 119	3eqtr2d	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) = ( ( M + ( b x. ( 2 x. N ) ) ) + ( 2 x. N ) ) )
121	120	oveq2d	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) = ( A rmY ( ( M + ( b x. ( 2 x. N ) ) ) + ( 2 x. N ) ) ) )
122		rmyadd	\|- ( ( A e. ( ZZ>= ` 2 ) /\ ( M + ( b x. ( 2 x. N ) ) ) e. ZZ /\ ( 2 x. N ) e. ZZ ) -> ( A rmY ( ( M + ( b x. ( 2 x. N ) ) ) + ( 2 x. N ) ) ) = ( ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmX ( 2 x. N ) ) ) + ( ( A rmX ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmY ( 2 x. N ) ) ) ) )
123	29 44 38 122	syl3anc	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmY ( ( M + ( b x. ( 2 x. N ) ) ) + ( 2 x. N ) ) ) = ( ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmX ( 2 x. N ) ) ) + ( ( A rmX ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmY ( 2 x. N ) ) ) ) )
124	121 123	eqtrd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) = ( ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmX ( 2 x. N ) ) ) + ( ( A rmX ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmY ( 2 x. N ) ) ) ) )
125	124	oveq1d	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) - -u ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) ) = ( ( ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmX ( 2 x. N ) ) ) + ( ( A rmX ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmY ( 2 x. N ) ) ) ) - -u ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) ) )
126	58	zcnd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmX ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmY ( 2 x. N ) ) ) e. CC )
127	51	zcnd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> -u ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) e. CC )
128	89 126 127	addsubd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmX ( 2 x. N ) ) ) + ( ( A rmX ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmY ( 2 x. N ) ) ) ) - -u ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) ) = ( ( ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmX ( 2 x. N ) ) ) - -u ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) ) + ( ( A rmX ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmY ( 2 x. N ) ) ) ) )
129	125 128	eqtrd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) - -u ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) ) = ( ( ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmX ( 2 x. N ) ) ) - -u ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) ) + ( ( A rmX ( M + ( b x. ( 2 x. N ) ) ) ) x. ( A rmY ( 2 x. N ) ) ) ) )
130	107 129	breqtrrd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( A rmX N ) \|\| ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) - -u ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) ) )
131	130	olcd	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) - ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) - -u ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) ) ) )
132		jm2.25lem1	\|- ( ( ( ( A rmX N ) e. ZZ /\ ( A rmY M ) e. ZZ ) /\ ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) e. ZZ /\ ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) e. ZZ ) /\ ( ( A rmX N ) \|\| ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) - ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) - -u ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) ) ) ) -> ( ( ( A rmX N ) \|\| ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) <-> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) ) )
133	31 33 42 46 131 132	syl221anc	\|- ( ( b e. ZZ /\ ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( ( A rmX N ) \|\| ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) <-> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) ) )
134	133	pm5.74da	\|- ( b e. ZZ -> ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) ) <-> ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) ) ) )
135		oveq1	\|- ( a = b -> ( a x. ( 2 x. N ) ) = ( b x. ( 2 x. N ) ) )
136	135	oveq2d	\|- ( a = b -> ( M + ( a x. ( 2 x. N ) ) ) = ( M + ( b x. ( 2 x. N ) ) ) )
137	136	oveq2d	\|- ( a = b -> ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) = ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) )
138	137	oveq1d	\|- ( a = b -> ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) = ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) )
139	138	breq2d	\|- ( a = b -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) <-> ( A rmX N ) \|\| ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) ) )
140	137	oveq1d	\|- ( a = b -> ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) = ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) )
141	140	breq2d	\|- ( a = b -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) <-> ( A rmX N ) \|\| ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) )
142	139 141	orbi12d	\|- ( a = b -> ( ( ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) <-> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) ) )
143	142	imbi2d	\|- ( a = b -> ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) ) <-> ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( b x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) ) ) )
144		oveq1	\|- ( a = ( b + 1 ) -> ( a x. ( 2 x. N ) ) = ( ( b + 1 ) x. ( 2 x. N ) ) )
145	144	oveq2d	\|- ( a = ( b + 1 ) -> ( M + ( a x. ( 2 x. N ) ) ) = ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) )
146	145	oveq2d	\|- ( a = ( b + 1 ) -> ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) = ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) )
147	146	oveq1d	\|- ( a = ( b + 1 ) -> ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) = ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) )
148	147	breq2d	\|- ( a = ( b + 1 ) -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) <-> ( A rmX N ) \|\| ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) ) )
149	146	oveq1d	\|- ( a = ( b + 1 ) -> ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) = ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) )
150	149	breq2d	\|- ( a = ( b + 1 ) -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) <-> ( A rmX N ) \|\| ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) )
151	148 150	orbi12d	\|- ( a = ( b + 1 ) -> ( ( ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) <-> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) ) )
152	151	imbi2d	\|- ( a = ( b + 1 ) -> ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) ) <-> ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( ( b + 1 ) x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) ) ) )
153		oveq1	\|- ( a = 0 -> ( a x. ( 2 x. N ) ) = ( 0 x. ( 2 x. N ) ) )
154	153	oveq2d	\|- ( a = 0 -> ( M + ( a x. ( 2 x. N ) ) ) = ( M + ( 0 x. ( 2 x. N ) ) ) )
155	154	oveq2d	\|- ( a = 0 -> ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) = ( A rmY ( M + ( 0 x. ( 2 x. N ) ) ) ) )
156	155	oveq1d	\|- ( a = 0 -> ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) = ( ( A rmY ( M + ( 0 x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) )
157	156	breq2d	\|- ( a = 0 -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) <-> ( A rmX N ) \|\| ( ( A rmY ( M + ( 0 x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) ) )
158	155	oveq1d	\|- ( a = 0 -> ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) = ( ( A rmY ( M + ( 0 x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) )
159	158	breq2d	\|- ( a = 0 -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) <-> ( A rmX N ) \|\| ( ( A rmY ( M + ( 0 x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) )
160	157 159	orbi12d	\|- ( a = 0 -> ( ( ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) <-> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( 0 x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( 0 x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) ) )
161	160	imbi2d	\|- ( a = 0 -> ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) ) <-> ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( 0 x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( 0 x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) ) ) )
162		oveq1	\|- ( a = I -> ( a x. ( 2 x. N ) ) = ( I x. ( 2 x. N ) ) )
163	162	oveq2d	\|- ( a = I -> ( M + ( a x. ( 2 x. N ) ) ) = ( M + ( I x. ( 2 x. N ) ) ) )
164	163	oveq2d	\|- ( a = I -> ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) = ( A rmY ( M + ( I x. ( 2 x. N ) ) ) ) )
165	164	oveq1d	\|- ( a = I -> ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) = ( ( A rmY ( M + ( I x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) )
166	165	breq2d	\|- ( a = I -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) <-> ( A rmX N ) \|\| ( ( A rmY ( M + ( I x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) ) )
167	164	oveq1d	\|- ( a = I -> ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) = ( ( A rmY ( M + ( I x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) )
168	167	breq2d	\|- ( a = I -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) <-> ( A rmX N ) \|\| ( ( A rmY ( M + ( I x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) )
169	166 168	orbi12d	\|- ( a = I -> ( ( ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) <-> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( I x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( I x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) ) )
170	169	imbi2d	\|- ( a = I -> ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) ) <-> ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( I x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( I x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) ) ) )
171	134 143 152 161 170	zindbi	\|- ( I e. ZZ -> ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( 0 x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( 0 x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) ) <-> ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( I x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( I x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) ) ) )
172	28 171	mpbid	\|- ( I e. ZZ -> ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( I x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( I x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) ) )
173	172	impcom	\|- ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. ZZ ) -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( I x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( I x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) )
174	173	3impa	\|- ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) /\ I e. ZZ ) -> ( ( A rmX N ) \|\| ( ( A rmY ( M + ( I x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) \|\| ( ( A rmY ( M + ( I x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) )

Metamath Proof Explorer

Theorem jm2.25

Proof