Metamath Proof Explorer

Theorem vdwapun

Description: Remove the first element of an arithmetic progression. (Contributed by Mario Carneiro, 11-Sep-2014)

Ref Expression
Assertion vdwapun ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 ( AP ‘ ( 𝐾 + 1 ) ) 𝐷 ) = ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ 𝐾 ) 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 peano2nn0 ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 + 1 ) ∈ ℕ0 )
2 vdwapval ⊢ ( ( ( 𝐾 + 1 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝑥 ∈ ( 𝐴 ( AP ‘ ( 𝐾 + 1 ) ) 𝐷 ) ↔ ∃ 𝑛 ∈ ( 0 ... ( ( 𝐾 + 1 ) − 1 ) ) 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) )
3 1 2 syl3an1 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝑥 ∈ ( 𝐴 ( AP ‘ ( 𝐾 + 1 ) ) 𝐷 ) ↔ ∃ 𝑛 ∈ ( 0 ... ( ( 𝐾 + 1 ) − 1 ) ) 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) )
4 simp1 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → 𝐾 ∈ ℕ0 )
5 4 nn0cnd ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → 𝐾 ∈ ℂ )
6 ax-1cn ⊢ 1 ∈ ℂ
7 pncan ⊢ ( ( 𝐾 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐾 + 1 ) − 1 ) = 𝐾 )
8 5 6 7 sylancl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( ( 𝐾 + 1 ) − 1 ) = 𝐾 )
9 8 oveq2d ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 0 ... ( ( 𝐾 + 1 ) − 1 ) ) = ( 0 ... 𝐾 ) )
10 9 eleq2d ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝑛 ∈ ( 0 ... ( ( 𝐾 + 1 ) − 1 ) ) ↔ 𝑛 ∈ ( 0 ... 𝐾 ) ) )
11 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
12 4 11 eleqtrdi ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → 𝐾 ∈ ( ℤ≥ ‘ 0 ) )
13 elfzp12 ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 0 ) → ( 𝑛 ∈ ( 0 ... 𝐾 ) ↔ ( 𝑛 = 0 ∨ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) ) )
14 12 13 syl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝑛 ∈ ( 0 ... 𝐾 ) ↔ ( 𝑛 = 0 ∨ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) ) )
15 10 14 bitrd ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝑛 ∈ ( 0 ... ( ( 𝐾 + 1 ) − 1 ) ) ↔ ( 𝑛 = 0 ∨ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) ) )
16 15 anbi1d ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( ( 𝑛 ∈ ( 0 ... ( ( 𝐾 + 1 ) − 1 ) ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ↔ ( ( 𝑛 = 0 ∨ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ) )
17 andir ⊢ ( ( ( 𝑛 = 0 ∨ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ↔ ( ( 𝑛 = 0 ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ∨ ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ) )
18 16 17 bitrdi ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( ( 𝑛 ∈ ( 0 ... ( ( 𝐾 + 1 ) − 1 ) ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ↔ ( ( 𝑛 = 0 ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ∨ ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ) ) )
19 18 exbidv ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( ∃ 𝑛 ( 𝑛 ∈ ( 0 ... ( ( 𝐾 + 1 ) − 1 ) ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ↔ ∃ 𝑛 ( ( 𝑛 = 0 ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ∨ ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ) ) )
20 df-rex ⊢ ( ∃ 𝑛 ∈ ( 0 ... ( ( 𝐾 + 1 ) − 1 ) ) 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ↔ ∃ 𝑛 ( 𝑛 ∈ ( 0 ... ( ( 𝐾 + 1 ) − 1 ) ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) )
21 19.43 ⊢ ( ∃ 𝑛 ( ( 𝑛 = 0 ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ∨ ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ) ↔ ( ∃ 𝑛 ( 𝑛 = 0 ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ∨ ∃ 𝑛 ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ) )
22 21 bicomi ⊢ ( ( ∃ 𝑛 ( 𝑛 = 0 ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ∨ ∃ 𝑛 ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ) ↔ ∃ 𝑛 ( ( 𝑛 = 0 ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ∨ ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ) )
23 19 20 22 3bitr4g ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( ∃ 𝑛 ∈ ( 0 ... ( ( 𝐾 + 1 ) − 1 ) ) 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ↔ ( ∃ 𝑛 ( 𝑛 = 0 ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ∨ ∃ 𝑛 ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ) ) )
24 3 23 bitrd ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝑥 ∈ ( 𝐴 ( AP ‘ ( 𝐾 + 1 ) ) 𝐷 ) ↔ ( ∃ 𝑛 ( 𝑛 = 0 ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ∨ ∃ 𝑛 ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ) ) )
25 nncn ⊢ ( 𝐷 ∈ ℕ → 𝐷 ∈ ℂ )
26 25 3ad2ant3 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → 𝐷 ∈ ℂ )
27 26 mul02d ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 0 · 𝐷 ) = 0 )
28 27 oveq2d ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 + ( 0 · 𝐷 ) ) = ( 𝐴 + 0 ) )
29 nncn ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
30 29 3ad2ant2 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → 𝐴 ∈ ℂ )
31 30 addridd ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 + 0 ) = 𝐴 )
32 28 31 eqtrd ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 + ( 0 · 𝐷 ) ) = 𝐴 )
33 32 eqeq2d ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝑥 = ( 𝐴 + ( 0 · 𝐷 ) ) ↔ 𝑥 = 𝐴 ) )
34 c0ex ⊢ 0 ∈ V
35 oveq1 ⊢ ( 𝑛 = 0 → ( 𝑛 · 𝐷 ) = ( 0 · 𝐷 ) )
36 35 oveq2d ⊢ ( 𝑛 = 0 → ( 𝐴 + ( 𝑛 · 𝐷 ) ) = ( 𝐴 + ( 0 · 𝐷 ) ) )
37 36 eqeq2d ⊢ ( 𝑛 = 0 → ( 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ↔ 𝑥 = ( 𝐴 + ( 0 · 𝐷 ) ) ) )
38 34 37 ceqsexv ⊢ ( ∃ 𝑛 ( 𝑛 = 0 ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ↔ 𝑥 = ( 𝐴 + ( 0 · 𝐷 ) ) )
39 velsn ⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
40 33 38 39 3bitr4g ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( ∃ 𝑛 ( 𝑛 = 0 ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ↔ 𝑥 ∈ { 𝐴 } ) )
41 simpr ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) )
42 0p1e1 ⊢ ( 0 + 1 ) = 1
43 42 oveq1i ⊢ ( ( 0 + 1 ) ... 𝐾 ) = ( 1 ... 𝐾 )
44 41 43 eleqtrdi ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → 𝑛 ∈ ( 1 ... 𝐾 ) )
45 1zzd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → 1 ∈ ℤ )
46 4 adantr ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → 𝐾 ∈ ℕ0 )
47 46 nn0zd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → 𝐾 ∈ ℤ )
48 elfzelz ⊢ ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) → 𝑛 ∈ ℤ )
49 48 adantl ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → 𝑛 ∈ ℤ )
50 fzsubel ⊢ ( ( ( 1 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝑛 ∈ ( 1 ... 𝐾 ) ↔ ( 𝑛 − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝐾 − 1 ) ) ) )
51 45 47 49 45 50 syl22anc ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → ( 𝑛 ∈ ( 1 ... 𝐾 ) ↔ ( 𝑛 − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝐾 − 1 ) ) ) )
52 44 51 mpbid ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → ( 𝑛 − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝐾 − 1 ) ) )
53 1m1e0 ⊢ ( 1 − 1 ) = 0
54 53 oveq1i ⊢ ( ( 1 − 1 ) ... ( 𝐾 − 1 ) ) = ( 0 ... ( 𝐾 − 1 ) )
55 52 54 eleqtrdi ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → ( 𝑛 − 1 ) ∈ ( 0 ... ( 𝐾 − 1 ) ) )
56 49 zcnd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → 𝑛 ∈ ℂ )
57 1cnd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → 1 ∈ ℂ )
58 26 adantr ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → 𝐷 ∈ ℂ )
59 56 57 58 subdird ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → ( ( 𝑛 − 1 ) · 𝐷 ) = ( ( 𝑛 · 𝐷 ) − ( 1 · 𝐷 ) ) )
60 58 mullidd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → ( 1 · 𝐷 ) = 𝐷 )
61 60 oveq2d ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → ( ( 𝑛 · 𝐷 ) − ( 1 · 𝐷 ) ) = ( ( 𝑛 · 𝐷 ) − 𝐷 ) )
62 59 61 eqtrd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → ( ( 𝑛 − 1 ) · 𝐷 ) = ( ( 𝑛 · 𝐷 ) − 𝐷 ) )
63 62 oveq2d ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → ( 𝐷 + ( ( 𝑛 − 1 ) · 𝐷 ) ) = ( 𝐷 + ( ( 𝑛 · 𝐷 ) − 𝐷 ) ) )
64 56 58 mulcld ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → ( 𝑛 · 𝐷 ) ∈ ℂ )
65 58 64 pncan3d ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → ( 𝐷 + ( ( 𝑛 · 𝐷 ) − 𝐷 ) ) = ( 𝑛 · 𝐷 ) )
66 63 65 eqtr2d ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → ( 𝑛 · 𝐷 ) = ( 𝐷 + ( ( 𝑛 − 1 ) · 𝐷 ) ) )
67 66 oveq2d ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → ( 𝐴 + ( 𝑛 · 𝐷 ) ) = ( 𝐴 + ( 𝐷 + ( ( 𝑛 − 1 ) · 𝐷 ) ) ) )
68 30 adantr ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → 𝐴 ∈ ℂ )
69 subcl ⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑛 − 1 ) ∈ ℂ )
70 56 6 69 sylancl ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → ( 𝑛 − 1 ) ∈ ℂ )
71 70 58 mulcld ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → ( ( 𝑛 − 1 ) · 𝐷 ) ∈ ℂ )
72 68 58 71 addassd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → ( ( 𝐴 + 𝐷 ) + ( ( 𝑛 − 1 ) · 𝐷 ) ) = ( 𝐴 + ( 𝐷 + ( ( 𝑛 − 1 ) · 𝐷 ) ) ) )
73 67 72 eqtr4d ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → ( 𝐴 + ( 𝑛 · 𝐷 ) ) = ( ( 𝐴 + 𝐷 ) + ( ( 𝑛 − 1 ) · 𝐷 ) ) )
74 oveq1 ⊢ ( 𝑚 = ( 𝑛 − 1 ) → ( 𝑚 · 𝐷 ) = ( ( 𝑛 − 1 ) · 𝐷 ) )
75 74 oveq2d ⊢ ( 𝑚 = ( 𝑛 − 1 ) → ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) = ( ( 𝐴 + 𝐷 ) + ( ( 𝑛 − 1 ) · 𝐷 ) ) )
76 75 rspceeqv ⊢ ( ( ( 𝑛 − 1 ) ∈ ( 0 ... ( 𝐾 − 1 ) ) ∧ ( 𝐴 + ( 𝑛 · 𝐷 ) ) = ( ( 𝐴 + 𝐷 ) + ( ( 𝑛 − 1 ) · 𝐷 ) ) ) → ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐴 + ( 𝑛 · 𝐷 ) ) = ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) )
77 55 73 76 syl2anc ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐴 + ( 𝑛 · 𝐷 ) ) = ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) )
78 eqeq1 ⊢ ( 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) → ( 𝑥 = ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) ↔ ( 𝐴 + ( 𝑛 · 𝐷 ) ) = ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) ) )
79 78 rexbidv ⊢ ( 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) → ( ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) ↔ ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐴 + ( 𝑛 · 𝐷 ) ) = ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) ) )
80 77 79 syl5ibrcom ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ) → ( 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) → ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) ) )
81 80 expimpd ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) → ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) ) )
82 81 exlimdv ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( ∃ 𝑛 ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) → ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) ) )
83 simpr ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) )
84 0zd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 0 ∈ ℤ )
85 4 adantr ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝐾 ∈ ℕ0 )
86 85 nn0zd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝐾 ∈ ℤ )
87 peano2zm ⊢ ( 𝐾 ∈ ℤ → ( 𝐾 − 1 ) ∈ ℤ )
88 86 87 syl ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝐾 − 1 ) ∈ ℤ )
89 elfzelz ⊢ ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) → 𝑚 ∈ ℤ )
90 89 adantl ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝑚 ∈ ℤ )
91 1zzd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 1 ∈ ℤ )
92 fzaddel ⊢ ( ( ( 0 ∈ ℤ ∧ ( 𝐾 − 1 ) ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↔ ( 𝑚 + 1 ) ∈ ( ( 0 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ) )
93 84 88 90 91 92 syl22anc ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↔ ( 𝑚 + 1 ) ∈ ( ( 0 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ) )
94 83 93 mpbid ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝑚 + 1 ) ∈ ( ( 0 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) )
95 85 nn0cnd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝐾 ∈ ℂ )
96 npcan ⊢ ( ( 𝐾 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
97 95 6 96 sylancl ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
98 97 oveq2d ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( ( 0 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) = ( ( 0 + 1 ) ... 𝐾 ) )
99 94 98 eleqtrd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝑚 + 1 ) ∈ ( ( 0 + 1 ) ... 𝐾 ) )
100 30 adantr ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝐴 ∈ ℂ )
101 26 adantr ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝐷 ∈ ℂ )
102 90 zcnd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝑚 ∈ ℂ )
103 102 101 mulcld ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝑚 · 𝐷 ) ∈ ℂ )
104 100 101 103 addassd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) = ( 𝐴 + ( 𝐷 + ( 𝑚 · 𝐷 ) ) ) )
105 1cnd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 1 ∈ ℂ )
106 102 105 101 adddird ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( ( 𝑚 + 1 ) · 𝐷 ) = ( ( 𝑚 · 𝐷 ) + ( 1 · 𝐷 ) ) )
107 101 103 addcomd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝐷 + ( 𝑚 · 𝐷 ) ) = ( ( 𝑚 · 𝐷 ) + 𝐷 ) )
108 101 mullidd ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 1 · 𝐷 ) = 𝐷 )
109 108 oveq2d ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( ( 𝑚 · 𝐷 ) + ( 1 · 𝐷 ) ) = ( ( 𝑚 · 𝐷 ) + 𝐷 ) )
110 107 109 eqtr4d ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝐷 + ( 𝑚 · 𝐷 ) ) = ( ( 𝑚 · 𝐷 ) + ( 1 · 𝐷 ) ) )
111 106 110 eqtr4d ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( ( 𝑚 + 1 ) · 𝐷 ) = ( 𝐷 + ( 𝑚 · 𝐷 ) ) )
112 111 oveq2d ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝐴 + ( ( 𝑚 + 1 ) · 𝐷 ) ) = ( 𝐴 + ( 𝐷 + ( 𝑚 · 𝐷 ) ) ) )
113 104 112 eqtr4d ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) = ( 𝐴 + ( ( 𝑚 + 1 ) · 𝐷 ) ) )
114 ovex ⊢ ( 𝑚 + 1 ) ∈ V
115 eleq1 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ↔ ( 𝑚 + 1 ) ∈ ( ( 0 + 1 ) ... 𝐾 ) ) )
116 oveq1 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑛 · 𝐷 ) = ( ( 𝑚 + 1 ) · 𝐷 ) )
117 116 oveq2d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝐴 + ( 𝑛 · 𝐷 ) ) = ( 𝐴 + ( ( 𝑚 + 1 ) · 𝐷 ) ) )
118 117 eqeq2d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ↔ ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) = ( 𝐴 + ( ( 𝑚 + 1 ) · 𝐷 ) ) ) )
119 115 118 anbi12d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ↔ ( ( 𝑚 + 1 ) ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) = ( 𝐴 + ( ( 𝑚 + 1 ) · 𝐷 ) ) ) ) )
120 114 119 spcev ⊢ ( ( ( 𝑚 + 1 ) ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) = ( 𝐴 + ( ( 𝑚 + 1 ) · 𝐷 ) ) ) → ∃ 𝑛 ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) )
121 99 113 120 syl2anc ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ∃ 𝑛 ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) )
122 eqeq1 ⊢ ( 𝑥 = ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) → ( 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ↔ ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) )
123 122 anbi2d ⊢ ( 𝑥 = ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) → ( ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ↔ ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ) )
124 123 exbidv ⊢ ( 𝑥 = ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) → ( ∃ 𝑛 ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ↔ ∃ 𝑛 ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ) )
125 121 124 syl5ibrcom ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝑥 = ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) → ∃ 𝑛 ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ) )
126 125 rexlimdva ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) → ∃ 𝑛 ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ) )
127 82 126 impbid ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( ∃ 𝑛 ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ↔ ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) ) )
128 nnaddcl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 + 𝐷 ) ∈ ℕ )
129 128 3adant1 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 + 𝐷 ) ∈ ℕ )
130 vdwapval ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐴 + 𝐷 ) ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝑥 ∈ ( ( 𝐴 + 𝐷 ) ( AP ‘ 𝐾 ) 𝐷 ) ↔ ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) ) )
131 129 130 syld3an2 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝑥 ∈ ( ( 𝐴 + 𝐷 ) ( AP ‘ 𝐾 ) 𝐷 ) ↔ ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( ( 𝐴 + 𝐷 ) + ( 𝑚 · 𝐷 ) ) ) )
132 127 131 bitr4d ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( ∃ 𝑛 ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ↔ 𝑥 ∈ ( ( 𝐴 + 𝐷 ) ( AP ‘ 𝐾 ) 𝐷 ) ) )
133 40 132 orbi12d ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( ( ∃ 𝑛 ( 𝑛 = 0 ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ∨ ∃ 𝑛 ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ) ↔ ( 𝑥 ∈ { 𝐴 } ∨ 𝑥 ∈ ( ( 𝐴 + 𝐷 ) ( AP ‘ 𝐾 ) 𝐷 ) ) ) )
134 elun ⊢ ( 𝑥 ∈ ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ 𝐾 ) 𝐷 ) ) ↔ ( 𝑥 ∈ { 𝐴 } ∨ 𝑥 ∈ ( ( 𝐴 + 𝐷 ) ( AP ‘ 𝐾 ) 𝐷 ) ) )
135 133 134 bitr4di ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( ( ∃ 𝑛 ( 𝑛 = 0 ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ∨ ∃ 𝑛 ( 𝑛 ∈ ( ( 0 + 1 ) ... 𝐾 ) ∧ 𝑥 = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) ) ↔ 𝑥 ∈ ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ 𝐾 ) 𝐷 ) ) ) )
136 24 135 bitrd ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝑥 ∈ ( 𝐴 ( AP ‘ ( 𝐾 + 1 ) ) 𝐷 ) ↔ 𝑥 ∈ ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ 𝐾 ) 𝐷 ) ) ) )
137 136 eqrdv ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 ( AP ‘ ( 𝐾 + 1 ) ) 𝐷 ) = ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ 𝐾 ) 𝐷 ) ) )