Step |
Hyp |
Ref |
Expression |
1 |
|
nn0ind-raph.1 |
|- ( x = 0 -> ( ph <-> ps ) ) |
2 |
|
nn0ind-raph.2 |
|- ( x = y -> ( ph <-> ch ) ) |
3 |
|
nn0ind-raph.3 |
|- ( x = ( y + 1 ) -> ( ph <-> th ) ) |
4 |
|
nn0ind-raph.4 |
|- ( x = A -> ( ph <-> ta ) ) |
5 |
|
nn0ind-raph.5 |
|- ps |
6 |
|
nn0ind-raph.6 |
|- ( y e. NN0 -> ( ch -> th ) ) |
7 |
|
elnn0 |
|- ( A e. NN0 <-> ( A e. NN \/ A = 0 ) ) |
8 |
|
dfsbcq2 |
|- ( z = 1 -> ( [ z / x ] ph <-> [. 1 / x ]. ph ) ) |
9 |
|
nfv |
|- F/ x ch |
10 |
9 2
|
sbhypf |
|- ( z = y -> ( [ z / x ] ph <-> ch ) ) |
11 |
|
nfv |
|- F/ x th |
12 |
11 3
|
sbhypf |
|- ( z = ( y + 1 ) -> ( [ z / x ] ph <-> th ) ) |
13 |
|
nfv |
|- F/ x ta |
14 |
13 4
|
sbhypf |
|- ( z = A -> ( [ z / x ] ph <-> ta ) ) |
15 |
|
nfsbc1v |
|- F/ x [. 1 / x ]. ph |
16 |
|
1ex |
|- 1 e. _V |
17 |
|
c0ex |
|- 0 e. _V |
18 |
|
0nn0 |
|- 0 e. NN0 |
19 |
|
eleq1a |
|- ( 0 e. NN0 -> ( y = 0 -> y e. NN0 ) ) |
20 |
18 19
|
ax-mp |
|- ( y = 0 -> y e. NN0 ) |
21 |
5 1
|
mpbiri |
|- ( x = 0 -> ph ) |
22 |
|
eqeq2 |
|- ( y = 0 -> ( x = y <-> x = 0 ) ) |
23 |
22 2
|
syl6bir |
|- ( y = 0 -> ( x = 0 -> ( ph <-> ch ) ) ) |
24 |
23
|
pm5.74d |
|- ( y = 0 -> ( ( x = 0 -> ph ) <-> ( x = 0 -> ch ) ) ) |
25 |
21 24
|
mpbii |
|- ( y = 0 -> ( x = 0 -> ch ) ) |
26 |
25
|
com12 |
|- ( x = 0 -> ( y = 0 -> ch ) ) |
27 |
17 26
|
vtocle |
|- ( y = 0 -> ch ) |
28 |
20 27 6
|
sylc |
|- ( y = 0 -> th ) |
29 |
28
|
adantr |
|- ( ( y = 0 /\ x = 1 ) -> th ) |
30 |
|
oveq1 |
|- ( y = 0 -> ( y + 1 ) = ( 0 + 1 ) ) |
31 |
|
0p1e1 |
|- ( 0 + 1 ) = 1 |
32 |
30 31
|
eqtrdi |
|- ( y = 0 -> ( y + 1 ) = 1 ) |
33 |
32
|
eqeq2d |
|- ( y = 0 -> ( x = ( y + 1 ) <-> x = 1 ) ) |
34 |
33 3
|
syl6bir |
|- ( y = 0 -> ( x = 1 -> ( ph <-> th ) ) ) |
35 |
34
|
imp |
|- ( ( y = 0 /\ x = 1 ) -> ( ph <-> th ) ) |
36 |
29 35
|
mpbird |
|- ( ( y = 0 /\ x = 1 ) -> ph ) |
37 |
36
|
ex |
|- ( y = 0 -> ( x = 1 -> ph ) ) |
38 |
17 37
|
vtocle |
|- ( x = 1 -> ph ) |
39 |
|
sbceq1a |
|- ( x = 1 -> ( ph <-> [. 1 / x ]. ph ) ) |
40 |
38 39
|
mpbid |
|- ( x = 1 -> [. 1 / x ]. ph ) |
41 |
15 16 40
|
vtoclef |
|- [. 1 / x ]. ph |
42 |
|
nnnn0 |
|- ( y e. NN -> y e. NN0 ) |
43 |
42 6
|
syl |
|- ( y e. NN -> ( ch -> th ) ) |
44 |
8 10 12 14 41 43
|
nnind |
|- ( A e. NN -> ta ) |
45 |
|
nfv |
|- F/ x ( 0 = A -> ta ) |
46 |
|
eqeq1 |
|- ( x = 0 -> ( x = A <-> 0 = A ) ) |
47 |
1
|
bicomd |
|- ( x = 0 -> ( ps <-> ph ) ) |
48 |
47 4
|
sylan9bb |
|- ( ( x = 0 /\ x = A ) -> ( ps <-> ta ) ) |
49 |
5 48
|
mpbii |
|- ( ( x = 0 /\ x = A ) -> ta ) |
50 |
49
|
ex |
|- ( x = 0 -> ( x = A -> ta ) ) |
51 |
46 50
|
sylbird |
|- ( x = 0 -> ( 0 = A -> ta ) ) |
52 |
45 17 51
|
vtoclef |
|- ( 0 = A -> ta ) |
53 |
52
|
eqcoms |
|- ( A = 0 -> ta ) |
54 |
44 53
|
jaoi |
|- ( ( A e. NN \/ A = 0 ) -> ta ) |
55 |
7 54
|
sylbi |
|- ( A e. NN0 -> ta ) |