rmxdioph - Mathbox for Stefan O'Rear

	Mathbox for Stefan O'Rear		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > rmxdioph		Structured version Visualization version GIF version

Theorem rmxdioph 42486

Description: X is a Diophantine function. (Contributed by Stefan O'Rear, 17-Oct-2014.)

**Assertion**
Ref	Expression
rmxdioph	⊢ {𝑎 ∈ (ℕ₀ ↑_m (1...3)) ∣ ((𝑎‘1) ∈ (ℤ_≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) X_rm (𝑎‘2)))} ∈ (Dioph‘3)

Proof of Theorem rmxdioph Dummy variables 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 483	. . . . . 6 ⊢ ((𝑎 ∈ (ℕ₀ ↑_m (1...3)) ∧ (𝑎‘1) ∈ (ℤ_≥‘2)) → (𝑎‘1) ∈ (ℤ_≥‘2))
2		elmapi 8876	. . . . . . . 8 ⊢ (𝑎 ∈ (ℕ₀ ↑_m (1...3)) → 𝑎:(1...3)⟶ℕ₀)
3		df-3 12316	. . . . . . . . . 10 ⊢ 3 = (2 + 1)
4		ssid 4004	. . . . . . . . . 10 ⊢ (1...3) ⊆ (1...3)
5	3, 4	jm2.27dlem5 42483	. . . . . . . . 9 ⊢ (1...2) ⊆ (1...3)
6		2nn 12325	. . . . . . . . . 10 ⊢ 2 ∈ ℕ
7	6	jm2.27dlem3 42481	. . . . . . . . 9 ⊢ 2 ∈ (1...2)
8	5, 7	sselii 3979	. . . . . . . 8 ⊢ 2 ∈ (1...3)
9		ffvelcdm 7096	. . . . . . . 8 ⊢ ((𝑎:(1...3)⟶ℕ₀ ∧ 2 ∈ (1...3)) → (𝑎‘2) ∈ ℕ₀)
10	2, 8, 9	sylancl 584	. . . . . . 7 ⊢ (𝑎 ∈ (ℕ₀ ↑_m (1...3)) → (𝑎‘2) ∈ ℕ₀)
11	10	adantr 479	. . . . . 6 ⊢ ((𝑎 ∈ (ℕ₀ ↑_m (1...3)) ∧ (𝑎‘1) ∈ (ℤ_≥‘2)) → (𝑎‘2) ∈ ℕ₀)
12		3nn 12331	. . . . . . . . 9 ⊢ 3 ∈ ℕ
13	12	jm2.27dlem3 42481	. . . . . . . 8 ⊢ 3 ∈ (1...3)
14		ffvelcdm 7096	. . . . . . . 8 ⊢ ((𝑎:(1...3)⟶ℕ₀ ∧ 3 ∈ (1...3)) → (𝑎‘3) ∈ ℕ₀)
15	2, 13, 14	sylancl 584	. . . . . . 7 ⊢ (𝑎 ∈ (ℕ₀ ↑_m (1...3)) → (𝑎‘3) ∈ ℕ₀)
16	15	adantr 479	. . . . . 6 ⊢ ((𝑎 ∈ (ℕ₀ ↑_m (1...3)) ∧ (𝑎‘1) ∈ (ℤ_≥‘2)) → (𝑎‘3) ∈ ℕ₀)
17		rmxdiophlem 42485	. . . . . 6 ⊢ (((𝑎‘1) ∈ (ℤ_≥‘2) ∧ (𝑎‘2) ∈ ℕ₀ ∧ (𝑎‘3) ∈ ℕ₀) → ((𝑎‘3) = ((𝑎‘1) X_rm (𝑎‘2)) ↔ ∃𝑏 ∈ ℕ₀ (𝑏 = ((𝑎‘1) Y_rm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)))
18	1, 11, 16, 17	syl3anc 1368	. . . . 5 ⊢ ((𝑎 ∈ (ℕ₀ ↑_m (1...3)) ∧ (𝑎‘1) ∈ (ℤ_≥‘2)) → ((𝑎‘3) = ((𝑎‘1) X_rm (𝑎‘2)) ↔ ∃𝑏 ∈ ℕ₀ (𝑏 = ((𝑎‘1) Y_rm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)))
19	18	pm5.32da 577	. . . 4 ⊢ (𝑎 ∈ (ℕ₀ ↑_m (1...3)) → (((𝑎‘1) ∈ (ℤ_≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) X_rm (𝑎‘2))) ↔ ((𝑎‘1) ∈ (ℤ_≥‘2) ∧ ∃𝑏 ∈ ℕ₀ (𝑏 = ((𝑎‘1) Y_rm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1))))
20		anass 467	. . . . . 6 ⊢ ((((𝑎‘1) ∈ (ℤ_≥‘2) ∧ 𝑏 = ((𝑎‘1) Y_rm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1) ↔ ((𝑎‘1) ∈ (ℤ_≥‘2) ∧ (𝑏 = ((𝑎‘1) Y_rm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)))
21	20	rexbii 3091	. . . . 5 ⊢ (∃𝑏 ∈ ℕ₀ (((𝑎‘1) ∈ (ℤ_≥‘2) ∧ 𝑏 = ((𝑎‘1) Y_rm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1) ↔ ∃𝑏 ∈ ℕ₀ ((𝑎‘1) ∈ (ℤ_≥‘2) ∧ (𝑏 = ((𝑎‘1) Y_rm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)))
22		r19.42v 3188	. . . . 5 ⊢ (∃𝑏 ∈ ℕ₀ ((𝑎‘1) ∈ (ℤ_≥‘2) ∧ (𝑏 = ((𝑎‘1) Y_rm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)) ↔ ((𝑎‘1) ∈ (ℤ_≥‘2) ∧ ∃𝑏 ∈ ℕ₀ (𝑏 = ((𝑎‘1) Y_rm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)))
23	21, 22	bitr2i 275	. . . 4 ⊢ (((𝑎‘1) ∈ (ℤ_≥‘2) ∧ ∃𝑏 ∈ ℕ₀ (𝑏 = ((𝑎‘1) Y_rm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)) ↔ ∃𝑏 ∈ ℕ₀ (((𝑎‘1) ∈ (ℤ_≥‘2) ∧ 𝑏 = ((𝑎‘1) Y_rm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1))
24	19, 23	bitrdi 286	. . 3 ⊢ (𝑎 ∈ (ℕ₀ ↑_m (1...3)) → (((𝑎‘1) ∈ (ℤ_≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) X_rm (𝑎‘2))) ↔ ∃𝑏 ∈ ℕ₀ (((𝑎‘1) ∈ (ℤ_≥‘2) ∧ 𝑏 = ((𝑎‘1) Y_rm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)))
25	24	rabbiia 3434	. 2 ⊢ {𝑎 ∈ (ℕ₀ ↑_m (1...3)) ∣ ((𝑎‘1) ∈ (ℤ_≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) X_rm (𝑎‘2)))} = {𝑎 ∈ (ℕ₀ ↑_m (1...3)) ∣ ∃𝑏 ∈ ℕ₀ (((𝑎‘1) ∈ (ℤ_≥‘2) ∧ 𝑏 = ((𝑎‘1) Y_rm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)}
26		3nn0 12530	. . 3 ⊢ 3 ∈ ℕ₀
27		vex 3477	. . . . . . 7 ⊢ 𝑐 ∈ V
28	27	resex 6038	. . . . . 6 ⊢ (𝑐 ↾ (1...3)) ∈ V
29		fvex 6915	. . . . . 6 ⊢ (𝑐‘4) ∈ V
30		df-2 12315	. . . . . . . . . . . . 13 ⊢ 2 = (1 + 1)
31	30, 5	jm2.27dlem5 42483	. . . . . . . . . . . 12 ⊢ (1...1) ⊆ (1...3)
32		1nn 12263	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ
33	32	jm2.27dlem3 42481	. . . . . . . . . . . 12 ⊢ 1 ∈ (1...1)
34	31, 33	sselii 3979	. . . . . . . . . . 11 ⊢ 1 ∈ (1...3)
35	34	jm2.27dlem1 42479	. . . . . . . . . 10 ⊢ (𝑎 = (𝑐 ↾ (1...3)) → (𝑎‘1) = (𝑐‘1))
36	35	eleq1d 2814	. . . . . . . . 9 ⊢ (𝑎 = (𝑐 ↾ (1...3)) → ((𝑎‘1) ∈ (ℤ_≥‘2) ↔ (𝑐‘1) ∈ (ℤ_≥‘2)))
37	36	adantr 479	. . . . . . . 8 ⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((𝑎‘1) ∈ (ℤ_≥‘2) ↔ (𝑐‘1) ∈ (ℤ_≥‘2)))
38		simpr 483	. . . . . . . . 9 ⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → 𝑏 = (𝑐‘4))
39	8	jm2.27dlem1 42479	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑐 ↾ (1...3)) → (𝑎‘2) = (𝑐‘2))
40	35, 39	oveq12d 7444	. . . . . . . . . 10 ⊢ (𝑎 = (𝑐 ↾ (1...3)) → ((𝑎‘1) Y_rm (𝑎‘2)) = ((𝑐‘1) Y_rm (𝑐‘2)))
41	40	adantr 479	. . . . . . . . 9 ⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((𝑎‘1) Y_rm (𝑎‘2)) = ((𝑐‘1) Y_rm (𝑐‘2)))
42	38, 41	eqeq12d 2744	. . . . . . . 8 ⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → (𝑏 = ((𝑎‘1) Y_rm (𝑎‘2)) ↔ (𝑐‘4) = ((𝑐‘1) Y_rm (𝑐‘2))))
43	37, 42	anbi12d 630	. . . . . . 7 ⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → (((𝑎‘1) ∈ (ℤ_≥‘2) ∧ 𝑏 = ((𝑎‘1) Y_rm (𝑎‘2))) ↔ ((𝑐‘1) ∈ (ℤ_≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Y_rm (𝑐‘2)))))
44	13	jm2.27dlem1 42479	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑐 ↾ (1...3)) → (𝑎‘3) = (𝑐‘3))
45	44	oveq1d 7441	. . . . . . . . . 10 ⊢ (𝑎 = (𝑐 ↾ (1...3)) → ((𝑎‘3)↑2) = ((𝑐‘3)↑2))
46	45	adantr 479	. . . . . . . . 9 ⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((𝑎‘3)↑2) = ((𝑐‘3)↑2))
47	35	oveq1d 7441	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑐 ↾ (1...3)) → ((𝑎‘1)↑2) = ((𝑐‘1)↑2))
48	47	oveq1d 7441	. . . . . . . . . 10 ⊢ (𝑎 = (𝑐 ↾ (1...3)) → (((𝑎‘1)↑2) − 1) = (((𝑐‘1)↑2) − 1))
49		oveq1 7433	. . . . . . . . . 10 ⊢ (𝑏 = (𝑐‘4) → (𝑏↑2) = ((𝑐‘4)↑2))
50	48, 49	oveqan12d 7445	. . . . . . . . 9 ⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((((𝑎‘1)↑2) − 1) · (𝑏↑2)) = ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2)))
51	46, 50	oveq12d 7444	. . . . . . . 8 ⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))))
52	51	eqeq1d 2730	. . . . . . 7 ⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1 ↔ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) = 1))
53	43, 52	anbi12d 630	. . . . . 6 ⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((((𝑎‘1) ∈ (ℤ_≥‘2) ∧ 𝑏 = ((𝑎‘1) Y_rm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1) ↔ (((𝑐‘1) ∈ (ℤ_≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Y_rm (𝑐‘2))) ∧ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) = 1)))
54	28, 29, 53	sbc2ie 3861	. . . . 5 ⊢ ([(𝑐 ↾ (1...3)) / 𝑎][(𝑐‘4) / 𝑏](((𝑎‘1) ∈ (ℤ_≥‘2) ∧ 𝑏 = ((𝑎‘1) Y_rm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1) ↔ (((𝑐‘1) ∈ (ℤ_≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Y_rm (𝑐‘2))) ∧ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) = 1))
55	54	rabbii 3436	. . . 4 ⊢ {𝑐 ∈ (ℕ₀ ↑_m (1...4)) ∣ [(𝑐 ↾ (1...3)) / 𝑎][(𝑐‘4) / 𝑏](((𝑎‘1) ∈ (ℤ_≥‘2) ∧ 𝑏 = ((𝑎‘1) Y_rm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)} = {𝑐 ∈ (ℕ₀ ↑_m (1...4)) ∣ (((𝑐‘1) ∈ (ℤ_≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Y_rm (𝑐‘2))) ∧ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) = 1)}
56		4nn0 12531	. . . . . 6 ⊢ 4 ∈ ℕ₀
57		rmydioph 42484	. . . . . 6 ⊢ {𝑏 ∈ (ℕ₀ ↑_m (1...3)) ∣ ((𝑏‘1) ∈ (ℤ_≥‘2) ∧ (𝑏‘3) = ((𝑏‘1) Y_rm (𝑏‘2)))} ∈ (Dioph‘3)
58		simp1 1133	. . . . . . . . 9 ⊢ (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → (𝑏‘1) = (𝑐‘1))
59	58	eleq1d 2814	. . . . . . . 8 ⊢ (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → ((𝑏‘1) ∈ (ℤ_≥‘2) ↔ (𝑐‘1) ∈ (ℤ_≥‘2)))
60		simp3 1135	. . . . . . . . 9 ⊢ (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → (𝑏‘3) = (𝑐‘4))
61		simp2 1134	. . . . . . . . . 10 ⊢ (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → (𝑏‘2) = (𝑐‘2))
62	58, 61	oveq12d 7444	. . . . . . . . 9 ⊢ (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → ((𝑏‘1) Y_rm (𝑏‘2)) = ((𝑐‘1) Y_rm (𝑐‘2)))
63	60, 62	eqeq12d 2744	. . . . . . . 8 ⊢ (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → ((𝑏‘3) = ((𝑏‘1) Y_rm (𝑏‘2)) ↔ (𝑐‘4) = ((𝑐‘1) Y_rm (𝑐‘2))))
64	59, 63	anbi12d 630	. . . . . . 7 ⊢ (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → (((𝑏‘1) ∈ (ℤ_≥‘2) ∧ (𝑏‘3) = ((𝑏‘1) Y_rm (𝑏‘2))) ↔ ((𝑐‘1) ∈ (ℤ_≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Y_rm (𝑐‘2)))))
65		df-4 12317	. . . . . . . . . . 11 ⊢ 4 = (3 + 1)
66		ssid 4004	. . . . . . . . . . 11 ⊢ (1...4) ⊆ (1...4)
67	65, 66	jm2.27dlem5 42483	. . . . . . . . . 10 ⊢ (1...3) ⊆ (1...4)
68	3, 67	jm2.27dlem5 42483	. . . . . . . . 9 ⊢ (1...2) ⊆ (1...4)
69	30, 68	jm2.27dlem5 42483	. . . . . . . 8 ⊢ (1...1) ⊆ (1...4)
70	69, 33	sselii 3979	. . . . . . 7 ⊢ 1 ∈ (1...4)
71	68, 7	sselii 3979	. . . . . . 7 ⊢ 2 ∈ (1...4)
72		4nn 12335	. . . . . . . 8 ⊢ 4 ∈ ℕ
73	72	jm2.27dlem3 42481	. . . . . . 7 ⊢ 4 ∈ (1...4)
74	64, 70, 71, 73	rabren3dioph 42284	. . . . . 6 ⊢ ((4 ∈ ℕ₀ ∧ {𝑏 ∈ (ℕ₀ ↑_m (1...3)) ∣ ((𝑏‘1) ∈ (ℤ_≥‘2) ∧ (𝑏‘3) = ((𝑏‘1) Y_rm (𝑏‘2)))} ∈ (Dioph‘3)) → {𝑐 ∈ (ℕ₀ ↑_m (1...4)) ∣ ((𝑐‘1) ∈ (ℤ_≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Y_rm (𝑐‘2)))} ∈ (Dioph‘4))
75	56, 57, 74	mp2an 690	. . . . 5 ⊢ {𝑐 ∈ (ℕ₀ ↑_m (1...4)) ∣ ((𝑐‘1) ∈ (ℤ_≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Y_rm (𝑐‘2)))} ∈ (Dioph‘4)
76		ovex 7459	. . . . . . . . 9 ⊢ (1...4) ∈ V
77	67, 13	sselii 3979	. . . . . . . . 9 ⊢ 3 ∈ (1...4)
78		mzpproj 42206	. . . . . . . . 9 ⊢ (((1...4) ∈ V ∧ 3 ∈ (1...4)) → (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ (𝑐‘3)) ∈ (mzPoly‘(1...4)))
79	76, 77, 78	mp2an 690	. . . . . . . 8 ⊢ (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ (𝑐‘3)) ∈ (mzPoly‘(1...4))
80		2nn0 12529	. . . . . . . 8 ⊢ 2 ∈ ℕ₀
81		mzpexpmpt 42214	. . . . . . . 8 ⊢ (((𝑐 ∈ (ℤ ↑_m (1...4)) ↦ (𝑐‘3)) ∈ (mzPoly‘(1...4)) ∧ 2 ∈ ℕ₀) → (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ ((𝑐‘3)↑2)) ∈ (mzPoly‘(1...4)))
82	79, 80, 81	mp2an 690	. . . . . . 7 ⊢ (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ ((𝑐‘3)↑2)) ∈ (mzPoly‘(1...4))
83		mzpproj 42206	. . . . . . . . . . 11 ⊢ (((1...4) ∈ V ∧ 1 ∈ (1...4)) → (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ (𝑐‘1)) ∈ (mzPoly‘(1...4)))
84	76, 70, 83	mp2an 690	. . . . . . . . . 10 ⊢ (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ (𝑐‘1)) ∈ (mzPoly‘(1...4))
85		mzpexpmpt 42214	. . . . . . . . . 10 ⊢ (((𝑐 ∈ (ℤ ↑_m (1...4)) ↦ (𝑐‘1)) ∈ (mzPoly‘(1...4)) ∧ 2 ∈ ℕ₀) → (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ ((𝑐‘1)↑2)) ∈ (mzPoly‘(1...4)))
86	84, 80, 85	mp2an 690	. . . . . . . . 9 ⊢ (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ ((𝑐‘1)↑2)) ∈ (mzPoly‘(1...4))
87		1z 12632	. . . . . . . . . 10 ⊢ 1 ∈ ℤ
88		mzpconstmpt 42209	. . . . . . . . . 10 ⊢ (((1...4) ∈ V ∧ 1 ∈ ℤ) → (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ 1) ∈ (mzPoly‘(1...4)))
89	76, 87, 88	mp2an 690	. . . . . . . . 9 ⊢ (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ 1) ∈ (mzPoly‘(1...4))
90		mzpsubmpt 42212	. . . . . . . . 9 ⊢ (((𝑐 ∈ (ℤ ↑_m (1...4)) ↦ ((𝑐‘1)↑2)) ∈ (mzPoly‘(1...4)) ∧ (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ 1) ∈ (mzPoly‘(1...4))) → (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ (((𝑐‘1)↑2) − 1)) ∈ (mzPoly‘(1...4)))
91	86, 89, 90	mp2an 690	. . . . . . . 8 ⊢ (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ (((𝑐‘1)↑2) − 1)) ∈ (mzPoly‘(1...4))
92		mzpproj 42206	. . . . . . . . . 10 ⊢ (((1...4) ∈ V ∧ 4 ∈ (1...4)) → (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ (𝑐‘4)) ∈ (mzPoly‘(1...4)))
93	76, 73, 92	mp2an 690	. . . . . . . . 9 ⊢ (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ (𝑐‘4)) ∈ (mzPoly‘(1...4))
94		mzpexpmpt 42214	. . . . . . . . 9 ⊢ (((𝑐 ∈ (ℤ ↑_m (1...4)) ↦ (𝑐‘4)) ∈ (mzPoly‘(1...4)) ∧ 2 ∈ ℕ₀) → (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ ((𝑐‘4)↑2)) ∈ (mzPoly‘(1...4)))
95	93, 80, 94	mp2an 690	. . . . . . . 8 ⊢ (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ ((𝑐‘4)↑2)) ∈ (mzPoly‘(1...4))
96		mzpmulmpt 42211	. . . . . . . 8 ⊢ (((𝑐 ∈ (ℤ ↑_m (1...4)) ↦ (((𝑐‘1)↑2) − 1)) ∈ (mzPoly‘(1...4)) ∧ (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ ((𝑐‘4)↑2)) ∈ (mzPoly‘(1...4))) → (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) ∈ (mzPoly‘(1...4)))
97	91, 95, 96	mp2an 690	. . . . . . 7 ⊢ (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) ∈ (mzPoly‘(1...4))
98		mzpsubmpt 42212	. . . . . . 7 ⊢ (((𝑐 ∈ (ℤ ↑_m (1...4)) ↦ ((𝑐‘3)↑2)) ∈ (mzPoly‘(1...4)) ∧ (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) ∈ (mzPoly‘(1...4))) → (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2)))) ∈ (mzPoly‘(1...4)))
99	82, 97, 98	mp2an 690	. . . . . 6 ⊢ (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2)))) ∈ (mzPoly‘(1...4))
100		eqrabdioph 42246	. . . . . 6 ⊢ ((4 ∈ ℕ₀ ∧ (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2)))) ∈ (mzPoly‘(1...4)) ∧ (𝑐 ∈ (ℤ ↑_m (1...4)) ↦ 1) ∈ (mzPoly‘(1...4))) → {𝑐 ∈ (ℕ₀ ↑_m (1...4)) ∣ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) = 1} ∈ (Dioph‘4))
101	56, 99, 89, 100	mp3an 1457	. . . . 5 ⊢ {𝑐 ∈ (ℕ₀ ↑_m (1...4)) ∣ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) = 1} ∈ (Dioph‘4)
102		anrabdioph 42249	. . . . 5 ⊢ (({𝑐 ∈ (ℕ₀ ↑_m (1...4)) ∣ ((𝑐‘1) ∈ (ℤ_≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Y_rm (𝑐‘2)))} ∈ (Dioph‘4) ∧ {𝑐 ∈ (ℕ₀ ↑_m (1...4)) ∣ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) = 1} ∈ (Dioph‘4)) → {𝑐 ∈ (ℕ₀ ↑_m (1...4)) ∣ (((𝑐‘1) ∈ (ℤ_≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Y_rm (𝑐‘2))) ∧ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) = 1)} ∈ (Dioph‘4))
103	75, 101, 102	mp2an 690	. . . 4 ⊢ {𝑐 ∈ (ℕ₀ ↑_m (1...4)) ∣ (((𝑐‘1) ∈ (ℤ_≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Y_rm (𝑐‘2))) ∧ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) = 1)} ∈ (Dioph‘4)
104	55, 103	eqeltri 2825	. . 3 ⊢ {𝑐 ∈ (ℕ₀ ↑_m (1...4)) ∣ [(𝑐 ↾ (1...3)) / 𝑎][(𝑐‘4) / 𝑏](((𝑎‘1) ∈ (ℤ_≥‘2) ∧ 𝑏 = ((𝑎‘1) Y_rm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)} ∈ (Dioph‘4)
105	65	rexfrabdioph 42264	. . 3 ⊢ ((3 ∈ ℕ₀ ∧ {𝑐 ∈ (ℕ₀ ↑_m (1...4)) ∣ [(𝑐 ↾ (1...3)) / 𝑎][(𝑐‘4) / 𝑏](((𝑎‘1) ∈ (ℤ_≥‘2) ∧ 𝑏 = ((𝑎‘1) Y_rm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)} ∈ (Dioph‘4)) → {𝑎 ∈ (ℕ₀ ↑_m (1...3)) ∣ ∃𝑏 ∈ ℕ₀ (((𝑎‘1) ∈ (ℤ_≥‘2) ∧ 𝑏 = ((𝑎‘1) Y_rm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)} ∈ (Dioph‘3))
106	26, 104, 105	mp2an 690	. 2 ⊢ {𝑎 ∈ (ℕ₀ ↑_m (1...3)) ∣ ∃𝑏 ∈ ℕ₀ (((𝑎‘1) ∈ (ℤ_≥‘2) ∧ 𝑏 = ((𝑎‘1) Y_rm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)} ∈ (Dioph‘3)
107	25, 106	eqeltri 2825	1 ⊢ {𝑎 ∈ (ℕ₀ ↑_m (1...3)) ∣ ((𝑎‘1) ∈ (ℤ_≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) X_rm (𝑎‘2)))} ∈ (Dioph‘3)

Colors of variables: wff setvar class

Syntax hints: ↔ wb 205 ∧ wa 394 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ∃wrex 3067 {crab 3430 Vcvv 3473 [wsbc 3778 ↦ cmpt 5235 ↾ cres 5684 ⟶wf 6549 ‘cfv 6553 (class class class)co 7426 ↑_m cmap 8853 1c1 11149 · cmul 11153 − cmin 11484 2c2 12307 3c3 12308 4c4 12309 ℕ₀cn0 12512 ℤcz 12598 ℤ_≥cuz 12862 ...cfz 13526 ↑cexp 14068 mzPolycmzp 42191 Diophcdioph 42224 X_rm crmx 42369 Y_rm crmy 42370

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2699 ax-rep 5289 ax-sep 5303 ax-nul 5310 ax-pow 5369 ax-pr 5433 ax-un 7748 ax-inf2 9674 ax-cnex 11204 ax-resscn 11205 ax-1cn 11206 ax-icn 11207 ax-addcl 11208 ax-addrcl 11209 ax-mulcl 11210 ax-mulrcl 11211 ax-mulcom 11212 ax-addass 11213 ax-mulass 11214 ax-distr 11215 ax-i2m1 11216 ax-1ne0 11217 ax-1rid 11218 ax-rnegex 11219 ax-rrecex 11220 ax-cnre 11221 ax-pre-lttri 11222 ax-pre-lttrn 11223 ax-pre-ltadd 11224 ax-pre-mulgt0 11225 ax-pre-sup 11226 ax-addf 11227

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2529 df-eu 2558 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3475 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4327 df-if 4533 df-pw 4608 df-sn 4633 df-pr 4635 df-tp 4637 df-op 4639 df-uni 4913 df-int 4954 df-iun 5002 df-iin 5003 df-br 5153 df-opab 5215 df-mpt 5236 df-tr 5270 df-id 5580 df-eprel 5586 df-po 5594 df-so 5595 df-fr 5637 df-se 5638 df-we 5639 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-pred 6310 df-ord 6377 df-on 6378 df-lim 6379 df-suc 6380 df-iota 6505 df-fun 6555 df-fn 6556 df-f 6557 df-f1 6558 df-fo 6559 df-f1o 6560 df-fv 6561 df-isom 6562 df-riota 7382 df-ov 7429 df-oprab 7430 df-mpo 7431 df-of 7692 df-om 7879 df-1st 8001 df-2nd 8002 df-supp 8174 df-frecs 8295 df-wrecs 8326 df-recs 8400 df-rdg 8439 df-1o 8495 df-2o 8496 df-oadd 8499 df-omul 8500 df-er 8733 df-map 8855 df-pm 8856 df-ixp 8925 df-en 8973 df-dom 8974 df-sdom 8975 df-fin 8976 df-fsupp 9396 df-fi 9444 df-sup 9475 df-inf 9476 df-oi 9543 df-dju 9934 df-card 9972 df-acn 9975 df-pnf 11290 df-mnf 11291 df-xr 11292 df-ltxr 11293 df-le 11294 df-sub 11486 df-neg 11487 df-div 11912 df-nn 12253 df-2 12315 df-3 12316 df-4 12317 df-5 12318 df-6 12319 df-7 12320 df-8 12321 df-9 12322 df-n0 12513 df-xnn0 12585 df-z 12599 df-dec 12718 df-uz 12863 df-q 12973 df-rp 13017 df-xneg 13134 df-xadd 13135 df-xmul 13136 df-ioo 13370 df-ioc 13371 df-ico 13372 df-icc 13373 df-fz 13527 df-fzo 13670 df-fl 13799 df-mod 13877 df-seq 14009 df-exp 14069 df-fac 14275 df-bc 14304 df-hash 14332 df-shft 15056 df-cj 15088 df-re 15089 df-im 15090 df-sqrt 15224 df-abs 15225 df-limsup 15457 df-clim 15474 df-rlim 15475 df-sum 15675 df-ef 16053 df-sin 16055 df-cos 16056 df-pi 16058 df-dvds 16241 df-gcd 16479 df-prm 16652 df-numer 16716 df-denom 16717 df-struct 17125 df-sets 17142 df-slot 17160 df-ndx 17172 df-base 17190 df-ress 17219 df-plusg 17255 df-mulr 17256 df-starv 17257 df-sca 17258 df-vsca 17259 df-ip 17260 df-tset 17261 df-ple 17262 df-ds 17264 df-unif 17265 df-hom 17266 df-cco 17267 df-rest 17413 df-topn 17414 df-0g 17432 df-gsum 17433 df-topgen 17434 df-pt 17435 df-prds 17438 df-xrs 17493 df-qtop 17498 df-imas 17499 df-xps 17501 df-mre 17575 df-mrc 17576 df-acs 17578 df-mgm 18609 df-sgrp 18688 df-mnd 18704 df-submnd 18750 df-mulg 19038 df-cntz 19282 df-cmn 19751 df-psmet 21285 df-xmet 21286 df-met 21287 df-bl 21288 df-mopn 21289 df-fbas 21290 df-fg 21291 df-cnfld 21294 df-top 22824 df-topon 22841 df-topsp 22863 df-bases 22877 df-cld 22951 df-ntr 22952 df-cls 22953 df-nei 23030 df-lp 23068 df-perf 23069 df-cn 23159 df-cnp 23160 df-haus 23247 df-tx 23494 df-hmeo 23687 df-fil 23778 df-fm 23870 df-flim 23871 df-flf 23872 df-xms 24254 df-ms 24255 df-tms 24256 df-cncf 24826 df-limc 25823 df-dv 25824 df-log 26518 df-mzpcl 42192 df-mzp 42193 df-dioph 42225 df-squarenn 42310 df-pell1qr 42311 df-pell14qr 42312 df-pell1234qr 42313 df-pellfund 42314 df-rmx 42371 df-rmy 42372

This theorem is referenced by: expdiophlem2 42492

W3C validator