| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . . 5
⊢ (𝑦 = 𝑁 → (𝑦 · 𝐴) = (𝑁 · 𝐴)) |
| 2 | 1 | eqeq1d 2739 |
. . . 4
⊢ (𝑦 = 𝑁 → ((𝑦 · 𝐴) = 0 ↔ (𝑁 · 𝐴) = 0 )) |
| 3 | 2 | elrab 3692 |
. . 3
⊢ (𝑁 ∈ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 } ↔ (𝑁 ∈ ℕ ∧ (𝑁 · 𝐴) = 0 )) |
| 4 | | odcl.1 |
. . . . . 6
⊢ 𝑋 = (Base‘𝐺) |
| 5 | | odid.3 |
. . . . . 6
⊢ · =
(.g‘𝐺) |
| 6 | | odid.4 |
. . . . . 6
⊢ 0 =
(0g‘𝐺) |
| 7 | | odcl.2 |
. . . . . 6
⊢ 𝑂 = (od‘𝐺) |
| 8 | | eqid 2737 |
. . . . . 6
⊢ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 } = {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 } |
| 9 | 4, 5, 6, 7, 8 | odval 19552 |
. . . . 5
⊢ (𝐴 ∈ 𝑋 → (𝑂‘𝐴) = if({𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 } = ∅, 0, inf({𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }, ℝ, <
))) |
| 10 | | n0i 4340 |
. . . . . 6
⊢ (𝑁 ∈ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 } → ¬ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 } =
∅) |
| 11 | 10 | iffalsed 4536 |
. . . . 5
⊢ (𝑁 ∈ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 } → if({𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 } = ∅, 0, inf({𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }, ℝ, < )) =
inf({𝑦 ∈ ℕ
∣ (𝑦 · 𝐴) = 0 }, ℝ, <
)) |
| 12 | 9, 11 | sylan9eq 2797 |
. . . 4
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑁 ∈ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }) → (𝑂‘𝐴) = inf({𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }, ℝ, <
)) |
| 13 | | ssrab2 4080 |
. . . . . 6
⊢ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 } ⊆
ℕ |
| 14 | | nnuz 12921 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
| 15 | 13, 14 | sseqtri 4032 |
. . . . . . 7
⊢ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 } ⊆
(ℤ≥‘1) |
| 16 | | ne0i 4341 |
. . . . . . . 8
⊢ (𝑁 ∈ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 } → {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 } ≠
∅) |
| 17 | 16 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑁 ∈ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }) → {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 } ≠
∅) |
| 18 | | infssuzcl 12974 |
. . . . . . 7
⊢ (({𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 } ⊆
(ℤ≥‘1) ∧ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 } ≠ ∅) →
inf({𝑦 ∈ ℕ
∣ (𝑦 · 𝐴) = 0 }, ℝ, < ) ∈
{𝑦 ∈ ℕ ∣
(𝑦 · 𝐴) = 0 }) |
| 19 | 15, 17, 18 | sylancr 587 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑁 ∈ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }) → inf({𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }, ℝ, < ) ∈
{𝑦 ∈ ℕ ∣
(𝑦 · 𝐴) = 0 }) |
| 20 | 13, 19 | sselid 3981 |
. . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑁 ∈ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }) → inf({𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }, ℝ, < ) ∈
ℕ) |
| 21 | | infssuzle 12973 |
. . . . . . 7
⊢ (({𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 } ⊆
(ℤ≥‘1) ∧ 𝑁 ∈ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }) → inf({𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }, ℝ, < ) ≤
𝑁) |
| 22 | 15, 21 | mpan 690 |
. . . . . 6
⊢ (𝑁 ∈ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 } → inf({𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }, ℝ, < ) ≤
𝑁) |
| 23 | 22 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑁 ∈ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }) → inf({𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }, ℝ, < ) ≤
𝑁) |
| 24 | | elrabi 3687 |
. . . . . . . 8
⊢ (𝑁 ∈ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 } → 𝑁 ∈ ℕ) |
| 25 | 24 | nnzd 12640 |
. . . . . . 7
⊢ (𝑁 ∈ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 } → 𝑁 ∈ ℤ) |
| 26 | | fznn 13632 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ →
(inf({𝑦 ∈ ℕ
∣ (𝑦 · 𝐴) = 0 }, ℝ, < ) ∈
(1...𝑁) ↔ (inf({𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }, ℝ, < ) ∈
ℕ ∧ inf({𝑦 ∈
ℕ ∣ (𝑦 · 𝐴) = 0 }, ℝ, < ) ≤
𝑁))) |
| 27 | 25, 26 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 } → (inf({𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }, ℝ, < ) ∈
(1...𝑁) ↔ (inf({𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }, ℝ, < ) ∈
ℕ ∧ inf({𝑦 ∈
ℕ ∣ (𝑦 · 𝐴) = 0 }, ℝ, < ) ≤
𝑁))) |
| 28 | 27 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑁 ∈ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }) → (inf({𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }, ℝ, < ) ∈
(1...𝑁) ↔ (inf({𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }, ℝ, < ) ∈
ℕ ∧ inf({𝑦 ∈
ℕ ∣ (𝑦 · 𝐴) = 0 }, ℝ, < ) ≤
𝑁))) |
| 29 | 20, 23, 28 | mpbir2and 713 |
. . . 4
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑁 ∈ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }) → inf({𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }, ℝ, < ) ∈
(1...𝑁)) |
| 30 | 12, 29 | eqeltrd 2841 |
. . 3
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑁 ∈ {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }) → (𝑂‘𝐴) ∈ (1...𝑁)) |
| 31 | 3, 30 | sylan2br 595 |
. 2
⊢ ((𝐴 ∈ 𝑋 ∧ (𝑁 ∈ ℕ ∧ (𝑁 · 𝐴) = 0 )) → (𝑂‘𝐴) ∈ (1...𝑁)) |
| 32 | 31 | 3impb 1115 |
1
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ ∧ (𝑁 · 𝐴) = 0 ) → (𝑂‘𝐴) ∈ (1...𝑁)) |