Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . 3
β’ (π β β β π β
β) |
2 | | fzssz 13450 |
. . . . . . . 8
β’
(1...π₯) β
β€ |
3 | 2 | a1i 11 |
. . . . . . 7
β’ (π₯ β β β
(1...π₯) β
β€) |
4 | | fzfi 13884 |
. . . . . . . 8
β’
(1...π₯) β
Fin |
5 | 4 | a1i 11 |
. . . . . . 7
β’ (π₯ β β β
(1...π₯) β
Fin) |
6 | | 0nelfz1 13467 |
. . . . . . . 8
β’ 0 β
(1...π₯) |
7 | 6 | a1i 11 |
. . . . . . 7
β’ (π₯ β β β 0 β
(1...π₯)) |
8 | | lcmfn0cl 16509 |
. . . . . . 7
β’
(((1...π₯) β
β€ β§ (1...π₯)
β Fin β§ 0 β (1...π₯)) β (lcmβ(1...π₯)) β
β) |
9 | 3, 5, 7, 8 | syl3anc 1372 |
. . . . . 6
β’ (π₯ β β β
(lcmβ(1...π₯))
β β) |
10 | 9 | adantl 483 |
. . . . 5
β’ ((π β β β§ π₯ β β) β
(lcmβ(1...π₯))
β β) |
11 | | eqid 2737 |
. . . . 5
β’ (π₯ β β β¦
(lcmβ(1...π₯)))
= (π₯ β β β¦
(lcmβ(1...π₯))) |
12 | 10, 11 | fmptd 7067 |
. . . 4
β’ (π β β β (π₯ β β β¦
(lcmβ(1...π₯))):ββΆβ) |
13 | | nnex 12166 |
. . . . . 6
β’ β
β V |
14 | 13, 13 | pm3.2i 472 |
. . . . 5
β’ (β
β V β§ β β V) |
15 | | elmapg 8785 |
. . . . 5
β’ ((β
β V β§ β β V) β ((π₯ β β β¦
(lcmβ(1...π₯)))
β (β βm β) β (π₯ β β β¦
(lcmβ(1...π₯))):ββΆβ)) |
16 | 14, 15 | mp1i 13 |
. . . 4
β’ (π β β β ((π₯ β β β¦
(lcmβ(1...π₯)))
β (β βm β) β (π₯ β β β¦
(lcmβ(1...π₯))):ββΆβ)) |
17 | 12, 16 | mpbird 257 |
. . 3
β’ (π β β β (π₯ β β β¦
(lcmβ(1...π₯)))
β (β βm β)) |
18 | | prmgaplcmlem2 16931 |
. . . . 5
β’ ((π β β β§ π β (2...π)) β 1 <
(((lcmβ(1...π)) + π) gcd π)) |
19 | | eqidd 2738 |
. . . . . . . 8
β’ ((π β β β§ π β (2...π)) β (π₯ β β β¦
(lcmβ(1...π₯)))
= (π₯ β β β¦
(lcmβ(1...π₯)))) |
20 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π₯ = π β (1...π₯) = (1...π)) |
21 | 20 | fveq2d 6851 |
. . . . . . . . 9
β’ (π₯ = π β (lcmβ(1...π₯)) =
(lcmβ(1...π))) |
22 | 21 | adantl 483 |
. . . . . . . 8
β’ (((π β β β§ π β (2...π)) β§ π₯ = π) β (lcmβ(1...π₯)) =
(lcmβ(1...π))) |
23 | | simpl 484 |
. . . . . . . 8
β’ ((π β β β§ π β (2...π)) β π β β) |
24 | | fzssz 13450 |
. . . . . . . . . 10
β’
(1...π) β
β€ |
25 | | fzfi 13884 |
. . . . . . . . . 10
β’
(1...π) β
Fin |
26 | 24, 25 | pm3.2i 472 |
. . . . . . . . 9
β’
((1...π) β
β€ β§ (1...π)
β Fin) |
27 | | lcmfcl 16511 |
. . . . . . . . 9
β’
(((1...π) β
β€ β§ (1...π)
β Fin) β (lcmβ(1...π)) β
β0) |
28 | 26, 27 | mp1i 13 |
. . . . . . . 8
β’ ((π β β β§ π β (2...π)) β (lcmβ(1...π)) β
β0) |
29 | 19, 22, 23, 28 | fvmptd 6960 |
. . . . . . 7
β’ ((π β β β§ π β (2...π)) β ((π₯ β β β¦
(lcmβ(1...π₯)))βπ) = (lcmβ(1...π))) |
30 | 29 | oveq1d 7377 |
. . . . . 6
β’ ((π β β β§ π β (2...π)) β (((π₯ β β β¦
(lcmβ(1...π₯)))βπ) + π) = ((lcmβ(1...π)) + π)) |
31 | 30 | oveq1d 7377 |
. . . . 5
β’ ((π β β β§ π β (2...π)) β ((((π₯ β β β¦
(lcmβ(1...π₯)))βπ) + π) gcd π) = (((lcmβ(1...π)) + π) gcd π)) |
32 | 18, 31 | breqtrrd 5138 |
. . . 4
β’ ((π β β β§ π β (2...π)) β 1 < ((((π₯ β β β¦
(lcmβ(1...π₯)))βπ) + π) gcd π)) |
33 | 32 | ralrimiva 3144 |
. . 3
β’ (π β β β
βπ β (2...π)1 < ((((π₯ β β β¦
(lcmβ(1...π₯)))βπ) + π) gcd π)) |
34 | 1, 17, 33 | prmgaplem8 16937 |
. 2
β’ (π β β β
βπ β β
βπ β β
(π β€ (π β π) β§ βπ§ β ((π + 1)..^π)π§ β β)) |
35 | 34 | rgen 3067 |
1
β’
βπ β
β βπ β
β βπ β
β (π β€ (π β π) β§ βπ§ β ((π + 1)..^π)π§ β β) |