| Step | Hyp | Ref
| Expression |
| 1 | | domnsym 9139 |
. . . . . . . . 9
⊢ (ℕ
≼ 𝐵 → ¬
𝐵 ≺
ℕ) |
| 2 | | fimgmcyc.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ Fin) |
| 3 | | fisdomnn 42285 |
. . . . . . . . . 10
⊢ (𝐵 ∈ Fin → 𝐵 ≺
ℕ) |
| 4 | 2, 3 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ≺ ℕ) |
| 5 | 1, 4 | nsyl3 138 |
. . . . . . . 8
⊢ (𝜑 → ¬ ℕ ≼
𝐵) |
| 6 | | fimgmcyc.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑀) |
| 7 | 6 | fvexi 6920 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
| 8 | 7 | f1dom 9014 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ↦ (𝑛 · 𝐴)):ℕ–1-1→𝐵 → ℕ ≼ 𝐵) |
| 9 | 5, 8 | nsyl 140 |
. . . . . . 7
⊢ (𝜑 → ¬ (𝑛 ∈ ℕ ↦ (𝑛 · 𝐴)):ℕ–1-1→𝐵) |
| 10 | | fimgmcyc.s |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ Mgm) |
| 11 | 10 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ Mgm) |
| 12 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
| 13 | | fimgmcyc.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ 𝐵) |
| 14 | 13 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ 𝐵) |
| 15 | | fimgmcyc.m |
. . . . . . . . . . 11
⊢ · =
(.g‘𝑀) |
| 16 | 6, 15 | mulgnncl 19107 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ Mgm ∧ 𝑛 ∈ ℕ ∧ 𝐴 ∈ 𝐵) → (𝑛 · 𝐴) ∈ 𝐵) |
| 17 | 11, 12, 14, 16 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 · 𝐴) ∈ 𝐵) |
| 18 | 17 | fmpttd 7135 |
. . . . . . . 8
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (𝑛 · 𝐴)):ℕ⟶𝐵) |
| 19 | | dff13 7275 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ↦ (𝑛 · 𝐴)):ℕ–1-1→𝐵 ↔ ((𝑛 ∈ ℕ ↦ (𝑛 · 𝐴)):ℕ⟶𝐵 ∧ ∀𝑜 ∈ ℕ ∀𝑞 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑛 · 𝐴))‘𝑜) = ((𝑛 ∈ ℕ ↦ (𝑛 · 𝐴))‘𝑞) → 𝑜 = 𝑞))) |
| 20 | 19 | baib 535 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ↦ (𝑛 · 𝐴)):ℕ⟶𝐵 → ((𝑛 ∈ ℕ ↦ (𝑛 · 𝐴)):ℕ–1-1→𝐵 ↔ ∀𝑜 ∈ ℕ ∀𝑞 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑛 · 𝐴))‘𝑜) = ((𝑛 ∈ ℕ ↦ (𝑛 · 𝐴))‘𝑞) → 𝑜 = 𝑞))) |
| 21 | 18, 20 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑛 ∈ ℕ ↦ (𝑛 · 𝐴)):ℕ–1-1→𝐵 ↔ ∀𝑜 ∈ ℕ ∀𝑞 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑛 · 𝐴))‘𝑜) = ((𝑛 ∈ ℕ ↦ (𝑛 · 𝐴))‘𝑞) → 𝑜 = 𝑞))) |
| 22 | 9, 21 | mtbid 324 |
. . . . . 6
⊢ (𝜑 → ¬ ∀𝑜 ∈ ℕ ∀𝑞 ∈ ℕ (((𝑛 ∈ ℕ ↦ (𝑛 · 𝐴))‘𝑜) = ((𝑛 ∈ ℕ ↦ (𝑛 · 𝐴))‘𝑞) → 𝑜 = 𝑞)) |
| 23 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑜 → (𝑛 · 𝐴) = (𝑜 · 𝐴)) |
| 24 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦ (𝑛 · 𝐴)) = (𝑛 ∈ ℕ ↦ (𝑛 · 𝐴)) |
| 25 | | ovex 7464 |
. . . . . . . . . . 11
⊢ (𝑜 · 𝐴) ∈ V |
| 26 | 23, 24, 25 | fvmpt 7016 |
. . . . . . . . . 10
⊢ (𝑜 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑛 · 𝐴))‘𝑜) = (𝑜 · 𝐴)) |
| 27 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑞 → (𝑛 · 𝐴) = (𝑞 · 𝐴)) |
| 28 | | ovex 7464 |
. . . . . . . . . . 11
⊢ (𝑞 · 𝐴) ∈ V |
| 29 | 27, 24, 28 | fvmpt 7016 |
. . . . . . . . . 10
⊢ (𝑞 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑛 · 𝐴))‘𝑞) = (𝑞 · 𝐴)) |
| 30 | 26, 29 | eqeqan12d 2751 |
. . . . . . . . 9
⊢ ((𝑜 ∈ ℕ ∧ 𝑞 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ (𝑛 · 𝐴))‘𝑜) = ((𝑛 ∈ ℕ ↦ (𝑛 · 𝐴))‘𝑞) ↔ (𝑜 · 𝐴) = (𝑞 · 𝐴))) |
| 31 | 30 | imbi1d 341 |
. . . . . . . 8
⊢ ((𝑜 ∈ ℕ ∧ 𝑞 ∈ ℕ) →
((((𝑛 ∈ ℕ
↦ (𝑛 · 𝐴))‘𝑜) = ((𝑛 ∈ ℕ ↦ (𝑛 · 𝐴))‘𝑞) → 𝑜 = 𝑞) ↔ ((𝑜 · 𝐴) = (𝑞 · 𝐴) → 𝑜 = 𝑞))) |
| 32 | 31 | ralbidva 3176 |
. . . . . . 7
⊢ (𝑜 ∈ ℕ →
(∀𝑞 ∈ ℕ
(((𝑛 ∈ ℕ ↦
(𝑛 · 𝐴))‘𝑜) = ((𝑛 ∈ ℕ ↦ (𝑛 · 𝐴))‘𝑞) → 𝑜 = 𝑞) ↔ ∀𝑞 ∈ ℕ ((𝑜 · 𝐴) = (𝑞 · 𝐴) → 𝑜 = 𝑞))) |
| 33 | 32 | ralbiia 3091 |
. . . . . 6
⊢
(∀𝑜 ∈
ℕ ∀𝑞 ∈
ℕ (((𝑛 ∈ ℕ
↦ (𝑛 · 𝐴))‘𝑜) = ((𝑛 ∈ ℕ ↦ (𝑛 · 𝐴))‘𝑞) → 𝑜 = 𝑞) ↔ ∀𝑜 ∈ ℕ ∀𝑞 ∈ ℕ ((𝑜 · 𝐴) = (𝑞 · 𝐴) → 𝑜 = 𝑞)) |
| 34 | 22, 33 | sylnib 328 |
. . . . 5
⊢ (𝜑 → ¬ ∀𝑜 ∈ ℕ ∀𝑞 ∈ ℕ ((𝑜 · 𝐴) = (𝑞 · 𝐴) → 𝑜 = 𝑞)) |
| 35 | | df-ne 2941 |
. . . . . . . . 9
⊢ (𝑜 ≠ 𝑞 ↔ ¬ 𝑜 = 𝑞) |
| 36 | 35 | anbi1i 624 |
. . . . . . . 8
⊢ ((𝑜 ≠ 𝑞 ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴)) ↔ (¬ 𝑜 = 𝑞 ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴))) |
| 37 | | ancom 460 |
. . . . . . . 8
⊢ ((¬
𝑜 = 𝑞 ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴)) ↔ ((𝑜 · 𝐴) = (𝑞 · 𝐴) ∧ ¬ 𝑜 = 𝑞)) |
| 38 | | annim 403 |
. . . . . . . 8
⊢ (((𝑜 · 𝐴) = (𝑞 · 𝐴) ∧ ¬ 𝑜 = 𝑞) ↔ ¬ ((𝑜 · 𝐴) = (𝑞 · 𝐴) → 𝑜 = 𝑞)) |
| 39 | 36, 37, 38 | 3bitri 297 |
. . . . . . 7
⊢ ((𝑜 ≠ 𝑞 ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴)) ↔ ¬ ((𝑜 · 𝐴) = (𝑞 · 𝐴) → 𝑜 = 𝑞)) |
| 40 | 39 | 2rexbii 3129 |
. . . . . 6
⊢
(∃𝑜 ∈
ℕ ∃𝑞 ∈
ℕ (𝑜 ≠ 𝑞 ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴)) ↔ ∃𝑜 ∈ ℕ ∃𝑞 ∈ ℕ ¬ ((𝑜 · 𝐴) = (𝑞 · 𝐴) → 𝑜 = 𝑞)) |
| 41 | | rexnal2 3135 |
. . . . . 6
⊢
(∃𝑜 ∈
ℕ ∃𝑞 ∈
ℕ ¬ ((𝑜 · 𝐴) = (𝑞 · 𝐴) → 𝑜 = 𝑞) ↔ ¬ ∀𝑜 ∈ ℕ ∀𝑞 ∈ ℕ ((𝑜 · 𝐴) = (𝑞 · 𝐴) → 𝑜 = 𝑞)) |
| 42 | 40, 41 | bitri 275 |
. . . . 5
⊢
(∃𝑜 ∈
ℕ ∃𝑞 ∈
ℕ (𝑜 ≠ 𝑞 ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴)) ↔ ¬ ∀𝑜 ∈ ℕ ∀𝑞 ∈ ℕ ((𝑜 · 𝐴) = (𝑞 · 𝐴) → 𝑜 = 𝑞)) |
| 43 | 34, 42 | sylibr 234 |
. . . 4
⊢ (𝜑 → ∃𝑜 ∈ ℕ ∃𝑞 ∈ ℕ (𝑜 ≠ 𝑞 ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴))) |
| 44 | 43 | fimgmcyclem 42543 |
. . 3
⊢ (𝜑 → ∃𝑜 ∈ ℕ ∃𝑞 ∈ ℕ (𝑜 < 𝑞 ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴))) |
| 45 | | nnz 12634 |
. . . . . . . . . 10
⊢ (𝑜 ∈ ℕ → 𝑜 ∈
ℤ) |
| 46 | | eluzp1 42341 |
. . . . . . . . . 10
⊢ (𝑜 ∈ ℤ → (𝑞 ∈
(ℤ≥‘(𝑜 + 1)) ↔ (𝑞 ∈ ℤ ∧ 𝑜 < 𝑞))) |
| 47 | 45, 46 | syl 17 |
. . . . . . . . 9
⊢ (𝑜 ∈ ℕ → (𝑞 ∈
(ℤ≥‘(𝑜 + 1)) ↔ (𝑞 ∈ ℤ ∧ 𝑜 < 𝑞))) |
| 48 | | idd 24 |
. . . . . . . . . . . 12
⊢ ((𝑜 ∈ ℕ ∧ 𝑜 < 𝑞) → (𝑞 ∈ ℤ → 𝑞 ∈ ℤ)) |
| 49 | | nnz 12634 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ ℕ → 𝑞 ∈
ℤ) |
| 50 | 49 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑜 ∈ ℕ ∧ 𝑜 < 𝑞) → (𝑞 ∈ ℕ → 𝑞 ∈ ℤ)) |
| 51 | | 0red 11264 |
. . . . . . . . . . . . . . 15
⊢ (((𝑜 ∈ ℕ ∧ 𝑜 < 𝑞) ∧ 𝑞 ∈ ℤ) → 0 ∈
ℝ) |
| 52 | | nnre 12273 |
. . . . . . . . . . . . . . . 16
⊢ (𝑜 ∈ ℕ → 𝑜 ∈
ℝ) |
| 53 | 52 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝑜 ∈ ℕ ∧ 𝑜 < 𝑞) ∧ 𝑞 ∈ ℤ) → 𝑜 ∈ ℝ) |
| 54 | | zre 12617 |
. . . . . . . . . . . . . . . 16
⊢ (𝑞 ∈ ℤ → 𝑞 ∈
ℝ) |
| 55 | 54 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑜 ∈ ℕ ∧ 𝑜 < 𝑞) ∧ 𝑞 ∈ ℤ) → 𝑞 ∈ ℝ) |
| 56 | | nngt0 12297 |
. . . . . . . . . . . . . . . 16
⊢ (𝑜 ∈ ℕ → 0 <
𝑜) |
| 57 | 56 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝑜 ∈ ℕ ∧ 𝑜 < 𝑞) ∧ 𝑞 ∈ ℤ) → 0 < 𝑜) |
| 58 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢ (((𝑜 ∈ ℕ ∧ 𝑜 < 𝑞) ∧ 𝑞 ∈ ℤ) → 𝑜 < 𝑞) |
| 59 | 51, 53, 55, 57, 58 | lttrd 11422 |
. . . . . . . . . . . . . 14
⊢ (((𝑜 ∈ ℕ ∧ 𝑜 < 𝑞) ∧ 𝑞 ∈ ℤ) → 0 < 𝑞) |
| 60 | | elnnz 12623 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 ∈ ℕ ↔ (𝑞 ∈ ℤ ∧ 0 <
𝑞)) |
| 61 | 60 | rbaibr 537 |
. . . . . . . . . . . . . 14
⊢ (0 <
𝑞 → (𝑞 ∈ ℤ ↔ 𝑞 ∈
ℕ)) |
| 62 | 59, 61 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑜 ∈ ℕ ∧ 𝑜 < 𝑞) ∧ 𝑞 ∈ ℤ) → (𝑞 ∈ ℤ ↔ 𝑞 ∈ ℕ)) |
| 63 | 62 | ex 412 |
. . . . . . . . . . . 12
⊢ ((𝑜 ∈ ℕ ∧ 𝑜 < 𝑞) → (𝑞 ∈ ℤ → (𝑞 ∈ ℤ ↔ 𝑞 ∈ ℕ))) |
| 64 | 48, 50, 63 | pm5.21ndd 379 |
. . . . . . . . . . 11
⊢ ((𝑜 ∈ ℕ ∧ 𝑜 < 𝑞) → (𝑞 ∈ ℤ ↔ 𝑞 ∈ ℕ)) |
| 65 | 64 | ex 412 |
. . . . . . . . . 10
⊢ (𝑜 ∈ ℕ → (𝑜 < 𝑞 → (𝑞 ∈ ℤ ↔ 𝑞 ∈ ℕ))) |
| 66 | 65 | pm5.32rd 578 |
. . . . . . . . 9
⊢ (𝑜 ∈ ℕ → ((𝑞 ∈ ℤ ∧ 𝑜 < 𝑞) ↔ (𝑞 ∈ ℕ ∧ 𝑜 < 𝑞))) |
| 67 | 47, 66 | bitrd 279 |
. . . . . . . 8
⊢ (𝑜 ∈ ℕ → (𝑞 ∈
(ℤ≥‘(𝑜 + 1)) ↔ (𝑞 ∈ ℕ ∧ 𝑜 < 𝑞))) |
| 68 | 67 | anbi1d 631 |
. . . . . . 7
⊢ (𝑜 ∈ ℕ → ((𝑞 ∈
(ℤ≥‘(𝑜 + 1)) ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴)) ↔ ((𝑞 ∈ ℕ ∧ 𝑜 < 𝑞) ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴)))) |
| 69 | | anass 468 |
. . . . . . 7
⊢ (((𝑞 ∈ ℕ ∧ 𝑜 < 𝑞) ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴)) ↔ (𝑞 ∈ ℕ ∧ (𝑜 < 𝑞 ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴)))) |
| 70 | 68, 69 | bitrdi 287 |
. . . . . 6
⊢ (𝑜 ∈ ℕ → ((𝑞 ∈
(ℤ≥‘(𝑜 + 1)) ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴)) ↔ (𝑞 ∈ ℕ ∧ (𝑜 < 𝑞 ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴))))) |
| 71 | 70 | exbidv 1921 |
. . . . 5
⊢ (𝑜 ∈ ℕ →
(∃𝑞(𝑞 ∈
(ℤ≥‘(𝑜 + 1)) ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴)) ↔ ∃𝑞(𝑞 ∈ ℕ ∧ (𝑜 < 𝑞 ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴))))) |
| 72 | | df-rex 3071 |
. . . . 5
⊢
(∃𝑞 ∈
(ℤ≥‘(𝑜 + 1))(𝑜 · 𝐴) = (𝑞 · 𝐴) ↔ ∃𝑞(𝑞 ∈ (ℤ≥‘(𝑜 + 1)) ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴))) |
| 73 | | df-rex 3071 |
. . . . 5
⊢
(∃𝑞 ∈
ℕ (𝑜 < 𝑞 ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴)) ↔ ∃𝑞(𝑞 ∈ ℕ ∧ (𝑜 < 𝑞 ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴)))) |
| 74 | 71, 72, 73 | 3bitr4g 314 |
. . . 4
⊢ (𝑜 ∈ ℕ →
(∃𝑞 ∈
(ℤ≥‘(𝑜 + 1))(𝑜 · 𝐴) = (𝑞 · 𝐴) ↔ ∃𝑞 ∈ ℕ (𝑜 < 𝑞 ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴)))) |
| 75 | 74 | rexbiia 3092 |
. . 3
⊢
(∃𝑜 ∈
ℕ ∃𝑞 ∈
(ℤ≥‘(𝑜 + 1))(𝑜 · 𝐴) = (𝑞 · 𝐴) ↔ ∃𝑜 ∈ ℕ ∃𝑞 ∈ ℕ (𝑜 < 𝑞 ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴))) |
| 76 | 44, 75 | sylibr 234 |
. 2
⊢ (𝜑 → ∃𝑜 ∈ ℕ ∃𝑞 ∈ (ℤ≥‘(𝑜 + 1))(𝑜 · 𝐴) = (𝑞 · 𝐴)) |
| 77 | | simplr 769 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑝 ∈ ℕ) → 𝑜 ∈ ℕ) |
| 78 | 77 | peano2nnd 12283 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑝 ∈ ℕ) → (𝑜 + 1) ∈ ℕ) |
| 79 | 78 | nnzd 12640 |
. . . . 5
⊢ (((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑝 ∈ ℕ) → (𝑜 + 1) ∈ ℤ) |
| 80 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑝 ∈ ℕ) → 𝑝 ∈ ℕ) |
| 81 | 77, 80 | nnaddcld 12318 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑝 ∈ ℕ) → (𝑜 + 𝑝) ∈ ℕ) |
| 82 | 81 | nnzd 12640 |
. . . . 5
⊢ (((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑝 ∈ ℕ) → (𝑜 + 𝑝) ∈ ℤ) |
| 83 | | 1red 11262 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑝 ∈ ℕ) → 1 ∈
ℝ) |
| 84 | 80 | nnred 12281 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑝 ∈ ℕ) → 𝑝 ∈ ℝ) |
| 85 | 77 | nnred 12281 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑝 ∈ ℕ) → 𝑜 ∈ ℝ) |
| 86 | 80 | nnge1d 12314 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑝 ∈ ℕ) → 1 ≤ 𝑝) |
| 87 | 83, 84, 85, 86 | leadd2dd 11878 |
. . . . 5
⊢ (((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑝 ∈ ℕ) → (𝑜 + 1) ≤ (𝑜 + 𝑝)) |
| 88 | | eluz2 12884 |
. . . . 5
⊢ ((𝑜 + 𝑝) ∈ (ℤ≥‘(𝑜 + 1)) ↔ ((𝑜 + 1) ∈ ℤ ∧
(𝑜 + 𝑝) ∈ ℤ ∧ (𝑜 + 1) ≤ (𝑜 + 𝑝))) |
| 89 | 79, 82, 87, 88 | syl3anbrc 1344 |
. . . 4
⊢ (((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑝 ∈ ℕ) → (𝑜 + 𝑝) ∈ (ℤ≥‘(𝑜 + 1))) |
| 90 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑜 ∈ ℕ) → 𝑜 ∈ ℕ) |
| 91 | 90 | nnzd 12640 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑜 ∈ ℕ) → 𝑜 ∈ ℤ) |
| 92 | | eluzp1l 12905 |
. . . . . . 7
⊢ ((𝑜 ∈ ℤ ∧ 𝑞 ∈
(ℤ≥‘(𝑜 + 1))) → 𝑜 < 𝑞) |
| 93 | 91, 92 | sylan 580 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑞 ∈ (ℤ≥‘(𝑜 + 1))) → 𝑜 < 𝑞) |
| 94 | | simplr 769 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑞 ∈ (ℤ≥‘(𝑜 + 1))) → 𝑜 ∈
ℕ) |
| 95 | | peano2nn 12278 |
. . . . . . . . 9
⊢ (𝑜 ∈ ℕ → (𝑜 + 1) ∈
ℕ) |
| 96 | 95 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑜 ∈ ℕ) → (𝑜 + 1) ∈ ℕ) |
| 97 | | eluznn 12960 |
. . . . . . . 8
⊢ (((𝑜 + 1) ∈ ℕ ∧ 𝑞 ∈
(ℤ≥‘(𝑜 + 1))) → 𝑞 ∈ ℕ) |
| 98 | 96, 97 | sylan 580 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑞 ∈ (ℤ≥‘(𝑜 + 1))) → 𝑞 ∈
ℕ) |
| 99 | | nnsub 12310 |
. . . . . . 7
⊢ ((𝑜 ∈ ℕ ∧ 𝑞 ∈ ℕ) → (𝑜 < 𝑞 ↔ (𝑞 − 𝑜) ∈ ℕ)) |
| 100 | 94, 98, 99 | syl2anc 584 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑞 ∈ (ℤ≥‘(𝑜 + 1))) → (𝑜 < 𝑞 ↔ (𝑞 − 𝑜) ∈ ℕ)) |
| 101 | 93, 100 | mpbid 232 |
. . . . 5
⊢ (((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑞 ∈ (ℤ≥‘(𝑜 + 1))) → (𝑞 − 𝑜) ∈ ℕ) |
| 102 | | eluzelcn 12890 |
. . . . . . 7
⊢ (𝑞 ∈
(ℤ≥‘(𝑜 + 1)) → 𝑞 ∈ ℂ) |
| 103 | 102 | ad2antlr 727 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑞 ∈ (ℤ≥‘(𝑜 + 1))) ∧ 𝑝 = (𝑞 − 𝑜)) → 𝑞 ∈ ℂ) |
| 104 | | nncn 12274 |
. . . . . . . 8
⊢ (𝑜 ∈ ℕ → 𝑜 ∈
ℂ) |
| 105 | 104 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑜 ∈ ℕ) → 𝑜 ∈ ℂ) |
| 106 | 105 | ad2antrr 726 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑞 ∈ (ℤ≥‘(𝑜 + 1))) ∧ 𝑝 = (𝑞 − 𝑜)) → 𝑜 ∈ ℂ) |
| 107 | | simpr 484 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑞 ∈ (ℤ≥‘(𝑜 + 1))) ∧ 𝑝 = (𝑞 − 𝑜)) → 𝑝 = (𝑞 − 𝑜)) |
| 108 | 103, 106,
107 | rsubrotld 42313 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑞 ∈ (ℤ≥‘(𝑜 + 1))) ∧ 𝑝 = (𝑞 − 𝑜)) → 𝑞 = (𝑜 + 𝑝)) |
| 109 | 101, 108 | rspcedeq2vd 3630 |
. . . 4
⊢ (((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑞 ∈ (ℤ≥‘(𝑜 + 1))) → ∃𝑝 ∈ ℕ 𝑞 = (𝑜 + 𝑝)) |
| 110 | | oveq1 7438 |
. . . . . 6
⊢ (𝑞 = (𝑜 + 𝑝) → (𝑞 · 𝐴) = ((𝑜 + 𝑝) · 𝐴)) |
| 111 | 110 | eqeq2d 2748 |
. . . . 5
⊢ (𝑞 = (𝑜 + 𝑝) → ((𝑜 · 𝐴) = (𝑞 · 𝐴) ↔ (𝑜 · 𝐴) = ((𝑜 + 𝑝) · 𝐴))) |
| 112 | 111 | adantl 481 |
. . . 4
⊢ (((𝜑 ∧ 𝑜 ∈ ℕ) ∧ 𝑞 = (𝑜 + 𝑝)) → ((𝑜 · 𝐴) = (𝑞 · 𝐴) ↔ (𝑜 · 𝐴) = ((𝑜 + 𝑝) · 𝐴))) |
| 113 | 89, 109, 112 | rexxfrd 5409 |
. . 3
⊢ ((𝜑 ∧ 𝑜 ∈ ℕ) → (∃𝑞 ∈
(ℤ≥‘(𝑜 + 1))(𝑜 · 𝐴) = (𝑞 · 𝐴) ↔ ∃𝑝 ∈ ℕ (𝑜 · 𝐴) = ((𝑜 + 𝑝) · 𝐴))) |
| 114 | 113 | rexbidva 3177 |
. 2
⊢ (𝜑 → (∃𝑜 ∈ ℕ ∃𝑞 ∈ (ℤ≥‘(𝑜 + 1))(𝑜 · 𝐴) = (𝑞 · 𝐴) ↔ ∃𝑜 ∈ ℕ ∃𝑝 ∈ ℕ (𝑜 · 𝐴) = ((𝑜 + 𝑝) · 𝐴))) |
| 115 | 76, 114 | mpbid 232 |
1
⊢ (𝜑 → ∃𝑜 ∈ ℕ ∃𝑝 ∈ ℕ (𝑜 · 𝐴) = ((𝑜 + 𝑝) · 𝐴)) |