This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pceulem

Description: Lemma for pceu . (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 , < )
pceu.3 
|- U = sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < )
pceu.4 
|- V = sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < )
pceu.5 
|- ( ph -> P e. Prime )
pceu.6 
|- ( ph -> N =/= 0 )
pceu.7 
|- ( ph -> ( x e. ZZ /\ y e. NN ) )
pceu.8 
|- ( ph -> N = ( x / y ) )
pceu.9 
|- ( ph -> ( s e. ZZ /\ t e. NN ) )
pceu.10 
|- ( ph -> N = ( s / t ) )
Assertion pceulem 
|- ( ph -> ( S - T ) = ( U - V ) )

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 pceu.3 
 |-  U = sup ( { n e. NN0 | ( P ^ n ) || s } , RR , < )
4 pceu.4 
 |-  V = sup ( { n e. NN0 | ( P ^ n ) || t } , RR , < )
5 pceu.5 
 |-  ( ph -> P e. Prime )
6 pceu.6 
 |-  ( ph -> N =/= 0 )
7 pceu.7 
 |-  ( ph -> ( x e. ZZ /\ y e. NN ) )
8 pceu.8 
 |-  ( ph -> N = ( x / y ) )
9 pceu.9 
 |-  ( ph -> ( s e. ZZ /\ t e. NN ) )
10 pceu.10 
 |-  ( ph -> N = ( s / t ) )
11 7 simprd 
 |-  ( ph -> y e. NN )
12 11 nncnd 
 |-  ( ph -> y e. CC )
13 9 simpld 
 |-  ( ph -> s e. ZZ )
14 13 zcnd 
 |-  ( ph -> s e. CC )
15 12 14 mulcomd 
 |-  ( ph -> ( y x. s ) = ( s x. y ) )
16 10 8 eqtr3d 
 |-  ( ph -> ( s / t ) = ( x / y ) )
17 9 simprd 
 |-  ( ph -> t e. NN )
18 17 nncnd 
 |-  ( ph -> t e. CC )
19 7 simpld 
 |-  ( ph -> x e. ZZ )
20 19 zcnd 
 |-  ( ph -> x e. CC )
21 17 nnne0d 
 |-  ( ph -> t =/= 0 )
22 11 nnne0d 
 |-  ( ph -> y =/= 0 )
23 14 18 20 12 21 22 divmuleqd 
 |-  ( ph -> ( ( s / t ) = ( x / y ) <-> ( s x. y ) = ( x x. t ) ) )
24 16 23 mpbid 
 |-  ( ph -> ( s x. y ) = ( x x. t ) )
25 15 24 eqtrd 
 |-  ( ph -> ( y x. s ) = ( x x. t ) )
26 25 breq2d 
 |-  ( ph -> ( ( P ^ z ) || ( y x. s ) <-> ( P ^ z ) || ( x x. t ) ) )
27 26 rabbidv 
 |-  ( ph -> { z e. NN0 | ( P ^ z ) || ( y x. s ) } = { z e. NN0 | ( P ^ z ) || ( x x. t ) } )
28 oveq2 
 |-  ( n = z -> ( P ^ n ) = ( P ^ z ) )
29 28 breq1d 
 |-  ( n = z -> ( ( P ^ n ) || ( y x. s ) <-> ( P ^ z ) || ( y x. s ) ) )
30 29 cbvrabv 
 |-  { n e. NN0 | ( P ^ n ) || ( y x. s ) } = { z e. NN0 | ( P ^ z ) || ( y x. s ) }
31 28 breq1d 
 |-  ( n = z -> ( ( P ^ n ) || ( x x. t ) <-> ( P ^ z ) || ( x x. t ) ) )
32 31 cbvrabv 
 |-  { n e. NN0 | ( P ^ n ) || ( x x. t ) } = { z e. NN0 | ( P ^ z ) || ( x x. t ) }
33 27 30 32 3eqtr4g 
 |-  ( ph -> { n e. NN0 | ( P ^ n ) || ( y x. s ) } = { n e. NN0 | ( P ^ n ) || ( x x. t ) } )
34 33 supeq1d 
 |-  ( ph -> sup ( { n e. NN0 | ( P ^ n ) || ( y x. s ) } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || ( x x. t ) } , RR , < ) )
35 11 nnzd 
 |-  ( ph -> y e. ZZ )
36 18 21 div0d 
 |-  ( ph -> ( 0 / t ) = 0 )
37 oveq1 
 |-  ( s = 0 -> ( s / t ) = ( 0 / t ) )
38 37 eqeq1d 
 |-  ( s = 0 -> ( ( s / t ) = 0 <-> ( 0 / t ) = 0 ) )
39 36 38 syl5ibrcom 
 |-  ( ph -> ( s = 0 -> ( s / t ) = 0 ) )
40 10 eqeq1d 
 |-  ( ph -> ( N = 0 <-> ( s / t ) = 0 ) )
41 39 40 sylibrd 
 |-  ( ph -> ( s = 0 -> N = 0 ) )
42 41 necon3d 
 |-  ( ph -> ( N =/= 0 -> s =/= 0 ) )
