Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . 6
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℕ) |
2 | | vdwlem2.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
3 | | nnaddcl 10919 |
. . . . . 6
⊢ ((𝑎 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑎 + 𝑁) ∈ ℕ) |
4 | 1, 2, 3 | syl2anr 494 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → (𝑎 + 𝑁) ∈ ℕ) |
5 | | simpllr 795 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑎 ∈ ℕ) |
6 | 5 | nncnd 10913 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑎 ∈ ℂ) |
7 | 2 | ad3antrrr 762 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑁 ∈ ℕ) |
8 | 7 | nncnd 10913 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑁 ∈ ℂ) |
9 | | elfznn0 12302 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ (0...(𝐾 − 1)) → 𝑚 ∈ ℕ0) |
10 | 9 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℕ0) |
11 | 10 | nn0cnd 11230 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ) |
12 | | simplrl 796 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑑 ∈ ℕ) |
13 | 12 | nncnd 10913 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑑 ∈ ℂ) |
14 | 11, 13 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · 𝑑) ∈ ℂ) |
15 | 6, 8, 14 | add32d 10142 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑎 + 𝑁) + (𝑚 · 𝑑)) = ((𝑎 + (𝑚 · 𝑑)) + 𝑁)) |
16 | | simplrr 797 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐})) |
17 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 + (𝑚 · 𝑑)) = (𝑎 + (𝑚 · 𝑑)) |
18 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑚 → (𝑛 · 𝑑) = (𝑚 · 𝑑)) |
19 | 18 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑚 → (𝑎 + (𝑛 · 𝑑)) = (𝑎 + (𝑚 · 𝑑))) |
20 | 19 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑚 → ((𝑎 + (𝑚 · 𝑑)) = (𝑎 + (𝑛 · 𝑑)) ↔ (𝑎 + (𝑚 · 𝑑)) = (𝑎 + (𝑚 · 𝑑)))) |
21 | 20 | rspcev 3282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑚 ∈ (0...(𝐾 − 1)) ∧ (𝑎 + (𝑚 · 𝑑)) = (𝑎 + (𝑚 · 𝑑))) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) = (𝑎 + (𝑛 · 𝑑))) |
22 | 17, 21 | mpan2 703 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) = (𝑎 + (𝑛 · 𝑑))) |
23 | 22 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) = (𝑎 + (𝑛 · 𝑑))) |
24 | | vdwlem2.k |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
25 | 24 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) → 𝐾 ∈
ℕ0) |
26 | 25 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐾 ∈
ℕ0) |
27 | | vdwapval 15515 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐾 ∈ ℕ0
∧ 𝑎 ∈ ℕ
∧ 𝑑 ∈ ℕ)
→ ((𝑎 + (𝑚 · 𝑑)) ∈ (𝑎(AP‘𝐾)𝑑) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) = (𝑎 + (𝑛 · 𝑑)))) |
28 | 26, 5, 12, 27 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑎 + (𝑚 · 𝑑)) ∈ (𝑎(AP‘𝐾)𝑑) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) = (𝑎 + (𝑛 · 𝑑)))) |
29 | 23, 28 | mpbird 246 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑎 + (𝑚 · 𝑑)) ∈ (𝑎(AP‘𝐾)𝑑)) |
30 | 16, 29 | sseldd 3569 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐺 “ {𝑐})) |
31 | | elfznn 12241 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ (1...𝑊) → 𝑥 ∈ ℕ) |
32 | | nnaddcl 10919 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑥 + 𝑁) ∈ ℕ) |
33 | 31, 2, 32 | syl2anr 494 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑊)) → (𝑥 + 𝑁) ∈ ℕ) |
34 | | nnuz 11599 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ℕ =
(ℤ≥‘1) |
35 | 33, 34 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑊)) → (𝑥 + 𝑁) ∈
(ℤ≥‘1)) |
36 | | vdwlem2.m |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘(𝑊 + 𝑁))) |
37 | 36 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑊)) → 𝑀 ∈ (ℤ≥‘(𝑊 + 𝑁))) |
38 | | elfzuz3 12210 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ (1...𝑊) → 𝑊 ∈ (ℤ≥‘𝑥)) |
39 | 2 | nnzd 11357 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑁 ∈ ℤ) |
40 | | eluzadd 11592 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑊 ∈
(ℤ≥‘𝑥) ∧ 𝑁 ∈ ℤ) → (𝑊 + 𝑁) ∈
(ℤ≥‘(𝑥 + 𝑁))) |
41 | 38, 39, 40 | syl2anr 494 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑊)) → (𝑊 + 𝑁) ∈
(ℤ≥‘(𝑥 + 𝑁))) |
42 | | uztrn 11580 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀 ∈
(ℤ≥‘(𝑊 + 𝑁)) ∧ (𝑊 + 𝑁) ∈
(ℤ≥‘(𝑥 + 𝑁))) → 𝑀 ∈ (ℤ≥‘(𝑥 + 𝑁))) |
43 | 37, 41, 42 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑊)) → 𝑀 ∈ (ℤ≥‘(𝑥 + 𝑁))) |
44 | | elfzuzb 12207 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 + 𝑁) ∈ (1...𝑀) ↔ ((𝑥 + 𝑁) ∈ (ℤ≥‘1)
∧ 𝑀 ∈
(ℤ≥‘(𝑥 + 𝑁)))) |
45 | 35, 43, 44 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑊)) → (𝑥 + 𝑁) ∈ (1...𝑀)) |
46 | | vdwlem2.f |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐹:(1...𝑀)⟶𝑅) |
47 | 46 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑥 + 𝑁) ∈ (1...𝑀)) → (𝐹‘(𝑥 + 𝑁)) ∈ 𝑅) |
48 | 45, 47 | syldan 486 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑊)) → (𝐹‘(𝑥 + 𝑁)) ∈ 𝑅) |
49 | | vdwlem2.g |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐺 = (𝑥 ∈ (1...𝑊) ↦ (𝐹‘(𝑥 + 𝑁))) |
50 | 48, 49 | fmptd 6292 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐺:(1...𝑊)⟶𝑅) |
51 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐺:(1...𝑊)⟶𝑅 → 𝐺 Fn (1...𝑊)) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐺 Fn (1...𝑊)) |
53 | 52 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐺 Fn (1...𝑊)) |
54 | | fniniseg 6246 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 Fn (1...𝑊) → ((𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐺 “ {𝑐}) ↔ ((𝑎 + (𝑚 · 𝑑)) ∈ (1...𝑊) ∧ (𝐺‘(𝑎 + (𝑚 · 𝑑))) = 𝑐))) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐺 “ {𝑐}) ↔ ((𝑎 + (𝑚 · 𝑑)) ∈ (1...𝑊) ∧ (𝐺‘(𝑎 + (𝑚 · 𝑑))) = 𝑐))) |
56 | 30, 55 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑎 + (𝑚 · 𝑑)) ∈ (1...𝑊) ∧ (𝐺‘(𝑎 + (𝑚 · 𝑑))) = 𝑐)) |
57 | 56 | simpld 474 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑎 + (𝑚 · 𝑑)) ∈ (1...𝑊)) |
58 | 45 | ralrimiva 2949 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑥 ∈ (1...𝑊)(𝑥 + 𝑁) ∈ (1...𝑀)) |
59 | 58 | ad3antrrr 762 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ∀𝑥 ∈ (1...𝑊)(𝑥 + 𝑁) ∈ (1...𝑀)) |
60 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑎 + (𝑚 · 𝑑)) → (𝑥 + 𝑁) = ((𝑎 + (𝑚 · 𝑑)) + 𝑁)) |
61 | 60 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑎 + (𝑚 · 𝑑)) → ((𝑥 + 𝑁) ∈ (1...𝑀) ↔ ((𝑎 + (𝑚 · 𝑑)) + 𝑁) ∈ (1...𝑀))) |
62 | 61 | rspcv 3278 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 + (𝑚 · 𝑑)) ∈ (1...𝑊) → (∀𝑥 ∈ (1...𝑊)(𝑥 + 𝑁) ∈ (1...𝑀) → ((𝑎 + (𝑚 · 𝑑)) + 𝑁) ∈ (1...𝑀))) |
63 | 57, 59, 62 | sylc 63 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑎 + (𝑚 · 𝑑)) + 𝑁) ∈ (1...𝑀)) |
64 | 15, 63 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑎 + 𝑁) + (𝑚 · 𝑑)) ∈ (1...𝑀)) |
65 | 15 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘((𝑎 + 𝑁) + (𝑚 · 𝑑))) = (𝐹‘((𝑎 + (𝑚 · 𝑑)) + 𝑁))) |
66 | 60 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑎 + (𝑚 · 𝑑)) → (𝐹‘(𝑥 + 𝑁)) = (𝐹‘((𝑎 + (𝑚 · 𝑑)) + 𝑁))) |
67 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘((𝑎 + (𝑚 · 𝑑)) + 𝑁)) ∈ V |
68 | 66, 49, 67 | fvmpt 6191 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 + (𝑚 · 𝑑)) ∈ (1...𝑊) → (𝐺‘(𝑎 + (𝑚 · 𝑑))) = (𝐹‘((𝑎 + (𝑚 · 𝑑)) + 𝑁))) |
69 | 57, 68 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘(𝑎 + (𝑚 · 𝑑))) = (𝐹‘((𝑎 + (𝑚 · 𝑑)) + 𝑁))) |
70 | 56 | simprd 478 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘(𝑎 + (𝑚 · 𝑑))) = 𝑐) |
71 | 65, 69, 70 | 3eqtr2d 2650 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘((𝑎 + 𝑁) + (𝑚 · 𝑑))) = 𝑐) |
72 | 64, 71 | jca 553 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝑎 + 𝑁) + (𝑚 · 𝑑)) ∈ (1...𝑀) ∧ (𝐹‘((𝑎 + 𝑁) + (𝑚 · 𝑑))) = 𝑐)) |
73 | | eleq1 2676 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((𝑎 + 𝑁) + (𝑚 · 𝑑)) → (𝑥 ∈ (1...𝑀) ↔ ((𝑎 + 𝑁) + (𝑚 · 𝑑)) ∈ (1...𝑀))) |
74 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ((𝑎 + 𝑁) + (𝑚 · 𝑑)) → (𝐹‘𝑥) = (𝐹‘((𝑎 + 𝑁) + (𝑚 · 𝑑)))) |
75 | 74 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((𝑎 + 𝑁) + (𝑚 · 𝑑)) → ((𝐹‘𝑥) = 𝑐 ↔ (𝐹‘((𝑎 + 𝑁) + (𝑚 · 𝑑))) = 𝑐)) |
76 | 73, 75 | anbi12d 743 |
. . . . . . . . . . 11
⊢ (𝑥 = ((𝑎 + 𝑁) + (𝑚 · 𝑑)) → ((𝑥 ∈ (1...𝑀) ∧ (𝐹‘𝑥) = 𝑐) ↔ (((𝑎 + 𝑁) + (𝑚 · 𝑑)) ∈ (1...𝑀) ∧ (𝐹‘((𝑎 + 𝑁) + (𝑚 · 𝑑))) = 𝑐))) |
77 | 72, 76 | syl5ibrcom 236 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑥 = ((𝑎 + 𝑁) + (𝑚 · 𝑑)) → (𝑥 ∈ (1...𝑀) ∧ (𝐹‘𝑥) = 𝑐))) |
78 | 77 | rexlimdva 3013 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) → (∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝑎 + 𝑁) + (𝑚 · 𝑑)) → (𝑥 ∈ (1...𝑀) ∧ (𝐹‘𝑥) = 𝑐))) |
79 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) → (𝑎 + 𝑁) ∈ ℕ) |
80 | | simprl 790 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) → 𝑑 ∈ ℕ) |
81 | | vdwapval 15515 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ0
∧ (𝑎 + 𝑁) ∈ ℕ ∧ 𝑑 ∈ ℕ) → (𝑥 ∈ ((𝑎 + 𝑁)(AP‘𝐾)𝑑) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝑎 + 𝑁) + (𝑚 · 𝑑)))) |
82 | 25, 79, 80, 81 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) → (𝑥 ∈ ((𝑎 + 𝑁)(AP‘𝐾)𝑑) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝑎 + 𝑁) + (𝑚 · 𝑑)))) |
83 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ (𝐹:(1...𝑀)⟶𝑅 → 𝐹 Fn (1...𝑀)) |
84 | 46, 83 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 Fn (1...𝑀)) |
85 | 84 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) → 𝐹 Fn (1...𝑀)) |
86 | | fniniseg 6246 |
. . . . . . . . . 10
⊢ (𝐹 Fn (1...𝑀) → (𝑥 ∈ (◡𝐹 “ {𝑐}) ↔ (𝑥 ∈ (1...𝑀) ∧ (𝐹‘𝑥) = 𝑐))) |
87 | 85, 86 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) → (𝑥 ∈ (◡𝐹 “ {𝑐}) ↔ (𝑥 ∈ (1...𝑀) ∧ (𝐹‘𝑥) = 𝑐))) |
88 | 78, 82, 87 | 3imtr4d 282 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) → (𝑥 ∈ ((𝑎 + 𝑁)(AP‘𝐾)𝑑) → 𝑥 ∈ (◡𝐹 “ {𝑐}))) |
89 | 88 | ssrdv 3574 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) → ((𝑎 + 𝑁)(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})) |
90 | 89 | expr 641 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑑 ∈ ℕ) → ((𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}) → ((𝑎 + 𝑁)(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
91 | 90 | reximdva 3000 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → (∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}) → ∃𝑑 ∈ ℕ ((𝑎 + 𝑁)(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
92 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑏 = (𝑎 + 𝑁) → (𝑏(AP‘𝐾)𝑑) = ((𝑎 + 𝑁)(AP‘𝐾)𝑑)) |
93 | 92 | sseq1d 3595 |
. . . . . . 7
⊢ (𝑏 = (𝑎 + 𝑁) → ((𝑏(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}) ↔ ((𝑎 + 𝑁)(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
94 | 93 | rexbidv 3034 |
. . . . . 6
⊢ (𝑏 = (𝑎 + 𝑁) → (∃𝑑 ∈ ℕ (𝑏(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}) ↔ ∃𝑑 ∈ ℕ ((𝑎 + 𝑁)(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
95 | 94 | rspcev 3282 |
. . . . 5
⊢ (((𝑎 + 𝑁) ∈ ℕ ∧ ∃𝑑 ∈ ℕ ((𝑎 + 𝑁)(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})) → ∃𝑏 ∈ ℕ ∃𝑑 ∈ ℕ (𝑏(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})) |
96 | 4, 91, 95 | syl6an 566 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → (∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}) → ∃𝑏 ∈ ℕ ∃𝑑 ∈ ℕ (𝑏(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
97 | 96 | rexlimdva 3013 |
. . 3
⊢ (𝜑 → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}) → ∃𝑏 ∈ ℕ ∃𝑑 ∈ ℕ (𝑏(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
98 | 97 | eximdv 1833 |
. 2
⊢ (𝜑 → (∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}) → ∃𝑐∃𝑏 ∈ ℕ ∃𝑑 ∈ ℕ (𝑏(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
99 | | ovex 6577 |
. . 3
⊢
(1...𝑊) ∈
V |
100 | 99, 24, 50 | vdwmc 15520 |
. 2
⊢ (𝜑 → (𝐾 MonoAP 𝐺 ↔ ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐺 “ {𝑐}))) |
101 | | ovex 6577 |
. . 3
⊢
(1...𝑀) ∈
V |
102 | 101, 24, 46 | vdwmc 15520 |
. 2
⊢ (𝜑 → (𝐾 MonoAP 𝐹 ↔ ∃𝑐∃𝑏 ∈ ℕ ∃𝑑 ∈ ℕ (𝑏(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
103 | 98, 100, 102 | 3imtr4d 282 |
1
⊢ (𝜑 → (𝐾 MonoAP 𝐺 → 𝐾 MonoAP 𝐹)) |