| Step |
Hyp |
Ref |
Expression |
| 1 |
|
elmapi |
⊢ ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) → 𝑎 : ( 1 ... 3 ) ⟶ ℕ0 ) |
| 2 |
|
3nn |
⊢ 3 ∈ ℕ |
| 3 |
2
|
jm2.27dlem3 |
⊢ 3 ∈ ( 1 ... 3 ) |
| 4 |
|
ffvelrn |
⊢ ( ( 𝑎 : ( 1 ... 3 ) ⟶ ℕ0 ∧ 3 ∈ ( 1 ... 3 ) ) → ( 𝑎 ‘ 3 ) ∈ ℕ0 ) |
| 5 |
1 3 4
|
sylancl |
⊢ ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) → ( 𝑎 ‘ 3 ) ∈ ℕ0 ) |
| 6 |
|
expdiophlem1 |
⊢ ( ( 𝑎 ‘ 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 ) ) ) ) ) ) ) ) ) |
| 7 |
5 6
|
syl |
⊢ ( 𝑎 ∈ ( ℕ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 ) ) ) ) ) ) ) ) ) |
| 8 |
7
|
rabbiia |
⊢ { 𝑎 ∈ ( ℕ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 |
⊢ 3 ∈ ℕ0 |
| 10 |
|
fvex |
⊢ ( 𝑒 ‘ 5 ) ∈ V |
| 11 |
|
fvex |
⊢ ( 𝑒 ‘ 6 ) ∈ V |
| 12 |
|
eqeq1 |
⊢ ( 𝑐 = ( 𝑒 ‘ 5 ) → ( 𝑐 = ( 𝑏 Yrm ( 𝑎 ‘ 2 ) ) ↔ ( 𝑒 ‘ 5 ) = ( 𝑏 Yrm ( 𝑎 ‘ 2 ) ) ) ) |
| 13 |
12
|
anbi2d |
⊢ ( 𝑐 = ( 𝑒 ‘ 5 ) → ( ( 𝑏 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑐 = ( 𝑏 Yrm ( 𝑎 ‘ 2 ) ) ) ↔ ( 𝑏 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 5 ) = ( 𝑏 Yrm ( 𝑎 ‘ 2 ) ) ) ) ) |
| 14 |
13
|
adantr |
⊢ ( ( 𝑐 = ( 𝑒 ‘ 5 ) ∧ 𝑑 = ( 𝑒 ‘ 6 ) ) → ( ( 𝑏 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑐 = ( 𝑏 Yrm ( 𝑎 ‘ 2 ) ) ) ↔ ( 𝑏 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 5 ) = ( 𝑏 Yrm ( 𝑎 ‘ 2 ) ) ) ) ) |
| 15 |
|
eqeq1 |
⊢ ( 𝑑 = ( 𝑒 ‘ 6 ) → ( 𝑑 = ( 𝑏 Xrm ( 𝑎 ‘ 2 ) ) ↔ ( 𝑒 ‘ 6 ) = ( 𝑏 Xrm ( 𝑎 ‘ 2 ) ) ) ) |
| 16 |
15
|
anbi2d |
⊢ ( 𝑑 = ( 𝑒 ‘ 6 ) → ( ( 𝑏 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑑 = ( 𝑏 Xrm ( 𝑎 ‘ 2 ) ) ) ↔ ( 𝑏 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 6 ) = ( 𝑏 Xrm ( 𝑎 ‘ 2 ) ) ) ) ) |
| 17 |
16
|
adantl |
⊢ ( ( 𝑐 = ( 𝑒 ‘ 5 ) ∧ 𝑑 = ( 𝑒 ‘ 6 ) ) → ( ( 𝑏 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑑 = ( 𝑏 Xrm ( 𝑎 ‘ 2 ) ) ) ↔ ( 𝑏 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 6 ) = ( 𝑏 Xrm ( 𝑎 ‘ 2 ) ) ) ) ) |
| 18 |
|
simpr |
⊢ ( ( 𝑐 = ( 𝑒 ‘ 5 ) ∧ 𝑑 = ( 𝑒 ‘ 6 ) ) → 𝑑 = ( 𝑒 ‘ 6 ) ) |
| 19 |
|
oveq2 |
⊢ ( 𝑐 = ( 𝑒 ‘ 5 ) → ( ( 𝑏 − ( 𝑎 ‘ 1 ) ) · 𝑐 ) = ( ( 𝑏 − ( 𝑎 ‘ 1 ) ) · ( 𝑒 ‘ 5 ) ) ) |
| 20 |
19
|
adantr |
⊢ ( ( 𝑐 = ( 𝑒 ‘ 5 ) ∧ 𝑑 = ( 𝑒 ‘ 6 ) ) → ( ( 𝑏 − ( 𝑎 ‘ 1 ) ) · 𝑐 ) = ( ( 𝑏 − ( 𝑎 ‘ 1 ) ) · ( 𝑒 ‘ 5 ) ) ) |
| 21 |
18 20
|
oveq12d |
⊢ ( ( 𝑐 = ( 𝑒 ‘ 5 ) ∧ 𝑑 = ( 𝑒 ‘ 6 ) ) → ( 𝑑 − ( ( 𝑏 − ( 𝑎 ‘ 1 ) ) · 𝑐 ) ) = ( ( 𝑒 ‘ 6 ) − ( ( 𝑏 − ( 𝑎 ‘ 1 ) ) · ( 𝑒 ‘ 5 ) ) ) ) |
| 22 |
21
|
oveq1d |
⊢ ( ( 𝑐 = ( 𝑒 ‘ 5 ) ∧ 𝑑 = ( 𝑒 ‘ 6 ) ) → ( ( 𝑑 − ( ( 𝑏 − ( 𝑎 ‘ 1 ) ) · 𝑐 ) ) − ( 𝑎 ‘ 3 ) ) = ( ( ( 𝑒 ‘ 6 ) − ( ( 𝑏 − ( 𝑎 ‘ 1 ) ) · ( 𝑒 ‘ 5 ) ) ) − ( 𝑎 ‘ 3 ) ) ) |
| 23 |
22
|
breq2d |
⊢ ( ( 𝑐 = ( 𝑒 ‘ 5 ) ∧ 𝑑 = ( 𝑒 ‘ 6 ) ) → ( ( ( ( ( 2 · 𝑏 ) · ( 𝑎 ‘ 1 ) ) − ( ( 𝑎 ‘ 1 ) ↑ 2 ) ) − 1 ) ∥ ( ( 𝑑 − ( ( 𝑏 − ( 𝑎 ‘ 1 ) ) · 𝑐 ) ) − ( 𝑎 ‘ 3 ) ) ↔ ( ( ( ( 2 · 𝑏 ) · ( 𝑎 ‘ 1 ) ) − ( ( 𝑎 ‘ 1 ) ↑ 2 ) ) − 1 ) ∥ ( ( ( 𝑒 ‘ 6 ) − ( ( 𝑏 − ( 𝑎 ‘ 1 ) ) · ( 𝑒 ‘ 5 ) ) ) − ( 𝑎 ‘ 3 ) ) ) ) |
| 24 |
23
|
anbi2d |
⊢ ( ( 𝑐 = ( 𝑒 ‘ 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 ) ) ) ) ) |
| 25 |
17 24
|
anbi12d |
⊢ ( ( 𝑐 = ( 𝑒 ‘ 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 ) ) ) ) ) ) |
| 26 |
14 25
|
anbi12d |
⊢ ( ( 𝑐 = ( 𝑒 ‘ 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 ) ) ) ) ) ) ) |
| 27 |
26
|
anbi2d |
⊢ ( ( 𝑐 = ( 𝑒 ‘ 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 ) ) ) ) ) ) ) ) |
| 28 |
27
|
anbi2d |
⊢ ( ( 𝑐 = ( 𝑒 ‘ 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 ) ) ) ) ) ) ) ) ) |
| 29 |
10 11 28
|
sbc2ie |
⊢ ( [ ( 𝑒 ‘ 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 ) ) ) ) ) ) ) ) |
| 30 |
29
|
sbcbii |
⊢ ( [ ( 𝑒 ‘ 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 ) ) ) ) ) ) ) ) |
| 31 |
30
|
sbcbii |
⊢ ( [ ( 𝑒 ↾ ( 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 |
⊢ 𝑒 ∈ V |
| 33 |
32
|
resex |
⊢ ( 𝑒 ↾ ( 1 ... 3 ) ) ∈ V |
| 34 |
|
fvex |
⊢ ( 𝑒 ‘ 4 ) ∈ V |
| 35 |
|
df-2 |
⊢ 2 = ( 1 + 1 ) |
| 36 |
|
df-3 |
⊢ 3 = ( 2 + 1 ) |
| 37 |
|
ssid |
⊢ ( 1 ... 3 ) ⊆ ( 1 ... 3 ) |
| 38 |
36 37
|
jm2.27dlem5 |
⊢ ( 1 ... 2 ) ⊆ ( 1 ... 3 ) |
| 39 |
35 38
|
jm2.27dlem5 |
⊢ ( 1 ... 1 ) ⊆ ( 1 ... 3 ) |
| 40 |
|
1nn |
⊢ 1 ∈ ℕ |
| 41 |
40
|
jm2.27dlem3 |
⊢ 1 ∈ ( 1 ... 1 ) |
| 42 |
39 41
|
sselii |
⊢ 1 ∈ ( 1 ... 3 ) |
| 43 |
42
|
jm2.27dlem1 |
⊢ ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) → ( 𝑎 ‘ 1 ) = ( 𝑒 ‘ 1 ) ) |
| 44 |
43
|
eleq1d |
⊢ ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) → ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) ) |
| 45 |
|
2nn |
⊢ 2 ∈ ℕ |
| 46 |
45
|
jm2.27dlem3 |
⊢ 2 ∈ ( 1 ... 2 ) |
| 47 |
46 36 45
|
jm2.27dlem2 |
⊢ 2 ∈ ( 1 ... 3 ) |
| 48 |
47
|
jm2.27dlem1 |
⊢ ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) → ( 𝑎 ‘ 2 ) = ( 𝑒 ‘ 2 ) ) |
| 49 |
48
|
eleq1d |
⊢ ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) → ( ( 𝑎 ‘ 2 ) ∈ ℕ ↔ ( 𝑒 ‘ 2 ) ∈ ℕ ) ) |
| 50 |
44 49
|
anbi12d |
⊢ ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) → ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ↔ ( ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 2 ) ∈ ℕ ) ) ) |
| 51 |
50
|
adantr |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ↔ ( ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 2 ) ∈ ℕ ) ) ) |
| 52 |
44
|
adantr |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) ) |
| 53 |
|
id |
⊢ ( 𝑏 = ( 𝑒 ‘ 4 ) → 𝑏 = ( 𝑒 ‘ 4 ) ) |
| 54 |
48
|
oveq1d |
⊢ ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) → ( ( 𝑎 ‘ 2 ) + 1 ) = ( ( 𝑒 ‘ 2 ) + 1 ) ) |
| 55 |
43 54
|
oveq12d |
⊢ ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) → ( ( 𝑎 ‘ 1 ) Yrm ( ( 𝑎 ‘ 2 ) + 1 ) ) = ( ( 𝑒 ‘ 1 ) Yrm ( ( 𝑒 ‘ 2 ) + 1 ) ) ) |
| 56 |
53 55
|
eqeqan12rd |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( 𝑏 = ( ( 𝑎 ‘ 1 ) Yrm ( ( 𝑎 ‘ 2 ) + 1 ) ) ↔ ( 𝑒 ‘ 4 ) = ( ( 𝑒 ‘ 1 ) Yrm ( ( 𝑒 ‘ 2 ) + 1 ) ) ) ) |
| 57 |
52 56
|
anbi12d |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 = ( ( 𝑎 ‘ 1 ) Yrm ( ( 𝑎 ‘ 2 ) + 1 ) ) ) ↔ ( ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 4 ) = ( ( 𝑒 ‘ 1 ) Yrm ( ( 𝑒 ‘ 2 ) + 1 ) ) ) ) ) |
| 58 |
|
eleq1 |
⊢ ( 𝑏 = ( 𝑒 ‘ 4 ) → ( 𝑏 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑒 ‘ 4 ) ∈ ( ℤ≥ ‘ 2 ) ) ) |
| 59 |
58
|
adantl |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( 𝑏 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑒 ‘ 4 ) ∈ ( ℤ≥ ‘ 2 ) ) ) |
| 60 |
53 48
|
oveqan12rd |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( 𝑏 Yrm ( 𝑎 ‘ 2 ) ) = ( ( 𝑒 ‘ 4 ) Yrm ( 𝑒 ‘ 2 ) ) ) |
| 61 |
60
|
eqeq2d |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( ( 𝑒 ‘ 5 ) = ( 𝑏 Yrm ( 𝑎 ‘ 2 ) ) ↔ ( 𝑒 ‘ 5 ) = ( ( 𝑒 ‘ 4 ) Yrm ( 𝑒 ‘ 2 ) ) ) ) |
| 62 |
59 61
|
anbi12d |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( ( 𝑏 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 5 ) = ( 𝑏 Yrm ( 𝑎 ‘ 2 ) ) ) ↔ ( ( 𝑒 ‘ 4 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 5 ) = ( ( 𝑒 ‘ 4 ) Yrm ( 𝑒 ‘ 2 ) ) ) ) ) |
| 63 |
53 48
|
oveqan12rd |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( 𝑏 Xrm ( 𝑎 ‘ 2 ) ) = ( ( 𝑒 ‘ 4 ) Xrm ( 𝑒 ‘ 2 ) ) ) |
| 64 |
63
|
eqeq2d |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( ( 𝑒 ‘ 6 ) = ( 𝑏 Xrm ( 𝑎 ‘ 2 ) ) ↔ ( 𝑒 ‘ 6 ) = ( ( 𝑒 ‘ 4 ) Xrm ( 𝑒 ‘ 2 ) ) ) ) |
| 65 |
59 64
|
anbi12d |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( ( 𝑏 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 6 ) = ( 𝑏 Xrm ( 𝑎 ‘ 2 ) ) ) ↔ ( ( 𝑒 ‘ 4 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 6 ) = ( ( 𝑒 ‘ 4 ) Xrm ( 𝑒 ‘ 2 ) ) ) ) ) |
| 66 |
3
|
jm2.27dlem1 |
⊢ ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) → ( 𝑎 ‘ 3 ) = ( 𝑒 ‘ 3 ) ) |
| 67 |
66
|
adantr |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( 𝑎 ‘ 3 ) = ( 𝑒 ‘ 3 ) ) |
| 68 |
|
oveq2 |
⊢ ( 𝑏 = ( 𝑒 ‘ 4 ) → ( 2 · 𝑏 ) = ( 2 · ( 𝑒 ‘ 4 ) ) ) |
| 69 |
68 43
|
oveqan12rd |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( ( 2 · 𝑏 ) · ( 𝑎 ‘ 1 ) ) = ( ( 2 · ( 𝑒 ‘ 4 ) ) · ( 𝑒 ‘ 1 ) ) ) |
| 70 |
43
|
oveq1d |
⊢ ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) → ( ( 𝑎 ‘ 1 ) ↑ 2 ) = ( ( 𝑒 ‘ 1 ) ↑ 2 ) ) |
| 71 |
70
|
adantr |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( ( 𝑎 ‘ 1 ) ↑ 2 ) = ( ( 𝑒 ‘ 1 ) ↑ 2 ) ) |
| 72 |
69 71
|
oveq12d |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( ( ( 2 · 𝑏 ) · ( 𝑎 ‘ 1 ) ) − ( ( 𝑎 ‘ 1 ) ↑ 2 ) ) = ( ( ( 2 · ( 𝑒 ‘ 4 ) ) · ( 𝑒 ‘ 1 ) ) − ( ( 𝑒 ‘ 1 ) ↑ 2 ) ) ) |
| 73 |
72
|
oveq1d |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( ( ( ( 2 · 𝑏 ) · ( 𝑎 ‘ 1 ) ) − ( ( 𝑎 ‘ 1 ) ↑ 2 ) ) − 1 ) = ( ( ( ( 2 · ( 𝑒 ‘ 4 ) ) · ( 𝑒 ‘ 1 ) ) − ( ( 𝑒 ‘ 1 ) ↑ 2 ) ) − 1 ) ) |
| 74 |
67 73
|
breq12d |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( ( 𝑎 ‘ 3 ) < ( ( ( ( 2 · 𝑏 ) · ( 𝑎 ‘ 1 ) ) − ( ( 𝑎 ‘ 1 ) ↑ 2 ) ) − 1 ) ↔ ( 𝑒 ‘ 3 ) < ( ( ( ( 2 · ( 𝑒 ‘ 4 ) ) · ( 𝑒 ‘ 1 ) ) − ( ( 𝑒 ‘ 1 ) ↑ 2 ) ) − 1 ) ) ) |
| 75 |
|
simpr |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → 𝑏 = ( 𝑒 ‘ 4 ) ) |
| 76 |
43
|
adantr |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( 𝑎 ‘ 1 ) = ( 𝑒 ‘ 1 ) ) |
| 77 |
75 76
|
oveq12d |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( 𝑏 − ( 𝑎 ‘ 1 ) ) = ( ( 𝑒 ‘ 4 ) − ( 𝑒 ‘ 1 ) ) ) |
| 78 |
77
|
oveq1d |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( ( 𝑏 − ( 𝑎 ‘ 1 ) ) · ( 𝑒 ‘ 5 ) ) = ( ( ( 𝑒 ‘ 4 ) − ( 𝑒 ‘ 1 ) ) · ( 𝑒 ‘ 5 ) ) ) |
| 79 |
78
|
oveq2d |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( ( 𝑒 ‘ 6 ) − ( ( 𝑏 − ( 𝑎 ‘ 1 ) ) · ( 𝑒 ‘ 5 ) ) ) = ( ( 𝑒 ‘ 6 ) − ( ( ( 𝑒 ‘ 4 ) − ( 𝑒 ‘ 1 ) ) · ( 𝑒 ‘ 5 ) ) ) ) |
| 80 |
79 67
|
oveq12d |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( ( ( 𝑒 ‘ 6 ) − ( ( 𝑏 − ( 𝑎 ‘ 1 ) ) · ( 𝑒 ‘ 5 ) ) ) − ( 𝑎 ‘ 3 ) ) = ( ( ( 𝑒 ‘ 6 ) − ( ( ( 𝑒 ‘ 4 ) − ( 𝑒 ‘ 1 ) ) · ( 𝑒 ‘ 5 ) ) ) − ( 𝑒 ‘ 3 ) ) ) |
| 81 |
73 80
|
breq12d |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑒 ‘ 4 ) ) → ( ( ( ( ( 2 · 𝑏 ) · ( 𝑎 ‘ 1 ) ) − ( ( 𝑎 ‘ 1 ) ↑ 2 ) ) − 1 ) ∥ ( ( ( 𝑒 ‘ 6 ) − ( ( 𝑏 − ( 𝑎 ‘ 1 ) ) · ( 𝑒 ‘ 5 ) ) ) − ( 𝑎 ‘ 3 ) ) ↔ ( ( ( ( 2 · ( 𝑒 ‘ 4 ) ) · ( 𝑒 ‘ 1 ) ) − ( ( 𝑒 ‘ 1 ) ↑ 2 ) ) − 1 ) ∥ ( ( ( 𝑒 ‘ 6 ) − ( ( ( 𝑒 ‘ 4 ) − ( 𝑒 ‘ 1 ) ) · ( 𝑒 ‘ 5 ) ) ) − ( 𝑒 ‘ 3 ) ) ) ) |
| 82 |
74 81
|
anbi12d |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 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 ) ) ) ) ) |
| 83 |
65 82
|
anbi12d |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 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 ) ) ) ) ) ) |
| 84 |
62 83
|
anbi12d |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 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 ) ) ) ) ) ) ) |
| 85 |
57 84
|
anbi12d |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 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 ) ) ) ) ) ) ) ) |
| 86 |
51 85
|
anbi12d |
⊢ ( ( 𝑎 = ( 𝑒 ↾ ( 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 ) ) ) ) ) ) ) ) ) |
| 87 |
33 34 86
|
sbc2ie |
⊢ ( [ ( 𝑒 ↾ ( 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 ) ) ) ) ) ) ) ) |
| 88 |
31 87
|
bitri |
⊢ ( [ ( 𝑒 ↾ ( 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 ) ) ) ) ) ) ) ) |
| 89 |
88
|
rabbii |
⊢ { 𝑒 ∈ ( ℕ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 |
⊢ 6 ∈ ℕ0 |
| 91 |
|
2z |
⊢ 2 ∈ ℤ |
| 92 |
|
ovex |
⊢ ( 1 ... 6 ) ∈ V |
| 93 |
|
df-4 |
⊢ 4 = ( 3 + 1 ) |
| 94 |
|
df-5 |
⊢ 5 = ( 4 + 1 ) |
| 95 |
|
df-6 |
⊢ 6 = ( 5 + 1 ) |
| 96 |
|
ssid |
⊢ ( 1 ... 6 ) ⊆ ( 1 ... 6 ) |
| 97 |
95 96
|
jm2.27dlem5 |
⊢ ( 1 ... 5 ) ⊆ ( 1 ... 6 ) |
| 98 |
94 97
|
jm2.27dlem5 |
⊢ ( 1 ... 4 ) ⊆ ( 1 ... 6 ) |
| 99 |
93 98
|
jm2.27dlem5 |
⊢ ( 1 ... 3 ) ⊆ ( 1 ... 6 ) |
| 100 |
36 99
|
jm2.27dlem5 |
⊢ ( 1 ... 2 ) ⊆ ( 1 ... 6 ) |
| 101 |
35 100
|
jm2.27dlem5 |
⊢ ( 1 ... 1 ) ⊆ ( 1 ... 6 ) |
| 102 |
101 41
|
sselii |
⊢ 1 ∈ ( 1 ... 6 ) |
| 103 |
|
mzpproj |
⊢ ( ( ( 1 ... 6 ) ∈ V ∧ 1 ∈ ( 1 ... 6 ) ) → ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 𝑒 ‘ 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ) |
| 104 |
92 102 103
|
mp2an |
⊢ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 𝑒 ‘ 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) |
| 105 |
|
eluzrabdioph |
⊢ ( ( 6 ∈ ℕ0 ∧ 2 ∈ ℤ ∧ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 𝑒 ‘ 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ) → { 𝑒 ∈ ( ℕ0 ↑m ( 1 ... 6 ) ) ∣ ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) } ∈ ( Dioph ‘ 6 ) ) |
| 106 |
90 91 104 105
|
mp3an |
⊢ { 𝑒 ∈ ( ℕ0 ↑m ( 1 ... 6 ) ) ∣ ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) } ∈ ( Dioph ‘ 6 ) |
| 107 |
100 46
|
sselii |
⊢ 2 ∈ ( 1 ... 6 ) |
| 108 |
|
mzpproj |
⊢ ( ( ( 1 ... 6 ) ∈ V ∧ 2 ∈ ( 1 ... 6 ) ) → ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 𝑒 ‘ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ) |
| 109 |
92 107 108
|
mp2an |
⊢ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 𝑒 ‘ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) |
| 110 |
|
elnnrabdioph |
⊢ ( ( 6 ∈ ℕ0 ∧ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 𝑒 ‘ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ) → { 𝑒 ∈ ( ℕ0 ↑m ( 1 ... 6 ) ) ∣ ( 𝑒 ‘ 2 ) ∈ ℕ } ∈ ( Dioph ‘ 6 ) ) |
| 111 |
90 109 110
|
mp2an |
⊢ { 𝑒 ∈ ( ℕ0 ↑m ( 1 ... 6 ) ) ∣ ( 𝑒 ‘ 2 ) ∈ ℕ } ∈ ( Dioph ‘ 6 ) |
| 112 |
|
anrabdioph |
⊢ ( ( { 𝑒 ∈ ( ℕ0 ↑m ( 1 ... 6 ) ) ∣ ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) } ∈ ( Dioph ‘ 6 ) ∧ { 𝑒 ∈ ( ℕ0 ↑m ( 1 ... 6 ) ) ∣ ( 𝑒 ‘ 2 ) ∈ ℕ } ∈ ( Dioph ‘ 6 ) ) → { 𝑒 ∈ ( ℕ0 ↑m ( 1 ... 6 ) ) ∣ ( ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 2 ) ∈ ℕ ) } ∈ ( Dioph ‘ 6 ) ) |
| 113 |
106 111 112
|
mp2an |
⊢ { 𝑒 ∈ ( ℕ0 ↑m ( 1 ... 6 ) ) ∣ ( ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 2 ) ∈ ℕ ) } ∈ ( Dioph ‘ 6 ) |
| 114 |
|
elmapi |
⊢ ( 𝑒 ∈ ( ℕ0 ↑m ( 1 ... 6 ) ) → 𝑒 : ( 1 ... 6 ) ⟶ ℕ0 ) |
| 115 |
|
ffvelrn |
⊢ ( ( 𝑒 : ( 1 ... 6 ) ⟶ ℕ0 ∧ 2 ∈ ( 1 ... 6 ) ) → ( 𝑒 ‘ 2 ) ∈ ℕ0 ) |
| 116 |
114 107 115
|
sylancl |
⊢ ( 𝑒 ∈ ( ℕ0 ↑m ( 1 ... 6 ) ) → ( 𝑒 ‘ 2 ) ∈ ℕ0 ) |
| 117 |
|
peano2nn0 |
⊢ ( ( 𝑒 ‘ 2 ) ∈ ℕ0 → ( ( 𝑒 ‘ 2 ) + 1 ) ∈ ℕ0 ) |
| 118 |
|
oveq2 |
⊢ ( 𝑏 = ( ( 𝑒 ‘ 2 ) + 1 ) → ( ( 𝑒 ‘ 1 ) Yrm 𝑏 ) = ( ( 𝑒 ‘ 1 ) Yrm ( ( 𝑒 ‘ 2 ) + 1 ) ) ) |
| 119 |
118
|
eqeq2d |
⊢ ( 𝑏 = ( ( 𝑒 ‘ 2 ) + 1 ) → ( ( 𝑒 ‘ 4 ) = ( ( 𝑒 ‘ 1 ) Yrm 𝑏 ) ↔ ( 𝑒 ‘ 4 ) = ( ( 𝑒 ‘ 1 ) Yrm ( ( 𝑒 ‘ 2 ) + 1 ) ) ) ) |
| 120 |
119
|
anbi2d |
⊢ ( 𝑏 = ( ( 𝑒 ‘ 2 ) + 1 ) → ( ( ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 4 ) = ( ( 𝑒 ‘ 1 ) Yrm 𝑏 ) ) ↔ ( ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 4 ) = ( ( 𝑒 ‘ 1 ) Yrm ( ( 𝑒 ‘ 2 ) + 1 ) ) ) ) ) |
| 121 |
120
|
ceqsrexv |
⊢ ( ( ( 𝑒 ‘ 2 ) + 1 ) ∈ ℕ0 → ( ∃ 𝑏 ∈ ℕ0 ( 𝑏 = ( ( 𝑒 ‘ 2 ) + 1 ) ∧ ( ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 4 ) = ( ( 𝑒 ‘ 1 ) Yrm 𝑏 ) ) ) ↔ ( ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 4 ) = ( ( 𝑒 ‘ 1 ) Yrm ( ( 𝑒 ‘ 2 ) + 1 ) ) ) ) ) |
| 122 |
116 117 121
|
3syl |
⊢ ( 𝑒 ∈ ( ℕ0 ↑m ( 1 ... 6 ) ) → ( ∃ 𝑏 ∈ ℕ0 ( 𝑏 = ( ( 𝑒 ‘ 2 ) + 1 ) ∧ ( ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 4 ) = ( ( 𝑒 ‘ 1 ) Yrm 𝑏 ) ) ) ↔ ( ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 4 ) = ( ( 𝑒 ‘ 1 ) Yrm ( ( 𝑒 ‘ 2 ) + 1 ) ) ) ) ) |
| 123 |
122
|
bicomd |
⊢ ( 𝑒 ∈ ( ℕ0 ↑m ( 1 ... 6 ) ) → ( ( ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 4 ) = ( ( 𝑒 ‘ 1 ) Yrm ( ( 𝑒 ‘ 2 ) + 1 ) ) ) ↔ ∃ 𝑏 ∈ ℕ0 ( 𝑏 = ( ( 𝑒 ‘ 2 ) + 1 ) ∧ ( ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 4 ) = ( ( 𝑒 ‘ 1 ) Yrm 𝑏 ) ) ) ) ) |
| 124 |
123
|
rabbiia |
⊢ { 𝑒 ∈ ( ℕ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 |
⊢ 𝑎 ∈ V |
| 126 |
125
|
resex |
⊢ ( 𝑎 ↾ ( 1 ... 6 ) ) ∈ V |
| 127 |
|
fvex |
⊢ ( 𝑎 ‘ 7 ) ∈ V |
| 128 |
|
id |
⊢ ( 𝑏 = ( 𝑎 ‘ 7 ) → 𝑏 = ( 𝑎 ‘ 7 ) ) |
| 129 |
107
|
jm2.27dlem1 |
⊢ ( 𝑒 = ( 𝑎 ↾ ( 1 ... 6 ) ) → ( 𝑒 ‘ 2 ) = ( 𝑎 ‘ 2 ) ) |
| 130 |
129
|
oveq1d |
⊢ ( 𝑒 = ( 𝑎 ↾ ( 1 ... 6 ) ) → ( ( 𝑒 ‘ 2 ) + 1 ) = ( ( 𝑎 ‘ 2 ) + 1 ) ) |
| 131 |
128 130
|
eqeqan12rd |
⊢ ( ( 𝑒 = ( 𝑎 ↾ ( 1 ... 6 ) ) ∧ 𝑏 = ( 𝑎 ‘ 7 ) ) → ( 𝑏 = ( ( 𝑒 ‘ 2 ) + 1 ) ↔ ( 𝑎 ‘ 7 ) = ( ( 𝑎 ‘ 2 ) + 1 ) ) ) |
| 132 |
102
|
jm2.27dlem1 |
⊢ ( 𝑒 = ( 𝑎 ↾ ( 1 ... 6 ) ) → ( 𝑒 ‘ 1 ) = ( 𝑎 ‘ 1 ) ) |
| 133 |
132
|
adantr |
⊢ ( ( 𝑒 = ( 𝑎 ↾ ( 1 ... 6 ) ) ∧ 𝑏 = ( 𝑎 ‘ 7 ) ) → ( 𝑒 ‘ 1 ) = ( 𝑎 ‘ 1 ) ) |
| 134 |
133
|
eleq1d |
⊢ ( ( 𝑒 = ( 𝑎 ↾ ( 1 ... 6 ) ) ∧ 𝑏 = ( 𝑎 ‘ 7 ) ) → ( ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) ) |
| 135 |
|
4nn |
⊢ 4 ∈ ℕ |
| 136 |
135
|
jm2.27dlem3 |
⊢ 4 ∈ ( 1 ... 4 ) |
| 137 |
98 136
|
sselii |
⊢ 4 ∈ ( 1 ... 6 ) |
| 138 |
137
|
jm2.27dlem1 |
⊢ ( 𝑒 = ( 𝑎 ↾ ( 1 ... 6 ) ) → ( 𝑒 ‘ 4 ) = ( 𝑎 ‘ 4 ) ) |
| 139 |
138
|
adantr |
⊢ ( ( 𝑒 = ( 𝑎 ↾ ( 1 ... 6 ) ) ∧ 𝑏 = ( 𝑎 ‘ 7 ) ) → ( 𝑒 ‘ 4 ) = ( 𝑎 ‘ 4 ) ) |
| 140 |
132 128
|
oveqan12d |
⊢ ( ( 𝑒 = ( 𝑎 ↾ ( 1 ... 6 ) ) ∧ 𝑏 = ( 𝑎 ‘ 7 ) ) → ( ( 𝑒 ‘ 1 ) Yrm 𝑏 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 7 ) ) ) |
| 141 |
139 140
|
eqeq12d |
⊢ ( ( 𝑒 = ( 𝑎 ↾ ( 1 ... 6 ) ) ∧ 𝑏 = ( 𝑎 ‘ 7 ) ) → ( ( 𝑒 ‘ 4 ) = ( ( 𝑒 ‘ 1 ) Yrm 𝑏 ) ↔ ( 𝑎 ‘ 4 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 7 ) ) ) ) |
| 142 |
134 141
|
anbi12d |
⊢ ( ( 𝑒 = ( 𝑎 ↾ ( 1 ... 6 ) ) ∧ 𝑏 = ( 𝑎 ‘ 7 ) ) → ( ( ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 4 ) = ( ( 𝑒 ‘ 1 ) Yrm 𝑏 ) ) ↔ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑎 ‘ 4 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 7 ) ) ) ) ) |
| 143 |
131 142
|
anbi12d |
⊢ ( ( 𝑒 = ( 𝑎 ↾ ( 1 ... 6 ) ) ∧ 𝑏 = ( 𝑎 ‘ 7 ) ) → ( ( 𝑏 = ( ( 𝑒 ‘ 2 ) + 1 ) ∧ ( ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 4 ) = ( ( 𝑒 ‘ 1 ) Yrm 𝑏 ) ) ) ↔ ( ( 𝑎 ‘ 7 ) = ( ( 𝑎 ‘ 2 ) + 1 ) ∧ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑎 ‘ 4 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 7 ) ) ) ) ) ) |
| 144 |
126 127 143
|
sbc2ie |
⊢ ( [ ( 𝑎 ↾ ( 1 ... 6 ) ) / 𝑒 ] [ ( 𝑎 ‘ 7 ) / 𝑏 ] ( 𝑏 = ( ( 𝑒 ‘ 2 ) + 1 ) ∧ ( ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 4 ) = ( ( 𝑒 ‘ 1 ) Yrm 𝑏 ) ) ) ↔ ( ( 𝑎 ‘ 7 ) = ( ( 𝑎 ‘ 2 ) + 1 ) ∧ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑎 ‘ 4 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 7 ) ) ) ) ) |
| 145 |
144
|
rabbii |
⊢ { 𝑎 ∈ ( ℕ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 |
⊢ 7 ∈ ℕ0 |
| 147 |
|
ovex |
⊢ ( 1 ... 7 ) ∈ V |
| 148 |
|
7nn |
⊢ 7 ∈ ℕ |
| 149 |
148
|
jm2.27dlem3 |
⊢ 7 ∈ ( 1 ... 7 ) |
| 150 |
|
mzpproj |
⊢ ( ( ( 1 ... 7 ) ∈ V ∧ 7 ∈ ( 1 ... 7 ) ) → ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 7 ) ) ↦ ( 𝑎 ‘ 7 ) ) ∈ ( mzPoly ‘ ( 1 ... 7 ) ) ) |
| 151 |
147 149 150
|
mp2an |
⊢ ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 7 ) ) ↦ ( 𝑎 ‘ 7 ) ) ∈ ( mzPoly ‘ ( 1 ... 7 ) ) |
| 152 |
|
df-7 |
⊢ 7 = ( 6 + 1 ) |
| 153 |
|
6nn |
⊢ 6 ∈ ℕ |
| 154 |
107 152 153
|
jm2.27dlem2 |
⊢ 2 ∈ ( 1 ... 7 ) |
| 155 |
|
mzpproj |
⊢ ( ( ( 1 ... 7 ) ∈ V ∧ 2 ∈ ( 1 ... 7 ) ) → ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 7 ) ) ↦ ( 𝑎 ‘ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 7 ) ) ) |
| 156 |
147 154 155
|
mp2an |
⊢ ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 7 ) ) ↦ ( 𝑎 ‘ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 7 ) ) |
| 157 |
|
1z |
⊢ 1 ∈ ℤ |
| 158 |
|
mzpconstmpt |
⊢ ( ( ( 1 ... 7 ) ∈ V ∧ 1 ∈ ℤ ) → ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 7 ) ) ↦ 1 ) ∈ ( mzPoly ‘ ( 1 ... 7 ) ) ) |
| 159 |
147 157 158
|
mp2an |
⊢ ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 7 ) ) ↦ 1 ) ∈ ( mzPoly ‘ ( 1 ... 7 ) ) |
| 160 |
|
mzpaddmpt |
⊢ ( ( ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 7 ) ) ↦ ( 𝑎 ‘ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 7 ) ) ∧ ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 7 ) ) ↦ 1 ) ∈ ( mzPoly ‘ ( 1 ... 7 ) ) ) → ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 7 ) ) ↦ ( ( 𝑎 ‘ 2 ) + 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 7 ) ) ) |
| 161 |
156 159 160
|
mp2an |
⊢ ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 7 ) ) ↦ ( ( 𝑎 ‘ 2 ) + 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 7 ) ) |
| 162 |
|
eqrabdioph |
⊢ ( ( 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 ) ) |
| 163 |
146 151 161 162
|
mp3an |
⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 7 ) ) ∣ ( 𝑎 ‘ 7 ) = ( ( 𝑎 ‘ 2 ) + 1 ) } ∈ ( Dioph ‘ 7 ) |
| 164 |
|
rmydioph |
⊢ { 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( ( 𝑏 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑏 ‘ 3 ) = ( ( 𝑏 ‘ 1 ) Yrm ( 𝑏 ‘ 2 ) ) ) } ∈ ( Dioph ‘ 3 ) |
| 165 |
|
simp1 |
⊢ ( ( ( 𝑏 ‘ 1 ) = ( 𝑎 ‘ 1 ) ∧ ( 𝑏 ‘ 2 ) = ( 𝑎 ‘ 7 ) ∧ ( 𝑏 ‘ 3 ) = ( 𝑎 ‘ 4 ) ) → ( 𝑏 ‘ 1 ) = ( 𝑎 ‘ 1 ) ) |
| 166 |
165
|
eleq1d |
⊢ ( ( ( 𝑏 ‘ 1 ) = ( 𝑎 ‘ 1 ) ∧ ( 𝑏 ‘ 2 ) = ( 𝑎 ‘ 7 ) ∧ ( 𝑏 ‘ 3 ) = ( 𝑎 ‘ 4 ) ) → ( ( 𝑏 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) ) |
| 167 |
|
simp3 |
⊢ ( ( ( 𝑏 ‘ 1 ) = ( 𝑎 ‘ 1 ) ∧ ( 𝑏 ‘ 2 ) = ( 𝑎 ‘ 7 ) ∧ ( 𝑏 ‘ 3 ) = ( 𝑎 ‘ 4 ) ) → ( 𝑏 ‘ 3 ) = ( 𝑎 ‘ 4 ) ) |
| 168 |
|
simp2 |
⊢ ( ( ( 𝑏 ‘ 1 ) = ( 𝑎 ‘ 1 ) ∧ ( 𝑏 ‘ 2 ) = ( 𝑎 ‘ 7 ) ∧ ( 𝑏 ‘ 3 ) = ( 𝑎 ‘ 4 ) ) → ( 𝑏 ‘ 2 ) = ( 𝑎 ‘ 7 ) ) |
| 169 |
165 168
|
oveq12d |
⊢ ( ( ( 𝑏 ‘ 1 ) = ( 𝑎 ‘ 1 ) ∧ ( 𝑏 ‘ 2 ) = ( 𝑎 ‘ 7 ) ∧ ( 𝑏 ‘ 3 ) = ( 𝑎 ‘ 4 ) ) → ( ( 𝑏 ‘ 1 ) Yrm ( 𝑏 ‘ 2 ) ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 7 ) ) ) |
| 170 |
167 169
|
eqeq12d |
⊢ ( ( ( 𝑏 ‘ 1 ) = ( 𝑎 ‘ 1 ) ∧ ( 𝑏 ‘ 2 ) = ( 𝑎 ‘ 7 ) ∧ ( 𝑏 ‘ 3 ) = ( 𝑎 ‘ 4 ) ) → ( ( 𝑏 ‘ 3 ) = ( ( 𝑏 ‘ 1 ) Yrm ( 𝑏 ‘ 2 ) ) ↔ ( 𝑎 ‘ 4 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 7 ) ) ) ) |
| 171 |
166 170
|
anbi12d |
⊢ ( ( ( 𝑏 ‘ 1 ) = ( 𝑎 ‘ 1 ) ∧ ( 𝑏 ‘ 2 ) = ( 𝑎 ‘ 7 ) ∧ ( 𝑏 ‘ 3 ) = ( 𝑎 ‘ 4 ) ) → ( ( ( 𝑏 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑏 ‘ 3 ) = ( ( 𝑏 ‘ 1 ) Yrm ( 𝑏 ‘ 2 ) ) ) ↔ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑎 ‘ 4 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 7 ) ) ) ) ) |
| 172 |
102 152 153
|
jm2.27dlem2 |
⊢ 1 ∈ ( 1 ... 7 ) |
| 173 |
137 152 153
|
jm2.27dlem2 |
⊢ 4 ∈ ( 1 ... 7 ) |
| 174 |
171 172 149 173
|
rabren3dioph |
⊢ ( ( 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 ) ) |
| 175 |
146 164 174
|
mp2an |
⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 7 ) ) ∣ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑎 ‘ 4 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 7 ) ) ) } ∈ ( Dioph ‘ 7 ) |
| 176 |
|
anrabdioph |
⊢ ( ( { 𝑎 ∈ ( ℕ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 ) ) |
| 177 |
163 175 176
|
mp2an |
⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 7 ) ) ∣ ( ( 𝑎 ‘ 7 ) = ( ( 𝑎 ‘ 2 ) + 1 ) ∧ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑎 ‘ 4 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 7 ) ) ) ) } ∈ ( Dioph ‘ 7 ) |
| 178 |
145 177
|
eqeltri |
⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 7 ) ) ∣ [ ( 𝑎 ↾ ( 1 ... 6 ) ) / 𝑒 ] [ ( 𝑎 ‘ 7 ) / 𝑏 ] ( 𝑏 = ( ( 𝑒 ‘ 2 ) + 1 ) ∧ ( ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 4 ) = ( ( 𝑒 ‘ 1 ) Yrm 𝑏 ) ) ) } ∈ ( Dioph ‘ 7 ) |
| 179 |
152
|
rexfrabdioph |
⊢ ( ( 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 ) ) |
| 180 |
90 178 179
|
mp2an |
⊢ { 𝑒 ∈ ( ℕ0 ↑m ( 1 ... 6 ) ) ∣ ∃ 𝑏 ∈ ℕ0 ( 𝑏 = ( ( 𝑒 ‘ 2 ) + 1 ) ∧ ( ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 4 ) = ( ( 𝑒 ‘ 1 ) Yrm 𝑏 ) ) ) } ∈ ( Dioph ‘ 6 ) |
| 181 |
124 180
|
eqeltri |
⊢ { 𝑒 ∈ ( ℕ0 ↑m ( 1 ... 6 ) ) ∣ ( ( 𝑒 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 4 ) = ( ( 𝑒 ‘ 1 ) Yrm ( ( 𝑒 ‘ 2 ) + 1 ) ) ) } ∈ ( Dioph ‘ 6 ) |
| 182 |
|
rmydioph |
⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ) } ∈ ( Dioph ‘ 3 ) |
| 183 |
|
simp1 |
⊢ ( ( ( 𝑎 ‘ 1 ) = ( 𝑒 ‘ 4 ) ∧ ( 𝑎 ‘ 2 ) = ( 𝑒 ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( 𝑒 ‘ 5 ) ) → ( 𝑎 ‘ 1 ) = ( 𝑒 ‘ 4 ) ) |
| 184 |
183
|
eleq1d |
⊢ ( ( ( 𝑎 ‘ 1 ) = ( 𝑒 ‘ 4 ) ∧ ( 𝑎 ‘ 2 ) = ( 𝑒 ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( 𝑒 ‘ 5 ) ) → ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑒 ‘ 4 ) ∈ ( ℤ≥ ‘ 2 ) ) ) |
| 185 |
|
simp3 |
⊢ ( ( ( 𝑎 ‘ 1 ) = ( 𝑒 ‘ 4 ) ∧ ( 𝑎 ‘ 2 ) = ( 𝑒 ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( 𝑒 ‘ 5 ) ) → ( 𝑎 ‘ 3 ) = ( 𝑒 ‘ 5 ) ) |
| 186 |
|
simp2 |
⊢ ( ( ( 𝑎 ‘ 1 ) = ( 𝑒 ‘ 4 ) ∧ ( 𝑎 ‘ 2 ) = ( 𝑒 ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( 𝑒 ‘ 5 ) ) → ( 𝑎 ‘ 2 ) = ( 𝑒 ‘ 2 ) ) |
| 187 |
183 186
|
oveq12d |
⊢ ( ( ( 𝑎 ‘ 1 ) = ( 𝑒 ‘ 4 ) ∧ ( 𝑎 ‘ 2 ) = ( 𝑒 ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( 𝑒 ‘ 5 ) ) → ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) = ( ( 𝑒 ‘ 4 ) Yrm ( 𝑒 ‘ 2 ) ) ) |
| 188 |
185 187
|
eqeq12d |
⊢ ( ( ( 𝑎 ‘ 1 ) = ( 𝑒 ‘ 4 ) ∧ ( 𝑎 ‘ 2 ) = ( 𝑒 ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( 𝑒 ‘ 5 ) ) → ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ↔ ( 𝑒 ‘ 5 ) = ( ( 𝑒 ‘ 4 ) Yrm ( 𝑒 ‘ 2 ) ) ) ) |
| 189 |
184 188
|
anbi12d |
⊢ ( ( ( 𝑎 ‘ 1 ) = ( 𝑒 ‘ 4 ) ∧ ( 𝑎 ‘ 2 ) = ( 𝑒 ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( 𝑒 ‘ 5 ) ) → ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ) ↔ ( ( 𝑒 ‘ 4 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 5 ) = ( ( 𝑒 ‘ 4 ) Yrm ( 𝑒 ‘ 2 ) ) ) ) ) |
| 190 |
|
5nn |
⊢ 5 ∈ ℕ |
| 191 |
190
|
jm2.27dlem3 |
⊢ 5 ∈ ( 1 ... 5 ) |
| 192 |
191 95 190
|
jm2.27dlem2 |
⊢ 5 ∈ ( 1 ... 6 ) |
| 193 |
189 137 107 192
|
rabren3dioph |
⊢ ( ( 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 ) ) |
| 194 |
90 182 193
|
mp2an |
⊢ { 𝑒 ∈ ( ℕ0 ↑m ( 1 ... 6 ) ) ∣ ( ( 𝑒 ‘ 4 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 5 ) = ( ( 𝑒 ‘ 4 ) Yrm ( 𝑒 ‘ 2 ) ) ) } ∈ ( Dioph ‘ 6 ) |
| 195 |
|
rmxdioph |
⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Xrm ( 𝑎 ‘ 2 ) ) ) } ∈ ( Dioph ‘ 3 ) |
| 196 |
|
simp1 |
⊢ ( ( ( 𝑎 ‘ 1 ) = ( 𝑒 ‘ 4 ) ∧ ( 𝑎 ‘ 2 ) = ( 𝑒 ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( 𝑒 ‘ 6 ) ) → ( 𝑎 ‘ 1 ) = ( 𝑒 ‘ 4 ) ) |
| 197 |
196
|
eleq1d |
⊢ ( ( ( 𝑎 ‘ 1 ) = ( 𝑒 ‘ 4 ) ∧ ( 𝑎 ‘ 2 ) = ( 𝑒 ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( 𝑒 ‘ 6 ) ) → ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑒 ‘ 4 ) ∈ ( ℤ≥ ‘ 2 ) ) ) |
| 198 |
|
simp3 |
⊢ ( ( ( 𝑎 ‘ 1 ) = ( 𝑒 ‘ 4 ) ∧ ( 𝑎 ‘ 2 ) = ( 𝑒 ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( 𝑒 ‘ 6 ) ) → ( 𝑎 ‘ 3 ) = ( 𝑒 ‘ 6 ) ) |
| 199 |
|
simp2 |
⊢ ( ( ( 𝑎 ‘ 1 ) = ( 𝑒 ‘ 4 ) ∧ ( 𝑎 ‘ 2 ) = ( 𝑒 ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( 𝑒 ‘ 6 ) ) → ( 𝑎 ‘ 2 ) = ( 𝑒 ‘ 2 ) ) |
| 200 |
196 199
|
oveq12d |
⊢ ( ( ( 𝑎 ‘ 1 ) = ( 𝑒 ‘ 4 ) ∧ ( 𝑎 ‘ 2 ) = ( 𝑒 ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( 𝑒 ‘ 6 ) ) → ( ( 𝑎 ‘ 1 ) Xrm ( 𝑎 ‘ 2 ) ) = ( ( 𝑒 ‘ 4 ) Xrm ( 𝑒 ‘ 2 ) ) ) |
| 201 |
198 200
|
eqeq12d |
⊢ ( ( ( 𝑎 ‘ 1 ) = ( 𝑒 ‘ 4 ) ∧ ( 𝑎 ‘ 2 ) = ( 𝑒 ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( 𝑒 ‘ 6 ) ) → ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Xrm ( 𝑎 ‘ 2 ) ) ↔ ( 𝑒 ‘ 6 ) = ( ( 𝑒 ‘ 4 ) Xrm ( 𝑒 ‘ 2 ) ) ) ) |
| 202 |
197 201
|
anbi12d |
⊢ ( ( ( 𝑎 ‘ 1 ) = ( 𝑒 ‘ 4 ) ∧ ( 𝑎 ‘ 2 ) = ( 𝑒 ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( 𝑒 ‘ 6 ) ) → ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Xrm ( 𝑎 ‘ 2 ) ) ) ↔ ( ( 𝑒 ‘ 4 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 6 ) = ( ( 𝑒 ‘ 4 ) Xrm ( 𝑒 ‘ 2 ) ) ) ) ) |
| 203 |
153
|
jm2.27dlem3 |
⊢ 6 ∈ ( 1 ... 6 ) |
| 204 |
202 137 107 203
|
rabren3dioph |
⊢ ( ( 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 ) ) |
| 205 |
90 195 204
|
mp2an |
⊢ { 𝑒 ∈ ( ℕ0 ↑m ( 1 ... 6 ) ) ∣ ( ( 𝑒 ‘ 4 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑒 ‘ 6 ) = ( ( 𝑒 ‘ 4 ) Xrm ( 𝑒 ‘ 2 ) ) ) } ∈ ( Dioph ‘ 6 ) |
| 206 |
99 3
|
sselii |
⊢ 3 ∈ ( 1 ... 6 ) |
| 207 |
|
mzpproj |
⊢ ( ( ( 1 ... 6 ) ∈ V ∧ 3 ∈ ( 1 ... 6 ) ) → ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 𝑒 ‘ 3 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ) |
| 208 |
92 206 207
|
mp2an |
⊢ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 𝑒 ‘ 3 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) |
| 209 |
|
mzpconstmpt |
⊢ ( ( ( 1 ... 6 ) ∈ V ∧ 2 ∈ ℤ ) → ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ 2 ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ) |
| 210 |
92 91 209
|
mp2an |
⊢ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ 2 ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) |
| 211 |
|
mzpproj |
⊢ ( ( ( 1 ... 6 ) ∈ V ∧ 4 ∈ ( 1 ... 6 ) ) → ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 𝑒 ‘ 4 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ) |
| 212 |
92 137 211
|
mp2an |
⊢ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 𝑒 ‘ 4 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) |
| 213 |
|
mzpmulmpt |
⊢ ( ( ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ 2 ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ∧ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 𝑒 ‘ 4 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ) → ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 2 · ( 𝑒 ‘ 4 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ) |
| 214 |
210 212 213
|
mp2an |
⊢ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 2 · ( 𝑒 ‘ 4 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) |
| 215 |
|
mzpmulmpt |
⊢ ( ( ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 2 · ( 𝑒 ‘ 4 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ∧ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 𝑒 ‘ 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ) → ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( ( 2 · ( 𝑒 ‘ 4 ) ) · ( 𝑒 ‘ 1 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ) |
| 216 |
214 104 215
|
mp2an |
⊢ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( ( 2 · ( 𝑒 ‘ 4 ) ) · ( 𝑒 ‘ 1 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) |
| 217 |
|
2nn0 |
⊢ 2 ∈ ℕ0 |
| 218 |
|
mzpexpmpt |
⊢ ( ( ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 𝑒 ‘ 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ∧ 2 ∈ ℕ0 ) → ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( ( 𝑒 ‘ 1 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ) |
| 219 |
104 217 218
|
mp2an |
⊢ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( ( 𝑒 ‘ 1 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) |
| 220 |
|
mzpsubmpt |
⊢ ( ( ( 𝑒 ∈ ( ℤ ↑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 ) ) ) |
| 221 |
216 219 220
|
mp2an |
⊢ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( ( ( 2 · ( 𝑒 ‘ 4 ) ) · ( 𝑒 ‘ 1 ) ) − ( ( 𝑒 ‘ 1 ) ↑ 2 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) |
| 222 |
|
mzpconstmpt |
⊢ ( ( ( 1 ... 6 ) ∈ V ∧ 1 ∈ ℤ ) → ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ 1 ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ) |
| 223 |
92 157 222
|
mp2an |
⊢ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ 1 ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) |
| 224 |
|
mzpsubmpt |
⊢ ( ( ( 𝑒 ∈ ( ℤ ↑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 ) ) ) |
| 225 |
221 223 224
|
mp2an |
⊢ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( ( ( ( 2 · ( 𝑒 ‘ 4 ) ) · ( 𝑒 ‘ 1 ) ) − ( ( 𝑒 ‘ 1 ) ↑ 2 ) ) − 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) |
| 226 |
|
ltrabdioph |
⊢ ( ( 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 ) ) |
| 227 |
90 208 225 226
|
mp3an |
⊢ { 𝑒 ∈ ( ℕ0 ↑m ( 1 ... 6 ) ) ∣ ( 𝑒 ‘ 3 ) < ( ( ( ( 2 · ( 𝑒 ‘ 4 ) ) · ( 𝑒 ‘ 1 ) ) − ( ( 𝑒 ‘ 1 ) ↑ 2 ) ) − 1 ) } ∈ ( Dioph ‘ 6 ) |
| 228 |
|
mzpproj |
⊢ ( ( ( 1 ... 6 ) ∈ V ∧ 6 ∈ ( 1 ... 6 ) ) → ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 𝑒 ‘ 6 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ) |
| 229 |
92 203 228
|
mp2an |
⊢ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 𝑒 ‘ 6 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) |
| 230 |
|
mzpsubmpt |
⊢ ( ( ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 𝑒 ‘ 4 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ∧ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 𝑒 ‘ 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ) → ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( ( 𝑒 ‘ 4 ) − ( 𝑒 ‘ 1 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ) |
| 231 |
212 104 230
|
mp2an |
⊢ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( ( 𝑒 ‘ 4 ) − ( 𝑒 ‘ 1 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) |
| 232 |
|
mzpproj |
⊢ ( ( ( 1 ... 6 ) ∈ V ∧ 5 ∈ ( 1 ... 6 ) ) → ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 𝑒 ‘ 5 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ) |
| 233 |
92 192 232
|
mp2an |
⊢ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 𝑒 ‘ 5 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) |
| 234 |
|
mzpmulmpt |
⊢ ( ( ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( ( 𝑒 ‘ 4 ) − ( 𝑒 ‘ 1 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ∧ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( 𝑒 ‘ 5 ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ) → ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( ( ( 𝑒 ‘ 4 ) − ( 𝑒 ‘ 1 ) ) · ( 𝑒 ‘ 5 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) ) |
| 235 |
231 233 234
|
mp2an |
⊢ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( ( ( 𝑒 ‘ 4 ) − ( 𝑒 ‘ 1 ) ) · ( 𝑒 ‘ 5 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) |
| 236 |
|
mzpsubmpt |
⊢ ( ( ( 𝑒 ∈ ( ℤ ↑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 ) ) ) |
| 237 |
229 235 236
|
mp2an |
⊢ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( ( 𝑒 ‘ 6 ) − ( ( ( 𝑒 ‘ 4 ) − ( 𝑒 ‘ 1 ) ) · ( 𝑒 ‘ 5 ) ) ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) |
| 238 |
|
mzpsubmpt |
⊢ ( ( ( 𝑒 ∈ ( ℤ ↑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 ) ) ) |
| 239 |
237 208 238
|
mp2an |
⊢ ( 𝑒 ∈ ( ℤ ↑m ( 1 ... 6 ) ) ↦ ( ( ( 𝑒 ‘ 6 ) − ( ( ( 𝑒 ‘ 4 ) − ( 𝑒 ‘ 1 ) ) · ( 𝑒 ‘ 5 ) ) ) − ( 𝑒 ‘ 3 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 6 ) ) |
| 240 |
|
dvdsrabdioph |
⊢ ( ( 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 ) ) |
| 241 |
90 225 239 240
|
mp3an |
⊢ { 𝑒 ∈ ( ℕ0 ↑m ( 1 ... 6 ) ) ∣ ( ( ( ( 2 · ( 𝑒 ‘ 4 ) ) · ( 𝑒 ‘ 1 ) ) − ( ( 𝑒 ‘ 1 ) ↑ 2 ) ) − 1 ) ∥ ( ( ( 𝑒 ‘ 6 ) − ( ( ( 𝑒 ‘ 4 ) − ( 𝑒 ‘ 1 ) ) · ( 𝑒 ‘ 5 ) ) ) − ( 𝑒 ‘ 3 ) ) } ∈ ( Dioph ‘ 6 ) |
| 242 |
|
anrabdioph |
⊢ ( ( { 𝑒 ∈ ( ℕ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 ) ) |
| 243 |
227 241 242
|
mp2an |
⊢ { 𝑒 ∈ ( ℕ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 |
⊢ ( ( { 𝑒 ∈ ( ℕ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 ) ) |
| 245 |
205 243 244
|
mp2an |
⊢ { 𝑒 ∈ ( ℕ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 |
⊢ ( ( { 𝑒 ∈ ( ℕ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 ) ) |
| 247 |
194 245 246
|
mp2an |
⊢ { 𝑒 ∈ ( ℕ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 |
⊢ ( ( { 𝑒 ∈ ( ℕ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 ) ) |
| 249 |
181 247 248
|
mp2an |
⊢ { 𝑒 ∈ ( ℕ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 |
⊢ ( ( { 𝑒 ∈ ( ℕ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 ) ) |
| 251 |
113 249 250
|
mp2an |
⊢ { 𝑒 ∈ ( ℕ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 ) |
| 252 |
89 251
|
eqeltri |
⊢ { 𝑒 ∈ ( ℕ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 ) |
| 253 |
93 94 95
|
3rexfrabdioph |
⊢ ( ( 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 ) ) |
| 254 |
9 252 253
|
mp2an |
⊢ { 𝑎 ∈ ( ℕ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 ) |
| 255 |
8 254
|
eqeltri |
⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ) } ∈ ( Dioph ‘ 3 ) |