Step | Hyp | Ref
| Expression |
1 | | 1xr 11219 |
. 2
โข 1 โ
โ* |
2 | | pnfxr 11214 |
. 2
โข +โ
โ โ* |
3 | | fprodge1.ph |
. . 3
โข
โฒ๐๐ |
4 | | 1re 11160 |
. . . . . 6
โข 1 โ
โ |
5 | | icossre 13351 |
. . . . . 6
โข ((1
โ โ โง +โ โ โ*) โ (1[,)+โ)
โ โ) |
6 | 4, 2, 5 | mp2an 691 |
. . . . 5
โข
(1[,)+โ) โ โ |
7 | | ax-resscn 11113 |
. . . . 5
โข โ
โ โ |
8 | 6, 7 | sstri 3954 |
. . . 4
โข
(1[,)+โ) โ โ |
9 | 8 | a1i 11 |
. . 3
โข (๐ โ (1[,)+โ) โ
โ) |
10 | 1 | a1i 11 |
. . . . 5
โข ((๐ฅ โ (1[,)+โ) โง
๐ฆ โ (1[,)+โ))
โ 1 โ โ*) |
11 | 2 | a1i 11 |
. . . . 5
โข ((๐ฅ โ (1[,)+โ) โง
๐ฆ โ (1[,)+โ))
โ +โ โ โ*) |
12 | 6 | sseli 3941 |
. . . . . . . 8
โข (๐ฅ โ (1[,)+โ) โ
๐ฅ โ
โ) |
13 | 12 | adantr 482 |
. . . . . . 7
โข ((๐ฅ โ (1[,)+โ) โง
๐ฆ โ (1[,)+โ))
โ ๐ฅ โ
โ) |
14 | 6 | sseli 3941 |
. . . . . . . 8
โข (๐ฆ โ (1[,)+โ) โ
๐ฆ โ
โ) |
15 | 14 | adantl 483 |
. . . . . . 7
โข ((๐ฅ โ (1[,)+โ) โง
๐ฆ โ (1[,)+โ))
โ ๐ฆ โ
โ) |
16 | 13, 15 | remulcld 11190 |
. . . . . 6
โข ((๐ฅ โ (1[,)+โ) โง
๐ฆ โ (1[,)+โ))
โ (๐ฅ ยท ๐ฆ) โ
โ) |
17 | 16 | rexrd 11210 |
. . . . 5
โข ((๐ฅ โ (1[,)+โ) โง
๐ฆ โ (1[,)+โ))
โ (๐ฅ ยท ๐ฆ) โ
โ*) |
18 | | 1t1e1 12320 |
. . . . . 6
โข (1
ยท 1) = 1 |
19 | 4 | a1i 11 |
. . . . . . 7
โข ((๐ฅ โ (1[,)+โ) โง
๐ฆ โ (1[,)+โ))
โ 1 โ โ) |
20 | | 0le1 11683 |
. . . . . . . 8
โข 0 โค
1 |
21 | 20 | a1i 11 |
. . . . . . 7
โข ((๐ฅ โ (1[,)+โ) โง
๐ฆ โ (1[,)+โ))
โ 0 โค 1) |
22 | | icogelb 13321 |
. . . . . . . . 9
โข ((1
โ โ* โง +โ โ โ* โง
๐ฅ โ (1[,)+โ))
โ 1 โค ๐ฅ) |
23 | 1, 2, 22 | mp3an12 1452 |
. . . . . . . 8
โข (๐ฅ โ (1[,)+โ) โ 1
โค ๐ฅ) |
24 | 23 | adantr 482 |
. . . . . . 7
โข ((๐ฅ โ (1[,)+โ) โง
๐ฆ โ (1[,)+โ))
โ 1 โค ๐ฅ) |
25 | | icogelb 13321 |
. . . . . . . . 9
โข ((1
โ โ* โง +โ โ โ* โง
๐ฆ โ (1[,)+โ))
โ 1 โค ๐ฆ) |
26 | 1, 2, 25 | mp3an12 1452 |
. . . . . . . 8
โข (๐ฆ โ (1[,)+โ) โ 1
โค ๐ฆ) |
27 | 26 | adantl 483 |
. . . . . . 7
โข ((๐ฅ โ (1[,)+โ) โง
๐ฆ โ (1[,)+โ))
โ 1 โค ๐ฆ) |
28 | 19, 13, 19, 15, 21, 21, 24, 27 | lemul12ad 12102 |
. . . . . 6
โข ((๐ฅ โ (1[,)+โ) โง
๐ฆ โ (1[,)+โ))
โ (1 ยท 1) โค (๐ฅ ยท ๐ฆ)) |
29 | 18, 28 | eqbrtrrid 5142 |
. . . . 5
โข ((๐ฅ โ (1[,)+โ) โง
๐ฆ โ (1[,)+โ))
โ 1 โค (๐ฅ ยท
๐ฆ)) |
30 | 16 | ltpnfd 13047 |
. . . . 5
โข ((๐ฅ โ (1[,)+โ) โง
๐ฆ โ (1[,)+โ))
โ (๐ฅ ยท ๐ฆ) <
+โ) |
31 | 10, 11, 17, 29, 30 | elicod 13320 |
. . . 4
โข ((๐ฅ โ (1[,)+โ) โง
๐ฆ โ (1[,)+โ))
โ (๐ฅ ยท ๐ฆ) โ
(1[,)+โ)) |
32 | 31 | adantl 483 |
. . 3
โข ((๐ โง (๐ฅ โ (1[,)+โ) โง ๐ฆ โ (1[,)+โ))) โ
(๐ฅ ยท ๐ฆ) โ
(1[,)+โ)) |
33 | | fprodge1.a |
. . 3
โข (๐ โ ๐ด โ Fin) |
34 | 1 | a1i 11 |
. . . 4
โข ((๐ โง ๐ โ ๐ด) โ 1 โ
โ*) |
35 | 2 | a1i 11 |
. . . 4
โข ((๐ โง ๐ โ ๐ด) โ +โ โ
โ*) |
36 | | fprodge1.b |
. . . . 5
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) |
37 | 36 | rexrd 11210 |
. . . 4
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ
โ*) |
38 | | fprodge1.ge |
. . . 4
โข ((๐ โง ๐ โ ๐ด) โ 1 โค ๐ต) |
39 | 36 | ltpnfd 13047 |
. . . 4
โข ((๐ โง ๐ โ ๐ด) โ ๐ต < +โ) |
40 | 34, 35, 37, 38, 39 | elicod 13320 |
. . 3
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (1[,)+โ)) |
41 | | 1le1 11788 |
. . . . 5
โข 1 โค
1 |
42 | | ltpnf 13046 |
. . . . . 6
โข (1 โ
โ โ 1 < +โ) |
43 | 4, 42 | ax-mp 5 |
. . . . 5
โข 1 <
+โ |
44 | | elico2 13334 |
. . . . . 6
โข ((1
โ โ โง +โ โ โ*) โ (1 โ
(1[,)+โ) โ (1 โ โ โง 1 โค 1 โง 1 <
+โ))) |
45 | 4, 2, 44 | mp2an 691 |
. . . . 5
โข (1 โ
(1[,)+โ) โ (1 โ โ โง 1 โค 1 โง 1 <
+โ)) |
46 | 4, 41, 43, 45 | mpbir3an 1342 |
. . . 4
โข 1 โ
(1[,)+โ) |
47 | 46 | a1i 11 |
. . 3
โข (๐ โ 1 โ
(1[,)+โ)) |
48 | 3, 9, 32, 33, 40, 47 | fprodcllemf 15846 |
. 2
โข (๐ โ โ๐ โ ๐ด ๐ต โ (1[,)+โ)) |
49 | | icogelb 13321 |
. 2
โข ((1
โ โ* โง +โ โ โ* โง
โ๐ โ ๐ด ๐ต โ (1[,)+โ)) โ 1 โค
โ๐ โ ๐ด ๐ต) |
50 | 1, 2, 48, 49 | mp3an12i 1466 |
1
โข (๐ โ 1 โค โ๐ โ ๐ด ๐ต) |