Step | Hyp | Ref
| Expression |
1 | | opelxpi 4660 |
. . . 4
β’ ((π΅ β β€ β§ πΆ β β) β
β¨π΅, πΆβ© β (β€ Γ
β)) |
2 | 1 | 3adant1 1015 |
. . 3
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
β¨π΅, πΆβ© β (β€ Γ
β)) |
3 | | qredeu 12099 |
. . . 4
β’ (π΄ β β β
β!π β (β€
Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) |
4 | 3 | 3ad2ant1 1018 |
. . 3
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
β!π β (β€
Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) |
5 | | fveq2 5517 |
. . . . . . 7
β’ (π = β¨π΅, πΆβ© β (1st βπ) = (1st
ββ¨π΅, πΆβ©)) |
6 | | fveq2 5517 |
. . . . . . 7
β’ (π = β¨π΅, πΆβ© β (2nd βπ) = (2nd
ββ¨π΅, πΆβ©)) |
7 | 5, 6 | oveq12d 5895 |
. . . . . 6
β’ (π = β¨π΅, πΆβ© β ((1st βπ) gcd (2nd
βπ)) =
((1st ββ¨π΅, πΆβ©) gcd (2nd
ββ¨π΅, πΆβ©))) |
8 | 7 | eqeq1d 2186 |
. . . . 5
β’ (π = β¨π΅, πΆβ© β (((1st βπ) gcd (2nd
βπ)) = 1 β
((1st ββ¨π΅, πΆβ©) gcd (2nd
ββ¨π΅, πΆβ©)) = 1)) |
9 | 5, 6 | oveq12d 5895 |
. . . . . 6
β’ (π = β¨π΅, πΆβ© β ((1st βπ) / (2nd βπ)) = ((1st
ββ¨π΅, πΆβ©) / (2nd
ββ¨π΅, πΆβ©))) |
10 | 9 | eqeq2d 2189 |
. . . . 5
β’ (π = β¨π΅, πΆβ© β (π΄ = ((1st βπ) / (2nd βπ)) β π΄ = ((1st ββ¨π΅, πΆβ©) / (2nd ββ¨π΅, πΆβ©)))) |
11 | 8, 10 | anbi12d 473 |
. . . 4
β’ (π = β¨π΅, πΆβ© β ((((1st
βπ) gcd
(2nd βπ))
= 1 β§ π΄ =
((1st βπ)
/ (2nd βπ))) β (((1st
ββ¨π΅, πΆβ©) gcd (2nd
ββ¨π΅, πΆβ©)) = 1 β§ π΄ = ((1st
ββ¨π΅, πΆβ©) / (2nd
ββ¨π΅, πΆβ©))))) |
12 | 11 | riota2 5855 |
. . 3
β’
((β¨π΅, πΆβ© β (β€ Γ
β) β§ β!π
β (β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) β ((((1st
ββ¨π΅, πΆβ©) gcd (2nd
ββ¨π΅, πΆβ©)) = 1 β§ π΄ = ((1st
ββ¨π΅, πΆβ©) / (2nd
ββ¨π΅, πΆβ©))) β
(β©π β
(β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) = β¨π΅, πΆβ©)) |
13 | 2, 4, 12 | syl2anc 411 |
. 2
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
((((1st ββ¨π΅, πΆβ©) gcd (2nd
ββ¨π΅, πΆβ©)) = 1 β§ π΄ = ((1st
ββ¨π΅, πΆβ©) / (2nd
ββ¨π΅, πΆβ©))) β
(β©π β
(β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) = β¨π΅, πΆβ©)) |
14 | | op1stg 6153 |
. . . . . 6
β’ ((π΅ β β€ β§ πΆ β β) β
(1st ββ¨π΅, πΆβ©) = π΅) |
15 | | op2ndg 6154 |
. . . . . 6
β’ ((π΅ β β€ β§ πΆ β β) β
(2nd ββ¨π΅, πΆβ©) = πΆ) |
16 | 14, 15 | oveq12d 5895 |
. . . . 5
β’ ((π΅ β β€ β§ πΆ β β) β
((1st ββ¨π΅, πΆβ©) gcd (2nd
ββ¨π΅, πΆβ©)) = (π΅ gcd πΆ)) |
17 | 16 | 3adant1 1015 |
. . . 4
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
((1st ββ¨π΅, πΆβ©) gcd (2nd
ββ¨π΅, πΆβ©)) = (π΅ gcd πΆ)) |
18 | 17 | eqeq1d 2186 |
. . 3
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
(((1st ββ¨π΅, πΆβ©) gcd (2nd
ββ¨π΅, πΆβ©)) = 1 β (π΅ gcd πΆ) = 1)) |
19 | 14 | 3adant1 1015 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
(1st ββ¨π΅, πΆβ©) = π΅) |
20 | 15 | 3adant1 1015 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
(2nd ββ¨π΅, πΆβ©) = πΆ) |
21 | 19, 20 | oveq12d 5895 |
. . . 4
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
((1st ββ¨π΅, πΆβ©) / (2nd ββ¨π΅, πΆβ©)) = (π΅ / πΆ)) |
22 | 21 | eqeq2d 2189 |
. . 3
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β (π΄ = ((1st
ββ¨π΅, πΆβ©) / (2nd
ββ¨π΅, πΆβ©)) β π΄ = (π΅ / πΆ))) |
23 | 18, 22 | anbi12d 473 |
. 2
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
((((1st ββ¨π΅, πΆβ©) gcd (2nd
ββ¨π΅, πΆβ©)) = 1 β§ π΄ = ((1st
ββ¨π΅, πΆβ©) / (2nd
ββ¨π΅, πΆβ©))) β ((π΅ gcd πΆ) = 1 β§ π΄ = (π΅ / πΆ)))) |
24 | | riotacl 5847 |
. . . . . . 7
β’
(β!π β
(β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ))) β (β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) β (β€ Γ
β)) |
25 | | 1st2nd2 6178 |
. . . . . . 7
β’
((β©π
β (β€ Γ β)(((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 βπ)))))β©) |
26 | 3, 24, 25 | 3syl 17 |
. . . . . 6
β’ (π΄ β β β
(β©π β
(β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) = β¨(1st
β(β©π
β (β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ))))), (2nd
β(β©π
β (β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))))β©) |
27 | | qnumval 12187 |
. . . . . . 7
β’ (π΄ β β β
(numerβπ΄) =
(1st β(β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))))) |
28 | | qdenval 12188 |
. . . . . . 7
β’ (π΄ β β β
(denomβπ΄) =
(2nd β(β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))))) |
29 | 27, 28 | opeq12d 3788 |
. . . . . 6
β’ (π΄ β β β
β¨(numerβπ΄),
(denomβπ΄)β© =
β¨(1st β(β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ))))), (2nd
β(β©π
β (β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))))β©) |
30 | 26, 29 | eqtr4d 2213 |
. . . . 5
β’ (π΄ β β β
(β©π β
(β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) = β¨(numerβπ΄), (denomβπ΄)β©) |
31 | 30 | eqeq1d 2186 |
. . . 4
β’ (π΄ β β β
((β©π β
(β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) = β¨π΅, πΆβ© β β¨(numerβπ΄), (denomβπ΄)β© = β¨π΅, πΆβ©)) |
32 | 31 | 3ad2ant1 1018 |
. . 3
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
((β©π β
(β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) = β¨π΅, πΆβ© β β¨(numerβπ΄), (denomβπ΄)β© = β¨π΅, πΆβ©)) |
33 | | qnumcl 12190 |
. . . . 5
β’ (π΄ β β β
(numerβπ΄) β
β€) |
34 | | qdencl 12191 |
. . . . 5
β’ (π΄ β β β
(denomβπ΄) β
β) |
35 | | opthg 4240 |
. . . . 5
β’
(((numerβπ΄)
β β€ β§ (denomβπ΄) β β) β
(β¨(numerβπ΄),
(denomβπ΄)β© =
β¨π΅, πΆβ© β ((numerβπ΄) = π΅ β§ (denomβπ΄) = πΆ))) |
36 | 33, 34, 35 | syl2anc 411 |
. . . 4
β’ (π΄ β β β
(β¨(numerβπ΄),
(denomβπ΄)β© =
β¨π΅, πΆβ© β ((numerβπ΄) = π΅ β§ (denomβπ΄) = πΆ))) |
37 | 36 | 3ad2ant1 1018 |
. . 3
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
(β¨(numerβπ΄),
(denomβπ΄)β© =
β¨π΅, πΆβ© β ((numerβπ΄) = π΅ β§ (denomβπ΄) = πΆ))) |
38 | 32, 37 | bitrd 188 |
. 2
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
((β©π β
(β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) = β¨π΅, πΆβ© β ((numerβπ΄) = π΅ β§ (denomβπ΄) = πΆ))) |
39 | 13, 23, 38 | 3bitr3d 218 |
1
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β (((π΅ gcd πΆ) = 1 β§ π΄ = (π΅ / πΆ)) β ((numerβπ΄) = π΅ β§ (denomβπ΄) = πΆ))) |