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

Theorem expdiophlem2 41746
Description: Lemma for expdioph 41747. Exponentiation on a restricted domain is Diophantine. (Contributed by Stefan O'Rear, 17-Oct-2014.)
Assertion
Ref Expression
expdiophlem2 {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (π‘Žβ€˜3) = ((π‘Žβ€˜1)↑(π‘Žβ€˜2)))} ∈ (Diophβ€˜3)

Proof of Theorem expdiophlem2
Dummy variables 𝑏 𝑐 𝑑 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elmapi 8839 . . . . 5 (π‘Ž ∈ (β„•0 ↑m (1...3)) β†’ π‘Ž:(1...3)βŸΆβ„•0)
2 3nn 12287 . . . . . 6 3 ∈ β„•
32jm2.27dlem3 41735 . . . . 5 3 ∈ (1...3)
4 ffvelcdm 7080 . . . . 5 ((π‘Ž:(1...3)βŸΆβ„•0 ∧ 3 ∈ (1...3)) β†’ (π‘Žβ€˜3) ∈ β„•0)
51, 3, 4sylancl 586 . . . 4 (π‘Ž ∈ (β„•0 ↑m (1...3)) β†’ (π‘Žβ€˜3) ∈ β„•0)
6 expdiophlem1 41745 . . . 4 ((π‘Žβ€˜3) ∈ β„•0 β†’ ((((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (π‘Žβ€˜3) = ((π‘Žβ€˜1)↑(π‘Žβ€˜2))) ↔ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑐 = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑑 = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ ((𝑑 βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐)) βˆ’ (π‘Žβ€˜3)))))))))
75, 6syl 17 . . 3 (π‘Ž ∈ (β„•0 ↑m (1...3)) β†’ ((((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (π‘Žβ€˜3) = ((π‘Žβ€˜1)↑(π‘Žβ€˜2))) ↔ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑐 = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑑 = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ ((𝑑 βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐)) βˆ’ (π‘Žβ€˜3)))))))))
87rabbiia 3436 . 2 {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (π‘Žβ€˜3) = ((π‘Žβ€˜1)↑(π‘Žβ€˜2)))} = {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑐 = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑑 = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ ((𝑑 βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐)) βˆ’ (π‘Žβ€˜3)))))))}
9 3nn0 12486 . . 3 3 ∈ β„•0
10 fvex 6901 . . . . . . . . 9 (π‘’β€˜5) ∈ V
11 fvex 6901 . . . . . . . . 9 (π‘’β€˜6) ∈ V
12 eqeq1 2736 . . . . . . . . . . . . . 14 (𝑐 = (π‘’β€˜5) β†’ (𝑐 = (𝑏 Yrm (π‘Žβ€˜2)) ↔ (π‘’β€˜5) = (𝑏 Yrm (π‘Žβ€˜2))))
1312anbi2d 629 . . . . . . . . . . . . 13 (𝑐 = (π‘’β€˜5) β†’ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑐 = (𝑏 Yrm (π‘Žβ€˜2))) ↔ (𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = (𝑏 Yrm (π‘Žβ€˜2)))))
1413adantr 481 . . . . . . . . . . . 12 ((𝑐 = (π‘’β€˜5) ∧ 𝑑 = (π‘’β€˜6)) β†’ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑐 = (𝑏 Yrm (π‘Žβ€˜2))) ↔ (𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = (𝑏 Yrm (π‘Žβ€˜2)))))
15 eqeq1 2736 . . . . . . . . . . . . . . 15 (𝑑 = (π‘’β€˜6) β†’ (𝑑 = (𝑏 Xrm (π‘Žβ€˜2)) ↔ (π‘’β€˜6) = (𝑏 Xrm (π‘Žβ€˜2))))
1615anbi2d 629 . . . . . . . . . . . . . 14 (𝑑 = (π‘’β€˜6) β†’ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑑 = (𝑏 Xrm (π‘Žβ€˜2))) ↔ (𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = (𝑏 Xrm (π‘Žβ€˜2)))))
1716adantl 482 . . . . . . . . . . . . 13 ((𝑐 = (π‘’β€˜5) ∧ 𝑑 = (π‘’β€˜6)) β†’ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑑 = (𝑏 Xrm (π‘Žβ€˜2))) ↔ (𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = (𝑏 Xrm (π‘Žβ€˜2)))))
18 simpr 485 . . . . . . . . . . . . . . . . 17 ((𝑐 = (π‘’β€˜5) ∧ 𝑑 = (π‘’β€˜6)) β†’ 𝑑 = (π‘’β€˜6))
19 oveq2 7413 . . . . . . . . . . . . . . . . . 18 (𝑐 = (π‘’β€˜5) β†’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐) = ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5)))
2019adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑐 = (π‘’β€˜5) ∧ 𝑑 = (π‘’β€˜6)) β†’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐) = ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5)))
2118, 20oveq12d 7423 . . . . . . . . . . . . . . . 16 ((𝑐 = (π‘’β€˜5) ∧ 𝑑 = (π‘’β€˜6)) β†’ (𝑑 βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐)) = ((π‘’β€˜6) βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5))))
2221oveq1d 7420 . . . . . . . . . . . . . . 15 ((𝑐 = (π‘’β€˜5) ∧ 𝑑 = (π‘’β€˜6)) β†’ ((𝑑 βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐)) βˆ’ (π‘Žβ€˜3)) = (((π‘’β€˜6) βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘Žβ€˜3)))
2322breq2d 5159 . . . . . . . . . . . . . 14 ((𝑐 = (π‘’β€˜5) ∧ 𝑑 = (π‘’β€˜6)) β†’ (((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ ((𝑑 βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐)) βˆ’ (π‘Žβ€˜3)) ↔ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘Žβ€˜3))))
2423anbi2d 629 . . . . . . . . . . . . 13 ((𝑐 = (π‘’β€˜5) ∧ 𝑑 = (π‘’β€˜6)) β†’ (((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ ((𝑑 βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐)) βˆ’ (π‘Žβ€˜3))) ↔ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘Žβ€˜3)))))
2517, 24anbi12d 631 . . . . . . . . . . . 12 ((𝑐 = (π‘’β€˜5) ∧ 𝑑 = (π‘’β€˜6)) β†’ (((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑑 = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ ((𝑑 βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐)) βˆ’ (π‘Žβ€˜3)))) ↔ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘Žβ€˜3))))))
2614, 25anbi12d 631 . . . . . . . . . . 11 ((𝑐 = (π‘’β€˜5) ∧ 𝑑 = (π‘’β€˜6)) β†’ (((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑐 = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑑 = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ ((𝑑 βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐)) βˆ’ (π‘Žβ€˜3))))) ↔ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘Žβ€˜3)))))))
2726anbi2d 629 . . . . . . . . . 10 ((𝑐 = (π‘’β€˜5) ∧ 𝑑 = (π‘’β€˜6)) β†’ ((((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑐 = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑑 = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ ((𝑑 βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐)) βˆ’ (π‘Žβ€˜3)))))) ↔ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘Žβ€˜3))))))))
2827anbi2d 629 . . . . . . . . 9 ((𝑐 = (π‘’β€˜5) ∧ 𝑑 = (π‘’β€˜6)) β†’ ((((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑐 = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑑 = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ ((𝑑 βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐)) βˆ’ (π‘Žβ€˜3))))))) ↔ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘Žβ€˜3)))))))))
2910, 11, 28sbc2ie 3859 . . . . . . . 8 ([(π‘’β€˜5) / 𝑐][(π‘’β€˜6) / 𝑑](((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑐 = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑑 = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ ((𝑑 βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐)) βˆ’ (π‘Žβ€˜3))))))) ↔ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘Žβ€˜3))))))))
3029sbcbii 3836 . . . . . . 7 ([(π‘’β€˜4) / 𝑏][(π‘’β€˜5) / 𝑐][(π‘’β€˜6) / 𝑑](((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑐 = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑑 = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ ((𝑑 βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐)) βˆ’ (π‘Žβ€˜3))))))) ↔ [(π‘’β€˜4) / 𝑏](((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘Žβ€˜3))))))))
3130sbcbii 3836 . . . . . 6 ([(𝑒 β†Ύ (1...3)) / π‘Ž][(π‘’β€˜4) / 𝑏][(π‘’β€˜5) / 𝑐][(π‘’β€˜6) / 𝑑](((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑐 = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑑 = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ ((𝑑 βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐)) βˆ’ (π‘Žβ€˜3))))))) ↔ [(𝑒 β†Ύ (1...3)) / π‘Ž][(π‘’β€˜4) / 𝑏](((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘Žβ€˜3))))))))
32 vex 3478 . . . . . . . 8 𝑒 ∈ V
3332resex 6027 . . . . . . 7 (𝑒 β†Ύ (1...3)) ∈ V
34 fvex 6901 . . . . . . 7 (π‘’β€˜4) ∈ V
35 df-2 12271 . . . . . . . . . . . . . 14 2 = (1 + 1)
36 df-3 12272 . . . . . . . . . . . . . . 15 3 = (2 + 1)
37 ssid 4003 . . . . . . . . . . . . . . 15 (1...3) βŠ† (1...3)
3836, 37jm2.27dlem5 41737 . . . . . . . . . . . . . 14 (1...2) βŠ† (1...3)
3935, 38jm2.27dlem5 41737 . . . . . . . . . . . . 13 (1...1) βŠ† (1...3)
40 1nn 12219 . . . . . . . . . . . . . 14 1 ∈ β„•
4140jm2.27dlem3 41735 . . . . . . . . . . . . 13 1 ∈ (1...1)
4239, 41sselii 3978 . . . . . . . . . . . 12 1 ∈ (1...3)
4342jm2.27dlem1 41733 . . . . . . . . . . 11 (π‘Ž = (𝑒 β†Ύ (1...3)) β†’ (π‘Žβ€˜1) = (π‘’β€˜1))
4443eleq1d 2818 . . . . . . . . . 10 (π‘Ž = (𝑒 β†Ύ (1...3)) β†’ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ↔ (π‘’β€˜1) ∈ (β„€β‰₯β€˜2)))
45 2nn 12281 . . . . . . . . . . . . . 14 2 ∈ β„•
4645jm2.27dlem3 41735 . . . . . . . . . . . . 13 2 ∈ (1...2)
4746, 36, 45jm2.27dlem2 41734 . . . . . . . . . . . 12 2 ∈ (1...3)
4847jm2.27dlem1 41733 . . . . . . . . . . 11 (π‘Ž = (𝑒 β†Ύ (1...3)) β†’ (π‘Žβ€˜2) = (π‘’β€˜2))
4948eleq1d 2818 . . . . . . . . . 10 (π‘Ž = (𝑒 β†Ύ (1...3)) β†’ ((π‘Žβ€˜2) ∈ β„• ↔ (π‘’β€˜2) ∈ β„•))
5044, 49anbi12d 631 . . . . . . . . 9 (π‘Ž = (𝑒 β†Ύ (1...3)) β†’ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ↔ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜2) ∈ β„•)))
5150adantr 481 . . . . . . . 8 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ↔ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜2) ∈ β„•)))
5244adantr 481 . . . . . . . . . 10 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ↔ (π‘’β€˜1) ∈ (β„€β‰₯β€˜2)))
53 id 22 . . . . . . . . . . 11 (𝑏 = (π‘’β€˜4) β†’ 𝑏 = (π‘’β€˜4))
5448oveq1d 7420 . . . . . . . . . . . 12 (π‘Ž = (𝑒 β†Ύ (1...3)) β†’ ((π‘Žβ€˜2) + 1) = ((π‘’β€˜2) + 1))
5543, 54oveq12d 7423 . . . . . . . . . . 11 (π‘Ž = (𝑒 β†Ύ (1...3)) β†’ ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1)) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1)))
5653, 55eqeqan12rd 2747 . . . . . . . . . 10 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ (𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1)) ↔ (π‘’β€˜4) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1))))
5752, 56anbi12d 631 . . . . . . . . 9 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ↔ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1)))))
58 eleq1 2821 . . . . . . . . . . . 12 (𝑏 = (π‘’β€˜4) β†’ (𝑏 ∈ (β„€β‰₯β€˜2) ↔ (π‘’β€˜4) ∈ (β„€β‰₯β€˜2)))
5958adantl 482 . . . . . . . . . . 11 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ (𝑏 ∈ (β„€β‰₯β€˜2) ↔ (π‘’β€˜4) ∈ (β„€β‰₯β€˜2)))
6053, 48oveqan12rd 7425 . . . . . . . . . . . 12 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ (𝑏 Yrm (π‘Žβ€˜2)) = ((π‘’β€˜4) Yrm (π‘’β€˜2)))
6160eqeq2d 2743 . . . . . . . . . . 11 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ ((π‘’β€˜5) = (𝑏 Yrm (π‘Žβ€˜2)) ↔ (π‘’β€˜5) = ((π‘’β€˜4) Yrm (π‘’β€˜2))))
6259, 61anbi12d 631 . . . . . . . . . 10 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = (𝑏 Yrm (π‘Žβ€˜2))) ↔ ((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = ((π‘’β€˜4) Yrm (π‘’β€˜2)))))
6353, 48oveqan12rd 7425 . . . . . . . . . . . . 13 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ (𝑏 Xrm (π‘Žβ€˜2)) = ((π‘’β€˜4) Xrm (π‘’β€˜2)))
6463eqeq2d 2743 . . . . . . . . . . . 12 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ ((π‘’β€˜6) = (𝑏 Xrm (π‘Žβ€˜2)) ↔ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2))))
6559, 64anbi12d 631 . . . . . . . . . . 11 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = (𝑏 Xrm (π‘Žβ€˜2))) ↔ ((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2)))))
663jm2.27dlem1 41733 . . . . . . . . . . . . . 14 (π‘Ž = (𝑒 β†Ύ (1...3)) β†’ (π‘Žβ€˜3) = (π‘’β€˜3))
6766adantr 481 . . . . . . . . . . . . 13 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ (π‘Žβ€˜3) = (π‘’β€˜3))
68 oveq2 7413 . . . . . . . . . . . . . . . 16 (𝑏 = (π‘’β€˜4) β†’ (2 Β· 𝑏) = (2 Β· (π‘’β€˜4)))
6968, 43oveqan12rd 7425 . . . . . . . . . . . . . . 15 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ ((2 Β· 𝑏) Β· (π‘Žβ€˜1)) = ((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)))
7043oveq1d 7420 . . . . . . . . . . . . . . . 16 (π‘Ž = (𝑒 β†Ύ (1...3)) β†’ ((π‘Žβ€˜1)↑2) = ((π‘’β€˜1)↑2))
7170adantr 481 . . . . . . . . . . . . . . 15 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ ((π‘Žβ€˜1)↑2) = ((π‘’β€˜1)↑2))
7269, 71oveq12d 7423 . . . . . . . . . . . . . 14 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ (((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) = (((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)))
7372oveq1d 7420 . . . . . . . . . . . . 13 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) = ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1))
7467, 73breq12d 5160 . . . . . . . . . . . 12 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ↔ (π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1)))
75 simpr 485 . . . . . . . . . . . . . . . . 17 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ 𝑏 = (π‘’β€˜4))
7643adantr 481 . . . . . . . . . . . . . . . . 17 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ (π‘Žβ€˜1) = (π‘’β€˜1))
7775, 76oveq12d 7423 . . . . . . . . . . . . . . . 16 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ (𝑏 βˆ’ (π‘Žβ€˜1)) = ((π‘’β€˜4) βˆ’ (π‘’β€˜1)))
7877oveq1d 7420 . . . . . . . . . . . . . . 15 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5)) = (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5)))
7978oveq2d 7421 . . . . . . . . . . . . . 14 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ ((π‘’β€˜6) βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5))) = ((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))))
8079, 67oveq12d 7423 . . . . . . . . . . . . 13 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ (((π‘’β€˜6) βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘Žβ€˜3)) = (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3)))
8173, 80breq12d 5160 . . . . . . . . . . . 12 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ (((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘Žβ€˜3)) ↔ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3))))
8274, 81anbi12d 631 . . . . . . . . . . 11 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ (((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘Žβ€˜3))) ↔ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3)))))
8365, 82anbi12d 631 . . . . . . . . . 10 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ (((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘Žβ€˜3)))) ↔ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2))) ∧ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3))))))
8462, 83anbi12d 631 . . . . . . . . 9 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ (((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘Žβ€˜3))))) ↔ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = ((π‘’β€˜4) Yrm (π‘’β€˜2))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2))) ∧ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3)))))))
8557, 84anbi12d 631 . . . . . . . 8 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ ((((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘Žβ€˜3)))))) ↔ (((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = ((π‘’β€˜4) Yrm (π‘’β€˜2))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2))) ∧ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3))))))))
8651, 85anbi12d 631 . . . . . . 7 ((π‘Ž = (𝑒 β†Ύ (1...3)) ∧ 𝑏 = (π‘’β€˜4)) β†’ ((((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘Žβ€˜3))))))) ↔ (((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜2) ∈ β„•) ∧ (((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = ((π‘’β€˜4) Yrm (π‘’β€˜2))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2))) ∧ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3)))))))))
8733, 34, 86sbc2ie 3859 . . . . . 6 ([(𝑒 β†Ύ (1...3)) / π‘Ž][(π‘’β€˜4) / 𝑏](((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘Žβ€˜3))))))) ↔ (((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜2) ∈ β„•) ∧ (((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = ((π‘’β€˜4) Yrm (π‘’β€˜2))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2))) ∧ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3))))))))
8831, 87bitri 274 . . . . 5 ([(𝑒 β†Ύ (1...3)) / π‘Ž][(π‘’β€˜4) / 𝑏][(π‘’β€˜5) / 𝑐][(π‘’β€˜6) / 𝑑](((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑐 = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑑 = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ ((𝑑 βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐)) βˆ’ (π‘Žβ€˜3))))))) ↔ (((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜2) ∈ β„•) ∧ (((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = ((π‘’β€˜4) Yrm (π‘’β€˜2))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2))) ∧ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3))))))))
8988rabbii 3438 . . . 4 {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ [(𝑒 β†Ύ (1...3)) / π‘Ž][(π‘’β€˜4) / 𝑏][(π‘’β€˜5) / 𝑐][(π‘’β€˜6) / 𝑑](((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑐 = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑑 = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ ((𝑑 βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐)) βˆ’ (π‘Žβ€˜3)))))))} = {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ (((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜2) ∈ β„•) ∧ (((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = ((π‘’β€˜4) Yrm (π‘’β€˜2))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2))) ∧ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3)))))))}
90 6nn0 12489 . . . . . . 7 6 ∈ β„•0
91 2z 12590 . . . . . . 7 2 ∈ β„€
92 ovex 7438 . . . . . . . 8 (1...6) ∈ V
93 df-4 12273 . . . . . . . . . . . 12 4 = (3 + 1)
94 df-5 12274 . . . . . . . . . . . . 13 5 = (4 + 1)
95 df-6 12275 . . . . . . . . . . . . . 14 6 = (5 + 1)
96 ssid 4003 . . . . . . . . . . . . . 14 (1...6) βŠ† (1...6)
9795, 96jm2.27dlem5 41737 . . . . . . . . . . . . 13 (1...5) βŠ† (1...6)
9894, 97jm2.27dlem5 41737 . . . . . . . . . . . 12 (1...4) βŠ† (1...6)
9993, 98jm2.27dlem5 41737 . . . . . . . . . . 11 (1...3) βŠ† (1...6)
10036, 99jm2.27dlem5 41737 . . . . . . . . . 10 (1...2) βŠ† (1...6)
10135, 100jm2.27dlem5 41737 . . . . . . . . 9 (1...1) βŠ† (1...6)
102101, 41sselii 3978 . . . . . . . 8 1 ∈ (1...6)
103 mzpproj 41460 . . . . . . . 8 (((1...6) ∈ V ∧ 1 ∈ (1...6)) β†’ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜1)) ∈ (mzPolyβ€˜(1...6)))
10492, 102, 103mp2an 690 . . . . . . 7 (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜1)) ∈ (mzPolyβ€˜(1...6))
105 eluzrabdioph 41529 . . . . . . 7 ((6 ∈ β„•0 ∧ 2 ∈ β„€ ∧ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜1)) ∈ (mzPolyβ€˜(1...6))) β†’ {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ (π‘’β€˜1) ∈ (β„€β‰₯β€˜2)} ∈ (Diophβ€˜6))
10690, 91, 104, 105mp3an 1461 . . . . . 6 {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ (π‘’β€˜1) ∈ (β„€β‰₯β€˜2)} ∈ (Diophβ€˜6)
107100, 46sselii 3978 . . . . . . . 8 2 ∈ (1...6)
108 mzpproj 41460 . . . . . . . 8 (((1...6) ∈ V ∧ 2 ∈ (1...6)) β†’ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜2)) ∈ (mzPolyβ€˜(1...6)))
10992, 107, 108mp2an 690 . . . . . . 7 (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜2)) ∈ (mzPolyβ€˜(1...6))
110 elnnrabdioph 41530 . . . . . . 7 ((6 ∈ β„•0 ∧ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜2)) ∈ (mzPolyβ€˜(1...6))) β†’ {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ (π‘’β€˜2) ∈ β„•} ∈ (Diophβ€˜6))
11190, 109, 110mp2an 690 . . . . . 6 {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ (π‘’β€˜2) ∈ β„•} ∈ (Diophβ€˜6)
112 anrabdioph 41503 . . . . . 6 (({𝑒 ∈ (β„•0 ↑m (1...6)) ∣ (π‘’β€˜1) ∈ (β„€β‰₯β€˜2)} ∈ (Diophβ€˜6) ∧ {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ (π‘’β€˜2) ∈ β„•} ∈ (Diophβ€˜6)) β†’ {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜2) ∈ β„•)} ∈ (Diophβ€˜6))
113106, 111, 112mp2an 690 . . . . 5 {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜2) ∈ β„•)} ∈ (Diophβ€˜6)
114 elmapi 8839 . . . . . . . . . . 11 (𝑒 ∈ (β„•0 ↑m (1...6)) β†’ 𝑒:(1...6)βŸΆβ„•0)
115 ffvelcdm 7080 . . . . . . . . . . 11 ((𝑒:(1...6)βŸΆβ„•0 ∧ 2 ∈ (1...6)) β†’ (π‘’β€˜2) ∈ β„•0)
116114, 107, 115sylancl 586 . . . . . . . . . 10 (𝑒 ∈ (β„•0 ↑m (1...6)) β†’ (π‘’β€˜2) ∈ β„•0)
117 peano2nn0 12508 . . . . . . . . . 10 ((π‘’β€˜2) ∈ β„•0 β†’ ((π‘’β€˜2) + 1) ∈ β„•0)
118 oveq2 7413 . . . . . . . . . . . . 13 (𝑏 = ((π‘’β€˜2) + 1) β†’ ((π‘’β€˜1) Yrm 𝑏) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1)))
119118eqeq2d 2743 . . . . . . . . . . . 12 (𝑏 = ((π‘’β€˜2) + 1) β†’ ((π‘’β€˜4) = ((π‘’β€˜1) Yrm 𝑏) ↔ (π‘’β€˜4) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1))))
120119anbi2d 629 . . . . . . . . . . 11 (𝑏 = ((π‘’β€˜2) + 1) β†’ (((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm 𝑏)) ↔ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1)))))
121120ceqsrexv 3642 . . . . . . . . . 10 (((π‘’β€˜2) + 1) ∈ β„•0 β†’ (βˆƒπ‘ ∈ β„•0 (𝑏 = ((π‘’β€˜2) + 1) ∧ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm 𝑏))) ↔ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1)))))
122116, 117, 1213syl 18 . . . . . . . . 9 (𝑒 ∈ (β„•0 ↑m (1...6)) β†’ (βˆƒπ‘ ∈ β„•0 (𝑏 = ((π‘’β€˜2) + 1) ∧ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm 𝑏))) ↔ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1)))))
123122bicomd 222 . . . . . . . 8 (𝑒 ∈ (β„•0 ↑m (1...6)) β†’ (((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1))) ↔ βˆƒπ‘ ∈ β„•0 (𝑏 = ((π‘’β€˜2) + 1) ∧ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm 𝑏)))))
124123rabbiia 3436 . . . . . . 7 {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1)))} = {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ βˆƒπ‘ ∈ β„•0 (𝑏 = ((π‘’β€˜2) + 1) ∧ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm 𝑏)))}
125 vex 3478 . . . . . . . . . . . 12 π‘Ž ∈ V
126125resex 6027 . . . . . . . . . . 11 (π‘Ž β†Ύ (1...6)) ∈ V
127 fvex 6901 . . . . . . . . . . 11 (π‘Žβ€˜7) ∈ V
128 id 22 . . . . . . . . . . . . 13 (𝑏 = (π‘Žβ€˜7) β†’ 𝑏 = (π‘Žβ€˜7))
129107jm2.27dlem1 41733 . . . . . . . . . . . . . 14 (𝑒 = (π‘Ž β†Ύ (1...6)) β†’ (π‘’β€˜2) = (π‘Žβ€˜2))
130129oveq1d 7420 . . . . . . . . . . . . 13 (𝑒 = (π‘Ž β†Ύ (1...6)) β†’ ((π‘’β€˜2) + 1) = ((π‘Žβ€˜2) + 1))
131128, 130eqeqan12rd 2747 . . . . . . . . . . . 12 ((𝑒 = (π‘Ž β†Ύ (1...6)) ∧ 𝑏 = (π‘Žβ€˜7)) β†’ (𝑏 = ((π‘’β€˜2) + 1) ↔ (π‘Žβ€˜7) = ((π‘Žβ€˜2) + 1)))
132102jm2.27dlem1 41733 . . . . . . . . . . . . . . 15 (𝑒 = (π‘Ž β†Ύ (1...6)) β†’ (π‘’β€˜1) = (π‘Žβ€˜1))
133132adantr 481 . . . . . . . . . . . . . 14 ((𝑒 = (π‘Ž β†Ύ (1...6)) ∧ 𝑏 = (π‘Žβ€˜7)) β†’ (π‘’β€˜1) = (π‘Žβ€˜1))
134133eleq1d 2818 . . . . . . . . . . . . 13 ((𝑒 = (π‘Ž β†Ύ (1...6)) ∧ 𝑏 = (π‘Žβ€˜7)) β†’ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ↔ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)))
135 4nn 12291 . . . . . . . . . . . . . . . . . 18 4 ∈ β„•
136135jm2.27dlem3 41735 . . . . . . . . . . . . . . . . 17 4 ∈ (1...4)
13798, 136sselii 3978 . . . . . . . . . . . . . . . 16 4 ∈ (1...6)
138137jm2.27dlem1 41733 . . . . . . . . . . . . . . 15 (𝑒 = (π‘Ž β†Ύ (1...6)) β†’ (π‘’β€˜4) = (π‘Žβ€˜4))
139138adantr 481 . . . . . . . . . . . . . 14 ((𝑒 = (π‘Ž β†Ύ (1...6)) ∧ 𝑏 = (π‘Žβ€˜7)) β†’ (π‘’β€˜4) = (π‘Žβ€˜4))
140132, 128oveqan12d 7424 . . . . . . . . . . . . . 14 ((𝑒 = (π‘Ž β†Ύ (1...6)) ∧ 𝑏 = (π‘Žβ€˜7)) β†’ ((π‘’β€˜1) Yrm 𝑏) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜7)))
141139, 140eqeq12d 2748 . . . . . . . . . . . . 13 ((𝑒 = (π‘Ž β†Ύ (1...6)) ∧ 𝑏 = (π‘Žβ€˜7)) β†’ ((π‘’β€˜4) = ((π‘’β€˜1) Yrm 𝑏) ↔ (π‘Žβ€˜4) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜7))))
142134, 141anbi12d 631 . . . . . . . . . . . 12 ((𝑒 = (π‘Ž β†Ύ (1...6)) ∧ 𝑏 = (π‘Žβ€˜7)) β†’ (((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm 𝑏)) ↔ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜4) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜7)))))
143131, 142anbi12d 631 . . . . . . . . . . 11 ((𝑒 = (π‘Ž β†Ύ (1...6)) ∧ 𝑏 = (π‘Žβ€˜7)) β†’ ((𝑏 = ((π‘’β€˜2) + 1) ∧ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm 𝑏))) ↔ ((π‘Žβ€˜7) = ((π‘Žβ€˜2) + 1) ∧ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜4) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜7))))))
144126, 127, 143sbc2ie 3859 . . . . . . . . . 10 ([(π‘Ž β†Ύ (1...6)) / 𝑒][(π‘Žβ€˜7) / 𝑏](𝑏 = ((π‘’β€˜2) + 1) ∧ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm 𝑏))) ↔ ((π‘Žβ€˜7) = ((π‘Žβ€˜2) + 1) ∧ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜4) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜7)))))
145144rabbii 3438 . . . . . . . . 9 {π‘Ž ∈ (β„•0 ↑m (1...7)) ∣ [(π‘Ž β†Ύ (1...6)) / 𝑒][(π‘Žβ€˜7) / 𝑏](𝑏 = ((π‘’β€˜2) + 1) ∧ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm 𝑏)))} = {π‘Ž ∈ (β„•0 ↑m (1...7)) ∣ ((π‘Žβ€˜7) = ((π‘Žβ€˜2) + 1) ∧ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜4) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜7))))}
146 7nn0 12490 . . . . . . . . . . 11 7 ∈ β„•0
147 ovex 7438 . . . . . . . . . . . 12 (1...7) ∈ V
148 7nn 12300 . . . . . . . . . . . . 13 7 ∈ β„•
149148jm2.27dlem3 41735 . . . . . . . . . . . 12 7 ∈ (1...7)
150 mzpproj 41460 . . . . . . . . . . . 12 (((1...7) ∈ V ∧ 7 ∈ (1...7)) β†’ (π‘Ž ∈ (β„€ ↑m (1...7)) ↦ (π‘Žβ€˜7)) ∈ (mzPolyβ€˜(1...7)))
151147, 149, 150mp2an 690 . . . . . . . . . . 11 (π‘Ž ∈ (β„€ ↑m (1...7)) ↦ (π‘Žβ€˜7)) ∈ (mzPolyβ€˜(1...7))
152 df-7 12276 . . . . . . . . . . . . . 14 7 = (6 + 1)
153 6nn 12297 . . . . . . . . . . . . . 14 6 ∈ β„•
154107, 152, 153jm2.27dlem2 41734 . . . . . . . . . . . . 13 2 ∈ (1...7)
155 mzpproj 41460 . . . . . . . . . . . . 13 (((1...7) ∈ V ∧ 2 ∈ (1...7)) β†’ (π‘Ž ∈ (β„€ ↑m (1...7)) ↦ (π‘Žβ€˜2)) ∈ (mzPolyβ€˜(1...7)))
156147, 154, 155mp2an 690 . . . . . . . . . . . 12 (π‘Ž ∈ (β„€ ↑m (1...7)) ↦ (π‘Žβ€˜2)) ∈ (mzPolyβ€˜(1...7))
157 1z 12588 . . . . . . . . . . . . 13 1 ∈ β„€
158 mzpconstmpt 41463 . . . . . . . . . . . . 13 (((1...7) ∈ V ∧ 1 ∈ β„€) β†’ (π‘Ž ∈ (β„€ ↑m (1...7)) ↦ 1) ∈ (mzPolyβ€˜(1...7)))
159147, 157, 158mp2an 690 . . . . . . . . . . . 12 (π‘Ž ∈ (β„€ ↑m (1...7)) ↦ 1) ∈ (mzPolyβ€˜(1...7))
160 mzpaddmpt 41464 . . . . . . . . . . . 12 (((π‘Ž ∈ (β„€ ↑m (1...7)) ↦ (π‘Žβ€˜2)) ∈ (mzPolyβ€˜(1...7)) ∧ (π‘Ž ∈ (β„€ ↑m (1...7)) ↦ 1) ∈ (mzPolyβ€˜(1...7))) β†’ (π‘Ž ∈ (β„€ ↑m (1...7)) ↦ ((π‘Žβ€˜2) + 1)) ∈ (mzPolyβ€˜(1...7)))
161156, 159, 160mp2an 690 . . . . . . . . . . 11 (π‘Ž ∈ (β„€ ↑m (1...7)) ↦ ((π‘Žβ€˜2) + 1)) ∈ (mzPolyβ€˜(1...7))
162 eqrabdioph 41500 . . . . . . . . . . 11 ((7 ∈ β„•0 ∧ (π‘Ž ∈ (β„€ ↑m (1...7)) ↦ (π‘Žβ€˜7)) ∈ (mzPolyβ€˜(1...7)) ∧ (π‘Ž ∈ (β„€ ↑m (1...7)) ↦ ((π‘Žβ€˜2) + 1)) ∈ (mzPolyβ€˜(1...7))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...7)) ∣ (π‘Žβ€˜7) = ((π‘Žβ€˜2) + 1)} ∈ (Diophβ€˜7))
163146, 151, 161, 162mp3an 1461 . . . . . . . . . 10 {π‘Ž ∈ (β„•0 ↑m (1...7)) ∣ (π‘Žβ€˜7) = ((π‘Žβ€˜2) + 1)} ∈ (Diophβ€˜7)
164 rmydioph 41738 . . . . . . . . . . 11 {𝑏 ∈ (β„•0 ↑m (1...3)) ∣ ((π‘β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘β€˜3) = ((π‘β€˜1) Yrm (π‘β€˜2)))} ∈ (Diophβ€˜3)
165 simp1 1136 . . . . . . . . . . . . . 14 (((π‘β€˜1) = (π‘Žβ€˜1) ∧ (π‘β€˜2) = (π‘Žβ€˜7) ∧ (π‘β€˜3) = (π‘Žβ€˜4)) β†’ (π‘β€˜1) = (π‘Žβ€˜1))
166165eleq1d 2818 . . . . . . . . . . . . 13 (((π‘β€˜1) = (π‘Žβ€˜1) ∧ (π‘β€˜2) = (π‘Žβ€˜7) ∧ (π‘β€˜3) = (π‘Žβ€˜4)) β†’ ((π‘β€˜1) ∈ (β„€β‰₯β€˜2) ↔ (π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2)))
167 simp3 1138 . . . . . . . . . . . . . 14 (((π‘β€˜1) = (π‘Žβ€˜1) ∧ (π‘β€˜2) = (π‘Žβ€˜7) ∧ (π‘β€˜3) = (π‘Žβ€˜4)) β†’ (π‘β€˜3) = (π‘Žβ€˜4))
168 simp2 1137 . . . . . . . . . . . . . . 15 (((π‘β€˜1) = (π‘Žβ€˜1) ∧ (π‘β€˜2) = (π‘Žβ€˜7) ∧ (π‘β€˜3) = (π‘Žβ€˜4)) β†’ (π‘β€˜2) = (π‘Žβ€˜7))
169165, 168oveq12d 7423 . . . . . . . . . . . . . 14 (((π‘β€˜1) = (π‘Žβ€˜1) ∧ (π‘β€˜2) = (π‘Žβ€˜7) ∧ (π‘β€˜3) = (π‘Žβ€˜4)) β†’ ((π‘β€˜1) Yrm (π‘β€˜2)) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜7)))
170167, 169eqeq12d 2748 . . . . . . . . . . . . 13 (((π‘β€˜1) = (π‘Žβ€˜1) ∧ (π‘β€˜2) = (π‘Žβ€˜7) ∧ (π‘β€˜3) = (π‘Žβ€˜4)) β†’ ((π‘β€˜3) = ((π‘β€˜1) Yrm (π‘β€˜2)) ↔ (π‘Žβ€˜4) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜7))))
171166, 170anbi12d 631 . . . . . . . . . . . 12 (((π‘β€˜1) = (π‘Žβ€˜1) ∧ (π‘β€˜2) = (π‘Žβ€˜7) ∧ (π‘β€˜3) = (π‘Žβ€˜4)) β†’ (((π‘β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘β€˜3) = ((π‘β€˜1) Yrm (π‘β€˜2))) ↔ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜4) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜7)))))
172102, 152, 153jm2.27dlem2 41734 . . . . . . . . . . . 12 1 ∈ (1...7)
173137, 152, 153jm2.27dlem2 41734 . . . . . . . . . . . 12 4 ∈ (1...7)
174171, 172, 149, 173rabren3dioph 41538 . . . . . . . . . . 11 ((7 ∈ β„•0 ∧ {𝑏 ∈ (β„•0 ↑m (1...3)) ∣ ((π‘β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘β€˜3) = ((π‘β€˜1) Yrm (π‘β€˜2)))} ∈ (Diophβ€˜3)) β†’ {π‘Ž ∈ (β„•0 ↑m (1...7)) ∣ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜4) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜7)))} ∈ (Diophβ€˜7))
175146, 164, 174mp2an 690 . . . . . . . . . 10 {π‘Ž ∈ (β„•0 ↑m (1...7)) ∣ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜4) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜7)))} ∈ (Diophβ€˜7)
176 anrabdioph 41503 . . . . . . . . . 10 (({π‘Ž ∈ (β„•0 ↑m (1...7)) ∣ (π‘Žβ€˜7) = ((π‘Žβ€˜2) + 1)} ∈ (Diophβ€˜7) ∧ {π‘Ž ∈ (β„•0 ↑m (1...7)) ∣ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜4) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜7)))} ∈ (Diophβ€˜7)) β†’ {π‘Ž ∈ (β„•0 ↑m (1...7)) ∣ ((π‘Žβ€˜7) = ((π‘Žβ€˜2) + 1) ∧ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜4) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜7))))} ∈ (Diophβ€˜7))
177163, 175, 176mp2an 690 . . . . . . . . 9 {π‘Ž ∈ (β„•0 ↑m (1...7)) ∣ ((π‘Žβ€˜7) = ((π‘Žβ€˜2) + 1) ∧ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜4) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜7))))} ∈ (Diophβ€˜7)
178145, 177eqeltri 2829 . . . . . . . 8 {π‘Ž ∈ (β„•0 ↑m (1...7)) ∣ [(π‘Ž β†Ύ (1...6)) / 𝑒][(π‘Žβ€˜7) / 𝑏](𝑏 = ((π‘’β€˜2) + 1) ∧ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm 𝑏)))} ∈ (Diophβ€˜7)
179152rexfrabdioph 41518 . . . . . . . 8 ((6 ∈ β„•0 ∧ {π‘Ž ∈ (β„•0 ↑m (1...7)) ∣ [(π‘Ž β†Ύ (1...6)) / 𝑒][(π‘Žβ€˜7) / 𝑏](𝑏 = ((π‘’β€˜2) + 1) ∧ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm 𝑏)))} ∈ (Diophβ€˜7)) β†’ {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ βˆƒπ‘ ∈ β„•0 (𝑏 = ((π‘’β€˜2) + 1) ∧ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm 𝑏)))} ∈ (Diophβ€˜6))
18090, 178, 179mp2an 690 . . . . . . 7 {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ βˆƒπ‘ ∈ β„•0 (𝑏 = ((π‘’β€˜2) + 1) ∧ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm 𝑏)))} ∈ (Diophβ€˜6)
181124, 180eqeltri 2829 . . . . . 6 {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1)))} ∈ (Diophβ€˜6)
182 rmydioph 41738 . . . . . . . 8 {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)))} ∈ (Diophβ€˜3)
183 simp1 1136 . . . . . . . . . . 11 (((π‘Žβ€˜1) = (π‘’β€˜4) ∧ (π‘Žβ€˜2) = (π‘’β€˜2) ∧ (π‘Žβ€˜3) = (π‘’β€˜5)) β†’ (π‘Žβ€˜1) = (π‘’β€˜4))
184183eleq1d 2818 . . . . . . . . . 10 (((π‘Žβ€˜1) = (π‘’β€˜4) ∧ (π‘Žβ€˜2) = (π‘’β€˜2) ∧ (π‘Žβ€˜3) = (π‘’β€˜5)) β†’ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ↔ (π‘’β€˜4) ∈ (β„€β‰₯β€˜2)))
185 simp3 1138 . . . . . . . . . . 11 (((π‘Žβ€˜1) = (π‘’β€˜4) ∧ (π‘Žβ€˜2) = (π‘’β€˜2) ∧ (π‘Žβ€˜3) = (π‘’β€˜5)) β†’ (π‘Žβ€˜3) = (π‘’β€˜5))
186 simp2 1137 . . . . . . . . . . . 12 (((π‘Žβ€˜1) = (π‘’β€˜4) ∧ (π‘Žβ€˜2) = (π‘’β€˜2) ∧ (π‘Žβ€˜3) = (π‘’β€˜5)) β†’ (π‘Žβ€˜2) = (π‘’β€˜2))
187183, 186oveq12d 7423 . . . . . . . . . . 11 (((π‘Žβ€˜1) = (π‘’β€˜4) ∧ (π‘Žβ€˜2) = (π‘’β€˜2) ∧ (π‘Žβ€˜3) = (π‘’β€˜5)) β†’ ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) = ((π‘’β€˜4) Yrm (π‘’β€˜2)))
188185, 187eqeq12d 2748 . . . . . . . . . 10 (((π‘Žβ€˜1) = (π‘’β€˜4) ∧ (π‘Žβ€˜2) = (π‘’β€˜2) ∧ (π‘Žβ€˜3) = (π‘’β€˜5)) β†’ ((π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)) ↔ (π‘’β€˜5) = ((π‘’β€˜4) Yrm (π‘’β€˜2))))
189184, 188anbi12d 631 . . . . . . . . 9 (((π‘Žβ€˜1) = (π‘’β€˜4) ∧ (π‘Žβ€˜2) = (π‘’β€˜2) ∧ (π‘Žβ€˜3) = (π‘’β€˜5)) β†’ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2))) ↔ ((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = ((π‘’β€˜4) Yrm (π‘’β€˜2)))))
190 5nn 12294 . . . . . . . . . . 11 5 ∈ β„•
191190jm2.27dlem3 41735 . . . . . . . . . 10 5 ∈ (1...5)
192191, 95, 190jm2.27dlem2 41734 . . . . . . . . 9 5 ∈ (1...6)
193189, 137, 107, 192rabren3dioph 41538 . . . . . . . 8 ((6 ∈ β„•0 ∧ {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜3) = ((π‘Žβ€˜1) Yrm (π‘Žβ€˜2)))} ∈ (Diophβ€˜3)) β†’ {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ ((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = ((π‘’β€˜4) Yrm (π‘’β€˜2)))} ∈ (Diophβ€˜6))
19490, 182, 193mp2an 690 . . . . . . 7 {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ ((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = ((π‘’β€˜4) Yrm (π‘’β€˜2)))} ∈ (Diophβ€˜6)
195 rmxdioph 41740 . . . . . . . . 9 {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜3) = ((π‘Žβ€˜1) Xrm (π‘Žβ€˜2)))} ∈ (Diophβ€˜3)
196 simp1 1136 . . . . . . . . . . . 12 (((π‘Žβ€˜1) = (π‘’β€˜4) ∧ (π‘Žβ€˜2) = (π‘’β€˜2) ∧ (π‘Žβ€˜3) = (π‘’β€˜6)) β†’ (π‘Žβ€˜1) = (π‘’β€˜4))
197196eleq1d 2818 . . . . . . . . . . 11 (((π‘Žβ€˜1) = (π‘’β€˜4) ∧ (π‘Žβ€˜2) = (π‘’β€˜2) ∧ (π‘Žβ€˜3) = (π‘’β€˜6)) β†’ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ↔ (π‘’β€˜4) ∈ (β„€β‰₯β€˜2)))
198 simp3 1138 . . . . . . . . . . . 12 (((π‘Žβ€˜1) = (π‘’β€˜4) ∧ (π‘Žβ€˜2) = (π‘’β€˜2) ∧ (π‘Žβ€˜3) = (π‘’β€˜6)) β†’ (π‘Žβ€˜3) = (π‘’β€˜6))
199 simp2 1137 . . . . . . . . . . . . 13 (((π‘Žβ€˜1) = (π‘’β€˜4) ∧ (π‘Žβ€˜2) = (π‘’β€˜2) ∧ (π‘Žβ€˜3) = (π‘’β€˜6)) β†’ (π‘Žβ€˜2) = (π‘’β€˜2))
200196, 199oveq12d 7423 . . . . . . . . . . . 12 (((π‘Žβ€˜1) = (π‘’β€˜4) ∧ (π‘Žβ€˜2) = (π‘’β€˜2) ∧ (π‘Žβ€˜3) = (π‘’β€˜6)) β†’ ((π‘Žβ€˜1) Xrm (π‘Žβ€˜2)) = ((π‘’β€˜4) Xrm (π‘’β€˜2)))
201198, 200eqeq12d 2748 . . . . . . . . . . 11 (((π‘Žβ€˜1) = (π‘’β€˜4) ∧ (π‘Žβ€˜2) = (π‘’β€˜2) ∧ (π‘Žβ€˜3) = (π‘’β€˜6)) β†’ ((π‘Žβ€˜3) = ((π‘Žβ€˜1) Xrm (π‘Žβ€˜2)) ↔ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2))))
202197, 201anbi12d 631 . . . . . . . . . 10 (((π‘Žβ€˜1) = (π‘’β€˜4) ∧ (π‘Žβ€˜2) = (π‘’β€˜2) ∧ (π‘Žβ€˜3) = (π‘’β€˜6)) β†’ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜3) = ((π‘Žβ€˜1) Xrm (π‘Žβ€˜2))) ↔ ((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2)))))
203153jm2.27dlem3 41735 . . . . . . . . . 10 6 ∈ (1...6)
204202, 137, 107, 203rabren3dioph 41538 . . . . . . . . 9 ((6 ∈ β„•0 ∧ {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ ((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜3) = ((π‘Žβ€˜1) Xrm (π‘Žβ€˜2)))} ∈ (Diophβ€˜3)) β†’ {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ ((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2)))} ∈ (Diophβ€˜6))
20590, 195, 204mp2an 690 . . . . . . . 8 {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ ((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2)))} ∈ (Diophβ€˜6)
20699, 3sselii 3978 . . . . . . . . . . 11 3 ∈ (1...6)
207 mzpproj 41460 . . . . . . . . . . 11 (((1...6) ∈ V ∧ 3 ∈ (1...6)) β†’ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜3)) ∈ (mzPolyβ€˜(1...6)))
20892, 206, 207mp2an 690 . . . . . . . . . 10 (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜3)) ∈ (mzPolyβ€˜(1...6))
209 mzpconstmpt 41463 . . . . . . . . . . . . . . 15 (((1...6) ∈ V ∧ 2 ∈ β„€) β†’ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ 2) ∈ (mzPolyβ€˜(1...6)))
21092, 91, 209mp2an 690 . . . . . . . . . . . . . 14 (𝑒 ∈ (β„€ ↑m (1...6)) ↦ 2) ∈ (mzPolyβ€˜(1...6))
211 mzpproj 41460 . . . . . . . . . . . . . . 15 (((1...6) ∈ V ∧ 4 ∈ (1...6)) β†’ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜4)) ∈ (mzPolyβ€˜(1...6)))
21292, 137, 211mp2an 690 . . . . . . . . . . . . . 14 (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜4)) ∈ (mzPolyβ€˜(1...6))
213 mzpmulmpt 41465 . . . . . . . . . . . . . 14 (((𝑒 ∈ (β„€ ↑m (1...6)) ↦ 2) ∈ (mzPolyβ€˜(1...6)) ∧ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜4)) ∈ (mzPolyβ€˜(1...6))) β†’ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (2 Β· (π‘’β€˜4))) ∈ (mzPolyβ€˜(1...6)))
214210, 212, 213mp2an 690 . . . . . . . . . . . . 13 (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (2 Β· (π‘’β€˜4))) ∈ (mzPolyβ€˜(1...6))
215 mzpmulmpt 41465 . . . . . . . . . . . . 13 (((𝑒 ∈ (β„€ ↑m (1...6)) ↦ (2 Β· (π‘’β€˜4))) ∈ (mzPolyβ€˜(1...6)) ∧ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜1)) ∈ (mzPolyβ€˜(1...6))) β†’ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ ((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1))) ∈ (mzPolyβ€˜(1...6)))
216214, 104, 215mp2an 690 . . . . . . . . . . . 12 (𝑒 ∈ (β„€ ↑m (1...6)) ↦ ((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1))) ∈ (mzPolyβ€˜(1...6))
217 2nn0 12485 . . . . . . . . . . . . 13 2 ∈ β„•0
218 mzpexpmpt 41468 . . . . . . . . . . . . 13 (((𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜1)) ∈ (mzPolyβ€˜(1...6)) ∧ 2 ∈ β„•0) β†’ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ ((π‘’β€˜1)↑2)) ∈ (mzPolyβ€˜(1...6)))
219104, 217, 218mp2an 690 . . . . . . . . . . . 12 (𝑒 ∈ (β„€ ↑m (1...6)) ↦ ((π‘’β€˜1)↑2)) ∈ (mzPolyβ€˜(1...6))
220 mzpsubmpt 41466 . . . . . . . . . . . 12 (((𝑒 ∈ (β„€ ↑m (1...6)) ↦ ((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1))) ∈ (mzPolyβ€˜(1...6)) ∧ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ ((π‘’β€˜1)↑2)) ∈ (mzPolyβ€˜(1...6))) β†’ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2))) ∈ (mzPolyβ€˜(1...6)))
221216, 219, 220mp2an 690 . . . . . . . . . . 11 (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2))) ∈ (mzPolyβ€˜(1...6))
222 mzpconstmpt 41463 . . . . . . . . . . . 12 (((1...6) ∈ V ∧ 1 ∈ β„€) β†’ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ 1) ∈ (mzPolyβ€˜(1...6)))
22392, 157, 222mp2an 690 . . . . . . . . . . 11 (𝑒 ∈ (β„€ ↑m (1...6)) ↦ 1) ∈ (mzPolyβ€˜(1...6))
224 mzpsubmpt 41466 . . . . . . . . . . 11 (((𝑒 ∈ (β„€ ↑m (1...6)) ↦ (((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2))) ∈ (mzPolyβ€˜(1...6)) ∧ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ 1) ∈ (mzPolyβ€˜(1...6))) β†’ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1)) ∈ (mzPolyβ€˜(1...6)))
225221, 223, 224mp2an 690 . . . . . . . . . 10 (𝑒 ∈ (β„€ ↑m (1...6)) ↦ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1)) ∈ (mzPolyβ€˜(1...6))
226 ltrabdioph 41531 . . . . . . . . . 10 ((6 ∈ β„•0 ∧ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜3)) ∈ (mzPolyβ€˜(1...6)) ∧ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1)) ∈ (mzPolyβ€˜(1...6))) β†’ {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ (π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1)} ∈ (Diophβ€˜6))
22790, 208, 225, 226mp3an 1461 . . . . . . . . 9 {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ (π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1)} ∈ (Diophβ€˜6)
228 mzpproj 41460 . . . . . . . . . . . . 13 (((1...6) ∈ V ∧ 6 ∈ (1...6)) β†’ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜6)) ∈ (mzPolyβ€˜(1...6)))
22992, 203, 228mp2an 690 . . . . . . . . . . . 12 (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜6)) ∈ (mzPolyβ€˜(1...6))
230 mzpsubmpt 41466 . . . . . . . . . . . . . 14 (((𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜4)) ∈ (mzPolyβ€˜(1...6)) ∧ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜1)) ∈ (mzPolyβ€˜(1...6))) β†’ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ ((π‘’β€˜4) βˆ’ (π‘’β€˜1))) ∈ (mzPolyβ€˜(1...6)))
231212, 104, 230mp2an 690 . . . . . . . . . . . . 13 (𝑒 ∈ (β„€ ↑m (1...6)) ↦ ((π‘’β€˜4) βˆ’ (π‘’β€˜1))) ∈ (mzPolyβ€˜(1...6))
232 mzpproj 41460 . . . . . . . . . . . . . 14 (((1...6) ∈ V ∧ 5 ∈ (1...6)) β†’ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜5)) ∈ (mzPolyβ€˜(1...6)))
23392, 192, 232mp2an 690 . . . . . . . . . . . . 13 (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜5)) ∈ (mzPolyβ€˜(1...6))
234 mzpmulmpt 41465 . . . . . . . . . . . . 13 (((𝑒 ∈ (β„€ ↑m (1...6)) ↦ ((π‘’β€˜4) βˆ’ (π‘’β€˜1))) ∈ (mzPolyβ€˜(1...6)) ∧ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜5)) ∈ (mzPolyβ€˜(1...6))) β†’ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) ∈ (mzPolyβ€˜(1...6)))
235231, 233, 234mp2an 690 . . . . . . . . . . . 12 (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) ∈ (mzPolyβ€˜(1...6))
236 mzpsubmpt 41466 . . . . . . . . . . . 12 (((𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜6)) ∈ (mzPolyβ€˜(1...6)) ∧ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) ∈ (mzPolyβ€˜(1...6))) β†’ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ ((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5)))) ∈ (mzPolyβ€˜(1...6)))
237229, 235, 236mp2an 690 . . . . . . . . . . 11 (𝑒 ∈ (β„€ ↑m (1...6)) ↦ ((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5)))) ∈ (mzPolyβ€˜(1...6))
238 mzpsubmpt 41466 . . . . . . . . . . 11 (((𝑒 ∈ (β„€ ↑m (1...6)) ↦ ((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5)))) ∈ (mzPolyβ€˜(1...6)) ∧ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (π‘’β€˜3)) ∈ (mzPolyβ€˜(1...6))) β†’ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3))) ∈ (mzPolyβ€˜(1...6)))
239237, 208, 238mp2an 690 . . . . . . . . . 10 (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3))) ∈ (mzPolyβ€˜(1...6))
240 dvdsrabdioph 41533 . . . . . . . . . 10 ((6 ∈ β„•0 ∧ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1)) ∈ (mzPolyβ€˜(1...6)) ∧ (𝑒 ∈ (β„€ ↑m (1...6)) ↦ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3))) ∈ (mzPolyβ€˜(1...6))) β†’ {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3))} ∈ (Diophβ€˜6))
24190, 225, 239, 240mp3an 1461 . . . . . . . . 9 {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3))} ∈ (Diophβ€˜6)
242 anrabdioph 41503 . . . . . . . . 9 (({𝑒 ∈ (β„•0 ↑m (1...6)) ∣ (π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1)} ∈ (Diophβ€˜6) ∧ {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3))} ∈ (Diophβ€˜6)) β†’ {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3)))} ∈ (Diophβ€˜6))
243227, 241, 242mp2an 690 . . . . . . . 8 {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3)))} ∈ (Diophβ€˜6)
244 anrabdioph 41503 . . . . . . . 8 (({𝑒 ∈ (β„•0 ↑m (1...6)) ∣ ((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2)))} ∈ (Diophβ€˜6) ∧ {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3)))} ∈ (Diophβ€˜6)) β†’ {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2))) ∧ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3))))} ∈ (Diophβ€˜6))
245205, 243, 244mp2an 690 . . . . . . 7 {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2))) ∧ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3))))} ∈ (Diophβ€˜6)
246 anrabdioph 41503 . . . . . . 7 (({𝑒 ∈ (β„•0 ↑m (1...6)) ∣ ((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = ((π‘’β€˜4) Yrm (π‘’β€˜2)))} ∈ (Diophβ€˜6) ∧ {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2))) ∧ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3))))} ∈ (Diophβ€˜6)) β†’ {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = ((π‘’β€˜4) Yrm (π‘’β€˜2))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2))) ∧ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3)))))} ∈ (Diophβ€˜6))
247194, 245, 246mp2an 690 . . . . . 6 {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = ((π‘’β€˜4) Yrm (π‘’β€˜2))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2))) ∧ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3)))))} ∈ (Diophβ€˜6)
248 anrabdioph 41503 . . . . . 6 (({𝑒 ∈ (β„•0 ↑m (1...6)) ∣ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1)))} ∈ (Diophβ€˜6) ∧ {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = ((π‘’β€˜4) Yrm (π‘’β€˜2))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2))) ∧ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3)))))} ∈ (Diophβ€˜6)) β†’ {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ (((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = ((π‘’β€˜4) Yrm (π‘’β€˜2))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2))) ∧ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3))))))} ∈ (Diophβ€˜6))
249181, 247, 248mp2an 690 . . . . 5 {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ (((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = ((π‘’β€˜4) Yrm (π‘’β€˜2))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2))) ∧ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3))))))} ∈ (Diophβ€˜6)
250 anrabdioph 41503 . . . . 5 (({𝑒 ∈ (β„•0 ↑m (1...6)) ∣ ((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜2) ∈ β„•)} ∈ (Diophβ€˜6) ∧ {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ (((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = ((π‘’β€˜4) Yrm (π‘’β€˜2))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2))) ∧ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3))))))} ∈ (Diophβ€˜6)) β†’ {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ (((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜2) ∈ β„•) ∧ (((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = ((π‘’β€˜4) Yrm (π‘’β€˜2))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2))) ∧ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3)))))))} ∈ (Diophβ€˜6))
251113, 249, 250mp2an 690 . . . 4 {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ (((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜2) ∈ β„•) ∧ (((π‘’β€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜4) = ((π‘’β€˜1) Yrm ((π‘’β€˜2) + 1))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜5) = ((π‘’β€˜4) Yrm (π‘’β€˜2))) ∧ (((π‘’β€˜4) ∈ (β„€β‰₯β€˜2) ∧ (π‘’β€˜6) = ((π‘’β€˜4) Xrm (π‘’β€˜2))) ∧ ((π‘’β€˜3) < ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· (π‘’β€˜4)) Β· (π‘’β€˜1)) βˆ’ ((π‘’β€˜1)↑2)) βˆ’ 1) βˆ₯ (((π‘’β€˜6) βˆ’ (((π‘’β€˜4) βˆ’ (π‘’β€˜1)) Β· (π‘’β€˜5))) βˆ’ (π‘’β€˜3)))))))} ∈ (Diophβ€˜6)
25289, 251eqeltri 2829 . . 3 {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ [(𝑒 β†Ύ (1...3)) / π‘Ž][(π‘’β€˜4) / 𝑏][(π‘’β€˜5) / 𝑐][(π‘’β€˜6) / 𝑑](((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑐 = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑑 = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ ((𝑑 βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐)) βˆ’ (π‘Žβ€˜3)))))))} ∈ (Diophβ€˜6)
25393, 94, 953rexfrabdioph 41520 . . 3 ((3 ∈ β„•0 ∧ {𝑒 ∈ (β„•0 ↑m (1...6)) ∣ [(𝑒 β†Ύ (1...3)) / π‘Ž][(π‘’β€˜4) / 𝑏][(π‘’β€˜5) / 𝑐][(π‘’β€˜6) / 𝑑](((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑐 = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑑 = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ ((𝑑 βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐)) βˆ’ (π‘Žβ€˜3)))))))} ∈ (Diophβ€˜6)) β†’ {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑐 = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑑 = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ ((𝑑 βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐)) βˆ’ (π‘Žβ€˜3)))))))} ∈ (Diophβ€˜3))
2549, 252, 253mp2an 690 . 2 {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ βˆƒπ‘ ∈ β„•0 βˆƒπ‘ ∈ β„•0 βˆƒπ‘‘ ∈ β„•0 (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ 𝑏 = ((π‘Žβ€˜1) Yrm ((π‘Žβ€˜2) + 1))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑐 = (𝑏 Yrm (π‘Žβ€˜2))) ∧ ((𝑏 ∈ (β„€β‰₯β€˜2) ∧ 𝑑 = (𝑏 Xrm (π‘Žβ€˜2))) ∧ ((π‘Žβ€˜3) < ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) ∧ ((((2 Β· 𝑏) Β· (π‘Žβ€˜1)) βˆ’ ((π‘Žβ€˜1)↑2)) βˆ’ 1) βˆ₯ ((𝑑 βˆ’ ((𝑏 βˆ’ (π‘Žβ€˜1)) Β· 𝑐)) βˆ’ (π‘Žβ€˜3)))))))} ∈ (Diophβ€˜3)
2558, 254eqeltri 2829 1 {π‘Ž ∈ (β„•0 ↑m (1...3)) ∣ (((π‘Žβ€˜1) ∈ (β„€β‰₯β€˜2) ∧ (π‘Žβ€˜2) ∈ β„•) ∧ (π‘Žβ€˜3) = ((π‘Žβ€˜1)↑(π‘Žβ€˜2)))} ∈ (Diophβ€˜3)
Colors of variables: wff setvar class
Syntax hints:   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  βˆƒwrex 3070  {crab 3432  Vcvv 3474  [wsbc 3776   class class class wbr 5147   ↦ cmpt 5230   β†Ύ cres 5677  βŸΆwf 6536  β€˜cfv 6540  (class class class)co 7405   ↑m cmap 8816  1c1 11107   + caddc 11109   Β· cmul 11111   < clt 11244   βˆ’ cmin 11440  β„•cn 12208  2c2 12263  3c3 12264  4c4 12265  5c5 12266  6c6 12267  7c7 12268  β„•0cn0 12468  β„€cz 12554  β„€β‰₯cuz 12818  ...cfz 13480  β†‘cexp 14023   βˆ₯ cdvds 16193  mzPolycmzp 41445  Diophcdioph 41478   Xrm crmx 41623   Yrm crmy 41624
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185  ax-mulf 11186
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7666  df-om 7852  df-1st 7971  df-2nd 7972  df-supp 8143  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-oadd 8466  df-omul 8467  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-dju 9892  df-card 9930  df-acn 9933  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-xnn0 12541  df-z 12555  df-dec 12674  df-uz 12819  df-q 12929  df-rp 12971  df-xneg 13088  df-xadd 13089  df-xmul 13090  df-ioo 13324  df-ioc 13325  df-ico 13326  df-icc 13327  df-fz 13481  df-fzo 13624  df-fl 13753  df-mod 13831  df-seq 13963  df-exp 14024  df-fac 14230  df-bc 14259  df-hash 14287  df-shft 15010  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-limsup 15411  df-clim 15428  df-rlim 15429  df-sum 15629  df-ef 16007  df-sin 16009  df-cos 16010  df-pi 16012  df-dvds 16194  df-gcd 16432  df-prm 16605  df-numer 16667  df-denom 16668  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-starv 17208  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-unif 17216  df-hom 17217  df-cco 17218  df-rest 17364  df-topn 17365  df-0g 17383  df-gsum 17384  df-topgen 17385  df-pt 17386  df-prds 17389  df-xrs 17444  df-qtop 17449  df-imas 17450  df-xps 17452  df-mre 17526  df-mrc 17527  df-acs 17529  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-submnd 18668  df-mulg 18945  df-cntz 19175  df-cmn 19644  df-psmet 20928  df-xmet 20929  df-met 20930  df-bl 20931  df-mopn 20932  df-fbas 20933  df-fg 20934  df-cnfld 20937  df-top 22387  df-topon 22404  df-topsp 22426  df-bases 22440  df-cld 22514  df-ntr 22515  df-cls 22516  df-nei 22593  df-lp 22631  df-perf 22632  df-cn 22722  df-cnp 22723  df-haus 22810  df-tx 23057  df-hmeo 23250  df-fil 23341  df-fm 23433  df-flim 23434  df-flf 23435  df-xms 23817  df-ms 23818  df-tms 23819  df-cncf 24385  df-limc 25374  df-dv 25375  df-log 26056  df-mzpcl 41446  df-mzp 41447  df-dioph 41479  df-squarenn 41564  df-pell1qr 41565  df-pell14qr 41566  df-pell1234qr 41567  df-pellfund 41568  df-rmx 41625  df-rmy 41626
This theorem is referenced by:  expdioph  41747
  Copyright terms: Public domain W3C validator