Users' Mathboxes Mathbox for Jim Kingdon < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  trilpolemlt1 GIF version

Theorem trilpolemlt1 14792
Description: Lemma for trilpo 14794. The ๐ด < 1 case. We can use the distance between ๐ด and one (that is, 1 โˆ’ ๐ด) to find a position in the sequence ๐‘› where terms after that point will not add up to as much as 1 โˆ’ ๐ด. By finomni 7138 we know the terms up to ๐‘› either contain a zero or are all one. But if they are all one that contradicts the way we constructed ๐‘›, so we know that the sequence contains a zero. (Contributed by Jim Kingdon, 23-Aug-2023.)
Hypotheses
Ref Expression
trilpolemgt1.f (๐œ‘ โ†’ ๐น:โ„•โŸถ{0, 1})
trilpolemgt1.a ๐ด = ฮฃ๐‘– โˆˆ โ„• ((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–))
trilpolemlt1.a (๐œ‘ โ†’ ๐ด < 1)
Assertion
Ref Expression
trilpolemlt1 (๐œ‘ โ†’ โˆƒ๐‘ฅ โˆˆ โ„• (๐นโ€˜๐‘ฅ) = 0)
Distinct variable groups:   ๐ด,๐‘–,๐‘ฅ   ๐‘ฅ,๐น,๐‘–   ๐œ‘,๐‘–,๐‘ฅ

