Step |
Hyp |
Ref |
Expression |
1 |
|
fltne.a |
|- ( ph -> A e. NN ) |
2 |
|
fltne.b |
|- ( ph -> B e. NN ) |
3 |
|
fltne.c |
|- ( ph -> C e. NN ) |
4 |
|
fltne.n |
|- ( ph -> N e. ( ZZ>= ` 2 ) ) |
5 |
|
fltne.1 |
|- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) ) |
6 |
|
2prm |
|- 2 e. Prime |
7 |
|
rtprmirr |
|- ( ( 2 e. Prime /\ N e. ( ZZ>= ` 2 ) ) -> ( 2 ^c ( 1 / N ) ) e. ( RR \ QQ ) ) |
8 |
6 4 7
|
sylancr |
|- ( ph -> ( 2 ^c ( 1 / N ) ) e. ( RR \ QQ ) ) |
9 |
8
|
eldifbd |
|- ( ph -> -. ( 2 ^c ( 1 / N ) ) e. QQ ) |
10 |
3
|
nnzd |
|- ( ph -> C e. ZZ ) |
11 |
|
znq |
|- ( ( C e. ZZ /\ A e. NN ) -> ( C / A ) e. QQ ) |
12 |
10 1 11
|
syl2anc |
|- ( ph -> ( C / A ) e. QQ ) |
13 |
|
eleq1a |
|- ( ( C / A ) e. QQ -> ( ( 2 ^c ( 1 / N ) ) = ( C / A ) -> ( 2 ^c ( 1 / N ) ) e. QQ ) ) |
14 |
12 13
|
syl |
|- ( ph -> ( ( 2 ^c ( 1 / N ) ) = ( C / A ) -> ( 2 ^c ( 1 / N ) ) e. QQ ) ) |
15 |
14
|
necon3bd |
|- ( ph -> ( -. ( 2 ^c ( 1 / N ) ) e. QQ -> ( 2 ^c ( 1 / N ) ) =/= ( C / A ) ) ) |
16 |
9 15
|
mpd |
|- ( ph -> ( 2 ^c ( 1 / N ) ) =/= ( C / A ) ) |
17 |
|
2rp |
|- 2 e. RR+ |
18 |
17
|
a1i |
|- ( ph -> 2 e. RR+ ) |
19 |
|
eluz2nn |
|- ( N e. ( ZZ>= ` 2 ) -> N e. NN ) |
20 |
4 19
|
syl |
|- ( ph -> N e. NN ) |
21 |
20
|
nnrecred |
|- ( ph -> ( 1 / N ) e. RR ) |
22 |
18 21
|
rpcxpcld |
|- ( ph -> ( 2 ^c ( 1 / N ) ) e. RR+ ) |
23 |
22
|
adantr |
|- ( ( ph /\ A = B ) -> ( 2 ^c ( 1 / N ) ) e. RR+ ) |
24 |
3
|
nnrpd |
|- ( ph -> C e. RR+ ) |
25 |
1
|
nnrpd |
|- ( ph -> A e. RR+ ) |
26 |
24 25
|
rpdivcld |
|- ( ph -> ( C / A ) e. RR+ ) |
27 |
26
|
adantr |
|- ( ( ph /\ A = B ) -> ( C / A ) e. RR+ ) |
28 |
20
|
adantr |
|- ( ( ph /\ A = B ) -> N e. NN ) |
29 |
20
|
nnnn0d |
|- ( ph -> N e. NN0 ) |
30 |
1 29
|
nnexpcld |
|- ( ph -> ( A ^ N ) e. NN ) |
31 |
30
|
adantr |
|- ( ( ph /\ A = B ) -> ( A ^ N ) e. NN ) |
32 |
31
|
nncnd |
|- ( ( ph /\ A = B ) -> ( A ^ N ) e. CC ) |
33 |
|
2cnd |
|- ( ( ph /\ A = B ) -> 2 e. CC ) |
34 |
31
|
nnne0d |
|- ( ( ph /\ A = B ) -> ( A ^ N ) =/= 0 ) |
35 |
30
|
nncnd |
|- ( ph -> ( A ^ N ) e. CC ) |
36 |
35
|
times2d |
|- ( ph -> ( ( A ^ N ) x. 2 ) = ( ( A ^ N ) + ( A ^ N ) ) ) |
37 |
36
|
adantr |
|- ( ( ph /\ A = B ) -> ( ( A ^ N ) x. 2 ) = ( ( A ^ N ) + ( A ^ N ) ) ) |
38 |
|
simpr |
|- ( ( ph /\ A = B ) -> A = B ) |
39 |
38
|
oveq1d |
|- ( ( ph /\ A = B ) -> ( A ^ N ) = ( B ^ N ) ) |
40 |
39
|
oveq2d |
|- ( ( ph /\ A = B ) -> ( ( A ^ N ) + ( A ^ N ) ) = ( ( A ^ N ) + ( B ^ N ) ) ) |
41 |
5
|
adantr |
|- ( ( ph /\ A = B ) -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) ) |
42 |
37 40 41
|
3eqtrd |
|- ( ( ph /\ A = B ) -> ( ( A ^ N ) x. 2 ) = ( C ^ N ) ) |
43 |
32 33 34 42
|
mvllmuld |
|- ( ( ph /\ A = B ) -> 2 = ( ( C ^ N ) / ( A ^ N ) ) ) |
44 |
|
2cn |
|- 2 e. CC |
45 |
|
cxproot |
|- ( ( 2 e. CC /\ N e. NN ) -> ( ( 2 ^c ( 1 / N ) ) ^ N ) = 2 ) |
46 |
44 20 45
|
sylancr |
|- ( ph -> ( ( 2 ^c ( 1 / N ) ) ^ N ) = 2 ) |
47 |
46
|
adantr |
|- ( ( ph /\ A = B ) -> ( ( 2 ^c ( 1 / N ) ) ^ N ) = 2 ) |
48 |
3
|
nncnd |
|- ( ph -> C e. CC ) |
49 |
1
|
nncnd |
|- ( ph -> A e. CC ) |
50 |
1
|
nnne0d |
|- ( ph -> A =/= 0 ) |
51 |
48 49 50 29
|
expdivd |
|- ( ph -> ( ( C / A ) ^ N ) = ( ( C ^ N ) / ( A ^ N ) ) ) |
52 |
51
|
adantr |
|- ( ( ph /\ A = B ) -> ( ( C / A ) ^ N ) = ( ( C ^ N ) / ( A ^ N ) ) ) |
53 |
43 47 52
|
3eqtr4d |
|- ( ( ph /\ A = B ) -> ( ( 2 ^c ( 1 / N ) ) ^ N ) = ( ( C / A ) ^ N ) ) |
54 |
23 27 28 53
|
exp11nnd |
|- ( ( ph /\ A = B ) -> ( 2 ^c ( 1 / N ) ) = ( C / A ) ) |
55 |
16 54
|
mteqand |
|- ( ph -> A =/= B ) |