jm2.27

Description: Lemma 2.27 of JonesMatijasevic p. 697; rmY is a diophantine relation. 0 was excluded from the range of B and the lower limit of G was imposed because the source proof does not seem to work otherwise; quite possible I'm just missing something. The source proof uses both i and I; i has been changed to j to avoid collision. This theorem is basically nothing but substitution instances, all the work is done in jm2.27a and jm2.27c . Once Diophantine relations have been defined, the content of the theorem is "rmY is Diophantine". (Contributed by Stefan O'Rear, 4-Oct-2014)

		Ref	Expression
	Assertion	jm2.27	$⊢ (A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \to (C = A Y_{rm} B \leftrightarrow \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} \exists i \in ℕ_{0} \exists j \in ℕ_{0} (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))))$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land C = A Y_{rm} B) \to A \in ℤ_{\geq 2}$
2		simpl2	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land C = A Y_{rm} B) \to B \in ℕ$
3		simpl3	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land C = A Y_{rm} B) \to C \in ℕ$
4		simpr	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land C = A Y_{rm} B) \to C = A Y_{rm} B$
5		eqid	$⊢ A X_{rm} B = A X_{rm} B$
6		eqid	$⊢ B (A Y_{rm} B) = B (A Y_{rm} B)$
7		eqid	$⊢ A Y_{rm} 2 B (A Y_{rm} B) = A Y_{rm} 2 B (A Y_{rm} B)$
8		eqid	$⊢ A X_{rm} 2 B (A Y_{rm} B) = A X_{rm} 2 B (A Y_{rm} B)$
9		eqid	$⊢ A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) = A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)$
10		eqid	$⊢ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B$
11		eqid	$⊢ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B$
12		eqid	$⊢ (\frac{A Y_{rm} 2 B (A Y_{rm} B)}{2 C^{2}}) - 1 = (\frac{A Y_{rm} 2 B (A Y_{rm} B)}{2 C^{2}}) - 1$
13	1 2 3 4 5 6 7 8 9 10 11 12	jm2.27c	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land C = A Y_{rm} B) \to (((A X_{rm} B \in ℕ_{0} \land A Y_{rm} 2 B (A Y_{rm} B) \in ℕ_{0} \land A X_{rm} 2 B (A Y_{rm} B) \in ℕ_{0}) \land (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℕ_{0} \land (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B \in ℕ_{0} \land (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B \in ℕ_{0})) \land ((\frac{A Y_{rm} 2 B (A Y_{rm} B)}{2 C^{2}}) - 1 \in ℕ_{0} \land ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land ({((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B)}^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = ((\frac{A Y_{rm} 2 B (A Y_{rm} B)}{2 C^{2}}) - 1 + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))) \land ((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - C)) \land (2 C ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - B) \land B \leq C)))))$
14	13	simpld	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land C = A Y_{rm} B) \to ((A X_{rm} B \in ℕ_{0} \land A Y_{rm} 2 B (A Y_{rm} B) \in ℕ_{0} \land A X_{rm} 2 B (A Y_{rm} B) \in ℕ_{0}) \land (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℕ_{0} \land (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B \in ℕ_{0} \land (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B \in ℕ_{0}))$
15	14	simpld	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land C = A Y_{rm} B) \to (A X_{rm} B \in ℕ_{0} \land A Y_{rm} 2 B (A Y_{rm} B) \in ℕ_{0} \land A X_{rm} 2 B (A Y_{rm} B) \in ℕ_{0})$
16	14	simprd	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land C = A Y_{rm} B) \to (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℕ_{0} \land (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B \in ℕ_{0} \land (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B \in ℕ_{0})$
17	13	simprd	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land C = A Y_{rm} B) \to ((\frac{A Y_{rm} 2 B (A Y_{rm} B)}{2 C^{2}}) - 1 \in ℕ_{0} \land ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land ({((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B)}^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = ((\frac{A Y_{rm} 2 B (A Y_{rm} B)}{2 C^{2}}) - 1 + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))) \land ((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - C)) \land (2 C ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - B) \land B \leq C))))$
18		oveq1	$⊢ j = (\frac{A Y_{rm} 2 B (A Y_{rm} B)}{2 C^{2}}) - 1 \to j + 1 = (\frac{A Y_{rm} 2 B (A Y_{rm} B)}{2 C^{2}}) - 1 + 1$
19	18	oveq1d	$⊢ j = (\frac{A Y_{rm} 2 B (A Y_{rm} B)}{2 C^{2}}) - 1 \to (j + 1) 2 C^{2} = ((\frac{A Y_{rm} 2 B (A Y_{rm} B)}{2 C^{2}}) - 1 + 1) 2 C^{2}$
20	19	eqeq2d	$⊢ j = (\frac{A Y_{rm} 2 B (A Y_{rm} B)}{2 C^{2}}) - 1 \to (A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \leftrightarrow A Y_{rm} 2 B (A Y_{rm} B) = ((\frac{A Y_{rm} 2 B (A Y_{rm} B)}{2 C^{2}}) - 1 + 1) 2 C^{2})$
21	20	3anbi2d	$⊢ j = (\frac{A Y_{rm} 2 B (A Y_{rm} B)}{2 C^{2}}) - 1 \to (({((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B)}^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A)) \leftrightarrow ({((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B)}^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = ((\frac{A Y_{rm} 2 B (A Y_{rm} B)}{2 C^{2}}) - 1 + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A)))$
22	21	anbi2d	$⊢ j = (\frac{A Y_{rm} 2 B (A Y_{rm} B)}{2 C^{2}}) - 1 \to ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land ({((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B)}^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))) \leftrightarrow (({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land ({((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B)}^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = ((\frac{A Y_{rm} 2 B (A Y_{rm} B)}{2 C^{2}}) - 1 + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))))$
23	22	anbi1d	$⊢ j = (\frac{A Y_{rm} 2 B (A Y_{rm} B)}{2 C^{2}}) - 1 \to (((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land ({((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B)}^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))) \land ((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - C)) \land (2 C ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - B) \land B \leq C))) \leftrightarrow ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land ({((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B)}^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = ((\frac{A Y_{rm} 2 B (A Y_{rm} B)}{2 C^{2}}) - 1 + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))) \land ((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - C)) \land (2 C ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - B) \land B \leq C))))$
24	23	rspcev	$⊢ ((\frac{A Y_{rm} 2 B (A Y_{rm} B)}{2 C^{2}}) - 1 \in ℕ_{0} \land ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land ({((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B)}^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = ((\frac{A Y_{rm} 2 B (A Y_{rm} B)}{2 C^{2}}) - 1 + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))) \land ((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - C)) \land (2 C ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - B) \land B \leq C)))) \to \exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land ({((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B)}^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))) \land ((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - C)) \land (2 C ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - B) \land B \leq C)))$
25	17 24	syl	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land C = A Y_{rm} B) \to \exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land ({((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B)}^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))) \land ((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - C)) \land (2 C ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - B) \land B \leq C)))$
26		eleq1	$⊢ g = A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \to (g \in ℤ_{\geq 2} \leftrightarrow A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2})$
27	26	3anbi3d	$⊢ g = A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \to (({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}) \leftrightarrow ({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}))$
28		oveq1	$⊢ g = A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \to g^{2} = {(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2}$
29	28	oveq1d	$⊢ g = A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \to g^{2} - 1 = {(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1$
30	29	oveq1d	$⊢ g = A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \to (g^{2} - 1) h^{2} = ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) h^{2}$
31	30	oveq2d	$⊢ g = A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \to i^{2} - (g^{2} - 1) h^{2} = i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) h^{2}$
32	31	eqeq1d	$⊢ g = A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \to (i^{2} - (g^{2} - 1) h^{2} = 1 \leftrightarrow i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) h^{2} = 1)$
33		oveq1	$⊢ g = A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \to g - A = A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A$
34	33	breq2d	$⊢ g = A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \to ((A X_{rm} 2 B (A Y_{rm} B)) ∥ (g - A) \leftrightarrow (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))$
35	32 34	3anbi13d	$⊢ g = A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \to ((i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (g - A)) \leftrightarrow (i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A)))$
36	27 35	anbi12d	$⊢ g = A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \to ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (g - A))) \leftrightarrow (({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land (i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))))$
37		oveq1	$⊢ g = A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \to g - 1 = A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1$
38	37	breq2d	$⊢ g = A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \to (2 C ∥ (g - 1) \leftrightarrow 2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1))$
39	38	anbi1d	$⊢ g = A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \to ((2 C ∥ (g - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C)) \leftrightarrow (2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C)))$
40	39	anbi1d	$⊢ g = A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \to (((2 C ∥ (g - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)) \leftrightarrow ((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))$
41	36 40	anbi12d	$⊢ g = A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \to (((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (g - A))) \land ((2 C ∥ (g - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \leftrightarrow ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land (i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))) \land ((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))))$
42	41	rexbidv	$⊢ g = A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \to (\exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (g - A))) \land ((2 C ∥ (g - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \leftrightarrow \exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land (i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))) \land ((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))))$
43		oveq1	$⊢ h = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B \to h^{2} = {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2}$
44	43	oveq2d	$⊢ h = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B \to ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) h^{2} = ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2}$
45	44	oveq2d	$⊢ h = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B \to i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) h^{2} = i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2}$
46	45	eqeq1d	$⊢ h = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B \to (i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) h^{2} = 1 \leftrightarrow i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1)$
47	46	3anbi1d	$⊢ h = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B \to ((i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A)) \leftrightarrow (i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A)))$
48	47	anbi2d	$⊢ h = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B \to ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land (i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))) \leftrightarrow (({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land (i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))))$
49		oveq1	$⊢ h = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B \to h - C = ((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - C$
50	49	breq2d	$⊢ h = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B \to ((A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C) \leftrightarrow (A X_{rm} 2 B (A Y_{rm} B)) ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - C))$
51	50	anbi2d	$⊢ h = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B \to ((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C)) \leftrightarrow (2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - C)))$
52		oveq1	$⊢ h = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B \to h - B = ((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - B$
53	52	breq2d	$⊢ h = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B \to (2 C ∥ (h - B) \leftrightarrow 2 C ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - B))$
54	53	anbi1d	$⊢ h = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B \to ((2 C ∥ (h - B) \land B \leq C) \leftrightarrow (2 C ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - B) \land B \leq C))$
55	51 54	anbi12d	$⊢ h = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B \to (((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)) \leftrightarrow ((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - C)) \land (2 C ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - B) \land B \leq C)))$
56	48 55	anbi12d	$⊢ h = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B \to (((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land (i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))) \land ((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \leftrightarrow ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land (i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))) \land ((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - C)) \land (2 C ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - B) \land B \leq C))))$
57	56	rexbidv	$⊢ h = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B \to (\exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land (i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))) \land ((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \leftrightarrow \exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land (i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))) \land ((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - C)) \land (2 C ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - B) \land B \leq C))))$
58		oveq1	$⊢ i = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B \to i^{2} = {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B)}^{2}$
59	58	oveq1d	$⊢ i = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B \to i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B)}^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2}$
60	59	eqeq1d	$⊢ i = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B \to (i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \leftrightarrow {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B)}^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1)$
61	60	3anbi1d	$⊢ i = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B \to ((i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A)) \leftrightarrow ({((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B)}^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A)))$
62	61	anbi2d	$⊢ i = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B \to ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land (i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))) \leftrightarrow (({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land ({((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B)}^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))))$
63	62	anbi1d	$⊢ i = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B \to (((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land (i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))) \land ((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - C)) \land (2 C ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - B) \land B \leq C))) \leftrightarrow ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land ({((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B)}^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))) \land ((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - C)) \land (2 C ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - B) \land B \leq C))))$
64	63	rexbidv	$⊢ i = (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B \to (\exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land (i^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))) \land ((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - C)) \land (2 C ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - B) \land B \leq C))) \leftrightarrow \exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land ({((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B)}^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))) \land ((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - C)) \land (2 C ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - B) \land B \leq C))))$
65	42 57 64	rspc3ev	$⊢ ((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℕ_{0} \land (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B \in ℕ_{0} \land (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B \in ℕ_{0}) \land \exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) \in ℤ_{\geq 2}) \land ({((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) X_{rm} B)}^{2} - ({(A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A))}^{2} - 1) {((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B)}^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - A))) \land ((2 C ∥ (A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A) - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - C)) \land (2 C ∥ (((A + {(A X_{rm} 2 B (A Y_{rm} B))}^{2} ({(A X_{rm} 2 B (A Y_{rm} B))}^{2} - A)) Y_{rm} B) - B) \land B \leq C)))) \to \exists g \in ℕ_{0} \exists h \in ℕ_{0} \exists i \in ℕ_{0} \exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (g - A))) \land ((2 C ∥ (g - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))$
66	16 25 65	syl2anc	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land C = A Y_{rm} B) \to \exists g \in ℕ_{0} \exists h \in ℕ_{0} \exists i \in ℕ_{0} \exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (g - A))) \land ((2 C ∥ (g - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))$
67		oveq1	$⊢ d = A X_{rm} B \to d^{2} = {(A X_{rm} B)}^{2}$
68	67	oveq1d	$⊢ d = A X_{rm} B \to d^{2} - (A^{2} - 1) C^{2} = {(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2}$
69	68	eqeq1d	$⊢ d = A X_{rm} B \to (d^{2} - (A^{2} - 1) C^{2} = 1 \leftrightarrow {(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1)$
70	69	3anbi1d	$⊢ d = A X_{rm} B \to ((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \leftrightarrow ({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}))$
71	70	anbi1d	$⊢ d = A X_{rm} B \to (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \leftrightarrow (({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))))$
72	71	anbi1d	$⊢ d = A X_{rm} B \to ((((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \leftrightarrow ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))))$
73	72	2rexbidv	$⊢ d = A X_{rm} B \to (\exists i \in ℕ_{0} \exists j \in ℕ_{0} (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \leftrightarrow \exists i \in ℕ_{0} \exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))))$
74	73	2rexbidv	$⊢ d = A X_{rm} B \to (\exists g \in ℕ_{0} \exists h \in ℕ_{0} \exists i \in ℕ_{0} \exists j \in ℕ_{0} (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \leftrightarrow \exists g \in ℕ_{0} \exists h \in ℕ_{0} \exists i \in ℕ_{0} \exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))))$
75		oveq1	$⊢ e = A Y_{rm} 2 B (A Y_{rm} B) \to e^{2} = {(A Y_{rm} 2 B (A Y_{rm} B))}^{2}$
76	75	oveq2d	$⊢ e = A Y_{rm} 2 B (A Y_{rm} B) \to (A^{2} - 1) e^{2} = (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2}$
77	76	oveq2d	$⊢ e = A Y_{rm} 2 B (A Y_{rm} B) \to f^{2} - (A^{2} - 1) e^{2} = f^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2}$
78	77	eqeq1d	$⊢ e = A Y_{rm} 2 B (A Y_{rm} B) \to (f^{2} - (A^{2} - 1) e^{2} = 1 \leftrightarrow f^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1)$
79	78	3anbi2d	$⊢ e = A Y_{rm} 2 B (A Y_{rm} B) \to (({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \leftrightarrow ({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}))$
80		eqeq1	$⊢ e = A Y_{rm} 2 B (A Y_{rm} B) \to (e = (j + 1) 2 C^{2} \leftrightarrow A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2})$
81	80	3anbi2d	$⊢ e = A Y_{rm} 2 B (A Y_{rm} B) \to ((i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A)) \leftrightarrow (i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land f ∥ (g - A)))$
82	79 81	anbi12d	$⊢ e = A Y_{rm} 2 B (A Y_{rm} B) \to ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \leftrightarrow (({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land f ∥ (g - A))))$
83	82	anbi1d	$⊢ e = A Y_{rm} 2 B (A Y_{rm} B) \to (((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \leftrightarrow ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))))$
84	83	2rexbidv	$⊢ e = A Y_{rm} 2 B (A Y_{rm} B) \to (\exists i \in ℕ_{0} \exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \leftrightarrow \exists i \in ℕ_{0} \exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))))$
85	84	2rexbidv	$⊢ e = A Y_{rm} 2 B (A Y_{rm} B) \to (\exists g \in ℕ_{0} \exists h \in ℕ_{0} \exists i \in ℕ_{0} \exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \leftrightarrow \exists g \in ℕ_{0} \exists h \in ℕ_{0} \exists i \in ℕ_{0} \exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))))$
86		oveq1	$⊢ f = A X_{rm} 2 B (A Y_{rm} B) \to f^{2} = {(A X_{rm} 2 B (A Y_{rm} B))}^{2}$
87	86	oveq1d	$⊢ f = A X_{rm} 2 B (A Y_{rm} B) \to f^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2}$
88	87	eqeq1d	$⊢ f = A X_{rm} 2 B (A Y_{rm} B) \to (f^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \leftrightarrow {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1)$
89	88	3anbi2d	$⊢ f = A X_{rm} 2 B (A Y_{rm} B) \to (({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}) \leftrightarrow ({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}))$
90		breq1	$⊢ f = A X_{rm} 2 B (A Y_{rm} B) \to (f ∥ (g - A) \leftrightarrow (A X_{rm} 2 B (A Y_{rm} B)) ∥ (g - A))$
91	90	3anbi3d	$⊢ f = A X_{rm} 2 B (A Y_{rm} B) \to ((i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land f ∥ (g - A)) \leftrightarrow (i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (g - A)))$
92	89 91	anbi12d	$⊢ f = A X_{rm} 2 B (A Y_{rm} B) \to ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land f ∥ (g - A))) \leftrightarrow (({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (g - A))))$
93		breq1	$⊢ f = A X_{rm} 2 B (A Y_{rm} B) \to (f ∥ (h - C) \leftrightarrow (A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C))$
94	93	anbi2d	$⊢ f = A X_{rm} 2 B (A Y_{rm} B) \to ((2 C ∥ (g - 1) \land f ∥ (h - C)) \leftrightarrow (2 C ∥ (g - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C)))$
95	94	anbi1d	$⊢ f = A X_{rm} 2 B (A Y_{rm} B) \to (((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)) \leftrightarrow ((2 C ∥ (g - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))$
96	92 95	anbi12d	$⊢ f = A X_{rm} 2 B (A Y_{rm} B) \to (((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \leftrightarrow ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (g - A))) \land ((2 C ∥ (g - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))))$
97	96	2rexbidv	$⊢ f = A X_{rm} 2 B (A Y_{rm} B) \to (\exists i \in ℕ_{0} \exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \leftrightarrow \exists i \in ℕ_{0} \exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (g - A))) \land ((2 C ∥ (g - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))))$
98	97	2rexbidv	$⊢ f = A X_{rm} 2 B (A Y_{rm} B) \to (\exists g \in ℕ_{0} \exists h \in ℕ_{0} \exists i \in ℕ_{0} \exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \leftrightarrow \exists g \in ℕ_{0} \exists h \in ℕ_{0} \exists i \in ℕ_{0} \exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (g - A))) \land ((2 C ∥ (g - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))))$
99	74 85 98	rspc3ev	$⊢ ((A X_{rm} B \in ℕ_{0} \land A Y_{rm} 2 B (A Y_{rm} B) \in ℕ_{0} \land A X_{rm} 2 B (A Y_{rm} B) \in ℕ_{0}) \land \exists g \in ℕ_{0} \exists h \in ℕ_{0} \exists i \in ℕ_{0} \exists j \in ℕ_{0} ((({(A X_{rm} B)}^{2} - (A^{2} - 1) C^{2} = 1 \land {(A X_{rm} 2 B (A Y_{rm} B))}^{2} - (A^{2} - 1) {(A Y_{rm} 2 B (A Y_{rm} B))}^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land A Y_{rm} 2 B (A Y_{rm} B) = (j + 1) 2 C^{2} \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (g - A))) \land ((2 C ∥ (g - 1) \land (A X_{rm} 2 B (A Y_{rm} B)) ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} \exists i \in ℕ_{0} \exists j \in ℕ_{0} (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))$
100	15 66 99	syl2anc	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land C = A Y_{rm} B) \to \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} \exists i \in ℕ_{0} \exists j \in ℕ_{0} (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))$
101	100	ex	$⊢ (A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \to (C = A Y_{rm} B \to \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} \exists i \in ℕ_{0} \exists j \in ℕ_{0} (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))))$
102		simpll1	$⊢ (((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \to A \in ℤ_{\geq 2}$
103	102	ad3antrrr	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to A \in ℤ_{\geq 2}$
104		simpll2	$⊢ (((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \to B \in ℕ$
105	104	ad3antrrr	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to B \in ℕ$
106		simpll3	$⊢ (((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \to C \in ℕ$
107	106	ad3antrrr	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to C \in ℕ$
108		simplrl	$⊢ (((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \to d \in ℕ_{0}$
109	108	ad3antrrr	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to d \in ℕ_{0}$
110		simplrr	$⊢ (((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \to e \in ℕ_{0}$
111	110	ad3antrrr	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to e \in ℕ_{0}$
112		simprl	$⊢ (((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \to f \in ℕ_{0}$
113	112	ad3antrrr	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to f \in ℕ_{0}$
114		simprr	$⊢ (((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \to g \in ℕ_{0}$
115	114	ad3antrrr	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to g \in ℕ_{0}$
116		simprl	$⊢ ((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \to h \in ℕ_{0}$
117	116	ad2antrr	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to h \in ℕ_{0}$
118		simprr	$⊢ ((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \to i \in ℕ_{0}$
119	118	ad2antrr	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to i \in ℕ_{0}$
120		simplr	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to j \in ℕ_{0}$
121		simp2l1	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land ((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \to d^{2} - (A^{2} - 1) C^{2} = 1$
122	121	3expb	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to d^{2} - (A^{2} - 1) C^{2} = 1$
123		simp2l2	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land ((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \to f^{2} - (A^{2} - 1) e^{2} = 1$
124	123	3expb	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to f^{2} - (A^{2} - 1) e^{2} = 1$
125		simp2l3	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land ((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \to g \in ℤ_{\geq 2}$
126	125	3expb	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to g \in ℤ_{\geq 2}$
127		simp2r1	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land ((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \to i^{2} - (g^{2} - 1) h^{2} = 1$
128	127	3expb	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to i^{2} - (g^{2} - 1) h^{2} = 1$
129		simp2r2	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land ((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \to e = (j + 1) 2 C^{2}$
130	129	3expb	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to e = (j + 1) 2 C^{2}$
131		simp2r3	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land ((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \to f ∥ (g - A)$
132	131	3expb	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to f ∥ (g - A)$
133		simp3ll	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land ((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \to 2 C ∥ (g - 1)$
134	133	3expb	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to 2 C ∥ (g - 1)$
135		simp3lr	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land ((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \to f ∥ (h - C)$
136	135	3expb	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to f ∥ (h - C)$
137		simp3rl	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land ((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \to 2 C ∥ (h - B)$
138	137	3expb	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to 2 C ∥ (h - B)$
139		simp3rr	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land ((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \to B \leq C$
140	139	3expb	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to B \leq C$
141	103 105 107 109 111 113 115 117 119 120 122 124 126 128 130 132 134 136 138 140	jm2.27b	$⊢ ((((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \land j \in ℕ_{0}) \land (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C)))) \to C = A Y_{rm} B$
142	141	rexlimdva2	$⊢ ((((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \land (h \in ℕ_{0} \land i \in ℕ_{0})) \to (\exists j \in ℕ_{0} (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \to C = A Y_{rm} B)$
143	142	rexlimdvva	$⊢ (((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \land (f \in ℕ_{0} \land g \in ℕ_{0})) \to (\exists h \in ℕ_{0} \exists i \in ℕ_{0} \exists j \in ℕ_{0} (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \to C = A Y_{rm} B)$
144	143	rexlimdvva	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \land (d \in ℕ_{0} \land e \in ℕ_{0})) \to (\exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} \exists i \in ℕ_{0} \exists j \in ℕ_{0} (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \to C = A Y_{rm} B)$
145	144	rexlimdvva	$⊢ (A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \to (\exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} \exists i \in ℕ_{0} \exists j \in ℕ_{0} (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))) \to C = A Y_{rm} B)$
146	101 145	impbid	$⊢ (A \in ℤ_{\geq 2} \land B \in ℕ \land C \in ℕ) \to (C = A Y_{rm} B \leftrightarrow \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} \exists i \in ℕ_{0} \exists j \in ℕ_{0} (((d^{2} - (A^{2} - 1) C^{2} = 1 \land f^{2} - (A^{2} - 1) e^{2} = 1 \land g \in ℤ_{\geq 2}) \land (i^{2} - (g^{2} - 1) h^{2} = 1 \land e = (j + 1) 2 C^{2} \land f ∥ (g - A))) \land ((2 C ∥ (g - 1) \land f ∥ (h - C)) \land (2 C ∥ (h - B) \land B \leq C))))$

Metamath Proof Explorer

Theorem jm2.27

Proof