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 ) )