Step | Hyp | Ref
| Expression |
1 | | elfz1 13438 |
. . 3
โข ((๐ โ โค โง ๐ โ โค) โ (๐ฝ โ (๐...๐) โ (๐ฝ โ โค โง ๐ โค ๐ฝ โง ๐ฝ โค ๐))) |
2 | 1 | 3adant3 1133 |
. 2
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โ) โ (๐ฝ โ (๐...๐) โ (๐ฝ โ โค โง ๐ โค ๐ฝ โง ๐ฝ โค ๐))) |
3 | | zre 12511 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
โ) |
4 | | zre 12511 |
. . . . . . . . . . . 12
โข (๐ฝ โ โค โ ๐ฝ โ
โ) |
5 | | nnre 12168 |
. . . . . . . . . . . . 13
โข (๐พ โ โ โ ๐พ โ
โ) |
6 | | nngt0 12192 |
. . . . . . . . . . . . 13
โข (๐พ โ โ โ 0 <
๐พ) |
7 | 5, 6 | jca 513 |
. . . . . . . . . . . 12
โข (๐พ โ โ โ (๐พ โ โ โง 0 <
๐พ)) |
8 | | lemul2 12016 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ฝ โ โ โง (๐พ โ โ โง 0 <
๐พ)) โ (๐ โค ๐ฝ โ (๐พ ยท ๐) โค (๐พ ยท ๐ฝ))) |
9 | 3, 4, 7, 8 | syl3an 1161 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ฝ โ โค โง ๐พ โ โ) โ (๐ โค ๐ฝ โ (๐พ ยท ๐) โค (๐พ ยท ๐ฝ))) |
10 | 9 | 3expa 1119 |
. . . . . . . . . 10
โข (((๐ โ โค โง ๐ฝ โ โค) โง ๐พ โ โ) โ (๐ โค ๐ฝ โ (๐พ ยท ๐) โค (๐พ ยท ๐ฝ))) |
11 | 10 | biimpd 228 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ฝ โ โค) โง ๐พ โ โ) โ (๐ โค ๐ฝ โ (๐พ ยท ๐) โค (๐พ ยท ๐ฝ))) |
12 | 11 | adantllr 718 |
. . . . . . . 8
โข ((((๐ โ โค โง ๐ โ โค) โง ๐ฝ โ โค) โง ๐พ โ โ) โ (๐ โค ๐ฝ โ (๐พ ยท ๐) โค (๐พ ยท ๐ฝ))) |
13 | | zre 12511 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ ๐ โ
โ) |
14 | | lemul2 12016 |
. . . . . . . . . . . . 13
โข ((๐ฝ โ โ โง ๐ โ โ โง (๐พ โ โ โง 0 <
๐พ)) โ (๐ฝ โค ๐ โ (๐พ ยท ๐ฝ) โค (๐พ ยท ๐))) |
15 | 4, 13, 7, 14 | syl3an 1161 |
. . . . . . . . . . . 12
โข ((๐ฝ โ โค โง ๐ โ โค โง ๐พ โ โ) โ (๐ฝ โค ๐ โ (๐พ ยท ๐ฝ) โค (๐พ ยท ๐))) |
16 | 15 | 3expa 1119 |
. . . . . . . . . . 11
โข (((๐ฝ โ โค โง ๐ โ โค) โง ๐พ โ โ) โ (๐ฝ โค ๐ โ (๐พ ยท ๐ฝ) โค (๐พ ยท ๐))) |
17 | 16 | ancom1s 652 |
. . . . . . . . . 10
โข (((๐ โ โค โง ๐ฝ โ โค) โง ๐พ โ โ) โ (๐ฝ โค ๐ โ (๐พ ยท ๐ฝ) โค (๐พ ยท ๐))) |
18 | 17 | biimpd 228 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ฝ โ โค) โง ๐พ โ โ) โ (๐ฝ โค ๐ โ (๐พ ยท ๐ฝ) โค (๐พ ยท ๐))) |
19 | 18 | adantlll 717 |
. . . . . . . 8
โข ((((๐ โ โค โง ๐ โ โค) โง ๐ฝ โ โค) โง ๐พ โ โ) โ (๐ฝ โค ๐ โ (๐พ ยท ๐ฝ) โค (๐พ ยท ๐))) |
20 | 12, 19 | anim12d 610 |
. . . . . . 7
โข ((((๐ โ โค โง ๐ โ โค) โง ๐ฝ โ โค) โง ๐พ โ โ) โ ((๐ โค ๐ฝ โง ๐ฝ โค ๐) โ ((๐พ ยท ๐) โค (๐พ ยท ๐ฝ) โง (๐พ ยท ๐ฝ) โค (๐พ ยท ๐)))) |
21 | | zmulcl 12560 |
. . . . . . . . . . . . 13
โข ((๐พ โ โค โง ๐ โ โค) โ (๐พ ยท ๐) โ โค) |
22 | 21 | ex 414 |
. . . . . . . . . . . 12
โข (๐พ โ โค โ (๐ โ โค โ (๐พ ยท ๐) โ โค)) |
23 | | zmulcl 12560 |
. . . . . . . . . . . . 13
โข ((๐พ โ โค โง ๐ โ โค) โ (๐พ ยท ๐) โ โค) |
24 | 23 | ex 414 |
. . . . . . . . . . . 12
โข (๐พ โ โค โ (๐ โ โค โ (๐พ ยท ๐) โ โค)) |
25 | | zmulcl 12560 |
. . . . . . . . . . . . 13
โข ((๐พ โ โค โง ๐ฝ โ โค) โ (๐พ ยท ๐ฝ) โ โค) |
26 | 25 | ex 414 |
. . . . . . . . . . . 12
โข (๐พ โ โค โ (๐ฝ โ โค โ (๐พ ยท ๐ฝ) โ โค)) |
27 | 22, 24, 26 | 3anim123d 1444 |
. . . . . . . . . . 11
โข (๐พ โ โค โ ((๐ โ โค โง ๐ โ โค โง ๐ฝ โ โค) โ ((๐พ ยท ๐) โ โค โง (๐พ ยท ๐) โ โค โง (๐พ ยท ๐ฝ) โ โค))) |
28 | | elfz 13439 |
. . . . . . . . . . . 12
โข (((๐พ ยท ๐ฝ) โ โค โง (๐พ ยท ๐) โ โค โง (๐พ ยท ๐) โ โค) โ ((๐พ ยท ๐ฝ) โ ((๐พ ยท ๐)...(๐พ ยท ๐)) โ ((๐พ ยท ๐) โค (๐พ ยท ๐ฝ) โง (๐พ ยท ๐ฝ) โค (๐พ ยท ๐)))) |
29 | 28 | 3coml 1128 |
. . . . . . . . . . 11
โข (((๐พ ยท ๐) โ โค โง (๐พ ยท ๐) โ โค โง (๐พ ยท ๐ฝ) โ โค) โ ((๐พ ยท ๐ฝ) โ ((๐พ ยท ๐)...(๐พ ยท ๐)) โ ((๐พ ยท ๐) โค (๐พ ยท ๐ฝ) โง (๐พ ยท ๐ฝ) โค (๐พ ยท ๐)))) |
30 | 27, 29 | syl6 35 |
. . . . . . . . . 10
โข (๐พ โ โค โ ((๐ โ โค โง ๐ โ โค โง ๐ฝ โ โค) โ ((๐พ ยท ๐ฝ) โ ((๐พ ยท ๐)...(๐พ ยท ๐)) โ ((๐พ ยท ๐) โค (๐พ ยท ๐ฝ) โง (๐พ ยท ๐ฝ) โค (๐พ ยท ๐))))) |
31 | | nnz 12528 |
. . . . . . . . . 10
โข (๐พ โ โ โ ๐พ โ
โค) |
32 | 30, 31 | syl11 33 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค โง ๐ฝ โ โค) โ (๐พ โ โ โ ((๐พ ยท ๐ฝ) โ ((๐พ ยท ๐)...(๐พ ยท ๐)) โ ((๐พ ยท ๐) โค (๐พ ยท ๐ฝ) โง (๐พ ยท ๐ฝ) โค (๐พ ยท ๐))))) |
33 | 32 | 3expa 1119 |
. . . . . . . 8
โข (((๐ โ โค โง ๐ โ โค) โง ๐ฝ โ โค) โ (๐พ โ โ โ ((๐พ ยท ๐ฝ) โ ((๐พ ยท ๐)...(๐พ ยท ๐)) โ ((๐พ ยท ๐) โค (๐พ ยท ๐ฝ) โง (๐พ ยท ๐ฝ) โค (๐พ ยท ๐))))) |
34 | 33 | imp 408 |
. . . . . . 7
โข ((((๐ โ โค โง ๐ โ โค) โง ๐ฝ โ โค) โง ๐พ โ โ) โ ((๐พ ยท ๐ฝ) โ ((๐พ ยท ๐)...(๐พ ยท ๐)) โ ((๐พ ยท ๐) โค (๐พ ยท ๐ฝ) โง (๐พ ยท ๐ฝ) โค (๐พ ยท ๐)))) |
35 | 20, 34 | sylibrd 259 |
. . . . . 6
โข ((((๐ โ โค โง ๐ โ โค) โง ๐ฝ โ โค) โง ๐พ โ โ) โ ((๐ โค ๐ฝ โง ๐ฝ โค ๐) โ (๐พ ยท ๐ฝ) โ ((๐พ ยท ๐)...(๐พ ยท ๐)))) |
36 | 35 | an32s 651 |
. . . . 5
โข ((((๐ โ โค โง ๐ โ โค) โง ๐พ โ โ) โง ๐ฝ โ โค) โ ((๐ โค ๐ฝ โง ๐ฝ โค ๐) โ (๐พ ยท ๐ฝ) โ ((๐พ ยท ๐)...(๐พ ยท ๐)))) |
37 | 36 | exp4b 432 |
. . . 4
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ โ โ) โ (๐ฝ โ โค โ (๐ โค ๐ฝ โ (๐ฝ โค ๐ โ (๐พ ยท ๐ฝ) โ ((๐พ ยท ๐)...(๐พ ยท ๐)))))) |
38 | 37 | 3impd 1349 |
. . 3
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ โ โ) โ ((๐ฝ โ โค โง ๐ โค ๐ฝ โง ๐ฝ โค ๐) โ (๐พ ยท ๐ฝ) โ ((๐พ ยท ๐)...(๐พ ยท ๐)))) |
39 | 38 | 3impa 1111 |
. 2
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โ) โ ((๐ฝ โ โค โง ๐ โค ๐ฝ โง ๐ฝ โค ๐) โ (๐พ ยท ๐ฝ) โ ((๐พ ยท ๐)...(๐พ ยท ๐)))) |
40 | 2, 39 | sylbid 239 |
1
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โ) โ (๐ฝ โ (๐...๐) โ (๐พ ยท ๐ฝ) โ ((๐พ ยท ๐)...(๐พ ยท ๐)))) |