Metamath Proof Explorer

Theorem pceu

Description: Uniqueness for the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Hypotheses pcval.1 
|- S = sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < )
pcval.2 
|- T = sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < )
Assertion pceu 
|- ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> E! z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) )

Proof

Step Hyp Ref Expression
1 pcval.1 
 |-  S = sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < )
2 pcval.2 
 |-  T = sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < )
3 simprl 
 |-  ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> N e. QQ )
4 elq 
 |-  ( N e. QQ <-> E. x e. ZZ E. y e. NN N = ( x / y ) )
5 3 4 sylib 
 |-  ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> E. x e. ZZ E. y e. NN N = ( x / y ) )
6 ovex 
 |-  ( S - T ) e. _V
7 biidd 
 |-  ( z = ( S - T ) -> ( N = ( x / y ) <-> N = ( x / y ) ) )
8 6 7 ceqsexv 
 |-  ( E. z ( z = ( S - T ) /\ N = ( x / y ) ) <-> N = ( x / y ) )
9 exancom 
 |-  ( E. z ( z = ( S - T ) /\ N = ( x / y ) ) <-> E. z ( N = ( x / y ) /\ z = ( S - T ) ) )
10 8 9 bitr3i 
 |-  ( N = ( x / y ) <-> E. z ( N = ( x / y ) /\ z = ( S - T ) ) )
11 10 rexbii 
 |-  ( E. y e. NN N = ( x / y ) <-> E. y e. NN E. z ( N = ( x / y ) /\ z = ( S - T ) ) )
12 rexcom4 
 |-  ( E. y e. NN E. z ( N = ( x / y ) /\ z = ( S - T ) ) <-> E. z E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) )
13 11 12 bitri 
 |-  ( E. y e. NN N = ( x / y ) <-> E. z E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) )
14 13 rexbii 
 |-  ( E. x e. ZZ E. y e. NN N = ( x / y ) <-> E. x e. ZZ E. z E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) )
15 rexcom4 
 |-  ( E. x e. ZZ E. z E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) <-> E. z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) )
16 14 15 bitri 
 |-  ( E. x e. ZZ E. y e. NN N = ( x / y ) <-> E. z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) )
17 5 16 sylib 
 |-  ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> E. z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) )
18 eqid 
 |-  sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < )
19 eqid 
 |-  sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < )
20 simp11l 
 |-  ( ( ( ( P e. Prime /\ N =/= 0 ) /\ ( x e. ZZ /\ y e. NN ) /\ ( N = ( x / y ) /\ z = ( S - T ) ) ) /\ ( s e. ZZ /\ t e. NN ) /\ ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) ) -> P e. Prime )
21 simp11r 
 |-  ( ( ( ( P e. Prime /\ N =/= 0 ) /\ ( x e. ZZ /\ y e. NN ) /\ ( N = ( x / y ) /\ z = ( S - T ) ) ) /\ ( s e. ZZ /\ t e. NN ) /\ ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) ) -> N =/= 0 )
22 simp12 
 |-  ( ( ( ( P e. Prime /\ N =/= 0 ) /\ ( x e. ZZ /\ y e. NN ) /\ ( N = ( x / y ) /\ z = ( S - T ) ) ) /\ ( s e. ZZ /\ t e. NN ) /\ ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) ) -> ( x e. ZZ /\ y e. NN ) )
23 simp13l 
 |-  ( ( ( ( P e. Prime /\ N =/= 0 ) /\ ( x e. ZZ /\ y e. NN ) /\ ( N = ( x / y ) /\ z = ( S - T ) ) ) /\ ( s e. ZZ /\ t e. NN ) /\ ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) ) -> N = ( x / y ) )
24 simp2 
 |-  ( ( ( ( P e. Prime /\ N =/= 0 ) /\ ( x e. ZZ /\ y e. NN ) /\ ( N = ( x / y ) /\ z = ( S - T ) ) ) /\ ( s e. ZZ /\ t e. NN ) /\ ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) ) -> ( s e. ZZ /\ t e. NN ) )
25 simp3l 
 |-  ( ( ( ( P e. Prime /\ N =/= 0 ) /\ ( x e. ZZ /\ y e. NN ) /\ ( N = ( x / y ) /\ z = ( S - T ) ) ) /\ ( s e. ZZ /\ t e. NN ) /\ ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) ) -> N = ( s / t ) )
26 1 2 18 19 20 21 22 23 24 25 pceulem 
 |-  ( ( ( ( P e. Prime /\ N =/= 0 ) /\ ( x e. ZZ /\ y e. NN ) /\ ( N = ( x / y ) /\ z = ( S - T ) ) ) /\ ( s e. ZZ /\ t e. NN ) /\ ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) ) -> ( S - T ) = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) )
27 simp13r 
 |-  ( ( ( ( P e. Prime /\ N =/= 0 ) /\ ( x e. ZZ /\ y e. NN ) /\ ( N = ( x / y ) /\ z = ( S - T ) ) ) /\ ( s e. ZZ /\ t e. NN ) /\ ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) ) -> z = ( S - T ) )
28 simp3r 
 |-  ( ( ( ( P e. Prime /\ N =/= 0 ) /\ ( x e. ZZ /\ y e. NN ) /\ ( N = ( x / y ) /\ z = ( S - T ) ) ) /\ ( s e. ZZ /\ t e. NN ) /\ ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) ) -> w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) )
