Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β§ (πΎ Yrm
(π + 1)) β€ π΄) β π΄ β
(β€β₯β2)) |
2 | | simpl2 1193 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β§ (πΎ Yrm
(π + 1)) β€ π΄) β πΎ β
(β€β₯β2)) |
3 | | simpl3 1194 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β§ (πΎ Yrm
(π + 1)) β€ π΄) β π β β) |
4 | | simpr 486 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β§ (πΎ Yrm
(π + 1)) β€ π΄) β (πΎ Yrm (π + 1)) β€ π΄) |
5 | 1, 2, 3, 4 | jm3.1lem2 41385 |
. 2
β’ (((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β§ (πΎ Yrm
(π + 1)) β€ π΄) β (πΎβπ) < ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1)) |
6 | | eluzge2nn0 12817 |
. . . . 5
β’ (πΎ β
(β€β₯β2) β πΎ β
β0) |
7 | 6 | 3ad2ant2 1135 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β πΎ β
β0) |
8 | 7 | adantr 482 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β§ (πΎ Yrm
(π + 1)) β€ π΄) β πΎ β
β0) |
9 | 3 | nnnn0d 12478 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β§ (πΎ Yrm
(π + 1)) β€ π΄) β π β
β0) |
10 | | jm2.18 41355 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β0 β§ π β β0)
β ((((2 Β· π΄)
Β· πΎ) β (πΎβ2)) β 1) β₯
(((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))) |
11 | 1, 8, 9, 10 | syl3anc 1372 |
. 2
β’ (((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β§ (πΎ Yrm
(π + 1)) β€ π΄) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))) |
12 | | simp1 1137 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β π΄ β
(β€β₯β2)) |
13 | | nnz 12525 |
. . . . . . . 8
β’ (π β β β π β
β€) |
14 | 13 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β π β
β€) |
15 | | frmx 41280 |
. . . . . . . 8
β’
Xrm :((β€β₯β2) Γ
β€)βΆβ0 |
16 | 15 | fovcl 7485 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β
β0) |
17 | 12, 14, 16 | syl2anc 585 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β (π΄ Xrm
π) β
β0) |
18 | 17 | nn0zd 12530 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β (π΄ Xrm
π) β
β€) |
19 | | eluzelz 12778 |
. . . . . . . 8
β’ (π΄ β
(β€β₯β2) β π΄ β β€) |
20 | | eluzelz 12778 |
. . . . . . . 8
β’ (πΎ β
(β€β₯β2) β πΎ β β€) |
21 | | zsubcl 12550 |
. . . . . . . 8
β’ ((π΄ β β€ β§ πΎ β β€) β (π΄ β πΎ) β β€) |
22 | 19, 20, 21 | syl2an 597 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2))
β (π΄ β πΎ) β
β€) |
23 | 22 | 3adant3 1133 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β (π΄ β πΎ) β
β€) |
24 | | frmy 41281 |
. . . . . . . 8
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
25 | 24 | fovcl 7485 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
26 | 12, 14, 25 | syl2anc 585 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β (π΄ Yrm
π) β
β€) |
27 | 23, 26 | zmulcld 12618 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β ((π΄ β πΎ) Β· (π΄ Yrm π)) β β€) |
28 | 18, 27 | zsubcld 12617 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β ((π΄ Xrm
π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β β€) |
29 | 28 | adantr 482 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β§ (πΎ Yrm
(π + 1)) β€ π΄) β ((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β β€) |
30 | 1, 2, 3, 4 | jm3.1lem3 41386 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β§ (πΎ Yrm
(π + 1)) β€ π΄) β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β
β) |
31 | | nnnn0 12425 |
. . . . . 6
β’ (π β β β π β
β0) |
32 | 31 | 3ad2ant3 1136 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β π β
β0) |
33 | 7, 32 | nn0expcld 14155 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β (πΎβπ) β
β0) |
34 | 33 | adantr 482 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β§ (πΎ Yrm
(π + 1)) β€ π΄) β (πΎβπ) β
β0) |
35 | | divalgmodcl 16294 |
. . 3
β’ ((((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β β€ β§ ((((2 Β·
π΄) Β· πΎ) β (πΎβ2)) β 1) β β β§
(πΎβπ) β β0) β ((πΎβπ) = (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) mod ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1)) β ((πΎβπ) < ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β§ ((((2 Β·
π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))))) |
36 | 29, 30, 34, 35 | syl3anc 1372 |
. 2
β’ (((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β§ (πΎ Yrm
(π + 1)) β€ π΄) β ((πΎβπ) = (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) mod ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1)) β ((πΎβπ) < ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β§ ((((2 Β·
π΄) Β· πΎ) β (πΎβ2)) β 1) β₯ (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) β (πΎβπ))))) |
37 | 5, 11, 36 | mpbir2and 712 |
1
β’ (((π΄ β
(β€β₯β2) β§ πΎ β (β€β₯β2)
β§ π β β)
β§ (πΎ Yrm
(π + 1)) β€ π΄) β (πΎβπ) = (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) mod ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1))) |