Theorem pceulem

Description: Lemma for pceu . (Contributed by Mario Carneiro, 23-Feb-2014)

	Ref	Expression
Hypotheses	pcval.1	⊢ 𝑆 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < )
	pcval.2	⊢ 𝑇 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < )
	pceu.3	⊢ 𝑈 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < )
	pceu.4	⊢ 𝑉 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < )
	pceu.5	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	pceu.6	⊢ ( 𝜑 → 𝑁 ≠ 0 )
	pceu.7	⊢ ( 𝜑 → ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) )
	pceu.8	⊢ ( 𝜑 → 𝑁 = ( 𝑥 / 𝑦 ) )
	pceu.9	⊢ ( 𝜑 → ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ ) )
	pceu.10	⊢ ( 𝜑 → 𝑁 = ( 𝑠 / 𝑡 ) )
Assertion	pceulem	⊢ ( 𝜑 → ( 𝑆 − 𝑇 ) = ( 𝑈 − 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		pcval.1	⊢ 𝑆 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < )
2		pcval.2	⊢ 𝑇 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < )
3		pceu.3	⊢ 𝑈 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } , ℝ , < )
4		pceu.4	⊢ 𝑉 = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } , ℝ , < )
5		pceu.5	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
6		pceu.6	⊢ ( 𝜑 → 𝑁 ≠ 0 )
7		pceu.7	⊢ ( 𝜑 → ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) )
8		pceu.8	⊢ ( 𝜑 → 𝑁 = ( 𝑥 / 𝑦 ) )
9		pceu.9	⊢ ( 𝜑 → ( 𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ ) )
10		pceu.10	⊢ ( 𝜑 → 𝑁 = ( 𝑠 / 𝑡 ) )
11	7	simprd	⊢ ( 𝜑 → 𝑦 ∈ ℕ )
12	11	nncnd	⊢ ( 𝜑 → 𝑦 ∈ ℂ )
13	9	simpld	⊢ ( 𝜑 → 𝑠 ∈ ℤ )
14	13	zcnd	⊢ ( 𝜑 → 𝑠 ∈ ℂ )
15	12 14	mulcomd	⊢ ( 𝜑 → ( 𝑦 · 𝑠 ) = ( 𝑠 · 𝑦 ) )
16	10 8	eqtr3d	⊢ ( 𝜑 → ( 𝑠 / 𝑡 ) = ( 𝑥 / 𝑦 ) )
17	9	simprd	⊢ ( 𝜑 → 𝑡 ∈ ℕ )
18	17	nncnd	⊢ ( 𝜑 → 𝑡 ∈ ℂ )
19	7	simpld	⊢ ( 𝜑 → 𝑥 ∈ ℤ )
20	19	zcnd	⊢ ( 𝜑 → 𝑥 ∈ ℂ )
21	17	nnne0d	⊢ ( 𝜑 → 𝑡 ≠ 0 )
22	11	nnne0d	⊢ ( 𝜑 → 𝑦 ≠ 0 )
23	14 18 20 12 21 22	divmuleqd	⊢ ( 𝜑 → ( ( 𝑠 / 𝑡 ) = ( 𝑥 / 𝑦 ) ↔ ( 𝑠 · 𝑦 ) = ( 𝑥 · 𝑡 ) ) )
24	16 23	mpbid	⊢ ( 𝜑 → ( 𝑠 · 𝑦 ) = ( 𝑥 · 𝑡 ) )
25	15 24	eqtrd	⊢ ( 𝜑 → ( 𝑦 · 𝑠 ) = ( 𝑥 · 𝑡 ) )
26	25	breq2d	⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑧 ) ∥ ( 𝑦 · 𝑠 ) ↔ ( 𝑃 ↑ 𝑧 ) ∥ ( 𝑥 · 𝑡 ) ) )
27	26	rabbidv	⊢ ( 𝜑 → { 𝑧 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑧 ) ∥ ( 𝑦 · 𝑠 ) } = { 𝑧 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑧 ) ∥ ( 𝑥 · 𝑡 ) } )
28		oveq2	⊢ ( 𝑛 = 𝑧 → ( 𝑃 ↑ 𝑛 ) = ( 𝑃 ↑ 𝑧 ) )
29	28	breq1d	⊢ ( 𝑛 = 𝑧 → ( ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑦 · 𝑠 ) ↔ ( 𝑃 ↑ 𝑧 ) ∥ ( 𝑦 · 𝑠 ) ) )
30	29	cbvrabv	⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑦 · 𝑠 ) } = { 𝑧 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑧 ) ∥ ( 𝑦 · 𝑠 ) }
31	28	breq1d	⊢ ( 𝑛 = 𝑧 → ( ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑥 · 𝑡 ) ↔ ( 𝑃 ↑ 𝑧 ) ∥ ( 𝑥 · 𝑡 ) ) )
32	31	cbvrabv	⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑥 · 𝑡 ) } = { 𝑧 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑧 ) ∥ ( 𝑥 · 𝑡 ) }
33	27 30 32	3eqtr4g	⊢ ( 𝜑 → { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑦 · 𝑠 ) } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑥 · 𝑡 ) } )
34	33	supeq1d	⊢ ( 𝜑 → sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑦 · 𝑠 ) } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑥 · 𝑡 ) } , ℝ , < ) )
35	11	nnzd	⊢ ( 𝜑 → 𝑦 ∈ ℤ )
36	18 21	div0d	⊢ ( 𝜑 → ( 0 / 𝑡 ) = 0 )
37		oveq1	⊢ ( 𝑠 = 0 → ( 𝑠 / 𝑡 ) = ( 0 / 𝑡 ) )
38	37	eqeq1d	⊢ ( 𝑠 = 0 → ( ( 𝑠 / 𝑡 ) = 0 ↔ ( 0 / 𝑡 ) = 0 ) )
39	36 38	syl5ibrcom	⊢ ( 𝜑 → ( 𝑠 = 0 → ( 𝑠 / 𝑡 ) = 0 ) )
40	10	eqeq1d	⊢ ( 𝜑 → ( 𝑁 = 0 ↔ ( 𝑠 / 𝑡 ) = 0 ) )
41	39 40	sylibrd	⊢ ( 𝜑 → ( 𝑠 = 0 → 𝑁 = 0 ) )
42	41	necon3d	⊢ ( 𝜑 → ( 𝑁 ≠ 0 → 𝑠 ≠ 0 ) )
43	6 42	mpd	⊢ ( 𝜑 → 𝑠 ≠ 0 )
44		eqid	⊢ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑦 · 𝑠 ) } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑦 · 𝑠 ) } , ℝ , < )
45	2 3 44	pcpremul	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑠 ≠ 0 ) ) → ( 𝑇 + 𝑈 ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑦 · 𝑠 ) } , ℝ , < ) )
46	5 35 22 13 43 45	syl122anc	⊢ ( 𝜑 → ( 𝑇 + 𝑈 ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑦 · 𝑠 ) } , ℝ , < ) )
47	12 22	div0d	⊢ ( 𝜑 → ( 0 / 𝑦 ) = 0 )
48		oveq1	⊢ ( 𝑥 = 0 → ( 𝑥 / 𝑦 ) = ( 0 / 𝑦 ) )
49	48	eqeq1d	⊢ ( 𝑥 = 0 → ( ( 𝑥 / 𝑦 ) = 0 ↔ ( 0 / 𝑦 ) = 0 ) )
50	47 49	syl5ibrcom	⊢ ( 𝜑 → ( 𝑥 = 0 → ( 𝑥 / 𝑦 ) = 0 ) )
51	8	eqeq1d	⊢ ( 𝜑 → ( 𝑁 = 0 ↔ ( 𝑥 / 𝑦 ) = 0 ) )
52	50 51	sylibrd	⊢ ( 𝜑 → ( 𝑥 = 0 → 𝑁 = 0 ) )
53	52	necon3d	⊢ ( 𝜑 → ( 𝑁 ≠ 0 → 𝑥 ≠ 0 ) )
54	6 53	mpd	⊢ ( 𝜑 → 𝑥 ≠ 0 )
55	17	nnzd	⊢ ( 𝜑 → 𝑡 ∈ ℤ )
56		eqid	⊢ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑥 · 𝑡 ) } , ℝ , < ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑥 · 𝑡 ) } , ℝ , < )
57	1 4 56	pcpremul	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑡 ∈ ℤ ∧ 𝑡 ≠ 0 ) ) → ( 𝑆 + 𝑉 ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑥 · 𝑡 ) } , ℝ , < ) )
58	5 19 54 55 21 57	syl122anc	⊢ ( 𝜑 → ( 𝑆 + 𝑉 ) = sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ ( 𝑥 · 𝑡 ) } , ℝ , < ) )
59	34 46 58	3eqtr4d	⊢ ( 𝜑 → ( 𝑇 + 𝑈 ) = ( 𝑆 + 𝑉 ) )
60		prmuz2	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
61	5 60	syl	⊢ ( 𝜑 → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
62		eqid	⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑦 }
63	62 2	pcprecl	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ) ) → ( 𝑇 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑇 ) ∥ 𝑦 ) )
64	63	simpld	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ) ) → 𝑇 ∈ ℕ0 )
65	61 35 22 64	syl12anc	⊢ ( 𝜑 → 𝑇 ∈ ℕ0 )
66	65	nn0cnd	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
67		eqid	⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑠 }
68	67 3	pcprecl	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑠 ≠ 0 ) ) → ( 𝑈 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑈 ) ∥ 𝑠 ) )
69	68	simpld	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑠 ∈ ℤ ∧ 𝑠 ≠ 0 ) ) → 𝑈 ∈ ℕ0 )
70	61 13 43 69	syl12anc	⊢ ( 𝜑 → 𝑈 ∈ ℕ0 )
71	70	nn0cnd	⊢ ( 𝜑 → 𝑈 ∈ ℂ )
72		eqid	⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑥 }
73	72 1	pcprecl	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) → ( 𝑆 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑆 ) ∥ 𝑥 ) )
74	73	simpld	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) → 𝑆 ∈ ℕ0 )
75	61 19 54 74	syl12anc	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
76	75	nn0cnd	⊢ ( 𝜑 → 𝑆 ∈ ℂ )
77		eqid	⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 } = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑡 }
78	77 4	pcprecl	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑡 ∈ ℤ ∧ 𝑡 ≠ 0 ) ) → ( 𝑉 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑉 ) ∥ 𝑡 ) )
79	78	simpld	⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑡 ∈ ℤ ∧ 𝑡 ≠ 0 ) ) → 𝑉 ∈ ℕ0 )
80	61 55 21 79	syl12anc	⊢ ( 𝜑 → 𝑉 ∈ ℕ0 )
81	80	nn0cnd	⊢ ( 𝜑 → 𝑉 ∈ ℂ )
82	66 71 76 81	addsubeq4d	⊢ ( 𝜑 → ( ( 𝑇 + 𝑈 ) = ( 𝑆 + 𝑉 ) ↔ ( 𝑆 − 𝑇 ) = ( 𝑈 − 𝑉 ) ) )
83	59 82	mpbid	⊢ ( 𝜑 → ( 𝑆 − 𝑇 ) = ( 𝑈 − 𝑉 ) )