29 26 27 28 3eqtr4d 
 |-  ( ( ( ( P e. Prime /\ N =/= 0 ) /\ ( x e. ZZ /\ y e. NN ) /\ ( N = ( x / y ) /\ z = ( S - T ) ) ) /\ ( s e. ZZ /\ t e. NN ) /\ ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) ) -> z = w )
30 29 3exp 
 |-  ( ( ( P e. Prime /\ N =/= 0 ) /\ ( x e. ZZ /\ y e. NN ) /\ ( N = ( x / y ) /\ z = ( S - T ) ) ) -> ( ( s e. ZZ /\ t e. NN ) -> ( ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) -> z = w ) ) )
31 30 rexlimdvv 
 |-  ( ( ( P e. Prime /\ N =/= 0 ) /\ ( x e. ZZ /\ y e. NN ) /\ ( N = ( x / y ) /\ z = ( S - T ) ) ) -> ( E. s e. ZZ E. t e. NN ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) -> z = w ) )
32 31 3exp 
 |-  ( ( P e. Prime /\ N =/= 0 ) -> ( ( x e. ZZ /\ y e. NN ) -> ( ( N = ( x / y ) /\ z = ( S - T ) ) -> ( E. s e. ZZ E. t e. NN ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) -> z = w ) ) ) )
33 32 adantrl 
 |-  ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> ( ( x e. ZZ /\ y e. NN ) -> ( ( N = ( x / y ) /\ z = ( S - T ) ) -> ( E. s e. ZZ E. t e. NN ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) -> z = w ) ) ) )
34 33 rexlimdvv 
 |-  ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> ( E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) -> ( E. s e. ZZ E. t e. NN ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) -> z = w ) ) )
35 34 impd 
 |-  ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> ( ( E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) /\ E. s e. ZZ E. t e. NN ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) ) -> z = w ) )
36 35 alrimivv 
 |-  ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> A. z A. w ( ( E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) /\ E. s e. ZZ E. t e. NN ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) ) -> z = w ) )
37 eqeq1 
 |-  ( z = w -> ( z = ( S - T ) <-> w = ( S - T ) ) )
38 37 anbi2d 
 |-  ( z = w -> ( ( N = ( x / y ) /\ z = ( S - T ) ) <-> ( N = ( x / y ) /\ w = ( S - T ) ) ) )
39 38 2rexbidv 
 |-  ( z = w -> ( E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) <-> E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ w = ( S - T ) ) ) )
40 oveq1 
 |-  ( x = s -> ( x / y ) = ( s / y ) )
41 40 eqeq2d 
 |-  ( x = s -> ( N = ( x / y ) <-> N = ( s / y ) ) )
42 breq2 
 |-  ( x = s -> ( ( P ^ n ) || x <-> ( P ^ n ) || s ) )
43 42 rabbidv 
 |-  ( x = s -> { n e. NN0 | ( P ^ n ) || x } = { n e. NN0 | ( P ^ n ) || s } )
44 43 supeq1d 
 |-  ( x = s -> sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) )
45 1 44 syl5eq 
 |-  ( x = s -> S = sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) )
46 45 oveq1d 
 |-  ( x = s -> ( S - T ) = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - T ) )
47 46 eqeq2d 
 |-  ( x = s -> ( w = ( S - T ) <-> w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - T ) ) )
48 41 47 anbi12d 
 |-  ( x = s -> ( ( N = ( x / y ) /\ w = ( S - T ) ) <-> ( N = ( s / y ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - T ) ) ) )
49 48 rexbidv 
 |-  ( x = s -> ( E. y e. NN ( N = ( x / y ) /\ w = ( S - T ) ) <-> E. y e. NN ( N = ( s / y ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - T ) ) ) )
50 oveq2 
 |-  ( y = t -> ( s / y ) = ( s / t ) )
51 50 eqeq2d 
 |-  ( y = t -> ( N = ( s / y ) <-> N = ( s / t ) ) )
52 breq2 
 |-  ( y = t -> ( ( P ^ n ) || y <-> ( P ^ n ) || t ) )
53 52 rabbidv 
 |-  ( y = t -> { n e. NN0 | ( P ^ n ) || y } = { n e. NN0 | ( P ^ n ) || t } )
54 53 supeq1d 
 |-  ( y = t -> sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) )
55 2 54 syl5eq 
 |-  ( y = t -> T = sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) )
56 55 oveq2d 
 |-  ( y = t -> ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - T ) = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) )
57 56 eqeq2d 
 |-  ( y = t -> ( w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - T ) <-> w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) )
58 51 57 anbi12d 
 |-  ( y = t -> ( ( N = ( s / y ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - T ) ) <-> ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) ) )
59 58 cbvrexvw 
 |-  ( E. y e. NN ( N = ( s / y ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - T ) ) <-> E. t e. NN ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) )
60 49 59 bitrdi 
 |-  ( x = s -> ( E. y e. NN ( N = ( x / y ) /\ w = ( S - T ) ) <-> E. t e. NN ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) ) )
61 60 cbvrexvw 
 |-  ( E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ w = ( S - T ) ) <-> E. s e. ZZ E. t e. NN ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) )
62 39 61 bitrdi 
 |-  ( z = w -> ( E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) <-> E. s e. ZZ E. t e. NN ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) ) )
63 62 eu4 
 |-  ( E! z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) <-> ( E. z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) /\ A. z A. w ( ( E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) /\ E. s e. ZZ E. t e. NN ( N = ( s / t ) /\ w = ( sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < ) ) ) ) -> z = w ) ) )
64 17 36 63 sylanbrc 
 |-  ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> E! z E. x e. ZZ E. y e. NN ( N = ( x / y ) /\ z = ( S - T ) ) )