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 
|- ( ( K e. NN0 /\ A e. NN /\ D e. NN ) -> ( A ( AP ` ( K + 1 ) ) D ) = ( { A } u. ( ( A + D ) ( AP ` K ) D ) ) )

Proof

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