Users' Mathboxes Mathbox for Asger C. Ipsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  knoppndvlem2 Structured version   Visualization version   GIF version

Theorem knoppndvlem2 35377
Description: Lemma for knoppndv 35398. (Contributed by Asger C. Ipsen, 15-Jun-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
Hypotheses
Ref Expression
knoppndvlem2.n (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
knoppndvlem2.i (๐œ‘ โ†’ ๐ผ โˆˆ โ„ค)
knoppndvlem2.j (๐œ‘ โ†’ ๐ฝ โˆˆ โ„ค)
knoppndvlem2.m (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
knoppndvlem2.1 (๐œ‘ โ†’ ๐ฝ < ๐ผ)
Assertion
Ref Expression
knoppndvlem2 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘๐ผ) ยท ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ๐‘€)) โˆˆ โ„ค)

Proof of Theorem knoppndvlem2
StepHypRef Expression
1 2cnd 12286 . . . . . . 7 (๐œ‘ โ†’ 2 โˆˆ โ„‚)
2 knoppndvlem2.n . . . . . . . . 9 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
3 nnz 12575 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„ค)
42, 3syl 17 . . . . . . . 8 (๐œ‘ โ†’ ๐‘ โˆˆ โ„ค)
54zcnd 12663 . . . . . . 7 (๐œ‘ โ†’ ๐‘ โˆˆ โ„‚)
61, 5mulcld 11230 . . . . . 6 (๐œ‘ โ†’ (2 ยท ๐‘) โˆˆ โ„‚)
7 2ne0 12312 . . . . . . . 8 2 โ‰  0
87a1i 11 . . . . . . 7 (๐œ‘ โ†’ 2 โ‰  0)
9 0red 11213 . . . . . . . . 9 (๐œ‘ โ†’ 0 โˆˆ โ„)
10 1red 11211 . . . . . . . . . 10 (๐œ‘ โ†’ 1 โˆˆ โ„)
114zred 12662 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘ โˆˆ โ„)
12 0lt1 11732 . . . . . . . . . . 11 0 < 1
1312a1i 11 . . . . . . . . . 10 (๐œ‘ โ†’ 0 < 1)
14 nnge1 12236 . . . . . . . . . . 11 (๐‘ โˆˆ โ„• โ†’ 1 โ‰ค ๐‘)
152, 14syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ 1 โ‰ค ๐‘)
169, 10, 11, 13, 15ltletrd 11370 . . . . . . . . 9 (๐œ‘ โ†’ 0 < ๐‘)
179, 16ltned 11346 . . . . . . . 8 (๐œ‘ โ†’ 0 โ‰  ๐‘)
1817necomd 2996 . . . . . . 7 (๐œ‘ โ†’ ๐‘ โ‰  0)
191, 5, 8, 18mulne0d 11862 . . . . . 6 (๐œ‘ โ†’ (2 ยท ๐‘) โ‰  0)
20 knoppndvlem2.i . . . . . 6 (๐œ‘ โ†’ ๐ผ โˆˆ โ„ค)
216, 19, 20expclzd 14112 . . . . 5 (๐œ‘ โ†’ ((2 ยท ๐‘)โ†‘๐ผ) โˆˆ โ„‚)
22 knoppndvlem2.j . . . . . . . 8 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„ค)
2322znegcld 12664 . . . . . . 7 (๐œ‘ โ†’ -๐ฝ โˆˆ โ„ค)
246, 19, 23expclzd 14112 . . . . . 6 (๐œ‘ โ†’ ((2 ยท ๐‘)โ†‘-๐ฝ) โˆˆ โ„‚)
2524, 1, 8divcld 11986 . . . . 5 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘-๐ฝ) / 2) โˆˆ โ„‚)
26 knoppndvlem2.m . . . . . 6 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
2726zcnd 12663 . . . . 5 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„‚)
2821, 25, 27mulassd 11233 . . . 4 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘๐ผ) ยท (((2 ยท ๐‘)โ†‘-๐ฝ) / 2)) ยท ๐‘€) = (((2 ยท ๐‘)โ†‘๐ผ) ยท ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ๐‘€)))
2928eqcomd 2738 . . 3 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘๐ผ) ยท ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ๐‘€)) = ((((2 ยท ๐‘)โ†‘๐ผ) ยท (((2 ยท ๐‘)โ†‘-๐ฝ) / 2)) ยท ๐‘€))
3021, 24, 1, 8divassd 12021 . . . . . 6 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘๐ผ) ยท ((2 ยท ๐‘)โ†‘-๐ฝ)) / 2) = (((2 ยท ๐‘)โ†‘๐ผ) ยท (((2 ยท ๐‘)โ†‘-๐ฝ) / 2)))
3130eqcomd 2738 . . . . 5 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘๐ผ) ยท (((2 ยท ๐‘)โ†‘-๐ฝ) / 2)) = ((((2 ยท ๐‘)โ†‘๐ผ) ยท ((2 ยท ๐‘)โ†‘-๐ฝ)) / 2))
326, 19jca 512 . . . . . . . . . 10 (๐œ‘ โ†’ ((2 ยท ๐‘) โˆˆ โ„‚ โˆง (2 ยท ๐‘) โ‰  0))
3320, 23jca 512 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ผ โˆˆ โ„ค โˆง -๐ฝ โˆˆ โ„ค))
3432, 33jca 512 . . . . . . . . 9 (๐œ‘ โ†’ (((2 ยท ๐‘) โˆˆ โ„‚ โˆง (2 ยท ๐‘) โ‰  0) โˆง (๐ผ โˆˆ โ„ค โˆง -๐ฝ โˆˆ โ„ค)))
35 expaddz 14068 . . . . . . . . 9 ((((2 ยท ๐‘) โˆˆ โ„‚ โˆง (2 ยท ๐‘) โ‰  0) โˆง (๐ผ โˆˆ โ„ค โˆง -๐ฝ โˆˆ โ„ค)) โ†’ ((2 ยท ๐‘)โ†‘(๐ผ + -๐ฝ)) = (((2 ยท ๐‘)โ†‘๐ผ) ยท ((2 ยท ๐‘)โ†‘-๐ฝ)))
3634, 35syl 17 . . . . . . . 8 (๐œ‘ โ†’ ((2 ยท ๐‘)โ†‘(๐ผ + -๐ฝ)) = (((2 ยท ๐‘)โ†‘๐ผ) ยท ((2 ยท ๐‘)โ†‘-๐ฝ)))
3736eqcomd 2738 . . . . . . 7 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘๐ผ) ยท ((2 ยท ๐‘)โ†‘-๐ฝ)) = ((2 ยท ๐‘)โ†‘(๐ผ + -๐ฝ)))
3820zcnd 12663 . . . . . . . . 9 (๐œ‘ โ†’ ๐ผ โˆˆ โ„‚)
3922zcnd 12663 . . . . . . . . 9 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„‚)
4038, 39negsubd 11573 . . . . . . . 8 (๐œ‘ โ†’ (๐ผ + -๐ฝ) = (๐ผ โˆ’ ๐ฝ))
4140oveq2d 7421 . . . . . . 7 (๐œ‘ โ†’ ((2 ยท ๐‘)โ†‘(๐ผ + -๐ฝ)) = ((2 ยท ๐‘)โ†‘(๐ผ โˆ’ ๐ฝ)))
42 knoppndvlem2.1 . . . . . . . . . 10 (๐œ‘ โ†’ ๐ฝ < ๐ผ)
4322, 20jca 512 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ฝ โˆˆ โ„ค โˆง ๐ผ โˆˆ โ„ค))
44 znnsub 12604 . . . . . . . . . . 11 ((๐ฝ โˆˆ โ„ค โˆง ๐ผ โˆˆ โ„ค) โ†’ (๐ฝ < ๐ผ โ†” (๐ผ โˆ’ ๐ฝ) โˆˆ โ„•))
4543, 44syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ฝ < ๐ผ โ†” (๐ผ โˆ’ ๐ฝ) โˆˆ โ„•))
4642, 45mpbid 231 . . . . . . . . 9 (๐œ‘ โ†’ (๐ผ โˆ’ ๐ฝ) โˆˆ โ„•)
476, 46jca 512 . . . . . . . 8 (๐œ‘ โ†’ ((2 ยท ๐‘) โˆˆ โ„‚ โˆง (๐ผ โˆ’ ๐ฝ) โˆˆ โ„•))
48 expm1t 14052 . . . . . . . 8 (((2 ยท ๐‘) โˆˆ โ„‚ โˆง (๐ผ โˆ’ ๐ฝ) โˆˆ โ„•) โ†’ ((2 ยท ๐‘)โ†‘(๐ผ โˆ’ ๐ฝ)) = (((2 ยท ๐‘)โ†‘((๐ผ โˆ’ ๐ฝ) โˆ’ 1)) ยท (2 ยท ๐‘)))
4947, 48syl 17 . . . . . . 7 (๐œ‘ โ†’ ((2 ยท ๐‘)โ†‘(๐ผ โˆ’ ๐ฝ)) = (((2 ยท ๐‘)โ†‘((๐ผ โˆ’ ๐ฝ) โˆ’ 1)) ยท (2 ยท ๐‘)))
5037, 41, 493eqtrd 2776 . . . . . 6 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘๐ผ) ยท ((2 ยท ๐‘)โ†‘-๐ฝ)) = (((2 ยท ๐‘)โ†‘((๐ผ โˆ’ ๐ฝ) โˆ’ 1)) ยท (2 ยท ๐‘)))
5150oveq1d 7420 . . . . 5 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘๐ผ) ยท ((2 ยท ๐‘)โ†‘-๐ฝ)) / 2) = ((((2 ยท ๐‘)โ†‘((๐ผ โˆ’ ๐ฝ) โˆ’ 1)) ยท (2 ยท ๐‘)) / 2))
5220, 22jca 512 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐ผ โˆˆ โ„ค โˆง ๐ฝ โˆˆ โ„ค))
53 zsubcl 12600 . . . . . . . . . . . 12 ((๐ผ โˆˆ โ„ค โˆง ๐ฝ โˆˆ โ„ค) โ†’ (๐ผ โˆ’ ๐ฝ) โˆˆ โ„ค)
5452, 53syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ผ โˆ’ ๐ฝ) โˆˆ โ„ค)
55 peano2zm 12601 . . . . . . . . . . 11 ((๐ผ โˆ’ ๐ฝ) โˆˆ โ„ค โ†’ ((๐ผ โˆ’ ๐ฝ) โˆ’ 1) โˆˆ โ„ค)
5654, 55syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ผ โˆ’ ๐ฝ) โˆ’ 1) โˆˆ โ„ค)
5722zred 12662 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„)
5820zred 12662 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐ผ โˆˆ โ„)
5957, 58posdifd 11797 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐ฝ < ๐ผ โ†” 0 < (๐ผ โˆ’ ๐ฝ)))
6042, 59mpbid 231 . . . . . . . . . . 11 (๐œ‘ โ†’ 0 < (๐ผ โˆ’ ๐ฝ))
61 0zd 12566 . . . . . . . . . . . . 13 (๐œ‘ โ†’ 0 โˆˆ โ„ค)
6261, 54jca 512 . . . . . . . . . . . 12 (๐œ‘ โ†’ (0 โˆˆ โ„ค โˆง (๐ผ โˆ’ ๐ฝ) โˆˆ โ„ค))
63 zltlem1 12611 . . . . . . . . . . . 12 ((0 โˆˆ โ„ค โˆง (๐ผ โˆ’ ๐ฝ) โˆˆ โ„ค) โ†’ (0 < (๐ผ โˆ’ ๐ฝ) โ†” 0 โ‰ค ((๐ผ โˆ’ ๐ฝ) โˆ’ 1)))
6462, 63syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ (0 < (๐ผ โˆ’ ๐ฝ) โ†” 0 โ‰ค ((๐ผ โˆ’ ๐ฝ) โˆ’ 1)))
6560, 64mpbid 231 . . . . . . . . . 10 (๐œ‘ โ†’ 0 โ‰ค ((๐ผ โˆ’ ๐ฝ) โˆ’ 1))
6656, 65jca 512 . . . . . . . . 9 (๐œ‘ โ†’ (((๐ผ โˆ’ ๐ฝ) โˆ’ 1) โˆˆ โ„ค โˆง 0 โ‰ค ((๐ผ โˆ’ ๐ฝ) โˆ’ 1)))
67 elnn0z 12567 . . . . . . . . 9 (((๐ผ โˆ’ ๐ฝ) โˆ’ 1) โˆˆ โ„•0 โ†” (((๐ผ โˆ’ ๐ฝ) โˆ’ 1) โˆˆ โ„ค โˆง 0 โ‰ค ((๐ผ โˆ’ ๐ฝ) โˆ’ 1)))
6866, 67sylibr 233 . . . . . . . 8 (๐œ‘ โ†’ ((๐ผ โˆ’ ๐ฝ) โˆ’ 1) โˆˆ โ„•0)
696, 68expcld 14107 . . . . . . 7 (๐œ‘ โ†’ ((2 ยท ๐‘)โ†‘((๐ผ โˆ’ ๐ฝ) โˆ’ 1)) โˆˆ โ„‚)
7069, 6, 1, 8divassd 12021 . . . . . 6 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘((๐ผ โˆ’ ๐ฝ) โˆ’ 1)) ยท (2 ยท ๐‘)) / 2) = (((2 ยท ๐‘)โ†‘((๐ผ โˆ’ ๐ฝ) โˆ’ 1)) ยท ((2 ยท ๐‘) / 2)))
715, 1, 8divcan3d 11991 . . . . . . 7 (๐œ‘ โ†’ ((2 ยท ๐‘) / 2) = ๐‘)
7271oveq2d 7421 . . . . . 6 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘((๐ผ โˆ’ ๐ฝ) โˆ’ 1)) ยท ((2 ยท ๐‘) / 2)) = (((2 ยท ๐‘)โ†‘((๐ผ โˆ’ ๐ฝ) โˆ’ 1)) ยท ๐‘))
7370, 72eqtrd 2772 . . . . 5 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘((๐ผ โˆ’ ๐ฝ) โˆ’ 1)) ยท (2 ยท ๐‘)) / 2) = (((2 ยท ๐‘)โ†‘((๐ผ โˆ’ ๐ฝ) โˆ’ 1)) ยท ๐‘))
7431, 51, 733eqtrd 2776 . . . 4 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘๐ผ) ยท (((2 ยท ๐‘)โ†‘-๐ฝ) / 2)) = (((2 ยท ๐‘)โ†‘((๐ผ โˆ’ ๐ฝ) โˆ’ 1)) ยท ๐‘))
7574oveq1d 7420 . . 3 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘๐ผ) ยท (((2 ยท ๐‘)โ†‘-๐ฝ) / 2)) ยท ๐‘€) = ((((2 ยท ๐‘)โ†‘((๐ผ โˆ’ ๐ฝ) โˆ’ 1)) ยท ๐‘) ยท ๐‘€))
7629, 75eqtrd 2772 . 2 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘๐ผ) ยท ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ๐‘€)) = ((((2 ยท ๐‘)โ†‘((๐ผ โˆ’ ๐ฝ) โˆ’ 1)) ยท ๐‘) ยท ๐‘€))
77 2z 12590 . . . . . . . . 9 2 โˆˆ โ„ค
7877a1i 11 . . . . . . . 8 (๐œ‘ โ†’ 2 โˆˆ โ„ค)
7978, 4jca 512 . . . . . . 7 (๐œ‘ โ†’ (2 โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค))
80 zmulcl 12607 . . . . . . 7 ((2 โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (2 ยท ๐‘) โˆˆ โ„ค)
8179, 80syl 17 . . . . . 6 (๐œ‘ โ†’ (2 ยท ๐‘) โˆˆ โ„ค)
8281, 68jca 512 . . . . 5 (๐œ‘ โ†’ ((2 ยท ๐‘) โˆˆ โ„ค โˆง ((๐ผ โˆ’ ๐ฝ) โˆ’ 1) โˆˆ โ„•0))
83 zexpcl 14038 . . . . 5 (((2 ยท ๐‘) โˆˆ โ„ค โˆง ((๐ผ โˆ’ ๐ฝ) โˆ’ 1) โˆˆ โ„•0) โ†’ ((2 ยท ๐‘)โ†‘((๐ผ โˆ’ ๐ฝ) โˆ’ 1)) โˆˆ โ„ค)
8482, 83syl 17 . . . 4 (๐œ‘ โ†’ ((2 ยท ๐‘)โ†‘((๐ผ โˆ’ ๐ฝ) โˆ’ 1)) โˆˆ โ„ค)
8584, 4zmulcld 12668 . . 3 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘((๐ผ โˆ’ ๐ฝ) โˆ’ 1)) ยท ๐‘) โˆˆ โ„ค)
8685, 26zmulcld 12668 . 2 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘((๐ผ โˆ’ ๐ฝ) โˆ’ 1)) ยท ๐‘) ยท ๐‘€) โˆˆ โ„ค)
8776, 86eqeltrd 2833 1 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘๐ผ) ยท ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ๐‘€)) โˆˆ โ„ค)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 396   = wceq 1541   โˆˆ wcel 2106   โ‰  wne 2940   class class class wbr 5147  (class class class)co 7405  โ„‚cc 11104  0cc0 11106  1c1 11107   + caddc 11109   ยท cmul 11111   < clt 11244   โ‰ค cle 11245   โˆ’ cmin 11440  -cneg 11441   / cdiv 11867  โ„•cn 12208  2c2 12263  โ„•0cn0 12468  โ„คcz 12554  โ†‘cexp 14023
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-n0 12469  df-z 12555  df-uz 12819  df-seq 13963  df-exp 14024
This theorem is referenced by:  knoppndvlem6  35381
  Copyright terms: Public domain W3C validator