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	⊢ ( 𝜑 → 𝐴 ∈ ( ℤ_≥ ‘ 2 ) )
	jm2.27a2	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
	jm2.27a3	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
	jm2.27a4	⊢ ( 𝜑 → 𝐷 ∈ ℕ₀ )
	jm2.27a5	⊢ ( 𝜑 → 𝐸 ∈ ℕ₀ )
	jm2.27a6	⊢ ( 𝜑 → 𝐹 ∈ ℕ₀ )
	jm2.27a7	⊢ ( 𝜑 → 𝐺 ∈ ℕ₀ )
	jm2.27a8	⊢ ( 𝜑 → 𝐻 ∈ ℕ₀ )
	jm2.27a9	⊢ ( 𝜑 → 𝐼 ∈ ℕ₀ )
	jm2.27a10	⊢ ( 𝜑 → 𝐽 ∈ ℕ₀ )
	jm2.27a11	⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐶 ↑ 2 ) ) ) = 1 )
	jm2.27a12	⊢ ( 𝜑 → ( ( 𝐹 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) ) = 1 )
	jm2.27a13	⊢ ( 𝜑 → 𝐺 ∈ ( ℤ_≥ ‘ 2 ) )
	jm2.27a14	⊢ ( 𝜑 → ( ( 𝐼 ↑ 2 ) − ( ( ( 𝐺 ↑ 2 ) − 1 ) · ( 𝐻 ↑ 2 ) ) ) = 1 )
	jm2.27a15	⊢ ( 𝜑 → 𝐸 = ( ( 𝐽 + 1 ) · ( 2 · ( 𝐶 ↑ 2 ) ) ) )
	jm2.27a16	⊢ ( 𝜑 → 𝐹 ∥ ( 𝐺 − 𝐴 ) )
	jm2.27a17	⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ ( 𝐺 − 1 ) )
	jm2.27a18	⊢ ( 𝜑 → 𝐹 ∥ ( 𝐻 − 𝐶 ) )
	jm2.27a19	⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ ( 𝐻 − 𝐵 ) )
	jm2.27a20	⊢ ( 𝜑 → 𝐵 ≤ 𝐶 )
