MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vdwapun Structured version   Visualization version   GIF version

Theorem vdwapun 16298
Description: Remove the first element of an arithmetic progression. (Contributed by Mario Carneiro, 11-Sep-2014.)
Assertion
Ref Expression
vdwapun ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴(AP‘(𝐾 + 1))𝐷) = ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘𝐾)𝐷)))

Proof of Theorem vdwapun
Dummy variables 𝑚 𝑛 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 peano2nn0 11925 . . . . 5 (𝐾 ∈ ℕ0 → (𝐾 + 1) ∈ ℕ0)
2 vdwapval 16297 . . . . 5 (((𝐾 + 1) ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑥 ∈ (𝐴(AP‘(𝐾 + 1))𝐷) ↔ ∃𝑛 ∈ (0...((𝐾 + 1) − 1))𝑥 = (𝐴 + (𝑛 · 𝐷))))
31, 2syl3an1 1155 . . . 4 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑥 ∈ (𝐴(AP‘(𝐾 + 1))𝐷) ↔ ∃𝑛 ∈ (0...((𝐾 + 1) − 1))𝑥 = (𝐴 + (𝑛 · 𝐷))))
4 simp1 1128 . . . . . . . . . . . . 13 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐾 ∈ ℕ0)
54nn0cnd 11945 . . . . . . . . . . . 12 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐾 ∈ ℂ)
6 ax-1cn 10583 . . . . . . . . . . . 12 1 ∈ ℂ
7 pncan 10880 . . . . . . . . . . . 12 ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 + 1) − 1) = 𝐾)
85, 6, 7sylancl 586 . . . . . . . . . . 11 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → ((𝐾 + 1) − 1) = 𝐾)
98oveq2d 7161 . . . . . . . . . 10 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (0...((𝐾 + 1) − 1)) = (0...𝐾))
109eleq2d 2895 . . . . . . . . 9 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑛 ∈ (0...((𝐾 + 1) − 1)) ↔ 𝑛 ∈ (0...𝐾)))
11 nn0uz 12268 . . . . . . . . . . 11 0 = (ℤ‘0)
124, 11eleqtrdi 2920 . . . . . . . . . 10 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐾 ∈ (ℤ‘0))
13 elfzp12 12974 . . . . . . . . . 10 (𝐾 ∈ (ℤ‘0) → (𝑛 ∈ (0...𝐾) ↔ (𝑛 = 0 ∨ 𝑛 ∈ ((0 + 1)...𝐾))))
1412, 13syl 17 . . . . . . . . 9 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑛 ∈ (0...𝐾) ↔ (𝑛 = 0 ∨ 𝑛 ∈ ((0 + 1)...𝐾))))
1510, 14bitrd 280 . . . . . . . 8 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑛 ∈ (0...((𝐾 + 1) − 1)) ↔ (𝑛 = 0 ∨ 𝑛 ∈ ((0 + 1)...𝐾))))
1615anbi1d 629 . . . . . . 7 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → ((𝑛 ∈ (0...((𝐾 + 1) − 1)) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ↔ ((𝑛 = 0 ∨ 𝑛 ∈ ((0 + 1)...𝐾)) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷)))))
17 andir 1002 . . . . . . 7 (((𝑛 = 0 ∨ 𝑛 ∈ ((0 + 1)...𝐾)) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ↔ ((𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ (𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷)))))
1816, 17syl6bb 288 . . . . . 6 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → ((𝑛 ∈ (0...((𝐾 + 1) − 1)) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ↔ ((𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ (𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))))))
1918exbidv 1913 . . . . 5 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (∃𝑛(𝑛 ∈ (0...((𝐾 + 1) − 1)) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ↔ ∃𝑛((𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ (𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))))))
20 df-rex 3141 . . . . 5 (∃𝑛 ∈ (0...((𝐾 + 1) − 1))𝑥 = (𝐴 + (𝑛 · 𝐷)) ↔ ∃𝑛(𝑛 ∈ (0...((𝐾 + 1) − 1)) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))))
21 19.43 1874 . . . . . 6 (∃𝑛((𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ (𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷)))) ↔ (∃𝑛(𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷)))))
2221bicomi 225 . . . . 5 ((∃𝑛(𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷)))) ↔ ∃𝑛((𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ (𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷)))))
2319, 20, 223bitr4g 315 . . . 4 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (∃𝑛 ∈ (0...((𝐾 + 1) − 1))𝑥 = (𝐴 + (𝑛 · 𝐷)) ↔ (∃𝑛(𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))))))
243, 23bitrd 280 . . 3 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑥 ∈ (𝐴(AP‘(𝐾 + 1))𝐷) ↔ (∃𝑛(𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))))))
25 nncn 11634 . . . . . . . . . . 11 (𝐷 ∈ ℕ → 𝐷 ∈ ℂ)
26253ad2ant3 1127 . . . . . . . . . 10 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐷 ∈ ℂ)
2726mul02d 10826 . . . . . . . . 9 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (0 · 𝐷) = 0)
2827oveq2d 7161 . . . . . . . 8 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴 + (0 · 𝐷)) = (𝐴 + 0))
29 nncn 11634 . . . . . . . . . 10 (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
30293ad2ant2 1126 . . . . . . . . 9 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐴 ∈ ℂ)
3130addid1d 10828 . . . . . . . 8 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴 + 0) = 𝐴)
3228, 31eqtrd 2853 . . . . . . 7 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴 + (0 · 𝐷)) = 𝐴)
3332eqeq2d 2829 . . . . . 6 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑥 = (𝐴 + (0 · 𝐷)) ↔ 𝑥 = 𝐴))
34 c0ex 10623 . . . . . . 7 0 ∈ V
35 oveq1 7152 . . . . . . . . 9 (𝑛 = 0 → (𝑛 · 𝐷) = (0 · 𝐷))
3635oveq2d 7161 . . . . . . . 8 (𝑛 = 0 → (𝐴 + (𝑛 · 𝐷)) = (𝐴 + (0 · 𝐷)))
3736eqeq2d 2829 . . . . . . 7 (𝑛 = 0 → (𝑥 = (𝐴 + (𝑛 · 𝐷)) ↔ 𝑥 = (𝐴 + (0 · 𝐷))))
3834, 37ceqsexv 3539 . . . . . 6 (∃𝑛(𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ↔ 𝑥 = (𝐴 + (0 · 𝐷)))
39 velsn 4573 . . . . . 6 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
4033, 38, 393bitr4g 315 . . . . 5 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (∃𝑛(𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ↔ 𝑥 ∈ {𝐴}))
41 simpr 485 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → 𝑛 ∈ ((0 + 1)...𝐾))
42 0p1e1 11747 . . . . . . . . . . . . . . 15 (0 + 1) = 1
4342oveq1i 7155 . . . . . . . . . . . . . 14 ((0 + 1)...𝐾) = (1...𝐾)
4441, 43eleqtrdi 2920 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → 𝑛 ∈ (1...𝐾))
45 1zzd 12001 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → 1 ∈ ℤ)
464adantr 481 . . . . . . . . . . . . . . 15 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → 𝐾 ∈ ℕ0)
4746nn0zd 12073 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → 𝐾 ∈ ℤ)
48 elfzelz 12896 . . . . . . . . . . . . . . 15 (𝑛 ∈ ((0 + 1)...𝐾) → 𝑛 ∈ ℤ)
4948adantl 482 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → 𝑛 ∈ ℤ)
50 fzsubel 12931 . . . . . . . . . . . . . 14 (((1 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑛 ∈ (1...𝐾) ↔ (𝑛 − 1) ∈ ((1 − 1)...(𝐾 − 1))))
5145, 47, 49, 45, 50syl22anc 834 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝑛 ∈ (1...𝐾) ↔ (𝑛 − 1) ∈ ((1 − 1)...(𝐾 − 1))))
5244, 51mpbid 233 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝑛 − 1) ∈ ((1 − 1)...(𝐾 − 1)))
53 1m1e0 11697 . . . . . . . . . . . . 13 (1 − 1) = 0
5453oveq1i 7155 . . . . . . . . . . . 12 ((1 − 1)...(𝐾 − 1)) = (0...(𝐾 − 1))
5552, 54eleqtrdi 2920 . . . . . . . . . . 11 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝑛 − 1) ∈ (0...(𝐾 − 1)))
5649zcnd 12076 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → 𝑛 ∈ ℂ)
57 1cnd 10624 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → 1 ∈ ℂ)
5826adantr 481 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → 𝐷 ∈ ℂ)
5956, 57, 58subdird 11085 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → ((𝑛 − 1) · 𝐷) = ((𝑛 · 𝐷) − (1 · 𝐷)))
6058mulid2d 10647 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (1 · 𝐷) = 𝐷)
6160oveq2d 7161 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → ((𝑛 · 𝐷) − (1 · 𝐷)) = ((𝑛 · 𝐷) − 𝐷))
6259, 61eqtrd 2853 . . . . . . . . . . . . . . 15 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → ((𝑛 − 1) · 𝐷) = ((𝑛 · 𝐷) − 𝐷))
6362oveq2d 7161 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝐷 + ((𝑛 − 1) · 𝐷)) = (𝐷 + ((𝑛 · 𝐷) − 𝐷)))
6456, 58mulcld 10649 . . . . . . . . . . . . . . 15 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝑛 · 𝐷) ∈ ℂ)
6558, 64pncan3d 10988 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝐷 + ((𝑛 · 𝐷) − 𝐷)) = (𝑛 · 𝐷))
6663, 65eqtr2d 2854 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝑛 · 𝐷) = (𝐷 + ((𝑛 − 1) · 𝐷)))
6766oveq2d 7161 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝐴 + (𝑛 · 𝐷)) = (𝐴 + (𝐷 + ((𝑛 − 1) · 𝐷))))
6830adantr 481 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → 𝐴 ∈ ℂ)
69 subcl 10873 . . . . . . . . . . . . . . 15 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑛 − 1) ∈ ℂ)
7056, 6, 69sylancl 586 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝑛 − 1) ∈ ℂ)
7170, 58mulcld 10649 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → ((𝑛 − 1) · 𝐷) ∈ ℂ)
7268, 58, 71addassd 10651 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → ((𝐴 + 𝐷) + ((𝑛 − 1) · 𝐷)) = (𝐴 + (𝐷 + ((𝑛 − 1) · 𝐷))))
7367, 72eqtr4d 2856 . . . . . . . . . . 11 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝐴 + (𝑛 · 𝐷)) = ((𝐴 + 𝐷) + ((𝑛 − 1) · 𝐷)))
74 oveq1 7152 . . . . . . . . . . . . 13 (𝑚 = (𝑛 − 1) → (𝑚 · 𝐷) = ((𝑛 − 1) · 𝐷))
7574oveq2d 7161 . . . . . . . . . . . 12 (𝑚 = (𝑛 − 1) → ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = ((𝐴 + 𝐷) + ((𝑛 − 1) · 𝐷)))
7675rspceeqv 3635 . . . . . . . . . . 11 (((𝑛 − 1) ∈ (0...(𝐾 − 1)) ∧ (𝐴 + (𝑛 · 𝐷)) = ((𝐴 + 𝐷) + ((𝑛 − 1) · 𝐷))) → ∃𝑚 ∈ (0...(𝐾 − 1))(𝐴 + (𝑛 · 𝐷)) = ((𝐴 + 𝐷) + (𝑚 · 𝐷)))
7755, 73, 76syl2anc 584 . . . . . . . . . 10 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → ∃𝑚 ∈ (0...(𝐾 − 1))(𝐴 + (𝑛 · 𝐷)) = ((𝐴 + 𝐷) + (𝑚 · 𝐷)))
78 eqeq1 2822 . . . . . . . . . . 11 (𝑥 = (𝐴 + (𝑛 · 𝐷)) → (𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷)) ↔ (𝐴 + (𝑛 · 𝐷)) = ((𝐴 + 𝐷) + (𝑚 · 𝐷))))
7978rexbidv 3294 . . . . . . . . . 10 (𝑥 = (𝐴 + (𝑛 · 𝐷)) → (∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))(𝐴 + (𝑛 · 𝐷)) = ((𝐴 + 𝐷) + (𝑚 · 𝐷))))
8077, 79syl5ibrcom 248 . . . . . . . . 9 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝑥 = (𝐴 + (𝑛 · 𝐷)) → ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷))))
8180expimpd 454 . . . . . . . 8 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → ((𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) → ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷))))
8281exlimdv 1925 . . . . . . 7 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) → ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷))))
83 simpr 485 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ (0...(𝐾 − 1)))
84 0zd 11981 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 0 ∈ ℤ)
854adantr 481 . . . . . . . . . . . . . . 15 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐾 ∈ ℕ0)
8685nn0zd 12073 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐾 ∈ ℤ)
87 peano2zm 12013 . . . . . . . . . . . . . 14 (𝐾 ∈ ℤ → (𝐾 − 1) ∈ ℤ)
8886, 87syl 17 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐾 − 1) ∈ ℤ)
89 elfzelz 12896 . . . . . . . . . . . . . 14 (𝑚 ∈ (0...(𝐾 − 1)) → 𝑚 ∈ ℤ)
9089adantl 482 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℤ)
91 1zzd 12001 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 1 ∈ ℤ)
92 fzaddel 12929 . . . . . . . . . . . . 13 (((0 ∈ ℤ ∧ (𝐾 − 1) ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑚 ∈ (0...(𝐾 − 1)) ↔ (𝑚 + 1) ∈ ((0 + 1)...((𝐾 − 1) + 1))))
9384, 88, 90, 91, 92syl22anc 834 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 ∈ (0...(𝐾 − 1)) ↔ (𝑚 + 1) ∈ ((0 + 1)...((𝐾 − 1) + 1))))
9483, 93mpbid 233 . . . . . . . . . . 11 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 + 1) ∈ ((0 + 1)...((𝐾 − 1) + 1)))
9585nn0cnd 11945 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐾 ∈ ℂ)
96 npcan 10883 . . . . . . . . . . . . 13 ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 − 1) + 1) = 𝐾)
9795, 6, 96sylancl 586 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐾 − 1) + 1) = 𝐾)
9897oveq2d 7161 . . . . . . . . . . 11 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((0 + 1)...((𝐾 − 1) + 1)) = ((0 + 1)...𝐾))
9994, 98eleqtrd 2912 . . . . . . . . . 10 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 + 1) ∈ ((0 + 1)...𝐾))
10030adantr 481 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐴 ∈ ℂ)
10126adantr 481 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐷 ∈ ℂ)
10290zcnd 12076 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ)
103102, 101mulcld 10649 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · 𝐷) ∈ ℂ)
104100, 101, 103addassd 10651 . . . . . . . . . . 11 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + (𝐷 + (𝑚 · 𝐷))))
105 1cnd 10624 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 1 ∈ ℂ)
106102, 105, 101adddird 10654 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑚 + 1) · 𝐷) = ((𝑚 · 𝐷) + (1 · 𝐷)))
107101, 103addcomd 10830 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐷 + (𝑚 · 𝐷)) = ((𝑚 · 𝐷) + 𝐷))
108101mulid2d 10647 . . . . . . . . . . . . . . 15 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (1 · 𝐷) = 𝐷)
109108oveq2d 7161 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑚 · 𝐷) + (1 · 𝐷)) = ((𝑚 · 𝐷) + 𝐷))
110107, 109eqtr4d 2856 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐷 + (𝑚 · 𝐷)) = ((𝑚 · 𝐷) + (1 · 𝐷)))
111106, 110eqtr4d 2856 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑚 + 1) · 𝐷) = (𝐷 + (𝑚 · 𝐷)))
112111oveq2d 7161 . . . . . . . . . . 11 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + ((𝑚 + 1) · 𝐷)) = (𝐴 + (𝐷 + (𝑚 · 𝐷))))
113104, 112eqtr4d 2856 . . . . . . . . . 10 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + ((𝑚 + 1) · 𝐷)))
114 ovex 7178 . . . . . . . . . . 11 (𝑚 + 1) ∈ V
115 eleq1 2897 . . . . . . . . . . . 12 (𝑛 = (𝑚 + 1) → (𝑛 ∈ ((0 + 1)...𝐾) ↔ (𝑚 + 1) ∈ ((0 + 1)...𝐾)))
116 oveq1 7152 . . . . . . . . . . . . . 14 (𝑛 = (𝑚 + 1) → (𝑛 · 𝐷) = ((𝑚 + 1) · 𝐷))
117116oveq2d 7161 . . . . . . . . . . . . 13 (𝑛 = (𝑚 + 1) → (𝐴 + (𝑛 · 𝐷)) = (𝐴 + ((𝑚 + 1) · 𝐷)))
118117eqeq2d 2829 . . . . . . . . . . . 12 (𝑛 = (𝑚 + 1) → (((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)) ↔ ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + ((𝑚 + 1) · 𝐷))))
119115, 118anbi12d 630 . . . . . . . . . . 11 (𝑛 = (𝑚 + 1) → ((𝑛 ∈ ((0 + 1)...𝐾) ∧ ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))) ↔ ((𝑚 + 1) ∈ ((0 + 1)...𝐾) ∧ ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + ((𝑚 + 1) · 𝐷)))))
120114, 119spcev 3604 . . . . . . . . . 10 (((𝑚 + 1) ∈ ((0 + 1)...𝐾) ∧ ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + ((𝑚 + 1) · 𝐷))) → ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
12199, 113, 120syl2anc 584 . . . . . . . . 9 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
122 eqeq1 2822 . . . . . . . . . . 11 (𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷)) → (𝑥 = (𝐴 + (𝑛 · 𝐷)) ↔ ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
123122anbi2d 628 . . . . . . . . . 10 (𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷)) → ((𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ↔ (𝑛 ∈ ((0 + 1)...𝐾) ∧ ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))))
124123exbidv 1913 . . . . . . . . 9 (𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷)) → (∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ↔ ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))))
125121, 124syl5ibrcom 248 . . . . . . . 8 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷)) → ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷)))))
126125rexlimdva 3281 . . . . . . 7 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷)) → ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷)))))
12782, 126impbid 213 . . . . . 6 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷))))
128 nnaddcl 11648 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴 + 𝐷) ∈ ℕ)
1291283adant1 1122 . . . . . . 7 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴 + 𝐷) ∈ ℕ)
130 vdwapval 16297 . . . . . . 7 ((𝐾 ∈ ℕ0 ∧ (𝐴 + 𝐷) ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑥 ∈ ((𝐴 + 𝐷)(AP‘𝐾)𝐷) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷))))
131129, 130syld3an2 1403 . . . . . 6 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑥 ∈ ((𝐴 + 𝐷)(AP‘𝐾)𝐷) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷))))
132127, 131bitr4d 283 . . . . 5 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ↔ 𝑥 ∈ ((𝐴 + 𝐷)(AP‘𝐾)𝐷)))
13340, 132orbi12d 912 . . . 4 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → ((∃𝑛(𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷)))) ↔ (𝑥 ∈ {𝐴} ∨ 𝑥 ∈ ((𝐴 + 𝐷)(AP‘𝐾)𝐷))))
134 elun 4122 . . . 4 (𝑥 ∈ ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘𝐾)𝐷)) ↔ (𝑥 ∈ {𝐴} ∨ 𝑥 ∈ ((𝐴 + 𝐷)(AP‘𝐾)𝐷)))
135133, 134syl6bbr 290 . . 3 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → ((∃𝑛(𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷)))) ↔ 𝑥 ∈ ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘𝐾)𝐷))))
13624, 135bitrd 280 . 2 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑥 ∈ (𝐴(AP‘(𝐾 + 1))𝐷) ↔ 𝑥 ∈ ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘𝐾)𝐷))))
137136eqrdv 2816 1 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴(AP‘(𝐾 + 1))𝐷) = ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘𝐾)𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wo 841  w3a 1079   = wceq 1528  wex 1771  wcel 2105  wrex 3136  cun 3931  {csn 4557  cfv 6348  (class class class)co 7145  cc 10523  0cc0 10525  1c1 10526   + caddc 10528   · cmul 10530  cmin 10858  cn 11626  0cn0 11885  cz 11969  cuz 12231  ...cfz 12880  APcvdwa 16289
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-nn 11627  df-n0 11886  df-z 11970  df-uz 12232  df-fz 12881  df-vdwap 16292
This theorem is referenced by:  vdwapid1  16299  vdwap1  16301  vdwlem1  16305  vdwlem5  16309  vdwlem8  16312  vdwlem12  16316
  Copyright terms: Public domain W3C validator