Metamath Proof Explorer

Theorem vdwapval

Description: Value of the arithmetic progression function. (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Assertion vdwapval ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝑋 ∈ ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) ↔ ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑋 = ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) )

Proof

Step Hyp Ref Expression
1 vdwapfval ⊢ ( 𝐾 ∈ ℕ0 → ( AP ‘ 𝐾 ) = ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ) )
2 1 3ad2ant1 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( AP ‘ 𝐾 ) = ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ) )
3 2 oveqd ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) = ( 𝐴 ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ) 𝐷 ) )
4 oveq2 ⊢ ( 𝑑 = 𝐷 → ( 𝑚 · 𝑑 ) = ( 𝑚 · 𝐷 ) )
5 oveq12 ⊢ ( ( 𝑎 = 𝐴 ∧ ( 𝑚 · 𝑑 ) = ( 𝑚 · 𝐷 ) ) → ( 𝑎 + ( 𝑚 · 𝑑 ) ) = ( 𝐴 + ( 𝑚 · 𝐷 ) ) )
6 4 5 sylan2 ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑑 = 𝐷 ) → ( 𝑎 + ( 𝑚 · 𝑑 ) ) = ( 𝐴 + ( 𝑚 · 𝐷 ) ) )
7 6 mpteq2dv ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑑 = 𝐷 ) → ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) = ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) )
8 7 rneqd ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑑 = 𝐷 ) → ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) = ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) )
9 eqid ⊢ ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ) = ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) )
10 ovex ⊢ ( 0 ... ( 𝐾 − 1 ) ) ∈ V
11 10 mptex ⊢ ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) ∈ V
12 11 rnex ⊢ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) ∈ V
13 8 9 12 ovmpoa ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ) 𝐷 ) = ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) )
14 13 3adant1 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ) 𝐷 ) = ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) )
15 3 14 eqtrd ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) = ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) )
16 eqid ⊢ ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) = ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝐴 + ( 𝑚 · 𝐷 ) ) )
17 16 rnmpt ⊢ ran ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↦ ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) = { 𝑥 ∣ ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( 𝐴 + ( 𝑚 · 𝐷 ) ) }
18 15 17 eqtrdi ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) = { 𝑥 ∣ ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( 𝐴 + ( 𝑚 · 𝐷 ) ) } )
19 18 eleq2d ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝑋 ∈ ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) ↔ 𝑋 ∈ { 𝑥 ∣ ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( 𝐴 + ( 𝑚 · 𝐷 ) ) } ) )
20 id ⊢ ( 𝑋 = ( 𝐴 + ( 𝑚 · 𝐷 ) ) → 𝑋 = ( 𝐴 + ( 𝑚 · 𝐷 ) ) )
21 ovex ⊢ ( 𝐴 + ( 𝑚 · 𝐷 ) ) ∈ V
22 20 21 eqeltrdi ⊢ ( 𝑋 = ( 𝐴 + ( 𝑚 · 𝐷 ) ) → 𝑋 ∈ V )
23 22 rexlimivw ⊢ ( ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑋 = ( 𝐴 + ( 𝑚 · 𝐷 ) ) → 𝑋 ∈ V )
24 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = ( 𝐴 + ( 𝑚 · 𝐷 ) ) ↔ 𝑋 = ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) )
25 24 rexbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( 𝐴 + ( 𝑚 · 𝐷 ) ) ↔ ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑋 = ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) )
26 23 25 elab3 ⊢ ( 𝑋 ∈ { 𝑥 ∣ ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( 𝐴 + ( 𝑚 · 𝐷 ) ) } ↔ ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑋 = ( 𝐴 + ( 𝑚 · 𝐷 ) ) )
27 19 26 bitrdi ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝑋 ∈ ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) ↔ ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑋 = ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) )