| Step | Hyp | Ref
| Expression |
| 1 | | id 22 |
. . . . . 6
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℕ) |
| 2 | | vdwlem2.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 3 | | nnaddcl 12289 |
. . . . . 6
⊢ ((𝑎 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑎 + 𝑁) ∈ ℕ) |
| 4 | 1, 2, 3 | syl2anr 597 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → (𝑎 + 𝑁) ∈ ℕ) |
| 5 | | simpllr 776 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑎 ∈ ℕ) |
| 6 | 5 | nncnd 12282 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑎 ∈ ℂ) |
| 7 | 2 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑁 ∈ ℕ) |
| 8 | 7 | nncnd 12282 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑁 ∈ ℂ) |
| 9 | | elfznn0 13660 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ (0...(𝐾 − 1)) → 𝑚 ∈ ℕ0) |
| 10 | 9 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℕ0) |
| 11 | 10 | nn0cnd 12589 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ) |
| 12 | | simplrl 777 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑑 ∈ ℕ) |
| 13 | 12 | nncnd 12282 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑑 ∈ ℂ) |
| 14 | 11, 13 | mulcld 11281 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · 𝑑) ∈ ℂ) |
| 15 | 6, 8, 14 | add32d 11489 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑎 + 𝑁) + (𝑚 · 𝑑)) = ((𝑎 + (𝑚 · 𝑑)) + 𝑁)) |
| 16 | | oveq1 7438 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑎 + (𝑚 · 𝑑)) → (𝑥 + 𝑁) = ((𝑎 + (𝑚 · 𝑑)) + 𝑁)) |
| 17 | 16 | eleq1d 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑎 + (𝑚 · 𝑑)) → ((𝑥 + 𝑁) ∈ (1...𝑀) ↔ ((𝑎 + (𝑚 · 𝑑)) + 𝑁) ∈ (1...𝑀))) |
| 18 | | elfznn 13593 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (1...𝑊) → 𝑥 ∈ ℕ) |
| 19 | | nnaddcl 12289 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑥 + 𝑁) ∈ ℕ) |
| 20 | 18, 2, 19 | syl2anr 597 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑊)) → (𝑥 + 𝑁) ∈ ℕ) |
| 21 | | nnuz 12921 |
. . . . . . . . . . . . . . . . . 18
⊢ ℕ =
(ℤ≥‘1) |
| 22 | 20, 21 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑊)) → (𝑥 + 𝑁) ∈
(ℤ≥‘1)) |
| 23 | | vdwlem2.m |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘(𝑊 + 𝑁))) |
| 24 | | elfzuz3 13561 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (1...𝑊) → 𝑊 ∈ (ℤ≥‘𝑥)) |
| 25 | 2 | nnzd 12640 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 26 | | eluzadd 12907 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈
(ℤ≥‘𝑥) ∧ 𝑁 ∈ ℤ) → (𝑊 + 𝑁) ∈
(ℤ≥‘(𝑥 + 𝑁))) |
| 27 | 24, 25, 26 | syl2anr 597 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑊)) → (𝑊 + 𝑁) ∈
(ℤ≥‘(𝑥 + 𝑁))) |
| 28 | | uztrn 12896 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈
(ℤ≥‘(𝑊 + 𝑁)) ∧ (𝑊 + 𝑁) ∈
(ℤ≥‘(𝑥 + 𝑁))) → 𝑀 ∈ (ℤ≥‘(𝑥 + 𝑁))) |
| 29 | 23, 27, 28 | syl2an2r 685 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑊)) → 𝑀 ∈ (ℤ≥‘(𝑥 + 𝑁))) |
| 30 | | elfzuzb 13558 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 + 𝑁) ∈ (1...𝑀) ↔ ((𝑥 + 𝑁) ∈ (ℤ≥‘1)
∧ 𝑀 ∈
(ℤ≥‘(𝑥 + 𝑁)))) |
| 31 | 22, 29, 30 | sylanbrc 583 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑊)) → (𝑥 + 𝑁) ∈ (1...𝑀)) |
| 32 | 31 | ralrimiva 3146 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑥 ∈ (1...𝑊)(𝑥 + 𝑁) ∈ (1...𝑀)) |
| 33 | 32 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ∀𝑥 ∈ (1...𝑊)(𝑥 + 𝑁) ∈ (1...𝑀)) |
| 34 | | simplrr 778 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐})) |
| 35 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 + (𝑚 · 𝑑)) = (𝑎 + (𝑚 · 𝑑)) |
| 36 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑚 → (𝑛 · 𝑑) = (𝑚 · 𝑑)) |
| 37 | 36 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑚 → (𝑎 + (𝑛 · 𝑑)) = (𝑎 + (𝑚 · 𝑑))) |
| 38 | 37 | rspceeqv 3645 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑚 ∈ (0...(𝐾 − 1)) ∧ (𝑎 + (𝑚 · 𝑑)) = (𝑎 + (𝑚 · 𝑑))) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) = (𝑎 + (𝑛 · 𝑑))) |
| 39 | 35, 38 | mpan2 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) = (𝑎 + (𝑛 · 𝑑))) |
| 40 | 39 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) = (𝑎 + (𝑛 · 𝑑))) |
| 41 | | vdwlem2.k |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
| 42 | 41 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) → 𝐾 ∈
ℕ0) |
| 43 | 42 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐾 ∈
ℕ0) |
| 44 | | vdwapval 17011 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐾 ∈ ℕ0
∧ 𝑎 ∈ ℕ
∧ 𝑑 ∈ ℕ)
→ ((𝑎 + (𝑚 · 𝑑)) ∈ (𝑎(AP‘𝐾)𝑑) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) = (𝑎 + (𝑛 · 𝑑)))) |
| 45 | 43, 5, 12, 44 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑎 + (𝑚 · 𝑑)) ∈ (𝑎(AP‘𝐾)𝑑) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) = (𝑎 + (𝑛 · 𝑑)))) |
| 46 | 40, 45 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑎 + (𝑚 · 𝑑)) ∈ (𝑎(AP‘𝐾)𝑑)) |
| 47 | 34, 46 | sseldd 3984 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐺 “ {𝑐})) |
| 48 | | vdwlem2.f |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐹:(1...𝑀)⟶𝑅) |
| 49 | 48 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑥 + 𝑁) ∈ (1...𝑀)) → (𝐹‘(𝑥 + 𝑁)) ∈ 𝑅) |
| 50 | 31, 49 | syldan 591 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑊)) → (𝐹‘(𝑥 + 𝑁)) ∈ 𝑅) |
| 51 | | vdwlem2.g |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐺 = (𝑥 ∈ (1...𝑊) ↦ (𝐹‘(𝑥 + 𝑁))) |
| 52 | 50, 51 | fmptd 7134 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐺:(1...𝑊)⟶𝑅) |
| 53 | 52 | ffnd 6737 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐺 Fn (1...𝑊)) |
| 54 | 53 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐺 Fn (1...𝑊)) |
| 55 | | fniniseg 7080 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 Fn (1...𝑊) → ((𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐺 “ {𝑐}) ↔ ((𝑎 + (𝑚 · 𝑑)) ∈ (1...𝑊) ∧ (𝐺‘(𝑎 + (𝑚 · 𝑑))) = 𝑐))) |
| 56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐺 “ {𝑐}) ↔ ((𝑎 + (𝑚 · 𝑑)) ∈ (1...𝑊) ∧ (𝐺‘(𝑎 + (𝑚 · 𝑑))) = 𝑐))) |
| 57 | 47, 56 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑎 + (𝑚 · 𝑑)) ∈ (1...𝑊) ∧ (𝐺‘(𝑎 + (𝑚 · 𝑑))) = 𝑐)) |
| 58 | 57 | simpld 494 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑎 + (𝑚 · 𝑑)) ∈ (1...𝑊)) |
| 59 | 17, 33, 58 | rspcdva 3623 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑎 + (𝑚 · 𝑑)) + 𝑁) ∈ (1...𝑀)) |
| 60 | 15, 59 | eqeltrd 2841 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑎 + 𝑁) + (𝑚 · 𝑑)) ∈ (1...𝑀)) |
| 61 | 15 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘((𝑎 + 𝑁) + (𝑚 · 𝑑))) = (𝐹‘((𝑎 + (𝑚 · 𝑑)) + 𝑁))) |
| 62 | 16 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑎 + (𝑚 · 𝑑)) → (𝐹‘(𝑥 + 𝑁)) = (𝐹‘((𝑎 + (𝑚 · 𝑑)) + 𝑁))) |
| 63 | | fvex 6919 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘((𝑎 + (𝑚 · 𝑑)) + 𝑁)) ∈ V |
| 64 | 62, 51, 63 | fvmpt 7016 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 + (𝑚 · 𝑑)) ∈ (1...𝑊) → (𝐺‘(𝑎 + (𝑚 · 𝑑))) = (𝐹‘((𝑎 + (𝑚 · 𝑑)) + 𝑁))) |
| 65 | 58, 64 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘(𝑎 + (𝑚 · 𝑑))) = (𝐹‘((𝑎 + (𝑚 · 𝑑)) + 𝑁))) |
| 66 | 57 | simprd 495 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘(𝑎 + (𝑚 · 𝑑))) = 𝑐) |
| 67 | 61, 65, 66 | 3eqtr2d 2783 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘((𝑎 + 𝑁) + (𝑚 · 𝑑))) = 𝑐) |
| 68 | 60, 67 | jca 511 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝑎 + 𝑁) + (𝑚 · 𝑑)) ∈ (1...𝑀) ∧ (𝐹‘((𝑎 + 𝑁) + (𝑚 · 𝑑))) = 𝑐)) |
| 69 | | eleq1 2829 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((𝑎 + 𝑁) + (𝑚 · 𝑑)) → (𝑥 ∈ (1...𝑀) ↔ ((𝑎 + 𝑁) + (𝑚 · 𝑑)) ∈ (1...𝑀))) |
| 70 | | fveqeq2 6915 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((𝑎 + 𝑁) + (𝑚 · 𝑑)) → ((𝐹‘𝑥) = 𝑐 ↔ (𝐹‘((𝑎 + 𝑁) + (𝑚 · 𝑑))) = 𝑐)) |
| 71 | 69, 70 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑥 = ((𝑎 + 𝑁) + (𝑚 · 𝑑)) → ((𝑥 ∈ (1...𝑀) ∧ (𝐹‘𝑥) = 𝑐) ↔ (((𝑎 + 𝑁) + (𝑚 · 𝑑)) ∈ (1...𝑀) ∧ (𝐹‘((𝑎 + 𝑁) + (𝑚 · 𝑑))) = 𝑐))) |
| 72 | 68, 71 | syl5ibrcom 247 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑥 = ((𝑎 + 𝑁) + (𝑚 · 𝑑)) → (𝑥 ∈ (1...𝑀) ∧ (𝐹‘𝑥) = 𝑐))) |
| 73 | 72 | rexlimdva 3155 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) → (∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝑎 + 𝑁) + (𝑚 · 𝑑)) → (𝑥 ∈ (1...𝑀) ∧ (𝐹‘𝑥) = 𝑐))) |
| 74 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) → (𝑎 + 𝑁) ∈ ℕ) |
| 75 | | simprl 771 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) → 𝑑 ∈ ℕ) |
| 76 | | vdwapval 17011 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ0
∧ (𝑎 + 𝑁) ∈ ℕ ∧ 𝑑 ∈ ℕ) → (𝑥 ∈ ((𝑎 + 𝑁)(AP‘𝐾)𝑑) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝑎 + 𝑁) + (𝑚 · 𝑑)))) |
| 77 | 42, 74, 75, 76 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) → (𝑥 ∈ ((𝑎 + 𝑁)(AP‘𝐾)𝑑) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝑎 + 𝑁) + (𝑚 · 𝑑)))) |
| 78 | 48 | ffnd 6737 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 Fn (1...𝑀)) |
| 79 | 78 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) → 𝐹 Fn (1...𝑀)) |
| 80 | | fniniseg 7080 |
. . . . . . . . . 10
⊢ (𝐹 Fn (1...𝑀) → (𝑥 ∈ (◡𝐹 “ {𝑐}) ↔ (𝑥 ∈ (1...𝑀) ∧ (𝐹‘𝑥) = 𝑐))) |
| 81 | 79, 80 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) → (𝑥 ∈ (◡𝐹 “ {𝑐}) ↔ (𝑥 ∈ (1...𝑀) ∧ (𝐹‘𝑥) = 𝑐))) |
| 82 | 73, 77, 81 | 3imtr4d 294 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) → (𝑥 ∈ ((𝑎 + 𝑁)(AP‘𝐾)𝑑) → 𝑥 ∈ (◡𝐹 “ {𝑐}))) |
| 83 | 82 | ssrdv 3989 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) → ((𝑎 + 𝑁)(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})) |
| 84 | 83 | expr 456 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑑 ∈ ℕ) → ((𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}) → ((𝑎 + 𝑁)(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
| 85 | 84 | reximdva 3168 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → (∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}) → ∃𝑑 ∈ ℕ ((𝑎 + 𝑁)(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
| 86 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑏 = (𝑎 + 𝑁) → (𝑏(AP‘𝐾)𝑑) = ((𝑎 + 𝑁)(AP‘𝐾)𝑑)) |
| 87 | 86 | sseq1d 4015 |
. . . . . . 7
⊢ (𝑏 = (𝑎 + 𝑁) → ((𝑏(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}) ↔ ((𝑎 + 𝑁)(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
| 88 | 87 | rexbidv 3179 |
. . . . . 6
⊢ (𝑏 = (𝑎 + 𝑁) → (∃𝑑 ∈ ℕ (𝑏(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}) ↔ ∃𝑑 ∈ ℕ ((𝑎 + 𝑁)(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
| 89 | 88 | rspcev 3622 |
. . . . 5
⊢ (((𝑎 + 𝑁) ∈ ℕ ∧ ∃𝑑 ∈ ℕ ((𝑎 + 𝑁)(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})) → ∃𝑏 ∈ ℕ ∃𝑑 ∈ ℕ (𝑏(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})) |
| 90 | 4, 85, 89 | syl6an 684 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → (∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}) → ∃𝑏 ∈ ℕ ∃𝑑 ∈ ℕ (𝑏(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
| 91 | 90 | rexlimdva 3155 |
. . 3
⊢ (𝜑 → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}) → ∃𝑏 ∈ ℕ ∃𝑑 ∈ ℕ (𝑏(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
| 92 | 91 | eximdv 1917 |
. 2
⊢ (𝜑 → (∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}) → ∃𝑐∃𝑏 ∈ ℕ ∃𝑑 ∈ ℕ (𝑏(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
| 93 | | ovex 7464 |
. . 3
⊢
(1...𝑊) ∈
V |
| 94 | 93, 41, 52 | vdwmc 17016 |
. 2
⊢ (𝜑 → (𝐾 MonoAP 𝐺 ↔ ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) |
| 95 | | ovex 7464 |
. . 3
⊢
(1...𝑀) ∈
V |
| 96 | 95, 41, 48 | vdwmc 17016 |
. 2
⊢ (𝜑 → (𝐾 MonoAP 𝐹 ↔ ∃𝑐∃𝑏 ∈ ℕ ∃𝑑 ∈ ℕ (𝑏(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
| 97 | 92, 94, 96 | 3imtr4d 294 |
1
⊢ (𝜑 → (𝐾 MonoAP 𝐺 → 𝐾 MonoAP 𝐹)) |