Users' Mathboxes 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 39009
Description: X is a Diophantine function. (Contributed by Stefan O'Rear, 17-Oct-2014.)
Assertion
Ref Expression
rmxdioph {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ ((𝑎‘1) ∈ (ℤ‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)))} ∈ (Dioph‘3)

Proof of Theorem rmxdioph
Dummy variables 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 477 . . . . . 6 ((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) → (𝑎‘1) ∈ (ℤ‘2))
2 elmapi 8222 . . . . . . . 8 (𝑎 ∈ (ℕ0𝑚 (1...3)) → 𝑎:(1...3)⟶ℕ0)
3 df-3 11498 . . . . . . . . . 10 3 = (2 + 1)
4 ssid 3873 . . . . . . . . . 10 (1...3) ⊆ (1...3)
53, 4jm2.27dlem5 39006 . . . . . . . . 9 (1...2) ⊆ (1...3)
6 2nn 11507 . . . . . . . . . 10 2 ∈ ℕ
76jm2.27dlem3 39004 . . . . . . . . 9 2 ∈ (1...2)
85, 7sselii 3849 . . . . . . . 8 2 ∈ (1...3)
9 ffvelrn 6668 . . . . . . . 8 ((𝑎:(1...3)⟶ℕ0 ∧ 2 ∈ (1...3)) → (𝑎‘2) ∈ ℕ0)
102, 8, 9sylancl 577 . . . . . . 7 (𝑎 ∈ (ℕ0𝑚 (1...3)) → (𝑎‘2) ∈ ℕ0)
1110adantr 473 . . . . . 6 ((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) → (𝑎‘2) ∈ ℕ0)
12 3nn 11513 . . . . . . . . 9 3 ∈ ℕ
1312jm2.27dlem3 39004 . . . . . . . 8 3 ∈ (1...3)
14 ffvelrn 6668 . . . . . . . 8 ((𝑎:(1...3)⟶ℕ0 ∧ 3 ∈ (1...3)) → (𝑎‘3) ∈ ℕ0)
152, 13, 14sylancl 577 . . . . . . 7 (𝑎 ∈ (ℕ0𝑚 (1...3)) → (𝑎‘3) ∈ ℕ0)
1615adantr 473 . . . . . 6 ((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) → (𝑎‘3) ∈ ℕ0)
17 rmxdiophlem 39008 . . . . . 6 (((𝑎‘1) ∈ (ℤ‘2) ∧ (𝑎‘2) ∈ ℕ0 ∧ (𝑎‘3) ∈ ℕ0) → ((𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)) ↔ ∃𝑏 ∈ ℕ0 (𝑏 = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)))
181, 11, 16, 17syl3anc 1351 . . . . 5 ((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) → ((𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)) ↔ ∃𝑏 ∈ ℕ0 (𝑏 = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)))
1918pm5.32da 571 . . . 4 (𝑎 ∈ (ℕ0𝑚 (1...3)) → (((𝑎‘1) ∈ (ℤ‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2))) ↔ ((𝑎‘1) ∈ (ℤ‘2) ∧ ∃𝑏 ∈ ℕ0 (𝑏 = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1))))
20 anass 461 . . . . . 6 ((((𝑎‘1) ∈ (ℤ‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1) ↔ ((𝑎‘1) ∈ (ℤ‘2) ∧ (𝑏 = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)))
2120rexbii 3188 . . . . 5 (∃𝑏 ∈ ℕ0 (((𝑎‘1) ∈ (ℤ‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1) ↔ ∃𝑏 ∈ ℕ0 ((𝑎‘1) ∈ (ℤ‘2) ∧ (𝑏 = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)))
22 r19.42v 3285 . . . . 5 (∃𝑏 ∈ ℕ0 ((𝑎‘1) ∈ (ℤ‘2) ∧ (𝑏 = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)) ↔ ((𝑎‘1) ∈ (ℤ‘2) ∧ ∃𝑏 ∈ ℕ0 (𝑏 = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)))
2321, 22bitr2i 268 . . . 4 (((𝑎‘1) ∈ (ℤ‘2) ∧ ∃𝑏 ∈ ℕ0 (𝑏 = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)) ↔ ∃𝑏 ∈ ℕ0 (((𝑎‘1) ∈ (ℤ‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1))
2419, 23syl6bb 279 . . 3 (𝑎 ∈ (ℕ0𝑚 (1...3)) → (((𝑎‘1) ∈ (ℤ‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2))) ↔ ∃𝑏 ∈ ℕ0 (((𝑎‘1) ∈ (ℤ‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)))
2524rabbiia 3392 . 2 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ ((𝑎‘1) ∈ (ℤ‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)))} = {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ ∃𝑏 ∈ ℕ0 (((𝑎‘1) ∈ (ℤ‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)}
26 3nn0 11721 . . 3 3 ∈ ℕ0
27 vex 3412 . . . . . . 7 𝑐 ∈ V
2827resex 5738 . . . . . 6 (𝑐 ↾ (1...3)) ∈ V
29 fvex 6506 . . . . . 6 (𝑐‘4) ∈ V
30 df-2 11497 . . . . . . . . . . . . 13 2 = (1 + 1)
3130, 5jm2.27dlem5 39006 . . . . . . . . . . . 12 (1...1) ⊆ (1...3)
32 1nn 11446 . . . . . . . . . . . . 13 1 ∈ ℕ
3332jm2.27dlem3 39004 . . . . . . . . . . . 12 1 ∈ (1...1)
3431, 33sselii 3849 . . . . . . . . . . 11 1 ∈ (1...3)
3534jm2.27dlem1 39002 . . . . . . . . . 10 (𝑎 = (𝑐 ↾ (1...3)) → (𝑎‘1) = (𝑐‘1))
3635eleq1d 2844 . . . . . . . . 9 (𝑎 = (𝑐 ↾ (1...3)) → ((𝑎‘1) ∈ (ℤ‘2) ↔ (𝑐‘1) ∈ (ℤ‘2)))
3736adantr 473 . . . . . . . 8 ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((𝑎‘1) ∈ (ℤ‘2) ↔ (𝑐‘1) ∈ (ℤ‘2)))
38 simpr 477 . . . . . . . . 9 ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → 𝑏 = (𝑐‘4))
398jm2.27dlem1 39002 . . . . . . . . . . 11 (𝑎 = (𝑐 ↾ (1...3)) → (𝑎‘2) = (𝑐‘2))
4035, 39oveq12d 6988 . . . . . . . . . 10 (𝑎 = (𝑐 ↾ (1...3)) → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑐‘1) Yrm (𝑐‘2)))
4140adantr 473 . . . . . . . . 9 ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑐‘1) Yrm (𝑐‘2)))
4238, 41eqeq12d 2787 . . . . . . . 8 ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → (𝑏 = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2))))
4337, 42anbi12d 621 . . . . . . 7 ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → (((𝑎‘1) ∈ (ℤ‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ↔ ((𝑐‘1) ∈ (ℤ‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2)))))
4413jm2.27dlem1 39002 . . . . . . . . . . 11 (𝑎 = (𝑐 ↾ (1...3)) → (𝑎‘3) = (𝑐‘3))
4544oveq1d 6985 . . . . . . . . . 10 (𝑎 = (𝑐 ↾ (1...3)) → ((𝑎‘3)↑2) = ((𝑐‘3)↑2))
4645adantr 473 . . . . . . . . 9 ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((𝑎‘3)↑2) = ((𝑐‘3)↑2))
4735oveq1d 6985 . . . . . . . . . . 11 (𝑎 = (𝑐 ↾ (1...3)) → ((𝑎‘1)↑2) = ((𝑐‘1)↑2))
4847oveq1d 6985 . . . . . . . . . 10 (𝑎 = (𝑐 ↾ (1...3)) → (((𝑎‘1)↑2) − 1) = (((𝑐‘1)↑2) − 1))
49 oveq1 6977 . . . . . . . . . 10 (𝑏 = (𝑐‘4) → (𝑏↑2) = ((𝑐‘4)↑2))
5048, 49oveqan12d 6989 . . . . . . . . 9 ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((((𝑎‘1)↑2) − 1) · (𝑏↑2)) = ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2)))
5146, 50oveq12d 6988 . . . . . . . 8 ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))))
5251eqeq1d 2774 . . . . . . 7 ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1 ↔ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) = 1))
5343, 52anbi12d 621 . . . . . 6 ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((((𝑎‘1) ∈ (ℤ‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1) ↔ (((𝑐‘1) ∈ (ℤ‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2))) ∧ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) = 1)))
5428, 29, 53sbc2ie 3747 . . . . 5 ([(𝑐 ↾ (1...3)) / 𝑎][(𝑐‘4) / 𝑏](((𝑎‘1) ∈ (ℤ‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1) ↔ (((𝑐‘1) ∈ (ℤ‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2))) ∧ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) = 1))
5554rabbii 3393 . . . 4 {𝑐 ∈ (ℕ0𝑚 (1...4)) ∣ [(𝑐 ↾ (1...3)) / 𝑎][(𝑐‘4) / 𝑏](((𝑎‘1) ∈ (ℤ‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)} = {𝑐 ∈ (ℕ0𝑚 (1...4)) ∣ (((𝑐‘1) ∈ (ℤ‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2))) ∧ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) = 1)}
56 4nn0 11722 . . . . . 6 4 ∈ ℕ0
57 rmydioph 39007 . . . . . 6 {𝑏 ∈ (ℕ0𝑚 (1...3)) ∣ ((𝑏‘1) ∈ (ℤ‘2) ∧ (𝑏‘3) = ((𝑏‘1) Yrm (𝑏‘2)))} ∈ (Dioph‘3)
58 simp1 1116 . . . . . . . . 9 (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → (𝑏‘1) = (𝑐‘1))
5958eleq1d 2844 . . . . . . . 8 (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → ((𝑏‘1) ∈ (ℤ‘2) ↔ (𝑐‘1) ∈ (ℤ‘2)))
60 simp3 1118 . . . . . . . . 9 (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → (𝑏‘3) = (𝑐‘4))
61 simp2 1117 . . . . . . . . . 10 (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → (𝑏‘2) = (𝑐‘2))
6258, 61oveq12d 6988 . . . . . . . . 9 (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → ((𝑏‘1) Yrm (𝑏‘2)) = ((𝑐‘1) Yrm (𝑐‘2)))
6360, 62eqeq12d 2787 . . . . . . . 8 (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → ((𝑏‘3) = ((𝑏‘1) Yrm (𝑏‘2)) ↔ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2))))
6459, 63anbi12d 621 . . . . . . 7 (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → (((𝑏‘1) ∈ (ℤ‘2) ∧ (𝑏‘3) = ((𝑏‘1) Yrm (𝑏‘2))) ↔ ((𝑐‘1) ∈ (ℤ‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2)))))
65 df-4 11499 . . . . . . . . . . 11 4 = (3 + 1)
66 ssid 3873 . . . . . . . . . . 11 (1...4) ⊆ (1...4)
6765, 66jm2.27dlem5 39006 . . . . . . . . . 10 (1...3) ⊆ (1...4)
683, 67jm2.27dlem5 39006 . . . . . . . . 9 (1...2) ⊆ (1...4)
6930, 68jm2.27dlem5 39006 . . . . . . . 8 (1...1) ⊆ (1...4)
7069, 33sselii 3849 . . . . . . 7 1 ∈ (1...4)
7168, 7sselii 3849 . . . . . . 7 2 ∈ (1...4)
72 4nn 11518 . . . . . . . 8 4 ∈ ℕ
7372jm2.27dlem3 39004 . . . . . . 7 4 ∈ (1...4)
7464, 70, 71, 73rabren3dioph 38808 . . . . . 6 ((4 ∈ ℕ0 ∧ {𝑏 ∈ (ℕ0𝑚 (1...3)) ∣ ((𝑏‘1) ∈ (ℤ‘2) ∧ (𝑏‘3) = ((𝑏‘1) Yrm (𝑏‘2)))} ∈ (Dioph‘3)) → {𝑐 ∈ (ℕ0𝑚 (1...4)) ∣ ((𝑐‘1) ∈ (ℤ‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2)))} ∈ (Dioph‘4))
7556, 57, 74mp2an 679 . . . . 5 {𝑐 ∈ (ℕ0𝑚 (1...4)) ∣ ((𝑐‘1) ∈ (ℤ‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2)))} ∈ (Dioph‘4)
76 ovex 7002 . . . . . . . . 9 (1...4) ∈ V
7767, 13sselii 3849 . . . . . . . . 9 3 ∈ (1...4)
78 mzpproj 38729 . . . . . . . . 9 (((1...4) ∈ V ∧ 3 ∈ (1...4)) → (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ (𝑐‘3)) ∈ (mzPoly‘(1...4)))
7976, 77, 78mp2an 679 . . . . . . . 8 (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ (𝑐‘3)) ∈ (mzPoly‘(1...4))
80 2nn0 11720 . . . . . . . 8 2 ∈ ℕ0
81 mzpexpmpt 38737 . . . . . . . 8 (((𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ (𝑐‘3)) ∈ (mzPoly‘(1...4)) ∧ 2 ∈ ℕ0) → (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ ((𝑐‘3)↑2)) ∈ (mzPoly‘(1...4)))
8279, 80, 81mp2an 679 . . . . . . 7 (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ ((𝑐‘3)↑2)) ∈ (mzPoly‘(1...4))
83 mzpproj 38729 . . . . . . . . . . 11 (((1...4) ∈ V ∧ 1 ∈ (1...4)) → (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ (𝑐‘1)) ∈ (mzPoly‘(1...4)))
8476, 70, 83mp2an 679 . . . . . . . . . 10 (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ (𝑐‘1)) ∈ (mzPoly‘(1...4))
85 mzpexpmpt 38737 . . . . . . . . . 10 (((𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ (𝑐‘1)) ∈ (mzPoly‘(1...4)) ∧ 2 ∈ ℕ0) → (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ ((𝑐‘1)↑2)) ∈ (mzPoly‘(1...4)))
8684, 80, 85mp2an 679 . . . . . . . . 9 (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ ((𝑐‘1)↑2)) ∈ (mzPoly‘(1...4))
87 1z 11819 . . . . . . . . . 10 1 ∈ ℤ
88 mzpconstmpt 38732 . . . . . . . . . 10 (((1...4) ∈ V ∧ 1 ∈ ℤ) → (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ 1) ∈ (mzPoly‘(1...4)))
8976, 87, 88mp2an 679 . . . . . . . . 9 (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ 1) ∈ (mzPoly‘(1...4))
90 mzpsubmpt 38735 . . . . . . . . 9 (((𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ ((𝑐‘1)↑2)) ∈ (mzPoly‘(1...4)) ∧ (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ 1) ∈ (mzPoly‘(1...4))) → (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ (((𝑐‘1)↑2) − 1)) ∈ (mzPoly‘(1...4)))
9186, 89, 90mp2an 679 . . . . . . . 8 (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ (((𝑐‘1)↑2) − 1)) ∈ (mzPoly‘(1...4))
92 mzpproj 38729 . . . . . . . . . 10 (((1...4) ∈ V ∧ 4 ∈ (1...4)) → (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ (𝑐‘4)) ∈ (mzPoly‘(1...4)))
9376, 73, 92mp2an 679 . . . . . . . . 9 (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ (𝑐‘4)) ∈ (mzPoly‘(1...4))
94 mzpexpmpt 38737 . . . . . . . . 9 (((𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ (𝑐‘4)) ∈ (mzPoly‘(1...4)) ∧ 2 ∈ ℕ0) → (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ ((𝑐‘4)↑2)) ∈ (mzPoly‘(1...4)))
9593, 80, 94mp2an 679 . . . . . . . 8 (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ ((𝑐‘4)↑2)) ∈ (mzPoly‘(1...4))
96 mzpmulmpt 38734 . . . . . . . 8 (((𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ (((𝑐‘1)↑2) − 1)) ∈ (mzPoly‘(1...4)) ∧ (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ ((𝑐‘4)↑2)) ∈ (mzPoly‘(1...4))) → (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) ∈ (mzPoly‘(1...4)))
9791, 95, 96mp2an 679 . . . . . . 7 (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) ∈ (mzPoly‘(1...4))
98 mzpsubmpt 38735 . . . . . . 7 (((𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ ((𝑐‘3)↑2)) ∈ (mzPoly‘(1...4)) ∧ (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) ∈ (mzPoly‘(1...4))) → (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2)))) ∈ (mzPoly‘(1...4)))
9982, 97, 98mp2an 679 . . . . . 6 (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2)))) ∈ (mzPoly‘(1...4))
100 eqrabdioph 38770 . . . . . 6 ((4 ∈ ℕ0 ∧ (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2)))) ∈ (mzPoly‘(1...4)) ∧ (𝑐 ∈ (ℤ ↑𝑚 (1...4)) ↦ 1) ∈ (mzPoly‘(1...4))) → {𝑐 ∈ (ℕ0𝑚 (1...4)) ∣ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) = 1} ∈ (Dioph‘4))
10156, 99, 89, 100mp3an 1440 . . . . 5 {𝑐 ∈ (ℕ0𝑚 (1...4)) ∣ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) = 1} ∈ (Dioph‘4)
102 anrabdioph 38773 . . . . 5 (({𝑐 ∈ (ℕ0𝑚 (1...4)) ∣ ((𝑐‘1) ∈ (ℤ‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2)))} ∈ (Dioph‘4) ∧ {𝑐 ∈ (ℕ0𝑚 (1...4)) ∣ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) = 1} ∈ (Dioph‘4)) → {𝑐 ∈ (ℕ0𝑚 (1...4)) ∣ (((𝑐‘1) ∈ (ℤ‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2))) ∧ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) = 1)} ∈ (Dioph‘4))
10375, 101, 102mp2an 679 . . . 4 {𝑐 ∈ (ℕ0𝑚 (1...4)) ∣ (((𝑐‘1) ∈ (ℤ‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2))) ∧ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) = 1)} ∈ (Dioph‘4)
10455, 103eqeltri 2856 . . 3 {𝑐 ∈ (ℕ0𝑚 (1...4)) ∣ [(𝑐 ↾ (1...3)) / 𝑎][(𝑐‘4) / 𝑏](((𝑎‘1) ∈ (ℤ‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)} ∈ (Dioph‘4)
10565rexfrabdioph 38788 . . 3 ((3 ∈ ℕ0 ∧ {𝑐 ∈ (ℕ0𝑚 (1...4)) ∣ [(𝑐 ↾ (1...3)) / 𝑎][(𝑐‘4) / 𝑏](((𝑎‘1) ∈ (ℤ‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)} ∈ (Dioph‘4)) → {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ ∃𝑏 ∈ ℕ0 (((𝑎‘1) ∈ (ℤ‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)} ∈ (Dioph‘3))
10626, 104, 105mp2an 679 . 2 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ ∃𝑏 ∈ ℕ0 (((𝑎‘1) ∈ (ℤ‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1) · (𝑏↑2))) = 1)} ∈ (Dioph‘3)
10725, 106eqeltri 2856 1 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ ((𝑎‘1) ∈ (ℤ‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)))} ∈ (Dioph‘3)
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 387  w3a 1068   = wceq 1507  wcel 2050  wrex 3083  {crab 3086  Vcvv 3409  [wsbc 3675  cmpt 5002  cres 5403  wf 6178  cfv 6182  (class class class)co 6970  𝑚 cmap 8200  1c1 10330   · cmul 10334  cmin 10664  2c2 11489  3c3 11490  4c4 11491  0cn0 11701  cz 11787  cuz 12052  ...cfz 12702  cexp 13238  mzPolycmzp 38714  Diophcdioph 38747   Xrm crmx 38893   Yrm crmy 38894
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-inf2 8892  ax-cnex 10385  ax-resscn 10386  ax-1cn 10387  ax-icn 10388  ax-addcl 10389  ax-addrcl 10390  ax-mulcl 10391  ax-mulrcl 10392  ax-mulcom 10393  ax-addass 10394  ax-mulass 10395  ax-distr 10396  ax-i2m1 10397  ax-1ne0 10398  ax-1rid 10399  ax-rnegex 10400  ax-rrecex 10401  ax-cnre 10402  ax-pre-lttri 10403  ax-pre-lttrn 10404  ax-pre-ltadd 10405  ax-pre-mulgt0 10406  ax-pre-sup 10407  ax-addf 10408  ax-mulf 10409
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-rab 3091  df-v 3411  df-sbc 3676  df-csb 3781  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-pss 3839  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4707  df-int 4744  df-iun 4788  df-iin 4789  df-br 4924  df-opab 4986  df-mpt 5003  df-tr 5025  df-id 5306  df-eprel 5311  df-po 5320  df-so 5321  df-fr 5360  df-se 5361  df-we 5362  df-xp 5407  df-rel 5408  df-cnv 5409  df-co 5410  df-dm 5411  df-rn 5412  df-res 5413  df-ima 5414  df-pred 5980  df-ord 6026  df-on 6027  df-lim 6028  df-suc 6029  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-isom 6191  df-riota 6931  df-ov 6973  df-oprab 6974  df-mpo 6975  df-of 7221  df-om 7391  df-1st 7495  df-2nd 7496  df-supp 7628  df-wrecs 7744  df-recs 7806  df-rdg 7844  df-1o 7899  df-2o 7900  df-oadd 7903  df-omul 7904  df-er 8083  df-map 8202  df-pm 8203  df-ixp 8254  df-en 8301  df-dom 8302  df-sdom 8303  df-fin 8304  df-fsupp 8623  df-fi 8664  df-sup 8695  df-inf 8696  df-oi 8763  df-dju 9118  df-card 9156  df-acn 9159  df-cda 9382  df-pnf 10470  df-mnf 10471  df-xr 10472  df-ltxr 10473  df-le 10474  df-sub 10666  df-neg 10667  df-div 11093  df-nn 11434  df-2 11497  df-3 11498  df-4 11499  df-5 11500  df-6 11501  df-7 11502  df-8 11503  df-9 11504  df-n0 11702  df-xnn0 11774  df-z 11788  df-dec 11906  df-uz 12053  df-q 12157  df-rp 12199  df-xneg 12318  df-xadd 12319  df-xmul 12320  df-ioo 12552  df-ioc 12553  df-ico 12554  df-icc 12555  df-fz 12703  df-fzo 12844  df-fl 12971  df-mod 13047  df-seq 13179  df-exp 13239  df-fac 13443  df-bc 13472  df-hash 13500  df-shft 14281  df-cj 14313  df-re 14314  df-im 14315  df-sqrt 14449  df-abs 14450  df-limsup 14683  df-clim 14700  df-rlim 14701  df-sum 14898  df-ef 15275  df-sin 15277  df-cos 15278  df-pi 15280  df-dvds 15462  df-gcd 15698  df-prm 15866  df-numer 15925  df-denom 15926  df-struct 16335  df-ndx 16336  df-slot 16337  df-base 16339  df-sets 16340  df-ress 16341  df-plusg 16428  df-mulr 16429  df-starv 16430  df-sca 16431  df-vsca 16432  df-ip 16433  df-tset 16434  df-ple 16435  df-ds 16437  df-unif 16438  df-hom 16439  df-cco 16440  df-rest 16546  df-topn 16547  df-0g 16565  df-gsum 16566  df-topgen 16567  df-pt 16568  df-prds 16571  df-xrs 16625  df-qtop 16630  df-imas 16631  df-xps 16633  df-mre 16709  df-mrc 16710  df-acs 16712  df-mgm 17704  df-sgrp 17746  df-mnd 17757  df-submnd 17798  df-mulg 18006  df-cntz 18212  df-cmn 18662  df-psmet 20233  df-xmet 20234  df-met 20235  df-bl 20236  df-mopn 20237  df-fbas 20238  df-fg 20239  df-cnfld 20242  df-top 21200  df-topon 21217  df-topsp 21239  df-bases 21252  df-cld 21325  df-ntr 21326  df-cls 21327  df-nei 21404  df-lp 21442  df-perf 21443  df-cn 21533  df-cnp 21534  df-haus 21621  df-tx 21868  df-hmeo 22061  df-fil 22152  df-fm 22244  df-flim 22245  df-flf 22246  df-xms 22627  df-ms 22628  df-tms 22629  df-cncf 23183  df-limc 24161  df-dv 24162  df-log 24835  df-mzpcl 38715  df-mzp 38716  df-dioph 38748  df-squarenn 38834  df-pell1qr 38835  df-pell14qr 38836  df-pell1234qr 38837  df-pellfund 38838  df-rmx 38895  df-rmy 38896
This theorem is referenced by:  expdiophlem2  39015
  Copyright terms: Public domain W3C validator