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

Theorem knoppndvlem14 35064
Description: Lemma for knoppndv 35073. (Contributed by Asger C. Ipsen, 1-Jul-2021.) (Revised by Asger C. Ipsen, 7-Jul-2021.)
Hypotheses
Ref Expression
knoppndvlem14.t ๐‘‡ = (๐‘ฅ โˆˆ โ„ โ†ฆ (absโ€˜((โŒŠโ€˜(๐‘ฅ + (1 / 2))) โˆ’ ๐‘ฅ)))
knoppndvlem14.f ๐น = (๐‘ฆ โˆˆ โ„ โ†ฆ (๐‘› โˆˆ โ„•0 โ†ฆ ((๐ถโ†‘๐‘›) ยท (๐‘‡โ€˜(((2 ยท ๐‘)โ†‘๐‘›) ยท ๐‘ฆ)))))
knoppndvlem14.a ๐ด = ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ๐‘€)
knoppndvlem14.b ๐ต = ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท (๐‘€ + 1))
knoppndvlem14.c (๐œ‘ โ†’ ๐ถ โˆˆ (-1(,)1))
knoppndvlem14.j (๐œ‘ โ†’ ๐ฝ โˆˆ โ„•0)
knoppndvlem14.m (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
knoppndvlem14.n (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
knoppndvlem14.1 (๐œ‘ โ†’ 1 < (๐‘ ยท (absโ€˜๐ถ)))
Assertion
Ref Expression
knoppndvlem14 (๐œ‘ โ†’ (absโ€˜(ฮฃ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))((๐นโ€˜๐ต)โ€˜๐‘–) โˆ’ ฮฃ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))((๐นโ€˜๐ด)โ€˜๐‘–))) โ‰ค ((((absโ€˜๐ถ)โ†‘๐ฝ) / 2) ยท (1 / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1))))
Distinct variable groups:   ๐ด,๐‘–,๐‘›,๐‘ฆ   ๐‘ฅ,๐ด,๐‘–   ๐ต,๐‘–,๐‘›,๐‘ฆ   ๐‘ฅ,๐ต   ๐ถ,๐‘–,๐‘›,๐‘ฆ   ๐‘–,๐ฝ,๐‘›,๐‘ฆ   ๐‘–,๐‘,๐‘›,๐‘ฆ   ๐‘ฅ,๐‘   ๐‘‡,๐‘›,๐‘ฆ   ๐œ‘,๐‘–,๐‘›,๐‘ฆ
Allowed substitution hints:   ๐œ‘(๐‘ฅ)   ๐ถ(๐‘ฅ)   ๐‘‡(๐‘ฅ,๐‘–)   ๐น(๐‘ฅ,๐‘ฆ,๐‘–,๐‘›)   ๐ฝ(๐‘ฅ)   ๐‘€(๐‘ฅ,๐‘ฆ,๐‘–,๐‘›)

