Theorem rmydioph 42997

Description: jm2.27 42991 restated in terms of Diophantine sets. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)

Assertion

Ref	Expression
rmydioph	⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} ∈ (Dioph‘3)

Proof of Theorem rmydioph

Dummy variables 𝑏 𝑐 𝑑 𝑒 𝑓 𝑔 ℎ 𝑖 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elmapi 8776	. . . . . . 7 ⊢ (𝑎 ∈ (ℕ0 ↑m (1...3)) → 𝑎:(1...3)⟶ℕ0)
2		2nn 12201	. . . . . . . . 9 ⊢ 2 ∈ ℕ
3	2	jm2.27dlem3 42994	. . . . . . . 8 ⊢ 2 ∈ (1...2)
4		df-3 12192	. . . . . . . 8 ⊢ 3 = (2 + 1)
5	3, 4, 2	jm2.27dlem2 42993	. . . . . . 7 ⊢ 2 ∈ (1...3)
6		ffvelcdm 7015	. . . . . . 7 ⊢ ((𝑎:(1...3)⟶ℕ0 ∧ 2 ∈ (1...3)) → (𝑎‘2) ∈ ℕ0)
7	1, 5, 6	sylancl 586	. . . . . 6 ⊢ (𝑎 ∈ (ℕ0 ↑m (1...3)) → (𝑎‘2) ∈ ℕ0)
8		elnn0 12386	. . . . . 6 ⊢ ((𝑎‘2) ∈ ℕ0 ↔ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0))
9	7, 8	sylib 218	. . . . 5 ⊢ (𝑎 ∈ (ℕ0 ↑m (1...3)) → ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0))
10		iba 527	. . . . . . 7 ⊢ (((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0))))
11		andi 1009	. . . . . . 7 ⊢ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0)) ↔ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0)))
12	10, 11	bitrdi 287	. . . . . 6 ⊢ (((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0))))
13	12	anbi2d 630	. . . . 5 ⊢ (((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0) → (((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2))) ↔ ((𝑎‘1) ∈ (ℤ≥‘2) ∧ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0)))))
14	9, 13	syl 17	. . . 4 ⊢ (𝑎 ∈ (ℕ0 ↑m (1...3)) → (((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2))) ↔ ((𝑎‘1) ∈ (ℤ≥‘2) ∧ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0)))))
15		simplr 768	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → (𝑎‘1) ∈ (ℤ≥‘2))
16		nnz 12492	. . . . . . . . . . . . . 14 ⊢ ((𝑎‘2) ∈ ℕ → (𝑎‘2) ∈ ℤ)
17	16	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → (𝑎‘2) ∈ ℤ)
18		frmy 42897	. . . . . . . . . . . . . 14 ⊢ Yrm :((ℤ≥‘2) × ℤ)⟶ℤ
19	18	fovcl 7477	. . . . . . . . . . . . 13 ⊢ (((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘2) ∈ ℤ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℤ)
20	15, 17, 19	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℤ)
21		rmy0 42912	. . . . . . . . . . . . . 14 ⊢ ((𝑎‘1) ∈ (ℤ≥‘2) → ((𝑎‘1) Yrm 0) = 0)
22	21	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm 0) = 0)
23		nngt0 12159	. . . . . . . . . . . . . . 15 ⊢ ((𝑎‘2) ∈ ℕ → 0 < (𝑎‘2))
24	23	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 < (𝑎‘2))
25		0zd 12483	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 ∈ ℤ)
26		ltrmy 42935	. . . . . . . . . . . . . . 15 ⊢ (((𝑎‘1) ∈ (ℤ≥‘2) ∧ 0 ∈ ℤ ∧ (𝑎‘2) ∈ ℤ) → (0 < (𝑎‘2) ↔ ((𝑎‘1) Yrm 0) < ((𝑎‘1) Yrm (𝑎‘2))))
27	15, 25, 17, 26	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → (0 < (𝑎‘2) ↔ ((𝑎‘1) Yrm 0) < ((𝑎‘1) Yrm (𝑎‘2))))
28	24, 27	mpbid 232	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm 0) < ((𝑎‘1) Yrm (𝑎‘2)))
29	22, 28	eqbrtrrd 5116	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 < ((𝑎‘1) Yrm (𝑎‘2)))
30		elnnz 12481	. . . . . . . . . . . 12 ⊢ (((𝑎‘1) Yrm (𝑎‘2)) ∈ ℕ ↔ (((𝑎‘1) Yrm (𝑎‘2)) ∈ ℤ ∧ 0 < ((𝑎‘1) Yrm (𝑎‘2))))
31	20, 29, 30	sylanbrc 583	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℕ)
32		eleq1 2816	. . . . . . . . . . 11 ⊢ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) → ((𝑎‘3) ∈ ℕ ↔ ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℕ))
33	31, 32	syl5ibrcom 247	. . . . . . . . . 10 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) → (𝑎‘3) ∈ ℕ))
34	33	pm4.71rd 562	. . . . . . . . 9 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ((𝑎‘3) ∈ ℕ ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))))
35		simpllr 775	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) → (𝑎‘1) ∈ (ℤ≥‘2))
36		simplr 768	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) → (𝑎‘2) ∈ ℕ)
37		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) → (𝑎‘3) ∈ ℕ)
38		jm2.27 42991	. . . . . . . . . . 11 ⊢ (((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ ∧ (𝑎‘3) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))))
39	35, 36, 37, 38	syl3anc 1373	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))))
40	39	pm5.32da 579	. . . . . . . . 9 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → (((𝑎‘3) ∈ ℕ ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2))) ↔ ((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))))
41	34, 40	bitrd 279	. . . . . . . 8 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))))
42	41	ex 412	. . . . . . 7 ⊢ ((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) → ((𝑎‘2) ∈ ℕ → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))))))
43	42	pm5.32rd 578	. . . . . 6 ⊢ ((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) → (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ↔ (((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ)))
44		oveq2 7357	. . . . . . . . . . 11 ⊢ ((𝑎‘2) = 0 → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑎‘1) Yrm 0))
45	44	adantl 481	. . . . . . . . . 10 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑎‘1) Yrm 0))
46	21	ad2antlr 727	. . . . . . . . . 10 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm 0) = 0)
47	45, 46	eqtrd 2764	. . . . . . . . 9 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm (𝑎‘2)) = 0)
48	47	eqeq2d 2740	. . . . . . . 8 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (𝑎‘3) = 0))
49	48	ex 412	. . . . . . 7 ⊢ ((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) → ((𝑎‘2) = 0 → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (𝑎‘3) = 0)))
50	49	pm5.32rd 578	. . . . . 6 ⊢ ((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) → (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0) ↔ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)))
51	43, 50	orbi12d 918	. . . . 5 ⊢ ((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) → ((((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0)) ↔ ((((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0))))
52	51	pm5.32da 579	. . . 4 ⊢ (𝑎 ∈ (ℕ0 ↑m (1...3)) → (((𝑎‘1) ∈ (ℤ≥‘2) ∧ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0))) ↔ ((𝑎‘1) ∈ (ℤ≥‘2) ∧ ((((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)))))
53	14, 52	bitrd 279	. . 3 ⊢ (𝑎 ∈ (ℕ0 ↑m (1...3)) → (((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2))) ↔ ((𝑎‘1) ∈ (ℤ≥‘2) ∧ ((((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)))))
54	53	rabbiia 3398	. 2 ⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} = {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ((𝑎‘1) ∈ (ℤ≥‘2) ∧ ((((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)))}
55		3nn0 12402	. . . 4 ⊢ 3 ∈ ℕ0
56		2z 12507	. . . 4 ⊢ 2 ∈ ℤ
57		ovex 7382	. . . . 5 ⊢ (1...3) ∈ V
58		1nn 12139	. . . . . . . 8 ⊢ 1 ∈ ℕ
59	58	jm2.27dlem3 42994	. . . . . . 7 ⊢ 1 ∈ (1...1)
60		df-2 12191	. . . . . . 7 ⊢ 2 = (1 + 1)
61	59, 60, 58	jm2.27dlem2 42993	. . . . . 6 ⊢ 1 ∈ (1...2)
62	61, 4, 2	jm2.27dlem2 42993	. . . . 5 ⊢ 1 ∈ (1...3)
63		mzpproj 42720	. . . . 5 ⊢ (((1...3) ∈ V ∧ 1 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑m (1...3)) ↦ (𝑎‘1)) ∈ (mzPoly‘(1...3)))
64	57, 62, 63	mp2an 692	. . . 4 ⊢ (𝑎 ∈ (ℤ ↑m (1...3)) ↦ (𝑎‘1)) ∈ (mzPoly‘(1...3))
65		eluzrabdioph 42789	. . . 4 ⊢ ((3 ∈ ℕ0 ∧ 2 ∈ ℤ ∧ (𝑎 ∈ (ℤ ↑m (1...3)) ↦ (𝑎‘1)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘1) ∈ (ℤ≥‘2)} ∈ (Dioph‘3))
66	55, 56, 64, 65	mp3an 1463	. . 3 ⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘1) ∈ (ℤ≥‘2)} ∈ (Dioph‘3)
67		3nn 12207	. . . . . . . . 9 ⊢ 3 ∈ ℕ
68	67	jm2.27dlem3 42994	. . . . . . . 8 ⊢ 3 ∈ (1...3)
69		mzpproj 42720	. . . . . . . 8 ⊢ (((1...3) ∈ V ∧ 3 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑m (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3)))
70	57, 68, 69	mp2an 692	. . . . . . 7 ⊢ (𝑎 ∈ (ℤ ↑m (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3))
71		elnnrabdioph 42790	. . . . . . 7 ⊢ ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑m (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘3) ∈ ℕ} ∈ (Dioph‘3))
72	55, 70, 71	mp2an 692	. . . . . 6 ⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘3) ∈ ℕ} ∈ (Dioph‘3)
73		fvex 6835	. . . . . . . . . . . . . . . 16 ⊢ (𝑖‘8) ∈ V
74		fvex 6835	. . . . . . . . . . . . . . . 16 ⊢ (𝑖‘9) ∈ V
75		fvex 6835	. . . . . . . . . . . . . . . 16 ⊢ (𝑖‘;10) ∈ V
76		oveq1 7356	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑖‘9) → (𝑔↑2) = ((𝑖‘9)↑2))
77		oveq1 7356	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = (𝑖‘8) → (𝑓↑2) = ((𝑖‘8)↑2))
78	77	oveq2d 7365	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = (𝑖‘8) → (((𝑒↑2) − 1) · (𝑓↑2)) = (((𝑒↑2) − 1) · ((𝑖‘8)↑2)))
79	76, 78	oveqan12rd 7369	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9)) → ((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))))
80	79	eqeq1d 2731	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9)) → (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ↔ (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1))
81	80	3adant3 1132	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ ℎ = (𝑖‘;10)) → (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ↔ (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1))
82		oveq1 7356	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ = (𝑖‘;10) → (ℎ + 1) = ((𝑖‘;10) + 1))
83	82	oveq1d 7364	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ = (𝑖‘;10) → ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))))
84	83	eqeq2d 2740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = (𝑖‘;10) → (𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ↔ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2)))))
85	84	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ ℎ = (𝑖‘;10)) → (𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ↔ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2)))))
86	81, 85	3anbi12d 1439	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ ℎ = (𝑖‘;10)) → ((((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1))) ↔ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))))
87	86	anbi2d 630	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ ℎ = (𝑖‘;10)) → (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ↔ ((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1))))))
88		oveq1 7356	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑖‘8) → (𝑓 − (𝑎‘3)) = ((𝑖‘8) − (𝑎‘3)))
89	88	breq2d 5104	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑖‘8) → (𝑑 ∥ (𝑓 − (𝑎‘3)) ↔ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))))
90	89	anbi2d 630	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑖‘8) → (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ↔ ((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3)))))
91		oveq1 7356	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑖‘8) → (𝑓 − (𝑎‘2)) = ((𝑖‘8) − (𝑎‘2)))
92	91	breq2d 5104	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑖‘8) → ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ↔ (2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2))))
93	92	anbi1d 631	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑖‘8) → (((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)) ↔ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))
94	90, 93	anbi12d 632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑖‘8) → ((((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))) ↔ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))
95	94	3ad2ant1 1133	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ ℎ = (𝑖‘;10)) → ((((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))) ↔ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))
96	87, 95	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ ℎ = (𝑖‘;10)) → ((((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))))
97	73, 74, 75, 96	sbc3ie 3820	. . . . . . . . . . . . . . 15 ⊢ ([(𝑖‘8) / 𝑓][(𝑖‘9) / 𝑔][(𝑖‘;10) / ℎ](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))
98	97	sbcbii 3799	. . . . . . . . . . . . . 14 ⊢ ([(𝑖‘7) / 𝑒][(𝑖‘8) / 𝑓][(𝑖‘9) / 𝑔][(𝑖‘;10) / ℎ](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ [(𝑖‘7) / 𝑒](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))
99	98	sbcbii 3799	. . . . . . . . . . . . 13 ⊢ ([(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒][(𝑖‘8) / 𝑓][(𝑖‘9) / 𝑔][(𝑖‘;10) / ℎ](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ [(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))
100	99	sbcbii 3799	. . . . . . . . . . . 12 ⊢ ([(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒][(𝑖‘8) / 𝑓][(𝑖‘9) / 𝑔][(𝑖‘;10) / ℎ](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ [(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))
101	100	sbcbii 3799	. . . . . . . . . . 11 ⊢ ([(𝑖‘4) / 𝑏][(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒][(𝑖‘8) / 𝑓][(𝑖‘9) / 𝑔][(𝑖‘;10) / ℎ](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ [(𝑖‘4) / 𝑏][(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))
102	101	sbcbii 3799	. . . . . . . . . 10 ⊢ ([(𝑖 ↾ (1...3)) / 𝑎][(𝑖‘4) / 𝑏][(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒][(𝑖‘8) / 𝑓][(𝑖‘9) / 𝑔][(𝑖‘;10) / ℎ](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ [(𝑖 ↾ (1...3)) / 𝑎][(𝑖‘4) / 𝑏][(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))
103		fvex 6835	. . . . . . . . . . . . 13 ⊢ (𝑖‘5) ∈ V
104		fvex 6835	. . . . . . . . . . . . 13 ⊢ (𝑖‘6) ∈ V
105		fvex 6835	. . . . . . . . . . . . 13 ⊢ (𝑖‘7) ∈ V
106		oveq1 7356	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = (𝑖‘6) → (𝑑↑2) = ((𝑖‘6)↑2))
107	106	3ad2ant2 1134	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑑↑2) = ((𝑖‘6)↑2))
108		oveq1 7356	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑖‘5) → (𝑐↑2) = ((𝑖‘5)↑2))
109	108	oveq2d 7365	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑖‘5) → ((((𝑎‘1)↑2) − 1) · (𝑐↑2)) = ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2)))
110	109	3ad2ant1 1133	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((𝑎‘1)↑2) − 1) · (𝑐↑2)) = ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2)))
111	107, 110	oveq12d 7367	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))))
112	111	eqeq1d 2731	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ↔ (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1))
113		eleq1 2816	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = (𝑖‘7) → (𝑒 ∈ (ℤ≥‘2) ↔ (𝑖‘7) ∈ (ℤ≥‘2)))
114	113	3ad2ant3 1135	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑒 ∈ (ℤ≥‘2) ↔ (𝑖‘7) ∈ (ℤ≥‘2)))
115	112, 114	3anbi23d 1441	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ↔ (((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2))))
116		oveq1 7356	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = (𝑖‘7) → (𝑒↑2) = ((𝑖‘7)↑2))
117	116	oveq1d 7364	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = (𝑖‘7) → ((𝑒↑2) − 1) = (((𝑖‘7)↑2) − 1))
118	117	oveq1d 7364	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖‘7) → (((𝑒↑2) − 1) · ((𝑖‘8)↑2)) = ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2)))
119	118	oveq2d 7365	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑖‘7) → (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))))
120	119	eqeq1d 2731	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = (𝑖‘7) → ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ↔ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1))
121	120	3ad2ant3 1135	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ↔ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1))
122		eqeq1 2733	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑖‘5) → (𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2)))))
123	122	3ad2ant1 1133	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2)))))
124		simp2 1137	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → 𝑑 = (𝑖‘6))
125		oveq1 7356	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑖‘7) → (𝑒 − (𝑎‘1)) = ((𝑖‘7) − (𝑎‘1)))
126	125	3ad2ant3 1135	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑒 − (𝑎‘1)) = ((𝑖‘7) − (𝑎‘1)))
127	124, 126	breq12d 5105	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑑 ∥ (𝑒 − (𝑎‘1)) ↔ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1))))
128	121, 123, 127	3anbi123d 1438	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1))) ↔ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)))))
129	115, 128	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ↔ ((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1))))))
130		oveq1 7356	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑖‘7) → (𝑒 − 1) = ((𝑖‘7) − 1))
131	130	breq2d 5104	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = (𝑖‘7) → ((2 · (𝑎‘3)) ∥ (𝑒 − 1) ↔ (2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1)))
132		breq1 5095	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = (𝑖‘6) → (𝑑 ∥ ((𝑖‘8) − (𝑎‘3)) ↔ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))))
133	131, 132	bi2anan9r 639	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ↔ ((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3)))))
134	133	anbi1d 631	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))) ↔ (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))
135	134	3adant1 1130	. . . . . . . . . . . . . 14 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))) ↔ (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))
136	129, 135	anbi12d 632	. . . . . . . . . . . . 13 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))))
137	103, 104, 105, 136	sbc3ie 3820	. . . . . . . . . . . 12 ⊢ ([(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))
138	137	sbcbii 3799	. . . . . . . . . . 11 ⊢ ([(𝑖‘4) / 𝑏][(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ [(𝑖‘4) / 𝑏](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))
139	138	sbcbii 3799	. . . . . . . . . 10 ⊢ ([(𝑖 ↾ (1...3)) / 𝑎][(𝑖‘4) / 𝑏][(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ [(𝑖 ↾ (1...3)) / 𝑎][(𝑖‘4) / 𝑏](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))
140		vex 3440	. . . . . . . . . . . 12 ⊢ 𝑖 ∈ V
141	140	resex 5980	. . . . . . . . . . 11 ⊢ (𝑖 ↾ (1...3)) ∈ V
142		fvex 6835	. . . . . . . . . . 11 ⊢ (𝑖‘4) ∈ V
143		oveq1 7356	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑖‘4) → (𝑏↑2) = ((𝑖‘4)↑2))
144	62	jm2.27dlem1 42992	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘1) = (𝑖‘1))
145	144	oveq1d 7364	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘1)↑2) = ((𝑖‘1)↑2))
146	145	oveq1d 7364	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((𝑎‘1)↑2) − 1) = (((𝑖‘1)↑2) − 1))
147	68	jm2.27dlem1 42992	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘3) = (𝑖‘3))
148	147	oveq1d 7364	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘3)↑2) = ((𝑖‘3)↑2))
149	146, 148	oveq12d 7367	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2)) = ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2)))
150	143, 149	oveqan12rd 7369	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))))
151	150	eqeq1d 2731	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → (((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ↔ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1))
152	146	oveq1d 7364	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2)) = ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2)))
153	152	oveq2d 7365	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))))
154	153	eqeq1d 2731	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ↔ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1))
155	154	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ↔ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1))
156	151, 155	3anbi12d 1439	. . . . . . . . . . . . 13 ⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2)) ↔ ((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2))))
157	148	oveq2d 7365	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (2 · ((𝑎‘3)↑2)) = (2 · ((𝑖‘3)↑2)))
158	157	oveq2d 7365	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))))
159	158	eqeq2d 2740	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))))
160	144	oveq2d 7365	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘7) − (𝑎‘1)) = ((𝑖‘7) − (𝑖‘1)))
161	160	breq2d 5104	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)) ↔ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))))
162	159, 161	3anbi23d 1441	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1))) ↔ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))))
163	162	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → (((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1))) ↔ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))))
164	156, 163	anbi12d 632	. . . . . . . . . . . 12 ⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)))) ↔ (((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))))))
165	147	oveq2d 7365	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (2 · (𝑎‘3)) = (2 · (𝑖‘3)))
166	165	breq1d 5102	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ↔ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)))
167	147	oveq2d 7365	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘8) − (𝑎‘3)) = ((𝑖‘8) − (𝑖‘3)))
168	167	breq2d 5104	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3)) ↔ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))))
169	166, 168	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ↔ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))))
170	5	jm2.27dlem1 42992	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘2) = (𝑖‘2))
171	170	oveq2d 7365	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘8) − (𝑎‘2)) = ((𝑖‘8) − (𝑖‘2)))
172	165, 171	breq12d 5105	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ↔ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))))
173	170, 147	breq12d 5105	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘2) ≤ (𝑎‘3) ↔ (𝑖‘2) ≤ (𝑖‘3)))
174	172, 173	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)) ↔ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))))
175	169, 174	anbi12d 632	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))) ↔ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))))
176	175	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))) ↔ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))))
177	164, 176	anbi12d 632	. . . . . . . . . . 11 ⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ ((((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))) ∧ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))))))
178	141, 142, 177	sbc2ie 3818	. . . . . . . . . 10 ⊢ ([(𝑖 ↾ (1...3)) / 𝑎][(𝑖‘4) / 𝑏](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ ((((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))) ∧ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))))
179	102, 139, 178	3bitri 297	. . . . . . . . 9 ⊢ ([(𝑖 ↾ (1...3)) / 𝑎][(𝑖‘4) / 𝑏][(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒][(𝑖‘8) / 𝑓][(𝑖‘9) / 𝑔][(𝑖‘;10) / ℎ](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ ((((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))) ∧ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))))
180	179	rabbii 3400	. . . . . . . 8 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ [(𝑖 ↾ (1...3)) / 𝑎][(𝑖‘4) / 𝑏][(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒][(𝑖‘8) / 𝑓][(𝑖‘9) / 𝑔][(𝑖‘;10) / ℎ](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))} = {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ ((((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))) ∧ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))))}
181		10nn0 12609	. . . . . . . . . . . 12 ⊢ ;10 ∈ ℕ0
182		ovex 7382	. . . . . . . . . . . . . . 15 ⊢ (1...;10) ∈ V
183		df-5 12194	. . . . . . . . . . . . . . . . 17 ⊢ 5 = (4 + 1)
184		df-6 12195	. . . . . . . . . . . . . . . . . 18 ⊢ 6 = (5 + 1)
185		df-7 12196	. . . . . . . . . . . . . . . . . . 19 ⊢ 7 = (6 + 1)
186		df-8 12197	. . . . . . . . . . . . . . . . . . . 20 ⊢ 8 = (7 + 1)
187		df-9 12198	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 9 = (8 + 1)
188		9p1e10 12593	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (9 + 1) = ;10
189	188	eqcomi 2738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ;10 = (9 + 1)
190		ssid 3958	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1...;10) ⊆ (1...;10)
191	189, 190	jm2.27dlem5 42996	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1...9) ⊆ (1...;10)
192	187, 191	jm2.27dlem5 42996	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...8) ⊆ (1...;10)
193	186, 192	jm2.27dlem5 42996	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...7) ⊆ (1...;10)
194	185, 193	jm2.27dlem5 42996	. . . . . . . . . . . . . . . . . 18 ⊢ (1...6) ⊆ (1...;10)
195	184, 194	jm2.27dlem5 42996	. . . . . . . . . . . . . . . . 17 ⊢ (1...5) ⊆ (1...;10)
196	183, 195	jm2.27dlem5 42996	. . . . . . . . . . . . . . . 16 ⊢ (1...4) ⊆ (1...;10)
197		4nn 12211	. . . . . . . . . . . . . . . . 17 ⊢ 4 ∈ ℕ
198	197	jm2.27dlem3 42994	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ (1...4)
199	196, 198	sselii 3932	. . . . . . . . . . . . . . 15 ⊢ 4 ∈ (1...;10)
200		mzpproj 42720	. . . . . . . . . . . . . . 15 ⊢ (((1...;10) ∈ V ∧ 4 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘4)) ∈ (mzPoly‘(1...;10)))
201	182, 199, 200	mp2an 692	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘4)) ∈ (mzPoly‘(1...;10))
202		2nn0 12401	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ0
203		mzpexpmpt 42728	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘4)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘4)↑2)) ∈ (mzPoly‘(1...;10)))
204	201, 202, 203	mp2an 692	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘4)↑2)) ∈ (mzPoly‘(1...;10))
205		df-4 12193	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 4 = (3 + 1)
206	205, 196	jm2.27dlem5 42996	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...3) ⊆ (1...;10)
207	4, 206	jm2.27dlem5 42996	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...2) ⊆ (1...;10)
208	60, 207	jm2.27dlem5 42996	. . . . . . . . . . . . . . . . . 18 ⊢ (1...1) ⊆ (1...;10)
209	208, 59	sselii 3932	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ (1...;10)
210		mzpproj 42720	. . . . . . . . . . . . . . . . 17 ⊢ (((1...;10) ∈ V ∧ 1 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...;10)))
211	182, 209, 210	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...;10))
212		mzpexpmpt 42728	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘1)↑2)) ∈ (mzPoly‘(1...;10)))
213	211, 202, 212	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘1)↑2)) ∈ (mzPoly‘(1...;10))
214		1z 12505	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℤ
215		mzpconstmpt 42723	. . . . . . . . . . . . . . . 16 ⊢ (((1...;10) ∈ V ∧ 1 ∈ ℤ) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10)))
216	182, 214, 215	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))
217		mzpsubmpt 42726	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘1)↑2)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘1)↑2) − 1)) ∈ (mzPoly‘(1...;10)))
218	213, 216, 217	mp2an 692	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘1)↑2) − 1)) ∈ (mzPoly‘(1...;10))
219	206, 68	sselii 3932	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ (1...;10)
220		mzpproj 42720	. . . . . . . . . . . . . . . 16 ⊢ (((1...;10) ∈ V ∧ 3 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...;10)))
221	182, 219, 220	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...;10))
222		mzpexpmpt 42728	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘3)↑2)) ∈ (mzPoly‘(1...;10)))
223	221, 202, 222	mp2an 692	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘3)↑2)) ∈ (mzPoly‘(1...;10))
224		mzpmulmpt 42725	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘1)↑2) − 1)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘3)↑2)) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...;10)))
225	218, 223, 224	mp2an 692	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...;10))
226		mzpsubmpt 42726	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘4)↑2)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2)))) ∈ (mzPoly‘(1...;10)))
227	204, 225, 226	mp2an 692	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2)))) ∈ (mzPoly‘(1...;10))
228		eqrabdioph 42760	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2)))) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1} ∈ (Dioph‘;10))
229	181, 227, 216, 228	mp3an 1463	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1} ∈ (Dioph‘;10)
230		6nn 12217	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℕ
231	230	jm2.27dlem3 42994	. . . . . . . . . . . . . . . 16 ⊢ 6 ∈ (1...6)
232	194, 231	sselii 3932	. . . . . . . . . . . . . . 15 ⊢ 6 ∈ (1...;10)
233		mzpproj 42720	. . . . . . . . . . . . . . 15 ⊢ (((1...;10) ∈ V ∧ 6 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...;10)))
234	182, 232, 233	mp2an 692	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...;10))
235		mzpexpmpt 42728	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘6)↑2)) ∈ (mzPoly‘(1...;10)))
236	234, 202, 235	mp2an 692	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘6)↑2)) ∈ (mzPoly‘(1...;10))
237		5nn 12214	. . . . . . . . . . . . . . . . . 18 ⊢ 5 ∈ ℕ
238	237	jm2.27dlem3 42994	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ (1...5)
239	195, 238	sselii 3932	. . . . . . . . . . . . . . . 16 ⊢ 5 ∈ (1...;10)
240		mzpproj 42720	. . . . . . . . . . . . . . . 16 ⊢ (((1...;10) ∈ V ∧ 5 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...;10)))
241	182, 239, 240	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...;10))
242		mzpexpmpt 42728	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘5)↑2)) ∈ (mzPoly‘(1...;10)))
243	241, 202, 242	mp2an 692	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘5)↑2)) ∈ (mzPoly‘(1...;10))
244		mzpmulmpt 42725	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘1)↑2) − 1)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘5)↑2)) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) ∈ (mzPoly‘(1...;10)))
245	218, 243, 244	mp2an 692	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) ∈ (mzPoly‘(1...;10))
246		mzpsubmpt 42726	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘6)↑2)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2)))) ∈ (mzPoly‘(1...;10)))
247	236, 245, 246	mp2an 692	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2)))) ∈ (mzPoly‘(1...;10))
248		eqrabdioph 42760	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2)))) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1} ∈ (Dioph‘;10))
249	181, 247, 216, 248	mp3an 1463	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1} ∈ (Dioph‘;10)
250		7nn 12220	. . . . . . . . . . . . . . 15 ⊢ 7 ∈ ℕ
251	250	jm2.27dlem3 42994	. . . . . . . . . . . . . 14 ⊢ 7 ∈ (1...7)
252	193, 251	sselii 3932	. . . . . . . . . . . . 13 ⊢ 7 ∈ (1...;10)
253		mzpproj 42720	. . . . . . . . . . . . 13 ⊢ (((1...;10) ∈ V ∧ 7 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10)))
254	182, 252, 253	mp2an 692	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10))
255		eluzrabdioph 42789	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℕ0 ∧ 2 ∈ ℤ ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (𝑖‘7) ∈ (ℤ≥‘2)} ∈ (Dioph‘;10))
256	181, 56, 254, 255	mp3an 1463	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (𝑖‘7) ∈ (ℤ≥‘2)} ∈ (Dioph‘;10)
257		3anrabdioph 42765	. . . . . . . . . . 11 ⊢ (({𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (𝑖‘7) ∈ (ℤ≥‘2)} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ ((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2))} ∈ (Dioph‘;10))
258	229, 249, 256, 257	mp3an 1463	. . . . . . . . . 10 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ ((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2))} ∈ (Dioph‘;10)
259		9nn 12226	. . . . . . . . . . . . . . . . 17 ⊢ 9 ∈ ℕ
260	259	jm2.27dlem3 42994	. . . . . . . . . . . . . . . 16 ⊢ 9 ∈ (1...9)
261	260, 189, 259	jm2.27dlem2 42993	. . . . . . . . . . . . . . 15 ⊢ 9 ∈ (1...;10)
262		mzpproj 42720	. . . . . . . . . . . . . . 15 ⊢ (((1...;10) ∈ V ∧ 9 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘9)) ∈ (mzPoly‘(1...;10)))
263	182, 261, 262	mp2an 692	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘9)) ∈ (mzPoly‘(1...;10))
264		mzpexpmpt 42728	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘9)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘9)↑2)) ∈ (mzPoly‘(1...;10)))
265	263, 202, 264	mp2an 692	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘9)↑2)) ∈ (mzPoly‘(1...;10))
266		mzpexpmpt 42728	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘7)↑2)) ∈ (mzPoly‘(1...;10)))
267	254, 202, 266	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘7)↑2)) ∈ (mzPoly‘(1...;10))
268		mzpsubmpt 42726	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘7)↑2)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘7)↑2) − 1)) ∈ (mzPoly‘(1...;10)))
269	267, 216, 268	mp2an 692	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘7)↑2) − 1)) ∈ (mzPoly‘(1...;10))
270		8nn 12223	. . . . . . . . . . . . . . . . . 18 ⊢ 8 ∈ ℕ
271	270	jm2.27dlem3 42994	. . . . . . . . . . . . . . . . 17 ⊢ 8 ∈ (1...8)
272	192, 271	sselii 3932	. . . . . . . . . . . . . . . 16 ⊢ 8 ∈ (1...;10)
273		mzpproj 42720	. . . . . . . . . . . . . . . 16 ⊢ (((1...;10) ∈ V ∧ 8 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...;10)))
274	182, 272, 273	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...;10))
275		mzpexpmpt 42728	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘8)↑2)) ∈ (mzPoly‘(1...;10)))
276	274, 202, 275	mp2an 692	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘8)↑2)) ∈ (mzPoly‘(1...;10))
277		mzpmulmpt 42725	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘7)↑2) − 1)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘8)↑2)) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) ∈ (mzPoly‘(1...;10)))
278	269, 276, 277	mp2an 692	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) ∈ (mzPoly‘(1...;10))
279		mzpsubmpt 42726	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘9)↑2)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2)))) ∈ (mzPoly‘(1...;10)))
280	265, 278, 279	mp2an 692	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2)))) ∈ (mzPoly‘(1...;10))
281		eqrabdioph 42760	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2)))) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1} ∈ (Dioph‘;10))
282	181, 280, 216, 281	mp3an 1463	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1} ∈ (Dioph‘;10)
283		10nn 12607	. . . . . . . . . . . . . . . 16 ⊢ ;10 ∈ ℕ
284	283	jm2.27dlem3 42994	. . . . . . . . . . . . . . 15 ⊢ ;10 ∈ (1...;10)
285		mzpproj 42720	. . . . . . . . . . . . . . 15 ⊢ (((1...;10) ∈ V ∧ ;10 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘;10)) ∈ (mzPoly‘(1...;10)))
286	182, 284, 285	mp2an 692	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘;10)) ∈ (mzPoly‘(1...;10))
287		mzpaddmpt 42724	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘;10)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘;10) + 1)) ∈ (mzPoly‘(1...;10)))
288	286, 216, 287	mp2an 692	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘;10) + 1)) ∈ (mzPoly‘(1...;10))
289		mzpconstmpt 42723	. . . . . . . . . . . . . . 15 ⊢ (((1...;10) ∈ V ∧ 2 ∈ ℤ) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ 2) ∈ (mzPoly‘(1...;10)))
290	182, 56, 289	mp2an 692	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ 2) ∈ (mzPoly‘(1...;10))
291		mzpmulmpt 42725	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ 2) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘3)↑2)) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (2 · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...;10)))
292	290, 223, 291	mp2an 692	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (2 · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...;10))
293		mzpmulmpt 42725	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘;10) + 1)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (2 · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))) ∈ (mzPoly‘(1...;10)))
294	288, 292, 293	mp2an 692	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))) ∈ (mzPoly‘(1...;10))
295		eqrabdioph 42760	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))} ∈ (Dioph‘;10))
296	181, 241, 294, 295	mp3an 1463	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))} ∈ (Dioph‘;10)
297		mzpsubmpt 42726	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘7) − (𝑖‘1))) ∈ (mzPoly‘(1...;10)))
298	254, 211, 297	mp2an 692	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘7) − (𝑖‘1))) ∈ (mzPoly‘(1...;10))
299		dvdsrabdioph 42793	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘7) − (𝑖‘1))) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))} ∈ (Dioph‘;10))
300	181, 234, 298, 299	mp3an 1463	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))} ∈ (Dioph‘;10)
301		3anrabdioph 42765	. . . . . . . . . . 11 ⊢ (({𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))} ∈ (Dioph‘;10))
302	282, 296, 300, 301	mp3an 1463	. . . . . . . . . 10 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))} ∈ (Dioph‘;10)
303		anrabdioph 42763	. . . . . . . . . 10 ⊢ (({𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ ((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2))} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))))} ∈ (Dioph‘;10))
304	258, 302, 303	mp2an 692	. . . . . . . . 9 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))))} ∈ (Dioph‘;10)
305		mzpmulmpt 42725	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ 2) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...;10)))
306	290, 221, 305	mp2an 692	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...;10))
307		mzpsubmpt 42726	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘7) − 1)) ∈ (mzPoly‘(1...;10)))
308	254, 216, 307	mp2an 692	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘7) − 1)) ∈ (mzPoly‘(1...;10))
309		dvdsrabdioph 42793	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘7) − 1)) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)} ∈ (Dioph‘;10))
310	181, 306, 308, 309	mp3an 1463	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)} ∈ (Dioph‘;10)
311		mzpsubmpt 42726	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘8) − (𝑖‘3))) ∈ (mzPoly‘(1...;10)))
312	274, 221, 311	mp2an 692	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘8) − (𝑖‘3))) ∈ (mzPoly‘(1...;10))
313		dvdsrabdioph 42793	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘8) − (𝑖‘3))) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))} ∈ (Dioph‘;10))
314	181, 234, 312, 313	mp3an 1463	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))} ∈ (Dioph‘;10)
315		anrabdioph 42763	. . . . . . . . . . 11 ⊢ (({𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))} ∈ (Dioph‘;10))
316	310, 314, 315	mp2an 692	. . . . . . . . . 10 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))} ∈ (Dioph‘;10)
317	207, 3	sselii 3932	. . . . . . . . . . . . . 14 ⊢ 2 ∈ (1...;10)
318		mzpproj 42720	. . . . . . . . . . . . . 14 ⊢ (((1...;10) ∈ V ∧ 2 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...;10)))
319	182, 317, 318	mp2an 692	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...;10))
320		mzpsubmpt 42726	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘8) − (𝑖‘2))) ∈ (mzPoly‘(1...;10)))
321	274, 319, 320	mp2an 692	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘8) − (𝑖‘2))) ∈ (mzPoly‘(1...;10))
322		dvdsrabdioph 42793	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘8) − (𝑖‘2))) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))} ∈ (Dioph‘;10))
323	181, 306, 321, 322	mp3an 1463	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))} ∈ (Dioph‘;10)
324		lerabdioph 42788	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (𝑖‘2) ≤ (𝑖‘3)} ∈ (Dioph‘;10))
325	181, 319, 221, 324	mp3an 1463	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (𝑖‘2) ≤ (𝑖‘3)} ∈ (Dioph‘;10)
326		anrabdioph 42763	. . . . . . . . . . 11 ⊢ (({𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (𝑖‘2) ≤ (𝑖‘3)} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))} ∈ (Dioph‘;10))
327	323, 325, 326	mp2an 692	. . . . . . . . . 10 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))} ∈ (Dioph‘;10)
328		anrabdioph 42763	. . . . . . . . . 10 ⊢ (({𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))} ∈ (Dioph‘;10))
329	316, 327, 328	mp2an 692	. . . . . . . . 9 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))} ∈ (Dioph‘;10)
330		anrabdioph 42763	. . . . . . . . 9 ⊢ (({𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))))} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ ((((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))) ∧ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))))} ∈ (Dioph‘;10))
331	304, 329, 330	mp2an 692	. . . . . . . 8 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ ((((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))) ∧ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))))} ∈ (Dioph‘;10)
332	180, 331	eqeltri 2824	. . . . . . 7 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ [(𝑖 ↾ (1...3)) / 𝑎][(𝑖‘4) / 𝑏][(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒][(𝑖‘8) / 𝑓][(𝑖‘9) / 𝑔][(𝑖‘;10) / ℎ](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))} ∈ (Dioph‘;10)
333	205, 183, 184, 185, 186, 187, 189	7rexfrabdioph 42783	. . . . . . 7 ⊢ ((3 ∈ ℕ0 ∧ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ [(𝑖 ↾ (1...3)) / 𝑎][(𝑖‘4) / 𝑏][(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒][(𝑖‘8) / 𝑓][(𝑖‘9) / 𝑔][(𝑖‘;10) / ℎ](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))} ∈ (Dioph‘;10)) → {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))} ∈ (Dioph‘3))
334	55, 332, 333	mp2an 692	. . . . . 6 ⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))} ∈ (Dioph‘3)
335		anrabdioph 42763	. . . . . 6 ⊢ (({𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘3) ∈ ℕ} ∈ (Dioph‘3) ∧ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))} ∈ (Dioph‘3)) → {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))} ∈ (Dioph‘3))
336	72, 334, 335	mp2an 692	. . . . 5 ⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))} ∈ (Dioph‘3)
337		mzpproj 42720	. . . . . . 7 ⊢ (((1...3) ∈ V ∧ 2 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑m (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3)))
338	57, 5, 337	mp2an 692	. . . . . 6 ⊢ (𝑎 ∈ (ℤ ↑m (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3))
339		elnnrabdioph 42790	. . . . . 6 ⊢ ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑m (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈ (Dioph‘3))
340	55, 338, 339	mp2an 692	. . . . 5 ⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈ (Dioph‘3)
341		anrabdioph 42763	. . . . 5 ⊢ (({𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))} ∈ (Dioph‘3) ∧ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈ (Dioph‘3)) → {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ)} ∈ (Dioph‘3))
342	336, 340, 341	mp2an 692	. . . 4 ⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ)} ∈ (Dioph‘3)
343		eq0rabdioph 42759	. . . . . 6 ⊢ ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑m (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘3) = 0} ∈ (Dioph‘3))
344	55, 70, 343	mp2an 692	. . . . 5 ⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘3) = 0} ∈ (Dioph‘3)
345		eq0rabdioph 42759	. . . . . 6 ⊢ ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑m (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘2) = 0} ∈ (Dioph‘3))
346	55, 338, 345	mp2an 692	. . . . 5 ⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘2) = 0} ∈ (Dioph‘3)
347		anrabdioph 42763	. . . . 5 ⊢ (({𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘3) = 0} ∈ (Dioph‘3) ∧ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘2) = 0} ∈ (Dioph‘3)) → {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)} ∈ (Dioph‘3))
348	344, 346, 347	mp2an 692	. . . 4 ⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)} ∈ (Dioph‘3)
349		orrabdioph 42764	. . . 4 ⊢ (({𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ)} ∈ (Dioph‘3) ∧ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)} ∈ (Dioph‘3)) → {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ((((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0))} ∈ (Dioph‘3))
350	342, 348, 349	mp2an 692	. . 3 ⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ((((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0))} ∈ (Dioph‘3)
351		anrabdioph 42763	. . 3 ⊢ (({𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘1) ∈ (ℤ≥‘2)} ∈ (Dioph‘3) ∧ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ((((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0))} ∈ (Dioph‘3)) → {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ((𝑎‘1) ∈ (ℤ≥‘2) ∧ ((((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)))} ∈ (Dioph‘3))
352	66, 350, 351	mp2an 692	. 2 ⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ((𝑎‘1) ∈ (ℤ≥‘2) ∧ ((((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)))} ∈ (Dioph‘3)
353	54, 352	eqeltri 2824	1 ⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} ∈ (Dioph‘3)

Syntax hints:   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∃wrex 3053  {crab 3394  Vcvv 3436  [wsbc 3742   class class class wbr 5092   ↦ cmpt 5173   ↾ cres 5621  ⟶wf 6478  ‘cfv 6482  (class class class)co 7349   ↑_m cmap 8753  0cc0 11009  1c1 11010   + caddc 11012   · cmul 11014   < clt 11149   ≤ cle 11150   − cmin 11347  ℕcn 12128  2c2 12183  3c3 12184  4c4 12185  5c5 12186  6c6 12187  7c7 12188  8c8 12189  9c9 12190  ℕ₀cn0 12384  ℤcz 12471  ;cdc 12591  ℤ_≥cuz 12735  ...cfz 13410  ↑cexp 13968   ∥ cdvds 16163  mzPolycmzp 42705  Diophcdioph 42738   Y_rm crmy 42884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-inf2 9537  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086  ax-pre-sup 11087  ax-addf 11088

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-tp 4582  df-op 4584  df-uni 4859  df-int 4897  df-iun 4943  df-iin 4944  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-se 5573  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-isom 6491  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-of 7613  df-om 7800  df-1st 7924  df-2nd 7925  df-supp 8094  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-1o 8388  df-2o 8389  df-oadd 8392  df-omul 8393  df-er 8625  df-map 8755  df-pm 8756  df-ixp 8825  df-en 8873  df-dom 8874  df-sdom 8875  df-fin 8876  df-fsupp 9252  df-fi 9301  df-sup 9332  df-inf 9333  df-oi 9402  df-dju 9797  df-card 9835  df-acn 9838  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-div 11778  df-nn 12129  df-2 12191  df-3 12192  df-4 12193  df-5 12194  df-6 12195  df-7 12196  df-8 12197  df-9 12198  df-n0 12385  df-xnn0 12458  df-z 12472  df-dec 12592  df-uz 12736  df-q 12850  df-rp 12894  df-xneg 13014  df-xadd 13015  df-xmul 13016  df-ioo 13252  df-ioc 13253  df-ico 13254  df-icc 13255  df-fz 13411  df-fzo 13558  df-fl 13696  df-mod 13774  df-seq 13909  df-exp 13969  df-fac 14181  df-bc 14210  df-hash 14238  df-shft 14974  df-cj 15006  df-re 15007  df-im 15008  df-sqrt 15142  df-abs 15143  df-limsup 15378  df-clim 15395  df-rlim 15396  df-sum 15594  df-ef 15974  df-sin 15976  df-cos 15977  df-pi 15979  df-dvds 16164  df-gcd 16406  df-prm 16583  df-numer 16646  df-denom 16647  df-struct 17058  df-sets 17075  df-slot 17093  df-ndx 17105  df-base 17121  df-ress 17142  df-plusg 17174  df-mulr 17175  df-starv 17176  df-sca 17177  df-vsca 17178  df-ip 17179  df-tset 17180  df-ple 17181  df-ds 17183  df-unif 17184  df-hom 17185  df-cco 17186  df-rest 17326  df-topn 17327  df-0g 17345  df-gsum 17346  df-topgen 17347  df-pt 17348  df-prds 17351  df-xrs 17406  df-qtop 17411  df-imas 17412  df-xps 17414  df-mre 17488  df-mrc 17489  df-acs 17491  df-mgm 18514  df-sgrp 18593  df-mnd 18609  df-submnd 18658  df-mulg 18947  df-cntz 19196  df-cmn 19661  df-psmet 21253  df-xmet 21254  df-met 21255  df-bl 21256  df-mopn 21257  df-fbas 21258  df-fg 21259  df-cnfld 21262  df-top 22779  df-topon 22796  df-topsp 22818  df-bases 22831  df-cld 22904  df-ntr 22905  df-cls 22906  df-nei 22983  df-lp 23021  df-perf 23022  df-cn 23112  df-cnp 23113  df-haus 23200  df-tx 23447  df-hmeo 23640  df-fil 23731  df-fm 23823  df-flim 23824  df-flf 23825  df-xms 24206  df-ms 24207  df-tms 24208  df-cncf 24769  df-limc 25765  df-dv 25766  df-log 26463  df-mzpcl 42706  df-mzp 42707  df-dioph 42739  df-squarenn 42824  df-pell1qr 42825  df-pell14qr 42826  df-pell1234qr 42827  df-pellfund 42828  df-rmx 42885  df-rmy 42886

This theorem is referenced by:  rmxdioph  42999  expdiophlem2  43005