Step | Hyp | Ref
| Expression |
1 | | 1red 11161 |
. . . 4
โข ((๐ โง โ๐ โ ๐ด ๐ต โ 0) โ 1 โ
โ) |
2 | | fprodle.kph |
. . . . . 6
โข
โฒ๐๐ |
3 | | nfra1 3266 |
. . . . . 6
โข
โฒ๐โ๐ โ ๐ด ๐ต โ 0 |
4 | 2, 3 | nfan 1903 |
. . . . 5
โข
โฒ๐(๐ โง โ๐ โ ๐ด ๐ต โ 0) |
5 | | fprodle.a |
. . . . . 6
โข (๐ โ ๐ด โ Fin) |
6 | 5 | adantr 482 |
. . . . 5
โข ((๐ โง โ๐ โ ๐ด ๐ต โ 0) โ ๐ด โ Fin) |
7 | | fprodle.c |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) |
8 | 7 | adantlr 714 |
. . . . . 6
โข (((๐ โง โ๐ โ ๐ด ๐ต โ 0) โง ๐ โ ๐ด) โ ๐ถ โ โ) |
9 | | fprodle.b |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) |
10 | 9 | adantlr 714 |
. . . . . 6
โข (((๐ โง โ๐ โ ๐ด ๐ต โ 0) โง ๐ โ ๐ด) โ ๐ต โ โ) |
11 | | rspa 3230 |
. . . . . . 7
โข
((โ๐ โ
๐ด ๐ต โ 0 โง ๐ โ ๐ด) โ ๐ต โ 0) |
12 | 11 | adantll 713 |
. . . . . 6
โข (((๐ โง โ๐ โ ๐ด ๐ต โ 0) โง ๐ โ ๐ด) โ ๐ต โ 0) |
13 | 8, 10, 12 | redivcld 11988 |
. . . . 5
โข (((๐ โง โ๐ โ ๐ด ๐ต โ 0) โง ๐ โ ๐ด) โ (๐ถ / ๐ต) โ โ) |
14 | 4, 6, 13 | fprodreclf 15847 |
. . . 4
โข ((๐ โง โ๐ โ ๐ด ๐ต โ 0) โ โ๐ โ ๐ด (๐ถ / ๐ต) โ โ) |
15 | 2, 5, 9 | fprodreclf 15847 |
. . . . 5
โข (๐ โ โ๐ โ ๐ด ๐ต โ โ) |
16 | 15 | adantr 482 |
. . . 4
โข ((๐ โง โ๐ โ ๐ด ๐ต โ 0) โ โ๐ โ ๐ด ๐ต โ โ) |
17 | | fprodle.0l3b |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ 0 โค ๐ต) |
18 | 2, 5, 9, 17 | fprodge0 15881 |
. . . . 5
โข (๐ โ 0 โค โ๐ โ ๐ด ๐ต) |
19 | 18 | adantr 482 |
. . . 4
โข ((๐ โง โ๐ โ ๐ด ๐ต โ 0) โ 0 โค โ๐ โ ๐ด ๐ต) |
20 | 17 | adantlr 714 |
. . . . . . . 8
โข (((๐ โง โ๐ โ ๐ด ๐ต โ 0) โง ๐ โ ๐ด) โ 0 โค ๐ต) |
21 | 10, 20, 12 | ne0gt0d 11297 |
. . . . . . 7
โข (((๐ โง โ๐ โ ๐ด ๐ต โ 0) โง ๐ โ ๐ด) โ 0 < ๐ต) |
22 | 10, 21 | elrpd 12959 |
. . . . . 6
โข (((๐ โง โ๐ โ ๐ด ๐ต โ 0) โง ๐ โ ๐ด) โ ๐ต โ
โ+) |
23 | | fprodle.blec |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โค ๐ถ) |
24 | 23 | adantlr 714 |
. . . . . 6
โข (((๐ โง โ๐ โ ๐ด ๐ต โ 0) โง ๐ โ ๐ด) โ ๐ต โค ๐ถ) |
25 | | divge1 12988 |
. . . . . 6
โข ((๐ต โ โ+
โง ๐ถ โ โ
โง ๐ต โค ๐ถ) โ 1 โค (๐ถ / ๐ต)) |
26 | 22, 8, 24, 25 | syl3anc 1372 |
. . . . 5
โข (((๐ โง โ๐ โ ๐ด ๐ต โ 0) โง ๐ โ ๐ด) โ 1 โค (๐ถ / ๐ต)) |
27 | 4, 6, 13, 26 | fprodge1 15883 |
. . . 4
โข ((๐ โง โ๐ โ ๐ด ๐ต โ 0) โ 1 โค โ๐ โ ๐ด (๐ถ / ๐ต)) |
28 | 1, 14, 16, 19, 27 | lemul2ad 12100 |
. . 3
โข ((๐ โง โ๐ โ ๐ด ๐ต โ 0) โ (โ๐ โ ๐ด ๐ต ยท 1) โค (โ๐ โ ๐ด ๐ต ยท โ๐ โ ๐ด (๐ถ / ๐ต))) |
29 | 9 | recnd 11188 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) |
30 | 2, 5, 29 | fprodclf 15880 |
. . . . 5
โข (๐ โ โ๐ โ ๐ด ๐ต โ โ) |
31 | 30 | mulid1d 11177 |
. . . 4
โข (๐ โ (โ๐ โ ๐ด ๐ต ยท 1) = โ๐ โ ๐ด ๐ต) |
32 | 31 | adantr 482 |
. . 3
โข ((๐ โง โ๐ โ ๐ด ๐ต โ 0) โ (โ๐ โ ๐ด ๐ต ยท 1) = โ๐ โ ๐ด ๐ต) |
33 | 7 | recnd 11188 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) |
34 | 33 | adantlr 714 |
. . . . . 6
โข (((๐ โง โ๐ โ ๐ด ๐ต โ 0) โง ๐ โ ๐ด) โ ๐ถ โ โ) |
35 | 29 | adantlr 714 |
. . . . . 6
โข (((๐ โง โ๐ โ ๐ด ๐ต โ 0) โง ๐ โ ๐ด) โ ๐ต โ โ) |
36 | 4, 6, 34, 35, 12 | fproddivf 15875 |
. . . . 5
โข ((๐ โง โ๐ โ ๐ด ๐ต โ 0) โ โ๐ โ ๐ด (๐ถ / ๐ต) = (โ๐ โ ๐ด ๐ถ / โ๐ โ ๐ด ๐ต)) |
37 | 36 | oveq2d 7374 |
. . . 4
โข ((๐ โง โ๐ โ ๐ด ๐ต โ 0) โ (โ๐ โ ๐ด ๐ต ยท โ๐ โ ๐ด (๐ถ / ๐ต)) = (โ๐ โ ๐ด ๐ต ยท (โ๐ โ ๐ด ๐ถ / โ๐ โ ๐ด ๐ต))) |
38 | 2, 5, 33 | fprodclf 15880 |
. . . . . 6
โข (๐ โ โ๐ โ ๐ด ๐ถ โ โ) |
39 | 38 | adantr 482 |
. . . . 5
โข ((๐ โง โ๐ โ ๐ด ๐ต โ 0) โ โ๐ โ ๐ด ๐ถ โ โ) |
40 | 30 | adantr 482 |
. . . . 5
โข ((๐ โง โ๐ โ ๐ด ๐ต โ 0) โ โ๐ โ ๐ด ๐ต โ โ) |
41 | 4, 6, 35, 12 | fprodn0f 15879 |
. . . . 5
โข ((๐ โง โ๐ โ ๐ด ๐ต โ 0) โ โ๐ โ ๐ด ๐ต โ 0) |
42 | 39, 40, 41 | divcan2d 11938 |
. . . 4
โข ((๐ โง โ๐ โ ๐ด ๐ต โ 0) โ (โ๐ โ ๐ด ๐ต ยท (โ๐ โ ๐ด ๐ถ / โ๐ โ ๐ด ๐ต)) = โ๐ โ ๐ด ๐ถ) |
43 | 37, 42 | eqtrd 2773 |
. . 3
โข ((๐ โง โ๐ โ ๐ด ๐ต โ 0) โ (โ๐ โ ๐ด ๐ต ยท โ๐ โ ๐ด (๐ถ / ๐ต)) = โ๐ โ ๐ด ๐ถ) |
44 | 28, 32, 43 | 3brtr3d 5137 |
. 2
โข ((๐ โง โ๐ โ ๐ด ๐ต โ 0) โ โ๐ โ ๐ด ๐ต โค โ๐ โ ๐ด ๐ถ) |
45 | | nne 2944 |
. . . . 5
โข (ยฌ
๐ต โ 0 โ ๐ต = 0) |
46 | 45 | rexbii 3094 |
. . . 4
โข
(โ๐ โ
๐ด ยฌ ๐ต โ 0 โ โ๐ โ ๐ด ๐ต = 0) |
47 | | rexnal 3100 |
. . . 4
โข
(โ๐ โ
๐ด ยฌ ๐ต โ 0 โ ยฌ โ๐ โ ๐ด ๐ต โ 0) |
48 | | nfv 1918 |
. . . . 5
โข
โฒ๐ ๐ต = 0 |
49 | | nfcsb1v 3881 |
. . . . . 6
โข
โฒ๐โฆ๐ / ๐โฆ๐ต |
50 | 49 | nfeq1 2919 |
. . . . 5
โข
โฒ๐โฆ๐ / ๐โฆ๐ต = 0 |
51 | | csbeq1a 3870 |
. . . . . 6
โข (๐ = ๐ โ ๐ต = โฆ๐ / ๐โฆ๐ต) |
52 | 51 | eqeq1d 2735 |
. . . . 5
โข (๐ = ๐ โ (๐ต = 0 โ โฆ๐ / ๐โฆ๐ต = 0)) |
53 | 48, 50, 52 | cbvrexw 3289 |
. . . 4
โข
(โ๐ โ
๐ด ๐ต = 0 โ โ๐ โ ๐ด โฆ๐ / ๐โฆ๐ต = 0) |
54 | 46, 47, 53 | 3bitr3i 301 |
. . 3
โข (ยฌ
โ๐ โ ๐ด ๐ต โ 0 โ โ๐ โ ๐ด โฆ๐ / ๐โฆ๐ต = 0) |
55 | | nfv 1918 |
. . . . . . . 8
โข
โฒ๐ ๐ โ ๐ด |
56 | 2, 55, 50 | nf3an 1905 |
. . . . . . 7
โข
โฒ๐(๐ โง ๐ โ ๐ด โง โฆ๐ / ๐โฆ๐ต = 0) |
57 | 5 | 3ad2ant1 1134 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด โง โฆ๐ / ๐โฆ๐ต = 0) โ ๐ด โ Fin) |
58 | 29 | 3ad2antl1 1186 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐ด โง โฆ๐ / ๐โฆ๐ต = 0) โง ๐ โ ๐ด) โ ๐ต โ โ) |
59 | | simp2 1138 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด โง โฆ๐ / ๐โฆ๐ต = 0) โ ๐ โ ๐ด) |
60 | 52 | biimparc 481 |
. . . . . . . 8
โข
((โฆ๐ /
๐โฆ๐ต = 0 โง ๐ = ๐) โ ๐ต = 0) |
61 | 60 | 3ad2antl3 1188 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐ด โง โฆ๐ / ๐โฆ๐ต = 0) โง ๐ = ๐) โ ๐ต = 0) |
62 | 56, 57, 58, 59, 61 | fprodeq0g 15882 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด โง โฆ๐ / ๐โฆ๐ต = 0) โ โ๐ โ ๐ด ๐ต = 0) |
63 | 62 | rexlimdv3a 3153 |
. . . . 5
โข (๐ โ (โ๐ โ ๐ด โฆ๐ / ๐โฆ๐ต = 0 โ โ๐ โ ๐ด ๐ต = 0)) |
64 | 63 | imp 408 |
. . . 4
โข ((๐ โง โ๐ โ ๐ด โฆ๐ / ๐โฆ๐ต = 0) โ โ๐ โ ๐ด ๐ต = 0) |
65 | | 0red 11163 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด) โ 0 โ โ) |
66 | 65, 9, 7, 17, 23 | letrd 11317 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ 0 โค ๐ถ) |
67 | 2, 5, 7, 66 | fprodge0 15881 |
. . . . 5
โข (๐ โ 0 โค โ๐ โ ๐ด ๐ถ) |
68 | 67 | adantr 482 |
. . . 4
โข ((๐ โง โ๐ โ ๐ด โฆ๐ / ๐โฆ๐ต = 0) โ 0 โค โ๐ โ ๐ด ๐ถ) |
69 | 64, 68 | eqbrtrd 5128 |
. . 3
โข ((๐ โง โ๐ โ ๐ด โฆ๐ / ๐โฆ๐ต = 0) โ โ๐ โ ๐ด ๐ต โค โ๐ โ ๐ด ๐ถ) |
70 | 54, 69 | sylan2b 595 |
. 2
โข ((๐ โง ยฌ โ๐ โ ๐ด ๐ต โ 0) โ โ๐ โ ๐ด ๐ต โค โ๐ โ ๐ด ๐ถ) |
71 | 44, 70 | pm2.61dan 812 |
1
โข (๐ โ โ๐ โ ๐ด ๐ต โค โ๐ โ ๐ด ๐ถ) |