Step |
Hyp |
Ref |
Expression |
1 |
|
1e0p1 |
⊢ 1 = ( 0 + 1 ) |
2 |
1
|
fveq2i |
⊢ ( AP ‘ 1 ) = ( AP ‘ ( 0 + 1 ) ) |
3 |
2
|
oveqi |
⊢ ( 𝐴 ( AP ‘ 1 ) 𝐷 ) = ( 𝐴 ( AP ‘ ( 0 + 1 ) ) 𝐷 ) |
4 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
5 |
|
vdwapun |
⊢ ( ( 0 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 ( AP ‘ ( 0 + 1 ) ) 𝐷 ) = ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ 0 ) 𝐷 ) ) ) |
6 |
4 5
|
mp3an1 |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 ( AP ‘ ( 0 + 1 ) ) 𝐷 ) = ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ 0 ) 𝐷 ) ) ) |
7 |
3 6
|
syl5eq |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 ( AP ‘ 1 ) 𝐷 ) = ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ 0 ) 𝐷 ) ) ) |
8 |
|
nnaddcl |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 + 𝐷 ) ∈ ℕ ) |
9 |
|
vdwap0 |
⊢ ( ( ( 𝐴 + 𝐷 ) ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( ( 𝐴 + 𝐷 ) ( AP ‘ 0 ) 𝐷 ) = ∅ ) |
10 |
8 9
|
sylancom |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( ( 𝐴 + 𝐷 ) ( AP ‘ 0 ) 𝐷 ) = ∅ ) |
11 |
10
|
uneq2d |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ 0 ) 𝐷 ) ) = ( { 𝐴 } ∪ ∅ ) ) |
12 |
|
un0 |
⊢ ( { 𝐴 } ∪ ∅ ) = { 𝐴 } |
13 |
11 12
|
eqtrdi |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ 0 ) 𝐷 ) ) = { 𝐴 } ) |
14 |
7 13
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 ( AP ‘ 1 ) 𝐷 ) = { 𝐴 } ) |