Theorem jm2.27c

Description: Lemma for jm2.27 . Forward direction with substitutions. (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.27c4	$$⊢\phi \to C=A{Y}_{\mathrm{rm}}B$$
	jm2.27c5	$$⊢D=A{X}_{\mathrm{rm}}B$$
	jm2.27c6	$$⊢Q=B\left(A{Y}_{\mathrm{rm}}B\right)$$
	jm2.27c7	$$⊢E=A{Y}_{\mathrm{rm}}2Q$$
	jm2.27c8	$$⊢F=A{X}_{\mathrm{rm}}2Q$$
	jm2.27c9	$$⊢G=A+F^2\left(F^2-A\right)$$
	jm2.27c10	$$⊢H=G{Y}_{\mathrm{rm}}B$$
	jm2.27c11	$$⊢I=G{X}_{\mathrm{rm}}B$$
	jm2.27c12	$$⊢J=\left(\frac{E}{2C^2}\right)-1$$
Assertion	jm2.27c	$$⊢\phi \to \left(\left(\left(D\in {\mathbb{N}}_0\wedge E\in {\mathbb{N}}_0\wedge F\in {\mathbb{N}}_0\right)\wedge \left(G\in {\mathbb{N}}_0\wedge H\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\right)\wedge \left(J\in {\mathbb{N}}_0\wedge \left(\left(\left(D^2-\left(A^2-1\right)C^2=1\wedge F^2-\left(A^2-1\right)E^2=1\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\wedge \left(I^2-\left(G^2-1\right)H^2=1\wedge E=\left(J+1\right)2C^2\wedge F\parallel \left(G-A\right)\right)\right)\wedge \left(\left(2C\parallel \left(G-1\right)\wedge F\parallel \left(H-C\right)\right)\wedge \left(2C\parallel \left(H-B\right)\wedge B\le C\right)\right)\right)\right)\right)$$

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.27c4	$$⊢\phi \to C=A{Y}_{\mathrm{rm}}B$$
5		jm2.27c5	$$⊢D=A{X}_{\mathrm{rm}}B$$
6		jm2.27c6	$$⊢Q=B\left(A{Y}_{\mathrm{rm}}B\right)$$
7		jm2.27c7	$$⊢E=A{Y}_{\mathrm{rm}}2Q$$
8		jm2.27c8	$$⊢F=A{X}_{\mathrm{rm}}2Q$$
9		jm2.27c9	$$⊢G=A+F^2\left(F^2-A\right)$$
10		jm2.27c10	$$⊢H=G{Y}_{\mathrm{rm}}B$$
11		jm2.27c11	$$⊢I=G{X}_{\mathrm{rm}}B$$
12		jm2.27c12	$$⊢J=\left(\frac{E}{2C^2}\right)-1$$
13	2	nnzd	$$⊢\phi \to B\in \mathbb{Z}$$
14		frmx	$$⊢X_{\mathrm{rm}}:{\mathbb{Z}}_{\ge 2}\times \mathbb{Z}⟶{\mathbb{N}}_0$$
15	14	fovcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in \mathbb{Z}\right)\to A{X}_{\mathrm{rm}}B\in {\mathbb{N}}_0$$
16	1 13 15	syl2anc	$$⊢\phi \to A{X}_{\mathrm{rm}}B\in {\mathbb{N}}_0$$
17	5 16	eqeltrid	$$⊢\phi \to D\in {\mathbb{N}}_0$$
18		2z	$$⊢2\in \mathbb{Z}$$
19	3	nnzd	$$⊢\phi \to C\in \mathbb{Z}$$
20	4 19	eqeltrrd	$$⊢\phi \to A{Y}_{\mathrm{rm}}B\in \mathbb{Z}$$
21	13 20	zmulcld	$$⊢\phi \to B\left(A{Y}_{\mathrm{rm}}B\right)\in \mathbb{Z}$$
22	6 21	eqeltrid	$$⊢\phi \to Q\in \mathbb{Z}$$
23		zmulcl	$$⊢\left(2\in \mathbb{Z}\wedge Q\in \mathbb{Z}\right)\to 2Q\in \mathbb{Z}$$
24	18 22 23	sylancr	$$⊢\phi \to 2Q\in \mathbb{Z}$$
25		frmy	$$⊢Y_{\mathrm{rm}}:{\mathbb{Z}}_{\ge 2}\times \mathbb{Z}⟶\mathbb{Z}$$
26	25	fovcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge 2Q\in \mathbb{Z}\right)\to A{Y}_{\mathrm{rm}}2Q\in \mathbb{Z}$$
27	1 24 26	syl2anc	$$⊢\phi \to A{Y}_{\mathrm{rm}}2Q\in \mathbb{Z}$$
28		rmy0	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A{Y}_{\mathrm{rm}}0=0$$
29	1 28	syl	$$⊢\phi \to A{Y}_{\mathrm{rm}}0=0$$
30		2nn	$$⊢2\in \mathbb{N}$$
31	4 3	eqeltrrd	$$⊢\phi \to A{Y}_{\mathrm{rm}}B\in \mathbb{N}$$
32	2 31	nnmulcld	$$⊢\phi \to B\left(A{Y}_{\mathrm{rm}}B\right)\in \mathbb{N}$$
33	6 32	eqeltrid	$$⊢\phi \to Q\in \mathbb{N}$$
34		nnmulcl	$$⊢\left(2\in \mathbb{N}\wedge Q\in \mathbb{N}\right)\to 2Q\in \mathbb{N}$$
35	30 33 34	sylancr	$$⊢\phi \to 2Q\in \mathbb{N}$$
36	35	nnnn0d	$$⊢\phi \to 2Q\in {\mathbb{N}}_0$$
37	36	nn0ge0d	$$⊢\phi \to 0\le 2Q$$
38		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
39		lermy	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge 0\in \mathbb{Z}\wedge 2Q\in \mathbb{Z}\right)\to \left(0\le 2Q\leftrightarrow A{Y}_{\mathrm{rm}}0\le A{Y}_{\mathrm{rm}}2Q\right)$$
40	1 38 24 39	syl3anc	$$⊢\phi \to \left(0\le 2Q\leftrightarrow A{Y}_{\mathrm{rm}}0\le A{Y}_{\mathrm{rm}}2Q\right)$$
41	37 40	mpbid	$$⊢\phi \to A{Y}_{\mathrm{rm}}0\le A{Y}_{\mathrm{rm}}2Q$$
42	29 41	eqbrtrrd	$$⊢\phi \to 0\le A{Y}_{\mathrm{rm}}2Q$$
43		elnn0z	$$⊢A{Y}_{\mathrm{rm}}2Q\in {\mathbb{N}}_0\leftrightarrow \left(A{Y}_{\mathrm{rm}}2Q\in \mathbb{Z}\wedge 0\le A{Y}_{\mathrm{rm}}2Q\right)$$
44	27 42 43	sylanbrc	$$⊢\phi \to A{Y}_{\mathrm{rm}}2Q\in {\mathbb{N}}_0$$
45	7 44	eqeltrid	$$⊢\phi \to E\in {\mathbb{N}}_0$$
46	14	fovcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge 2Q\in \mathbb{Z}\right)\to A{X}_{\mathrm{rm}}2Q\in {\mathbb{N}}_0$$
47	1 24 46	syl2anc	$$⊢\phi \to A{X}_{\mathrm{rm}}2Q\in {\mathbb{N}}_0$$
48	8 47	eqeltrid	$$⊢\phi \to F\in {\mathbb{N}}_0$$
49	17 45 48	3jca	$$⊢\phi \to \left(D\in {\mathbb{N}}_0\wedge E\in {\mathbb{N}}_0\wedge F\in {\mathbb{N}}_0\right)$$
50		2nn0	$$⊢2\in {\mathbb{N}}_0$$
51	48	nn0cnd	$$⊢\phi \to F\in ℂ$$
52	51	sqvald	$$⊢\phi \to F^2=FF$$
53	48 48	nn0mulcld	$$⊢\phi \to FF\in {\mathbb{N}}_0$$
54	52 53	eqeltrd	$$⊢\phi \to F^2\in {\mathbb{N}}_0$$
55		eluz2nn	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in \mathbb{N}$$
56	1 55	syl	$$⊢\phi \to A\in \mathbb{N}$$
57	56	nnnn0d	$$⊢\phi \to A\in {\mathbb{N}}_0$$
58	57	nn0red	$$⊢\phi \to A\in ℝ$$
59	48	nn0red	$$⊢\phi \to F\in ℝ$$
60	59 59	remulcld	$$⊢\phi \to FF\in ℝ$$
61		rmx1	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A{X}_{\mathrm{rm}}1=A$$
62	1 61	syl	$$⊢\phi \to A{X}_{\mathrm{rm}}1=A$$
63	35	nnge1d	$$⊢\phi \to 1\le 2Q$$
64		1nn0	$$⊢1\in {\mathbb{N}}_0$$
65	64	a1i	$$⊢\phi \to 1\in {\mathbb{N}}_0$$
66		lermxnn0	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge 1\in {\mathbb{N}}_0\wedge 2Q\in {\mathbb{N}}_0\right)\to \left(1\le 2Q\leftrightarrow A{X}_{\mathrm{rm}}1\le A{X}_{\mathrm{rm}}2Q\right)$$
67	1 65 36 66	syl3anc	$$⊢\phi \to \left(1\le 2Q\leftrightarrow A{X}_{\mathrm{rm}}1\le A{X}_{\mathrm{rm}}2Q\right)$$
68	63 67	mpbid	$$⊢\phi \to A{X}_{\mathrm{rm}}1\le A{X}_{\mathrm{rm}}2Q$$
69	62 68	eqbrtrrd	$$⊢\phi \to A\le A{X}_{\mathrm{rm}}2Q$$
70	69 8	breqtrrdi	$$⊢\phi \to A\le F$$
71	48	nn0ge0d	$$⊢\phi \to 0\le F$$
72		rmxnn	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge 2Q\in \mathbb{Z}\right)\to A{X}_{\mathrm{rm}}2Q\in \mathbb{N}$$
73	1 24 72	syl2anc	$$⊢\phi \to A{X}_{\mathrm{rm}}2Q\in \mathbb{N}$$
74	8 73	eqeltrid	$$⊢\phi \to F\in \mathbb{N}$$
75	74	nnge1d	$$⊢\phi \to 1\le F$$
76	59 59 71 75	lemulge12d	$$⊢\phi \to F\le FF$$
77	58 59 60 70 76	letrd	$$⊢\phi \to A\le FF$$
78	77 52	breqtrrd	$$⊢\phi \to A\le F^2$$
79		nn0sub	$$⊢\left(A\in {\mathbb{N}}_0\wedge F^2\in {\mathbb{N}}_0\right)\to \left(A\le F^2\leftrightarrow F^2-A\in {\mathbb{N}}_0\right)$$
80	57 54 79	syl2anc	$$⊢\phi \to \left(A\le F^2\leftrightarrow F^2-A\in {\mathbb{N}}_0\right)$$
81	78 80	mpbid	$$⊢\phi \to F^2-A\in {\mathbb{N}}_0$$
82	54 81	nn0mulcld	$$⊢\phi \to F^2\left(F^2-A\right)\in {\mathbb{N}}_0$$
83		uzaddcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge F^2\left(F^2-A\right)\in {\mathbb{N}}_0\right)\to A+F^2\left(F^2-A\right)\in {\mathbb{Z}}_{\ge 2}$$
84	1 82 83	syl2anc	$$⊢\phi \to A+F^2\left(F^2-A\right)\in {\mathbb{Z}}_{\ge 2}$$
85	9 84	eqeltrid	$$⊢\phi \to G\in {\mathbb{Z}}_{\ge 2}$$
86		eluznn0	$$⊢\left(2\in {\mathbb{N}}_0\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\to G\in {\mathbb{N}}_0$$
87	50 85 86	sylancr	$$⊢\phi \to G\in {\mathbb{N}}_0$$
88	25	fovcl	$$⊢\left(G\in {\mathbb{Z}}_{\ge 2}\wedge B\in \mathbb{Z}\right)\to G{Y}_{\mathrm{rm}}B\in \mathbb{Z}$$
89	85 13 88	syl2anc	$$⊢\phi \to G{Y}_{\mathrm{rm}}B\in \mathbb{Z}$$
90		rmy0	$$⊢G\in {\mathbb{Z}}_{\ge 2}\to G{Y}_{\mathrm{rm}}0=0$$
91	85 90	syl	$$⊢\phi \to G{Y}_{\mathrm{rm}}0=0$$
92	2	nnnn0d	$$⊢\phi \to B\in {\mathbb{N}}_0$$
93	92	nn0ge0d	$$⊢\phi \to 0\le B$$
94		lermy	$$⊢\left(G\in {\mathbb{Z}}_{\ge 2}\wedge 0\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to \left(0\le B\leftrightarrow G{Y}_{\mathrm{rm}}0\le G{Y}_{\mathrm{rm}}B\right)$$
95	85 38 13 94	syl3anc	$$⊢\phi \to \left(0\le B\leftrightarrow G{Y}_{\mathrm{rm}}0\le G{Y}_{\mathrm{rm}}B\right)$$
96	93 95	mpbid	$$⊢\phi \to G{Y}_{\mathrm{rm}}0\le G{Y}_{\mathrm{rm}}B$$
97	91 96	eqbrtrrd	$$⊢\phi \to 0\le G{Y}_{\mathrm{rm}}B$$
98		elnn0z	$$⊢G{Y}_{\mathrm{rm}}B\in {\mathbb{N}}_0\leftrightarrow \left(G{Y}_{\mathrm{rm}}B\in \mathbb{Z}\wedge 0\le G{Y}_{\mathrm{rm}}B\right)$$
99	89 97 98	sylanbrc	$$⊢\phi \to G{Y}_{\mathrm{rm}}B\in {\mathbb{N}}_0$$
100	10 99	eqeltrid	$$⊢\phi \to H\in {\mathbb{N}}_0$$
101	14	fovcl	$$⊢\left(G\in {\mathbb{Z}}_{\ge 2}\wedge B\in \mathbb{Z}\right)\to G{X}_{\mathrm{rm}}B\in {\mathbb{N}}_0$$
102	85 13 101	syl2anc	$$⊢\phi \to G{X}_{\mathrm{rm}}B\in {\mathbb{N}}_0$$
103	11 102	eqeltrid	$$⊢\phi \to I\in {\mathbb{N}}_0$$
104	87 100 103	3jca	$$⊢\phi \to \left(G\in {\mathbb{N}}_0\wedge H\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)$$
105		zsqcl	$$⊢A{Y}_{\mathrm{rm}}B\in \mathbb{Z}\to {\left(A{Y}_{\mathrm{rm}}B\right)}^2\in \mathbb{Z}$$
106	20 105	syl	$$⊢\phi \to {\left(A{Y}_{\mathrm{rm}}B\right)}^2\in \mathbb{Z}$$
107		zmulcl	$$⊢\left(2\in \mathbb{Z}\wedge {\left(A{Y}_{\mathrm{rm}}B\right)}^2\in \mathbb{Z}\right)\to 2{\left(A{Y}_{\mathrm{rm}}B\right)}^2\in \mathbb{Z}$$
108	18 106 107	sylancr	$$⊢\phi \to 2{\left(A{Y}_{\mathrm{rm}}B\right)}^2\in \mathbb{Z}$$
109	25	fovcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge Q\in \mathbb{Z}\right)\to A{Y}_{\mathrm{rm}}Q\in \mathbb{Z}$$
110	1 22 109	syl2anc	$$⊢\phi \to A{Y}_{\mathrm{rm}}Q\in \mathbb{Z}$$
111		zmulcl	$$⊢\left(2\in \mathbb{Z}\wedge A{Y}_{\mathrm{rm}}Q\in \mathbb{Z}\right)\to 2\left(A{Y}_{\mathrm{rm}}Q\right)\in \mathbb{Z}$$
112	18 110 111	sylancr	$$⊢\phi \to 2\left(A{Y}_{\mathrm{rm}}Q\right)\in \mathbb{Z}$$
113		iddvds	$$⊢B\left(A{Y}_{\mathrm{rm}}B\right)\in \mathbb{Z}\to B\left(A{Y}_{\mathrm{rm}}B\right)\parallel B\left(A{Y}_{\mathrm{rm}}B\right)$$
114	21 113	syl	$$⊢\phi \to B\left(A{Y}_{\mathrm{rm}}B\right)\parallel B\left(A{Y}_{\mathrm{rm}}B\right)$$
115	114 6	breqtrrdi	$$⊢\phi \to B\left(A{Y}_{\mathrm{rm}}B\right)\parallel Q$$
116		jm2.20nn	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge Q\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to \left({\left(A{Y}_{\mathrm{rm}}B\right)}^2\parallel \left(A{Y}_{\mathrm{rm}}Q\right)\leftrightarrow B\left(A{Y}_{\mathrm{rm}}B\right)\parallel Q\right)$$
117	1 33 2 116	syl3anc	$$⊢\phi \to \left({\left(A{Y}_{\mathrm{rm}}B\right)}^2\parallel \left(A{Y}_{\mathrm{rm}}Q\right)\leftrightarrow B\left(A{Y}_{\mathrm{rm}}B\right)\parallel Q\right)$$
118	115 117	mpbird	$$⊢\phi \to {\left(A{Y}_{\mathrm{rm}}B\right)}^2\parallel \left(A{Y}_{\mathrm{rm}}Q\right)$$
119	18	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
120		dvdscmul	$$⊢\left({\left(A{Y}_{\mathrm{rm}}B\right)}^2\in \mathbb{Z}\wedge A{Y}_{\mathrm{rm}}Q\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\to \left({\left(A{Y}_{\mathrm{rm}}B\right)}^2\parallel \left(A{Y}_{\mathrm{rm}}Q\right)\to 2{\left(A{Y}_{\mathrm{rm}}B\right)}^2\parallel 2\left(A{Y}_{\mathrm{rm}}Q\right)\right)$$
121	106 110 119 120	syl3anc	$$⊢\phi \to \left({\left(A{Y}_{\mathrm{rm}}B\right)}^2\parallel \left(A{Y}_{\mathrm{rm}}Q\right)\to 2{\left(A{Y}_{\mathrm{rm}}B\right)}^2\parallel 2\left(A{Y}_{\mathrm{rm}}Q\right)\right)$$
122	118 121	mpd	$$⊢\phi \to 2{\left(A{Y}_{\mathrm{rm}}B\right)}^2\parallel 2\left(A{Y}_{\mathrm{rm}}Q\right)$$
123	14	fovcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge Q\in \mathbb{Z}\right)\to A{X}_{\mathrm{rm}}Q\in {\mathbb{N}}_0$$
124	1 22 123	syl2anc	$$⊢\phi \to A{X}_{\mathrm{rm}}Q\in {\mathbb{N}}_0$$
125	124	nn0zd	$$⊢\phi \to A{X}_{\mathrm{rm}}Q\in \mathbb{Z}$$
126		dvdsmul1	$$⊢\left(2\left(A{Y}_{\mathrm{rm}}Q\right)\in \mathbb{Z}\wedge A{X}_{\mathrm{rm}}Q\in \mathbb{Z}\right)\to 2\left(A{Y}_{\mathrm{rm}}Q\right)\parallel 2\left(A{Y}_{\mathrm{rm}}Q\right)\left(A{X}_{\mathrm{rm}}Q\right)$$
127	112 125 126	syl2anc	$$⊢\phi \to 2\left(A{Y}_{\mathrm{rm}}Q\right)\parallel 2\left(A{Y}_{\mathrm{rm}}Q\right)\left(A{X}_{\mathrm{rm}}Q\right)$$
128		rmydbl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge Q\in \mathbb{Z}\right)\to A{Y}_{\mathrm{rm}}2Q=2\left(A{X}_{\mathrm{rm}}Q\right)\left(A{Y}_{\mathrm{rm}}Q\right)$$
129	1 22 128	syl2anc	$$⊢\phi \to A{Y}_{\mathrm{rm}}2Q=2\left(A{X}_{\mathrm{rm}}Q\right)\left(A{Y}_{\mathrm{rm}}Q\right)$$
130		2cnd	$$⊢\phi \to 2\in ℂ$$
131	124	nn0cnd	$$⊢\phi \to A{X}_{\mathrm{rm}}Q\in ℂ$$
132	110	zcnd	$$⊢\phi \to A{Y}_{\mathrm{rm}}Q\in ℂ$$
133	130 131 132	mul32d	$$⊢\phi \to 2\left(A{X}_{\mathrm{rm}}Q\right)\left(A{Y}_{\mathrm{rm}}Q\right)=2\left(A{Y}_{\mathrm{rm}}Q\right)\left(A{X}_{\mathrm{rm}}Q\right)$$
134	129 133	eqtrd	$$⊢\phi \to A{Y}_{\mathrm{rm}}2Q=2\left(A{Y}_{\mathrm{rm}}Q\right)\left(A{X}_{\mathrm{rm}}Q\right)$$
135	127 134	breqtrrd	$$⊢\phi \to 2\left(A{Y}_{\mathrm{rm}}Q\right)\parallel \left(A{Y}_{\mathrm{rm}}2Q\right)$$
136	108 112 27 122 135	dvdstrd	$$⊢\phi \to 2{\left(A{Y}_{\mathrm{rm}}B\right)}^2\parallel \left(A{Y}_{\mathrm{rm}}2Q\right)$$
137	4	oveq1d	$$⊢\phi \to C^2={\left(A{Y}_{\mathrm{rm}}B\right)}^2$$
138	137	oveq2d	$$⊢\phi \to 2C^2=2{\left(A{Y}_{\mathrm{rm}}B\right)}^2$$
139	7	a1i	$$⊢\phi \to E=A{Y}_{\mathrm{rm}}2Q$$
140	136 138 139	3brtr4d	$$⊢\phi \to 2C^2\parallel E$$
141	7 27	eqeltrid	$$⊢\phi \to E\in \mathbb{Z}$$
142	35	nngt0d	$$⊢\phi \to 0<2Q$$
143		ltrmy	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge 0\in \mathbb{Z}\wedge 2Q\in \mathbb{Z}\right)\to \left(0<2Q\leftrightarrow A{Y}_{\mathrm{rm}}0<A{Y}_{\mathrm{rm}}2Q\right)$$
144	1 38 24 143	syl3anc	$$⊢\phi \to \left(0<2Q\leftrightarrow A{Y}_{\mathrm{rm}}0<A{Y}_{\mathrm{rm}}2Q\right)$$
145	142 144	mpbid	$$⊢\phi \to A{Y}_{\mathrm{rm}}0<A{Y}_{\mathrm{rm}}2Q$$
146	29	eqcomd	$$⊢\phi \to 0=A{Y}_{\mathrm{rm}}0$$
147	145 146 139	3brtr4d	$$⊢\phi \to 0<E$$
148		elnnz	$$⊢E\in \mathbb{N}\leftrightarrow \left(E\in \mathbb{Z}\wedge 0<E\right)$$
149	141 147 148	sylanbrc	$$⊢\phi \to E\in \mathbb{N}$$
150	3	nnsqcld	$$⊢\phi \to C^2\in \mathbb{N}$$
151		nnmulcl	$$⊢\left(2\in \mathbb{N}\wedge C^2\in \mathbb{N}\right)\to 2C^2\in \mathbb{N}$$
152	30 150 151	sylancr	$$⊢\phi \to 2C^2\in \mathbb{N}$$
153		nndivdvds	$$⊢\left(E\in \mathbb{N}\wedge 2C^2\in \mathbb{N}\right)\to \left(2C^2\parallel E\leftrightarrow \frac{E}{2C^2}\in \mathbb{N}\right)$$
154	149 152 153	syl2anc	$$⊢\phi \to \left(2C^2\parallel E\leftrightarrow \frac{E}{2C^2}\in \mathbb{N}\right)$$
155	140 154	mpbid	$$⊢\phi \to \frac{E}{2C^2}\in \mathbb{N}$$
156		nnm1nn0	$$⊢\frac{E}{2C^2}\in \mathbb{N}\to \left(\frac{E}{2C^2}\right)-1\in {\mathbb{N}}_0$$
157	155 156	syl	$$⊢\phi \to \left(\frac{E}{2C^2}\right)-1\in {\mathbb{N}}_0$$
158	12 157	eqeltrid	$$⊢\phi \to J\in {\mathbb{N}}_0$$
159	5	oveq1i	$$⊢D^2={\left(A{X}_{\mathrm{rm}}B\right)}^2$$
160	159	a1i	$$⊢\phi \to D^2={\left(A{X}_{\mathrm{rm}}B\right)}^2$$
161	137	oveq2d	$$⊢\phi \to \left(A^2-1\right)C^2=\left(A^2-1\right){\left(A{Y}_{\mathrm{rm}}B\right)}^2$$
162	160 161	oveq12d	$$⊢\phi \to D^2-\left(A^2-1\right)C^2={\left(A{X}_{\mathrm{rm}}B\right)}^2-\left(A^2-1\right){\left(A{Y}_{\mathrm{rm}}B\right)}^2$$
163		rmxynorm	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in \mathbb{Z}\right)\to {\left(A{X}_{\mathrm{rm}}B\right)}^2-\left(A^2-1\right){\left(A{Y}_{\mathrm{rm}}B\right)}^2=1$$
164	1 13 163	syl2anc	$$⊢\phi \to {\left(A{X}_{\mathrm{rm}}B\right)}^2-\left(A^2-1\right){\left(A{Y}_{\mathrm{rm}}B\right)}^2=1$$
165	162 164	eqtrd	$$⊢\phi \to D^2-\left(A^2-1\right)C^2=1$$
166	8	oveq1i	$$⊢F^2={\left(A{X}_{\mathrm{rm}}2Q\right)}^2$$
167	7	oveq1i	$$⊢E^2={\left(A{Y}_{\mathrm{rm}}2Q\right)}^2$$
168	167	oveq2i	$$⊢\left(A^2-1\right)E^2=\left(A^2-1\right){\left(A{Y}_{\mathrm{rm}}2Q\right)}^2$$
169	166 168	oveq12i	$$⊢F^2-\left(A^2-1\right)E^2={\left(A{X}_{\mathrm{rm}}2Q\right)}^2-\left(A^2-1\right){\left(A{Y}_{\mathrm{rm}}2Q\right)}^2$$
170		rmxynorm	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge 2Q\in \mathbb{Z}\right)\to {\left(A{X}_{\mathrm{rm}}2Q\right)}^2-\left(A^2-1\right){\left(A{Y}_{\mathrm{rm}}2Q\right)}^2=1$$
171	1 24 170	syl2anc	$$⊢\phi \to {\left(A{X}_{\mathrm{rm}}2Q\right)}^2-\left(A^2-1\right){\left(A{Y}_{\mathrm{rm}}2Q\right)}^2=1$$
172	169 171	eqtrid	$$⊢\phi \to F^2-\left(A^2-1\right)E^2=1$$
173	165 172 85	3jca	$$⊢\phi \to \left(D^2-\left(A^2-1\right)C^2=1\wedge F^2-\left(A^2-1\right)E^2=1\wedge G\in {\mathbb{Z}}_{\ge 2}\right)$$
174	11	oveq1i	$$⊢I^2={\left(G{X}_{\mathrm{rm}}B\right)}^2$$
175	10	oveq1i	$$⊢H^2={\left(G{Y}_{\mathrm{rm}}B\right)}^2$$
176	175	oveq2i	$$⊢\left(G^2-1\right)H^2=\left(G^2-1\right){\left(G{Y}_{\mathrm{rm}}B\right)}^2$$
177	174 176	oveq12i	$$⊢I^2-\left(G^2-1\right)H^2={\left(G{X}_{\mathrm{rm}}B\right)}^2-\left(G^2-1\right){\left(G{Y}_{\mathrm{rm}}B\right)}^2$$
178		rmxynorm	$$⊢\left(G\in {\mathbb{Z}}_{\ge 2}\wedge B\in \mathbb{Z}\right)\to {\left(G{X}_{\mathrm{rm}}B\right)}^2-\left(G^2-1\right){\left(G{Y}_{\mathrm{rm}}B\right)}^2=1$$
179	85 13 178	syl2anc	$$⊢\phi \to {\left(G{X}_{\mathrm{rm}}B\right)}^2-\left(G^2-1\right){\left(G{Y}_{\mathrm{rm}}B\right)}^2=1$$
180	177 179	eqtrid	$$⊢\phi \to I^2-\left(G^2-1\right)H^2=1$$
181	12	a1i	$$⊢\phi \to J=\left(\frac{E}{2C^2}\right)-1$$
182	181	oveq1d	$$⊢\phi \to J+1=\left(\frac{E}{2C^2}\right)-1+1$$
183	141	zcnd	$$⊢\phi \to E\in ℂ$$
184	152	nncnd	$$⊢\phi \to 2C^2\in ℂ$$
185	152	nnne0d	$$⊢\phi \to 2C^2\ne 0$$
186	183 184 185	divcld	$$⊢\phi \to \frac{E}{2C^2}\in ℂ$$
187		ax-1cn	$$⊢1\in ℂ$$
188		npcan	$$⊢\left(\frac{E}{2C^2}\in ℂ\wedge 1\in ℂ\right)\to \left(\frac{E}{2C^2}\right)-1+1=\frac{E}{2C^2}$$
189	186 187 188	sylancl	$$⊢\phi \to \left(\frac{E}{2C^2}\right)-1+1=\frac{E}{2C^2}$$
190	182 189	eqtrd	$$⊢\phi \to J+1=\frac{E}{2C^2}$$
191	190	oveq1d	$$⊢\phi \to \left(J+1\right)2C^2=\left(\frac{E}{2C^2}\right)2C^2$$
192	183 184 185	divcan1d	$$⊢\phi \to \left(\frac{E}{2C^2}\right)2C^2=E$$
193	191 192	eqtr2d	$$⊢\phi \to E=\left(J+1\right)2C^2$$
194	48	nn0zd	$$⊢\phi \to F\in \mathbb{Z}$$
195	81	nn0zd	$$⊢\phi \to F^2-A\in \mathbb{Z}$$
196	194 195	zmulcld	$$⊢\phi \to F\left(F^2-A\right)\in \mathbb{Z}$$
197		dvdsmul1	$$⊢\left(F\in \mathbb{Z}\wedge F\left(F^2-A\right)\in \mathbb{Z}\right)\to F\parallel FF\left(F^2-A\right)$$
198	194 196 197	syl2anc	$$⊢\phi \to F\parallel FF\left(F^2-A\right)$$
199	9	oveq1i	$$⊢G-A=A+F^2\left(F^2-A\right)-A$$
200	57	nn0cnd	$$⊢\phi \to A\in ℂ$$
201	82	nn0cnd	$$⊢\phi \to F^2\left(F^2-A\right)\in ℂ$$
202	200 201	pncan2d	$$⊢\phi \to A+F^2\left(F^2-A\right)-A=F^2\left(F^2-A\right)$$
203	52	oveq1d	$$⊢\phi \to F^2\left(F^2-A\right)=FF\left(F^2-A\right)$$
204	81	nn0cnd	$$⊢\phi \to F^2-A\in ℂ$$
205	51 51 204	mulassd	$$⊢\phi \to FF\left(F^2-A\right)=FF\left(F^2-A\right)$$
206	202 203 205	3eqtrd	$$⊢\phi \to A+F^2\left(F^2-A\right)-A=FF\left(F^2-A\right)$$
207	199 206	eqtrid	$$⊢\phi \to G-A=FF\left(F^2-A\right)$$
208	198 207	breqtrrd	$$⊢\phi \to F\parallel \left(G-A\right)$$
209	180 193 208	3jca	$$⊢\phi \to \left(I^2-\left(G^2-1\right)H^2=1\wedge E=\left(J+1\right)2C^2\wedge F\parallel \left(G-A\right)\right)$$
210		zmulcl	$$⊢\left(2\in \mathbb{Z}\wedge C\in \mathbb{Z}\right)\to 2C\in \mathbb{Z}$$
211	18 19 210	sylancr	$$⊢\phi \to 2C\in \mathbb{Z}$$
212		eluzelz	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in \mathbb{Z}$$
213	1 212	syl	$$⊢\phi \to A\in \mathbb{Z}$$
214	82	nn0zd	$$⊢\phi \to F^2\left(F^2-A\right)\in \mathbb{Z}$$
215		1z	$$⊢1\in \mathbb{Z}$$
216		zsubcl	$$⊢\left(1\in \mathbb{Z}\wedge A\in \mathbb{Z}\right)\to 1-A\in \mathbb{Z}$$
217	215 213 216	sylancr	$$⊢\phi \to 1-A\in \mathbb{Z}$$
218		zmulcl	$$⊢\left(1\in \mathbb{Z}\wedge 1-A\in \mathbb{Z}\right)\to 1\left(1-A\right)\in \mathbb{Z}$$
219	215 217 218	sylancr	$$⊢\phi \to 1\left(1-A\right)\in \mathbb{Z}$$
220		congid	$$⊢\left(2C\in \mathbb{Z}\wedge A\in \mathbb{Z}\right)\to 2C\parallel \left(A-A\right)$$
221	211 213 220	syl2anc	$$⊢\phi \to 2C\parallel \left(A-A\right)$$
222	54	nn0zd	$$⊢\phi \to F^2\in \mathbb{Z}$$
223	215	a1i	$$⊢\phi \to 1\in \mathbb{Z}$$
224	3	nncnd	$$⊢\phi \to C\in ℂ$$
225	130 224 224	mulassd	$$⊢\phi \to 2CC=2CC$$
226	224	sqvald	$$⊢\phi \to C^2=CC$$
227	226	oveq2d	$$⊢\phi \to 2C^2=2CC$$
228	225 227	eqtr4d	$$⊢\phi \to 2CC=2C^2$$
229	228 140	eqbrtrd	$$⊢\phi \to 2CC\parallel E$$
230		muldvds1	$$⊢\left(2C\in \mathbb{Z}\wedge C\in \mathbb{Z}\wedge E\in \mathbb{Z}\right)\to \left(2CC\parallel E\to 2C\parallel E\right)$$
231	211 19 141 230	syl3anc	$$⊢\phi \to \left(2CC\parallel E\to 2C\parallel E\right)$$
232	229 231	mpd	$$⊢\phi \to 2C\parallel E$$
233		zsqcl	$$⊢A\in \mathbb{Z}\to A^2\in \mathbb{Z}$$
234	213 233	syl	$$⊢\phi \to A^2\in \mathbb{Z}$$
235		peano2zm	$$⊢A^2\in \mathbb{Z}\to A^2-1\in \mathbb{Z}$$
236	234 235	syl	$$⊢\phi \to A^2-1\in \mathbb{Z}$$
237	236 141	zmulcld	$$⊢\phi \to \left(A^2-1\right)E\in \mathbb{Z}$$
238		dvdsmultr2	$$⊢\left(2C\in \mathbb{Z}\wedge \left(A^2-1\right)E\in \mathbb{Z}\wedge E\in \mathbb{Z}\right)\to \left(2C\parallel E\to 2C\parallel \left(A^2-1\right)EE\right)$$
239	211 237 141 238	syl3anc	$$⊢\phi \to \left(2C\parallel E\to 2C\parallel \left(A^2-1\right)EE\right)$$
240	232 239	mpd	$$⊢\phi \to 2C\parallel \left(A^2-1\right)EE$$
241	183	sqvald	$$⊢\phi \to E^2=EE$$
242	241	oveq2d	$$⊢\phi \to \left(A^2-1\right)E^2=\left(A^2-1\right)EE$$
243	200	sqcld	$$⊢\phi \to A^2\in ℂ$$
244		subcl	$$⊢\left(A^2\in ℂ\wedge 1\in ℂ\right)\to A^2-1\in ℂ$$
245	243 187 244	sylancl	$$⊢\phi \to A^2-1\in ℂ$$
246	245 183 183	mulassd	$$⊢\phi \to \left(A^2-1\right)EE=\left(A^2-1\right)EE$$
247	242 246	eqtr4d	$$⊢\phi \to \left(A^2-1\right)E^2=\left(A^2-1\right)EE$$
248	240 247	breqtrrd	$$⊢\phi \to 2C\parallel \left(A^2-1\right)E^2$$
249	51	sqcld	$$⊢\phi \to F^2\in ℂ$$
250	183	sqcld	$$⊢\phi \to E^2\in ℂ$$
251	245 250	mulcld	$$⊢\phi \to \left(A^2-1\right)E^2\in ℂ$$
252	187	a1i	$$⊢\phi \to 1\in ℂ$$
253		subsub23	$$⊢\left(F^2\in ℂ\wedge \left(A^2-1\right)E^2\in ℂ\wedge 1\in ℂ\right)\to \left(F^2-\left(A^2-1\right)E^2=1\leftrightarrow F^2-1=\left(A^2-1\right)E^2\right)$$
254	249 251 252 253	syl3anc	$$⊢\phi \to \left(F^2-\left(A^2-1\right)E^2=1\leftrightarrow F^2-1=\left(A^2-1\right)E^2\right)$$
255	172 254	mpbid	$$⊢\phi \to F^2-1=\left(A^2-1\right)E^2$$
256	248 255	breqtrrd	$$⊢\phi \to 2C\parallel \left(F^2-1\right)$$
257		congsub	$$⊢\left(\left(2C\in \mathbb{Z}\wedge F^2\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)\wedge \left(A\in \mathbb{Z}\wedge A\in \mathbb{Z}\right)\wedge \left(2C\parallel \left(F^2-1\right)\wedge 2C\parallel \left(A-A\right)\right)\right)\to 2C\parallel \left(F^2-A-\left(1-A\right)\right)$$
258	211 222 223 213 213 256 221 257	syl322anc	$$⊢\phi \to 2C\parallel \left(F^2-A-\left(1-A\right)\right)$$
259		congmul	$$⊢\left(\left(2C\in \mathbb{Z}\wedge F^2\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)\wedge \left(F^2-A\in \mathbb{Z}\wedge 1-A\in \mathbb{Z}\right)\wedge \left(2C\parallel \left(F^2-1\right)\wedge 2C\parallel \left(F^2-A-\left(1-A\right)\right)\right)\right)\to 2C\parallel \left(F^2\left(F^2-A\right)-1\left(1-A\right)\right)$$
260	211 222 223 195 217 256 258 259	syl322anc	$$⊢\phi \to 2C\parallel \left(F^2\left(F^2-A\right)-1\left(1-A\right)\right)$$
261		congadd	$$⊢\left(\left(2C\in \mathbb{Z}\wedge A\in \mathbb{Z}\wedge A\in \mathbb{Z}\right)\wedge \left(F^2\left(F^2-A\right)\in \mathbb{Z}\wedge 1\left(1-A\right)\in \mathbb{Z}\right)\wedge \left(2C\parallel \left(A-A\right)\wedge 2C\parallel \left(F^2\left(F^2-A\right)-1\left(1-A\right)\right)\right)\right)\to 2C\parallel \left(A+F^2\left(F^2-A\right)-\left(A+1\left(1-A\right)\right)\right)$$
262	211 213 213 214 219 221 260 261	syl322anc	$$⊢\phi \to 2C\parallel \left(A+F^2\left(F^2-A\right)-\left(A+1\left(1-A\right)\right)\right)$$
263	9	a1i	$$⊢\phi \to G=A+F^2\left(F^2-A\right)$$
264	217	zcnd	$$⊢\phi \to 1-A\in ℂ$$
265	264	mullidd	$$⊢\phi \to 1\left(1-A\right)=1-A$$
266	265	oveq2d	$$⊢\phi \to A+1\left(1-A\right)=A+1-A$$
267		pncan3	$$⊢\left(A\in ℂ\wedge 1\in ℂ\right)\to A+1-A=1$$
268	200 187 267	sylancl	$$⊢\phi \to A+1-A=1$$
269	266 268	eqtr2d	$$⊢\phi \to 1=A+1\left(1-A\right)$$
270	263 269	oveq12d	$$⊢\phi \to G-1=A+F^2\left(F^2-A\right)-\left(A+1\left(1-A\right)\right)$$
271	262 270	breqtrrd	$$⊢\phi \to 2C\parallel \left(G-1\right)$$
272		eluzelz	$$⊢G\in {\mathbb{Z}}_{\ge 2}\to G\in \mathbb{Z}$$
273	85 272	syl	$$⊢\phi \to G\in \mathbb{Z}$$
274	273 213	zsubcld	$$⊢\phi \to G-A\in \mathbb{Z}$$
275	10 89	eqeltrid	$$⊢\phi \to H\in \mathbb{Z}$$
276	275 19	zsubcld	$$⊢\phi \to H-C\in \mathbb{Z}$$
277		jm2.15nn0	$$⊢\left(G\in {\mathbb{Z}}_{\ge 2}\wedge A\in {\mathbb{Z}}_{\ge 2}\wedge B\in {\mathbb{N}}_0\right)\to \left(G-A\right)\parallel \left(\left(G{Y}_{\mathrm{rm}}B\right)-\left(A{Y}_{\mathrm{rm}}B\right)\right)$$
278	85 1 92 277	syl3anc	$$⊢\phi \to \left(G-A\right)\parallel \left(\left(G{Y}_{\mathrm{rm}}B\right)-\left(A{Y}_{\mathrm{rm}}B\right)\right)$$
279	10	a1i	$$⊢\phi \to H=G{Y}_{\mathrm{rm}}B$$
280	279 4	oveq12d	$$⊢\phi \to H-C=\left(G{Y}_{\mathrm{rm}}B\right)-\left(A{Y}_{\mathrm{rm}}B\right)$$
281	278 280	breqtrrd	$$⊢\phi \to \left(G-A\right)\parallel \left(H-C\right)$$
282	194 274 276 208 281	dvdstrd	$$⊢\phi \to F\parallel \left(H-C\right)$$
283		peano2zm	$$⊢G\in \mathbb{Z}\to G-1\in \mathbb{Z}$$
284	273 283	syl	$$⊢\phi \to G-1\in \mathbb{Z}$$
285	275 13	zsubcld	$$⊢\phi \to H-B\in \mathbb{Z}$$
286		jm2.16nn0	$$⊢\left(G\in {\mathbb{Z}}_{\ge 2}\wedge B\in {\mathbb{N}}_0\right)\to \left(G-1\right)\parallel \left(\left(G{Y}_{\mathrm{rm}}B\right)-B\right)$$
287	85 92 286	syl2anc	$$⊢\phi \to \left(G-1\right)\parallel \left(\left(G{Y}_{\mathrm{rm}}B\right)-B\right)$$
288	10	oveq1i	$$⊢H-B=\left(G{Y}_{\mathrm{rm}}B\right)-B$$
289	287 288	breqtrrdi	$$⊢\phi \to \left(G-1\right)\parallel \left(H-B\right)$$
290	211 284 285 271 289	dvdstrd	$$⊢\phi \to 2C\parallel \left(H-B\right)$$
291		rmygeid	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in {\mathbb{N}}_0\right)\to B\le A{Y}_{\mathrm{rm}}B$$
292	1 92 291	syl2anc	$$⊢\phi \to B\le A{Y}_{\mathrm{rm}}B$$
293	292 4	breqtrrd	$$⊢\phi \to B\le C$$
294	290 293	jca	$$⊢\phi \to \left(2C\parallel \left(H-B\right)\wedge B\le C\right)$$
295	271 282 294	jca31	$$⊢\phi \to \left(\left(2C\parallel \left(G-1\right)\wedge F\parallel \left(H-C\right)\right)\wedge \left(2C\parallel \left(H-B\right)\wedge B\le C\right)\right)$$
296	173 209 295	jca31	$$⊢\phi \to \left(\left(\left(D^2-\left(A^2-1\right)C^2=1\wedge F^2-\left(A^2-1\right)E^2=1\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\wedge \left(I^2-\left(G^2-1\right)H^2=1\wedge E=\left(J+1\right)2C^2\wedge F\parallel \left(G-A\right)\right)\right)\wedge \left(\left(2C\parallel \left(G-1\right)\wedge F\parallel \left(H-C\right)\right)\wedge \left(2C\parallel \left(H-B\right)\wedge B\le C\right)\right)\right)$$
297	158 296	jca	$$⊢\phi \to \left(J\in {\mathbb{N}}_0\wedge \left(\left(\left(D^2-\left(A^2-1\right)C^2=1\wedge F^2-\left(A^2-1\right)E^2=1\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\wedge \left(I^2-\left(G^2-1\right)H^2=1\wedge E=\left(J+1\right)2C^2\wedge F\parallel \left(G-A\right)\right)\right)\wedge \left(\left(2C\parallel \left(G-1\right)\wedge F\parallel \left(H-C\right)\right)\wedge \left(2C\parallel \left(H-B\right)\wedge B\le C\right)\right)\right)\right)$$
298	49 104 297	jca31	$$⊢\phi \to \left(\left(\left(D\in {\mathbb{N}}_0\wedge E\in {\mathbb{N}}_0\wedge F\in {\mathbb{N}}_0\right)\wedge \left(G\in {\mathbb{N}}_0\wedge H\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\right)\wedge \left(J\in {\mathbb{N}}_0\wedge \left(\left(\left(D^2-\left(A^2-1\right)C^2=1\wedge F^2-\left(A^2-1\right)E^2=1\wedge G\in {\mathbb{Z}}_{\ge 2}\right)\wedge \left(I^2-\left(G^2-1\right)H^2=1\wedge E=\left(J+1\right)2C^2\wedge F\parallel \left(G-A\right)\right)\right)\wedge \left(\left(2C\parallel \left(G-1\right)\wedge F\parallel \left(H-C\right)\right)\wedge \left(2C\parallel \left(H-B\right)\wedge B\le C\right)\right)\right)\right)\right)$$