Proof of Theorem knoppndvlem14
StepHypRef Expression
1 knoppndvlem14.t . . . . . 6 ๐‘‡ = (๐‘ฅ โˆˆ โ„ โ†ฆ (absโ€˜((โŒŠโ€˜(๐‘ฅ + (1 / 2))) โˆ’ ๐‘ฅ)))
2 knoppndvlem14.f . . . . . 6 ๐น = (๐‘ฆ โˆˆ โ„ โ†ฆ (๐‘› โˆˆ โ„•0 โ†ฆ ((๐ถโ†‘๐‘›) ยท (๐‘‡โ€˜(((2 ยท ๐‘)โ†‘๐‘›) ยท ๐‘ฆ)))))
3 knoppndvlem14.b . . . . . . . 8 ๐ต = ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท (๐‘€ + 1))
43a1i 11 . . . . . . 7 (๐œ‘ โ†’ ๐ต = ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท (๐‘€ + 1)))
5 knoppndvlem14.n . . . . . . . 8 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
6 knoppndvlem14.j . . . . . . . . 9 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„•0)
76nn0zd 12534 . . . . . . . 8 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„ค)
8 knoppndvlem14.m . . . . . . . . 9 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
98peano2zd 12619 . . . . . . . 8 (๐œ‘ โ†’ (๐‘€ + 1) โˆˆ โ„ค)
105, 7, 9knoppndvlem1 35051 . . . . . . 7 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท (๐‘€ + 1)) โˆˆ โ„)
114, 10eqeltrd 2832 . . . . . 6 (๐œ‘ โ†’ ๐ต โˆˆ โ„)
12 knoppndvlem14.c . . . . . . . 8 (๐œ‘ โ†’ ๐ถ โˆˆ (-1(,)1))
1312knoppndvlem3 35053 . . . . . . 7 (๐œ‘ โ†’ (๐ถ โˆˆ โ„ โˆง (absโ€˜๐ถ) < 1))
1413simpld 495 . . . . . 6 (๐œ‘ โ†’ ๐ถ โˆˆ โ„)
151, 2, 11, 14, 5knoppndvlem5 35055 . . . . 5 (๐œ‘ โ†’ ฮฃ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))((๐นโ€˜๐ต)โ€˜๐‘–) โˆˆ โ„)
16 knoppndvlem14.a . . . . . . . 8 ๐ด = ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ๐‘€)
1716a1i 11 . . . . . . 7 (๐œ‘ โ†’ ๐ด = ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ๐‘€))
185, 7, 8knoppndvlem1 35051 . . . . . . 7 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ๐‘€) โˆˆ โ„)
1917, 18eqeltrd 2832 . . . . . 6 (๐œ‘ โ†’ ๐ด โˆˆ โ„)
201, 2, 19, 14, 5knoppndvlem5 35055 . . . . 5 (๐œ‘ โ†’ ฮฃ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))((๐นโ€˜๐ด)โ€˜๐‘–) โˆˆ โ„)
2115, 20resubcld 11592 . . . 4 (๐œ‘ โ†’ (ฮฃ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))((๐นโ€˜๐ต)โ€˜๐‘–) โˆ’ ฮฃ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))((๐นโ€˜๐ด)โ€˜๐‘–)) โˆˆ โ„)
2221recnd 11192 . . 3 (๐œ‘ โ†’ (ฮฃ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))((๐นโ€˜๐ต)โ€˜๐‘–) โˆ’ ฮฃ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))((๐นโ€˜๐ด)โ€˜๐‘–)) โˆˆ โ„‚)
2322abscld 15333 . 2 (๐œ‘ โ†’ (absโ€˜(ฮฃ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))((๐นโ€˜๐ต)โ€˜๐‘–) โˆ’ ฮฃ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))((๐นโ€˜๐ด)โ€˜๐‘–))) โˆˆ โ„)
2411, 19resubcld 11592 . . . . 5 (๐œ‘ โ†’ (๐ต โˆ’ ๐ด) โˆˆ โ„)
2524recnd 11192 . . . 4 (๐œ‘ โ†’ (๐ต โˆ’ ๐ด) โˆˆ โ„‚)
2625abscld 15333 . . 3 (๐œ‘ โ†’ (absโ€˜(๐ต โˆ’ ๐ด)) โˆˆ โ„)
27 fzfid 13888 . . . 4 (๐œ‘ โ†’ (0...(๐ฝ โˆ’ 1)) โˆˆ Fin)
28 2re 12236 . . . . . . . . 9 2 โˆˆ โ„
2928a1i 11 . . . . . . . 8 (๐œ‘ โ†’ 2 โˆˆ โ„)
30 nnre 12169 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„)
315, 30syl 17 . . . . . . . 8 (๐œ‘ โ†’ ๐‘ โˆˆ โ„)
3229, 31remulcld 11194 . . . . . . 7 (๐œ‘ โ†’ (2 ยท ๐‘) โˆˆ โ„)
3314recnd 11192 . . . . . . . 8 (๐œ‘ โ†’ ๐ถ โˆˆ โ„‚)
3433abscld 15333 . . . . . . 7 (๐œ‘ โ†’ (absโ€˜๐ถ) โˆˆ โ„)
3532, 34remulcld 11194 . . . . . 6 (๐œ‘ โ†’ ((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆˆ โ„)
3635adantr 481 . . . . 5 ((๐œ‘ โˆง ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))) โ†’ ((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆˆ โ„)
37 elfznn0 13544 . . . . . 6 (๐‘– โˆˆ (0...(๐ฝ โˆ’ 1)) โ†’ ๐‘– โˆˆ โ„•0)
3837adantl 482 . . . . 5 ((๐œ‘ โˆง ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))) โ†’ ๐‘– โˆˆ โ„•0)
3936, 38reexpcld 14078 . . . 4 ((๐œ‘ โˆง ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))) โ†’ (((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐‘–) โˆˆ โ„)
4027, 39fsumrecl 15630 . . 3 (๐œ‘ โ†’ ฮฃ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))(((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐‘–) โˆˆ โ„)
4126, 40remulcld 11194 . 2 (๐œ‘ โ†’ ((absโ€˜(๐ต โˆ’ ๐ด)) ยท ฮฃ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))(((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐‘–)) โˆˆ โ„)
4234, 6reexpcld 14078 . . . 4 (๐œ‘ โ†’ ((absโ€˜๐ถ)โ†‘๐ฝ) โˆˆ โ„)
43 2ne0 12266 . . . . 5 2 โ‰  0
4443a1i 11 . . . 4 (๐œ‘ โ†’ 2 โ‰  0)
4542, 29, 44redivcld 11992 . . 3 (๐œ‘ โ†’ (((absโ€˜๐ถ)โ†‘๐ฝ) / 2) โˆˆ โ„)
46 1red 11165 . . . 4 (๐œ‘ โ†’ 1 โˆˆ โ„)
4735, 46resubcld 11592 . . . 4 (๐œ‘ โ†’ (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1) โˆˆ โ„)
48 0red 11167 . . . . . 6 (๐œ‘ โ†’ 0 โˆˆ โ„)
49 0lt1 11686 . . . . . . . 8 0 < 1
5049a1i 11 . . . . . . 7 (๐œ‘ โ†’ 0 < 1)
51 knoppndvlem14.1 . . . . . . . . 9 (๐œ‘ โ†’ 1 < (๐‘ ยท (absโ€˜๐ถ)))
5212, 5, 51knoppndvlem12 35062 . . . . . . . 8 (๐œ‘ โ†’ (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โ‰  1 โˆง 1 < (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1)))
5352simprd 496 . . . . . . 7 (๐œ‘ โ†’ 1 < (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1))
5448, 46, 47, 50, 53lttrd 11325 . . . . . 6 (๐œ‘ โ†’ 0 < (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1))
5548, 54jca 512 . . . . 5 (๐œ‘ โ†’ (0 โˆˆ โ„ โˆง 0 < (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1)))
56 ltne 11261 . . . . 5 ((0 โˆˆ โ„ โˆง 0 < (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1)) โ†’ (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1) โ‰  0)
5755, 56syl 17 . . . 4 (๐œ‘ โ†’ (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1) โ‰  0)
5846, 47, 57redivcld 11992 . . 3 (๐œ‘ โ†’ (1 / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1)) โˆˆ โ„)
5945, 58remulcld 11194 . 2 (๐œ‘ โ†’ ((((absโ€˜๐ถ)โ†‘๐ฝ) / 2) ยท (1 / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1))) โˆˆ โ„)
601, 2, 19, 11, 12, 6, 5knoppndvlem11 35061 . 2 (๐œ‘ โ†’ (absโ€˜(ฮฃ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))((๐นโ€˜๐ต)โ€˜๐‘–) โˆ’ ฮฃ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))((๐นโ€˜๐ด)โ€˜๐‘–))) โ‰ค ((absโ€˜(๐ต โˆ’ ๐ด)) ยท ฮฃ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))(((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐‘–)))
614, 17oveq12d 7380 . . . . . . 7 (๐œ‘ โ†’ (๐ต โˆ’ ๐ด) = (((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท (๐‘€ + 1)) โˆ’ ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ๐‘€)))
6229recnd 11192 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 2 โˆˆ โ„‚)
6331recnd 11192 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘ โˆˆ โ„‚)
64 nnge1 12190 . . . . . . . . . . . . . . . . . 18 (๐‘ โˆˆ โ„• โ†’ 1 โ‰ค ๐‘)
655, 64syl 17 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 1 โ‰ค ๐‘)
6648, 46, 31, 50, 65ltletrd 11324 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 0 < ๐‘)
6748, 66jca 512 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (0 โˆˆ โ„ โˆง 0 < ๐‘))
68 ltne 11261 . . . . . . . . . . . . . . 15 ((0 โˆˆ โ„ โˆง 0 < ๐‘) โ†’ ๐‘ โ‰  0)
6967, 68syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘ โ‰  0)
7062, 63, 44, 69mulne0d 11816 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (2 ยท ๐‘) โ‰  0)
717znegcld 12618 . . . . . . . . . . . . 13 (๐œ‘ โ†’ -๐ฝ โˆˆ โ„ค)
7232, 70, 71reexpclzd 14162 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((2 ยท ๐‘)โ†‘-๐ฝ) โˆˆ โ„)
7372, 29, 44redivcld 11992 . . . . . . . . . . 11 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘-๐ฝ) / 2) โˆˆ โ„)
7473recnd 11192 . . . . . . . . . 10 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘-๐ฝ) / 2) โˆˆ โ„‚)
759zcnd 12617 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘€ + 1) โˆˆ โ„‚)
768zcnd 12617 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„‚)
7774, 75, 76subdid 11620 . . . . . . . . 9 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ((๐‘€ + 1) โˆ’ ๐‘€)) = (((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท (๐‘€ + 1)) โˆ’ ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ๐‘€)))
7877eqcomd 2737 . . . . . . . 8 (๐œ‘ โ†’ (((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท (๐‘€ + 1)) โˆ’ ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ๐‘€)) = ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ((๐‘€ + 1) โˆ’ ๐‘€)))
79 1cnd 11159 . . . . . . . . . 10 (๐œ‘ โ†’ 1 โˆˆ โ„‚)
8076, 79pncan2d 11523 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘€ + 1) โˆ’ ๐‘€) = 1)
8180oveq2d 7378 . . . . . . . 8 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ((๐‘€ + 1) โˆ’ ๐‘€)) = ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท 1))
8274mulridd 11181 . . . . . . . 8 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท 1) = (((2 ยท ๐‘)โ†‘-๐ฝ) / 2))
8378, 81, 823eqtrd 2775 . . . . . . 7 (๐œ‘ โ†’ (((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท (๐‘€ + 1)) โˆ’ ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ๐‘€)) = (((2 ยท ๐‘)โ†‘-๐ฝ) / 2))
8461, 83eqtrd 2771 . . . . . 6 (๐œ‘ โ†’ (๐ต โˆ’ ๐ด) = (((2 ยท ๐‘)โ†‘-๐ฝ) / 2))
8584fveq2d 6851 . . . . 5 (๐œ‘ โ†’ (absโ€˜(๐ต โˆ’ ๐ด)) = (absโ€˜(((2 ยท ๐‘)โ†‘-๐ฝ) / 2)))
8672recnd 11192 . . . . . . 7 (๐œ‘ โ†’ ((2 ยท ๐‘)โ†‘-๐ฝ) โˆˆ โ„‚)
8786, 62, 44absdivd 15352 . . . . . 6 (๐œ‘ โ†’ (absโ€˜(((2 ยท ๐‘)โ†‘-๐ฝ) / 2)) = ((absโ€˜((2 ยท ๐‘)โ†‘-๐ฝ)) / (absโ€˜2)))
8862, 63mulcld 11184 . . . . . . . . . 10 (๐œ‘ โ†’ (2 ยท ๐‘) โˆˆ โ„‚)
8988, 70, 713jca 1128 . . . . . . . . 9 (๐œ‘ โ†’ ((2 ยท ๐‘) โˆˆ โ„‚ โˆง (2 ยท ๐‘) โ‰  0 โˆง -๐ฝ โˆˆ โ„ค))
90 absexpz 15202 . . . . . . . . 9 (((2 ยท ๐‘) โˆˆ โ„‚ โˆง (2 ยท ๐‘) โ‰  0 โˆง -๐ฝ โˆˆ โ„ค) โ†’ (absโ€˜((2 ยท ๐‘)โ†‘-๐ฝ)) = ((absโ€˜(2 ยท ๐‘))โ†‘-๐ฝ))
9189, 90syl 17 . . . . . . . 8 (๐œ‘ โ†’ (absโ€˜((2 ยท ๐‘)โ†‘-๐ฝ)) = ((absโ€˜(2 ยท ๐‘))โ†‘-๐ฝ))
9262, 63absmuld 15351 . . . . . . . . . 10 (๐œ‘ โ†’ (absโ€˜(2 ยท ๐‘)) = ((absโ€˜2) ยท (absโ€˜๐‘)))
93 0le2 12264 . . . . . . . . . . . . . 14 0 โ‰ค 2
9428, 93pm3.2i 471 . . . . . . . . . . . . 13 (2 โˆˆ โ„ โˆง 0 โ‰ค 2)
95 absid 15193 . . . . . . . . . . . . 13 ((2 โˆˆ โ„ โˆง 0 โ‰ค 2) โ†’ (absโ€˜2) = 2)
9694, 95ax-mp 5 . . . . . . . . . . . 12 (absโ€˜2) = 2
9796a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ (absโ€˜2) = 2)
9848, 31, 66ltled 11312 . . . . . . . . . . . 12 (๐œ‘ โ†’ 0 โ‰ค ๐‘)
9931, 98absidd 15319 . . . . . . . . . . 11 (๐œ‘ โ†’ (absโ€˜๐‘) = ๐‘)
10097, 99oveq12d 7380 . . . . . . . . . 10 (๐œ‘ โ†’ ((absโ€˜2) ยท (absโ€˜๐‘)) = (2 ยท ๐‘))
10192, 100eqtrd 2771 . . . . . . . . 9 (๐œ‘ โ†’ (absโ€˜(2 ยท ๐‘)) = (2 ยท ๐‘))
102101oveq1d 7377 . . . . . . . 8 (๐œ‘ โ†’ ((absโ€˜(2 ยท ๐‘))โ†‘-๐ฝ) = ((2 ยท ๐‘)โ†‘-๐ฝ))
10391, 102eqtrd 2771 . . . . . . 7 (๐œ‘ โ†’ (absโ€˜((2 ยท ๐‘)โ†‘-๐ฝ)) = ((2 ยท ๐‘)โ†‘-๐ฝ))
104103, 97oveq12d 7380 . . . . . 6 (๐œ‘ โ†’ ((absโ€˜((2 ยท ๐‘)โ†‘-๐ฝ)) / (absโ€˜2)) = (((2 ยท ๐‘)โ†‘-๐ฝ) / 2))
10587, 104eqtrd 2771 . . . . 5 (๐œ‘ โ†’ (absโ€˜(((2 ยท ๐‘)โ†‘-๐ฝ) / 2)) = (((2 ยท ๐‘)โ†‘-๐ฝ) / 2))
10685, 105eqtrd 2771 . . . 4 (๐œ‘ โ†’ (absโ€˜(๐ต โˆ’ ๐ด)) = (((2 ยท ๐‘)โ†‘-๐ฝ) / 2))
10735recnd 11192 . . . . . 6 (๐œ‘ โ†’ ((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆˆ โ„‚)
10852simpld 495 . . . . . 6 (๐œ‘ โ†’ ((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โ‰  1)
109107, 108, 6geoser 15763 . . . . 5 (๐œ‘ โ†’ ฮฃ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))(((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐‘–) = ((1 โˆ’ (((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ)) / (1 โˆ’ ((2 ยท ๐‘) ยท (absโ€˜๐ถ)))))
110107, 6expcld 14061 . . . . . 6 (๐œ‘ โ†’ (((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) โˆˆ โ„‚)
111108necomd 2995 . . . . . 6 (๐œ‘ โ†’ 1 โ‰  ((2 ยท ๐‘) ยท (absโ€˜๐ถ)))
11279, 110, 79, 107, 111div2subd 11990 . . . . 5 (๐œ‘ โ†’ ((1 โˆ’ (((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ)) / (1 โˆ’ ((2 ยท ๐‘) ยท (absโ€˜๐ถ)))) = (((((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) โˆ’ 1) / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1)))
113109, 112eqtrd 2771 . . . 4 (๐œ‘ โ†’ ฮฃ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))(((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐‘–) = (((((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) โˆ’ 1) / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1)))
114106, 113oveq12d 7380 . . 3 (๐œ‘ โ†’ ((absโ€˜(๐ต โˆ’ ๐ด)) ยท ฮฃ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))(((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐‘–)) = ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท (((((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) โˆ’ 1) / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1))))
115113, 40eqeltrrd 2833 . . . . 5 (๐œ‘ โ†’ (((((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) โˆ’ 1) / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1)) โˆˆ โ„)
11635, 6reexpcld 14078 . . . . . 6 (๐œ‘ โ†’ (((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) โˆˆ โ„)
117116, 47, 57redivcld 11992 . . . . 5 (๐œ‘ โ†’ ((((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1)) โˆˆ โ„)
118 2rp 12929 . . . . . . 7 2 โˆˆ โ„+
119118a1i 11 . . . . . 6 (๐œ‘ โ†’ 2 โˆˆ โ„+)
120119rpgt0d 12969 . . . . . . . . . 10 (๐œ‘ โ†’ 0 < 2)
12129, 31, 120, 66mulgt0d 11319 . . . . . . . . 9 (๐œ‘ โ†’ 0 < (2 ยท ๐‘))
12232, 71, 1213jca 1128 . . . . . . . 8 (๐œ‘ โ†’ ((2 ยท ๐‘) โˆˆ โ„ โˆง -๐ฝ โˆˆ โ„ค โˆง 0 < (2 ยท ๐‘)))
123 expgt0 14011 . . . . . . . 8 (((2 ยท ๐‘) โˆˆ โ„ โˆง -๐ฝ โˆˆ โ„ค โˆง 0 < (2 ยท ๐‘)) โ†’ 0 < ((2 ยท ๐‘)โ†‘-๐ฝ))
124122, 123syl 17 . . . . . . 7 (๐œ‘ โ†’ 0 < ((2 ยท ๐‘)โ†‘-๐ฝ))
12548, 72, 124ltled 11312 . . . . . 6 (๐œ‘ โ†’ 0 โ‰ค ((2 ยท ๐‘)โ†‘-๐ฝ))
12672, 119, 125divge0d 13006 . . . . 5 (๐œ‘ โ†’ 0 โ‰ค (((2 ยท ๐‘)โ†‘-๐ฝ) / 2))
127116, 46resubcld 11592 . . . . . 6 (๐œ‘ โ†’ ((((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) โˆ’ 1) โˆˆ โ„)
12847, 54elrpd 12963 . . . . . 6 (๐œ‘ โ†’ (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1) โˆˆ โ„+)
129116lem1d 12097 . . . . . 6 (๐œ‘ โ†’ ((((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) โˆ’ 1) โ‰ค (((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ))
130127, 116, 128, 129lediv1dd 13024 . . . . 5 (๐œ‘ โ†’ (((((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) โˆ’ 1) / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1)) โ‰ค ((((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1)))
131115, 117, 73, 126, 130lemul2ad 12104 . . . 4 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท (((((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) โˆ’ 1) / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1))) โ‰ค ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ((((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1))))
13247recnd 11192 . . . . . . 7 (๐œ‘ โ†’ (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1) โˆˆ โ„‚)
133110, 132, 57divrecd 11943 . . . . . 6 (๐œ‘ โ†’ ((((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1)) = ((((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) ยท (1 / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1))))
134133oveq2d 7378 . . . . 5 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ((((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1))) = ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ((((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) ยท (1 / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1)))))
13558recnd 11192 . . . . . . 7 (๐œ‘ โ†’ (1 / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1)) โˆˆ โ„‚)
13674, 110, 135mulassd 11187 . . . . . 6 (๐œ‘ โ†’ (((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท (((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ)) ยท (1 / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1))) = ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ((((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) ยท (1 / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1)))))
137136eqcomd 2737 . . . . 5 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ((((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) ยท (1 / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1)))) = (((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท (((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ)) ยท (1 / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1))))
13886, 110, 62, 44div23d 11977 . . . . . . . 8 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘-๐ฝ) ยท (((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ)) / 2) = ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท (((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ)))
139138eqcomd 2737 . . . . . . 7 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท (((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ)) = ((((2 ยท ๐‘)โ†‘-๐ฝ) ยท (((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ)) / 2))
14088, 70jca 512 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((2 ยท ๐‘) โˆˆ โ„‚ โˆง (2 ยท ๐‘) โ‰  0))
14134recnd 11192 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (absโ€˜๐ถ) โˆˆ โ„‚)
14212, 5, 51knoppndvlem13 35063 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐ถ โ‰  0)
14333, 142absne0d 15344 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (absโ€˜๐ถ) โ‰  0)
144141, 143jca 512 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((absโ€˜๐ถ) โˆˆ โ„‚ โˆง (absโ€˜๐ถ) โ‰  0))
145140, 144, 73jca 1128 . . . . . . . . . . 11 (๐œ‘ โ†’ (((2 ยท ๐‘) โˆˆ โ„‚ โˆง (2 ยท ๐‘) โ‰  0) โˆง ((absโ€˜๐ถ) โˆˆ โ„‚ โˆง (absโ€˜๐ถ) โ‰  0) โˆง ๐ฝ โˆˆ โ„ค))
146 mulexpz 14018 . . . . . . . . . . 11 ((((2 ยท ๐‘) โˆˆ โ„‚ โˆง (2 ยท ๐‘) โ‰  0) โˆง ((absโ€˜๐ถ) โˆˆ โ„‚ โˆง (absโ€˜๐ถ) โ‰  0) โˆง ๐ฝ โˆˆ โ„ค) โ†’ (((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) = (((2 ยท ๐‘)โ†‘๐ฝ) ยท ((absโ€˜๐ถ)โ†‘๐ฝ)))
147145, 146syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ (((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) = (((2 ยท ๐‘)โ†‘๐ฝ) ยท ((absโ€˜๐ถ)โ†‘๐ฝ)))
148147oveq2d 7378 . . . . . . . . 9 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘-๐ฝ) ยท (((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ)) = (((2 ยท ๐‘)โ†‘-๐ฝ) ยท (((2 ยท ๐‘)โ†‘๐ฝ) ยท ((absโ€˜๐ถ)โ†‘๐ฝ))))
14988, 6expcld 14061 . . . . . . . . . . 11 (๐œ‘ โ†’ ((2 ยท ๐‘)โ†‘๐ฝ) โˆˆ โ„‚)
15042recnd 11192 . . . . . . . . . . 11 (๐œ‘ โ†’ ((absโ€˜๐ถ)โ†‘๐ฝ) โˆˆ โ„‚)
15186, 149, 150mulassd 11187 . . . . . . . . . 10 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘-๐ฝ) ยท ((2 ยท ๐‘)โ†‘๐ฝ)) ยท ((absโ€˜๐ถ)โ†‘๐ฝ)) = (((2 ยท ๐‘)โ†‘-๐ฝ) ยท (((2 ยท ๐‘)โ†‘๐ฝ) ยท ((absโ€˜๐ถ)โ†‘๐ฝ))))
152151eqcomd 2737 . . . . . . . . 9 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘-๐ฝ) ยท (((2 ยท ๐‘)โ†‘๐ฝ) ยท ((absโ€˜๐ถ)โ†‘๐ฝ))) = ((((2 ยท ๐‘)โ†‘-๐ฝ) ยท ((2 ยท ๐‘)โ†‘๐ฝ)) ยท ((absโ€˜๐ถ)โ†‘๐ฝ)))
153140, 71, 7jca32 516 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((2 ยท ๐‘) โˆˆ โ„‚ โˆง (2 ยท ๐‘) โ‰  0) โˆง (-๐ฝ โˆˆ โ„ค โˆง ๐ฝ โˆˆ โ„ค)))
154 expaddz 14022 . . . . . . . . . . . . . 14 ((((2 ยท ๐‘) โˆˆ โ„‚ โˆง (2 ยท ๐‘) โ‰  0) โˆง (-๐ฝ โˆˆ โ„ค โˆง ๐ฝ โˆˆ โ„ค)) โ†’ ((2 ยท ๐‘)โ†‘(-๐ฝ + ๐ฝ)) = (((2 ยท ๐‘)โ†‘-๐ฝ) ยท ((2 ยท ๐‘)โ†‘๐ฝ)))
155153, 154syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((2 ยท ๐‘)โ†‘(-๐ฝ + ๐ฝ)) = (((2 ยท ๐‘)โ†‘-๐ฝ) ยท ((2 ยท ๐‘)โ†‘๐ฝ)))
156155eqcomd 2737 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘-๐ฝ) ยท ((2 ยท ๐‘)โ†‘๐ฝ)) = ((2 ยท ๐‘)โ†‘(-๐ฝ + ๐ฝ)))
15771zcnd 12617 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ -๐ฝ โˆˆ โ„‚)
1586nn0cnd 12484 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ฝ โˆˆ โ„‚)
159157, 158addcomd 11366 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (-๐ฝ + ๐ฝ) = (๐ฝ + -๐ฝ))
160158negidd 11511 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ฝ + -๐ฝ) = 0)
161159, 160eqtrd 2771 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (-๐ฝ + ๐ฝ) = 0)
162161oveq2d 7378 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((2 ยท ๐‘)โ†‘(-๐ฝ + ๐ฝ)) = ((2 ยท ๐‘)โ†‘0))
16388exp0d 14055 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((2 ยท ๐‘)โ†‘0) = 1)
164156, 162, 1633eqtrd 2775 . . . . . . . . . . 11 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘-๐ฝ) ยท ((2 ยท ๐‘)โ†‘๐ฝ)) = 1)
165164oveq1d 7377 . . . . . . . . . 10 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘-๐ฝ) ยท ((2 ยท ๐‘)โ†‘๐ฝ)) ยท ((absโ€˜๐ถ)โ†‘๐ฝ)) = (1 ยท ((absโ€˜๐ถ)โ†‘๐ฝ)))
166150mullidd 11182 . . . . . . . . . 10 (๐œ‘ โ†’ (1 ยท ((absโ€˜๐ถ)โ†‘๐ฝ)) = ((absโ€˜๐ถ)โ†‘๐ฝ))
167165, 166eqtrd 2771 . . . . . . . . 9 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘-๐ฝ) ยท ((2 ยท ๐‘)โ†‘๐ฝ)) ยท ((absโ€˜๐ถ)โ†‘๐ฝ)) = ((absโ€˜๐ถ)โ†‘๐ฝ))
168148, 152, 1673eqtrd 2775 . . . . . . . 8 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘-๐ฝ) ยท (((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ)) = ((absโ€˜๐ถ)โ†‘๐ฝ))
169168oveq1d 7377 . . . . . . 7 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘-๐ฝ) ยท (((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ)) / 2) = (((absโ€˜๐ถ)โ†‘๐ฝ) / 2))
170139, 169eqtrd 2771 . . . . . 6 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท (((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ)) = (((absโ€˜๐ถ)โ†‘๐ฝ) / 2))
171170oveq1d 7377 . . . . 5 (๐œ‘ โ†’ (((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท (((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ)) ยท (1 / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1))) = ((((absโ€˜๐ถ)โ†‘๐ฝ) / 2) ยท (1 / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1))))
172134, 137, 1713eqtrd 2775 . . . 4 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท ((((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1))) = ((((absโ€˜๐ถ)โ†‘๐ฝ) / 2) ยท (1 / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1))))
173131, 172breqtrd 5136 . . 3 (๐œ‘ โ†’ ((((2 ยท ๐‘)โ†‘-๐ฝ) / 2) ยท (((((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐ฝ) โˆ’ 1) / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1))) โ‰ค ((((absโ€˜๐ถ)โ†‘๐ฝ) / 2) ยท (1 / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1))))
174114, 173eqbrtrd 5132 . 2 (๐œ‘ โ†’ ((absโ€˜(๐ต โˆ’ ๐ด)) ยท ฮฃ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))(((2 ยท ๐‘) ยท (absโ€˜๐ถ))โ†‘๐‘–)) โ‰ค ((((absโ€˜๐ถ)โ†‘๐ฝ) / 2) ยท (1 / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1))))
17523, 41, 59, 60, 174letrd 11321 1 (๐œ‘ โ†’ (absโ€˜(ฮฃ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))((๐นโ€˜๐ต)โ€˜๐‘–) โˆ’ ฮฃ๐‘– โˆˆ (0...(๐ฝ โˆ’ 1))((๐นโ€˜๐ด)โ€˜๐‘–))) โ‰ค ((((absโ€˜๐ถ)โ†‘๐ฝ) / 2) ยท (1 / (((2 ยท ๐‘) ยท (absโ€˜๐ถ)) โˆ’ 1))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 396   โˆง w3a 1087   = wceq 1541   โˆˆ wcel 2106   โ‰  wne 2939   class class class wbr 5110   โ†ฆ cmpt 5193  โ€˜cfv 6501  (class class class)co 7362  โ„‚cc 11058  โ„cr 11059  0cc0 11060  1c1 11061   + caddc 11063   ยท cmul 11065   < clt 11198   โ‰ค cle 11199   โˆ’ cmin 11394  -cneg 11395   / cdiv 11821  โ„•cn 12162  2c2 12217  โ„•0cn0 12422  โ„คcz 12508  โ„+crp 12924  (,)cioo 13274  ...cfz 13434  โŒŠcfl 13705  โ†‘cexp 13977  abscabs 15131  ฮฃcsu 15582
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 2702  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9586  ax-cnex 11116  ax-resscn 11117  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-addrcl 11121  ax-mulcl 11122  ax-mulrcl 11123  ax-mulcom 11124  ax-addass 11125  ax-mulass 11126  ax-distr 11127  ax-i2m1 11128  ax-1ne0 11129  ax-1rid 11130  ax-rnegex 11131  ax-rrecex 11132  ax-cnre 11133  ax-pre-lttri 11134  ax-pre-lttrn 11135  ax-pre-ltadd 11136  ax-pre-mulgt0 11137  ax-pre-sup 11138
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 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9387  df-inf 9388  df-oi 9455  df-card 9884  df-pnf 11200  df-mnf 11201  df-xr 11202  df-ltxr 11203  df-le 11204  df-sub 11396  df-neg 11397  df-div 11822  df-nn 12163  df-2 12225  df-3 12226  df-n0 12423  df-z 12509  df-uz 12773  df-rp 12925  df-ioo 13278  df-ico 13280  df-fz 13435  df-fzo 13578  df-fl 13707  df-seq 13917  df-exp 13978  df-hash 14241  df-cj 14996  df-re 14997  df-im 14998  df-sqrt 15132  df-abs 15133  df-clim 15382  df-sum 15583
This theorem is referenced by:  knoppndvlem15  35065
  Copyright terms: Public domain W3C validator