Theorem rmydioph 43818

Description: jm2.27 43812 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 8852	. . . . . . 7 ⊢ (𝑎 ∈ (ℕ0 ↑m (1...3)) → 𝑎:(1...3)⟶ℕ0)
2		2nn 12333	. . . . . . . . 9 ⊢ 2 ∈ ℕ
3	2	jm2.27dlem3 43815	. . . . . . . 8 ⊢ 2 ∈ (1...2)
4		df-3 12323	. . . . . . . 8 ⊢ 3 = (2 + 1)
5	3, 4, 2	jm2.27dlem2 43814	. . . . . . 7 ⊢ 2 ∈ (1...3)
6		ffvelcdm 7080	. . . . . . 7 ⊢ ((𝑎:(1...3)⟶ℕ0 ∧ 2 ∈ (1...3)) → (𝑎‘2) ∈ ℕ0)
7	1, 5, 6	sylancl 598	. . . . . 6 ⊢ (𝑎 ∈ (ℕ0 ↑m (1...3)) → (𝑎‘2) ∈ ℕ0)
8		elnn0 12525	. . . . . 6 ⊢ ((𝑎‘2) ∈ ℕ0 ↔ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0))
9	7, 8	sylib 221	. . . . 5 ⊢ (𝑎 ∈ (ℕ0 ↑m (1...3)) → ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0))
10		iba 537	. . . . . . 7 ⊢ (((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0))))
11		andi 1025	. . . . . . 7 ⊢ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0)) ↔ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0)))
12	10, 11	bitrdi 290	. . . . . 6 ⊢ (((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0))))
13	12	anbi2d 642	. . . . 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 18	. . . 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 781	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → (𝑎‘1) ∈ (ℤ≥‘2))
16		nnz 12631	. . . . . . . . . . . . . 14 ⊢ ((𝑎‘2) ∈ ℕ → (𝑎‘2) ∈ ℤ)
17	16	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → (𝑎‘2) ∈ ℤ)
18		frmy 43718	. . . . . . . . . . . . . 14 ⊢ Yrm :((ℤ≥‘2) × ℤ)⟶ℤ
19	18	fovcl 7547	. . . . . . . . . . . . 13 ⊢ (((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘2) ∈ ℤ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℤ)
20	15, 17, 19	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℤ)
21		rmy0 43733	. . . . . . . . . . . . . 14 ⊢ ((𝑎‘1) ∈ (ℤ≥‘2) → ((𝑎‘1) Yrm 0) = 0)
22	21	ad2antlr 740	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm 0) = 0)
23		nngt0 12286	. . . . . . . . . . . . . . 15 ⊢ ((𝑎‘2) ∈ ℕ → 0 < (𝑎‘2))
24	23	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 < (𝑎‘2))
25		0zd 12622	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 ∈ ℤ)
26		ltrmy 43756	. . . . . . . . . . . . . . 15 ⊢ (((𝑎‘1) ∈ (ℤ≥‘2) ∧ 0 ∈ ℤ ∧ (𝑎‘2) ∈ ℤ) → (0 < (𝑎‘2) ↔ ((𝑎‘1) Yrm 0) < ((𝑎‘1) Yrm (𝑎‘2))))
27	15, 25, 17, 26	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → (0 < (𝑎‘2) ↔ ((𝑎‘1) Yrm 0) < ((𝑎‘1) Yrm (𝑎‘2))))
28	24, 27	mpbid 235	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm 0) < ((𝑎‘1) Yrm (𝑎‘2)))
29	22, 28	eqbrtrrd 5137	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 < ((𝑎‘1) Yrm (𝑎‘2)))
30		elnnz 12620	. . . . . . . . . . . 12 ⊢ (((𝑎‘1) Yrm (𝑎‘2)) ∈ ℕ ↔ (((𝑎‘1) Yrm (𝑎‘2)) ∈ ℤ ∧ 0 < ((𝑎‘1) Yrm (𝑎‘2))))
31	20, 29, 30	sylanbrc 595	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℕ)
32		eleq1 2853	. . . . . . . . . . 11 ⊢ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) → ((𝑎‘3) ∈ ℕ ↔ ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℕ))
33	31, 32	syl5ibrcom 250	. . . . . . . . . 10 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) → (𝑎‘3) ∈ ℕ))
34	33	pm4.71rd 572	. . . . . . . . 9 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ((𝑎‘3) ∈ ℕ ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))))
35		simpllr 788	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) → (𝑎‘1) ∈ (ℤ≥‘2))
36		simplr 781	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) → (𝑎‘2) ∈ ℕ)
37		simpr 490	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) → (𝑎‘3) ∈ ℕ)
38		jm2.27 43812	. . . . . . . . . . 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 1398	. . . . . . . . . 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 590	. . . . . . . . 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 282	. . . . . . . 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 418	. . . . . . 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 589	. . . . . 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 7427	. . . . . . . . . . 11 ⊢ ((𝑎‘2) = 0 → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑎‘1) Yrm 0))
45	44	adantl 487	. . . . . . . . . 10 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑎‘1) Yrm 0))
46	21	ad2antlr 740	. . . . . . . . . 10 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm 0) = 0)
47	45, 46	eqtrd 2800	. . . . . . . . 9 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm (𝑎‘2)) = 0)
48	47	eqeq2d 2776	. . . . . . . 8 ⊢ (((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (𝑎‘3) = 0))
49	48	ex 418	. . . . . . 7 ⊢ ((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) → ((𝑎‘2) = 0 → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (𝑎‘3) = 0)))
50	49	pm5.32rd 589	. . . . . 6 ⊢ ((𝑎 ∈ (ℕ0 ↑m (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) → (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0) ↔ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)))
51	43, 50	orbi12d 932	. . . . 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 590	. . . 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 282	. . 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 3422	. 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 12541	. . . 4 ⊢ 3 ∈ ℕ0
56		2z 12645	. . . 4 ⊢ 2 ∈ ℤ
57		ovex 7452	. . . . 5 ⊢ (1...3) ∈ V
58		1nn 12263	. . . . . . . 8 ⊢ 1 ∈ ℕ
59	58	jm2.27dlem3 43815	. . . . . . 7 ⊢ 1 ∈ (1...1)
60		df-2 12322	. . . . . . 7 ⊢ 2 = (1 + 1)
61	59, 60, 58	jm2.27dlem2 43814	. . . . . 6 ⊢ 1 ∈ (1...2)
62	61, 4, 2	jm2.27dlem2 43814	. . . . 5 ⊢ 1 ∈ (1...3)
63		mzpproj 43545	. . . . 5 ⊢ (((1...3) ∈ V ∧ 1 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑m (1...3)) ↦ (𝑎‘1)) ∈ (mzPoly‘(1...3)))
64	57, 62, 63	mp2an 705	. . . 4 ⊢ (𝑎 ∈ (ℤ ↑m (1...3)) ↦ (𝑎‘1)) ∈ (mzPoly‘(1...3))
65		eluzrabdioph 43610	. . . 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 1490	. . 3 ⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘1) ∈ (ℤ≥‘2)} ∈ (Dioph‘3)
67		3nn 12339	. . . . . . . . 9 ⊢ 3 ∈ ℕ
68	67	jm2.27dlem3 43815	. . . . . . . 8 ⊢ 3 ∈ (1...3)
69		mzpproj 43545	. . . . . . . 8 ⊢ (((1...3) ∈ V ∧ 3 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑m (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3)))
70	57, 68, 69	mp2an 705	. . . . . . 7 ⊢ (𝑎 ∈ (ℤ ↑m (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3))
71		elnnrabdioph 43611	. . . . . . 7 ⊢ ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑m (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘3) ∈ ℕ} ∈ (Dioph‘3))
72	55, 70, 71	mp2an 705	. . . . . 6 ⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘3) ∈ ℕ} ∈ (Dioph‘3)
73		fvex 6898	. . . . . . . . . . . . . . . 16 ⊢ (𝑖‘8) ∈ V
74		fvex 6898	. . . . . . . . . . . . . . . 16 ⊢ (𝑖‘9) ∈ V
75		fvex 6898	. . . . . . . . . . . . . . . 16 ⊢ (𝑖‘;10) ∈ V
76		oveq1 7426	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑖‘9) → (𝑔↑2) = ((𝑖‘9)↑2))
77		oveq1 7426	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = (𝑖‘8) → (𝑓↑2) = ((𝑖‘8)↑2))
78	77	oveq2d 7435	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = (𝑖‘8) → (((𝑒↑2) − 1) · (𝑓↑2)) = (((𝑒↑2) − 1) · ((𝑖‘8)↑2)))
79	76, 78	oveqan12rd 7439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9)) → ((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))))
80	79	eqeq1d 2767	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9)) → (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ↔ (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1))
81	80	3adant3 1150	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ ℎ = (𝑖‘;10)) → (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ↔ (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1))
82		oveq1 7426	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ = (𝑖‘;10) → (ℎ + 1) = ((𝑖‘;10) + 1))
83	82	oveq1d 7434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ = (𝑖‘;10) → ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))))
84	83	eqeq2d 2776	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = (𝑖‘;10) → (𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ↔ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2)))))
85	84	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ ℎ = (𝑖‘;10)) → (𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ↔ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2)))))
86	81, 85	3anbi12d 1465	. . . . . . . . . . . . . . . . . 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 642	. . . . . . . . . . . . . . . . 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 7426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑖‘8) → (𝑓 − (𝑎‘3)) = ((𝑖‘8) − (𝑎‘3)))
89	88	breq2d 5123	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑖‘8) → (𝑑 ∥ (𝑓 − (𝑎‘3)) ↔ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))))
90	89	anbi2d 642	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑖‘8) → (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ↔ ((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3)))))
91		oveq1 7426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑖‘8) → (𝑓 − (𝑎‘2)) = ((𝑖‘8) − (𝑎‘2)))
92	91	breq2d 5123	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑖‘8) → ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ↔ (2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2))))
93	92	anbi1d 643	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑖‘8) → (((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)) ↔ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))
94	90, 93	anbi12d 644	. . . . . . . . . . . . . . . . . 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 1151	. . . . . . . . . . . . . . . . 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 644	. . . . . . . . . . . . . . . 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 3823	. . . . . . . . . . . . . . 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 3802	. . . . . . . . . . . . . 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 3802	. . . . . . . . . . . . 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 3802	. . . . . . . . . . . 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 3802	. . . . . . . . . . 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 3802	. . . . . . . . . 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 6898	. . . . . . . . . . . . 13 ⊢ (𝑖‘5) ∈ V
104		fvex 6898	. . . . . . . . . . . . 13 ⊢ (𝑖‘6) ∈ V
105		fvex 6898	. . . . . . . . . . . . 13 ⊢ (𝑖‘7) ∈ V
106		oveq1 7426	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = (𝑖‘6) → (𝑑↑2) = ((𝑖‘6)↑2))
107	106	3ad2ant2 1152	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑑↑2) = ((𝑖‘6)↑2))
108		oveq1 7426	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑖‘5) → (𝑐↑2) = ((𝑖‘5)↑2))
109	108	oveq2d 7435	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑖‘5) → ((((𝑎‘1)↑2) − 1) · (𝑐↑2)) = ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2)))
110	109	3ad2ant1 1151	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((𝑎‘1)↑2) − 1) · (𝑐↑2)) = ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2)))
111	107, 110	oveq12d 7437	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))))
112	111	eqeq1d 2767	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ↔ (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1))
113		eleq1 2853	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = (𝑖‘7) → (𝑒 ∈ (ℤ≥‘2) ↔ (𝑖‘7) ∈ (ℤ≥‘2)))
114	113	3ad2ant3 1153	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑒 ∈ (ℤ≥‘2) ↔ (𝑖‘7) ∈ (ℤ≥‘2)))
115	112, 114	3anbi23d 1467	. . . . . . . . . . . . . . 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 7426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = (𝑖‘7) → (𝑒↑2) = ((𝑖‘7)↑2))
117	116	oveq1d 7434	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = (𝑖‘7) → ((𝑒↑2) − 1) = (((𝑖‘7)↑2) − 1))
118	117	oveq1d 7434	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖‘7) → (((𝑒↑2) − 1) · ((𝑖‘8)↑2)) = ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2)))
119	118	oveq2d 7435	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑖‘7) → (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))))
120	119	eqeq1d 2767	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = (𝑖‘7) → ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ↔ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1))
121	120	3ad2ant3 1153	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ↔ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1))
122		eqeq1 2769	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑖‘5) → (𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2)))))
123	122	3ad2ant1 1151	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2)))))
124		simp2 1155	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → 𝑑 = (𝑖‘6))
125		oveq1 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑖‘7) → (𝑒 − (𝑎‘1)) = ((𝑖‘7) − (𝑎‘1)))
126	125	3ad2ant3 1153	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑒 − (𝑎‘1)) = ((𝑖‘7) − (𝑎‘1)))
127	124, 126	breq12d 5124	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑑 ∥ (𝑒 − (𝑎‘1)) ↔ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1))))
128	121, 123, 127	3anbi123d 1464	. . . . . . . . . . . . . . 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 644	. . . . . . . . . . . . . 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 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑖‘7) → (𝑒 − 1) = ((𝑖‘7) − 1))
131	130	breq2d 5123	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = (𝑖‘7) → ((2 · (𝑎‘3)) ∥ (𝑒 − 1) ↔ (2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1)))
132		breq1 5114	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = (𝑖‘6) → (𝑑 ∥ ((𝑖‘8) − (𝑎‘3)) ↔ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))))
133	131, 132	bi2anan9r 651	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ↔ ((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3)))))
134	133	anbi1d 643	. . . . . . . . . . . . . . 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 1148	. . . . . . . . . . . . . 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 644	. . . . . . . . . . . . 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 3823	. . . . . . . . . . . 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 3802	. . . . . . . . . . 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 3802	. . . . . . . . . 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 3461	. . . . . . . . . . . 12 ⊢ 𝑖 ∈ V
141	140	resex 6030	. . . . . . . . . . 11 ⊢ (𝑖 ↾ (1...3)) ∈ V
142		fvex 6898	. . . . . . . . . . 11 ⊢ (𝑖‘4) ∈ V
143		oveq1 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑖‘4) → (𝑏↑2) = ((𝑖‘4)↑2))
144	62	jm2.27dlem1 43813	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘1) = (𝑖‘1))
145	144	oveq1d 7434	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘1)↑2) = ((𝑖‘1)↑2))
146	145	oveq1d 7434	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((𝑎‘1)↑2) − 1) = (((𝑖‘1)↑2) − 1))
147	68	jm2.27dlem1 43813	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘3) = (𝑖‘3))
148	147	oveq1d 7434	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘3)↑2) = ((𝑖‘3)↑2))
149	146, 148	oveq12d 7437	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2)) = ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2)))
150	143, 149	oveqan12rd 7439	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))))
151	150	eqeq1d 2767	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → (((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ↔ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1))
152	146	oveq1d 7434	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2)) = ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2)))
153	152	oveq2d 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))))
154	153	eqeq1d 2767	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ↔ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1))
155	154	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ↔ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1))
156	151, 155	3anbi12d 1465	. . . . . . . . . . . . 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 7435	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (2 · ((𝑎‘3)↑2)) = (2 · ((𝑖‘3)↑2)))
158	157	oveq2d 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))))
159	158	eqeq2d 2776	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))))
160	144	oveq2d 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘7) − (𝑎‘1)) = ((𝑖‘7) − (𝑖‘1)))
161	160	breq2d 5123	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)) ↔ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))))
162	159, 161	3anbi23d 1467	. . . . . . . . . . . . . 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 486	. . . . . . . . . . . . 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 644	. . . . . . . . . . . 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 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (2 · (𝑎‘3)) = (2 · (𝑖‘3)))
166	165	breq1d 5121	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ↔ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)))
167	147	oveq2d 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘8) − (𝑎‘3)) = ((𝑖‘8) − (𝑖‘3)))
168	167	breq2d 5123	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3)) ↔ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))))
169	166, 168	anbi12d 644	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ↔ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))))
170	5	jm2.27dlem1 43813	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘2) = (𝑖‘2))
171	170	oveq2d 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘8) − (𝑎‘2)) = ((𝑖‘8) − (𝑖‘2)))
172	165, 171	breq12d 5124	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ↔ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))))
173	170, 147	breq12d 5124	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘2) ≤ (𝑎‘3) ↔ (𝑖‘2) ≤ (𝑖‘3)))
174	172, 173	anbi12d 644	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)) ↔ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))))
175	169, 174	anbi12d 644	. . . . . . . . . . . . 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 486	. . . . . . . . . . . 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 644	. . . . . . . . . . 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 3821	. . . . . . . . . 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 300	. . . . . . . . 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 3423	. . . . . . . 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 12753	. . . . . . . . . . . 12 ⊢ ;10 ∈ ℕ0
182		ovex 7452	. . . . . . . . . . . . . . 15 ⊢ (1...;10) ∈ V
183		df-5 12325	. . . . . . . . . . . . . . . . 17 ⊢ 5 = (4 + 1)
184		df-6 12326	. . . . . . . . . . . . . . . . . 18 ⊢ 6 = (5 + 1)
185		df-7 12327	. . . . . . . . . . . . . . . . . . 19 ⊢ 7 = (6 + 1)
186		df-8 12328	. . . . . . . . . . . . . . . . . . . 20 ⊢ 8 = (7 + 1)
187		df-9 12329	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 9 = (8 + 1)
188		9p1e10 12733	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (9 + 1) = ;10
189	188	eqcomi 2774	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ;10 = (9 + 1)
190		ssid 3960	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1...;10) ⊆ (1...;10)
191	189, 190	jm2.27dlem5 43817	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1...9) ⊆ (1...;10)
192	187, 191	jm2.27dlem5 43817	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...8) ⊆ (1...;10)
193	186, 192	jm2.27dlem5 43817	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...7) ⊆ (1...;10)
194	185, 193	jm2.27dlem5 43817	. . . . . . . . . . . . . . . . . 18 ⊢ (1...6) ⊆ (1...;10)
195	184, 194	jm2.27dlem5 43817	. . . . . . . . . . . . . . . . 17 ⊢ (1...5) ⊆ (1...;10)
196	183, 195	jm2.27dlem5 43817	. . . . . . . . . . . . . . . 16 ⊢ (1...4) ⊆ (1...;10)
197		4nn 12343	. . . . . . . . . . . . . . . . 17 ⊢ 4 ∈ ℕ
198	197	jm2.27dlem3 43815	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ (1...4)
199	196, 198	sselii 3935	. . . . . . . . . . . . . . 15 ⊢ 4 ∈ (1...;10)
200		mzpproj 43545	. . . . . . . . . . . . . . 15 ⊢ (((1...;10) ∈ V ∧ 4 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘4)) ∈ (mzPoly‘(1...;10)))
201	182, 199, 200	mp2an 705	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘4)) ∈ (mzPoly‘(1...;10))
202		2nn0 12540	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ0
203		mzpexpmpt 43553	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘4)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘4)↑2)) ∈ (mzPoly‘(1...;10)))
204	201, 202, 203	mp2an 705	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘4)↑2)) ∈ (mzPoly‘(1...;10))
205		df-4 12324	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 4 = (3 + 1)
206	205, 196	jm2.27dlem5 43817	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...3) ⊆ (1...;10)
207	4, 206	jm2.27dlem5 43817	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...2) ⊆ (1...;10)
208	60, 207	jm2.27dlem5 43817	. . . . . . . . . . . . . . . . . 18 ⊢ (1...1) ⊆ (1...;10)
209	208, 59	sselii 3935	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ (1...;10)
210		mzpproj 43545	. . . . . . . . . . . . . . . . 17 ⊢ (((1...;10) ∈ V ∧ 1 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...;10)))
211	182, 209, 210	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...;10))
212		mzpexpmpt 43553	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘1)↑2)) ∈ (mzPoly‘(1...;10)))
213	211, 202, 212	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘1)↑2)) ∈ (mzPoly‘(1...;10))
214		1z 12643	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℤ
215		mzpconstmpt 43548	. . . . . . . . . . . . . . . 16 ⊢ (((1...;10) ∈ V ∧ 1 ∈ ℤ) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10)))
216	182, 214, 215	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))
217		mzpsubmpt 43551	. . . . . . . . . . . . . . 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 705	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘1)↑2) − 1)) ∈ (mzPoly‘(1...;10))
219	206, 68	sselii 3935	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ (1...;10)
220		mzpproj 43545	. . . . . . . . . . . . . . . 16 ⊢ (((1...;10) ∈ V ∧ 3 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...;10)))
221	182, 219, 220	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...;10))
222		mzpexpmpt 43553	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘3)↑2)) ∈ (mzPoly‘(1...;10)))
223	221, 202, 222	mp2an 705	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘3)↑2)) ∈ (mzPoly‘(1...;10))
224		mzpmulmpt 43550	. . . . . . . . . . . . . 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 705	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...;10))
226		mzpsubmpt 43551	. . . . . . . . . . . . 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 705	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2)))) ∈ (mzPoly‘(1...;10))
228		eqrabdioph 43585	. . . . . . . . . . . 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 1490	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1} ∈ (Dioph‘;10)
230		6nn 12349	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℕ
231	230	jm2.27dlem3 43815	. . . . . . . . . . . . . . . 16 ⊢ 6 ∈ (1...6)
232	194, 231	sselii 3935	. . . . . . . . . . . . . . 15 ⊢ 6 ∈ (1...;10)
233		mzpproj 43545	. . . . . . . . . . . . . . 15 ⊢ (((1...;10) ∈ V ∧ 6 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...;10)))
234	182, 232, 233	mp2an 705	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...;10))
235		mzpexpmpt 43553	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘6)↑2)) ∈ (mzPoly‘(1...;10)))
236	234, 202, 235	mp2an 705	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘6)↑2)) ∈ (mzPoly‘(1...;10))
237		5nn 12346	. . . . . . . . . . . . . . . . . 18 ⊢ 5 ∈ ℕ
238	237	jm2.27dlem3 43815	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ (1...5)
239	195, 238	sselii 3935	. . . . . . . . . . . . . . . 16 ⊢ 5 ∈ (1...;10)
240		mzpproj 43545	. . . . . . . . . . . . . . . 16 ⊢ (((1...;10) ∈ V ∧ 5 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...;10)))
241	182, 239, 240	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...;10))
242		mzpexpmpt 43553	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘5)↑2)) ∈ (mzPoly‘(1...;10)))
243	241, 202, 242	mp2an 705	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘5)↑2)) ∈ (mzPoly‘(1...;10))
244		mzpmulmpt 43550	. . . . . . . . . . . . . 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 705	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) ∈ (mzPoly‘(1...;10))
246		mzpsubmpt 43551	. . . . . . . . . . . . 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 705	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2)))) ∈ (mzPoly‘(1...;10))
248		eqrabdioph 43585	. . . . . . . . . . . 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 1490	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1} ∈ (Dioph‘;10)
250		7nn 12352	. . . . . . . . . . . . . . 15 ⊢ 7 ∈ ℕ
251	250	jm2.27dlem3 43815	. . . . . . . . . . . . . 14 ⊢ 7 ∈ (1...7)
252	193, 251	sselii 3935	. . . . . . . . . . . . 13 ⊢ 7 ∈ (1...;10)
253		mzpproj 43545	. . . . . . . . . . . . 13 ⊢ (((1...;10) ∈ V ∧ 7 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10)))
254	182, 252, 253	mp2an 705	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10))
255		eluzrabdioph 43610	. . . . . . . . . . . 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 1490	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (𝑖‘7) ∈ (ℤ≥‘2)} ∈ (Dioph‘;10)
257		3anrabdioph 43590	. . . . . . . . . . 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 1490	. . . . . . . . . 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 12358	. . . . . . . . . . . . . . . . 17 ⊢ 9 ∈ ℕ
260	259	jm2.27dlem3 43815	. . . . . . . . . . . . . . . 16 ⊢ 9 ∈ (1...9)
261	260, 189, 259	jm2.27dlem2 43814	. . . . . . . . . . . . . . 15 ⊢ 9 ∈ (1...;10)
262		mzpproj 43545	. . . . . . . . . . . . . . 15 ⊢ (((1...;10) ∈ V ∧ 9 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘9)) ∈ (mzPoly‘(1...;10)))
263	182, 261, 262	mp2an 705	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘9)) ∈ (mzPoly‘(1...;10))
264		mzpexpmpt 43553	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘9)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘9)↑2)) ∈ (mzPoly‘(1...;10)))
265	263, 202, 264	mp2an 705	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘9)↑2)) ∈ (mzPoly‘(1...;10))
266		mzpexpmpt 43553	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘7)↑2)) ∈ (mzPoly‘(1...;10)))
267	254, 202, 266	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘7)↑2)) ∈ (mzPoly‘(1...;10))
268		mzpsubmpt 43551	. . . . . . . . . . . . . . 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 705	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘7)↑2) − 1)) ∈ (mzPoly‘(1...;10))
270		8nn 12355	. . . . . . . . . . . . . . . . . 18 ⊢ 8 ∈ ℕ
271	270	jm2.27dlem3 43815	. . . . . . . . . . . . . . . . 17 ⊢ 8 ∈ (1...8)
272	192, 271	sselii 3935	. . . . . . . . . . . . . . . 16 ⊢ 8 ∈ (1...;10)
273		mzpproj 43545	. . . . . . . . . . . . . . . 16 ⊢ (((1...;10) ∈ V ∧ 8 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...;10)))
274	182, 272, 273	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...;10))
275		mzpexpmpt 43553	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘8)↑2)) ∈ (mzPoly‘(1...;10)))
276	274, 202, 275	mp2an 705	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘8)↑2)) ∈ (mzPoly‘(1...;10))
277		mzpmulmpt 43550	. . . . . . . . . . . . . 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 705	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) ∈ (mzPoly‘(1...;10))
279		mzpsubmpt 43551	. . . . . . . . . . . . 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 705	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2)))) ∈ (mzPoly‘(1...;10))
281		eqrabdioph 43585	. . . . . . . . . . . 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 1490	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1} ∈ (Dioph‘;10)
283		10nn 12751	. . . . . . . . . . . . . . . 16 ⊢ ;10 ∈ ℕ
284	283	jm2.27dlem3 43815	. . . . . . . . . . . . . . 15 ⊢ ;10 ∈ (1...;10)
285		mzpproj 43545	. . . . . . . . . . . . . . 15 ⊢ (((1...;10) ∈ V ∧ ;10 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘;10)) ∈ (mzPoly‘(1...;10)))
286	182, 284, 285	mp2an 705	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘;10)) ∈ (mzPoly‘(1...;10))
287		mzpaddmpt 43549	. . . . . . . . . . . . . 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 705	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘;10) + 1)) ∈ (mzPoly‘(1...;10))
289		mzpconstmpt 43548	. . . . . . . . . . . . . . 15 ⊢ (((1...;10) ∈ V ∧ 2 ∈ ℤ) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ 2) ∈ (mzPoly‘(1...;10)))
290	182, 56, 289	mp2an 705	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ 2) ∈ (mzPoly‘(1...;10))
291		mzpmulmpt 43550	. . . . . . . . . . . . . 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 705	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (2 · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...;10))
293		mzpmulmpt 43550	. . . . . . . . . . . . 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 705	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))) ∈ (mzPoly‘(1...;10))
295		eqrabdioph 43585	. . . . . . . . . . . 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 1490	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))} ∈ (Dioph‘;10)
297		mzpsubmpt 43551	. . . . . . . . . . . . 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 705	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘7) − (𝑖‘1))) ∈ (mzPoly‘(1...;10))
299		dvdsrabdioph 43614	. . . . . . . . . . . 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 1490	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))} ∈ (Dioph‘;10)
301		3anrabdioph 43590	. . . . . . . . . . 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 1490	. . . . . . . . . 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 43588	. . . . . . . . . 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 705	. . . . . . . . 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 43550	. . . . . . . . . . . . 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 705	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...;10))
307		mzpsubmpt 43551	. . . . . . . . . . . . 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 705	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘7) − 1)) ∈ (mzPoly‘(1...;10))
309		dvdsrabdioph 43614	. . . . . . . . . . . 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 1490	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)} ∈ (Dioph‘;10)
311		mzpsubmpt 43551	. . . . . . . . . . . . 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 705	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘8) − (𝑖‘3))) ∈ (mzPoly‘(1...;10))
313		dvdsrabdioph 43614	. . . . . . . . . . . 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 1490	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))} ∈ (Dioph‘;10)
315		anrabdioph 43588	. . . . . . . . . . 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 705	. . . . . . . . . 10 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))} ∈ (Dioph‘;10)
317	207, 3	sselii 3935	. . . . . . . . . . . . . 14 ⊢ 2 ∈ (1...;10)
318		mzpproj 43545	. . . . . . . . . . . . . 14 ⊢ (((1...;10) ∈ V ∧ 2 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...;10)))
319	182, 317, 318	mp2an 705	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...;10))
320		mzpsubmpt 43551	. . . . . . . . . . . . 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 705	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑m (1...;10)) ↦ ((𝑖‘8) − (𝑖‘2))) ∈ (mzPoly‘(1...;10))
322		dvdsrabdioph 43614	. . . . . . . . . . . 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 1490	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))} ∈ (Dioph‘;10)
324		lerabdioph 43609	. . . . . . . . . . . 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 1490	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (𝑖‘2) ≤ (𝑖‘3)} ∈ (Dioph‘;10)
326		anrabdioph 43588	. . . . . . . . . . 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 705	. . . . . . . . . 10 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))} ∈ (Dioph‘;10)
328		anrabdioph 43588	. . . . . . . . . 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 705	. . . . . . . . 9 ⊢ {𝑖 ∈ (ℕ0 ↑m (1...;10)) ∣ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))} ∈ (Dioph‘;10)
330		anrabdioph 43588	. . . . . . . . 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 705	. . . . . . . 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 2861	. . . . . . 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 43604	. . . . . . 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 705	. . . . . 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 43588	. . . . . 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 705	. . . . 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 43545	. . . . . . 7 ⊢ (((1...3) ∈ V ∧ 2 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑m (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3)))
338	57, 5, 337	mp2an 705	. . . . . 6 ⊢ (𝑎 ∈ (ℤ ↑m (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3))
339		elnnrabdioph 43611	. . . . . 6 ⊢ ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑m (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈ (Dioph‘3))
340	55, 338, 339	mp2an 705	. . . . 5 ⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈ (Dioph‘3)
341		anrabdioph 43588	. . . . 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 705	. . . 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 43584	. . . . . 6 ⊢ ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑m (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘3) = 0} ∈ (Dioph‘3))
344	55, 70, 343	mp2an 705	. . . . 5 ⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘3) = 0} ∈ (Dioph‘3)
345		eq0rabdioph 43584	. . . . . 6 ⊢ ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑m (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘2) = 0} ∈ (Dioph‘3))
346	55, 338, 345	mp2an 705	. . . . 5 ⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘2) = 0} ∈ (Dioph‘3)
347		anrabdioph 43588	. . . . 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 705	. . . 4 ⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)} ∈ (Dioph‘3)
349		orrabdioph 43589	. . . 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 705	. . 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 43588	. . 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 705	. 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 2861	1 ⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} ∈ (Dioph‘3)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  ∃wrex 3091  {crab 3418  Vcvv 3457  [wsbc 3746   class class class wbr 5111   ↦ cmpt 5194   ↾ cres 5665  ⟶wf 6536  ‘cfv 6540  (class class class)co 7419   ↑_m cmap 8830  0cc0 11119  1c1 11120   + caddc 11122   · cmul 11124   < clt 11262   ≤ cle 11263   − cmin 11460  ℕcn 12252  2c2 12314  3c3 12315  4c4 12316  5c5 12317  6c6 12318  7c7 12319  8c8 12320  9c9 12321  ℕ₀cn0 12523  ℤcz 12610  ;cdc 12731  ℤ_≥cuz 12882  ...cfz 13555  ↑cexp 14119   ∥ cdvds 16336  mzPolycmzp 43530  Diophcdioph 43563   Y_rm crmy 43705

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-inf2 9617  ax-cnex 11175  ax-resscn 11176  ax-1cn 11177  ax-icn 11178  ax-addcl 11179  ax-addrcl 11180  ax-mulcl 11181  ax-mulrcl 11182  ax-mulcom 11183  ax-addass 11184  ax-mulass 11185  ax-distr 11186  ax-i2m1 11187  ax-1ne0 11188  ax-1rid 11189  ax-rnegex 11190  ax-rrecex 11191  ax-cnre 11192  ax-pre-lttri 11193  ax-pre-lttrn 11194  ax-pre-ltadd 11195  ax-pre-mulgt0 11196  ax-pre-sup 11197  ax-addf 11198

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-iin 4961  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-se 5617  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-of 7684  df-om 7869  df-1st 7992  df-2nd 7993  df-supp 8163  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-1o 8459  df-2o 8460  df-oadd 8463  df-omul 8464  df-er 8700  df-map 8832  df-pm 8833  df-ixp 8902  df-en 8950  df-dom 8951  df-sdom 8952  df-fin 8953  df-fsupp 9329  df-fi 9378  df-sup 9409  df-inf 9410  df-oi 9479  df-dju 9903  df-card 9941  df-acn 9944  df-pnf 11264  df-mnf 11265  df-xr 11266  df-ltxr 11267  df-le 11268  df-sub 11462  df-neg 11463  df-div 11891  df-nn 12253  df-2 12322  df-3 12323  df-4 12324  df-5 12325  df-6 12326  df-7 12327  df-8 12328  df-9 12329  df-n0 12524  df-xnn0 12597  df-z 12611  df-dec 12732  df-uz 12883  df-q 12993  df-rp 13037  df-xneg 13157  df-xadd 13158  df-xmul 13159  df-ioo 13396  df-ioc 13397  df-ico 13398  df-icc 13399  df-fz 13556  df-fzo 13704  df-fl 13847  df-mod 13925  df-seq 14060  df-exp 14120  df-fac 14332  df-bc 14361  df-hash 14389  df-shft 15132  df-cj 15178  df-re 15179  df-im 15180  df-sqrt 15314  df-abs 15315  df-limsup 15550  df-clim 15567  df-rlim 15568  df-sum 15766  df-ef 16147  df-sin 16149  df-cos 16150  df-pi 16152  df-dvds 16337  df-gcd 16579  df-prm 16756  df-numer 16820  df-denom 16821  df-struct 17233  df-sets 17250  df-slot 17268  df-ndx 17280  df-base 17296  df-ress 17317  df-plusg 17349  df-mulr 17350  df-starv 17351  df-sca 17352  df-vsca 17353  df-ip 17354  df-tset 17355  df-ple 17356  df-ds 17358  df-unif 17359  df-hom 17360  df-cco 17361  df-rest 17501  df-topn 17502  df-0g 17520  df-gsum 17521  df-topgen 17522  df-pt 17523  df-prds 17526  df-xrs 17582  df-qtop 17587  df-imas 17588  df-xps 17590  df-mre 17664  df-mrc 17665  df-acs 17667  df-mgm 18724  df-sgrp 18813  df-mnd 18829  df-submnd 18883  df-mulg 19182  df-cntz 19435  df-cmn 19900  df-psmet 21568  df-xmet 21569  df-met 21570  df-bl 21571  df-mopn 21572  df-fbas 21573  df-fg 21574  df-cnfld 21577  df-top 23105  df-topon 23122  df-topsp 23144  df-bases 23157  df-cld 23230  df-ntr 23231  df-cls 23232  df-nei 23309  df-lp 23347  df-perf 23348  df-cn 23438  df-cnp 23439  df-haus 23526  df-tx 23774  df-hmeo 23967  df-fil 24058  df-fm 24150  df-flim 24151  df-flf 24152  df-xms 24532  df-ms 24533  df-tms 24534  df-cncf 25092  df-limc 26080  df-dv 26081  df-log 26776  df-mzpcl 43531  df-mzp 43532  df-dioph 43564  df-squarenn 43645  df-pell1qr 43646  df-pell14qr 43647  df-pell1234qr 43648  df-pellfund 43649  df-rmx 43706  df-rmy 43707

This theorem is used by:  rmxdioph  43820  expdiophlem2  43826