pcaddlem

Description: Lemma for pcadd . The original numbers A and B have been decomposed using the prime count function as ( P ^ M ) x. ( R / S ) where R , S are both not divisible by P and M = ( P pCnt A ) , and similarly for B . (Contributed by Mario Carneiro, 9-Sep-2014)

	Ref	Expression
Hypotheses	pcaddlem.1	$⊢ φ \to P \in ℙ$
	pcaddlem.2	$⊢ φ \to A = P^{M} (\frac{R}{S})$
	pcaddlem.3	$⊢ φ \to B = P^{N} (\frac{T}{U})$
	pcaddlem.4	$⊢ φ \to N \in ℤ_{\geq M}$
	pcaddlem.5	$⊢ φ \to (R \in ℤ \land \neg P ∥ R)$
	pcaddlem.6	$⊢ φ \to (S \in ℕ \land \neg P ∥ S)$
	pcaddlem.7	$⊢ φ \to (T \in ℤ \land \neg P ∥ T)$
	pcaddlem.8	$⊢ φ \to (U \in ℕ \land \neg P ∥ U)$
Assertion	pcaddlem	$⊢ φ \to M \leq P pCnt (A + B)$

Proof

Step	Hyp	Ref	Expression
1		pcaddlem.1	$⊢ φ \to P \in ℙ$
2		pcaddlem.2	$⊢ φ \to A = P^{M} (\frac{R}{S})$
3		pcaddlem.3	$⊢ φ \to B = P^{N} (\frac{T}{U})$
4		pcaddlem.4	$⊢ φ \to N \in ℤ_{\geq M}$
5		pcaddlem.5	$⊢ φ \to (R \in ℤ \land \neg P ∥ R)$
6		pcaddlem.6	$⊢ φ \to (S \in ℕ \land \neg P ∥ S)$
7		pcaddlem.7	$⊢ φ \to (T \in ℤ \land \neg P ∥ T)$
8		pcaddlem.8	$⊢ φ \to (U \in ℕ \land \neg P ∥ U)$
9		oveq2	$⊢ A + B = 0 \to P pCnt (A + B) = P pCnt 0$
10	9	breq2d	$⊢ A + B = 0 \to (M \leq P pCnt (A + B) \leftrightarrow M \leq P pCnt 0)$
11		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
12	4 11	syl	$⊢ φ \to M \in ℤ$
13	12	zred	$⊢ φ \to M \in ℝ$
14	13	adantr	$⊢ (φ \land A + B \neq 0) \to M \in ℝ$
15		prmnn	$⊢ P \in ℙ \to P \in ℕ$
16	1 15	syl	$⊢ φ \to P \in ℕ$
17	16	nncnd	$⊢ φ \to P \in ℂ$
18	16	nnne0d	$⊢ φ \to P \neq 0$
19		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
20	4 19	syl	$⊢ φ \to N \in ℤ$
21	20 12	zsubcld	$⊢ φ \to N - M \in ℤ$
22	17 18 21	expclzd	$⊢ φ \to P^{N - M} \in ℂ$
23	7	simpld	$⊢ φ \to T \in ℤ$
24	23	zcnd	$⊢ φ \to T \in ℂ$
25	8	simpld	$⊢ φ \to U \in ℕ$
26	25	nncnd	$⊢ φ \to U \in ℂ$
27	25	nnne0d	$⊢ φ \to U \neq 0$
28	22 24 26 27	divassd	$⊢ φ \to \frac{P^{N - M} T}{U} = P^{N - M} (\frac{T}{U})$
29	28	oveq2d	$⊢ φ \to (\frac{R}{S}) + (\frac{P^{N - M} T}{U}) = (\frac{R}{S}) + P^{N - M} (\frac{T}{U})$
30	5	simpld	$⊢ φ \to R \in ℤ$
31	30	zcnd	$⊢ φ \to R \in ℂ$
32	6	simpld	$⊢ φ \to S \in ℕ$
33	32	nncnd	$⊢ φ \to S \in ℂ$
34	22 24	mulcld	$⊢ φ \to P^{N - M} T \in ℂ$
35	32	nnne0d	$⊢ φ \to S \neq 0$
36	31 33 34 26 35 27	divadddivd	$⊢ φ \to (\frac{R}{S}) + (\frac{P^{N - M} T}{U}) = \frac{R U + P^{N - M} T S}{S U}$
37	29 36	eqtr3d	$⊢ φ \to (\frac{R}{S}) + P^{N - M} (\frac{T}{U}) = \frac{R U + P^{N - M} T S}{S U}$
38	37	oveq2d	$⊢ φ \to P pCnt ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})) = P pCnt (\frac{R U + P^{N - M} T S}{S U})$
39	38	adantr	$⊢ (φ \land A + B \neq 0) \to P pCnt ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})) = P pCnt (\frac{R U + P^{N - M} T S}{S U})$
40	1	adantr	$⊢ (φ \land A + B \neq 0) \to P \in ℙ$
41	25	nnzd	$⊢ φ \to U \in ℤ$
42	30 41	zmulcld	$⊢ φ \to R U \in ℤ$
43		uznn0sub	$⊢ N \in ℤ_{\geq M} \to N - M \in ℕ_{0}$
44	4 43	syl	$⊢ φ \to N - M \in ℕ_{0}$
45	16 44	nnexpcld	$⊢ φ \to P^{N - M} \in ℕ$
46	45	nnzd	$⊢ φ \to P^{N - M} \in ℤ$
47	46 23	zmulcld	$⊢ φ \to P^{N - M} T \in ℤ$
48	32	nnzd	$⊢ φ \to S \in ℤ$
49	47 48	zmulcld	$⊢ φ \to P^{N - M} T S \in ℤ$
50	42 49	zaddcld	$⊢ φ \to R U + P^{N - M} T S \in ℤ$
51	50	adantr	$⊢ (φ \land A + B \neq 0) \to R U + P^{N - M} T S \in ℤ$
52	17 18 12	expclzd	$⊢ φ \to P^{M} \in ℂ$
53	52	mul01d	$⊢ φ \to P^{M} \cdot 0 = 0$
54		oveq2	$⊢ (\frac{R}{S}) + P^{N - M} (\frac{T}{U}) = 0 \to P^{M} ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})) = P^{M} \cdot 0$
55	54	eqeq1d	$⊢ (\frac{R}{S}) + P^{N - M} (\frac{T}{U}) = 0 \to (P^{M} ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})) = 0 \leftrightarrow P^{M} \cdot 0 = 0)$
56	53 55	syl5ibrcom	$⊢ φ \to ((\frac{R}{S}) + P^{N - M} (\frac{T}{U}) = 0 \to P^{M} ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})) = 0)$
57	56	necon3d	$⊢ φ \to (P^{M} ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})) \neq 0 \to (\frac{R}{S}) + P^{N - M} (\frac{T}{U}) \neq 0)$
58	31 33 35	divcld	$⊢ φ \to \frac{R}{S} \in ℂ$
59	24 26 27	divcld	$⊢ φ \to \frac{T}{U} \in ℂ$
60	22 59	mulcld	$⊢ φ \to P^{N - M} (\frac{T}{U}) \in ℂ$
61	52 58 60	adddid	$⊢ φ \to P^{M} ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})) = P^{M} (\frac{R}{S}) + P^{M} P^{N - M} (\frac{T}{U})$
62	12	zcnd	$⊢ φ \to M \in ℂ$
63	20	zcnd	$⊢ φ \to N \in ℂ$
64	62 63	pncan3d	$⊢ φ \to M + N - M = N$
65	64	oveq2d	$⊢ φ \to P^{M + N - M} = P^{N}$
66		expaddz	$⊢ ((P \in ℂ \land P \neq 0) \land (M \in ℤ \land N - M \in ℤ)) \to P^{M + N - M} = P^{M} P^{N - M}$
67	17 18 12 21 66	syl22anc	$⊢ φ \to P^{M + N - M} = P^{M} P^{N - M}$
68	65 67	eqtr3d	$⊢ φ \to P^{N} = P^{M} P^{N - M}$
69	68	oveq1d	$⊢ φ \to P^{N} (\frac{T}{U}) = P^{M} P^{N - M} (\frac{T}{U})$
70	52 22 59	mulassd	$⊢ φ \to P^{M} P^{N - M} (\frac{T}{U}) = P^{M} P^{N - M} (\frac{T}{U})$
71	3 69 70	3eqtrd	$⊢ φ \to B = P^{M} P^{N - M} (\frac{T}{U})$
72	2 71	oveq12d	$⊢ φ \to A + B = P^{M} (\frac{R}{S}) + P^{M} P^{N - M} (\frac{T}{U})$
73	61 72	eqtr4d	$⊢ φ \to P^{M} ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})) = A + B$
74	73	neeq1d	$⊢ φ \to (P^{M} ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})) \neq 0 \leftrightarrow A + B \neq 0)$
75	37	neeq1d	$⊢ φ \to ((\frac{R}{S}) + P^{N - M} (\frac{T}{U}) \neq 0 \leftrightarrow \frac{R U + P^{N - M} T S}{S U} \neq 0)$
76	57 74 75	3imtr3d	$⊢ φ \to (A + B \neq 0 \to \frac{R U + P^{N - M} T S}{S U} \neq 0)$
77	32 25	nnmulcld	$⊢ φ \to S U \in ℕ$
78	77	nncnd	$⊢ φ \to S U \in ℂ$
79	77	nnne0d	$⊢ φ \to S U \neq 0$
80	78 79	div0d	$⊢ φ \to \frac{0}{S U} = 0$
81		oveq1	$⊢ R U + P^{N - M} T S = 0 \to \frac{R U + P^{N - M} T S}{S U} = \frac{0}{S U}$
82	81	eqeq1d	$⊢ R U + P^{N - M} T S = 0 \to (\frac{R U + P^{N - M} T S}{S U} = 0 \leftrightarrow \frac{0}{S U} = 0)$
83	80 82	syl5ibrcom	$⊢ φ \to (R U + P^{N - M} T S = 0 \to \frac{R U + P^{N - M} T S}{S U} = 0)$
84	83	necon3d	$⊢ φ \to (\frac{R U + P^{N - M} T S}{S U} \neq 0 \to R U + P^{N - M} T S \neq 0)$
85	76 84	syld	$⊢ φ \to (A + B \neq 0 \to R U + P^{N - M} T S \neq 0)$
86	85	imp	$⊢ (φ \land A + B \neq 0) \to R U + P^{N - M} T S \neq 0$
87	77	adantr	$⊢ (φ \land A + B \neq 0) \to S U \in ℕ$
88		pcdiv	$⊢ (P \in ℙ \land (R U + P^{N - M} T S \in ℤ \land R U + P^{N - M} T S \neq 0) \land S U \in ℕ) \to P pCnt (\frac{R U + P^{N - M} T S}{S U}) = (P pCnt (R U + P^{N - M} T S)) - (P pCnt S U)$
89	40 51 86 87 88	syl121anc	$⊢ (φ \land A + B \neq 0) \to P pCnt (\frac{R U + P^{N - M} T S}{S U}) = (P pCnt (R U + P^{N - M} T S)) - (P pCnt S U)$
90		pcmul	$⊢ (P \in ℙ \land (S \in ℤ \land S \neq 0) \land (U \in ℤ \land U \neq 0)) \to P pCnt S U = (P pCnt S) + (P pCnt U)$
91	1 48 35 41 27 90	syl122anc	$⊢ φ \to P pCnt S U = (P pCnt S) + (P pCnt U)$
92	6	simprd	$⊢ φ \to \neg P ∥ S$
93		pceq0	$⊢ (P \in ℙ \land S \in ℕ) \to (P pCnt S = 0 \leftrightarrow \neg P ∥ S)$
94	1 32 93	syl2anc	$⊢ φ \to (P pCnt S = 0 \leftrightarrow \neg P ∥ S)$
95	92 94	mpbird	$⊢ φ \to P pCnt S = 0$
96	8	simprd	$⊢ φ \to \neg P ∥ U$
97		pceq0	$⊢ (P \in ℙ \land U \in ℕ) \to (P pCnt U = 0 \leftrightarrow \neg P ∥ U)$
98	1 25 97	syl2anc	$⊢ φ \to (P pCnt U = 0 \leftrightarrow \neg P ∥ U)$
99	96 98	mpbird	$⊢ φ \to P pCnt U = 0$
100	95 99	oveq12d	$⊢ φ \to (P pCnt S) + (P pCnt U) = 0 + 0$
101		00id	$⊢ 0 + 0 = 0$
102	100 101	eqtrdi	$⊢ φ \to (P pCnt S) + (P pCnt U) = 0$
103	91 102	eqtrd	$⊢ φ \to P pCnt S U = 0$
104	103	oveq2d	$⊢ φ \to (P pCnt (R U + P^{N - M} T S)) - (P pCnt S U) = (P pCnt (R U + P^{N - M} T S)) - 0$
105	104	adantr	$⊢ (φ \land A + B \neq 0) \to (P pCnt (R U + P^{N - M} T S)) - (P pCnt S U) = (P pCnt (R U + P^{N - M} T S)) - 0$
106		pczcl	$⊢ (P \in ℙ \land (R U + P^{N - M} T S \in ℤ \land R U + P^{N - M} T S \neq 0)) \to P pCnt (R U + P^{N - M} T S) \in ℕ_{0}$
107	40 51 86 106	syl12anc	$⊢ (φ \land A + B \neq 0) \to P pCnt (R U + P^{N - M} T S) \in ℕ_{0}$
108	107	nn0cnd	$⊢ (φ \land A + B \neq 0) \to P pCnt (R U + P^{N - M} T S) \in ℂ$
109	108	subid1d	$⊢ (φ \land A + B \neq 0) \to (P pCnt (R U + P^{N - M} T S)) - 0 = P pCnt (R U + P^{N - M} T S)$
110	105 109	eqtrd	$⊢ (φ \land A + B \neq 0) \to (P pCnt (R U + P^{N - M} T S)) - (P pCnt S U) = P pCnt (R U + P^{N - M} T S)$
111	39 89 110	3eqtrd	$⊢ (φ \land A + B \neq 0) \to P pCnt ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})) = P pCnt (R U + P^{N - M} T S)$
112	111 107	eqeltrd	$⊢ (φ \land A + B \neq 0) \to P pCnt ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})) \in ℕ_{0}$
113		nn0addge1	$⊢ (M \in ℝ \land P pCnt ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})) \in ℕ_{0}) \to M \leq M + (P pCnt ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})))$
114	14 112 113	syl2anc	$⊢ (φ \land A + B \neq 0) \to M \leq M + (P pCnt ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})))$
115		nnq	$⊢ P \in ℕ \to P \in ℚ$
116	16 115	syl	$⊢ φ \to P \in ℚ$
117		qexpclz	$⊢ (P \in ℚ \land P \neq 0 \land M \in ℤ) \to P^{M} \in ℚ$
118	116 18 12 117	syl3anc	$⊢ φ \to P^{M} \in ℚ$
119	118	adantr	$⊢ (φ \land A + B \neq 0) \to P^{M} \in ℚ$
120	17 18 12	expne0d	$⊢ φ \to P^{M} \neq 0$
121	120	adantr	$⊢ (φ \land A + B \neq 0) \to P^{M} \neq 0$
122		znq	$⊢ (R \in ℤ \land S \in ℕ) \to \frac{R}{S} \in ℚ$
123	30 32 122	syl2anc	$⊢ φ \to \frac{R}{S} \in ℚ$
124		qexpclz	$⊢ (P \in ℚ \land P \neq 0 \land N - M \in ℤ) \to P^{N - M} \in ℚ$
125	116 18 21 124	syl3anc	$⊢ φ \to P^{N - M} \in ℚ$
126		znq	$⊢ (T \in ℤ \land U \in ℕ) \to \frac{T}{U} \in ℚ$
127	23 25 126	syl2anc	$⊢ φ \to \frac{T}{U} \in ℚ$
128		qmulcl	$⊢ (P^{N - M} \in ℚ \land \frac{T}{U} \in ℚ) \to P^{N - M} (\frac{T}{U}) \in ℚ$
129	125 127 128	syl2anc	$⊢ φ \to P^{N - M} (\frac{T}{U}) \in ℚ$
130		qaddcl	$⊢ (\frac{R}{S} \in ℚ \land P^{N - M} (\frac{T}{U}) \in ℚ) \to (\frac{R}{S}) + P^{N - M} (\frac{T}{U}) \in ℚ$
131	123 129 130	syl2anc	$⊢ φ \to (\frac{R}{S}) + P^{N - M} (\frac{T}{U}) \in ℚ$
132	131	adantr	$⊢ (φ \land A + B \neq 0) \to (\frac{R}{S}) + P^{N - M} (\frac{T}{U}) \in ℚ$
133	74 57	sylbird	$⊢ φ \to (A + B \neq 0 \to (\frac{R}{S}) + P^{N - M} (\frac{T}{U}) \neq 0)$
134	133	imp	$⊢ (φ \land A + B \neq 0) \to (\frac{R}{S}) + P^{N - M} (\frac{T}{U}) \neq 0$
135		pcqmul	$⊢ (P \in ℙ \land (P^{M} \in ℚ \land P^{M} \neq 0) \land ((\frac{R}{S}) + P^{N - M} (\frac{T}{U}) \in ℚ \land (\frac{R}{S}) + P^{N - M} (\frac{T}{U}) \neq 0)) \to P pCnt P^{M} ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})) = (P pCnt P^{M}) + (P pCnt ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})))$
136	40 119 121 132 134 135	syl122anc	$⊢ (φ \land A + B \neq 0) \to P pCnt P^{M} ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})) = (P pCnt P^{M}) + (P pCnt ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})))$
137	73	oveq2d	$⊢ φ \to P pCnt P^{M} ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})) = P pCnt (A + B)$
138	137	adantr	$⊢ (φ \land A + B \neq 0) \to P pCnt P^{M} ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})) = P pCnt (A + B)$
139		pcid	$⊢ (P \in ℙ \land M \in ℤ) \to P pCnt P^{M} = M$
140	1 12 139	syl2anc	$⊢ φ \to P pCnt P^{M} = M$
141	140	oveq1d	$⊢ φ \to (P pCnt P^{M}) + (P pCnt ((\frac{R}{S}) + P^{N - M} (\frac{T}{U}))) = M + (P pCnt ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})))$
142	141	adantr	$⊢ (φ \land A + B \neq 0) \to (P pCnt P^{M}) + (P pCnt ((\frac{R}{S}) + P^{N - M} (\frac{T}{U}))) = M + (P pCnt ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})))$
143	136 138 142	3eqtr3d	$⊢ (φ \land A + B \neq 0) \to P pCnt (A + B) = M + (P pCnt ((\frac{R}{S}) + P^{N - M} (\frac{T}{U})))$
144	114 143	breqtrrd	$⊢ (φ \land A + B \neq 0) \to M \leq P pCnt (A + B)$
145	13	rexrd	$⊢ φ \to M \in ℝ^{*}$
146		pnfge	$⊢ M \in ℝ^{*} \to M \leq +∞$
147	145 146	syl	$⊢ φ \to M \leq +∞$
148		pc0	$⊢ P \in ℙ \to P pCnt 0 = +∞$
149	1 148	syl	$⊢ φ \to P pCnt 0 = +∞$
150	147 149	breqtrrd	$⊢ φ \to M \leq P pCnt 0$
151	10 144 150	pm2.61ne	$⊢ φ \to M \leq P pCnt (A + B)$

Metamath Proof Explorer

Theorem pcaddlem

Proof