Step | Hyp | Ref
| Expression |
1 | | prmgaplem7.f |
. . . 4
β’ (π β πΉ β (β βm
β)) |
2 | | elmapi 8794 |
. . . 4
β’ (πΉ β (β
βm β) β πΉ:ββΆβ) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β πΉ:ββΆβ) |
4 | | prmgaplem7.n |
. . 3
β’ (π β π β β) |
5 | 3, 4 | ffvelcdmd 7041 |
. 2
β’ (π β (πΉβπ) β β) |
6 | | simpr 486 |
. . . . . . 7
β’ ((π β§ (πΉβπ) β β) β (πΉβπ) β β) |
7 | | elnnuz 12814 |
. . . . . . 7
β’ ((πΉβπ) β β β (πΉβπ) β
(β€β₯β1)) |
8 | 6, 7 | sylib 217 |
. . . . . 6
β’ ((π β§ (πΉβπ) β β) β (πΉβπ) β
(β€β₯β1)) |
9 | | 2z 12542 |
. . . . . . 7
β’ 2 β
β€ |
10 | 9 | eluzaddi 12801 |
. . . . . 6
β’ ((πΉβπ) β (β€β₯β1)
β ((πΉβπ) + 2) β
(β€β₯β(1 + 2))) |
11 | 8, 10 | syl 17 |
. . . . 5
β’ ((π β§ (πΉβπ) β β) β ((πΉβπ) + 2) β
(β€β₯β(1 + 2))) |
12 | | 1p2e3 12303 |
. . . . . . 7
β’ (1 + 2) =
3 |
13 | 12 | eqcomi 2746 |
. . . . . 6
β’ 3 = (1 +
2) |
14 | 13 | fveq2i 6850 |
. . . . 5
β’
(β€β₯β3) = (β€β₯β(1 +
2)) |
15 | 11, 14 | eleqtrrdi 2849 |
. . . 4
β’ ((π β§ (πΉβπ) β β) β ((πΉβπ) + 2) β
(β€β₯β3)) |
16 | | prmgaplem5 16934 |
. . . 4
β’ (((πΉβπ) + 2) β
(β€β₯β3) β βπ β β (π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β)) |
17 | 15, 16 | syl 17 |
. . 3
β’ ((π β§ (πΉβπ) β β) β βπ β β (π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β)) |
18 | 4 | anim1ci 617 |
. . . . 5
β’ ((π β§ (πΉβπ) β β) β ((πΉβπ) β β β§ π β β)) |
19 | | nnaddcl 12183 |
. . . . 5
β’ (((πΉβπ) β β β§ π β β) β ((πΉβπ) + π) β β) |
20 | 18, 19 | syl 17 |
. . . 4
β’ ((π β§ (πΉβπ) β β) β ((πΉβπ) + π) β β) |
21 | | prmgaplem6 16935 |
. . . 4
β’ (((πΉβπ) + π) β β β βπ β β (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β)) |
22 | 20, 21 | syl 17 |
. . 3
β’ ((π β§ (πΉβπ) β β) β βπ β β (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β)) |
23 | | reeanv 3220 |
. . . 4
β’
(βπ β
β βπ β
β ((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β)) β (βπ β β (π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ βπ β β (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β))) |
24 | | simprll 778 |
. . . . . . . 8
β’
(((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β§ ((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β))) β π < ((πΉβπ) + 2)) |
25 | | simprrl 780 |
. . . . . . . 8
β’
(((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β§ ((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β))) β ((πΉβπ) + π) < π) |
26 | | nnz 12527 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉβπ) β β β (πΉβπ) β β€) |
27 | 26 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (πΉβπ) β β) β (πΉβπ) β β€) |
28 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (πΉβπ) β β) β 2 β
β€) |
29 | 27, 28 | zaddcld 12618 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (πΉβπ) β β) β ((πΉβπ) + 2) β β€) |
30 | 29 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β ((πΉβπ) + 2) β β€) |
31 | 30 | anim1ci 617 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β§ π§ β ((π + 1)..^π)) β (π§ β ((π + 1)..^π) β§ ((πΉβπ) + 2) β β€)) |
32 | | fzospliti 13611 |
. . . . . . . . . . . . . 14
β’ ((π§ β ((π + 1)..^π) β§ ((πΉβπ) + 2) β β€) β (π§ β ((π + 1)..^((πΉβπ) + 2)) β¨ π§ β (((πΉβπ) + 2)..^π))) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . 13
β’
(((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β§ π§ β ((π + 1)..^π)) β (π§ β ((π + 1)..^((πΉβπ) + 2)) β¨ π§ β (((πΉβπ) + 2)..^π))) |
34 | 33 | ex 414 |
. . . . . . . . . . . 12
β’ ((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β (π§ β ((π + 1)..^π) β (π§ β ((π + 1)..^((πΉβπ) + 2)) β¨ π§ β (((πΉβπ) + 2)..^π)))) |
35 | | neleq1 3055 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π§ β (π β β β π§ β β)) |
36 | 35 | rspcv 3580 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β ((π + 1)..^((πΉβπ) + 2)) β (βπ β ((π + 1)..^((πΉβπ) + 2))π β β β π§ β β)) |
37 | 36 | adantld 492 |
. . . . . . . . . . . . . . . 16
β’ (π§ β ((π + 1)..^((πΉβπ) + 2)) β ((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β π§ β β)) |
38 | 37 | adantrd 493 |
. . . . . . . . . . . . . . 15
β’ (π§ β ((π + 1)..^((πΉβπ) + 2)) β (((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β)) β π§ β β)) |
39 | 38 | a1d 25 |
. . . . . . . . . . . . . 14
β’ (π§ β ((π + 1)..^((πΉβπ) + 2)) β ((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β (((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β)) β π§ β β))) |
40 | 20 | nnzd 12533 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (πΉβπ) β β) β ((πΉβπ) + π) β β€) |
41 | 40 | peano2zd 12617 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (πΉβπ) β β) β (((πΉβπ) + π) + 1) β β€) |
42 | 41 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β (((πΉβπ) + π) + 1) β β€) |
43 | 42 | anim1ci 617 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β§ π§ β (((πΉβπ) + 2)..^π)) β (π§ β (((πΉβπ) + 2)..^π) β§ (((πΉβπ) + π) + 1) β β€)) |
44 | | fzospliti 13611 |
. . . . . . . . . . . . . . . . 17
β’ ((π§ β (((πΉβπ) + 2)..^π) β§ (((πΉβπ) + π) + 1) β β€) β (π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β¨ π§ β ((((πΉβπ) + π) + 1)..^π))) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β§ π§ β (((πΉβπ) + 2)..^π)) β (π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β¨ π§ β ((((πΉβπ) + π) + 1)..^π))) |
46 | 45 | ex 414 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β (π§ β (((πΉβπ) + 2)..^π) β (π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β¨ π§ β ((((πΉβπ) + π) + 1)..^π)))) |
47 | | prmgaplem7.i |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β βπ β (2...π)1 < (((πΉβπ) + π) gcd π)) |
48 | 4 | nnzd 12533 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π β β€) |
49 | | fzshftral 13536 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((2
β β€ β§ π
β β€ β§ (πΉβπ) β β€) β (βπ β (2...π)1 < (((πΉβπ) + π) gcd π) β βπ β ((2 + (πΉβπ))...(π + (πΉβπ)))[(π β (πΉβπ)) / π]1 < (((πΉβπ) + π) gcd π))) |
50 | 9, 48, 26, 49 | mp3an3an 1468 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (πΉβπ) β β) β (βπ β (2...π)1 < (((πΉβπ) + π) gcd π) β βπ β ((2 + (πΉβπ))...(π + (πΉβπ)))[(π β (πΉβπ)) / π]1 < (((πΉβπ) + π) gcd π))) |
51 | | 2cnd 12238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β 2 β
β) |
52 | | nncn 12168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((πΉβπ) β β β (πΉβπ) β β) |
53 | | addcom 11348 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((2
β β β§ (πΉβπ) β β) β (2 + (πΉβπ)) = ((πΉβπ) + 2)) |
54 | 51, 52, 53 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ (πΉβπ) β β) β (2 + (πΉβπ)) = ((πΉβπ) + 2)) |
55 | 4 | nncnd 12176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β π β β) |
56 | | addcom 11348 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β β β§ (πΉβπ) β β) β (π + (πΉβπ)) = ((πΉβπ) + π)) |
57 | 55, 52, 56 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ (πΉβπ) β β) β (π + (πΉβπ)) = ((πΉβπ) + π)) |
58 | 54, 57 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ (πΉβπ) β β) β ((2 + (πΉβπ))...(π + (πΉβπ))) = (((πΉβπ) + 2)...((πΉβπ) + π))) |
59 | | ovex 7395 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (πΉβπ)) β V |
60 | | sbcbr2g 5168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β (πΉβπ)) β V β ([(π β (πΉβπ)) / π]1 < (((πΉβπ) + π) gcd π) β 1 < β¦(π β (πΉβπ)) / πβ¦(((πΉβπ) + π) gcd π))) |
61 | 59, 60 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ (πΉβπ) β β) β ([(π β (πΉβπ)) / π]1 < (((πΉβπ) + π) gcd π) β 1 < β¦(π β (πΉβπ)) / πβ¦(((πΉβπ) + π) gcd π))) |
62 | | csbov12g 7406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β (πΉβπ)) β V β β¦(π β (πΉβπ)) / πβ¦(((πΉβπ) + π) gcd π) = (β¦(π β (πΉβπ)) / πβ¦((πΉβπ) + π) gcd β¦(π β (πΉβπ)) / πβ¦π)) |
63 | 59, 62 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ (πΉβπ) β β) β
β¦(π β
(πΉβπ)) / πβ¦(((πΉβπ) + π) gcd π) = (β¦(π β (πΉβπ)) / πβ¦((πΉβπ) + π) gcd β¦(π β (πΉβπ)) / πβ¦π)) |
64 | | csbov2g 7408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β (πΉβπ)) β V β β¦(π β (πΉβπ)) / πβ¦((πΉβπ) + π) = ((πΉβπ) + β¦(π β (πΉβπ)) / πβ¦π)) |
65 | 59, 64 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ (πΉβπ) β β) β
β¦(π β
(πΉβπ)) / πβ¦((πΉβπ) + π) = ((πΉβπ) + β¦(π β (πΉβπ)) / πβ¦π)) |
66 | | csbvarg 4396 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β (πΉβπ)) β V β β¦(π β (πΉβπ)) / πβ¦π = (π β (πΉβπ))) |
67 | 66 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β (πΉβπ)) β V β ((πΉβπ) + β¦(π β (πΉβπ)) / πβ¦π) = ((πΉβπ) + (π β (πΉβπ)))) |
68 | 59, 67 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ (πΉβπ) β β) β ((πΉβπ) + β¦(π β (πΉβπ)) / πβ¦π) = ((πΉβπ) + (π β (πΉβπ)))) |
69 | 65, 68 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ (πΉβπ) β β) β
β¦(π β
(πΉβπ)) / πβ¦((πΉβπ) + π) = ((πΉβπ) + (π β (πΉβπ)))) |
70 | 59, 66 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ (πΉβπ) β β) β
β¦(π β
(πΉβπ)) / πβ¦π = (π β (πΉβπ))) |
71 | 69, 70 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ (πΉβπ) β β) β
(β¦(π β
(πΉβπ)) / πβ¦((πΉβπ) + π) gcd β¦(π β (πΉβπ)) / πβ¦π) = (((πΉβπ) + (π β (πΉβπ))) gcd (π β (πΉβπ)))) |
72 | 63, 71 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ (πΉβπ) β β) β
β¦(π β
(πΉβπ)) / πβ¦(((πΉβπ) + π) gcd π) = (((πΉβπ) + (π β (πΉβπ))) gcd (π β (πΉβπ)))) |
73 | 72 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ (πΉβπ) β β) β (1 <
β¦(π β
(πΉβπ)) / πβ¦(((πΉβπ) + π) gcd π) β 1 < (((πΉβπ) + (π β (πΉβπ))) gcd (π β (πΉβπ))))) |
74 | 61, 73 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ (πΉβπ) β β) β ([(π β (πΉβπ)) / π]1 < (((πΉβπ) + π) gcd π) β 1 < (((πΉβπ) + (π β (πΉβπ))) gcd (π β (πΉβπ))))) |
75 | 58, 74 | raleqbidv 3322 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ (πΉβπ) β β) β (βπ β ((2 + (πΉβπ))...(π + (πΉβπ)))[(π β (πΉβπ)) / π]1 < (((πΉβπ) + π) gcd π) β βπ β (((πΉβπ) + 2)...((πΉβπ) + π))1 < (((πΉβπ) + (π β (πΉβπ))) gcd (π β (πΉβπ))))) |
76 | | fzval3 13648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((πΉβπ) + π) β β€ β (((πΉβπ) + 2)...((πΉβπ) + π)) = (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) |
77 | 76 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((πΉβπ) + π) β β€ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) = (((πΉβπ) + 2)...((πΉβπ) + π))) |
78 | 40, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ (πΉβπ) β β) β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) = (((πΉβπ) + 2)...((πΉβπ) + π))) |
79 | 78 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ (πΉβπ) β β) β (π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β π§ β (((πΉβπ) + 2)...((πΉβπ) + π)))) |
80 | 79 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ (πΉβπ) β β) β§ π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) β π§ β (((πΉβπ) + 2)...((πΉβπ) + π))) |
81 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = π§ β (π β (πΉβπ)) = (π§ β (πΉβπ))) |
82 | 81 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π = π§ β ((πΉβπ) + (π β (πΉβπ))) = ((πΉβπ) + (π§ β (πΉβπ)))) |
83 | 82, 81 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π = π§ β (((πΉβπ) + (π β (πΉβπ))) gcd (π β (πΉβπ))) = (((πΉβπ) + (π§ β (πΉβπ))) gcd (π§ β (πΉβπ)))) |
84 | 83 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = π§ β (1 < (((πΉβπ) + (π β (πΉβπ))) gcd (π β (πΉβπ))) β 1 < (((πΉβπ) + (π§ β (πΉβπ))) gcd (π§ β (πΉβπ))))) |
85 | 84 | rspcv 3580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π§ β (((πΉβπ) + 2)...((πΉβπ) + π)) β (βπ β (((πΉβπ) + 2)...((πΉβπ) + π))1 < (((πΉβπ) + (π β (πΉβπ))) gcd (π β (πΉβπ))) β 1 < (((πΉβπ) + (π§ β (πΉβπ))) gcd (π§ β (πΉβπ))))) |
86 | 80, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ (πΉβπ) β β) β§ π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) β (βπ β (((πΉβπ) + 2)...((πΉβπ) + π))1 < (((πΉβπ) + (π β (πΉβπ))) gcd (π β (πΉβπ))) β 1 < (((πΉβπ) + (π§ β (πΉβπ))) gcd (π§ β (πΉβπ))))) |
87 | 52 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β§ (πΉβπ) β β) β (πΉβπ) β β) |
88 | | elfzoelz 13579 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β π§ β β€) |
89 | 88 | zcnd 12615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β π§ β β) |
90 | | pncan3 11416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((πΉβπ) β β β§ π§ β β) β ((πΉβπ) + (π§ β (πΉβπ))) = π§) |
91 | 87, 89, 90 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ (πΉβπ) β β) β§ π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) β ((πΉβπ) + (π§ β (πΉβπ))) = π§) |
92 | 91 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ (πΉβπ) β β) β§ π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) β (((πΉβπ) + (π§ β (πΉβπ))) gcd (π§ β (πΉβπ))) = (π§ gcd (π§ β (πΉβπ)))) |
93 | 88 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ (πΉβπ) β β) β§ π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) β π§ β β€) |
94 | | zsubcl 12552 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π§ β β€ β§ (πΉβπ) β β€) β (π§ β (πΉβπ)) β β€) |
95 | 88, 27, 94 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ (πΉβπ) β β) β§ π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) β (π§ β (πΉβπ)) β β€) |
96 | 93, 95 | gcdcomd 16401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ (πΉβπ) β β) β§ π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) β (π§ gcd (π§ β (πΉβπ))) = ((π§ β (πΉβπ)) gcd π§)) |
97 | 92, 96 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ (πΉβπ) β β) β§ π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) β (((πΉβπ) + (π§ β (πΉβπ))) gcd (π§ β (πΉβπ))) = ((π§ β (πΉβπ)) gcd π§)) |
98 | 97 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ (πΉβπ) β β) β§ π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) β (1 < (((πΉβπ) + (π§ β (πΉβπ))) gcd (π§ β (πΉβπ))) β 1 < ((π§ β (πΉβπ)) gcd π§))) |
99 | | elfzo2 13582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β (π§ β (β€β₯β((πΉβπ) + 2)) β§ (((πΉβπ) + π) + 1) β β€ β§ π§ < (((πΉβπ) + π) + 1))) |
100 | | eluz2 12776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π§ β
(β€β₯β((πΉβπ) + 2)) β (((πΉβπ) + 2) β β€ β§ π§ β β€ β§ ((πΉβπ) + 2) β€ π§)) |
101 | | nnre 12167 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((πΉβπ) β β β (πΉβπ) β β) |
102 | 101 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((π§ β β€ β§ (π β§ (πΉβπ) β β)) β (πΉβπ) β β) |
103 | | 2rp 12927 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ 2 β
β+ |
104 | 103 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((π§ β β€ β§ (π β§ (πΉβπ) β β)) β 2 β
β+) |
105 | 102, 104 | ltaddrpd 12997 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π§ β β€ β§ (π β§ (πΉβπ) β β)) β (πΉβπ) < ((πΉβπ) + 2)) |
106 | | 2re 12234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ 2 β
β |
107 | 106 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((πΉβπ) β β β 2 β
β) |
108 | 101, 107 | readdcld 11191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((πΉβπ) β β β ((πΉβπ) + 2) β β) |
109 | 108 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((π§ β β€ β§ (π β§ (πΉβπ) β β)) β ((πΉβπ) + 2) β β) |
110 | | zre 12510 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ (π§ β β€ β π§ β
β) |
111 | 110 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((π§ β β€ β§ (π β§ (πΉβπ) β β)) β π§ β β) |
112 | | ltletr 11254 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (((πΉβπ) β β β§ ((πΉβπ) + 2) β β β§ π§ β β) β (((πΉβπ) < ((πΉβπ) + 2) β§ ((πΉβπ) + 2) β€ π§) β (πΉβπ) < π§)) |
113 | 102, 109,
111, 112 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π§ β β€ β§ (π β§ (πΉβπ) β β)) β (((πΉβπ) < ((πΉβπ) + 2) β§ ((πΉβπ) + 2) β€ π§) β (πΉβπ) < π§)) |
114 | 105, 113 | mpand 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π§ β β€ β§ (π β§ (πΉβπ) β β)) β (((πΉβπ) + 2) β€ π§ β (πΉβπ) < π§)) |
115 | 114 | impancom 453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π§ β β€ β§ ((πΉβπ) + 2) β€ π§) β ((π β§ (πΉβπ) β β) β (πΉβπ) < π§)) |
116 | 115 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((((πΉβπ) + 2) β β€ β§ π§ β β€ β§ ((πΉβπ) + 2) β€ π§) β ((π β§ (πΉβπ) β β) β (πΉβπ) < π§)) |
117 | 100, 116 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π§ β
(β€β₯β((πΉβπ) + 2)) β ((π β§ (πΉβπ) β β) β (πΉβπ) < π§)) |
118 | 117 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π§ β
(β€β₯β((πΉβπ) + 2)) β§ (((πΉβπ) + π) + 1) β β€ β§ π§ < (((πΉβπ) + π) + 1)) β ((π β§ (πΉβπ) β β) β (πΉβπ) < π§)) |
119 | 99, 118 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β ((π β§ (πΉβπ) β β) β (πΉβπ) < π§)) |
120 | 119 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ (πΉβπ) β β) β§ π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) β (πΉβπ) < π§) |
121 | 101 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β§ (πΉβπ) β β) β (πΉβπ) β β) |
122 | 88 | zred 12614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β π§ β β) |
123 | | posdif 11655 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((πΉβπ) β β β§ π§ β β) β ((πΉβπ) < π§ β 0 < (π§ β (πΉβπ)))) |
124 | 121, 122,
123 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ (πΉβπ) β β) β§ π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) β ((πΉβπ) < π§ β 0 < (π§ β (πΉβπ)))) |
125 | 120, 124 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ (πΉβπ) β β) β§ π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) β 0 < (π§ β (πΉβπ))) |
126 | | elnnz 12516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π§ β (πΉβπ)) β β β ((π§ β (πΉβπ)) β β€ β§ 0 < (π§ β (πΉβπ)))) |
127 | 95, 125, 126 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ (πΉβπ) β β) β§ π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) β (π§ β (πΉβπ)) β β) |
128 | 106 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π§ β β€ β§ (π β§ (πΉβπ) β β)) β 2 β
β) |
129 | | nngt0 12191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((πΉβπ) β β β 0 < (πΉβπ)) |
130 | 129 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π§ β β€ β§ (π β§ (πΉβπ) β β)) β 0 < (πΉβπ)) |
131 | | 2pos 12263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ 0 <
2 |
132 | 131 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π§ β β€ β§ (π β§ (πΉβπ) β β)) β 0 <
2) |
133 | 102, 128,
130, 132 | addgt0d 11737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π§ β β€ β§ (π β§ (πΉβπ) β β)) β 0 < ((πΉβπ) + 2)) |
134 | | 0red 11165 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π§ β β€ β§ (π β§ (πΉβπ) β β)) β 0 β
β) |
135 | | ltletr 11254 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((0
β β β§ ((πΉβπ) + 2) β β β§ π§ β β) β ((0 <
((πΉβπ) + 2) β§ ((πΉβπ) + 2) β€ π§) β 0 < π§)) |
136 | 134, 109,
111, 135 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π§ β β€ β§ (π β§ (πΉβπ) β β)) β ((0 < ((πΉβπ) + 2) β§ ((πΉβπ) + 2) β€ π§) β 0 < π§)) |
137 | 133, 136 | mpand 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π§ β β€ β§ (π β§ (πΉβπ) β β)) β (((πΉβπ) + 2) β€ π§ β 0 < π§)) |
138 | 137 | impancom 453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π§ β β€ β§ ((πΉβπ) + 2) β€ π§) β ((π β§ (πΉβπ) β β) β 0 < π§)) |
139 | 138 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((((πΉβπ) + 2) β β€ β§ π§ β β€ β§ ((πΉβπ) + 2) β€ π§) β ((π β§ (πΉβπ) β β) β 0 < π§)) |
140 | 100, 139 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π§ β
(β€β₯β((πΉβπ) + 2)) β ((π β§ (πΉβπ) β β) β 0 < π§)) |
141 | 140 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π§ β
(β€β₯β((πΉβπ) + 2)) β§ (((πΉβπ) + π) + 1) β β€ β§ π§ < (((πΉβπ) + π) + 1)) β ((π β§ (πΉβπ) β β) β 0 < π§)) |
142 | 99, 141 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β ((π β§ (πΉβπ) β β) β 0 < π§)) |
143 | 142 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ (πΉβπ) β β) β§ π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) β 0 < π§) |
144 | | elnnz 12516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π§ β β β (π§ β β€ β§ 0 <
π§)) |
145 | 93, 143, 144 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ (πΉβπ) β β) β§ π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) β π§ β β) |
146 | 129 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β§ (πΉβπ) β β) β 0 < (πΉβπ)) |
147 | 146 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ (πΉβπ) β β) β§ π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) β 0 < (πΉβπ)) |
148 | | ltsubpos 11654 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((πΉβπ) β β β§ π§ β β) β (0 < (πΉβπ) β (π§ β (πΉβπ)) < π§)) |
149 | 121, 122,
148 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ (πΉβπ) β β) β§ π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) β (0 < (πΉβπ) β (π§ β (πΉβπ)) < π§)) |
150 | 147, 149 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ (πΉβπ) β β) β§ π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) β (π§ β (πΉβπ)) < π§) |
151 | | ncoprmlnprm 16610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π§ β (πΉβπ)) β β β§ π§ β β β§ (π§ β (πΉβπ)) < π§) β (1 < ((π§ β (πΉβπ)) gcd π§) β π§ β β)) |
152 | 127, 145,
150, 151 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ (πΉβπ) β β) β§ π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) β (1 < ((π§ β (πΉβπ)) gcd π§) β π§ β β)) |
153 | 98, 152 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ (πΉβπ) β β) β§ π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) β (1 < (((πΉβπ) + (π§ β (πΉβπ))) gcd (π§ β (πΉβπ))) β π§ β β)) |
154 | 86, 153 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ (πΉβπ) β β) β§ π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1))) β (βπ β (((πΉβπ) + 2)...((πΉβπ) + π))1 < (((πΉβπ) + (π β (πΉβπ))) gcd (π β (πΉβπ))) β π§ β β)) |
155 | 154 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ (πΉβπ) β β) β (π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β (βπ β (((πΉβπ) + 2)...((πΉβπ) + π))1 < (((πΉβπ) + (π β (πΉβπ))) gcd (π β (πΉβπ))) β π§ β β))) |
156 | 155 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ (πΉβπ) β β) β (βπ β (((πΉβπ) + 2)...((πΉβπ) + π))1 < (((πΉβπ) + (π β (πΉβπ))) gcd (π β (πΉβπ))) β (π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β π§ β β))) |
157 | 75, 156 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (πΉβπ) β β) β (βπ β ((2 + (πΉβπ))...(π + (πΉβπ)))[(π β (πΉβπ)) / π]1 < (((πΉβπ) + π) gcd π) β (π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β π§ β β))) |
158 | 50, 157 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (πΉβπ) β β) β (βπ β (2...π)1 < (((πΉβπ) + π) gcd π) β (π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β π§ β β))) |
159 | 158 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β ((πΉβπ) β β β (βπ β (2...π)1 < (((πΉβπ) + π) gcd π) β (π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β π§ β β)))) |
160 | 47, 159 | mpid 44 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((πΉβπ) β β β (π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β π§ β β))) |
161 | 160 | imp 408 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (πΉβπ) β β) β (π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β π§ β β)) |
162 | 161 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β (π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β π§ β β)) |
163 | 162 | impcom 409 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β§ (((π β§ (πΉβπ) β β) β§ π β β) β§ π β β)) β π§ β β) |
164 | 163 | a1d 25 |
. . . . . . . . . . . . . . . . . 18
β’ ((π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β§ (((π β§ (πΉβπ) β β) β§ π β β) β§ π β β)) β (((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β)) β π§ β β)) |
165 | 164 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β ((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β (((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β)) β π§ β β))) |
166 | | neleq1 3055 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π§ β (π β β β π§ β β)) |
167 | 166 | rspcv 3580 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ β ((((πΉβπ) + π) + 1)..^π) β (βπ β ((((πΉβπ) + π) + 1)..^π)π β β β π§ β β)) |
168 | 167 | adantld 492 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β ((((πΉβπ) + π) + 1)..^π) β ((((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β) β π§ β β)) |
169 | 168 | adantld 492 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β ((((πΉβπ) + π) + 1)..^π) β (((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β)) β π§ β β)) |
170 | 169 | a1d 25 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β ((((πΉβπ) + π) + 1)..^π) β ((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β (((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β)) β π§ β β))) |
171 | 165, 170 | jaoi 856 |
. . . . . . . . . . . . . . . 16
β’ ((π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β¨ π§ β ((((πΉβπ) + π) + 1)..^π)) β ((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β (((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β)) β π§ β β))) |
172 | 171 | com12 32 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β ((π§ β (((πΉβπ) + 2)..^(((πΉβπ) + π) + 1)) β¨ π§ β ((((πΉβπ) + π) + 1)..^π)) β (((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β)) β π§ β β))) |
173 | 46, 172 | syldc 48 |
. . . . . . . . . . . . . 14
β’ (π§ β (((πΉβπ) + 2)..^π) β ((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β (((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β)) β π§ β β))) |
174 | 39, 173 | jaoi 856 |
. . . . . . . . . . . . 13
β’ ((π§ β ((π + 1)..^((πΉβπ) + 2)) β¨ π§ β (((πΉβπ) + 2)..^π)) β ((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β (((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β)) β π§ β β))) |
175 | 174 | com12 32 |
. . . . . . . . . . . 12
β’ ((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β ((π§ β ((π + 1)..^((πΉβπ) + 2)) β¨ π§ β (((πΉβπ) + 2)..^π)) β (((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β)) β π§ β β))) |
176 | 34, 175 | syld 47 |
. . . . . . . . . . 11
β’ ((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β (π§ β ((π + 1)..^π) β (((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β)) β π§ β β))) |
177 | 176 | com23 86 |
. . . . . . . . . 10
β’ ((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β (((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β)) β (π§ β ((π + 1)..^π) β π§ β β))) |
178 | 177 | imp31 419 |
. . . . . . . . 9
β’
((((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β§ ((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β))) β§ π§ β ((π + 1)..^π)) β π§ β β) |
179 | 178 | ralrimiva 3144 |
. . . . . . . 8
β’
(((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β§ ((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β))) β βπ§ β ((π + 1)..^π)π§ β β) |
180 | 24, 25, 179 | 3jca 1129 |
. . . . . . 7
β’
(((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β§ ((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β))) β (π < ((πΉβπ) + 2) β§ ((πΉβπ) + π) < π β§ βπ§ β ((π + 1)..^π)π§ β β)) |
181 | 180 | ex 414 |
. . . . . 6
β’ ((((π β§ (πΉβπ) β β) β§ π β β) β§ π β β) β (((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β)) β (π < ((πΉβπ) + 2) β§ ((πΉβπ) + π) < π β§ βπ§ β ((π + 1)..^π)π§ β β))) |
182 | 181 | reximdva 3166 |
. . . . 5
β’ (((π β§ (πΉβπ) β β) β§ π β β) β (βπ β β ((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β)) β βπ β β (π < ((πΉβπ) + 2) β§ ((πΉβπ) + π) < π β§ βπ§ β ((π + 1)..^π)π§ β β))) |
183 | 182 | reximdva 3166 |
. . . 4
β’ ((π β§ (πΉβπ) β β) β (βπ β β βπ β β ((π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β)) β βπ β β βπ β β (π < ((πΉβπ) + 2) β§ ((πΉβπ) + π) < π β§ βπ§ β ((π + 1)..^π)π§ β β))) |
184 | 23, 183 | biimtrrid 242 |
. . 3
β’ ((π β§ (πΉβπ) β β) β ((βπ β β (π < ((πΉβπ) + 2) β§ βπ β ((π + 1)..^((πΉβπ) + 2))π β β) β§ βπ β β (((πΉβπ) + π) < π β§ βπ β ((((πΉβπ) + π) + 1)..^π)π β β)) β βπ β β βπ β β (π < ((πΉβπ) + 2) β§ ((πΉβπ) + π) < π β§ βπ§ β ((π + 1)..^π)π§ β β))) |
185 | 17, 22, 184 | mp2and 698 |
. 2
β’ ((π β§ (πΉβπ) β β) β βπ β β βπ β β (π < ((πΉβπ) + 2) β§ ((πΉβπ) + π) < π β§ βπ§ β ((π + 1)..^π)π§ β β)) |
186 | 5, 185 | mpdan 686 |
1
β’ (π β βπ β β βπ β β (π < ((πΉβπ) + 2) β§ ((πΉβπ) + π) < π β§ βπ§ β ((π + 1)..^π)π§ β β)) |