Theorem rmydioph 37581

Description: jm2.27 37575 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 ↑𝑚 (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 7879	. . . . . . 7 ⊢ (𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) → 𝑎:(1...3)⟶ℕ0)
2		2nn 11185	. . . . . . . . 9 ⊢ 2 ∈ ℕ
3	2	jm2.27dlem3 37578	. . . . . . . 8 ⊢ 2 ∈ (1...2)
4		df-3 11080	. . . . . . . 8 ⊢ 3 = (2 + 1)
5	3, 4, 2	jm2.27dlem2 37577	. . . . . . 7 ⊢ 2 ∈ (1...3)
6		ffvelrn 6357	. . . . . . 7 ⊢ ((𝑎:(1...3)⟶ℕ0 ∧ 2 ∈ (1...3)) → (𝑎‘2) ∈ ℕ0)
7	1, 5, 6	sylancl 694	. . . . . 6 ⊢ (𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) → (𝑎‘2) ∈ ℕ0)
8		elnn0 11294	. . . . . 6 ⊢ ((𝑎‘2) ∈ ℕ0 ↔ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0))
9	7, 8	sylib 208	. . . . 5 ⊢ (𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) → ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0))
10		iba 524	. . . . . . 7 ⊢ (((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0))))
11		andi 911	. . . . . . 7 ⊢ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0)) ↔ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0)))
12	10, 11	syl6bb 276	. . . . . 6 ⊢ (((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0))))
13	12	anbi2d 740	. . . . 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 ↑𝑚 (1...3)) → (((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2))) ↔ ((𝑎‘1) ∈ (ℤ≥‘2) ∧ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0)))))
15		simplr 792	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → (𝑎‘1) ∈ (ℤ≥‘2))
16		nnz 11399	. . . . . . . . . . . . . 14 ⊢ ((𝑎‘2) ∈ ℕ → (𝑎‘2) ∈ ℤ)
17	16	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → (𝑎‘2) ∈ ℤ)
18		frmy 37479	. . . . . . . . . . . . . 14 ⊢ Yrm :((ℤ≥‘2) × ℤ)⟶ℤ
19	18	fovcl 6765	. . . . . . . . . . . . 13 ⊢ (((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘2) ∈ ℤ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℤ)
20	15, 17, 19	syl2anc 693	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℤ)
21		rmy0 37494	. . . . . . . . . . . . . 14 ⊢ ((𝑎‘1) ∈ (ℤ≥‘2) → ((𝑎‘1) Yrm 0) = 0)
22	21	ad2antlr 763	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm 0) = 0)
23		nngt0 11049	. . . . . . . . . . . . . . 15 ⊢ ((𝑎‘2) ∈ ℕ → 0 < (𝑎‘2))
24	23	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 < (𝑎‘2))
25		0zd 11389	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 ∈ ℤ)
26		ltrmy 37519	. . . . . . . . . . . . . . 15 ⊢ (((𝑎‘1) ∈ (ℤ≥‘2) ∧ 0 ∈ ℤ ∧ (𝑎‘2) ∈ ℤ) → (0 < (𝑎‘2) ↔ ((𝑎‘1) Yrm 0) < ((𝑎‘1) Yrm (𝑎‘2))))
27	15, 25, 17, 26	syl3anc 1326	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → (0 < (𝑎‘2) ↔ ((𝑎‘1) Yrm 0) < ((𝑎‘1) Yrm (𝑎‘2))))
28	24, 27	mpbid 222	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm 0) < ((𝑎‘1) Yrm (𝑎‘2)))
29	22, 28	eqbrtrrd 4677	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 < ((𝑎‘1) Yrm (𝑎‘2)))
30		elnnz 11387	. . . . . . . . . . . 12 ⊢ (((𝑎‘1) Yrm (𝑎‘2)) ∈ ℕ ↔ (((𝑎‘1) Yrm (𝑎‘2)) ∈ ℤ ∧ 0 < ((𝑎‘1) Yrm (𝑎‘2))))
31	20, 29, 30	sylanbrc 698	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℕ)
32		eleq1 2689	. . . . . . . . . . 11 ⊢ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) → ((𝑎‘3) ∈ ℕ ↔ ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℕ))
33	31, 32	syl5ibrcom 237	. . . . . . . . . 10 ⊢ (((𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) → (𝑎‘3) ∈ ℕ))
34	33	pm4.71rd 667	. . . . . . . . 9 ⊢ (((𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ((𝑎‘3) ∈ ℕ ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))))
35		simpllr 799	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) → (𝑎‘1) ∈ (ℤ≥‘2))
36		simplr 792	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) → (𝑎‘2) ∈ ℕ)
37		simpr 477	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) → (𝑎‘3) ∈ ℕ)
38		jm2.27 37575	. . . . . . . . . . 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 1326	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ (ℕ0 ↑𝑚 (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 673	. . . . . . . . 9 ⊢ (((𝑎 ∈ (ℕ0 ↑𝑚 (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 268	. . . . . . . 8 ⊢ (((𝑎 ∈ (ℕ0 ↑𝑚 (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 450	. . . . . . 7 ⊢ ((𝑎 ∈ (ℕ0 ↑𝑚 (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 672	. . . . . 6 ⊢ ((𝑎 ∈ (ℕ0 ↑𝑚 (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 6658	. . . . . . . . . . 11 ⊢ ((𝑎‘2) = 0 → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑎‘1) Yrm 0))
45	44	adantl 482	. . . . . . . . . 10 ⊢ (((𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑎‘1) Yrm 0))
46	21	ad2antlr 763	. . . . . . . . . 10 ⊢ (((𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm 0) = 0)
47	45, 46	eqtrd 2656	. . . . . . . . 9 ⊢ (((𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm (𝑎‘2)) = 0)
48	47	eqeq2d 2632	. . . . . . . 8 ⊢ (((𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (𝑎‘3) = 0))
49	48	ex 450	. . . . . . 7 ⊢ ((𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) → ((𝑎‘2) = 0 → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (𝑎‘3) = 0)))
50	49	pm5.32rd 672	. . . . . 6 ⊢ ((𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ≥‘2)) → (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0) ↔ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)))
51	43, 50	orbi12d 746	. . . . 5 ⊢ ((𝑎 ∈ (ℕ0 ↑𝑚 (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 673	. . . 4 ⊢ (𝑎 ∈ (ℕ0 ↑𝑚 (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 268	. . 3 ⊢ (𝑎 ∈ (ℕ0 ↑𝑚 (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 3185	. 2 ⊢ {𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ ((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} = {𝑎 ∈ (ℕ0 ↑𝑚 (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 11310	. . . 4 ⊢ 3 ∈ ℕ0
56		2z 11409	. . . 4 ⊢ 2 ∈ ℤ
57		ovex 6678	. . . . 5 ⊢ (1...3) ∈ V
58		1nn 11031	. . . . . . . 8 ⊢ 1 ∈ ℕ
59	58	jm2.27dlem3 37578	. . . . . . 7 ⊢ 1 ∈ (1...1)
60		df-2 11079	. . . . . . 7 ⊢ 2 = (1 + 1)
61	59, 60, 58	jm2.27dlem2 37577	. . . . . 6 ⊢ 1 ∈ (1...2)
62	61, 4, 2	jm2.27dlem2 37577	. . . . 5 ⊢ 1 ∈ (1...3)
63		mzpproj 37300	. . . . 5 ⊢ (((1...3) ∈ V ∧ 1 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘1)) ∈ (mzPoly‘(1...3)))
64	57, 62, 63	mp2an 708	. . . 4 ⊢ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘1)) ∈ (mzPoly‘(1...3))
65		eluzrabdioph 37370	. . . 4 ⊢ ((3 ∈ ℕ0 ∧ 2 ∈ ℤ ∧ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘1)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ (𝑎‘1) ∈ (ℤ≥‘2)} ∈ (Dioph‘3))
66	55, 56, 64, 65	mp3an 1424	. . 3 ⊢ {𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ (𝑎‘1) ∈ (ℤ≥‘2)} ∈ (Dioph‘3)
67		3nn 11186	. . . . . . . . 9 ⊢ 3 ∈ ℕ
68	67	jm2.27dlem3 37578	. . . . . . . 8 ⊢ 3 ∈ (1...3)
69		mzpproj 37300	. . . . . . . 8 ⊢ (((1...3) ∈ V ∧ 3 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3)))
70	57, 68, 69	mp2an 708	. . . . . . 7 ⊢ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3))
71		elnnrabdioph 37371	. . . . . . 7 ⊢ ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ (𝑎‘3) ∈ ℕ} ∈ (Dioph‘3))
72	55, 70, 71	mp2an 708	. . . . . 6 ⊢ {𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ (𝑎‘3) ∈ ℕ} ∈ (Dioph‘3)
73		fvex 6201	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖‘8) ∈ V
74		fvex 6201	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖‘9) ∈ V
75		fvex 6201	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖‘;10) ∈ V
76		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 = (𝑖‘9) → (𝑔↑2) = ((𝑖‘9)↑2))
77		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = (𝑖‘8) → (𝑓↑2) = ((𝑖‘8)↑2))
78	77	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = (𝑖‘8) → (((𝑒↑2) − 1) · (𝑓↑2)) = (((𝑒↑2) − 1) · ((𝑖‘8)↑2)))
79	76, 78	oveqan12rd 6670	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9)) → ((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))))
80	79	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9)) → (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ↔ (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1))
81	80	3adant3 1081	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ ℎ = (𝑖‘;10)) → (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ↔ (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1))
82		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = (𝑖‘;10) → (ℎ + 1) = ((𝑖‘;10) + 1))
83	82	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ = (𝑖‘;10) → ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))))
84	83	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ = (𝑖‘;10) → (𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ↔ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2)))))
85	84	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ ℎ = (𝑖‘;10)) → (𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ↔ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2)))))
86	81, 85	3anbi12d 1400	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 = (𝑖‘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 740	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 = (𝑖‘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 6657	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = (𝑖‘8) → (𝑓 − (𝑎‘3)) = ((𝑖‘8) − (𝑎‘3)))
89	88	breq2d 4665	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑖‘8) → (𝑑 ∥ (𝑓 − (𝑎‘3)) ↔ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))))
90	89	anbi2d 740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑖‘8) → (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ↔ ((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3)))))
91		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = (𝑖‘8) → (𝑓 − (𝑎‘2)) = ((𝑖‘8) − (𝑎‘2)))
92	91	breq2d 4665	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑖‘8) → ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ↔ (2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2))))
93	92	anbi1d 741	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑖‘8) → (((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)) ↔ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))
94	90, 93	anbi12d 747	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑖‘8) → ((((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))) ↔ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))
95	94	3ad2ant1 1082	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 = (𝑖‘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 747	. . . . . . . . . . . . . . . . 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 · (𝑎‘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 3507	. . . . . . . . . . . . . . . 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)))))
98	97	sbcbii 3491	. . . . . . . . . . . . . . 15 ⊢ ([(𝑖‘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 3491	. . . . . . . . . . . . . 14 ⊢ ([(𝑖‘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 3491	. . . . . . . . . . . . 13 ⊢ ([(𝑖‘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 3491	. . . . . . . . . . . 12 ⊢ ([(𝑖‘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 3491	. . . . . . . . . . 11 ⊢ ([(𝑖 ↾ (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 6201	. . . . . . . . . . . . . 14 ⊢ (𝑖‘5) ∈ V
104		fvex 6201	. . . . . . . . . . . . . 14 ⊢ (𝑖‘6) ∈ V
105		fvex 6201	. . . . . . . . . . . . . 14 ⊢ (𝑖‘7) ∈ V
106		oveq1 6657	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = (𝑖‘6) → (𝑑↑2) = ((𝑖‘6)↑2))
107	106	3ad2ant2 1083	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑑↑2) = ((𝑖‘6)↑2))
108		oveq1 6657	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = (𝑖‘5) → (𝑐↑2) = ((𝑖‘5)↑2))
109	108	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑖‘5) → ((((𝑎‘1)↑2) − 1) · (𝑐↑2)) = ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2)))
110	109	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((𝑎‘1)↑2) − 1) · (𝑐↑2)) = ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2)))
111	107, 110	oveq12d 6668	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))))
112	111	eqeq1d 2624	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ↔ (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1))
113		eleq1 2689	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑖‘7) → (𝑒 ∈ (ℤ≥‘2) ↔ (𝑖‘7) ∈ (ℤ≥‘2)))
114	113	3ad2ant3 1084	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑒 ∈ (ℤ≥‘2) ↔ (𝑖‘7) ∈ (ℤ≥‘2)))
115	112, 114	3anbi23d 1402	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = (𝑖‘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 6657	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑒 = (𝑖‘7) → (𝑒↑2) = ((𝑖‘7)↑2))
117	116	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = (𝑖‘7) → ((𝑒↑2) − 1) = (((𝑖‘7)↑2) − 1))
118	117	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = (𝑖‘7) → (((𝑒↑2) − 1) · ((𝑖‘8)↑2)) = ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2)))
119	118	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖‘7) → (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))))
120	119	eqeq1d 2624	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑖‘7) → ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ↔ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1))
121	120	3ad2ant3 1084	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ↔ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1))
122		eqeq1 2626	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑖‘5) → (𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2)))))
123	122	3ad2ant1 1082	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2)))))
124		simp2 1062	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → 𝑑 = (𝑖‘6))
125		oveq1 6657	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖‘7) → (𝑒 − (𝑎‘1)) = ((𝑖‘7) − (𝑎‘1)))
126	125	3ad2ant3 1084	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑒 − (𝑎‘1)) = ((𝑖‘7) − (𝑎‘1)))
127	124, 126	breq12d 4666	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑑 ∥ (𝑒 − (𝑎‘1)) ↔ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1))))
128	121, 123, 127	3anbi123d 1399	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = (𝑖‘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 747	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 = (𝑖‘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 6657	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖‘7) → (𝑒 − 1) = ((𝑖‘7) − 1))
131	130	breq2d 4665	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑖‘7) → ((2 · (𝑎‘3)) ∥ (𝑒 − 1) ↔ (2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1)))
132		breq1 4656	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = (𝑖‘6) → (𝑑 ∥ ((𝑖‘8) − (𝑎‘3)) ↔ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))))
133	131, 132	bi2anan9r 918	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ↔ ((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3)))))
134	133	anbi1d 741	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 = (𝑖‘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 1079	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 = (𝑖‘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 747	. . . . . . . . . . . . . 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 · (𝑎‘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 3507	. . . . . . . . . . . . 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)))))
138	137	sbcbii 3491	. . . . . . . . . . . 12 ⊢ ([(𝑖‘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 3491	. . . . . . . . . . 11 ⊢ ([(𝑖 ↾ (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 3203	. . . . . . . . . . . . 13 ⊢ 𝑖 ∈ V
141	140	resex 5443	. . . . . . . . . . . 12 ⊢ (𝑖 ↾ (1...3)) ∈ V
142		fvex 6201	. . . . . . . . . . . 12 ⊢ (𝑖‘4) ∈ V
143		oveq1 6657	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑖‘4) → (𝑏↑2) = ((𝑖‘4)↑2))
144	62	jm2.27dlem1 37576	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘1) = (𝑖‘1))
145	144	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘1)↑2) = ((𝑖‘1)↑2))
146	145	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((𝑎‘1)↑2) − 1) = (((𝑖‘1)↑2) − 1))
147	68	jm2.27dlem1 37576	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘3) = (𝑖‘3))
148	147	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘3)↑2) = ((𝑖‘3)↑2))
149	146, 148	oveq12d 6668	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2)) = ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2)))
150	143, 149	oveqan12rd 6670	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))))
151	150	eqeq1d 2624	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → (((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ↔ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1))
152	146	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2)) = ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2)))
153	152	oveq2d 6666	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))))
154	153	eqeq1d 2624	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ↔ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1))
155	154	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ↔ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1))
156	151, 155	3anbi12d 1400	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = (𝑖 ↾ (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 6666	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (2 · ((𝑎‘3)↑2)) = (2 · ((𝑖‘3)↑2)))
158	157	oveq2d 6666	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))))
159	158	eqeq2d 2632	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))))
160	144	oveq2d 6666	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘7) − (𝑎‘1)) = ((𝑖‘7) − (𝑖‘1)))
161	160	breq2d 4665	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)) ↔ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))))
162	159, 161	3anbi23d 1402	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑖 ↾ (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 481	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = (𝑖 ↾ (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 747	. . . . . . . . . . . . 13 ⊢ ((𝑎 = (𝑖 ↾ (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 6666	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (2 · (𝑎‘3)) = (2 · (𝑖‘3)))
166	165	breq1d 4663	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ↔ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)))
167	147	oveq2d 6666	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘8) − (𝑎‘3)) = ((𝑖‘8) − (𝑖‘3)))
168	167	breq2d 4665	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3)) ↔ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))))
169	166, 168	anbi12d 747	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ↔ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))))
170	5	jm2.27dlem1 37576	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘2) = (𝑖‘2))
171	170	oveq2d 6666	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘8) − (𝑎‘2)) = ((𝑖‘8) − (𝑖‘2)))
172	165, 171	breq12d 4666	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ↔ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))))
173	170, 147	breq12d 4666	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘2) ≤ (𝑎‘3) ↔ (𝑖‘2) ≤ (𝑖‘3)))
174	172, 173	anbi12d 747	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)) ↔ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))))
175	169, 174	anbi12d 747	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝑖 ↾ (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 481	. . . . . . . . . . . . 13 ⊢ ((𝑎 = (𝑖 ↾ (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 747	. . . . . . . . . . . 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)))) ∧ (((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 3505	. . . . . . . . . . 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)))))
179	102, 139, 178	3bitri 286	. . . . . . . . . 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)))) ↔ ((((((𝑖‘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	a1i 11	. . . . . . . . 9 ⊢ (𝑖 ∈ (ℕ0 ↑𝑚 (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)))) ↔ ((((((𝑖‘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	180	rabbiia 3185	. . . . . . . 8 ⊢ {𝑖 ∈ (ℕ0 ↑𝑚 (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 ↑𝑚 (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))))}
182		10nn0 11516	. . . . . . . . . . . 12 ⊢ ;10 ∈ ℕ0
183		ovex 6678	. . . . . . . . . . . . . . 15 ⊢ (1...;10) ∈ V
184		df-5 11082	. . . . . . . . . . . . . . . . 17 ⊢ 5 = (4 + 1)
185		df-6 11083	. . . . . . . . . . . . . . . . . 18 ⊢ 6 = (5 + 1)
186		df-7 11084	. . . . . . . . . . . . . . . . . . 19 ⊢ 7 = (6 + 1)
187		df-8 11085	. . . . . . . . . . . . . . . . . . . 20 ⊢ 8 = (7 + 1)
188		df-9 11086	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 9 = (8 + 1)
189		9p1e10 11496	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (9 + 1) = ;10
190	189	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ;10 = (9 + 1)
191		ssid 3624	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1...;10) ⊆ (1...;10)
192	190, 191	jm2.27dlem5 37580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1...9) ⊆ (1...;10)
193	188, 192	jm2.27dlem5 37580	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...8) ⊆ (1...;10)
194	187, 193	jm2.27dlem5 37580	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...7) ⊆ (1...;10)
195	186, 194	jm2.27dlem5 37580	. . . . . . . . . . . . . . . . . 18 ⊢ (1...6) ⊆ (1...;10)
196	185, 195	jm2.27dlem5 37580	. . . . . . . . . . . . . . . . 17 ⊢ (1...5) ⊆ (1...;10)
197	184, 196	jm2.27dlem5 37580	. . . . . . . . . . . . . . . 16 ⊢ (1...4) ⊆ (1...;10)
198		4nn 11187	. . . . . . . . . . . . . . . . 17 ⊢ 4 ∈ ℕ
199	198	jm2.27dlem3 37578	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ (1...4)
200	197, 199	sselii 3600	. . . . . . . . . . . . . . 15 ⊢ 4 ∈ (1...;10)
201		mzpproj 37300	. . . . . . . . . . . . . . 15 ⊢ (((1...;10) ∈ V ∧ 4 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘4)) ∈ (mzPoly‘(1...;10)))
202	183, 200, 201	mp2an 708	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘4)) ∈ (mzPoly‘(1...;10))
203		2nn0 11309	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ0
204		mzpexpmpt 37308	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘4)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘4)↑2)) ∈ (mzPoly‘(1...;10)))
205	202, 203, 204	mp2an 708	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘4)↑2)) ∈ (mzPoly‘(1...;10))
206		df-4 11081	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 4 = (3 + 1)
207	206, 197	jm2.27dlem5 37580	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...3) ⊆ (1...;10)
208	4, 207	jm2.27dlem5 37580	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...2) ⊆ (1...;10)
209	60, 208	jm2.27dlem5 37580	. . . . . . . . . . . . . . . . . 18 ⊢ (1...1) ⊆ (1...;10)
210	209, 59	sselii 3600	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ (1...;10)
211		mzpproj 37300	. . . . . . . . . . . . . . . . 17 ⊢ (((1...;10) ∈ V ∧ 1 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...;10)))
212	183, 210, 211	mp2an 708	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...;10))
213		mzpexpmpt 37308	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘1)↑2)) ∈ (mzPoly‘(1...;10)))
214	212, 203, 213	mp2an 708	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘1)↑2)) ∈ (mzPoly‘(1...;10))
215		1z 11407	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℤ
216		mzpconstmpt 37303	. . . . . . . . . . . . . . . 16 ⊢ (((1...;10) ∈ V ∧ 1 ∈ ℤ) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10)))
217	183, 215, 216	mp2an 708	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))
218		mzpsubmpt 37306	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘1)↑2)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (((𝑖‘1)↑2) − 1)) ∈ (mzPoly‘(1...;10)))
219	214, 217, 218	mp2an 708	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (((𝑖‘1)↑2) − 1)) ∈ (mzPoly‘(1...;10))
220	207, 68	sselii 3600	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ (1...;10)
221		mzpproj 37300	. . . . . . . . . . . . . . . 16 ⊢ (((1...;10) ∈ V ∧ 3 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...;10)))
222	183, 220, 221	mp2an 708	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...;10))
223		mzpexpmpt 37308	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘3)↑2)) ∈ (mzPoly‘(1...;10)))
224	222, 203, 223	mp2an 708	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘3)↑2)) ∈ (mzPoly‘(1...;10))
225		mzpmulmpt 37305	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (((𝑖‘1)↑2) − 1)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘3)↑2)) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...;10)))
226	219, 224, 225	mp2an 708	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...;10))
227		mzpsubmpt 37306	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘4)↑2)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2)))) ∈ (mzPoly‘(1...;10)))
228	205, 226, 227	mp2an 708	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2)))) ∈ (mzPoly‘(1...;10))
229		eqrabdioph 37341	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2)))) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1} ∈ (Dioph‘;10))
230	182, 228, 217, 229	mp3an 1424	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1} ∈ (Dioph‘;10)
231		6nn 11189	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℕ
232	231	jm2.27dlem3 37578	. . . . . . . . . . . . . . . 16 ⊢ 6 ∈ (1...6)
233	195, 232	sselii 3600	. . . . . . . . . . . . . . 15 ⊢ 6 ∈ (1...;10)
234		mzpproj 37300	. . . . . . . . . . . . . . 15 ⊢ (((1...;10) ∈ V ∧ 6 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...;10)))
235	183, 233, 234	mp2an 708	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...;10))
236		mzpexpmpt 37308	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘6)↑2)) ∈ (mzPoly‘(1...;10)))
237	235, 203, 236	mp2an 708	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘6)↑2)) ∈ (mzPoly‘(1...;10))
238		5nn 11188	. . . . . . . . . . . . . . . . . 18 ⊢ 5 ∈ ℕ
239	238	jm2.27dlem3 37578	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ (1...5)
240	196, 239	sselii 3600	. . . . . . . . . . . . . . . 16 ⊢ 5 ∈ (1...;10)
241		mzpproj 37300	. . . . . . . . . . . . . . . 16 ⊢ (((1...;10) ∈ V ∧ 5 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...;10)))
242	183, 240, 241	mp2an 708	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...;10))
243		mzpexpmpt 37308	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘5)↑2)) ∈ (mzPoly‘(1...;10)))
244	242, 203, 243	mp2an 708	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘5)↑2)) ∈ (mzPoly‘(1...;10))
245		mzpmulmpt 37305	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (((𝑖‘1)↑2) − 1)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘5)↑2)) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) ∈ (mzPoly‘(1...;10)))
246	219, 244, 245	mp2an 708	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) ∈ (mzPoly‘(1...;10))
247		mzpsubmpt 37306	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘6)↑2)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2)))) ∈ (mzPoly‘(1...;10)))
248	237, 246, 247	mp2an 708	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2)))) ∈ (mzPoly‘(1...;10))
249		eqrabdioph 37341	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2)))) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1} ∈ (Dioph‘;10))
250	182, 248, 217, 249	mp3an 1424	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1} ∈ (Dioph‘;10)
251		7nn 11190	. . . . . . . . . . . . . . 15 ⊢ 7 ∈ ℕ
252	251	jm2.27dlem3 37578	. . . . . . . . . . . . . 14 ⊢ 7 ∈ (1...7)
253	194, 252	sselii 3600	. . . . . . . . . . . . 13 ⊢ 7 ∈ (1...;10)
254		mzpproj 37300	. . . . . . . . . . . . 13 ⊢ (((1...;10) ∈ V ∧ 7 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10)))
255	183, 253, 254	mp2an 708	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10))
256		eluzrabdioph 37370	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℕ0 ∧ 2 ∈ ℤ ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (𝑖‘7) ∈ (ℤ≥‘2)} ∈ (Dioph‘;10))
257	182, 56, 255, 256	mp3an 1424	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (𝑖‘7) ∈ (ℤ≥‘2)} ∈ (Dioph‘;10)
258		3anrabdioph 37346	. . . . . . . . . . 11 ⊢ (({𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (𝑖‘7) ∈ (ℤ≥‘2)} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ ((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2))} ∈ (Dioph‘;10))
259	230, 250, 257, 258	mp3an 1424	. . . . . . . . . 10 ⊢ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ ((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2))} ∈ (Dioph‘;10)
260		9nn 11192	. . . . . . . . . . . . . . . . 17 ⊢ 9 ∈ ℕ
261	260	jm2.27dlem3 37578	. . . . . . . . . . . . . . . 16 ⊢ 9 ∈ (1...9)
262	261, 190, 260	jm2.27dlem2 37577	. . . . . . . . . . . . . . 15 ⊢ 9 ∈ (1...;10)
263		mzpproj 37300	. . . . . . . . . . . . . . 15 ⊢ (((1...;10) ∈ V ∧ 9 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘9)) ∈ (mzPoly‘(1...;10)))
264	183, 262, 263	mp2an 708	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘9)) ∈ (mzPoly‘(1...;10))
265		mzpexpmpt 37308	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘9)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘9)↑2)) ∈ (mzPoly‘(1...;10)))
266	264, 203, 265	mp2an 708	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘9)↑2)) ∈ (mzPoly‘(1...;10))
267		mzpexpmpt 37308	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘7)↑2)) ∈ (mzPoly‘(1...;10)))
268	255, 203, 267	mp2an 708	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘7)↑2)) ∈ (mzPoly‘(1...;10))
269		mzpsubmpt 37306	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘7)↑2)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (((𝑖‘7)↑2) − 1)) ∈ (mzPoly‘(1...;10)))
270	268, 217, 269	mp2an 708	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (((𝑖‘7)↑2) − 1)) ∈ (mzPoly‘(1...;10))
271		8nn 11191	. . . . . . . . . . . . . . . . . 18 ⊢ 8 ∈ ℕ
272	271	jm2.27dlem3 37578	. . . . . . . . . . . . . . . . 17 ⊢ 8 ∈ (1...8)
273	193, 272	sselii 3600	. . . . . . . . . . . . . . . 16 ⊢ 8 ∈ (1...;10)
274		mzpproj 37300	. . . . . . . . . . . . . . . 16 ⊢ (((1...;10) ∈ V ∧ 8 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...;10)))
275	183, 273, 274	mp2an 708	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...;10))
276		mzpexpmpt 37308	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘8)↑2)) ∈ (mzPoly‘(1...;10)))
277	275, 203, 276	mp2an 708	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘8)↑2)) ∈ (mzPoly‘(1...;10))
278		mzpmulmpt 37305	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (((𝑖‘7)↑2) − 1)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘8)↑2)) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) ∈ (mzPoly‘(1...;10)))
279	270, 277, 278	mp2an 708	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) ∈ (mzPoly‘(1...;10))
280		mzpsubmpt 37306	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘9)↑2)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2)))) ∈ (mzPoly‘(1...;10)))
281	266, 279, 280	mp2an 708	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2)))) ∈ (mzPoly‘(1...;10))
282		eqrabdioph 37341	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2)))) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1} ∈ (Dioph‘;10))
283	182, 281, 217, 282	mp3an 1424	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1} ∈ (Dioph‘;10)
284		10nn 11514	. . . . . . . . . . . . . . . 16 ⊢ ;10 ∈ ℕ
285	284	jm2.27dlem3 37578	. . . . . . . . . . . . . . 15 ⊢ ;10 ∈ (1...;10)
286		mzpproj 37300	. . . . . . . . . . . . . . 15 ⊢ (((1...;10) ∈ V ∧ ;10 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘;10)) ∈ (mzPoly‘(1...;10)))
287	183, 285, 286	mp2an 708	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘;10)) ∈ (mzPoly‘(1...;10))
288		mzpaddmpt 37304	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘;10)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘;10) + 1)) ∈ (mzPoly‘(1...;10)))
289	287, 217, 288	mp2an 708	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘;10) + 1)) ∈ (mzPoly‘(1...;10))
290		mzpconstmpt 37303	. . . . . . . . . . . . . . 15 ⊢ (((1...;10) ∈ V ∧ 2 ∈ ℤ) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ 2) ∈ (mzPoly‘(1...;10)))
291	183, 56, 290	mp2an 708	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ 2) ∈ (mzPoly‘(1...;10))
292		mzpmulmpt 37305	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ 2) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘3)↑2)) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (2 · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...;10)))
293	291, 224, 292	mp2an 708	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (2 · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...;10))
294		mzpmulmpt 37305	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘;10) + 1)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (2 · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))) ∈ (mzPoly‘(1...;10)))
295	289, 293, 294	mp2an 708	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))) ∈ (mzPoly‘(1...;10))
296		eqrabdioph 37341	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))} ∈ (Dioph‘;10))
297	182, 242, 295, 296	mp3an 1424	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))} ∈ (Dioph‘;10)
298		mzpsubmpt 37306	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘7) − (𝑖‘1))) ∈ (mzPoly‘(1...;10)))
299	255, 212, 298	mp2an 708	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘7) − (𝑖‘1))) ∈ (mzPoly‘(1...;10))
300		dvdsrabdioph 37374	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘7) − (𝑖‘1))) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))} ∈ (Dioph‘;10))
301	182, 235, 299, 300	mp3an 1424	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))} ∈ (Dioph‘;10)
302		3anrabdioph 37346	. . . . . . . . . . 11 ⊢ (({𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))} ∈ (Dioph‘;10))
303	283, 297, 301, 302	mp3an 1424	. . . . . . . . . 10 ⊢ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))} ∈ (Dioph‘;10)
304		anrabdioph 37344	. . . . . . . . . 10 ⊢ (({𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ ((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈ (ℤ≥‘2))} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0 ↑𝑚 (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	259, 303, 304	mp2an 708	. . . . . . . . 9 ⊢ {𝑖 ∈ (ℕ0 ↑𝑚 (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)
306		mzpmulmpt 37305	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ 2) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...;10)))
307	291, 222, 306	mp2an 708	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...;10))
308		mzpsubmpt 37306	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘7) − 1)) ∈ (mzPoly‘(1...;10)))
309	255, 217, 308	mp2an 708	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘7) − 1)) ∈ (mzPoly‘(1...;10))
310		dvdsrabdioph 37374	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘7) − 1)) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)} ∈ (Dioph‘;10))
311	182, 307, 309, 310	mp3an 1424	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)} ∈ (Dioph‘;10)
312		mzpsubmpt 37306	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘8) − (𝑖‘3))) ∈ (mzPoly‘(1...;10)))
313	275, 222, 312	mp2an 708	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘8) − (𝑖‘3))) ∈ (mzPoly‘(1...;10))
314		dvdsrabdioph 37374	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘8) − (𝑖‘3))) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))} ∈ (Dioph‘;10))
315	182, 235, 313, 314	mp3an 1424	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))} ∈ (Dioph‘;10)
316		anrabdioph 37344	. . . . . . . . . . 11 ⊢ (({𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))} ∈ (Dioph‘;10))
317	311, 315, 316	mp2an 708	. . . . . . . . . 10 ⊢ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))} ∈ (Dioph‘;10)
318	208, 3	sselii 3600	. . . . . . . . . . . . . 14 ⊢ 2 ∈ (1...;10)
319		mzpproj 37300	. . . . . . . . . . . . . 14 ⊢ (((1...;10) ∈ V ∧ 2 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...;10)))
320	183, 318, 319	mp2an 708	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...;10))
321		mzpsubmpt 37306	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘8) − (𝑖‘2))) ∈ (mzPoly‘(1...;10)))
322	275, 320, 321	mp2an 708	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘8) − (𝑖‘2))) ∈ (mzPoly‘(1...;10))
323		dvdsrabdioph 37374	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ ((𝑖‘8) − (𝑖‘2))) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))} ∈ (Dioph‘;10))
324	182, 307, 322, 323	mp3an 1424	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))} ∈ (Dioph‘;10)
325		lerabdioph 37369	. . . . . . . . . . . 12 ⊢ ((;10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (𝑖‘2) ≤ (𝑖‘3)} ∈ (Dioph‘;10))
326	182, 320, 222, 325	mp3an 1424	. . . . . . . . . . 11 ⊢ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (𝑖‘2) ≤ (𝑖‘3)} ∈ (Dioph‘;10)
327		anrabdioph 37344	. . . . . . . . . . 11 ⊢ (({𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (𝑖‘2) ≤ (𝑖‘3)} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))} ∈ (Dioph‘;10))
328	324, 326, 327	mp2an 708	. . . . . . . . . 10 ⊢ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))} ∈ (Dioph‘;10)
329		anrabdioph 37344	. . . . . . . . . 10 ⊢ (({𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))} ∈ (Dioph‘;10))
330	317, 328, 329	mp2an 708	. . . . . . . . 9 ⊢ {𝑖 ∈ (ℕ0 ↑𝑚 (1...;10)) ∣ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))} ∈ (Dioph‘;10)
331		anrabdioph 37344	. . . . . . . . 9 ⊢ (({𝑖 ∈ (ℕ0 ↑𝑚 (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 ↑𝑚 (1...;10)) ∣ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0 ↑𝑚 (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	305, 330, 331	mp2an 708	. . . . . . . 8 ⊢ {𝑖 ∈ (ℕ0 ↑𝑚 (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)
333	181, 332	eqeltri 2697	. . . . . . 7 ⊢ {𝑖 ∈ (ℕ0 ↑𝑚 (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)
334	206, 184, 185, 186, 187, 188, 190	7rexfrabdioph 37364	. . . . . . 7 ⊢ ((3 ∈ ℕ0 ∧ {𝑖 ∈ (ℕ0 ↑𝑚 (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 ↑𝑚 (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	55, 333, 334	mp2an 708	. . . . . 6 ⊢ {𝑎 ∈ (ℕ0 ↑𝑚 (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)
336		anrabdioph 37344	. . . . . 6 ⊢ (({𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ (𝑎‘3) ∈ ℕ} ∈ (Dioph‘3) ∧ {𝑎 ∈ (ℕ0 ↑𝑚 (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 ↑𝑚 (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	72, 335, 336	mp2an 708	. . . . 5 ⊢ {𝑎 ∈ (ℕ0 ↑𝑚 (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)
338		mzpproj 37300	. . . . . . 7 ⊢ (((1...3) ∈ V ∧ 2 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3)))
339	57, 5, 338	mp2an 708	. . . . . 6 ⊢ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3))
340		elnnrabdioph 37371	. . . . . 6 ⊢ ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈ (Dioph‘3))
341	55, 339, 340	mp2an 708	. . . . 5 ⊢ {𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈ (Dioph‘3)
342		anrabdioph 37344	. . . . 5 ⊢ (({𝑎 ∈ (ℕ0 ↑𝑚 (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 ↑𝑚 (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈ (Dioph‘3)) → {𝑎 ∈ (ℕ0 ↑𝑚 (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	337, 341, 342	mp2an 708	. . . 4 ⊢ {𝑎 ∈ (ℕ0 ↑𝑚 (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)
344		eq0rabdioph 37340	. . . . . 6 ⊢ ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ (𝑎‘3) = 0} ∈ (Dioph‘3))
345	55, 70, 344	mp2an 708	. . . . 5 ⊢ {𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ (𝑎‘3) = 0} ∈ (Dioph‘3)
346		eq0rabdioph 37340	. . . . . 6 ⊢ ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ (𝑎‘2) = 0} ∈ (Dioph‘3))
347	55, 339, 346	mp2an 708	. . . . 5 ⊢ {𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ (𝑎‘2) = 0} ∈ (Dioph‘3)
348		anrabdioph 37344	. . . . 5 ⊢ (({𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ (𝑎‘3) = 0} ∈ (Dioph‘3) ∧ {𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ (𝑎‘2) = 0} ∈ (Dioph‘3)) → {𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)} ∈ (Dioph‘3))
349	345, 347, 348	mp2an 708	. . . 4 ⊢ {𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)} ∈ (Dioph‘3)
350		orrabdioph 37345	. . . 4 ⊢ (({𝑎 ∈ (ℕ0 ↑𝑚 (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 ↑𝑚 (1...3)) ∣ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)} ∈ (Dioph‘3)) → {𝑎 ∈ (ℕ0 ↑𝑚 (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	343, 349, 350	mp2an 708	. . 3 ⊢ {𝑎 ∈ (ℕ0 ↑𝑚 (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)
352		anrabdioph 37344	. . 3 ⊢ (({𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ (𝑎‘1) ∈ (ℤ≥‘2)} ∈ (Dioph‘3) ∧ {𝑎 ∈ (ℕ0 ↑𝑚 (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 ↑𝑚 (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	66, 351, 352	mp2an 708	. 2 ⊢ {𝑎 ∈ (ℕ0 ↑𝑚 (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)
354	54, 353	eqeltri 2697	1 ⊢ {𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ ((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} ∈ (Dioph‘3)

Syntax hints:   ↔ wb 196   ∨ wo 383   ∧ wa 384   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990  ∃wrex 2913  {crab 2916  Vcvv 3200  [wsbc 3435   class class class wbr 4653   ↦ cmpt 4729   ↾ cres 5116  ⟶wf 5884  ‘cfv 5888  (class class class)co 6650   ↑_𝑚 cmap 7857  0cc0 9936  1c1 9937   + caddc 9939   · cmul 9941   < clt 10074   ≤ cle 10075   − cmin 10266  ℕcn 11020  2c2 11070  3c3 11071  4c4 11072  5c5 11073  6c6 11074  7c7 11075  8c8 11076  9c9 11077  ℕ₀cn0 11292  ℤcz 11377  ;cdc 11493  ℤ_≥cuz 11687  ...cfz 12326  ↑cexp 12860   ∥ cdvds 14983  mzPolycmzp 37285  Diophcdioph 37318   Y_rm crmy 37465

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015  ax-mulf 10016

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-omul 7565  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-fi 8317  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-acn 8768  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-xnn0 11364  df-z 11378  df-dec 11494  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-ioc 12180  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593  df-mod 12669  df-seq 12802  df-exp 12861  df-fac 13061  df-bc 13090  df-hash 13118  df-shft 13807  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-limsup 14202  df-clim 14219  df-rlim 14220  df-sum 14417  df-ef 14798  df-sin 14800  df-cos 14801  df-pi 14803  df-dvds 14984  df-gcd 15217  df-prm 15386  df-numer 15443  df-denom 15444  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-hom 15966  df-cco 15967  df-rest 16083  df-topn 16084  df-0g 16102  df-gsum 16103  df-topgen 16104  df-pt 16105  df-prds 16108  df-xrs 16162  df-qtop 16167  df-imas 16168  df-xps 16170  df-mre 16246  df-mrc 16247  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-submnd 17336  df-mulg 17541  df-cntz 17750  df-cmn 18195  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-fbas 19743  df-fg 19744  df-cnfld 19747  df-top 20699  df-topon 20716  df-topsp 20737  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825  df-nei 20902  df-lp 20940  df-perf 20941  df-cn 21031  df-cnp 21032  df-haus 21119  df-tx 21365  df-hmeo 21558  df-fil 21650  df-fm 21742  df-flim 21743  df-flf 21744  df-xms 22125  df-ms 22126  df-tms 22127  df-cncf 22681  df-limc 23630  df-dv 23631  df-log 24303  df-mzpcl 37286  df-mzp 37287  df-dioph 37319  df-squarenn 37405  df-pell1qr 37406  df-pell14qr 37407  df-pell1234qr 37408  df-pellfund 37409  df-rmx 37466  df-rmy 37467

This theorem is referenced by:  rmxdioph  37583  expdiophlem2  37589