Step |
Hyp |
Ref |
Expression |
1 |
|
rabdiophlem1 |
⊢ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) → ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ ) |
2 |
|
rabdiophlem1 |
⊢ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) → ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐵 ∈ ℤ ) |
3 |
|
zre |
⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ ) |
4 |
|
zre |
⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℝ ) |
5 |
|
lttri2 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≠ 𝐵 ↔ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ) ) |
6 |
3 4 5
|
syl2an |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ≠ 𝐵 ↔ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ) ) |
7 |
6
|
ralimi |
⊢ ( ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝐴 ≠ 𝐵 ↔ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ) ) |
8 |
|
r19.26 |
⊢ ( ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ↔ ( ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ ∧ ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐵 ∈ ℤ ) ) |
9 |
|
rabbi |
⊢ ( ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝐴 ≠ 𝐵 ↔ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ) ↔ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 ≠ 𝐵 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) } ) |
10 |
7 8 9
|
3imtr3i |
⊢ ( ( ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ ∧ ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐵 ∈ ℤ ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 ≠ 𝐵 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) } ) |
11 |
1 2 10
|
syl2an |
⊢ ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 ≠ 𝐵 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) } ) |
12 |
11
|
3adant1 |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 ≠ 𝐵 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) } ) |
13 |
|
ltrabdioph |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 < 𝐵 } ∈ ( Dioph ‘ 𝑁 ) ) |
14 |
|
ltrabdioph |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐵 < 𝐴 } ∈ ( Dioph ‘ 𝑁 ) ) |
15 |
14
|
3com23 |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐵 < 𝐴 } ∈ ( Dioph ‘ 𝑁 ) ) |
16 |
|
orrabdioph |
⊢ ( ( { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 < 𝐵 } ∈ ( Dioph ‘ 𝑁 ) ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐵 < 𝐴 } ∈ ( Dioph ‘ 𝑁 ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) } ∈ ( Dioph ‘ 𝑁 ) ) |
17 |
13 15 16
|
syl2anc |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) } ∈ ( Dioph ‘ 𝑁 ) ) |
18 |
12 17
|
eqeltrd |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 ≠ 𝐵 } ∈ ( Dioph ‘ 𝑁 ) ) |