| Step | Hyp | Ref
| Expression |
|---|
| 1 | | nnex 12183 |
. . . . 5
β’ β
β V |
| 2 | 1, 1 | xpex 7707 |
. . . 4
β’ (β
Γ β) β V |
| 3 | | opabssxp 5744 |
. . . 4
β’
{β¨π¦, π§β© β£ ((π¦ β β β§ π§ β β) β§ (((π¦β2) β (π· Β· (π§β2))) β 0 β§ (absβ((π¦β2) β (π· Β· (π§β2)))) < (1 + (2 Β·
(ββπ·)))))}
β (β Γ β) |
| 4 | | ssdomg 8962 |
. . . 4
β’ ((β
Γ β) β V β ({β¨π¦, π§β© β£ ((π¦ β β β§ π§ β β) β§ (((π¦β2) β (π· Β· (π§β2))) β 0 β§ (absβ((π¦β2) β (π· Β· (π§β2)))) < (1 + (2 Β·
(ββπ·)))))}
β (β Γ β) β {β¨π¦, π§β© β£ ((π¦ β β β§ π§ β β) β§ (((π¦β2) β (π· Β· (π§β2))) β 0 β§ (absβ((π¦β2) β (π· Β· (π§β2)))) < (1 + (2 Β·
(ββπ·)))))}
βΌ (β Γ β))) |
| 5 | 2, 3, 4 | mp2 9 |
. . 3
β’
{β¨π¦, π§β© β£ ((π¦ β β β§ π§ β β) β§ (((π¦β2) β (π· Β· (π§β2))) β 0 β§ (absβ((π¦β2) β (π· Β· (π§β2)))) < (1 + (2 Β·
(ββπ·)))))}
βΌ (β Γ β) |
| 6 | | xpnnen 16119 |
. . 3
β’ (β
Γ β) β β |
| 7 | | domentr 8975 |
. . 3
β’
(({β¨π¦, π§β© β£ ((π¦ β β β§ π§ β β) β§ (((π¦β2) β (π· Β· (π§β2))) β 0 β§ (absβ((π¦β2) β (π· Β· (π§β2)))) < (1 + (2 Β·
(ββπ·)))))}
βΌ (β Γ β) β§ (β Γ β) β
β) β {β¨π¦,
π§β© β£ ((π¦ β β β§ π§ β β) β§ (((π¦β2) β (π· Β· (π§β2))) β 0 β§ (absβ((π¦β2) β (π· Β· (π§β2)))) < (1 + (2 Β·
(ββπ·)))))}
βΌ β) |
| 8 | 5, 6, 7 | mp2an 690 |
. 2
β’
{β¨π¦, π§β© β£ ((π¦ β β β§ π§ β β) β§ (((π¦β2) β (π· Β· (π§β2))) β 0 β§ (absβ((π¦β2) β (π· Β· (π§β2)))) < (1 + (2 Β·
(ββπ·)))))}
βΌ β |
| 9 | | nnrp 12950 |
. . . . . . 7
β’ (π· β β β π· β
β+) |
| 10 | 9 | rpsqrtcld 15323 |
. . . . . 6
β’ (π· β β β
(ββπ·) β
β+) |
| 11 | 10 | anim1i 615 |
. . . . 5
β’ ((π· β β β§ Β¬
(ββπ·) β
β) β ((ββπ·) β β+ β§ Β¬
(ββπ·) β
β)) |
| 12 | | eldif 3938 |
. . . . 5
β’
((ββπ·)
β (β+ β β) β ((ββπ·) β β+
β§ Β¬ (ββπ·) β β)) |
| 13 | 11, 12 | sylibr 233 |
. . . 4
β’ ((π· β β β§ Β¬
(ββπ·) β
β) β (ββπ·) β (β+ β
β)) |
| 14 | | irrapx1 41242 |
. . . 4
β’
((ββπ·)
β (β+ β β) β {π β β β£ (0 < π β§ (absβ(π β (ββπ·))) < ((denomβπ)β-2))} β
β) |
| 15 | | ensym 8965 |
. . . 4
β’ ({π β β β£ (0 <
π β§ (absβ(π β (ββπ·))) < ((denomβπ)β-2))} β β
β β β {π
β β β£ (0 < π β§ (absβ(π β (ββπ·))) < ((denomβπ)β-2))}) |
| 16 | 13, 14, 15 | 3syl 18 |
. . 3
β’ ((π· β β β§ Β¬
(ββπ·) β
β) β β β {π β β β£ (0 < π β§ (absβ(π β (ββπ·))) < ((denomβπ)β-2))}) |
| 17 | | pellexlem3 41245 |
. . 3
β’ ((π· β β β§ Β¬
(ββπ·) β
β) β {π β
β β£ (0 < π
β§ (absβ(π β
(ββπ·))) <
((denomβπ)β-2))}
βΌ {β¨π¦, π§β© β£ ((π¦ β β β§ π§ β β) β§ (((π¦β2) β (π· Β· (π§β2))) β 0 β§ (absβ((π¦β2) β (π· Β· (π§β2)))) < (1 + (2 Β·
(ββπ·)))))}) |
| 18 | | endomtr 8974 |
. . 3
β’ ((β
β {π β β
β£ (0 < π β§
(absβ(π β
(ββπ·))) <
((denomβπ)β-2))}
β§ {π β β
β£ (0 < π β§
(absβ(π β
(ββπ·))) <
((denomβπ)β-2))}
βΌ {β¨π¦, π§β© β£ ((π¦ β β β§ π§ β β) β§ (((π¦β2) β (π· Β· (π§β2))) β 0 β§ (absβ((π¦β2) β (π· Β· (π§β2)))) < (1 + (2 Β·
(ββπ·)))))})
β β βΌ {β¨π¦, π§β© β£ ((π¦ β β β§ π§ β β) β§ (((π¦β2) β (π· Β· (π§β2))) β 0 β§ (absβ((π¦β2) β (π· Β· (π§β2)))) < (1 + (2 Β·
(ββπ·)))))}) |
| 19 | 16, 17, 18 | syl2anc 584 |
. 2
β’ ((π· β β β§ Β¬
(ββπ·) β
β) β β βΌ {β¨π¦, π§β© β£ ((π¦ β β β§ π§ β β) β§ (((π¦β2) β (π· Β· (π§β2))) β 0 β§ (absβ((π¦β2) β (π· Β· (π§β2)))) < (1 + (2 Β·
(ββπ·)))))}) |
| 20 | | sbth 9059 |
. 2
β’
(({β¨π¦, π§β© β£ ((π¦ β β β§ π§ β β) β§ (((π¦β2) β (π· Β· (π§β2))) β 0 β§ (absβ((π¦β2) β (π· Β· (π§β2)))) < (1 + (2 Β·
(ββπ·)))))}
βΌ β β§ β βΌ {β¨π¦, π§β© β£ ((π¦ β β β§ π§ β β) β§ (((π¦β2) β (π· Β· (π§β2))) β 0 β§ (absβ((π¦β2) β (π· Β· (π§β2)))) < (1 + (2 Β·
(ββπ·)))))})
β {β¨π¦, π§β© β£ ((π¦ β β β§ π§ β β) β§ (((π¦β2) β (π· Β· (π§β2))) β 0 β§ (absβ((π¦β2) β (π· Β· (π§β2)))) < (1 + (2 Β·
(ββπ·)))))}
β β) |
| 21 | 8, 19, 20 | sylancr 587 |
1
β’ ((π· β β β§ Β¬
(ββπ·) β
β) β {β¨π¦,
π§β© β£ ((π¦ β β β§ π§ β β) β§ (((π¦β2) β (π· Β· (π§β2))) β 0 β§ (absβ((π¦β2) β (π· Β· (π§β2)))) < (1 + (2 Β·
(ββπ·)))))}
β β) |
