Step | Hyp | Ref
| Expression |
1 | | qredeu 16591 |
. . . . . . 7
β’ (π΄ β β β
β!π β (β€
Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) |
2 | | riotacl 7379 |
. . . . . . 7
β’
(β!π β
(β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ))) β (β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) β (β€ Γ
β)) |
3 | | 1st2nd2 8010 |
. . . . . . 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 βπ)))))β©) |
4 | 1, 2, 3 | 3syl 18 |
. . . . . 6
β’ (π΄ β β β
(β©π β
(β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) = β¨(1st
β(β©π
β (β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ))))), (2nd
β(β©π
β (β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))))β©) |
5 | | qnumval 16669 |
. . . . . . 7
β’ (π΄ β β β
(numerβπ΄) =
(1st β(β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))))) |
6 | | qdenval 16670 |
. . . . . . 7
β’ (π΄ β β β
(denomβπ΄) =
(2nd β(β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))))) |
7 | 5, 6 | opeq12d 4880 |
. . . . . 6
β’ (π΄ β β β
β¨(numerβπ΄),
(denomβπ΄)β© =
β¨(1st β(β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ))))), (2nd
β(β©π
β (β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))))β©) |
8 | 4, 7 | eqtr4d 2775 |
. . . . 5
β’ (π΄ β β β
(β©π β
(β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) = β¨(numerβπ΄), (denomβπ΄)β©) |
9 | 8 | eqeq1d 2734 |
. . . 4
β’ (π΄ β β β
((β©π β
(β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) = β¨π΅, πΆβ© β β¨(numerβπ΄), (denomβπ΄)β© = β¨π΅, πΆβ©)) |
10 | 9 | 3ad2ant1 1133 |
. . 3
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
((β©π β
(β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) = β¨π΅, πΆβ© β β¨(numerβπ΄), (denomβπ΄)β© = β¨π΅, πΆβ©)) |
11 | | fvex 6901 |
. . . 4
β’
(numerβπ΄)
β V |
12 | | fvex 6901 |
. . . 4
β’
(denomβπ΄)
β V |
13 | 11, 12 | opth 5475 |
. . 3
β’
(β¨(numerβπ΄), (denomβπ΄)β© = β¨π΅, πΆβ© β ((numerβπ΄) = π΅ β§ (denomβπ΄) = πΆ)) |
14 | 10, 13 | bitr2di 287 |
. 2
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
(((numerβπ΄) = π΅ β§ (denomβπ΄) = πΆ) β (β©π β (β€ Γ
β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) = β¨π΅, πΆβ©)) |
15 | | opelxpi 5712 |
. . . 4
β’ ((π΅ β β€ β§ πΆ β β) β
β¨π΅, πΆβ© β (β€ Γ
β)) |
16 | 15 | 3adant1 1130 |
. . 3
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
β¨π΅, πΆβ© β (β€ Γ
β)) |
17 | 1 | 3ad2ant1 1133 |
. . 3
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
β!π β (β€
Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) |
18 | | fveq2 6888 |
. . . . . . 7
β’ (π = β¨π΅, πΆβ© β (1st βπ) = (1st
ββ¨π΅, πΆβ©)) |
19 | | fveq2 6888 |
. . . . . . 7
β’ (π = β¨π΅, πΆβ© β (2nd βπ) = (2nd
ββ¨π΅, πΆβ©)) |
20 | 18, 19 | oveq12d 7423 |
. . . . . 6
β’ (π = β¨π΅, πΆβ© β ((1st βπ) gcd (2nd
βπ)) =
((1st ββ¨π΅, πΆβ©) gcd (2nd
ββ¨π΅, πΆβ©))) |
21 | 20 | eqeq1d 2734 |
. . . . 5
β’ (π = β¨π΅, πΆβ© β (((1st βπ) gcd (2nd
βπ)) = 1 β
((1st ββ¨π΅, πΆβ©) gcd (2nd
ββ¨π΅, πΆβ©)) = 1)) |
22 | 18, 19 | oveq12d 7423 |
. . . . . 6
β’ (π = β¨π΅, πΆβ© β ((1st βπ) / (2nd βπ)) = ((1st
ββ¨π΅, πΆβ©) / (2nd
ββ¨π΅, πΆβ©))) |
23 | 22 | eqeq2d 2743 |
. . . . 5
β’ (π = β¨π΅, πΆβ© β (π΄ = ((1st βπ) / (2nd βπ)) β π΄ = ((1st ββ¨π΅, πΆβ©) / (2nd ββ¨π΅, πΆβ©)))) |
24 | 21, 23 | anbi12d 631 |
. . . 4
β’ (π = β¨π΅, πΆβ© β ((((1st
βπ) gcd
(2nd βπ))
= 1 β§ π΄ =
((1st βπ)
/ (2nd βπ))) β (((1st
ββ¨π΅, πΆβ©) gcd (2nd
ββ¨π΅, πΆβ©)) = 1 β§ π΄ = ((1st
ββ¨π΅, πΆβ©) / (2nd
ββ¨π΅, πΆβ©))))) |
25 | 24 | riota2 7387 |
. . 3
β’
((β¨π΅, πΆβ© β (β€ Γ
β) β§ β!π
β (β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) β ((((1st
ββ¨π΅, πΆβ©) gcd (2nd
ββ¨π΅, πΆβ©)) = 1 β§ π΄ = ((1st
ββ¨π΅, πΆβ©) / (2nd
ββ¨π΅, πΆβ©))) β
(β©π β
(β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) = β¨π΅, πΆβ©)) |
26 | 16, 17, 25 | syl2anc 584 |
. 2
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
((((1st ββ¨π΅, πΆβ©) gcd (2nd
ββ¨π΅, πΆβ©)) = 1 β§ π΄ = ((1st
ββ¨π΅, πΆβ©) / (2nd
ββ¨π΅, πΆβ©))) β
(β©π β
(β€ Γ β)(((1st βπ) gcd (2nd βπ)) = 1 β§ π΄ = ((1st βπ) / (2nd βπ)))) = β¨π΅, πΆβ©)) |
27 | | op1stg 7983 |
. . . . . 6
β’ ((π΅ β β€ β§ πΆ β β) β
(1st ββ¨π΅, πΆβ©) = π΅) |
28 | | op2ndg 7984 |
. . . . . 6
β’ ((π΅ β β€ β§ πΆ β β) β
(2nd ββ¨π΅, πΆβ©) = πΆ) |
29 | 27, 28 | oveq12d 7423 |
. . . . 5
β’ ((π΅ β β€ β§ πΆ β β) β
((1st ββ¨π΅, πΆβ©) gcd (2nd
ββ¨π΅, πΆβ©)) = (π΅ gcd πΆ)) |
30 | 29 | 3adant1 1130 |
. . . 4
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
((1st ββ¨π΅, πΆβ©) gcd (2nd
ββ¨π΅, πΆβ©)) = (π΅ gcd πΆ)) |
31 | 30 | eqeq1d 2734 |
. . 3
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
(((1st ββ¨π΅, πΆβ©) gcd (2nd
ββ¨π΅, πΆβ©)) = 1 β (π΅ gcd πΆ) = 1)) |
32 | 27 | 3adant1 1130 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
(1st ββ¨π΅, πΆβ©) = π΅) |
33 | 28 | 3adant1 1130 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
(2nd ββ¨π΅, πΆβ©) = πΆ) |
34 | 32, 33 | oveq12d 7423 |
. . . 4
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
((1st ββ¨π΅, πΆβ©) / (2nd ββ¨π΅, πΆβ©)) = (π΅ / πΆ)) |
35 | 34 | eqeq2d 2743 |
. . 3
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β (π΄ = ((1st
ββ¨π΅, πΆβ©) / (2nd
ββ¨π΅, πΆβ©)) β π΄ = (π΅ / πΆ))) |
36 | 31, 35 | anbi12d 631 |
. 2
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β
((((1st ββ¨π΅, πΆβ©) gcd (2nd
ββ¨π΅, πΆβ©)) = 1 β§ π΄ = ((1st
ββ¨π΅, πΆβ©) / (2nd
ββ¨π΅, πΆβ©))) β ((π΅ gcd πΆ) = 1 β§ π΄ = (π΅ / πΆ)))) |
37 | 14, 26, 36 | 3bitr2rd 307 |
1
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β (((π΅ gcd πΆ) = 1 β§ π΄ = (π΅ / πΆ)) β ((numerβπ΄) = π΅ β§ (denomβπ΄) = πΆ))) |