MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sadcaddlem Unicode version

Theorem sadcaddlem 14107
Description: Lemma for sadcadd 14108. (Contributed by Mario Carneiro, 8-Sep-2016.)
Hypotheses
Ref Expression
sadval.a
sadval.b
sadval.c
sadcp1.n
sadcadd.k
sadcaddlem.1
Assertion
Ref Expression
sadcaddlem
Distinct variable groups:   , ,   , ,   , ,   ,N

Proof of Theorem sadcaddlem
StepHypRef Expression
1 cad1 1465 . . . . 5
21adantl 466 . . . 4
3 2nn 10718 . . . . . . . . . . 11
43a1i 11 . . . . . . . . . 10
5 sadcp1.n . . . . . . . . . 10
64, 5nnexpcld 12331 . . . . . . . . 9
76nnred 10576 . . . . . . . 8
87ad2antrr 725 . . . . . . 7
9 inss1 3717 . . . . . . . . . . . . 13
10 sadval.a . . . . . . . . . . . . 13
119, 10syl5ss 3514 . . . . . . . . . . . 12
12 fzofi 12084 . . . . . . . . . . . . . 14
1312a1i 11 . . . . . . . . . . . . 13
14 inss2 3718 . . . . . . . . . . . . 13
15 ssfi 7760 . . . . . . . . . . . . 13
1613, 14, 15sylancl 662 . . . . . . . . . . . 12
17 elfpw 7842 . . . . . . . . . . . 12
1811, 16, 17sylanbrc 664 . . . . . . . . . . 11
19 bitsf1o 14095 . . . . . . . . . . . . . . 15
20 f1ocnv 5833 . . . . . . . . . . . . . . 15
2119, 20ax-mp 5 . . . . . . . . . . . . . 14
22 sadcadd.k . . . . . . . . . . . . . . 15
23 f1oeq1 5812 . . . . . . . . . . . . . . 15
2422, 23ax-mp 5 . . . . . . . . . . . . . 14
2521, 24mpbir 209 . . . . . . . . . . . . 13
26 f1of 5821 . . . . . . . . . . . . 13
2725, 26ax-mp 5 . . . . . . . . . . . 12
2827ffvelrni 6030 . . . . . . . . . . 11
2918, 28syl 16 . . . . . . . . . 10
30 inss1 3717 . . . . . . . . . . . . 13
31 sadval.b . . . . . . . . . . . . 13
3230, 31syl5ss 3514 . . . . . . . . . . . 12
33 inss2 3718 . . . . . . . . . . . . 13
34 ssfi 7760 . . . . . . . . . . . . 13
3513, 33, 34sylancl 662 . . . . . . . . . . . 12
36 elfpw 7842 . . . . . . . . . . . 12
3732, 35, 36sylanbrc 664 . . . . . . . . . . 11
3827ffvelrni 6030 . . . . . . . . . . 11
3937, 38syl 16 . . . . . . . . . 10
4029, 39nn0addcld 10881 . . . . . . . . 9
4140nn0red 10878 . . . . . . . 8
4241ad2antrr 725 . . . . . . 7
43 2nn0 10837 . . . . . . . . . . . . 13
4443a1i 11 . . . . . . . . . . . 12
455adantr 465 . . . . . . . . . . . 12
4644, 45nn0expcld 12332 . . . . . . . . . . 11
47 0nn0 10835 . . . . . . . . . . . 12
4847a1i 11 . . . . . . . . . . 11
4946, 48ifclda 3973 . . . . . . . . . 10
5043a1i 11 . . . . . . . . . . . 12
515adantr 465 . . . . . . . . . . . 12
5250, 51nn0expcld 12332 . . . . . . . . . . 11
5347a1i 11 . . . . . . . . . . 11
5452, 53ifclda 3973 . . . . . . . . . 10
5549, 54nn0addcld 10881 . . . . . . . . 9
5655nn0red 10878 . . . . . . . 8
5756ad2antrr 725 . . . . . . 7
58 sadcaddlem.1 . . . . . . . . 9
5958biimpa 484 . . . . . . . 8
6059adantr 465 . . . . . . 7
616nnnn0d 10877 . . . . . . . . . . . . 13
62 ifcl 3983 . . . . . . . . . . . . 13
6361, 47, 62sylancl 662 . . . . . . . . . . . 12
6463nn0ge0d 10880 . . . . . . . . . . 11
657adantr 465 . . . . . . . . . . . . 13
66 0red 9618 . . . . . . . . . . . . 13
6765, 66ifclda 3973 . . . . . . . . . . . 12
687, 67addge01d 10165 . . . . . . . . . . 11
6964, 68mpbid 210 . . . . . . . . . 10
7069ad2antrr 725 . . . . . . . . 9
71 iftrue 3947 . . . . . . . . . . 11
7271adantl 466 . . . . . . . . . 10
7372oveq1d 6311 . . . . . . . . 9
7470, 73breqtrrd 4478 . . . . . . . 8
75 ifcl 3983 . . . . . . . . . . . . 13
7661, 47, 75sylancl 662 . . . . . . . . . . . 12
7776nn0ge0d 10880 . . . . . . . . . . 11
787adantr 465 . . . . . . . . . . . . 13
79 0red 9618 . . . . . . . . . . . . 13
8078, 79ifclda 3973 . . . . . . . . . . . 12
817, 80addge02d 10166 . . . . . . . . . . 11
8277, 81mpbid 210 . . . . . . . . . 10
8382ad2antrr 725 . . . . . . . . 9
84 iftrue 3947 . . . . . . . . . . 11
8584adantl 466 . . . . . . . . . 10
8685oveq2d 6312 . . . . . . . . 9
8783, 86breqtrrd 4478 . . . . . . . 8
8874, 87jaodan 785 . . . . . . 7
898, 8, 42, 57, 60, 88le2addd 10195 . . . . . 6
9089ex 434 . . . . 5
91 ioran 490 . . . . . 6
92 iffalse 3950 . . . . . . . . . . . . . 14
9392ad2antrl 727 . . . . . . . . . . . . 13
94 iffalse 3950 . . . . . . . . . . . . . 14
9594ad2antll 728 . . . . . . . . . . . . 13
9693, 95oveq12d 6314 . . . . . . . . . . . 12
97 00id 9776 . . . . . . . . . . . 12
9896, 97syl6eq 2514 . . . . . . . . . . 11
9998oveq2d 6312 . . . . . . . . . 10
10029nn0red 10878 . . . . . . . . . . . . . 14
101100ad2antrr 725 . . . . . . . . . . . . 13
10239nn0red 10878 . . . . . . . . . . . . . 14
103102ad2antrr 725 . . . . . . . . . . . . 13
104101, 103readdcld 9644 . . . . . . . . . . . 12
105104recnd 9643 . . . . . . . . . . 11
106105addid1d 9801 . . . . . . . . . 10
10799, 106eqtrd 2498 . . . . . . . . 9
10822fveq1i 5872 . . . . . . . . . . . . . . . 16
109108fveq2i 5874 . . . . . . . . . . . . . . 15
110 fvres 5885 . . . . . . . . . . . . . . . 16
11129, 110syl 16 . . . . . . . . . . . . . . 15
112 f1ocnvfv2 6183 . . . . . . . . . . . . . . . 16
11319, 18, 112sylancr 663 . . . . . . . . . . . . . . 15
114109, 111, 1133eqtr3a 2522 . . . . . . . . . . . . . 14
115114, 14syl6eqss 3553 . . . . . . . . . . . . 13
11629nn0zd 10992 . . . . . . . . . . . . . 14
117 bitsfzo 14085 . . . . . . . . . . . . . 14
118116, 5, 117syl2anc 661 . . . . . . . . . . . . 13
119115, 118mpbird 232 . . . . . . . . . . . 12
120 elfzolt2 11837 . . . . . . . . . . . 12
121119, 120syl 16 . . . . . . . . . . 11
12222fveq1i 5872 . . . . . . . . . . . . . . . 16
123122fveq2i 5874 . . . . . . . . . . . . . . 15
124 fvres 5885 . . . . . . . . . . . . . . . 16
12539, 124syl 16 . . . . . . . . . . . . . . 15
126 f1ocnvfv2 6183 . . . . . . . . . . . . . . . 16
12719, 37, 126sylancr 663 . . . . . . . . . . . . . . 15
128123, 125, 1273eqtr3a 2522 . . . . . . . . . . . . . 14
129128, 33syl6eqss 3553 . . . . . . . . . . . . 13
13039nn0zd 10992 . . . . . . . . . . . . . 14
131 bitsfzo 14085 . . . . . . . . . . . . . 14
132130, 5, 131syl2anc 661 . . . . . . . . . . . . 13
133129, 132mpbird 232 . . . . . . . . . . . 12
134 elfzolt2 11837 . . . . . . . . . . . 12
135133, 134syl 16 . . . . . . . . . . 11
136100, 102, 7, 7, 121, 135lt2addd 10199 . . . . . . . . . 10
137136ad2antrr 725 . . . . . . . . 9
138107, 137eqbrtrd 4472 . . . . . . . 8
13980ad2antrr 725 . . . . . . . . . . 11
14067ad2antrr 725 . . . . . . . . . . 11
141139, 140readdcld 9644 . . . . . . . . . 10
142104, 141readdcld 9644 . . . . . . . . 9
1437ad2antrr 725 . . . . . . . . . 10
144143, 143readdcld 9644 . . . . . . . . 9
145142, 144ltnled 9753 . . . . . . . 8
146138, 145mpbid 210 . . . . . . 7
147146ex 434 . . . . . 6
14891, 147syl5bi 217 . . . . 5
14990, 148impcon4bid 205 . . . 4
1502, 149bitrd 253 . . 3
151 cad0 1467 . . . . 5
152151adantl 466 . . . 4
15340nn0ge0d 10880 . . . . . . . . 9
1547, 7readdcld 9644 . . . . . . . . . 10
155154, 41addge02d 10166 . . . . . . . . 9
156153, 155mpbid 210 . . . . . . . 8
157156ad2antrr 725 . . . . . . 7
15871, 84oveqan12d 6315 . . . . . . . . 9
159158adantl 466 . . . . . . . 8
160159oveq2d 6312 . . . . . . 7
161157, 160breqtrrd 4478 . . . . . 6
162161ex 434 . . . . 5
163100adantr 465 . . . . . . . . . 10
164102adantr 465 . . . . . . . . . 10
165163, 164readdcld 9644 . . . . . . . . 9
1667adantr 465 . . . . . . . . 9
1677, 41lenltd 9752 . . . . . . . . . . . 12
16858, 167bitrd 253 . . . . . . . . . . 11
169168con2bid 329 . . . . . . . . . 10
170169biimpar 485 . . . . . . . . 9
171165, 166, 166, 170ltadd1dd 10188 . . . . . . . 8
172165, 166readdcld 9644 . . . . . . . . 9
173154adantr 465 . . . . . . . . 9
17441, 56readdcld 9644 . . . . . . . . . 10
175174adantr 465 . . . . . . . . 9
176 ltletr 9697 . . . . . . . . 9
177172, 173, 175, 176syl3anc 1228 . . . . . . . 8
178171, 177mpand 675 . . . . . . 7
17956adantr 465 . . . . . . . 8