jm2.27b

Description: Lemma for jm2.27 . Expand existential quantifiers for reverse direction. (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$
Assertion	jm2.27b	$⊢ φ \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	3	nnzd	$⊢ φ \to C \in ℤ$
22		rmxycomplete	$⊢ (A \in ℤ_{\geq 2} \land D \in ℕ_{0} \land C \in ℤ) \to (D^{2} - (A^{2} - 1) C^{2} = 1 \leftrightarrow \exists p \in ℤ (D = A X_{rm} p \land C = A Y_{rm} p))$
23	1 4 21 22	syl3anc	$⊢ φ \to (D^{2} - (A^{2} - 1) C^{2} = 1 \leftrightarrow \exists p \in ℤ (D = A X_{rm} p \land C = A Y_{rm} p))$
24	11 23	mpbid	$⊢ φ \to \exists p \in ℤ (D = A X_{rm} p \land C = A Y_{rm} p)$
25	12	adantr	$⊢ (φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \to F^{2} - (A^{2} - 1) E^{2} = 1$
26	1	adantr	$⊢ (φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \to A \in ℤ_{\geq 2}$
27	6	adantr	$⊢ (φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \to F \in ℕ_{0}$
28	5	nn0zd	$⊢ φ \to E \in ℤ$
29	28	adantr	$⊢ (φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \to E \in ℤ$
30		rmxycomplete	$⊢ (A \in ℤ_{\geq 2} \land F \in ℕ_{0} \land E \in ℤ) \to (F^{2} - (A^{2} - 1) E^{2} = 1 \leftrightarrow \exists q \in ℤ (F = A X_{rm} q \land E = A Y_{rm} q))$
31	26 27 29 30	syl3anc	$⊢ (φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \to (F^{2} - (A^{2} - 1) E^{2} = 1 \leftrightarrow \exists q \in ℤ (F = A X_{rm} q \land E = A Y_{rm} q))$
32	25 31	mpbid	$⊢ (φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \to \exists q \in ℤ (F = A X_{rm} q \land E = A Y_{rm} q)$
33	14	ad2antrr	$⊢ ((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \to I^{2} - (G^{2} - 1) H^{2} = 1$
34	13	ad2antrr	$⊢ ((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \to G \in ℤ_{\geq 2}$
35	9	ad2antrr	$⊢ ((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \to I \in ℕ_{0}$
36	8	nn0zd	$⊢ φ \to H \in ℤ$
37	36	ad2antrr	$⊢ ((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \to H \in ℤ$
38		rmxycomplete	$⊢ (G \in ℤ_{\geq 2} \land I \in ℕ_{0} \land H \in ℤ) \to (I^{2} - (G^{2} - 1) H^{2} = 1 \leftrightarrow \exists r \in ℤ (I = G X_{rm} r \land H = G Y_{rm} r))$
39	34 35 37 38	syl3anc	$⊢ ((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \to (I^{2} - (G^{2} - 1) H^{2} = 1 \leftrightarrow \exists r \in ℤ (I = G X_{rm} r \land H = G Y_{rm} r))$
40	33 39	mpbid	$⊢ ((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \to \exists r \in ℤ (I = G X_{rm} r \land H = G Y_{rm} r)$
41	1	ad3antrrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to A \in ℤ_{\geq 2}$
42	2	ad3antrrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to B \in ℕ$
43	3	ad3antrrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to C \in ℕ$
44	4	ad3antrrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to D \in ℕ_{0}$
45	5	ad3antrrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to E \in ℕ_{0}$
46	6	ad3antrrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to F \in ℕ_{0}$
47	7	ad3antrrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to G \in ℕ_{0}$
48	8	ad3antrrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to H \in ℕ_{0}$
49	9	ad3antrrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to I \in ℕ_{0}$
50	10	ad3antrrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to J \in ℕ_{0}$
51	11	ad3antrrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to D^{2} - (A^{2} - 1) C^{2} = 1$
52	12	ad3antrrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to F^{2} - (A^{2} - 1) E^{2} = 1$
53	13	ad3antrrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to G \in ℤ_{\geq 2}$
54	14	ad3antrrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to I^{2} - (G^{2} - 1) H^{2} = 1$
55	15	ad3antrrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to E = (J + 1) 2 C^{2}$
56	16	ad3antrrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to F ∥ (G - A)$
57	17	ad3antrrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to 2 C ∥ (G - 1)$
58	18	ad3antrrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to F ∥ (H - C)$
59	19	ad3antrrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to 2 C ∥ (H - B)$
60	20	ad3antrrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to B \leq C$
61		simprl	$⊢ (φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \to p \in ℤ$
62	61	ad2antrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to p \in ℤ$
63		simprrl	$⊢ (φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \to D = A X_{rm} p$
64	63	ad2antrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to D = A X_{rm} p$
65		simprrr	$⊢ (φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \to C = A Y_{rm} p$
66	65	ad2antrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to C = A Y_{rm} p$
67		simplrl	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to q \in ℤ$
68		simprl	$⊢ (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q)) \to F = A X_{rm} q$
69	68	ad2antlr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to F = A X_{rm} q$
70		simprr	$⊢ (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q)) \to E = A Y_{rm} q$
71	70	ad2antlr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to E = A Y_{rm} q$
72		simprl	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to r \in ℤ$
73		simprrl	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to I = G X_{rm} r$
74		simprrr	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to H = G Y_{rm} r$
75	41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 62 64 66 67 69 71 72 73 74	jm2.27a	$⊢ (((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \land (r \in ℤ \land (I = G X_{rm} r \land H = G Y_{rm} r))) \to C = A Y_{rm} B$
76	40 75	rexlimddv	$⊢ ((φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \land (q \in ℤ \land (F = A X_{rm} q \land E = A Y_{rm} q))) \to C = A Y_{rm} B$
77	32 76	rexlimddv	$⊢ (φ \land (p \in ℤ \land (D = A X_{rm} p \land C = A Y_{rm} p))) \to C = A Y_{rm} B$
78	24 77	rexlimddv	$⊢ φ \to C = A Y_{rm} B$

Metamath Proof Explorer

Theorem jm2.27b

Proof