Metamath Proof Explorer


Theorem 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 φ P
pcaddlem.2 φ A = P M R S
pcaddlem.3 φ B = P N T U
pcaddlem.4 φ N M
pcaddlem.5 φ R ¬ P R
pcaddlem.6 φ S ¬ P S
pcaddlem.7 φ T ¬ P T
pcaddlem.8 φ U ¬ P U
Assertion pcaddlem φ M P pCnt A + B

Proof

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