Step | Hyp | Ref
| Expression |
1 | | breq2 5153 |
. . . . . . . . . . . . 13
โข (๐ = if(๐ โ โค, ๐, 1) โ (๐ < ๐ โ ๐ < if(๐ โ โค, ๐, 1))) |
2 | | oveq2 7417 |
. . . . . . . . . . . . . 14
โข (๐ = if(๐ โ โค, ๐, 1) โ (๐ ยท ๐) = (๐ ยท if(๐ โ โค, ๐, 1))) |
3 | 2 | neeq1d 3001 |
. . . . . . . . . . . . 13
โข (๐ = if(๐ โ โค, ๐, 1) โ ((๐ ยท ๐) โ ๐ โ (๐ ยท if(๐ โ โค, ๐, 1)) โ ๐)) |
4 | 1, 3 | imbi12d 345 |
. . . . . . . . . . . 12
โข (๐ = if(๐ โ โค, ๐, 1) โ ((๐ < ๐ โ (๐ ยท ๐) โ ๐) โ (๐ < if(๐ โ โค, ๐, 1) โ (๐ ยท if(๐ โ โค, ๐, 1)) โ ๐))) |
5 | | breq1 5152 |
. . . . . . . . . . . . 13
โข (๐ = if(๐ โ โ, ๐, 1) โ (๐ < if(๐ โ โค, ๐, 1) โ if(๐ โ โ, ๐, 1) < if(๐ โ โค, ๐, 1))) |
6 | | neeq2 3005 |
. . . . . . . . . . . . 13
โข (๐ = if(๐ โ โ, ๐, 1) โ ((๐ ยท if(๐ โ โค, ๐, 1)) โ ๐ โ (๐ ยท if(๐ โ โค, ๐, 1)) โ if(๐ โ โ, ๐, 1))) |
7 | 5, 6 | imbi12d 345 |
. . . . . . . . . . . 12
โข (๐ = if(๐ โ โ, ๐, 1) โ ((๐ < if(๐ โ โค, ๐, 1) โ (๐ ยท if(๐ โ โค, ๐, 1)) โ ๐) โ (if(๐ โ โ, ๐, 1) < if(๐ โ โค, ๐, 1) โ (๐ ยท if(๐ โ โค, ๐, 1)) โ if(๐ โ โ, ๐, 1)))) |
8 | | oveq1 7416 |
. . . . . . . . . . . . . 14
โข (๐ = if(๐ โ โค, ๐, 1) โ (๐ ยท if(๐ โ โค, ๐, 1)) = (if(๐ โ โค, ๐, 1) ยท if(๐ โ โค, ๐, 1))) |
9 | 8 | neeq1d 3001 |
. . . . . . . . . . . . 13
โข (๐ = if(๐ โ โค, ๐, 1) โ ((๐ ยท if(๐ โ โค, ๐, 1)) โ if(๐ โ โ, ๐, 1) โ (if(๐ โ โค, ๐, 1) ยท if(๐ โ โค, ๐, 1)) โ if(๐ โ โ, ๐, 1))) |
10 | 9 | imbi2d 341 |
. . . . . . . . . . . 12
โข (๐ = if(๐ โ โค, ๐, 1) โ ((if(๐ โ โ, ๐, 1) < if(๐ โ โค, ๐, 1) โ (๐ ยท if(๐ โ โค, ๐, 1)) โ if(๐ โ โ, ๐, 1)) โ (if(๐ โ โ, ๐, 1) < if(๐ โ โค, ๐, 1) โ (if(๐ โ โค, ๐, 1) ยท if(๐ โ โค, ๐, 1)) โ if(๐ โ โ, ๐, 1)))) |
11 | | 1z 12592 |
. . . . . . . . . . . . . 14
โข 1 โ
โค |
12 | 11 | elimel 4598 |
. . . . . . . . . . . . 13
โข if(๐ โ โค, ๐, 1) โ
โค |
13 | | 1nn 12223 |
. . . . . . . . . . . . . 14
โข 1 โ
โ |
14 | 13 | elimel 4598 |
. . . . . . . . . . . . 13
โข if(๐ โ โ, ๐, 1) โ
โ |
15 | 11 | elimel 4598 |
. . . . . . . . . . . . 13
โข if(๐ โ โค, ๐, 1) โ
โค |
16 | 12, 14, 15 | dvdslelem 16252 |
. . . . . . . . . . . 12
โข (if(๐ โ โ, ๐, 1) < if(๐ โ โค, ๐, 1) โ (if(๐ โ โค, ๐, 1) ยท if(๐ โ โค, ๐, 1)) โ if(๐ โ โ, ๐, 1)) |
17 | 4, 7, 10, 16 | dedth3h 4589 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โ โง ๐ โ โค) โ (๐ < ๐ โ (๐ ยท ๐) โ ๐)) |
18 | 17 | 3expia 1122 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โ) โ (๐ โ โค โ (๐ < ๐ โ (๐ ยท ๐) โ ๐))) |
19 | 18 | com23 86 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ (๐ < ๐ โ (๐ โ โค โ (๐ ยท ๐) โ ๐))) |
20 | 19 | 3impia 1118 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ โง ๐ < ๐) โ (๐ โ โค โ (๐ ยท ๐) โ ๐)) |
21 | 20 | imp 408 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โ โง ๐ < ๐) โง ๐ โ โค) โ (๐ ยท ๐) โ ๐) |
22 | 21 | neneqd 2946 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โ โง ๐ < ๐) โง ๐ โ โค) โ ยฌ (๐ ยท ๐) = ๐) |
23 | 22 | nrexdv 3150 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โ โง ๐ < ๐) โ ยฌ โ๐ โ โค (๐ ยท ๐) = ๐) |
24 | | nnz 12579 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โค) |
25 | | divides 16199 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ โ๐ โ โค (๐ ยท ๐) = ๐)) |
26 | 24, 25 | sylan2 594 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โ) โ (๐ โฅ ๐ โ โ๐ โ โค (๐ ยท ๐) = ๐)) |
27 | 26 | 3adant3 1133 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โ โง ๐ < ๐) โ (๐ โฅ ๐ โ โ๐ โ โค (๐ ยท ๐) = ๐)) |
28 | 23, 27 | mtbird 325 |
. . . 4
โข ((๐ โ โค โง ๐ โ โ โง ๐ < ๐) โ ยฌ ๐ โฅ ๐) |
29 | 28 | 3expia 1122 |
. . 3
โข ((๐ โ โค โง ๐ โ โ) โ (๐ < ๐ โ ยฌ ๐ โฅ ๐)) |
30 | 29 | con2d 134 |
. 2
โข ((๐ โ โค โง ๐ โ โ) โ (๐ โฅ ๐ โ ยฌ ๐ < ๐)) |
31 | | zre 12562 |
. . 3
โข (๐ โ โค โ ๐ โ
โ) |
32 | | nnre 12219 |
. . 3
โข (๐ โ โ โ ๐ โ
โ) |
33 | | lenlt 11292 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โค ๐ โ ยฌ ๐ < ๐)) |
34 | 31, 32, 33 | syl2an 597 |
. 2
โข ((๐ โ โค โง ๐ โ โ) โ (๐ โค ๐ โ ยฌ ๐ < ๐)) |
35 | 30, 34 | sylibrd 259 |
1
โข ((๐ โ โค โง ๐ โ โ) โ (๐ โฅ ๐ โ ๐ โค ๐)) |