Step | Hyp | Ref
| Expression |
1 | | qredeu 16541 |
. . 3
β’ (π΄ β β β
β!π β (β€
Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) |
2 | | riotacl 7336 |
. . 3
β’
(β!π β
(β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ))) β (β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) β (β€ Γ
β)) |
3 | 1, 2 | syl 17 |
. 2
β’ (π΄ β β β
(β©π β
(β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) β (β€ Γ
β)) |
4 | | elxp6 7960 |
. . 3
β’
((β©π
β (β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) β (β€ Γ
β) β ((β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) = β¨(1st
β(β©π
β (β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ))))), (2nd
β(β©π
β (β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))))β© β§
((1st β(β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ))))) β β€ β§
(2nd β(β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ))))) β
β))) |
5 | | qnumval 16619 |
. . . . . . 7
β’ (π΄ β β β
(numerβπ΄) =
(1st β(β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))))) |
6 | 5 | eleq1d 2823 |
. . . . . 6
β’ (π΄ β β β
((numerβπ΄) β
β€ β (1st β(β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ))))) β
β€)) |
7 | | qdenval 16620 |
. . . . . . 7
β’ (π΄ β β β
(denomβπ΄) =
(2nd β(β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))))) |
8 | 7 | eleq1d 2823 |
. . . . . 6
β’ (π΄ β β β
((denomβπ΄) β
β β (2nd β(β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ))))) β
β)) |
9 | 6, 8 | anbi12d 632 |
. . . . 5
β’ (π΄ β β β
(((numerβπ΄) β
β€ β§ (denomβπ΄) β β) β ((1st
β(β©π
β (β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ))))) β β€ β§
(2nd β(β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ))))) β
β))) |
10 | 9 | biimprd 248 |
. . . 4
β’ (π΄ β β β
(((1st β(β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ))))) β β€ β§
(2nd β(β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ))))) β β) β
((numerβπ΄) β
β€ β§ (denomβπ΄) β β))) |
11 | 10 | adantld 492 |
. . 3
β’ (π΄ β β β
(((β©π β
(β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) = β¨(1st
β(β©π
β (β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ))))), (2nd
β(β©π
β (β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))))β© β§
((1st β(β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ))))) β β€ β§
(2nd β(β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ))))) β β)) β
((numerβπ΄) β
β€ β§ (denomβπ΄) β β))) |
12 | 4, 11 | biimtrid 241 |
. 2
β’ (π΄ β β β
((β©π β
(β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) β (β€ Γ
β) β ((numerβπ΄) β β€ β§ (denomβπ΄) β
β))) |
13 | 3, 12 | mpd 15 |
1
β’ (π΄ β β β
((numerβπ΄) β
β€ β§ (denomβπ΄) β β)) |