43 6 42 mpd 
 |-  ( ph -> s =/= 0 )
44 eqid 
 |-  sup ( { n e. NN0 | ( P ^ n ) || ( y x. s ) } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || ( y x. s ) } , RR , < )
45 2 3 44 pcpremul 
 |-  ( ( P e. Prime /\ ( y e. ZZ /\ y =/= 0 ) /\ ( s e. ZZ /\ s =/= 0 ) ) -> ( T + U ) = sup ( { n e. NN0 | ( P ^ n ) || ( y x. s ) } , RR , < ) )
46 5 35 22 13 43 45 syl122anc 
 |-  ( ph -> ( T + U ) = sup ( { n e. NN0 | ( P ^ n ) || ( y x. s ) } , RR , < ) )
47 12 22 div0d 
 |-  ( ph -> ( 0 / y ) = 0 )
48 oveq1 
 |-  ( x = 0 -> ( x / y ) = ( 0 / y ) )
49 48 eqeq1d 
 |-  ( x = 0 -> ( ( x / y ) = 0 <-> ( 0 / y ) = 0 ) )
50 47 49 syl5ibrcom 
 |-  ( ph -> ( x = 0 -> ( x / y ) = 0 ) )
51 8 eqeq1d 
 |-  ( ph -> ( N = 0 <-> ( x / y ) = 0 ) )
52 50 51 sylibrd 
 |-  ( ph -> ( x = 0 -> N = 0 ) )
53 52 necon3d 
 |-  ( ph -> ( N =/= 0 -> x =/= 0 ) )
54 6 53 mpd 
 |-  ( ph -> x =/= 0 )
55 17 nnzd 
 |-  ( ph -> t e. ZZ )
56 eqid 
 |-  sup ( { n e. NN0 | ( P ^ n ) || ( x x. t ) } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || ( x x. t ) } , RR , < )
57 1 4 56 pcpremul 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ x =/= 0 ) /\ ( t e. ZZ /\ t =/= 0 ) ) -> ( S + V ) = sup ( { n e. NN0 | ( P ^ n ) || ( x x. t ) } , RR , < ) )
58 5 19 54 55 21 57 syl122anc 
 |-  ( ph -> ( S + V ) = sup ( { n e. NN0 | ( P ^ n ) || ( x x. t ) } , RR , < ) )
59 34 46 58 3eqtr4d 
 |-  ( ph -> ( T + U ) = ( S + V ) )
60 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
61 5 60 syl 
 |-  ( ph -> P e. ( ZZ>= ` 2 ) )
62 eqid 
 |-  { n e. NN0 | ( P ^ n ) || y } = { n e. NN0 | ( P ^ n ) || y }
63 62 2 pcprecl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( y e. ZZ /\ y =/= 0 ) ) -> ( T e. NN0 /\ ( P ^ T ) || y ) )
64 63 simpld 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( y e. ZZ /\ y =/= 0 ) ) -> T e. NN0 )
65 61 35 22 64 syl12anc 
 |-  ( ph -> T e. NN0 )
66 65 nn0cnd 
 |-  ( ph -> T e. CC )
67 eqid 
 |-  { n e. NN0 | ( P ^ n ) || s } = { n e. NN0 | ( P ^ n ) || s }
68 67 3 pcprecl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( s e. ZZ /\ s =/= 0 ) ) -> ( U e. NN0 /\ ( P ^ U ) || s ) )
69 68 simpld 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( s e. ZZ /\ s =/= 0 ) ) -> U e. NN0 )
70 61 13 43 69 syl12anc 
 |-  ( ph -> U e. NN0 )
71 70 nn0cnd 
 |-  ( ph -> U e. CC )
72 eqid 
 |-  { n e. NN0 | ( P ^ n ) || x } = { n e. NN0 | ( P ^ n ) || x }
73 72 1 pcprecl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( x e. ZZ /\ x =/= 0 ) ) -> ( S e. NN0 /\ ( P ^ S ) || x ) )
74 73 simpld 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( x e. ZZ /\ x =/= 0 ) ) -> S e. NN0 )
75 61 19 54 74 syl12anc 
 |-  ( ph -> S e. NN0 )
76 75 nn0cnd 
 |-  ( ph -> S e. CC )
77 eqid 
 |-  { n e. NN0 | ( P ^ n ) || t } = { n e. NN0 | ( P ^ n ) || t }
78 77 4 pcprecl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( t e. ZZ /\ t =/= 0 ) ) -> ( V e. NN0 /\ ( P ^ V ) || t ) )
79 78 simpld 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( t e. ZZ /\ t =/= 0 ) ) -> V e. NN0 )
80 61 55 21 79 syl12anc 
 |-  ( ph -> V e. NN0 )
81 80 nn0cnd 
 |-  ( ph -> V e. CC )
82 66 71 76 81 addsubeq4d 
 |-  ( ph -> ( ( T + U ) = ( S + V ) <-> ( S - T ) = ( U - V ) ) )
83 59 82 mpbid 
 |-  ( ph -> ( S - T ) = ( U - V ) )