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	$⊢ φ \to A \in ℤ_{\geq 2}$
	jm2.27a2	$⊢ φ \to B \in ℕ$
	jm2.27a3	$⊢ φ \to C \in ℕ$
	jm2.27a4	$⊢ φ \to D \in ℕ_{0}$
	jm2.27a5	$⊢ φ \to E \in ℕ_{0}$
	jm2.27a6	$⊢ φ \to F \in ℕ_{0}$
	jm2.27a7	$⊢ φ \to G \in ℕ_{0}$
	jm2.27a8	$⊢ φ \to H \in ℕ_{0}$
	jm2.27a9	$⊢ φ \to I \in ℕ_{0}$
	jm2.27a10	$⊢ φ \to J \in ℕ_{0}$
	jm2.27a11	$⊢ φ \to D^{2} - (A^{2} - 1) C^{2} = 1$
	jm2.27a12	$⊢ φ \to F^{2} - (A^{2} - 1) E^{2} = 1$
	jm2.27a13	$⊢ φ \to G \in ℤ_{\geq 2}$
	jm2.27a14	$⊢ φ \to I^{2} - (G^{2} - 1) H^{2} = 1$
	jm2.27a15	$⊢ φ \to E = (J + 1) 2 C^{2}$
	jm2.27a16	$⊢ φ \to F ∥ (G - A)$
	jm2.27a17	$⊢ φ \to 2 C ∥ (G - 1)$
	jm2.27a18	$⊢ φ \to F ∥ (H - C)$
	jm2.27a19	$⊢ φ \to 2 C ∥ (H - B)$
	jm2.27a20	$⊢ φ \to B \leq C$
	jm2.27a21	$⊢ φ \to P \in ℤ$
	jm2.27a22	$⊢ φ \to D = A X_{rm} P$
	jm2.27a23	$⊢ φ \to C = A Y_{rm} P$
	jm2.27a24	$⊢ φ \to Q \in ℤ$
	jm2.27a25	$⊢ φ \to F = A X_{rm} Q$
	jm2.27a26	$⊢ φ \to E = A Y_{rm} Q$
	jm2.27a27	$⊢ φ \to R \in ℤ$
	jm2.27a28	$⊢ φ \to I = G X_{rm} R$
	jm2.27a29	$⊢ φ \to H = G Y_{rm} R$
Assertion	jm2.27a	$⊢ φ \to C = A Y_{rm} B$

Proof

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

Metamath Proof Explorer

Theorem jm2.27a

Proof