Metamath Proof Explorer

Theorem vdwapval

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

Ref Expression
Assertion vdwapval ⊢K∈ℕ0∧A∈ℕ∧D∈ℕ→X∈AAP⁡KD↔∃m∈0…K−1X=A+m⁢D

Proof

Step Hyp Ref Expression
1 vdwapfval ⊢K∈ℕ0→AP⁡K=a∈ℕ,d∈ℕ⟼ran⁡m∈0…K−1⟼a+m⁢d
2 1 3ad2ant1 ⊢K∈ℕ0∧A∈ℕ∧D∈ℕ→AP⁡K=a∈ℕ,d∈ℕ⟼ran⁡m∈0…K−1⟼a+m⁢d
3 2 oveqd ⊢K∈ℕ0∧A∈ℕ∧D∈ℕ→AAP⁡KD=Aa∈ℕ,d∈ℕ⟼ran⁡m∈0…K−1⟼a+m⁢dD
4 oveq2 ⊢d=D→m⁢d=m⁢D
5 oveq12 ⊢a=A∧m⁢d=m⁢D→a+m⁢d=A+m⁢D
6 4 5 sylan2 ⊢a=A∧d=D→a+m⁢d=A+m⁢D
7 6 mpteq2dv ⊢a=A∧d=D→m∈0…K−1⟼a+m⁢d=m∈0…K−1⟼A+m⁢D
8 7 rneqd ⊢a=A∧d=D→ran⁡m∈0…K−1⟼a+m⁢d=ran⁡m∈0…K−1⟼A+m⁢D
9 eqid ⊢a∈ℕ,d∈ℕ⟼ran⁡m∈0…K−1⟼a+m⁢d=a∈ℕ,d∈ℕ⟼ran⁡m∈0…K−1⟼a+m⁢d
10 ovex ⊢0…K−1∈V
11 10 mptex ⊢m∈0…K−1⟼A+m⁢D∈V
12 11 rnex ⊢ran⁡m∈0…K−1⟼A+m⁢D∈V
13 8 9 12 ovmpoa ⊢A∈ℕ∧D∈ℕ→Aa∈ℕ,d∈ℕ⟼ran⁡m∈0…K−1⟼a+m⁢dD=ran⁡m∈0…K−1⟼A+m⁢D
14 13 3adant1 ⊢K∈ℕ0∧A∈ℕ∧D∈ℕ→Aa∈ℕ,d∈ℕ⟼ran⁡m∈0…K−1⟼a+m⁢dD=ran⁡m∈0…K−1⟼A+m⁢D
15 3 14 eqtrd ⊢K∈ℕ0∧A∈ℕ∧D∈ℕ→AAP⁡KD=ran⁡m∈0…K−1⟼A+m⁢D
16 eqid ⊢m∈0…K−1⟼A+m⁢D=m∈0…K−1⟼A+m⁢D
17 16 rnmpt ⊢ran⁡m∈0…K−1⟼A+m⁢D=x|∃m∈0…K−1x=A+m⁢D
18 15 17 eqtrdi ⊢K∈ℕ0∧A∈ℕ∧D∈ℕ→AAP⁡KD=x|∃m∈0…K−1x=A+m⁢D
19 18 eleq2d ⊢K∈ℕ0∧A∈ℕ∧D∈ℕ→X∈AAP⁡KD↔X∈x|∃m∈0…K−1x=A+m⁢D
20 id ⊢X=A+m⁢D→X=A+m⁢D
21 ovex ⊢A+m⁢D∈V
22 20 21 eqeltrdi ⊢X=A+m⁢D→X∈V
23 22 rexlimivw ⊢∃m∈0…K−1X=A+m⁢D→X∈V
24 eqeq1 ⊢x=X→x=A+m⁢D↔X=A+m⁢D
25 24 rexbidv ⊢x=X→∃m∈0…K−1x=A+m⁢D↔∃m∈0…K−1X=A+m⁢D
26 23 25 elab3 ⊢X∈x|∃m∈0…K−1x=A+m⁢D↔∃m∈0…K−1X=A+m⁢D
27 19 26 bitrdi ⊢K∈ℕ0∧A∈ℕ∧D∈ℕ→X∈AAP⁡KD↔∃m∈0…K−1X=A+m⁢D