Proof of Theorem trilpolemlt1
Dummy variables ๐‘› ๐‘“ ๐‘— are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1red 7972 . . . 4 (๐œ‘ โ†’ 1 โˆˆ โ„)
2 trilpolemgt1.f . . . . 5 (๐œ‘ โ†’ ๐น:โ„•โŸถ{0, 1})
3 trilpolemgt1.a . . . . 5 ๐ด = ฮฃ๐‘– โˆˆ โ„• ((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–))
42, 3trilpolemcl 14788 . . . 4 (๐œ‘ โ†’ ๐ด โˆˆ โ„)
51, 4resubcld 8338 . . 3 (๐œ‘ โ†’ (1 โˆ’ ๐ด) โˆˆ โ„)
6 trilpolemlt1.a . . . 4 (๐œ‘ โ†’ ๐ด < 1)
74, 1posdifd 8489 . . . 4 (๐œ‘ โ†’ (๐ด < 1 โ†” 0 < (1 โˆ’ ๐ด)))
86, 7mpbid 147 . . 3 (๐œ‘ โ†’ 0 < (1 โˆ’ ๐ด))
9 nnrecl 9174 . . 3 (((1 โˆ’ ๐ด) โˆˆ โ„ โˆง 0 < (1 โˆ’ ๐ด)) โ†’ โˆƒ๐‘› โˆˆ โ„• (1 / ๐‘›) < (1 โˆ’ ๐ด))
105, 8, 9syl2anc 411 . 2 (๐œ‘ โ†’ โˆƒ๐‘› โˆˆ โ„• (1 / ๐‘›) < (1 โˆ’ ๐ด))
11 elfznn 10054 . . . . . . 7 (๐‘ฅ โˆˆ (1...๐‘›) โ†’ ๐‘ฅ โˆˆ โ„•)
1211ad2antrl 490 . . . . . 6 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง (๐‘ฅ โˆˆ (1...๐‘›) โˆง ((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 0)) โ†’ ๐‘ฅ โˆˆ โ„•)
13 simprl 529 . . . . . . . 8 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง (๐‘ฅ โˆˆ (1...๐‘›) โˆง ((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 0)) โ†’ ๐‘ฅ โˆˆ (1...๐‘›))
1413fvresd 5541 . . . . . . 7 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง (๐‘ฅ โˆˆ (1...๐‘›) โˆง ((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 0)) โ†’ ((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = (๐นโ€˜๐‘ฅ))
15 simprr 531 . . . . . . 7 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง (๐‘ฅ โˆˆ (1...๐‘›) โˆง ((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 0)) โ†’ ((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 0)
1614, 15eqtr3d 2212 . . . . . 6 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง (๐‘ฅ โˆˆ (1...๐‘›) โˆง ((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 0)) โ†’ (๐นโ€˜๐‘ฅ) = 0)
1712, 16jca 306 . . . . 5 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง (๐‘ฅ โˆˆ (1...๐‘›) โˆง ((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 0)) โ†’ (๐‘ฅ โˆˆ โ„• โˆง (๐นโ€˜๐‘ฅ) = 0))
1817ex 115 . . . 4 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ ((๐‘ฅ โˆˆ (1...๐‘›) โˆง ((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 0) โ†’ (๐‘ฅ โˆˆ โ„• โˆง (๐นโ€˜๐‘ฅ) = 0)))
1918reximdv2 2576 . . 3 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ (โˆƒ๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 0 โ†’ โˆƒ๐‘ฅ โˆˆ โ„• (๐นโ€˜๐‘ฅ) = 0))
20 2rp 9658 . . . . . . . . . 10 2 โˆˆ โ„+
2120a1i 9 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ 2 โˆˆ โ„+)
22 simprl 529 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ ๐‘› โˆˆ โ„•)
2322nnzd 9374 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ ๐‘› โˆˆ โ„ค)
2421, 23rpexpcld 10678 . . . . . . . 8 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ (2โ†‘๐‘›) โˆˆ โ„+)
2524rprecred 9708 . . . . . . 7 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ (1 / (2โ†‘๐‘›)) โˆˆ โ„)
2622nnrecred 8966 . . . . . . 7 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ (1 / ๐‘›) โˆˆ โ„)
275adantr 276 . . . . . . 7 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ (1 โˆ’ ๐ด) โˆˆ โ„)
28 2z 9281 . . . . . . . . . 10 2 โˆˆ โ„ค
29 uzid 9542 . . . . . . . . . 10 (2 โˆˆ โ„ค โ†’ 2 โˆˆ (โ„คโ‰ฅโ€˜2))
3028, 29mp1i 10 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ 2 โˆˆ (โ„คโ‰ฅโ€˜2))
3122nnnn0d 9229 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ ๐‘› โˆˆ โ„•0)
32 bernneq3 10643 . . . . . . . . 9 ((2 โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘› โˆˆ โ„•0) โ†’ ๐‘› < (2โ†‘๐‘›))
3330, 31, 32syl2anc 411 . . . . . . . 8 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ ๐‘› < (2โ†‘๐‘›))
3422nnrpd 9694 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ ๐‘› โˆˆ โ„+)
3534, 24ltrecd 9715 . . . . . . . 8 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ (๐‘› < (2โ†‘๐‘›) โ†” (1 / (2โ†‘๐‘›)) < (1 / ๐‘›)))
3633, 35mpbid 147 . . . . . . 7 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ (1 / (2โ†‘๐‘›)) < (1 / ๐‘›))
37 simprr 531 . . . . . . 7 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ (1 / ๐‘›) < (1 โˆ’ ๐ด))
3825, 26, 27, 36, 37lttrd 8083 . . . . . 6 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ (1 / (2โ†‘๐‘›)) < (1 โˆ’ ๐ด))
3938adantr 276 . . . . 5 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ (1 / (2โ†‘๐‘›)) < (1 โˆ’ ๐ด))
4027adantr 276 . . . . . 6 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ (1 โˆ’ ๐ด) โˆˆ โ„)
4125adantr 276 . . . . . 6 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ (1 / (2โ†‘๐‘›)) โˆˆ โ„)
42 1red 7972 . . . . . . 7 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ 1 โˆˆ โ„)
434ad2antrr 488 . . . . . . 7 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ ๐ด โˆˆ โ„)
44 0red 7958 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ 0 โˆˆ โ„)
45 eqid 2177 . . . . . . . . . . 11 (โ„คโ‰ฅโ€˜(๐‘› + 1)) = (โ„คโ‰ฅโ€˜(๐‘› + 1))
4622adantr 276 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ ๐‘› โˆˆ โ„•)
4746peano2nnd 8934 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ (๐‘› + 1) โˆˆ โ„•)
4847nnzd 9374 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ (๐‘› + 1) โˆˆ โ„ค)
49 eluznn 9600 . . . . . . . . . . . . 13 (((๐‘› + 1) โˆˆ โ„• โˆง ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ๐‘– โˆˆ โ„•)
5047, 49sylan 283 . . . . . . . . . . . 12 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ๐‘– โˆˆ โ„•)
51 eqid 2177 . . . . . . . . . . . . 13 (๐‘— โˆˆ โ„• โ†ฆ ((1 / (2โ†‘๐‘—)) ยท (๐นโ€˜๐‘—))) = (๐‘— โˆˆ โ„• โ†ฆ ((1 / (2โ†‘๐‘—)) ยท (๐นโ€˜๐‘—)))
52 oveq2 5883 . . . . . . . . . . . . . . 15 (๐‘— = ๐‘– โ†’ (2โ†‘๐‘—) = (2โ†‘๐‘–))
5352oveq2d 5891 . . . . . . . . . . . . . 14 (๐‘— = ๐‘– โ†’ (1 / (2โ†‘๐‘—)) = (1 / (2โ†‘๐‘–)))
54 fveq2 5516 . . . . . . . . . . . . . 14 (๐‘— = ๐‘– โ†’ (๐นโ€˜๐‘—) = (๐นโ€˜๐‘–))
5553, 54oveq12d 5893 . . . . . . . . . . . . 13 (๐‘— = ๐‘– โ†’ ((1 / (2โ†‘๐‘—)) ยท (๐นโ€˜๐‘—)) = ((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–)))
56 simpr 110 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ โ„•) โ†’ ๐‘– โˆˆ โ„•)
5720a1i 9 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ โ„•) โ†’ 2 โˆˆ โ„+)
5856nnzd 9374 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ โ„•) โ†’ ๐‘– โˆˆ โ„ค)
5957, 58rpexpcld 10678 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ โ„•) โ†’ (2โ†‘๐‘–) โˆˆ โ„+)
6059rprecred 9708 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ โ„•) โ†’ (1 / (2โ†‘๐‘–)) โˆˆ โ„)
61 0re 7957 . . . . . . . . . . . . . . . 16 0 โˆˆ โ„
62 1re 7956 . . . . . . . . . . . . . . . 16 1 โˆˆ โ„
63 prssi 3751 . . . . . . . . . . . . . . . 16 ((0 โˆˆ โ„ โˆง 1 โˆˆ โ„) โ†’ {0, 1} โŠ† โ„)
6461, 62, 63mp2an 426 . . . . . . . . . . . . . . 15 {0, 1} โŠ† โ„
652adantr 276 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ ๐น:โ„•โŸถ{0, 1})
6665ad2antrr 488 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ โ„•) โ†’ ๐น:โ„•โŸถ{0, 1})
6766, 56ffvelcdmd 5653 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ โ„•) โ†’ (๐นโ€˜๐‘–) โˆˆ {0, 1})
6864, 67sselid 3154 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ โ„•) โ†’ (๐นโ€˜๐‘–) โˆˆ โ„)
6960, 68remulcld 7988 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ โ„•) โ†’ ((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–)) โˆˆ โ„)
7051, 55, 56, 69fvmptd3 5610 . . . . . . . . . . . 12 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ โ„•) โ†’ ((๐‘— โˆˆ โ„• โ†ฆ ((1 / (2โ†‘๐‘—)) ยท (๐นโ€˜๐‘—)))โ€˜๐‘–) = ((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–)))
7150, 70syldan 282 . . . . . . . . . . 11 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((๐‘— โˆˆ โ„• โ†ฆ ((1 / (2โ†‘๐‘—)) ยท (๐นโ€˜๐‘—)))โ€˜๐‘–) = ((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–)))
7250, 69syldan 282 . . . . . . . . . . 11 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–)) โˆˆ โ„)
7365adantr 276 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ ๐น:โ„•โŸถ{0, 1})
7473, 51trilpolemclim 14787 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ seq1( + , (๐‘— โˆˆ โ„• โ†ฆ ((1 / (2โ†‘๐‘—)) ยท (๐นโ€˜๐‘—)))) โˆˆ dom โ‡ )
75 nnuz 9563 . . . . . . . . . . . . 13 โ„• = (โ„คโ‰ฅโ€˜1)
7669recnd 7986 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ โ„•) โ†’ ((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–)) โˆˆ โ„‚)
7770, 76eqeltrd 2254 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ โ„•) โ†’ ((๐‘— โˆˆ โ„• โ†ฆ ((1 / (2โ†‘๐‘—)) ยท (๐นโ€˜๐‘—)))โ€˜๐‘–) โˆˆ โ„‚)
7875, 47, 77iserex 11347 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ (seq1( + , (๐‘— โˆˆ โ„• โ†ฆ ((1 / (2โ†‘๐‘—)) ยท (๐นโ€˜๐‘—)))) โˆˆ dom โ‡ โ†” seq(๐‘› + 1)( + , (๐‘— โˆˆ โ„• โ†ฆ ((1 / (2โ†‘๐‘—)) ยท (๐นโ€˜๐‘—)))) โˆˆ dom โ‡ ))
7974, 78mpbid 147 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ seq(๐‘› + 1)( + , (๐‘— โˆˆ โ„• โ†ฆ ((1 / (2โ†‘๐‘—)) ยท (๐นโ€˜๐‘—)))) โˆˆ dom โ‡ )
8045, 48, 71, 72, 79isumrecl 11437 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ ฮฃ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–)) โˆˆ โ„)
81 1zzd 9280 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ 1 โˆˆ โ„ค)
8281, 23fzfigd 10431 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ (1...๐‘›) โˆˆ Fin)
8382adantr 276 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ (1...๐‘›) โˆˆ Fin)
8420a1i 9 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ 2 โˆˆ โ„+)
85 elfzelz 10025 . . . . . . . . . . . . . 14 (๐‘– โˆˆ (1...๐‘›) โ†’ ๐‘– โˆˆ โ„ค)
8685adantl 277 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ ๐‘– โˆˆ โ„ค)
8784, 86rpexpcld 10678 . . . . . . . . . . . 12 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ (2โ†‘๐‘–) โˆˆ โ„+)
8887rprecred 9708 . . . . . . . . . . 11 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ (1 / (2โ†‘๐‘–)) โˆˆ โ„)
8983, 88fsumrecl 11409 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ ฮฃ๐‘– โˆˆ (1...๐‘›)(1 / (2โ†‘๐‘–)) โˆˆ โ„)
9050, 60syldan 282 . . . . . . . . . . . 12 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (1 / (2โ†‘๐‘–)) โˆˆ โ„)
9150, 68syldan 282 . . . . . . . . . . . 12 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐นโ€˜๐‘–) โˆˆ โ„)
9259rpreccld 9707 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ โ„•) โ†’ (1 / (2โ†‘๐‘–)) โˆˆ โ„+)
9350, 92syldan 282 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (1 / (2โ†‘๐‘–)) โˆˆ โ„+)
9493rpge0d 9700 . . . . . . . . . . . 12 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ 0 โ‰ค (1 / (2โ†‘๐‘–)))
95 0le0 9008 . . . . . . . . . . . . . 14 0 โ‰ค 0
96 simpr 110 . . . . . . . . . . . . . 14 (((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง (๐นโ€˜๐‘–) = 0) โ†’ (๐นโ€˜๐‘–) = 0)
9795, 96breqtrrid 4042 . . . . . . . . . . . . 13 (((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง (๐นโ€˜๐‘–) = 0) โ†’ 0 โ‰ค (๐นโ€˜๐‘–))
98 0le1 8438 . . . . . . . . . . . . . 14 0 โ‰ค 1
99 simpr 110 . . . . . . . . . . . . . 14 (((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง (๐นโ€˜๐‘–) = 1) โ†’ (๐นโ€˜๐‘–) = 1)
10098, 99breqtrrid 4042 . . . . . . . . . . . . 13 (((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โˆง (๐นโ€˜๐‘–) = 1) โ†’ 0 โ‰ค (๐นโ€˜๐‘–))
10173adantr 276 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ๐น:โ„•โŸถ{0, 1})
102101, 50ffvelcdmd 5653 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ (๐นโ€˜๐‘–) โˆˆ {0, 1})
103 elpri 3616 . . . . . . . . . . . . . 14 ((๐นโ€˜๐‘–) โˆˆ {0, 1} โ†’ ((๐นโ€˜๐‘–) = 0 โˆจ (๐นโ€˜๐‘–) = 1))
104102, 103syl 14 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ ((๐นโ€˜๐‘–) = 0 โˆจ (๐นโ€˜๐‘–) = 1))
10597, 100, 104mpjaodan 798 . . . . . . . . . . . 12 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ 0 โ‰ค (๐นโ€˜๐‘–))
10690, 91, 94, 105mulge0d 8578 . . . . . . . . . . 11 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))) โ†’ 0 โ‰ค ((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–)))
10745, 48, 71, 72, 79, 106isumge0 11438 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ 0 โ‰ค ฮฃ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–)))
10844, 80, 89, 107leadd2dd 8517 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ (ฮฃ๐‘– โˆˆ (1...๐‘›)(1 / (2โ†‘๐‘–)) + 0) โ‰ค (ฮฃ๐‘– โˆˆ (1...๐‘›)(1 / (2โ†‘๐‘–)) + ฮฃ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–))))
10989recnd 7986 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ ฮฃ๐‘– โˆˆ (1...๐‘›)(1 / (2โ†‘๐‘–)) โˆˆ โ„‚)
110109addid1d 8106 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ (ฮฃ๐‘– โˆˆ (1...๐‘›)(1 / (2โ†‘๐‘–)) + 0) = ฮฃ๐‘– โˆˆ (1...๐‘›)(1 / (2โ†‘๐‘–)))
111110eqcomd 2183 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ ฮฃ๐‘– โˆˆ (1...๐‘›)(1 / (2โ†‘๐‘–)) = (ฮฃ๐‘– โˆˆ (1...๐‘›)(1 / (2โ†‘๐‘–)) + 0))
11275, 45, 47, 70, 76, 74isumsplit 11499 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ ฮฃ๐‘– โˆˆ โ„• ((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–)) = (ฮฃ๐‘– โˆˆ (1...((๐‘› + 1) โˆ’ 1))((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–)) + ฮฃ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–))))
1133, 112eqtrid 2222 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ ๐ด = (ฮฃ๐‘– โˆˆ (1...((๐‘› + 1) โˆ’ 1))((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–)) + ฮฃ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–))))
11446nncnd 8933 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ ๐‘› โˆˆ โ„‚)
115 1cnd 7973 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ 1 โˆˆ โ„‚)
116114, 115pncand 8269 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ ((๐‘› + 1) โˆ’ 1) = ๐‘›)
117116oveq2d 5891 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ (1...((๐‘› + 1) โˆ’ 1)) = (1...๐‘›))
118 simpr 110 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ ๐‘– โˆˆ (1...๐‘›))
119118fvresd 5541 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ ((๐น โ†พ (1...๐‘›))โ€˜๐‘–) = (๐นโ€˜๐‘–))
120 fveqeq2 5525 . . . . . . . . . . . . . . . 16 (๐‘ฅ = ๐‘– โ†’ (((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1 โ†” ((๐น โ†พ (1...๐‘›))โ€˜๐‘–) = 1))
121 simplr 528 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1)
122120, 121, 118rspcdva 2847 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ ((๐น โ†พ (1...๐‘›))โ€˜๐‘–) = 1)
123119, 122eqtr3d 2212 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ (๐นโ€˜๐‘–) = 1)
124123oveq2d 5891 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ ((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–)) = ((1 / (2โ†‘๐‘–)) ยท 1))
12587rpreccld 9707 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ (1 / (2โ†‘๐‘–)) โˆˆ โ„+)
126125rpcnd 9698 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ (1 / (2โ†‘๐‘–)) โˆˆ โ„‚)
127126mulridd 7974 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ ((1 / (2โ†‘๐‘–)) ยท 1) = (1 / (2โ†‘๐‘–)))
128124, 127eqtrd 2210 . . . . . . . . . . . 12 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โˆง ๐‘– โˆˆ (1...๐‘›)) โ†’ ((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–)) = (1 / (2โ†‘๐‘–)))
129117, 128sumeq12rdv 11381 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ ฮฃ๐‘– โˆˆ (1...((๐‘› + 1) โˆ’ 1))((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–)) = ฮฃ๐‘– โˆˆ (1...๐‘›)(1 / (2โ†‘๐‘–)))
130129oveq1d 5890 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ (ฮฃ๐‘– โˆˆ (1...((๐‘› + 1) โˆ’ 1))((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–)) + ฮฃ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–))) = (ฮฃ๐‘– โˆˆ (1...๐‘›)(1 / (2โ†‘๐‘–)) + ฮฃ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–))))
131113, 130eqtrd 2210 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ ๐ด = (ฮฃ๐‘– โˆˆ (1...๐‘›)(1 / (2โ†‘๐‘–)) + ฮฃ๐‘– โˆˆ (โ„คโ‰ฅโ€˜(๐‘› + 1))((1 / (2โ†‘๐‘–)) ยท (๐นโ€˜๐‘–))))
132108, 111, 1313brtr4d 4036 . . . . . . . 8 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ ฮฃ๐‘– โˆˆ (1...๐‘›)(1 / (2โ†‘๐‘–)) โ‰ค ๐ด)
133 geo2sum 11522 . . . . . . . . . 10 ((๐‘› โˆˆ โ„• โˆง 1 โˆˆ โ„‚) โ†’ ฮฃ๐‘– โˆˆ (1...๐‘›)(1 / (2โ†‘๐‘–)) = (1 โˆ’ (1 / (2โ†‘๐‘›))))
134133breq1d 4014 . . . . . . . . 9 ((๐‘› โˆˆ โ„• โˆง 1 โˆˆ โ„‚) โ†’ (ฮฃ๐‘– โˆˆ (1...๐‘›)(1 / (2โ†‘๐‘–)) โ‰ค ๐ด โ†” (1 โˆ’ (1 / (2โ†‘๐‘›))) โ‰ค ๐ด))
13546, 115, 134syl2anc 411 . . . . . . . 8 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ (ฮฃ๐‘– โˆˆ (1...๐‘›)(1 / (2โ†‘๐‘–)) โ‰ค ๐ด โ†” (1 โˆ’ (1 / (2โ†‘๐‘›))) โ‰ค ๐ด))
136132, 135mpbid 147 . . . . . . 7 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ (1 โˆ’ (1 / (2โ†‘๐‘›))) โ‰ค ๐ด)
13742, 41, 43, 136subled 8505 . . . . . 6 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ (1 โˆ’ ๐ด) โ‰ค (1 / (2โ†‘๐‘›)))
13840, 41, 137lensymd 8079 . . . . 5 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ ยฌ (1 / (2โ†‘๐‘›)) < (1 โˆ’ ๐ด))
13939, 138pm2.21dd 620 . . . 4 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โˆง โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1) โ†’ โˆƒ๐‘ฅ โˆˆ โ„• (๐นโ€˜๐‘ฅ) = 0)
140139ex 115 . . 3 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ (โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1 โ†’ โˆƒ๐‘ฅ โˆˆ โ„• (๐นโ€˜๐‘ฅ) = 0))
141 fveq1 5515 . . . . . . 7 (๐‘“ = (๐น โ†พ (1...๐‘›)) โ†’ (๐‘“โ€˜๐‘ฅ) = ((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ))
142141eqeq1d 2186 . . . . . 6 (๐‘“ = (๐น โ†พ (1...๐‘›)) โ†’ ((๐‘“โ€˜๐‘ฅ) = 0 โ†” ((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 0))
143142rexbidv 2478 . . . . 5 (๐‘“ = (๐น โ†พ (1...๐‘›)) โ†’ (โˆƒ๐‘ฅ โˆˆ (1...๐‘›)(๐‘“โ€˜๐‘ฅ) = 0 โ†” โˆƒ๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 0))
144141eqeq1d 2186 . . . . . 6 (๐‘“ = (๐น โ†พ (1...๐‘›)) โ†’ ((๐‘“โ€˜๐‘ฅ) = 1 โ†” ((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1))
145144ralbidv 2477 . . . . 5 (๐‘“ = (๐น โ†พ (1...๐‘›)) โ†’ (โˆ€๐‘ฅ โˆˆ (1...๐‘›)(๐‘“โ€˜๐‘ฅ) = 1 โ†” โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1))
146143, 145orbi12d 793 . . . 4 (๐‘“ = (๐น โ†พ (1...๐‘›)) โ†’ ((โˆƒ๐‘ฅ โˆˆ (1...๐‘›)(๐‘“โ€˜๐‘ฅ) = 0 โˆจ โˆ€๐‘ฅ โˆˆ (1...๐‘›)(๐‘“โ€˜๐‘ฅ) = 1) โ†” (โˆƒ๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 0 โˆจ โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1)))
147 finomni 7138 . . . . . 6 ((1...๐‘›) โˆˆ Fin โ†’ (1...๐‘›) โˆˆ Omni)
14882, 147syl 14 . . . . 5 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ (1...๐‘›) โˆˆ Omni)
149 isomninn 14782 . . . . . 6 ((1...๐‘›) โˆˆ Omni โ†’ ((1...๐‘›) โˆˆ Omni โ†” โˆ€๐‘“ โˆˆ ({0, 1} โ†‘๐‘š (1...๐‘›))(โˆƒ๐‘ฅ โˆˆ (1...๐‘›)(๐‘“โ€˜๐‘ฅ) = 0 โˆจ โˆ€๐‘ฅ โˆˆ (1...๐‘›)(๐‘“โ€˜๐‘ฅ) = 1)))
150148, 149syl 14 . . . . 5 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ ((1...๐‘›) โˆˆ Omni โ†” โˆ€๐‘“ โˆˆ ({0, 1} โ†‘๐‘š (1...๐‘›))(โˆƒ๐‘ฅ โˆˆ (1...๐‘›)(๐‘“โ€˜๐‘ฅ) = 0 โˆจ โˆ€๐‘ฅ โˆˆ (1...๐‘›)(๐‘“โ€˜๐‘ฅ) = 1)))
151148, 150mpbid 147 . . . 4 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ โˆ€๐‘“ โˆˆ ({0, 1} โ†‘๐‘š (1...๐‘›))(โˆƒ๐‘ฅ โˆˆ (1...๐‘›)(๐‘“โ€˜๐‘ฅ) = 0 โˆจ โˆ€๐‘ฅ โˆˆ (1...๐‘›)(๐‘“โ€˜๐‘ฅ) = 1))
152 fz1ssnn 10056 . . . . . . 7 (1...๐‘›) โŠ† โ„•
153152a1i 9 . . . . . 6 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ (1...๐‘›) โŠ† โ„•)
15465, 153fssresd 5393 . . . . 5 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ (๐น โ†พ (1...๐‘›)):(1...๐‘›)โŸถ{0, 1})
155 0red 7958 . . . . . . 7 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ 0 โˆˆ โ„)
156 1red 7972 . . . . . . 7 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ 1 โˆˆ โ„)
157 prexg 4212 . . . . . . 7 ((0 โˆˆ โ„ โˆง 1 โˆˆ โ„) โ†’ {0, 1} โˆˆ V)
158155, 156, 157syl2anc 411 . . . . . 6 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ {0, 1} โˆˆ V)
159158, 82elmapd 6662 . . . . 5 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ ((๐น โ†พ (1...๐‘›)) โˆˆ ({0, 1} โ†‘๐‘š (1...๐‘›)) โ†” (๐น โ†พ (1...๐‘›)):(1...๐‘›)โŸถ{0, 1}))
160154, 159mpbird 167 . . . 4 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ (๐น โ†พ (1...๐‘›)) โˆˆ ({0, 1} โ†‘๐‘š (1...๐‘›)))
161146, 151, 160rspcdva 2847 . . 3 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ (โˆƒ๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 0 โˆจ โˆ€๐‘ฅ โˆˆ (1...๐‘›)((๐น โ†พ (1...๐‘›))โ€˜๐‘ฅ) = 1))
16219, 140, 161mpjaod 718 . 2 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง (1 / ๐‘›) < (1 โˆ’ ๐ด))) โ†’ โˆƒ๐‘ฅ โˆˆ โ„• (๐นโ€˜๐‘ฅ) = 0)
16310, 162rexlimddv 2599 1 (๐œ‘ โ†’ โˆƒ๐‘ฅ โˆˆ โ„• (๐นโ€˜๐‘ฅ) = 0)
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆจ wo 708   = wceq 1353   โˆˆ wcel 2148  โˆ€wral 2455  โˆƒwrex 2456  Vcvv 2738   โŠ† wss 3130  {cpr 3594   class class class wbr 4004   โ†ฆ cmpt 4065  dom cdm 4627   โ†พ cres 4629  โŸถwf 5213  โ€˜cfv 5217  (class class class)co 5875   โ†‘๐‘š cmap 6648  Fincfn 6740  Omnicomni 7132  โ„‚cc 7809  โ„cr 7810  0cc0 7811  1c1 7812   + caddc 7814   ยท cmul 7816   < clt 7992   โ‰ค cle 7993   โˆ’ cmin 8128   / cdiv 8629  โ„•cn 8919  2c2 8970  โ„•0cn0 9176  โ„คcz 9253  โ„คโ‰ฅcuz 9528  โ„+crp 9653  ...cfz 10008  seqcseq 10445  โ†‘cexp 10519   โ‡ cli 11286  ฮฃcsu 11361
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4119  ax-sep 4122  ax-nul 4130  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537  ax-iinf 4588  ax-cnex 7902  ax-resscn 7903  ax-1cn 7904  ax-1re 7905  ax-icn 7906  ax-addcl 7907  ax-addrcl 7908  ax-mulcl 7909  ax-mulrcl 7910  ax-addcom 7911  ax-mulcom 7912  ax-addass 7913  ax-mulass 7914  ax-distr 7915  ax-i2m1 7916  ax-0lt1 7917  ax-1rid 7918  ax-0id 7919  ax-rnegex 7920  ax-precex 7921  ax-cnre 7922  ax-pre-ltirr 7923  ax-pre-ltwlin 7924  ax-pre-lttrn 7925  ax-pre-apti 7926  ax-pre-ltadd 7927  ax-pre-mulgt0 7928  ax-pre-mulext 7929  ax-arch 7930  ax-caucvg 7931
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2740  df-sbc 2964  df-csb 3059  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-if 3536  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-int 3846  df-iun 3889  df-br 4005  df-opab 4066  df-mpt 4067  df-tr 4103  df-id 4294  df-po 4297  df-iso 4298  df-iord 4367  df-on 4369  df-ilim 4370  df-suc 4372  df-iom 4591  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-ima 4640  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-f1 5222  df-fo 5223  df-f1o 5224  df-fv 5225  df-isom 5226  df-riota 5831  df-ov 5878  df-oprab 5879  df-mpo 5880  df-1st 6141  df-2nd 6142  df-recs 6306  df-irdg 6371  df-frec 6392  df-1o 6417  df-2o 6418  df-oadd 6421  df-er 6535  df-map 6650  df-en 6741  df-dom 6742  df-fin 6743  df-omni 7133  df-pnf 7994  df-mnf 7995  df-xr 7996  df-ltxr 7997  df-le 7998  df-sub 8130  df-neg 8131  df-reap 8532  df-ap 8539  df-div 8630  df-inn 8920  df-2 8978  df-3 8979  df-4 8980  df-n0 9177  df-z 9254  df-uz 9529  df-q 9620  df-rp 9654  df-ico 9894  df-fz 10009  df-fzo 10143  df-seqfrec 10446  df-exp 10520  df-ihash 10756  df-cj 10851  df-re 10852  df-im 10853  df-rsqrt 11007  df-abs 11008  df-clim 11287  df-sumdc 11362
This theorem is referenced by:  trilpolemres  14793  neapmkvlem  14817
  Copyright terms: Public domain W3C validator