MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  perfectlem2 Structured version   Visualization version   GIF version

Theorem perfectlem2 26723
Description: Lemma for perfect 26724. (Contributed by Mario Carneiro, 17-May-2016.) Replace OLD theorem. (Revised by Wolf Lammen, 17-Sep-2020.)
Hypotheses
Ref Expression
perfectlem.1 (๐œ‘ โ†’ ๐ด โˆˆ โ„•)
perfectlem.2 (๐œ‘ โ†’ ๐ต โˆˆ โ„•)
perfectlem.3 (๐œ‘ โ†’ ยฌ 2 โˆฅ ๐ต)
perfectlem.4 (๐œ‘ โ†’ (1 ฯƒ ((2โ†‘๐ด) ยท ๐ต)) = (2 ยท ((2โ†‘๐ด) ยท ๐ต)))
Assertion
Ref Expression
perfectlem2 (๐œ‘ โ†’ (๐ต โˆˆ โ„™ โˆง ๐ต = ((2โ†‘(๐ด + 1)) โˆ’ 1)))

Proof of Theorem perfectlem2
Dummy variables ๐‘˜ ๐‘› ๐‘ฅ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 perfectlem.2 . . . 4 (๐œ‘ โ†’ ๐ต โˆˆ โ„•)
2 1red 11212 . . . . 5 (๐œ‘ โ†’ 1 โˆˆ โ„)
3 perfectlem.1 . . . . . . . 8 (๐œ‘ โ†’ ๐ด โˆˆ โ„•)
4 perfectlem.3 . . . . . . . 8 (๐œ‘ โ†’ ยฌ 2 โˆฅ ๐ต)
5 perfectlem.4 . . . . . . . 8 (๐œ‘ โ†’ (1 ฯƒ ((2โ†‘๐ด) ยท ๐ต)) = (2 ยท ((2โ†‘๐ด) ยท ๐ต)))
63, 1, 4, 5perfectlem1 26722 . . . . . . 7 (๐œ‘ โ†’ ((2โ†‘(๐ด + 1)) โˆˆ โ„• โˆง ((2โ†‘(๐ด + 1)) โˆ’ 1) โˆˆ โ„• โˆง (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆˆ โ„•))
76simp3d 1145 . . . . . 6 (๐œ‘ โ†’ (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆˆ โ„•)
87nnred 12224 . . . . 5 (๐œ‘ โ†’ (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆˆ โ„)
91nnred 12224 . . . . 5 (๐œ‘ โ†’ ๐ต โˆˆ โ„)
107nnge1d 12257 . . . . 5 (๐œ‘ โ†’ 1 โ‰ค (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)))
11 2cn 12284 . . . . . . . . . . 11 2 โˆˆ โ„‚
12 exp1 14030 . . . . . . . . . . 11 (2 โˆˆ โ„‚ โ†’ (2โ†‘1) = 2)
1311, 12ax-mp 5 . . . . . . . . . 10 (2โ†‘1) = 2
14 df-2 12272 . . . . . . . . . 10 2 = (1 + 1)
1513, 14eqtri 2761 . . . . . . . . 9 (2โ†‘1) = (1 + 1)
16 2re 12283 . . . . . . . . . . 11 2 โˆˆ โ„
1716a1i 11 . . . . . . . . . 10 (๐œ‘ โ†’ 2 โˆˆ โ„)
18 1zzd 12590 . . . . . . . . . 10 (๐œ‘ โ†’ 1 โˆˆ โ„ค)
193peano2nnd 12226 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ด + 1) โˆˆ โ„•)
2019nnzd 12582 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ด + 1) โˆˆ โ„ค)
21 1lt2 12380 . . . . . . . . . . 11 1 < 2
2221a1i 11 . . . . . . . . . 10 (๐œ‘ โ†’ 1 < 2)
23 1re 11211 . . . . . . . . . . . 12 1 โˆˆ โ„
243nnrpd 13011 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ด โˆˆ โ„+)
25 ltaddrp 13008 . . . . . . . . . . . 12 ((1 โˆˆ โ„ โˆง ๐ด โˆˆ โ„+) โ†’ 1 < (1 + ๐ด))
2623, 24, 25sylancr 588 . . . . . . . . . . 11 (๐œ‘ โ†’ 1 < (1 + ๐ด))
27 ax-1cn 11165 . . . . . . . . . . . 12 1 โˆˆ โ„‚
283nncnd 12225 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
29 addcom 11397 . . . . . . . . . . . 12 ((1 โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚) โ†’ (1 + ๐ด) = (๐ด + 1))
3027, 28, 29sylancr 588 . . . . . . . . . . 11 (๐œ‘ โ†’ (1 + ๐ด) = (๐ด + 1))
3126, 30breqtrd 5174 . . . . . . . . . 10 (๐œ‘ โ†’ 1 < (๐ด + 1))
32 ltexp2a 14128 . . . . . . . . . 10 (((2 โˆˆ โ„ โˆง 1 โˆˆ โ„ค โˆง (๐ด + 1) โˆˆ โ„ค) โˆง (1 < 2 โˆง 1 < (๐ด + 1))) โ†’ (2โ†‘1) < (2โ†‘(๐ด + 1)))
3317, 18, 20, 22, 31, 32syl32anc 1379 . . . . . . . . 9 (๐œ‘ โ†’ (2โ†‘1) < (2โ†‘(๐ด + 1)))
3415, 33eqbrtrrid 5184 . . . . . . . 8 (๐œ‘ โ†’ (1 + 1) < (2โ†‘(๐ด + 1)))
356simp1d 1143 . . . . . . . . . 10 (๐œ‘ โ†’ (2โ†‘(๐ด + 1)) โˆˆ โ„•)
3635nnred 12224 . . . . . . . . 9 (๐œ‘ โ†’ (2โ†‘(๐ด + 1)) โˆˆ โ„)
372, 2, 36ltaddsubd 11811 . . . . . . . 8 (๐œ‘ โ†’ ((1 + 1) < (2โ†‘(๐ด + 1)) โ†” 1 < ((2โ†‘(๐ด + 1)) โˆ’ 1)))
3834, 37mpbid 231 . . . . . . 7 (๐œ‘ โ†’ 1 < ((2โ†‘(๐ด + 1)) โˆ’ 1))
39 0lt1 11733 . . . . . . . . 9 0 < 1
4039a1i 11 . . . . . . . 8 (๐œ‘ โ†’ 0 < 1)
41 peano2rem 11524 . . . . . . . . 9 ((2โ†‘(๐ด + 1)) โˆˆ โ„ โ†’ ((2โ†‘(๐ด + 1)) โˆ’ 1) โˆˆ โ„)
4236, 41syl 17 . . . . . . . 8 (๐œ‘ โ†’ ((2โ†‘(๐ด + 1)) โˆ’ 1) โˆˆ โ„)
43 expgt1 14063 . . . . . . . . . 10 ((2 โˆˆ โ„ โˆง (๐ด + 1) โˆˆ โ„• โˆง 1 < 2) โ†’ 1 < (2โ†‘(๐ด + 1)))
4416, 19, 22, 43mp3an2i 1467 . . . . . . . . 9 (๐œ‘ โ†’ 1 < (2โ†‘(๐ด + 1)))
45 posdif 11704 . . . . . . . . . 10 ((1 โˆˆ โ„ โˆง (2โ†‘(๐ด + 1)) โˆˆ โ„) โ†’ (1 < (2โ†‘(๐ด + 1)) โ†” 0 < ((2โ†‘(๐ด + 1)) โˆ’ 1)))
4623, 36, 45sylancr 588 . . . . . . . . 9 (๐œ‘ โ†’ (1 < (2โ†‘(๐ด + 1)) โ†” 0 < ((2โ†‘(๐ด + 1)) โˆ’ 1)))
4744, 46mpbid 231 . . . . . . . 8 (๐œ‘ โ†’ 0 < ((2โ†‘(๐ด + 1)) โˆ’ 1))
481nngt0d 12258 . . . . . . . 8 (๐œ‘ โ†’ 0 < ๐ต)
49 ltdiv2 12097 . . . . . . . 8 (((1 โˆˆ โ„ โˆง 0 < 1) โˆง (((2โ†‘(๐ด + 1)) โˆ’ 1) โˆˆ โ„ โˆง 0 < ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆง (๐ต โˆˆ โ„ โˆง 0 < ๐ต)) โ†’ (1 < ((2โ†‘(๐ด + 1)) โˆ’ 1) โ†” (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) < (๐ต / 1)))
502, 40, 42, 47, 9, 48, 49syl222anc 1387 . . . . . . 7 (๐œ‘ โ†’ (1 < ((2โ†‘(๐ด + 1)) โˆ’ 1) โ†” (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) < (๐ต / 1)))
5138, 50mpbid 231 . . . . . 6 (๐œ‘ โ†’ (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) < (๐ต / 1))
521nncnd 12225 . . . . . . 7 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
5352div1d 11979 . . . . . 6 (๐œ‘ โ†’ (๐ต / 1) = ๐ต)
5451, 53breqtrd 5174 . . . . 5 (๐œ‘ โ†’ (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) < ๐ต)
552, 8, 9, 10, 54lelttrd 11369 . . . 4 (๐œ‘ โ†’ 1 < ๐ต)
56 eluz2b2 12902 . . . 4 (๐ต โˆˆ (โ„คโ‰ฅโ€˜2) โ†” (๐ต โˆˆ โ„• โˆง 1 < ๐ต))
571, 55, 56sylanbrc 584 . . 3 (๐œ‘ โ†’ ๐ต โˆˆ (โ„คโ‰ฅโ€˜2))
58 fzfid 13935 . . . . . . . . . . . 12 (๐œ‘ โ†’ (1...๐ต) โˆˆ Fin)
59 dvdsssfz1 16258 . . . . . . . . . . . . 13 (๐ต โˆˆ โ„• โ†’ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต} โŠ† (1...๐ต))
601, 59syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต} โŠ† (1...๐ต))
6158, 60ssfid 9264 . . . . . . . . . . 11 (๐œ‘ โ†’ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต} โˆˆ Fin)
6261ad2antrr 725 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต} โˆˆ Fin)
63 ssrab2 4077 . . . . . . . . . . . . 13 {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต} โŠ† โ„•
6463a1i 11 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต} โŠ† โ„•)
6564sselda 3982 . . . . . . . . . . 11 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โˆง ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต}) โ†’ ๐‘˜ โˆˆ โ„•)
6665nnred 12224 . . . . . . . . . 10 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โˆง ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต}) โ†’ ๐‘˜ โˆˆ โ„)
6765nnnn0d 12529 . . . . . . . . . . 11 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โˆง ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต}) โ†’ ๐‘˜ โˆˆ โ„•0)
6867nn0ge0d 12532 . . . . . . . . . 10 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โˆง ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต}) โ†’ 0 โ‰ค ๐‘˜)
69 df-tp 4633 . . . . . . . . . . . 12 {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, ๐‘›} = ({(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต} โˆช {๐‘›})
707, 1prssd 4825 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต} โŠ† โ„•)
7170ad2antrr 725 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต} โŠ† โ„•)
72 simplrl 776 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ ๐‘› โˆˆ โ„•)
7372snssd 4812 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ {๐‘›} โŠ† โ„•)
7471, 73unssd 4186 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ ({(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต} โˆช {๐‘›}) โŠ† โ„•)
7569, 74eqsstrid 4030 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, ๐‘›} โŠ† โ„•)
766simp2d 1144 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((2โ†‘(๐ด + 1)) โˆ’ 1) โˆˆ โ„•)
7776nnzd 12582 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((2โ†‘(๐ด + 1)) โˆ’ 1) โˆˆ โ„ค)
787nnzd 12582 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆˆ โ„ค)
79 dvdsmul2 16219 . . . . . . . . . . . . . . . . 17 ((((2โ†‘(๐ด + 1)) โˆ’ 1) โˆˆ โ„ค โˆง (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆˆ โ„ค) โ†’ (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆฅ (((2โ†‘(๐ด + 1)) โˆ’ 1) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))))
8077, 78, 79syl2anc 585 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆฅ (((2โ†‘(๐ด + 1)) โˆ’ 1) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))))
8176nncnd 12225 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((2โ†‘(๐ด + 1)) โˆ’ 1) โˆˆ โ„‚)
8276nnne0d 12259 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((2โ†‘(๐ด + 1)) โˆ’ 1) โ‰  0)
8352, 81, 82divcan2d 11989 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((2โ†‘(๐ด + 1)) โˆ’ 1) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) = ๐ต)
8480, 83breqtrd 5174 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆฅ ๐ต)
85 breq1 5151 . . . . . . . . . . . . . . 15 (๐‘ฅ = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ†’ (๐‘ฅ โˆฅ ๐ต โ†” (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆฅ ๐ต))
8684, 85syl5ibrcom 246 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘ฅ = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ†’ ๐‘ฅ โˆฅ ๐ต))
8786ad2antrr 725 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ (๐‘ฅ = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ†’ ๐‘ฅ โˆฅ ๐ต))
881nnzd 12582 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ต โˆˆ โ„ค)
89 iddvds 16210 . . . . . . . . . . . . . . . 16 (๐ต โˆˆ โ„ค โ†’ ๐ต โˆฅ ๐ต)
9088, 89syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ต โˆฅ ๐ต)
91 breq1 5151 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐ต โ†’ (๐‘ฅ โˆฅ ๐ต โ†” ๐ต โˆฅ ๐ต))
9290, 91syl5ibrcom 246 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘ฅ = ๐ต โ†’ ๐‘ฅ โˆฅ ๐ต))
9392ad2antrr 725 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ (๐‘ฅ = ๐ต โ†’ ๐‘ฅ โˆฅ ๐ต))
94 simplrr 777 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ ๐‘› โˆฅ ๐ต)
95 breq1 5151 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘› โ†’ (๐‘ฅ โˆฅ ๐ต โ†” ๐‘› โˆฅ ๐ต))
9694, 95syl5ibrcom 246 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ (๐‘ฅ = ๐‘› โ†’ ๐‘ฅ โˆฅ ๐ต))
9787, 93, 963jaod 1429 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ ((๐‘ฅ = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆจ ๐‘ฅ = ๐ต โˆจ ๐‘ฅ = ๐‘›) โ†’ ๐‘ฅ โˆฅ ๐ต))
98 eltpi 4691 . . . . . . . . . . . 12 (๐‘ฅ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, ๐‘›} โ†’ (๐‘ฅ = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆจ ๐‘ฅ = ๐ต โˆจ ๐‘ฅ = ๐‘›))
9997, 98impel 507 . . . . . . . . . . 11 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โˆง ๐‘ฅ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, ๐‘›}) โ†’ ๐‘ฅ โˆฅ ๐ต)
10075, 99ssrabdv 4071 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, ๐‘›} โŠ† {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต})
10162, 66, 68, 100fsumless 15739 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ ฮฃ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, ๐‘›}๐‘˜ โ‰ค ฮฃ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต}๐‘˜)
102 simpr 486 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต})
103 disjsn 4715 . . . . . . . . . . . 12 (({(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต} โˆฉ {๐‘›}) = โˆ… โ†” ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต})
104102, 103sylibr 233 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ ({(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต} โˆฉ {๐‘›}) = โˆ…)
10569a1i 11 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, ๐‘›} = ({(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต} โˆช {๐‘›}))
106 tpfi 9320 . . . . . . . . . . . 12 {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, ๐‘›} โˆˆ Fin
107106a1i 11 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, ๐‘›} โˆˆ Fin)
10875sselda 3982 . . . . . . . . . . . 12 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โˆง ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, ๐‘›}) โ†’ ๐‘˜ โˆˆ โ„•)
109108nncnd 12225 . . . . . . . . . . 11 ((((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โˆง ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, ๐‘›}) โ†’ ๐‘˜ โˆˆ โ„‚)
110104, 105, 107, 109fsumsplit 15684 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ ฮฃ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, ๐‘›}๐‘˜ = (ฮฃ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}๐‘˜ + ฮฃ๐‘˜ โˆˆ {๐‘›}๐‘˜))
1117nncnd 12225 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆˆ โ„‚)
112 id 22 . . . . . . . . . . . . . . . 16 (๐‘˜ = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ†’ ๐‘˜ = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)))
113112sumsn 15689 . . . . . . . . . . . . . . 15 (((๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆˆ โ„• โˆง (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆˆ โ„‚) โ†’ ฮฃ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))}๐‘˜ = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)))
1147, 111, 113syl2anc 585 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))}๐‘˜ = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)))
115 id 22 . . . . . . . . . . . . . . . 16 (๐‘˜ = ๐ต โ†’ ๐‘˜ = ๐ต)
116115sumsn 15689 . . . . . . . . . . . . . . 15 ((๐ต โˆˆ โ„• โˆง ๐ต โˆˆ โ„‚) โ†’ ฮฃ๐‘˜ โˆˆ {๐ต}๐‘˜ = ๐ต)
1171, 52, 116syl2anc 585 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ {๐ต}๐‘˜ = ๐ต)
118114, 117oveq12d 7424 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))}๐‘˜ + ฮฃ๐‘˜ โˆˆ {๐ต}๐‘˜) = ((๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) + ๐ต))
119 incom 4201 . . . . . . . . . . . . . . 15 ({๐ต} โˆฉ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))}) = ({(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))} โˆฉ {๐ต})
1208, 54gtned 11346 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ต โ‰  (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)))
121 disjsn2 4716 . . . . . . . . . . . . . . . 16 (๐ต โ‰  (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ†’ ({๐ต} โˆฉ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))}) = โˆ…)
122120, 121syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ({๐ต} โˆฉ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))}) = โˆ…)
123119, 122eqtr3id 2787 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ({(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))} โˆฉ {๐ต}) = โˆ…)
124 df-pr 4631 . . . . . . . . . . . . . . 15 {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต} = ({(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))} โˆช {๐ต})
125124a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต} = ({(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))} โˆช {๐ต}))
126 prfi 9319 . . . . . . . . . . . . . . 15 {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต} โˆˆ Fin
127126a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต} โˆˆ Fin)
12870sselda 3982 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ ๐‘˜ โˆˆ โ„•)
129128nncnd 12225 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ ๐‘˜ โˆˆ โ„‚)
130123, 125, 127, 129fsumsplit 15684 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}๐‘˜ = (ฮฃ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))}๐‘˜ + ฮฃ๐‘˜ โˆˆ {๐ต}๐‘˜))
13181, 52mulcld 11231 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((2โ†‘(๐ด + 1)) โˆ’ 1) ยท ๐ต) โˆˆ โ„‚)
13252, 131, 81, 82divdird 12025 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐ต + (((2โ†‘(๐ด + 1)) โˆ’ 1) ยท ๐ต)) / ((2โ†‘(๐ด + 1)) โˆ’ 1)) = ((๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) + ((((2โ†‘(๐ด + 1)) โˆ’ 1) ยท ๐ต) / ((2โ†‘(๐ด + 1)) โˆ’ 1))))
13335nncnd 12225 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (2โ†‘(๐ด + 1)) โˆˆ โ„‚)
134 1cnd 11206 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ 1 โˆˆ โ„‚)
135133, 134, 52subdird 11668 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (((2โ†‘(๐ด + 1)) โˆ’ 1) ยท ๐ต) = (((2โ†‘(๐ด + 1)) ยท ๐ต) โˆ’ (1 ยท ๐ต)))
13652mullidd 11229 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (1 ยท ๐ต) = ๐ต)
137136oveq2d 7422 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (((2โ†‘(๐ด + 1)) ยท ๐ต) โˆ’ (1 ยท ๐ต)) = (((2โ†‘(๐ด + 1)) ยท ๐ต) โˆ’ ๐ต))
138135, 137eqtrd 2773 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (((2โ†‘(๐ด + 1)) โˆ’ 1) ยท ๐ต) = (((2โ†‘(๐ด + 1)) ยท ๐ต) โˆ’ ๐ต))
139138oveq2d 7422 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐ต + (((2โ†‘(๐ด + 1)) โˆ’ 1) ยท ๐ต)) = (๐ต + (((2โ†‘(๐ด + 1)) ยท ๐ต) โˆ’ ๐ต)))
140133, 52mulcld 11231 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((2โ†‘(๐ด + 1)) ยท ๐ต) โˆˆ โ„‚)
14152, 140pncan3d 11571 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐ต + (((2โ†‘(๐ด + 1)) ยท ๐ต) โˆ’ ๐ต)) = ((2โ†‘(๐ด + 1)) ยท ๐ต))
142139, 141eqtrd 2773 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐ต + (((2โ†‘(๐ด + 1)) โˆ’ 1) ยท ๐ต)) = ((2โ†‘(๐ด + 1)) ยท ๐ต))
143142oveq1d 7421 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ต + (((2โ†‘(๐ด + 1)) โˆ’ 1) ยท ๐ต)) / ((2โ†‘(๐ด + 1)) โˆ’ 1)) = (((2โ†‘(๐ด + 1)) ยท ๐ต) / ((2โ†‘(๐ด + 1)) โˆ’ 1)))
144133, 52, 81, 82divassd 12022 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((2โ†‘(๐ด + 1)) ยท ๐ต) / ((2โ†‘(๐ด + 1)) โˆ’ 1)) = ((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))))
145143, 144eqtrd 2773 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐ต + (((2โ†‘(๐ด + 1)) โˆ’ 1) ยท ๐ต)) / ((2โ†‘(๐ด + 1)) โˆ’ 1)) = ((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))))
14652, 81, 82divcan3d 11992 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((((2โ†‘(๐ด + 1)) โˆ’ 1) ยท ๐ต) / ((2โ†‘(๐ด + 1)) โˆ’ 1)) = ๐ต)
147146oveq2d 7422 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) + ((((2โ†‘(๐ด + 1)) โˆ’ 1) ยท ๐ต) / ((2โ†‘(๐ด + 1)) โˆ’ 1))) = ((๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) + ๐ต))
148132, 145, 1473eqtr3d 2781 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) = ((๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) + ๐ต))
149118, 130, 1483eqtr4d 2783 . . . . . . . . . . . 12 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}๐‘˜ = ((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))))
150149ad2antrr 725 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ ฮฃ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}๐‘˜ = ((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))))
15172nncnd 12225 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ ๐‘› โˆˆ โ„‚)
152 id 22 . . . . . . . . . . . . 13 (๐‘˜ = ๐‘› โ†’ ๐‘˜ = ๐‘›)
153152sumsn 15689 . . . . . . . . . . . 12 ((๐‘› โˆˆ โ„‚ โˆง ๐‘› โˆˆ โ„‚) โ†’ ฮฃ๐‘˜ โˆˆ {๐‘›}๐‘˜ = ๐‘›)
154151, 151, 153syl2anc 585 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ ฮฃ๐‘˜ โˆˆ {๐‘›}๐‘˜ = ๐‘›)
155150, 154oveq12d 7424 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ (ฮฃ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}๐‘˜ + ฮฃ๐‘˜ โˆˆ {๐‘›}๐‘˜) = (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) + ๐‘›))
156110, 155eqtrd 2773 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ ฮฃ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, ๐‘›}๐‘˜ = (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) + ๐‘›))
1573nnnn0d 12529 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ๐ด โˆˆ โ„•0)
158 expp1 14031 . . . . . . . . . . . . . . . . 17 ((2 โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„•0) โ†’ (2โ†‘(๐ด + 1)) = ((2โ†‘๐ด) ยท 2))
15911, 157, 158sylancr 588 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (2โ†‘(๐ด + 1)) = ((2โ†‘๐ด) ยท 2))
160 2nn 12282 . . . . . . . . . . . . . . . . . . 19 2 โˆˆ โ„•
161 nnexpcl 14037 . . . . . . . . . . . . . . . . . . 19 ((2 โˆˆ โ„• โˆง ๐ด โˆˆ โ„•0) โ†’ (2โ†‘๐ด) โˆˆ โ„•)
162160, 157, 161sylancr 588 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (2โ†‘๐ด) โˆˆ โ„•)
163162nncnd 12225 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (2โ†‘๐ด) โˆˆ โ„‚)
164 mulcom 11193 . . . . . . . . . . . . . . . . 17 (((2โ†‘๐ด) โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚) โ†’ ((2โ†‘๐ด) ยท 2) = (2 ยท (2โ†‘๐ด)))
165163, 11, 164sylancl 587 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((2โ†‘๐ด) ยท 2) = (2 ยท (2โ†‘๐ด)))
166159, 165eqtrd 2773 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (2โ†‘(๐ด + 1)) = (2 ยท (2โ†‘๐ด)))
167166oveq1d 7421 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((2โ†‘(๐ด + 1)) ยท ๐ต) = ((2 ยท (2โ†‘๐ด)) ยท ๐ต))
168 2cnd 12287 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 2 โˆˆ โ„‚)
169168, 163, 52mulassd 11234 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((2 ยท (2โ†‘๐ด)) ยท ๐ต) = (2 ยท ((2โ†‘๐ด) ยท ๐ต)))
170 2prm 16626 . . . . . . . . . . . . . . . . . . 19 2 โˆˆ โ„™
171 coprm 16645 . . . . . . . . . . . . . . . . . . 19 ((2 โˆˆ โ„™ โˆง ๐ต โˆˆ โ„ค) โ†’ (ยฌ 2 โˆฅ ๐ต โ†” (2 gcd ๐ต) = 1))
172170, 88, 171sylancr 588 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (ยฌ 2 โˆฅ ๐ต โ†” (2 gcd ๐ต) = 1))
1734, 172mpbid 231 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (2 gcd ๐ต) = 1)
174 2z 12591 . . . . . . . . . . . . . . . . . 18 2 โˆˆ โ„ค
175 rpexp1i 16657 . . . . . . . . . . . . . . . . . 18 ((2 โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ด โˆˆ โ„•0) โ†’ ((2 gcd ๐ต) = 1 โ†’ ((2โ†‘๐ด) gcd ๐ต) = 1))
176174, 88, 157, 175mp3an2i 1467 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((2 gcd ๐ต) = 1 โ†’ ((2โ†‘๐ด) gcd ๐ต) = 1))
177173, 176mpd 15 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((2โ†‘๐ด) gcd ๐ต) = 1)
178 sgmmul 26694 . . . . . . . . . . . . . . . 16 ((1 โˆˆ โ„‚ โˆง ((2โ†‘๐ด) โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ((2โ†‘๐ด) gcd ๐ต) = 1)) โ†’ (1 ฯƒ ((2โ†‘๐ด) ยท ๐ต)) = ((1 ฯƒ (2โ†‘๐ด)) ยท (1 ฯƒ ๐ต)))
179134, 162, 1, 177, 178syl13anc 1373 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (1 ฯƒ ((2โ†‘๐ด) ยท ๐ต)) = ((1 ฯƒ (2โ†‘๐ด)) ยท (1 ฯƒ ๐ต)))
180 pncan 11463 . . . . . . . . . . . . . . . . . . . 20 ((๐ด โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ ((๐ด + 1) โˆ’ 1) = ๐ด)
18128, 27, 180sylancl 587 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((๐ด + 1) โˆ’ 1) = ๐ด)
182181oveq2d 7422 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (2โ†‘((๐ด + 1) โˆ’ 1)) = (2โ†‘๐ด))
183182oveq2d 7422 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (1 ฯƒ (2โ†‘((๐ด + 1) โˆ’ 1))) = (1 ฯƒ (2โ†‘๐ด)))
184 1sgm2ppw 26693 . . . . . . . . . . . . . . . . . 18 ((๐ด + 1) โˆˆ โ„• โ†’ (1 ฯƒ (2โ†‘((๐ด + 1) โˆ’ 1))) = ((2โ†‘(๐ด + 1)) โˆ’ 1))
18519, 184syl 17 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (1 ฯƒ (2โ†‘((๐ด + 1) โˆ’ 1))) = ((2โ†‘(๐ด + 1)) โˆ’ 1))
186183, 185eqtr3d 2775 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (1 ฯƒ (2โ†‘๐ด)) = ((2โ†‘(๐ด + 1)) โˆ’ 1))
187186oveq1d 7421 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((1 ฯƒ (2โ†‘๐ด)) ยท (1 ฯƒ ๐ต)) = (((2โ†‘(๐ด + 1)) โˆ’ 1) ยท (1 ฯƒ ๐ต)))
188179, 5, 1873eqtr3d 2781 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (2 ยท ((2โ†‘๐ด) ยท ๐ต)) = (((2โ†‘(๐ด + 1)) โˆ’ 1) ยท (1 ฯƒ ๐ต)))
189167, 169, 1883eqtrd 2777 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((2โ†‘(๐ด + 1)) ยท ๐ต) = (((2โ†‘(๐ด + 1)) โˆ’ 1) ยท (1 ฯƒ ๐ต)))
190189oveq1d 7421 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((2โ†‘(๐ด + 1)) ยท ๐ต) / ((2โ†‘(๐ด + 1)) โˆ’ 1)) = ((((2โ†‘(๐ด + 1)) โˆ’ 1) ยท (1 ฯƒ ๐ต)) / ((2โ†‘(๐ด + 1)) โˆ’ 1)))
191 1nn0 12485 . . . . . . . . . . . . . . 15 1 โˆˆ โ„•0
192 sgmnncl 26641 . . . . . . . . . . . . . . 15 ((1 โˆˆ โ„•0 โˆง ๐ต โˆˆ โ„•) โ†’ (1 ฯƒ ๐ต) โˆˆ โ„•)
193191, 1, 192sylancr 588 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (1 ฯƒ ๐ต) โˆˆ โ„•)
194193nncnd 12225 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (1 ฯƒ ๐ต) โˆˆ โ„‚)
195194, 81, 82divcan3d 11992 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((((2โ†‘(๐ด + 1)) โˆ’ 1) ยท (1 ฯƒ ๐ต)) / ((2โ†‘(๐ด + 1)) โˆ’ 1)) = (1 ฯƒ ๐ต))
196190, 144, 1953eqtr3d 2781 . . . . . . . . . . 11 (๐œ‘ โ†’ ((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) = (1 ฯƒ ๐ต))
197 sgmval 26636 . . . . . . . . . . . 12 ((1 โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„•) โ†’ (1 ฯƒ ๐ต) = ฮฃ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต} (๐‘˜โ†‘๐‘1))
19827, 1, 197sylancr 588 . . . . . . . . . . 11 (๐œ‘ โ†’ (1 ฯƒ ๐ต) = ฮฃ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต} (๐‘˜โ†‘๐‘1))
199 simpr 486 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต}) โ†’ ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต})
20063, 199sselid 3980 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต}) โ†’ ๐‘˜ โˆˆ โ„•)
201200nncnd 12225 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต}) โ†’ ๐‘˜ โˆˆ โ„‚)
202201cxp1d 26206 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต}) โ†’ (๐‘˜โ†‘๐‘1) = ๐‘˜)
203202sumeq2dv 15646 . . . . . . . . . . 11 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต} (๐‘˜โ†‘๐‘1) = ฮฃ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต}๐‘˜)
204196, 198, 2033eqtrrd 2778 . . . . . . . . . 10 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต}๐‘˜ = ((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))))
205204ad2antrr 725 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ ฮฃ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต}๐‘˜ = ((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))))
206101, 156, 2053brtr3d 5179 . . . . . . . 8 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) + ๐‘›) โ‰ค ((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))))
20736, 8remulcld 11241 . . . . . . . . . . 11 (๐œ‘ โ†’ ((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) โˆˆ โ„)
208207ad2antrr 725 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ ((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) โˆˆ โ„)
20972nnrpd 13011 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ ๐‘› โˆˆ โ„+)
210208, 209ltaddrpd 13046 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ ((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) < (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) + ๐‘›))
21172nnred 12224 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ ๐‘› โˆˆ โ„)
212208, 211readdcld 11240 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) + ๐‘›) โˆˆ โ„)
213208, 212ltnled 11358 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) < (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) + ๐‘›) โ†” ยฌ (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) + ๐‘›) โ‰ค ((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)))))
214210, 213mpbid 231 . . . . . . . 8 (((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โˆง ยฌ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}) โ†’ ยฌ (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) + ๐‘›) โ‰ค ((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))))
215206, 214condan 817 . . . . . . 7 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โ†’ ๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต})
216 elpri 4650 . . . . . . 7 (๐‘› โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต} โ†’ (๐‘› = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆจ ๐‘› = ๐ต))
217215, 216syl 17 . . . . . 6 ((๐œ‘ โˆง (๐‘› โˆˆ โ„• โˆง ๐‘› โˆฅ ๐ต)) โ†’ (๐‘› = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆจ ๐‘› = ๐ต))
218217expr 458 . . . . 5 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ (๐‘› โˆฅ ๐ต โ†’ (๐‘› = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆจ ๐‘› = ๐ต)))
219218ralrimiva 3147 . . . 4 (๐œ‘ โ†’ โˆ€๐‘› โˆˆ โ„• (๐‘› โˆฅ ๐ต โ†’ (๐‘› = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆจ ๐‘› = ๐ต)))
2202, 55gtned 11346 . . . . . . . . . 10 (๐œ‘ โ†’ ๐ต โ‰  1)
221220necomd 2997 . . . . . . . . 9 (๐œ‘ โ†’ 1 โ‰  ๐ต)
222 1dvds 16211 . . . . . . . . . . . . 13 (๐ต โˆˆ โ„ค โ†’ 1 โˆฅ ๐ต)
22388, 222syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ 1 โˆฅ ๐ต)
224 breq1 5151 . . . . . . . . . . . . . 14 (๐‘› = 1 โ†’ (๐‘› โˆฅ ๐ต โ†” 1 โˆฅ ๐ต))
225 eqeq1 2737 . . . . . . . . . . . . . . 15 (๐‘› = 1 โ†’ (๐‘› = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ†” 1 = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))))
226 eqeq1 2737 . . . . . . . . . . . . . . 15 (๐‘› = 1 โ†’ (๐‘› = ๐ต โ†” 1 = ๐ต))
227225, 226orbi12d 918 . . . . . . . . . . . . . 14 (๐‘› = 1 โ†’ ((๐‘› = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆจ ๐‘› = ๐ต) โ†” (1 = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆจ 1 = ๐ต)))
228224, 227imbi12d 345 . . . . . . . . . . . . 13 (๐‘› = 1 โ†’ ((๐‘› โˆฅ ๐ต โ†’ (๐‘› = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆจ ๐‘› = ๐ต)) โ†” (1 โˆฅ ๐ต โ†’ (1 = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆจ 1 = ๐ต))))
229 1nn 12220 . . . . . . . . . . . . . 14 1 โˆˆ โ„•
230229a1i 11 . . . . . . . . . . . . 13 (๐œ‘ โ†’ 1 โˆˆ โ„•)
231228, 219, 230rspcdva 3614 . . . . . . . . . . . 12 (๐œ‘ โ†’ (1 โˆฅ ๐ต โ†’ (1 = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆจ 1 = ๐ต)))
232223, 231mpd 15 . . . . . . . . . . 11 (๐œ‘ โ†’ (1 = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆจ 1 = ๐ต))
233232ord 863 . . . . . . . . . 10 (๐œ‘ โ†’ (ยฌ 1 = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ†’ 1 = ๐ต))
234233necon1ad 2958 . . . . . . . . 9 (๐œ‘ โ†’ (1 โ‰  ๐ต โ†’ 1 = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))))
235221, 234mpd 15 . . . . . . . 8 (๐œ‘ โ†’ 1 = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)))
236235eqeq2d 2744 . . . . . . 7 (๐œ‘ โ†’ (๐‘› = 1 โ†” ๐‘› = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))))
237236orbi1d 916 . . . . . 6 (๐œ‘ โ†’ ((๐‘› = 1 โˆจ ๐‘› = ๐ต) โ†” (๐‘› = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆจ ๐‘› = ๐ต)))
238237imbi2d 341 . . . . 5 (๐œ‘ โ†’ ((๐‘› โˆฅ ๐ต โ†’ (๐‘› = 1 โˆจ ๐‘› = ๐ต)) โ†” (๐‘› โˆฅ ๐ต โ†’ (๐‘› = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆจ ๐‘› = ๐ต))))
239238ralbidv 3178 . . . 4 (๐œ‘ โ†’ (โˆ€๐‘› โˆˆ โ„• (๐‘› โˆฅ ๐ต โ†’ (๐‘› = 1 โˆจ ๐‘› = ๐ต)) โ†” โˆ€๐‘› โˆˆ โ„• (๐‘› โˆฅ ๐ต โ†’ (๐‘› = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆจ ๐‘› = ๐ต))))
240219, 239mpbird 257 . . 3 (๐œ‘ โ†’ โˆ€๐‘› โˆˆ โ„• (๐‘› โˆฅ ๐ต โ†’ (๐‘› = 1 โˆจ ๐‘› = ๐ต)))
241 isprm2 16616 . . 3 (๐ต โˆˆ โ„™ โ†” (๐ต โˆˆ (โ„คโ‰ฅโ€˜2) โˆง โˆ€๐‘› โˆˆ โ„• (๐‘› โˆฅ ๐ต โ†’ (๐‘› = 1 โˆจ ๐‘› = ๐ต))))
24257, 240, 241sylanbrc 584 . 2 (๐œ‘ โ†’ ๐ต โˆˆ โ„™)
243207ltp1d 12141 . . . 4 (๐œ‘ โ†’ ((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) < (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) + 1))
244 peano2re 11384 . . . . . 6 (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) โˆˆ โ„ โ†’ (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) + 1) โˆˆ โ„)
245207, 244syl 17 . . . . 5 (๐œ‘ โ†’ (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) + 1) โˆˆ โ„)
246207, 245ltnled 11358 . . . 4 (๐œ‘ โ†’ (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) < (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) + 1) โ†” ยฌ (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) + 1) โ‰ค ((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)))))
247243, 246mpbid 231 . . 3 (๐œ‘ โ†’ ยฌ (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) + 1) โ‰ค ((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))))
248200nnred 12224 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต}) โ†’ ๐‘˜ โˆˆ โ„)
249200nnnn0d 12529 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต}) โ†’ ๐‘˜ โˆˆ โ„•0)
250249nn0ge0d 12532 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต}) โ†’ 0 โ‰ค ๐‘˜)
251 df-tp 4633 . . . . . . . . . 10 {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, 1} = ({(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต} โˆช {1})
252 snssi 4811 . . . . . . . . . . . 12 (1 โˆˆ โ„• โ†’ {1} โŠ† โ„•)
253229, 252mp1i 13 . . . . . . . . . . 11 (๐œ‘ โ†’ {1} โŠ† โ„•)
25470, 253unssd 4186 . . . . . . . . . 10 (๐œ‘ โ†’ ({(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต} โˆช {1}) โŠ† โ„•)
255251, 254eqsstrid 4030 . . . . . . . . 9 (๐œ‘ โ†’ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, 1} โŠ† โ„•)
256 breq1 5151 . . . . . . . . . . . 12 (๐‘ฅ = 1 โ†’ (๐‘ฅ โˆฅ ๐ต โ†” 1 โˆฅ ๐ต))
257223, 256syl5ibrcom 246 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ฅ = 1 โ†’ ๐‘ฅ โˆฅ ๐ต))
25886, 92, 2573jaod 1429 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘ฅ = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆจ ๐‘ฅ = ๐ต โˆจ ๐‘ฅ = 1) โ†’ ๐‘ฅ โˆฅ ๐ต))
259 eltpi 4691 . . . . . . . . . 10 (๐‘ฅ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, 1} โ†’ (๐‘ฅ = (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆจ ๐‘ฅ = ๐ต โˆจ ๐‘ฅ = 1))
260258, 259impel 507 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, 1}) โ†’ ๐‘ฅ โˆฅ ๐ต)
261255, 260ssrabdv 4071 . . . . . . . 8 (๐œ‘ โ†’ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, 1} โŠ† {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต})
26261, 248, 250, 261fsumless 15739 . . . . . . 7 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, 1}๐‘˜ โ‰ค ฮฃ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต}๐‘˜)
263262adantr 482 . . . . . 6 ((๐œ‘ โˆง ๐ต โ‰  ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ†’ ฮฃ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, 1}๐‘˜ โ‰ค ฮฃ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต}๐‘˜)
26452, 81, 82diveq1ad 11996 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) = 1 โ†” ๐ต = ((2โ†‘(๐ด + 1)) โˆ’ 1)))
265264necon3bid 2986 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ‰  1 โ†” ๐ต โ‰  ((2โ†‘(๐ด + 1)) โˆ’ 1)))
266265biimpar 479 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐ต โ‰  ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ†’ (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ‰  1)
267266necomd 2997 . . . . . . . . . 10 ((๐œ‘ โˆง ๐ต โ‰  ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ†’ 1 โ‰  (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)))
268221adantr 482 . . . . . . . . . 10 ((๐œ‘ โˆง ๐ต โ‰  ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ†’ 1 โ‰  ๐ต)
269267, 268nelprd 4659 . . . . . . . . 9 ((๐œ‘ โˆง ๐ต โ‰  ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ†’ ยฌ 1 โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต})
270 disjsn 4715 . . . . . . . . 9 (({(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต} โˆฉ {1}) = โˆ… โ†” ยฌ 1 โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต})
271269, 270sylibr 233 . . . . . . . 8 ((๐œ‘ โˆง ๐ต โ‰  ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ†’ ({(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต} โˆฉ {1}) = โˆ…)
272251a1i 11 . . . . . . . 8 ((๐œ‘ โˆง ๐ต โ‰  ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ†’ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, 1} = ({(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต} โˆช {1}))
273 tpfi 9320 . . . . . . . . 9 {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, 1} โˆˆ Fin
274273a1i 11 . . . . . . . 8 ((๐œ‘ โˆง ๐ต โ‰  ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ†’ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, 1} โˆˆ Fin)
275255adantr 482 . . . . . . . . . 10 ((๐œ‘ โˆง ๐ต โ‰  ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ†’ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, 1} โŠ† โ„•)
276275sselda 3982 . . . . . . . . 9 (((๐œ‘ โˆง ๐ต โ‰  ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆง ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, 1}) โ†’ ๐‘˜ โˆˆ โ„•)
277276nncnd 12225 . . . . . . . 8 (((๐œ‘ โˆง ๐ต โ‰  ((2โ†‘(๐ด + 1)) โˆ’ 1)) โˆง ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, 1}) โ†’ ๐‘˜ โˆˆ โ„‚)
278271, 272, 274, 277fsumsplit 15684 . . . . . . 7 ((๐œ‘ โˆง ๐ต โ‰  ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ†’ ฮฃ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, 1}๐‘˜ = (ฮฃ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}๐‘˜ + ฮฃ๐‘˜ โˆˆ {1}๐‘˜))
279 id 22 . . . . . . . . . . 11 (๐‘˜ = 1 โ†’ ๐‘˜ = 1)
280279sumsn 15689 . . . . . . . . . 10 ((1 โˆˆ โ„ โˆง 1 โˆˆ โ„‚) โ†’ ฮฃ๐‘˜ โˆˆ {1}๐‘˜ = 1)
2812, 27, 280sylancl 587 . . . . . . . . 9 (๐œ‘ โ†’ ฮฃ๐‘˜ โˆˆ {1}๐‘˜ = 1)
282149, 281oveq12d 7424 . . . . . . . 8 (๐œ‘ โ†’ (ฮฃ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}๐‘˜ + ฮฃ๐‘˜ โˆˆ {1}๐‘˜) = (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) + 1))
283282adantr 482 . . . . . . 7 ((๐œ‘ โˆง ๐ต โ‰  ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ†’ (ฮฃ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต}๐‘˜ + ฮฃ๐‘˜ โˆˆ {1}๐‘˜) = (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) + 1))
284278, 283eqtrd 2773 . . . . . 6 ((๐œ‘ โˆง ๐ต โ‰  ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ†’ ฮฃ๐‘˜ โˆˆ {(๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)), ๐ต, 1}๐‘˜ = (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) + 1))
285204adantr 482 . . . . . 6 ((๐œ‘ โˆง ๐ต โ‰  ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ†’ ฮฃ๐‘˜ โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐ต}๐‘˜ = ((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))))
286263, 284, 2853brtr3d 5179 . . . . 5 ((๐œ‘ โˆง ๐ต โ‰  ((2โ†‘(๐ด + 1)) โˆ’ 1)) โ†’ (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) + 1) โ‰ค ((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))))
287286ex 414 . . . 4 (๐œ‘ โ†’ (๐ต โ‰  ((2โ†‘(๐ด + 1)) โˆ’ 1) โ†’ (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) + 1) โ‰ค ((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1)))))
288287necon1bd 2959 . . 3 (๐œ‘ โ†’ (ยฌ (((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) + 1) โ‰ค ((2โ†‘(๐ด + 1)) ยท (๐ต / ((2โ†‘(๐ด + 1)) โˆ’ 1))) โ†’ ๐ต = ((2โ†‘(๐ด + 1)) โˆ’ 1)))
289247, 288mpd 15 . 2 (๐œ‘ โ†’ ๐ต = ((2โ†‘(๐ด + 1)) โˆ’ 1))
290242, 289jca 513 1 (๐œ‘ โ†’ (๐ต โˆˆ โ„™ โˆง ๐ต = ((2โ†‘(๐ด + 1)) โˆ’ 1)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 846   โˆจ w3o 1087   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2941  โˆ€wral 3062  {crab 3433   โˆช cun 3946   โˆฉ cin 3947   โŠ† wss 3948  โˆ…c0 4322  {csn 4628  {cpr 4630  {ctp 4632   class class class wbr 5148  โ€˜cfv 6541  (class class class)co 7406  Fincfn 8936  โ„‚cc 11105  โ„cr 11106  0cc0 11107  1c1 11108   + caddc 11110   ยท cmul 11112   < clt 11245   โ‰ค cle 11246   โˆ’ cmin 11441   / cdiv 11868  โ„•cn 12209  2c2 12264  โ„•0cn0 12469  โ„คcz 12555  โ„คโ‰ฅcuz 12819  โ„+crp 12971  ...cfz 13481  โ†‘cexp 14024  ฮฃcsu 15629   โˆฅ cdvds 16194   gcd cgcd 16432  โ„™cprime 16605  โ†‘๐‘ccxp 26056   ฯƒ csgm 26590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-inf2 9633  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185  ax-addf 11186  ax-mulf 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-of 7667  df-om 7853  df-1st 7972  df-2nd 7973  df-supp 8144  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-2o 8464  df-er 8700  df-map 8819  df-pm 8820  df-ixp 8889  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fsupp 9359  df-fi 9403  df-sup 9434  df-inf 9435  df-oi 9502  df-card 9931  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ioc 13326  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-mod 13832  df-seq 13964  df-exp 14025  df-fac 14231  df-bc 14260  df-hash 14288  df-shft 15011  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-limsup 15412  df-clim 15429  df-rlim 15430  df-sum 15630  df-ef 16008  df-sin 16010  df-cos 16011  df-pi 16013  df-dvds 16195  df-gcd 16433  df-prm 16606  df-pc 16767  df-struct 17077  df-sets 17094  df-slot 17112  df-ndx 17124  df-base 17142  df-ress 17171  df-plusg 17207  df-mulr 17208  df-starv 17209  df-sca 17210  df-vsca 17211  df-ip 17212  df-tset 17213  df-ple 17214  df-ds 17216  df-unif 17217  df-hom 17218  df-cco 17219  df-rest 17365  df-topn 17366  df-0g 17384  df-gsum 17385  df-topgen 17386  df-pt 17387  df-prds 17390  df-xrs 17445  df-qtop 17450  df-imas 17451  df-xps 17453  df-mre 17527  df-mrc 17528  df-acs 17530  df-mgm 18558  df-sgrp 18607  df-mnd 18623  df-submnd 18669  df-mulg 18946  df-cntz 19176  df-cmn 19645  df-psmet 20929  df-xmet 20930  df-met 20931  df-bl 20932  df-mopn 20933  df-fbas 20934  df-fg 20935  df-cnfld 20938  df-top 22388  df-topon 22405  df-topsp 22427  df-bases 22441  df-cld 22515  df-ntr 22516  df-cls 22517  df-nei 22594  df-lp 22632  df-perf 22633  df-cn 22723  df-cnp 22724  df-haus 22811  df-tx 23058  df-hmeo 23251  df-fil 23342  df-fm 23434  df-flim 23435  df-flf 23436  df-xms 23818  df-ms 23819  df-tms 23820  df-cncf 24386  df-limc 25375  df-dv 25376  df-log 26057  df-cxp 26058  df-sgm 26596
This theorem is referenced by:  perfect  26724
  Copyright terms: Public domain W3C validator