Step | Hyp | Ref
| Expression |
1 | | oveq2 5885 |
. . . . . . . 8
โข (๐ฆ = ๐ก โ (๐ต ยท ๐ฆ) = (๐ต ยท ๐ก)) |
2 | 1 | oveq2d 5893 |
. . . . . . 7
โข (๐ฆ = ๐ก โ ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ก))) |
3 | 2 | eqeq2d 2189 |
. . . . . 6
โข (๐ฆ = ๐ก โ (๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ก)))) |
4 | 3 | cbvrexv 2706 |
. . . . 5
โข
(โ๐ฆ โ
โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ก โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ก))) |
5 | 4 | rexbii 2484 |
. . . 4
โข
(โ๐ฅ โ
โค โ๐ฆ โ
โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ฅ โ โค โ๐ก โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ก))) |
6 | | oveq2 5885 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (๐ด ยท ๐ฅ) = (๐ด ยท ๐ )) |
7 | 6 | oveq1d 5892 |
. . . . . . 7
โข (๐ฅ = ๐ โ ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ก)) = ((๐ด ยท ๐ ) + (๐ต ยท ๐ก))) |
8 | 7 | eqeq2d 2189 |
. . . . . 6
โข (๐ฅ = ๐ โ (๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ก)) โ ๐ = ((๐ด ยท ๐ ) + (๐ต ยท ๐ก)))) |
9 | 8 | rexbidv 2478 |
. . . . 5
โข (๐ฅ = ๐ โ (โ๐ก โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ก)) โ โ๐ก โ โค ๐ = ((๐ด ยท ๐ ) + (๐ต ยท ๐ก)))) |
10 | 9 | cbvrexv 2706 |
. . . 4
โข
(โ๐ฅ โ
โค โ๐ก โ
โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ก)) โ โ๐ โ โค โ๐ก โ โค ๐ = ((๐ด ยท ๐ ) + (๐ต ยท ๐ก))) |
11 | 5, 10 | bitri 184 |
. . 3
โข
(โ๐ฅ โ
โค โ๐ฆ โ
โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ โ โค โ๐ก โ โค ๐ = ((๐ด ยท ๐ ) + (๐ต ยท ๐ก))) |
12 | | simpl 109 |
. . 3
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ ๐ด โ
โ0) |
13 | | simpr 110 |
. . 3
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ ๐ต โ
โ0) |
14 | 11, 12, 13 | bezoutlemb 12003 |
. 2
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ [๐ต / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) |
15 | | dfsbcq2 2967 |
. . . 4
โข (๐ = ๐ต โ ([๐ / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ [๐ต / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) |
16 | | breq2 4009 |
. . . . . . . . 9
โข (๐ = ๐ต โ (๐ง โฅ ๐ โ ๐ง โฅ ๐ต)) |
17 | 16 | anbi2d 464 |
. . . . . . . 8
โข (๐ = ๐ต โ ((๐ง โฅ ๐ด โง ๐ง โฅ ๐) โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต))) |
18 | 17 | imbi2d 230 |
. . . . . . 7
โข (๐ = ๐ต โ ((๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐)) โ (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)))) |
19 | 18 | ralbidv 2477 |
. . . . . 6
โข (๐ = ๐ต โ (โ๐ง โ โ0 (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐)) โ โ๐ง โ โ0 (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)))) |
20 | 19 | anbi1d 465 |
. . . . 5
โข (๐ = ๐ต โ ((โ๐ง โ โ0 (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ (โ๐ง โ โ0 (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))))) |
21 | 20 | rexbidv 2478 |
. . . 4
โข (๐ = ๐ต โ (โ๐ โ โ0 (โ๐ง โ โ0
(๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ โ๐ โ โ0 (โ๐ง โ โ0
(๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))))) |
22 | 15, 21 | imbi12d 234 |
. . 3
โข (๐ = ๐ต โ (([๐ / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ โ โ0 (โ๐ง โ โ0
(๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) โ ([๐ต / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ โ โ0 (โ๐ง โ โ0
(๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))))) |
23 | 11, 12, 13 | bezoutlema 12002 |
. . . 4
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ [๐ด / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) |
24 | | dfsbcq2 2967 |
. . . . . 6
โข (๐ = ๐ด โ ([๐ / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ [๐ด / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) |
25 | | breq2 4009 |
. . . . . . . . . . . . 13
โข (๐ = ๐ด โ (๐ง โฅ ๐ โ ๐ง โฅ ๐ด)) |
26 | 25 | anbi1d 465 |
. . . . . . . . . . . 12
โข (๐ = ๐ด โ ((๐ง โฅ ๐ โง ๐ง โฅ ๐) โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐))) |
27 | 26 | imbi2d 230 |
. . . . . . . . . . 11
โข (๐ = ๐ด โ ((๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)) โ (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐)))) |
28 | 27 | ralbidv 2477 |
. . . . . . . . . 10
โข (๐ = ๐ด โ (โ๐ง โ โ0 (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)) โ โ๐ง โ โ0 (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐)))) |
29 | 28 | anbi1d 465 |
. . . . . . . . 9
โข (๐ = ๐ด โ ((โ๐ง โ โ0 (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ (โ๐ง โ โ0 (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))))) |
30 | 29 | rexbidv 2478 |
. . . . . . . 8
โข (๐ = ๐ด โ (โ๐ โ โ0 (โ๐ง โ โ0
(๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ โ๐ โ โ0 (โ๐ง โ โ0
(๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))))) |
31 | 30 | imbi2d 230 |
. . . . . . 7
โข (๐ = ๐ด โ (([๐ / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ โ โ0 (โ๐ง โ โ0
(๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) โ ([๐ / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ โ โ0 (โ๐ง โ โ0
(๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))))) |
32 | 31 | ralbidv 2477 |
. . . . . 6
โข (๐ = ๐ด โ (โ๐ โ โ0 ([๐ / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ โ โ0 (โ๐ง โ โ0
(๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) โ โ๐ โ โ0 ([๐ / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ โ โ0 (โ๐ง โ โ0
(๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))))) |
33 | 24, 32 | imbi12d 234 |
. . . . 5
โข (๐ = ๐ด โ (([๐ / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ โ โ0 ([๐ / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ โ โ0 (โ๐ง โ โ0
(๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))))) โ ([๐ด / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ โ โ0 ([๐ / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ โ โ0 (โ๐ง โ โ0
(๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))))))) |
34 | | breq1 4008 |
. . . . . . . 8
โข (๐ง = ๐ค โ (๐ง โฅ ๐ โ ๐ค โฅ ๐)) |
35 | | breq1 4008 |
. . . . . . . . 9
โข (๐ง = ๐ค โ (๐ง โฅ ๐ โ ๐ค โฅ ๐)) |
36 | | breq1 4008 |
. . . . . . . . 9
โข (๐ง = ๐ค โ (๐ง โฅ ๐ โ ๐ค โฅ ๐)) |
37 | 35, 36 | anbi12d 473 |
. . . . . . . 8
โข (๐ง = ๐ค โ ((๐ง โฅ ๐ โง ๐ง โฅ ๐) โ (๐ค โฅ ๐ โง ๐ค โฅ ๐))) |
38 | 34, 37 | imbi12d 234 |
. . . . . . 7
โข (๐ง = ๐ค โ ((๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)) โ (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)))) |
39 | 38 | cbvralv 2705 |
. . . . . 6
โข
(โ๐ง โ
โ0 (๐ง
โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)) โ โ๐ค โ โ0 (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐))) |
40 | 11, 39, 12, 13 | bezoutlemmain 12001 |
. . . . 5
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ โ๐ โ โ0 ([๐ / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ โ โ0 ([๐ / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ โ โ0 (โ๐ง โ โ0
(๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))))) |
41 | 33, 40, 12 | rspcdva 2848 |
. . . 4
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ ([๐ด / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ โ โ0 ([๐ / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ โ โ0 (โ๐ง โ โ0
(๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))))) |
42 | 23, 41 | mpd 13 |
. . 3
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ โ๐ โ โ0 ([๐ / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ โ โ0 (โ๐ง โ โ0
(๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))))) |
43 | 22, 42, 13 | rspcdva 2848 |
. 2
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ ([๐ต / ๐]โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ โ โ0 (โ๐ง โ โ0
(๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))))) |
44 | 14, 43 | mpd 13 |
1
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ โ๐ โ โ0 (โ๐ง โ โ0
(๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) |