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

Theorem vdwapun 15725
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 11371 . . . . 5 (𝐾 ∈ ℕ0 → (𝐾 + 1) ∈ ℕ0)
2 vdwapval 15724 . . . . 5 (((𝐾 + 1) ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑥 ∈ (𝐴(AP‘(𝐾 + 1))𝐷) ↔ ∃𝑛 ∈ (0...((𝐾 + 1) − 1))𝑥 = (𝐴 + (𝑛 · 𝐷))))
31, 2syl3an1 1399 . . . 4 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑥 ∈ (𝐴(AP‘(𝐾 + 1))𝐷) ↔ ∃𝑛 ∈ (0...((𝐾 + 1) − 1))𝑥 = (𝐴 + (𝑛 · 𝐷))))
4 simp1 1081 . . . . . . . . . . . . 13 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐾 ∈ ℕ0)
54nn0cnd 11391 . . . . . . . . . . . 12 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐾 ∈ ℂ)
6 ax-1cn 10032 . . . . . . . . . . . 12 1 ∈ ℂ
7 pncan 10325 . . . . . . . . . . . 12 ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 + 1) − 1) = 𝐾)
85, 6, 7sylancl 695 . . . . . . . . . . 11 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → ((𝐾 + 1) − 1) = 𝐾)
98oveq2d 6706 . . . . . . . . . 10 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (0...((𝐾 + 1) − 1)) = (0...𝐾))
109eleq2d 2716 . . . . . . . . 9 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑛 ∈ (0...((𝐾 + 1) − 1)) ↔ 𝑛 ∈ (0...𝐾)))
11 nn0uz 11760 . . . . . . . . . . 11 0 = (ℤ‘0)
124, 11syl6eleq 2740 . . . . . . . . . 10 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐾 ∈ (ℤ‘0))
13 elfzp12 12457 . . . . . . . . . 10 (𝐾 ∈ (ℤ‘0) → (𝑛 ∈ (0...𝐾) ↔ (𝑛 = 0 ∨ 𝑛 ∈ ((0 + 1)...𝐾))))
1412, 13syl 17 . . . . . . . . 9 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑛 ∈ (0...𝐾) ↔ (𝑛 = 0 ∨ 𝑛 ∈ ((0 + 1)...𝐾))))
1510, 14bitrd 268 . . . . . . . 8 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑛 ∈ (0...((𝐾 + 1) − 1)) ↔ (𝑛 = 0 ∨ 𝑛 ∈ ((0 + 1)...𝐾))))
1615anbi1d 741 . . . . . . 7 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → ((𝑛 ∈ (0...((𝐾 + 1) − 1)) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ↔ ((𝑛 = 0 ∨ 𝑛 ∈ ((0 + 1)...𝐾)) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷)))))
17 andir 930 . . . . . . 7 (((𝑛 = 0 ∨ 𝑛 ∈ ((0 + 1)...𝐾)) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ↔ ((𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ (𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷)))))
1816, 17syl6bb 276 . . . . . 6 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → ((𝑛 ∈ (0...((𝐾 + 1) − 1)) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ↔ ((𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ (𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))))))
1918exbidv 1890 . . . . 5 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (∃𝑛(𝑛 ∈ (0...((𝐾 + 1) − 1)) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ↔ ∃𝑛((𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ (𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))))))
20 df-rex 2947 . . . . 5 (∃𝑛 ∈ (0...((𝐾 + 1) − 1))𝑥 = (𝐴 + (𝑛 · 𝐷)) ↔ ∃𝑛(𝑛 ∈ (0...((𝐾 + 1) − 1)) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))))
21 19.43 1850 . . . . . 6 (∃𝑛((𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ (𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷)))) ↔ (∃𝑛(𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷)))))
2221bicomi 214 . . . . 5 ((∃𝑛(𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷)))) ↔ ∃𝑛((𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ (𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷)))))
2319, 20, 223bitr4g 303 . . . 4 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (∃𝑛 ∈ (0...((𝐾 + 1) − 1))𝑥 = (𝐴 + (𝑛 · 𝐷)) ↔ (∃𝑛(𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))))))
243, 23bitrd 268 . . 3 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑥 ∈ (𝐴(AP‘(𝐾 + 1))𝐷) ↔ (∃𝑛(𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))))))
25 nncn 11066 . . . . . . . . . . 11 (𝐷 ∈ ℕ → 𝐷 ∈ ℂ)
26253ad2ant3 1104 . . . . . . . . . 10 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐷 ∈ ℂ)
2726mul02d 10272 . . . . . . . . 9 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (0 · 𝐷) = 0)
2827oveq2d 6706 . . . . . . . 8 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴 + (0 · 𝐷)) = (𝐴 + 0))
29 nncn 11066 . . . . . . . . . 10 (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
30293ad2ant2 1103 . . . . . . . . 9 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐴 ∈ ℂ)
3130addid1d 10274 . . . . . . . 8 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴 + 0) = 𝐴)
3228, 31eqtrd 2685 . . . . . . 7 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴 + (0 · 𝐷)) = 𝐴)
3332eqeq2d 2661 . . . . . 6 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑥 = (𝐴 + (0 · 𝐷)) ↔ 𝑥 = 𝐴))
34 c0ex 10072 . . . . . . 7 0 ∈ V
35 oveq1 6697 . . . . . . . . 9 (𝑛 = 0 → (𝑛 · 𝐷) = (0 · 𝐷))
3635oveq2d 6706 . . . . . . . 8 (𝑛 = 0 → (𝐴 + (𝑛 · 𝐷)) = (𝐴 + (0 · 𝐷)))
3736eqeq2d 2661 . . . . . . 7 (𝑛 = 0 → (𝑥 = (𝐴 + (𝑛 · 𝐷)) ↔ 𝑥 = (𝐴 + (0 · 𝐷))))
3834, 37ceqsexv 3273 . . . . . 6 (∃𝑛(𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ↔ 𝑥 = (𝐴 + (0 · 𝐷)))
39 velsn 4226 . . . . . 6 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
4033, 38, 393bitr4g 303 . . . . 5 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (∃𝑛(𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ↔ 𝑥 ∈ {𝐴}))
41 simpr 476 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → 𝑛 ∈ ((0 + 1)...𝐾))
42 0p1e1 11170 . . . . . . . . . . . . . . 15 (0 + 1) = 1
4342oveq1i 6700 . . . . . . . . . . . . . 14 ((0 + 1)...𝐾) = (1...𝐾)
4441, 43syl6eleq 2740 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → 𝑛 ∈ (1...𝐾))
45 1zzd 11446 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → 1 ∈ ℤ)
464adantr 480 . . . . . . . . . . . . . . 15 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → 𝐾 ∈ ℕ0)
4746nn0zd 11518 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → 𝐾 ∈ ℤ)
48 elfzelz 12380 . . . . . . . . . . . . . . 15 (𝑛 ∈ ((0 + 1)...𝐾) → 𝑛 ∈ ℤ)
4948adantl 481 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → 𝑛 ∈ ℤ)
50 fzsubel 12415 . . . . . . . . . . . . . 14 (((1 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑛 ∈ (1...𝐾) ↔ (𝑛 − 1) ∈ ((1 − 1)...(𝐾 − 1))))
5145, 47, 49, 45, 50syl22anc 1367 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝑛 ∈ (1...𝐾) ↔ (𝑛 − 1) ∈ ((1 − 1)...(𝐾 − 1))))
5244, 51mpbid 222 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝑛 − 1) ∈ ((1 − 1)...(𝐾 − 1)))
53 1m1e0 11127 . . . . . . . . . . . . 13 (1 − 1) = 0
5453oveq1i 6700 . . . . . . . . . . . 12 ((1 − 1)...(𝐾 − 1)) = (0...(𝐾 − 1))
5552, 54syl6eleq 2740 . . . . . . . . . . 11 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝑛 − 1) ∈ (0...(𝐾 − 1)))
5649zcnd 11521 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → 𝑛 ∈ ℂ)
57 1cnd 10094 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → 1 ∈ ℂ)
5826adantr 480 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → 𝐷 ∈ ℂ)
5956, 57, 58subdird 10525 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → ((𝑛 − 1) · 𝐷) = ((𝑛 · 𝐷) − (1 · 𝐷)))
6058mulid2d 10096 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (1 · 𝐷) = 𝐷)
6160oveq2d 6706 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → ((𝑛 · 𝐷) − (1 · 𝐷)) = ((𝑛 · 𝐷) − 𝐷))
6259, 61eqtrd 2685 . . . . . . . . . . . . . . 15 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → ((𝑛 − 1) · 𝐷) = ((𝑛 · 𝐷) − 𝐷))
6362oveq2d 6706 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝐷 + ((𝑛 − 1) · 𝐷)) = (𝐷 + ((𝑛 · 𝐷) − 𝐷)))
6456, 58mulcld 10098 . . . . . . . . . . . . . . 15 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝑛 · 𝐷) ∈ ℂ)
6558, 64pncan3d 10433 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝐷 + ((𝑛 · 𝐷) − 𝐷)) = (𝑛 · 𝐷))
6663, 65eqtr2d 2686 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝑛 · 𝐷) = (𝐷 + ((𝑛 − 1) · 𝐷)))
6766oveq2d 6706 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝐴 + (𝑛 · 𝐷)) = (𝐴 + (𝐷 + ((𝑛 − 1) · 𝐷))))
6830adantr 480 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → 𝐴 ∈ ℂ)
69 subcl 10318 . . . . . . . . . . . . . . 15 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑛 − 1) ∈ ℂ)
7056, 6, 69sylancl 695 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝑛 − 1) ∈ ℂ)
7170, 58mulcld 10098 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → ((𝑛 − 1) · 𝐷) ∈ ℂ)
7268, 58, 71addassd 10100 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → ((𝐴 + 𝐷) + ((𝑛 − 1) · 𝐷)) = (𝐴 + (𝐷 + ((𝑛 − 1) · 𝐷))))
7367, 72eqtr4d 2688 . . . . . . . . . . 11 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝐴 + (𝑛 · 𝐷)) = ((𝐴 + 𝐷) + ((𝑛 − 1) · 𝐷)))
74 oveq1 6697 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 − 1) → (𝑚 · 𝐷) = ((𝑛 − 1) · 𝐷))
7574oveq2d 6706 . . . . . . . . . . . . 13 (𝑚 = (𝑛 − 1) → ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = ((𝐴 + 𝐷) + ((𝑛 − 1) · 𝐷)))
7675eqeq2d 2661 . . . . . . . . . . . 12 (𝑚 = (𝑛 − 1) → ((𝐴 + (𝑛 · 𝐷)) = ((𝐴 + 𝐷) + (𝑚 · 𝐷)) ↔ (𝐴 + (𝑛 · 𝐷)) = ((𝐴 + 𝐷) + ((𝑛 − 1) · 𝐷))))
7776rspcev 3340 . . . . . . . . . . 11 (((𝑛 − 1) ∈ (0...(𝐾 − 1)) ∧ (𝐴 + (𝑛 · 𝐷)) = ((𝐴 + 𝐷) + ((𝑛 − 1) · 𝐷))) → ∃𝑚 ∈ (0...(𝐾 − 1))(𝐴 + (𝑛 · 𝐷)) = ((𝐴 + 𝐷) + (𝑚 · 𝐷)))
7855, 73, 77syl2anc 694 . . . . . . . . . 10 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → ∃𝑚 ∈ (0...(𝐾 − 1))(𝐴 + (𝑛 · 𝐷)) = ((𝐴 + 𝐷) + (𝑚 · 𝐷)))
79 eqeq1 2655 . . . . . . . . . . 11 (𝑥 = (𝐴 + (𝑛 · 𝐷)) → (𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷)) ↔ (𝐴 + (𝑛 · 𝐷)) = ((𝐴 + 𝐷) + (𝑚 · 𝐷))))
8079rexbidv 3081 . . . . . . . . . 10 (𝑥 = (𝐴 + (𝑛 · 𝐷)) → (∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))(𝐴 + (𝑛 · 𝐷)) = ((𝐴 + 𝐷) + (𝑚 · 𝐷))))
8178, 80syl5ibrcom 237 . . . . . . . . 9 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑛 ∈ ((0 + 1)...𝐾)) → (𝑥 = (𝐴 + (𝑛 · 𝐷)) → ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷))))
8281expimpd 628 . . . . . . . 8 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → ((𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) → ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷))))
8382exlimdv 1901 . . . . . . 7 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) → ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷))))
84 simpr 476 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ (0...(𝐾 − 1)))
85 0zd 11427 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 0 ∈ ℤ)
864adantr 480 . . . . . . . . . . . . . . 15 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐾 ∈ ℕ0)
8786nn0zd 11518 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐾 ∈ ℤ)
88 peano2zm 11458 . . . . . . . . . . . . . 14 (𝐾 ∈ ℤ → (𝐾 − 1) ∈ ℤ)
8987, 88syl 17 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐾 − 1) ∈ ℤ)
90 elfzelz 12380 . . . . . . . . . . . . . 14 (𝑚 ∈ (0...(𝐾 − 1)) → 𝑚 ∈ ℤ)
9190adantl 481 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℤ)
92 1zzd 11446 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 1 ∈ ℤ)
93 fzaddel 12413 . . . . . . . . . . . . 13 (((0 ∈ ℤ ∧ (𝐾 − 1) ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑚 ∈ (0...(𝐾 − 1)) ↔ (𝑚 + 1) ∈ ((0 + 1)...((𝐾 − 1) + 1))))
9485, 89, 91, 92, 93syl22anc 1367 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 ∈ (0...(𝐾 − 1)) ↔ (𝑚 + 1) ∈ ((0 + 1)...((𝐾 − 1) + 1))))
9584, 94mpbid 222 . . . . . . . . . . 11 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 + 1) ∈ ((0 + 1)...((𝐾 − 1) + 1)))
9686nn0cnd 11391 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐾 ∈ ℂ)
97 npcan 10328 . . . . . . . . . . . . 13 ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 − 1) + 1) = 𝐾)
9896, 6, 97sylancl 695 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐾 − 1) + 1) = 𝐾)
9998oveq2d 6706 . . . . . . . . . . 11 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((0 + 1)...((𝐾 − 1) + 1)) = ((0 + 1)...𝐾))
10095, 99eleqtrd 2732 . . . . . . . . . 10 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 + 1) ∈ ((0 + 1)...𝐾))
10130adantr 480 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐴 ∈ ℂ)
10226adantr 480 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐷 ∈ ℂ)
10391zcnd 11521 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ)
104103, 102mulcld 10098 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · 𝐷) ∈ ℂ)
105101, 102, 104addassd 10100 . . . . . . . . . . 11 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + (𝐷 + (𝑚 · 𝐷))))
106 1cnd 10094 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 1 ∈ ℂ)
107103, 106, 102adddird 10103 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑚 + 1) · 𝐷) = ((𝑚 · 𝐷) + (1 · 𝐷)))
108102, 104addcomd 10276 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐷 + (𝑚 · 𝐷)) = ((𝑚 · 𝐷) + 𝐷))
109102mulid2d 10096 . . . . . . . . . . . . . . 15 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (1 · 𝐷) = 𝐷)
110109oveq2d 6706 . . . . . . . . . . . . . 14 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑚 · 𝐷) + (1 · 𝐷)) = ((𝑚 · 𝐷) + 𝐷))
111108, 110eqtr4d 2688 . . . . . . . . . . . . 13 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐷 + (𝑚 · 𝐷)) = ((𝑚 · 𝐷) + (1 · 𝐷)))
112107, 111eqtr4d 2688 . . . . . . . . . . . 12 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑚 + 1) · 𝐷) = (𝐷 + (𝑚 · 𝐷)))
113112oveq2d 6706 . . . . . . . . . . 11 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + ((𝑚 + 1) · 𝐷)) = (𝐴 + (𝐷 + (𝑚 · 𝐷))))
114105, 113eqtr4d 2688 . . . . . . . . . 10 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + ((𝑚 + 1) · 𝐷)))
115 ovex 6718 . . . . . . . . . . 11 (𝑚 + 1) ∈ V
116 eleq1 2718 . . . . . . . . . . . 12 (𝑛 = (𝑚 + 1) → (𝑛 ∈ ((0 + 1)...𝐾) ↔ (𝑚 + 1) ∈ ((0 + 1)...𝐾)))
117 oveq1 6697 . . . . . . . . . . . . . 14 (𝑛 = (𝑚 + 1) → (𝑛 · 𝐷) = ((𝑚 + 1) · 𝐷))
118117oveq2d 6706 . . . . . . . . . . . . 13 (𝑛 = (𝑚 + 1) → (𝐴 + (𝑛 · 𝐷)) = (𝐴 + ((𝑚 + 1) · 𝐷)))
119118eqeq2d 2661 . . . . . . . . . . . 12 (𝑛 = (𝑚 + 1) → (((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)) ↔ ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + ((𝑚 + 1) · 𝐷))))
120116, 119anbi12d 747 . . . . . . . . . . 11 (𝑛 = (𝑚 + 1) → ((𝑛 ∈ ((0 + 1)...𝐾) ∧ ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))) ↔ ((𝑚 + 1) ∈ ((0 + 1)...𝐾) ∧ ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + ((𝑚 + 1) · 𝐷)))))
121115, 120spcev 3331 . . . . . . . . . 10 (((𝑚 + 1) ∈ ((0 + 1)...𝐾) ∧ ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + ((𝑚 + 1) · 𝐷))) → ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
122100, 114, 121syl2anc 694 . . . . . . . . 9 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
123 eqeq1 2655 . . . . . . . . . . 11 (𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷)) → (𝑥 = (𝐴 + (𝑛 · 𝐷)) ↔ ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
124123anbi2d 740 . . . . . . . . . 10 (𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷)) → ((𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ↔ (𝑛 ∈ ((0 + 1)...𝐾) ∧ ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))))
125124exbidv 1890 . . . . . . . . 9 (𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷)) → (∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ↔ ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ ((𝐴 + 𝐷) + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))))
126122, 125syl5ibrcom 237 . . . . . . . 8 (((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷)) → ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷)))))
127126rexlimdva 3060 . . . . . . 7 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷)) → ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷)))))
12883, 127impbid 202 . . . . . 6 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷))))
129 nnaddcl 11080 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴 + 𝐷) ∈ ℕ)
1301293adant1 1099 . . . . . . 7 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴 + 𝐷) ∈ ℕ)
131 vdwapval 15724 . . . . . . 7 ((𝐾 ∈ ℕ0 ∧ (𝐴 + 𝐷) ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑥 ∈ ((𝐴 + 𝐷)(AP‘𝐾)𝐷) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷))))
132130, 131syld3an2 1413 . . . . . 6 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑥 ∈ ((𝐴 + 𝐷)(AP‘𝐾)𝐷) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝐴 + 𝐷) + (𝑚 · 𝐷))))
133128, 132bitr4d 271 . . . . 5 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ↔ 𝑥 ∈ ((𝐴 + 𝐷)(AP‘𝐾)𝐷)))
13440, 133orbi12d 746 . . . 4 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → ((∃𝑛(𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷)))) ↔ (𝑥 ∈ {𝐴} ∨ 𝑥 ∈ ((𝐴 + 𝐷)(AP‘𝐾)𝐷))))
135 elun 3786 . . . 4 (𝑥 ∈ ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘𝐾)𝐷)) ↔ (𝑥 ∈ {𝐴} ∨ 𝑥 ∈ ((𝐴 + 𝐷)(AP‘𝐾)𝐷)))
136134, 135syl6bbr 278 . . 3 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → ((∃𝑛(𝑛 = 0 ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷))) ∨ ∃𝑛(𝑛 ∈ ((0 + 1)...𝐾) ∧ 𝑥 = (𝐴 + (𝑛 · 𝐷)))) ↔ 𝑥 ∈ ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘𝐾)𝐷))))
13724, 136bitrd 268 . 2 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑥 ∈ (𝐴(AP‘(𝐾 + 1))𝐷) ↔ 𝑥 ∈ ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘𝐾)𝐷))))
138137eqrdv 2649 1 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴(AP‘(𝐾 + 1))𝐷) = ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘𝐾)𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382  wa 383  w3a 1054   = wceq 1523  wex 1744  wcel 2030  wrex 2942  cun 3605  {csn 4210  cfv 5926  (class class class)co 6690  cc 9972  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  cmin 10304  cn 11058  0cn0 11330  cz 11415  cuz 11725  ...cfz 12364  APcvdwa 15716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-vdwap 15719
This theorem is referenced by:  vdwapid1  15726  vdwap1  15728  vdwlem1  15732  vdwlem5  15736  vdwlem8  15739  vdwlem12  15743
  Copyright terms: Public domain W3C validator