Metamath Proof Explorer


Theorem axpaschlem

Description: Lemma for axpasch . Set up coefficents used in the proof. (Contributed by Scott Fenton, 5-Jun-2013)

Ref Expression
Assertion axpaschlem T01S01r01p01p=1r1Tr=1p1S1rT=1pS

Proof

Step Hyp Ref Expression
1 1re 1
2 elicc01 T01T0TT1
3 2 simp1bi T01T
4 3 ad2antrl S=0T01S01T
5 resubcl 1T1T
6 1 4 5 sylancr S=0T01S011T
7 6 recnd S=0T01S011T
8 7 mul02d S=0T01S0101T=0
9 8 eqcomd S=0T01S010=01T
10 elicc01 S01S0SS1
11 10 simp1bi S01S
12 11 ad2antll S=0T01S01S
13 resubcl 1S1S
14 1 12 13 sylancr S=0T01S011S
15 14 recnd S=0T01S011S
16 15 mulid2d S=0T01S0111S=1S
17 oveq2 S=01S=10
18 17 adantr S=0T01S011S=10
19 1m0e1 10=1
20 18 19 eqtrdi S=0T01S011S=1
21 16 20 eqtr2d S=0T01S011=11S
22 4 recnd S=0T01S01T
23 22 mul02d S=0T01S010T=0
24 oveq2 S=01S=10
25 24 adantr S=0T01S011S=10
26 ax-1cn 1
27 26 mul01i 10=0
28 25 27 eqtrdi S=0T01S011S=0
29 23 28 eqtr4d S=0T01S010T=1S
30 1elunit 101
31 0elunit 001
32 oveq2 r=11r=11
33 1m1e0 11=0
34 32 33 eqtrdi r=11r=0
35 34 oveq1d r=11r1T=01T
36 35 eqeq2d r=1p=1r1Tp=01T
37 eqeq1 r=1r=1p1S1=1p1S
38 34 oveq1d r=11rT=0T
39 38 eqeq1d r=11rT=1pS0T=1pS
40 36 37 39 3anbi123d r=1p=1r1Tr=1p1S1rT=1pSp=01T1=1p1S0T=1pS
41 eqeq1 p=0p=01T0=01T
42 oveq2 p=01p=10
43 42 19 eqtrdi p=01p=1
44 43 oveq1d p=01p1S=11S
45 44 eqeq2d p=01=1p1S1=11S
46 43 oveq1d p=01pS=1S
47 46 eqeq2d p=00T=1pS0T=1S
48 41 45 47 3anbi123d p=0p=01T1=1p1S0T=1pS0=01T1=11S0T=1S
49 40 48 rspc2ev 1010010=01T1=11S0T=1Sr01p01p=1r1Tr=1p1S1rT=1pS
50 30 31 49 mp3an12 0=01T1=11S0T=1Sr01p01p=1r1Tr=1p1S1rT=1pS
51 9 21 29 50 syl3anc S=0T01S01r01p01p=1r1Tr=1p1S1rT=1pS
52 51 ex S=0T01S01r01p01p=1r1Tr=1p1S1rT=1pS
53 3 ad2antrl S0T01S01T
54 11 ad2antll S0T01S01S
55 54 53 remulcld S0T01S01ST
56 53 55 resubcld S0T01S01TST
57 54 53 readdcld S0T01S01S+T
58 57 55 resubcld S0T01S01S+T-ST
59 1red S0T01S011
60 2 simp2bi T010T
61 60 ad2antrl S0T01S010T
62 10 simp3bi S01S1
63 62 ad2antll S0T01S01S1
64 54 59 53 61 63 lemul1ad S0T01S01ST1T
65 53 recnd S0T01S01T
66 65 mulid2d S0T01S011T=T
67 64 66 breqtrd S0T01S01STT
68 10 simp2bi S010S
69 68 ad2antll S0T01S010S
70 simpl S0T01S01S0
71 54 69 70 ne0gt0d S0T01S010<S
72 54 53 ltaddpos2d S0T01S010<ST<S+T
73 71 72 mpbid S0T01S01T<S+T
74 55 53 57 67 73 lelttrd S0T01S01ST<S+T
75 55 57 posdifd S0T01S01ST<S+T0<S+T-ST
76 74 75 mpbid S0T01S010<S+T-ST
77 76 gt0ne0d S0T01S01S+T-ST0
78 56 58 77 redivcld S0T01S01TSTS+T-ST
79 53 55 subge0d S0T01S010TSTSTT
80 67 79 mpbird S0T01S010TST
81 divge0 TST0TSTS+T-ST0<S+T-ST0TSTS+T-ST
82 56 80 58 76 81 syl22anc S0T01S010TSTS+T-ST
83 53 57 73 ltled S0T01S01TS+T
84 53 57 55 83 lesub1dd S0T01S01TSTS+T-ST
85 58 recnd S0T01S01S+T-ST
86 85 mulid2d S0T01S011S+T-ST=S+T-ST
87 84 86 breqtrrd S0T01S01TST1S+T-ST
88 ledivmul2 TST1S+T-ST0<S+T-STTSTS+T-ST1TST1S+T-ST
89 56 59 58 76 88 syl112anc S0T01S01TSTS+T-ST1TST1S+T-ST
90 87 89 mpbird S0T01S01TSTS+T-ST1
91 elicc01 TSTS+T-ST01TSTS+T-ST0TSTS+T-STTSTS+T-ST1
92 78 82 90 91 syl3anbrc S0T01S01TSTS+T-ST01
93 54 55 resubcld S0T01S01SST
94 93 58 77 redivcld S0T01S01SSTS+T-ST
95 2 simp3bi T01T1
96 95 ad2antrl S0T01S01T1
97 53 59 54 69 96 lemul2ad S0T01S01STS1
98 54 recnd S0T01S01S
99 98 mulid1d S0T01S01S1=S
100 97 99 breqtrd S0T01S01STS
101 54 55 subge0d S0T01S010SSTSTS
102 100 101 mpbird S0T01S010SST
103 divge0 SST0SSTS+T-ST0<S+T-ST0SSTS+T-ST
104 93 102 58 76 103 syl22anc S0T01S010SSTS+T-ST
105 54 53 addge01d S0T01S010TSS+T
106 61 105 mpbid S0T01S01SS+T
107 54 57 55 106 lesub1dd S0T01S01SSTS+T-ST
108 107 86 breqtrrd S0T01S01SST1S+T-ST
109 ledivmul2 SST1S+T-ST0<S+T-STSSTS+T-ST1SST1S+T-ST
110 93 59 58 76 109 syl112anc S0T01S01SSTS+T-ST1SST1S+T-ST
111 108 110 mpbird S0T01S01SSTS+T-ST1
112 elicc01 SSTS+T-ST01SSTS+T-ST0SSTS+T-STSSTS+T-ST1
113 94 104 111 112 syl3anbrc S0T01S01SSTS+T-ST01
114 1 53 5 sylancr S0T01S011T
115 114 recnd S0T01S011T
116 98 115 85 77 div23d S0T01S01S1TS+T-ST=SS+T-ST1T
117 subdi S1TS1T=S1ST
118 26 117 mp3an2 STS1T=S1ST
119 98 65 118 syl2anc S0T01S01S1T=S1ST
120 99 oveq1d S0T01S01S1ST=SST
121 119 120 eqtrd S0T01S01S1T=SST
122 121 oveq1d S0T01S01S1TS+T-ST=SSTS+T-ST
123 56 recnd S0T01S01TST
124 85 123 85 77 divsubdird S0T01S01S+T-ST-TSTS+T-ST=S+T-STS+T-STTSTS+T-ST
125 57 recnd S0T01S01S+T
126 55 recnd S0T01S01ST
127 125 65 126 nnncan2d S0T01S01S+T-ST-TST=S+T-T
128 98 65 pncand S0T01S01S+T-T=S
129 127 128 eqtrd S0T01S01S+T-ST-TST=S
130 129 oveq1d S0T01S01S+T-ST-TSTS+T-ST=SS+T-ST
131 85 77 dividd S0T01S01S+T-STS+T-ST=1
132 131 oveq1d S0T01S01S+T-STS+T-STTSTS+T-ST=1TSTS+T-ST
133 124 130 132 3eqtr3d S0T01S01SS+T-ST=1TSTS+T-ST
134 133 oveq1d S0T01S01SS+T-ST1T=1TSTS+T-ST1T
135 116 122 134 3eqtr3d S0T01S01SSTS+T-ST=1TSTS+T-ST1T
136 1 54 13 sylancr S0T01S011S
137 136 recnd S0T01S011S
138 65 137 85 77 div23d S0T01S01T1SS+T-ST=TS+T-ST1S
139 subdi T1ST1S=T1TS
140 26 139 mp3an2 TST1S=T1TS
141 65 98 140 syl2anc S0T01S01T1S=T1TS
142 65 mulid1d S0T01S01T1=T
143 65 98 mulcomd S0T01S01TS=ST
144 142 143 oveq12d S0T01S01T1TS=TST
145 141 144 eqtrd S0T01S01T1S=TST
146 145 oveq1d S0T01S01T1SS+T-ST=TSTS+T-ST
147 93 recnd S0T01S01SST
148 85 147 85 77 divsubdird S0T01S01S+T-ST-SSTS+T-ST=S+T-STS+T-STSSTS+T-ST
149 125 98 126 nnncan2d S0T01S01S+T-ST-SST=S+T-S
150 98 65 pncan2d S0T01S01S+T-S=T
151 149 150 eqtrd S0T01S01S+T-ST-SST=T
152 151 oveq1d S0T01S01S+T-ST-SSTS+T-ST=TS+T-ST
153 131 oveq1d S0T01S01S+T-STS+T-STSSTS+T-ST=1SSTS+T-ST
154 148 152 153 3eqtr3d S0T01S01TS+T-ST=1SSTS+T-ST
155 154 oveq1d S0T01S01TS+T-ST1S=1SSTS+T-ST1S
156 138 146 155 3eqtr3d S0T01S01TSTS+T-ST=1SSTS+T-ST1S
157 98 65 mulcomd S0T01S01ST=TS
158 157 oveq1d S0T01S01STS+T-ST=TSS+T-ST
159 98 65 85 77 div23d S0T01S01STS+T-ST=SS+T-STT
160 133 oveq1d S0T01S01SS+T-STT=1TSTS+T-STT
161 159 160 eqtrd S0T01S01STS+T-ST=1TSTS+T-STT
162 65 98 85 77 div23d S0T01S01TSS+T-ST=TS+T-STS
163 154 oveq1d S0T01S01TS+T-STS=1SSTS+T-STS
164 162 163 eqtrd S0T01S01TSS+T-ST=1SSTS+T-STS
165 158 161 164 3eqtr3d S0T01S011TSTS+T-STT=1SSTS+T-STS
166 oveq2 r=TSTS+T-ST1r=1TSTS+T-ST
167 166 oveq1d r=TSTS+T-ST1r1T=1TSTS+T-ST1T
168 167 eqeq2d r=TSTS+T-STp=1r1Tp=1TSTS+T-ST1T
169 eqeq1 r=TSTS+T-STr=1p1STSTS+T-ST=1p1S
170 166 oveq1d r=TSTS+T-ST1rT=1TSTS+T-STT
171 170 eqeq1d r=TSTS+T-ST1rT=1pS1TSTS+T-STT=1pS
172 168 169 171 3anbi123d r=TSTS+T-STp=1r1Tr=1p1S1rT=1pSp=1TSTS+T-ST1TTSTS+T-ST=1p1S1TSTS+T-STT=1pS
173 eqeq1 p=SSTS+T-STp=1TSTS+T-ST1TSSTS+T-ST=1TSTS+T-ST1T
174 oveq2 p=SSTS+T-ST1p=1SSTS+T-ST
175 174 oveq1d p=SSTS+T-ST1p1S=1SSTS+T-ST1S
176 175 eqeq2d p=SSTS+T-STTSTS+T-ST=1p1STSTS+T-ST=1SSTS+T-ST1S
177 174 oveq1d p=SSTS+T-ST1pS=1SSTS+T-STS
178 177 eqeq2d p=SSTS+T-ST1TSTS+T-STT=1pS1TSTS+T-STT=1SSTS+T-STS
179 173 176 178 3anbi123d p=SSTS+T-STp=1TSTS+T-ST1TTSTS+T-ST=1p1S1TSTS+T-STT=1pSSSTS+T-ST=1TSTS+T-ST1TTSTS+T-ST=1SSTS+T-ST1S1TSTS+T-STT=1SSTS+T-STS
180 172 179 rspc2ev TSTS+T-ST01SSTS+T-ST01SSTS+T-ST=1TSTS+T-ST1TTSTS+T-ST=1SSTS+T-ST1S1TSTS+T-STT=1SSTS+T-STSr01p01p=1r1Tr=1p1S1rT=1pS
181 92 113 135 156 165 180 syl113anc S0T01S01r01p01p=1r1Tr=1p1S1rT=1pS
182 181 ex S0T01S01r01p01p=1r1Tr=1p1S1rT=1pS
183 52 182 pm2.61ine T01S01r01p01p=1r1Tr=1p1S1rT=1pS