Step | Hyp | Ref
| Expression |
1 | | 2re 12234 |
. . . . . . . . . . 11
β’ 2 β
β |
2 | 1 | a1i 11 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π΅ β β) β 2 β
β) |
3 | | nnre 12167 |
. . . . . . . . . . . 12
β’ (π΅ β β β π΅ β
β) |
4 | | peano2re 11335 |
. . . . . . . . . . . 12
β’ (π΅ β β β (π΅ + 1) β
β) |
5 | 3, 4 | syl 17 |
. . . . . . . . . . 11
β’ (π΅ β β β (π΅ + 1) β
β) |
6 | 5 | adantl 483 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π΅ β β) β (π΅ + 1) β β) |
7 | | nnz 12527 |
. . . . . . . . . . . . 13
β’ (π΅ β β β π΅ β
β€) |
8 | 7 | peano2zd 12617 |
. . . . . . . . . . . 12
β’ (π΅ β β β (π΅ + 1) β
β€) |
9 | | frmy 41267 |
. . . . . . . . . . . . 13
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
10 | 9 | fovcl 7489 |
. . . . . . . . . . . 12
β’ ((π΄ β
(β€β₯β2) β§ (π΅ + 1) β β€) β (π΄ Yrm (π΅ + 1)) β
β€) |
11 | 8, 10 | sylan2 594 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ π΅ β β) β (π΄ Yrm (π΅ + 1)) β β€) |
12 | 11 | zred 12614 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π΅ β β) β (π΄ Yrm (π΅ + 1)) β β) |
13 | | elnnuz 12814 |
. . . . . . . . . . . . 13
β’ (π΅ β β β π΅ β
(β€β₯β1)) |
14 | | eluzp1p1 12798 |
. . . . . . . . . . . . . 14
β’ (π΅ β
(β€β₯β1) β (π΅ + 1) β
(β€β₯β(1 + 1))) |
15 | | df-2 12223 |
. . . . . . . . . . . . . . 15
β’ 2 = (1 +
1) |
16 | 15 | fveq2i 6850 |
. . . . . . . . . . . . . 14
β’
(β€β₯β2) = (β€β₯β(1 +
1)) |
17 | 14, 16 | eleqtrrdi 2849 |
. . . . . . . . . . . . 13
β’ (π΅ β
(β€β₯β1) β (π΅ + 1) β
(β€β₯β2)) |
18 | 13, 17 | sylbi 216 |
. . . . . . . . . . . 12
β’ (π΅ β β β (π΅ + 1) β
(β€β₯β2)) |
19 | | eluzle 12783 |
. . . . . . . . . . . 12
β’ ((π΅ + 1) β
(β€β₯β2) β 2 β€ (π΅ + 1)) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . 11
β’ (π΅ β β β 2 β€
(π΅ + 1)) |
21 | 20 | adantl 483 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π΅ β β) β 2 β€ (π΅ + 1)) |
22 | | nnnn0 12427 |
. . . . . . . . . . . 12
β’ (π΅ β β β π΅ β
β0) |
23 | | peano2nn0 12460 |
. . . . . . . . . . . 12
β’ (π΅ β β0
β (π΅ + 1) β
β0) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . 11
β’ (π΅ β β β (π΅ + 1) β
β0) |
25 | | rmygeid 41317 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ (π΅ + 1) β β0) β
(π΅ + 1) β€ (π΄ Yrm (π΅ + 1))) |
26 | 24, 25 | sylan2 594 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π΅ β β) β (π΅ + 1) β€ (π΄ Yrm (π΅ + 1))) |
27 | 2, 6, 12, 21, 26 | letrd 11319 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π΅ β β) β 2 β€ (π΄ Yrm (π΅ + 1))) |
28 | | 2z 12542 |
. . . . . . . . . 10
β’ 2 β
β€ |
29 | | eluz 12784 |
. . . . . . . . . 10
β’ ((2
β β€ β§ (π΄
Yrm (π΅ + 1))
β β€) β ((π΄
Yrm (π΅ + 1))
β (β€β₯β2) β 2 β€ (π΄ Yrm (π΅ + 1)))) |
30 | 28, 11, 29 | sylancr 588 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π΅ β β) β ((π΄ Yrm (π΅ + 1)) β
(β€β₯β2) β 2 β€ (π΄ Yrm (π΅ + 1)))) |
31 | 27, 30 | mpbird 257 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π΅ β β) β (π΄ Yrm (π΅ + 1)) β
(β€β₯β2)) |
32 | 31 | adantl 483 |
. . . . . . 7
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β (π΄ Yrm (π΅ + 1)) β
(β€β₯β2)) |
33 | | simprl 770 |
. . . . . . 7
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β π΄ β
(β€β₯β2)) |
34 | | simprr 772 |
. . . . . . 7
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β π΅ β β) |
35 | 12 | leidd 11728 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π΅ β β) β (π΄ Yrm (π΅ + 1)) β€ (π΄ Yrm (π΅ + 1))) |
36 | 35 | adantl 483 |
. . . . . . 7
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β (π΄ Yrm (π΅ + 1)) β€ (π΄ Yrm (π΅ + 1))) |
37 | | jm3.1 41373 |
. . . . . . 7
β’ ((((π΄ Yrm (π΅ + 1)) β
(β€β₯β2) β§ π΄ β (β€β₯β2)
β§ π΅ β β)
β§ (π΄ Yrm
(π΅ + 1)) β€ (π΄ Yrm (π΅ + 1))) β (π΄βπ΅) = ((((π΄ Yrm (π΅ + 1)) Xrm π΅) β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) mod ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1))) |
38 | 32, 33, 34, 36, 37 | syl31anc 1374 |
. . . . . 6
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β (π΄βπ΅) = ((((π΄ Yrm (π΅ + 1)) Xrm π΅) β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) mod ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1))) |
39 | 38 | eqeq2d 2748 |
. . . . 5
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β (πΆ = (π΄βπ΅) β πΆ = ((((π΄ Yrm (π΅ + 1)) Xrm π΅) β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) mod ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1)))) |
40 | 7 | adantl 483 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π΅ β β) β π΅ β β€) |
41 | | frmx 41266 |
. . . . . . . . . . 11
β’
Xrm :((β€β₯β2) Γ
β€)βΆβ0 |
42 | 41 | fovcl 7489 |
. . . . . . . . . 10
β’ (((π΄ Yrm (π΅ + 1)) β
(β€β₯β2) β§ π΅ β β€) β ((π΄ Yrm (π΅ + 1)) Xrm π΅) β
β0) |
43 | 31, 40, 42 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π΅ β β) β ((π΄ Yrm (π΅ + 1)) Xrm π΅) β
β0) |
44 | 43 | nn0zd 12532 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π΅ β β) β ((π΄ Yrm (π΅ + 1)) Xrm π΅) β β€) |
45 | | eluzelz 12780 |
. . . . . . . . . . 11
β’ (π΄ β
(β€β₯β2) β π΄ β β€) |
46 | 45 | adantr 482 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π΅ β β) β π΄ β β€) |
47 | 11, 46 | zsubcld 12619 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π΅ β β) β ((π΄ Yrm (π΅ + 1)) β π΄) β β€) |
48 | 9 | fovcl 7489 |
. . . . . . . . . 10
β’ (((π΄ Yrm (π΅ + 1)) β
(β€β₯β2) β§ π΅ β β€) β ((π΄ Yrm (π΅ + 1)) Yrm π΅) β β€) |
49 | 31, 40, 48 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π΅ β β) β ((π΄ Yrm (π΅ + 1)) Yrm π΅) β β€) |
50 | 47, 49 | zmulcld 12620 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π΅ β β) β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅)) β β€) |
51 | 44, 50 | zsubcld 12619 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π΅ β β) β (((π΄ Yrm (π΅ + 1)) Xrm π΅) β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β β€) |
52 | 51 | adantl 483 |
. . . . . 6
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β (((π΄ Yrm (π΅ + 1)) Xrm π΅) β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β β€) |
53 | 32, 33, 34, 36 | jm3.1lem3 41372 |
. . . . . 6
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β
β) |
54 | | simpl 484 |
. . . . . 6
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β πΆ β
β0) |
55 | | divalgmodcl 16296 |
. . . . . 6
β’
(((((π΄
Yrm (π΅ + 1))
Xrm π΅) β
(((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β β€ β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β β β§
πΆ β
β0) β (πΆ = ((((π΄ Yrm (π΅ + 1)) Xrm π΅) β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) mod ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1)) β (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((((π΄ Yrm (π΅ + 1)) Xrm π΅) β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ)))) |
56 | 52, 53, 54, 55 | syl3anc 1372 |
. . . . 5
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β (πΆ = ((((π΄ Yrm (π΅ + 1)) Xrm π΅) β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) mod ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1)) β (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((((π΄ Yrm (π΅ + 1)) Xrm π΅) β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ)))) |
57 | 39, 56 | bitrd 279 |
. . . 4
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β (πΆ = (π΄βπ΅) β (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((((π΄ Yrm (π΅ + 1)) Xrm π΅) β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ)))) |
58 | | rmynn0 41310 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ (π΅ + 1) β β0) β
(π΄ Yrm (π΅ + 1)) β
β0) |
59 | 24, 58 | sylan2 594 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π΅ β β) β (π΄ Yrm (π΅ + 1)) β
β0) |
60 | 59 | adantl 483 |
. . . . . . . 8
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β (π΄ Yrm (π΅ + 1)) β
β0) |
61 | | oveq1 7369 |
. . . . . . . . . . . 12
β’ (π = (π΄ Yrm (π΅ + 1)) β (π Yrm π΅) = ((π΄ Yrm (π΅ + 1)) Yrm π΅)) |
62 | 61 | eqeq2d 2748 |
. . . . . . . . . . 11
β’ (π = (π΄ Yrm (π΅ + 1)) β (π = (π Yrm π΅) β π = ((π΄ Yrm (π΅ + 1)) Yrm π΅))) |
63 | | oveq1 7369 |
. . . . . . . . . . . . . 14
β’ (π = (π΄ Yrm (π΅ + 1)) β (π Xrm π΅) = ((π΄ Yrm (π΅ + 1)) Xrm π΅)) |
64 | 63 | eqeq2d 2748 |
. . . . . . . . . . . . 13
β’ (π = (π΄ Yrm (π΅ + 1)) β (π = (π Xrm π΅) β π = ((π΄ Yrm (π΅ + 1)) Xrm π΅))) |
65 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π΄ Yrm (π΅ + 1)) β (2 Β· π) = (2 Β· (π΄ Yrm (π΅ + 1)))) |
66 | 65 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π΄ Yrm (π΅ + 1)) β ((2 Β· π) Β· π΄) = ((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄)) |
67 | 66 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
β’ (π = (π΄ Yrm (π΅ + 1)) β (((2 Β· π) Β· π΄) β (π΄β2)) = (((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2))) |
68 | 67 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
β’ (π = (π΄ Yrm (π΅ + 1)) β ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) = ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1)) |
69 | 68 | breq2d 5122 |
. . . . . . . . . . . . . 14
β’ (π = (π΄ Yrm (π΅ + 1)) β (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1))) |
70 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π΄ Yrm (π΅ + 1)) β (π β π΄) = ((π΄ Yrm (π΅ + 1)) β π΄)) |
71 | 70 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π΄ Yrm (π΅ + 1)) β ((π β π΄) Β· π) = (((π΄ Yrm (π΅ + 1)) β π΄) Β· π)) |
72 | 71 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ (π = (π΄ Yrm (π΅ + 1)) β (π β ((π β π΄) Β· π)) = (π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· π))) |
73 | 72 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
β’ (π = (π΄ Yrm (π΅ + 1)) β ((π β ((π β π΄) Β· π)) β πΆ) = ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· π)) β πΆ)) |
74 | 68, 73 | breq12d 5123 |
. . . . . . . . . . . . . 14
β’ (π = (π΄ Yrm (π΅ + 1)) β (((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ) β ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· π)) β πΆ))) |
75 | 69, 74 | anbi12d 632 |
. . . . . . . . . . . . 13
β’ (π = (π΄ Yrm (π΅ + 1)) β ((πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)) β (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· π)) β πΆ)))) |
76 | 64, 75 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (π = (π΄ Yrm (π΅ + 1)) β ((π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))) β (π = ((π΄ Yrm (π΅ + 1)) Xrm π΅) β§ (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· π)) β πΆ))))) |
77 | 76 | rexbidv 3176 |
. . . . . . . . . . 11
β’ (π = (π΄ Yrm (π΅ + 1)) β (βπ β β0 (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))) β βπ β β0 (π = ((π΄ Yrm (π΅ + 1)) Xrm π΅) β§ (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· π)) β πΆ))))) |
78 | 62, 77 | anbi12d 632 |
. . . . . . . . . 10
β’ (π = (π΄ Yrm (π΅ + 1)) β ((π = (π Yrm π΅) β§ βπ β β0 (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))) β (π = ((π΄ Yrm (π΅ + 1)) Yrm π΅) β§ βπ β β0 (π = ((π΄ Yrm (π΅ + 1)) Xrm π΅) β§ (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· π)) β πΆ)))))) |
79 | 78 | rexbidv 3176 |
. . . . . . . . 9
β’ (π = (π΄ Yrm (π΅ + 1)) β (βπ β β0 (π = (π Yrm π΅) β§ βπ β β0 (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))) β βπ β β0 (π = ((π΄ Yrm (π΅ + 1)) Yrm π΅) β§ βπ β β0 (π = ((π΄ Yrm (π΅ + 1)) Xrm π΅) β§ (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· π)) β πΆ)))))) |
80 | 79 | ceqsrexv 3610 |
. . . . . . . 8
β’ ((π΄ Yrm (π΅ + 1)) β
β0 β (βπ β β0 (π = (π΄ Yrm (π΅ + 1)) β§ βπ β β0 (π = (π Yrm π΅) β§ βπ β β0 (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))) β βπ β β0 (π = ((π΄ Yrm (π΅ + 1)) Yrm π΅) β§ βπ β β0 (π = ((π΄ Yrm (π΅ + 1)) Xrm π΅) β§ (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· π)) β πΆ)))))) |
81 | 60, 80 | syl 17 |
. . . . . . 7
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β (βπ β β0
(π = (π΄ Yrm (π΅ + 1)) β§ βπ β β0 (π = (π Yrm π΅) β§ βπ β β0 (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))) β βπ β β0 (π = ((π΄ Yrm (π΅ + 1)) Yrm π΅) β§ βπ β β0 (π = ((π΄ Yrm (π΅ + 1)) Xrm π΅) β§ (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· π)) β πΆ)))))) |
82 | 22 | ad2antll 728 |
. . . . . . . . 9
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β π΅ β
β0) |
83 | | rmynn0 41310 |
. . . . . . . . 9
β’ (((π΄ Yrm (π΅ + 1)) β
(β€β₯β2) β§ π΅ β β0) β ((π΄ Yrm (π΅ + 1)) Yrm π΅) β
β0) |
84 | 32, 82, 83 | syl2anc 585 |
. . . . . . . 8
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β ((π΄ Yrm (π΅ + 1)) Yrm π΅) β
β0) |
85 | | oveq2 7370 |
. . . . . . . . . . . . . . 15
β’ (π = ((π΄ Yrm (π΅ + 1)) Yrm π΅) β (((π΄ Yrm (π΅ + 1)) β π΄) Β· π) = (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) |
86 | 85 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (π = ((π΄ Yrm (π΅ + 1)) Yrm π΅) β (π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· π)) = (π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅)))) |
87 | 86 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (π = ((π΄ Yrm (π΅ + 1)) Yrm π΅) β ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· π)) β πΆ) = ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ)) |
88 | 87 | breq2d 5122 |
. . . . . . . . . . . 12
β’ (π = ((π΄ Yrm (π΅ + 1)) Yrm π΅) β (((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· π)) β πΆ) β ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ))) |
89 | 88 | anbi2d 630 |
. . . . . . . . . . 11
β’ (π = ((π΄ Yrm (π΅ + 1)) Yrm π΅) β ((πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· π)) β πΆ)) β (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ)))) |
90 | 89 | anbi2d 630 |
. . . . . . . . . 10
β’ (π = ((π΄ Yrm (π΅ + 1)) Yrm π΅) β ((π = ((π΄ Yrm (π΅ + 1)) Xrm π΅) β§ (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· π)) β πΆ))) β (π = ((π΄ Yrm (π΅ + 1)) Xrm π΅) β§ (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ))))) |
91 | 90 | rexbidv 3176 |
. . . . . . . . 9
β’ (π = ((π΄ Yrm (π΅ + 1)) Yrm π΅) β (βπ β β0 (π = ((π΄ Yrm (π΅ + 1)) Xrm π΅) β§ (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· π)) β πΆ))) β βπ β β0 (π = ((π΄ Yrm (π΅ + 1)) Xrm π΅) β§ (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ))))) |
92 | 91 | ceqsrexv 3610 |
. . . . . . . 8
β’ (((π΄ Yrm (π΅ + 1)) Yrm π΅) β β0
β (βπ β
β0 (π =
((π΄ Yrm (π΅ + 1)) Yrm π΅) β§ βπ β β0
(π = ((π΄ Yrm (π΅ + 1)) Xrm π΅) β§ (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· π)) β πΆ)))) β βπ β β0 (π = ((π΄ Yrm (π΅ + 1)) Xrm π΅) β§ (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ))))) |
93 | 84, 92 | syl 17 |
. . . . . . 7
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β (βπ β β0
(π = ((π΄ Yrm (π΅ + 1)) Yrm π΅) β§ βπ β β0 (π = ((π΄ Yrm (π΅ + 1)) Xrm π΅) β§ (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· π)) β πΆ)))) β βπ β β0 (π = ((π΄ Yrm (π΅ + 1)) Xrm π΅) β§ (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ))))) |
94 | 7 | ad2antll 728 |
. . . . . . . . 9
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β π΅ β β€) |
95 | 32, 94, 42 | syl2anc 585 |
. . . . . . . 8
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β ((π΄ Yrm (π΅ + 1)) Xrm π΅) β
β0) |
96 | | oveq1 7369 |
. . . . . . . . . . . 12
β’ (π = ((π΄ Yrm (π΅ + 1)) Xrm π΅) β (π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) = (((π΄ Yrm (π΅ + 1)) Xrm π΅) β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅)))) |
97 | 96 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (π = ((π΄ Yrm (π΅ + 1)) Xrm π΅) β ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ) = ((((π΄ Yrm (π΅ + 1)) Xrm π΅) β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ)) |
98 | 97 | breq2d 5122 |
. . . . . . . . . 10
β’ (π = ((π΄ Yrm (π΅ + 1)) Xrm π΅) β (((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ) β ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((((π΄ Yrm (π΅ + 1)) Xrm π΅) β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ))) |
99 | 98 | anbi2d 630 |
. . . . . . . . 9
β’ (π = ((π΄ Yrm (π΅ + 1)) Xrm π΅) β ((πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ)) β (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((((π΄ Yrm (π΅ + 1)) Xrm π΅) β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ)))) |
100 | 99 | ceqsrexv 3610 |
. . . . . . . 8
β’ (((π΄ Yrm (π΅ + 1)) Xrm π΅) β β0
β (βπ β
β0 (π =
((π΄ Yrm (π΅ + 1)) Xrm π΅) β§ (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ))) β (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((((π΄ Yrm (π΅ + 1)) Xrm π΅) β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ)))) |
101 | 95, 100 | syl 17 |
. . . . . . 7
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β (βπ β β0
(π = ((π΄ Yrm (π΅ + 1)) Xrm π΅) β§ (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((π β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ))) β (πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((((π΄ Yrm (π΅ + 1)) Xrm π΅) β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ)))) |
102 | 81, 93, 101 | 3bitrrd 306 |
. . . . . 6
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β ((πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((((π΄ Yrm (π΅ + 1)) Xrm π΅) β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ)) β βπ β β0 (π = (π΄ Yrm (π΅ + 1)) β§ βπ β β0 (π = (π Yrm π΅) β§ βπ β β0 (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))))) |
103 | | r19.42v 3188 |
. . . . . . . . . 10
β’
(βπ β
β0 (π =
(π΄ Yrm (π΅ + 1)) β§ (π = (π Yrm π΅) β§ (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))) β (π = (π΄ Yrm (π΅ + 1)) β§ βπ β β0 (π = (π Yrm π΅) β§ (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))))) |
104 | | r19.42v 3188 |
. . . . . . . . . . 11
β’
(βπ β
β0 (π =
(π Yrm π΅) β§ (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))) β (π = (π Yrm π΅) β§ βπ β β0 (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))) |
105 | 104 | anbi2i 624 |
. . . . . . . . . 10
β’ ((π = (π΄ Yrm (π΅ + 1)) β§ βπ β β0 (π = (π Yrm π΅) β§ (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))) β (π = (π΄ Yrm (π΅ + 1)) β§ (π = (π Yrm π΅) β§ βπ β β0 (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))))) |
106 | 103, 105 | bitri 275 |
. . . . . . . . 9
β’
(βπ β
β0 (π =
(π΄ Yrm (π΅ + 1)) β§ (π = (π Yrm π΅) β§ (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))) β (π = (π΄ Yrm (π΅ + 1)) β§ (π = (π Yrm π΅) β§ βπ β β0 (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))))) |
107 | 106 | rexbii 3098 |
. . . . . . . 8
β’
(βπ β
β0 βπ β β0 (π = (π΄ Yrm (π΅ + 1)) β§ (π = (π Yrm π΅) β§ (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))) β βπ β β0 (π = (π΄ Yrm (π΅ + 1)) β§ (π = (π Yrm π΅) β§ βπ β β0 (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))))) |
108 | | r19.42v 3188 |
. . . . . . . 8
β’
(βπ β
β0 (π =
(π΄ Yrm (π΅ + 1)) β§ (π = (π Yrm π΅) β§ βπ β β0 (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))) β (π = (π΄ Yrm (π΅ + 1)) β§ βπ β β0 (π = (π Yrm π΅) β§ βπ β β0 (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))))) |
109 | 107, 108 | bitri 275 |
. . . . . . 7
β’
(βπ β
β0 βπ β β0 (π = (π΄ Yrm (π΅ + 1)) β§ (π = (π Yrm π΅) β§ (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))) β (π = (π΄ Yrm (π΅ + 1)) β§ βπ β β0 (π = (π Yrm π΅) β§ βπ β β0 (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))))) |
110 | 109 | rexbii 3098 |
. . . . . 6
β’
(βπ β
β0 βπ β β0 βπ β β0
(π = (π΄ Yrm (π΅ + 1)) β§ (π = (π Yrm π΅) β§ (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))) β βπ β β0 (π = (π΄ Yrm (π΅ + 1)) β§ βπ β β0 (π = (π Yrm π΅) β§ βπ β β0 (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))))) |
111 | 102, 110 | bitr4di 289 |
. . . . 5
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β ((πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((((π΄ Yrm (π΅ + 1)) Xrm π΅) β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ)) β βπ β β0 βπ β β0
βπ β
β0 (π =
(π΄ Yrm (π΅ + 1)) β§ (π = (π Yrm π΅) β§ (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))))) |
112 | | eleq1 2826 |
. . . . . . . . . . . 12
β’ (π = (π΄ Yrm (π΅ + 1)) β (π β (β€β₯β2)
β (π΄ Yrm
(π΅ + 1)) β
(β€β₯β2))) |
113 | 32, 112 | syl5ibrcom 247 |
. . . . . . . . . . 11
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β (π = (π΄ Yrm (π΅ + 1)) β π β
(β€β₯β2))) |
114 | 113 | imp 408 |
. . . . . . . . . 10
β’ (((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β§ π = (π΄ Yrm (π΅ + 1))) β π β
(β€β₯β2)) |
115 | | ibar 530 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β2) β (π = (π Yrm π΅) β (π β (β€β₯β2)
β§ π = (π Yrm π΅)))) |
116 | | ibar 530 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β2) β (π = (π Xrm π΅) β (π β (β€β₯β2)
β§ π = (π Xrm π΅)))) |
117 | 116 | anbi1d 631 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β2) β ((π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))) β ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))) |
118 | 115, 117 | anbi12d 632 |
. . . . . . . . . 10
β’ (π β
(β€β₯β2) β ((π = (π Yrm π΅) β§ (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))) β ((π β (β€β₯β2)
β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))))) |
119 | 114, 118 | syl 17 |
. . . . . . . . 9
β’ (((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β§ π = (π΄ Yrm (π΅ + 1))) β ((π = (π Yrm π΅) β§ (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))) β ((π β (β€β₯β2)
β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))))) |
120 | 119 | pm5.32da 580 |
. . . . . . . 8
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β ((π = (π΄ Yrm (π΅ + 1)) β§ (π = (π Yrm π΅) β§ (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))) β (π = (π΄ Yrm (π΅ + 1)) β§ ((π β (β€β₯β2)
β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))))) |
121 | | ibar 530 |
. . . . . . . . . 10
β’ (π΄ β
(β€β₯β2) β (π = (π΄ Yrm (π΅ + 1)) β (π΄ β (β€β₯β2)
β§ π = (π΄ Yrm (π΅ + 1))))) |
122 | 121 | ad2antrl 727 |
. . . . . . . . 9
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β (π = (π΄ Yrm (π΅ + 1)) β (π΄ β (β€β₯β2)
β§ π = (π΄ Yrm (π΅ + 1))))) |
123 | 122 | anbi1d 631 |
. . . . . . . 8
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β ((π = (π΄ Yrm (π΅ + 1)) β§ ((π β (β€β₯β2)
β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))) β ((π΄ β (β€β₯β2)
β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β
(β€β₯β2) β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))))) |
124 | 120, 123 | bitrd 279 |
. . . . . . 7
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β ((π = (π΄ Yrm (π΅ + 1)) β§ (π = (π Yrm π΅) β§ (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))) β ((π΄ β (β€β₯β2)
β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β
(β€β₯β2) β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))))) |
125 | 124 | rexbidv 3176 |
. . . . . 6
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β (βπ β β0
(π = (π΄ Yrm (π΅ + 1)) β§ (π = (π Yrm π΅) β§ (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))) β βπ β β0 ((π΄ β
(β€β₯β2) β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))))) |
126 | 125 | 2rexbidv 3214 |
. . . . 5
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β (βπ β β0
βπ β
β0 βπ β β0 (π = (π΄ Yrm (π΅ + 1)) β§ (π = (π Yrm π΅) β§ (π = (π Xrm π΅) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))) β βπ β β0 βπ β β0
βπ β
β0 ((π΄
β (β€β₯β2) β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))))) |
127 | 111, 126 | bitrd 279 |
. . . 4
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β ((πΆ < ((((2 Β· (π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
(π΄ Yrm (π΅ + 1))) Β· π΄) β (π΄β2)) β 1) β₯ ((((π΄ Yrm (π΅ + 1)) Xrm π΅) β (((π΄ Yrm (π΅ + 1)) β π΄) Β· ((π΄ Yrm (π΅ + 1)) Yrm π΅))) β πΆ)) β βπ β β0 βπ β β0
βπ β
β0 ((π΄
β (β€β₯β2) β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))))) |
128 | 57, 127 | bitrd 279 |
. . 3
β’ ((πΆ β β0
β§ (π΄ β
(β€β₯β2) β§ π΅ β β)) β (πΆ = (π΄βπ΅) β βπ β β0 βπ β β0
βπ β
β0 ((π΄
β (β€β₯β2) β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))))) |
129 | 128 | pm5.32da 580 |
. 2
β’ (πΆ β β0
β (((π΄ β
(β€β₯β2) β§ π΅ β β) β§ πΆ = (π΄βπ΅)) β ((π΄ β (β€β₯β2)
β§ π΅ β β)
β§ βπ β
β0 βπ β β0 βπ β β0
((π΄ β
(β€β₯β2) β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))))))) |
130 | | r19.42v 3188 |
. . . 4
β’
(βπ β
β0 ((π΄
β (β€β₯β2) β§ π΅ β β) β§ ((π΄ β (β€β₯β2)
β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β
(β€β₯β2) β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))))) β ((π΄ β (β€β₯β2)
β§ π΅ β β)
β§ βπ β
β0 ((π΄
β (β€β₯β2) β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))))) |
131 | 130 | 2rexbii 3129 |
. . 3
β’
(βπ β
β0 βπ β β0 βπ β β0
((π΄ β
(β€β₯β2) β§ π΅ β β) β§ ((π΄ β (β€β₯β2)
β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β
(β€β₯β2) β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))))) β βπ β β0 βπ β β0
((π΄ β
(β€β₯β2) β§ π΅ β β) β§ βπ β β0
((π΄ β
(β€β₯β2) β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))))) |
132 | | r19.42v 3188 |
. . . . 5
β’
(βπ β
β0 ((π΄
β (β€β₯β2) β§ π΅ β β) β§ βπ β β0
((π΄ β
(β€β₯β2) β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))))) β ((π΄ β (β€β₯β2)
β§ π΅ β β)
β§ βπ β
β0 βπ β β0 ((π΄ β
(β€β₯β2) β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))))) |
133 | 132 | rexbii 3098 |
. . . 4
β’
(βπ β
β0 βπ β β0 ((π΄ β
(β€β₯β2) β§ π΅ β β) β§ βπ β β0
((π΄ β
(β€β₯β2) β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))))) β βπ β β0 ((π΄ β
(β€β₯β2) β§ π΅ β β) β§ βπ β β0
βπ β
β0 ((π΄
β (β€β₯β2) β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))))) |
134 | | r19.42v 3188 |
. . . 4
β’
(βπ β
β0 ((π΄
β (β€β₯β2) β§ π΅ β β) β§ βπ β β0
βπ β
β0 ((π΄
β (β€β₯β2) β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))))) β ((π΄ β (β€β₯β2)
β§ π΅ β β)
β§ βπ β
β0 βπ β β0 βπ β β0
((π΄ β
(β€β₯β2) β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))))) |
135 | 133, 134 | bitri 275 |
. . 3
β’
(βπ β
β0 βπ β β0 ((π΄ β
(β€β₯β2) β§ π΅ β β) β§ βπ β β0
((π΄ β
(β€β₯β2) β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))))) β ((π΄ β (β€β₯β2)
β§ π΅ β β)
β§ βπ β
β0 βπ β β0 βπ β β0
((π΄ β
(β€β₯β2) β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))))) |
136 | 131, 135 | bitri 275 |
. 2
β’
(βπ β
β0 βπ β β0 βπ β β0
((π΄ β
(β€β₯β2) β§ π΅ β β) β§ ((π΄ β (β€β₯β2)
β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β
(β€β₯β2) β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))))) β ((π΄ β (β€β₯β2)
β§ π΅ β β)
β§ βπ β
β0 βπ β β0 βπ β β0
((π΄ β
(β€β₯β2) β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β (β€β₯β2)
β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ))))))) |
137 | 129, 136 | bitr4di 289 |
1
β’ (πΆ β β0
β (((π΄ β
(β€β₯β2) β§ π΅ β β) β§ πΆ = (π΄βπ΅)) β βπ β β0 βπ β β0
βπ β
β0 ((π΄
β (β€β₯β2) β§ π΅ β β) β§ ((π΄ β (β€β₯β2)
β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β
(β€β₯β2) β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2)
β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β·
π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))))))) |