Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . 3
β’ (π β β β π β
β) |
2 | | eqid 2733 |
. . . . . 6
β’ (π β β β¦
βπ β (1...π)((π β β β¦ if(π β β, π, 1))βπ)) = (π β β β¦ βπ β (1...π)((π β β β¦ if(π β β, π, 1))βπ)) |
3 | | fzfid 13938 |
. . . . . . 7
β’ (π β β β
(1...π) β
Fin) |
4 | | eqidd 2734 |
. . . . . . . . 9
β’ ((π β β β§ π β (1...π)) β (π β β β¦ if(π β β, π, 1)) = (π β β β¦ if(π β β, π, 1))) |
5 | | eleq1 2822 |
. . . . . . . . . . 11
β’ (π = π β (π β β β π β β)) |
6 | | id 22 |
. . . . . . . . . . 11
β’ (π = π β π = π) |
7 | 5, 6 | ifbieq1d 4553 |
. . . . . . . . . 10
β’ (π = π β if(π β β, π, 1) = if(π β β, π, 1)) |
8 | 7 | adantl 483 |
. . . . . . . . 9
β’ (((π β β β§ π β (1...π)) β§ π = π) β if(π β β, π, 1) = if(π β β, π, 1)) |
9 | | elfznn 13530 |
. . . . . . . . . 10
β’ (π β (1...π) β π β β) |
10 | 9 | adantl 483 |
. . . . . . . . 9
β’ ((π β β β§ π β (1...π)) β π β β) |
11 | | 1nn 12223 |
. . . . . . . . . . . 12
β’ 1 β
β |
12 | 11 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (1...π) β 1 β β) |
13 | 9, 12 | ifcld 4575 |
. . . . . . . . . 10
β’ (π β (1...π) β if(π β β, π, 1) β β) |
14 | 13 | adantl 483 |
. . . . . . . . 9
β’ ((π β β β§ π β (1...π)) β if(π β β, π, 1) β β) |
15 | 4, 8, 10, 14 | fvmptd 7006 |
. . . . . . . 8
β’ ((π β β β§ π β (1...π)) β ((π β β β¦ if(π β β, π, 1))βπ) = if(π β β, π, 1)) |
16 | 15, 14 | eqeltrd 2834 |
. . . . . . 7
β’ ((π β β β§ π β (1...π)) β ((π β β β¦ if(π β β, π, 1))βπ) β β) |
17 | 3, 16 | fprodnncl 15899 |
. . . . . 6
β’ (π β β β
βπ β (1...π)((π β β β¦ if(π β β, π, 1))βπ) β β) |
18 | 2, 17 | fmpti 7112 |
. . . . 5
β’ (π β β β¦
βπ β (1...π)((π β β β¦ if(π β β, π, 1))βπ)):ββΆβ |
19 | | nnex 12218 |
. . . . . 6
β’ β
β V |
20 | 19, 19 | elmap 8865 |
. . . . 5
β’ ((π β β β¦
βπ β (1...π)((π β β β¦ if(π β β, π, 1))βπ)) β (β βm
β) β (π β
β β¦ βπ
β (1...π)((π β β β¦ if(π β β, π, 1))βπ)):ββΆβ) |
21 | 18, 20 | mpbir 230 |
. . . 4
β’ (π β β β¦
βπ β (1...π)((π β β β¦ if(π β β, π, 1))βπ)) β (β βm
β) |
22 | 21 | a1i 11 |
. . 3
β’ (π β β β (π β β β¦
βπ β (1...π)((π β β β¦ if(π β β, π, 1))βπ)) β (β βm
β)) |
23 | | prmgapprmolem 16994 |
. . . . 5
β’ ((π β β β§ π β (2...π)) β 1 < (((#pβπ) + π) gcd π)) |
24 | | eqidd 2734 |
. . . . . . . . . . . 12
β’ ((((π β β β§ π β (2...π)) β§ π β β) β§ π β (1...π)) β (π β β β¦ if(π β β, π, 1)) = (π β β β¦ if(π β β, π, 1))) |
25 | 7 | adantl 483 |
. . . . . . . . . . . 12
β’
(((((π β
β β§ π β
(2...π)) β§ π β β) β§ π β (1...π)) β§ π = π) β if(π β β, π, 1) = if(π β β, π, 1)) |
26 | 9 | adantl 483 |
. . . . . . . . . . . 12
β’ ((((π β β β§ π β (2...π)) β§ π β β) β§ π β (1...π)) β π β β) |
27 | | elfzelz 13501 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β π β β€) |
28 | | 1zzd 12593 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β 1 β β€) |
29 | 27, 28 | ifcld 4575 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β if(π β β, π, 1) β β€) |
30 | 29 | adantl 483 |
. . . . . . . . . . . 12
β’ ((((π β β β§ π β (2...π)) β§ π β β) β§ π β (1...π)) β if(π β β, π, 1) β β€) |
31 | 24, 25, 26, 30 | fvmptd 7006 |
. . . . . . . . . . 11
β’ ((((π β β β§ π β (2...π)) β§ π β β) β§ π β (1...π)) β ((π β β β¦ if(π β β, π, 1))βπ) = if(π β β, π, 1)) |
32 | 31 | prodeq2dv 15867 |
. . . . . . . . . 10
β’ (((π β β β§ π β (2...π)) β§ π β β) β βπ β (1...π)((π β β β¦ if(π β β, π, 1))βπ) = βπ β (1...π)if(π β β, π, 1)) |
33 | 32 | mpteq2dva 5249 |
. . . . . . . . 9
β’ ((π β β β§ π β (2...π)) β (π β β β¦ βπ β (1...π)((π β β β¦ if(π β β, π, 1))βπ)) = (π β β β¦ βπ β (1...π)if(π β β, π, 1))) |
34 | | oveq2 7417 |
. . . . . . . . . . 11
β’ (π = π β (1...π) = (1...π)) |
35 | 34 | prodeq1d 15865 |
. . . . . . . . . 10
β’ (π = π β βπ β (1...π)if(π β β, π, 1) = βπ β (1...π)if(π β β, π, 1)) |
36 | 35 | adantl 483 |
. . . . . . . . 9
β’ (((π β β β§ π β (2...π)) β§ π = π) β βπ β (1...π)if(π β β, π, 1) = βπ β (1...π)if(π β β, π, 1)) |
37 | | simpl 484 |
. . . . . . . . 9
β’ ((π β β β§ π β (2...π)) β π β β) |
38 | | fzfid 13938 |
. . . . . . . . . 10
β’ ((π β β β§ π β (2...π)) β (1...π) β Fin) |
39 | | elfznn 13530 |
. . . . . . . . . . . 12
β’ (π β (1...π) β π β β) |
40 | 11 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (1...π) β 1 β β) |
41 | 39, 40 | ifcld 4575 |
. . . . . . . . . . 11
β’ (π β (1...π) β if(π β β, π, 1) β β) |
42 | 41 | adantl 483 |
. . . . . . . . . 10
β’ (((π β β β§ π β (2...π)) β§ π β (1...π)) β if(π β β, π, 1) β β) |
43 | 38, 42 | fprodnncl 15899 |
. . . . . . . . 9
β’ ((π β β β§ π β (2...π)) β βπ β (1...π)if(π β β, π, 1) β β) |
44 | 33, 36, 37, 43 | fvmptd 7006 |
. . . . . . . 8
β’ ((π β β β§ π β (2...π)) β ((π β β β¦ βπ β (1...π)((π β β β¦ if(π β β, π, 1))βπ))βπ) = βπ β (1...π)if(π β β, π, 1)) |
45 | | nnnn0 12479 |
. . . . . . . . . . 11
β’ (π β β β π β
β0) |
46 | | prmoval 16966 |
. . . . . . . . . . 11
β’ (π β β0
β (#pβπ) = βπ β (1...π)if(π β β, π, 1)) |
47 | 45, 46 | syl 17 |
. . . . . . . . . 10
β’ (π β β β
(#pβπ) =
βπ β (1...π)if(π β β, π, 1)) |
48 | 47 | eqcomd 2739 |
. . . . . . . . 9
β’ (π β β β
βπ β (1...π)if(π β β, π, 1) = (#pβπ)) |
49 | 48 | adantr 482 |
. . . . . . . 8
β’ ((π β β β§ π β (2...π)) β βπ β (1...π)if(π β β, π, 1) = (#pβπ)) |
50 | 44, 49 | eqtrd 2773 |
. . . . . . 7
β’ ((π β β β§ π β (2...π)) β ((π β β β¦ βπ β (1...π)((π β β β¦ if(π β β, π, 1))βπ))βπ) = (#pβπ)) |
51 | 50 | oveq1d 7424 |
. . . . . 6
β’ ((π β β β§ π β (2...π)) β (((π β β β¦ βπ β (1...π)((π β β β¦ if(π β β, π, 1))βπ))βπ) + π) = ((#pβπ) + π)) |
52 | 51 | oveq1d 7424 |
. . . . 5
β’ ((π β β β§ π β (2...π)) β ((((π β β β¦ βπ β (1...π)((π β β β¦ if(π β β, π, 1))βπ))βπ) + π) gcd π) = (((#pβπ) + π) gcd π)) |
53 | 23, 52 | breqtrrd 5177 |
. . . 4
β’ ((π β β β§ π β (2...π)) β 1 < ((((π β β β¦ βπ β (1...π)((π β β β¦ if(π β β, π, 1))βπ))βπ) + π) gcd π)) |
54 | 53 | ralrimiva 3147 |
. . 3
β’ (π β β β
βπ β (2...π)1 < ((((π β β β¦ βπ β (1...π)((π β β β¦ if(π β β, π, 1))βπ))βπ) + π) gcd π)) |
55 | 1, 22, 54 | prmgaplem8 16991 |
. 2
β’ (π β β β
βπ β β
βπ β β
(π β€ (π β π) β§ βπ§ β ((π + 1)..^π)π§ β β)) |
56 | 55 | rgen 3064 |
1
β’
βπ β
β βπ β
β βπ β
β (π β€ (π β π) β§ βπ§ β ((π + 1)..^π)π§ β β) |