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

Theorem rmydioph 41367
Description: jm2.27 41361 restated in terms of Diophantine sets. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
Assertion
Ref Expression
rmydioph {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)))} ∈ (Diophβ€˜3)

Proof of Theorem rmydioph
Dummy variables 𝑏 𝑐 𝑑 𝑒 𝑓 𝑔 β„Ž 𝑖 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elmapi 8794 . . . . . . 7 (π‘Ž ∈ (β„•0 ↑m (1...3)) β†’ π‘Ž:(1...3)βŸΆβ„•0)
2 2nn 12233 . . . . . . . . 9 2 ∈ β„•
32jm2.27dlem3 41364 . . . . . . . 8 2 ∈ (1...2)
4 df-3 12224 . . . . . . . 8 3 = (2 + 1)
53, 4, 2jm2.27dlem2 41363 . . . . . . 7 2 ∈ (1...3)
6 ffvelcdm 7037 . . . . . . 7 ((π‘Ž:(1...3)βŸΆβ„•0 ∧ 2 ∈ (1...3)) β†’ (π‘Žβ€˜2) ∈ β„•0)
71, 5, 6sylancl 587 . . . . . 6 (π‘Ž ∈ (β„•0 ↑m (1...3)) β†’ (π‘Žβ€˜2) ∈ β„•0)
8 elnn0 12422 . . . . . 6 ((π‘Žβ€˜2) ∈ β„•0 ↔ ((π‘Žβ€˜2) ∈ β„• ∨ (π‘Žβ€˜2) = 0))
97, 8sylib 217 . . . . 5 (π‘Ž ∈ (β„•0 ↑m (1...3)) β†’ ((π‘Žβ€˜2) ∈ β„• ∨ (π‘Žβ€˜2) = 0))
10 iba 529 . . . . . . 7 (((π‘Žβ€˜2) ∈ β„• ∨ (π‘Žβ€˜2) = 0) β†’ ((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ↔ ((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∧ ((π‘Žβ€˜2) ∈ β„• ∨ (π‘Žβ€˜2) = 0))))
11 andi 1007 . . . . . . 7 (((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∧ ((π‘Žβ€˜2) ∈ β„• ∨ (π‘Žβ€˜2) = 0)) ↔ (((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) ∨ ((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) = 0)))
1210, 11bitrdi 287 . . . . . 6 (((π‘Žβ€˜2) ∈ β„• ∨ (π‘Žβ€˜2) = 0) β†’ ((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ↔ (((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) ∨ ((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) = 0))))
1312anbi2d 630 . . . . 5 (((π‘Žβ€˜2) ∈ β„• ∨ (π‘Žβ€˜2) = 0) β†’ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2))) ↔ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) ∨ ((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) = 0)))))
149, 13syl 17 . . . 4 (π‘Ž ∈ (β„•0 ↑m (1...3)) β†’ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2))) ↔ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) ∨ ((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) = 0)))))
15 simplr 768 . . . . . . . . . . . . 13 (((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) β†’ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2))
16 nnz 12527 . . . . . . . . . . . . . 14 ((π‘Žβ€˜2) ∈ β„• β†’ (π‘Žβ€˜2) ∈ β„€)
1716adantl 483 . . . . . . . . . . . . 13 (((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) β†’ (π‘Žβ€˜2) ∈ β„€)
18 frmy 41267 . . . . . . . . . . . . . 14 Yrm :((β„€β‰₯β€˜2) Γ— β„€)βŸΆβ„€
1918fovcl 7489 . . . . . . . . . . . . 13 (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„€) β†’ ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∈ β„€)
2015, 17, 19syl2anc 585 . . . . . . . . . . . 12 (((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) β†’ ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∈ β„€)
21 rmy0 41282 . . . . . . . . . . . . . 14 ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) β†’ ((π‘Žβ€˜1) Yrm 0) = 0)
2221ad2antlr 726 . . . . . . . . . . . . 13 (((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) β†’ ((π‘Žβ€˜1) Yrm 0) = 0)
23 nngt0 12191 . . . . . . . . . . . . . . 15 ((π‘Žβ€˜2) ∈ β„• β†’ 0 < (π‘Žβ€˜2))
2423adantl 483 . . . . . . . . . . . . . 14 (((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) β†’ 0 < (π‘Žβ€˜2))
25 0zd 12518 . . . . . . . . . . . . . . 15 (((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) β†’ 0 ∈ β„€)
26 ltrmy 41305 . . . . . . . . . . . . . . 15 (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 0 ∈ β„€ ∧ (π‘Žβ€˜2) ∈ β„€) β†’ (0 < (π‘Žβ€˜2) ↔ ((π‘Žβ€˜1) Yrm 0) < ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2))))
2715, 25, 17, 26syl3anc 1372 . . . . . . . . . . . . . 14 (((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) β†’ (0 < (π‘Žβ€˜2) ↔ ((π‘Žβ€˜1) Yrm 0) < ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2))))
2824, 27mpbid 231 . . . . . . . . . . . . 13 (((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) β†’ ((π‘Žβ€˜1) Yrm 0) < ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)))
2922, 28eqbrtrrd 5134 . . . . . . . . . . . 12 (((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) β†’ 0 < ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)))
30 elnnz 12516 . . . . . . . . . . . 12 (((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∈ β„• ↔ (((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∈ β„€ ∧ 0 < ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2))))
3120, 29, 30sylanbrc 584 . . . . . . . . . . 11 (((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) β†’ ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∈ β„•)
32 eleq1 2826 . . . . . . . . . . 11 ((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) β†’ ((π‘Žβ€˜3) ∈ β„• ↔ ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∈ β„•))
3331, 32syl5ibrcom 247 . . . . . . . . . 10 (((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) β†’ ((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) β†’ (π‘Žβ€˜3) ∈ β„•))
3433pm4.71rd 564 . . . . . . . . 9 (((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) β†’ ((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ↔ ((π‘Žβ€˜3) ∈ β„• ∧ (π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)))))
35 simpllr 775 . . . . . . . . . . 11 ((((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (π‘Žβ€˜3) ∈ β„•) β†’ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2))
36 simplr 768 . . . . . . . . . . 11 ((((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (π‘Žβ€˜3) ∈ β„•) β†’ (π‘Žβ€˜2) ∈ β„•)
37 simpr 486 . . . . . . . . . . 11 ((((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (π‘Žβ€˜3) ∈ β„•) β†’ (π‘Žβ€˜3) ∈ β„•)
38 jm2.27 41361 . . . . . . . . . . 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))))))
3935, 36, 37, 38syl3anc 1372 . . . . . . . . . 10 ((((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (π‘Žβ€˜3) ∈ β„•) β†’ ((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ↔ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))))
4039pm5.32da 580 . . . . . . . . 9 (((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) β†’ (((π‘Žβ€˜3) ∈ β„• ∧ (π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2))) ↔ ((π‘Žβ€˜3) ∈ β„• ∧ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))))))
4134, 40bitrd 279 . . . . . . . 8 (((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) β†’ ((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ↔ ((π‘Žβ€˜3) ∈ β„• ∧ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))))))
4241ex 414 . . . . . . 7 ((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) β†’ ((π‘Žβ€˜2) ∈ β„• β†’ ((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ↔ ((π‘Žβ€˜3) ∈ β„• ∧ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))))))
4342pm5.32rd 579 . . . . . 6 ((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) β†’ (((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) ↔ (((π‘Žβ€˜3) ∈ β„• ∧ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))) ∧ (π‘Žβ€˜2) ∈ β„•)))
44 oveq2 7370 . . . . . . . . . . 11 ((π‘Žβ€˜2) = 0 β†’ ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) = ((π‘Žβ€˜1) Yrm 0))
4544adantl 483 . . . . . . . . . 10 (((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) = 0) β†’ ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) = ((π‘Žβ€˜1) Yrm 0))
4621ad2antlr 726 . . . . . . . . . 10 (((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) = 0) β†’ ((π‘Žβ€˜1) Yrm 0) = 0)
4745, 46eqtrd 2777 . . . . . . . . 9 (((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) = 0) β†’ ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) = 0)
4847eqeq2d 2748 . . . . . . . 8 (((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) ∧ (π‘Žβ€˜2) = 0) β†’ ((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ↔ (π‘Žβ€˜3) = 0))
4948ex 414 . . . . . . 7 ((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) β†’ ((π‘Žβ€˜2) = 0 β†’ ((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ↔ (π‘Žβ€˜3) = 0)))
5049pm5.32rd 579 . . . . . 6 ((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) β†’ (((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) = 0) ↔ ((π‘Žβ€˜3) = 0 ∧ (π‘Žβ€˜2) = 0)))
5143, 50orbi12d 918 . . . . 5 ((π‘Ž ∈ (β„•0 ↑m (1...3)) ∧ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)) β†’ ((((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) ∨ ((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) = 0)) ↔ ((((π‘Žβ€˜3) ∈ β„• ∧ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))) ∧ (π‘Žβ€˜2) ∈ β„•) ∨ ((π‘Žβ€˜3) = 0 ∧ (π‘Žβ€˜2) = 0))))
5251pm5.32da 580 . . . 4 (π‘Ž ∈ (β„•0 ↑m (1...3)) β†’ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ∈ β„•) ∨ ((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) = 0))) ↔ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ ((((π‘Žβ€˜3) ∈ β„• ∧ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))) ∧ (π‘Žβ€˜2) ∈ β„•) ∨ ((π‘Žβ€˜3) = 0 ∧ (π‘Žβ€˜2) = 0)))))
5314, 52bitrd 279 . . 3 (π‘Ž ∈ (β„•0 ↑m (1...3)) β†’ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2))) ↔ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ ((((π‘Žβ€˜3) ∈ β„• ∧ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))) ∧ (π‘Žβ€˜2) ∈ β„•) ∨ ((π‘Žβ€˜3) = 0 ∧ (π‘Žβ€˜2) = 0)))))
5453rabbiia 3414 . 2 {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)))} = {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ ((((π‘Žβ€˜3) ∈ β„• ∧ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))) ∧ (π‘Žβ€˜2) ∈ β„•) ∨ ((π‘Žβ€˜3) = 0 ∧ (π‘Žβ€˜2) = 0)))}
55 3nn0 12438 . . . 4 3 ∈ β„•0
56 2z 12542 . . . 4 2 ∈ β„€
57 ovex 7395 . . . . 5 (1...3) ∈ V
58 1nn 12171 . . . . . . . 8 1 ∈ β„•
5958jm2.27dlem3 41364 . . . . . . 7 1 ∈ (1...1)
60 df-2 12223 . . . . . . 7 2 = (1 + 1)
6159, 60, 58jm2.27dlem2 41363 . . . . . 6 1 ∈ (1...2)
6261, 4, 2jm2.27dlem2 41363 . . . . 5 1 ∈ (1...3)
63 mzpproj 41089 . . . . 5 (((1...3) ∈ V ∧ 1 ∈ (1...3)) β†’ (π‘Ž ∈ (β„€ ↑m (1...3)) ↦ (π‘Žβ€˜1)) ∈ (mzPolyβ€˜(1...3)))
6457, 62, 63mp2an 691 . . . 4 (π‘Ž ∈ (β„€ ↑m (1...3)) ↦ (π‘Žβ€˜1)) ∈ (mzPolyβ€˜(1...3))
65 eluzrabdioph 41158 . . . 4 ((3 ∈ β„•0 ∧ 2 ∈ β„€ ∧ (π‘Ž ∈ (β„€ ↑m (1...3)) ↦ (π‘Žβ€˜1)) ∈ (mzPolyβ€˜(1...3))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)} ∈ (Diophβ€˜3))
6655, 56, 64, 65mp3an 1462 . . 3 {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)} ∈ (Diophβ€˜3)
67 3nn 12239 . . . . . . . . 9 3 ∈ β„•
6867jm2.27dlem3 41364 . . . . . . . 8 3 ∈ (1...3)
69 mzpproj 41089 . . . . . . . 8 (((1...3) ∈ V ∧ 3 ∈ (1...3)) β†’ (π‘Ž ∈ (β„€ ↑m (1...3)) ↦ (π‘Žβ€˜3)) ∈ (mzPolyβ€˜(1...3)))
7057, 68, 69mp2an 691 . . . . . . 7 (π‘Ž ∈ (β„€ ↑m (1...3)) ↦ (π‘Žβ€˜3)) ∈ (mzPolyβ€˜(1...3))
71 elnnrabdioph 41159 . . . . . . 7 ((3 ∈ β„•0 ∧ (π‘Ž ∈ (β„€ ↑m (1...3)) ↦ (π‘Žβ€˜3)) ∈ (mzPolyβ€˜(1...3))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ (π‘Žβ€˜3) ∈ β„•} ∈ (Diophβ€˜3))
7255, 70, 71mp2an 691 . . . . . 6 {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ (π‘Žβ€˜3) ∈ β„•} ∈ (Diophβ€˜3)
73 fvex 6860 . . . . . . . . . . . . . . . 16 (π‘–β€˜8) ∈ V
74 fvex 6860 . . . . . . . . . . . . . . . 16 (π‘–β€˜9) ∈ V
75 fvex 6860 . . . . . . . . . . . . . . . 16 (π‘–β€˜10) ∈ V
76 oveq1 7369 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (π‘–β€˜9) β†’ (𝑔↑2) = ((π‘–β€˜9)↑2))
77 oveq1 7369 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = (π‘–β€˜8) β†’ (𝑓↑2) = ((π‘–β€˜8)↑2))
7877oveq2d 7378 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (π‘–β€˜8) β†’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2)) = (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2)))
7976, 78oveqan12rd 7382 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 = (π‘–β€˜8) ∧ 𝑔 = (π‘–β€˜9)) β†’ ((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = (((π‘–β€˜9)↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))))
8079eqeq1d 2739 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 = (π‘–β€˜8) ∧ 𝑔 = (π‘–β€˜9)) β†’ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ↔ (((π‘–β€˜9)↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1))
81803adant3 1133 . . . . . . . . . . . . . . . . . . 19 ((𝑓 = (π‘–β€˜8) ∧ 𝑔 = (π‘–β€˜9) ∧ β„Ž = (π‘–β€˜10)) β†’ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ↔ (((π‘–β€˜9)↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1))
82 oveq1 7369 . . . . . . . . . . . . . . . . . . . . . 22 (β„Ž = (π‘–β€˜10) β†’ (β„Ž + 1) = ((π‘–β€˜10) + 1))
8382oveq1d 7377 . . . . . . . . . . . . . . . . . . . . 21 (β„Ž = (π‘–β€˜10) β†’ ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))))
8483eqeq2d 2748 . . . . . . . . . . . . . . . . . . . 20 (β„Ž = (π‘–β€˜10) β†’ (𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ↔ 𝑐 = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2)))))
85843ad2ant3 1136 . . . . . . . . . . . . . . . . . . 19 ((𝑓 = (π‘–β€˜8) ∧ 𝑔 = (π‘–β€˜9) ∧ β„Ž = (π‘–β€˜10)) β†’ (𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ↔ 𝑐 = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2)))))
8681, 853anbi12d 1438 . . . . . . . . . . . . . . . . . 18 ((𝑓 = (π‘–β€˜8) ∧ 𝑔 = (π‘–β€˜9) ∧ β„Ž = (π‘–β€˜10)) β†’ ((((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1))) ↔ ((((π‘–β€˜9)↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ 𝑐 = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))))
8786anbi2d 630 . . . . . . . . . . . . . . . . 17 ((𝑓 = (π‘–β€˜8) ∧ 𝑔 = (π‘–β€˜9) ∧ β„Ž = (π‘–β€˜10)) β†’ (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ↔ ((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ 𝑐 = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1))))))
88 oveq1 7369 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (π‘–β€˜8) β†’ (𝑓 βˆ’ (π‘Žβ€˜3)) = ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3)))
8988breq2d 5122 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (π‘–β€˜8) β†’ (𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3)) ↔ 𝑑 βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))))
9089anbi2d 630 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (π‘–β€˜8) β†’ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ↔ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3)))))
91 oveq1 7369 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (π‘–β€˜8) β†’ (𝑓 βˆ’ (π‘Žβ€˜2)) = ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)))
9291breq2d 5122 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (π‘–β€˜8) β†’ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ↔ (2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2))))
9392anbi1d 631 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (π‘–β€˜8) β†’ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)) ↔ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))
9490, 93anbi12d 632 . . . . . . . . . . . . . . . . . 18 (𝑓 = (π‘–β€˜8) β†’ ((((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))) ↔ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))))
95943ad2ant1 1134 . . . . . . . . . . . . . . . . 17 ((𝑓 = (π‘–β€˜8) ∧ 𝑔 = (π‘–β€˜9) ∧ β„Ž = (π‘–β€˜10)) β†’ ((((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))) ↔ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))))
9687, 95anbi12d 632 . . . . . . . . . . . . . . . 16 ((𝑓 = (π‘–β€˜8) ∧ 𝑔 = (π‘–β€˜9) ∧ β„Ž = (π‘–β€˜10)) β†’ ((((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))) ↔ (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ 𝑐 = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))))
9773, 74, 75, 96sbc3ie 3830 . . . . . . . . . . . . . . 15 ([(π‘–β€˜8) / 𝑓][(π‘–β€˜9) / 𝑔][(π‘–β€˜10) / β„Ž](((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))) ↔ (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ 𝑐 = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))))
9897sbcbii 3804 . . . . . . . . . . . . . 14 ([(π‘–β€˜7) / 𝑒][(π‘–β€˜8) / 𝑓][(π‘–β€˜9) / 𝑔][(π‘–β€˜10) / β„Ž](((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))) ↔ [(π‘–β€˜7) / 𝑒](((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ 𝑐 = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))))
9998sbcbii 3804 . . . . . . . . . . . . 13 ([(π‘–β€˜6) / 𝑑][(π‘–β€˜7) / 𝑒][(π‘–β€˜8) / 𝑓][(π‘–β€˜9) / 𝑔][(π‘–β€˜10) / β„Ž](((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))) ↔ [(π‘–β€˜6) / 𝑑][(π‘–β€˜7) / 𝑒](((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ 𝑐 = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))))
10099sbcbii 3804 . . . . . . . . . . . 12 ([(π‘–β€˜5) / 𝑐][(π‘–β€˜6) / 𝑑][(π‘–β€˜7) / 𝑒][(π‘–β€˜8) / 𝑓][(π‘–β€˜9) / 𝑔][(π‘–β€˜10) / β„Ž](((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))) ↔ [(π‘–β€˜5) / 𝑐][(π‘–β€˜6) / 𝑑][(π‘–β€˜7) / 𝑒](((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ 𝑐 = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))))
101100sbcbii 3804 . . . . . . . . . . 11 ([(π‘–β€˜4) / 𝑏][(π‘–β€˜5) / 𝑐][(π‘–β€˜6) / 𝑑][(π‘–β€˜7) / 𝑒][(π‘–β€˜8) / 𝑓][(π‘–β€˜9) / 𝑔][(π‘–β€˜10) / β„Ž](((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))) ↔ [(π‘–β€˜4) / 𝑏][(π‘–β€˜5) / 𝑐][(π‘–β€˜6) / 𝑑][(π‘–β€˜7) / 𝑒](((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ 𝑐 = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))))
102101sbcbii 3804 . . . . . . . . . 10 ([(𝑖 β†Ύ (1...3)) / π‘Ž][(π‘–β€˜4) / 𝑏][(π‘–β€˜5) / 𝑐][(π‘–β€˜6) / 𝑑][(π‘–β€˜7) / 𝑒][(π‘–β€˜8) / 𝑓][(π‘–β€˜9) / 𝑔][(π‘–β€˜10) / β„Ž](((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))) ↔ [(𝑖 β†Ύ (1...3)) / π‘Ž][(π‘–β€˜4) / 𝑏][(π‘–β€˜5) / 𝑐][(π‘–β€˜6) / 𝑑][(π‘–β€˜7) / 𝑒](((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ 𝑐 = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))))
103 fvex 6860 . . . . . . . . . . . . 13 (π‘–β€˜5) ∈ V
104 fvex 6860 . . . . . . . . . . . . 13 (π‘–β€˜6) ∈ V
105 fvex 6860 . . . . . . . . . . . . 13 (π‘–β€˜7) ∈ V
106 oveq1 7369 . . . . . . . . . . . . . . . . . . 19 (𝑑 = (π‘–β€˜6) β†’ (𝑑↑2) = ((π‘–β€˜6)↑2))
1071063ad2ant2 1135 . . . . . . . . . . . . . . . . . 18 ((𝑐 = (π‘–β€˜5) ∧ 𝑑 = (π‘–β€˜6) ∧ 𝑒 = (π‘–β€˜7)) β†’ (𝑑↑2) = ((π‘–β€˜6)↑2))
108 oveq1 7369 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = (π‘–β€˜5) β†’ (𝑐↑2) = ((π‘–β€˜5)↑2))
109108oveq2d 7378 . . . . . . . . . . . . . . . . . . 19 (𝑐 = (π‘–β€˜5) β†’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2)) = ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2)))
1101093ad2ant1 1134 . . . . . . . . . . . . . . . . . 18 ((𝑐 = (π‘–β€˜5) ∧ 𝑑 = (π‘–β€˜6) ∧ 𝑒 = (π‘–β€˜7)) β†’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2)) = ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2)))
111107, 110oveq12d 7380 . . . . . . . . . . . . . . . . 17 ((𝑐 = (π‘–β€˜5) ∧ 𝑑 = (π‘–β€˜6) ∧ 𝑒 = (π‘–β€˜7)) β†’ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = (((π‘–β€˜6)↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))))
112111eqeq1d 2739 . . . . . . . . . . . . . . . 16 ((𝑐 = (π‘–β€˜5) ∧ 𝑑 = (π‘–β€˜6) ∧ 𝑒 = (π‘–β€˜7)) β†’ (((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ↔ (((π‘–β€˜6)↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1))
113 eleq1 2826 . . . . . . . . . . . . . . . . 17 (𝑒 = (π‘–β€˜7) β†’ (𝑒 ∈ (β„€β‰₯β€˜2) ↔ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)))
1141133ad2ant3 1136 . . . . . . . . . . . . . . . 16 ((𝑐 = (π‘–β€˜5) ∧ 𝑑 = (π‘–β€˜6) ∧ 𝑒 = (π‘–β€˜7)) β†’ (𝑒 ∈ (β„€β‰₯β€˜2) ↔ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)))
115112, 1143anbi23d 1440 . . . . . . . . . . . . . . 15 ((𝑐 = (π‘–β€˜5) ∧ 𝑑 = (π‘–β€˜6) ∧ 𝑒 = (π‘–β€˜7)) β†’ ((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ↔ (((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2))))
116 oveq1 7369 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = (π‘–β€˜7) β†’ (𝑒↑2) = ((π‘–β€˜7)↑2))
117116oveq1d 7377 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = (π‘–β€˜7) β†’ ((𝑒↑2) βˆ’ 1) = (((π‘–β€˜7)↑2) βˆ’ 1))
118117oveq1d 7377 . . . . . . . . . . . . . . . . . . 19 (𝑒 = (π‘–β€˜7) β†’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2)) = ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2)))
119118oveq2d 7378 . . . . . . . . . . . . . . . . . 18 (𝑒 = (π‘–β€˜7) β†’ (((π‘–β€˜9)↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = (((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))))
120119eqeq1d 2739 . . . . . . . . . . . . . . . . 17 (𝑒 = (π‘–β€˜7) β†’ ((((π‘–β€˜9)↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ↔ (((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1))
1211203ad2ant3 1136 . . . . . . . . . . . . . . . 16 ((𝑐 = (π‘–β€˜5) ∧ 𝑑 = (π‘–β€˜6) ∧ 𝑒 = (π‘–β€˜7)) β†’ ((((π‘–β€˜9)↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ↔ (((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1))
122 eqeq1 2741 . . . . . . . . . . . . . . . . 17 (𝑐 = (π‘–β€˜5) β†’ (𝑐 = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ↔ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2)))))
1231223ad2ant1 1134 . . . . . . . . . . . . . . . 16 ((𝑐 = (π‘–β€˜5) ∧ 𝑑 = (π‘–β€˜6) ∧ 𝑒 = (π‘–β€˜7)) β†’ (𝑐 = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ↔ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2)))))
124 simp2 1138 . . . . . . . . . . . . . . . . 17 ((𝑐 = (π‘–β€˜5) ∧ 𝑑 = (π‘–β€˜6) ∧ 𝑒 = (π‘–β€˜7)) β†’ 𝑑 = (π‘–β€˜6))
125 oveq1 7369 . . . . . . . . . . . . . . . . . 18 (𝑒 = (π‘–β€˜7) β†’ (𝑒 βˆ’ (π‘Žβ€˜1)) = ((π‘–β€˜7) βˆ’ (π‘Žβ€˜1)))
1261253ad2ant3 1136 . . . . . . . . . . . . . . . . 17 ((𝑐 = (π‘–β€˜5) ∧ 𝑑 = (π‘–β€˜6) ∧ 𝑒 = (π‘–β€˜7)) β†’ (𝑒 βˆ’ (π‘Žβ€˜1)) = ((π‘–β€˜7) βˆ’ (π‘Žβ€˜1)))
127124, 126breq12d 5123 . . . . . . . . . . . . . . . 16 ((𝑐 = (π‘–β€˜5) ∧ 𝑑 = (π‘–β€˜6) ∧ 𝑒 = (π‘–β€˜7)) β†’ (𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)) ↔ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘Žβ€˜1))))
128121, 123, 1273anbi123d 1437 . . . . . . . . . . . . . . 15 ((𝑐 = (π‘–β€˜5) ∧ 𝑑 = (π‘–β€˜6) ∧ 𝑒 = (π‘–β€˜7)) β†’ (((((π‘–β€˜9)↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ 𝑐 = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1))) ↔ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘Žβ€˜1)))))
129115, 128anbi12d 632 . . . . . . . . . . . . . 14 ((𝑐 = (π‘–β€˜5) ∧ 𝑑 = (π‘–β€˜6) ∧ 𝑒 = (π‘–β€˜7)) β†’ (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ 𝑐 = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ↔ ((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘Žβ€˜1))))))
130 oveq1 7369 . . . . . . . . . . . . . . . . . 18 (𝑒 = (π‘–β€˜7) β†’ (𝑒 βˆ’ 1) = ((π‘–β€˜7) βˆ’ 1))
131130breq2d 5122 . . . . . . . . . . . . . . . . 17 (𝑒 = (π‘–β€˜7) β†’ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ↔ (2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1)))
132 breq1 5113 . . . . . . . . . . . . . . . . 17 (𝑑 = (π‘–β€˜6) β†’ (𝑑 βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3)) ↔ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))))
133131, 132bi2anan9r 639 . . . . . . . . . . . . . . . 16 ((𝑑 = (π‘–β€˜6) ∧ 𝑒 = (π‘–β€˜7)) β†’ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ↔ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3)))))
134133anbi1d 631 . . . . . . . . . . . . . . 15 ((𝑑 = (π‘–β€˜6) ∧ 𝑒 = (π‘–β€˜7)) β†’ ((((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))) ↔ (((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))))
1351343adant1 1131 . . . . . . . . . . . . . 14 ((𝑐 = (π‘–β€˜5) ∧ 𝑑 = (π‘–β€˜6) ∧ 𝑒 = (π‘–β€˜7)) β†’ ((((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))) ↔ (((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))))
136129, 135anbi12d 632 . . . . . . . . . . . . 13 ((𝑐 = (π‘–β€˜5) ∧ 𝑑 = (π‘–β€˜6) ∧ 𝑒 = (π‘–β€˜7)) β†’ ((((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ 𝑐 = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))) ↔ (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))))
137103, 104, 105, 136sbc3ie 3830 . . . . . . . . . . . 12 ([(π‘–β€˜5) / 𝑐][(π‘–β€˜6) / 𝑑][(π‘–β€˜7) / 𝑒](((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ 𝑐 = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))) ↔ (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))))
138137sbcbii 3804 . . . . . . . . . . 11 ([(π‘–β€˜4) / 𝑏][(π‘–β€˜5) / 𝑐][(π‘–β€˜6) / 𝑑][(π‘–β€˜7) / 𝑒](((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ 𝑐 = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))) ↔ [(π‘–β€˜4) / 𝑏](((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))))
139138sbcbii 3804 . . . . . . . . . 10 ([(𝑖 β†Ύ (1...3)) / π‘Ž][(π‘–β€˜4) / 𝑏][(π‘–β€˜5) / 𝑐][(π‘–β€˜6) / 𝑑][(π‘–β€˜7) / 𝑒](((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ 𝑐 = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))) ↔ [(𝑖 β†Ύ (1...3)) / π‘Ž][(π‘–β€˜4) / 𝑏](((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))))
140 vex 3452 . . . . . . . . . . . 12 𝑖 ∈ V
141140resex 5990 . . . . . . . . . . 11 (𝑖 β†Ύ (1...3)) ∈ V
142 fvex 6860 . . . . . . . . . . 11 (π‘–β€˜4) ∈ V
143 oveq1 7369 . . . . . . . . . . . . . . . 16 (𝑏 = (π‘–β€˜4) β†’ (𝑏↑2) = ((π‘–β€˜4)↑2))
14462jm2.27dlem1 41362 . . . . . . . . . . . . . . . . . . 19 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ (π‘Žβ€˜1) = (π‘–β€˜1))
145144oveq1d 7377 . . . . . . . . . . . . . . . . . 18 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ ((π‘Žβ€˜1)↑2) = ((π‘–β€˜1)↑2))
146145oveq1d 7377 . . . . . . . . . . . . . . . . 17 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ (((π‘Žβ€˜1)↑2) βˆ’ 1) = (((π‘–β€˜1)↑2) βˆ’ 1))
14768jm2.27dlem1 41362 . . . . . . . . . . . . . . . . . 18 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ (π‘Žβ€˜3) = (π‘–β€˜3))
148147oveq1d 7377 . . . . . . . . . . . . . . . . 17 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ ((π‘Žβ€˜3)↑2) = ((π‘–β€˜3)↑2))
149146, 148oveq12d 7380 . . . . . . . . . . . . . . . 16 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2)) = ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2)))
150143, 149oveqan12rd 7382 . . . . . . . . . . . . . . 15 ((π‘Ž = (𝑖 β†Ύ (1...3)) ∧ 𝑏 = (π‘–β€˜4)) β†’ ((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = (((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))))
151150eqeq1d 2739 . . . . . . . . . . . . . 14 ((π‘Ž = (𝑖 β†Ύ (1...3)) ∧ 𝑏 = (π‘–β€˜4)) β†’ (((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ↔ (((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))) = 1))
152146oveq1d 7377 . . . . . . . . . . . . . . . . 17 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2)) = ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2)))
153152oveq2d 7378 . . . . . . . . . . . . . . . 16 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ (((π‘–β€˜6)↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))))
154153eqeq1d 2739 . . . . . . . . . . . . . . 15 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ ((((π‘–β€˜6)↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ↔ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1))
155154adantr 482 . . . . . . . . . . . . . 14 ((π‘Ž = (𝑖 β†Ύ (1...3)) ∧ 𝑏 = (π‘–β€˜4)) β†’ ((((π‘–β€˜6)↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ↔ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1))
156151, 1553anbi12d 1438 . . . . . . . . . . . . 13 ((π‘Ž = (𝑖 β†Ύ (1...3)) ∧ 𝑏 = (π‘–β€˜4)) β†’ ((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)) ↔ ((((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2))))
157148oveq2d 7378 . . . . . . . . . . . . . . . . 17 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ (2 Β· ((π‘Žβ€˜3)↑2)) = (2 Β· ((π‘–β€˜3)↑2)))
158157oveq2d 7378 . . . . . . . . . . . . . . . 16 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2))))
159158eqeq2d 2748 . . . . . . . . . . . . . . 15 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ ((π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ↔ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2)))))
160144oveq2d 7378 . . . . . . . . . . . . . . . 16 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ ((π‘–β€˜7) βˆ’ (π‘Žβ€˜1)) = ((π‘–β€˜7) βˆ’ (π‘–β€˜1)))
161160breq2d 5122 . . . . . . . . . . . . . . 15 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ ((π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘Žβ€˜1)) ↔ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘–β€˜1))))
162159, 1613anbi23d 1440 . . . . . . . . . . . . . 14 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ (((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘Žβ€˜1))) ↔ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘–β€˜1)))))
163162adantr 482 . . . . . . . . . . . . 13 ((π‘Ž = (𝑖 β†Ύ (1...3)) ∧ 𝑏 = (π‘–β€˜4)) β†’ (((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘Žβ€˜1))) ↔ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘–β€˜1)))))
164156, 163anbi12d 632 . . . . . . . . . . . 12 ((π‘Ž = (𝑖 β†Ύ (1...3)) ∧ 𝑏 = (π‘–β€˜4)) β†’ (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘Žβ€˜1)))) ↔ (((((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘–β€˜1))))))
165147oveq2d 7378 . . . . . . . . . . . . . . . 16 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ (2 Β· (π‘Žβ€˜3)) = (2 Β· (π‘–β€˜3)))
166165breq1d 5120 . . . . . . . . . . . . . . 15 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ↔ (2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1)))
167147oveq2d 7378 . . . . . . . . . . . . . . . 16 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3)) = ((π‘–β€˜8) βˆ’ (π‘–β€˜3)))
168167breq2d 5122 . . . . . . . . . . . . . . 15 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ ((π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3)) ↔ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜3))))
169166, 168anbi12d 632 . . . . . . . . . . . . . 14 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ (((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ↔ ((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜3)))))
1705jm2.27dlem1 41362 . . . . . . . . . . . . . . . . 17 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ (π‘Žβ€˜2) = (π‘–β€˜2))
171170oveq2d 7378 . . . . . . . . . . . . . . . 16 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) = ((π‘–β€˜8) βˆ’ (π‘–β€˜2)))
172165, 171breq12d 5123 . . . . . . . . . . . . . . 15 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ↔ (2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜2))))
173170, 147breq12d 5123 . . . . . . . . . . . . . . 15 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ ((π‘Žβ€˜2) ≀ (π‘Žβ€˜3) ↔ (π‘–β€˜2) ≀ (π‘–β€˜3)))
174172, 173anbi12d 632 . . . . . . . . . . . . . 14 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ (((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)) ↔ ((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜2)) ∧ (π‘–β€˜2) ≀ (π‘–β€˜3))))
175169, 174anbi12d 632 . . . . . . . . . . . . 13 (π‘Ž = (𝑖 β†Ύ (1...3)) β†’ ((((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))) ↔ (((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜3))) ∧ ((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜2)) ∧ (π‘–β€˜2) ≀ (π‘–β€˜3)))))
176175adantr 482 . . . . . . . . . . . 12 ((π‘Ž = (𝑖 β†Ύ (1...3)) ∧ 𝑏 = (π‘–β€˜4)) β†’ ((((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))) ↔ (((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜3))) ∧ ((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜2)) ∧ (π‘–β€˜2) ≀ (π‘–β€˜3)))))
177164, 176anbi12d 632 . . . . . . . . . . 11 ((π‘Ž = (𝑖 β†Ύ (1...3)) ∧ 𝑏 = (π‘–β€˜4)) β†’ ((((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))) ↔ ((((((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘–β€˜1)))) ∧ (((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜3))) ∧ ((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜2)) ∧ (π‘–β€˜2) ≀ (π‘–β€˜3))))))
178141, 142, 177sbc2ie 3827 . . . . . . . . . 10 ([(𝑖 β†Ύ (1...3)) / π‘Ž][(π‘–β€˜4) / 𝑏](((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))) ↔ ((((((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘–β€˜1)))) ∧ (((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜3))) ∧ ((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜2)) ∧ (π‘–β€˜2) ≀ (π‘–β€˜3)))))
179102, 139, 1783bitri 297 . . . . . . . . 9 ([(𝑖 β†Ύ (1...3)) / π‘Ž][(π‘–β€˜4) / 𝑏][(π‘–β€˜5) / 𝑐][(π‘–β€˜6) / 𝑑][(π‘–β€˜7) / 𝑒][(π‘–β€˜8) / 𝑓][(π‘–β€˜9) / 𝑔][(π‘–β€˜10) / β„Ž](((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))) ↔ ((((((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘–β€˜1)))) ∧ (((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜3))) ∧ ((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜2)) ∧ (π‘–β€˜2) ≀ (π‘–β€˜3)))))
180179rabbii 3416 . . . . . . . 8 {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ [(𝑖 β†Ύ (1...3)) / π‘Ž][(π‘–β€˜4) / 𝑏][(π‘–β€˜5) / 𝑐][(π‘–β€˜6) / 𝑑][(π‘–β€˜7) / 𝑒][(π‘–β€˜8) / 𝑓][(π‘–β€˜9) / 𝑔][(π‘–β€˜10) / β„Ž](((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))} = {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ ((((((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘–β€˜1)))) ∧ (((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜3))) ∧ ((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜2)) ∧ (π‘–β€˜2) ≀ (π‘–β€˜3))))}
181 10nn0 12643 . . . . . . . . . . . 12 10 ∈ β„•0
182 ovex 7395 . . . . . . . . . . . . . . 15 (1...10) ∈ V
183 df-5 12226 . . . . . . . . . . . . . . . . 17 5 = (4 + 1)
184 df-6 12227 . . . . . . . . . . . . . . . . . 18 6 = (5 + 1)
185 df-7 12228 . . . . . . . . . . . . . . . . . . 19 7 = (6 + 1)
186 df-8 12229 . . . . . . . . . . . . . . . . . . . 20 8 = (7 + 1)
187 df-9 12230 . . . . . . . . . . . . . . . . . . . . 21 9 = (8 + 1)
188 9p1e10 12627 . . . . . . . . . . . . . . . . . . . . . . 23 (9 + 1) = 10
189188eqcomi 2746 . . . . . . . . . . . . . . . . . . . . . 22 10 = (9 + 1)
190 ssid 3971 . . . . . . . . . . . . . . . . . . . . . 22 (1...10) βŠ† (1...10)
191189, 190jm2.27dlem5 41366 . . . . . . . . . . . . . . . . . . . . 21 (1...9) βŠ† (1...10)
192187, 191jm2.27dlem5 41366 . . . . . . . . . . . . . . . . . . . 20 (1...8) βŠ† (1...10)
193186, 192jm2.27dlem5 41366 . . . . . . . . . . . . . . . . . . 19 (1...7) βŠ† (1...10)
194185, 193jm2.27dlem5 41366 . . . . . . . . . . . . . . . . . 18 (1...6) βŠ† (1...10)
195184, 194jm2.27dlem5 41366 . . . . . . . . . . . . . . . . 17 (1...5) βŠ† (1...10)
196183, 195jm2.27dlem5 41366 . . . . . . . . . . . . . . . 16 (1...4) βŠ† (1...10)
197 4nn 12243 . . . . . . . . . . . . . . . . 17 4 ∈ β„•
198197jm2.27dlem3 41364 . . . . . . . . . . . . . . . 16 4 ∈ (1...4)
199196, 198sselii 3946 . . . . . . . . . . . . . . 15 4 ∈ (1...10)
200 mzpproj 41089 . . . . . . . . . . . . . . 15 (((1...10) ∈ V ∧ 4 ∈ (1...10)) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜4)) ∈ (mzPolyβ€˜(1...10)))
201182, 199, 200mp2an 691 . . . . . . . . . . . . . 14 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜4)) ∈ (mzPolyβ€˜(1...10))
202 2nn0 12437 . . . . . . . . . . . . . 14 2 ∈ β„•0
203 mzpexpmpt 41097 . . . . . . . . . . . . . 14 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜4)) ∈ (mzPolyβ€˜(1...10)) ∧ 2 ∈ β„•0) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜4)↑2)) ∈ (mzPolyβ€˜(1...10)))
204201, 202, 203mp2an 691 . . . . . . . . . . . . 13 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜4)↑2)) ∈ (mzPolyβ€˜(1...10))
205 df-4 12225 . . . . . . . . . . . . . . . . . . . . 21 4 = (3 + 1)
206205, 196jm2.27dlem5 41366 . . . . . . . . . . . . . . . . . . . 20 (1...3) βŠ† (1...10)
2074, 206jm2.27dlem5 41366 . . . . . . . . . . . . . . . . . . 19 (1...2) βŠ† (1...10)
20860, 207jm2.27dlem5 41366 . . . . . . . . . . . . . . . . . 18 (1...1) βŠ† (1...10)
209208, 59sselii 3946 . . . . . . . . . . . . . . . . 17 1 ∈ (1...10)
210 mzpproj 41089 . . . . . . . . . . . . . . . . 17 (((1...10) ∈ V ∧ 1 ∈ (1...10)) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜1)) ∈ (mzPolyβ€˜(1...10)))
211182, 209, 210mp2an 691 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜1)) ∈ (mzPolyβ€˜(1...10))
212 mzpexpmpt 41097 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜1)) ∈ (mzPolyβ€˜(1...10)) ∧ 2 ∈ β„•0) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜1)↑2)) ∈ (mzPolyβ€˜(1...10)))
213211, 202, 212mp2an 691 . . . . . . . . . . . . . . 15 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜1)↑2)) ∈ (mzPolyβ€˜(1...10))
214 1z 12540 . . . . . . . . . . . . . . . 16 1 ∈ β„€
215 mzpconstmpt 41092 . . . . . . . . . . . . . . . 16 (((1...10) ∈ V ∧ 1 ∈ β„€) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ 1) ∈ (mzPolyβ€˜(1...10)))
216182, 214, 215mp2an 691 . . . . . . . . . . . . . . 15 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ 1) ∈ (mzPolyβ€˜(1...10))
217 mzpsubmpt 41095 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜1)↑2)) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ 1) ∈ (mzPolyβ€˜(1...10))) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (((π‘–β€˜1)↑2) βˆ’ 1)) ∈ (mzPolyβ€˜(1...10)))
218213, 216, 217mp2an 691 . . . . . . . . . . . . . 14 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (((π‘–β€˜1)↑2) βˆ’ 1)) ∈ (mzPolyβ€˜(1...10))
219206, 68sselii 3946 . . . . . . . . . . . . . . . 16 3 ∈ (1...10)
220 mzpproj 41089 . . . . . . . . . . . . . . . 16 (((1...10) ∈ V ∧ 3 ∈ (1...10)) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜3)) ∈ (mzPolyβ€˜(1...10)))
221182, 219, 220mp2an 691 . . . . . . . . . . . . . . 15 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜3)) ∈ (mzPolyβ€˜(1...10))
222 mzpexpmpt 41097 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜3)) ∈ (mzPolyβ€˜(1...10)) ∧ 2 ∈ β„•0) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜3)↑2)) ∈ (mzPolyβ€˜(1...10)))
223221, 202, 222mp2an 691 . . . . . . . . . . . . . 14 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜3)↑2)) ∈ (mzPolyβ€˜(1...10))
224 mzpmulmpt 41094 . . . . . . . . . . . . . 14 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ (((π‘–β€˜1)↑2) βˆ’ 1)) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜3)↑2)) ∈ (mzPolyβ€˜(1...10))) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))) ∈ (mzPolyβ€˜(1...10)))
225218, 223, 224mp2an 691 . . . . . . . . . . . . 13 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))) ∈ (mzPolyβ€˜(1...10))
226 mzpsubmpt 41095 . . . . . . . . . . . . 13 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜4)↑2)) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))) ∈ (mzPolyβ€˜(1...10))) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2)))) ∈ (mzPolyβ€˜(1...10)))
227204, 225, 226mp2an 691 . . . . . . . . . . . 12 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2)))) ∈ (mzPolyβ€˜(1...10))
228 eqrabdioph 41129 . . . . . . . . . . . 12 ((10 ∈ β„•0 ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2)))) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ 1) ∈ (mzPolyβ€˜(1...10))) β†’ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))) = 1} ∈ (Diophβ€˜10))
229181, 227, 216, 228mp3an 1462 . . . . . . . . . . 11 {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))) = 1} ∈ (Diophβ€˜10)
230 6nn 12249 . . . . . . . . . . . . . . . . 17 6 ∈ β„•
231230jm2.27dlem3 41364 . . . . . . . . . . . . . . . 16 6 ∈ (1...6)
232194, 231sselii 3946 . . . . . . . . . . . . . . 15 6 ∈ (1...10)
233 mzpproj 41089 . . . . . . . . . . . . . . 15 (((1...10) ∈ V ∧ 6 ∈ (1...10)) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜6)) ∈ (mzPolyβ€˜(1...10)))
234182, 232, 233mp2an 691 . . . . . . . . . . . . . 14 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜6)) ∈ (mzPolyβ€˜(1...10))
235 mzpexpmpt 41097 . . . . . . . . . . . . . 14 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜6)) ∈ (mzPolyβ€˜(1...10)) ∧ 2 ∈ β„•0) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜6)↑2)) ∈ (mzPolyβ€˜(1...10)))
236234, 202, 235mp2an 691 . . . . . . . . . . . . 13 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜6)↑2)) ∈ (mzPolyβ€˜(1...10))
237 5nn 12246 . . . . . . . . . . . . . . . . . 18 5 ∈ β„•
238237jm2.27dlem3 41364 . . . . . . . . . . . . . . . . 17 5 ∈ (1...5)
239195, 238sselii 3946 . . . . . . . . . . . . . . . 16 5 ∈ (1...10)
240 mzpproj 41089 . . . . . . . . . . . . . . . 16 (((1...10) ∈ V ∧ 5 ∈ (1...10)) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜5)) ∈ (mzPolyβ€˜(1...10)))
241182, 239, 240mp2an 691 . . . . . . . . . . . . . . 15 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜5)) ∈ (mzPolyβ€˜(1...10))
242 mzpexpmpt 41097 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜5)) ∈ (mzPolyβ€˜(1...10)) ∧ 2 ∈ β„•0) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜5)↑2)) ∈ (mzPolyβ€˜(1...10)))
243241, 202, 242mp2an 691 . . . . . . . . . . . . . 14 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜5)↑2)) ∈ (mzPolyβ€˜(1...10))
244 mzpmulmpt 41094 . . . . . . . . . . . . . 14 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ (((π‘–β€˜1)↑2) βˆ’ 1)) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜5)↑2)) ∈ (mzPolyβ€˜(1...10))) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) ∈ (mzPolyβ€˜(1...10)))
245218, 243, 244mp2an 691 . . . . . . . . . . . . 13 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) ∈ (mzPolyβ€˜(1...10))
246 mzpsubmpt 41095 . . . . . . . . . . . . 13 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜6)↑2)) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) ∈ (mzPolyβ€˜(1...10))) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2)))) ∈ (mzPolyβ€˜(1...10)))
247236, 245, 246mp2an 691 . . . . . . . . . . . 12 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2)))) ∈ (mzPolyβ€˜(1...10))
248 eqrabdioph 41129 . . . . . . . . . . . 12 ((10 ∈ β„•0 ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2)))) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ 1) ∈ (mzPolyβ€˜(1...10))) β†’ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1} ∈ (Diophβ€˜10))
249181, 247, 216, 248mp3an 1462 . . . . . . . . . . 11 {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1} ∈ (Diophβ€˜10)
250 7nn 12252 . . . . . . . . . . . . . . 15 7 ∈ β„•
251250jm2.27dlem3 41364 . . . . . . . . . . . . . 14 7 ∈ (1...7)
252193, 251sselii 3946 . . . . . . . . . . . . 13 7 ∈ (1...10)
253 mzpproj 41089 . . . . . . . . . . . . 13 (((1...10) ∈ V ∧ 7 ∈ (1...10)) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜7)) ∈ (mzPolyβ€˜(1...10)))
254182, 252, 253mp2an 691 . . . . . . . . . . . 12 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜7)) ∈ (mzPolyβ€˜(1...10))
255 eluzrabdioph 41158 . . . . . . . . . . . 12 ((10 ∈ β„•0 ∧ 2 ∈ β„€ ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜7)) ∈ (mzPolyβ€˜(1...10))) β†’ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)} ∈ (Diophβ€˜10))
256181, 56, 254, 255mp3an 1462 . . . . . . . . . . 11 {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)} ∈ (Diophβ€˜10)
257 3anrabdioph 41134 . . . . . . . . . . 11 (({𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))) = 1} ∈ (Diophβ€˜10) ∧ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1} ∈ (Diophβ€˜10) ∧ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)} ∈ (Diophβ€˜10)) β†’ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ ((((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2))} ∈ (Diophβ€˜10))
258229, 249, 256, 257mp3an 1462 . . . . . . . . . 10 {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ ((((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2))} ∈ (Diophβ€˜10)
259 9nn 12258 . . . . . . . . . . . . . . . . 17 9 ∈ β„•
260259jm2.27dlem3 41364 . . . . . . . . . . . . . . . 16 9 ∈ (1...9)
261260, 189, 259jm2.27dlem2 41363 . . . . . . . . . . . . . . 15 9 ∈ (1...10)
262 mzpproj 41089 . . . . . . . . . . . . . . 15 (((1...10) ∈ V ∧ 9 ∈ (1...10)) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜9)) ∈ (mzPolyβ€˜(1...10)))
263182, 261, 262mp2an 691 . . . . . . . . . . . . . 14 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜9)) ∈ (mzPolyβ€˜(1...10))
264 mzpexpmpt 41097 . . . . . . . . . . . . . 14 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜9)) ∈ (mzPolyβ€˜(1...10)) ∧ 2 ∈ β„•0) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜9)↑2)) ∈ (mzPolyβ€˜(1...10)))
265263, 202, 264mp2an 691 . . . . . . . . . . . . 13 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜9)↑2)) ∈ (mzPolyβ€˜(1...10))
266 mzpexpmpt 41097 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜7)) ∈ (mzPolyβ€˜(1...10)) ∧ 2 ∈ β„•0) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜7)↑2)) ∈ (mzPolyβ€˜(1...10)))
267254, 202, 266mp2an 691 . . . . . . . . . . . . . . 15 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜7)↑2)) ∈ (mzPolyβ€˜(1...10))
268 mzpsubmpt 41095 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜7)↑2)) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ 1) ∈ (mzPolyβ€˜(1...10))) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (((π‘–β€˜7)↑2) βˆ’ 1)) ∈ (mzPolyβ€˜(1...10)))
269267, 216, 268mp2an 691 . . . . . . . . . . . . . 14 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (((π‘–β€˜7)↑2) βˆ’ 1)) ∈ (mzPolyβ€˜(1...10))
270 8nn 12255 . . . . . . . . . . . . . . . . . 18 8 ∈ β„•
271270jm2.27dlem3 41364 . . . . . . . . . . . . . . . . 17 8 ∈ (1...8)
272192, 271sselii 3946 . . . . . . . . . . . . . . . 16 8 ∈ (1...10)
273 mzpproj 41089 . . . . . . . . . . . . . . . 16 (((1...10) ∈ V ∧ 8 ∈ (1...10)) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜8)) ∈ (mzPolyβ€˜(1...10)))
274182, 272, 273mp2an 691 . . . . . . . . . . . . . . 15 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜8)) ∈ (mzPolyβ€˜(1...10))
275 mzpexpmpt 41097 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜8)) ∈ (mzPolyβ€˜(1...10)) ∧ 2 ∈ β„•0) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜8)↑2)) ∈ (mzPolyβ€˜(1...10)))
276274, 202, 275mp2an 691 . . . . . . . . . . . . . 14 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜8)↑2)) ∈ (mzPolyβ€˜(1...10))
277 mzpmulmpt 41094 . . . . . . . . . . . . . 14 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ (((π‘–β€˜7)↑2) βˆ’ 1)) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜8)↑2)) ∈ (mzPolyβ€˜(1...10))) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) ∈ (mzPolyβ€˜(1...10)))
278269, 276, 277mp2an 691 . . . . . . . . . . . . 13 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) ∈ (mzPolyβ€˜(1...10))
279 mzpsubmpt 41095 . . . . . . . . . . . . 13 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜9)↑2)) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) ∈ (mzPolyβ€˜(1...10))) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2)))) ∈ (mzPolyβ€˜(1...10)))
280265, 278, 279mp2an 691 . . . . . . . . . . . 12 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2)))) ∈ (mzPolyβ€˜(1...10))
281 eqrabdioph 41129 . . . . . . . . . . . 12 ((10 ∈ β„•0 ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2)))) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ 1) ∈ (mzPolyβ€˜(1...10))) β†’ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1} ∈ (Diophβ€˜10))
282181, 280, 216, 281mp3an 1462 . . . . . . . . . . 11 {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1} ∈ (Diophβ€˜10)
283 10nn 12641 . . . . . . . . . . . . . . . 16 10 ∈ β„•
284283jm2.27dlem3 41364 . . . . . . . . . . . . . . 15 10 ∈ (1...10)
285 mzpproj 41089 . . . . . . . . . . . . . . 15 (((1...10) ∈ V ∧ 10 ∈ (1...10)) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜10)) ∈ (mzPolyβ€˜(1...10)))
286182, 284, 285mp2an 691 . . . . . . . . . . . . . 14 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜10)) ∈ (mzPolyβ€˜(1...10))
287 mzpaddmpt 41093 . . . . . . . . . . . . . 14 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜10)) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ 1) ∈ (mzPolyβ€˜(1...10))) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜10) + 1)) ∈ (mzPolyβ€˜(1...10)))
288286, 216, 287mp2an 691 . . . . . . . . . . . . 13 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜10) + 1)) ∈ (mzPolyβ€˜(1...10))
289 mzpconstmpt 41092 . . . . . . . . . . . . . . 15 (((1...10) ∈ V ∧ 2 ∈ β„€) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ 2) ∈ (mzPolyβ€˜(1...10)))
290182, 56, 289mp2an 691 . . . . . . . . . . . . . 14 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ 2) ∈ (mzPolyβ€˜(1...10))
291 mzpmulmpt 41094 . . . . . . . . . . . . . 14 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ 2) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜3)↑2)) ∈ (mzPolyβ€˜(1...10))) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (2 Β· ((π‘–β€˜3)↑2))) ∈ (mzPolyβ€˜(1...10)))
292290, 223, 291mp2an 691 . . . . . . . . . . . . 13 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (2 Β· ((π‘–β€˜3)↑2))) ∈ (mzPolyβ€˜(1...10))
293 mzpmulmpt 41094 . . . . . . . . . . . . 13 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜10) + 1)) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (2 Β· ((π‘–β€˜3)↑2))) ∈ (mzPolyβ€˜(1...10))) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2)))) ∈ (mzPolyβ€˜(1...10)))
294288, 292, 293mp2an 691 . . . . . . . . . . . 12 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2)))) ∈ (mzPolyβ€˜(1...10))
295 eqrabdioph 41129 . . . . . . . . . . . 12 ((10 ∈ β„•0 ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜5)) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2)))) ∈ (mzPolyβ€˜(1...10))) β†’ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2)))} ∈ (Diophβ€˜10))
296181, 241, 294, 295mp3an 1462 . . . . . . . . . . 11 {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2)))} ∈ (Diophβ€˜10)
297 mzpsubmpt 41095 . . . . . . . . . . . . 13 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜7)) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜1)) ∈ (mzPolyβ€˜(1...10))) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜7) βˆ’ (π‘–β€˜1))) ∈ (mzPolyβ€˜(1...10)))
298254, 211, 297mp2an 691 . . . . . . . . . . . 12 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜7) βˆ’ (π‘–β€˜1))) ∈ (mzPolyβ€˜(1...10))
299 dvdsrabdioph 41162 . . . . . . . . . . . 12 ((10 ∈ β„•0 ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜6)) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜7) βˆ’ (π‘–β€˜1))) ∈ (mzPolyβ€˜(1...10))) β†’ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘–β€˜1))} ∈ (Diophβ€˜10))
300181, 234, 298, 299mp3an 1462 . . . . . . . . . . 11 {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘–β€˜1))} ∈ (Diophβ€˜10)
301 3anrabdioph 41134 . . . . . . . . . . 11 (({𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1} ∈ (Diophβ€˜10) ∧ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2)))} ∈ (Diophβ€˜10) ∧ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘–β€˜1))} ∈ (Diophβ€˜10)) β†’ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘–β€˜1)))} ∈ (Diophβ€˜10))
302282, 296, 300, 301mp3an 1462 . . . . . . . . . 10 {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘–β€˜1)))} ∈ (Diophβ€˜10)
303 anrabdioph 41132 . . . . . . . . . 10 (({𝑖 ∈ (β„•0 ↑m (1...10)) ∣ ((((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2))} ∈ (Diophβ€˜10) ∧ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘–β€˜1)))} ∈ (Diophβ€˜10)) β†’ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (((((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘–β€˜1))))} ∈ (Diophβ€˜10))
304258, 302, 303mp2an 691 . . . . . . . . 9 {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (((((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘–β€˜1))))} ∈ (Diophβ€˜10)
305 mzpmulmpt 41094 . . . . . . . . . . . . 13 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ 2) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜3)) ∈ (mzPolyβ€˜(1...10))) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (2 Β· (π‘–β€˜3))) ∈ (mzPolyβ€˜(1...10)))
306290, 221, 305mp2an 691 . . . . . . . . . . . 12 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (2 Β· (π‘–β€˜3))) ∈ (mzPolyβ€˜(1...10))
307 mzpsubmpt 41095 . . . . . . . . . . . . 13 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜7)) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ 1) ∈ (mzPolyβ€˜(1...10))) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜7) βˆ’ 1)) ∈ (mzPolyβ€˜(1...10)))
308254, 216, 307mp2an 691 . . . . . . . . . . . 12 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜7) βˆ’ 1)) ∈ (mzPolyβ€˜(1...10))
309 dvdsrabdioph 41162 . . . . . . . . . . . 12 ((10 ∈ β„•0 ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (2 Β· (π‘–β€˜3))) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜7) βˆ’ 1)) ∈ (mzPolyβ€˜(1...10))) β†’ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1)} ∈ (Diophβ€˜10))
310181, 306, 308, 309mp3an 1462 . . . . . . . . . . 11 {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1)} ∈ (Diophβ€˜10)
311 mzpsubmpt 41095 . . . . . . . . . . . . 13 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜8)) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜3)) ∈ (mzPolyβ€˜(1...10))) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜8) βˆ’ (π‘–β€˜3))) ∈ (mzPolyβ€˜(1...10)))
312274, 221, 311mp2an 691 . . . . . . . . . . . 12 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜8) βˆ’ (π‘–β€˜3))) ∈ (mzPolyβ€˜(1...10))
313 dvdsrabdioph 41162 . . . . . . . . . . . 12 ((10 ∈ β„•0 ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜6)) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜8) βˆ’ (π‘–β€˜3))) ∈ (mzPolyβ€˜(1...10))) β†’ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜3))} ∈ (Diophβ€˜10))
314181, 234, 312, 313mp3an 1462 . . . . . . . . . . 11 {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜3))} ∈ (Diophβ€˜10)
315 anrabdioph 41132 . . . . . . . . . . 11 (({𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1)} ∈ (Diophβ€˜10) ∧ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜3))} ∈ (Diophβ€˜10)) β†’ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ ((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜3)))} ∈ (Diophβ€˜10))
316310, 314, 315mp2an 691 . . . . . . . . . 10 {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ ((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜3)))} ∈ (Diophβ€˜10)
317207, 3sselii 3946 . . . . . . . . . . . . . 14 2 ∈ (1...10)
318 mzpproj 41089 . . . . . . . . . . . . . 14 (((1...10) ∈ V ∧ 2 ∈ (1...10)) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜2)) ∈ (mzPolyβ€˜(1...10)))
319182, 317, 318mp2an 691 . . . . . . . . . . . . 13 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜2)) ∈ (mzPolyβ€˜(1...10))
320 mzpsubmpt 41095 . . . . . . . . . . . . 13 (((𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜8)) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜2)) ∈ (mzPolyβ€˜(1...10))) β†’ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜8) βˆ’ (π‘–β€˜2))) ∈ (mzPolyβ€˜(1...10)))
321274, 319, 320mp2an 691 . . . . . . . . . . . 12 (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜8) βˆ’ (π‘–β€˜2))) ∈ (mzPolyβ€˜(1...10))
322 dvdsrabdioph 41162 . . . . . . . . . . . 12 ((10 ∈ β„•0 ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (2 Β· (π‘–β€˜3))) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ ((π‘–β€˜8) βˆ’ (π‘–β€˜2))) ∈ (mzPolyβ€˜(1...10))) β†’ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜2))} ∈ (Diophβ€˜10))
323181, 306, 321, 322mp3an 1462 . . . . . . . . . . 11 {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜2))} ∈ (Diophβ€˜10)
324 lerabdioph 41157 . . . . . . . . . . . 12 ((10 ∈ β„•0 ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜2)) ∈ (mzPolyβ€˜(1...10)) ∧ (𝑖 ∈ (β„€ ↑m (1...10)) ↦ (π‘–β€˜3)) ∈ (mzPolyβ€˜(1...10))) β†’ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (π‘–β€˜2) ≀ (π‘–β€˜3)} ∈ (Diophβ€˜10))
325181, 319, 221, 324mp3an 1462 . . . . . . . . . . 11 {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (π‘–β€˜2) ≀ (π‘–β€˜3)} ∈ (Diophβ€˜10)
326 anrabdioph 41132 . . . . . . . . . . 11 (({𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜2))} ∈ (Diophβ€˜10) ∧ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (π‘–β€˜2) ≀ (π‘–β€˜3)} ∈ (Diophβ€˜10)) β†’ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ ((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜2)) ∧ (π‘–β€˜2) ≀ (π‘–β€˜3))} ∈ (Diophβ€˜10))
327323, 325, 326mp2an 691 . . . . . . . . . 10 {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ ((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜2)) ∧ (π‘–β€˜2) ≀ (π‘–β€˜3))} ∈ (Diophβ€˜10)
328 anrabdioph 41132 . . . . . . . . . 10 (({𝑖 ∈ (β„•0 ↑m (1...10)) ∣ ((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜3)))} ∈ (Diophβ€˜10) ∧ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ ((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜2)) ∧ (π‘–β€˜2) ≀ (π‘–β€˜3))} ∈ (Diophβ€˜10)) β†’ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜3))) ∧ ((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜2)) ∧ (π‘–β€˜2) ≀ (π‘–β€˜3)))} ∈ (Diophβ€˜10))
329316, 327, 328mp2an 691 . . . . . . . . 9 {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜3))) ∧ ((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜2)) ∧ (π‘–β€˜2) ≀ (π‘–β€˜3)))} ∈ (Diophβ€˜10)
330 anrabdioph 41132 . . . . . . . . 9 (({𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (((((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘–β€˜1))))} ∈ (Diophβ€˜10) ∧ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ (((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜3))) ∧ ((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜2)) ∧ (π‘–β€˜2) ≀ (π‘–β€˜3)))} ∈ (Diophβ€˜10)) β†’ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ ((((((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘–β€˜1)))) ∧ (((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜3))) ∧ ((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜2)) ∧ (π‘–β€˜2) ≀ (π‘–β€˜3))))} ∈ (Diophβ€˜10))
331304, 329, 330mp2an 691 . . . . . . . 8 {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ ((((((π‘–β€˜4)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜3)↑2))) = 1 ∧ (((π‘–β€˜6)↑2) βˆ’ ((((π‘–β€˜1)↑2) βˆ’ 1) Β· ((π‘–β€˜5)↑2))) = 1 ∧ (π‘–β€˜7) ∈ (β„€β‰₯β€˜2)) ∧ ((((π‘–β€˜9)↑2) βˆ’ ((((π‘–β€˜7)↑2) βˆ’ 1) Β· ((π‘–β€˜8)↑2))) = 1 ∧ (π‘–β€˜5) = (((π‘–β€˜10) + 1) Β· (2 Β· ((π‘–β€˜3)↑2))) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜7) βˆ’ (π‘–β€˜1)))) ∧ (((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜7) βˆ’ 1) ∧ (π‘–β€˜6) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜3))) ∧ ((2 Β· (π‘–β€˜3)) βˆ₯ ((π‘–β€˜8) βˆ’ (π‘–β€˜2)) ∧ (π‘–β€˜2) ≀ (π‘–β€˜3))))} ∈ (Diophβ€˜10)
332180, 331eqeltri 2834 . . . . . . 7 {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ [(𝑖 β†Ύ (1...3)) / π‘Ž][(π‘–β€˜4) / 𝑏][(π‘–β€˜5) / 𝑐][(π‘–β€˜6) / 𝑑][(π‘–β€˜7) / 𝑒][(π‘–β€˜8) / 𝑓][(π‘–β€˜9) / 𝑔][(π‘–β€˜10) / β„Ž](((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))} ∈ (Diophβ€˜10)
333205, 183, 184, 185, 186, 187, 1897rexfrabdioph 41152 . . . . . . 7 ((3 ∈ β„•0 ∧ {𝑖 ∈ (β„•0 ↑m (1...10)) ∣ [(𝑖 β†Ύ (1...3)) / π‘Ž][(π‘–β€˜4) / 𝑏][(π‘–β€˜5) / 𝑐][(π‘–β€˜6) / 𝑑][(π‘–β€˜7) / 𝑒][(π‘–β€˜8) / 𝑓][(π‘–β€˜9) / 𝑔][(π‘–β€˜10) / β„Ž](((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))} ∈ (Diophβ€˜10)) β†’ {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))} ∈ (Diophβ€˜3))
33455, 332, 333mp2an 691 . . . . . 6 {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))} ∈ (Diophβ€˜3)
335 anrabdioph 41132 . . . . . 6 (({π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ (π‘Žβ€˜3) ∈ β„•} ∈ (Diophβ€˜3) ∧ {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))} ∈ (Diophβ€˜3)) β†’ {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ ((π‘Žβ€˜3) ∈ β„• ∧ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))))} ∈ (Diophβ€˜3))
33672, 334, 335mp2an 691 . . . . 5 {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ ((π‘Žβ€˜3) ∈ β„• ∧ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))))} ∈ (Diophβ€˜3)
337 mzpproj 41089 . . . . . . 7 (((1...3) ∈ V ∧ 2 ∈ (1...3)) β†’ (π‘Ž ∈ (β„€ ↑m (1...3)) ↦ (π‘Žβ€˜2)) ∈ (mzPolyβ€˜(1...3)))
33857, 5, 337mp2an 691 . . . . . 6 (π‘Ž ∈ (β„€ ↑m (1...3)) ↦ (π‘Žβ€˜2)) ∈ (mzPolyβ€˜(1...3))
339 elnnrabdioph 41159 . . . . . 6 ((3 ∈ β„•0 ∧ (π‘Ž ∈ (β„€ ↑m (1...3)) ↦ (π‘Žβ€˜2)) ∈ (mzPolyβ€˜(1...3))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ (π‘Žβ€˜2) ∈ β„•} ∈ (Diophβ€˜3))
34055, 338, 339mp2an 691 . . . . 5 {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ (π‘Žβ€˜2) ∈ β„•} ∈ (Diophβ€˜3)
341 anrabdioph 41132 . . . . 5 (({π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ ((π‘Žβ€˜3) ∈ β„• ∧ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3)))))} ∈ (Diophβ€˜3) ∧ {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ (π‘Žβ€˜2) ∈ β„•} ∈ (Diophβ€˜3)) β†’ {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ (((π‘Žβ€˜3) ∈ β„• ∧ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))) ∧ (π‘Žβ€˜2) ∈ β„•)} ∈ (Diophβ€˜3))
342336, 340, 341mp2an 691 . . . 4 {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ (((π‘Žβ€˜3) ∈ β„• ∧ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))) ∧ (π‘Žβ€˜2) ∈ β„•)} ∈ (Diophβ€˜3)
343 eq0rabdioph 41128 . . . . . 6 ((3 ∈ β„•0 ∧ (π‘Ž ∈ (β„€ ↑m (1...3)) ↦ (π‘Žβ€˜3)) ∈ (mzPolyβ€˜(1...3))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ (π‘Žβ€˜3) = 0} ∈ (Diophβ€˜3))
34455, 70, 343mp2an 691 . . . . 5 {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ (π‘Žβ€˜3) = 0} ∈ (Diophβ€˜3)
345 eq0rabdioph 41128 . . . . . 6 ((3 ∈ β„•0 ∧ (π‘Ž ∈ (β„€ ↑m (1...3)) ↦ (π‘Žβ€˜2)) ∈ (mzPolyβ€˜(1...3))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ (π‘Žβ€˜2) = 0} ∈ (Diophβ€˜3))
34655, 338, 345mp2an 691 . . . . 5 {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ (π‘Žβ€˜2) = 0} ∈ (Diophβ€˜3)
347 anrabdioph 41132 . . . . 5 (({π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ (π‘Žβ€˜3) = 0} ∈ (Diophβ€˜3) ∧ {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ (π‘Žβ€˜2) = 0} ∈ (Diophβ€˜3)) β†’ {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ ((π‘Žβ€˜3) = 0 ∧ (π‘Žβ€˜2) = 0)} ∈ (Diophβ€˜3))
348344, 346, 347mp2an 691 . . . 4 {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ ((π‘Žβ€˜3) = 0 ∧ (π‘Žβ€˜2) = 0)} ∈ (Diophβ€˜3)
349 orrabdioph 41133 . . . 4 (({π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ (((π‘Žβ€˜3) ∈ β„• ∧ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))) ∧ (π‘Žβ€˜2) ∈ β„•)} ∈ (Diophβ€˜3) ∧ {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ ((π‘Žβ€˜3) = 0 ∧ (π‘Žβ€˜2) = 0)} ∈ (Diophβ€˜3)) β†’ {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ ((((π‘Žβ€˜3) ∈ β„• ∧ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))) ∧ (π‘Žβ€˜2) ∈ β„•) ∨ ((π‘Žβ€˜3) = 0 ∧ (π‘Žβ€˜2) = 0))} ∈ (Diophβ€˜3))
350342, 348, 349mp2an 691 . . 3 {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ ((((π‘Žβ€˜3) ∈ β„• ∧ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))) ∧ (π‘Žβ€˜2) ∈ β„•) ∨ ((π‘Žβ€˜3) = 0 ∧ (π‘Žβ€˜2) = 0))} ∈ (Diophβ€˜3)
351 anrabdioph 41132 . . 3 (({π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)} ∈ (Diophβ€˜3) ∧ {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ ((((π‘Žβ€˜3) ∈ β„• ∧ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))) ∧ (π‘Žβ€˜2) ∈ β„•) ∨ ((π‘Žβ€˜3) = 0 ∧ (π‘Žβ€˜2) = 0))} ∈ (Diophβ€˜3)) β†’ {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ ((((π‘Žβ€˜3) ∈ β„• ∧ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))) ∧ (π‘Žβ€˜2) ∈ β„•) ∨ ((π‘Žβ€˜3) = 0 ∧ (π‘Žβ€˜2) = 0)))} ∈ (Diophβ€˜3))
35266, 350, 351mp2an 691 . 2 {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ ((((π‘Žβ€˜3) ∈ β„• ∧ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 βˆƒπ‘’ ∈ β„•0 βˆƒπ‘“ ∈ β„•0 βˆƒπ‘” ∈ β„•0 βˆƒβ„Ž ∈ β„•0 (((((𝑏↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· ((π‘Žβ€˜3)↑2))) = 1 ∧ ((𝑑↑2) βˆ’ ((((π‘Žβ€˜1)↑2) βˆ’ 1) Β· (𝑐↑2))) = 1 ∧ 𝑒 ∈ (β„€β‰₯β€˜2)) ∧ (((𝑔↑2) βˆ’ (((𝑒↑2) βˆ’ 1) Β· (𝑓↑2))) = 1 ∧ 𝑐 = ((β„Ž + 1) Β· (2 Β· ((π‘Žβ€˜3)↑2))) ∧ 𝑑 βˆ₯ (𝑒 βˆ’ (π‘Žβ€˜1)))) ∧ (((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑒 βˆ’ 1) ∧ 𝑑 βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜3))) ∧ ((2 Β· (π‘Žβ€˜3)) βˆ₯ (𝑓 βˆ’ (π‘Žβ€˜2)) ∧ (π‘Žβ€˜2) ≀ (π‘Žβ€˜3))))) ∧ (π‘Žβ€˜2) ∈ β„•) ∨ ((π‘Žβ€˜3) = 0 ∧ (π‘Žβ€˜2) = 0)))} ∈ (Diophβ€˜3)
35354, 352eqeltri 2834 1 {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)))} ∈ (Diophβ€˜3)
Colors of variables: wff setvar class
Syntax hints:   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆƒwrex 3074  {crab 3410  Vcvv 3448  [wsbc 3744   class class class wbr 5110   ↦ cmpt 5193   β†Ύ cres 5640  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362   ↑m cmap 8772  0cc0 11058  1c1 11059   + caddc 11061   Β· cmul 11063   < clt 11196   ≀ cle 11197   βˆ’ cmin 11392  β„•cn 12160  2c2 12215  3c3 12216  4c4 12217  5c5 12218  6c6 12219  7c7 12220  8c8 12221  9c9 12222  β„•0cn0 12420  β„€cz 12506  cdc 12625  β„€β‰₯cuz 12770  ...cfz 13431  β†‘cexp 13974   βˆ₯ cdvds 16143  mzPolycmzp 41074  Diophcdioph 41107   Yrm crmy 41253
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136  ax-addf 11137  ax-mulf 11138
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-oadd 8421  df-omul 8422  df-er 8655  df-map 8774  df-pm 8775  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-fi 9354  df-sup 9385  df-inf 9386  df-oi 9453  df-dju 9844  df-card 9882  df-acn 9885  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-xnn0 12493  df-z 12507  df-dec 12626  df-uz 12771  df-q 12881  df-rp 12923  df-xneg 13040  df-xadd 13041  df-xmul 13042  df-ioo 13275  df-ioc 13276  df-ico 13277  df-icc 13278  df-fz 13432  df-fzo 13575  df-fl 13704  df-mod 13782  df-seq 13914  df-exp 13975  df-fac 14181  df-bc 14210  df-hash 14238  df-shft 14959  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-limsup 15360  df-clim 15377  df-rlim 15378  df-sum 15578  df-ef 15957  df-sin 15959  df-cos 15960  df-pi 15962  df-dvds 16144  df-gcd 16382  df-prm 16555  df-numer 16617  df-denom 16618  df-struct 17026  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-mulr 17154  df-starv 17155  df-sca 17156  df-vsca 17157  df-ip 17158  df-tset 17159  df-ple 17160  df-ds 17162  df-unif 17163  df-hom 17164  df-cco 17165  df-rest 17311  df-topn 17312  df-0g 17330  df-gsum 17331  df-topgen 17332  df-pt 17333  df-prds 17336  df-xrs 17391  df-qtop 17396  df-imas 17397  df-xps 17399  df-mre 17473  df-mrc 17474  df-acs 17476  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-submnd 18609  df-mulg 18880  df-cntz 19104  df-cmn 19571  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-limc 25246  df-dv 25247  df-log 25928  df-mzpcl 41075  df-mzp 41076  df-dioph 41108  df-squarenn 41193  df-pell1qr 41194  df-pell14qr 41195  df-pell1234qr 41196  df-pellfund 41197  df-rmx 41254  df-rmy 41255
This theorem is referenced by:  rmxdioph  41369  expdiophlem2  41375
  Copyright terms: Public domain W3C validator