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

Theorem 4sqlem16 14478
Description: Lemma for 4sq 14482. (Contributed by Mario Carneiro, 16-Jul-2014.)
Hypotheses
Ref Expression
4sq.1
4sq.2
4sq.3
4sq.4
4sq.5
4sq.6
4sq.7
4sq.m
4sq.a
4sq.b
4sq.c
4sq.d
4sq.e
4sq.f
4sq.g
4sq.h
4sq.r
4sq.p
Assertion
Ref Expression
4sqlem16
Distinct variable groups:   , , , ,   ,   ,   ,   ,   ,   ,   ,   ,   , ,M   ,N   P, ,   ,   S, ,   ,

Proof of Theorem 4sqlem16
StepHypRef Expression
1 4sq.r . . 3
2 4sq.a . . . . . . . . . . . 12
3 4sq.m . . . . . . . . . . . . 13
4 eluz2nn 11148 . . . . . . . . . . . . 13
53, 4syl 16 . . . . . . . . . . . 12
6 4sq.e . . . . . . . . . . . 12
72, 5, 64sqlem5 14460 . . . . . . . . . . 11
87simpld 459 . . . . . . . . . 10
9 zsqcl 12238 . . . . . . . . . 10
108, 9syl 16 . . . . . . . . 9
1110zred 10994 . . . . . . . 8
12 4sq.b . . . . . . . . . . . 12
13 4sq.f . . . . . . . . . . . 12
1412, 5, 134sqlem5 14460 . . . . . . . . . . 11
1514simpld 459 . . . . . . . . . 10
16 zsqcl 12238 . . . . . . . . . 10
1715, 16syl 16 . . . . . . . . 9
1817zred 10994 . . . . . . . 8
1911, 18readdcld 9644 . . . . . . 7
20 4sq.c . . . . . . . . . . . 12
21 4sq.g . . . . . . . . . . . 12
2220, 5, 214sqlem5 14460 . . . . . . . . . . 11
2322simpld 459 . . . . . . . . . 10
24 zsqcl 12238 . . . . . . . . . 10
2523, 24syl 16 . . . . . . . . 9
2625zred 10994 . . . . . . . 8
27 4sq.d . . . . . . . . . . . 12
28 4sq.h . . . . . . . . . . . 12
2927, 5, 284sqlem5 14460 . . . . . . . . . . 11
3029simpld 459 . . . . . . . . . 10
31 zsqcl 12238 . . . . . . . . . 10
3230, 31syl 16 . . . . . . . . 9
3332zred 10994 . . . . . . . 8
3426, 33readdcld 9644 . . . . . . 7
355nnred 10576 . . . . . . . . 9
3635resqcld 12336 . . . . . . . 8
3736rehalfcld 10810 . . . . . . 7
3837rehalfcld 10810 . . . . . . . . 9
392, 5, 64sqlem7 14462 . . . . . . . . 9
4012, 5, 134sqlem7 14462 . . . . . . . . 9
4111, 18, 38, 38, 39, 40le2addd 10195 . . . . . . . 8
4237recnd 9643 . . . . . . . . 9
43422halvesd 10809 . . . . . . . 8
4441, 43breqtrd 4476 . . . . . . 7
4520, 5, 214sqlem7 14462 . . . . . . . . 9
4627, 5, 284sqlem7 14462 . . . . . . . . 9
4726, 33, 38, 38, 45, 46le2addd 10195 . . . . . . . 8
4847, 43breqtrd 4476 . . . . . . 7
4919, 34, 37, 37, 44, 48le2addd 10195 . . . . . 6
5036recnd 9643 . . . . . . 7
51502halvesd 10809 . . . . . 6
5249, 51breqtrd 4476 . . . . 5
5335recnd 9643 . . . . . 6
5453sqvald 12307 . . . . 5
5552, 54breqtrd 4476 . . . 4
5619, 34readdcld 9644 . . . . 5
575nngt0d 10604 . . . . 5
58 ledivmul 10443 . . . . 5
5956, 35, 35, 57, 58syl112anc 1232 . . . 4
6055, 59mpbird 232 . . 3
611, 60syl5eqbr 4485 . 2
62 simpr 461 . . . . . . . . . . . . 13
631, 62syl5eqr 2512 . . . . . . . . . . . 12
6456recnd 9643 . . . . . . . . . . . . . . 15
655nnne0d 10605 . . . . . . . . . . . . . . 15
6664, 53, 65diveq0ad 10355 . . . . . . . . . . . . . 14
67 zsqcl2 12245 . . . . . . . . . . . . . . . . . 18
688, 67syl 16 . . . . . . . . . . . . . . . . 17
69 zsqcl2 12245 . . . . . . . . . . . . . . . . . 18
7015, 69syl 16 . . . . . . . . . . . . . . . . 17
7168, 70nn0addcld 10881 . . . . . . . . . . . . . . . 16
7271nn0ge0d 10880 . . . . . . . . . . . . . . 15
73 zsqcl2 12245 . . . . . . . . . . . . . . . . . 18
7423, 73syl 16 . . . . . . . . . . . . . . . . 17
75 zsqcl2 12245 . . . . . . . . . . . . . . . . . 18
7630, 75syl 16 . . . . . . . . . . . . . . . . 17
7774, 76nn0addcld 10881 . . . . . . . . . . . . . . . 16
7877nn0ge0d 10880 . . . . . . . . . . . . . . 15
79 add20 10089 . . . . . . . . . . . . . . 15
8019, 72, 34, 78, 79syl22anc 1229 . . . . . . . . . . . . . 14
8166, 80bitrd 253 . . . . . . . . . . . . 13
8281biimpa 484 . . . . . . . . . . . 12
8363, 82syldan 470 . . . . . . . . . . 11
8483simpld 459 . . . . . . . . . 10
8568nn0ge0d 10880 . . . . . . . . . . . 12
8670nn0ge0d 10880 . . . . . . . . . . . 12
87 add20 10089 . . . . . . . . . . . 12
8811, 85, 18, 86, 87syl22anc 1229 . . . . . . . . . . 11
8988biimpa 484 . . . . . . . . . 10
9084, 89syldan 470 . . . . . . . . 9
9190simpld 459 . . . . . . . 8
922, 5, 6, 914sqlem9 14464 . . . . . . 7
9390simprd 463 . . . . . . . 8
9412, 5, 13, 934sqlem9 14464 . . . . . . 7
955nnsqcld 12330 . . . . . . . . . 10
9695nnzd 10993 . . . . . . . . 9
97 zsqcl 12238 . . . . . . . . . 10
982, 97syl 16 . . . . . . . . 9
99 zsqcl 12238 . . . . . . . . . 10
10012, 99syl 16 . . . . . . . . 9
101 dvds2add 14015 . . . . . . . . 9
10296, 98, 100, 101syl3anc 1228 . . . . . . . 8
103102adantr 465 . . . . . . 7
10492, 94, 103mp2and 679 . . . . . 6
10583simprd 463 . . . . . . . . . 10
10674nn0ge0d 10880 . . . . . . . . . . . 12
10776nn0ge0d 10880 . . . . . . . . . . . 12
108 add20 10089 . . . . . . . . . . . 12
10926, 106, 33, 107, 108syl22anc 1229 . . . . . . . . . . 11
110109biimpa 484 . . . . . . . . . 10
111105, 110syldan 470 . . . . . . . . 9
112111simpld 459 . . . . . . . 8
11320, 5, 21, 1124sqlem9 14464 . . . . . . 7
114111simprd 463 . . . . . . . 8
11527, 5, 28, 1144sqlem9 14464 . . . . . . 7
116 zsqcl 12238 . . . . . . . . . 10
11720, 116syl 16 . . . . . . . . 9
118 zsqcl 12238 . . . . . . . . . 10
11927, 118syl 16 . . . . . . . . 9
120 dvds2add 14015 . . . . . . . . 9
12196, 117, 119, 120syl3anc 1228 . . . . . . . 8
122121adantr 465 . . . . . . 7
123113, 115, 122mp2and 679 . . . . . 6
12498, 100zaddcld 10998 . . . . . . . 8
125117, 119zaddcld 10998 . . . . . . . 8
126 dvds2add 14015 . . . . . . . 8
12796, 124, 125, 126syl3anc 1228 . . . . . . 7
128127adantr 465 . . . . . 6
129104, 123, 128mp2and 679 . . . . 5
130 4sq.1 . . . . . . . . . . . . . 14
131 4sq.2 . . . . . . . . . . . . . 14
132 4sq.3 . . . . . . . . . . . . . 14
133 4sq.4 . . . . . . . . . . . . . 14
134 4sq.5 . . . . . . . . . . . . . 14
135 4sq.6 . . . . . . . . . . . . . 14
136 4sq.7 . . . . . . . . . . . . . 14
137 4sq.p . . . . . . . . . . . . . 14
138130, 131, 132, 133, 134, 135, 136, 3, 2, 12, 20, 27, 6, 13, 21, 28, 1, 1374sqlem15 14477 . . . . . . . . . . . . 13
139138simpld 459 . . . . . . . . . . . 12
140139simpld 459 . . . . . . . . . . 11
1412, 5, 6, 1404sqlem10 14465 . . . . . . . . . 10
142139simprd 463 . . . . . . . . . . 11
14312, 5, 13, 1424sqlem10 14465 . . . . . . . . . 10
14496adantr 465 . . . . . . . . . . 11
14598adantr 465 . . . . . . . . . . . 12
14638recnd 9643 . . . . . . . . . . . . . . . 16
14710zcnd 10995 . . . . . . . . . . . . . . . 16
148146, 147subeq0ad 9964 . . . . . . . . . . . . . . 15
149148adantr 465 . . . . . . . . . . . . . 14
150140, 149mpbid 210 . . . . . . . . . . . . 13
15110adantr 465 . . . . . . . . . . . . 13
152150, 151eqeltrd 2545 . . . . . . . . . . . 12
153145, 152zsubcld 10999 . . . . . . . . . . 11
154100adantr 465 . . . . . . . . . . . 12
155154, 152zsubcld 10999 . . . . . . . . . . 11
156 dvds2add 14015 . . . . . . . . . . 11
157144, 153, 155, 156syl3anc 1228 . . . . . . . . . 10
158141, 143, 157mp2and 679 . . . . . . . . 9
15998zcnd 10995 . . . . . . . . . . . 12
160100zcnd 10995 . . . . . . . . . . . 12
161159, 160, 146, 146addsub4d 10001 . . . . . . . . . . 11
16243oveq2d 6312 . . . . . . . . . . 11
163161, 162eqtr3d 2500 . . . . . . . . . 10
164163adantr 465 . . . . . . . . 9
165158, 164breqtrd 4476 . . . . . . . 8
166138simprd 463 . . . . . . . . . . . 12
167166simpld 459 . . . . . . . . . . 11
16820, 5, 21, 1674sqlem10 14465 . . . . . . . . . 10
169166simprd 463 . . . . . . . . . . 11
17027, 5, 28, 1694sqlem10 14465 . . . . . . . . . 10
171117adantr 465 . . . . . . . . . . . 12
172171, 152zsubcld 10999 . . . . . . . . . . 11
173119adantr 465 . . . . . . . . . . . 12
174173, 152zsubcld 10999 . . . . . . . . . . 11
175 dvds2add 14015 . . . . . . . . . . 11
176144, 172, 174, 175syl3anc 1228 . . . . . . . . . 10
177168, 170, 176mp2and 679 . . . . . . . . 9
178117zcnd 10995 . . . . . . . . . . . 12
179119zcnd 10995 . . . . . . . . . . . 12
180178, 179, 146, 146addsub4d 10001 . . . . . . . . . . 11
18143oveq2d 6312 . . . . . . . . . . 11
182180, 181eqtr3d 2500 . . . . . . . . . 10
183182adantr 465 . . . . . . . . 9
184177, 183breqtrd 4476 . . . . . . . 8
185124adantr 465 . . . . . . . . . 10
18643adantr 465 . . . . . . . . . . 11
187152, 152zaddcld 10998 . . . . . . . . . . 11
188186, 187eqeltrrd 2546 . . . . . . . . . 10
189185, 188zsubcld 10999 . . . . . . . . 9
190125adantr 465 . . . . . . . . . 10
191190, 188zsubcld 10999 . . . . . . . . 9
192 dvds2add 14015 . . . . . . . . 9
193144, 189, 191, 192syl3anc 1228 . . . . . . . 8
194165, 184, 193mp2and 679 . . . . . . 7
195124zcnd 10995 . . . . . . . . . 10
196125zcnd 10995 . . . . . . . . . 10
197195, 196, 42, 42addsub4d 10001 . . . . . . . . 9
19851oveq2d 6312 . . . . . . . . 9
199197, 198eqtr3d 2500 . . . . . . . 8
200199adantr 465 . . . . . . 7
201194, 200breqtrd 4476 . . . . . 6
202124, 125zaddcld 10998 . . . . . . . 8
203202adantr 465 . . . . . . 7
204 dvdssubr 14027 . . . . . . 7
205144, 203, 204syl2anc 661 . . . . . 6
206201, 205mpbird 232 . . . . 5
207129, 206jaodan 785 . . . 4
208137adantr 465 . . . 4
209207, 208breqtrrd 4478 . . 3
210209ex 434 . 2
21161, 210jca 532 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  \/wo 368  /\wa 369  =wceq 1395  e.wcel 1818  {cab 2442  E.wrex 2808  {crab 2811  C_wss 3475   class class class wbr 4452  `'ccnv 5003  `cfv 5593  (class class class)co 6296  supcsup 7920   cr 9512  0cc0 9513  1c1 9514   caddc 9516   cmul 9518   clt 9649   cle 9650   cmin 9828   cdiv 10231   cn 10561  2c2 10610   cn0 10820   cz 10889   cuz 11110   cfz 11701   cmo 11996   cexp 12166   cdvds 13986   cprime 14217
This theorem is referenced by:  4sqlem17  14479
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-cnex 9569  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-mulcom 9577  ax-addass 9578  ax-mulass 9579  ax-distr 9580  ax-i2m1 9581  ax-1ne0 9582  ax-1rid 9583  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586  ax-pre-lttri 9587  ax-pre-lttrn 9588  ax-pre-ltadd 9589  ax-pre-mulgt0 9590  ax-pre-sup 9591
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6701  df-2nd 6801  df-recs 7061  df-rdg 7095  df-er 7330  df-en 7537  df-dom 7538  df-sdom 7539  df-sup 7921  df-pnf 9651  df-mnf 9652  df-xr 9653  df-ltxr 9654  df-le 9655  df-sub 9830  df-neg 9831  df-div 10232  df-nn 10562  df-2 10619  df-3 10620  df-n0 10821  df-z 10890  df-uz 11111  df-rp 11250  df-fl 11929  df-mod 11997  df-seq 12108  df-exp 12167  df-cj 12932  df-re 12933  df-im 12934  df-sqrt 13068  df-abs 13069  df-dvds 13987  df-gcd 14145
  Copyright terms: Public domain W3C validator