Theorem jm2.27a

Description: Lemma for jm2.27 . Reverse direction after existential quantifiers are expanded. (Contributed by Stefan O'Rear, 4-Oct-2014)

	Ref	Expression
Hypotheses	jm2.27a1	$$⊢\phi \to A\in {\mathbb{Z}}_{\ge 2}$$
	jm2.27a2	$$⊢\phi \to B\in \mathbb{N}$$
	jm2.27a3	$$⊢\phi \to C\in \mathbb{N}$$
	jm2.27a4	$$⊢\phi \to D\in {\mathbb{N}}_0$$
	jm2.27a5	$$⊢\phi \to E\in {\mathbb{N}}_0$$
	jm2.27a6	$$⊢\phi \to F\in {\mathbb{N}}_0$$
	jm2.27a7	$$⊢\phi \to G\in {\mathbb{N}}_0$$
	jm2.27a8	$$⊢\phi \to H\in {\mathbb{N}}_0$$
	jm2.27a9	$$⊢\phi \to I\in {\mathbb{N}}_0$$
	jm2.27a10	$$⊢\phi \to J\in {\mathbb{N}}_0$$
	jm2.27a11	$$⊢\phi \to D^2-\left(A^2-1\right)C^2=1$$
	jm2.27a12	$$⊢\phi \to F^2-\left(A^2-1\right)E^2=1$$
	jm2.27a13	$$⊢\phi \to G\in {\mathbb{Z}}_{\ge 2}$$
	jm2.27a14	$$⊢\phi \to I^2-\left(G^2-1\right)H^2=1$$
	jm2.27a15	$$⊢\phi \to E=\left(J+1\right)2C^2$$
	jm2.27a16	$$⊢\phi \to F\parallel \left(G-A\right)$$
	jm2.27a17	$$⊢\phi \to 2C\parallel \left(G-1\right)$$
	jm2.27a18	$$⊢\phi \to F\parallel \left(H-C\right)$$
	jm2.27a19	$$⊢\phi \to 2C\parallel \left(H-B\right)$$
	jm2.27a20	$$⊢\phi \to B\le C$$
	jm2.27a21	$$⊢\phi \to P\in \mathbb{Z}$$
	jm2.27a22	$$⊢\phi \to D=A{X}_{\mathrm{rm}}P$$
	jm2.27a23	$$⊢\phi \to C=A{Y}_{\mathrm{rm}}P$$
	jm2.27a24	$$⊢\phi \to Q\in \mathbb{Z}$$
	jm2.27a25	$$⊢\phi \to F=A{X}_{\mathrm{rm}}Q$$
	jm2.27a26	$$⊢\phi \to E=A{Y}_{\mathrm{rm}}Q$$
	jm2.27a27	$$⊢\phi \to R\in \mathbb{Z}$$
	jm2.27a28	$$⊢\phi \to I=G{X}_{\mathrm{rm}}R$$
	jm2.27a29	$$⊢\phi \to H=G{Y}_{\mathrm{rm}}R$$
Assertion	jm2.27a	$$⊢\phi \to C=A{Y}_{\mathrm{rm}}B$$

Proof

Step	Hyp	Ref	Expression
1		jm2.27a1	$$⊢\phi \to A\in {\mathbb{Z}}_{\ge 2}$$
2		jm2.27a2	$$⊢\phi \to B\in \mathbb{N}$$
3		jm2.27a3	$$⊢\phi \to C\in \mathbb{N}$$
4		jm2.27a4	$$⊢\phi \to D\in {\mathbb{N}}_0$$
5		jm2.27a5	$$⊢\phi \to E\in {\mathbb{N}}_0$$
6		jm2.27a6	$$⊢\phi \to F\in {\mathbb{N}}_0$$
7		jm2.27a7	$$⊢\phi \to G\in {\mathbb{N}}_0$$
8		jm2.27a8	$$⊢\phi \to H\in {\mathbb{N}}_0$$
9		jm2.27a9	$$⊢\phi \to I\in {\mathbb{N}}_0$$
10		jm2.27a10	$$⊢\phi \to J\in {\mathbb{N}}_0$$
11		jm2.27a11	$$⊢\phi \to D^2-\left(A^2-1\right)C^2=1$$
12		jm2.27a12	$$⊢\phi \to F^2-\left(A^2-1\right)E^2=1$$
13		jm2.27a13	$$⊢\phi \to G\in {\mathbb{Z}}_{\ge 2}$$
14		jm2.27a14	$$⊢\phi \to I^2-\left(G^2-1\right)H^2=1$$
15		jm2.27a15	$$⊢\phi \to E=\left(J+1\right)2C^2$$
16		jm2.27a16	$$⊢\phi \to F\parallel \left(G-A\right)$$
17		jm2.27a17	$$⊢\phi \to 2C\parallel \left(G-1\right)$$
18		jm2.27a18	$$⊢\phi \to F\parallel \left(H-C\right)$$
19		jm2.27a19	$$⊢\phi \to 2C\parallel \left(H-B\right)$$
20		jm2.27a20	$$⊢\phi \to B\le C$$
21		jm2.27a21	$$⊢\phi \to P\in \mathbb{Z}$$
22		jm2.27a22	$$⊢\phi \to D=A{X}_{\mathrm{rm}}P$$
23		jm2.27a23	$$⊢\phi \to C=A{Y}_{\mathrm{rm}}P$$
24		jm2.27a24	$$⊢\phi \to Q\in \mathbb{Z}$$
25		jm2.27a25	$$⊢\phi \to F=A{X}_{\mathrm{rm}}Q$$
26		jm2.27a26	$$⊢\phi \to E=A{Y}_{\mathrm{rm}}Q$$
27		jm2.27a27	$$⊢\phi \to R\in \mathbb{Z}$$
28		jm2.27a28	$$⊢\phi \to I=G{X}_{\mathrm{rm}}R$$
29		jm2.27a29	$$⊢\phi \to H=G{Y}_{\mathrm{rm}}R$$
30		2z	$$⊢2\in \mathbb{Z}$$
31	3	nnzd	$$⊢\phi \to C\in \mathbb{Z}$$
32		zmulcl	$$⊢\left(2\in \mathbb{Z}\wedge C\in \mathbb{Z}\right)\to 2C\in \mathbb{Z}$$
33	30 31 32	sylancr	$$⊢\phi \to 2C\in \mathbb{Z}$$
34	2	nnzd	$$⊢\phi \to B\in \mathbb{Z}$$
35	8	nn0zd	$$⊢\phi \to H\in \mathbb{Z}$$
36		congsym	$$⊢\left(\left(2C\in \mathbb{Z}\wedge H\in \mathbb{Z}\right)\wedge \left(B\in \mathbb{Z}\wedge 2C\parallel \left(H-B\right)\right)\right)\to 2C\parallel \left(B-H\right)$$
37	33 35 34 19 36	syl22anc	$$⊢\phi \to 2C\parallel \left(B-H\right)$$
38	7	nn0zd	$$⊢\phi \to G\in \mathbb{Z}$$
39		peano2zm	$$⊢G\in \mathbb{Z}\to G-1\in \mathbb{Z}$$
40	38 39	syl	$$⊢\phi \to G-1\in \mathbb{Z}$$
41	35 27	zsubcld	$$⊢\phi \to H-R\in \mathbb{Z}$$
42	8	nn0ge0d	$$⊢\phi \to 0\le H$$
43		rmy0	$$⊢G\in {\mathbb{Z}}_{\ge 2}\to G{Y}_{\mathrm{rm}}0=0$$
44	13 43	syl	$$⊢\phi \to G{Y}_{\mathrm{rm}}0=0$$
45	29	eqcomd	$$⊢\phi \to G{Y}_{\mathrm{rm}}R=H$$
46	42 44 45	3brtr4d	$$⊢\phi \to G{Y}_{\mathrm{rm}}0\le G{Y}_{\mathrm{rm}}R$$
47		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
48		lermy	$$⊢\left(G\in {\mathbb{Z}}_{\ge 2}\wedge 0\in \mathbb{Z}\wedge R\in \mathbb{Z}\right)\to \left(0\le R\leftrightarrow G{Y}_{\mathrm{rm}}0\le G{Y}_{\mathrm{rm}}R\right)$$
49	13 47 27 48	syl3anc	$$⊢\phi \to \left(0\le R\leftrightarrow G{Y}_{\mathrm{rm}}0\le G{Y}_{\mathrm{rm}}R\right)$$
50	46 49	mpbird	$$⊢\phi \to 0\le R$$
51		elnn0z	$$⊢R\in {\mathbb{N}}_0\leftrightarrow \left(R\in \mathbb{Z}\wedge 0\le R\right)$$
52	27 50 51	sylanbrc	$$⊢\phi \to R\in {\mathbb{N}}_0$$
53		jm2.16nn0	$$⊢\left(G\in {\mathbb{Z}}_{\ge 2}\wedge R\in {\mathbb{N}}_0\right)\to \left(G-1\right)\parallel \left(\left(G{Y}_{\mathrm{rm}}R\right)-R\right)$$
54	13 52 53	syl2anc	$$⊢\phi \to \left(G-1\right)\parallel \left(\left(G{Y}_{\mathrm{rm}}R\right)-R\right)$$
55	29	oveq1d	$$⊢\phi \to H-R=\left(G{Y}_{\mathrm{rm}}R\right)-R$$
56	54 55	breqtrrd	$$⊢\phi \to \left(G-1\right)\parallel \left(H-R\right)$$
57	33 40 41 17 56	dvdstrd	$$⊢\phi \to 2C\parallel \left(H-R\right)$$
58		congtr	$$⊢\left(\left(2C\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\wedge \left(H\in \mathbb{Z}\wedge R\in \mathbb{Z}\right)\wedge \left(2C\parallel \left(B-H\right)\wedge 2C\parallel \left(H-R\right)\right)\right)\to 2C\parallel \left(B-R\right)$$
59	33 34 35 27 37 57 58	syl222anc	$$⊢\phi \to 2C\parallel \left(B-R\right)$$
60	59	orcd	$$⊢\phi \to \left(2C\parallel \left(B-R\right)\vee 2C\parallel \left(B-\left(-R\right)\right)\right)$$
61		zmulcl	$$⊢\left(2\in \mathbb{Z}\wedge Q\in \mathbb{Z}\right)\to 2Q\in \mathbb{Z}$$
62	30 24 61	sylancr	$$⊢\phi \to 2Q\in \mathbb{Z}$$
63		zsqcl	$$⊢C\in \mathbb{Z}\to C^2\in \mathbb{Z}$$
64	31 63	syl	$$⊢\phi \to C^2\in \mathbb{Z}$$
65		dvdsmul2	$$⊢\left(2\in \mathbb{Z}\wedge C^2\in \mathbb{Z}\right)\to C^2\parallel 2C^2$$
66	30 64 65	sylancr	$$⊢\phi \to C^2\parallel 2C^2$$
67	10	nn0zd	$$⊢\phi \to J\in \mathbb{Z}$$
68	67	peano2zd	$$⊢\phi \to J+1\in \mathbb{Z}$$
69		zmulcl	$$⊢\left(2\in \mathbb{Z}\wedge C^2\in \mathbb{Z}\right)\to 2C^2\in \mathbb{Z}$$
70	30 64 69	sylancr	$$⊢\phi \to 2C^2\in \mathbb{Z}$$
71		dvdsmultr2	$$⊢\left(C^2\in \mathbb{Z}\wedge J+1\in \mathbb{Z}\wedge 2C^2\in \mathbb{Z}\right)\to \left(C^2\parallel 2C^2\to C^2\parallel \left(J+1\right)2C^2\right)$$
72	64 68 70 71	syl3anc	$$⊢\phi \to \left(C^2\parallel 2C^2\to C^2\parallel \left(J+1\right)2C^2\right)$$
73	66 72	mpd	$$⊢\phi \to C^2\parallel \left(J+1\right)2C^2$$
74	23	oveq1d	$$⊢\phi \to C^2={\left(A{Y}_{\mathrm{rm}}P\right)}^2$$
75	15 26	eqtr3d	$$⊢\phi \to \left(J+1\right)2C^2=A{Y}_{\mathrm{rm}}Q$$
76	73 74 75	3brtr3d	$$⊢\phi \to {\left(A{Y}_{\mathrm{rm}}P\right)}^2\parallel \left(A{Y}_{\mathrm{rm}}Q\right)$$
77	68	zred	$$⊢\phi \to J+1\in ℝ$$
78	70	zred	$$⊢\phi \to 2C^2\in ℝ$$
79		nn0p1nn	$$⊢J\in {\mathbb{N}}_0\to J+1\in \mathbb{N}$$
80	10 79	syl	$$⊢\phi \to J+1\in \mathbb{N}$$
81	80	nngt0d	$$⊢\phi \to 0<J+1$$
82		2nn	$$⊢2\in \mathbb{N}$$
83	3	nnsqcld	$$⊢\phi \to C^2\in \mathbb{N}$$
84		nnmulcl	$$⊢\left(2\in \mathbb{N}\wedge C^2\in \mathbb{N}\right)\to 2C^2\in \mathbb{N}$$
85	82 83 84	sylancr	$$⊢\phi \to 2C^2\in \mathbb{N}$$
86	85	nngt0d	$$⊢\phi \to 0<2C^2$$
87	77 78 81 86	mulgt0d	$$⊢\phi \to 0<\left(J+1\right)2C^2$$
88	87 15	breqtrrd	$$⊢\phi \to 0<E$$
89		rmy0	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A{Y}_{\mathrm{rm}}0=0$$
90	1 89	syl	$$⊢\phi \to A{Y}_{\mathrm{rm}}0=0$$
91	26	eqcomd	$$⊢\phi \to A{Y}_{\mathrm{rm}}Q=E$$
92	88 90 91	3brtr4d	$$⊢\phi \to A{Y}_{\mathrm{rm}}0<A{Y}_{\mathrm{rm}}Q$$
93		ltrmy	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge 0\in \mathbb{Z}\wedge Q\in \mathbb{Z}\right)\to \left(0<Q\leftrightarrow A{Y}_{\mathrm{rm}}0<A{Y}_{\mathrm{rm}}Q\right)$$
94	1 47 24 93	syl3anc	$$⊢\phi \to \left(0<Q\leftrightarrow A{Y}_{\mathrm{rm}}0<A{Y}_{\mathrm{rm}}Q\right)$$
95	92 94	mpbird	$$⊢\phi \to 0<Q$$
96		elnnz	$$⊢Q\in \mathbb{N}\leftrightarrow \left(Q\in \mathbb{Z}\wedge 0<Q\right)$$
97	24 95 96	sylanbrc	$$⊢\phi \to Q\in \mathbb{N}$$
98	3	nngt0d	$$⊢\phi \to 0<C$$
99	23	eqcomd	$$⊢\phi \to A{Y}_{\mathrm{rm}}P=C$$
100	98 90 99	3brtr4d	$$⊢\phi \to A{Y}_{\mathrm{rm}}0<A{Y}_{\mathrm{rm}}P$$
101		ltrmy	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge 0\in \mathbb{Z}\wedge P\in \mathbb{Z}\right)\to \left(0<P\leftrightarrow A{Y}_{\mathrm{rm}}0<A{Y}_{\mathrm{rm}}P\right)$$
102	1 47 21 101	syl3anc	$$⊢\phi \to \left(0<P\leftrightarrow A{Y}_{\mathrm{rm}}0<A{Y}_{\mathrm{rm}}P\right)$$
103	100 102	mpbird	$$⊢\phi \to 0<P$$
104		elnnz	$$⊢P\in \mathbb{N}\leftrightarrow \left(P\in \mathbb{Z}\wedge 0<P\right)$$
105	21 103 104	sylanbrc	$$⊢\phi \to P\in \mathbb{N}$$
106		jm2.20nn	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge Q\in \mathbb{N}\wedge P\in \mathbb{N}\right)\to \left({\left(A{Y}_{\mathrm{rm}}P\right)}^2\parallel \left(A{Y}_{\mathrm{rm}}Q\right)\leftrightarrow P\left(A{Y}_{\mathrm{rm}}P\right)\parallel Q\right)$$
107	1 97 105 106	syl3anc	$$⊢\phi \to \left({\left(A{Y}_{\mathrm{rm}}P\right)}^2\parallel \left(A{Y}_{\mathrm{rm}}Q\right)\leftrightarrow P\left(A{Y}_{\mathrm{rm}}P\right)\parallel Q\right)$$
108	76 107	mpbid	$$⊢\phi \to P\left(A{Y}_{\mathrm{rm}}P\right)\parallel Q$$
109	23 31	eqeltrrd	$$⊢\phi \to A{Y}_{\mathrm{rm}}P\in \mathbb{Z}$$
110		muldvds2	$$⊢\left(P\in \mathbb{Z}\wedge A{Y}_{\mathrm{rm}}P\in \mathbb{Z}\wedge Q\in \mathbb{Z}\right)\to \left(P\left(A{Y}_{\mathrm{rm}}P\right)\parallel Q\to \left(A{Y}_{\mathrm{rm}}P\right)\parallel Q\right)$$
111	21 109 24 110	syl3anc	$$⊢\phi \to \left(P\left(A{Y}_{\mathrm{rm}}P\right)\parallel Q\to \left(A{Y}_{\mathrm{rm}}P\right)\parallel Q\right)$$
112	108 111	mpd	$$⊢\phi \to \left(A{Y}_{\mathrm{rm}}P\right)\parallel Q$$
113	23 112	eqbrtrd	$$⊢\phi \to C\parallel Q$$
114	30	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
115		dvdscmul	$$⊢\left(C\in \mathbb{Z}\wedge Q\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\to \left(C\parallel Q\to 2C\parallel 2Q\right)$$
116	31 24 114 115	syl3anc	$$⊢\phi \to \left(C\parallel Q\to 2C\parallel 2Q\right)$$
117	113 116	mpd	$$⊢\phi \to 2C\parallel 2Q$$
118	6	nn0zd	$$⊢\phi \to F\in \mathbb{Z}$$
119	25 118	eqeltrrd	$$⊢\phi \to A{X}_{\mathrm{rm}}Q\in \mathbb{Z}$$
120		frmy	$$⊢Y_{\mathrm{rm}}:{\mathbb{Z}}_{\ge 2}\times \mathbb{Z}⟶\mathbb{Z}$$
121	120	fovcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge R\in \mathbb{Z}\right)\to A{Y}_{\mathrm{rm}}R\in \mathbb{Z}$$
122	1 27 121	syl2anc	$$⊢\phi \to A{Y}_{\mathrm{rm}}R\in \mathbb{Z}$$
123	29 35	eqeltrrd	$$⊢\phi \to G{Y}_{\mathrm{rm}}R\in \mathbb{Z}$$
124		eluzelz	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in \mathbb{Z}$$
125	1 124	syl	$$⊢\phi \to A\in \mathbb{Z}$$
126	125 38	zsubcld	$$⊢\phi \to A-G\in \mathbb{Z}$$
127	122 123	zsubcld	$$⊢\phi \to \left(A{Y}_{\mathrm{rm}}R\right)-\left(G{Y}_{\mathrm{rm}}R\right)\in \mathbb{Z}$$
128		congsym	$$⊢\left(\left(F\in \mathbb{Z}\wedge G\in \mathbb{Z}\right)\wedge \left(A\in \mathbb{Z}\wedge F\parallel \left(G-A\right)\right)\right)\to F\parallel \left(A-G\right)$$
129	118 38 125 16 128	syl22anc	$$⊢\phi \to F\parallel \left(A-G\right)$$
130	25 129	eqbrtrrd	$$⊢\phi \to \left(A{X}_{\mathrm{rm}}Q\right)\parallel \left(A-G\right)$$
131		jm2.15nn0	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge G\in {\mathbb{Z}}_{\ge 2}\wedge R\in {\mathbb{N}}_0\right)\to \left(A-G\right)\parallel \left(\left(A{Y}_{\mathrm{rm}}R\right)-\left(G{Y}_{\mathrm{rm}}R\right)\right)$$
132	1 13 52 131	syl3anc	$$⊢\phi \to \left(A-G\right)\parallel \left(\left(A{Y}_{\mathrm{rm}}R\right)-\left(G{Y}_{\mathrm{rm}}R\right)\right)$$
133	119 126 127 130 132	dvdstrd	$$⊢\phi \to \left(A{X}_{\mathrm{rm}}Q\right)\parallel \left(\left(A{Y}_{\mathrm{rm}}R\right)-\left(G{Y}_{\mathrm{rm}}R\right)\right)$$
134	29 23	oveq12d	$$⊢\phi \to H-C=\left(G{Y}_{\mathrm{rm}}R\right)-\left(A{Y}_{\mathrm{rm}}P\right)$$
135	18 25 134	3brtr3d	$$⊢\phi \to \left(A{X}_{\mathrm{rm}}Q\right)\parallel \left(\left(G{Y}_{\mathrm{rm}}R\right)-\left(A{Y}_{\mathrm{rm}}P\right)\right)$$
136		congtr	$$⊢\left(\left(A{X}_{\mathrm{rm}}Q\in \mathbb{Z}\wedge A{Y}_{\mathrm{rm}}R\in \mathbb{Z}\right)\wedge \left(G{Y}_{\mathrm{rm}}R\in \mathbb{Z}\wedge A{Y}_{\mathrm{rm}}P\in \mathbb{Z}\right)\wedge \left(\left(A{X}_{\mathrm{rm}}Q\right)\parallel \left(\left(A{Y}_{\mathrm{rm}}R\right)-\left(G{Y}_{\mathrm{rm}}R\right)\right)\wedge \left(A{X}_{\mathrm{rm}}Q\right)\parallel \left(\left(G{Y}_{\mathrm{rm}}R\right)-\left(A{Y}_{\mathrm{rm}}P\right)\right)\right)\right)\to \left(A{X}_{\mathrm{rm}}Q\right)\parallel \left(\left(A{Y}_{\mathrm{rm}}R\right)-\left(A{Y}_{\mathrm{rm}}P\right)\right)$$
137	119 122 123 109 133 135 136	syl222anc	$$⊢\phi \to \left(A{X}_{\mathrm{rm}}Q\right)\parallel \left(\left(A{Y}_{\mathrm{rm}}R\right)-\left(A{Y}_{\mathrm{rm}}P\right)\right)$$
138	137	orcd	$$⊢\phi \to \left(\left(A{X}_{\mathrm{rm}}Q\right)\parallel \left(\left(A{Y}_{\mathrm{rm}}R\right)-\left(A{Y}_{\mathrm{rm}}P\right)\right)\vee \left(A{X}_{\mathrm{rm}}Q\right)\parallel \left(\left(A{Y}_{\mathrm{rm}}R\right)-\left(-\left(A{Y}_{\mathrm{rm}}P\right)\right)\right)\right)$$
139		jm2.26	$$⊢\left(\left(A\in {\mathbb{Z}}_{\ge 2}\wedge Q\in \mathbb{N}\right)\wedge \left(R\in \mathbb{Z}\wedge P\in \mathbb{Z}\right)\right)\to \left(\left(\left(A{X}_{\mathrm{rm}}Q\right)\parallel \left(\left(A{Y}_{\mathrm{rm}}R\right)-\left(A{Y}_{\mathrm{rm}}P\right)\right)\vee \left(A{X}_{\mathrm{rm}}Q\right)\parallel \left(\left(A{Y}_{\mathrm{rm}}R\right)-\left(-\left(A{Y}_{\mathrm{rm}}P\right)\right)\right)\right)\leftrightarrow \left(2Q\parallel \left(R-P\right)\vee 2Q\parallel \left(R-\left(-P\right)\right)\right)\right)$$
140	1 97 27 21 139	syl22anc	$$⊢\phi \to \left(\left(\left(A{X}_{\mathrm{rm}}Q\right)\parallel \left(\left(A{Y}_{\mathrm{rm}}R\right)-\left(A{Y}_{\mathrm{rm}}P\right)\right)\vee \left(A{X}_{\mathrm{rm}}Q\right)\parallel \left(\left(A{Y}_{\mathrm{rm}}R\right)-\left(-\left(A{Y}_{\mathrm{rm}}P\right)\right)\right)\right)\leftrightarrow \left(2Q\parallel \left(R-P\right)\vee 2Q\parallel \left(R-\left(-P\right)\right)\right)\right)$$
141	138 140	mpbid	$$⊢\phi \to \left(2Q\parallel \left(R-P\right)\vee 2Q\parallel \left(R-\left(-P\right)\right)\right)$$
142		dvdsacongtr	$$⊢\left(\left(2Q\in \mathbb{Z}\wedge R\in \mathbb{Z}\right)\wedge \left(P\in \mathbb{Z}\wedge 2C\in \mathbb{Z}\right)\wedge \left(2C\parallel 2Q\wedge \left(2Q\parallel \left(R-P\right)\vee 2Q\parallel \left(R-\left(-P\right)\right)\right)\right)\right)\to \left(2C\parallel \left(R-P\right)\vee 2C\parallel \left(R-\left(-P\right)\right)\right)$$
143	62 27 21 33 117 141 142	syl222anc	$$⊢\phi \to \left(2C\parallel \left(R-P\right)\vee 2C\parallel \left(R-\left(-P\right)\right)\right)$$
144		acongtr	$$⊢\left(\left(2C\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\wedge \left(R\in \mathbb{Z}\wedge P\in \mathbb{Z}\right)\wedge \left(\left(2C\parallel \left(B-R\right)\vee 2C\parallel \left(B-\left(-R\right)\right)\right)\wedge \left(2C\parallel \left(R-P\right)\vee 2C\parallel \left(R-\left(-P\right)\right)\right)\right)\right)\to \left(2C\parallel \left(B-P\right)\vee 2C\parallel \left(B-\left(-P\right)\right)\right)$$
145	33 34 27 21 60 143 144	syl222anc	$$⊢\phi \to \left(2C\parallel \left(B-P\right)\vee 2C\parallel \left(B-\left(-P\right)\right)\right)$$
146	2	nnnn0d	$$⊢\phi \to B\in {\mathbb{N}}_0$$
147	3	nnnn0d	$$⊢\phi \to C\in {\mathbb{N}}_0$$
148		elfz2nn0	$$⊢B\in \left(0\dots C\right)\leftrightarrow \left(B\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\wedge B\le C\right)$$
149	146 147 20 148	syl3anbrc	$$⊢\phi \to B\in \left(0\dots C\right)$$
150	105	nnnn0d	$$⊢\phi \to P\in {\mathbb{N}}_0$$
151		rmygeid	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge P\in {\mathbb{N}}_0\right)\to P\le A{Y}_{\mathrm{rm}}P$$
152	1 150 151	syl2anc	$$⊢\phi \to P\le A{Y}_{\mathrm{rm}}P$$
153	152 23	breqtrrd	$$⊢\phi \to P\le C$$
154		elfz2nn0	$$⊢P\in \left(0\dots C\right)\leftrightarrow \left(P\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\wedge P\le C\right)$$
155	150 147 153 154	syl3anbrc	$$⊢\phi \to P\in \left(0\dots C\right)$$
156		acongeq	$$⊢\left(C\in \mathbb{N}\wedge B\in \left(0\dots C\right)\wedge P\in \left(0\dots C\right)\right)\to \left(B=P\leftrightarrow \left(2C\parallel \left(B-P\right)\vee 2C\parallel \left(B-\left(-P\right)\right)\right)\right)$$
157	3 149 155 156	syl3anc	$$⊢\phi \to \left(B=P\leftrightarrow \left(2C\parallel \left(B-P\right)\vee 2C\parallel \left(B-\left(-P\right)\right)\right)\right)$$
158	145 157	mpbird	$$⊢\phi \to B=P$$
159	158	oveq2d	$$⊢\phi \to A{Y}_{\mathrm{rm}}B=A{Y}_{\mathrm{rm}}P$$
160	23 159	eqtr4d	$$⊢\phi \to C=A{Y}_{\mathrm{rm}}B$$