Assertion	jm2.27b	⊢ ( 𝜑 → 𝐶 = ( 𝐴 Y_rm 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		jm2.27a1	⊢ ( 𝜑 → 𝐴 ∈ ( ℤ_≥ ‘ 2 ) )
2		jm2.27a2	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3		jm2.27a3	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4		jm2.27a4	⊢ ( 𝜑 → 𝐷 ∈ ℕ₀ )
5		jm2.27a5	⊢ ( 𝜑 → 𝐸 ∈ ℕ₀ )
6		jm2.27a6	⊢ ( 𝜑 → 𝐹 ∈ ℕ₀ )
7		jm2.27a7	⊢ ( 𝜑 → 𝐺 ∈ ℕ₀ )
8		jm2.27a8	⊢ ( 𝜑 → 𝐻 ∈ ℕ₀ )
9		jm2.27a9	⊢ ( 𝜑 → 𝐼 ∈ ℕ₀ )
10		jm2.27a10	⊢ ( 𝜑 → 𝐽 ∈ ℕ₀ )
11		jm2.27a11	⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐶 ↑ 2 ) ) ) = 1 )
12		jm2.27a12	⊢ ( 𝜑 → ( ( 𝐹 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) ) = 1 )
13		jm2.27a13	⊢ ( 𝜑 → 𝐺 ∈ ( ℤ_≥ ‘ 2 ) )
14		jm2.27a14	⊢ ( 𝜑 → ( ( 𝐼 ↑ 2 ) − ( ( ( 𝐺 ↑ 2 ) − 1 ) · ( 𝐻 ↑ 2 ) ) ) = 1 )
15		jm2.27a15	⊢ ( 𝜑 → 𝐸 = ( ( 𝐽 + 1 ) · ( 2 · ( 𝐶 ↑ 2 ) ) ) )
16		jm2.27a16	⊢ ( 𝜑 → 𝐹 ∥ ( 𝐺 − 𝐴 ) )
17		jm2.27a17	⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ ( 𝐺 − 1 ) )
18		jm2.27a18	⊢ ( 𝜑 → 𝐹 ∥ ( 𝐻 − 𝐶 ) )
19		jm2.27a19	⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ ( 𝐻 − 𝐵 ) )
20		jm2.27a20	⊢ ( 𝜑 → 𝐵 ≤ 𝐶 )
21	3	nnzd	⊢ ( 𝜑 → 𝐶 ∈ ℤ )
22		rmxycomplete	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝐷 ∈ ℕ₀ ∧ 𝐶 ∈ ℤ ) → ( ( ( 𝐷 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐶 ↑ 2 ) ) ) = 1 ↔ ∃ 𝑝 ∈ ℤ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) )
23	1 4 21 22	syl3anc	⊢ ( 𝜑 → ( ( ( 𝐷 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐶 ↑ 2 ) ) ) = 1 ↔ ∃ 𝑝 ∈ ℤ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) )
24	11 23	mpbid	⊢ ( 𝜑 → ∃ 𝑝 ∈ ℤ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) )
25	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) → ( ( 𝐹 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) ) = 1 )
26	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) → 𝐴 ∈ ( ℤ_≥ ‘ 2 ) )
27	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) → 𝐹 ∈ ℕ₀ )
28	5	nn0zd	⊢ ( 𝜑 → 𝐸 ∈ ℤ )
29	28	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) → 𝐸 ∈ ℤ )
30		rmxycomplete	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝐹 ∈ ℕ₀ ∧ 𝐸 ∈ ℤ ) → ( ( ( 𝐹 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) ) = 1 ↔ ∃ 𝑞 ∈ ℤ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) )
31	26 27 29 30	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) → ( ( ( 𝐹 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) ) = 1 ↔ ∃ 𝑞 ∈ ℤ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) )
32	25 31	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) → ∃ 𝑞 ∈ ℤ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) )
33	14	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) → ( ( 𝐼 ↑ 2 ) − ( ( ( 𝐺 ↑ 2 ) − 1 ) · ( 𝐻 ↑ 2 ) ) ) = 1 )
34	13	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) → 𝐺 ∈ ( ℤ_≥ ‘ 2 ) )
35	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) → 𝐼 ∈ ℕ₀ )
36	8	nn0zd	⊢ ( 𝜑 → 𝐻 ∈ ℤ )
37	36	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) → 𝐻 ∈ ℤ )
38		rmxycomplete	⊢ ( ( 𝐺 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝐼 ∈ ℕ₀ ∧ 𝐻 ∈ ℤ ) → ( ( ( 𝐼 ↑ 2 ) − ( ( ( 𝐺 ↑ 2 ) − 1 ) · ( 𝐻 ↑ 2 ) ) ) = 1 ↔ ∃ 𝑟 ∈ ℤ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) )
39	34 35 37 38	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) → ( ( ( 𝐼 ↑ 2 ) − ( ( ( 𝐺 ↑ 2 ) − 1 ) · ( 𝐻 ↑ 2 ) ) ) = 1 ↔ ∃ 𝑟 ∈ ℤ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) )
40	33 39	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) → ∃ 𝑟 ∈ ℤ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) )
41	1	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐴 ∈ ( ℤ_≥ ‘ 2 ) )
42	2	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐵 ∈ ℕ )
43	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐶 ∈ ℕ )
44	4	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐷 ∈ ℕ₀ )
45	5	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐸 ∈ ℕ₀ )
46	6	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐹 ∈ ℕ₀ )
47	7	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐺 ∈ ℕ₀ )
48	8	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐻 ∈ ℕ₀ )
49	9	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐼 ∈ ℕ₀ )
50	10	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐽 ∈ ℕ₀ )
51	11	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → ( ( 𝐷 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐶 ↑ 2 ) ) ) = 1 )
52	12	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → ( ( 𝐹 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) ) = 1 )
53	13	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐺 ∈ ( ℤ_≥ ‘ 2 ) )
54	14	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → ( ( 𝐼 ↑ 2 ) − ( ( ( 𝐺 ↑ 2 ) − 1 ) · ( 𝐻 ↑ 2 ) ) ) = 1 )
55	15	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐸 = ( ( 𝐽 + 1 ) · ( 2 · ( 𝐶 ↑ 2 ) ) ) )
56	16	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐹 ∥ ( 𝐺 − 𝐴 ) )
57	17	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → ( 2 · 𝐶 ) ∥ ( 𝐺 − 1 ) )
58	18	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐹 ∥ ( 𝐻 − 𝐶 ) )
59	19	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → ( 2 · 𝐶 ) ∥ ( 𝐻 − 𝐵 ) )
60	20	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐵 ≤ 𝐶 )
61		simprl	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) → 𝑝 ∈ ℤ )
62	61	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝑝 ∈ ℤ )
63		simprrl	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) → 𝐷 = ( 𝐴 X_rm 𝑝 ) )
64	63	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐷 = ( 𝐴 X_rm 𝑝 ) )
65		simprrr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) → 𝐶 = ( 𝐴 Y_rm 𝑝 ) )
66	65	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐶 = ( 𝐴 Y_rm 𝑝 ) )
67		simplrl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝑞 ∈ ℤ )
68		simprl	⊢ ( ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) → 𝐹 = ( 𝐴 X_rm 𝑞 ) )
69	68	ad2antlr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐹 = ( 𝐴 X_rm 𝑞 ) )
70		simprr	⊢ ( ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) → 𝐸 = ( 𝐴 Y_rm 𝑞 ) )
71	70	ad2antlr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐸 = ( 𝐴 Y_rm 𝑞 ) )
72		simprl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝑟 ∈ ℤ )
73		simprrl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐼 = ( 𝐺 X_rm 𝑟 ) )
74		simprrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐻 = ( 𝐺 Y_rm 𝑟 ) )
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	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) ∧ ( 𝑟 ∈ ℤ ∧ ( 𝐼 = ( 𝐺 X_rm 𝑟 ) ∧ 𝐻 = ( 𝐺 Y_rm 𝑟 ) ) ) ) → 𝐶 = ( 𝐴 Y_rm 𝐵 ) )
76	40 75	rexlimddv	⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) ∧ ( 𝑞 ∈ ℤ ∧ ( 𝐹 = ( 𝐴 X_rm 𝑞 ) ∧ 𝐸 = ( 𝐴 Y_rm 𝑞 ) ) ) ) → 𝐶 = ( 𝐴 Y_rm 𝐵 ) )
77	32 76	rexlimddv	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℤ ∧ ( 𝐷 = ( 𝐴 X_rm 𝑝 ) ∧ 𝐶 = ( 𝐴 Y_rm 𝑝 ) ) ) ) → 𝐶 = ( 𝐴 Y_rm 𝐵 ) )
78	24 77	rexlimddv	⊢ ( 𝜑 → 𝐶 = ( 𝐴 Y_rm 𝐵 ) )

Metamath Proof Explorer

Theorem jm2.27b

Proof